src/HOL/Library/Cardinality.thy
changeset 48070 02d64fd40852
parent 48067 9f458b3efb5c
child 48164 e97369f20c30
     1.1 --- a/src/HOL/Library/Cardinality.thy	Sun Jun 03 15:49:55 2012 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Mon Jun 04 09:50:57 2012 +0200
     1.3 @@ -170,9 +170,7 @@
     1.4  subsection {* A type class for computing the cardinality of types *}
     1.5  
     1.6  definition is_list_UNIV :: "'a list \<Rightarrow> bool"
     1.7 -where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
     1.8 -
     1.9 -lemmas [code_unfold] = is_list_UNIV_def[abs_def]
    1.10 +where [code del]: "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
    1.11  
    1.12  lemma is_list_UNIV_iff: "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
    1.13  by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] 
    1.14 @@ -185,6 +183,11 @@
    1.15  lemma card_UNIV_code [code_unfold]: "CARD('a :: card_UNIV) = card_UNIV TYPE('a)"
    1.16  by(simp add: card_UNIV)
    1.17  
    1.18 +lemma is_list_UNIV_code [code]:
    1.19 +  "is_list_UNIV (xs :: 'a list) = 
    1.20 +  (let c = CARD('a :: card_UNIV) in if c = 0 then False else size (remdups xs) = c)"
    1.21 +by(rule is_list_UNIV_def)
    1.22 +
    1.23  lemma finite_UNIV_conv_card_UNIV [code_unfold]:
    1.24    "finite (UNIV :: 'a :: card_UNIV set) \<longleftrightarrow> card_UNIV TYPE('a) > 0"
    1.25  by(simp add: card_UNIV card_gt_0_iff)