theory DomainSepInv

lemma set_object_tcb_context_update_neg_cte_wp_at:
  "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s \<and> obj_at ((=) (TCB tcb)) ptr s\<rbrace>
   set_object ptr (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))
   \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" apply (wp set_object_wp) apply clarsimp apply (case_tac "ptr = fst slot") apply (erule cte_wp_atE) apply (fastforce simp: obj_at_def) apply (erule notE) apply (clarsimp simp: obj_at_def) apply (rule cte_wp_at_tcbI) apply simp apply (fastforce) apply (fastforce simp: tcb_cap_cases_def split: if_splits) apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s \<and> ko_at (TCB tcb) ptr s\<rbrace> set_object ptr (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>)) \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> cte_wp_at P slot s \<and> ko_at (TCB tcb) ptr s \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>); ptr = fst slot\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>); ptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s sz fun cte. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; ptr = fst slot; kheap (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>) (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; P cte\<rbrakk> \<Longrightarrow> False
 2. \<And>s tcba getF setF restr. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; ptr = fst slot; kheap (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>) (fst slot) = Some (TCB tcba); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcba)\<rbrakk> \<Longrightarrow> False
 3. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>); ptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s tcba getF setF restr. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; ptr = fst slot; kheap (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>) (fst slot) = Some (TCB tcba); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcba)\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>); ptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s tcba getF setF restr. \<lbrakk>ko_at (TCB tcb) ptr s; ptr = fst slot; kheap (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>) (fst slot) = Some (TCB tcba); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcba)\<rbrakk> \<Longrightarrow> cte_wp_at P slot s
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>); ptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); ptr = fst slot; tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rbrakk> \<Longrightarrow> cte_wp_at P slot s
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>); ptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); ptr = fst slot; tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rbrakk> \<Longrightarrow> kheap s (fst slot) = Some (TCB (?tcb17 s getF setF restr))
 2. \<And>s getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); ptr = fst slot; tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd slot) = Some (?getF17 s getF setF restr, ?setF17 s getF setF restr)
 3. \<And>s getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); ptr = fst slot; tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rbrakk> \<Longrightarrow> P (?getF17 s getF setF restr (?tcb17 s getF setF restr))
 4. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>); ptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); ptr = fst slot; tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd slot) = Some (?getF17 s getF setF restr, ?setF17 s getF setF restr)
 2. \<And>s getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); ptr = fst slot; tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rbrakk> \<Longrightarrow> P (?getF17 s getF setF restr tcb)
 3. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>); ptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s getF setF restr. \<lbrakk>kheap s (fst slot) = Some (TCB tcb); ptr = fst slot; tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rbrakk> \<Longrightarrow> P (getF tcb)
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>); ptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; ko_at (TCB tcb) ptr s; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>))\<rparr>); ptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!