theory Detype_AI

lemma non_null_present:
    "\<And>p. cte_wp_at ((\<noteq>) cap.NullCap) p s \<Longrightarrow> fst p \<notin> untyped_range cap" apply (drule if_unsafe_then_capD[OF _ ifunsafe], simp) apply (drule ex_cte_cap_to_obj_ref_disj, erule disjE) apply clarsimp apply (erule untyped_children_in_mdbEE[OF child cap untyped]) apply blast apply (drule descendants_range_inD[OF drange]) apply (simp add:cte_wp_at_caps_of_state) apply (simp add:untyped) apply (clarsimp simp: irq_node) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p. cte_wp_at ((\<noteq>) NullCap) p s \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>p. ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. NullCap \<noteq> cap' \<and> appropriate_cte_cap cap' cap) p s \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>p. \<exists>ptr'. cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) ptr' s \<Longrightarrow> fst p \<notin> untyped_range cap
 2. \<And>p. \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, []) \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>a aa ba. \<lbrakk>cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, ba) s; a \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, []) \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>a aa ba cap'. \<lbrakk>a \<in> untyped_range cap; cte_wp_at ((=) cap') (aa, ba) s; a \<in> obj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {}
 2. \<And>a aa ba cap'. \<lbrakk>a \<in> untyped_range cap; cte_wp_at ((=) cap') (aa, ba) s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; (aa, ba) \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<And>p. \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, []) \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>a aa ba cap'. \<lbrakk>a \<in> untyped_range cap; cte_wp_at ((=) cap') (aa, ba) s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; (aa, ba) \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, []) \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>a aa ba cap'. \<lbrakk>a \<in> untyped_range cap; cte_wp_at ((=) cap') (aa, ba) s; cap_range cap' \<inter> untyped_range cap \<noteq> {}\<rbrakk> \<Longrightarrow> caps_of_state s (aa, ba) = Some (?cap28 a aa ba cap')
 2. \<And>a aa ba cap'. \<lbrakk>a \<in> untyped_range cap; cte_wp_at ((=) cap') (aa, ba) s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; cap_range (?cap28 a aa ba cap') \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False
 3. \<And>p. \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, []) \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>a aa ba cap'. \<lbrakk>a \<in> untyped_range cap; cte_wp_at ((=) cap') (aa, ba) s; cap_range cap' \<inter> untyped_range cap \<noteq> {}; cap_range cap' \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, []) \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>p. \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, []) \<Longrightarrow> fst p \<notin> untyped_range cap proof (prove)
goal:
No subgoals!