theory Scheduler_IF

lemma cur_thread_update_not_subject_reads_respects_scheduler:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
    "reads_respects_scheduler aag l (\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l \<and>
                                         pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))
                              (modify (cur_thread_update (\<lambda>_. t)))" apply (rule ev_modify) apply (clarsimp simp: scheduler_affects_equiv_def scheduler_equiv_def domain_fields_equiv_def
                        globals_equiv_scheduler_def states_equiv_for_def equiv_for_def
                        equiv_asids_def scheduler_globals_frame_equiv_def idle_equiv_def) apply (blast dest: domains_distinct[THEN pas_domains_distinct_inj]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l \<and> pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)) (modify (cur_thread_update (\<lambda>_. t))) proof (prove)
goal (1 subgoal):
 1. \<And>s ta. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l \<and> pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s); pasObjectAbs aag t \<notin> reads_scheduler aag l \<and> pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain ta); scheduler_affects_equiv aag l s ta; scheduler_equiv aag s ta\<rbrakk> \<Longrightarrow> scheduler_equiv aag (s\<lparr>cur_thread := t\<rparr>) (ta\<lparr>cur_thread := t\<rparr>) \<and> scheduler_affects_equiv aag l (s\<lparr>cur_thread := t\<rparr>) (ta\<lparr>cur_thread := t\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ta. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain ta); \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> kheap s x = kheap ta x; cur_domain s = cur_domain ta; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state ta) x; domain_time s = domain_time ta; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> device_state (machine_state s) x = device_state (machine_state ta) x; domain_index s = domain_index ta; \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. cdt s (a, b) = cdt ta (a, b)); domain_list s = domain_list ta; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> ekheap s x = ekheap ta x; \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. cdt_list s (a, b) = cdt_list ta (a, b)); arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. is_original_cap s (a, b) = is_original_cap ta (a, b)); idle_thread s = cur_thread ta; \<forall>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<longrightarrow> interrupt_states s x = interrupt_states ta x; \<forall>tcb. kheap s (cur_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (cur_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); \<forall>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<longrightarrow> interrupt_irq_node s x = interrupt_irq_node ta x; tcb_at (cur_thread ta) s = tcb_at (cur_thread ta) ta; \<forall>x. (\<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) \<longrightarrow> ready_queues s x = ready_queues ta x; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); \<forall>asid. asid \<noteq> 0 \<and> pasASIDAbs aag asid \<in> reads_scheduler aag l \<longrightarrow> equiv_asid asid s ta; silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); reads_scheduler_cur_domain aag l ta; t \<noteq> cur_thread ta; idle_thread ta = cur_thread ta; scheduler_action s = scheduler_action ta; work_units_completed s = work_units_completed ta; \<not> arch_scheduler_affects_equiv s ta; cur_thread s = cur_thread ta\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!