3 files changed, 93 insertions, 0 deletions
diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy
index ee7a5fa6..a6c2ee3d 100644
--- a/lib/isabelle/Hoare.thy
+++ b/lib/isabelle/Hoare.thy
@@ -130,6 +130,36 @@ lemma PrePost_let[intro, PrePost_intro]:
   shows "PrePost P (let x = y in m x) Q"
   using assms by auto
 
+lemma PrePost_and_boolS[PrePost_intro]:
+  assumes r: "PrePost R r Q"
+    and l: "PrePost P l (\<lambda>r. case r of Value True \<Rightarrow> R | _ \<Rightarrow> Q r)"
+  shows "PrePost P (and_boolS l r) Q"
+  unfolding and_boolS_def
+proof (rule PrePost_bindS)
+  fix s a s'
+  assume "(Value a, s') \<in> l s"
+  show "PrePost (if a then R else Q (Value False)) (if a then r else returnS False) Q"
+    using r by auto
+next
+  show "PrePost P l (\<lambda>r. case r of Value a \<Rightarrow> if a then R else Q (Value False) | Ex e \<Rightarrow> Q (Ex e))"
+    using l by (elim PrePost_weaken_post) (auto split: result.splits)
+qed
+
+lemma PrePost_or_boolS[PrePost_intro]:
+  assumes r: "PrePost R r Q"
+    and l: "PrePost P l (\<lambda>r. case r of Value False \<Rightarrow> R | _ \<Rightarrow> Q r)"
+  shows "PrePost P (or_boolS l r) Q"
+  unfolding or_boolS_def
+proof (rule PrePost_bindS)
+  fix s a s'
+  assume "(Value a, s') \<in> l s"
+  show "PrePost (if a then Q (Value True) else R) (if a then returnS True else r) Q"
+    using r by auto
+next
+  show "PrePost P l (\<lambda>r. case r of Value a \<Rightarrow> if a then Q (Value True) else R | Ex e \<Rightarrow> Q (Ex e))"
+    using l by (elim PrePost_weaken_post) (auto split: result.splits)
+qed
+
 lemma PrePost_assert_expS[intro, PrePost_intro]: "PrePost (if c then P (Value ()) else P (Ex (Failure m))) (assert_expS c m) P"
   unfolding PrePost_def assert_expS_def by (auto simp: returnS_def failS_def)
 
@@ -293,6 +323,20 @@ lemma PrePostE_let[PrePostE_intro]:
   shows "PrePostE P (let x = y in m x) Q E"
   using assms by auto
 
+lemma PrePostE_and_boolS[PrePostE_intro]:
+  assumes r: "PrePostE R r Q E"
+    and l: "PrePostE P l (\<lambda>r. if r then R else Q False) E"
+  shows "PrePostE P (and_boolS l r) Q E"
+  using assms unfolding PrePostE_def
+  by (intro PrePost_and_boolS) (auto elim: PrePost_weaken_post split: if_splits result.splits)
+
+lemma PrePostE_or_boolS[PrePostE_intro]:
+  assumes r: "PrePostE R r Q E"
+    and l: "PrePostE P l (\<lambda>r. if r then Q True else R) E"
+  shows "PrePostE P (or_boolS l r) Q E"
+  using assms unfolding PrePostE_def
+  by (intro PrePost_or_boolS) (auto elim: PrePost_weaken_post split: if_splits result.splits)
+
 lemma PrePostE_assert_expS[PrePostE_intro, intro]:
   "PrePostE (if c then P () else Q (Failure m)) (assert_expS c m) P Q"
   unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre)
diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy
index e883c2a0..7a3a108d 100644
--- a/lib/isabelle/Prompt_monad_lemmas.thy
+++ b/lib/isabelle/Prompt_monad_lemmas.thy
@@ -17,6 +17,7 @@ lemmas bind_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_e
 
 lemma bind_return[simp]: "bind (return a) f = f a"
   by (auto simp: return_def)
+lemma bind_return_right[simp]: "bind x return = x" by (induction x) (auto simp: return_def)
 
 lemma bind_assoc[simp]: "bind (bind m f) g = bind m (\<lambda>x. bind (f x) g)"
   by (induction m f arbitrary: g rule: bind.induct) auto
diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy
index 253c21b9..f7c171a8 100644
--- a/lib/isabelle/State_lemmas.thy
+++ b/lib/isabelle/State_lemmas.thy
@@ -30,6 +30,12 @@ lemma liftState_footprint[simp]: "liftState r (footprint ()) = returnS ()" by (a
 lemma liftState_undefined[simp]: "liftState r (undefined_bool ()) = undefined_boolS ()" by (auto simp: undefined_bool_def)
 lemma liftState_maybe_fail[simp]: "liftState r (maybe_fail msg x) = maybe_failS msg x"
   by (auto simp: maybe_fail_def maybe_failS_def split: option.splits)
+lemma liftState_and_boolM[simp]:
+  "liftState r (and_boolM x y) = and_boolS (liftState r x) (liftState r y)"
+  by (auto simp: and_boolM_def and_boolS_def cong: bindS_cong if_cong)
+lemma liftState_or_boolM[simp]:
+  "liftState r (or_boolM x y) = or_boolS (liftState r x) (liftState r y)"
+  by (auto simp: or_boolM_def or_boolS_def cong: bindS_cong if_cong)
 
 lemma liftState_try_catch[simp]:
   "liftState r (try_catch m h) = try_catchS (liftState r m) (liftState r \<circ> h)"
@@ -199,4 +205,46 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState
   qed auto
 qed
 
+(* Simplification rules for monadic Boolean connectives *)
+
+lemma if_return_return[simp]: "(if a then return True else return False) = return a" by auto
+
+lemma and_boolM_simps[simp]:
+  "and_boolM (return b) y = (if b then y else return False)"
+  "and_boolM x (return True) = x"
+  "and_boolM x (return False) = x \<bind> (\<lambda>_. return False)"
+  "\<And>x y z. and_boolM (x \<bind> y) z = (x \<bind> (\<lambda>r. and_boolM (y r) z))"
+  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]:
+  "or_boolM (return b) y = (if b then return True else y)"
+  "or_boolM x (return True) = x \<bind> (\<lambda>_. return True)"
+  "or_boolM x (return False) = x"
+  "\<And>x y z. or_boolM (x \<bind> y) z = (x \<bind> (\<lambda>r. or_boolM (y r) z))"
+  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
+
+lemma and_boolS_simps[simp]:
+  "and_boolS (returnS b) y = (if b then y else returnS False)"
+  "and_boolS x (returnS True) = x"
+  "and_boolS x (returnS False) = bindS x (\<lambda>_. returnS False)"
+  "\<And>x y z. and_boolS (bindS x y) z = (bindS x (\<lambda>r. and_boolS (y r) z))"
+  by (auto simp: and_boolS_def)
+
+lemmas and_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolS x y" for y]
+
+lemma or_boolS_simps[simp]:
+  "or_boolS (returnS b) y = (if b then returnS True else y)"
+  "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))"
+  by (auto simp: or_boolS_def)
+
+lemmas or_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolS x y" for y]
+
 end