theory Deterministic_AI

lemma next_sib:
  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_sib p (t(src_p := list_insert_after (t src_p) src dest)) n
    = (if p = src \<and> m src \<noteq> None then Some dest
       else if p = dest then next_sib src t m
       else next_sib p t m)" apply(subgoal_tac "dest \<notin> set (t src_p) \<and> src \<in> set (t src_p)") prefer 2 apply(simp add: valid_list_2_def) apply(simp add: next_sib_def n_def neq list_insert_after_after valid_list_2_def) apply(case_tac "m p") apply(simp) apply(simp add: list_insert_after_after) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p\<rbrakk> \<Longrightarrow> next_sib p (t(src_p := list_insert_after (t src_p) src dest)) n = (if p = src \<and> m src \<noteq> None then Some dest else if p = dest then next_sib src t m else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; dest \<notin> set (t src_p) \<and> src \<in> set (t src_p)\<rbrakk> \<Longrightarrow> next_sib p (t(src_p := list_insert_after (t src_p) src dest)) n = (if p = src \<and> m src \<noteq> None then Some dest else if p = dest then next_sib src t m else next_sib p t m)
 2. \<lbrakk>valid_list_2 t m; m src = Some src_p\<rbrakk> \<Longrightarrow> dest \<notin> set (t src_p) \<and> src \<in> set (t src_p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p\<rbrakk> \<Longrightarrow> dest \<notin> set (t src_p) \<and> src \<in> set (t src_p)
 2. \<lbrakk>valid_list_2 t m; m src = Some src_p; dest \<notin> set (t src_p) \<and> src \<in> set (t src_p)\<rbrakk> \<Longrightarrow> next_sib p (t(src_p := list_insert_after (t src_p) src dest)) n = (if p = src \<and> m src \<noteq> None then Some dest else if p = dest then next_sib src t m else next_sib p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; dest \<notin> set (t src_p) \<and> src \<in> set (t src_p)\<rbrakk> \<Longrightarrow> next_sib p (t(src_p := list_insert_after (t src_p) src dest)) n = (if p = src \<and> m src \<noteq> None then Some dest else if p = dest then next_sib src t m else next_sib p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m src = Some src_p\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = src_p then list_insert_after (t src_p) src dest else t pa) p) = (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m src = Some src_p; m p = None\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = src_p then list_insert_after (t src_p) src dest else t pa) p) = (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p)
 2. \<And>a. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m src = Some src_p; m p = Some a\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = src_p then list_insert_after (t src_p) src dest else t pa) p) = (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m src = Some src_p; m p = Some a\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = src_p then list_insert_after (t src_p) src dest else t pa) p) = (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) proof (prove)
goal:
No subgoals!