theory CNodeInv_R

lemma capSwap_cte_wp_cteCap:
  "\<lbrace>\<lambda>s. p \<noteq> sl \<and>
       (p = p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) sl s) \<and>
       (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)\<rbrace>
  capSwapForDelete p' sl
  \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>" apply(simp add: capSwapForDelete_def) apply(wp) apply(rule cteSwap_cte_wp_cteCap) apply(wp getCTE_wp getCTE_cte_wp_at hoare_weak_lift_imp)+ apply(clarsimp) apply(rule conjI) apply(simp add: cte_at_cte_wp_atD) apply(clarsimp simp: cte_wp_at_cteCap_norm) apply(unfold cte_at'_def cte_wp_at'_def) apply(clarsimp) apply(clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) sl s) \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)\<rbrace> capSwapForDelete p' sl \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) sl s) \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)\<rbrace> when (p' \<noteq> sl) (do cap1 <- liftM cteCap (getCTE p');
cap2 <- liftM cteCap (getCTE sl);
cteSwap cap1 p' cap2 sl
od) \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cap1 cap2. p' \<noteq> sl \<Longrightarrow> \<lbrace>?B3 cap1 cap2\<rbrace> cteSwap cap1 p' cap2 sl \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>
 2. \<And>cap1. p' \<noteq> sl \<Longrightarrow> \<lbrace>?B2 cap1\<rbrace> liftM cteCap (getCTE sl) \<lbrace>?B3 cap1\<rbrace>
 3. p' \<noteq> sl \<Longrightarrow> \<lbrace>?Q1\<rbrace> liftM cteCap (getCTE p') \<lbrace>?B2\<rbrace>
 4. \<And>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) sl s) \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s) \<Longrightarrow> (if p' \<noteq> sl then ?Q1 else cte_wp_at' (\<lambda>c. P (cteCap c)) p) s proof (prove)
goal (3 subgoals):
 1. \<And>cap1. p' \<noteq> sl \<Longrightarrow> \<lbrace>?B2 cap1\<rbrace> liftM cteCap (getCTE sl) \<lbrace>\<lambda>cap2 s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<and> P cap2) \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)\<rbrace>
 2. p' \<noteq> sl \<Longrightarrow> \<lbrace>?Q1\<rbrace> liftM cteCap (getCTE p') \<lbrace>?B2\<rbrace>
 3. \<And>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) sl s) \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s) \<Longrightarrow> (if p' \<noteq> sl then ?Q1 else cte_wp_at' (\<lambda>c. P (cteCap c)) p) s proof (prove)
goal (1 subgoal):
 1. \<And>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) sl s) \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s) \<Longrightarrow> (if p' \<noteq> sl then \<lambda>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p' s \<and> ((\<lambda>rv s. cte_wp_at' (\<lambda>_. True) sl s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) sl s \<and> ((\<lambda>rv s. cte_wp_at' (\<lambda>_. True) p' s \<and> P rv) \<circ> cteCap) cte s)) \<circ> cteCap) cte s)) \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p' s \<and> ((\<lambda>rv s. cte_wp_at' (\<lambda>_. True) sl s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) sl s \<and> ((\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p) \<circ> cteCap) cte s)) \<circ> cteCap) cte s)) else cte_wp_at' (\<lambda>c. P (cteCap c)) p) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p \<noteq> sl; p = p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) sl s; p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s; p' \<noteq> sl\<rbrakk> \<Longrightarrow> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p' s) \<and> (cte_wp_at' (\<lambda>_. True) sl s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) sl s \<and> P (cteCap cte)))) \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p' s) \<and> (cte_wp_at' (\<lambda>_. True) sl s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) sl s))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>p \<noteq> sl; p = p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) sl s; p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s; p' \<noteq> sl\<rbrakk> \<Longrightarrow> p = p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p' s) \<and> (cte_wp_at' (\<lambda>_. True) sl s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) sl s \<and> P (cteCap cte)))
 2. \<And>s. \<lbrakk>p \<noteq> sl; p = p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) sl s; p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s; p' \<noteq> sl\<rbrakk> \<Longrightarrow> p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p' s) \<and> (cte_wp_at' (\<lambda>_. True) sl s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) sl s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>p \<noteq> sl; p = p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) sl s; p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s; p' \<noteq> sl\<rbrakk> \<Longrightarrow> p = p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<longrightarrow> cte_wp_at' (\<lambda>_. True) sl s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) sl s \<and> P (cteCap cte))
 2. \<And>s. \<lbrakk>p \<noteq> sl; p = p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) sl s; p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s; p' \<noteq> sl\<rbrakk> \<Longrightarrow> p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p' s) \<and> (cte_wp_at' (\<lambda>_. True) sl s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) sl s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>p' \<noteq> sl; p = p'; cte_wp_at' (\<lambda>_. True) p' s; cte_wp_at' (\<lambda>_. True) sl s; cte_wp_at' (\<lambda>c. cteCap c = cap) sl s; P cap\<rbrakk> \<Longrightarrow> \<exists>cte. cte_wp_at' ((=) cte) sl s \<and> P (cteCap cte)
 2. \<And>s. \<lbrakk>p \<noteq> sl; p = p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) sl s; p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s; p' \<noteq> sl\<rbrakk> \<Longrightarrow> p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p' s) \<and> (cte_wp_at' (\<lambda>_. True) sl s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) sl s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>p' \<noteq> sl; p = p'; \<exists>cte. fst (getObject p' s) = {(cte, s)}; \<exists>cte. fst (getObject sl s) = {(cte, s)}; \<exists>cte. fst (getObject sl s) = {(cte, s)} \<and> cteCap cte = cap; P cap\<rbrakk> \<Longrightarrow> \<exists>cte. (\<exists>ctea. fst (getObject sl s) = {(ctea, s)} \<and> cte = ctea) \<and> P (cteCap cte)
 2. \<And>s. \<lbrakk>p \<noteq> sl; p = p' \<longrightarrow> (\<exists>cte. fst (getObject sl s) = {(cte, s)} \<and> P (cteCap cte)); p \<noteq> p' \<longrightarrow> (\<exists>cte. fst (getObject p s) = {(cte, s)} \<and> P (cteCap cte)); p' \<noteq> sl\<rbrakk> \<Longrightarrow> p \<noteq> p' \<longrightarrow> (\<exists>cte. fst (getObject p' s) = {(cte, s)}) \<longrightarrow> (\<exists>cte ctea. fst (getObject p' s) = {(ctea, s)} \<and> cte = ctea) \<and> ((\<exists>cte. fst (getObject sl s) = {(cte, s)}) \<longrightarrow> (\<exists>cte ctea. fst (getObject sl s) = {(ctea, s)} \<and> cte = ctea)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p \<noteq> sl; p = p' \<longrightarrow> (\<exists>cte. fst (getObject sl s) = {(cte, s)} \<and> P (cteCap cte)); p \<noteq> p' \<longrightarrow> (\<exists>cte. fst (getObject p s) = {(cte, s)} \<and> P (cteCap cte)); p' \<noteq> sl\<rbrakk> \<Longrightarrow> p \<noteq> p' \<longrightarrow> (\<exists>cte. fst (getObject p' s) = {(cte, s)}) \<longrightarrow> (\<exists>cte ctea. fst (getObject p' s) = {(ctea, s)} \<and> cte = ctea) \<and> ((\<exists>cte. fst (getObject sl s) = {(cte, s)}) \<longrightarrow> (\<exists>cte ctea. fst (getObject sl s) = {(ctea, s)} \<and> cte = ctea)) proof (prove)
goal:
No subgoals!