deleted card definition as code lemma; authentic syntax for card
authorhaftmann
Fri Nov 23 21:09:32 2007 +0100 (2007-11-23)
changeset 25459d1dce7d0731c
parent 25458 ba8f5e4fa336
child 25460 b80087af2274
deleted card definition as code lemma; authentic syntax for card
NEWS
src/HOL/Finite_Set.thy
src/HOL/Library/Numeral_Type.thy
     1.1 --- a/NEWS	Fri Nov 23 21:09:30 2007 +0100
     1.2 +++ b/NEWS	Fri Nov 23 21:09:32 2007 +0100
     1.3 @@ -548,6 +548,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Constant "card" now with authentic syntax.
     1.8 +
     1.9  * Method "metis" proves goals by applying the Metis general-purpose
    1.10  resolution prover (see also http://gilith.com/software/metis/).
    1.11  Examples are in the directory MetisExamples.  WARNING: the
     2.1 --- a/src/HOL/Finite_Set.thy	Fri Nov 23 21:09:30 2007 +0100
     2.2 +++ b/src/HOL/Finite_Set.thy	Fri Nov 23 21:09:32 2007 +0100
     2.3 @@ -1500,9 +1500,10 @@
     2.4  But now that we have @{text setsum} things are easy:
     2.5  *}
     2.6  
     2.7 -constdefs
     2.8 -  card :: "'a set => nat"
     2.9 -  "card A == setsum (%x. 1::nat) A"
    2.10 +definition
    2.11 +  card :: "'a set \<Rightarrow> nat"
    2.12 +where
    2.13 +  [code func del]: "card A = setsum (\<lambda>x. 1) A"
    2.14  
    2.15  lemma card_empty [simp]: "card {} = 0"
    2.16  by (simp add: card_def)
     3.1 --- a/src/HOL/Library/Numeral_Type.thy	Fri Nov 23 21:09:30 2007 +0100
     3.2 +++ b/src/HOL/Library/Numeral_Type.thy	Fri Nov 23 21:09:32 2007 +0100
     3.3 @@ -52,7 +52,7 @@
     3.4  
     3.5  syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
     3.6  
     3.7 -translations "CARD(t)" => "card (UNIV::t set)"
     3.8 +translations "CARD(t)" => "CONST card (UNIV \<Colon> t set)"
     3.9  
    3.10  typed_print_translation {*
    3.11  let
    3.12 @@ -239,8 +239,6 @@
    3.13  
    3.14  subsection {* Examples *}
    3.15  
    3.16 -term "TYPE(10)"
    3.17 -
    3.18  lemma "CARD(0) = 0" by simp
    3.19  lemma "CARD(17) = 17" by simp
    3.20