theory Detype_AI

lemma untyped_children_in_mdbEE:
  assumes ass: "untyped_children_in_mdb s" "cte_wp_at ((=) cap) ptr s" "is_untyped_cap cap" "cte_wp_at P ptr' s"
  and  step1: "\<And>cap'. \<lbrakk>cte_wp_at ((=) cap') ptr' s; P cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {}"
  and  step2: "\<And>cap'. \<lbrakk>cte_wp_at ((=) cap') ptr' s; cap_range cap' \<inter> untyped_range cap \<noteq> {};ptr' \<in> descendants_of ptr (cdt s) \<rbrakk> \<Longrightarrow> Q"
  shows "Q" using ass apply (clarsimp simp:cte_wp_at_caps_of_state) apply (rule step2) apply (simp add:cte_wp_at_caps_of_state) apply (drule step1[rotated]) apply (simp add:cte_wp_at_caps_of_state) apply (simp add:cap_range_def) apply blast apply (simp add:untyped_children_in_mdb_def del:split_paired_All) apply (drule_tac x = ptr in spec) apply (drule_tac x = ptr' in spec) apply (erule impE) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (drule step1[rotated]) apply (clarsimp simp:cte_wp_at_caps_of_state)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q proof (prove)
using this:
untyped_children_in_mdb s
cte_wp_at ((=) cap) ptr s
is_untyped_cap cap
cte_wp_at P ptr' s

goal (1 subgoal):
 1. Q proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (3 subgoals):
 1. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap'6 capa)) ptr' s
 2. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa\<rbrakk> \<Longrightarrow> cap_range (?cap'6 capa) \<inter> untyped_range cap \<noteq> {}
 3. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa\<rbrakk> \<Longrightarrow> cap_range capa \<inter> untyped_range cap \<noteq> {}
 2. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa\<rbrakk> \<Longrightarrow> cte_wp_at ((=) capa) ptr' s
 2. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; obj_refs capa \<inter> untyped_range cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_range capa \<inter> untyped_range cap \<noteq> {}
 3. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; obj_refs capa \<inter> untyped_range cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap_range capa \<inter> untyped_range cap \<noteq> {}
 2. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; obj_refs capa \<inter> untyped_range cap \<noteq> {}\<rbrakk> \<Longrightarrow> (untyped_range capa \<union> obj_refs capa) \<inter> untyped_range cap \<noteq> {}
 2. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>untyped_children_in_mdb s; caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>\<forall>ptr ptr'. (\<exists>cap. cte_wp_at ((=) cap) ptr s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>cap'. obj_refs cap' \<inter> untyped_range cap \<noteq> {}) ptr' s) \<longrightarrow> ptr' \<in> descendants_of ptr (cdt s); caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa; \<forall>ptr'. (\<exists>cap. cte_wp_at ((=) cap) ptr s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>cap'. obj_refs cap' \<inter> untyped_range cap \<noteq> {}) ptr' s) \<longrightarrow> ptr' \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa; (\<exists>cap. cte_wp_at ((=) cap) ptr s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>cap'. obj_refs cap' \<inter> untyped_range cap \<noteq> {}) ptr' s) \<longrightarrow> ptr' \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at ((=) cap) ptr s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>cap'. obj_refs cap' \<inter> untyped_range cap \<noteq> {}) ptr' s
 2. \<And>capa. \<lbrakk>caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa; ptr' \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa; obj_refs capa \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>capa. \<lbrakk>caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa; ptr' \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>capa. \<lbrakk>caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; obj_refs capa \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) capa) ptr' s
 2. \<And>capa. \<lbrakk>caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; obj_refs capa \<inter> untyped_range cap = {}; obj_refs capa \<inter> untyped_range cap \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>capa. \<lbrakk>caps_of_state s ptr = Some cap; is_untyped_cap cap; caps_of_state s ptr' = Some capa; P capa; ptr' \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr (cdt s) proof (prove)
goal:
No subgoals!