theory Deterministic_AI

lemma next_sib_2_eq_next_sib:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p\<rbrakk>
    \<Longrightarrow> next_sib slot (cdt_list s) (cdt s) = Some next" apply(frule finite_depth, subgoal_tac "no_mloop (cdt s)") prefer 2 apply(simp add: valid_mdb_def) apply(frule(2) next_sib_2_in_next_slot_set) apply(frule(2) next_sib_2_sib) apply(frule(5) next_slot_set_after_in_list) apply(simp add: next_sib_set_def) apply(drule tranclD2) apply(elim exE conjE) apply(simp) apply(drule rtranclD) apply(erule disjE, simp) apply(frule_tac q=z in between_next_sib_2_not_sib) apply(rule next_sib_in_next_slot_set) apply(simp, simp, simp) apply(rule next_sib_set_in_next_slot_set) apply(fastforce simp: next_sib_set_def, simp, simp) apply(simp, simp) apply(fastforce dest: next_sib_same_parent) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p\<rbrakk> \<Longrightarrow> next_sib slot (cdt_list s) (cdt s) = Some next proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s)\<rbrakk> \<Longrightarrow> next_sib slot (cdt_list s) (cdt s) = Some next
 2. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s)\<rbrakk> \<Longrightarrow> no_mloop (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s)\<rbrakk> \<Longrightarrow> no_mloop (cdt s)
 2. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s)\<rbrakk> \<Longrightarrow> next_sib slot (cdt_list s) (cdt s) = Some next proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s)\<rbrakk> \<Longrightarrow> next_sib slot (cdt_list s) (cdt s) = Some next proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_sib slot (cdt_list s) (cdt s) = Some next proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p\<rbrakk> \<Longrightarrow> next_sib slot (cdt_list s) (cdt s) = Some next proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next \<in> next_sib_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> next_sib slot (cdt_list s) (cdt s) = Some next proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (next, slot) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib slot (cdt_list s) (cdt s) = Some next proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; \<exists>z. (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>* \<and> (z, slot) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<rbrakk> \<Longrightarrow> next_sib slot (cdt_list s) (cdt s) = Some next proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>*; (z, slot) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<rbrakk> \<Longrightarrow> next_sib slot (cdt_list s) (cdt s) = Some next proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>*; next_sib slot (cdt_list s) (cdt s) = Some z\<rbrakk> \<Longrightarrow> z = next proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next = z \<or> next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z = next proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z = next proof (prove)
goal (5 subgoals):
 1. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> z \<in> next_slot_set slot (cdt_list s) (cdt s)
 2. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_slot_set z (cdt_list s) (cdt s)
 3. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_list s
 4. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_mdb s
 5. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; cdt s z \<noteq> Some p\<rbrakk> \<Longrightarrow> z = next proof (prove)
goal (7 subgoals):
 1. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> next_sib slot (cdt_list s) (cdt s) = Some z
 2. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_list s
 3. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_mdb s
 4. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_slot_set z (cdt_list s) (cdt s)
 5. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_list s
 6. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_mdb s
 7. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; cdt s z \<noteq> Some p\<rbrakk> \<Longrightarrow> z = next proof (prove)
goal (4 subgoals):
 1. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_slot_set z (cdt_list s) (cdt s)
 2. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_list s
 3. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_mdb s
 4. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; cdt s z \<noteq> Some p\<rbrakk> \<Longrightarrow> z = next proof (prove)
goal (6 subgoals):
 1. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> next \<in> next_sib_set z (cdt_list s) (cdt s)
 2. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_list s
 3. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_mdb s
 4. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_list s
 5. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_mdb s
 6. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; cdt s z \<noteq> Some p\<rbrakk> \<Longrightarrow> z = next proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_list s
 2. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> valid_mdb s
 3. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; cdt s z \<noteq> Some p\<rbrakk> \<Longrightarrow> z = next proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p; finite_depth (cdt s); no_mloop (cdt s); next \<in> next_slot_set slot (cdt_list s) (cdt s); cdt s next = Some p; next_sib slot (cdt_list s) (cdt s) = Some z; next \<noteq> z \<and> (next, z) \<in> {(next, p). next_sib p (cdt_list s) (cdt s) = Some next}\<^sup>+; cdt s z \<noteq> Some p\<rbrakk> \<Longrightarrow> z = next proof (prove)
goal:
No subgoals!