theory Intent_DR

lemma weak_det_spec_get_cap:
  "weak_det_spec P (get_cap slot)" apply (case_tac slot) apply (simp add:get_cap_def) apply (rule weak_det_spec_compose)+ apply (simp_all add:weak_det_spec_simps weak_det_spec_get_object) apply (case_tac r) apply (simp_all add:weak_det_spec_simps weak_det_spec_get_object) apply (rule weak_det_spec_compose) apply (simp_all add:weak_det_spec_simps weak_det_spec_get_object) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (CSpaceAcc_A.get_cap slot) proof (prove)
goal (1 subgoal):
 1. \<And>a b. slot = (a, b) \<Longrightarrow> weak_det_spec P (CSpaceAcc_A.get_cap slot) proof (prove)
goal (1 subgoal):
 1. \<And>a b. slot = (a, b) \<Longrightarrow> weak_det_spec P (do obj <- KHeap_A.get_object a;
caps <- case obj of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return (tcb_cnode_map tcb) | _ \<Rightarrow> fail;
assert_opt (caps b)
od) proof (prove)
goal (3 subgoals):
 1. \<And>a b Q r Qa ra. slot = (a, b) \<Longrightarrow> weak_det_spec (Qa ra) (assert_opt (ra b))
 2. \<And>a b Q r P. slot = (a, b) \<Longrightarrow> weak_det_spec P (case r of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return (tcb_cnode_map tcb) | _ \<Rightarrow> fail)
 3. \<And>a b P. slot = (a, b) \<Longrightarrow> weak_det_spec P (KHeap_A.get_object a) proof (prove)
goal (1 subgoal):
 1. \<And>a b r P. slot = (a, b) \<Longrightarrow> weak_det_spec P (case r of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return (tcb_cnode_map tcb) | _ \<Rightarrow> fail) proof (prove)
goal (5 subgoals):
 1. \<And>a b r P x11 x12. \<lbrakk>slot = (a, b); r = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> weak_det_spec P (case r of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return (tcb_cnode_map tcb) | _ \<Rightarrow> fail)
 2. \<And>a b r P x2. \<lbrakk>slot = (a, b); r = TCB x2\<rbrakk> \<Longrightarrow> weak_det_spec P (case r of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return (tcb_cnode_map tcb) | _ \<Rightarrow> fail)
 3. \<And>a b r P x3. \<lbrakk>slot = (a, b); r = kernel_object.Endpoint x3\<rbrakk> \<Longrightarrow> weak_det_spec P (case r of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return (tcb_cnode_map tcb) | _ \<Rightarrow> fail)
 4. \<And>a b r P x4. \<lbrakk>slot = (a, b); r = kernel_object.Notification x4\<rbrakk> \<Longrightarrow> weak_det_spec P (case r of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return (tcb_cnode_map tcb) | _ \<Rightarrow> fail)
 5. \<And>a b r P x5. \<lbrakk>slot = (a, b); r = ArchObj x5\<rbrakk> \<Longrightarrow> weak_det_spec P (case r of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return (tcb_cnode_map tcb) | _ \<Rightarrow> fail) proof (prove)
goal (1 subgoal):
 1. \<And>a b r P x11 x12. \<lbrakk>slot = (a, b); r = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> weak_det_spec P (do y <- assert (well_formed_cnode_n x11 x12);
return x12
od) proof (prove)
goal (2 subgoals):
 1. \<And>a b r P x11 x12 Q ra. \<lbrakk>slot = (a, b); r = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> weak_det_spec (Q ra) (return x12)
 2. \<And>a b r P x11 x12 Pa. \<lbrakk>slot = (a, b); r = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> weak_det_spec Pa (assert (well_formed_cnode_n x11 x12)) proof (prove)
goal:
No subgoals!