equal
deleted
inserted
replaced
50 |
50 |
51 subsection {* Cardinalities of types *} |
51 subsection {* Cardinalities of types *} |
52 |
52 |
53 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") |
53 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") |
54 |
54 |
55 translations "CARD(t)" => "card (UNIV::t set)" |
55 translations "CARD(t)" => "CONST card (UNIV \<Colon> t set)" |
56 |
56 |
57 typed_print_translation {* |
57 typed_print_translation {* |
58 let |
58 let |
59 fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T]))] = |
59 fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T]))] = |
60 Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T; |
60 Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T; |
237 instance bit1 :: (finite) card2 |
237 instance bit1 :: (finite) card2 |
238 by intro_classes (simp add: one_le_card_finite) |
238 by intro_classes (simp add: one_le_card_finite) |
239 |
239 |
240 subsection {* Examples *} |
240 subsection {* Examples *} |
241 |
241 |
242 term "TYPE(10)" |
|
243 |
|
244 lemma "CARD(0) = 0" by simp |
242 lemma "CARD(0) = 0" by simp |
245 lemma "CARD(17) = 17" by simp |
243 lemma "CARD(17) = 17" by simp |
246 |
244 |
247 end |
245 end |