Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Rules for Lib #704

Merged
merged 21 commits into from
Jan 15, 2024
Merged
Changes from 1 commit
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
e4ec9f3
lib+refine: strengthen corres_assert_assume_l and move to Lib
michaelmcinerney Jan 9, 2024
ca3624e
lib: add corres_if_strong
michaelmcinerney Jan 9, 2024
45ece43
lib: add some rules involving ex_abs_underlying, including corres_fro…
michaelmcinerney Jan 9, 2024
48f8ea7
lib: strengthen no_ofail_gets_the
michaelmcinerney Jan 9, 2024
d13c538
lib: add monadic_rewrite_guard_arg_cong
michaelmcinerney Jan 9, 2024
0078984
lib: generalise monadic_rewrite_is_valid
michaelmcinerney Jan 9, 2024
25968fd
lib: add monadic_rewrite_corres_r_generic_ex_abs
michaelmcinerney Jan 9, 2024
962d097
lib: add ifM_to_top_of_bind
michaelmcinerney Jan 9, 2024
f2b047f
lib: add ifM_corres' and orM_corres'
michaelmcinerney Jan 9, 2024
4edbe22
lib: reorder assumptions of no_fail_bind
michaelmcinerney Jan 9, 2024
04e7eea
lib: modify no_ofail_obind and no_ofail_pre_imp
michaelmcinerney Jan 9, 2024
943ab13
lib: add ovalid_post_taut
michaelmcinerney Jan 9, 2024
82abdf8
lib: add no_ofail_if
michaelmcinerney Jan 9, 2024
c486058
lib: add defn of list_insert_before, and some lemmas
michaelmcinerney Jan 10, 2024
fd6656c
lib: add Heap_List.thy, for reasoning about linked lists on heaps
michaelmcinerney Jan 10, 2024
0f5987a
lib: heap_ls lemmas relating an update to the list to an update to th…
michaelmcinerney Jan 10, 2024
b2962e9
lib: add heap_path_sym_heap_non_nil_lookup_prev
michaelmcinerney Jan 9, 2024
d04daa5
lib: add fun_upd_swap
michaelmcinerney Jan 9, 2024
d588c6c
lib: several miscellaneous lemmas for heap_ls
michaelmcinerney Jan 9, 2024
1991f59
lib: add "no loops" lemmas for heap_ls
michaelmcinerney Jan 9, 2024
58d5752
lib: some sym_heap lemmas regarding heap updates
michaelmcinerney Jan 9, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
lib+refine: strengthen corres_assert_assume_l and move to Lib
Signed-off-by: Michael McInerney <[email protected]>
  • Loading branch information
michaelmcinerney committed Jan 15, 2024
commit e4ec9f319d997c4a393da5fbda8a248058f84749
5 changes: 5 additions & 0 deletions lib/Corres_UL.thy
Original file line number Diff line number Diff line change
@@ -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"
lsf37 marked this conversation as resolved.
Show resolved Hide resolved
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 changes: 0 additions & 5 deletions proof/refine/AARCH64/Schedule_R.thy
Original file line number Diff line number Diff line change
@@ -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 changes: 0 additions & 5 deletions proof/refine/ARM/Schedule_R.thy
Original file line number Diff line number Diff line change
@@ -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 changes: 0 additions & 5 deletions proof/refine/ARM_HYP/Schedule_R.thy
Original file line number Diff line number Diff line change
@@ -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 changes: 0 additions & 5 deletions proof/refine/RISCV64/Schedule_R.thy
Original file line number Diff line number Diff line change
@@ -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 changes: 0 additions & 5 deletions proof/refine/X64/Schedule_R.thy
Original file line number Diff line number Diff line change
@@ -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)"