# HG changeset patch
# User haftmann
# Date 1190831275 -7200
# Node ID e2b3a1065676b8f348ac6d8af3d9a605cc39669d
# Parent  dd9ea6b72eb9e6b0cf15f0194384134984c9591d
moved Finite_Set before Datatype

diff -r dd9ea6b72eb9 -r e2b3a1065676 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Sep 26 19:19:38 2007 +0200
+++ b/src/HOL/Datatype.thy	Wed Sep 26 20:27:55 2007 +0200
@@ -9,7 +9,7 @@
 header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
 
 theory Datatype
-imports Nat
+imports Finite_Set
 begin
 
 typedef (Node)
@@ -613,6 +613,22 @@
   | (Some) y where "x = Some y" and "Q y"
   using c by (cases x) simp_all
 
+lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
+  by (rule set_ext, case_tac x) auto
+
+instance option :: (finite) finite
+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
+
+lemma univ_option [noatp, code func]:
+  "UNIV = insert (None \<Colon> 'a\<Colon>finite option) (image Some UNIV)"
+  unfolding insert_None_conv_UNIV ..
+
 
 subsubsection {* Operations *}
 
@@ -638,7 +654,6 @@
 lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
   by (cases xo) auto
 
-
 constdefs
   option_map :: "('a => 'b) => ('a option => 'b option)"
   "option_map == %f y. case y of None => None | Some x => Some (f x)"
diff -r dd9ea6b72eb9 -r e2b3a1065676 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Wed Sep 26 19:19:38 2007 +0200
+++ b/src/HOL/Equiv_Relations.thy	Wed Sep 26 20:27:55 2007 +0200
@@ -6,7 +6,7 @@
 header {* Equivalence Relations in Higher-Order Set Theory *}
 
 theory Equiv_Relations
-imports Relation
+imports Finite_Set Relation
 begin
 
 subsection {* Equivalence relations *}
@@ -292,4 +292,45 @@
          erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+
   done
 
+
+subsection {* Quotients and finiteness *}
+
+text {*Suggested by Florian Kammüller*}
+
+lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
+  -- {* recall @{thm equiv_type} *}
+  apply (rule finite_subset)
+   apply (erule_tac [2] finite_Pow_iff [THEN iffD2])
+  apply (unfold quotient_def)
+  apply blast
+  done
+
+lemma finite_equiv_class:
+  "finite A ==> r \<subseteq> A \<times> A ==> X \<in> A//r ==> finite X"
+  apply (unfold quotient_def)
+  apply (rule finite_subset)
+   prefer 2 apply assumption
+  apply blast
+  done
+
+lemma equiv_imp_dvd_card:
+  "finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X
+    ==> k dvd card A"
+  apply (rule Union_quotient [THEN subst])
+   apply assumption
+  apply (rule dvd_partition)
+     prefer 3 apply (blast dest: quotient_disj)
+    apply (simp_all add: Union_quotient equiv_type)
+  done
+
+lemma card_quotient_disjoint:
+ "\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A"
+apply(simp add:quotient_def)
+apply(subst card_UN_disjoint)
+   apply assumption
+  apply simp
+ apply(fastsimp simp add:inj_on_def)
+apply (simp add:setsum_constant)
+done
+
 end
diff -r dd9ea6b72eb9 -r e2b3a1065676 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Sep 26 19:19:38 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Sep 26 20:27:55 2007 +0200
@@ -7,7 +7,7 @@
 header {* Finite sets *}
 
 theory Finite_Set
-imports IntDef Divides Datatype
+imports Divides
 begin
 
 subsection {* Definition and basic properties *}
@@ -2272,92 +2272,6 @@
 apply(simp add: neq_commute less_le)
 done
 
