# HG changeset patch
# User Andreas Lochbihler
# Date 1338476651 -7200
# Node ID b74766e4c11ee20b7a6d0ad06fe74ce8b9a7de40
# Parent  53a0df441e20a5f4274cbc434be9ec4e41786c5f
tuned instantiations
dropped redundant lemmas

diff -r 53a0df441e20 -r b74766e4c11e src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Thu May 31 16:58:38 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy	Thu May 31 17:04:11 2012 +0200
@@ -161,7 +161,7 @@
 
 instantiation int :: card_UNIV begin
 
-definition "card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)"
+definition "card_UNIV = (\<lambda>a :: int itself. 0)"
 
 instance proof
   fix x :: "int itself"
@@ -175,7 +175,7 @@
 
 instantiation list :: (type) card_UNIV begin
 
-definition "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)"
+definition "card_UNIV = (\<lambda>a :: 'a list itself. 0)"
 
 instance proof
   fix x :: "'a list itself"
@@ -187,13 +187,9 @@
 
 subsubsection {* @{typ "unit"} *}
 
-lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
-  unfolding UNIV_unit by simp
-
 instantiation unit :: card_UNIV begin
 
-definition card_UNIV_unit_def: 
-  "card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)"
+definition "card_UNIV = (\<lambda>a :: unit itself. 1)"
 
 instance proof
   fix x :: "unit itself"
@@ -205,13 +201,9 @@
 
 subsubsection {* @{typ "bool"} *}
 
-lemma card_UNIV_bool: "card (UNIV :: bool set) = 2"
-  unfolding UNIV_bool by simp
-
 instantiation bool :: card_UNIV begin
 
-definition card_UNIV_bool_def: 
-  "card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)"
+definition "card_UNIV = (\<lambda>a :: bool itself. 2)"
 
 instance proof
   fix x :: "bool itself"
@@ -235,8 +227,7 @@
 
 instantiation char :: card_UNIV begin
 
-definition card_UNIV_char_def: 
-  "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
+definition "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
 
 instance proof
   fix x :: "char itself"
@@ -250,13 +241,12 @@
 
 instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
 
-definition card_UNIV_product_def: 
-  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
+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_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
+    by(simp add: card_UNIV_prod_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
 qed
 
 end
@@ -265,9 +255,9 @@
 
 instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
 
-definition card_UNIV_sum_def: 
-  "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)"
+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"
@@ -281,9 +271,9 @@
 
 instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
 
-definition card_UNIV_fun_def: 
-  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
-                           in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
+definition "card_UNIV = 
+  (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
+                            in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
 
 instance proof
   fix x :: "('a \<Rightarrow> 'b) itself"
@@ -354,9 +344,7 @@
 instantiation option :: (card_UNIV) card_UNIV
 begin
 
-definition card_UNIV_option_def: 
-  "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a))
-                           in if c \<noteq> 0 then Suc c else 0)"
+definition "card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a)) in if c \<noteq> 0 then Suc c else 0)"
 
 instance proof
   fix x :: "'a option itself"