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

lib: enforce simp (no_asm) in Corres_Method 

The subst_all rule in the standard simp set can circumvent the (no_asm)
mode of simp, which we are using in the corres method.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-06-30 19:00:37 +10:00
parent 1482841847
commit 51ebfd6ebe
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/Corres_Method.thy
View File

@ -161,6 +161,10 @@ method corres
section \<open>Corres rule setup\<close>
(* Avoid using equations in the assumptions. subst_all gets around (no_asm_use) in some cases,
which we don't want. *)
lemmas [corres_no_simp] = subst_all
lemmas [corres_splits] =
corres_split
corres_splitEE