theory Untyped_AI

lemma untyped_incD2:
  "\<lbrakk>cs p = Some c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_inc m cs\<rbrakk>
  \<Longrightarrow> untyped_range c \<inter> untyped_range c' \<noteq> {} \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<subseteq> untyped_range c'
    \<or> p' \<in> descendants_of p m \<and> untyped_range c'\<subseteq> untyped_range c
    \<or> p = p'" apply (drule(4) untyped_incD) apply (rule ccontr) apply (elim conjE subset_splitE) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs p = Some c; is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_inc m cs\<rbrakk> \<Longrightarrow> untyped_range c \<inter> untyped_range c' \<noteq> {} \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<subseteq> untyped_range c' \<or> p' \<in> descendants_of p m \<and> untyped_range c' \<subseteq> untyped_range c \<or> p = p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_inc m cs; (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p')\<rbrakk> \<Longrightarrow> untyped_range c \<inter> untyped_range c' \<noteq> {} \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<subseteq> untyped_range c' \<or> p' \<in> descendants_of p m \<and> untyped_range c' \<subseteq> untyped_range c \<or> p = p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_inc m cs; (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p'); \<not> (untyped_range c \<inter> untyped_range c' \<noteq> {} \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<subseteq> untyped_range c' \<or> p' \<in> descendants_of p m \<and> untyped_range c' \<subseteq> untyped_range c \<or> p = p')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_inc m cs; \<not> (untyped_range c \<inter> untyped_range c' \<noteq> {} \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<subseteq> untyped_range c' \<or> p' \<in> descendants_of p m \<and> untyped_range c' \<subseteq> untyped_range c \<or> p = p'); untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}; untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}; untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p'; untyped_range c \<subset> untyped_range c'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_inc m cs; \<not> (untyped_range c \<inter> untyped_range c' \<noteq> {} \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<subseteq> untyped_range c' \<or> p' \<in> descendants_of p m \<and> untyped_range c' \<subseteq> untyped_range c \<or> p = p'); untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}; untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}; untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p'; untyped_range c' \<subset> untyped_range c\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_inc m cs; \<not> (untyped_range c \<inter> untyped_range c' \<noteq> {} \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<subseteq> untyped_range c' \<or> p' \<in> descendants_of p m \<and> untyped_range c' \<subseteq> untyped_range c \<or> p = p'); untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}; untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}; untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p'; untyped_range c = untyped_range c'\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>is_untyped_cap c; cs p' = Some c'; is_untyped_cap c'; untyped_inc m cs; \<not> (untyped_range c \<inter> untyped_range c' \<noteq> {} \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<subseteq> untyped_range c' \<or> p' \<in> descendants_of p m \<and> untyped_range c' \<subseteq> untyped_range c \<or> p = p'); untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}; untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}; untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p'; untyped_range c \<inter> untyped_range c' = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!