theory ArchScheduler_IF

lemma globals_equiv_scheduler_inv'[Scheduler_IF_assms]:
  "(\<And>st. \<lbrace>P and globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>)
   \<Longrightarrow> \<lbrace>P and globals_equiv_scheduler s\<rbrace> f \<lbrace>\<lambda>_. globals_equiv_scheduler s\<rbrace>" apply atomize apply (rule use_spec) apply (simp add: spec_valid_def) apply (erule_tac x="(swap_things sa s)" in allE) apply (rule_tac Q="\<lambda>r st. globals_equiv (swap_things sa s) st" in hoare_strengthen_post) apply (rule hoare_pre) apply assumption apply (clarsimp simp: globals_equiv_def swap_things_def globals_equiv_scheduler_def
                         arch_globals_equiv_scheduler_def arch_scheduler_affects_equiv_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>st. \<lbrace>P and globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>) \<Longrightarrow> \<lbrace>P and globals_equiv_scheduler s\<rbrace> f \<lbrace>\<lambda>_. globals_equiv_scheduler s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>st. \<lbrace>P and globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace> \<Longrightarrow> \<lbrace>P and globals_equiv_scheduler s\<rbrace> f \<lbrace>\<lambda>_. globals_equiv_scheduler s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<forall>st. \<lbrace>P and globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace> \<Longrightarrow> sa \<turnstile> \<lbrace>P and globals_equiv_scheduler s\<rbrace> f \<lbrace>\<lambda>_. globals_equiv_scheduler s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<forall>st. \<lbrace>P and globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>sb. sb = sa \<and> P sb \<and> globals_equiv_scheduler s sb\<rbrace> f \<lbrace>\<lambda>_. globals_equiv_scheduler s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrace>P and globals_equiv (swap_things sa s)\<rbrace> f \<lbrace>\<lambda>_. globals_equiv (swap_things sa s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>sb. sb = sa \<and> P sb \<and> globals_equiv_scheduler s sb\<rbrace> f \<lbrace>\<lambda>_. globals_equiv_scheduler s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrace>P and globals_equiv (swap_things sa s)\<rbrace> f \<lbrace>\<lambda>_. globals_equiv (swap_things sa s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>sb. sb = sa \<and> P sb \<and> globals_equiv_scheduler s sb\<rbrace> f \<lbrace>\<lambda>r. globals_equiv (swap_things sa s)\<rbrace>
 2. \<And>sa rv saa. \<lbrakk>\<lbrace>P and globals_equiv (swap_things sa s)\<rbrace> f \<lbrace>\<lambda>_. globals_equiv (swap_things sa s)\<rbrace>; globals_equiv (swap_things sa s) saa\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s saa proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrace>P and globals_equiv (swap_things sa s)\<rbrace> f \<lbrace>\<lambda>_. globals_equiv (swap_things sa s)\<rbrace> \<Longrightarrow> \<lbrace>?Q5 sa\<rbrace> f \<lbrace>\<lambda>r. globals_equiv (swap_things sa s)\<rbrace>
 2. \<And>sa saa. \<lbrakk>\<lbrace>P and globals_equiv (swap_things sa s)\<rbrace> f \<lbrace>\<lambda>_. globals_equiv (swap_things sa s)\<rbrace>; saa = sa \<and> P saa \<and> globals_equiv_scheduler s saa\<rbrakk> \<Longrightarrow> ?Q5 sa saa
 3. \<And>sa rv saa. \<lbrakk>\<lbrace>P and globals_equiv (swap_things sa s)\<rbrace> f \<lbrace>\<lambda>_. globals_equiv (swap_things sa s)\<rbrace>; globals_equiv (swap_things sa s) saa\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s saa proof (prove)
goal (2 subgoals):
 1. \<And>sa saa. \<lbrakk>\<lbrace>P and globals_equiv (swap_things sa s)\<rbrace> f \<lbrace>\<lambda>_. globals_equiv (swap_things sa s)\<rbrace>; saa = sa \<and> P saa \<and> globals_equiv_scheduler s saa\<rbrakk> \<Longrightarrow> (P and globals_equiv (swap_things sa s)) saa
 2. \<And>sa rv saa. \<lbrakk>\<lbrace>P and globals_equiv (swap_things sa s)\<rbrace> f \<lbrace>\<lambda>_. globals_equiv (swap_things sa s)\<rbrace>; globals_equiv (swap_things sa s) saa\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s saa proof (prove)
goal:
No subgoals!