theory Arch_IF

lemma ev2_invisible:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
  "\<lbrakk> labels_are_invisible aag l L; labels_are_invisible aag l L';
     modifies_at_most aag L Q f; modifies_at_most aag L' Q' g;
     \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>(rva,s') \<in> fst (f s). \<forall>(rvb,t') \<in> fst (g t). W rva rvb) \<rbrakk>
     \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l)
                        W (P and Q) (P' and Q') f g" apply (clarsimp simp: equiv_valid_2_def) apply (rule conjI) apply blast apply (drule_tac s=s in modifies_at_mostD, assumption+) apply (drule_tac s=t in modifies_at_mostD, assumption+) apply (frule (1) equiv_but_for_reads_equiv[OF domains_distinct]) apply (frule_tac s=t in equiv_but_for_reads_equiv[OF domains_distinct], assumption) apply (drule (1) equiv_but_for_affects_equiv[OF domains_distinct]) apply (drule_tac s=t in equiv_but_for_affects_equiv[OF domains_distinct], assumption) apply (blast intro: reads_equiv_trans reads_equiv_sym affects_equiv_trans affects_equiv_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; modifies_at_most aag L Q f; modifies_at_most aag L' Q' g; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>(rva, s')\<in>fst (f s). \<forall>(rvb, t')\<in>fst (g t). W rva rvb)\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) W (P and Q) (P' and Q') f g proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; modifies_at_most aag L Q f; modifies_at_most aag L' Q' g; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> W a aa \<and> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; modifies_at_most aag L Q f; modifies_at_most aag L' Q' g; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> W a aa
 2. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; modifies_at_most aag L Q f; modifies_at_most aag L' Q' g; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; modifies_at_most aag L Q f; modifies_at_most aag L' Q' g; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; modifies_at_most aag L' Q' g; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv aag s t; affects_equiv aag l s t; equiv_but_for_labels aag L s b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv aag s t; affects_equiv aag l s t; equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv aag s t; affects_equiv aag l s t; equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; reads_equiv aag s b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L; labels_are_invisible aag l L'; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv aag s t; affects_equiv aag l s t; equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; reads_equiv aag s b; reads_equiv aag t ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>labels_are_invisible aag l L'; \<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv aag s t; affects_equiv aag l s t; equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P' t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> W rva rvb); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g t); P s; Q s; P' t; Q' t; reads_equiv aag s t; affects_equiv aag l s t; equiv_but_for_labels aag L s b; equiv_but_for_labels aag L' t ba; reads_equiv aag s b; reads_equiv aag t ba; affects_equiv aag l s b; affects_equiv aag l t ba\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal:
No subgoals!