src/HOL/Library/Cardinality.thy
changeset 48062 9014e78ccde2
parent 48060 1f4d00a7f59f
child 48067 9f458b3efb5c
     1.1 --- a/src/HOL/Library/Cardinality.thy	Fri Jun 01 15:35:49 2012 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Fri Jun 01 20:40:34 2012 +0200
     1.3 @@ -204,7 +204,6 @@
     1.4  instance by intro_classes (simp add: card_UNIV_int_def infinite_UNIV_int)
     1.5  end
     1.6  
     1.7 -print_classes
     1.8  instantiation list :: (type) card_UNIV begin
     1.9  definition "card_UNIV = (\<lambda>a :: 'a list itself. 0)"
    1.10  instance by intro_classes (simp add: card_UNIV_list_def infinite_UNIV_listI)
    1.11 @@ -303,19 +302,49 @@
    1.12  instance by intro_classes (simp add: UNIV_finite_5 card_UNIV_finite_5_def)
    1.13  end
    1.14  
    1.15 -subsection {* Code setup for equality on sets *}
    1.16 -
    1.17 -definition eq_set :: "'a :: card_UNIV set \<Rightarrow> 'a :: card_UNIV set \<Rightarrow> bool"
    1.18 -where [simp, code del]: "eq_set = op ="
    1.19 -
    1.20 -lemmas [code_unfold] = eq_set_def[symmetric]
    1.21 +subsection {* Code setup for sets *}
    1.22  
    1.23  lemma card_Compl:
    1.24    "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
    1.25  by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
    1.26  
    1.27 +context fixes xs :: "'a :: card_UNIV list"
    1.28 +begin
    1.29 +
    1.30 +definition card' :: "'a set \<Rightarrow> nat" 
    1.31 +where [simp, code del, code_abbrev]: "card' = card"
    1.32 +
    1.33 +lemma card'_code [code]:
    1.34 +  "card' (set xs) = length (remdups xs)"
    1.35 +  "card' (List.coset xs) =  card_UNIV TYPE('a) - length (remdups xs)"
    1.36 +by(simp_all add: List.card_set card_Compl card_UNIV)
    1.37 +
    1.38 +lemma card'_UNIV [code_unfold]: "card' (UNIV :: 'a :: card_UNIV set) = card_UNIV TYPE('a)"
    1.39 +by(simp add: card_UNIV)
    1.40 +
    1.41 +definition finite' :: "'a set \<Rightarrow> bool"
    1.42 +where [simp, code del, code_abbrev]: "finite' = finite"
    1.43 +
    1.44 +lemma finite'_code [code]:
    1.45 +  "finite' (set xs) \<longleftrightarrow> True"
    1.46 +  "finite' (List.coset xs) \<longleftrightarrow> CARD('a) > 0"
    1.47 +by(simp_all add: card_gt_0_iff)
    1.48 +
    1.49 +definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    1.50 +where [simp, code del, code_abbrev]: "subset' = op \<subseteq>"
    1.51 +
    1.52 +lemma subset'_code [code]:
    1.53 +  "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)"
    1.54 +  "subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)"
    1.55 +  "subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)"
    1.56 +by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
    1.57 +  (metis finite_compl finite_set rev_finite_subset)
    1.58 +
    1.59 +definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    1.60 +where [simp, code del, code_abbrev]: "eq_set = op ="
    1.61 +
    1.62  lemma eq_set_code [code]:
    1.63 -  fixes xs ys :: "'a :: card_UNIV list"
    1.64 +  fixes ys
    1.65    defines "rhs \<equiv> 
    1.66    let n = CARD('a)
    1.67    in if n = 0 then False else 
    1.68 @@ -340,7 +369,13 @@
    1.69    show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
    1.70  qed
    1.71  
    1.72 -(* test code setup *)
    1.73 -value [code] "List.coset [True] = set [False] \<and> set [] = List.coset [True, False]"
    1.74 +end
    1.75 +
    1.76 +notepad begin (* test code setup *)
    1.77 +have "List.coset [True] = set [False] \<and> List.coset [] \<subseteq> List.set [True, False] \<and> finite (List.coset [True])"
    1.78 +  by eval
    1.79 +end
    1.80 +
    1.81 +hide_const (open) card' finite' subset' eq_set
    1.82  
    1.83  end