theory Detype_R

lemma magnitudeCheck_det:
  "\<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko);
    ps_clear ptr (objBitsKO ko) s\<rbrakk>
   \<Longrightarrow> magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s)))
                          (objBitsKO ko) s =
       ({((), s)},False)" apply (frule in_magnitude_check'[THEN iffD2]) apply (case_tac ko) apply (simp add: objBits_simps' pageBits_def)+ apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object) apply (simp add:archObjSize_def pageBits_def pteBits_def pdeBits_def)+ apply (subgoal_tac
    "\<not> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s)") apply (drule singleton_in_magnitude_check) apply (drule_tac x = s in spec) apply (case_tac
    "(magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s)") apply simp apply (rule ccontr) apply (clarsimp simp:magnitudeCheck_assert assert_def fail_def return_def
    split:if_splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s = ({((), s)}, False) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBitsKO ko
 2. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ksPSpace ?s ptr = Some ?y
 3. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ?ps = ksPSpace ?s
 4. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ?s' = ?s \<and> ps_clear ptr (objBitsKO ko) ?s
 5. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; (?v, ?s') \<in> fst (magnitudeCheck ptr (snd (lookupAround2 ptr ?ps)) (objBitsKO ko) ?s)\<rbrakk> \<Longrightarrow> magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s = ({((), s)}, False) proof (prove)
goal (12 subgoals):
 1. \<And>x1. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ko = KOEndpoint x1\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBitsKO ko
 2. \<And>x2. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ko = KONotification x2\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBitsKO ko
 3. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ko = KOKernelData\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBitsKO ko
 4. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ko = KOUserData\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBitsKO ko
 5. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ko = KOUserDataDevice\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBitsKO ko
 6. \<And>x6. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ko = KOTCB x6\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBitsKO ko
 7. \<And>x7. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ko = KOCTE x7\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBitsKO ko
 8. \<And>x8. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ko = KOArch x8\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBitsKO ko
 9. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ksPSpace ?s ptr = Some ?y
 10. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ?ps = ksPSpace ?s
A total of 12 subgoals... proof (prove)
goal (5 subgoals):
 1. \<And>x8. \<lbrakk>ksPSpace s ptr = Some (KOArch x8); is_aligned ptr (archObjSize x8); ps_clear ptr (archObjSize x8) s; ko = KOArch x8\<rbrakk> \<Longrightarrow> 1 < 2 ^ archObjSize x8
 2. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ksPSpace ?s ptr = Some ?y
 3. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ?ps = ksPSpace ?s
 4. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ?s' = ?s \<and> ps_clear ptr (objBitsKO ko) ?s
 5. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; (?v, ?s') \<in> fst (magnitudeCheck ptr (snd (lookupAround2 ptr ?ps)) (objBitsKO ko) ?s)\<rbrakk> \<Longrightarrow> magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s = ({((), s)}, False) proof (prove)
goal (5 subgoals):
 1. \<And>arch_kernel_object. \<lbrakk>ksPSpace s ptr = Some (KOArch arch_kernel_object); is_aligned ptr (archObjSize arch_kernel_object); ps_clear ptr (archObjSize arch_kernel_object) s; ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> 1 < 2 ^ archObjSize arch_kernel_object
 2. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ksPSpace ?s ptr = Some ?y
 3. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ?ps = ksPSpace ?s
 4. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ?s' = ?s \<and> ps_clear ptr (objBitsKO ko) ?s
 5. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; (?v, ?s') \<in> fst (magnitudeCheck ptr (snd (lookupAround2 ptr ?ps)) (objBitsKO ko) ?s)\<rbrakk> \<Longrightarrow> magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s = ({((), s)}, False) proof (prove)
goal (7 subgoals):
 1. \<And>arch_kernel_object x1. \<lbrakk>ksPSpace s ptr = Some (KOArch arch_kernel_object); is_aligned ptr (archObjSize arch_kernel_object); ps_clear ptr (archObjSize arch_kernel_object) s; ko = KOArch arch_kernel_object; arch_kernel_object = KOASIDPool x1\<rbrakk> \<Longrightarrow> 1 < 2 ^ archObjSize arch_kernel_object
 2. \<And>arch_kernel_object x2. \<lbrakk>ksPSpace s ptr = Some (KOArch arch_kernel_object); is_aligned ptr (archObjSize arch_kernel_object); ps_clear ptr (archObjSize arch_kernel_object) s; ko = KOArch arch_kernel_object; arch_kernel_object = KOPTE x2\<rbrakk> \<Longrightarrow> 1 < 2 ^ archObjSize arch_kernel_object
 3. \<And>arch_kernel_object x3. \<lbrakk>ksPSpace s ptr = Some (KOArch arch_kernel_object); is_aligned ptr (archObjSize arch_kernel_object); ps_clear ptr (archObjSize arch_kernel_object) s; ko = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> 1 < 2 ^ archObjSize arch_kernel_object
 4. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ksPSpace ?s ptr = Some ?y
 5. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ?ps = ksPSpace ?s
 6. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ?s' = ?s \<and> ps_clear ptr (objBitsKO ko) ?s
 7. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; (?v, ?s') \<in> fst (magnitudeCheck ptr (snd (lookupAround2 ptr ?ps)) (objBitsKO ko) ?s)\<rbrakk> \<Longrightarrow> magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s = ({((), s)}, False) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ((), s) \<in> fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s)\<rbrakk> \<Longrightarrow> magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s = ({((), s)}, False) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ((), s) \<in> fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s); \<not> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s)\<rbrakk> \<Longrightarrow> magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s = ({((), s)}, False)
 2. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ((), s) \<in> fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s)\<rbrakk> \<Longrightarrow> \<not> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; \<not> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s); \<forall>s'. fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s') = {((), s')}\<rbrakk> \<Longrightarrow> magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s = ({((), s)}, False)
 2. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ((), s) \<in> fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s)\<rbrakk> \<Longrightarrow> \<not> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; \<not> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s); fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s) = {((), s)}\<rbrakk> \<Longrightarrow> magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s = ({((), s)}, False)
 2. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ((), s) \<in> fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s)\<rbrakk> \<Longrightarrow> \<not> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; \<not> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s); fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s) = {((), s)}; magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s = (a, b)\<rbrakk> \<Longrightarrow> magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s = ({((), s)}, False)
 2. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ((), s) \<in> fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s)\<rbrakk> \<Longrightarrow> \<not> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ((), s) \<in> fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s)\<rbrakk> \<Longrightarrow> \<not> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; ((), s) \<in> fst (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s); \<not> \<not> snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!