theory Deterministic_AI

lemma next_slot:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []\<rbrakk>
    \<Longrightarrow> next_slot p (t(src_p := list_insert_after (t src_p) src dest)) n
    = (if p = src then Some dest
       else if p = dest then next_slot src t m
       else next_slot p t m)" apply(simp) apply(intro impI conjI) apply(simp add: next_slot_def next_child next_not_child empty_list_empty_desc desc) apply(rule impI, insert dest_no_parent_d, simp)[1] apply(simp add: next_slot_def next_child next_not_child) apply(rule impI, simp add: no_mloop_weaken) apply(simp add: next_slot_def next_child next_not_child) apply(intro conjI impI) apply(simp_all) apply(erule conjE, drule_tac a=src_p and c=src_p in descendants_trans,
            simp add: child_descendant, simp add: no_mloop_descendants)+ apply(simp add: empty_list_empty_desc) apply(simp only: set_empty[symmetric]) apply(simp add: set_list_insert_after) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []\<rbrakk> \<Longrightarrow> next_slot p (t(src_p := list_insert_after (t src_p) src dest)) n = (if p = src then Some dest else if p = dest then next_slot src t m else next_slot p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> next_slot dest (t(src_p := list_insert_after (t src_p) src dest)) n = next_slot src t m) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_slot src (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest) \<and> (p \<noteq> src \<longrightarrow> next_slot p (t(src_p := list_insert_after (t src_p) src dest)) n = next_slot p t m)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p = dest\<rbrakk> \<Longrightarrow> next_slot dest (t(src_p := list_insert_after (t src_p) src dest)) n = next_slot src t m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_slot src (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_slot p (t(src_p := list_insert_after (t src_p) src dest)) n = next_slot p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; descendants_of src m = {}; p = dest\<rbrakk> \<Longrightarrow> dest = src_p \<longrightarrow> list_insert_after (t src_p) src src_p \<noteq> [] \<longrightarrow> next_child src_p t = next_not_child src t m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_slot src (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_slot p (t(src_p := list_insert_after (t src_p) src dest)) n = next_slot p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> next_slot src (t(src_p := list_insert_after (t src_p) src dest)) n = Some dest
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_slot p (t(src_p := list_insert_after (t src_p) src dest)) n = next_slot p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; src \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> src = src_p \<longrightarrow> list_insert_after (t src_p) src_p dest \<noteq> [] \<longrightarrow> next_child src_p t = Some dest
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_slot p (t(src_p := list_insert_after (t src_p) src dest)) n = next_slot p t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_slot p (t(src_p := list_insert_after (t src_p) src dest)) n = next_slot p t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> (src_p \<in> descendants_of src m \<and> next_not_child src_p t m = next_not_child src t m \<longrightarrow> (p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m \<longrightarrow> (p = src_p \<longrightarrow> (list_insert_after (t src_p) src dest \<noteq> [] \<longrightarrow> t src_p = [] \<longrightarrow> next_child src_p t = next_not_child src t m) \<and> (list_insert_after (t src_p) src dest = [] \<longrightarrow> (t src_p \<noteq> [] \<longrightarrow> Some dest = next_child src_p t) \<and> (t src_p = [] \<longrightarrow> Some dest = next_not_child src t m))) \<and> (p \<noteq> src_p \<longrightarrow> t p = [] \<longrightarrow> Some dest = next_not_child src t m)) \<and> ((p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m) \<longrightarrow> p = src_p \<longrightarrow> (list_insert_after (t src_p) src dest \<noteq> [] \<longrightarrow> t src_p = [] \<longrightarrow> next_child src_p t = next_not_child src t m) \<and> (list_insert_after (t src_p) src dest = [] \<longrightarrow> (t src_p \<noteq> [] \<longrightarrow> Some dest = next_child src_p t) \<and> (t src_p = [] \<longrightarrow> Some dest = next_not_child src t m)))) \<and> ((src_p \<in> descendants_of src m \<longrightarrow> next_not_child src_p t m \<noteq> next_not_child src t m) \<longrightarrow> (p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m \<longrightarrow> (p = src_p \<longrightarrow> (list_insert_after (t src_p) src dest \<noteq> [] \<longrightarrow> t src_p = [] \<longrightarrow> next_child src_p t = next_not_child src_p t m) \<and> (list_insert_after (t src_p) src dest = [] \<longrightarrow> t src_p \<noteq> [] \<longrightarrow> next_not_child src_p t m = next_child src_p t)) \<and> (p \<noteq> src_p \<longrightarrow> t p = [] \<longrightarrow> Some dest = next_not_child src t m)) \<and> ((p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m) \<longrightarrow> p = src_p \<longrightarrow> (list_insert_after (t src_p) src dest \<noteq> [] \<longrightarrow> t src_p = [] \<longrightarrow> next_child src_p t = next_not_child src_p t m) \<and> (list_insert_after (t src_p) src dest = [] \<longrightarrow> t src_p \<noteq> [] \<longrightarrow> next_not_child src_p t m = next_child src_p t))) proof (prove)
goal (12 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src; src_p \<in> descendants_of src m \<and> next_not_child src_p t m = next_not_child src t m; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p = src_p; list_insert_after (t src_p) src dest \<noteq> []; t src_p = []\<rbrakk> \<Longrightarrow> next_child src_p t = next_not_child src t m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src; src_p \<in> descendants_of src m \<and> next_not_child src_p t m = next_not_child src t m; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p = src_p; list_insert_after (t src_p) src dest = []; t src_p \<noteq> []\<rbrakk> \<Longrightarrow> Some dest = next_child src_p t
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src; src_p \<in> descendants_of src m \<and> next_not_child src_p t m = next_not_child src t m; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p = src_p; list_insert_after (t src_p) src dest = []; t src_p = []\<rbrakk> \<Longrightarrow> Some dest = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src; src_p \<in> descendants_of src m \<and> next_not_child src_p t m = next_not_child src t m; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> src_p; t p = []\<rbrakk> \<Longrightarrow> Some dest = next_not_child src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src; src_p \<in> descendants_of src m \<and> next_not_child src_p t m = next_not_child src t m; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = src_p; list_insert_after (t src_p) src dest \<noteq> []; t src_p = []\<rbrakk> \<Longrightarrow> next_child src_p t = next_not_child src t m
 6. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src; src_p \<in> descendants_of src m \<and> next_not_child src_p t m = next_not_child src t m; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = src_p; list_insert_after (t src_p) src dest = []; t src_p \<noteq> []\<rbrakk> \<Longrightarrow> Some dest = next_child src_p t
 7. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src; src_p \<in> descendants_of src m \<and> next_not_child src_p t m = next_not_child src t m; p \<in> descendants_of src m \<longrightarrow> next_not_child p t m \<noteq> next_not_child src t m; p = src_p; list_insert_after (t src_p) src dest = []; t src_p = []\<rbrakk> \<Longrightarrow> Some dest = next_not_child src t m
 8. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src; src_p \<in> descendants_of src m \<longrightarrow> next_not_child src_p t m \<noteq> next_not_child src t m; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p = src_p; list_insert_after (t src_p) src dest \<noteq> []; t src_p = []\<rbrakk> \<Longrightarrow> next_child src_p t = next_not_child src_p t m
 9. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src; src_p \<in> descendants_of src m \<longrightarrow> next_not_child src_p t m \<noteq> next_not_child src t m; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p = src_p; list_insert_after (t src_p) src dest = []; t src_p \<noteq> []\<rbrakk> \<Longrightarrow> next_not_child src_p t m = next_child src_p t
 10. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src; src_p \<in> descendants_of src m \<longrightarrow> next_not_child src_p t m \<noteq> next_not_child src t m; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> src_p; t p = []\<rbrakk> \<Longrightarrow> Some dest = next_not_child src t m
A total of 12 subgoals... proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; src_p \<noteq> dest; src_p \<noteq> src; src_p \<in> descendants_of src m \<and> next_not_child src_p t m = next_not_child src t m; p = src_p; list_insert_after (t src_p) src dest = []; t src_p \<noteq> []\<rbrakk> \<Longrightarrow> Some dest = next_child src_p t
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; src_p \<noteq> dest; src_p \<noteq> src; src_p \<in> descendants_of src m \<and> next_not_child src_p t m = next_not_child src t m; p = src_p; t src_p = []\<rbrakk> \<Longrightarrow> Some dest = next_not_child src t m
 3. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src; src_p \<in> descendants_of src m \<and> next_not_child src_p t m = next_not_child src t m; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> src_p; t p = []\<rbrakk> \<Longrightarrow> Some dest = next_not_child src t m
 4. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src; src_p \<in> descendants_of src m \<longrightarrow> next_not_child src_p t m \<noteq> next_not_child src t m; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> src_p; t p = []\<rbrakk> \<Longrightarrow> Some dest = next_not_child src t m
 5. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; src_p \<noteq> dest; src_p \<noteq> src; src_p \<in> descendants_of src m \<longrightarrow> next_not_child src_p t m \<noteq> next_not_child src t m; p = src_p; list_insert_after (t src_p) src dest = []; t src_p \<noteq> []\<rbrakk> \<Longrightarrow> next_not_child src_p t m = next_child src_p t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; p \<noteq> dest; p \<noteq> src; src_p \<in> descendants_of src m \<longrightarrow> next_not_child src_p t m \<noteq> next_not_child src t m; p \<in> descendants_of src m \<and> next_not_child p t m = next_not_child src t m; p \<noteq> src_p; t p = []\<rbrakk> \<Longrightarrow> Some dest = next_not_child src t m
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; src_p \<noteq> dest; src_p \<noteq> src; src_p \<in> descendants_of src m \<longrightarrow> next_not_child src_p t m \<noteq> next_not_child src t m; p = src_p; list_insert_after (t src_p) src dest = []; t src_p \<noteq> []\<rbrakk> \<Longrightarrow> next_not_child src_p t m = next_child src_p t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; t src = []; src_p \<noteq> dest; src_p \<noteq> src; src_p \<in> descendants_of src m \<longrightarrow> next_not_child src_p t m \<noteq> next_not_child src t m; p = src_p; list_insert_after (t src_p) src dest = []; t src_p \<noteq> []\<rbrakk> \<Longrightarrow> next_not_child src_p t m = next_child src_p t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; m src = Some src_p; set (t src) = {}; src_p \<noteq> dest; src_p \<noteq> src; src_p \<in> descendants_of src m \<longrightarrow> next_not_child src_p t m \<noteq> next_not_child src t m; p = src_p; set (list_insert_after (t src_p) src dest) = {}; set (t src_p) \<noteq> {}\<rbrakk> \<Longrightarrow> next_not_child src_p t m = next_child src_p t proof (prove)
goal:
No subgoals!