# HG changeset patch
# User Andreas Lochbihler
# Date 1338304901 -7200
# Node ID ba9e0f5b686d64d9075a7b8860799eaa42b49667
# Parent  bbf95f3595abcdf10f4393c52cb05277a67ffb91
add code equation for coset xs = set ys

diff -r bbf95f3595ab -r ba9e0f5b686d src/HOL/Library/Card_Univ.thy
--- a/src/HOL/Library/Card_Univ.thy	Tue May 29 17:17:57 2012 +0200
+++ b/src/HOL/Library/Card_Univ.thy	Tue May 29 17:21:41 2012 +0200
@@ -60,6 +60,33 @@
 
 end
 
+lemma card_Compl:
+  "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
+by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
+
+lemma eq_coset_set_code [code]:
+  fixes xs ys :: "'a :: card_UNIV list"
+  defines "rhs \<equiv> 
+  let n = card_UNIV TYPE('a)
+  in if n = 0 then False else 
+        let xs' = remdups xs; ys' = remdups ys 
+        in length xs' + length ys' = n \<and> list_all (\<lambda>y. \<not> List.member ys' y) xs' \<and> list_all (\<lambda>x. \<not> List.member xs' x) ys'"
+  shows "HOL.eq (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
+  and "HOL.eq (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
+proof -
+  show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
+  proof
+    assume ?lhs thus ?rhs
+      by(auto simp add: rhs_def Let_def List.member_def list_all_iff card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
+  next
+    assume ?rhs
+    moreover have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
+    ultimately show ?lhs
+      by(auto simp add: rhs_def Let_def List.member_def list_all_iff card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
+  qed
+  thus ?thesis2 by blast
+qed
+
 subsection {* Instantiations for @{text "card_UNIV"} *}
 
 subsubsection {* @{typ "nat"} *}