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

lib: add monadic_rewrite_corres_r_generic_ex_abs 

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney 2024-01-09 18:21:47 +10:30 committed by Achim D. Brucker
parent e508d15554
commit e160e257a0
1 changed files with 8 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
lib/MonadicRewrite.thy
View File

@ -10,7 +10,7 @@
theory MonadicRewrite
imports
Monads.Nondet_VCG
Corres_UL
ExtraCorres
Monads.Nondet_Empty_Fail
Rules_Tac
begin
@ -744,6 +744,13 @@ lemma monadic_rewrite_corres_r_generic:
\<Longrightarrow> corres_underlying R nf nf' r P (P' and Q) a c"
by (fastforce simp: corres_underlying_def monadic_rewrite_def)
lemma monadic_rewrite_corres_r_generic_ex_abs:
"\<lbrakk> monadic_rewrite F E (\<lambda>s'. Q s' \<and> ex_abs_underlying sr P s') c' c;
corres_underlying sr nf nf'' r P P' a c';
F \<longrightarrow> nf''; nf' \<longrightarrow> nf'' \<rbrakk>
\<Longrightarrow> corres_underlying sr nf nf' r P (P' and Q) a c"
by (fastforce simp: corres_underlying_def monadic_rewrite_def)
lemma monadic_rewrite_corres_r:
"\<lbrakk> monadic_rewrite False True Q c c';
corres_underlying R nf nf' r P P' a c' \<rbrakk>