theory CSpaceInv_AI

lemma descendants_inc_minor:
  "\<lbrakk>descendants_inc m cs; mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> cap.NullCap \<noteq> c) m;
   \<forall>x\<in> dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x))\<rbrakk>
  \<Longrightarrow> descendants_inc m cs'" apply (simp add: descendants_inc_def del: split_paired_All) apply (intro impI allI) apply (drule spec)+ apply (erule(1) impE) apply (clarsimp simp: descendants_of_def) apply (frule tranclD) apply (drule tranclD2) apply (simp add: cdt_parent_rel_def is_cdt_parent_def) apply (elim conjE exE) apply (drule(1) mdb_cte_atD)+ apply (elim conjE exE) apply (drule_tac m1 = cs in bspec[OF _ domI,rotated],assumption)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_inc m cs; mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<forall>x\<in>dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x))\<rbrakk> \<Longrightarrow> descendants_inc m cs' proof (prove)
goal (1 subgoal):
 1. \<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')); mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<forall>x\<in>dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x))\<rbrakk> \<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')); mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<forall>x\<in>dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x)); 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>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<forall>x\<in>dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x)); p \<in> descendants_of p' m; ?p3 p p' \<in> descendants_of (?p'5 p p') m \<longrightarrow> cap_class (the (cs (?p3 p p'))) = cap_class (the (cs (?p'5 p p'))) \<and> cap_range (the (cs (?p3 p p'))) \<subseteq> cap_range (the (cs (?p'5 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>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<forall>x\<in>dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x)); 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>a b aa ba. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<forall>x\<in>dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x)); m \<Turnstile> (aa, ba) \<rightarrow> (a, b); cap_class (the (cs (a, b))) = cap_class (the (cs (aa, ba))); cap_range (the (cs (a, b))) \<subseteq> cap_range (the (cs (aa, ba)))\<rbrakk> \<Longrightarrow> cap_class (the (cs' (a, b))) = cap_class (the (cs' (aa, ba))) \<and> cap_range (the (cs' (a, b))) \<subseteq> cap_range (the (cs' (aa, ba))) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<forall>x\<in>dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x)); m \<Turnstile> (aa, ba) \<rightarrow> (a, b); cap_class (the (cs (a, b))) = cap_class (the (cs (aa, ba))); cap_range (the (cs (a, b))) \<subseteq> cap_range (the (cs (aa, ba))); \<exists>z. m \<Turnstile> (aa, ba) \<leadsto> z \<and> m \<Turnstile> z \<rightarrow>* (a, b)\<rbrakk> \<Longrightarrow> cap_class (the (cs' (a, b))) = cap_class (the (cs' (aa, ba))) \<and> cap_range (the (cs' (a, b))) \<subseteq> cap_range (the (cs' (aa, ba))) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<forall>x\<in>dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x)); cap_class (the (cs (a, b))) = cap_class (the (cs (aa, ba))); cap_range (the (cs (a, b))) \<subseteq> cap_range (the (cs (aa, ba))); \<exists>z. m \<Turnstile> (aa, ba) \<leadsto> z \<and> m \<Turnstile> z \<rightarrow>* (a, b); \<exists>z. m \<Turnstile> (aa, ba) \<rightarrow>* z \<and> m \<Turnstile> z \<leadsto> (a, b)\<rbrakk> \<Longrightarrow> cap_class (the (cs' (a, b))) = cap_class (the (cs' (aa, ba))) \<and> cap_range (the (cs' (a, b))) \<subseteq> cap_range (the (cs' (aa, ba))) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<forall>x\<in>dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x)); cap_class (the (cs (a, b))) = cap_class (the (cs (aa, ba))); cap_range (the (cs (a, b))) \<subseteq> cap_range (the (cs (aa, ba))); \<exists>ab bb. m (ab, bb) = Some (aa, ba) \<and> ((ab, bb), a, b) \<in> {(p, c). m c = Some p}\<^sup>*; \<exists>ab bb. ((aa, ba), ab, bb) \<in> {(p, c). m c = Some p}\<^sup>* \<and> m (a, b) = Some (ab, bb)\<rbrakk> \<Longrightarrow> cap_class (the (cs' (a, b))) = cap_class (the (cs' (aa, ba))) \<and> cap_range (the (cs' (a, b))) \<subseteq> cap_range (the (cs' (aa, ba))) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab ac bb bc. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<forall>x\<in>dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x)); cap_class (the (cs (a, b))) = cap_class (the (cs (aa, ba))); cap_range (the (cs (a, b))) \<subseteq> cap_range (the (cs (aa, ba))); m (ab, bb) = Some (aa, ba); ((ab, bb), a, b) \<in> {(p, c). m c = Some p}\<^sup>*; ((aa, ba), ac, bc) \<in> {(p, c). m c = Some p}\<^sup>*; m (a, b) = Some (ac, bc)\<rbrakk> \<Longrightarrow> cap_class (the (cs' (a, b))) = cap_class (the (cs' (aa, ba))) \<and> cap_range (the (cs' (a, b))) \<subseteq> cap_range (the (cs' (aa, ba))) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab ac bb bc. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<forall>x\<in>dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x)); cap_class (the (cs (a, b))) = cap_class (the (cs (aa, ba))); cap_range (the (cs (a, b))) \<subseteq> cap_range (the (cs (aa, ba))); ((ab, bb), a, b) \<in> {(p, c). m c = Some p}\<^sup>*; ((aa, ba), ac, bc) \<in> {(p, c). m c = Some p}\<^sup>*; (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (ab, bb) = Some c \<and> NullCap \<noteq> c); (\<exists>c. cs (ac, bc) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> cap_class (the (cs' (a, b))) = cap_class (the (cs' (aa, ba))) \<and> cap_range (the (cs' (a, b))) \<subseteq> cap_range (the (cs' (aa, ba))) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab ac bb bc c ca cb cc. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<forall>x\<in>dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x)); cap_class (the (cs (a, b))) = cap_class (the (cs (aa, ba))); cap_range (the (cs (a, b))) \<subseteq> cap_range (the (cs (aa, ba))); ((ab, bb), a, b) \<in> {(p, c). m c = Some p}\<^sup>*; ((aa, ba), ac, bc) \<in> {(p, c). m c = Some p}\<^sup>*; cs (aa, ba) = Some c; NullCap \<noteq> c; cs (ab, bb) = Some ca; NullCap \<noteq> ca; cs (ac, bc) = Some cb; NullCap \<noteq> cb; cs (a, b) = Some cc; NullCap \<noteq> cc\<rbrakk> \<Longrightarrow> cap_class (the (cs' (a, b))) = cap_class (the (cs' (aa, ba))) \<and> cap_range (the (cs' (a, b))) \<subseteq> cap_range (the (cs' (aa, ba))) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab ac bb bc c ca cb cc. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<forall>x\<in>dom cs. cap_class (the (cs' x)) = cap_class (the (cs x)) \<and> cap_range (the (cs' x)) = cap_range (the (cs x)); cap_class (the (cs (a, b))) = cap_class (the (cs (aa, ba))); cap_range (the (cs (a, b))) \<subseteq> cap_range (the (cs (aa, ba))); ((ab, bb), a, b) \<in> {(p, c). m c = Some p}\<^sup>*; ((aa, ba), ac, bc) \<in> {(p, c). m c = Some p}\<^sup>*; NullCap \<noteq> c; NullCap \<noteq> ca; NullCap \<noteq> cb; NullCap \<noteq> cc; cap_class (the (cs' (aa, ba))) = cap_class (the (cs (aa, ba))) \<and> cap_range (the (cs' (aa, ba))) = cap_range (the (cs (aa, ba))); cap_class (the (cs' (ab, bb))) = cap_class (the (cs (ab, bb))) \<and> cap_range (the (cs' (ab, bb))) = cap_range (the (cs (ab, bb))); cap_class (the (cs' (ac, bc))) = cap_class (the (cs (ac, bc))) \<and> cap_range (the (cs' (ac, bc))) = cap_range (the (cs (ac, bc))); cap_class (the (cs' (a, b))) = cap_class (the (cs (a, b))) \<and> cap_range (the (cs' (a, b))) = cap_range (the (cs (a, b)))\<rbrakk> \<Longrightarrow> cap_class (the (cs' (a, b))) = cap_class (the (cs' (aa, ba))) \<and> cap_range (the (cs' (a, b))) \<subseteq> cap_range (the (cs' (aa, ba))) proof (prove)
goal:
No subgoals!