theory CSpace_AI

lemma descendants_of_self:
  assumes "descendants_of dest m = {}"
  shows "descendants_of x (m(dest \<mapsto> dest)) =
   (if x = dest then {dest} else descendants_of x m - {dest})" using assms apply (clarsimp simp: descendants_of_def cdt_parent_defs) apply (rule conjI) apply clarsimp apply (fastforce split: if_split_asm elim: trancl_into_trancl trancl_induct) apply clarsimp apply (rule set_eqI) apply clarsimp apply (rule iffI) apply (erule trancl_induct) apply fastforce apply clarsimp apply (erule trancl_into_trancl) apply clarsimp apply clarsimp apply (rule_tac P="(a,b) \<noteq> dest" in mp) prefer 2 apply assumption apply (thin_tac "(a,b) \<noteq> dest") apply (erule trancl_induct) apply fastforce apply (fastforce split: if_split_asm elim: trancl_into_trancl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of x (m(dest \<mapsto> dest)) = (if x = dest then {dest} else descendants_of x m - {dest}) proof (prove)
using this:
descendants_of dest m = {}

goal (1 subgoal):
 1. descendants_of x (m(dest \<mapsto> dest)) = (if x = dest then {dest} else descendants_of x m - {dest}) proof (prove)
goal (1 subgoal):
 1. \<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> (x = dest \<longrightarrow> {q. (dest, q) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+} = {dest}) \<and> (x \<noteq> dest \<longrightarrow> {q. (x, q) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (2 subgoals):
 1. \<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> x = dest \<longrightarrow> {q. (dest, q) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+} = {dest}
 2. \<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> x \<noteq> dest \<longrightarrow> {q. (x, q) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x = dest\<rbrakk> \<Longrightarrow> {q. (dest, q) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+} = {dest}
 2. \<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> x \<noteq> dest \<longrightarrow> {q. (x, q) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (1 subgoal):
 1. \<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> x \<noteq> dest \<longrightarrow> {q. (x, q) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest\<rbrakk> \<Longrightarrow> {q. (x, q) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+} = {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest} proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest\<rbrakk> \<Longrightarrow> (xa \<in> {q. (x, q) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+}) = (xa \<in> {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+} - {dest}) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest\<rbrakk> \<Longrightarrow> ((x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+) = ((x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (a, b) \<noteq> dest) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+\<rbrakk> \<Longrightarrow> (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (a, b) \<noteq> dest
 2. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>a b y. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, y) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<rbrakk> \<Longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+ \<and> y \<noteq> dest
 2. \<And>a b y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, y) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+; (y, z) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}; (x, y) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+ \<and> y \<noteq> dest\<rbrakk> \<Longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+ \<and> z \<noteq> dest
 3. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, y) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+; (y, z) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}; (x, y) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+ \<and> y \<noteq> dest\<rbrakk> \<Longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> m c = Some p}\<^sup>+ \<and> z \<noteq> dest
 2. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+; (aa, ba) \<noteq> dest; m (aa, ba) = Some (a, b); (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+; (aa, ba) \<noteq> dest; m (aa, ba) = Some (a, b); (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> {(p, c). m c = Some p}
 2. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<and> (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (a, b) \<noteq> dest \<longrightarrow> (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+
 2. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (a, b) \<noteq> dest proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (a, b) \<noteq> dest
 2. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (a, b) \<noteq> dest \<longrightarrow> (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (a, b) \<noteq> dest \<longrightarrow> (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, a, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<noteq> dest \<longrightarrow> (x, a, b) \<in> {(p, c). (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, y) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> y \<noteq> dest \<longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+
 2. \<And>a b y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; y \<noteq> dest \<longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b y z. \<lbrakk>\<forall>a b. (dest, a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; x \<noteq> dest; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; y \<noteq> dest \<longrightarrow> (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (c = dest \<longrightarrow> dest = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+ proof (prove)
goal:
No subgoals!