kings-crown/FVELER_Isabelle huggingface dataset:
theory Deterministic_AI

lemma next_not_child_termination:
  "finite_depth m \<Longrightarrow> next_not_child_dom (slot, t, m)" apply(induct_tac rule: cdt_induct[where m=m]) apply(rule next_not_child_domintros) apply(simp) apply(rule next_not_child_domintros) apply(simp) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite_depth m \<Longrightarrow> next_not_child_dom (slot, t, m) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>finite_depth m; m x = None\<rbrakk> \<Longrightarrow> next_not_child_dom (x, t, m)
 2. \<And>x y. \<lbrakk>finite_depth m; m x = Some y; next_not_child_dom (y, t, m)\<rbrakk> \<Longrightarrow> next_not_child_dom (x, t, m)
 3. finite_depth m \<Longrightarrow> finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>finite_depth m; m x = None; next_sib x t m = None; m x = Some xa\<rbrakk> \<Longrightarrow> next_not_child_dom (xa, t, m)
 2. \<And>x y. \<lbrakk>finite_depth m; m x = Some y; next_not_child_dom (y, t, m)\<rbrakk> \<Longrightarrow> next_not_child_dom (x, t, m)
 3. finite_depth m \<Longrightarrow> finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>finite_depth m; m x = Some y; next_not_child_dom (y, t, m)\<rbrakk> \<Longrightarrow> next_not_child_dom (x, t, m)
 2. finite_depth m \<Longrightarrow> finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>x y xa. \<lbrakk>finite_depth m; m x = Some y; next_not_child_dom (y, t, m); next_sib x t m = None; m x = Some xa\<rbrakk> \<Longrightarrow> next_not_child_dom (xa, t, m)
 2. finite_depth m \<Longrightarrow> finite_depth m proof (prove)
goal (1 subgoal):
 1. finite_depth m \<Longrightarrow> finite_depth m proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_not_child_pinduct':
  "\<lbrakk>next_not_child_dom (slot, t, m);
   \<And>slot.
      \<lbrakk>next_not_child_dom (slot, t, m);
       \<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a t m\<rbrakk>
      \<Longrightarrow> P slot t m\<rbrakk>
  \<Longrightarrow> P slot t m" apply(induct rule: next_not_child.pinduct) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_not_child_dom (slot, t, m); \<And>slot. \<lbrakk>next_not_child_dom (slot, t, m); \<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a t m\<rbrakk> \<Longrightarrow> P slot t m\<rbrakk> \<Longrightarrow> P slot t m proof (prove)
goal (1 subgoal):
 1. \<And>slot t m. \<lbrakk>next_not_child_dom (slot, t, m); \<And>x2. \<lbrakk>next_sib slot t m = None; m slot = Some x2; \<And>slot. \<lbrakk>next_not_child_dom (slot, t, m); \<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a t m\<rbrakk> \<Longrightarrow> P slot t m\<rbrakk> \<Longrightarrow> P x2 t m; \<And>slot. \<lbrakk>next_not_child_dom (slot, t, m); \<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a t m\<rbrakk> \<Longrightarrow> P slot t m\<rbrakk> \<Longrightarrow> P slot t m proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_not_child_pinduct:
  "\<lbrakk>\<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a\<rbrakk>
    \<Longrightarrow> P slot; finite_depth m\<rbrakk>
      \<Longrightarrow> P slot" apply(rule_tac t=t and m=m in next_not_child_pinduct') apply(rule next_not_child_termination) apply(assumption) apply(fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>slot. (\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a) \<Longrightarrow> P slot; finite_depth m\<rbrakk> \<Longrightarrow> P slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>slot. (\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a) \<Longrightarrow> P slot; finite_depth m\<rbrakk> \<Longrightarrow> next_not_child_dom (slot, t, m)
 2. \<And>slot. \<lbrakk>\<And>slot. (\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a) \<Longrightarrow> P slot; finite_depth m; next_not_child_dom (slot, t, m); \<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a\<rbrakk> \<Longrightarrow> P slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>slot. (\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a) \<Longrightarrow> P slot; finite_depth m\<rbrakk> \<Longrightarrow> finite_depth m
 2. \<And>slot. \<lbrakk>\<And>slot. (\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a) \<Longrightarrow> P slot; finite_depth m; next_not_child_dom (slot, t, m); \<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a\<rbrakk> \<Longrightarrow> P slot proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>\<And>slot. (\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a) \<Longrightarrow> P slot; finite_depth m; next_not_child_dom (slot, t, m); \<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a\<rbrakk> \<Longrightarrow> P a\<rbrakk> \<Longrightarrow> P slot proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_not_child_pinduct2:
  "\<lbrakk>\<And>a slot. \<lbrakk>next_sib a t m = None; m a = Some slot; P a\<rbrakk> \<Longrightarrow> P slot;
    next_not_child p t m = Some n; P p;
    \<forall>a slot. next_sib a t m = Some slot \<longrightarrow> P slot; finite_depth m\<rbrakk>
    \<Longrightarrow> P n" by (rule next_not_child_pinduct2', simp_all add: next_not_child_termination)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a slot. \<lbrakk>next_sib a t m = None; m a = Some slot; P a\<rbrakk> \<Longrightarrow> P slot; next_not_child p t m = Some n; P p; \<forall>a slot. next_sib a t m = Some slot \<longrightarrow> P slot; finite_depth m\<rbrakk> \<Longrightarrow> P n
