tuned instantiations
authorAndreas Lochbihler
Thu May 31 17:04:11 2012 +0200 (2012-05-31)
changeset 48052b74766e4c11e
parent 48051 53a0df441e20
child 48053 9bc78a08ff0a
tuned instantiations
dropped redundant lemmas
src/HOL/Library/Cardinality.thy
     1.1 --- a/src/HOL/Library/Cardinality.thy	Thu May 31 16:58:38 2012 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Thu May 31 17:04:11 2012 +0200
     1.3 @@ -161,7 +161,7 @@
     1.4  
     1.5  instantiation int :: card_UNIV begin
     1.6  
     1.7 -definition "card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)"
     1.8 +definition "card_UNIV = (\<lambda>a :: int itself. 0)"
     1.9  
    1.10  instance proof
    1.11    fix x :: "int itself"
    1.12 @@ -175,7 +175,7 @@
    1.13  
    1.14  instantiation list :: (type) card_UNIV begin
    1.15  
    1.16 -definition "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)"
    1.17 +definition "card_UNIV = (\<lambda>a :: 'a list itself. 0)"
    1.18  
    1.19  instance proof
    1.20    fix x :: "'a list itself"
    1.21 @@ -187,13 +187,9 @@
    1.22  
    1.23  subsubsection {* @{typ "unit"} *}
    1.24  
    1.25 -lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
    1.26 -  unfolding UNIV_unit by simp
    1.27 -
    1.28  instantiation unit :: card_UNIV begin
    1.29  
    1.30 -definition card_UNIV_unit_def: 
    1.31 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)"
    1.32 +definition "card_UNIV = (\<lambda>a :: unit itself. 1)"
    1.33  
    1.34  instance proof
    1.35    fix x :: "unit itself"
    1.36 @@ -205,13 +201,9 @@
    1.37  
    1.38  subsubsection {* @{typ "bool"} *}
    1.39  
    1.40 -lemma card_UNIV_bool: "card (UNIV :: bool set) = 2"
    1.41 -  unfolding UNIV_bool by simp
    1.42 -
    1.43  instantiation bool :: card_UNIV begin
    1.44  
    1.45 -definition card_UNIV_bool_def: 
    1.46 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)"
    1.47 +definition "card_UNIV = (\<lambda>a :: bool itself. 2)"
    1.48  
    1.49  instance proof
    1.50    fix x :: "bool itself"
    1.51 @@ -235,8 +227,7 @@
    1.52  
    1.53  instantiation char :: card_UNIV begin
    1.54  
    1.55 -definition card_UNIV_char_def: 
    1.56 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
    1.57 +definition "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
    1.58  
    1.59  instance proof
    1.60    fix x :: "char itself"
    1.61 @@ -250,13 +241,12 @@
    1.62  
    1.63  instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
    1.64  
    1.65 -definition card_UNIV_product_def: 
    1.66 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
    1.67 +definition "card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
    1.68  
    1.69  instance proof
    1.70    fix x :: "('a \<times> 'b) itself"
    1.71    show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
    1.72 -    by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
    1.73 +    by(simp add: card_UNIV_prod_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
    1.74  qed
    1.75  
    1.76  end
    1.77 @@ -265,9 +255,9 @@
    1.78  
    1.79  instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
    1.80  
    1.81 -definition card_UNIV_sum_def: 
    1.82 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
    1.83 -                           in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
    1.84 +definition "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. 
    1.85 +  let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
    1.86 +  in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
    1.87  
    1.88  instance proof
    1.89    fix x :: "('a + 'b) itself"
    1.90 @@ -281,9 +271,9 @@
    1.91  
    1.92  instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
    1.93  
    1.94 -definition card_UNIV_fun_def: 
    1.95 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
    1.96 -                           in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
    1.97 +definition "card_UNIV = 
    1.98 +  (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
    1.99 +                            in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
   1.100  
   1.101  instance proof
   1.102    fix x :: "('a \<Rightarrow> 'b) itself"
   1.103 @@ -354,9 +344,7 @@
   1.104  instantiation option :: (card_UNIV) card_UNIV
   1.105  begin
   1.106  
   1.107 -definition card_UNIV_option_def: 
   1.108 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a))
   1.109 -                           in if c \<noteq> 0 then Suc c else 0)"
   1.110 +definition "card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a)) in if c \<noteq> 0 then Suc c else 0)"
   1.111  
   1.112  instance proof
   1.113    fix x :: "'a option itself"