theory CNodeInv_AI

lemma descendants_inc_n:
  shows "descendants_inc n cs'" proof - from valid_mdb have "descendants_inc m cs" by (simp add:cs_def m valid_mdb_def2) thus ?thesis using cap cap' sder dder apply (simp add:descendants_inc_def descendants_of_def del: split_paired_All) apply (intro impI allI) apply (simp add:parency cs'_def del:split_paired_All) apply (drule spec)+ apply (erule(1) impE) apply (simp add: weak_derived_cap_range) apply (intro conjI impI) apply (simp add:s_d_swap_other)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_inc n cs' proof (state)
goal (1 subgoal):
 1. descendants_inc n cs' proof (chain)
picking this:
valid_mdb s proof (prove)
using this:
valid_mdb s

goal (1 subgoal):
 1. descendants_inc m cs proof (state)
this:
descendants_inc m cs

goal (1 subgoal):
 1. descendants_inc n cs' proof (prove)
using this:
descendants_inc m cs

goal (1 subgoal):
 1. descendants_inc n cs' proof (prove)
using this:
descendants_inc m cs
cs src = Some cap
cs dest = Some cap'
weak_derived scap cap
weak_derived dcap cap'

goal (1 subgoal):
 1. descendants_inc n cs' proof (prove)
goal (1 subgoal):
 1. \<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 cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'\<rbrakk> \<Longrightarrow> \<forall>p p'. n \<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')) proof (prove)
