theory Deterministic_AI

lemma descendants_linear:
  "\<lbrakk>a \<in> descendants_of b m; a \<in> descendants_of c m; b \<noteq> c\<rbrakk>
    \<Longrightarrow> b \<in> descendants_of c m \<or> c \<in> descendants_of b m" apply(clarsimp) apply(simp add: descendants_of_def cdt_parent_rel_def is_cdt_parent_def) apply(induct b a rule: trancl.induct) apply(simp) apply(erule tranclE) apply(simp) apply(simp) apply(simp) apply(subgoal_tac "(c, b) \<in> {(p, c). m c = Some p}\<^sup>+") apply(simp) apply(subgoal_tac "b \<noteq> c") apply(erule_tac a=c and b=ca in tranclE) apply(simp) apply(simp) apply(fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> descendants_of b m; a \<in> descendants_of c m; b \<noteq> c\<rbrakk> \<Longrightarrow> b \<in> descendants_of c m \<or> c \<in> descendants_of b m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> descendants_of b m; a \<in> descendants_of c m; b \<noteq> c; c \<notin> descendants_of b m\<rbrakk> \<Longrightarrow> b \<in> descendants_of c m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(b, a) \<in> {(p, c). m c = Some p}\<^sup>+; (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; b \<noteq> c; (b, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; \<lbrakk>(c, b) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; (b, ca) \<in> {(p, c). m c = Some p}; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>m b = Some a; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; \<lbrakk>(c, b) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; (b, ca) \<in> {(p, c). m c = Some p}; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>m b = Some a; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>a b ca. \<lbrakk>m b = Some a; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; (ca, b) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+
 3. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; \<lbrakk>(c, b) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; (b, ca) \<in> {(p, c). m c = Some p}; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b ca. \<lbrakk>m b = Some a; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; (ca, b) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; \<lbrakk>(c, b) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; (b, ca) \<in> {(p, c). m c = Some p}; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; \<lbrakk>(c, b) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; (b, ca) \<in> {(p, c). m c = Some p}; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; m ca = Some b; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; m ca = Some b; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; m ca = Some b; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; m ca = Some b; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; m ca = Some b; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+; b \<noteq> c\<rbrakk> \<Longrightarrow> (c, b) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; m ca = Some b; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> b \<noteq> c proof (prove)
goal (3 subgoals):
 1. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; m ca = Some b; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+; b \<noteq> c; (c, ca) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> (c, b) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>a b ca caa. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; m ca = Some b; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+; b \<noteq> c; (c, caa) \<in> {(p, c). m c = Some p}\<^sup>+; (caa, ca) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> (c, b) \<in> {(p, c). m c = Some p}\<^sup>+
 3. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; m ca = Some b; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> b \<noteq> c proof (prove)
goal (2 subgoals):
 1. \<And>a b ca caa. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; m ca = Some b; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+; b \<noteq> c; (c, caa) \<in> {(p, c). m c = Some p}\<^sup>+; (caa, ca) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> (c, b) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; m ca = Some b; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> b \<noteq> c proof (prove)
goal (1 subgoal):
 1. \<And>a b ca. \<lbrakk>(a, b) \<in> {(p, c). m c = Some p}\<^sup>+; (c, b) \<in> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> (c, a) \<in> {(p, c). m c = Some p}\<^sup>+; m ca = Some b; (c, ca) \<in> {(p, c). m c = Some p}\<^sup>+; a \<noteq> c; (a, c) \<notin> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> b \<noteq> c proof (prove)
goal:
No subgoals!