--- a/src/HOL/Finite_Set.thy Mon Oct 15 12:25:33 2007 +0200
+++ b/src/HOL/Finite_Set.thy Mon Oct 15 15:29:39 2007 +0200
@@ -2622,6 +2622,7 @@
setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
class finite (attach UNIV) = type +
+ fixes itself :: "'a itself"
assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
setup {* Sign.parent_path *}
hide const finite
@@ -2633,6 +2634,7 @@
"UNIV = {()}" by auto
instance unit :: finite
+ "Finite_Set.itself \<equiv> TYPE(unit)"
proof
have "finite {()}" by simp
also note univ_unit [symmetric]
@@ -2645,6 +2647,7 @@
"UNIV = {False, True}" by auto
instance bool :: finite
+ "itself \<equiv> TYPE(bool)"
proof
have "finite {False, True}" by simp
also note univ_bool [symmetric]
@@ -2654,6 +2657,7 @@
lemmas [code func] = univ_bool
instance * :: (finite, finite) finite
+ "itself \<equiv> TYPE('a\<Colon>finite)"
proof
show "finite (UNIV :: ('a \<times> 'b) set)"
proof (rule finite_Prod_UNIV)
@@ -2667,6 +2671,7 @@
unfolding UNIV_Times_UNIV ..
instance "+" :: (finite, finite) finite
+ "itself \<equiv> TYPE('a\<Colon>finite + 'b\<Colon>finite)"
proof
have a: "finite (UNIV :: 'a set)" by (rule finite)
have b: "finite (UNIV :: 'b set)" by (rule finite)
@@ -2680,6 +2685,7 @@
unfolding UNIV_Plus_UNIV ..
instance set :: (finite) finite
+ "itself \<equiv> TYPE('a\<Colon>finite set)"
proof
have "finite (UNIV :: 'a set)" by (rule finite)
hence "finite (Pow (UNIV :: 'a set))"
@@ -2694,6 +2700,7 @@
by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
instance "fun" :: (finite, finite) finite
+ "itself \<equiv> TYPE('a\<Colon>finite \<Rightarrow> 'b\<Colon>finite)"
proof
show "finite (UNIV :: ('a => 'b) set)"
proof (rule finite_imageD)
@@ -2703,6 +2710,7 @@
qed
qed
+hide (open) const itself
subsection {* Equality and order on functions *}