1 files changed, 113 insertions, 2 deletions

diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index 124722ab..ba69d0d8 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -23,6 +23,14 @@ lemma Value_liftState_Run:
 
 lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra]
 
+lemma Value_bindS_iff:
+  "(Value b, s'') \<in> bindS m f s \<longleftrightarrow> (\<exists>a s'. (Value a, s') \<in> m s \<and> (Value b, s'') \<in> f a s')"
+  by (auto elim!: bindS_cases intro: bindS_intros)
+
+lemma Ex_bindS_iff:
+  "(Ex e, s'') \<in> bindS m f s \<longleftrightarrow> (Ex e, s'') \<in> m s \<or> (\<exists>a s'. (Value a, s') \<in> m s \<and> (Ex e, s'') \<in> f a s')"
+  by (auto elim!: bindS_cases intro: bindS_intros)
+
 lemma liftState_throw[liftState_simp]: "liftState r (throw e) = throwS e"
   by (auto simp: throw_def)
 lemma liftState_assert[liftState_simp]: "liftState r (assert_exp c msg) = assert_expS c msg"
@@ -51,7 +59,7 @@ lemma liftState_try_catch[liftState_simp]:
   by (induction m h rule: try_catch_induct) (auto simp: try_catchS_bindS_no_throw)
 
 lemma liftState_early_return[liftState_simp]:
-  "liftState r (early_return r) = early_returnS r"
+  "liftState r (early_return x) = early_returnS x"
   by (auto simp: early_return_def early_returnS_def liftState_simp)
 
 lemma liftState_catch_early_return[liftState_simp]:
@@ -66,6 +74,10 @@ lemma liftState_try_catchR[liftState_simp]:
   "liftState r (try_catchR m h) = try_catchRS (liftState r m) (liftState r \<circ> h)"
   by (auto simp: try_catchR_def try_catchRS_def sum.case_distrib liftState_simp cong: sum.case_cong)
 
+lemma liftState_bool_of_bitU_nondet[liftState_simp]:
+  "liftState r (bool_of_bitU_nondet b) = bool_of_bitU_nondetS b"
+  by (cases b; auto simp: bool_of_bitU_nondet_def bool_of_bitU_nondetS_def liftState_simp)
+
 lemma liftState_read_mem_BC:
   assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
   shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz"
@@ -87,7 +99,7 @@ lemma liftState_write_mem_ea[liftState_simp]:
   "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = write_mem_eaS BC_bitU_list rk a (nat sz)"
   by (auto simp: liftState_write_mem_ea_BC)
 
-lemma liftState_write_mem_val:
+lemma liftState_write_mem_val[liftState_simp]:
   "liftState r (write_mem_val BC v) = write_mem_valS BC v"
   by (auto simp: write_mem_val_def write_mem_valS_def liftState_simp split: option.splits)
 
@@ -126,6 +138,80 @@ lemma liftState_foreachM[liftState_simp]:
   by (induction xs vars "\<lambda>x vars. liftState r (body x vars)" rule: foreachS.induct)
      (auto simp: liftState_simp cong: bindS_cong)
 
