Progress on completing the trace monad rule set #667
Conversation
|
Should probably start making issues for this, but I think the next step would be to start on a Trace_RG_VCG theory. We could try to lift the existing We probably also want Looking at how equal all those existing proofs are to the nondet-monad it really is a bit of a shame that we can't do monads generically. I'm almost tempted to try some locales with way too general types that have large instantiations. One wouldn't get the definitions from the locales because of the too general types, but one could potentially get a lot of lemmas. They'd probably have large instantiations (all the definitions). Anyway. That one is lower priority -- the RG rules are not going to follow from the locales and those are the ones we really want to have in the end. |
|
This PR now also copies |
corlewis
force-pushed
the
trace_more_rules
branch
from
1532ec6 to
41c4adf
Compare
|
|
||
| text \<open>Useful in forcing otherwise unknown executions to have the @{const empty_fail} property.\<close> | ||
| \<comment> \<open>definition mk_ef :: "'a set \<times> bool \<Rightarrow> 'a set \<times> bool" where | ||
| "mk_ef S \<equiv> (fst S, fst S = {} \<or> snd S)"\<close> |
There was a problem hiding this comment.
Yes, I had commented it out due to it requiring more thought about how to define mk_ef for the trace monad. Thanks for getting me to look at it again though, I came up with a simple idea which while untested for use in proofs at least works for the basic empty_fail_mk_ef lemma.
See d026ada#diff-91fa50fb5dc2c82d728a640bb01749119aefd9da2a65256f460fe8b83c814a8fR24 for the new definition.
| Collect generic empty_fail lemmas here: | ||
| - naming convention is emtpy_fail_NAME. | ||
| - add lemmas with assumptions to [empty_fail_cond] set | ||
| - add lemmas without assumption to [empty_fail_term] set |
There was a problem hiding this comment.
bit off-topic and beyond the scope of this PR, but would it be possible to write attributes that can check you're not putting the wrong thing into one of these sets, or automatically select which set to put it into?
There was a problem hiding this comment.
Ooh, interesting idea. That does feel possible, although I don't have experience with these lemma sets to know how they are used in practice and what the end result would be for us as users.
There was a problem hiding this comment.
It's certainly possible to do, but the attribute(s) would be manually written ML code like [simp] and it would still be hard to prevent the user from just adding theorems to the set directly (without making it much harder to use, at least).
In terms of maintainability trade-off, the simple named-thms sets probably win out, because we don't usually dynamically add new stuff to these sets.
There was a problem hiding this comment.
OK, if it's not going to get dynamically added to the wrong set by some future genius, then it's not worth it. Only wanted to point out that it's possible to programmatically check whether something has assumptions or not before the set add.
|
|
||
| \<comment> \<open>lemma empty_fail_mk_ef[empty_fail_term]: | ||
| "empty_fail (mk_ef o m)" | ||
| by (simp add: empty_fail_def mk_ef_def)\<close> |
There was a problem hiding this comment.
any reason this one's commented out without a FIXME or indication of what to do?
There was a problem hiding this comment.
It is uncommented out now that I have given mk_ef a new definition for the trace monad.
| c \<leftarrow> C; | ||
| whileLoop (\<lambda>c s. c) (\<lambda>_. do B; C od) c; | ||
| return () | ||
| od" |
There was a problem hiding this comment.
not sure about whether this is the PR for it, but these are not the new definition style, the wrapping is (as I was reminded recently):
definition name ::
very_long_type
where
...
56bd415 to
d026ada
Compare
corlewis
force-pushed
the
trace_more_rules
branch
from
d026ada to
7390538
Compare
This fills out the trace monad rule set by copying in as many definitions and rules as possible from the nondet monad. Most of these do not immediately work for the trace monad, see the next commit for the required changes. Signed-off-by: Corey Lewis <[email protected]>
This commit has all of the changes required so that the definitions and rules added in the previous commit work for the trace monad. Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
corlewis
force-pushed
the
trace_more_rules
branch
from
7390538 to
4b55c95
Compare
This fills out the rule set by copying in as many definitions and rules as possible from the nondet monad.
Note, for review purposes the first commit has been separated into two. The first commit currently seen here copies in verbatim from nondet monad and can be ignored. The second commit updates as required for the trace monad and the third is completely new content. Both should be reviewed as normal, although there is quite a bit of crossover between the second commit here and the first commit in #666.