theory Detype_AI

lemma descendants_inc_empty_slot:
  assumes desc_inc :"descendants_inc m cs'"
  assumes mdb:"mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> cap.NullCap \<noteq> c) m"
  assumes dom:"\<forall>x\<in> dom cs.  (cs' x = cs x)"
  shows "descendants_inc m cs" using desc_inc apply (simp add:descendants_inc_def del:split_paired_All) apply (intro allI impI) apply (drule spec)+ apply (erule(1) impE) apply (simp add:descendants_of_def) apply (frule tranclD) apply (drule tranclD2) apply (simp add:cdt_parent_rel_def is_cdt_parent_def) apply (elim exE conjE) apply (drule mdb_cte_atD[OF _ mdb])+ apply (elim exE conjE) apply (drule bspec[OF dom,OF domI])+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_inc m cs proof (prove)
using this:
descendants_inc m cs'

goal (1 subgoal):
 1. descendants_inc m cs proof (prove)
goal (1 subgoal):
 1. \<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs' p)) = cap_class (the (cs' p')) \<and> cap_range (the (cs' p)) \<subseteq> cap_range (the (cs' p')) \<Longrightarrow> \<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs' p)) = cap_class (the (cs' p')) \<and> cap_range (the (cs' p)) \<subseteq> cap_range (the (cs' p')); p \<in> descendants_of p' m\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> descendants_of p' m; ?p4 p p' \<in> descendants_of (?p'6 p p') m \<longrightarrow> cap_class (the (cs' (?p4 p p'))) = cap_class (the (cs' (?p'6 p p'))) \<and> cap_range (the (cs' (?p4 p p'))) \<subseteq> cap_range (the (cs' (?p'6 p p')))\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>p \<in> descendants_of p' m; cap_class (the (cs' p)) = cap_class (the (cs' p')) \<and> cap_range (the (cs' p)) \<subseteq> cap_range (the (cs' p'))\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>m \<Turnstile> p' \<rightarrow> p; cap_class (the (cs' p)) = cap_class (the (cs' p')) \<and> cap_range (the (cs' p)) \<subseteq> cap_range (the (cs' p'))\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>m \<Turnstile> p' \<rightarrow> p; cap_class (the (cs' p)) = cap_class (the (cs' p')) \<and> cap_range (the (cs' p)) \<subseteq> cap_range (the (cs' p')); \<exists>z. m \<Turnstile> p' \<leadsto> z \<and> m \<Turnstile> z \<rightarrow>* p\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>cap_class (the (cs' p)) = cap_class (the (cs' p')) \<and> cap_range (the (cs' p)) \<subseteq> cap_range (the (cs' p')); \<exists>z. m \<Turnstile> p' \<leadsto> z \<and> m \<Turnstile> z \<rightarrow>* p; \<exists>z. m \<Turnstile> p' \<rightarrow>* z \<and> m \<Turnstile> z \<leadsto> p\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>cap_class (the (cs' p)) = cap_class (the (cs' p')) \<and> cap_range (the (cs' p)) \<subseteq> cap_range (the (cs' p')); \<exists>a b. m (a, b) = Some p' \<and> ((a, b), p) \<in> {(p, c). m c = Some p}\<^sup>*; \<exists>a b. (p', a, b) \<in> {(p, c). m c = Some p}\<^sup>* \<and> m p = Some (a, b)\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' a aa b ba. \<lbrakk>cap_class (the (cs' p)) = cap_class (the (cs' p')); cap_range (the (cs' p)) \<subseteq> cap_range (the (cs' p')); m (a, b) = Some p'; ((a, b), p) \<in> {(p, c). m c = Some p}\<^sup>*; (p', aa, ba) \<in> {(p, c). m c = Some p}\<^sup>*; m p = Some (aa, ba)\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' a aa b ba. \<lbrakk>cap_class (the (cs' p)) = cap_class (the (cs' p')); cap_range (the (cs' p)) \<subseteq> cap_range (the (cs' p')); ((a, b), p) \<in> {(p, c). m c = Some p}\<^sup>*; (p', aa, ba) \<in> {(p, c). m c = Some p}\<^sup>*; (\<exists>c. cs p' = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c); (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs p = Some c \<and> NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' a aa b ba c ca cb cc. \<lbrakk>cap_class (the (cs' p)) = cap_class (the (cs' p')); cap_range (the (cs' p)) \<subseteq> cap_range (the (cs' p')); ((a, b), p) \<in> {(p, c). m c = Some p}\<^sup>*; (p', aa, ba) \<in> {(p, c). m c = Some p}\<^sup>*; cs p' = Some c; NullCap \<noteq> c; cs (a, b) = Some ca; NullCap \<noteq> ca; cs (aa, ba) = Some cb; NullCap \<noteq> cb; cs p = Some cc; NullCap \<noteq> cc\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' a aa b ba c ca cb cc. \<lbrakk>cap_class (the (cs' p)) = cap_class (the (cs' p')); cap_range (the (cs' p)) \<subseteq> cap_range (the (cs' p')); ((a, b), p) \<in> {(p, c). m c = Some p}\<^sup>*; (p', aa, ba) \<in> {(p, c). m c = Some p}\<^sup>*; NullCap \<noteq> c; NullCap \<noteq> ca; NullCap \<noteq> cb; NullCap \<noteq> cc; cs' p' = cs p'; cs' (a, b) = cs (a, b); cs' (aa, ba) = cs (aa, ba); cs' p = cs p\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal:
No subgoals!