--- 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)"
--- 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
--- 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)
--- 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:
--- 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 *}