theory ArchCNode_IF

lemma set_object_globals_equiv:
  "\<lbrace>globals_equiv s and (\<lambda>s. ptr \<noteq> arm_global_pd (arch_state s)) and
    (\<lambda>t. ptr = idle_thread t
         \<longrightarrow> (\<forall>tcb. kheap t (idle_thread t) = Some (TCB tcb)
                    \<longrightarrow> (\<exists>tcb'. obj = (TCB tcb')
                              \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and>
             (\<forall>tcb'. obj = (TCB tcb') \<longrightarrow> tcb_at (idle_thread t) t))\<rbrace>
   set_object ptr obj
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" apply (wpsimp wp: set_object_wp) apply (case_tac "ptr = idle_thread sa") apply (clarsimp simp: globals_equiv_def idle_equiv_def tcb_at_def2) apply (intro impI conjI allI notI iffI | clarsimp)+ apply (clarsimp simp: globals_equiv_def idle_equiv_def tcb_at_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and (\<lambda>s. ptr \<noteq> arm_global_pd (arch_state s)) and (\<lambda>t. ptr = idle_thread t \<longrightarrow> (\<forall>tcb. kheap t (idle_thread t) = Some (TCB tcb) \<longrightarrow> (\<exists>tcb'. obj = TCB tcb' \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> (\<forall>tcb'. obj = TCB tcb' \<longrightarrow> tcb_at (idle_thread t) t))\<rbrace> set_object ptr obj \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>globals_equiv s sa; ptr \<noteq> arm_global_pd (arch_state sa); ptr = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> (\<exists>tcb'. obj = TCB tcb' \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> ((\<exists>tcb'. obj = TCB tcb') \<longrightarrow> tcb_at (idle_thread sa) sa)\<rbrakk> \<Longrightarrow> globals_equiv s (sa\<lparr>kheap := (kheap sa)(ptr \<mapsto> obj)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>globals_equiv s sa; ptr \<noteq> arm_global_pd (arch_state sa); ptr = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> (\<exists>tcb'. obj = TCB tcb' \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> ((\<exists>tcb'. obj = TCB tcb') \<longrightarrow> tcb_at (idle_thread sa) sa); ptr = idle_thread sa\<rbrakk> \<Longrightarrow> globals_equiv s (sa\<lparr>kheap := (kheap sa)(ptr \<mapsto> obj)\<rparr>)
 2. \<And>sa. \<lbrakk>globals_equiv s sa; ptr \<noteq> arm_global_pd (arch_state sa); ptr = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> (\<exists>tcb'. obj = TCB tcb' \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> ((\<exists>tcb'. obj = TCB tcb') \<longrightarrow> tcb_at (idle_thread sa) sa); ptr \<noteq> idle_thread sa\<rbrakk> \<Longrightarrow> globals_equiv s (sa\<lparr>kheap := (kheap sa)(ptr \<mapsto> obj)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>idle_thread sa \<noteq> arm_global_pd (arch_state sa); ptr = idle_thread sa; arm_global_pd (arch_state s) = arm_global_pd (arch_state sa); \<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> (\<exists>tcb'. obj = TCB tcb' \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); (\<exists>tcb'. obj = TCB tcb') \<longrightarrow> (\<exists>tcb. kheap sa (idle_thread sa) = Some (TCB tcb)); kheap s (arm_global_pd (arch_state sa)) = kheap sa (arm_global_pd (arch_state sa)); cur_thread sa \<noteq> idle_thread sa \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state sa); idle_thread s = idle_thread sa; \<forall>tcb. kheap s (idle_thread sa) = Some (TCB tcb) \<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 tcb')); (\<exists>tcb. kheap s (idle_thread sa) = Some (TCB tcb)) = (\<exists>tcb. kheap sa (idle_thread sa) = Some (TCB tcb)); cur_thread s = cur_thread sa; dom (device_state (machine_state s)) = dom (device_state (machine_state sa))\<rbrakk> \<Longrightarrow> (\<forall>tcb. kheap s (idle_thread sa) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. obj = TCB tcb' \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> (\<exists>tcb. kheap sa (idle_thread sa) = Some (TCB tcb)) = (\<exists>tcb. obj = TCB tcb)
 2. \<And>sa. \<lbrakk>globals_equiv s sa; ptr \<noteq> arm_global_pd (arch_state sa); ptr = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> (\<exists>tcb'. obj = TCB tcb' \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> ((\<exists>tcb'. obj = TCB tcb') \<longrightarrow> tcb_at (idle_thread sa) sa); ptr \<noteq> idle_thread sa\<rbrakk> \<Longrightarrow> globals_equiv s (sa\<lparr>kheap := (kheap sa)(ptr \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>globals_equiv s sa; ptr \<noteq> arm_global_pd (arch_state sa); ptr \<noteq> idle_thread sa\<rbrakk> \<Longrightarrow> globals_equiv s (sa\<lparr>kheap := (kheap sa)(ptr \<mapsto> obj)\<rparr>) proof (prove)
goal:
No subgoals!