theory Deterministic_AI

lemma next_sib_2_in_next_slot_set:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  assumes "next_sib_2 slot p s = Some next" "valid_list s" "valid_mdb s"
  shows "next \<in> next_slot_set slot (cdt_list s) (cdt s)" using assms apply(induct rule: next_slot_induct[where s=s]) apply(simp add: next_sib_2_termination split: if_splits) apply(simp add: next_sib_2_termination split: if_splits) apply(fastforce simp: next_slot_set_def intro: trancl_into_trancl) apply(fastforce simp: next_slot_set_def intro: trancl_into_trancl) apply(insert assms, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
using this:
next_sib_2 slot p s = Some next
valid_list s
valid_mdb s

goal (1 subgoal):
 1. next \<in> next_slot_set slot (cdt_list s) (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>next_slot x (cdt_list s) (cdt s) = None; next_sib_2 x p s = Some next; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> next \<in> next_slot_set x (cdt_list s) (cdt s)
 2. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> next \<in> next_slot_set y (cdt_list s) (cdt s); next_sib_2 x p s = Some next; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> next \<in> next_slot_set x (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; \<lbrakk>next_sib_2 y p s = Some next; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> next \<in> next_slot_set y (cdt_list s) (cdt s); next_sib_2 x p s = Some next; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> next \<in> next_slot_set x (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>(if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None else None else None else None else None else None else None else None else None else None else None else None else None) = Some next \<Longrightarrow> next \<in> next_slot_set next (cdt_list s) (cdt s); valid_list s; valid_mdb s; next_slot x (cdt_list s) (cdt s) = Some next; x \<in> descendants_of p (cdt s); cdt s next = Some p; y = next\<rbrakk> \<Longrightarrow> next \<in> next_slot_set x (cdt_list s) (cdt s)
 2. \<And>x y. \<lbrakk>next \<in> next_slot_set y (cdt_list s) (cdt s); valid_list s; valid_mdb s; next_slot x (cdt_list s) (cdt s) = Some y; x \<in> descendants_of p (cdt s); cdt s y \<noteq> Some p; y \<in> descendants_of p (cdt s); (case next_slot y (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None else None else None else None else None else None else None else None else None else None else None else None else None) = Some next\<rbrakk> \<Longrightarrow> next \<in> next_slot_set x (cdt_list s) (cdt s)
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>next \<in> next_slot_set y (cdt_list s) (cdt s); valid_list s; valid_mdb s; next_slot x (cdt_list s) (cdt s) = Some y; x \<in> descendants_of p (cdt s); cdt s y \<noteq> Some p; y \<in> descendants_of p (cdt s); (case next_slot y (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else if next \<in> descendants_of p (cdt s) then case next_slot next (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None else None else None else None else None else None else None else None else None else None else None else None else None) = Some next\<rbrakk> \<Longrightarrow> next \<in> next_slot_set x (cdt_list s) (cdt s)
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (2 subgoals):
 1. valid_mdb s
 2. valid_list s proof (prove)
goal:
No subgoals!