kings-crown/FVELER_Isabelle huggingface dataset:
theory Deterministic_AI

lemma next_sib_no_parent:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "valid_list_2 t m \<Longrightarrow> m src = None
    \<Longrightarrow> next_sib p (t(src := [], dest := t src)) m'
      = (if p = src then None
         else if p = dest then next_sib src t m
         else if next_sib p t m = Some src then Some dest
         else next_sib p t m)" apply (simp add: next_sib_def m'_def m''_def split: if_split) apply (intro impI conjI) apply (simp split: option.splits  | drule(1) valid_list_2D[OF _ after_in_list_in_list])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_sib p (t(src := [], dest := t src)) m' = (if p = src then None else if p = dest then next_sib src t m else if next_sib p t m = Some src then Some dest else next_sib p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> (m p = Some src \<longrightarrow> after_in_list (t src) p = Some src \<longrightarrow> p \<noteq> dest \<longrightarrow> p = src) \<and> (m p \<noteq> Some src \<longrightarrow> ((case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) = Some src \<longrightarrow> p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = dest then t src else if pa = src then [] else t pa) p) = Some dest) \<and> ((case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) \<noteq> Some src \<longrightarrow> p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = dest then t src else if pa = src then [] else t pa) p) = (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m src = None; m p = Some src; after_in_list (t src) p = Some src; p \<noteq> dest\<rbrakk> \<Longrightarrow> p = src
 2. \<lbrakk>valid_list_2 t m; m src = None; m p \<noteq> Some src; (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) = Some src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = dest then t src else if pa = src then [] else t pa) p) = Some dest
 3. \<lbrakk>valid_list_2 t m; m src = None; m p \<noteq> Some src; (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) \<noteq> Some src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = dest then t src else if pa = src then [] 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!
theory Deterministic_AI

lemma next_not_child_root:
  assumes findepth: "finite_depth k"
  shows
  "k p = None \<Longrightarrow> next_not_child p t k = None" apply (subst next_not_child.psimps[OF next_not_child_termination[OF findepth]]) apply (simp add: next_sib_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. k p = None \<Longrightarrow> next_not_child p t k = None proof (prove)
goal (1 subgoal):
 1. k p = None \<Longrightarrow> (if next_sib p t k = None then case k p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t k else next_sib p t k) = None proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma m'_helper: "m src = k \<Longrightarrow> m' dest = k" apply (clarsimp simp: m'_def m''_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m src = k \<Longrightarrow> m' dest = k proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma m'_helper2: "x \<noteq> src \<Longrightarrow> x \<noteq> dest \<Longrightarrow> m x \<noteq> Some src \<Longrightarrow> m' x = m x" apply (clarsimp simp: m'_def m''_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> src; x \<noteq> dest; m x \<noteq> Some src\<rbrakk> \<Longrightarrow> m' x = m x proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma m'_helper3: "x \<noteq> dest \<Longrightarrow> m x = Some src \<Longrightarrow> m' x = Some dest" apply (clarsimp simp: m'_def m''_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> dest; m x = Some src\<rbrakk> \<Longrightarrow> m' x = Some dest proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma m'_helper4: "m' src = None" apply (clarsimp simp: m'_def m''_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' src = None proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma src_loop_facts:  "m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src" "m src = Some src_p \<Longrightarrow> src_p \<noteq> src" apply - apply (rule notI) apply (frule child_descendant) apply (frule parent_not_descendant[OF no_mloop],simp) apply (rule notI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src) &&& (m src = Some src_p \<Longrightarrow> src_p \<noteq> src) proof (prove)
goal (2 subgoals):
 1. m src = Some src_p \<Longrightarrow> m src_p \<noteq> Some src
 2. m src = Some src_p \<Longrightarrow> src_p \<noteq> src proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some src_p; m src_p = Some src\<rbrakk> \<Longrightarrow> False
 2. m src = Some src_p \<Longrightarrow> src_p \<noteq> src proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some src_p; m src_p = Some src; src \<in> descendants_of src_p m\<rbrakk> \<Longrightarrow> False
 2. m src = Some src_p \<Longrightarrow> src_p \<noteq> src proof (prove)
goal (1 subgoal):
 1. m src = Some src_p \<Longrightarrow> src_p \<noteq> src proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some src_p; src_p = src\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_not_child_helper':
notes split_paired_All[simp del] split_paired_Ex[simp del]
  notes nnext = next_not_child.psimps[OF next_not_child_termination[OF findepth]]
  notes nnext' = next_not_child.psimps[OF next_not_child_termination[OF finite_depth]]
shows
"\<lbrakk>valid_list_2 t m; m src = Some src_p; m slot = None\<rbrakk>
           \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src))
               m' =
              (if slot = src then None
               else if slot = dest then next_not_child src t m
                    else if next_not_child slot t m = Some src then Some dest
                         else next_not_child slot t m)" apply (simp add: next_sib m'_helpers
          nnext[where slot=slot]
          nnext[where slot=dest]
          nnext[where slot=src]
          nnext'[where slot=slot]
          nnext'[where slot=dest]
          nnext'[where slot=src]) apply (intro impI conjI,simp_all) apply (rule next_not_child_parent,simp+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; m slot = None\<rbrakk> \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; m slot = None\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; m dest = None; next_sib src t m = None; slot = dest\<rbrakk> \<Longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src_p t m proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_not_child_helper'':
