# HG changeset patch
# User nipkow
# Date 1123237230 -7200
# Node ID b257300c3a9c7c0a2900a10fbb05a66517142b47
# Parent  1c361a3de73da1c3754a63f25086b215acb7ad75
added Brian Hufmann's finite instances

diff -r 1c361a3de73d -r b257300c3a9c src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Aug 03 16:43:39 2005 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Aug 05 12:20:30 2005 +0200
@@ -305,6 +305,9 @@
   by (blast intro: finite_UN_I finite_subset)
 
 
+lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)"
+by (simp add: Plus_def)
+
 text {* Sigma of finite sets *}
 
 lemma finite_SigmaI [simp]:
@@ -353,23 +356,6 @@
 done
 
 
-instance unit :: finite
-proof
-  have "finite {()}" by simp
-  also have "{()} = UNIV" by auto
-  finally show "finite (UNIV :: unit set)" .
-qed
-
-instance * :: (finite, finite) finite
-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
-
-
 text {* The powerset of a finite set *}
 
 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
@@ -2313,4 +2299,67 @@
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
 by(simp add: Max_def max.fold1_below_iff)
 
+subsection {* Properties of axclass @{text finite} *}
+
+text{* Many of these are by Brian Huffman. *}
+
+lemma finite_set: "finite (A::'a::finite set)"
+by (rule finite_subset [OF subset_UNIV finite])
+
+
+instance unit :: finite
+proof
+  have "finite {()}" by simp
+  also have "{()} = UNIV" by auto
+  finally show "finite (UNIV :: unit set)" .
+qed
+
+instance bool :: finite
+proof
+  have "finite {True, False}" by simp
+  also have "{True, False} = UNIV" by auto
+  finally show "finite (UNIV :: bool set)" .
+qed
+
+
+instance * :: (finite, finite) finite
+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
+
+instance "+" :: (finite, finite) finite
+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
+
+
+instance set :: (finite) finite
+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
+
+lemma inj_graph: "inj (%f. {(x, y). y = f x})"
+by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
+
+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}"
+    show "finite (range ?graph)" by (rule finite_set)
+    show "inj ?graph" by (rule inj_graph)
+  qed
+qed
+
 end