theory Deterministic_AI

lemma next_child:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>valid_list_2 t m; m src = Some src_p\<rbrakk>
    \<Longrightarrow> next_child p (t(src_p := list_insert_after (t src_p) src dest)) = next_child p t" apply(simp add: next_child_def) apply(case_tac "list_insert_after (t src_p) src dest") apply(simp) apply(case_tac "t src_p") apply(simp) apply(simp split: if_split_asm) apply(simp) apply(case_tac "t src_p") apply(simp) apply(simp split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p\<rbrakk> \<Longrightarrow> next_child p (t(src_p := list_insert_after (t src_p) src dest)) = next_child p t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> (case list_insert_after (t src_p) src dest of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = []\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> (case list_insert_after (t src_p) src dest of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x)
 2. \<And>a list. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = a # list\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> (case list_insert_after (t src_p) src dest of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = []\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> None = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x)
 2. \<And>a list. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = a # list\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> (case list_insert_after (t src_p) src dest of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = []; t src_p = []\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> None = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x)
 2. \<And>a list. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = []; t src_p = a # list\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> None = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x)
 3. \<And>a list. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = a # list\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> (case list_insert_after (t src_p) src dest of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = []; t src_p = a # list\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> None = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x)
 2. \<And>a list. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = a # list\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> (case list_insert_after (t src_p) src dest of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = a # list\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> (case list_insert_after (t src_p) src dest of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = a # list\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> Some a = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = a # list; t src_p = []\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> Some a = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x)
 2. \<And>a list aa lista. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = a # list; t src_p = aa # lista\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> Some a = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>valid_list_2 t m; m src = Some src_p; list_insert_after (t src_p) src dest = a # list; t src_p = aa # lista\<rbrakk> \<Longrightarrow> p = src_p \<longrightarrow> Some a = (case t src_p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) proof (prove)
goal:
No subgoals!