theory ArchArch_IF

lemma thread_set_globals_equiv:
  "(\<And>tcb. arch_tcb_context_get (tcb_arch (f tcb)) = arch_tcb_context_get (tcb_arch tcb))
   \<Longrightarrow> \<lbrace>globals_equiv s and valid_arch_state\<rbrace> thread_set f tptr \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding thread_set_def apply (wp set_object_globals_equiv) apply simp apply (intro impI conjI allI) apply (fastforce simp: valid_arch_state_def obj_at_def get_tcb_def)+ apply (clarsimp simp: get_tcb_def tcb_at_def2 split: kernel_object.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. arch_tcb_context_get (tcb_arch (f tcb)) = arch_tcb_context_get (tcb_arch tcb)) \<Longrightarrow> \<lbrace>globals_equiv s and valid_arch_state\<rbrace> thread_set f tptr \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. arch_tcb_context_get (tcb_arch (f tcb)) = arch_tcb_context_get (tcb_arch tcb)) \<Longrightarrow> \<lbrace>globals_equiv s and valid_arch_state\<rbrace> do tcb <- gets_the $ get_tcb tptr;
set_object tptr $ TCB $ f tcb
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>\<And>tcb. arch_tcb_context_get (tcb_arch (f tcb)) = arch_tcb_context_get (tcb_arch tcb); (globals_equiv s and valid_arch_state) sa\<rbrakk> \<Longrightarrow> get_tcb tptr sa \<noteq> None \<longrightarrow> (globals_equiv s and (\<lambda>s. tptr \<noteq> arm_global_pd (arch_state s)) and (\<lambda>t. tptr = idle_thread t \<longrightarrow> (\<forall>tcb. kheap t (idle_thread t) = Some (TCB tcb) \<longrightarrow> (\<exists>tcb'. (TCB $ f (the (get_tcb tptr sa))) = TCB tcb' \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> (\<forall>tcb'. (TCB $ f (the (get_tcb tptr sa))) = TCB tcb' \<longrightarrow> tcb_at (idle_thread t) t))) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>\<And>tcb. arch_tcb_context_get (tcb_arch (f tcb)) = arch_tcb_context_get (tcb_arch tcb); globals_equiv s sa \<and> valid_arch_state sa\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb tptr sa = Some y) \<longrightarrow> tptr \<noteq> arm_global_pd (arch_state sa) \<and> (tptr = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch (the (get_tcb (idle_thread sa) sa)))) \<and> tcb_at (idle_thread sa) sa) proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrakk>\<And>tcb. arch_tcb_context_get (tcb_arch (f tcb)) = arch_tcb_context_get (tcb_arch tcb); globals_equiv s sa \<and> valid_arch_state sa; \<exists>y. get_tcb tptr sa = Some y\<rbrakk> \<Longrightarrow> tptr \<noteq> arm_global_pd (arch_state sa)
 2. \<And>sa tcb. \<lbrakk>\<And>tcb. arch_tcb_context_get (tcb_arch (f tcb)) = arch_tcb_context_get (tcb_arch tcb); globals_equiv s sa \<and> valid_arch_state sa; \<exists>y. get_tcb tptr sa = Some y; tptr = idle_thread sa; kheap sa (idle_thread sa) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch (the (get_tcb (idle_thread sa) sa)))
 3. \<And>sa. \<lbrakk>\<And>tcb. arch_tcb_context_get (tcb_arch (f tcb)) = arch_tcb_context_get (tcb_arch tcb); globals_equiv s sa \<and> valid_arch_state sa; \<exists>y. get_tcb tptr sa = Some y; tptr = idle_thread sa\<rbrakk> \<Longrightarrow> tcb_at (idle_thread sa) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>\<And>tcb. arch_tcb_context_get (tcb_arch (f tcb)) = arch_tcb_context_get (tcb_arch tcb); globals_equiv s sa \<and> valid_arch_state sa; \<exists>y. get_tcb tptr sa = Some y; tptr = idle_thread sa\<rbrakk> \<Longrightarrow> tcb_at (idle_thread sa) sa proof (prove)
goal:
No subgoals!