theory Scheduler_IF

lemma scheduler_equiv_lift':
  assumes s: "\<And>st. \<lbrace>P and globals_equiv_scheduler st\<rbrace>  f \<lbrace>\<lambda>_.(globals_equiv_scheduler st)\<rbrace>"
  assumes d: "\<And>Q. \<lbrace>P and (\<lambda>s. Q (cur_domain s))\<rbrace> f \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>"
  assumes i: "\<And>P. f \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace>"
  assumes e: "\<And>Q. \<lbrace>P and domain_fields Q\<rbrace> f \<lbrace>\<lambda>_. domain_fields Q\<rbrace>"
  assumes g: "\<And>P. f \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>"
  assumes f: "\<And>st. \<lbrace>P and silc_dom_equiv aag st\<rbrace> f \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace>"
  shows "\<lbrace>P and scheduler_equiv aag st\<rbrace> f \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>" apply (simp add: scheduler_equiv_def[abs_def] domain_fields_equiv_def) apply (rule hoare_pre) apply (wp d e s i f g) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and scheduler_equiv aag st\<rbrace> f \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and (\<lambda>s'. cur_domain st = cur_domain s' \<and> domain_time st = domain_time s' \<and> domain_index st = domain_index s' \<and> domain_list st = domain_list s' \<and> idle_thread st = idle_thread s' \<and> globals_equiv_scheduler st s' \<and> silc_dom_equiv aag st s' \<and> equiv_irq_state (machine_state st) (machine_state s'))\<rbrace> f \<lbrace>\<lambda>_ s'. cur_domain st = cur_domain s' \<and> domain_time st = domain_time s' \<and> domain_index st = domain_index s' \<and> domain_list st = domain_list s' \<and> idle_thread st = idle_thread s' \<and> globals_equiv_scheduler st s' \<and> silc_dom_equiv aag st s' \<and> equiv_irq_state (machine_state st) (machine_state s')\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>_ s'. cur_domain st = cur_domain s' \<and> domain_time st = domain_time s' \<and> domain_index st = domain_index s' \<and> domain_list st = domain_list s' \<and> idle_thread st = idle_thread s' \<and> globals_equiv_scheduler st s' \<and> silc_dom_equiv aag st s' \<and> equiv_irq_state (machine_state st) (machine_state s')\<rbrace>
 2. \<And>s. (P and (\<lambda>s'. cur_domain st = cur_domain s' \<and> domain_time st = domain_time s' \<and> domain_index st = domain_index s' \<and> domain_list st = domain_list s' \<and> idle_thread st = idle_thread s' \<and> globals_equiv_scheduler st s' \<and> silc_dom_equiv aag st s' \<and> equiv_irq_state (machine_state st) (machine_state s'))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (P and (\<lambda>s'. cur_domain st = cur_domain s' \<and> domain_time st = domain_time s' \<and> domain_index st = domain_index s' \<and> domain_list st = domain_list s' \<and> idle_thread st = idle_thread s' \<and> globals_equiv_scheduler st s' \<and> silc_dom_equiv aag st s' \<and> equiv_irq_state (machine_state st) (machine_state s'))) s \<Longrightarrow> (P and (\<lambda>s. cur_domain st = cur_domain s)) s \<and> (P and (\<lambda>s. domain_time st = domain_time s)) s \<and> (P and (\<lambda>s. domain_index st = domain_index s)) s \<and> (P and (\<lambda>s. domain_list st = domain_list s)) s \<and> idle_thread st = idle_thread s \<and> (P and globals_equiv_scheduler st) s \<and> (P and silc_dom_equiv aag st) s \<and> equiv_irq_state (machine_state st) (machine_state s) proof (prove)
goal:
No subgoals!