+lemma liftState_bools_of_bits_nondet[liftState_simp]:
+  "liftState r (bools_of_bits_nondet bs) = bools_of_bits_nondetS bs"
+  unfolding bools_of_bits_nondet_def bools_of_bits_nondetS_def
+  by (auto simp: liftState_simp comp_def)
+
+lemma liftState_internal_pick[liftState_simp]:
+  "liftState r (internal_pick xs) = internal_pickS xs"
+  by (auto simp: internal_pick_def internal_pickS_def liftState_simp comp_def
+                 option.case_distrib[where h = "liftState r"]
+           simp del: repeat.simps
+           cong: option.case_cong)
+
+lemma liftRS_returnS[simp]: "liftRS (returnS x) = returnS x"
+  by (auto simp: liftRS_def)
+
+lemma liftRS_bindS:
+  fixes m :: "('regs, 'a, 'e) monadS" and f :: "'a \<Rightarrow> ('regs, 'b, 'e) monadS"
+  shows "(liftRS (bindS m f) :: ('regs, 'b, 'r, 'e) monadRS) = bindS (liftRS m) (liftRS \<circ> f)"
+proof (intro ext set_eqI iffI)
+  fix s and rs' :: "('b, 'r + 'e) result \<times> 'regs sequential_state"
+  assume lhs: "rs' \<in> liftRS (bindS m f) s"
+  then show "rs' \<in> bindS (liftRS m) (liftRS \<circ> f) s"
+    by (cases rs')
+       (fastforce simp: liftRS_def throwS_def elim!: bindS_cases try_catchS_cases
+                  intro: bindS_intros try_catchS_intros)
+next
+  fix s and rs' :: "('b, 'r + 'e) result \<times> 'regs sequential_state"
+  assume "rs' \<in> bindS (liftRS m) (liftRS \<circ> f) s"
+  then show "rs' \<in> liftRS (bindS m f) s"
+    by (cases rs')
+       (fastforce simp: liftRS_def throwS_def elim!: bindS_cases try_catchS_cases
+                  intro: bindS_intros try_catchS_intros)
+qed
+
+lemma liftRS_assert_expS_True[simp]: "liftRS (assert_expS True msg) = returnS ()"
+  by (auto simp: liftRS_def assert_expS_def)
+
+lemma untilM_domI:
+  fixes V :: "'vars \<Rightarrow> nat"
+  assumes "Inv vars"
+    and "\<And>vars t vars' t'. \<lbrakk>Inv vars; Run (body vars) t vars'; Run (cond vars') t' False\<rbrakk> \<Longrightarrow> V vars' < V vars \<and> Inv vars'"
+  shows "untilM_dom (vars, cond, body)"
+  using assms
+  by (induction vars rule: measure_induct_rule[where f = V])
+     (auto intro: untilM.domintros)
+
+lemma untilM_dom_untilS_dom:
+  assumes "untilM_dom (vars, cond, body)"
+  shows "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)"
+  using assms
+  by (induction vars cond body arbitrary: s rule: untilM.pinduct)
+     (rule untilS.domintros, auto elim!: Value_liftState_Run)
+
+lemma measure2_induct:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> nat"
+  assumes "\<And>x1 y1. (\<And>x2 y2. f x2 y2 < f x1 y1 \<Longrightarrow> P x2 y2) \<Longrightarrow> P x1 y1"
+  shows "P x y"
+proof -
+  have "P (fst x) (snd x)" for x
+    by (induction x rule: measure_induct_rule[where f = "\<lambda>x. f (fst x) (snd x)"]) (auto intro: assms)
+  then show ?thesis by auto
+qed
+
+lemma untilS_domI:
+  fixes V :: "'vars \<Rightarrow> 'regs sequential_state \<Rightarrow> nat"
+  assumes "Inv vars s"
+    and "\<And>vars s vars' s' s''.
+           \<lbrakk>Inv vars s; (Value vars', s') \<in> body vars s; (Value False, s'') \<in> cond vars' s'\<rbrakk>
+            \<Longrightarrow> V vars' s'' < V vars s \<and> Inv vars' s''"
+  shows "untilS_dom (vars, cond, body, s)"
+  using assms
+  by (induction vars s rule: measure2_induct[where f = V])
+     (auto intro: untilS.domintros)
+
 lemma whileS_dom_step:
   assumes "whileS_dom (vars, cond, body, s)"
     and "(Value True, s') \<in> cond vars s"
@@ -230,6 +316,9 @@ lemma and_boolM_return_if:
   "and_boolM (return b) y = (if b then y else return False)"
   by (auto simp: and_boolM_def)
 
+lemma and_boolM_return_return_and[simp]: "and_boolM (return l) (return r) = return (l \<and> r)"
+  by (auto simp: and_boolM_def)
+
 lemmas and_boolM_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolM x y" for y]
 
 lemma or_boolM_simps[simp]:
@@ -243,6 +332,9 @@ lemma or_boolM_return_if:
   "or_boolM (return b) y = (if b then return True else y)"
   by (auto simp: or_boolM_def)
 
+lemma or_boolM_return_return_or[simp]: "or_boolM (return l) (return r) = return (l \<or> r)"
+  by (auto simp: or_boolM_def)
+
 lemmas or_boolM_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolM x y" for y]
 
 lemma if_returnS_returnS[simp]: "(if a then returnS True else returnS False) = returnS a" by auto
@@ -260,8 +352,12 @@ lemma and_boolS_returnS_if:
 
 lemmas and_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolS x y" for y]
 
+lemma and_boolS_returnS_True[simp]: "and_boolS (returnS True) c = c"
+  by (auto simp: and_boolS_def)
+
 lemma or_boolS_simps[simp]:
   "or_boolS (returnS b) (returnS c) = returnS (b \<or> c)"
+  "or_boolS (returnS False) m = m"
   "or_boolS x (returnS True) = bindS x (\<lambda>_. returnS True)"
   "or_boolS x (returnS False) = x"
   "\<And>x y z. or_boolS (bindS x y) z = (bindS x (\<lambda>r. or_boolS (y r) z))"
@@ -273,4 +369,19 @@ lemma or_boolS_returnS_if:
 
 lemmas or_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolS x y" for y]
 
+lemma Run_or_boolM_E:
+  assumes "Run (or_boolM l r) t a"
+  obtains "Run l t True" and "a"
+  | tl tr where "Run l tl False" and "Run r tr a" and "t = tl @ tr"
+  using assms by (auto simp: or_boolM_def elim!: Run_bindE Run_ifE Run_returnE)
+
+lemma Run_and_boolM_E:
+  assumes "Run (and_boolM l r) t a"
+  obtains "Run l t False" and "\<not>a"
+  | tl tr where "Run l tl True" and "Run r tr a" and "t = tl @ tr"
+  using assms by (auto simp: and_boolM_def elim!: Run_bindE Run_ifE Run_returnE)
+
+lemma maybe_failS_Some[simp]: "maybe_failS msg (Some v) = returnS v"
+  by (auto simp: maybe_failS_def)
+
 end