kings-crown/FVELER_Isabelle huggingface dataset:
theory Deterministic_AI

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

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

lemma next_child:
  "next_child p (t(src := dest # t src))
     = (if p = src then Some dest else next_child p t)" apply(fastforce simp: next_child_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_child p (t(src := dest # t src)) = (if p = src then Some dest else next_child p t) proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_child':
  "t src = []
    \<Longrightarrow> next_child p (t(src := [dest])) = (if p = src then Some dest else next_child p t)" by (fastforce simp: next_child_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t src = [] \<Longrightarrow> next_child p (t(src := [dest])) = (if p = src then Some dest else next_child p t)
theory Deterministic_AI

lemma next_sib':
  "\<lbrakk>valid_list_2 t m; t src = []\<rbrakk>
    \<Longrightarrow> next_sib p (t(src := [dest]))
        (m(dest \<mapsto> src))
     = (if p = dest then None else next_sib p t m)" by (fastforce dest: next_sib[where p=p] intro: next_child_NoneI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; t src = []\<rbrakk> \<Longrightarrow> next_sib p (t(src := [dest])) (m(dest \<mapsto> src)) = (if p = dest then None else next_sib p t m)
theory Deterministic_AI

lemma next_not_child':
  "\<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; t src = []\<rbrakk>
    \<Longrightarrow> next_not_child p (t(src := [dest])) (m(dest \<mapsto> src))
          = (if p = dest then next_not_child src t m
            else next_not_child p t m)" apply(drule(2) next_not_child[where p=p]) apply(simp add: next_slot_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; t src = []\<rbrakk> \<Longrightarrow> next_not_child p (t(src := [dest])) (m(dest \<mapsto> src)) = (if p = dest then next_not_child src t m else next_not_child p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite_depth m; no_mloop m; t src = []; next_not_child p (t(src := dest # t src)) (m(dest \<mapsto> src)) = (if p = dest then next_slot src t m else next_not_child p t m)\<rbrakk> \<Longrightarrow> next_not_child p (t(src := [dest])) (m(dest \<mapsto> src)) = (if p = dest then next_not_child src t m else next_not_child p t m) proof (prove)