-
-subsection {* Finiteness and quotients *}
-
-text {*Suggested by Florian Kammüller*}
-
-lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
-  -- {* recall @{thm equiv_type} *}
-  apply (rule finite_subset)
-   apply (erule_tac [2] finite_Pow_iff [THEN iffD2])
-  apply (unfold quotient_def)
-  apply blast
-  done
-
-lemma finite_equiv_class:
-  "finite A ==> r \<subseteq> A \<times> A ==> X \<in> A//r ==> finite X"
-  apply (unfold quotient_def)
-  apply (rule finite_subset)
-   prefer 2 apply assumption
-  apply blast
-  done
-
-lemma equiv_imp_dvd_card:
-  "finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X
-    ==> k dvd card A"
-  apply (rule Union_quotient [THEN subst])
-   apply assumption
-  apply (rule dvd_partition)
-     prefer 3 apply (blast dest: quotient_disj)
-    apply (simp_all add: Union_quotient equiv_type)
-  done
-
-lemma card_quotient_disjoint:
- "\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A"
-apply(simp add:quotient_def)
-apply(subst card_UN_disjoint)
-   apply assumption
-  apply simp
- apply(fastsimp simp add:inj_on_def)
-apply (simp add:setsum_constant)
-done
-
-
-subsection {* @{term setsum} and @{term setprod} on integers *}
-
-text {*By Jeremy Avigad*}
-
-lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
-  apply (cases "finite A")
-  apply (erule finite_induct, auto)
-  done
-
-lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
-  apply (cases "finite A")
-  apply (erule finite_induct, auto)
-  done
-
-lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
-  apply (cases "finite A")
-  apply (erule finite_induct, auto simp add: of_nat_mult)
-  done
-
-lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
-  apply (cases "finite A")
-  apply (erule finite_induct, auto)
-  done
-
-lemma setprod_nonzero_nat:
-    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
-  by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_nat:
-    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
-  by (rule setprod_zero_eq, auto)
-
-lemma setprod_nonzero_int:
-    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
-  by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_int:
-    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
-  by (rule setprod_zero_eq, auto)
-
-lemmas int_setsum = of_nat_setsum [where 'a=int]
-lemmas int_setprod = of_nat_setprod [where 'a=int]
-
-
 context lattice
 begin
 
@@ -2749,22 +2663,6 @@
   "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) <+> (UNIV \<Colon> 'b\<Colon>finite set)"
   unfolding UNIV_Plus_UNIV ..
 
-lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
-  by (rule set_ext, case_tac x, auto)
-
-instance option :: (finite) finite
-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
-
-lemma univ_option [noatp, code func]:
-  "UNIV = insert (None \<Colon> 'a\<Colon>finite option) (image Some UNIV)"
-  unfolding insert_None_conv_UNIV ..
-
 instance set :: (finite) finite
 proof
   have "finite (UNIV :: 'a set)" by (rule finite)
diff -r dd9ea6b72eb9 -r e2b3a1065676 src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Wed Sep 26 19:19:38 2007 +0200
+++ b/src/HOL/IntDef.thy	Wed Sep 26 20:27:55 2007 +0200
@@ -11,7 +11,6 @@
 imports Equiv_Relations Nat
 begin
 
-
 text {* the equivalence relation underlying the integers *}
 
 definition
@@ -579,6 +578,50 @@
   by (rule Ints_cases) auto
 
 
+subsection {* @{term setsum} and @{term setprod} *}
+
+text {*By Jeremy Avigad*}
+
+lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
+  apply (cases "finite A")
+  apply (erule finite_induct, auto)
+  done
+
+lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
+  apply (cases "finite A")
+  apply (erule finite_induct, auto)
+  done
+
+lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
+  apply (cases "finite A")
+  apply (erule finite_induct, auto simp add: of_nat_mult)
+  done
+
+lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
+  apply (cases "finite A")
+  apply (erule finite_induct, auto)
+  done
+
+lemma setprod_nonzero_nat:
+    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
+  by (rule setprod_nonzero, auto)
+
+lemma setprod_zero_eq_nat:
+    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
+  by (rule setprod_zero_eq, auto)
+
+lemma setprod_nonzero_int:
+    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
+  by (rule setprod_nonzero, auto)
+
+lemma setprod_zero_eq_int:
+    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
+  by (rule setprod_zero_eq, auto)
+
+lemmas int_setsum = of_nat_setsum [where 'a=int]
+lemmas int_setprod = of_nat_setprod [where 'a=int]
+
+
 subsection {* Further properties *}
 
 text{*Now we replace the case analysis rule by a more conventional one:
diff -r dd9ea6b72eb9 -r e2b3a1065676 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Wed Sep 26 19:19:38 2007 +0200
+++ b/src/HOLCF/Porder.thy	Wed Sep 26 20:27:55 2007 +0200
@@ -6,7 +6,7 @@
 header {* Partial orders *}
 
 theory Porder
-imports Finite_Set
+imports Datatype Finite_Set
 begin
 
 subsection {* Type class for partial orders *}