theory CSpacePre_AI

lemma set_cap_def2:
  "set_cap cap = (\<lambda>(oref, cref). do
     obj \<leftarrow> get_object oref;
     obj' \<leftarrow> (case (obj, tcb_cap_cases cref) of
     (CNode sz cs, _) \<Rightarrow> if cref \<in> dom cs \<and> well_formed_cnode_n sz cs
         then return $ CNode sz $ cs(cref \<mapsto> cap)
         else fail
   | (TCB tcb, Some (getF, setF, restr)) \<Rightarrow> return $ TCB (setF (\<lambda>x. cap) tcb)
   | _ \<Rightarrow> fail);
     set_object oref obj'
   od)" apply (rule ext, simp add: set_cap_def split_def) apply (intro bind_cong bind_apply_cong refl) apply (simp split: Structures_A.kernel_object.split) apply (simp add: tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_cap cap = (\<lambda>(oref, cref). do obj <- get_object oref;
(case (obj, tcb_cap_cases cref) of (CNode sz cs, x) \<Rightarrow> if cref \<in> dom cs \<and> well_formed_cnode_n sz cs then return $ CNode sz $ cs(cref \<mapsto> cap) else fail | (TCB tcb, None) \<Rightarrow> fail | (TCB tcb, Some (getF, setF, restr)) \<Rightarrow> return $ TCB (setF (\<lambda>x. cap) tcb) | (_, x) \<Rightarrow> fail) >>= set_object oref
od) proof (prove)
goal (1 subgoal):
 1. \<And>x. do obj <- get_object (fst x);
(case obj of CNode sz cn \<Rightarrow> if snd x \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd x \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd x = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd x = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd x = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd x = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd x = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object (fst x)
od = do obj <- get_object (fst x);
(case obj of CNode sz cs \<Rightarrow> if snd x \<in> dom cs \<and> well_formed_cnode_n sz cs then return $ CNode sz $ cs(snd x \<mapsto> cap) else fail | TCB tcb \<Rightarrow> case snd (obj, tcb_cap_cases (snd x)) of None \<Rightarrow> fail | Some (getF, setF, restr) \<Rightarrow> return $ TCB (setF (\<lambda>x. cap) tcb) | _ \<Rightarrow> fail) >>= set_object (fst x)
od proof (prove)
goal (1 subgoal):
 1. \<And>x v s s'. (v, s') \<in> fst (get_object (fst x) s) \<Longrightarrow> (case v of CNode sz cn \<Rightarrow> if snd x \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd x \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd x = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd x = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd x = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd x = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd x = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) s' = (case v of CNode sz cs \<Rightarrow> if snd x \<in> dom cs \<and> well_formed_cnode_n sz cs then return $ CNode sz $ cs(snd x \<mapsto> cap) else fail | TCB tcb \<Rightarrow> case snd (v, tcb_cap_cases (snd x)) of None \<Rightarrow> fail | Some (getF, setF, restr) \<Rightarrow> return $ TCB (setF (\<lambda>x. cap) tcb) | _ \<Rightarrow> fail) s' proof (prove)
goal (1 subgoal):
 1. \<And>x v s s'. (v, s') \<in> fst (get_object (fst x) s) \<Longrightarrow> snd x \<noteq> tcb_cnode_index 0 \<longrightarrow> snd x \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> snd x \<noteq> tcb_cnode_index 2 \<longrightarrow> snd x \<noteq> tcb_cnode_index 3 \<longrightarrow> snd x \<noteq> tcb_cnode_index 4 \<longrightarrow> (\<forall>x2. v = TCB x2 \<longrightarrow> fail s' = (case tcb_cap_cases (snd x) of None \<Rightarrow> fail | Some (getF, setF, restr) \<Rightarrow> return $ TCB (setF (\<lambda>x. cap) x2)) s') proof (prove)
goal:
No subgoals!