theory EquivValid

lemma bind_spec_ev:
  assumes reads_res_2: "\<And> rv s''. (rv, s'') \<in> fst (f s') \<Longrightarrow> spec_equiv_valid_inv s'' I A (Q rv) (g rv)"
  assumes reads_res_1: "spec_equiv_valid_inv s' I A P' f"
  assumes hoare: "\<lbrace>P''\<rbrace> f \<lbrace>Q\<rbrace>"
  shows "spec_equiv_valid_inv s' I A (\<lambda>s. P' s \<and> P'' s) (f >>= g)" using reads_res_1 apply (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def valid_def bind_def split_def) apply (rename_tac t a b aa ba ab bb ac bc) apply (erule_tac x=t in allE) apply clarsimp apply (erule_tac x="(a, b)" in ballE) apply (erule_tac x="(ab, bb)" in ballE) apply clarsimp apply (cut_tac reads_res_2) prefer 2 apply assumption apply (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def) apply(erule_tac x=bb in allE) using hoare apply (fastforce simp: valid_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_equiv_valid_inv s' I A (\<lambda>s. P' s \<and> P'' s) (f >>= g) proof (prove)
using this:
spec_equiv_valid_inv s' I A P' f

goal (1 subgoal):
 1. spec_equiv_valid_inv s' I A (\<lambda>s. P' s \<and> P'' s) (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<And>t a b aa ba ab bb ac bc. \<lbrakk>\<forall>t. P' t \<and> I s' t \<and> A s' t \<longrightarrow> (\<forall>x\<in>fst (f s'). \<forall>xa\<in>fst (f t). fst x = fst xa \<and> I (snd x) (snd xa) \<and> A (snd x) (snd xa)); (a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc proof (prove)
goal (1 subgoal):
 1. \<And>t a b aa ba ab bb ac bc. \<lbrakk>\<forall>t. P' t \<and> I s' t \<and> A s' t \<longrightarrow> (\<forall>x\<in>fst (f s'). \<forall>xa\<in>fst (f t). fst x = fst xa \<and> I (snd x) (snd xa) \<and> A (snd x) (snd xa)); (a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc proof (prove)
goal (1 subgoal):
 1. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; P' t \<and> I s' t \<and> A s' t \<longrightarrow> (\<forall>x\<in>fst (f s'). \<forall>xa\<in>fst (f t). fst x = fst xa \<and> I (snd x) (snd xa) \<and> A (snd x) (snd xa))\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc proof (prove)
goal (1 subgoal):
 1. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; \<forall>x\<in>fst (f s'). \<forall>xa\<in>fst (f t). fst x = fst xa \<and> I (snd x) (snd xa) \<and> A (snd x) (snd xa)\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc proof (prove)
goal (2 subgoals):
 1. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; \<forall>x\<in>fst (f t). fst (a, b) = fst x \<and> I (snd (a, b)) (snd x) \<and> A (snd (a, b)) (snd x)\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 2. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (a, b) \<notin> fst (f s')\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc proof (prove)
goal (3 subgoals):
 1. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; fst (a, b) = fst (ab, bb) \<and> I (snd (a, b)) (snd (ab, bb)) \<and> A (snd (a, b)) (snd (ab, bb))\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 2. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (ab, bb) \<notin> fst (f t)\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 3. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (a, b) \<notin> fst (f s')\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc proof (prove)
goal (3 subgoals):
 1. \<And>t a b aa ba bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (a, bb) \<in> fst (f t); (ac, bc) \<in> fst (g a bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; I b bb; A b bb\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 2. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (ab, bb) \<notin> fst (f t)\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 3. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (a, b) \<notin> fst (f s')\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc proof (prove)
goal (4 subgoals):
 1. \<And>t a b aa ba bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (a, bb) \<in> fst (f t); (ac, bc) \<in> fst (g a bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; I b bb; A b bb; spec_equiv_valid_inv (?s''47 t a b aa ba bb ac bc) I A (Q (?rv47 t a b aa ba bb ac bc)) (g (?rv47 t a b aa ba bb ac bc))\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 2. \<And>t a b aa ba bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (a, bb) \<in> fst (f t); (ac, bc) \<in> fst (g a bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; I b bb; A b bb\<rbrakk> \<Longrightarrow> (?rv47 t a b aa ba bb ac bc, ?s''47 t a b aa ba bb ac bc) \<in> fst (f s')
 3. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (ab, bb) \<notin> fst (f t)\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 4. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (a, b) \<notin> fst (f s')\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc proof (prove)
goal (4 subgoals):
 1. \<And>t a b aa ba bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (a, bb) \<in> fst (f t); (ac, bc) \<in> fst (g a bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; I b bb; A b bb\<rbrakk> \<Longrightarrow> (?rv47 t a b aa ba bb ac bc, ?s''47 t a b aa ba bb ac bc) \<in> fst (f s')
 2. \<And>t a b aa ba bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (a, bb) \<in> fst (f t); (ac, bc) \<in> fst (g a bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; I b bb; A b bb; spec_equiv_valid_inv (?s''47 t a b aa ba bb ac bc) I A (Q (?rv47 t a b aa ba bb ac bc)) (g (?rv47 t a b aa ba bb ac bc))\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 3. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (ab, bb) \<notin> fst (f t)\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 4. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (a, b) \<notin> fst (f s')\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc proof (prove)
goal (3 subgoals):
 1. \<And>t a b aa ba bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (a, bb) \<in> fst (f t); (ac, bc) \<in> fst (g a bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; I b bb; A b bb; spec_equiv_valid_inv b I A (Q a) (g a)\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 2. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (ab, bb) \<notin> fst (f t)\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 3. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (a, b) \<notin> fst (f s')\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc proof (prove)
goal (3 subgoals):
 1. \<And>t a b aa ba bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (a, bb) \<in> fst (f t); (ac, bc) \<in> fst (g a bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; I b bb; A b bb; \<forall>t. Q a b \<and> Q a t \<and> I b t \<and> A b t \<longrightarrow> (\<forall>x\<in>fst (g a b). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g a t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t')\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 2. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (ab, bb) \<notin> fst (f t)\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 3. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (a, b) \<notin> fst (f s')\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc proof (prove)
goal (3 subgoals):
 1. \<And>t a b aa ba bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (a, bb) \<in> fst (f t); (ac, bc) \<in> fst (g a bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; I b bb; A b bb; Q a b \<and> Q a bb \<and> I b bb \<and> A b bb \<longrightarrow> (\<forall>x\<in>fst (g a b). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g a bb). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t')\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 2. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (ab, bb) \<notin> fst (f t)\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 3. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (a, b) \<notin> fst (f s')\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc proof (prove)
using this:
\<lbrace>P''\<rbrace> f \<lbrace>Q\<rbrace>

goal (3 subgoals):
 1. \<And>t a b aa ba bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (a, bb) \<in> fst (f t); (ac, bc) \<in> fst (g a bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; I b bb; A b bb; Q a b \<and> Q a bb \<and> I b bb \<and> A b bb \<longrightarrow> (\<forall>x\<in>fst (g a b). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g a bb). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> A s' t')\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 2. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (ab, bb) \<notin> fst (f t)\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc
 3. \<And>t a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g ab bb); P' s'; P'' s'; P' t; P'' t; I s' t; A s' t; (a, b) \<notin> fst (f s')\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> A ba bc proof (prove)
goal:
No subgoals!