theory Deterministic_AI

lemma next_sib_2_sib':
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  assumes "next_sib_2 slot p s = Some next" "cdt s slot \<noteq> Some p" "valid_list s" "valid_mdb s"
  shows "cdt s next = Some p" apply(insert assms) apply(induct slot rule: next_sib_2_pinduct[where s=s and p=p]) apply(simp) apply(frule(2) next_sib_2_in_next_slot_set) apply(case_tac "next_slot slot (cdt_list s) (cdt s)") apply(fastforce simp: next_slot_set_def dest: tranclD2) apply(simp) apply(atomize) apply(erule_tac x=a in allE, simp) apply(case_tac "a=next") apply(simp add: next_sib_2_termination split: if_split_asm | erule impE)+ apply(insert assms, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt s next = Some p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; cdt s slot \<noteq> Some p; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> cdt s next = Some p proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p; next_sib_2 a p s = Some next; cdt s a \<noteq> Some p; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> cdt s next = Some p; next_sib_2 slot p s = Some next; cdt s slot \<noteq> Some p; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> cdt s next = Some p
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; next_sib_2 a p s = Some next; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s next = Some p; next_sib_2 slot p s = Some next; cdt s slot \<noteq> Some p; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> cdt s next = Some p
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; next_sib_2 a p s = Some next; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s next = Some p; next_sib_2 slot p s = Some next; cdt s slot \<noteq> Some p; valid_list s; valid_mdb s; next \<in> next_slot_set slot (cdt_list s) (cdt s)\<rbrakk> \<Longrightarrow> cdt s next = Some p
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; next_sib_2 a p s = Some next; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s next = Some p; next_sib_2 slot p s = Some next; cdt s slot \<noteq> Some p; valid_list s; valid_mdb s; next \<in> next_slot_set slot (cdt_list s) (cdt s); next_slot slot (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> cdt s next = Some p
 2. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; next_sib_2 a p s = Some next; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s next = Some p; next_sib_2 slot p s = Some next; cdt s slot \<noteq> Some p; valid_list s; valid_mdb s; next \<in> next_slot_set slot (cdt_list s) (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> cdt s next = Some p
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; next_sib_2 a p s = Some next; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s next = Some p; next_sib_2 slot p s = Some next; cdt s slot \<noteq> Some p; valid_list s; valid_mdb s; next \<in> next_slot_set slot (cdt_list s) (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> cdt s next = Some p
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>\<And>aa. \<lbrakk>slot \<in> descendants_of p (cdt s); a = aa; next_sib_2 aa p s = Some next; cdt s aa \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s next = Some p; next_sib_2 slot p s = Some next; cdt s slot \<noteq> Some p; valid_list s; valid_mdb s; next \<in> next_slot_set slot (cdt_list s) (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> cdt s next = Some p
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>aa. slot \<in> descendants_of p (cdt s) \<longrightarrow> a = aa \<longrightarrow> next_sib_2 aa p s = Some next \<longrightarrow> cdt s aa \<noteq> Some p \<longrightarrow> cdt s next = Some p; next_sib_2 slot p s = Some next; cdt s slot \<noteq> Some p; valid_list s; valid_mdb s; next \<in> next_slot_set slot (cdt_list s) (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a\<rbrakk> \<Longrightarrow> cdt s next = Some p
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>next_sib_2 slot p s = Some next; cdt s slot \<noteq> Some p; valid_list s; valid_mdb s; next \<in> next_slot_set slot (cdt_list s) (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next \<longrightarrow> cdt s a \<noteq> Some p \<longrightarrow> cdt s next = Some p\<rbrakk> \<Longrightarrow> cdt s next = Some p
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>next_sib_2 slot p s = Some next; cdt s slot \<noteq> Some p; valid_list s; valid_mdb s; next \<in> next_slot_set slot (cdt_list s) (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next \<longrightarrow> cdt s a \<noteq> Some p \<longrightarrow> cdt s next = Some p; a = next\<rbrakk> \<Longrightarrow> cdt s next = Some p
 2. \<And>slot a. \<lbrakk>next_sib_2 slot p s = Some next; cdt s slot \<noteq> Some p; valid_list s; valid_mdb s; next \<in> next_slot_set slot (cdt_list s) (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; slot \<in> descendants_of p (cdt s) \<longrightarrow> next_sib_2 a p s = Some next \<longrightarrow> cdt s a \<noteq> Some p \<longrightarrow> cdt s next = Some p; a \<noteq> next\<rbrakk> \<Longrightarrow> cdt s next = Some p
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (2 subgoals):
 1. valid_mdb s
 2. valid_list s proof (prove)
goal:
No subgoals!