adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib: on the use of corres_liftM_simp rules 

Explain that these are not nice simp rules, what one should do instead,
and why we leave them as is despite all that.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-08-30 16:06:53 +02:00
parent 7595c02d49
commit f80d7f8b37
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
lib/Corres_UL.thy
View File

@ -472,6 +472,13 @@ lemma corres_if3:
text \<open>Some equivalences about liftM and other useful simps\<close>
(* These rules are declared [simp], which in hindsight was not a good decision, because they
change the return relation which often is schematic when these rules apply in the goal.
In those circumstances it is usually safer to unfold liftM_def and proceed with the resulting
substituted term.
(We leave the [simp] attribute here, because too many proofs now depend on it)
*)
lemma corres_liftM_simp[simp]:
"corres_underlying sr nf nf' r P P' (liftM t f) g =
corres_underlying sr nf nf' (r \<circ> t) P P' f g"