theory IpcCancel_AI

lemma caps_of_state_tcb_index_trans:
  "\<lbrakk>get_tcb p s = Some tcb \<rbrakk> \<Longrightarrow> caps_of_state s (p, tcb_cnode_index n) = (tcb_cnode_map tcb) (tcb_cnode_index n)" apply (drule get_tcb_SomeD) apply (clarsimp simp: caps_of_state_def) apply (safe) apply (clarsimp simp: get_object_def get_cap_def) apply (simp add:set_eq_iff) apply (drule_tac x=cap in spec) apply (drule_tac x=s in spec) apply (clarsimp simp: in_monad) apply (clarsimp simp: get_cap_def get_object_def) apply (rule ccontr) apply (drule not_sym) apply (auto simp: set_eq_iff in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_tcb p s = Some tcb \<Longrightarrow> caps_of_state s (p, tcb_cnode_index n) = tcb_cnode_map tcb (tcb_cnode_index n) proof (prove)
goal (1 subgoal):
 1. kheap s p = Some (TCB tcb) \<Longrightarrow> caps_of_state s (p, tcb_cnode_index n) = tcb_cnode_map tcb (tcb_cnode_index n) proof (prove)
goal (1 subgoal):
 1. kheap s p = Some (TCB tcb) \<Longrightarrow> ((\<exists>cap. fst (get_cap (p, tcb_cnode_index n) s) = {(cap, s)}) \<longrightarrow> Some (THE cap. fst (get_cap (p, tcb_cnode_index n) s) = {(cap, s)}) = tcb_cnode_map tcb (tcb_cnode_index n)) \<and> ((\<forall>cap. fst (get_cap (p, tcb_cnode_index n) s) \<noteq> {(cap, s)}) \<longrightarrow> None = tcb_cnode_map tcb (tcb_cnode_index n)) proof (prove)
goal (2 subgoals):
 1. \<And>cap. \<lbrakk>kheap s p = Some (TCB tcb); fst (get_cap (p, tcb_cnode_index n) s) = {(cap, s)}\<rbrakk> \<Longrightarrow> Some (THE cap. fst (get_cap (p, tcb_cnode_index n) s) = {(cap, s)}) = tcb_cnode_map tcb (tcb_cnode_index n)
 2. \<lbrakk>kheap s p = Some (TCB tcb); \<forall>cap. fst (get_cap (p, tcb_cnode_index n) s) \<noteq> {(cap, s)}\<rbrakk> \<Longrightarrow> None = tcb_cnode_map tcb (tcb_cnode_index n) proof (prove)
goal (2 subgoals):
 1. \<And>cap. \<lbrakk>kheap s p = Some (TCB tcb); fst ((do obj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
caps <- case obj 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 (tcb_cnode_index n))
od) s) = {(cap, s)}\<rbrakk> \<Longrightarrow> Some cap = tcb_cnode_map tcb (tcb_cnode_index n)
 2. \<lbrakk>kheap s p = Some (TCB tcb); \<forall>cap. fst (get_cap (p, tcb_cnode_index n) s) \<noteq> {(cap, s)}\<rbrakk> \<Longrightarrow> None = tcb_cnode_map tcb (tcb_cnode_index n) proof (prove)
goal (2 subgoals):
 1. \<And>cap. \<lbrakk>kheap s p = Some (TCB tcb); \<forall>a b. ((a, b) \<in> fst ((do obj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
caps <- case obj 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 (tcb_cnode_index n))
od) s)) = (a = cap \<and> b = s)\<rbrakk> \<Longrightarrow> Some cap = tcb_cnode_map tcb (tcb_cnode_index n)
 2. \<lbrakk>kheap s p = Some (TCB tcb); \<forall>cap. fst (get_cap (p, tcb_cnode_index n) s) \<noteq> {(cap, s)}\<rbrakk> \<Longrightarrow> None = tcb_cnode_map tcb (tcb_cnode_index n) proof (prove)
goal (2 subgoals):
 1. \<And>cap. \<lbrakk>kheap s p = Some (TCB tcb); \<forall>b. ((cap, b) \<in> fst ((do obj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
caps <- case obj 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 (tcb_cnode_index n))
od) s)) = (cap = cap \<and> b = s)\<rbrakk> \<Longrightarrow> Some cap = tcb_cnode_map tcb (tcb_cnode_index n)
 2. \<lbrakk>kheap s p = Some (TCB tcb); \<forall>cap. fst (get_cap (p, tcb_cnode_index n) s) \<noteq> {(cap, s)}\<rbrakk> \<Longrightarrow> None = tcb_cnode_map tcb (tcb_cnode_index n) proof (prove)
goal (2 subgoals):
 1. \<And>cap. \<lbrakk>kheap s p = Some (TCB tcb); ((cap, s) \<in> fst ((do obj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
caps <- case obj 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 (tcb_cnode_index n))
od) s)) = (cap = cap \<and> s = s)\<rbrakk> \<Longrightarrow> Some cap = tcb_cnode_map tcb (tcb_cnode_index n)
 2. \<lbrakk>kheap s p = Some (TCB tcb); \<forall>cap. fst (get_cap (p, tcb_cnode_index n) s) \<noteq> {(cap, s)}\<rbrakk> \<Longrightarrow> None = tcb_cnode_map tcb (tcb_cnode_index n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (TCB tcb); \<forall>cap. fst (get_cap (p, tcb_cnode_index n) s) \<noteq> {(cap, s)}\<rbrakk> \<Longrightarrow> None = tcb_cnode_map tcb (tcb_cnode_index n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (TCB tcb); \<forall>cap. fst ((do obj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
caps <- case obj 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 (tcb_cnode_index n))
od) s) \<noteq> {(cap, s)}\<rbrakk> \<Longrightarrow> None = tcb_cnode_map tcb (tcb_cnode_index n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (TCB tcb); \<forall>cap. fst ((do obj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
caps <- case obj 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 (tcb_cnode_index n))
od) s) \<noteq> {(cap, s)}; None \<noteq> tcb_cnode_map tcb (tcb_cnode_index n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some (TCB tcb); \<forall>cap. fst ((do obj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
caps <- case obj 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 (tcb_cnode_index n))
od) s) \<noteq> {(cap, s)}; tcb_cnode_map tcb (tcb_cnode_index n) \<noteq> None\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!