theory Scheduler_IF

lemma scheduler_affects_equiv_trans[elim]:
  "\<lbrakk> scheduler_affects_equiv aag l s s'; scheduler_equiv aag s s';
     scheduler_affects_equiv aag l s' s''; scheduler_equiv aag s' s'' \<rbrakk>
     \<Longrightarrow> scheduler_affects_equiv aag l s s''" apply (simp add: scheduler_affects_equiv_def scheduler_equiv_trans[where s'=s'])+ apply clarify apply (rule conjI) apply (rule states_equiv_for_trans[where t=s']) apply simp+ apply (clarsimp simp: scheduler_globals_frame_equiv_trans[where s'=s']
                        scheduler_equiv_def domain_fields_equiv_def) apply (erule (1) arch_scheduler_affects_equiv_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scheduler_affects_equiv aag l s s'; scheduler_equiv aag s s'; scheduler_affects_equiv aag l s' s''; scheduler_equiv aag s' s''\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l s s'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s' \<and> ((pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> cur_thread s = cur_thread s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> idle_thread s = idle_thread s' \<and> (cur_thread s \<noteq> idle_thread s' \<longrightarrow> arch_scheduler_affects_equiv s s')); scheduler_equiv aag s s'; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s'' \<and> ((pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s'') \<longrightarrow> cur_thread s' = cur_thread s'' \<and> scheduler_action s' = scheduler_action s'' \<and> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> idle_thread s' = idle_thread s'' \<and> (cur_thread s' \<noteq> idle_thread s'' \<longrightarrow> arch_scheduler_affects_equiv s' s'')); scheduler_equiv aag s' s''\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'' \<and> ((pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s'') \<longrightarrow> cur_thread s = cur_thread s'' \<and> scheduler_action s = scheduler_action s'' \<and> work_units_completed s = work_units_completed s'' \<and> scheduler_globals_frame_equiv s s'' \<and> idle_thread s = idle_thread s'' \<and> (cur_thread s \<noteq> idle_thread s'' \<longrightarrow> arch_scheduler_affects_equiv s s'')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scheduler_equiv aag s s'; scheduler_equiv aag s' s''; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'; (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> cur_thread s = cur_thread s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> idle_thread s = idle_thread s' \<and> (cur_thread s \<noteq> idle_thread s' \<longrightarrow> arch_scheduler_affects_equiv s s'); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s''; (pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s'') \<longrightarrow> cur_thread s' = cur_thread s'' \<and> scheduler_action s' = scheduler_action s'' \<and> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> idle_thread s' = idle_thread s'' \<and> (cur_thread s' \<noteq> idle_thread s'' \<longrightarrow> arch_scheduler_affects_equiv s' s'')\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'' \<and> ((pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s'') \<longrightarrow> cur_thread s = cur_thread s'' \<and> scheduler_action s = scheduler_action s'' \<and> work_units_completed s = work_units_completed s'' \<and> scheduler_globals_frame_equiv s s'' \<and> idle_thread s = idle_thread s'' \<and> (cur_thread s \<noteq> idle_thread s'' \<longrightarrow> arch_scheduler_affects_equiv s s'')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>scheduler_equiv aag s s'; scheduler_equiv aag s' s''; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'; (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> cur_thread s = cur_thread s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> idle_thread s = idle_thread s' \<and> (cur_thread s \<noteq> idle_thread s' \<longrightarrow> arch_scheduler_affects_equiv s s'); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s''; (pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s'') \<longrightarrow> cur_thread s' = cur_thread s'' \<and> scheduler_action s' = scheduler_action s'' \<and> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> idle_thread s' = idle_thread s'' \<and> (cur_thread s' \<noteq> idle_thread s'' \<longrightarrow> arch_scheduler_affects_equiv s' s'')\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s''
 2. \<lbrakk>scheduler_equiv aag s s'; scheduler_equiv aag s' s''; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'; (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> cur_thread s = cur_thread s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> idle_thread s = idle_thread s' \<and> (cur_thread s \<noteq> idle_thread s' \<longrightarrow> arch_scheduler_affects_equiv s s'); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s''; (pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s'') \<longrightarrow> cur_thread s' = cur_thread s'' \<and> scheduler_action s' = scheduler_action s'' \<and> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> idle_thread s' = idle_thread s'' \<and> (cur_thread s' \<noteq> idle_thread s'' \<longrightarrow> arch_scheduler_affects_equiv s' s'')\<rbrakk> \<Longrightarrow> (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s'') \<longrightarrow> cur_thread s = cur_thread s'' \<and> scheduler_action s = scheduler_action s'' \<and> work_units_completed s = work_units_completed s'' \<and> scheduler_globals_frame_equiv s s'' \<and> idle_thread s = idle_thread s'' \<and> (cur_thread s \<noteq> idle_thread s'' \<longrightarrow> arch_scheduler_affects_equiv s s'') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>scheduler_equiv aag s s'; scheduler_equiv aag s' s''; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'; (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> cur_thread s = cur_thread s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> idle_thread s = idle_thread s' \<and> (cur_thread s \<noteq> idle_thread s' \<longrightarrow> arch_scheduler_affects_equiv s s'); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s''; (pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s'') \<longrightarrow> cur_thread s' = cur_thread s'' \<and> scheduler_action s' = scheduler_action s'' \<and> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> idle_thread s' = idle_thread s'' \<and> (cur_thread s' \<noteq> idle_thread s'' \<longrightarrow> arch_scheduler_affects_equiv s' s'')\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'
 2. \<lbrakk>scheduler_equiv aag s s'; scheduler_equiv aag s' s''; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'; (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> cur_thread s = cur_thread s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> idle_thread s = idle_thread s' \<and> (cur_thread s \<noteq> idle_thread s' \<longrightarrow> arch_scheduler_affects_equiv s s'); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s''; (pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s'') \<longrightarrow> cur_thread s' = cur_thread s'' \<and> scheduler_action s' = scheduler_action s'' \<and> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> idle_thread s' = idle_thread s'' \<and> (cur_thread s' \<noteq> idle_thread s'' \<longrightarrow> arch_scheduler_affects_equiv s' s'')\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s''
 3. \<lbrakk>scheduler_equiv aag s s'; scheduler_equiv aag s' s''; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'; (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> cur_thread s = cur_thread s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> idle_thread s = idle_thread s' \<and> (cur_thread s \<noteq> idle_thread s' \<longrightarrow> arch_scheduler_affects_equiv s s'); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s''; (pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s'') \<longrightarrow> cur_thread s' = cur_thread s'' \<and> scheduler_action s' = scheduler_action s'' \<and> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> idle_thread s' = idle_thread s'' \<and> (cur_thread s' \<noteq> idle_thread s'' \<longrightarrow> arch_scheduler_affects_equiv s' s'')\<rbrakk> \<Longrightarrow> (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s'') \<longrightarrow> cur_thread s = cur_thread s'' \<and> scheduler_action s = scheduler_action s'' \<and> work_units_completed s = work_units_completed s'' \<and> scheduler_globals_frame_equiv s s'' \<and> idle_thread s = idle_thread s'' \<and> (cur_thread s \<noteq> idle_thread s'' \<longrightarrow> arch_scheduler_affects_equiv s s'') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scheduler_equiv aag s s'; scheduler_equiv aag s' s''; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'; (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> cur_thread s = cur_thread s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> idle_thread s = idle_thread s' \<and> (cur_thread s \<noteq> idle_thread s' \<longrightarrow> arch_scheduler_affects_equiv s s'); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s''; (pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s'') \<longrightarrow> cur_thread s' = cur_thread s'' \<and> scheduler_action s' = scheduler_action s'' \<and> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> idle_thread s' = idle_thread s'' \<and> (cur_thread s' \<noteq> idle_thread s'' \<longrightarrow> arch_scheduler_affects_equiv s' s'')\<rbrakk> \<Longrightarrow> (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s'') \<longrightarrow> cur_thread s = cur_thread s'' \<and> scheduler_action s = scheduler_action s'' \<and> work_units_completed s = work_units_completed s'' \<and> scheduler_globals_frame_equiv s s'' \<and> idle_thread s = idle_thread s'' \<and> (cur_thread s \<noteq> idle_thread s'' \<longrightarrow> arch_scheduler_affects_equiv s s'') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s''; 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''); reads_scheduler_cur_domain aag l s''; cur_thread s'' \<noteq> idle_thread s''; cur_thread s = cur_thread s''; scheduler_action s = scheduler_action s''; work_units_completed s = work_units_completed s''; scheduler_globals_frame_equiv s s'; arch_scheduler_affects_equiv s s'; cur_thread s' = cur_thread s''; scheduler_action s' = scheduler_action s''; work_units_completed s' = work_units_completed s''; scheduler_globals_frame_equiv s' s''; arch_scheduler_affects_equiv s' s''\<rbrakk> \<Longrightarrow> arch_scheduler_affects_equiv s s'' proof (prove)
goal:
No subgoals!