theory Deterministic_AC

lemma cap_swap_list_integrity:
  notes split_paired_All[simp del]
  shows
  "\<lbrace>list_integ P st and K(P slot1) and K(P slot2)\<rbrace> cap_swap_ext slot1 slot2 slot1_p slot2_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>" apply (simp add: cap_swap_ext_def split del: if_split) apply (wp update_cdt_list_wp) by (intro impI conjI allI |
      simp add: list_filter_replace list_filter_swap 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 slot1) and K (P slot2)\<rbrace> cap_swap_ext slot1 slot2 slot1_p slot2_p \<lbrace>\<lambda>_. list_integ P st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>list_integ P st and (\<lambda>y. P slot1) and (\<lambda>y. P slot2)\<rbrace> do y <- update_cdt_list (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1));
update_cdt_list (\<lambda>list. case if slot2_p = Some slot1 then Some slot2 else if slot2_p = Some slot2 then Some slot1 else slot2_p of None \<Rightarrow> case if slot1_p = Some slot1 then Some slot2 else if slot1_p = Some slot2 then Some slot1 else slot1_p of None \<Rightarrow> list | Some slot2_p \<Rightarrow> list(slot2_p := list_replace (list slot2_p) slot1 slot2) | Some slot1_pa \<Rightarrow> case if slot1_p = Some slot1 then Some slot2 else if slot1_p = Some slot2 then Some slot1 else slot1_p of None \<Rightarrow> list(slot1_pa := list_replace (list slot1_pa) slot2 slot1) | Some slot2_p \<Rightarrow> if slot1_pa = slot2_p then list(slot2_p := list_swap (list slot2_p) slot1 slot2) else list(slot1_pa := list_replace (list slot1_pa) slot2 slot1, slot2_p := list_replace (list slot2_p) slot1 slot2))
od \<lbrace>\<lambda>_. list_integ P st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (list_integ P st and (\<lambda>y. P slot1) and (\<lambda>y. P slot2)) s \<Longrightarrow> list_integ P st (cdt_list_update (\<lambda>_. case if slot2_p = Some slot1 then Some slot2 else if slot2_p = Some slot2 then Some slot1 else slot2_p of None \<Rightarrow> case if slot1_p = Some slot1 then Some slot2 else if slot1_p = Some slot2 then Some slot1 else slot1_p of None \<Rightarrow> cdt_list (cdt_list_update (\<lambda>_. (cdt_list s)(slot1 := cdt_list s slot2, slot2 := cdt_list s slot1)) s) | Some slot2_p \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list s)(slot1 := cdt_list s slot2, slot2 := cdt_list s slot1)) s))(slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list s)(slot1 := cdt_list s slot2, slot2 := cdt_list s slot1)) s) slot2_p) slot1 slot2) | Some slot1_pa \<Rightarrow> case if slot1_p = Some slot1 then Some slot2 else if slot1_p = Some slot2 then Some slot1 else slot1_p of None \<Rightarrow> (cdt_list (cdt_list_update (\<lambda>_. (cdt_list s)(slot1 := cdt_list s slot2, slot2 := cdt_list s slot1)) s))(slot1_pa := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list s)(slot1 := cdt_list s slot2, slot2 := cdt_list s slot1)) s) slot1_pa) slot2 slot1) | Some slot2_p \<Rightarrow> if slot1_pa = slot2_p then (cdt_list (cdt_list_update (\<lambda>_. (cdt_list s)(slot1 := cdt_list s slot2, slot2 := cdt_list s slot1)) s))(slot2_p := list_swap (cdt_list (cdt_list_update (\<lambda>_. (cdt_list s)(slot1 := cdt_list s slot2, slot2 := cdt_list s slot1)) s) slot2_p) slot1 slot2) else (cdt_list (cdt_list_update (\<lambda>_. (cdt_list s)(slot1 := cdt_list s slot2, slot2 := cdt_list s slot1)) s))(slot1_pa := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list s)(slot1 := cdt_list s slot2, slot2 := cdt_list s slot1)) s) slot1_pa) slot2 slot1, slot2_p := list_replace (cdt_list (cdt_list_update (\<lambda>_. (cdt_list s)(slot1 := cdt_list s slot2, slot2 := cdt_list s slot1)) s) slot2_p) slot1 slot2)) (cdt_list_update (\<lambda>_. (cdt_list s)(slot1 := cdt_list s slot2, slot2 := cdt_list s slot1)) s))