theory Deterministic_AI

lemma (in mdb_insert_abs) cap_insert_ext_det_def2:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
 "valid_list_2 (cdt_list e) m \<Longrightarrow> no_mloop m \<Longrightarrow> src_p = (m src) \<Longrightarrow> dest_p = (m dest) \<Longrightarrow>
       cap_insert_ext src_parent src dest src_p dest_p e = (\<lambda> src_parent src_slot dest_slot src_p dest_p.
    update_cdt_list (\<lambda>list. case (m src_slot) of
      None \<Rightarrow> list (
        src_slot := if src_parent then [dest_slot] @ (list src_slot) else list src_slot) |
      Some p \<Rightarrow> list (
        src_slot := if src_parent then [dest_slot] @ (list src_slot) else list src_slot,
        p := if src_parent then list p else list_insert_after (list p) src_slot dest_slot))) src_parent src dest src_p dest_p e" apply (simp add: cap_insert_ext_def update_cdt_list_bind) apply (rule update_list_eq) apply (insert dest neq) apply (case_tac "m src") apply simp+ apply (frule no_mloop_weaken[where a=src]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; no_mloop m; src_p = m src; dest_p = m dest\<rbrakk> \<Longrightarrow> cap_insert_ext src_parent src dest src_p dest_p e = update_cdt_list (\<lambda>list. case m src of None \<Rightarrow> list(src := if src_parent then [dest] @ list src else list src) | Some p \<Rightarrow> list(src := if src_parent then [dest] @ list src else list src, p := if src_parent then list p else list_insert_after (list p) src dest)) e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; no_mloop 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))(src := if src_parent then dest # (case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest)) src else (case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest)) src) | Some p \<Rightarrow> (case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest))(src := if src_parent then dest # (case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest)) src else (case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest)) src, p := if src_parent \<and> p \<noteq> src then (case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest)) p else if src \<noteq> dest then list_insert_after ((case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest)) p) src dest else dest # (case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest)) p)) e = update_cdt_list (\<lambda>list. case m src of None \<Rightarrow> list(src := if src_parent then dest # list src else list src) | Some p \<Rightarrow> list(src := if src_parent then dest # list src else list src, p := if src_parent then list p else list_insert_after (list p) src dest)) e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; no_mloop 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))(src := if src_parent then dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src else (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src) | 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))(src := if src_parent then dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src else (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src, p := if src_parent \<and> p \<noteq> src then (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p else if src \<noteq> dest then list_insert_after ((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 else dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p)) = (case m src of None \<Rightarrow> (cdt_list e)(src := if src_parent then dest # cdt_list e src else cdt_list e src) | Some p \<Rightarrow> (cdt_list e)(src := if src_parent then dest # cdt_list e src else cdt_list e src, p := if src_parent then cdt_list e p else list_insert_after (cdt_list e p) src dest)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; no_mloop 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))(src := if src_parent then dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src else (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src) | 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))(src := if src_parent then dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src else (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src, p := if src_parent \<and> p \<noteq> src then (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p else if src \<noteq> dest then list_insert_after ((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 else dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p)) = (case m src of None \<Rightarrow> (cdt_list e)(src := if src_parent then dest # cdt_list e src else cdt_list e src) | Some p \<Rightarrow> (cdt_list e)(src := if src_parent then dest # cdt_list e src else cdt_list e src, p := if src_parent then cdt_list e p else list_insert_after (cdt_list e p) src dest)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; no_mloop 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))(src := if src_parent then dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src else (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src) | 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))(src := if src_parent then dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src else (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src, p := if src_parent \<and> p \<noteq> src then (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p else if src \<noteq> dest then list_insert_after ((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 else dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p)) = (case m src of None \<Rightarrow> (cdt_list e)(src := if src_parent then dest # cdt_list e src else cdt_list e src) | Some p \<Rightarrow> (cdt_list e)(src := if src_parent then dest # cdt_list e src else cdt_list e src, p := if src_parent then cdt_list e p else list_insert_after (cdt_list e p) src dest))
 2. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; no_mloop 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))(src := if src_parent then dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src else (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src) | 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))(src := if src_parent then dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src else (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) src, p := if src_parent \<and> p \<noteq> src then (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p else if src \<noteq> dest then list_insert_after ((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 else dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) p)) = (case m src of None \<Rightarrow> (cdt_list e)(src := if src_parent then dest # cdt_list e src else cdt_list e src) | Some p \<Rightarrow> (cdt_list e)(src := if src_parent then dest # cdt_list e src else cdt_list e src, p := if src_parent then cdt_list e p else list_insert_after (cdt_list e p) src dest)) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; no_mloop m; src_p = Some a; dest_p = None; m dest = None; src \<noteq> dest; m src = Some a\<rbrakk> \<Longrightarrow> a = src \<longrightarrow> src_parent \<longrightarrow> (cdt_list e)(src := list_insert_after (cdt_list e src) src dest) = cdt_list e proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; no_mloop m; src_p = Some a; dest_p = None; m dest = None; src \<noteq> dest; m src = Some a; m src \<noteq> Some src\<rbrakk> \<Longrightarrow> a = src \<longrightarrow> src_parent \<longrightarrow> (cdt_list e)(src := list_insert_after (cdt_list e src) src dest) = cdt_list e proof (prove)
goal:
No subgoals!