theory Detype_AI

lemma valid_cap2:
    "\<And>cap'. \<lbrakk> \<exists>p. cte_wp_at ((=) cap') p s \<rbrakk>
    \<Longrightarrow> obj_reply_refs cap' \<subseteq> (UNIV - untyped_range cap)" apply clarsimp apply (simp add: obj_reply_refs_def, erule disjE) 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 split: cap.split_asm bool.split_asm) apply (rename_tac t master rights) apply (case_tac master, simp_all) apply (frule valid_reply_mastersD' [OF _ vmaster]) apply (fastforce simp: cte_wp_at_caps_of_state dest: non_null_caps) apply (subgoal_tac "has_reply_cap t s") apply (drule valid_reply_capsD [OF _ vreply]) apply (simp add: pred_tcb_at_def) apply (fastforce simp: live_def dest: live_okE) apply (fastforce simp: has_reply_cap_def is_reply_cap_to_def elim:cte_wp_at_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<exists>p. cte_wp_at ((=) cap') p s \<Longrightarrow> obj_reply_refs cap' \<subseteq> UNIV - untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap' x a b. \<lbrakk>x \<in> obj_reply_refs cap'; cte_wp_at ((=) cap') (a, b) s; x \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cap' x a b. \<lbrakk>cte_wp_at ((=) cap') (a, b) s; x \<in> untyped_range cap; x \<in> obj_refs cap'\<rbrakk> \<Longrightarrow> False
 2. \<And>cap' x a b. \<lbrakk>cte_wp_at ((=) cap') (a, b) s; x \<in> untyped_range cap; x \<in> (case cap' of ReplyCap t m R \<Rightarrow> {t} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cap' x a b cap'a. \<lbrakk>x \<in> untyped_range cap; x \<in> obj_refs cap'; cte_wp_at ((=) cap'a) (a, b) s; cap' = cap'a\<rbrakk> \<Longrightarrow> obj_refs cap'a \<inter> untyped_range cap \<noteq> {}
 2. \<And>cap' x a b cap'a. \<lbrakk>x \<in> untyped_range cap; x \<in> obj_refs cap'; cte_wp_at ((=) cap'a) (a, b) s; cap_range cap'a \<inter> untyped_range cap \<noteq> {}; (a, b) \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<And>cap' x a b. \<lbrakk>cte_wp_at ((=) cap') (a, b) s; x \<in> untyped_range cap; x \<in> (case cap' of ReplyCap t m R \<Rightarrow> {t} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cap' x a b cap'a. \<lbrakk>x \<in> untyped_range cap; x \<in> obj_refs cap'; cte_wp_at ((=) cap'a) (a, b) s; cap_range cap'a \<inter> untyped_range cap \<noteq> {}; (a, b) \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<And>cap' x a b. \<lbrakk>cte_wp_at ((=) cap') (a, b) s; x \<in> untyped_range cap; x \<in> (case cap' of ReplyCap t m R \<Rightarrow> {t} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cap' x a b cap'a. \<lbrakk>x \<in> untyped_range cap; x \<in> obj_refs cap'; cte_wp_at ((=) cap'a) (a, b) s; cap_range cap'a \<inter> untyped_range cap \<noteq> {}\<rbrakk> \<Longrightarrow> caps_of_state s (a, b) = Some (?cap30 cap' x a b cap'a)
 2. \<And>cap' x a b cap'a. \<lbrakk>x \<in> untyped_range cap; x \<in> obj_refs cap'; cte_wp_at ((=) cap'a) (a, b) s; cap_range cap'a \<inter> untyped_range cap \<noteq> {}; cap_range (?cap30 cap' x a b cap'a) \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False
 3. \<And>cap' x a b. \<lbrakk>cte_wp_at ((=) cap') (a, b) s; x \<in> untyped_range cap; x \<in> (case cap' of ReplyCap t m R \<Rightarrow> {t} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cap' x a b cap'a. \<lbrakk>x \<in> untyped_range cap; x \<in> obj_refs cap'; cte_wp_at ((=) cap'a) (a, b) s; cap_range cap'a \<inter> untyped_range cap \<noteq> {}; cap_range cap'a \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cap' x a b. \<lbrakk>cte_wp_at ((=) cap') (a, b) s; x \<in> untyped_range cap; x \<in> (case cap' of ReplyCap t m R \<Rightarrow> {t} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap' x a b. \<lbrakk>cte_wp_at ((=) cap') (a, b) s; x \<in> untyped_range cap; x \<in> (case cap' of ReplyCap t m R \<Rightarrow> {t} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b x51 x52 x53. \<lbrakk>cte_wp_at ((=) (ReplyCap x51 x52 x53)) (a, b) s; x51 \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b t master rights. \<lbrakk>cte_wp_at ((=) (ReplyCap t master rights)) (a, b) s; t \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b t master rights. \<lbrakk>cte_wp_at ((=) (ReplyCap t True rights)) (a, b) s; t \<in> untyped_range cap; master\<rbrakk> \<Longrightarrow> False
 2. \<And>a b t master rights. \<lbrakk>cte_wp_at ((=) (ReplyCap t False rights)) (a, b) s; t \<in> untyped_range cap; \<not> master\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b t master rights. \<lbrakk>cte_wp_at ((=) (ReplyCap t True rights)) (a, b) s; t \<in> untyped_range cap; master; (a, b) = (t, tcb_cnode_index 2)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b t master rights. \<lbrakk>cte_wp_at ((=) (ReplyCap t False rights)) (a, b) s; t \<in> untyped_range cap; \<not> master\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b t master rights. \<lbrakk>cte_wp_at ((=) (ReplyCap t False rights)) (a, b) s; t \<in> untyped_range cap; \<not> master\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b t master rights. \<lbrakk>cte_wp_at ((=) (ReplyCap t False rights)) (a, b) s; t \<in> untyped_range cap; \<not> master; has_reply_cap t s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b t master rights. \<lbrakk>cte_wp_at ((=) (ReplyCap t False rights)) (a, b) s; t \<in> untyped_range cap; \<not> master\<rbrakk> \<Longrightarrow> has_reply_cap t s proof (prove)
goal (2 subgoals):
 1. \<And>a b t master rights. \<lbrakk>cte_wp_at ((=) (ReplyCap t False rights)) (a, b) s; t \<in> untyped_range cap; \<not> master; st_tcb_at awaiting_reply t s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b t master rights. \<lbrakk>cte_wp_at ((=) (ReplyCap t False rights)) (a, b) s; t \<in> untyped_range cap; \<not> master\<rbrakk> \<Longrightarrow> has_reply_cap t s proof (prove)
goal (2 subgoals):
 1. \<And>a b t master rights. \<lbrakk>cte_wp_at ((=) (ReplyCap t False rights)) (a, b) s; t \<in> untyped_range cap; \<not> master; obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> awaiting_reply (tcb_state tcb)) t s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b t master rights. \<lbrakk>cte_wp_at ((=) (ReplyCap t False rights)) (a, b) s; t \<in> untyped_range cap; \<not> master\<rbrakk> \<Longrightarrow> has_reply_cap t s proof (prove)
goal (1 subgoal):
 1. \<And>a b t master rights. \<lbrakk>cte_wp_at ((=) (ReplyCap t False rights)) (a, b) s; t \<in> untyped_range cap; \<not> master\<rbrakk> \<Longrightarrow> has_reply_cap t s proof (prove)
goal:
No subgoals!