theory CSpace_AI

lemma descendants_inc:
  notes  split_paired_All[simp del]
  assumes dc: "descendants_inc m cs"
  assumes s: "cs src = Some src_cap"
  assumes d: "cs dest = Some cap.NullCap"
  assumes c: "weak_derived cap src_cap"
  shows "descendants_inc m' (cs (dest \<mapsto> cap, src \<mapsto> cap.NullCap))" using dc s d c apply (simp add: descendants_inc_def descendants) apply (intro allI conjI) apply (intro impI allI) apply (drule spec)+ apply (erule(1) impE) apply (simp add:weak_derived_cap_range) apply (simp add:descendants_of_def) apply (intro impI) apply (drule spec)+ apply (erule(1) impE) apply (simp add:weak_derived_cap_range) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_inc m' (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) proof (prove)
using this:
descendants_inc m cs
cs src = Some src_cap
cs dest = Some NullCap
weak_derived cap src_cap

goal (1 subgoal):
 1. descendants_inc m' (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) 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')); cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap\<rbrakk> \<Longrightarrow> \<forall>p. (p = dest \<longrightarrow> (\<forall>p'. src \<in> descendants_of p' m \<longrightarrow> p' \<noteq> dest \<longrightarrow> p' \<noteq> src \<longrightarrow> cap_class src_cap = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p')))) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> NullClass = cap_class src_cap \<and> cap_range NullCap \<subseteq> cap_range cap) \<and> (p \<noteq> src \<longrightarrow> p \<in> descendants_of src m \<longrightarrow> cap_range (the (cs p)) \<subseteq> cap_range cap)) proof (prove)
goal (2 subgoals):
 1. \<And>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')); cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap\<rbrakk> \<Longrightarrow> p = dest \<longrightarrow> (\<forall>p'. src \<in> descendants_of p' m \<longrightarrow> p' \<noteq> dest \<longrightarrow> p' \<noteq> src \<longrightarrow> cap_class src_cap = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p')))
 2. \<And>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')); cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> NullClass = cap_class src_cap \<and> cap_range NullCap \<subseteq> cap_range cap) \<and> (p \<noteq> src \<longrightarrow> p \<in> descendants_of src m \<longrightarrow> cap_range (the (cs p)) \<subseteq> cap_range cap) proof (prove)
goal (2 subgoals):
 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')); cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap; p = dest; src \<in> descendants_of p' m; p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> cap_class src_cap = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>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')); cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> NullClass = cap_class src_cap \<and> cap_range NullCap \<subseteq> cap_range cap) \<and> (p \<noteq> src \<longrightarrow> p \<in> descendants_of src m \<longrightarrow> cap_range (the (cs p)) \<subseteq> cap_range cap) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap; p = dest; src \<in> descendants_of p' m; p' \<noteq> dest; p' \<noteq> src; ?p115 p p' \<in> descendants_of (?p'117 p p') m \<longrightarrow> cap_class (the (cs (?p115 p p'))) = cap_class (the (cs (?p'117 p p'))) \<and> cap_range (the (cs (?p115 p p'))) \<subseteq> cap_range (the (cs (?p'117 p p')))\<rbrakk> \<Longrightarrow> cap_class src_cap = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>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')); cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> NullClass = cap_class src_cap \<and> cap_range NullCap \<subseteq> cap_range cap) \<and> (p \<noteq> src \<longrightarrow> p \<in> descendants_of src m \<longrightarrow> cap_range (the (cs p)) \<subseteq> cap_range cap) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap; p = dest; src \<in> descendants_of p' m; p' \<noteq> dest; p' \<noteq> src; cap_class (the (cs src)) = cap_class (the (cs p')) \<and> cap_range (the (cs src)) \<subseteq> cap_range (the (cs p'))\<rbrakk> \<Longrightarrow> cap_class src_cap = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>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')); cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> NullClass = cap_class src_cap \<and> cap_range NullCap \<subseteq> cap_range cap) \<and> (p \<noteq> src \<longrightarrow> p \<in> descendants_of src m \<longrightarrow> cap_range (the (cs p)) \<subseteq> cap_range cap) proof (prove)
goal (1 subgoal):
 1. \<And>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')); cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> src \<in> descendants_of src m \<longrightarrow> NullClass = cap_class src_cap \<and> cap_range NullCap \<subseteq> cap_range cap) \<and> (p \<noteq> src \<longrightarrow> p \<in> descendants_of src m \<longrightarrow> cap_range (the (cs p)) \<subseteq> cap_range cap) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p p'. m \<Turnstile> p' \<rightarrow> p \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> m \<Turnstile> src \<rightarrow> p \<longrightarrow> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p p'. m \<Turnstile> p' \<rightarrow> p \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap; p \<noteq> dest; p \<noteq> src; m \<Turnstile> src \<rightarrow> p\<rbrakk> \<Longrightarrow> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap; p \<noteq> dest; p \<noteq> src; m \<Turnstile> src \<rightarrow> p; m \<Turnstile> ?p'127 p \<rightarrow> ?p125 p \<longrightarrow> cap_class (the (cs (?p125 p))) = cap_class (the (cs (?p'127 p))) \<and> cap_range (the (cs (?p125 p))) \<subseteq> cap_range (the (cs (?p'127 p)))\<rbrakk> \<Longrightarrow> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>cs src = Some src_cap; cs dest = Some NullCap; weak_derived cap src_cap; p \<noteq> dest; p \<noteq> src; m \<Turnstile> src \<rightarrow> p; cap_class (the (cs p)) = cap_class (the (cs src)) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs src))\<rbrakk> \<Longrightarrow> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal:
No subgoals!