notes split_paired_All[simp del] split_paired_Ex[simp del]
  notes nnext = next_not_child.psimps[OF next_not_child_termination[OF findepth]]
  notes nnext' = next_not_child.psimps[OF next_not_child_termination[OF finite_depth]]

shows
  "\<lbrakk>valid_list_2 t m; m src = Some src_p; m slot = Some a;
        next_sib slot t m = Some aa\<rbrakk>
       \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' =
          (if slot = src then None
           else if slot = dest then next_not_child src t m
                else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m)" apply (simp add: next_sib m'_helpers
          nnext[where slot=slot]
          nnext'[where slot=slot] ) apply (intro impI conjI,simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; m slot = Some a; next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; m slot = Some a; next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> (next_sib src t m = None \<longrightarrow> slot = dest \<longrightarrow> next_not_child src_p (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = next_not_child src t m) \<and> ((\<exists>y. next_sib src t m = Some y) \<longrightarrow> slot = dest \<longrightarrow> next_sib src t m = next_not_child src t m) proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma valid_list_post_no_parent:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>m slot = None\<rbrakk> \<Longrightarrow> valid_list_2 (t(slot := [])) n" apply (insert valid_list) apply(simp add: valid_list_2_def n_def) apply(intro conjI impI allI notI) apply(fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m slot = None \<Longrightarrow> valid_list_2 (t(slot := [])) n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = None; valid_list_2 t m\<rbrakk> \<Longrightarrow> valid_list_2 (t(slot := [])) n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p))\<rbrakk> \<Longrightarrow> \<forall>p. p \<noteq> slot \<longrightarrow> {c. m c = Some p} = {c. m c \<noteq> Some slot \<and> (m c \<noteq> Some slot \<longrightarrow> m c = Some p)} proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>m slot = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); p \<noteq> slot\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. m c \<noteq> Some slot \<and> (m c \<noteq> Some slot \<longrightarrow> m c = Some p)} proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma valid_list_post_self_parent:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>m slot = Some slot_p; slot_p = slot\<rbrakk>
    \<Longrightarrow> valid_list_2 (t(slot_p := list_remove (t slot_p) slot)) n" apply (insert valid_list) apply (simp add: valid_list_2_def n_def list_remove_removed list_remove_distinct) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = Some slot_p; slot_p = slot\<rbrakk> \<Longrightarrow> valid_list_2 (t(slot_p := list_remove (t slot_p) slot)) n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = Some slot_p; slot_p = slot; valid_list_2 t m\<rbrakk> \<Longrightarrow> valid_list_2 (t(slot_p := list_remove (t slot_p) slot)) n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = Some slot; slot_p = slot; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p))\<rbrakk> \<Longrightarrow> \<forall>p. (p = slot \<longrightarrow> {c. m c = Some slot} - {slot} = {c. c \<noteq> slot \<and> (c \<noteq> slot \<longrightarrow> m c = Some slot)}) \<and> (p \<noteq> slot \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> slot \<and> (c \<noteq> slot \<longrightarrow> m c = Some p)}) proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma valid_list_post:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk>
    \<Longrightarrow> valid_list_2 (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n" apply (insert valid_list) apply(simp add: valid_list_2_def n_def) apply(intro conjI impI allI) apply (fastforce simp: set_list_replace_list intro!: distinct_list_replace_list)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> valid_list_2 (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = Some slot_p; slot_p \<noteq> slot; valid_list_2 t m\<rbrakk> \<Longrightarrow> valid_list_2 (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = Some slot_p; slot_p \<noteq> slot; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p))\<rbrakk> \<Longrightarrow> (\<forall>p. (p = slot_p \<longrightarrow> set (list_replace_list (t slot_p) slot (t slot)) = {c. (m c = Some slot \<longrightarrow> c \<noteq> slot) \<and> (m c \<noteq> Some slot \<longrightarrow> c \<noteq> slot \<and> (c \<noteq> slot \<longrightarrow> m c = Some slot_p))}) \<and> (p \<noteq> slot_p \<longrightarrow> p \<noteq> slot \<longrightarrow> {c. m c = Some p} = {c. m c \<noteq> Some slot \<and> (m c \<noteq> Some slot \<longrightarrow> c \<noteq> slot \<and> (c \<noteq> slot \<longrightarrow> m c = Some p))})) \<and> distinct (list_replace_list (t slot_p) slot (t slot)) proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>m slot = Some slot_p; slot_p \<noteq> slot; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); p = slot_p\<rbrakk> \<Longrightarrow> set (list_replace_list (t slot_p) slot (t slot)) = {c. (m c = Some slot \<longrightarrow> c \<noteq> slot) \<and> (m c \<noteq> Some slot \<longrightarrow> c \<noteq> slot \<and> (c \<noteq> slot \<longrightarrow> m c = Some slot_p))}
 2. \<And>p. \<lbrakk>m slot = Some slot_p; slot_p \<noteq> slot; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); p \<noteq> slot_p; p \<noteq> slot\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. m c \<noteq> Some slot \<and> (m c \<noteq> Some slot \<longrightarrow> c \<noteq> slot \<and> (c \<noteq> slot \<longrightarrow> m c = Some p))}
 3. \<lbrakk>m slot = Some slot_p; slot_p \<noteq> slot; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p))\<rbrakk> \<Longrightarrow> distinct (list_replace_list (t slot_p) slot (t slot)) proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma valid_list_post_no_parents:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "m src = None \<Longrightarrow> m dest = None \<Longrightarrow> valid_list_2 t' n" apply (insert valid_list) apply (simp add: t'_def t''_def n_def n'_def valid_list_2_def) apply (intro impI conjI allI) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = None; m dest = None\<rbrakk> \<Longrightarrow> valid_list_2 t' n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = None; m dest = None; valid_list_2 t m\<rbrakk> \<Longrightarrow> valid_list_2 t' n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = None; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p))\<rbrakk> \<Longrightarrow> \<forall>p. p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> {c. m c = Some src} = {c. (m c = Some dest \<longrightarrow> dest = src) \<and> (m c \<noteq> Some dest \<longrightarrow> m c = Some src)}) \<and> (p \<noteq> dest \<longrightarrow> {c. m c = Some p} = {c. m c \<noteq> Some dest \<and> (m c \<noteq> Some dest \<longrightarrow> m c \<noteq> Some src \<and> (m c \<noteq> Some src \<longrightarrow> m c = Some p))}) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>m src = None; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); p \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> {c. m c = Some src} = {c. (m c = Some dest \<longrightarrow> dest = src) \<and> (m c \<noteq> Some dest \<longrightarrow> m c = Some src)}
 2. \<And>p. \<lbrakk>m src = None; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. m c \<noteq> Some dest \<and> (m c \<noteq> Some dest \<longrightarrow> m c \<noteq> Some src \<and> (m c \<noteq> Some src \<longrightarrow> m c = Some p))} proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma valid_list_post:
  "valid_list_2 t' n" apply (case_tac "m src") apply (case_tac "m dest") apply (simp add: valid_list_post_no_parents) apply (simp add: valid_list_post_dest_parent) apply (case_tac "m dest") apply (simp add: valid_list_post_src_parent) apply (simp add: valid_list_post_parents) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_list_2 t' n proof (prove)
