theory Retype_R

lemma cte_wp_at_obj_cases_mask:
  "cte_wp_at' P p s =
       (obj_at' P p s \<or>
          (p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases
             \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits))))
                     (p && ~~ mask tcbBlockSizeBits) s))" apply (simp add: cte_wp_at_obj_cases') apply (rule arg_cong [where f="\<lambda>x. F \<or> x" for F]) apply (rule iffI) apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) apply (frule(1) tcb_cte_cases_aligned_helpers) apply fastforce apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) apply (rule bexI[where x="p && mask tcbBlockSizeBits"]) apply (clarsimp simp: subtract_mask) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' P p s = (obj_at' P p s \<or> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s) proof (prove)
goal (1 subgoal):
 1. (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)) = (obj_at' P p s \<or> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s) proof (prove)
goal (1 subgoal):
 1. (\<exists>n\<in>dom tcb_cte_cases. obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s) = (p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s) proof (prove)
goal (2 subgoals):
 1. \<exists>n\<in>dom tcb_cte_cases. obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s \<Longrightarrow> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s
 2. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s \<Longrightarrow> \<exists>n\<in>dom tcb_cte_cases. obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s proof (prove)
goal (2 subgoals):
 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) tcbBlockSizeBits; P (a obj); ps_clear (p - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>ko. ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some ko \<and> is_aligned (p && ~~ mask tcbBlockSizeBits) (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj \<and> P (fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) obj) \<and> ps_clear (p && ~~ mask tcbBlockSizeBits) (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s))
 2. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s \<Longrightarrow> \<exists>n\<in>dom tcb_cte_cases. obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s proof (prove)
goal (2 subgoals):
 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) tcbBlockSizeBits; P (a obj); ps_clear (p - n) tcbBlockSizeBits s; p - n + n && mask tcbBlockSizeBits = n \<and> p - n + n && ~~ mask tcbBlockSizeBits = p - n\<rbrakk> \<Longrightarrow> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>ko. ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some ko \<and> is_aligned (p && ~~ mask tcbBlockSizeBits) (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj \<and> P (fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) obj) \<and> ps_clear (p && ~~ mask tcbBlockSizeBits) (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s))
 2. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s \<Longrightarrow> \<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. p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s \<Longrightarrow> \<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. \<And>a b obj. \<lbrakk>tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); P (a obj); ps_clear (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> \<exists>n\<in>dom tcb_cte_cases. \<exists>ko. ksPSpace s (p - n) = Some ko \<and> is_aligned (p - n) (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj \<and> P (fst (the (tcb_cte_cases n)) obj) \<and> ps_clear (p - n) (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s) proof (prove)
goal (2 subgoals):
 1. \<And>a b obj. \<lbrakk>tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); P (a obj); ps_clear (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s (p - (p && mask tcbBlockSizeBits)) = Some ko \<and> is_aligned (p - (p && mask tcbBlockSizeBits)) (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj \<and> P (fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits))) obj) \<and> ps_clear (p - (p && mask tcbBlockSizeBits)) (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s)
 2. \<And>a b obj. \<lbrakk>tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); P (a obj); ps_clear (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases proof (prove)
goal (1 subgoal):
 1. \<And>a b obj. \<lbrakk>tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (p && ~~ mask tcbBlockSizeBits) = Some (KOTCB obj); P (a obj); ps_clear (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases proof (prove)
goal:
No subgoals!