theory DomainSepInv

lemma cte_wp_at_weak_derived_ReplyCap:
  "cte_wp_at ((=) (ReplyCap x False R)) slot s
   \<Longrightarrow> cte_wp_at (weak_derived (ReplyCap x False R)) slot s" apply (erule cte_wp_atE) apply (rule cte_wp_at_cteI) apply assumption apply assumption apply assumption apply simp apply (rule cte_wp_at_tcbI) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at ((=) (ReplyCap x False R)) slot s \<Longrightarrow> cte_wp_at (weak_derived (ReplyCap x False R)) slot s proof (prove)
goal (2 subgoals):
 1. \<And>sz fun cte. \<lbrakk>kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; ReplyCap x False R = cte\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (ReplyCap x False R)) slot s
 2. \<And>tcb getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); ReplyCap x False R = getF tcb\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (ReplyCap x False R)) slot s proof (prove)
goal (5 subgoals):
 1. \<And>sz fun cte. \<lbrakk>kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; ReplyCap x False R = cte\<rbrakk> \<Longrightarrow> kheap s (fst slot) = Some (CNode (?sz3 sz fun cte) (?fun3 sz fun cte))
 2. \<And>sz fun cte. \<lbrakk>kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; ReplyCap x False R = cte\<rbrakk> \<Longrightarrow> well_formed_cnode_n (?sz3 sz fun cte) (?fun3 sz fun cte)
 3. \<And>sz fun cte. \<lbrakk>kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; ReplyCap x False R = cte\<rbrakk> \<Longrightarrow> ?fun3 sz fun cte (snd slot) = Some (?cte3 sz fun cte)
 4. \<And>sz fun cte. \<lbrakk>kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; ReplyCap x False R = cte\<rbrakk> \<Longrightarrow> weak_derived (ReplyCap x False R) (?cte3 sz fun cte)
 5. \<And>tcb getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); ReplyCap x False R = getF tcb\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (ReplyCap x False R)) slot s proof (prove)
goal (4 subgoals):
 1. \<And>sz fun cte. \<lbrakk>kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; ReplyCap x False R = cte\<rbrakk> \<Longrightarrow> well_formed_cnode_n sz fun
 2. \<And>sz fun cte. \<lbrakk>kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; ReplyCap x False R = cte\<rbrakk> \<Longrightarrow> fun (snd slot) = Some (?cte3 sz fun cte)
 3. \<And>sz fun cte. \<lbrakk>kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; ReplyCap x False R = cte\<rbrakk> \<Longrightarrow> weak_derived (ReplyCap x False R) (?cte3 sz fun cte)
 4. \<And>tcb getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); ReplyCap x False R = getF tcb\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (ReplyCap x False R)) slot s proof (prove)
goal (3 subgoals):
 1. \<And>sz fun cte. \<lbrakk>kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; ReplyCap x False R = cte\<rbrakk> \<Longrightarrow> fun (snd slot) = Some (?cte3 sz fun cte)
 2. \<And>sz fun cte. \<lbrakk>kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; ReplyCap x False R = cte\<rbrakk> \<Longrightarrow> weak_derived (ReplyCap x False R) (?cte3 sz fun cte)
 3. \<And>tcb getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); ReplyCap x False R = getF tcb\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (ReplyCap x False R)) slot s proof (prove)
goal (2 subgoals):
 1. \<And>sz fun cte. \<lbrakk>kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; ReplyCap x False R = cte\<rbrakk> \<Longrightarrow> weak_derived (ReplyCap x False R) cte
 2. \<And>tcb getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); ReplyCap x False R = getF tcb\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (ReplyCap x False R)) slot s proof (prove)
goal (1 subgoal):
 1. \<And>tcb getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); ReplyCap x False R = getF tcb\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (ReplyCap x False R)) slot s proof (prove)
goal (3 subgoals):
 1. \<And>tcb getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); ReplyCap x False R = getF tcb\<rbrakk> \<Longrightarrow> kheap s (fst slot) = Some (TCB (?tcb8 tcb getF setF restr))
 2. \<And>tcb getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); ReplyCap x False R = getF tcb\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd slot) = Some (?getF8 tcb getF setF restr, ?setF8 tcb getF setF restr)
 3. \<And>tcb getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); ReplyCap x False R = getF tcb\<rbrakk> \<Longrightarrow> weak_derived (ReplyCap x False R) (?getF8 tcb getF setF restr (?tcb8 tcb getF setF restr)) proof (prove)
goal:
No subgoals!