# HG changeset patch
# User Andreas Lochbihler
# Date 1338576034 -7200
# Node ID 9014e78ccde2fd0bf89281ac21145130dd168a5c
# Parent  3437685f69fbc0040602520dfc032e0a82858fef
improved code setup for card, finite, subset

diff -r 3437685f69fb -r 9014e78ccde2 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Fri Jun 01 15:35:49 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy	Fri Jun 01 20:40:34 2012 +0200
@@ -204,7 +204,6 @@
 instance by intro_classes (simp add: card_UNIV_int_def infinite_UNIV_int)
 end
 
-print_classes
 instantiation list :: (type) card_UNIV begin
 definition "card_UNIV = (\<lambda>a :: 'a list itself. 0)"
 instance by intro_classes (simp add: card_UNIV_list_def infinite_UNIV_listI)
@@ -303,19 +302,49 @@
 instance by intro_classes (simp add: UNIV_finite_5 card_UNIV_finite_5_def)
 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]
+subsection {* Code setup for sets *}
 
 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)
 
+context fixes xs :: "'a :: card_UNIV list"
+begin
+
+definition card' :: "'a set \<Rightarrow> nat" 
+where [simp, code del, code_abbrev]: "card' = card"
+
+lemma card'_code [code]:
+  "card' (set xs) = length (remdups xs)"
+  "card' (List.coset xs) =  card_UNIV TYPE('a) - length (remdups xs)"
+by(simp_all add: List.card_set card_Compl card_UNIV)
+
+lemma card'_UNIV [code_unfold]: "card' (UNIV :: 'a :: card_UNIV set) = card_UNIV TYPE('a)"
+by(simp add: card_UNIV)
+
+definition finite' :: "'a set \<Rightarrow> bool"
+where [simp, code del, code_abbrev]: "finite' = finite"
+
+lemma finite'_code [code]:
+  "finite' (set xs) \<longleftrightarrow> True"
+  "finite' (List.coset xs) \<longleftrightarrow> CARD('a) > 0"
+by(simp_all add: card_gt_0_iff)
+
+definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+where [simp, code del, code_abbrev]: "subset' = op \<subseteq>"
+
+lemma subset'_code [code]:
+  "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)"
+  "subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)"
+  "subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)"
+by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
+  (metis finite_compl finite_set rev_finite_subset)
+
+definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+where [simp, code del, code_abbrev]: "eq_set = op ="
+
 lemma eq_set_code [code]:
-  fixes xs ys :: "'a :: card_UNIV list"
+  fixes ys
   defines "rhs \<equiv> 
   let n = CARD('a)
   in if n = 0 then False else 
@@ -340,7 +369,13 @@
   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
+
+notepad begin (* test code setup *)
+have "List.coset [True] = set [False] \<and> List.coset [] \<subseteq> List.set [True, False] \<and> finite (List.coset [True])"
+  by eval
+end
+
+hide_const (open) card' finite' subset' eq_set
 
 end