theory Detype_AI

lemma no_obj_refs:
  "\<And>slot cap' x. \<lbrakk> caps_of_state s slot = Some cap';
                   x \<in> obj_refs cap'; x \<in> untyped_range cap \<rbrakk> \<Longrightarrow> False" using cap untyped apply (clarsimp simp: cte_wp_at_caps_of_state) apply (drule (2) untyped_mdbD) apply blast apply (rule ut_mdb) apply (drule descendants_range_inD[OF drange]) apply (simp add:cte_wp_at_caps_of_state) apply (simp add:cap_range_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>slot cap' x. \<lbrakk>caps_of_state s slot = Some cap'; x \<in> obj_refs cap'; x \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
cte_wp_at ((=) cap) ptr s
is_untyped_cap cap

goal (1 subgoal):
 1. \<And>slot cap' x. \<lbrakk>caps_of_state s slot = Some cap'; x \<in> obj_refs cap'; x \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap' x. \<lbrakk>caps_of_state s (a, b) = Some cap'; x \<in> obj_refs cap'; x \<in> untyped_range cap; caps_of_state s ptr = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b cap' x. \<lbrakk>caps_of_state s (a, b) = Some cap'; x \<in> obj_refs cap'; x \<in> untyped_range cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {}
 2. \<And>a b cap' x. \<lbrakk>caps_of_state s (a, b) = Some cap'; x \<in> obj_refs cap'; x \<in> untyped_range cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> untyped_mdb (?m2 a b cap' x) (caps_of_state s)
 3. \<And>a b cap' x. \<lbrakk>caps_of_state s (a, b) = Some cap'; x \<in> obj_refs cap'; x \<in> untyped_range cap; is_untyped_cap cap; (a, b) \<in> descendants_of ptr (?m2 a b cap' x)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b cap' x. \<lbrakk>caps_of_state s (a, b) = Some cap'; x \<in> obj_refs cap'; x \<in> untyped_range cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> untyped_mdb (?m2 a b cap' x) (caps_of_state s)
 2. \<And>a b cap' x. \<lbrakk>caps_of_state s (a, b) = Some cap'; x \<in> obj_refs cap'; x \<in> untyped_range cap; is_untyped_cap cap; (a, b) \<in> descendants_of ptr (?m2 a b cap' x)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap' x. \<lbrakk>caps_of_state s (a, b) = Some cap'; x \<in> obj_refs cap'; x \<in> untyped_range cap; is_untyped_cap cap; (a, b) \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b cap' x. \<lbrakk>caps_of_state s (a, b) = Some cap'; x \<in> obj_refs cap'; x \<in> untyped_range cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> caps_of_state s (a, b) = Some (?cap17 a b cap' x)
 2. \<And>a b cap' x. \<lbrakk>caps_of_state s (a, b) = Some cap'; x \<in> obj_refs cap'; x \<in> untyped_range cap; is_untyped_cap cap; cap_range (?cap17 a b cap' x) \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap' x. \<lbrakk>caps_of_state s (a, b) = Some cap'; x \<in> obj_refs cap'; x \<in> untyped_range cap; is_untyped_cap cap; cap_range cap' \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap' x. \<lbrakk>caps_of_state s (a, b) = Some cap'; x \<in> obj_refs cap'; x \<in> untyped_range cap; is_untyped_cap cap; (untyped_range cap' \<union> obj_refs cap') \<inter> (untyped_range cap \<union> obj_refs cap) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!