theory CNode_DR

lemma dcorres_thread_get_get_object_split:
  assumes c: "\<And>tcb tcb'. dcorres r P (P' tcb tcb') (a (Tcb tcb')) (c (f tcb))"
  shows   "dcorres r P ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow>
                            not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s)
                        and not_idle_thread ptr and valid_etcbs)
             (KHeap_D.get_object ptr >>= a) (thread_get f ptr >>= c)" apply (simp add: thread_get_def) apply (rule corres_guard_imp) apply (rule corres_symb_exec_r) apply (rule dcorres_get_object_special_2 [where AP_LIFT = "\<lambda>tcb etcb s. obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)"
         and AP_Q = "not_idle_thread ptr and valid_etcbs"]) apply (simp add: obj_tcb_def) apply (drule opt_object_tcb, simp, simp add: not_idle_thread_def) apply (simp add: transform_tcb_def obj_tcb_def) apply (rule c) apply wp+ apply clarsimp apply simp apply simp apply clarsimp apply (frule(1) valid_etcbs_get_tcb_get_etcb, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r P ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow> not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s) and not_idle_thread ptr and valid_etcbs) (KHeap_D.get_object ptr >>= a) (thread_get f ptr >>= c) proof (prove)
goal (1 subgoal):
 1. dcorres r P ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow> not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s) and not_idle_thread ptr and valid_etcbs) (KHeap_D.get_object ptr >>= a) (do tcb <- gets_the (get_tcb ptr);
c (f tcb)
od) proof (prove)
goal (3 subgoals):
 1. dcorres r ?Q ?Q' (KHeap_D.get_object ptr >>= a) (do tcb <- gets_the (get_tcb ptr);
