Monads: refactor reader_option and nondet connection

[corlewis]

My overall aim with these changes is to make it possible to use the reader_option monad with the trace monad, in the same way that it can currently be used with the nondet monad.

Without these changes, the reader_option files Reader_Option_ND.thy and Reader_Option_VCG.thy depend on nondet files, and prove various lemmas connecting reader_option concepts with nondet concepts. As an example,

lemma ovalid_gets_the:
  "ovalid P f Q ⟹ ⦃P⦄ gets_the f ⦃Q⦄"

shows that the nondet concept of validity of gets_the f can be derived from the reader_option concept of validity. Most of these lemmas were in Reader_Option_ND.thy, which was described by a comment as

(* Reader option monad syntax plus the connection between the reader option monad and the nondet monad *)

What I've done in the first commit is to basically reverse the dependency: the reader_option directory now only contains definitions and lemmas for the reader_option monad and there's a file in nondet that has the lemmas connecting the two monads. The third commit then adds a file in trace that is basically the same thing but for the trace monad.

I am very open to suggestions if anyone has an idea for a nicer way to structure this or to reduce the copied content. I had a brief attempt at a locale but couldn't find a way to get it to work that didn't involve even more copying.

[Xaphiosis]

Could you explain what you're trying to do? I'm seeing some theory files renamed and some proofs moved, and the commits refer to "reader_option and nondet connection" without any further description. I'm guessing you're doing something you then need for integration with the trace monad, but I'm really lost as to the intent. What do you mean by connection?

[corlewis]

Could you explain what you're trying to do? I'm seeing some theory files renamed and some proofs moved, and the commits refer to "reader_option and nondet connection" without any further description. I'm guessing you're doing something you then need for integration with the trace monad, but I'm really lost as to the intent. What do you mean by connection?

My overall aim with these changes is to make it possible to use the reader_option monad with the trace monad, in the same way that it can currently be used with the nondet monad.

Without these changes, the reader_option files Reader_Option_ND.thy and Reader_Option_VCG.thy depend on nondet files, and prove various lemmas connecting reader_option concepts with nondet concepts. As an example,

lemma ovalid_gets_the:
  "ovalid P f Q ⟹ ⦃P⦄ gets_the f ⦃Q⦄"

shows that the nondet concept of validity of gets_the f can be derived from the reader_option concept of validity. Most of these lemmas were in Reader_Option_ND.thy, which was described by a comment as

(* Reader option monad syntax plus the connection between the reader option monad and the nondet monad *)

What I've done in the first commit is to basically reverse the dependency: the reader_option directory now only contains definitions and lemmas for the reader_option monad and there's a file in nondet that has the lemmas connecting the two monads. The third commit then adds a file in trace that is basically the same thing but for the trace monad.

[Xaphiosis]

That's a very good explanation! Any chance some of it could make it to the commits? I had no idea until you explained it

[corlewis]

That's a very good explanation! Any chance some of it could make it to the commits? I had no idea until you explained it

Done, do those commit descriptions make sense to you?

I also rebased and updated copyrights, which I had forgotten to do.

[lsf37]

👍 This works for me with the updated commit messages. You might still foreshadow in the first msg why you're doing that refactor (so that you can produce the same setup later for the trace monad).

[michaelmcinerney]

I wish I knew more about the trace monad stuff to comment on that, but this looks like a very good thing to do!

[Xaphiosis]

That's a very good explanation! Any chance some of it could make it to the commits? I had no idea until you explained it

Done, do those commit descriptions make sense to you?

I also rebased and updated copyrights, which I had forgotten to do.

Thanks! What Gerwin said. Also, two commits have "reader_option" but one has "reader option".

[corlewis]

Commit messages updated, rebased over #725, and I realised that I had left a lemma collection in the nondet and trace files that was just about reader_option concepts and moved it.