theory CSpace_AI

lemma descendants_insert_evil_trancl_induct:
  assumes "src \<noteq> dest"
  assumes d: "descendants_of dest m = {}"
  assumes "src \<in> descendants_of x m"
  shows "src \<in> descendants_of x (m (dest \<mapsto> src))" proof - have r: "\<And>t. \<lbrakk> src \<in> descendants_of x m; t = src \<rbrakk> \<Longrightarrow> src \<noteq> dest \<longrightarrow> src \<in> descendants_of x (m (dest \<mapsto> t))" unfolding descendants_of_def cdt_parent_defs apply (simp (no_asm_use) del: fun_upd_apply) apply (erule trancl_induct) apply clarsimp apply (rule r_into_trancl) apply clarsimp apply (rule impI) apply (erule impE) apply (insert d)[1] apply (clarsimp simp: descendants_of_def cdt_parent_defs) apply fastforce apply (simp del: fun_upd_apply) apply (erule trancl_into_trancl) apply clarsimp done show ?thesis using assms apply - apply (rule r [THEN mp]) apply assumption apply (rule refl) apply assumption done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. src \<in> descendants_of x (m(dest \<mapsto> src)) proof (state)
goal (1 subgoal):
 1. src \<in> descendants_of x (m(dest \<mapsto> src)) proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>src \<in> descendants_of x m; t = src\<rbrakk> \<Longrightarrow> src \<noteq> dest \<longrightarrow> src \<in> descendants_of x (m(dest \<mapsto> t)) proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>src \<in> {q. (x, q) \<in> {(p, c). m c = Some p}\<^sup>+}; t = src\<rbrakk> \<Longrightarrow> src \<noteq> dest \<longrightarrow> src \<in> {q. (x, q) \<in> {(p, c). (m(dest \<mapsto> t)) c = Some p}\<^sup>+} proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>(x, src) \<in> {(p, c). m c = Some p}\<^sup>+; t = src\<rbrakk> \<Longrightarrow> src \<noteq> dest \<longrightarrow> (x, src) \<in> {(p, c). (m(dest \<mapsto> t)) c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>t y. \<lbrakk>t = src; (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> (m(dest \<mapsto> t)) c = Some p}\<^sup>+
 2. \<And>t y z. \<lbrakk>t = src; (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> (m(dest \<mapsto> t)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> t)) c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>m (aa, ba) = Some x; src = (a, b); (aa, ba) \<noteq> dest\<rbrakk> \<Longrightarrow> (x, aa, ba) \<in> {(p, c). (c = dest \<longrightarrow> (a, b) = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}\<^sup>+
 2. \<And>t y z. \<lbrakk>t = src; (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> (m(dest \<mapsto> t)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> t)) c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>m (aa, ba) = Some x; src = (a, b); (aa, ba) \<noteq> dest\<rbrakk> \<Longrightarrow> (x, aa, ba) \<in> {(p, c). (c = dest \<longrightarrow> (a, b) = p) \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}
 2. \<And>t y z. \<lbrakk>t = src; (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> (m(dest \<mapsto> t)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> t)) c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>t y z. \<lbrakk>t = src; (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> (m(dest \<mapsto> t)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> t)) c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>t y z. \<lbrakk>t = src; (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> (m(dest \<mapsto> t)) c = Some p}\<^sup>+; z \<noteq> dest\<rbrakk> \<Longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> t)) c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>t y z. \<lbrakk>t = src; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; z \<noteq> dest\<rbrakk> \<Longrightarrow> y \<noteq> dest
 2. \<And>t y z. \<lbrakk>t = src; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; z \<noteq> dest; (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> t)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> t)) c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>t y z. \<lbrakk>t = src; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; z \<noteq> dest; descendants_of dest m = {}\<rbrakk> \<Longrightarrow> y \<noteq> dest
 2. \<And>t y z. \<lbrakk>t = src; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; z \<noteq> dest; (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> t)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> t)) c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(x, aa, ba) \<in> {(p, c). m c = Some p}\<^sup>+; m (ab, bb) = Some (aa, ba); \<forall>a b. ((aa, ba), a, b) \<notin> {(p, c). m c = Some p}\<^sup>+; src = (a, b); dest = (aa, ba)\<rbrakk> \<Longrightarrow> ab = aa \<and> bb = ba
 2. \<And>t y z. \<lbrakk>t = src; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; z \<noteq> dest; (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> t)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> t)) c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>t y z. \<lbrakk>t = src; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; (y, z) \<in> {(p, c). m c = Some p}; z \<noteq> dest; (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> t)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> t)) c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>t y z. \<lbrakk>t = src; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; m z = Some y; z \<noteq> dest; (x, y) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>t y z. \<lbrakk>t = src; (x, y) \<in> {(p, c). m c = Some p}\<^sup>+; m z = Some y; z \<noteq> dest\<rbrakk> \<Longrightarrow> (y, z) \<in> {a. case a of (p, c) \<Rightarrow> (m(dest \<mapsto> src)) c = Some p} proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>src \<in> descendants_of x m; ?t = src\<rbrakk> \<Longrightarrow> src \<noteq> dest \<longrightarrow> src \<in> descendants_of x (m(dest \<mapsto> ?t))

goal (1 subgoal):
 1. src \<in> descendants_of x (m(dest \<mapsto> src)) proof (prove)
goal (1 subgoal):
 1. src \<in> descendants_of x (m(dest \<mapsto> src)) proof (prove)
using this:
src \<noteq> dest
descendants_of dest m = {}
src \<in> descendants_of x m

goal (1 subgoal):
 1. src \<in> descendants_of x (m(dest \<mapsto> src)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>src \<noteq> dest; descendants_of dest m = {}; src \<in> descendants_of x m\<rbrakk> \<Longrightarrow> src \<in> descendants_of x (m(dest \<mapsto> src)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>src \<noteq> dest; descendants_of dest m = {}; src \<in> descendants_of x m\<rbrakk> \<Longrightarrow> src \<in> descendants_of x m
 2. \<lbrakk>src \<noteq> dest; descendants_of dest m = {}; src \<in> descendants_of x m\<rbrakk> \<Longrightarrow> src = src
 3. \<lbrakk>src \<noteq> dest; descendants_of dest m = {}; src \<in> descendants_of x m\<rbrakk> \<Longrightarrow> src \<noteq> dest proof (prove)
goal (2 subgoals):
 1. \<lbrakk>src \<noteq> dest; descendants_of dest m = {}; src \<in> descendants_of x m\<rbrakk> \<Longrightarrow> src = src
 2. \<lbrakk>src \<noteq> dest; descendants_of dest m = {}; src \<in> descendants_of x m\<rbrakk> \<Longrightarrow> src \<noteq> dest proof (prove)
goal (1 subgoal):
 1. \<lbrakk>src \<noteq> dest; descendants_of dest m = {}; src \<in> descendants_of x m\<rbrakk> \<Longrightarrow> src \<noteq> dest proof (prove)
goal:
No subgoals! proof (state)
this:
src \<in> descendants_of x (m(dest \<mapsto> src))

goal:
No subgoals!