theory ArchInvariants_AI

lemma get_cap_update [iff]:
  "(fst (get_cap p (f s)) = {(cap, f s)}) = (fst (get_cap p s) = {(cap, s)})" apply (simp add: get_cap_def get_object_def bind_assoc
                   exec_gets split_def assert_def pspace) apply (clarsimp simp: fail_def) apply (case_tac y, simp_all add: assert_opt_def split: option.splits) apply (simp_all add: return_def fail_def assert_def bind_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (fst (get_cap p (f s)) = {(cap, f s)}) = (fst (get_cap p s) = {(cap, s)}) proof (prove)
goal (1 subgoal):
 1. ((\<exists>y. kheap s (fst p) = Some y) \<longrightarrow> (fst ((do caps <- case the (kheap s (fst p)) of 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 (snd p))
od) (f s)) = {(cap, f s)}) = (fst ((do caps <- case the (kheap s (fst p)) of 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 (snd p))
od) s) = {(cap, s)})) \<and> (kheap s (fst p) = None \<longrightarrow> (fst (fail (f s)) = {(cap, f s)}) = (fst (fail s) = {(cap, s)})) proof (prove)
goal (1 subgoal):
 1. \<And>y. kheap s (fst p) = Some y \<Longrightarrow> (fst ((do caps <- case y of 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 (snd p))
od) (f s)) = {(cap, f s)}) = (fst ((do caps <- case y of 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 (snd p))
od) s) = {(cap, s)}) proof (prove)
goal (5 subgoals):
 1. \<And>y x11 x12. \<lbrakk>kheap s (fst p) = Some (CNode x11 x12); y = CNode x11 x12\<rbrakk> \<Longrightarrow> (x12 (snd p) = None \<longrightarrow> (fst ((do y <- assert (well_formed_cnode_n x11 x12);
fail
od) (f s)) = {(cap, f s)}) = (fst ((do y <- assert (well_formed_cnode_n x11 x12);
fail
od) s) = {(cap, s)})) \<and> (\<forall>x2. x12 (snd p) = Some x2 \<longrightarrow> (fst ((do y <- assert (well_formed_cnode_n x11 x12);
return x2
od) (f s)) = {(cap, f s)}) = (fst ((do y <- assert (well_formed_cnode_n x11 x12);
return x2
od) s) = {(cap, s)}))
 2. \<And>y x2. \<lbrakk>kheap s (fst p) = Some (TCB x2); y = TCB x2\<rbrakk> \<Longrightarrow> (tcb_cnode_map x2 (snd p) = None \<longrightarrow> (fst (fail (f s)) = {(cap, f s)}) = (fst (fail s) = {(cap, s)})) \<and> (\<forall>x2a. tcb_cnode_map x2 (snd p) = Some x2a \<longrightarrow> (fst (return x2a (f s)) = {(cap, f s)}) = (fst (return x2a s) = {(cap, s)}))
 3. \<And>y x3. \<lbrakk>kheap s (fst p) = Some (Endpoint x3); y = Endpoint x3\<rbrakk> \<Longrightarrow> (fst (fail (f s)) = {(cap, f s)}) = (fst (fail s) = {(cap, s)})
 4. \<And>y x4. \<lbrakk>kheap s (fst p) = Some (Notification x4); y = Notification x4\<rbrakk> \<Longrightarrow> (fst (fail (f s)) = {(cap, f s)}) = (fst (fail s) = {(cap, s)})
 5. \<And>y x5. \<lbrakk>kheap s (fst p) = Some (ArchObj x5); y = ArchObj x5\<rbrakk> \<Longrightarrow> (fst (fail (f s)) = {(cap, f s)}) = (fst (fail s) = {(cap, s)}) proof (prove)
goal:
No subgoals!