theory Ipc_IF

lemma monadic_rewrite_reads_respects:
  "\<lbrakk> monadic_rewrite False False P f f'; reads_respects aag l P' (do x <- f; g x od) \<rbrakk>
     \<Longrightarrow> reads_respects aag l (P and P') (do x <- f'; g x od)" apply (clarsimp simp: monadic_rewrite_def spec_equiv_valid_def
                        equiv_valid_def equiv_valid_2_def bind_def) apply (frule_tac x=st in spec) apply (drule_tac x=t in spec) by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monadic_rewrite False False P f f'; reads_respects aag l P' (f >>= g)\<rbrakk> \<Longrightarrow> reads_respects aag l (P and P') (f' >>= g) proof (prove)
goal (1 subgoal):
 1. \<And>st t a b aa ba ab bb ac bc. \<lbrakk>\<forall>s. P s \<longrightarrow> fst (f' s) \<subseteq> fst (f s) \<and> (snd (f' s) \<longrightarrow> snd (f s)); \<forall>st t. P' st \<and> P' t \<and> reads_equiv aag st t \<and> affects_equiv aag l st t \<longrightarrow> (\<forall>y\<in>fst (f st). \<forall>x\<in>fst (case y of (x, xa) \<Rightarrow> g x xa). case x of (rva, s') \<Rightarrow> \<forall>y\<in>fst (f t). \<forall>x\<in>fst (case y of (x, xa) \<Rightarrow> g x xa). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> affects_equiv aag l s' t'); (a, b) \<in> fst (f' st); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f' t); (ac, bc) \<in> fst (g ab bb); P st; P' st; P t; P' t; reads_equiv aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> aa = ac \<and> reads_equiv aag ba bc \<and> affects_equiv aag l ba bc proof (prove)
goal (1 subgoal):
 1. \<And>st t a b aa ba ab bb ac bc. \<lbrakk>\<forall>s. P s \<longrightarrow> fst (f' s) \<subseteq> fst (f s) \<and> (snd (f' s) \<longrightarrow> snd (f s)); \<forall>st t. P' st \<and> P' t \<and> reads_equiv aag st t \<and> affects_equiv aag l st t \<longrightarrow> (\<forall>y\<in>fst (f st). \<forall>x\<in>fst (case y of (x, xa) \<Rightarrow> g x xa). case x of (rva, s') \<Rightarrow> \<forall>y\<in>fst (f t). \<forall>x\<in>fst (case y of (x, xa) \<Rightarrow> g x xa). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> affects_equiv aag l s' t'); (a, b) \<in> fst (f' st); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f' t); (ac, bc) \<in> fst (g ab bb); P st; P' st; P t; P' t; reads_equiv aag st t; affects_equiv aag l st t; P st \<longrightarrow> fst (f' st) \<subseteq> fst (f st) \<and> (snd (f' st) \<longrightarrow> snd (f st))\<rbrakk> \<Longrightarrow> aa = ac \<and> reads_equiv aag ba bc \<and> affects_equiv aag l ba bc proof (prove)
goal (1 subgoal):
 1. \<And>st t a b aa ba ab bb ac bc. \<lbrakk>\<forall>st t. P' st \<and> P' t \<and> reads_equiv aag st t \<and> affects_equiv aag l st t \<longrightarrow> (\<forall>y\<in>fst (f st). \<forall>x\<in>fst (case y of (x, xa) \<Rightarrow> g x xa). case x of (rva, s') \<Rightarrow> \<forall>y\<in>fst (f t). \<forall>x\<in>fst (case y of (x, xa) \<Rightarrow> g x xa). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> affects_equiv aag l s' t'); (a, b) \<in> fst (f' st); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f' t); (ac, bc) \<in> fst (g ab bb); P st; P' st; P t; P' t; reads_equiv aag st t; affects_equiv aag l st t; P st \<longrightarrow> fst (f' st) \<subseteq> fst (f st) \<and> (snd (f' st) \<longrightarrow> snd (f st)); P t \<longrightarrow> fst (f' t) \<subseteq> fst (f t) \<and> (snd (f' t) \<longrightarrow> snd (f t))\<rbrakk> \<Longrightarrow> aa = ac \<and> reads_equiv aag ba bc \<and> affects_equiv aag l ba bc