goal (1 subgoal):
 1. \<And>p 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 cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; n \<Turnstile> p' \<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>\<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 cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> p' \<noteq> src \<longrightarrow> (p' = dest \<longrightarrow> cap_class cap' = cap_class cap \<and> cap_range dcap \<subseteq> cap_range scap) \<and> (p' \<noteq> dest \<longrightarrow> cap_class cap' = cap_class (the (cs p')) \<and> cap_range dcap \<subseteq> cap_range (the (cs p')))) \<and> (p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> (p' = src \<longrightarrow> cap_class cap = cap_class cap' \<and> cap_range scap \<subseteq> cap_range dcap) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> cap_class cap = cap_class (the (cs p')) \<and> cap_range scap \<subseteq> cap_range (the (cs p')))) \<and> (p \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> cap_class (the (cs p)) = cap_class cap' \<and> cap_range (the (cs p)) \<subseteq> cap_range dcap) \<and> (p' \<noteq> src \<longrightarrow> (p' = dest \<longrightarrow> cap_class (the (cs p)) = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range scap) \<and> (p' \<noteq> dest \<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>cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest; m \<Turnstile> ?p'26 p p' \<rightarrow> ?p24 p p' \<longrightarrow> cap_class (the (cs (?p24 p p'))) = cap_class (the (cs (?p'26 p p'))) \<and> cap_range (the (cs (?p24 p p'))) \<subseteq> cap_range (the (cs (?p'26 p p')))\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> p' \<noteq> src \<longrightarrow> (p' = dest \<longrightarrow> cap_class cap' = cap_class cap \<and> cap_range dcap \<subseteq> cap_range scap) \<and> (p' \<noteq> dest \<longrightarrow> cap_class cap' = cap_class (the (cs p')) \<and> cap_range dcap \<subseteq> cap_range (the (cs p')))) \<and> (p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> (p' = src \<longrightarrow> cap_class cap = cap_class cap' \<and> cap_range scap \<subseteq> cap_range dcap) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> cap_class cap = cap_class (the (cs p')) \<and> cap_range scap \<subseteq> cap_range (the (cs p')))) \<and> (p \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> cap_class (the (cs p)) = cap_class cap' \<and> cap_range (the (cs p)) \<subseteq> cap_range dcap) \<and> (p' \<noteq> src \<longrightarrow> (p' = dest \<longrightarrow> cap_class (the (cs p)) = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range scap) \<and> (p' \<noteq> dest \<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>cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest; cap_class (the (cs (s_d_swap p src dest))) = cap_class (the (cs (s_d_swap p' src dest))) \<and> cap_range (the (cs (s_d_swap p src dest))) \<subseteq> cap_range (the (cs (s_d_swap p' src dest)))\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> p' \<noteq> src \<longrightarrow> (p' = dest \<longrightarrow> cap_class cap' = cap_class cap \<and> cap_range dcap \<subseteq> cap_range scap) \<and> (p' \<noteq> dest \<longrightarrow> cap_class cap' = cap_class (the (cs p')) \<and> cap_range dcap \<subseteq> cap_range (the (cs p')))) \<and> (p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> (p' = src \<longrightarrow> cap_class cap = cap_class cap' \<and> cap_range scap \<subseteq> cap_range dcap) \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> cap_class cap = cap_class (the (cs p')) \<and> cap_range scap \<subseteq> cap_range (the (cs p')))) \<and> (p \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> cap_class (the (cs p)) = cap_class cap' \<and> cap_range (the (cs p)) \<subseteq> cap_range dcap) \<and> (p' \<noteq> src \<longrightarrow> (p' = dest \<longrightarrow> cap_class (the (cs p)) = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range scap) \<and> (p' \<noteq> dest \<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>cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest; cap_class (the (cs (s_d_swap p src dest))) = cap_class (the (cs (s_d_swap p' src dest))) \<and> cap_range (the (cs (s_d_swap p src dest))) \<subseteq> cap_range (the (cs (s_d_swap p' src dest)))\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> p' \<noteq> src \<longrightarrow> (p' = dest \<longrightarrow> cap_class cap' = cap_class cap \<and> cap_range cap' \<subseteq> cap_range cap) \<and> (p' \<noteq> dest \<longrightarrow> cap_class cap' = cap_class (the (cs p')) \<and> cap_range cap' \<subseteq> cap_range (the (cs p')))) \<and> (p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> (p' = src \<longrightarrow> cap_class cap = cap_class cap' \<and> cap_range cap \<subseteq> cap_range cap') \<and> (p' \<noteq> src \<longrightarrow> p' \<noteq> dest \<longrightarrow> cap_class cap = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p')))) \<and> (p \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> cap_class (the (cs p)) = cap_class cap' \<and> cap_range (the (cs p)) \<subseteq> cap_range cap') \<and> (p' \<noteq> src \<longrightarrow> (p' = dest \<longrightarrow> cap_class (the (cs p)) = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) \<and> (p' \<noteq> dest \<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 (14 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest; cap_class (the (cs (s_d_swap p src dest))) = cap_class (the (cs (s_d_swap p' src dest))) \<and> cap_range (the (cs (s_d_swap p src dest))) \<subseteq> cap_range (the (cs (s_d_swap p' src dest))); p = src; p' \<noteq> src; p' = dest\<rbrakk> \<Longrightarrow> cap_class cap' = cap_class cap
 2. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest; cap_class (the (cs (s_d_swap p src dest))) = cap_class (the (cs (s_d_swap p' src dest))) \<and> cap_range (the (cs (s_d_swap p src dest))) \<subseteq> cap_range (the (cs (s_d_swap p' src dest))); p = src; p' \<noteq> src; p' = dest\<rbrakk> \<Longrightarrow> cap_range cap' \<subseteq> cap_range cap
 3. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest; cap_class (the (cs (s_d_swap p src dest))) = cap_class (the (cs (s_d_swap p' src dest))) \<and> cap_range (the (cs (s_d_swap p src dest))) \<subseteq> cap_range (the (cs (s_d_swap p' src dest))); p = src; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> cap_class cap' = cap_class (the (cs p'))
 4. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest; cap_class (the (cs (s_d_swap p src dest))) = cap_class (the (cs (s_d_swap p' src dest))) \<and> cap_range (the (cs (s_d_swap p src dest))) \<subseteq> cap_range (the (cs (s_d_swap p' src dest))); p = src; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> cap_range cap' \<subseteq> cap_range (the (cs p'))
 5. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest; cap_class (the (cs (s_d_swap p src dest))) = cap_class (the (cs (s_d_swap p' src dest))) \<and> cap_range (the (cs (s_d_swap p src dest))) \<subseteq> cap_range (the (cs (s_d_swap p' src dest))); p \<noteq> src; p = dest; p' = src\<rbrakk> \<Longrightarrow> cap_class cap = cap_class cap'
 6. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest; cap_class (the (cs (s_d_swap p src dest))) = cap_class (the (cs (s_d_swap p' src dest))) \<and> cap_range (the (cs (s_d_swap p src dest))) \<subseteq> cap_range (the (cs (s_d_swap p' src dest))); p \<noteq> src; p = dest; p' = src\<rbrakk> \<Longrightarrow> cap_range cap \<subseteq> cap_range cap'
 7. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest; cap_class (the (cs (s_d_swap p src dest))) = cap_class (the (cs (s_d_swap p' src dest))) \<and> cap_range (the (cs (s_d_swap p src dest))) \<subseteq> cap_range (the (cs (s_d_swap p' src dest))); p \<noteq> src; p = dest; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> cap_class cap = cap_class (the (cs p'))
 8. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest; cap_class (the (cs (s_d_swap p src dest))) = cap_class (the (cs (s_d_swap p' src dest))) \<and> cap_range (the (cs (s_d_swap p src dest))) \<subseteq> cap_range (the (cs (s_d_swap p' src dest))); p \<noteq> src; p = dest; p' \<noteq> src; p' \<noteq> dest\<rbrakk> \<Longrightarrow> cap_range cap \<subseteq> cap_range (the (cs p'))
 9. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest; cap_class (the (cs (s_d_swap p src dest))) = cap_class (the (cs (s_d_swap p' src dest))) \<and> cap_range (the (cs (s_d_swap p src dest))) \<subseteq> cap_range (the (cs (s_d_swap p' src dest))); p \<noteq> src; p \<noteq> dest; p' = src\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class cap'
 10. \<And>p p'. \<lbrakk>cs src = Some cap; cs dest = Some cap'; weak_derived scap cap; weak_derived dcap cap'; m \<Turnstile> s_d_swap p' src dest \<rightarrow> s_d_swap p src dest; cap_class (the (cs (s_d_swap p src dest))) = cap_class (the (cs (s_d_swap p' src dest))) \<and> cap_range (the (cs (s_d_swap p src dest))) \<subseteq> cap_range (the (cs (s_d_swap p' src dest))); p \<noteq> src; p \<noteq> dest; p' = src\<rbrakk> \<Longrightarrow> cap_range (the (cs p)) \<subseteq> cap_range cap'
A total of 14 subgoals... proof (prove)
goal:
No subgoals! proof (state)
this:
descendants_inc n cs'

goal:
No subgoals!