goal:
No subgoals!
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\<rbrakk>
    \<Longrightarrow> next_slot p (t(src := dest # t src)) (m(dest \<mapsto> src))
     = (if p = src then Some dest
        else if p = dest then next_slot src t m
        else next_slot p t m)" apply(simp add: next_slot_def next_not_child next_child next_not_child' next_child') apply(rule impI) apply(drule next_child_None_empty_desc[where slot=dest]) apply(simp add: next_child_def) apply(case_tac "t dest", simp, simp add: desc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m\<rbrakk> \<Longrightarrow> next_slot p (t(src := dest # t src)) (m(dest \<mapsto> src)) = (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\<rbrakk> \<Longrightarrow> t dest \<noteq> [] \<longrightarrow> (t src \<noteq> [] \<longrightarrow> p = dest \<longrightarrow> next_child dest t = next_child src t) \<and> (t src = [] \<longrightarrow> p = dest \<longrightarrow> next_child dest t = next_not_child src t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; t dest \<noteq> []\<rbrakk> \<Longrightarrow> (t src \<noteq> [] \<longrightarrow> p = dest \<longrightarrow> next_child dest t = next_child src t) \<and> (t src = [] \<longrightarrow> p = dest \<longrightarrow> next_child dest t = next_not_child src t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite_depth m; no_mloop m; t dest \<noteq> []; (next_child dest t = None) = (descendants_of dest m = {})\<rbrakk> \<Longrightarrow> (t src \<noteq> [] \<longrightarrow> p = dest \<longrightarrow> next_child dest t = next_child src t) \<and> (t src = [] \<longrightarrow> p = dest \<longrightarrow> next_child dest t = next_not_child src t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite_depth m; no_mloop m; t dest \<noteq> []; ((case t dest of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = None) = (descendants_of dest m = {})\<rbrakk> \<Longrightarrow> (t src \<noteq> [] \<longrightarrow> p = dest \<longrightarrow> (case t dest of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = (case t src of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x)) \<and> (t src = [] \<longrightarrow> p = dest \<longrightarrow> (case t dest of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = 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>valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> valid_list_2 t n" apply(insert dest) apply(fastforce simp: n_def valid_list_2_def) done

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

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

lemma next_sib_no_parent:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>valid_list_2 t m; m src = None\<rbrakk>
    \<Longrightarrow> next_sib p t 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(simp add: n_def next_sib_def) 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 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:
No subgoals!
theory Deterministic_AI

lemma set_cap_caps_of_state3:
  "\<lbrace>\<lambda>s. P ((caps_of_state s) (p \<mapsto> cap)) (cdt s)  (exst s) (is_original_cap s)\<rbrace>
  set_cap cap p
  \<lbrace>\<lambda>rv s. P (caps_of_state s) (cdt s) (exst s) (is_original_cap s)\<rbrace>" apply (rule_tac Q="\<lambda>rv s. \<exists>m mr t. P (caps_of_state s) m t mr
                    \<and> (cdt s = m) \<and> (exst s = t) \<and> (is_original_cap s = mr)"
           in hoare_post_imp) apply simp apply (wp hoare_vcg_ex_lift) apply (rule_tac x="cdt s" in exI) apply (rule_tac x="is_original_cap s" in exI) apply (simp add: fun_upd_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (exst s) (is_original_cap s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. P (caps_of_state s) (cdt s) (exst s) (is_original_cap s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<exists>m mr t. P (caps_of_state s) m t mr \<and> cdt s = m \<and> exst s = t \<and> is_original_cap s = mr \<Longrightarrow> P (caps_of_state s) (cdt s) (exst s) (is_original_cap s)
 2. \<lbrace>\<lambda>s. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (exst s) (is_original_cap s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<exists>m mr t. P (caps_of_state s) m t mr \<and> cdt s = m \<and> exst s = t \<and> is_original_cap s = mr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (exst s) (is_original_cap s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<exists>m mr t. P (caps_of_state s) m t mr \<and> cdt s = m \<and> exst s = t \<and> is_original_cap s = mr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (exst s) (is_original_cap s) \<Longrightarrow> \<exists>x xa xb. P ((caps_of_state s)(p \<mapsto> cap)) x xb xa \<and> cdt s = x \<and> exst s = xb \<and> is_original_cap s = xa proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (exst s) (is_original_cap s) \<Longrightarrow> \<exists>x xa. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) xa x \<and> cdt s = cdt s \<and> exst s = xa \<and> is_original_cap s = x proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (exst s) (is_original_cap s) \<Longrightarrow> \<exists>x. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) x (is_original_cap s) \<and> cdt s = cdt s \<and> exst s = x \<and> is_original_cap s = is_original_cap s proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma exst_cdt_update[iff]:
  "exst (s\<lparr>cdt := a\<rparr>) = exst s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. exst (s\<lparr>cdt := a\<rparr>) = exst s
theory Deterministic_AI

lemma self_parent_eq: "m src = Some src \<Longrightarrow> m(dest \<mapsto> src) = m (dest := m src)" by simp

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

lemma set_cap_match: "(\<And>s x. P s = P (s\<lparr>kheap := x\<rparr>)) \<Longrightarrow> \<lbrace>P\<rbrace> set_cap a b \<lbrace>\<lambda>_.P\<rbrace>" apply (simp add: set_cap_def split_def set_object_def get_object_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s x. P s = P (s\<lparr>kheap := x\<rparr>)) \<Longrightarrow> \<lbrace>P\<rbrace> set_cap a b \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>s x. P s = P (s\<lparr>kheap := x\<rparr>)) \<Longrightarrow> \<lbrace>P\<rbrace> do obj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh (fst b) = Some y);
return (the (kh (fst b)))
od;
obj' <- case obj of CNode sz cn \<Rightarrow> if snd b \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd b \<mapsto> a) else fail | TCB tcb \<Rightarrow> if snd b = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := a\<rparr> else if snd b = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := a\<rparr> else if snd b = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := a\<rparr> else if snd b = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := a\<rparr> else if snd b = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := a\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh (fst b) = Some y);
return (the (kh (fst b)))
od;
y <- assert (a_type kobj = a_type obj');
s <- get;
put (s\<lparr>kheap := (kheap s)(fst b \<mapsto> obj')\<rparr>)
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma Collect_union: "{c. P c} \<union> {c. Q c} = {c. P c \<or> Q c}" apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {c. P c} \<union> {c. Q c} = {c. P c \<or> Q c} proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma valid_list_post:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  notes replace_distinct[simplified list_replace_def,simp]
  shows "valid_list_2 (t''(src := [], dest := (t'' src) @ (t'' dest))) m'" apply (case_tac "m src") apply (case_tac "m dest") apply (simp add: valid_list_post_no_parents) apply (simp add: valid_list_post_src_no_parent) apply (case_tac "m dest") apply (simp add: valid_list_post_dest_no_parent) apply (simp add: valid_list_post_parents) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m' proof (prove)
goal (2 subgoals):
 1. m src = None \<Longrightarrow> valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m'
 2. \<And>a. m src = Some a \<Longrightarrow> valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m src = None; m dest = None\<rbrakk> \<Longrightarrow> valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m'
 2. \<And>a. \<lbrakk>m src = None; m dest = Some a\<rbrakk> \<Longrightarrow> valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m'
 3. \<And>a. m src = Some a \<Longrightarrow> valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m' proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>m src = None; m dest = Some a\<rbrakk> \<Longrightarrow> valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m'
 2. \<And>a. m src = Some a \<Longrightarrow> valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m' proof (prove)
goal (1 subgoal):
 1. \<And>a. m src = Some a \<Longrightarrow> valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m' proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>m src = Some a; m dest = None\<rbrakk> \<Longrightarrow> valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m'
 2. \<And>a aa. \<lbrakk>m src = Some a; m dest = Some aa\<rbrakk> \<Longrightarrow> valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m' proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>m src = Some a; m dest = Some aa\<rbrakk> \<Longrightarrow> valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m' 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 valid_list_post_helper:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>dest \<notin> set list;
     distinct list\<rbrakk>
    \<Longrightarrow> distinct
        (map (\<lambda>x. if x = src then dest else x) list)" apply (induct list) apply force+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dest \<notin> set list; distinct list\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. if x = src then dest else x) list) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dest \<notin> set []; distinct []\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. if x = src then dest else x) [])
 2. \<And>a list. \<lbrakk>\<lbrakk>dest \<notin> set list; distinct list\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. if x = src then dest else x) list); dest \<notin> set (a # list); distinct (a # list)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. if x = src then dest else x) (a # list)) 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>valid_list_2 t m; m src = Some src_p\<rbrakk>
    \<Longrightarrow> valid_list_2 (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m'" apply (simp add: valid_list_2_def) apply (rule Collect_cong | simp add: list_replace_def m'_def m''_def split: if_split_asm | intro iffI impI conjI notI allI | force | fastforce)+ apply clarsimp apply (subgoal_tac "dest \<notin> set (t src_p)") apply (blast intro: valid_list_post_helper) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p\<rbrakk> \<Longrightarrow> valid_list_2 (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) 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> (\<forall>p. (p = src_p \<longrightarrow> (src_p = src \<longrightarrow> (\<forall>x. m' x \<noteq> Some src)) \<and> (src_p \<noteq> src \<longrightarrow> (src_p = dest \<longrightarrow> {c. m c = Some src} = {c. m' c = Some dest}) \<and> (src_p \<noteq> dest \<longrightarrow> set (list_replace (t src_p) src dest) = {c. m' c = Some src_p}))) \<and> (p \<noteq> src_p \<longrightarrow> (p = src \<longrightarrow> (\<forall>x. m' x \<noteq> Some src)) \<and> (p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> {c. m c = Some src} = {c. m' c = Some dest}) \<and> (p \<noteq> dest \<longrightarrow> {c. m c = Some p} = {c. m' c = Some p})))) \<and> (src_p \<noteq> src \<longrightarrow> src_p \<noteq> dest \<longrightarrow> distinct (list_replace (t src_p) src dest)) 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; src_p \<noteq> src; src_p \<noteq> dest\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. if x = src then dest else x) (t src_p)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some src_p; src_p \<noteq> src; src_p \<noteq> dest; \<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. if x = src then dest else x) (t src_p)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some src_p; src_p \<noteq> src; src_p \<noteq> dest; \<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p); dest \<notin> set (t src_p)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. if x = src then dest else x) (t src_p))
 2. \<lbrakk>m src = Some src_p; src_p \<noteq> src; src_p \<noteq> dest; \<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p)\<rbrakk> \<Longrightarrow> dest \<notin> set (t src_p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some src_p; src_p \<noteq> src; src_p \<noteq> dest; \<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p)\<rbrakk> \<Longrightarrow> dest \<notin> set (t src_p) 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>valid_list_2 t m; m src = None\<rbrakk>\<Longrightarrow> valid_list_2 (t(src := [], dest := t src)) m'" apply(simp add: valid_list_2_def) apply (rule Collect_cong | simp add: list_replace_def m'_def m''_def split: if_split_asm | intro iffI impI conjI notI allI | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> valid_list_2 (t(src := [], dest := t src)) 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 = None\<rbrakk> \<Longrightarrow> \<forall>p. (p = src \<longrightarrow> (\<forall>x. m' x \<noteq> Some src)) \<and> (p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> {c. m c = Some src} = {c. m' c = Some dest}) \<and> (p \<noteq> dest \<longrightarrow> {c. m c = Some p} = {c. m' c = Some p})) proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_child_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_child p (t(src := [], dest := t src))
      = (if p = src then None
         else if p = dest then next_child src t
         else if next_child p t = Some src then Some dest
         else next_child p t)" apply (simp split: if_split) apply (clarsimp simp add: next_child_def) apply (fold next_child_def) apply (frule(1) next_childD,clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_child p (t(src := [], dest := t src)) = (if p = src then None else if p = dest then next_child src t else if next_child p t = Some src then Some dest else next_child p t) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> (next_child p t = Some src \<longrightarrow> (p = dest \<longrightarrow> next_child dest (t(src := [], dest := t src)) = next_child src t) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_child src (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = Some dest))) \<and> (next_child p t \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> next_child dest (t(src := [], dest := t src)) = next_child src t) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_child src (t(src := [], dest := t src)) = None) \<and> (p \<noteq> src \<longrightarrow> next_child p (t(src := [], dest := t src)) = next_child p t))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = None; (case t p of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = Some src; p \<noteq> dest\<rbrakk> \<Longrightarrow> p = src proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = None; next_child p t = Some src; p \<noteq> dest\<rbrakk> \<Longrightarrow> p = src proof (prove)
goal:
No subgoals!