theory Scheduler_IF

lemma scheduler_affects_equiv_sym[elim]:
  "scheduler_affects_equiv aag l s s' \<Longrightarrow> scheduler_affects_equiv aag l s' s" apply (simp add: scheduler_affects_equiv_def) 
  (* faster than the one-liner *)
   apply (clarsimp simp: scheduler_globals_frame_equiv_sym states_equiv_for_sym silc_dom_equiv_sym) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_affects_equiv aag l s s' \<Longrightarrow> scheduler_affects_equiv aag l s' s proof (prove)
goal (1 subgoal):
 1. 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')) \<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. 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')) \<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>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'); pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s\<rbrakk> \<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:
No subgoals!