theory EquivValid

lemma bind_spec_ev2:
  assumes reads_res_2: "\<And> rv s' rv'. \<lbrakk>(rv, s') \<in> fst (f s); R' rv rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A R (Q rv) (Q' rv') (g rv) (g' rv')"
  assumes reads_res_1: "spec_equiv_valid_2_inv s I A R' P P' f f'"
  assumes hoare: "\<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>"
  assumes hoare': "\<lbrace>S'\<rbrace> f' \<lbrace>Q'\<rbrace>"
  shows "spec_equiv_valid_2_inv s I A R (P and S) (P' and S') (f >>= g) (f' >>= g')" using reads_res_1 apply (clarsimp simp: spec_equiv_valid_2_inv_def equiv_valid_2_def bind_def split_def) apply (erule_tac x=t in allE) apply clarsimp apply (drule_tac x="(a, b)" in bspec, assumption) apply (drule_tac x="(ab, bb)" in bspec, assumption) apply clarsimp apply (cut_tac rv="a" and s'="b" in reads_res_2) apply assumption apply assumption apply (clarsimp simp: spec_equiv_valid_2_inv_def equiv_valid_2_def) apply(drule_tac x=bb in spec) apply clarsimp using hoare hoare' apply (fastforce simp: valid_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_equiv_valid_2_inv s I A R (P and S) (P' and S') (f >>= g) (f' >>= g') proof (prove)
using this:
spec_equiv_valid_2_inv s I A R' P P' f f'

goal (1 subgoal):
 1. spec_equiv_valid_2_inv s I A R (P and S) (P' and S') (f >>= g) (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). R' (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; S s; P' t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> R 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; S s; P' t; S' 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). R' (fst x) (fst xa) \<and> I (snd x) (snd xa) \<and> A (snd x) (snd xa))\<rbrakk> \<Longrightarrow> R 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; S s; P' t; S' t; I s t; A s t; \<forall>x\<in>fst (f s). \<forall>xa\<in>fst (f' t). R' (fst x) (fst xa) \<and> I (snd x) (snd xa) \<and> A (snd x) (snd xa)\<rbrakk> \<Longrightarrow> R 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; S s; P' t; S' t; I s t; A s t; \<forall>x\<in>fst (f' t). R' (fst (a, b)) (fst x) \<and> I (snd (a, b)) (snd x) \<and> A (snd (a, b)) (snd x)\<rbrakk> \<Longrightarrow> R 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; S s; P' t; S' t; I s t; A s t; R' (fst (a, b)) (fst (ab, bb)) \<and> I (snd (a, b)) (snd (ab, bb)) \<and> A (snd (a, b)) (snd (ab, bb))\<rbrakk> \<Longrightarrow> R 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; S s; P' t; S' t; I s t; A s t; R' a ab; I b bb; A b bb\<rbrakk> \<Longrightarrow> R 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; S s; P' t; S' t; I s t; A s t; R' a ab; I b bb; A b bb\<rbrakk> \<Longrightarrow> (a, b) \<in> fst (f s)
 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; S s; P' t; S' t; I s t; A s t; R' a ab; I b bb; A b bb\<rbrakk> \<Longrightarrow> R' a (?rv'47 t a b aa ba ab bb ac 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; S s; P' t; S' t; I s t; A s t; R' a ab; I b bb; A b bb; spec_equiv_valid_2_inv b I A R (Q a) (Q' (?rv'47 t a b aa ba ab bb ac bc)) (g a) (g' (?rv'47 t a b aa ba ab bb ac bc))\<rbrakk> \<Longrightarrow> R 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; S s; P' t; S' t; I s t; A s t; R' a ab; I b bb; A b bb\<rbrakk> \<Longrightarrow> R' a (?rv'47 t a b aa ba ab bb ac 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; S s; P' t; S' t; I s t; A s t; R' a ab; I b bb; A b bb; spec_equiv_valid_2_inv b I A R (Q a) (Q' (?rv'47 t a b aa ba ab bb ac bc)) (g a) (g' (?rv'47 t a b aa ba ab bb ac bc))\<rbrakk> \<Longrightarrow> R 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; S s; P' t; S' t; I s t; A s t; R' a ab; I b bb; A b bb; spec_equiv_valid_2_inv b I A R (Q a) (Q' ab) (g a) (g' ab)\<rbrakk> \<Longrightarrow> R 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; S s; P' t; S' t; I s t; A s t; R' a ab; I b bb; A b bb; \<forall>t. Q a b \<and> Q' ab 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' ab t). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> I s' t' \<and> A s' t')\<rbrakk> \<Longrightarrow> R 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; S s; P' t; S' t; I s t; A s t; R' a ab; I b bb; A b bb; Q a b \<and> Q' ab 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' ab bb). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> I s' t' \<and> A s' t')\<rbrakk> \<Longrightarrow> R 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; S s; P' t; S' t; I s t; A s t; R' a ab; I b bb; A b bb; Q a b \<and> Q' ab bb \<longrightarrow> (\<forall>x\<in>fst (g a b). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g' ab bb). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> I s' t' \<and> A s' t')\<rbrakk> \<Longrightarrow> R aa ac \<and> I ba bc \<and> A ba bc proof (prove)
using this:
\<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>
\<lbrace>S'\<rbrace> f' \<lbrace>Q'\<rbrace>

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; S s; P' t; S' t; I s t; A s t; R' a ab; I b bb; A b bb; Q a b \<and> Q' ab bb \<longrightarrow> (\<forall>x\<in>fst (g a b). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g' ab bb). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> I s' t' \<and> A s' t')\<rbrakk> \<Longrightarrow> R aa ac \<and> I ba bc \<and> A ba bc proof (prove)
goal:
No subgoals!