theory Deterministic_AI

lemma (in mdb_empty_abs') empty_slot_ext_det_def2:
 notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
 "valid_list_2 (cdt_list e) m \<Longrightarrow> slot_p = (m slot) \<Longrightarrow>
       empty_slot_ext slot slot_p e = (
    update_cdt_list (\<lambda>list. case (m slot) of None \<Rightarrow> list (slot := []) |
      Some p \<Rightarrow> list (p := list_replace_list (list p) slot (list slot), slot := []))) e" apply (simp add: empty_slot_ext_def update_cdt_list_bind) apply (rule update_list_eq) apply (case_tac "m slot") apply simp apply (cut_tac no_mloop_weaken[OF no_mloop, where a=slot]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; slot_p = m slot\<rbrakk> \<Longrightarrow> empty_slot_ext slot slot_p e = update_cdt_list (\<lambda>list. case m slot of None \<Rightarrow> list(slot := []) | Some p \<Rightarrow> list(p := list_replace_list (list p) slot (list slot), slot := [])) e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; slot_p = m slot\<rbrakk> \<Longrightarrow> update_cdt_list (\<lambda>list. case m slot of None \<Rightarrow> list(slot := []) | Some p \<Rightarrow> if p = slot then list(slot := list_remove (list slot) slot) else list(p := list_replace_list (list p) slot (list slot), slot := [])) e = update_cdt_list (\<lambda>list. case m slot of None \<Rightarrow> list(slot := []) | Some p \<Rightarrow> list(p := list_replace_list (list p) slot (list slot), slot := [])) e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; slot_p = m slot\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> (cdt_list e)(slot := []) | Some p \<Rightarrow> if p = slot then (cdt_list e)(slot := list_remove (cdt_list e slot) slot) else (cdt_list e)(p := list_replace_list (cdt_list e p) slot (cdt_list e slot), slot := [])) = (case m slot of None \<Rightarrow> (cdt_list e)(slot := []) | Some p \<Rightarrow> (cdt_list e)(p := list_replace_list (cdt_list e p) slot (cdt_list e slot), slot := [])) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; slot_p = m slot; m slot = None\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> (cdt_list e)(slot := []) | Some p \<Rightarrow> if p = slot then (cdt_list e)(slot := list_remove (cdt_list e slot) slot) else (cdt_list e)(p := list_replace_list (cdt_list e p) slot (cdt_list e slot), slot := [])) = (case m slot of None \<Rightarrow> (cdt_list e)(slot := []) | Some p \<Rightarrow> (cdt_list e)(p := list_replace_list (cdt_list e p) slot (cdt_list e slot), slot := []))
 2. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; slot_p = m slot; m slot = Some a\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> (cdt_list e)(slot := []) | Some p \<Rightarrow> if p = slot then (cdt_list e)(slot := list_remove (cdt_list e slot) slot) else (cdt_list e)(p := list_replace_list (cdt_list e p) slot (cdt_list e slot), slot := [])) = (case m slot of None \<Rightarrow> (cdt_list e)(slot := []) | Some p \<Rightarrow> (cdt_list e)(p := list_replace_list (cdt_list e p) slot (cdt_list e slot), slot := [])) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; slot_p = m slot; m slot = Some a\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> (cdt_list e)(slot := []) | Some p \<Rightarrow> if p = slot then (cdt_list e)(slot := list_remove (cdt_list e slot) slot) else (cdt_list e)(p := list_replace_list (cdt_list e p) slot (cdt_list e slot), slot := [])) = (case m slot of None \<Rightarrow> (cdt_list e)(slot := []) | Some p \<Rightarrow> (cdt_list e)(p := list_replace_list (cdt_list e p) slot (cdt_list e slot), slot := [])) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; slot_p = m slot; m slot = Some a; m slot \<noteq> Some slot\<rbrakk> \<Longrightarrow> (case m slot of None \<Rightarrow> (cdt_list e)(slot := []) | Some p \<Rightarrow> if p = slot then (cdt_list e)(slot := list_remove (cdt_list e slot) slot) else (cdt_list e)(p := list_replace_list (cdt_list e p) slot (cdt_list e slot), slot := [])) = (case m slot of None \<Rightarrow> (cdt_list e)(slot := []) | Some p \<Rightarrow> (cdt_list e)(p := list_replace_list (cdt_list e p) slot (cdt_list e slot), slot := [])) proof (prove)
goal:
No subgoals!