theory Deterministic_AI

lemma next_not_child_linearI':
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  assumes f_d: "finite_depth m" shows
  "\<lbrakk>finite_depth m'; m p = m' p; next_sib p t m = next_sib p t' m';
     \<forall>q. p \<in> descendants_of q m \<longrightarrow> m q = m' q
     \<and> (m q = m' q \<longrightarrow> next_sib q t m = next_sib q t' m')\<rbrakk>
    \<Longrightarrow> next_not_child p t' m' = next_not_child p t m" using f_d apply (rule next_not_child_linearI,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite_depth m'; m p = m' p; next_sib p t m = next_sib p t' m'; \<forall>q. p \<in> descendants_of q m \<longrightarrow> m q = m' q \<and> (m q = m' q \<longrightarrow> next_sib q t m = next_sib q t' m')\<rbrakk> \<Longrightarrow> next_not_child p t' m' = next_not_child p t m proof (prove)
using this:
finite_depth m

goal (1 subgoal):
 1. \<lbrakk>finite_depth m'; m p = m' p; next_sib p t m = next_sib p t' m'; \<forall>q. p \<in> descendants_of q m \<longrightarrow> m q = m' q \<and> (m q = m' q \<longrightarrow> next_sib q t m = next_sib q t' m')\<rbrakk> \<Longrightarrow> next_not_child p t' m' = next_not_child p t m proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_not_childI:
  "\<lbrakk>next_sib p t m = Some n \<or>
   (next_sib p t m = None \<and>
     (\<exists>q. next_sib q t m = Some n \<and> p \<in> descendants_of q m
     \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m
        \<longrightarrow> next_sib q' t m = None))); finite_depth m\<rbrakk>
    \<Longrightarrow> next_not_child p t m = Some n" by(simp add: next_not_childI')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib p t m = Some n \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)); finite_depth m\<rbrakk> \<Longrightarrow> next_not_child p t m = Some n
theory Deterministic_AI

lemma next_not_child_NoneI:
  "\<lbrakk>\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None;
    next_sib p t m = None; finite_depth m\<rbrakk>
    \<Longrightarrow> next_not_child p t m = None" by(simp add: next_not_child_NoneI')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib p t m = None; finite_depth m\<rbrakk> \<Longrightarrow> next_not_child p t m = None
theory Deterministic_AI

lemma next_not_childD:
   notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>next_not_child p t m = Some n; finite_depth m; no_mloop m\<rbrakk>
    \<Longrightarrow> next_sib p t m = Some n \<or>
       (next_sib p t m = None \<and>
         (\<exists>q. next_sib q t m = Some n \<and> p \<in> descendants_of q m
          \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m
           \<longrightarrow> next_sib q' t m = None)))" by (simp add: next_not_childD')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_not_child p t m = Some n; finite_depth m; no_mloop m\<rbrakk> \<Longrightarrow> next_sib p t m = Some n \<or> next_sib p t m = None \<and> (\<exists>q. next_sib q t m = Some n \<and> p \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> p \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))
theory Deterministic_AI

lemma next_not_child_NoneD:
  "\<lbrakk>next_not_child p t m = None; finite_depth m\<rbrakk>
    \<Longrightarrow> (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and>
        next_sib p t m = None" by (simp add: next_not_child_NoneD')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_not_child p t m = None; finite_depth m\<rbrakk> \<Longrightarrow> (\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<and> next_sib p t m = None
theory Deterministic_AI

lemma slot_in_one_list:
  "\<lbrakk>c \<in> set (t p); c \<in> set (t p'); valid_list_2 t m\<rbrakk> \<Longrightarrow> p = p'" by (simp only: valid_list_2_def, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> set (t p); c \<in> set (t p'); valid_list_2 t m\<rbrakk> \<Longrightarrow> p = p'
theory Deterministic_AI

lemma no_mloop_descendants:
  "no_mloop m = (\<forall>x. x \<notin> descendants_of x m)" by (clarsimp simp: no_mloop_def descendants_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_mloop m = (\<forall>x. x \<notin> descendants_of x m)
theory Deterministic_AI

lemma no_mloop_descendants':
  "no_mloop m \<Longrightarrow> x \<notin> descendants_of x m" by (simp add: no_mloop_descendants del: split_paired_All)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_mloop m \<Longrightarrow> x \<notin> descendants_of x m
theory Deterministic_AI

lemma valid_list_2D:
  notes split_paired_All[simp del]
  shows
  "valid_list_2 t m \<Longrightarrow> src \<in> set (t p) \<Longrightarrow> m src = Some p" apply (simp add: valid_list_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; src \<in> set (t p)\<rbrakk> \<Longrightarrow> m src = Some p proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma replace_parent_ignore:
  notes split_paired_All[simp del]
  shows
  "valid_list_2 t m \<Longrightarrow> m src \<noteq> Some src_p \<Longrightarrow> (list_replace (t src_p) src dest) = (t src_p)" apply (rule list_replace_ignore) apply (clarsimp simp add: valid_list_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src \<noteq> Some src_p\<rbrakk> \<Longrightarrow> list_replace (t src_p) src dest = t src_p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src \<noteq> Some src_p\<rbrakk> \<Longrightarrow> src \<notin> set (t src_p) proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma after_in_list_not_parent:
  notes split_paired_All[simp del]
  shows
  "valid_list_2 t m \<Longrightarrow> no_mloop m \<Longrightarrow> after_in_list (t x) z \<noteq> Some x" apply (rule notI) apply (frule(1) valid_list_2D[OF _ after_in_list_in_list]) apply (frule(1) no_mloop_neq,simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; no_mloop m\<rbrakk> \<Longrightarrow> after_in_list (t x) z \<noteq> Some x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; no_mloop m; after_in_list (t x) z = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; no_mloop m; after_in_list (t x) z = Some x; m x = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma ancestor_not_descendant:
notes split_paired_All[simp del]
shows
"no_mloop m \<Longrightarrow> src \<in> descendants_of src_p m \<Longrightarrow> src_p \<notin> descendants_of src m" apply (rule notI) apply (frule(1) descendants_trans) apply (simp add: no_mloop_def descendants_of_def) done

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

lemma next_sib_same_parent:
notes split_paired_All[simp del] split_paired_Ex[simp del]
shows
"valid_list_2 t m \<Longrightarrow> next_sib sib t m = Some me \<Longrightarrow> \<exists>p. m sib = Some p \<and> m me = Some p" apply (simp add: next_sib_def split: option.splits) apply (drule after_in_list_in_list) apply (simp add: valid_list_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; next_sib sib t m = Some me\<rbrakk> \<Longrightarrow> \<exists>p. m sib = Some p \<and> m me = Some p proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>valid_list_2 t m; m sib = Some x2; after_in_list (t x2) sib = Some me\<rbrakk> \<Longrightarrow> m me = Some x2 proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>valid_list_2 t m; m sib = Some x2; me \<in> set (t x2)\<rbrakk> \<Longrightarrow> m me = Some x2 proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma after_in_list_not_self:
  "\<lbrakk>m c = Some p; valid_list_2 t m\<rbrakk> \<Longrightarrow> after_in_list (t p) c \<noteq> Some c" apply (simp only: valid_list_2_def) apply (erule conjE) apply (drule_tac x = p in spec)+ apply (thin_tac "set (t p) = {c. m c = Some p}") apply (rule notI) apply (rule_tac x = "(t p, c)" in after_in_list.cases, simp, simp) apply (blast intro: after_in_list_not_self_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some p; valid_list_2 t m\<rbrakk> \<Longrightarrow> after_in_list (t p) c \<noteq> Some c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some p; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p))\<rbrakk> \<Longrightarrow> after_in_list (t p) c \<noteq> Some c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some p; \<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p)\<rbrakk> \<Longrightarrow> after_in_list (t p) c \<noteq> Some c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some p; set (t p) = {c. m c = Some p}; distinct (t p)\<rbrakk> \<Longrightarrow> after_in_list (t p) c \<noteq> Some c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some p; distinct (t p)\<rbrakk> \<Longrightarrow> after_in_list (t p) c \<noteq> Some c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some p; distinct (t p); after_in_list (t p) c = Some c\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x y xs a. \<lbrakk>m c = Some p; distinct (t p); after_in_list (t p) c = Some c; (t p, c) = (x # y # xs, a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma not_sib_self:
  "valid_list_2 t m \<Longrightarrow> next_sib slot t m \<noteq> Some slot" by (case_tac "m slot", auto simp: next_sib_def after_in_list_not_self)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_list_2 t m \<Longrightarrow> next_sib slot t m \<noteq> Some slot
theory Deterministic_AI

lemma remove_collect: "{y. P y} - {x} = {y. P y \<and> y \<noteq> x}" apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {y. P y} - {x} = {y. P y \<and> y \<noteq> x} proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma valid_list_post':
  "\<lbrakk> t' src = []\<rbrakk> \<Longrightarrow>
      valid_list_2 (t'(src := [dest]))
        (m(dest \<mapsto> src))" by (insert valid_list_post[where src=src],simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t' src = [] \<Longrightarrow> valid_list_2 (t'(src := [dest])) (m(dest \<mapsto> src))
theory Deterministic_AI

lemma valid_list_post':
  "\<lbrakk> t src = []\<rbrakk> \<Longrightarrow>
      valid_list_2 (t(src := [dest]))
        (m(dest \<mapsto> src))" by (insert valid_list_post[where src=src],simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t src = [] \<Longrightarrow> valid_list_2 (t(src := [dest])) (m(dest \<mapsto> src))
theory Deterministic_AI

lemma valid_list_post_no_parent:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>m src = None\<rbrakk> \<Longrightarrow> valid_list_2 t n" apply (insert valid_list dest) apply (simp add: valid_list_2_def n_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m src = None \<Longrightarrow> valid_list_2 t n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = None; valid_list_2 t m; m dest = None\<rbrakk> \<Longrightarrow> valid_list_2 t n 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 src = Some p\<rbrakk>
    \<Longrightarrow> valid_list_2 (t(p := list_insert_after (t p) src dest)) n" apply (insert valid_list dest neq) apply (simp add: valid_list_2_def n_def) apply (fastforce simp: distinct_list_insert_after  set_list_insert_after) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m src = Some p \<Longrightarrow> valid_list_2 (t(p := list_insert_after (t p) src dest)) n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some p; valid_list_2 t m; m dest = None; dest \<noteq> src\<rbrakk> \<Longrightarrow> valid_list_2 (t(p := list_insert_after (t p) src dest)) n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some p; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m dest = None; dest \<noteq> src\<rbrakk> \<Longrightarrow> (\<forall>pa. (pa = p \<longrightarrow> set (list_insert_after (t p) src dest) = {c. c \<noteq> dest \<longrightarrow> m c = Some p}) \<and> (pa \<noteq> p \<longrightarrow> {c. m c = Some pa} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some pa)})) \<and> distinct (list_insert_after (t p) src dest) 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 src = None\<rbrakk> \<Longrightarrow> valid_list_2 t' n" apply (insert valid_list dest) apply (simp add: valid_list_2_def t'_def n_def) apply (simp add: list_remove_removed insert_Collect remove_collect) apply (fastforce simp: list_remove_distinct cong: Collect_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m src = None \<Longrightarrow> valid_list_2 t' n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = None; valid_list_2 t m; m dest = Some dest_p\<rbrakk> \<Longrightarrow> valid_list_2 t' n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m dest = Some dest_p\<rbrakk> \<Longrightarrow> (\<forall>p. (p = dest_p \<longrightarrow> set (list_remove (t dest_p) dest) = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some dest_p)}) \<and> (p \<noteq> dest_p \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)})) \<and> distinct (list_remove (t dest_p) dest) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m dest = Some dest_p\<rbrakk> \<Longrightarrow> (\<forall>p. (p = dest_p \<longrightarrow> {c. m c = Some dest_p \<and> c \<noteq> dest} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some dest_p)}) \<and> (p \<noteq> dest_p \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)})) \<and> distinct (list_remove (t dest_p) dest) 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 src = Some p\<rbrakk>
    \<Longrightarrow> valid_list_2 (t'(p := list_insert_after (t' p) src dest)) n" apply (insert valid_list dest neq) apply (simp add: valid_list_2_def t'_def n_def) apply (fastforce simp: distinct_list_insert_after list_remove_distinct set_list_insert_after list_remove_removed) done

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

lemma valid_list_post:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "valid_list_2 t m
    \<Longrightarrow> valid_list_2 (t(src := dest # t src))
        (m(dest \<mapsto> src))" apply (insert dest) apply(fastforce simp: valid_list_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_list_2 t m \<Longrightarrow> valid_list_2 (t(src := dest # t src)) (m(dest \<mapsto> src)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m dest = None\<rbrakk> \<Longrightarrow> valid_list_2 (t(src := dest # t src)) (m(dest \<mapsto> src)) proof (prove)
goal:
No subgoals!