theory Scheduler_IF

lemma scheduler_equiv_trans[elim]:
  "\<lbrakk> scheduler_equiv aag s s'; scheduler_equiv aag s' s'' \<rbrakk>
     \<Longrightarrow> scheduler_equiv aag s s''" apply (simp add: scheduler_equiv_def domain_fields_equiv_def) apply clarify apply (rule conjI) apply (rule globals_equiv_scheduler_trans) apply simp+ apply (blast intro: silc_dom_equiv_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scheduler_equiv aag s s'; scheduler_equiv aag s' s''\<rbrakk> \<Longrightarrow> scheduler_equiv aag s s'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cur_domain s = cur_domain s'' \<and> domain_time s = domain_time s'' \<and> domain_index s = domain_index s'' \<and> domain_list s = domain_list s'' \<and> idle_thread s = idle_thread s'' \<and> globals_equiv_scheduler s s' \<and> silc_dom_equiv aag s s' \<and> equiv_irq_state (machine_state s) (machine_state s''); cur_domain s' = cur_domain s'' \<and> domain_time s' = domain_time s'' \<and> domain_index s' = domain_index s'' \<and> domain_list s' = domain_list s'' \<and> idle_thread s' = idle_thread s'' \<and> globals_equiv_scheduler s' s'' \<and> silc_dom_equiv aag s' s'' \<and> equiv_irq_state (machine_state s') (machine_state s'')\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s s'' \<and> silc_dom_equiv aag s s'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cur_domain s = cur_domain s''; cur_domain s' = cur_domain s''; domain_time s = domain_time s''; domain_time s' = domain_time s''; domain_index s = domain_index s''; domain_index s' = domain_index s''; domain_list s = domain_list s''; domain_list s' = domain_list s''; idle_thread s = idle_thread s''; idle_thread s' = idle_thread s''; globals_equiv_scheduler s s'; globals_equiv_scheduler s' s''; silc_dom_equiv aag s s'; equiv_irq_state (machine_state s) (machine_state s''); silc_dom_equiv aag s' s''; equiv_irq_state (machine_state s') (machine_state s'')\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s s'' \<and> silc_dom_equiv aag s s'' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cur_domain s = cur_domain s''; cur_domain s' = cur_domain s''; domain_time s = domain_time s''; domain_time s' = domain_time s''; domain_index s = domain_index s''; domain_index s' = domain_index s''; domain_list s = domain_list s''; domain_list s' = domain_list s''; idle_thread s = idle_thread s''; idle_thread s' = idle_thread s''; globals_equiv_scheduler s s'; globals_equiv_scheduler s' s''; silc_dom_equiv aag s s'; equiv_irq_state (machine_state s) (machine_state s''); silc_dom_equiv aag s' s''; equiv_irq_state (machine_state s') (machine_state s'')\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s s''
 2. \<lbrakk>cur_domain s = cur_domain s''; cur_domain s' = cur_domain s''; domain_time s = domain_time s''; domain_time s' = domain_time s''; domain_index s = domain_index s''; domain_index s' = domain_index s''; domain_list s = domain_list s''; domain_list s' = domain_list s''; idle_thread s = idle_thread s''; idle_thread s' = idle_thread s''; globals_equiv_scheduler s s'; globals_equiv_scheduler s' s''; silc_dom_equiv aag s s'; equiv_irq_state (machine_state s) (machine_state s''); silc_dom_equiv aag s' s''; equiv_irq_state (machine_state s') (machine_state s'')\<rbrakk> \<Longrightarrow> silc_dom_equiv aag s s'' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cur_domain s = cur_domain s''; cur_domain s' = cur_domain s''; domain_time s = domain_time s''; domain_time s' = domain_time s''; domain_index s = domain_index s''; domain_index s' = domain_index s''; domain_list s = domain_list s''; domain_list s' = domain_list s''; idle_thread s = idle_thread s''; idle_thread s' = idle_thread s''; globals_equiv_scheduler s s'; globals_equiv_scheduler s' s''; silc_dom_equiv aag s s'; equiv_irq_state (machine_state s) (machine_state s''); silc_dom_equiv aag s' s''; equiv_irq_state (machine_state s') (machine_state s'')\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s ?s'25
 2. \<lbrakk>cur_domain s = cur_domain s''; cur_domain s' = cur_domain s''; domain_time s = domain_time s''; domain_time s' = domain_time s''; domain_index s = domain_index s''; domain_index s' = domain_index s''; domain_list s = domain_list s''; domain_list s' = domain_list s''; idle_thread s = idle_thread s''; idle_thread s' = idle_thread s''; globals_equiv_scheduler s s'; globals_equiv_scheduler s' s''; silc_dom_equiv aag s s'; equiv_irq_state (machine_state s) (machine_state s''); silc_dom_equiv aag s' s''; equiv_irq_state (machine_state s') (machine_state s'')\<rbrakk> \<Longrightarrow> globals_equiv_scheduler ?s'25 s''
 3. \<lbrakk>cur_domain s = cur_domain s''; cur_domain s' = cur_domain s''; domain_time s = domain_time s''; domain_time s' = domain_time s''; domain_index s = domain_index s''; domain_index s' = domain_index s''; domain_list s = domain_list s''; domain_list s' = domain_list s''; idle_thread s = idle_thread s''; idle_thread s' = idle_thread s''; globals_equiv_scheduler s s'; globals_equiv_scheduler s' s''; silc_dom_equiv aag s s'; equiv_irq_state (machine_state s) (machine_state s''); silc_dom_equiv aag s' s''; equiv_irq_state (machine_state s') (machine_state s'')\<rbrakk> \<Longrightarrow> silc_dom_equiv aag s s'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cur_domain s = cur_domain s''; cur_domain s' = cur_domain s''; domain_time s = domain_time s''; domain_time s' = domain_time s''; domain_index s = domain_index s''; domain_index s' = domain_index s''; domain_list s = domain_list s''; domain_list s' = domain_list s''; idle_thread s = idle_thread s''; idle_thread s' = idle_thread s''; globals_equiv_scheduler s s'; globals_equiv_scheduler s' s''; silc_dom_equiv aag s s'; equiv_irq_state (machine_state s) (machine_state s''); silc_dom_equiv aag s' s''; equiv_irq_state (machine_state s') (machine_state s'')\<rbrakk> \<Longrightarrow> silc_dom_equiv aag s s'' proof (prove)
goal:
No subgoals!