theory ArchScheduler_IF

lemma thread_set_scheduler_affects_equiv[Scheduler_IF_assms, wp]:
  "\<lbrace>(\<lambda>s. x \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag x \<notin> reads_scheduler aag l) and
    (\<lambda>s. x = idle_thread s \<longrightarrow> tc = idle_context s) and scheduler_affects_equiv aag l st\<rbrace>
   thread_set (tcb_arch_update (arch_tcb_context_set tc)) x
   \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>" apply (simp add: thread_set_def) apply (wp set_object_wp) apply (intro impI conjI) apply (case_tac "x \<noteq> idle_thread s",simp_all) apply (clarsimp simp: scheduler_affects_equiv_def get_tcb_def scheduler_globals_frame_equiv_def
                  split: option.splits kernel_object.splits) apply (clarsimp simp: arch_scheduler_affects_equiv_def) apply (elim states_equiv_forE equiv_forE) apply (rule states_equiv_forI,simp_all add: equiv_for_def equiv_asids_def equiv_asid_def) apply (clarsimp simp: obj_at_def) apply (clarsimp simp: idle_context_def get_tcb_def
                  split: option.splits kernel_object.splits) apply (subst arch_tcb_update_aux) apply simp apply (subgoal_tac "s = (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)", simp) apply (rule state.equality) apply (rule ext) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. x \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag x \<notin> reads_scheduler aag l) and (\<lambda>s. x = idle_thread s \<longrightarrow> tc = idle_context s) and scheduler_affects_equiv aag l st\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) x \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. x \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag x \<notin> reads_scheduler aag l) and (\<lambda>s. x = idle_thread s \<longrightarrow> tc = idle_context s) and scheduler_affects_equiv aag l st\<rbrace> do tcb <- gets_the (get_tcb x);
