tuned proofs

--- a/src/HOL/Datatype.thy	Tue Feb 26 16:10:54 2008 +0100
+++ b/src/HOL/Datatype.thy	Tue Feb 26 20:38:10 2008 +0100
@@ -615,25 +615,8 @@
 lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
   by (rule set_ext, case_tac x) auto
 
-instantiation option :: (finite) finite
-begin
-
-definition
-  "Finite_Set.itself = TYPE('a option)"
-
-instance proof
-  have "finite (UNIV :: 'a set)" by (rule finite)
-  hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp
-  also have "insert None (Some ` (UNIV :: 'a set)) = UNIV"
-    by (rule insert_None_conv_UNIV)
-  finally show "finite (UNIV :: 'a option set)" .
-qed
-
-end
-
-lemma univ_option [noatp, code func]:
-  "UNIV = insert (None \<Colon> 'a\<Colon>finite option) (image Some UNIV)"
-  unfolding insert_None_conv_UNIV ..
+instance option :: (finite) finite
+  by default (simp add: insert_None_conv_UNIV [symmetric])
 
 
 subsubsection {* Operations *}

--- a/src/HOL/Finite_Set.thy	Tue Feb 26 16:10:54 2008 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Feb 26 20:38:10 2008 +0100
@@ -428,8 +428,7 @@
   by auto
 
 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
-class finite (attach UNIV) = type +
-  fixes itself :: "'a itself"
+class finite (attach UNIV) = itself +
   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
 setup {* Sign.parent_path *}
 hide const finite
@@ -437,112 +436,42 @@
 lemma finite [simp]: "finite (A \<Colon> 'a\<Colon>finite set)"
   by (rule finite_subset [OF subset_UNIV finite_UNIV])
 
-lemma univ_unit [noatp]:
+lemma UNIV_unit [noatp]:
   "UNIV = {()}" by auto
 
-instantiation unit :: finite
-begin
-
-definition
-  "itself = TYPE(unit)"
-
-instance proof
-  have "finite {()}" by simp
-  also note univ_unit [symmetric]
-  finally show "finite (UNIV :: unit set)" .
-qed
-
-end
-
-lemmas [code func] = univ_unit
-
-lemma univ_bool [noatp]:
+instance unit :: finite
+  by default (simp add: UNIV_unit)
+
+lemmas [code func] = UNIV_unit
+
+lemma UNIV_bool [noatp]:
   "UNIV = {False, True}" by auto
 
-instantiation bool :: finite
-begin
-
-definition
-  "itself = TYPE(bool)"
-
-instance proof
-  have "finite {False, True}" by simp
-  also note univ_bool [symmetric]
-  finally show "finite (UNIV :: bool set)" .
-qed
-
-end
-
-lemmas [code func] = univ_bool
-
-instantiation * :: (finite, finite) finite
-begin
-
-definition
-  "itself = TYPE('a \<times> 'b)"
-
-instance proof
-  show "finite (UNIV :: ('a \<times> 'b) set)"
-  proof (rule finite_Prod_UNIV)
-    show "finite (UNIV :: 'a set)" by (rule finite)
-    show "finite (UNIV :: 'b set)" by (rule finite)
-  qed
-qed
-
-end
-
-lemma univ_prod [noatp, code func]:
-  "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) \<times> (UNIV \<Colon> 'b\<Colon>finite set)"
-  unfolding UNIV_Times_UNIV ..
-
-instantiation "+" :: (finite, finite) finite
-begin
-
-definition
-  "itself = TYPE('a + 'b)"
-
-instance proof
-  have a: "finite (UNIV :: 'a set)" by (rule finite)
-  have b: "finite (UNIV :: 'b set)" by (rule finite)
-  from a b have "finite ((UNIV :: 'a set) <+> (UNIV :: 'b set))"
-    by (rule finite_Plus)
-  thus "finite (UNIV :: ('a + 'b) set)" by simp
-qed
-
-end
-
-lemma univ_sum [noatp, code func]:
-  "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) <+> (UNIV \<Colon> 'b\<Colon>finite set)"
-  unfolding UNIV_Plus_UNIV ..
-
-instantiation set :: (finite) finite
-begin
-
-definition
-  "itself = TYPE('a set)"
-
-instance proof
-  have "finite (UNIV :: 'a set)" by (rule finite)
-  hence "finite (Pow (UNIV :: 'a set))"
-    by (rule finite_Pow_iff [THEN iffD2])
-  thus "finite (UNIV :: 'a set set)" by simp
-qed
-
-end
-
-lemma univ_set [noatp, code func]:
-  "UNIV = Pow (UNIV \<Colon> 'a\<Colon>finite set)" unfolding Pow_UNIV ..
+instance bool :: finite
+  by default (simp add: UNIV_bool)
+
+lemmas [code func] = UNIV_bool
+
+instance * :: (finite, finite) finite
+  by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
+
+declare UNIV_Times_UNIV [symmetric, code func]
+
+instance "+" :: (finite, finite) finite
+  by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
+
+declare UNIV_Plus_UNIV [symmetric, code func]
+
+instance set :: (finite) finite
+  by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
+
+declare Pow_UNIV [symmetric, code func]
 
 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
 
-instantiation "fun" :: (finite, finite) finite
-begin
-
-definition
-  "itself \<equiv> TYPE('a \<Rightarrow> 'b)"
-
-instance proof
+instance "fun" :: (finite, finite) finite
+proof
   show "finite (UNIV :: ('a => 'b) set)"
   proof (rule finite_imageD)
     let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
@@ -551,9 +480,6 @@
   qed
 qed
 
-end
-
-hide (open) const itself
 
 subsection {* Equality and order on functions *}