theory Deterministic_AC

lemma empty_slot_list_integrity:
  notes split_paired_All[simp del]
  shows
  "\<lbrace>list_integ P st and (\<lambda>s. valid_list_2 (cdt_list s) m) and K(P slot) and K( all_children P m)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>" apply (simp add: empty_slot_ext_def split del: if_split) apply (wp update_cdt_list_wp) apply (intro impI conjI allI | simp add: list_filter_replace_list list_filter_remove split: option.splits | elim conjE  | simp add: list_integ_def)+ apply (drule_tac x="the slot_p" in spec) apply (elim disjE) apply (simp add: all_children_def valid_list_2_def list_filter_replace_list)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>list_integ P st and (\<lambda>s. valid_list_2 (cdt_list s) m) and K (P slot) and K (all_children P m)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>_. list_integ P st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>list_integ P st and (\<lambda>s. valid_list_2 (cdt_list s) m) and (\<lambda>y. P slot) and (\<lambda>y. all_children P m)\<rbrace> update_cdt_list (\<lambda>list. case slot_p 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 := [])) \<lbrace>\<lambda>_. list_integ P st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (list_integ P st and (\<lambda>s. valid_list_2 (cdt_list s) m) and (\<lambda>y. P slot) and (\<lambda>y. all_children P m)) s \<Longrightarrow> list_integ P st (cdt_list_update (\<lambda>_. case slot_p of None \<Rightarrow> (cdt_list s)(slot := []) | Some p \<Rightarrow> if p = slot then (cdt_list s)(slot := list_remove (cdt_list s slot) slot) else (cdt_list s)(p := list_replace_list (cdt_list s p) slot (cdt_list s slot), slot := [])) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>x2 \<noteq> slot; slot_p = Some x2; \<forall>x. P x \<or> filtered_eq P (cdt_list st x) (cdt_list s x); valid_list_2 (cdt_list s) m; P slot; all_children P m\<rbrakk> \<Longrightarrow> P x2 \<or> filtered_eq P (cdt_list st x2) (list_replace_list (cdt_list s x2) slot (cdt_list s slot)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>x2 \<noteq> slot; slot_p = Some x2; valid_list_2 (cdt_list s) m; P slot; all_children P m; P (the slot_p) \<or> filtered_eq P (cdt_list st (the slot_p)) (cdt_list s (the slot_p))\<rbrakk> \<Longrightarrow> P x2 \<or> filtered_eq P (cdt_list st x2) (list_replace_list (cdt_list s x2) slot (cdt_list s slot)) proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>x2 \<noteq> slot; slot_p = Some x2; valid_list_2 (cdt_list s) m; P slot; all_children P m; P (the slot_p)\<rbrakk> \<Longrightarrow> P x2 \<or> filtered_eq P (cdt_list st x2) (list_replace_list (cdt_list s x2) slot (cdt_list s slot))
 2. \<And>s x2. \<lbrakk>x2 \<noteq> slot; slot_p = Some x2; valid_list_2 (cdt_list s) m; P slot; all_children P m; filtered_eq P (cdt_list st (the slot_p)) (cdt_list s (the slot_p))\<rbrakk> \<Longrightarrow> P x2 \<or> filtered_eq P (cdt_list st x2) (list_replace_list (cdt_list s x2) slot (cdt_list s slot)) proof (prove)
goal:
No subgoals!