moved Finite_Set before Datatype
authorhaftmann
Wed Sep 26 20:27:55 2007 +0200 (2007-09-26)
changeset 24728e2b3a1065676
parent 24727 dd9ea6b72eb9
child 24729 f5015dd2431b
moved Finite_Set before Datatype
src/HOL/Datatype.thy
src/HOL/Equiv_Relations.thy
src/HOL/Finite_Set.thy
src/HOL/IntDef.thy
src/HOLCF/Porder.thy
     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.49 +apply(simp add:quotient_def)
    2.50 +apply(subst card_UN_disjoint)
    2.51 +   apply assumption
    2.52 +  apply simp
    2.53 + apply(fastsimp simp add:inj_on_def)
    2.54 +apply (simp add:setsum_constant)
    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.13  apply(simp add: neq_commute less_le)
    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.49 -apply(simp add:quotient_def)
    3.50 -apply(subst card_UN_disjoint)
    3.51 -   apply assumption
    3.52 -  apply simp
    3.53 - apply(fastsimp simp add:inj_on_def)
    3.54 -apply (simp add:setsum_constant)
    3.55 -done
    3.56 -
    3.57 -
    3.58 -subsection {* @{term setsum} and @{term setprod} on integers *}
    3.59 -
    3.60 -text {*By Jeremy Avigad*}
    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.17 +text {*By Jeremy Avigad*}
    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 *}