c (f tcb)
od)
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow> not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s) and not_idle_thread ptr and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>tcb. dcorres r ?Q (?Q'4 tcb) (KHeap_D.get_object ptr >>= a) (c (f tcb))
 2. \<lbrace>?Q'\<rbrace> gets_the (get_tcb ptr) \<lbrace>?Q'4\<rbrace>
 3. \<And>s. ?Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets_the (get_tcb ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail ?Q' (gets_the (get_tcb ptr))
 5. \<And>s. P s \<Longrightarrow> ?Q s
 6. \<And>s. ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow> not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s) and not_idle_thread ptr and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<And>tcb s obj etcb. \<lbrakk>get_tcb ptr s = Some obj; get_etcb ptr s = Some etcb; (not_idle_thread ptr and valid_etcbs) s\<rbrakk> \<Longrightarrow> cdl_objects (transform s) ptr = Some (Tcb (obj_tcb (transform_tcb (machine_state s) ptr obj etcb)))
 2. \<And>tcb obj. dcorres r (?R11 obj) (?R'9 tcb obj) (a (Tcb obj)) (c (f tcb))
 3. \<lbrace>?Q'\<rbrace> gets_the (get_tcb ptr) \<lbrace>\<lambda>tcb s. (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> ?R'9 tcb (obj_tcb (transform_tcb (machine_state s) ptr obj' etcb)) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb ptr s \<noteq> None \<and> (not_idle_thread ptr and valid_etcbs) s\<rbrace>
 4. \<And>s. ?Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets_the (get_tcb ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. False \<Longrightarrow> no_fail ?Q' (gets_the (get_tcb ptr))
 6. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> ?R11 obj s
 7. \<And>s. ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow> not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s) and not_idle_thread ptr and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<And>s obj etcb. \<lbrakk>get_tcb ptr s = Some obj; get_etcb ptr s = Some etcb; not_idle_thread ptr s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> cdl_objects (transform s) ptr = Some (Tcb (case transform_tcb (machine_state s) ptr obj etcb of Tcb tcb \<Rightarrow> tcb))
 2. \<And>tcb obj. dcorres r (?R11 obj) (?R'9 tcb obj) (a (Tcb obj)) (c (f tcb))
 3. \<lbrace>?Q'\<rbrace> gets_the (get_tcb ptr) \<lbrace>\<lambda>tcb s. (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> ?R'9 tcb (obj_tcb (transform_tcb (machine_state s) ptr obj' etcb)) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb ptr s \<noteq> None \<and> (not_idle_thread ptr and valid_etcbs) s\<rbrace>
 4. \<And>s. ?Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets_the (get_tcb ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. False \<Longrightarrow> no_fail ?Q' (gets_the (get_tcb ptr))
 6. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> ?R11 obj s
 7. \<And>s. ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow> not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s) and not_idle_thread ptr and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<And>s obj etcb. \<lbrakk>get_etcb ptr s = Some etcb; not_idle_thread ptr s \<and> valid_etcbs s; cdl_objects (transform s) ptr = Some (transform_tcb (machine_state s) ptr obj etcb)\<rbrakk> \<Longrightarrow> cdl_objects (transform s) ptr = Some (Tcb (case transform_tcb (machine_state s) ptr obj etcb of Tcb tcb \<Rightarrow> tcb))
 2. \<And>tcb obj. dcorres r (?R11 obj) (?R'9 tcb obj) (a (Tcb obj)) (c (f tcb))
 3. \<lbrace>?Q'\<rbrace> gets_the (get_tcb ptr) \<lbrace>\<lambda>tcb s. (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> ?R'9 tcb (obj_tcb (transform_tcb (machine_state s) ptr obj' etcb)) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb ptr s \<noteq> None \<and> (not_idle_thread ptr and valid_etcbs) s\<rbrace>
 4. \<And>s. ?Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets_the (get_tcb ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. False \<Longrightarrow> no_fail ?Q' (gets_the (get_tcb ptr))
 6. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> ?R11 obj s
 7. \<And>s. ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow> not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s) and not_idle_thread ptr and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>tcb obj. dcorres r (?R11 obj) (?R'9 tcb obj) (a (Tcb obj)) (c (f tcb))
 2. \<lbrace>?Q'\<rbrace> gets_the (get_tcb ptr) \<lbrace>\<lambda>tcb s. (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> ?R'9 tcb (obj_tcb (transform_tcb (machine_state s) ptr obj' etcb)) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb ptr s \<noteq> None \<and> (not_idle_thread ptr and valid_etcbs) s\<rbrace>
 3. \<And>s. ?Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets_the (get_tcb ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail ?Q' (gets_the (get_tcb ptr))
 5. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> ?R11 obj s
 6. \<And>s. ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow> not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s) and not_idle_thread ptr and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q'\<rbrace> gets_the (get_tcb ptr) \<lbrace>\<lambda>tcb s. (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr obj' etcb)) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb ptr s \<noteq> None \<and> (not_idle_thread ptr and valid_etcbs) s\<rbrace>
 2. \<And>s. ?Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets_the (get_tcb ptr) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail ?Q' (gets_the (get_tcb ptr))
 4. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> P s
 5. \<And>s. ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow> not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s) and not_idle_thread ptr and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (4 subgoals):
 1. \<And>s sa. \<lbrakk>get_tcb ptr s \<noteq> None \<longrightarrow> (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> P' (the (get_tcb ptr s)) (obj_tcb (transform_tcb (machine_state s) ptr obj' etcb)) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb ptr s \<noteq> None \<and> (not_idle_thread ptr and valid_etcbs) s; s = sa\<rbrakk> \<Longrightarrow> get_tcb ptr sa \<noteq> None \<longrightarrow> s = sa
 2. False \<Longrightarrow> no_fail (\<lambda>s. get_tcb ptr s \<noteq> None \<longrightarrow> (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> P' (the (get_tcb ptr s)) (obj_tcb (transform_tcb (machine_state s) ptr obj' etcb)) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb ptr s \<noteq> None \<and> (not_idle_thread ptr and valid_etcbs) s) (gets_the (get_tcb ptr))
 3. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> P s
 4. \<And>s. ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow> not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s) and not_idle_thread ptr and valid_etcbs) s \<Longrightarrow> get_tcb ptr s \<noteq> None \<longrightarrow> (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> P' (the (get_tcb ptr s)) (obj_tcb (transform_tcb (machine_state s) ptr obj' etcb)) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb ptr s \<noteq> None \<and> (not_idle_thread ptr and valid_etcbs) s proof (prove)
goal (3 subgoals):
 1. False \<Longrightarrow> no_fail (\<lambda>s. get_tcb ptr s \<noteq> None \<longrightarrow> (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> P' (the (get_tcb ptr s)) (obj_tcb (transform_tcb (machine_state s) ptr obj' etcb)) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb ptr s \<noteq> None \<and> (not_idle_thread ptr and valid_etcbs) s) (gets_the (get_tcb ptr))
 2. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> P s
 3. \<And>s. ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow> not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s) and not_idle_thread ptr and valid_etcbs) s \<Longrightarrow> get_tcb ptr s \<noteq> None \<longrightarrow> (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> P' (the (get_tcb ptr s)) (obj_tcb (transform_tcb (machine_state s) ptr obj' etcb)) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb ptr s \<noteq> None \<and> (not_idle_thread ptr and valid_etcbs) s proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (Tcb obj) \<longrightarrow> P s
 2. \<And>s. ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow> not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s) and not_idle_thread ptr and valid_etcbs) s \<Longrightarrow> get_tcb ptr s \<noteq> None \<longrightarrow> (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> P' (the (get_tcb ptr s)) (obj_tcb (transform_tcb (machine_state s) ptr obj' etcb)) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb ptr s \<noteq> None \<and> (not_idle_thread ptr and valid_etcbs) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>tcb etcb. get_tcb ptr s = Some tcb \<and> get_etcb ptr s = Some etcb \<longrightarrow> not_idle_thread ptr s \<and> P' tcb (obj_tcb (transform_tcb (machine_state s) ptr tcb etcb)) s) and not_idle_thread ptr and valid_etcbs) s \<Longrightarrow> get_tcb ptr s \<noteq> None \<longrightarrow> (\<forall>obj' etcb. get_tcb ptr s = Some obj' \<and> get_etcb ptr s = Some etcb \<longrightarrow> P' (the (get_tcb ptr s)) (obj_tcb (transform_tcb (machine_state s) ptr obj' etcb)) s) \<and> get_tcb ptr s \<noteq> None \<and> get_etcb ptr s \<noteq> None \<and> (not_idle_thread ptr and valid_etcbs) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<forall>etcb. get_etcb ptr s = Some etcb \<longrightarrow> P' y (obj_tcb (transform_tcb (machine_state s) ptr y etcb)) s; not_idle_thread ptr s; valid_etcbs s; get_tcb ptr s = Some y\<rbrakk> \<Longrightarrow> \<exists>y. get_etcb ptr s = Some y proof (prove)
goal:
No subgoals!