goal (2 subgoals):
 1. m src = None \<Longrightarrow> valid_list_2 t' n
 2. \<And>a. m src = Some a \<Longrightarrow> valid_list_2 t' n proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m src = None; m dest = None\<rbrakk> \<Longrightarrow> valid_list_2 t' n
 2. \<And>a. \<lbrakk>m src = None; m dest = Some a\<rbrakk> \<Longrightarrow> valid_list_2 t' n
 3. \<And>a. m src = Some a \<Longrightarrow> valid_list_2 t' n proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>m src = None; m dest = Some a\<rbrakk> \<Longrightarrow> valid_list_2 t' n
 2. \<And>a. m src = Some a \<Longrightarrow> valid_list_2 t' n proof (prove)
goal (1 subgoal):
 1. \<And>a. m src = Some a \<Longrightarrow> valid_list_2 t' n proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>m src = Some a; m dest = None\<rbrakk> \<Longrightarrow> valid_list_2 t' n
 2. \<And>a aa. \<lbrakk>m src = Some a; m dest = Some aa\<rbrakk> \<Longrightarrow> valid_list_2 t' n proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>m src = Some a; m dest = Some aa\<rbrakk> \<Longrightarrow> valid_list_2 t' n proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma findepth:
  "finite_depth m" apply (simp add: m) apply (rule Deterministic_AI.finite_depth) apply (rule valid_mdb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite_depth m proof (prove)
goal (1 subgoal):
 1. finite_depth (cdt s) proof (prove)
goal (1 subgoal):
 1. valid_mdb s proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma parency_antisym: "\<And>x y. m x = Some y \<Longrightarrow> m y \<noteq> Some x" apply (frule parent_not_descendant[OF no_mloop]) apply (rule notI) apply (frule_tac src=y and src_p=x in child_descendant,simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x y. m x = Some y \<Longrightarrow> m y \<noteq> Some x proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>m x = Some y; y \<notin> descendants_of x m\<rbrakk> \<Longrightarrow> m y \<noteq> Some x proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>m x = Some y; y \<notin> descendants_of x m; m y = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_child_antisym: "next_child x t = Some y \<Longrightarrow> next_child y t \<noteq> Some x" apply (rule notI) apply (clarsimp dest!: next_childD[OF _ valid_list]) apply (simp add: parency_antisym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_child x t = Some y \<Longrightarrow> next_child y t \<noteq> Some x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_child x t = Some y; next_child y t = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xs xsa. \<lbrakk>m y = Some x; t x = y # xs; m x = Some y; t y = x # xsa\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_childI'': "(\<exists>xs. t''' slot = child # xs) \<Longrightarrow> next_child slot t''' = Some child" apply (elim exE) apply (rule next_childI,simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>xs. t''' slot = child # xs \<Longrightarrow> next_child slot t''' = Some child proof (prove)
goal (1 subgoal):
 1. \<And>xs. t''' slot = child # xs \<Longrightarrow> next_child slot t''' = Some child proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_childD'':
 notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
"next_child slot t''' \<noteq> Some child \<Longrightarrow> t''' slot = [] \<or> (\<exists>xs a. t''' slot = a#xs \<and> a \<noteq> child)" apply (simp add: next_child_def) apply (case_tac "t''' slot") apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_child slot t''' \<noteq> Some child \<Longrightarrow> t''' slot = [] \<or> (\<exists>xs a. t''' slot = a # xs \<and> a \<noteq> child) proof (prove)
goal (1 subgoal):
 1. (case t''' slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) \<noteq> Some child \<Longrightarrow> t''' slot = [] \<or> (\<exists>xs a. t''' slot = a # xs \<and> a \<noteq> child) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(case t''' slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) \<noteq> Some child; t''' slot = []\<rbrakk> \<Longrightarrow> t''' slot = [] \<or> (\<exists>xs a. t''' slot = a # xs \<and> a \<noteq> child)
 2. \<And>a list. \<lbrakk>(case t''' slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) \<noteq> Some child; t''' slot = a # list\<rbrakk> \<Longrightarrow> t''' slot = [] \<or> (\<exists>xs a. t''' slot = a # xs \<and> a \<noteq> child) proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_child_eq_ignore: "g p = g' p \<Longrightarrow> next_child p g = next_child p g'" by(simp add: next_child_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. g p = g' p \<Longrightarrow> next_child p g = next_child p g'