theory Deterministic_AI

lemma desc_sib_ne:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>a \<in> descendants_of b m; next_sib b t m = Some c; valid_list_2 t m;
    no_mloop m\<rbrakk>
    \<Longrightarrow> a \<noteq> c" apply(rule notI) apply(drule next_sibD) apply(case_tac "m b", simp, simp) apply(subgoal_tac "aa \<in> descendants_of aa m") prefer 2 apply(simp add: descendants_of_def cdt_parent_defs) apply(rule_tac b=b in trancl_into_trancl2) apply(simp) apply(drule tranclD2) apply(simp) apply(drule after_in_list_in_list) apply(simp add: valid_list_2_def) apply(drule rtranclD) apply(fastforce) apply(simp add: no_mloop_descendants) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> descendants_of b m; next_sib b t m = Some c; valid_list_2 t m; no_mloop m\<rbrakk> \<Longrightarrow> a \<noteq> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> descendants_of b m; next_sib b t m = Some c; valid_list_2 t m; no_mloop m; a = c\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; \<exists>p. m b = Some p \<and> after_in_list (t p) b = Some c\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa; aa \<in> descendants_of aa m\<rbrakk> \<Longrightarrow> False
 2. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa\<rbrakk> \<Longrightarrow> aa \<in> descendants_of aa m proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa\<rbrakk> \<Longrightarrow> aa \<in> descendants_of aa m
 2. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa; aa \<in> descendants_of aa m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>(b, c) \<in> {(p, c). m c = Some p}\<^sup>+; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa\<rbrakk> \<Longrightarrow> (aa, aa) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa; aa \<in> descendants_of aa m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>aa. \<lbrakk>(b, c) \<in> {(p, c). m c = Some p}\<^sup>+; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa\<rbrakk> \<Longrightarrow> (aa, b) \<in> {(p, c). m c = Some p}
 2. \<And>aa. \<lbrakk>(b, c) \<in> {(p, c). m c = Some p}\<^sup>+; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa\<rbrakk> \<Longrightarrow> (b, aa) \<in> {(p, c). m c = Some p}\<^sup>+
 3. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa; aa \<in> descendants_of aa m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>(b, c) \<in> {(p, c). m c = Some p}\<^sup>+; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa\<rbrakk> \<Longrightarrow> (b, aa) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa; aa \<in> descendants_of aa m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa; \<exists>z. (b, z) \<in> {(p, c). m c = Some p}\<^sup>* \<and> (z, c) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> (b, aa) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa; aa \<in> descendants_of aa m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa; \<exists>z. (b, z) \<in> {(p, c). m c = Some p}\<^sup>* \<and> m c = Some z\<rbrakk> \<Longrightarrow> (b, aa) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa; aa \<in> descendants_of aa m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>valid_list_2 t m; no_mloop m; a = c; m b = Some aa; \<exists>z. (b, z) \<in> {(p, c). m c = Some p}\<^sup>* \<and> m c = Some z; c \<in> set (t aa)\<rbrakk> \<Longrightarrow> (b, aa) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa; aa \<in> descendants_of aa m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); no_mloop m; a = c; m b = Some aa; (b, aa) \<in> {(p, c). m c = Some p}\<^sup>*; m c = Some aa\<rbrakk> \<Longrightarrow> (b, aa) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa; aa \<in> descendants_of aa m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); no_mloop m; a = c; m b = Some aa; m c = Some aa; b = aa \<or> b \<noteq> aa \<and> (b, aa) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (b, aa) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa; aa \<in> descendants_of aa m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>c \<in> descendants_of b m; valid_list_2 t m; no_mloop m; a = c; after_in_list (t aa) b = Some c; m b = Some aa; aa \<in> descendants_of aa m\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!