theory Deterministic_AI

lemma next_sib_set_eq_after_in_list_set_Some:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>valid_list_2 t m; m x = Some p\<rbrakk>
    \<Longrightarrow> next_sib_set x t m = {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}" apply(intro equalityI subsetI) apply(simp add: next_sib_set_def) apply(drule trancl_Collect_rev) apply(rule trancl_Collect_rev) apply(erule trancl_induct) apply(fastforce simp: next_sib_def split: option.splits) apply(rule trancl_into_trancl) apply(simp) apply(subgoal_tac "y \<in> next_sib_set x t m")  (* bad *)
     prefer 2 apply(fastforce simp: next_sib_set_def intro: trancl_Collect_rev) apply(fastforce simp: next_sib_def split: option.splits dest: next_sib_set_same_parent) apply(simp) apply(drule trancl_Collect_rev) apply(erule trancl_induct) apply(fastforce simp: next_sib_set_def next_sib_def split: option.splits) apply(simp add: next_sib_set_def) apply(subgoal_tac "y \<in> next_sib_set x t m") prefer 2 apply(fastforce simp: next_sib_set_def intro: trancl_Collect_rev) apply(drule(1) next_sib_set_same_parent) apply(rule trancl_into_trancl2) apply(fastforce simp: next_sib_def split: option.splits) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m x = Some p\<rbrakk> \<Longrightarrow> next_sib_set x t m = {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+} proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> next_sib_set x t m\<rbrakk> \<Longrightarrow> xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}
 2. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; (xa, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (xa, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+
 2. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; (x, xa) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (xa, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+
 2. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; (x, xa) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (x, xa) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+
 2. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (3 subgoals):
 1. \<And>xa y. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, p). next_sib next t m = Some p}\<rbrakk> \<Longrightarrow> (x, y) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+
 2. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_sib next t m = Some p}; (x, y) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+\<rbrakk> \<Longrightarrow> (x, z) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+
 3. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (2 subgoals):
 1. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_sib next t m = Some p}; (x, y) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+\<rbrakk> \<Longrightarrow> (x, z) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+
 2. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (3 subgoals):
 1. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_sib next t m = Some p}; (x, y) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+\<rbrakk> \<Longrightarrow> (x, ?b15 xa y z) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+
 2. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_sib next t m = Some p}; (x, y) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+\<rbrakk> \<Longrightarrow> (?b15 xa y z, z) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}
 3. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (2 subgoals):
 1. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_sib next t m = Some p}; (x, y) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+\<rbrakk> \<Longrightarrow> (y, z) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}
 2. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (3 subgoals):
 1. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_sib next t m = Some p}; (x, y) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+; y \<in> next_sib_set x t m\<rbrakk> \<Longrightarrow> (y, z) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}
 2. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_sib next t m = Some p}; (x, y) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+\<rbrakk> \<Longrightarrow> y \<in> next_sib_set x t m
 3. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (3 subgoals):
 1. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_sib next t m = Some p}; (x, y) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+; y \<in> next_sib_set x t m\<rbrakk> \<Longrightarrow> (y, z) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}
 2. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_sib next t m = Some p}; (x, y) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+\<rbrakk> \<Longrightarrow> y \<in> next_sib_set x t m
 3. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (3 subgoals):
 1. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_sib next t m = Some p}; (x, y) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+\<rbrakk> \<Longrightarrow> y \<in> next_sib_set x t m
 2. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_sib next t m = Some p}; (x, y) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+; y \<in> next_sib_set x t m\<rbrakk> \<Longrightarrow> (y, z) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}
 3. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (2 subgoals):
 1. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, p). next_sib next t m = Some p}\<^sup>+; (y, z) \<in> {(next, p). next_sib next t m = Some p}; (x, y) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}\<^sup>+; y \<in> next_sib_set x t m\<rbrakk> \<Longrightarrow> (y, z) \<in> {a. case a of (next, c) \<Rightarrow> after_in_list (t p) next = Some c}
 2. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; xa \<in> {a. (a, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+}\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; (xa, x) \<in> {(next, c). after_in_list (t p) c = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>valid_list_2 t m; m x = Some p; (x, xa) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+\<rbrakk> \<Longrightarrow> xa \<in> next_sib_set x t m proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, c). after_in_list (t p) next = Some c}\<rbrakk> \<Longrightarrow> y \<in> next_sib_set x t m
 2. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+; (y, z) \<in> {(next, c). after_in_list (t p) next = Some c}; y \<in> next_sib_set x t m\<rbrakk> \<Longrightarrow> z \<in> next_sib_set x t m proof (prove)
goal (1 subgoal):
 1. \<And>xa y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+; (y, z) \<in> {(next, c). after_in_list (t p) next = Some c}; y \<in> next_sib_set x t m\<rbrakk> \<Longrightarrow> z \<in> next_sib_set x t m proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+; after_in_list (t p) y = Some z; (y, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> (z, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+; after_in_list (t p) y = Some z; (y, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+; y \<in> next_sib_set x t m\<rbrakk> \<Longrightarrow> (z, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+
 2. \<And>y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+; after_in_list (t p) y = Some z; (y, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> y \<in> next_sib_set x t m proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+; after_in_list (t p) y = Some z; (y, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> y \<in> next_sib_set x t m
 2. \<And>y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+; after_in_list (t p) y = Some z; (y, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+; y \<in> next_sib_set x t m\<rbrakk> \<Longrightarrow> (z, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+; after_in_list (t p) y = Some z; (y, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+; y \<in> next_sib_set x t m\<rbrakk> \<Longrightarrow> (z, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+; after_in_list (t p) y = Some z; (y, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+; \<exists>p. m x = Some p \<and> m y = Some p\<rbrakk> \<Longrightarrow> (z, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+; after_in_list (t p) y = Some z; (y, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+; \<exists>p. m x = Some p \<and> m y = Some p\<rbrakk> \<Longrightarrow> (z, ?b71 y z) \<in> {(next, p). next_sib p t m = Some next}
 2. \<And>y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+; after_in_list (t p) y = Some z; (y, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+; \<exists>p. m x = Some p \<and> m y = Some p\<rbrakk> \<Longrightarrow> (?b71 y z, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>valid_list_2 t m; m x = Some p; (x, y) \<in> {(next, c). after_in_list (t p) next = Some c}\<^sup>+; after_in_list (t p) y = Some z; (y, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+; \<exists>p. m x = Some p \<and> m y = Some p\<rbrakk> \<Longrightarrow> (y, x) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+ proof (prove)
goal:
No subgoals!