theory Deterministic_AI

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

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