typed print translation for CARD('a);
authorhuffman
Wed Aug 22 20:59:19 2007 +0200 (2007-08-22)
changeset 2440761b10ffb2549
parent 24406 d96eb21fc1bc
child 24408 058c5613a86f
typed print translation for CARD('a);
declare zero_less_card_finite [simp]
src/HOL/Library/Numeral_Type.thy
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Wed Aug 22 18:53:54 2007 +0200
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Aug 22 20:59:19 2007 +0200
     1.3 @@ -54,6 +54,14 @@
     1.4  
     1.5  translations "CARD(t)" => "card (UNIV::t set)"
     1.6  
     1.7 +typed_print_translation {*
     1.8 +let
     1.9 +  fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T]))] =
    1.10 +    Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
    1.11 +in [("card", card_univ_tr')]
    1.12 +end
    1.13 +*}
    1.14 +
    1.15  lemma card_unit: "CARD(unit) = 1"
    1.16    unfolding univ_unit by simp
    1.17  
    1.18 @@ -200,7 +208,7 @@
    1.19  
    1.20  text {* Class finite already captures "at least 1" *}
    1.21  
    1.22 -lemma zero_less_card_finite:
    1.23 +lemma zero_less_card_finite [simp]:
    1.24    "0 < CARD('a::finite)"
    1.25  proof (cases "CARD('a::finite) = 0")
    1.26    case False thus ?thesis by (simp del: card_0_eq)
    1.27 @@ -209,7 +217,7 @@
    1.28    thus ?thesis by (simp add: finite)
    1.29  qed
    1.30  
    1.31 -lemma one_le_card_finite:
    1.32 +lemma one_le_card_finite [simp]:
    1.33    "Suc 0 <= CARD('a::finite)"
    1.34    by (simp add: less_Suc_eq_le [symmetric] zero_less_card_finite)
    1.35