author haftmann Wed Sep 26 20:27:55 2007 +0200 (2007-09-26) changeset 24728 e2b3a1065676 parent 24727 dd9ea6b72eb9 child 24729 f5015dd2431b
moved Finite_Set before Datatype
 src/HOL/Datatype.thy file | annotate | diff | revisions src/HOL/Equiv_Relations.thy file | annotate | diff | revisions src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/IntDef.thy file | annotate | diff | revisions src/HOLCF/Porder.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Datatype.thy	Wed Sep 26 19:19:38 2007 +0200
1.2 +++ b/src/HOL/Datatype.thy	Wed Sep 26 20:27:55 2007 +0200
1.3 @@ -9,7 +9,7 @@
1.4  header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
1.5
1.6  theory Datatype
1.7 -imports Nat
1.8 +imports Finite_Set
1.9  begin
1.10
1.11  typedef (Node)
1.12 @@ -613,6 +613,22 @@
1.13    | (Some) y where "x = Some y" and "Q y"
1.14    using c by (cases x) simp_all
1.15
1.16 +lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
1.17 +  by (rule set_ext, case_tac x) auto
1.18 +
1.19 +instance option :: (finite) finite
1.20 +proof
1.21 +  have "finite (UNIV :: 'a set)" by (rule finite)
1.22 +  hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp
1.23 +  also have "insert None (Some ` (UNIV :: 'a set)) = UNIV"
1.24 +    by (rule insert_None_conv_UNIV)
1.25 +  finally show "finite (UNIV :: 'a option set)" .
1.26 +qed
1.27 +
1.28 +lemma univ_option [noatp, code func]:
1.29 +  "UNIV = insert (None \<Colon> 'a\<Colon>finite option) (image Some UNIV)"
1.30 +  unfolding insert_None_conv_UNIV ..
1.31 +
1.32
1.33  subsubsection {* Operations *}
1.34
1.35 @@ -638,7 +654,6 @@
1.36  lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
1.37    by (cases xo) auto
1.38
1.39 -
1.40  constdefs
1.41    option_map :: "('a => 'b) => ('a option => 'b option)"
1.42    "option_map == %f y. case y of None => None | Some x => Some (f x)"
```
```     2.1 --- a/src/HOL/Equiv_Relations.thy	Wed Sep 26 19:19:38 2007 +0200
2.2 +++ b/src/HOL/Equiv_Relations.thy	Wed Sep 26 20:27:55 2007 +0200
2.3 @@ -6,7 +6,7 @@
2.4  header {* Equivalence Relations in Higher-Order Set Theory *}
2.5
2.6  theory Equiv_Relations
2.7 -imports Relation
2.8 +imports Finite_Set Relation
2.9  begin
2.10
2.11  subsection {* Equivalence relations *}
2.12 @@ -292,4 +292,45 @@
2.13           erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+
2.14    done
2.15
2.16 +
2.17 +subsection {* Quotients and finiteness *}
2.18 +
2.19 +text {*Suggested by Florian Kammüller*}
2.20 +
2.21 +lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
2.22 +  -- {* recall @{thm equiv_type} *}
2.23 +  apply (rule finite_subset)
2.24 +   apply (erule_tac [2] finite_Pow_iff [THEN iffD2])
2.25 +  apply (unfold quotient_def)
2.26 +  apply blast
2.27 +  done
2.28 +
2.29 +lemma finite_equiv_class:
2.30 +  "finite A ==> r \<subseteq> A \<times> A ==> X \<in> A//r ==> finite X"
2.31 +  apply (unfold quotient_def)
2.32 +  apply (rule finite_subset)
2.33 +   prefer 2 apply assumption
2.34 +  apply blast
2.35 +  done
2.36 +
2.37 +lemma equiv_imp_dvd_card:
2.38 +  "finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X
2.39 +    ==> k dvd card A"
2.40 +  apply (rule Union_quotient [THEN subst])
2.41 +   apply assumption
2.42 +  apply (rule dvd_partition)
2.43 +     prefer 3 apply (blast dest: quotient_disj)
2.44 +    apply (simp_all add: Union_quotient equiv_type)
2.45 +  done
2.46 +
2.47 +lemma card_quotient_disjoint:
2.48 + "\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A"
2.50 +apply(subst card_UN_disjoint)
2.51 +   apply assumption
2.52 +  apply simp
2.55 +done
2.56 +
2.57  end
```
```     3.1 --- a/src/HOL/Finite_Set.thy	Wed Sep 26 19:19:38 2007 +0200
3.2 +++ b/src/HOL/Finite_Set.thy	Wed Sep 26 20:27:55 2007 +0200
3.3 @@ -7,7 +7,7 @@
3.4  header {* Finite sets *}
3.5
3.6  theory Finite_Set
3.7 -imports IntDef Divides Datatype
3.8 +imports Divides
3.9  begin
3.10
3.11  subsection {* Definition and basic properties *}
3.12 @@ -2272,92 +2272,6 @@
3.14  done
3.15
3.16 -
3.17 -subsection {* Finiteness and quotients *}
3.18 -
3.19 -text {*Suggested by Florian Kammüller*}
3.20 -
3.21 -lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
3.22 -  -- {* recall @{thm equiv_type} *}
3.23 -  apply (rule finite_subset)
3.24 -   apply (erule_tac [2] finite_Pow_iff [THEN iffD2])
3.25 -  apply (unfold quotient_def)
3.26 -  apply blast
3.27 -  done
3.28 -
3.29 -lemma finite_equiv_class:
3.30 -  "finite A ==> r \<subseteq> A \<times> A ==> X \<in> A//r ==> finite X"
3.31 -  apply (unfold quotient_def)
3.32 -  apply (rule finite_subset)
3.33 -   prefer 2 apply assumption
3.34 -  apply blast
3.35 -  done
3.36 -
3.37 -lemma equiv_imp_dvd_card:
3.38 -  "finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X
3.39 -    ==> k dvd card A"
3.40 -  apply (rule Union_quotient [THEN subst])
3.41 -   apply assumption
3.42 -  apply (rule dvd_partition)
3.43 -     prefer 3 apply (blast dest: quotient_disj)
3.44 -    apply (simp_all add: Union_quotient equiv_type)
3.45 -  done
3.46 -
3.47 -lemma card_quotient_disjoint:
3.48 - "\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A"
3.50 -apply(subst card_UN_disjoint)
3.51 -   apply assumption
3.52 -  apply simp
3.55 -done
3.56 -
3.57 -
3.58 -subsection {* @{term setsum} and @{term setprod} on integers *}
3.59 -
3.61 -
3.62 -lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
3.63 -  apply (cases "finite A")
3.64 -  apply (erule finite_induct, auto)
3.65 -  done
3.66 -
3.67 -lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
3.68 -  apply (cases "finite A")
3.69 -  apply (erule finite_induct, auto)
3.70 -  done
3.71 -
3.72 -lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
3.73 -  apply (cases "finite A")
3.74 -  apply (erule finite_induct, auto simp add: of_nat_mult)
3.75 -  done
3.76 -
3.77 -lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
3.78 -  apply (cases "finite A")
3.79 -  apply (erule finite_induct, auto)
3.80 -  done
3.81 -
3.82 -lemma setprod_nonzero_nat:
3.83 -    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
3.84 -  by (rule setprod_nonzero, auto)
3.85 -
3.86 -lemma setprod_zero_eq_nat:
3.87 -    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
3.88 -  by (rule setprod_zero_eq, auto)
3.89 -
3.90 -lemma setprod_nonzero_int:
3.91 -    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
3.92 -  by (rule setprod_nonzero, auto)
3.93 -
3.94 -lemma setprod_zero_eq_int:
3.95 -    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
3.96 -  by (rule setprod_zero_eq, auto)
3.97 -
3.98 -lemmas int_setsum = of_nat_setsum [where 'a=int]
3.99 -lemmas int_setprod = of_nat_setprod [where 'a=int]
3.100 -
3.101 -
3.102  context lattice
3.103  begin
3.104
3.105 @@ -2749,22 +2663,6 @@
3.106    "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) <+> (UNIV \<Colon> 'b\<Colon>finite set)"
3.107    unfolding UNIV_Plus_UNIV ..
3.108
3.109 -lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
3.110 -  by (rule set_ext, case_tac x, auto)
3.111 -
3.112 -instance option :: (finite) finite
3.113 -proof
3.114 -  have "finite (UNIV :: 'a set)" by (rule finite)
3.115 -  hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp
3.116 -  also have "insert None (Some ` (UNIV :: 'a set)) = UNIV"
3.117 -    by (rule insert_None_conv_UNIV)
3.118 -  finally show "finite (UNIV :: 'a option set)" .
3.119 -qed
3.120 -
3.121 -lemma univ_option [noatp, code func]:
3.122 -  "UNIV = insert (None \<Colon> 'a\<Colon>finite option) (image Some UNIV)"
3.123 -  unfolding insert_None_conv_UNIV ..
3.124 -
3.125  instance set :: (finite) finite
3.126  proof
3.127    have "finite (UNIV :: 'a set)" by (rule finite)
```
```     4.1 --- a/src/HOL/IntDef.thy	Wed Sep 26 19:19:38 2007 +0200
4.2 +++ b/src/HOL/IntDef.thy	Wed Sep 26 20:27:55 2007 +0200
4.3 @@ -11,7 +11,6 @@
4.4  imports Equiv_Relations Nat
4.5  begin
4.6
4.7 -
4.8  text {* the equivalence relation underlying the integers *}
4.9
4.10  definition
4.11 @@ -579,6 +578,50 @@
4.12    by (rule Ints_cases) auto
4.13
4.14
4.15 +subsection {* @{term setsum} and @{term setprod} *}
4.16 +
4.18 +
4.19 +lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
4.20 +  apply (cases "finite A")
4.21 +  apply (erule finite_induct, auto)
4.22 +  done
4.23 +
4.24 +lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
4.25 +  apply (cases "finite A")
4.26 +  apply (erule finite_induct, auto)
4.27 +  done
4.28 +
4.29 +lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
4.30 +  apply (cases "finite A")
4.31 +  apply (erule finite_induct, auto simp add: of_nat_mult)
4.32 +  done
4.33 +
4.34 +lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
4.35 +  apply (cases "finite A")
4.36 +  apply (erule finite_induct, auto)
4.37 +  done
4.38 +
4.39 +lemma setprod_nonzero_nat:
4.40 +    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
4.41 +  by (rule setprod_nonzero, auto)
4.42 +
4.43 +lemma setprod_zero_eq_nat:
4.44 +    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
4.45 +  by (rule setprod_zero_eq, auto)
4.46 +
4.47 +lemma setprod_nonzero_int:
4.48 +    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
4.49 +  by (rule setprod_nonzero, auto)
4.50 +
4.51 +lemma setprod_zero_eq_int:
4.52 +    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
4.53 +  by (rule setprod_zero_eq, auto)
4.54 +
4.55 +lemmas int_setsum = of_nat_setsum [where 'a=int]
4.56 +lemmas int_setprod = of_nat_setprod [where 'a=int]
4.57 +
4.58 +
4.59  subsection {* Further properties *}
4.60
4.61  text{*Now we replace the case analysis rule by a more conventional one:
```
```     5.1 --- a/src/HOLCF/Porder.thy	Wed Sep 26 19:19:38 2007 +0200
5.2 +++ b/src/HOLCF/Porder.thy	Wed Sep 26 20:27:55 2007 +0200
5.3 @@ -6,7 +6,7 @@
5.4  header {* Partial orders *}
5.5
5.6  theory Porder
5.7 -imports Finite_Set
5.8 +imports Datatype Finite_Set
5.9  begin
5.10
5.11  subsection {* Type class for partial orders *}
```