theory DomainSepInv

lemma set_cap_neg_cte_wp_at_other_helper':
  "\<lbrakk> oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s;
     tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr);
     kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda> x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb);
     tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb) \<rbrakk>
     \<Longrightarrow> cte_wp_at P slot s" apply (case_tac "fst oslot = fst slot") apply (rule cte_wp_at_tcbI) apply (fastforce split: if_splits simp: obj_at_def) apply assumption apply (fastforce split: if_splits simp: tcb_cap_cases_def dest: prod_eqI) apply (rule cte_wp_at_tcbI) apply (fastforce split: if_splits simp: obj_at_def) apply assumption apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P slot s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot = fst slot\<rbrakk> \<Longrightarrow> cte_wp_at P slot s
 2. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot \<noteq> fst slot\<rbrakk> \<Longrightarrow> cte_wp_at P slot s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot = fst slot\<rbrakk> \<Longrightarrow> kheap s (fst slot) = Some (TCB ?tcb1)
 2. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot = fst slot\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd slot) = Some (?getF1, ?setF1)
 3. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot = fst slot\<rbrakk> \<Longrightarrow> P (?getF1 ?tcb1)
 4. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot \<noteq> fst slot\<rbrakk> \<Longrightarrow> cte_wp_at P slot s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot = fst slot\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd slot) = Some (?getF1, ?setF1)
 2. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot = fst slot\<rbrakk> \<Longrightarrow> P (?getF1 x)
 3. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot \<noteq> fst slot\<rbrakk> \<Longrightarrow> cte_wp_at P slot s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot = fst slot\<rbrakk> \<Longrightarrow> P (getF x)
 2. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot \<noteq> fst slot\<rbrakk> \<Longrightarrow> cte_wp_at P slot s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot \<noteq> fst slot\<rbrakk> \<Longrightarrow> cte_wp_at P slot s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot \<noteq> fst slot\<rbrakk> \<Longrightarrow> kheap s (fst slot) = Some (TCB ?tcb993)
 2. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot \<noteq> fst slot\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd slot) = Some (?getF993, ?setF993)
 3. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot \<noteq> fst slot\<rbrakk> \<Longrightarrow> P (?getF993 ?tcb993) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot \<noteq> fst slot\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd slot) = Some (?getF993, ?setF993)
 2. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot \<noteq> fst slot\<rbrakk> \<Longrightarrow> P (?getF993 tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); kheap (s\<lparr>kheap := (kheap s)(fst oslot \<mapsto> TCB (osetF (\<lambda>x. cap) x))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); fst oslot \<noteq> fst slot\<rbrakk> \<Longrightarrow> P (getF tcb) proof (prove)
goal:
No subgoals!