# HG changeset patch
# User Andreas Lochbihler
# Date 1338477043 -7200
# Node ID 9bc78a08ff0a3e7c03d073f5e889feda7a1b570e
# Parent  b74766e4c11ee20b7a6d0ad06fe74ce8b9a7de40
tuned proofs

diff -r b74766e4c11e -r 9bc78a08ff0a src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Thu May 31 17:04:11 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy	Thu May 31 17:10:43 2012 +0200
@@ -146,71 +146,36 @@
 subsubsection {* @{typ "nat"} *}
 
 instantiation nat :: card_UNIV begin
-
 definition "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
-
-instance proof
-  fix x :: "nat itself"
-  show "card_UNIV x = card (UNIV :: nat set)"
-    unfolding card_UNIV_nat_def by simp
-qed
-
+instance by intro_classes (simp add: card_UNIV_nat_def)
 end
 
 subsubsection {* @{typ "int"} *}
 
 instantiation int :: card_UNIV begin
-
 definition "card_UNIV = (\<lambda>a :: int itself. 0)"
-
-instance proof
-  fix x :: "int itself"
-  show "card_UNIV x = card (UNIV :: int set)"
-    unfolding card_UNIV_int_def by(simp add: infinite_UNIV_int)
-qed
-
+instance by intro_classes (simp add: card_UNIV_int_def infinite_UNIV_int)
 end
 
 subsubsection {* @{typ "'a list"} *}
 
 instantiation list :: (type) card_UNIV begin
-
 definition "card_UNIV = (\<lambda>a :: 'a list itself. 0)"
-
-instance proof
-  fix x :: "'a list itself"
-  show "card_UNIV x = card (UNIV :: 'a list set)"
-    unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
-qed
-
+instance by intro_classes (simp add: card_UNIV_list_def infinite_UNIV_listI)
 end
 
 subsubsection {* @{typ "unit"} *}
 
 instantiation unit :: card_UNIV begin
-
 definition "card_UNIV = (\<lambda>a :: unit itself. 1)"
-
-instance proof
-  fix x :: "unit itself"
-  show "card_UNIV x = card (UNIV :: unit set)"
-    by(simp add: card_UNIV_unit_def card_UNIV_unit)
-qed
-
+instance by intro_classes (simp add: card_UNIV_unit_def card_UNIV_unit)
 end
 
 subsubsection {* @{typ "bool"} *}
 
 instantiation bool :: card_UNIV begin
-
 definition "card_UNIV = (\<lambda>a :: bool itself. 2)"
-
-instance proof
-  fix x :: "bool itself"
-  show "card_UNIV x = card (UNIV :: bool set)"
-    by(simp add: card_UNIV_bool_def card_UNIV_bool)
-qed
-
+instance by(intro_classes)(simp add: card_UNIV_bool_def card_UNIV_bool)
 end
 
 subsubsection {* @{typ "char"} *}
@@ -226,45 +191,26 @@
 qed
 
 instantiation char :: card_UNIV begin
-
 definition "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
-
-instance proof
-  fix x :: "char itself"
-  show "card_UNIV x = card (UNIV :: char set)"
-    by(simp add: card_UNIV_char_def card_UNIV_char)
-qed
-
+instance by intro_classes (simp add: card_UNIV_char_def card_UNIV_char)
 end
 
 subsubsection {* @{typ "'a \<times> 'b"} *}
 
 instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
-
 definition "card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
-
-instance proof
-  fix x :: "('a \<times> 'b) itself"
-  show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
-    by(simp add: card_UNIV_prod_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
-qed
-
+instance 
+  by intro_classes (simp add: card_UNIV_prod_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
 end
 
 subsubsection {* @{typ "'a + 'b"} *}
 
 instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
-
 definition "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. 
   let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
   in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
-
-instance proof
-  fix x :: "('a + 'b) itself"
-  show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
-    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)
-qed
-
+instance
+  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)
 end
 
 subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
@@ -295,7 +241,7 @@
     proof(rule UNIV_eq_I)
       fix f :: "'a \<Rightarrow> 'b"
       from as have "f = the \<circ> map_of (zip as (map f as))"
-        by(auto simp add: map_of_zip_map intro: ext)
+        by(auto simp add: map_of_zip_map)
       thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
     qed
     moreover have "distinct ?xs" unfolding distinct_map
@@ -329,7 +275,7 @@
       { fix y
         have "x y \<in> UNIV" ..
         hence "x y = b" unfolding b by simp }
-      thus "x \<in> {\<lambda>x. b}" by(auto intro: ext)
+      thus "x \<in> {\<lambda>x. b}" by(auto)
     qed
     have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
   ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
@@ -349,8 +295,7 @@
 instance proof
   fix x :: "'a option itself"
   show "card_UNIV x = card (UNIV :: 'a option set)"
-    unfolding UNIV_option_conv
-    by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
+    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)
       (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
 qed