theory Tcb_DR

lemma dcorres_idempotent_as_user_strong:
  assumes prem: "\<And>tcb ms ref etcb P.
                 \<lbrace> \<lambda>cxt. P (transform_tcb ms ref (tcb\<lparr>tcb_arch:=arch_tcb_context_set cxt (tcb_arch tcb)\<rparr>) etcb)\<rbrace>
                 x
                 \<lbrace> \<lambda>_ cxt. P (transform_tcb ms ref (tcb\<lparr>tcb_arch:=arch_tcb_context_set cxt (tcb_arch tcb)\<rparr>) etcb)\<rbrace>"
  shows "dcorres dc \<top> (tcb_at u) (return q) (as_user u x)" supply option.case_cong[cong] if_cong[cong] apply (clarsimp simp: as_user_def) apply (clarsimp simp: corres_underlying_def bind_def split_def set_object_def get_object_def
                        return_def get_def put_def get_tcb_def gets_the_def gets_def assert_opt_def
                        tcb_at_def select_f_def valid_def
                 split: option.split Structures_A.kernel_object.split) apply (clarsimp simp: transform_def transform_current_thread_def transform_objects_def restrict_map_def) apply (rule ext) apply (clarsimp simp: map_add_def split:option.splits) apply (drule use_valid[OF _ prem]) prefer 2 apply force apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at u) (return q) (as_user u x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at u) (return q) (as_user u x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at u) (return q) (do tcb <- gets_the (get_tcb u);
(a, uc') <- select_f (x (arch_tcb_context_get (tcb_arch tcb)));
y <- KHeap_A.set_object u (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>));
return a
od) proof (prove)
goal (1 subgoal):
 1. \<And>b x2 a ba. \<lbrakk>kheap b u = Some (TCB x2); (a, ba) \<in> fst (x (arch_tcb_context_get (tcb_arch x2)))\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap b)(u \<mapsto> TCB (x2\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch x2)\<rparr>))) b) = transform b proof (prove)
goal (1 subgoal):
 1. \<And>b x2 a ba. \<lbrakk>kheap b u = Some (TCB x2); (a, ba) \<in> fst (x (arch_tcb_context_get (tcb_arch x2)))\<rbrakk> \<Longrightarrow> (\<lambda>x. if x \<noteq> idle_thread b then Some cdl_object.Untyped else None) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr (if ptr \<noteq> idle_thread b then ekheap b ptr else None)) (if ptr \<noteq> idle_thread b then if ptr = u then Some (TCB (x2\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch x2)\<rparr>)) else kheap b ptr else None)) = (\<lambda>x. if x \<noteq> idle_thread b then Some cdl_object.Untyped else None) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr (if ptr \<noteq> idle_thread b then ekheap b ptr else None)) (if ptr \<noteq> idle_thread b then kheap b ptr else None)) proof (prove)
goal (1 subgoal):
 1. \<And>b x2 a ba xa. \<lbrakk>kheap b u = Some (TCB x2); (a, ba) \<in> fst (x (arch_tcb_context_get (tcb_arch x2)))\<rbrakk> \<Longrightarrow> ((\<lambda>x. if x \<noteq> idle_thread b then Some cdl_object.Untyped else None) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr (if ptr \<noteq> idle_thread b then ekheap b ptr else None)) (if ptr \<noteq> idle_thread b then if ptr = u then Some (TCB (x2\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch x2)\<rparr>)) else kheap b ptr else None))) xa = ((\<lambda>x. if x \<noteq> idle_thread b then Some cdl_object.Untyped else None) ++ (\<lambda>ptr. map_option (transform_object (machine_state b) ptr (if ptr \<noteq> idle_thread b then ekheap b ptr else None)) (if ptr \<noteq> idle_thread b then kheap b ptr else None))) xa proof (prove)
goal (1 subgoal):
 1. \<And>b x2 a ba x2a. \<lbrakk>kheap b u = Some (TCB x2); (a, ba) \<in> fst (x (arch_tcb_context_get (tcb_arch x2))); ekheap b u = Some x2a; u \<noteq> idle_thread b\<rbrakk> \<Longrightarrow> transform_tcb (machine_state b) u (x2\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch x2)\<rparr>) x2a = transform_tcb (machine_state b) u x2 x2a proof (prove)
goal (2 subgoals):
 1. \<And>b x2 a ba x2a. \<lbrakk>kheap b u = Some (TCB x2); ekheap b u = Some x2a; u \<noteq> idle_thread b\<rbrakk> \<Longrightarrow> ?P119 b x2 a ba x2a (transform_tcb (?ms119 b x2 a ba x2a) (?ref119 b x2 a ba x2a) (?tcb119 b x2 a ba x2a\<lparr>tcb_arch := arch_tcb_context_set (arch_tcb_context_get (tcb_arch x2)) (tcb_arch (?tcb119 b x2 a ba x2a))\<rparr>) (?etcb119 b x2 a ba x2a))
 2. \<And>b x2 a ba x2a. \<lbrakk>kheap b u = Some (TCB x2); ekheap b u = Some x2a; u \<noteq> idle_thread b; ?P119 b x2 a ba x2a (transform_tcb (?ms119 b x2 a ba x2a) (?ref119 b x2 a ba x2a) (?tcb119 b x2 a ba x2a\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch (?tcb119 b x2 a ba x2a))\<rparr>) (?etcb119 b x2 a ba x2a))\<rbrakk> \<Longrightarrow> transform_tcb (machine_state b) u (x2\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch x2)\<rparr>) x2a = transform_tcb (machine_state b) u x2 x2a proof (prove)
goal (2 subgoals):
 1. \<And>b x2 a ba x2a. \<lbrakk>kheap b u = Some (TCB x2); ekheap b u = Some x2a; u \<noteq> idle_thread b; ?P119 b x2 a ba x2a (transform_tcb (?ms119 b x2 a ba x2a) (?ref119 b x2 a ba x2a) (?tcb119 b x2 a ba x2a\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch (?tcb119 b x2 a ba x2a))\<rparr>) (?etcb119 b x2 a ba x2a))\<rbrakk> \<Longrightarrow> transform_tcb (machine_state b) u (x2\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch x2)\<rparr>) x2a = transform_tcb (machine_state b) u x2 x2a
 2. \<And>b x2 a ba x2a. \<lbrakk>kheap b u = Some (TCB x2); ekheap b u = Some x2a; u \<noteq> idle_thread b\<rbrakk> \<Longrightarrow> ?P119 b x2 a ba x2a (transform_tcb (?ms119 b x2 a ba x2a) (?ref119 b x2 a ba x2a) (?tcb119 b x2 a ba x2a\<lparr>tcb_arch := arch_tcb_context_set (arch_tcb_context_get (tcb_arch x2)) (tcb_arch (?tcb119 b x2 a ba x2a))\<rparr>) (?etcb119 b x2 a ba x2a)) proof (prove)
goal (1 subgoal):
 1. \<And>b x2 a ba x2a. \<lbrakk>kheap b u = Some (TCB x2); ekheap b u = Some x2a; u \<noteq> idle_thread b\<rbrakk> \<Longrightarrow> transform_tcb (machine_state b) u (x2\<lparr>tcb_arch := arch_tcb_context_set (arch_tcb_context_get (tcb_arch x2)) (tcb_arch x2)\<rparr>) x2a = transform_tcb (machine_state b) u x2 x2a proof (prove)
goal:
No subgoals!