kings-crown/FVELER_Isabelle huggingface dataset:
theory Rights_AI

lemma validate_vm_rights_inter:
  "validate_vm_rights (validate_vm_rights fun \<inter> msk) =
   validate_vm_rights (fun \<inter> msk)" by (simp add: validate_vm_rights_def vm_read_write_def vm_read_only_def
                vm_kernel_only_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. validate_vm_rights (validate_vm_rights fun \<inter> msk) = validate_vm_rights (fun \<inter> msk)
theory Rights_AI

lemma validate_vm_rights_eq[simp]:
  "rs \<in> valid_vm_rights \<Longrightarrow> validate_vm_rights rs = rs" by (auto simp add: validate_vm_rights_def valid_vm_rights_def
                     vm_read_write_def vm_read_only_def vm_kernel_only_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rs \<in> valid_vm_rights \<Longrightarrow> validate_vm_rights rs = rs
theory MonadicRewrite

lemma monadic_rewrite_inst:
  "monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F E P f g" by assumption

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F E P f g
theory MonadicRewrite

lemma monadic_rewrite_refl_generic:
  "monadic_rewrite F E P f f" by (simp add: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P f f
theory MonadicRewrite

lemma monadic_rewrite_sym:
  "monadic_rewrite False True P f g \<Longrightarrow> monadic_rewrite False True P g f" by (simp add: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False True P f g \<Longrightarrow> monadic_rewrite False True P g f
theory MonadicRewrite

lemma monadic_rewrite_impossible:
  "monadic_rewrite F E \<bottom> f g" by (clarsimp simp: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (\<lambda>_. False) f g
theory MonadicRewrite

lemma monadic_rewrite_guard_imp:
  "\<lbrakk> monadic_rewrite F E Q f g; \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> monadic_rewrite F E P f g" by (auto simp add: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E Q f g; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> monadic_rewrite F E P f g
theory MonadicRewrite

lemma monadic_rewrite_trans:
  "\<lbrakk> monadic_rewrite F E P f g; monadic_rewrite F E Q g h \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E (P and Q) f h" by (auto simp add: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P f g; monadic_rewrite F E Q g h\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and Q) f h
theory MonadicRewrite

lemma monadic_rewrite_trans_dup:
  "\<lbrakk> monadic_rewrite F E P f g; monadic_rewrite F E P g h \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E P f h" by (rule monadic_rewrite_guard_imp, (rule monadic_rewrite_trans; assumption), simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P f g; monadic_rewrite F E P g h\<rbrakk> \<Longrightarrow> monadic_rewrite F E P f h
theory MonadicRewrite

lemma monadic_rewrite_from_simple:
  "P \<longrightarrow> f = g \<Longrightarrow> monadic_rewrite F E (\<lambda>_. P) f g" by (simp add: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<longrightarrow> f = g \<Longrightarrow> monadic_rewrite F E (\<lambda>_. P) f g
theory MonadicRewrite

lemma monadic_rewrite_gen_asm:
  "\<lbrakk> P \<Longrightarrow> monadic_rewrite F E Q f g \<rbrakk> \<Longrightarrow> monadic_rewrite F E ((\<lambda>_. P) and Q) f g" by (auto simp add: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> monadic_rewrite F E Q f g) \<Longrightarrow> monadic_rewrite F E ((\<lambda>_. P) and Q) f g
theory MonadicRewrite

lemma monadic_rewrite_name_pre:
  "\<lbrakk> \<And>s. P s \<Longrightarrow> monadic_rewrite F E ((=) s) f g \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E P f g" by (auto simp add: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> monadic_rewrite F E ((=) s) f g) \<Longrightarrow> monadic_rewrite F E P f g
theory MonadicRewrite

lemma monadic_rewrite_cases:
  "\<lbrakk> P \<Longrightarrow> monadic_rewrite F E Q a b; \<not> P \<Longrightarrow> monadic_rewrite F E R a b \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) a b" by (cases P, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> monadic_rewrite F E Q a b; \<not> P \<Longrightarrow> monadic_rewrite F E R a b\<rbrakk> \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) a b
theory MonadicRewrite

lemma monadic_rewrite_is_refl:
  "x = y \<Longrightarrow> monadic_rewrite F E \<top> x y" by (simp add: monadic_rewrite_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = y \<Longrightarrow> monadic_rewrite F E (\<lambda>_. True) x y
theory MonadicRewrite

lemma monadic_rewrite_guard_arg_cong:
  "(\<And>s. P s \<Longrightarrow> x = y) \<Longrightarrow> monadic_rewrite F E P (f x) (f y)" by (clarsimp simp: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> x = y) \<Longrightarrow> monadic_rewrite F E P (f x) (f y)
theory MonadicRewrite

lemma monadic_rewrite_exists:
  "(\<And>v. monadic_rewrite F E (Q v) m m')
   \<Longrightarrow> monadic_rewrite F E ((\<lambda>s. \<forall>v. P v s \<longrightarrow> Q v s) and (\<lambda>s. \<exists>v. P v s)) m m'" by (auto simp: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>v. monadic_rewrite F E (Q v) m m') \<Longrightarrow> monadic_rewrite F E ((\<lambda>s. \<forall>v. P v s \<longrightarrow> Q v s) and (\<lambda>s. \<exists>v. P v s)) m m'
theory MonadicRewrite

lemma monadic_rewrite_exists_v:
  "\<lbrakk> \<And>v. monadic_rewrite E F (Q v) f g \<rbrakk>
   \<Longrightarrow> monadic_rewrite E F (\<lambda>x. (\<exists>v. P v x) & (\<forall>v. P v x \<longrightarrow> Q v x)) f g" by (rule monadic_rewrite_name_pre)
     (fastforce elim: monadic_rewrite_guard_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>v. monadic_rewrite E F (Q v) f g) \<Longrightarrow> monadic_rewrite E F (\<lambda>x. (\<exists>v. P v x) \<and> (\<forall>v. P v x \<longrightarrow> Q v x)) f g
theory MonadicRewrite

lemma monadic_rewrite_weaken_flags:
  "monadic_rewrite (F \<and> F') (E \<or> E') P f g
   \<Longrightarrow> monadic_rewrite F' E' P f g" by (auto simp: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite (F \<and> F') (E \<or> E') P f g \<Longrightarrow> monadic_rewrite F' E' P f g
theory MonadicRewrite

lemma monadic_rewrite_weaken_flags':
  "monadic_rewrite F E P f g
   \<Longrightarrow> monadic_rewrite F' E' ((\<lambda>_. (F \<longrightarrow> F') \<and> (E' \<longrightarrow> E)) and P) f g" apply (rule monadic_rewrite_gen_asm) apply (rule monadic_rewrite_weaken_flags[where F=F and E=E]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F' E' ((\<lambda>_. (F \<longrightarrow> F') \<and> (E' \<longrightarrow> E)) and P) f g proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P f g; (F \<longrightarrow> F') \<and> (E' \<longrightarrow> E)\<rbrakk> \<Longrightarrow> monadic_rewrite F' E' P f g proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P f g; (F \<longrightarrow> F') \<and> (E' \<longrightarrow> E)\<rbrakk> \<Longrightarrow> monadic_rewrite (F \<and> F') (E \<or> E') P f g proof (prove)
goal:
No subgoals!
theory MonadicRewrite

lemma snd_bind:
  "snd ((a >>= b) s) = (snd (a s) \<or> (\<exists>(r, s') \<in> fst (a s). snd (b r s')))" by (auto simp add: bind_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd ((a >>= b) s) = (snd (a s) \<or> (\<exists>(r, s')\<in>fst (a s). snd (b r s')))
theory MonadicRewrite

lemma monadic_rewrite_bind_head:
  "monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F E P (f >>= h) (g >>= h)" by (rule monadic_rewrite_bind[OF _ monadic_rewrite_refl hoare_vcg_prop,
                                simplified pred_top_right_neutral])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F E P (f >>= h) (g >>= h)
theory MonadicRewrite

lemma monadic_rewrite_bindE_head:
  "monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F E (P and (\<lambda>s. True)) (f >>=E h) (g >>=E h)" by (rule monadic_rewrite_bindE[OF _ monadic_rewrite_refl hoare_vcg_propE_R])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F E (P and (\<lambda>s. True)) (f >>=E h) (g >>=E h)
theory MonadicRewrite

lemma monadic_rewrite_bind_l:
  "\<lbrakk> monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= (\<lambda>x. h x)) (g >>= (\<lambda>x. j x))" using monadic_rewrite_trans[OF monadic_rewrite_bind_tail monadic_rewrite_bind_head] by (metis pred_conj_comm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= h) (g >>= j) proof (prove)
using this:
\<lbrakk>\<And>x. monadic_rewrite ?F ?E (?Q2 x) (?h2 x) (?h1 x); \<lbrace>?P\<rbrace> ?f1 \<lbrace>?Q2\<rbrace>; monadic_rewrite ?F ?E ?Q ?f1 ?g1\<rbrakk> \<Longrightarrow> monadic_rewrite ?F ?E (?P and ?Q) (?f1 >>= ?h2) (?g1 >>= ?h1)

goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= h) (g >>= j)
theory MonadicRewrite

lemma monadic_rewrite_named_bindE:
  "\<lbrakk> monadic_rewrite F E ((=) s) f f';
    \<And>rv s'. (Inr rv, s') \<in> fst (f' s) \<Longrightarrow> monadic_rewrite F E ((=) s') (g rv) (g' rv) \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E ((=) s) (f >>=E (\<lambda>rv. g rv)) (f' >>=E g')" apply (rule monadic_rewrite_guard_imp) apply (erule_tac R="(=) s" and Q="\<lambda>rv s'. (Inr rv, s') \<in> fst (f' s)" in monadic_rewrite_bindE) apply (rule monadic_rewrite_name_pre) apply (clarsimp simp add: validE_R_def validE_def valid_def
                       split: sum.split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E ((=) s) f f'; \<And>rv s'. (Inr rv, s') \<in> fst (f' s) \<Longrightarrow> monadic_rewrite F E ((=) s') (g rv) (g' rv)\<rbrakk> \<Longrightarrow> monadic_rewrite F E ((=) s) (f >>=E g) (f' >>=E g') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>monadic_rewrite F E ((=) s) f f'; \<And>rv s'. (Inr rv, s') \<in> fst (f' s) \<Longrightarrow> monadic_rewrite F E ((=) s') (g rv) (g' rv)\<rbrakk> \<Longrightarrow> monadic_rewrite F E ?Q (f >>=E g) (f' >>=E g')
 2. \<And>sa. \<lbrakk>monadic_rewrite F E ((=) s) f f'; \<And>rv s'. (Inr rv, s') \<in> fst (f' s) \<Longrightarrow> monadic_rewrite F E ((=) s') (g rv) (g' rv); s = sa\<rbrakk> \<Longrightarrow> ?Q sa proof (prove)
goal (3 subgoals):
 1. \<And>x. (\<And>rv s'. (Inr rv, s') \<in> fst (f' s) \<Longrightarrow> monadic_rewrite F E ((=) s') (g rv) (g' rv)) \<Longrightarrow> monadic_rewrite F E (\<lambda>s'. (Inr x, s') \<in> fst (f' s)) (g x) (g' x)
 2. (\<And>rv s'. (Inr rv, s') \<in> fst (f' s) \<Longrightarrow> monadic_rewrite F E ((=) s') (g rv) (g' rv)) \<Longrightarrow> \<lbrace>(=) s\<rbrace> f' \<lbrace>\<lambda>rv s'. (Inr rv, s') \<in> fst (f' s)\<rbrace>, -
 3. \<And>sa. \<lbrakk>monadic_rewrite F E ((=) s) f f'; \<And>rv s'. (Inr rv, s') \<in> fst (f' s) \<Longrightarrow> monadic_rewrite F E ((=) s') (g rv) (g' rv); s = sa\<rbrakk> \<Longrightarrow> ((=) s and (=) s) sa proof (prove)
goal (3 subgoals):
 1. \<And>x sa. \<lbrakk>\<And>rv s'. (Inr rv, s') \<in> fst (f' s) \<Longrightarrow> monadic_rewrite F E ((=) s') (g rv) (g' rv); (Inr x, sa) \<in> fst (f' s)\<rbrakk> \<Longrightarrow> monadic_rewrite F E ((=) sa) (g x) (g' x)
 2. (\<And>rv s'. (Inr rv, s') \<in> fst (f' s) \<Longrightarrow> monadic_rewrite F E ((=) s') (g rv) (g' rv)) \<Longrightarrow> \<lbrace>(=) s\<rbrace> f' \<lbrace>\<lambda>rv s'. (Inr rv, s') \<in> fst (f' s)\<rbrace>, -
 3. \<And>sa. \<lbrakk>monadic_rewrite F E ((=) s) f f'; \<And>rv s'. (Inr rv, s') \<in> fst (f' s) \<Longrightarrow> monadic_rewrite F E ((=) s') (g rv) (g' rv); s = sa\<rbrakk> \<Longrightarrow> ((=) s and (=) s) sa proof (prove)
goal:
No subgoals!
theory MonadicRewrite

lemma monadic_rewrite_drop_return:
  "monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F E P (do y \<leftarrow> return x; f od) g" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F E P (do y <- return x;
f
od) g
theory MonadicRewrite

lemma monadic_rewrite_add_return:
  "monadic_rewrite F E P (do y \<leftarrow> return x; f od) g \<Longrightarrow> monadic_rewrite F E P f g " by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P (do y <- return x;
f
od) g \<Longrightarrow> monadic_rewrite F E P f g
theory MonadicRewrite

lemma monadic_rewrite_do_flip:
  "monadic_rewrite E F P (do c \<leftarrow> j; a \<leftarrow> f; b \<leftarrow> g c; return (a, c) od)
                         (do c \<leftarrow> j; b \<leftarrow> g c; a \<leftarrow> f; return (a, c) od) \<Longrightarrow>
   monadic_rewrite E F P (do c \<leftarrow> j; a \<leftarrow> f; b \<leftarrow> g c; h a c od)
                         (do c \<leftarrow> j; b \<leftarrow> g c; a \<leftarrow> f; h a c od)" apply (drule_tac h="\<lambda>(a, b). h a b" in monadic_rewrite_bind_head) apply (simp add: bind_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite E F P (do c <- j;
a <- f;
b <- g c;
return (a, c)
od) (do c <- j;
b <- g c;
a <- f;
return (a, c)
od) \<Longrightarrow> monadic_rewrite E F P (do c <- j;
a <- f;
b <- g c;
h a c
od) (do c <- j;
b <- g c;
a <- f;
h a c
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite E F P (do (a, b) <- do c <- j;
a <- f;
b <- g c;
return (a, c)
od;
h a b
od) (do (a, b) <- do c <- j;
b <- g c;
a <- f;
return (a, c)
od;
h a b
od) \<Longrightarrow> monadic_rewrite E F P (do c <- j;
a <- f;
b <- g c;
h a c
od) (do c <- j;
b <- g c;
a <- f;
h a c
od) proof (prove)
goal:
No subgoals!
theory MonadicRewrite

lemma monadic_rewrite_bind_eta_r:
  "monadic_rewrite F E P f (do x <- g; h x od)
   \<Longrightarrow> monadic_rewrite F E P f (g >>= h)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P f (g >>= h) \<Longrightarrow> monadic_rewrite F E P f (g >>= h)
theory MonadicRewrite

lemma monadic_rewrite_bind_eta_l:
  "monadic_rewrite F E P (do x <- f; h x od) g
   \<Longrightarrow> monadic_rewrite F E P (f >>= h) g" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P (f >>= h) g \<Longrightarrow> monadic_rewrite F E P (f >>= h) g
theory MonadicRewrite

lemma monadic_rewrite_bindE_eta_r:
  "monadic_rewrite F E P f (doE x <- g; h x odE)
   \<Longrightarrow> monadic_rewrite F E P f (g >>=E h)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P f (g >>=E h) \<Longrightarrow> monadic_rewrite F E P f (g >>=E h)
theory MonadicRewrite

lemma monadic_rewrite_bindE_eta_l:
  "monadic_rewrite F E P (doE x <- f; h x odE) g
   \<Longrightarrow> monadic_rewrite F E P (f >>=E h) g" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E P (f >>=E h) g \<Longrightarrow> monadic_rewrite F E P (f >>=E h) g
theory MonadicRewrite

lemma monadic_rewrite_catch:
  "\<lbrakk> monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g -,\<lbrace>Q\<rbrace> \<rbrakk>
   \<Longrightarrow> monadic_rewrite F E (P and R) (f <catch> (\<lambda>x. h x)) (g <catch> (\<lambda>x. j x))" apply (simp add: catch_def) apply (erule monadic_rewrite_bind) defer apply (simp add: validE_E_def validE_def) apply (case_tac x, simp_all add: lift_def monadic_rewrite_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g -, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (f <catch> h) (g <catch> j) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g -, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E (P and R) (do x <- f;
case x of Inl e \<Rightarrow> h e | Inr b \<Rightarrow> return b
od) (do x <- g;
case x of Inl e \<Rightarrow> j e | Inr b \<Rightarrow> return b
od) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g -, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?Q x) (case x of Inl e \<Rightarrow> h e | Inr b \<Rightarrow> return b) (case x of Inl e \<Rightarrow> j e | Inr b \<Rightarrow> return b)
 2. \<lbrakk>\<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g -, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> g \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g -, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> g \<lbrace>?Q\<rbrace>
 2. \<And>x. \<lbrakk>\<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g -, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E (?Q x) (case x of Inl e \<Rightarrow> h e | Inr b \<Rightarrow> return b) (case x of Inl e \<Rightarrow> j e | Inr b \<Rightarrow> return b) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. monadic_rewrite F E (Q x) (h x) (j x); \<lbrace>R\<rbrace> g -, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F E (\<lambda>s. case x of Inl e \<Rightarrow> Q e s | Inr r \<Rightarrow> True) (case x of Inl e \<Rightarrow> h e | Inr b \<Rightarrow> return b) (case x of Inl e \<Rightarrow> j e | Inr b \<Rightarrow> return b) proof (prove)
goal:
No subgoals!
theory MonadicRewrite

lemma monadic_rewrite_drop_modify:
  "monadic_rewrite F E (\<lambda>s. f s = s) (modify f >>= v) (v ())" by (simp add: monadic_rewrite_def bind_def simpler_modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (\<lambda>s. f s = s) (modify f >>= v) (v ())
theory MonadicRewrite

lemma monadic_rewrite_modify_noop:
  "monadic_rewrite F E (\<lambda>s. f s = s) (modify f) (return ())" by (clarsimp simp: monadic_rewrite_def simpler_modify_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (\<lambda>s. f s = s) (modify f) (return ())
theory MonadicRewrite

lemma monadic_rewrite_symb_exec_l_F:
  "\<lbrakk> \<And>rv. monadic_rewrite True E (Q rv) (x rv) y;
     \<And>P. m \<lbrace>P\<rbrace>; empty_fail m;
     \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace> \<rbrakk>
   \<Longrightarrow> monadic_rewrite True E P (m >>= (\<lambda>rv. x rv)) y" by (rule monadic_rewrite_symb_exec_l'[where P'=\<top> and F=True, simplified])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. monadic_rewrite True E (Q rv) (x rv) y; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite True E P (m >>= x) y
theory MonadicRewrite

lemma monadic_rewrite_symb_exec_l_known_F:
  "\<lbrakk> monadic_rewrite True E Q (x rv) y;
     \<And>P. m \<lbrace>P\<rbrace>; empty_fail m;
     \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' _. rv' = rv \<rbrace> \<rbrakk>
   \<Longrightarrow> monadic_rewrite True E (P and Q) (m >>= x) y" by (erule monadic_rewrite_trans[rotated])
     (rule monadic_rewrite_symb_exec_l_F[OF monadic_rewrite_pre_imp_eq]; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite True E Q (x rv) y; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' _. rv' = rv\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite True E (P and Q) (m >>= x) y
theory MonadicRewrite

lemma monadic_rewrite_symb_exec_l_known_nF:
  "\<lbrakk> monadic_rewrite False E Q (x rv) y;
     \<And>P. m \<lbrace>P\<rbrace>; empty_fail m; no_fail P' m;
     \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv \<rbrace> \<rbrakk>
   \<Longrightarrow> monadic_rewrite False E (P and P' and Q) (m >>= x) y" by (erule monadic_rewrite_trans[rotated])
     (rule monadic_rewrite_symb_exec_l_nF[OF monadic_rewrite_pre_imp_eq]; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite False E Q (x rv) y; \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False E (P and P' and Q) (m >>= x) y
theory MonadicRewrite

lemma monadic_rewrite_symb_exec_r_known_E:
  "\<lbrakk> monadic_rewrite F True Q x (y rv);
     \<And>P. m \<lbrace>P\<rbrace>; empty_fail m; no_fail P' m;
     \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv \<rbrace> \<rbrakk>
   \<Longrightarrow> monadic_rewrite F True (P and P' and Q) x (m >>= y)" apply (rule monadic_rewrite_guard_imp) apply (erule monadic_rewrite_trans) apply (rule monadic_rewrite_symb_exec_r_E[OF monadic_rewrite_pre_imp_eq, rotated -1], simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite F True Q x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F True (P and P' and Q) x (m >>= y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>monadic_rewrite F True Q x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F True ?Q x (m >>= y)
 2. \<And>s. \<lbrakk>monadic_rewrite F True Q x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv\<rbrace>; (P and P' and Q) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite F True ?Q3 (y rv) (m >>= y)
 2. \<And>s. \<lbrakk>monadic_rewrite F True Q x (y rv); \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_. P\<rbrace>; empty_fail m; no_fail P' m; \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv\<rbrace>; (P and P' and Q) s\<rbrakk> \<Longrightarrow> (Q and ?Q3) s proof (prove)
goal:
No subgoals!