theory Deterministic_AC

lemma cap_insert_list_integrity:
  notes split_paired_All[simp del]
  shows
  "\<lbrace>list_integ P st and K(P dest)\<rbrace> cap_insert_ext src_parent src dest src_p dest_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>" apply (simp add: cap_insert_ext_def split del: if_split) apply (wp update_cdt_list_wp) by (intro impI conjI allI |
      simp add: list_filter_insert_after list_filter_remove split: option.splits |
      elim conjE | simp add: list_integ_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>list_integ P st and K (P dest)\<rbrace> cap_insert_ext src_parent src dest src_p dest_p \<lbrace>\<lambda>_. list_integ P st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>list_integ P st and (\<lambda>y. P dest)\<rbrace> do y <- update_cdt_list (\<lambda>list. case dest_p of None \<Rightarrow> list | Some p \<Rightarrow> list(p := list_remove (list p) dest));
update_cdt_list (\<lambda>list. case src_p 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 \<and> p \<noteq> src then list p else if src \<noteq> dest then list_insert_after (list p) src dest else dest # list p))
od \<lbrace>\<lambda>_. list_integ P st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (list_integ P st and (\<lambda>y. P dest)) s \<Longrightarrow> list_integ P st (cdt_list_update (\<lambda>_. case src_p of None \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) s))(src := if src_parent then dest # cdt_list (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) s) src else cdt_list (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) s) src) | Some p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) s))(src := if src_parent then dest # cdt_list (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) s) src else cdt_list (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) s) src, p := if src_parent \<and> p \<noteq> src then cdt_list (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) s) p else if src \<noteq> dest then list_insert_after (cdt_list (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) s) p) src dest else dest # cdt_list (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) s) p)) (cdt_list_update (\<lambda>_. case dest_p of None \<Rightarrow> cdt_list s | Some p \<Rightarrow> (cdt_list s)(p := list_remove (cdt_list s p) dest)) s))