theory Deterministic_AI

lemma (in mdb_move_abs') cap_move_ext_det_def2:
 notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
 "valid_list_2 (cdt_list e) m \<Longrightarrow> src_p = (m src) \<Longrightarrow> dest_p = (m dest) \<Longrightarrow>
       cap_move_ext src dest src_p dest_p e =
    (update_cdt_list (\<lambda>list. case (m src) of
      None \<Rightarrow> list (src := [], dest := list src) |
      Some p \<Rightarrow> list (p := list_replace (list p) src dest,
                      src := [], dest := list src))) e" apply (simp add: cap_move_ext_def update_cdt_list_bind) apply (rule update_list_eq) apply (insert dest_None neq) apply (case_tac "m src") apply (simp add: dest_empty_list) apply simp apply (insert no_mloop) apply (frule no_mloop_weaken[where a=src]) apply simp apply (insert dest_desc) apply (intro impI conjI) apply (simp add: no_children_empty_desc[symmetric]) apply (simp add: dest_empty_list) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = m src; dest_p = m dest\<rbrakk> \<Longrightarrow> cap_move_ext src dest src_p dest_p e = update_cdt_list (\<lambda>list. case m src of None \<Rightarrow> list(src := [], dest := list src) | Some p \<Rightarrow> list(p := list_replace (list p) src dest, src := [], dest := list src)) e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = m src; dest_p = m dest\<rbrakk> \<Longrightarrow> update_cdt_list (\<lambda>s. (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest))(p := list_replace ((case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest)) p) src dest))(src := [], dest := (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest))(p := list_replace ((case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest)) p) src dest)) src @ (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest))(p := list_replace ((case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest)) p) src dest)) dest)) e = update_cdt_list (\<lambda>list. case m src of None \<Rightarrow> list(src := [], dest := list src) | Some p \<Rightarrow> list(p := list_replace (list p) src dest, src := [], dest := list src)) e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = m src; dest_p = m dest\<rbrakk> \<Longrightarrow> (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest))(src := [], dest := (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest)) src @ (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest)) dest) = (case m src of None \<Rightarrow> (cdt_list e)(src := [], dest := cdt_list e src) | Some p \<Rightarrow> (cdt_list e)(p := list_replace (cdt_list e p) src dest, src := [], dest := cdt_list e src)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = m src; dest_p = m dest; m dest = None; src \<noteq> dest\<rbrakk> \<Longrightarrow> (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest))(src := [], dest := (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest)) src @ (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest)) dest) = (case m src of None \<Rightarrow> (cdt_list e)(src := [], dest := cdt_list e src) | Some p \<Rightarrow> (cdt_list e)(p := list_replace (cdt_list e p) src dest, src := [], dest := cdt_list e src)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = m src; dest_p = m dest; m dest = None; src \<noteq> dest; m src = None\<rbrakk> \<Longrightarrow> (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest))(src := [], dest := (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest)) src @ (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest)) dest) = (case m src of None \<Rightarrow> (cdt_list e)(src := [], dest := cdt_list e src) | Some p \<Rightarrow> (cdt_list e)(p := list_replace (cdt_list e p) src dest, src := [], dest := cdt_list e src))
 2. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = m src; dest_p = m dest; m dest = None; src \<noteq> dest; m src = Some a\<rbrakk> \<Longrightarrow> (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest))(src := [], dest := (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest)) src @ (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest)) dest) = (case m src of None \<Rightarrow> (cdt_list e)(src := [], dest := cdt_list e src) | Some p \<Rightarrow> (cdt_list e)(p := list_replace (cdt_list e p) src dest, src := [], dest := cdt_list e src)) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = m src; dest_p = m dest; m dest = None; src \<noteq> dest; m src = Some a\<rbrakk> \<Longrightarrow> (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest))(src := [], dest := (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest)) src @ (case m src of None \<Rightarrow> case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(p := list_replace ((case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p) src dest)) dest) = (case m src of None \<Rightarrow> (cdt_list e)(src := [], dest := cdt_list e src) | Some p \<Rightarrow> (cdt_list e)(p := list_replace (cdt_list e p) src dest, src := [], dest := cdt_list e src)) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = Some a; dest_p = None; m dest = None; m src = Some a\<rbrakk> \<Longrightarrow> (src = a \<longrightarrow> (dest = a \<longrightarrow> (cdt_list e)(a := list_replace (cdt_list e a) a a @ list_replace (cdt_list e a) a a) = cdt_list e) \<and> (dest \<noteq> a \<longrightarrow> (cdt_list e)(a := [], dest := list_replace (cdt_list e a) a dest @ cdt_list e dest) = (cdt_list e)(a := [], dest := cdt_list e a))) \<and> (src \<noteq> a \<longrightarrow> (dest = a \<longrightarrow> (cdt_list e)(src := [], a := cdt_list e src @ list_replace (cdt_list e a) src a) = (cdt_list e)(src := [], a := cdt_list e src)) \<and> (dest \<noteq> a \<longrightarrow> (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src @ cdt_list e dest) = (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src))) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = Some a; dest_p = None; m dest = None; m src = Some a; no_mloop m\<rbrakk> \<Longrightarrow> (src = a \<longrightarrow> (dest = a \<longrightarrow> (cdt_list e)(a := list_replace (cdt_list e a) a a @ list_replace (cdt_list e a) a a) = cdt_list e) \<and> (dest \<noteq> a \<longrightarrow> (cdt_list e)(a := [], dest := list_replace (cdt_list e a) a dest @ cdt_list e dest) = (cdt_list e)(a := [], dest := cdt_list e a))) \<and> (src \<noteq> a \<longrightarrow> (dest = a \<longrightarrow> (cdt_list e)(src := [], a := cdt_list e src @ list_replace (cdt_list e a) src a) = (cdt_list e)(src := [], a := cdt_list e src)) \<and> (dest \<noteq> a \<longrightarrow> (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src @ cdt_list e dest) = (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src))) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = Some a; dest_p = None; m dest = None; m src = Some a; no_mloop m; m src \<noteq> Some src\<rbrakk> \<Longrightarrow> (src = a \<longrightarrow> (dest = a \<longrightarrow> (cdt_list e)(a := list_replace (cdt_list e a) a a @ list_replace (cdt_list e a) a a) = cdt_list e) \<and> (dest \<noteq> a \<longrightarrow> (cdt_list e)(a := [], dest := list_replace (cdt_list e a) a dest @ cdt_list e dest) = (cdt_list e)(a := [], dest := cdt_list e a))) \<and> (src \<noteq> a \<longrightarrow> (dest = a \<longrightarrow> (cdt_list e)(src := [], a := cdt_list e src @ list_replace (cdt_list e a) src a) = (cdt_list e)(src := [], a := cdt_list e src)) \<and> (dest \<noteq> a \<longrightarrow> (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src @ cdt_list e dest) = (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src))) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = Some a; dest_p = None; m dest = None; m src = Some a; no_mloop m; a \<noteq> src\<rbrakk> \<Longrightarrow> (dest = a \<longrightarrow> (cdt_list e)(src := [], a := cdt_list e src @ list_replace (cdt_list e a) src a) = (cdt_list e)(src := [], a := cdt_list e src)) \<and> (dest \<noteq> a \<longrightarrow> (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src @ cdt_list e dest) = (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src)) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = Some a; dest_p = None; m dest = None; m src = Some a; no_mloop m; a \<noteq> src; descendants_of dest m = {}\<rbrakk> \<Longrightarrow> (dest = a \<longrightarrow> (cdt_list e)(src := [], a := cdt_list e src @ list_replace (cdt_list e a) src a) = (cdt_list e)(src := [], a := cdt_list e src)) \<and> (dest \<noteq> a \<longrightarrow> (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src @ cdt_list e dest) = (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src)) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = Some a; dest_p = None; m dest = None; m src = Some a; no_mloop m; a \<noteq> src; descendants_of dest m = {}; dest = a\<rbrakk> \<Longrightarrow> (cdt_list e)(src := [], a := cdt_list e src @ list_replace (cdt_list e a) src a) = (cdt_list e)(src := [], a := cdt_list e src)
 2. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = Some a; dest_p = None; m dest = None; m src = Some a; no_mloop m; a \<noteq> src; descendants_of dest m = {}; dest \<noteq> a\<rbrakk> \<Longrightarrow> (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src @ cdt_list e dest) = (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; src_p = Some a; dest_p = None; m dest = None; m src = Some a; no_mloop m; a \<noteq> src; descendants_of dest m = {}; dest \<noteq> a\<rbrakk> \<Longrightarrow> (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src @ cdt_list e dest) = (cdt_list e)(a := list_replace (cdt_list e a) src dest, src := [], dest := cdt_list e src) proof (prove)
goal:
No subgoals!