theory ArchScheduler_IF

lemma thread_set_context_globals_equiv[Scheduler_IF_assms]:
  "\<lbrace>(\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and invs and globals_equiv st\<rbrace>
   thread_set (tcb_arch_update (arch_tcb_context_set tc)) t
   \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>" apply (clarsimp simp: thread_set_def) apply (wpsimp wp: set_object_wp) apply (subgoal_tac "t \<noteq> arm_global_pd (arch_state s)") apply (clarsimp simp: idle_equiv_def globals_equiv_def tcb_at_def2 get_tcb_def idle_context_def) apply (clarsimp split: option.splits kernel_object.splits) apply (drule arm_global_pd_not_tcb[OF invs_arch_state]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and invs and globals_equiv st\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>rv. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and invs and globals_equiv st\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb_arch_update (arch_tcb_context_set tc) tcb))
od \<lbrace>\<lambda>rv. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>t = idle_thread s \<longrightarrow> tc = idle_context s; invs s; globals_equiv st s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> globals_equiv st (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) y))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>t = idle_thread s \<longrightarrow> tc = idle_context s; invs s; globals_equiv st s; get_tcb t s = Some y; t \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> globals_equiv st (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) y))\<rparr>)
 2. \<And>s y. \<lbrakk>t = idle_thread s \<longrightarrow> tc = idle_context s; invs s; globals_equiv st s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> t \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>tc = arch_tcb_context_get (tcb_arch y); invs s; (case kheap s (idle_thread s) of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | Some _ \<Rightarrow> None) = Some y; idle_thread s \<noteq> arm_global_pd (arch_state s); arm_global_pd (arch_state st) = arm_global_pd (arch_state s); kheap st (arm_global_pd (arch_state s)) = kheap s (arm_global_pd (arch_state s)); cur_thread s \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state st) = exclusive_state (machine_state s); idle_thread st = idle_thread s; \<forall>tcb. kheap st (idle_thread s) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap s (idle_thread s) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); (\<exists>tcb. kheap st (idle_thread s) = Some (TCB tcb)) = (\<exists>tcb. kheap s (idle_thread s) = Some (TCB tcb)); cur_thread st = cur_thread s; dom (device_state (machine_state st)) = dom (device_state (machine_state s)); t = idle_thread s\<rbrakk> \<Longrightarrow> (\<forall>tcb. kheap st (idle_thread s) = Some (TCB tcb) \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch y)) \<and> (\<exists>tcb. kheap s (idle_thread s) = Some (TCB tcb))
 2. \<And>s y. \<lbrakk>t = idle_thread s \<longrightarrow> tc = idle_context s; invs s; globals_equiv st s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> t \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>t = idle_thread s \<longrightarrow> tc = idle_context s; invs s; globals_equiv st s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> t \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>t = idle_thread s \<longrightarrow> tc = idle_context s; globals_equiv st s; get_tcb t s = Some y; get_tcb (arm_global_pd (arch_state s)) s = None\<rbrakk> \<Longrightarrow> t \<noteq> arm_global_pd (arch_state s) proof (prove)
goal:
No subgoals!