theory CSpace_AI

lemma descendants_inc_upd_nullcap:
  "\<lbrakk> mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> cap.NullCap \<noteq> c) m;
  descendants_inc m cs;
  cs slot = Some cap.NullCap\<rbrakk>
  \<Longrightarrow> descendants_inc m (cs(slot \<mapsto> cap))" apply (simp add:descendants_inc_def descendants_of_def del:split_paired_All) apply (intro allI impI) apply (rule conjI) apply (intro allI impI) apply (drule spec)+ apply (erule(1) impE) apply (drule tranclD2) apply (clarsimp simp:cdt_parent_rel_def is_cdt_parent_def) apply (drule(1) mdb_cte_atD) apply clarsimp apply (intro allI impI) apply (drule spec)+ apply (erule(1) impE) apply (drule tranclD) apply (clarsimp simp:cdt_parent_rel_def is_cdt_parent_def) apply (drule(1) mdb_cte_atD) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; descendants_inc m cs; cs slot = Some NullCap\<rbrakk> \<Longrightarrow> descendants_inc m (cs(slot \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<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 slot = Some NullCap\<rbrakk> \<Longrightarrow> \<forall>p. (p = slot \<longrightarrow> (\<forall>p'. p' \<noteq> slot \<longrightarrow> m \<Turnstile> p' \<rightarrow> slot \<longrightarrow> cap_class cap = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p')))) \<and> (p \<noteq> slot \<longrightarrow> m \<Turnstile> slot \<rightarrow> p \<longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<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 slot = Some NullCap\<rbrakk> \<Longrightarrow> (p = slot \<longrightarrow> (\<forall>p'. p' \<noteq> slot \<longrightarrow> m \<Turnstile> p' \<rightarrow> slot \<longrightarrow> cap_class cap = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p')))) \<and> (p \<noteq> slot \<longrightarrow> m \<Turnstile> slot \<rightarrow> p \<longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<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 slot = Some NullCap\<rbrakk> \<Longrightarrow> p = slot \<longrightarrow> (\<forall>p'. p' \<noteq> slot \<longrightarrow> m \<Turnstile> p' \<rightarrow> slot \<longrightarrow> cap_class cap = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p')))
 2. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<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 slot = Some NullCap\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> m \<Turnstile> slot \<rightarrow> p \<longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<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 slot = Some NullCap; p = slot; p' \<noteq> slot; m \<Turnstile> p' \<rightarrow> slot\<rbrakk> \<Longrightarrow> cap_class cap = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<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 slot = Some NullCap\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> m \<Turnstile> slot \<rightarrow> p \<longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; cs slot = Some NullCap; p = slot; p' \<noteq> slot; m \<Turnstile> p' \<rightarrow> slot; m \<Turnstile> ?p'45 p p' \<rightarrow> ?p43 p p' \<longrightarrow> cap_class (the (cs (?p43 p p'))) = cap_class (the (cs (?p'45 p p'))) \<and> cap_range (the (cs (?p43 p p'))) \<subseteq> cap_range (the (cs (?p'45 p p')))\<rbrakk> \<Longrightarrow> cap_class cap = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<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 slot = Some NullCap\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> m \<Turnstile> slot \<rightarrow> p \<longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; cs slot = Some NullCap; p = slot; p' \<noteq> slot; m \<Turnstile> p' \<rightarrow> slot; cap_class (the (cs slot)) = cap_class (the (cs p')) \<and> cap_range (the (cs slot)) \<subseteq> cap_range (the (cs p'))\<rbrakk> \<Longrightarrow> cap_class cap = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<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 slot = Some NullCap\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> m \<Turnstile> slot \<rightarrow> p \<longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; cs slot = Some NullCap; p = slot; p' \<noteq> slot; cap_class (the (cs slot)) = cap_class (the (cs p')) \<and> cap_range (the (cs slot)) \<subseteq> cap_range (the (cs p')); \<exists>z. m \<Turnstile> p' \<rightarrow>* z \<and> m \<Turnstile> z \<leadsto> slot\<rbrakk> \<Longrightarrow> cap_class cap = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<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 slot = Some NullCap\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> m \<Turnstile> slot \<rightarrow> p \<longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; cs (a, b) = Some NullCap; slot = (a, b); cap_class cap = NullClass \<longrightarrow> \<not> cap_range cap \<subseteq> cap_range (the (cs (aa, ba))); NullClass = cap_class (the (cs (aa, ba))); cap_range NullCap \<subseteq> cap_range (the (cs (aa, ba))); ((aa, ba), ab, bb) \<in> {(p, c). m c = Some p}\<^sup>*; m (a, b) = Some (ab, bb)\<rbrakk> \<Longrightarrow> aa = a \<and> ba = b
 2. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<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 slot = Some NullCap\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> m \<Turnstile> slot \<rightarrow> p \<longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; cs (a, b) = Some NullCap; slot = (a, b); cap_class cap = NullClass \<longrightarrow> \<not> cap_range cap \<subseteq> cap_range (the (cs (aa, ba))); NullClass = cap_class (the (cs (aa, ba))); cap_range NullCap \<subseteq> cap_range (the (cs (aa, ba))); ((aa, ba), ab, bb) \<in> {(p, c). m c = Some p}\<^sup>*; (\<exists>c. cs (ab, bb) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> aa = a \<and> ba = b
 2. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<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 slot = Some NullCap\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> m \<Turnstile> slot \<rightarrow> p \<longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<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 slot = Some NullCap\<rbrakk> \<Longrightarrow> p \<noteq> slot \<longrightarrow> m \<Turnstile> slot \<rightarrow> p \<longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; \<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 slot = Some NullCap; p \<noteq> slot; m \<Turnstile> slot \<rightarrow> p\<rbrakk> \<Longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; cs slot = Some NullCap; p \<noteq> slot; m \<Turnstile> slot \<rightarrow> p; m \<Turnstile> ?p'70 p \<rightarrow> ?p68 p \<longrightarrow> cap_class (the (cs (?p68 p))) = cap_class (the (cs (?p'70 p))) \<and> cap_range (the (cs (?p68 p))) \<subseteq> cap_range (the (cs (?p'70 p)))\<rbrakk> \<Longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; cs slot = Some NullCap; p \<noteq> slot; m \<Turnstile> slot \<rightarrow> p; cap_class (the (cs p)) = cap_class (the (cs slot)) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs slot))\<rbrakk> \<Longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; cs slot = Some NullCap; p \<noteq> slot; cap_class (the (cs p)) = cap_class (the (cs slot)) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs slot)); \<exists>z. m \<Turnstile> slot \<leadsto> z \<and> m \<Turnstile> z \<rightarrow>* p\<rbrakk> \<Longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs p)) \<subseteq> cap_range cap 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; cs slot = Some NullCap; (a, b) \<noteq> slot; cap_class (the (cs (a, b))) = NullClass; cap_range (the (cs (a, b))) \<subseteq> cap_range NullCap; m (aa, ba) = Some slot; ((aa, ba), a, b) \<in> {(p, c). m c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs (a, b))) \<subseteq> cap_range cap 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; cs slot = Some NullCap; (a, b) \<noteq> slot; cap_class (the (cs (a, b))) = NullClass; cap_range (the (cs (a, b))) \<subseteq> cap_range NullCap; ((aa, ba), a, b) \<in> {(p, c). m c = Some p}\<^sup>*; (\<exists>c. cs slot = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> NullClass = cap_class cap \<and> cap_range (the (cs (a, b))) \<subseteq> cap_range cap proof (prove)
goal:
No subgoals!