# HG changeset patch
# User Andreas Lochbihler
# Date 1338359654 -7200
# Node ID 65eb8910a7797a33f51e8ae24570536f9cba68f0
# Parent  ba9e0f5b686d64d9075a7b8860799eaa42b49667
improve code setup for set equality

diff -r ba9e0f5b686d -r 65eb8910a779 src/HOL/Library/Card_Univ.thy
--- a/src/HOL/Library/Card_Univ.thy	Tue May 29 17:21:41 2012 +0200
+++ b/src/HOL/Library/Card_Univ.thy	Wed May 30 08:34:14 2012 +0200
@@ -60,33 +60,6 @@
 
 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"} *}
@@ -317,4 +290,44 @@
 
 end
 
+subsection {* Code setup for equality on sets *}
+
+definition eq_set :: "'a :: card_UNIV set \<Rightarrow> 'a :: card_UNIV set \<Rightarrow> bool"
+where [simp, code del]: "eq_set = op ="
+
+lemmas [code_unfold] = eq_set_def[symmetric]
+
+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_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> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')"
+  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
+  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
+  and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis3)
+  and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis4)
+proof -
+  show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
+  proof
+    assume ?lhs thus ?rhs
+      by(auto simp add: rhs_def Let_def 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  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 unfolding eq_set_def by blast
+  show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
+qed
+
+(* test code setup *)
+value [code] "List.coset [True] = set [False] \<and> set [] = List.coset [True, False]"
+
 end
\ No newline at end of file