theory Detype_R

lemma locateCTE_case:
  "\<lbrace>\<top>\<rbrace> locateCTE src
   \<lbrace>\<lambda>r s. \<exists>obj. ksPSpace s r = Some obj \<and>
          (case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False)\<rbrace>" apply (clarsimp simp:locateCTE_def split_def | wp)+ apply (clarsimp simp: lookupAround2_char1) apply (case_tac b) apply (simp_all add:cte_check_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> locateCTE src \<lbrace>\<lambda>r s. \<exists>obj. ksPSpace s r = Some obj \<and> (case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>fst (lookupAround2 src (ksPSpace s)) = Some (a, b); cte_check b src a (snd (lookupAround2 src (ksPSpace s)))\<rbrakk> \<Longrightarrow> \<exists>obj. ksPSpace s a = Some obj \<and> (case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cte_check b src a (snd (lookupAround2 src (ksPSpace s))); a \<le> src; ksPSpace s a = Some b; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (8 subgoals):
 1. \<And>s a b x1. \<lbrakk>cte_check b src a (snd (lookupAround2 src (ksPSpace s))); a \<le> src; ksPSpace s a = Some b; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; b = KOEndpoint x1\<rbrakk> \<Longrightarrow> case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False
 2. \<And>s a b x2. \<lbrakk>cte_check b src a (snd (lookupAround2 src (ksPSpace s))); a \<le> src; ksPSpace s a = Some b; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; b = KONotification x2\<rbrakk> \<Longrightarrow> case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False
 3. \<And>s a b. \<lbrakk>cte_check b src a (snd (lookupAround2 src (ksPSpace s))); a \<le> src; ksPSpace s a = Some b; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; b = KOKernelData\<rbrakk> \<Longrightarrow> case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False
 4. \<And>s a b. \<lbrakk>cte_check b src a (snd (lookupAround2 src (ksPSpace s))); a \<le> src; ksPSpace s a = Some b; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; b = KOUserData\<rbrakk> \<Longrightarrow> case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False
 5. \<And>s a b. \<lbrakk>cte_check b src a (snd (lookupAround2 src (ksPSpace s))); a \<le> src; ksPSpace s a = Some b; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; b = KOUserDataDevice\<rbrakk> \<Longrightarrow> case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False
 6. \<And>s a b x6. \<lbrakk>cte_check b src a (snd (lookupAround2 src (ksPSpace s))); a \<le> src; ksPSpace s a = Some b; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; b = KOTCB x6\<rbrakk> \<Longrightarrow> case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False
 7. \<And>s a b x7. \<lbrakk>cte_check b src a (snd (lookupAround2 src (ksPSpace s))); a \<le> src; ksPSpace s a = Some b; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; b = KOCTE x7\<rbrakk> \<Longrightarrow> case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False
 8. \<And>s a b x8. \<lbrakk>cte_check b src a (snd (lookupAround2 src (ksPSpace s))); a \<le> src; ksPSpace s a = Some b; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; b = KOArch x8\<rbrakk> \<Longrightarrow> case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal:
No subgoals!