Yet more rules for Lib
#737
Conversation
|
Looks like there are still a few proof failures in the Orhpanage session. Probably missing a |
michaelmcinerney
force-pushed
the
michaelm-rules_for_Lib_Mar24
branch
from
e846569
to
91cce0c
Compare
|
Sorry to force push - I didn't realise that reviews had begun. The changes I made were just to the |
michaelmcinerney
force-pushed
the
michaelm-rules_for_Lib_Mar24
branch
from
91cce0c
to
d593972
Compare
lib/Corres_UL.thy
Outdated
| @@ -1176,6 +1176,18 @@ lemma corres_move_asm: | |||
|
|
|||
| lemmas corres_cross_over_guard = corres_move_asm[rotated] | |||
|
|
|||
| lemma corres_cross_add_guard: | |||
| "\<lbrakk> \<And>s s'. \<lbrakk>(s,s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> Q s'; | |||
| corres_underlying sr nf nf' r P (P' and Q) f g\<rbrakk> | |||
There was a problem hiding this comment.
extra space before (P', also wouldn't Q' make more sense than Q given it's on the concrete side?
There was a problem hiding this comment.
Yes it would make much more sense to use Q'. This is another rule copied straight over from the rt branch. Should I change it here? If I do change it for master, should I change it on the rt branch too? That would be quite annoying, because there would be many rules which do write where Q=blah
There was a problem hiding this comment.
Do we use corres_cross_add_guard that often? Or are you saying there are other rules which also followed the Q scheme for the concrete side?
There was a problem hiding this comment.
corres_cross_add_guard is used dozens and dozens of times on the rt branch. It wouldn't be horrible to change, but it would be a bit of a nuisance
There was a problem hiding this comment.
If it's only corres_cross_add_guard I'd vote for updating it and its uses, but if other lemmas follow the same scheme, I'd say defer to another round.
There was a problem hiding this comment.
OK I will update it on both branches
lib/Corres_UL.thy
Outdated
| lemma corres_cross_add_abs_guard: | ||
| "\<lbrakk> \<And>s s'. \<lbrakk>(s,s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> Q s; | ||
| corres_underlying sr nf nf' r (P and Q) P' f g\<rbrakk> | ||
| \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" |
There was a problem hiding this comment.
ah, I only now noticed this, shouldn't the ⟹ align with the ⟦? (on lemma above as well)
There was a problem hiding this comment.
There are quite a few lemmas in this theory file with this same problem. Should I fix up just this one, or all of them?
There was a problem hiding this comment.
Well, I can at least fix it in the lemmas I've introduced in this PR. But the one above is old and wrong, and there are other instances of this elsewhere
There was a problem hiding this comment.
For this round, I'd stick to the ones you're adding, but we'd welcome a future PR that consolidates the others.
michaelmcinerney
force-pushed
the
michaelm-rules_for_Lib_Mar24
branch
from
e59522c
to
8b9ae6d
Compare
michaelmcinerney
force-pushed
the
michaelm-rules_for_Lib_Mar24
branch
from
8b9ae6d
to
c3c32e7
Compare
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]> reindent corres_cross_add_guard and friend squash Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
michaelmcinerney
force-pushed
the
michaelm-rules_for_Lib_Mar24
branch
from
c3c32e7
to
e1da66e
Compare
|
Too late now, but one of the commit messages has an extra: |
No description provided.