theory Scheduler_IF

lemma asahi_ex_scheduler_affects_equiv_trans[elim]:
  "\<lbrakk> asahi_ex_scheduler_affects_equiv aag l s s'; scheduler_equiv aag s s';
     asahi_ex_scheduler_affects_equiv aag l s' s''; scheduler_equiv aag s' s'' \<rbrakk>
     \<Longrightarrow> asahi_ex_scheduler_affects_equiv aag l s s''" apply (simp add: asahi_ex_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 (auto intro: arch_scheduler_affects_equiv_trans
               simp: scheduler_globals_frame_equiv_trans[where s'=s']
                     scheduler_equiv_def domain_fields_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asahi_ex_scheduler_affects_equiv aag l s s'; scheduler_equiv aag s s'; asahi_ex_scheduler_affects_equiv aag l s' s''; scheduler_equiv aag s' s''\<rbrakk> \<Longrightarrow> asahi_ex_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> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> 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> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> 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> work_units_completed s = work_units_completed s'' \<and> scheduler_globals_frame_equiv s s'' \<and> 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> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> 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> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> 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> work_units_completed s = work_units_completed s'' \<and> scheduler_globals_frame_equiv s s'' \<and> 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> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> 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> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> 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> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> 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> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> 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> work_units_completed s = work_units_completed s'' \<and> scheduler_globals_frame_equiv s s'' \<and> 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> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> 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> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> 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> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> 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> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> 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> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> 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> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> 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> work_units_completed s = work_units_completed s'' \<and> scheduler_globals_frame_equiv s s'' \<and> 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> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> 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> work_units_completed s' = work_units_completed s'' \<and> scheduler_globals_frame_equiv s' s'' \<and> 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> work_units_completed s = work_units_completed s'' \<and> scheduler_globals_frame_equiv s s'' \<and> arch_scheduler_affects_equiv s s'' proof (prove)
goal:
No subgoals!