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

lib+refine: strengthen corres_assert_assume_l and move to Lib 

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney 2024-01-09 15:51:44 +10:30 committed by michaelmcinerney
parent 449cfc702e
commit dc62bfdfeb
6 changed files with 5 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
lib/Corres_UL.thy
View File

@ -740,6 +740,11 @@ lemma corres_assert_assume:
by (auto simp: bind_def assert_def fail_def return_def
corres_underlying_def)
lemma corres_assert_assume_l:
"corres_underlying sr nf nf' rrel P Q (f ()) g
\<Longrightarrow> corres_underlying sr nf nf' rrel (P and (\<lambda>s. P')) Q (assert P' >>= f) g"
by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
lemma corres_assert_gen_asm_cross:
"\<lbrakk> \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; Q' s'\<rbrakk> \<Longrightarrow> A;
A \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ()) \<rbrakk>

5
proof/refine/AARCH64/Schedule_R.thy
View File

@ -1575,11 +1575,6 @@ lemma corres_assert_ret:
apply (simp add: assert_def return_def fail_def)
done
lemma corres_assert_assume_l:
"corres dc P Q (f ()) g
\<Longrightarrow> corres dc (P and (\<lambda>s. P')) Q (assert P' >>= f) g"
by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
lemma corres_assert_assume_r:
"corres dc P Q f (g ())
\<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)"

5
proof/refine/ARM/Schedule_R.thy
View File

@ -1454,11 +1454,6 @@ lemma corres_assert_ret:
apply (simp add: assert_def return_def fail_def)
done
lemma corres_assert_assume_l:
"corres dc P Q (f ()) g
\<Longrightarrow> corres dc (P and (\<lambda>s. P')) Q (assert P' >>= f) g"
by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
lemma corres_assert_assume_r:
"corres dc P Q f (g ())
\<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)"

5
proof/refine/ARM_HYP/Schedule_R.thy
View File

@ -1550,11 +1550,6 @@ lemma corres_assert_ret:
apply (simp add: assert_def return_def fail_def)
done
lemma corres_assert_assume_l:
"corres dc P Q (f ()) g
\<Longrightarrow> corres dc (P and (\<lambda>s. P')) Q (assert P' >>= f) g"
by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
lemma corres_assert_assume_r:
"corres dc P Q f (g ())
\<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)"

5
proof/refine/RISCV64/Schedule_R.thy
View File

@ -1419,11 +1419,6 @@ lemma corres_assert_ret:
apply (simp add: assert_def return_def fail_def)
done
lemma corres_assert_assume_l:
"corres dc P Q (f ()) g
\<Longrightarrow> corres dc (P and (\<lambda>s. P')) Q (assert P' >>= f) g"
by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
lemma corres_assert_assume_r:
"corres dc P Q f (g ())
\<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)"

5
proof/refine/X64/Schedule_R.thy
View File

@ -1418,11 +1418,6 @@ lemma corres_assert_ret:
apply (simp add: assert_def return_def fail_def)
done
lemma corres_assert_assume_l:
"corres dc P Q (f ()) g
\<Longrightarrow> corres dc (P and (\<lambda>s. P')) Q (assert P' >>= f) g"
by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
lemma corres_assert_assume_r:
"corres dc P Q f (g ())
\<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)"