theory Deterministic_AI

lemma sib_not_desc:
  "\<lbrakk>no_mloop m; m x = Some p; m y = Some p\<rbrakk>
    \<Longrightarrow> x \<notin> descendants_of y m" apply(rule notI) apply(simp add: descendants_of_def cdt_parent_defs) apply(drule tranclD2) apply(elim conjE exE) apply(simp) apply(drule rtranclD) apply(erule disjE) apply(fastforce simp: no_mloop_def cdt_parent_defs) apply(erule conjE) apply(subgoal_tac "(z, z) \<in> {(p, c). m c = Some p}\<^sup>+") prefer 2 apply(rule_tac b=y in trancl_into_trancl2) apply(simp) apply(simp) apply(fastforce simp: no_mloop_def cdt_parent_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_mloop m; m x = Some p; m y = Some p\<rbrakk> \<Longrightarrow> x \<notin> descendants_of y m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_mloop m; m x = Some p; m y = Some p; x \<in> descendants_of y m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_mloop m; m x = Some p; m y = Some p; (y, x) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_mloop m; m x = Some p; m y = Some p; \<exists>z. (y, z) \<in> {(p, c). m c = Some p}\<^sup>* \<and> (z, x) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>no_mloop m; m x = Some p; m y = Some p; (y, z) \<in> {(p, c). m c = Some p}\<^sup>*; (z, x) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; (y, z) \<in> {(p, c). m c = Some p}\<^sup>*; p = z\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y = z \<or> y \<noteq> z \<and> (y, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y = z\<rbrakk> \<Longrightarrow> False
 2. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y \<noteq> z \<and> (y, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y \<noteq> z \<and> (y, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y \<noteq> z; (y, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y \<noteq> z; (y, z) \<in> {(p, c). m c = Some p}\<^sup>+; (z, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y \<noteq> z; (y, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (z, z) \<in> {(p, c). m c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y \<noteq> z; (y, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (z, z) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y \<noteq> z; (y, z) \<in> {(p, c). m c = Some p}\<^sup>+; (z, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y \<noteq> z; (y, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (z, y) \<in> {(p, c). m c = Some p}
 2. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y \<noteq> z; (y, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {(p, c). m c = Some p}\<^sup>+
 3. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y \<noteq> z; (y, z) \<in> {(p, c). m c = Some p}\<^sup>+; (z, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y \<noteq> z; (y, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y \<noteq> z; (y, z) \<in> {(p, c). m c = Some p}\<^sup>+; (z, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>no_mloop m; m x = Some z; m y = Some z; p = z; y \<noteq> z; (y, z) \<in> {(p, c). m c = Some p}\<^sup>+; (z, z) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!