theory MonadicRewrite

lemma monadic_rewrite_bind_alternative:
  "\<lbrakk> \<And>P. f \<lbrace>P\<rbrace> \<rbrakk>
   \<Longrightarrow> monadic_rewrite F False \<top> (alternative (f >>= (\<lambda>x. g x)) h)
                                (f >>= (\<lambda>x. alternative (g x) h))" apply (clarsimp simp: monadic_rewrite_def bind_def
                        alternative_def imp_conjL) apply (subgoal_tac "\<forall>x \<in> fst (f s). snd x = s") apply (simp add: image_image split_def cong: image_cong) apply fastforce apply clarsimp apply (drule hoare_eq_P) apply (frule use_valid, (assumption | rule refl | simp)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<Longrightarrow> monadic_rewrite F False (\<lambda>_. True) (f >>= g \<sqinter> h) (do x <- f;
g x \<sqinter> h
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; F \<longrightarrow> (\<forall>x\<in>fst (f s). \<not> snd (case x of (x, xa) \<Rightarrow> g x xa)) \<and> \<not> snd (f s) \<and> \<not> snd (h s)\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (f s). fst (case a of (x, s) \<Rightarrow> (fst (g x s) \<union> fst (h s), snd (g x s) \<or> snd (h s)))) \<subseteq> (\<Union>a\<in>fst (f s). fst (case a of (x, xa) \<Rightarrow> g x xa)) \<union> fst (h s) \<and> ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> (fst (g x s) \<union> fst (h s), snd (g x s) \<or> snd (h s)))) \<longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (x, xa) \<Rightarrow> g x xa)) \<or> snd (f s) \<or> snd (h s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; F \<longrightarrow> (\<forall>x\<in>fst (f s). \<not> snd (case x of (x, xa) \<Rightarrow> g x xa)) \<and> \<not> snd (f s) \<and> \<not> snd (h s); \<forall>x\<in>fst (f s). snd x = s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (f s). fst (case a of (x, s) \<Rightarrow> (fst (g x s) \<union> fst (h s), snd (g x s) \<or> snd (h s)))) \<subseteq> (\<Union>a\<in>fst (f s). fst (case a of (x, xa) \<Rightarrow> g x xa)) \<union> fst (h s) \<and> ((\<exists>x\<in>fst (f s). snd (case x of (x, s) \<Rightarrow> (fst (g x s) \<union> fst (h s), snd (g x s) \<or> snd (h s)))) \<longrightarrow> (\<exists>x\<in>fst (f s). snd (case x of (x, xa) \<Rightarrow> g x xa)) \<or> snd (f s) \<or> snd (h s))
 2. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; F \<longrightarrow> (\<forall>x\<in>fst (f s). \<not> snd (case x of (x, xa) \<Rightarrow> g x xa)) \<and> \<not> snd (f s) \<and> \<not> snd (h s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f s). snd x = s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; F \<longrightarrow> (\<forall>x\<in>fst (f s). \<not> snd (g (fst x) s)) \<and> \<not> snd (f s) \<and> \<not> snd (h s); \<forall>x\<in>fst (f s). snd x = s\<rbrakk> \<Longrightarrow> fst (f s) \<noteq> {} \<longrightarrow> (\<exists>x\<in>fst (f s). snd (g (fst x) s) \<or> snd (h s)) \<longrightarrow> (\<exists>x\<in>fst (f s). snd (g (fst x) s)) \<or> snd (f s) \<or> snd (h s)
 2. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; F \<longrightarrow> (\<forall>x\<in>fst (f s). \<not> snd (case x of (x, xa) \<Rightarrow> g x xa)) \<and> \<not> snd (f s) \<and> \<not> snd (h s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f s). snd x = s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; F \<longrightarrow> (\<forall>x\<in>fst (f s). \<not> snd (case x of (x, xa) \<Rightarrow> g x xa)) \<and> \<not> snd (f s) \<and> \<not> snd (h s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f s). snd x = s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; F \<longrightarrow> (\<forall>x\<in>fst (f s). \<not> snd (case x of (x, xa) \<Rightarrow> g x xa)) \<and> \<not> snd (f s) \<and> \<not> snd (h s); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> b = s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>F \<longrightarrow> (\<forall>x\<in>fst (f s). \<not> snd (case x of (x, xa) \<Rightarrow> g x xa)) \<and> \<not> snd (f s) \<and> \<not> snd (h s); (a, b) \<in> fst (f s); \<lbrace>(=) (?s45 s a b)\<rbrace> f \<lbrace>\<lambda>_. (=) (?s45 s a b)\<rbrace>\<rbrakk> \<Longrightarrow> b = s proof (prove)
goal:
No subgoals!