theory CSpace_I

lemma cte_wp_at_obj_cases':
  "cte_wp_at' P p s =
    (obj_at' P p s \<or> (\<exists>n \<in> dom tcb_cte_cases. obj_at' (P \<circ> (fst (the (tcb_cte_cases n)))) (p - n) s))" apply (simp add: cte_wp_at_cases' obj_at'_def) apply (rule iffI) apply (erule disjEI
           | clarsimp simp: objBits_simps' cte_level_bits_def projectKOs
           | rule rev_bexI, erule domI)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' P p s = (obj_at' P p s \<or> (\<exists>n\<in>dom tcb_cte_cases. obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s)) proof (prove)
goal (1 subgoal):
 1. ((\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s))) = ((\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> P obj \<and> ps_clear p (objBitsKO ko) s)) \<or> (\<exists>n\<in>dom tcb_cte_cases. \<exists>ko. ksPSpace s (p - n) = Some ko \<and> is_aligned (p - n) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> P (fst (the (tcb_cte_cases n)) obj) \<and> ps_clear (p - n) (objBitsKO ko) s))) proof (prove)
goal (2 subgoals):
 1. (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)) \<Longrightarrow> (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> P obj \<and> ps_clear p (objBitsKO ko) s)) \<or> (\<exists>n\<in>dom tcb_cte_cases. \<exists>ko. ksPSpace s (p - n) = Some ko \<and> is_aligned (p - n) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> P (fst (the (tcb_cte_cases n)) obj) \<and> ps_clear (p - n) (objBitsKO ko) s))
 2. (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> P obj \<and> ps_clear p (objBitsKO ko) s)) \<or> (\<exists>n\<in>dom tcb_cte_cases. \<exists>ko. ksPSpace s (p - n) = Some ko \<and> is_aligned (p - n) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> P (fst (the (tcb_cte_cases n)) obj) \<and> ps_clear (p - n) (objBitsKO ko) s)) \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s)) proof (prove)
goal (1 subgoal):
 1. \<And>n a b obj. \<lbrakk>tcb_cte_cases n = Some (a, b); ksPSpace s (p - n) = Some (KOTCB obj); is_aligned (p - n) 9; P (a obj); ps_clear (p - n) 9 s\<rbrakk> \<Longrightarrow> \<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s) proof (prove)
goal:
No subgoals!