theory Intent_DR

lemma empty_when_fail_get_cap:
  "empty_when_fail (get_cap slot)" apply (case_tac slot) apply (clarsimp simp:get_cap_def) apply (rule empty_when_fail_compose)+ apply (simp_all add:empty_when_fail_simps empty_when_fail_get_object weak_det_spec_get_object) apply (case_tac r) apply (simp_all add:empty_when_fail_simps empty_when_fail_get_object weak_det_spec_get_object) apply (rule empty_when_fail_compose) apply (simp_all add:empty_when_fail_simps weak_det_spec_simps empty_when_fail_get_object) apply (case_tac r) apply (simp_all add:empty_when_fail_simps weak_det_spec_simps empty_when_fail_get_object) apply (rule weak_det_spec_compose) apply (simp_all add:empty_when_fail_simps weak_det_spec_simps empty_when_fail_get_object) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail (CSpaceAcc_A.get_cap slot) proof (prove)
goal (1 subgoal):
 1. \<And>a b. slot = (a, b) \<Longrightarrow> empty_when_fail (CSpaceAcc_A.get_cap slot) proof (prove)
goal (1 subgoal):
 1. \<And>a b. slot = (a, b) \<Longrightarrow> empty_when_fail (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 (5 subgoals):
 1. \<And>a b r ra. slot = (a, b) \<Longrightarrow> empty_when_fail (assert_opt (ra b))
 2. \<And>a b r. slot = (a, b) \<Longrightarrow> empty_when_fail (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. 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)
 4. \<And>a b. slot = (a, b) \<Longrightarrow> empty_when_fail (KHeap_A.get_object a)
 5. \<And>a b P. slot = (a, b) \<Longrightarrow> weak_det_spec P (KHeap_A.get_object a) proof (prove)
goal (2 subgoals):
 1. \<And>a b r. slot = (a, b) \<Longrightarrow> empty_when_fail (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. 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 (6 subgoals):
 1. \<And>a b r x11 x12. \<lbrakk>slot = (a, b); r = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> empty_when_fail (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 x2. \<lbrakk>slot = (a, b); r = TCB x2\<rbrakk> \<Longrightarrow> empty_when_fail (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 x3. \<lbrakk>slot = (a, b); r = kernel_object.Endpoint x3\<rbrakk> \<Longrightarrow> empty_when_fail (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 x4. \<lbrakk>slot = (a, b); r = kernel_object.Notification x4\<rbrakk> \<Longrightarrow> empty_when_fail (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 x5. \<lbrakk>slot = (a, b); r = ArchObj x5\<rbrakk> \<Longrightarrow> empty_when_fail (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)
 6. \<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 (2 subgoals):
 1. \<And>a b r x11 x12. \<lbrakk>slot = (a, b); r = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> empty_when_fail (do y <- assert (well_formed_cnode_n x11 x12);
return x12
od)
 2. \<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 (4 subgoals):
 1. \<And>a b r x11 x12 ra. \<lbrakk>slot = (a, b); r = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> empty_when_fail (return x12)
 2. \<And>a b r x11 x12. \<lbrakk>slot = (a, b); r = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> empty_when_fail (assert (well_formed_cnode_n x11 x12))
 3. \<And>a b r x11 x12 P. \<lbrakk>slot = (a, b); r = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> weak_det_spec P (assert (well_formed_cnode_n x11 x12))
 4. \<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 (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!