src/HOL/Library/Cardinality.thy
changeset 48053 9bc78a08ff0a
parent 48052 b74766e4c11e
child 48058 11a732f7d79f
child 48063 f02b4302d5dd
     1.1 --- a/src/HOL/Library/Cardinality.thy	Thu May 31 17:04:11 2012 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Thu May 31 17:10:43 2012 +0200
     1.3 @@ -146,71 +146,36 @@
     1.4  subsubsection {* @{typ "nat"} *}
     1.5  
     1.6  instantiation nat :: card_UNIV begin
     1.7 -
     1.8  definition "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
     1.9 -
    1.10 -instance proof
    1.11 -  fix x :: "nat itself"
    1.12 -  show "card_UNIV x = card (UNIV :: nat set)"
    1.13 -    unfolding card_UNIV_nat_def by simp
    1.14 -qed
    1.15 -
    1.16 +instance by intro_classes (simp add: card_UNIV_nat_def)
    1.17  end
    1.18  
    1.19  subsubsection {* @{typ "int"} *}
    1.20  
    1.21  instantiation int :: card_UNIV begin
    1.22 -
    1.23  definition "card_UNIV = (\<lambda>a :: int itself. 0)"
    1.24 -
    1.25 -instance proof
    1.26 -  fix x :: "int itself"
    1.27 -  show "card_UNIV x = card (UNIV :: int set)"
    1.28 -    unfolding card_UNIV_int_def by(simp add: infinite_UNIV_int)
    1.29 -qed
    1.30 -
    1.31 +instance by intro_classes (simp add: card_UNIV_int_def infinite_UNIV_int)
    1.32  end
    1.33  
    1.34  subsubsection {* @{typ "'a list"} *}
    1.35  
    1.36  instantiation list :: (type) card_UNIV begin
    1.37 -
    1.38  definition "card_UNIV = (\<lambda>a :: 'a list itself. 0)"
    1.39 -
    1.40 -instance proof
    1.41 -  fix x :: "'a list itself"
    1.42 -  show "card_UNIV x = card (UNIV :: 'a list set)"
    1.43 -    unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
    1.44 -qed
    1.45 -
    1.46 +instance by intro_classes (simp add: card_UNIV_list_def infinite_UNIV_listI)
    1.47  end
    1.48  
    1.49  subsubsection {* @{typ "unit"} *}
    1.50  
    1.51  instantiation unit :: card_UNIV begin
    1.52 -
    1.53  definition "card_UNIV = (\<lambda>a :: unit itself. 1)"
    1.54 -
    1.55 -instance proof
    1.56 -  fix x :: "unit itself"
    1.57 -  show "card_UNIV x = card (UNIV :: unit set)"
    1.58 -    by(simp add: card_UNIV_unit_def card_UNIV_unit)
    1.59 -qed
    1.60 -
    1.61 +instance by intro_classes (simp add: card_UNIV_unit_def card_UNIV_unit)
    1.62  end
    1.63  
    1.64  subsubsection {* @{typ "bool"} *}
    1.65  
    1.66  instantiation bool :: card_UNIV begin
    1.67 -
    1.68  definition "card_UNIV = (\<lambda>a :: bool itself. 2)"
    1.69 -
    1.70 -instance proof
    1.71 -  fix x :: "bool itself"
    1.72 -  show "card_UNIV x = card (UNIV :: bool set)"
    1.73 -    by(simp add: card_UNIV_bool_def card_UNIV_bool)
    1.74 -qed
    1.75 -
    1.76 +instance by(intro_classes)(simp add: card_UNIV_bool_def card_UNIV_bool)
    1.77  end
    1.78  
    1.79  subsubsection {* @{typ "char"} *}
    1.80 @@ -226,45 +191,26 @@
    1.81  qed
    1.82  
    1.83  instantiation char :: card_UNIV begin
    1.84 -
    1.85  definition "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
    1.86 -
    1.87 -instance proof
    1.88 -  fix x :: "char itself"
    1.89 -  show "card_UNIV x = card (UNIV :: char set)"
    1.90 -    by(simp add: card_UNIV_char_def card_UNIV_char)
    1.91 -qed
    1.92 -
    1.93 +instance by intro_classes (simp add: card_UNIV_char_def card_UNIV_char)
    1.94  end
    1.95  
    1.96  subsubsection {* @{typ "'a \<times> 'b"} *}
    1.97  
    1.98  instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
    1.99 -
   1.100  definition "card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
   1.101 -
   1.102 -instance proof
   1.103 -  fix x :: "('a \<times> 'b) itself"
   1.104 -  show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
   1.105 -    by(simp add: card_UNIV_prod_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
   1.106 -qed
   1.107 -
   1.108 +instance 
   1.109 +  by intro_classes (simp add: card_UNIV_prod_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
   1.110  end
   1.111  
   1.112  subsubsection {* @{typ "'a + 'b"} *}
   1.113  
   1.114  instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
   1.115 -
   1.116  definition "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. 
   1.117    let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
   1.118    in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
   1.119 -
   1.120 -instance proof
   1.121 -  fix x :: "('a + 'b) itself"
   1.122 -  show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
   1.123 -    by (auto simp add: card_UNIV_sum_def card_UNIV card_eq_0_iff UNIV_Plus_UNIV[symmetric] finite_Plus_iff Let_def card_Plus simp del: UNIV_Plus_UNIV dest!: card_ge_0_finite)
   1.124 -qed
   1.125 -
   1.126 +instance
   1.127 +  by intro_classes (auto simp add: card_UNIV_sum_def card_UNIV card_eq_0_iff UNIV_Plus_UNIV[symmetric] finite_Plus_iff Let_def card_Plus simp del: UNIV_Plus_UNIV dest!: card_ge_0_finite)
   1.128  end
   1.129  
   1.130  subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
   1.131 @@ -295,7 +241,7 @@
   1.132      proof(rule UNIV_eq_I)
   1.133        fix f :: "'a \<Rightarrow> 'b"
   1.134        from as have "f = the \<circ> map_of (zip as (map f as))"
   1.135 -        by(auto simp add: map_of_zip_map intro: ext)
   1.136 +        by(auto simp add: map_of_zip_map)
   1.137        thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
   1.138      qed
   1.139      moreover have "distinct ?xs" unfolding distinct_map
   1.140 @@ -329,7 +275,7 @@
   1.141        { fix y
   1.142          have "x y \<in> UNIV" ..
   1.143          hence "x y = b" unfolding b by simp }
   1.144 -      thus "x \<in> {\<lambda>x. b}" by(auto intro: ext)
   1.145 +      thus "x \<in> {\<lambda>x. b}" by(auto)
   1.146      qed
   1.147      have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
   1.148    ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
   1.149 @@ -349,8 +295,7 @@
   1.150  instance proof
   1.151    fix x :: "'a option itself"
   1.152    show "card_UNIV x = card (UNIV :: 'a option set)"
   1.153 -    unfolding UNIV_option_conv
   1.154 -    by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
   1.155 +    by(auto simp add: UNIV_option_conv card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
   1.156        (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
   1.157  qed
   1.158