set_object x (TCB (tcb_arch_update (arch_tcb_context_set tc) tcb))
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. x \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag x \<notin> reads_scheduler aag l) and (\<lambda>s. x = idle_thread s \<longrightarrow> tc = idle_context s) and scheduler_affects_equiv aag l st) s \<Longrightarrow> get_tcb x s \<noteq> None \<longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb x s))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>((\<lambda>s. x \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag x \<notin> reads_scheduler aag l) and (\<lambda>s. x = idle_thread s \<longrightarrow> tc = idle_context s) and scheduler_affects_equiv aag l st) s; get_tcb x s \<noteq> None\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb x s))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> scheduler_affects_equiv aag l st s; \<exists>y. get_tcb x s = Some y; x \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb x s))))\<rparr>)
 2. \<And>s. \<lbrakk>tc = idle_context s \<and> scheduler_affects_equiv aag l st s; \<exists>y. get_tcb (idle_thread s) s = Some y; x = idle_thread s\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set (idle_context s)) (the (get_tcb (idle_thread s) s))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x2a. \<lbrakk>x \<noteq> idle_thread s; pasObjectAbs aag x \<notin> reads_scheduler aag l; 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) st s; (pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> cur_thread st = cur_thread s \<and> scheduler_action st = scheduler_action s \<and> work_units_completed st = work_units_completed s \<and> idle_thread st = idle_thread s \<and> (cur_thread st \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_equiv st s); kheap s x = Some (TCB x2a)\<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) st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) x2a))\<rparr>) \<and> ((pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> cur_thread s \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_equiv st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) x2a))\<rparr>))
 2. \<And>s. \<lbrakk>tc = idle_context s \<and> scheduler_affects_equiv aag l st s; \<exists>y. get_tcb (idle_thread s) s = Some y; x = idle_thread s\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set (idle_context s)) (the (get_tcb (idle_thread s) s))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x2a. \<lbrakk>x \<noteq> idle_thread s; pasObjectAbs aag x \<notin> reads_scheduler aag l; 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) st s; (pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> cur_thread st = cur_thread s \<and> scheduler_action st = scheduler_action s \<and> work_units_completed st = work_units_completed s \<and> idle_thread st = idle_thread s \<and> (cur_thread st \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state st) = exclusive_state (machine_state s)); kheap s x = Some (TCB x2a)\<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) st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) x2a))\<rparr>)
 2. \<And>s. \<lbrakk>tc = idle_context s \<and> scheduler_affects_equiv aag l st s; \<exists>y. get_tcb (idle_thread s) s = Some y; x = idle_thread s\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set (idle_context s)) (the (get_tcb (idle_thread s) s))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x2a. \<lbrakk>x \<noteq> idle_thread s; pasObjectAbs aag x \<notin> reads_scheduler aag l; (pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> cur_thread st = cur_thread s \<and> scheduler_action st = scheduler_action s \<and> work_units_completed st = work_units_completed s \<and> idle_thread st = idle_thread s \<and> (cur_thread st \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state st) = exclusive_state (machine_state s)); kheap s x = Some (TCB x2a); equiv_machine_state (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (machine_state st) (machine_state s); equiv_asids (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) st s; \<And>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> kheap st x = kheap s x; \<And>x. ((\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) \<circ> fst) x \<Longrightarrow> cdt st x = cdt s x; \<And>x. ((\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) \<circ> fst) x \<Longrightarrow> cdt_list st x = cdt_list s x; \<And>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> ekheap st x = ekheap s x; \<And>x. ((\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) \<circ> fst) x \<Longrightarrow> is_original_cap st x = is_original_cap s x; \<And>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> interrupt_states st x = interrupt_states s x; \<And>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> interrupt_irq_node st x = interrupt_irq_node s x; \<And>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l \<Longrightarrow> ready_queues st x = ready_queues s x\<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) st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) x2a))\<rparr>)
 2. \<And>s. \<lbrakk>tc = idle_context s \<and> scheduler_affects_equiv aag l st s; \<exists>y. get_tcb (idle_thread s) s = Some y; x = idle_thread s\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set (idle_context s)) (the (get_tcb (idle_thread s) s))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x2a. \<lbrakk>x \<noteq> idle_thread s; pasObjectAbs aag x \<notin> reads_scheduler aag l; (pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> cur_thread st = cur_thread s \<and> scheduler_action st = scheduler_action s \<and> work_units_completed st = work_units_completed s \<and> idle_thread st = idle_thread s \<and> (cur_thread st \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state st) = exclusive_state (machine_state s)); kheap s x = Some (TCB x2a); (\<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> underlying_memory (machine_state st) x = underlying_memory (machine_state s) x) \<and> (\<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> device_state (machine_state st) x = device_state (machine_state s) x); \<forall>asid. asid \<noteq> 0 \<and> pasASIDAbs aag asid \<in> reads_scheduler aag l \<longrightarrow> asid_table st (asid_high_bits_of asid) = asid_table s (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table st (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr st = typ_at (AArch AASIDPool) pool_ptr s \<and> (\<forall>asid_pool asid_pool'. kheap st pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))); \<And>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> kheap st x = kheap s x; \<And>x. pasObjectAbs aag (fst x) \<in> reads_scheduler aag l \<Longrightarrow> cdt st x = cdt s x; \<And>x. pasObjectAbs aag (fst x) \<in> reads_scheduler aag l \<Longrightarrow> cdt_list st x = cdt_list s x; \<And>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> ekheap st x = ekheap s x; \<And>x. pasObjectAbs aag (fst x) \<in> reads_scheduler aag l \<Longrightarrow> is_original_cap st x = is_original_cap s x; \<And>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> interrupt_states st x = interrupt_states s x; \<And>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> interrupt_irq_node st x = interrupt_irq_node s x; \<And>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l \<Longrightarrow> ready_queues st x = ready_queues s x\<rbrakk> \<Longrightarrow> \<forall>asid. asid \<noteq> 0 \<and> pasASIDAbs aag asid \<in> reads_scheduler aag l \<longrightarrow> (\<forall>pool_ptr. (pool_ptr = x \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some x \<longrightarrow> typ_at (AArch AASIDPool) x s = typ_at (AArch AASIDPool) x (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) x2a))\<rparr>)) \<and> (pool_ptr \<noteq> x \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> typ_at (AArch AASIDPool) pool_ptr s = typ_at (AArch AASIDPool) pool_ptr (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) x2a))\<rparr>)))
 2. \<And>s. \<lbrakk>tc = idle_context s \<and> scheduler_affects_equiv aag l st s; \<exists>y. get_tcb (idle_thread s) s = Some y; x = idle_thread s\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set (idle_context s)) (the (get_tcb (idle_thread s) s))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>tc = idle_context s \<and> scheduler_affects_equiv aag l st s; \<exists>y. get_tcb (idle_thread s) s = Some y; x = idle_thread s\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set (idle_context s)) (the (get_tcb (idle_thread s) s))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set (arch_tcb_context_get (tcb_arch y))) y))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set (arch_tcb_context_get (tcb_arch y)) (tcb_arch y)\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> s = s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr> proof (prove)
goal (11 subgoals):
 1. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> kheap s = kheap (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 2. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> cdt s = cdt (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 3. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> is_original_cap s = is_original_cap (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 4. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> cur_thread s = cur_thread (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 5. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> idle_thread s = idle_thread (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 6. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> machine_state s = machine_state (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 7. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> interrupt_irq_node s = interrupt_irq_node (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 8. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> interrupt_states s = interrupt_states (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 9. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> arch_state s = arch_state (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 10. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> exst s = exst (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>s y xa. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> kheap s xa = kheap (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>) xa
 2. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> cdt s = cdt (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 3. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> is_original_cap s = is_original_cap (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 4. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> cur_thread s = cur_thread (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 5. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> idle_thread s = idle_thread (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 6. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> machine_state s = machine_state (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 7. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> interrupt_irq_node s = interrupt_irq_node (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 8. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> interrupt_states s = interrupt_states (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 9. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> arch_state s = arch_state (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
 10. \<And>s y. \<lbrakk>x = idle_thread s; kheap s (idle_thread s) = Some (TCB y); tc = arch_tcb_context_get (tcb_arch y); scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> exst s = exst (s\<lparr>kheap := (kheap s)(idle_thread s \<mapsto> TCB y)\<rparr>)
A total of 11 subgoals... proof (prove)
goal:
No subgoals!