theory Monad_Lists

lemma filterM_distinct1:
  "\<lbrace>\<top> and K (P \<longrightarrow> distinct xs)\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. (P \<longrightarrow> distinct rv) \<and> set rv \<subseteq> set xs\<rbrace>" apply (rule hoare_gen_asm, erule rev_mp) apply (rule rev_induct [where xs=xs]) apply (clarsimp | wp)+ apply (simp add: filterM_append) apply (erule hoare_seq_ext[rotated]) apply (rule hoare_seq_ext[rotated], rule hoare_vcg_prop) apply (wp, clarsimp) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>_. True) and K (P \<longrightarrow> distinct xs)\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. (P \<longrightarrow> distinct rv) \<and> set rv \<subseteq> set xs\<rbrace> proof (prove)
goal (1 subgoal):
 1. (P \<longrightarrow> distinct xs) \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. (P \<longrightarrow> distinct rv) \<and> set rv \<subseteq> set xs\<rbrace> proof (prove)
goal (2 subgoals):
 1. (P \<longrightarrow> distinct []) \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> filterM m [] \<lbrace>\<lambda>rv s. (P \<longrightarrow> distinct rv) \<and> set rv \<subseteq> set []\<rbrace>
 2. \<And>x xs. (P \<longrightarrow> distinct xs) \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. (P \<longrightarrow> distinct rv) \<and> set rv \<subseteq> set xs\<rbrace> \<Longrightarrow> (P \<longrightarrow> distinct (xs @ [x])) \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> filterM m (xs @ [x]) \<lbrace>\<lambda>rv s. (P \<longrightarrow> distinct rv) \<and> set rv \<subseteq> set (xs @ [x])\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. (P \<longrightarrow> distinct rv) \<and> set rv \<subseteq> set xs\<rbrace>; P \<longrightarrow> distinct xs \<and> x \<notin> set xs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> filterM m (xs @ [x]) \<lbrace>\<lambda>rv s. (P \<longrightarrow> distinct rv) \<and> set rv \<subseteq> insert x (set xs)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrace>\<lambda>_. True\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. (P \<longrightarrow> distinct rv) \<and> set rv \<subseteq> set xs\<rbrace>; P \<longrightarrow> distinct xs \<and> x \<notin> set xs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do xs' <- filterM m xs;
b <- m x;
return (xs' @ (if b then [x] else []))
od \<lbrace>\<lambda>rv s. (P \<longrightarrow> distinct rv) \<and> set rv \<subseteq> insert x (set xs)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. P \<longrightarrow> distinct xs \<and> x \<notin> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> distinct xa) \<and> set xa \<subseteq> set xs\<rbrace> do b <- m x;
return (xa @ (if b then [x] else []))
od \<lbrace>\<lambda>rv s. (P \<longrightarrow> distinct rv) \<and> set rv \<subseteq> insert x (set xs)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa b. P \<longrightarrow> distinct xs \<and> x \<notin> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> distinct xa) \<and> set xa \<subseteq> set xs\<rbrace> return (xa @ (if b then [x] else [])) \<lbrace>\<lambda>rv s. (P \<longrightarrow> distinct rv) \<and> set rv \<subseteq> insert x (set xs)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa b. \<lbrakk>P \<longrightarrow> distinct xs \<and> x \<notin> set xs; P \<longrightarrow> distinct xa; set xa \<subseteq> set xs\<rbrakk> \<Longrightarrow> (b \<longrightarrow> (P \<longrightarrow> x \<notin> set xa) \<and> set xa \<subseteq> insert x (set xs)) \<and> (\<not> b \<longrightarrow> set xa \<subseteq> insert x (set xs)) proof (prove)
goal:
No subgoals!