theory Deterministic_AC

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>list_integ P st and K (P src) and K (P dest)\<rbrace> cap_move_ext 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 src) 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));
if src = dest then return () else do y <- update_cdt_list (\<lambda>list. case src_p of None \<Rightarrow> list | Some p \<Rightarrow> list(p := list_replace (list p) src dest));
update_cdt_list (\<lambda>list. list(src := [], dest := list src @ list dest))
od
od \<lbrace>\<lambda>_. list_integ P st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (list_integ P st and (\<lambda>y. P src) and (\<lambda>y. P dest)) s \<Longrightarrow> (src = dest \<longrightarrow> list_integ P st (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)) \<and> (src \<noteq> dest \<longrightarrow> list_integ P st (cdt_list_update (\<lambda>_. (cdt_list (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) | 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))(p := list_replace (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)) (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 := [], dest := cdt_list (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) | 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))(p := list_replace (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)) (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 @ cdt_list (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) | 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))(p := list_replace (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)) (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)) dest)) (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) | 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))(p := list_replace (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)) (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)))) proof (prove)
goal:
No subgoals!