theory Scheduler_IF

lemma equiv_valid_inv_unobservable:
  assumes f: "\<And>st. \<lbrace>P and I st and A st\<rbrace> f \<lbrace>\<lambda>_. I st\<rbrace>"
  assumes g: "\<And>st. \<lbrace>P' and I st and A st\<rbrace> f \<lbrace>\<lambda>_. A st\<rbrace>"
  assumes sym: "\<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s"
  assumes trans: "\<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''"
  assumes s: "\<And>s. Q s \<Longrightarrow> P s \<and> P' s"
  shows "equiv_valid_inv I A  Q (f :: 'a \<Rightarrow> (unit \<times> 'a) set \<times> bool)" apply (clarsimp simp add: equiv_valid_def spec_equiv_valid_def equiv_valid_2_def) apply (erule preserves_equivalence_weak,assumption) apply (rule hoare_pre) apply (rule hoare_vcg_conj_lift) apply (rule f) apply (rule g) apply force apply (insert s) apply (fastforce intro!: sym trans)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A Q f proof (prove)
goal (1 subgoal):
 1. \<And>st t b ba. \<lbrakk>((), b) \<in> fst (f st); ((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> I b ba \<and> A b ba proof (prove)
goal (6 subgoals):
 1. \<And>st t b ba sta. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<lbrace>?P25 st t b ba and (\<lambda>a. I sta a \<and> A sta a)\<rbrace> f \<lbrace>\<lambda>_ a. I sta a \<and> A sta a\<rbrace>
 2. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 3. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 4. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> I st t \<and> A st t
 5. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> ?P25 st t b ba st
 6. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> ?P25 st t b ba t proof (prove)
goal (7 subgoals):
 1. \<And>st t b ba sta. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 st t b ba sta\<rbrace> f \<lbrace>\<lambda>_ a. I sta a \<and> A sta a\<rbrace>
 2. \<And>st t b ba sta s. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t; (?P25 st t b ba and (\<lambda>a. I sta a \<and> A sta a)) s\<rbrakk> \<Longrightarrow> ?Q33 st t b ba sta s
 3. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 4. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 5. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> I st t \<and> A st t
 6. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> ?P25 st t b ba st
 7. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> ?P25 st t b ba t proof (prove)
goal (8 subgoals):
 1. \<And>st t b ba sta. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<lbrace>?P36 st t b ba sta\<rbrace> f \<lbrace>\<lambda>rv. I sta\<rbrace>
 2. \<And>st t b ba sta. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 st t b ba sta\<rbrace> f \<lbrace>\<lambda>rv. A sta\<rbrace>
 3. \<And>st t b ba sta s. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t; (?P25 st t b ba and (\<lambda>a. I sta a \<and> A sta a)) s\<rbrakk> \<Longrightarrow> ?P36 st t b ba sta s \<and> ?P'36 st t b ba sta s
 4. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 5. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 6. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> I st t \<and> A st t
 7. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> ?P25 st t b ba st
 8. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> ?P25 st t b ba t proof (prove)
goal (7 subgoals):
 1. \<And>st t b ba sta. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<lbrace>?P'36 st t b ba sta\<rbrace> f \<lbrace>\<lambda>rv. A sta\<rbrace>
 2. \<And>st t b ba sta s. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t; (?P25 st t b ba and (\<lambda>a. I sta a \<and> A sta a)) s\<rbrakk> \<Longrightarrow> (P and I sta and A sta) s \<and> ?P'36 st t b ba sta s
 3. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 4. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 5. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> I st t \<and> A st t
 6. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> ?P25 st t b ba st
 7. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> ?P25 st t b ba t proof (prove)
goal (6 subgoals):
 1. \<And>st t b ba sta s. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t; (?P25 st t b ba and (\<lambda>a. I sta a \<and> A sta a)) s\<rbrakk> \<Longrightarrow> (P and I sta and A sta) s \<and> (P' and I sta and A sta) s
 2. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 3. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 4. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> I st t \<and> A st t
 5. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> ?P25 st t b ba st
 6. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> ?P25 st t b ba t proof (prove)
goal (5 subgoals):
 1. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 2. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 3. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> I st t \<and> A st t
 4. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> P st \<and> P' st
 5. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t\<rbrakk> \<Longrightarrow> P t \<and> P' t proof (prove)
goal (5 subgoals):
 1. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t; \<And>s. Q s \<Longrightarrow> P s \<and> P' s\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 2. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t; \<And>s. Q s \<Longrightarrow> P s \<and> P' s\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 3. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t; \<And>s. Q s \<Longrightarrow> P s \<and> P' s\<rbrakk> \<Longrightarrow> I st t \<and> A st t
 4. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t; \<And>s. Q s \<Longrightarrow> P s \<and> P' s\<rbrakk> \<Longrightarrow> P st \<and> P' st
 5. \<And>st t b ba. \<lbrakk>((), ba) \<in> fst (f t); Q st; Q t; I st t; A st t; \<And>s. Q s \<Longrightarrow> P s \<and> P' s\<rbrakk> \<Longrightarrow> P t \<and> P' t proof (prove)
goal:
No subgoals!