--- a/src/HOL/Datatype.thy Sun Aug 24 14:24:03 2008 +0200
+++ b/src/HOL/Datatype.thy Sun Aug 24 14:42:22 2008 +0200
@@ -9,7 +9,7 @@
header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
theory Datatype
-imports Finite_Set
+imports Nat Relation
begin
typedef (Node)
@@ -605,9 +605,6 @@
lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
by (rule set_ext, case_tac x) auto
-instance option :: (finite) finite
- by default (simp add: insert_None_conv_UNIV [symmetric])
-
subsubsection {* Operations *}
--- a/src/HOL/Finite_Set.thy Sun Aug 24 14:24:03 2008 +0200
+++ b/src/HOL/Finite_Set.thy Sun Aug 24 14:42:22 2008 +0200
@@ -7,7 +7,7 @@
header {* Finite sets *}
theory Finite_Set
-imports Divides Transitive_Closure
+imports Datatype Divides Transitive_Closure
begin
subsection {* Definition and basic properties *}
@@ -452,9 +452,6 @@
instance * :: (finite, finite) finite
by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
-instance "+" :: (finite, finite) finite
- by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
-
lemma inj_graph: "inj (%f. {(x, y). y = f x})"
by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
@@ -472,6 +469,12 @@
qed
qed
+instance "+" :: (finite, finite) finite
+ by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
+
+instance option :: (finite) finite
+ by default (simp add: insert_None_conv_UNIV [symmetric])
+
subsection {* A fold functional for finite sets *}