new material from Avigad, and simplified treatment of division by 0
authorpaulson
Thu Mar 04 12:06:07 2004 +0100 (2004-03-04)
changeset 144305cb24165a2e1
parent 14429 0fce2d8bce0f
child 14431 ade3d26e0caf
new material from Avigad, and simplified treatment of division by 0
src/HOL/Complex/CLim.thy
src/HOL/Complex/CStar.thy
src/HOL/Complex/Complex.thy
src/HOL/Complex/NSCA.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Divides.thy
src/HOL/Finite_Set.thy
src/HOL/HOL.thy
src/HOL/HOL_lemmas.ML
src/HOL/Hyperreal/EvenOdd.ML
src/HOL/Hyperreal/EvenOdd.thy
src/HOL/Hyperreal/HLog.thy
src/HOL/Hyperreal/HTranscendental.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/Log.thy
src/HOL/Hyperreal/MacLaurin.ML
src/HOL/Hyperreal/NSA.thy
src/HOL/Hyperreal/Transcendental.ML
src/HOL/Integ/IntDef.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/NatSimprocs.thy
src/HOL/Integ/Parity.thy
src/HOL/Integ/nat_simprocs.ML
src/HOL/IsaMakefile
src/HOL/NumberTheory/Finite2.thy
src/HOL/PreList.thy
src/HOL/Real/PReal.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Ring_and_Field.thy
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Complex/CLim.thy	Thu Mar 04 10:06:13 2004 +0100
     1.2 +++ b/src/HOL/Complex/CLim.thy	Thu Mar 04 12:06:07 2004 +0100
     1.3 @@ -858,8 +858,7 @@
     1.4  apply (simp (no_asm_simp))
     1.5  apply (rule capprox_mult_hcomplex_of_complex)
     1.6  apply (auto intro!: NSCDERIVD1 intro: capprox_minus_iff [THEN iffD2] 
     1.7 -            simp add: diff_minus [symmetric] 
     1.8 -                      divide_inverse_zero [symmetric])
     1.9 +            simp add: diff_minus [symmetric] divide_inverse [symmetric])
    1.10  apply (blast intro: NSCDERIVD2)
    1.11  done
    1.12  
    1.13 @@ -968,8 +967,10 @@
    1.14  apply (simp add: complex_diff_def)
    1.15  apply (drule_tac f = g in CDERIV_inverse_fun)
    1.16  apply (drule_tac [2] CDERIV_mult, assumption+)
    1.17 -apply (simp add: divide_inverse_zero right_distrib power_inverse minus_mult_left mult_ac 
    1.18 -            del: complexpow_Suc minus_mult_right [symmetric] minus_mult_left [symmetric])
    1.19 +apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left 
    1.20 +                 mult_ac 
    1.21 +            del: minus_mult_right [symmetric] minus_mult_left [symmetric]
    1.22 +                 complexpow_Suc)
    1.23  done
    1.24  
    1.25  lemma NSCDERIV_quotient:
     2.1 --- a/src/HOL/Complex/CStar.thy	Thu Mar 04 10:06:13 2004 +0100
     2.2 +++ b/src/HOL/Complex/CStar.thy	Thu Mar 04 12:06:07 2004 +0100
     2.3 @@ -489,18 +489,17 @@
     2.4  done
     2.5  
     2.6  lemma starfunC_divide: "( *fc* f) y  / ( *fc* g) y = ( *fc* (%x. f x / g x)) y"
     2.7 -by (simp add: divide_inverse_zero)
     2.8 +by (simp add: divide_inverse)
     2.9  declare starfunC_divide [symmetric, simp]
    2.10  
    2.11  lemma starfunCR_divide:
    2.12    "( *fcR* f) y  / ( *fcR* g) y = ( *fcR* (%x. f x / g x)) y"
    2.13 -by (simp add: divide_inverse_zero)
    2.14 +by (simp add: divide_inverse)
    2.15  declare starfunCR_divide [symmetric, simp]
    2.16  
    2.17  lemma starfunRC_divide:
    2.18    "( *fRc* f) y  / ( *fRc* g) y = ( *fRc* (%x. f x / g x)) y"
    2.19 -apply (simp add: divide_inverse_zero)
    2.20 -done
    2.21 +by (simp add: divide_inverse)
    2.22  declare starfunRC_divide [symmetric, simp]
    2.23  
    2.24  
     3.1 --- a/src/HOL/Complex/Complex.thy	Thu Mar 04 10:06:13 2004 +0100
     3.2 +++ b/src/HOL/Complex/Complex.thy	Thu Mar 04 12:06:07 2004 +0100
     3.3 @@ -1,4 +1,5 @@
     3.4  (*  Title:       Complex.thy
     3.5 +    ID:      $Id$
     3.6      Author:      Jacques D. Fleuriot
     3.7      Copyright:   2001 University of Edinburgh
     3.8      Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
     3.9 @@ -216,7 +217,7 @@
    3.10  apply (induct z)
    3.11  apply (rename_tac x y)
    3.12  apply (auto simp add: complex_mult complex_inverse complex_one_def
    3.13 -       complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
    3.14 +      complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
    3.15  apply (drule_tac y = y in real_sum_squares_not_zero)
    3.16  apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto)
    3.17  done
    3.18 @@ -248,20 +249,17 @@
    3.19    show "(u + v) * w = u * w + v * w"
    3.20      by (simp add: complex_mult_def complex_add_def left_distrib 
    3.21                    diff_minus add_ac)
    3.22 -  assume neq: "w \<noteq> 0"
    3.23 -  thus "z / w = z * inverse w"
    3.24 +  show "z / w = z * inverse w"
    3.25      by (simp add: complex_divide_def)
    3.26 -  show "inverse w * w = 1"
    3.27 -    by (simp add: neq complex_mult_inv_left)
    3.28 +  assume "w \<noteq> 0"
    3.29 +  thus "inverse w * w = 1"
    3.30 +    by (simp add: complex_mult_inv_left)
    3.31  qed
    3.32  
    3.33  instance complex :: division_by_zero
    3.34  proof
    3.35 -  show inv: "inverse 0 = (0::complex)"
    3.36 +  show "inverse 0 = (0::complex)"
    3.37      by (simp add: complex_inverse_def complex_zero_def)
    3.38 -  fix x :: complex
    3.39 -  show "x/0 = 0"
    3.40 -    by (simp add: complex_divide_def inv)
    3.41  qed
    3.42  
    3.43  
    3.44 @@ -789,7 +787,7 @@
    3.45                complex_diff_def)
    3.46  
    3.47  lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
    3.48 -by (simp add: divide_inverse_zero rcis_def complex_of_real_inverse)
    3.49 +by (simp add: divide_inverse rcis_def complex_of_real_inverse)
    3.50  
    3.51  lemma cis_divide: "cis a / cis b = cis (a - b)"
    3.52  by (simp add: complex_divide_def cis_mult real_diff_def)
     4.1 --- a/src/HOL/Complex/NSCA.thy	Thu Mar 04 10:06:13 2004 +0100
     4.2 +++ b/src/HOL/Complex/NSCA.thy	Thu Mar 04 12:06:07 2004 +0100
     4.3 @@ -56,7 +56,7 @@
     4.4  done
     4.5  
     4.6  lemma SComplex_divide: "[| x \<in> SComplex;  y \<in> SComplex |] ==> x/y \<in> SComplex"
     4.7 -by (simp add: SComplex_mult SComplex_inverse divide_inverse_zero)
     4.8 +by (simp add: SComplex_mult SComplex_inverse divide_inverse)
     4.9  
    4.10  lemma SComplex_minus: "x \<in> SComplex ==> -x \<in> SComplex"
    4.11  apply (simp add: SComplex_def)
    4.12 @@ -98,7 +98,7 @@
    4.13  
    4.14  lemma SComplex_divide_number_of:
    4.15       "r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex"
    4.16 -apply (simp only: divide_inverse_zero)
    4.17 +apply (simp only: divide_inverse)
    4.18  apply (blast intro!: SComplex_number_of SComplex_mult SComplex_inverse)
    4.19  done
    4.20  
    4.21 @@ -618,7 +618,7 @@
    4.22  lemma CInfinitesimal_ratio:
    4.23       "[| y \<noteq> 0;  y \<in> CInfinitesimal;  x/y \<in> CFinite |] ==> x \<in> CInfinitesimal"
    4.24  apply (drule CInfinitesimal_CFinite_mult2, assumption)
    4.25 -apply (simp add: divide_inverse_zero hcomplex_mult_assoc)
    4.26 +apply (simp add: divide_inverse hcomplex_mult_assoc)
    4.27  done
    4.28  
    4.29  lemma SComplex_capprox_iff:
    4.30 @@ -1126,7 +1126,7 @@
    4.31  lemma stc_divide [simp]:
    4.32       "[| x \<in> CFinite; y \<in> CFinite; stc y \<noteq> 0 |]  
    4.33        ==> stc(x/y) = (stc x) / (stc y)"
    4.34 -by (simp add: divide_inverse_zero stc_mult stc_not_CInfinitesimal CFinite_inverse stc_inverse)
    4.35 +by (simp add: divide_inverse stc_mult stc_not_CInfinitesimal CFinite_inverse stc_inverse)
    4.36  
    4.37  lemma stc_idempotent [simp]: "x \<in> CFinite ==> stc(stc(x)) = stc(x)"
    4.38  by (blast intro: stc_CFinite stc_capprox_self capprox_stc_eq)
     5.1 --- a/src/HOL/Complex/NSComplex.thy	Thu Mar 04 10:06:13 2004 +0100
     5.2 +++ b/src/HOL/Complex/NSComplex.thy	Thu Mar 04 12:06:07 2004 +0100
     5.3 @@ -1,9 +1,12 @@
     5.4  (*  Title:       NSComplex.thy
     5.5 +    ID:      $Id$
     5.6      Author:      Jacques D. Fleuriot
     5.7      Copyright:   2001  University of Edinburgh
     5.8 -    Description: Nonstandard Complex numbers
     5.9 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
    5.10  *)
    5.11  
    5.12 +header{*Nonstandard Complex Numbers*}
    5.13 +
    5.14  theory NSComplex = NSInduct:
    5.15  
    5.16  constdefs
    5.17 @@ -394,20 +397,17 @@
    5.18      by (rule hcomplex_zero_not_eq_one)
    5.19    show "(u + v) * w = u * w + v * w"
    5.20      by (simp add: hcomplex_add_mult_distrib)
    5.21 -  assume neq: "w \<noteq> 0"
    5.22 -  thus "z / w = z * inverse w"
    5.23 +  show "z / w = z * inverse w"
    5.24      by (simp add: hcomplex_divide_def)
    5.25 -  show "inverse w * w = 1"
    5.26 +  assume "w \<noteq> 0"
    5.27 +  thus "inverse w * w = 1"
    5.28      by (rule hcomplex_mult_inv_left)
    5.29  qed
    5.30  
    5.31  instance hcomplex :: division_by_zero
    5.32  proof
    5.33 -  show inv: "inverse 0 = (0::hcomplex)"
    5.34 +  show "inverse 0 = (0::hcomplex)"
    5.35      by (simp add: hcomplex_inverse hcomplex_zero_def)
    5.36 -  fix x :: hcomplex
    5.37 -  show "x/0 = 0"
    5.38 -    by (simp add: hcomplex_divide_def inv)
    5.39  qed
    5.40  
    5.41  
     6.1 --- a/src/HOL/Divides.thy	Thu Mar 04 10:06:13 2004 +0100
     6.2 +++ b/src/HOL/Divides.thy	Thu Mar 04 12:06:07 2004 +0100
     6.3 @@ -14,8 +14,6 @@
     6.4    div < type
     6.5  
     6.6  instance  nat :: div ..
     6.7 -instance  nat :: plus_ac0
     6.8 -proof qed (rule add_commute add_assoc add_0)+
     6.9  
    6.10  consts
    6.11    div  :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a"          (infixl 70)
     7.1 --- a/src/HOL/Finite_Set.thy	Thu Mar 04 10:06:13 2004 +0100
     7.2 +++ b/src/HOL/Finite_Set.thy	Thu Mar 04 12:06:07 2004 +0100
     7.3 @@ -1,6 +1,7 @@
     7.4  (*  Title:      HOL/Finite_Set.thy
     7.5      ID:         $Id$
     7.6      Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     7.7 +                Additions by Jeremy Avigad in Feb 2004
     7.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     7.9  *)
    7.10  
    7.11 @@ -8,6 +9,65 @@
    7.12  
    7.13  theory Finite_Set = Divides + Power + Inductive + SetInterval:
    7.14  
    7.15 +subsection {* Types Classes @{text plus_ac0} and @{text times_ac1} *}
    7.16 +
    7.17 +axclass plus_ac0 < plus, zero
    7.18 +  commute:     "x + y = y + x"
    7.19 +  assoc:       "(x + y) + z = x + (y + z)"
    7.20 +  zero [simp]: "0 + x = x"
    7.21 +
    7.22 +lemma plus_ac0_left_commute: "x + (y+z) = y + ((x+z)::'a::plus_ac0)"
    7.23 +apply (rule plus_ac0.commute [THEN trans])
    7.24 +apply (rule plus_ac0.assoc [THEN trans])
    7.25 +apply (rule plus_ac0.commute [THEN arg_cong])
    7.26 +done
    7.27 +
    7.28 +lemma plus_ac0_zero_right [simp]: "x + 0 = (x ::'a::plus_ac0)"
    7.29 +apply (rule plus_ac0.commute [THEN trans])
    7.30 +apply (rule plus_ac0.zero)
    7.31 +done
    7.32 +
    7.33 +lemmas plus_ac0 = plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute
    7.34 +                  plus_ac0.zero plus_ac0_zero_right
    7.35 +
    7.36 +instance semiring < plus_ac0
    7.37 +proof qed (rule add_commute add_assoc almost_semiring.add_0)+
    7.38 +
    7.39 +axclass times_ac1 < times, one
    7.40 +  commute: "x * y = y * x"
    7.41 +  assoc:   "(x * y) * z = x * (y * z)"
    7.42 +  one:    "1 * x = x"
    7.43 +
    7.44 +theorem times_ac1_left_commute: "(x::'a::times_ac1) * ((y::'a) * z) =
    7.45 +  y * (x * z)"
    7.46 +proof -
    7.47 +  have "(x::'a::times_ac1) * (y * z) = (x * y) * z"
    7.48 +    by (rule times_ac1.assoc [THEN sym])
    7.49 +  also have "x * y = y * x"
    7.50 +    by (rule times_ac1.commute)
    7.51 +  also have "(y * x) * z = y * (x * z)"
    7.52 +    by (rule times_ac1.assoc)
    7.53 +  finally show ?thesis .
    7.54 +qed
    7.55 +
    7.56 +theorem times_ac1_one_right: "(x::'a::times_ac1) * 1 = x"
    7.57 +proof -
    7.58 +  have "x * 1 = 1 * x"
    7.59 +    by (rule times_ac1.commute)
    7.60 +  also have "... = x"
    7.61 +    by (rule times_ac1.one)
    7.62 +  finally show ?thesis .
    7.63 +qed
    7.64 +
    7.65 +instance semiring < times_ac1
    7.66 +  apply intro_classes
    7.67 +  apply (rule mult_commute)
    7.68 +  apply (rule mult_assoc, simp)
    7.69 +  done
    7.70 +
    7.71 +theorems times_ac1 = times_ac1.assoc times_ac1.commute times_ac1_left_commute
    7.72 +  times_ac1.one times_ac1_one_right
    7.73 +
    7.74  subsection {* Collection of finite sets *}
    7.75  
    7.76  consts Finites :: "'a set set"
    7.77 @@ -25,8 +85,8 @@
    7.78    finite: "finite UNIV"
    7.79  
    7.80  lemma ex_new_if_finite: -- "does not depend on def of finite at all"
    7.81 - "\<lbrakk> ~finite(UNIV::'a set); finite A \<rbrakk> \<Longrightarrow> \<exists>a::'a. a ~: A"
    7.82 -by(subgoal_tac "A ~= UNIV", blast, blast)
    7.83 + "[| ~finite(UNIV::'a set); finite A  |] ==> \<exists>a::'a. a \<notin> A"
    7.84 +by(subgoal_tac "A \<noteq> UNIV", blast, blast)
    7.85  
    7.86  
    7.87  lemma finite_induct [case_names empty insert, induct set: Finites]:
    7.88 @@ -167,6 +227,11 @@
    7.89    -- {* The image of a finite set is finite. *}
    7.90    by (induct set: Finites) simp_all
    7.91  
    7.92 +lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
    7.93 +  apply (frule finite_imageI)
    7.94 +  apply (erule finite_subset, assumption)
    7.95 +  done
    7.96 +
    7.97  lemma finite_range_imageI:
    7.98      "finite (range g) ==> finite (range (%x. f (g x)))"
    7.99    apply (drule finite_imageI, simp)
   7.100 @@ -195,16 +260,16 @@
   7.101  lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
   7.102    -- {* The inverse image of a singleton under an injective function
   7.103           is included in a singleton. *}
   7.104 -  apply (auto simp add: inj_on_def) 
   7.105 -  apply (blast intro: the_equality [symmetric]) 
   7.106 +  apply (auto simp add: inj_on_def)
   7.107 +  apply (blast intro: the_equality [symmetric])
   7.108    done
   7.109  
   7.110  lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
   7.111    -- {* The inverse image of a finite set under an injective function
   7.112           is finite. *}
   7.113 -  apply (induct set: Finites, simp_all) 
   7.114 -  apply (subst vimage_insert) 
   7.115 -  apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
   7.116 +  apply (induct set: Finites, simp_all)
   7.117 +  apply (subst vimage_insert)
   7.118 +  apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
   7.119    done
   7.120  
   7.121  
   7.122 @@ -215,10 +280,10 @@
   7.123  
   7.124  text {*
   7.125    Strengthen RHS to
   7.126 -  @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x ~= {}})"}?
   7.127 +  @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
   7.128  
   7.129    We'd need to prove
   7.130 -  @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x ~= {}}"}
   7.131 +  @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
   7.132    by induction. *}
   7.133  
   7.134  lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
   7.135 @@ -281,6 +346,9 @@
   7.136    apply simp
   7.137    done
   7.138  
   7.139 +
   7.140 +subsubsection {* Intervals of nats *}
   7.141 +
   7.142  lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
   7.143    by (induct k) (simp_all add: lessThan_Suc)
   7.144  
   7.145 @@ -337,6 +405,10 @@
   7.146     apply (auto simp add: finite_Field)
   7.147    done
   7.148  
   7.149 +lemma finite_cartesian_product: "[| finite A; finite B |] ==>
   7.150 +    finite (A <*> B)"
   7.151 +  by (rule finite_SigmaI)
   7.152 +
   7.153  
   7.154  subsection {* Finite cardinality *}
   7.155  
   7.156 @@ -521,8 +593,7 @@
   7.157    done
   7.158  
   7.159  lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
   7.160 -  apply (induct set: Finites, simp_all, atomize)
   7.161 -  apply safe
   7.162 +  apply (induct set: Finites, simp_all, atomize, safe)
   7.163     apply (unfold inj_on_def, blast)
   7.164    apply (subst card_insert_disjoint)
   7.165      apply (erule finite_imageI, blast, blast)
   7.166 @@ -553,7 +624,7 @@
   7.167  lemma dvd_partition:
   7.168    "finite C ==> finite (Union C) ==>
   7.169      ALL c : C. k dvd card c ==>
   7.170 -    (ALL c1: C. ALL c2: C. c1 ~= c2 --> c1 Int c2 = {}) ==>
   7.171 +    (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
   7.172    k dvd card (Union C)"
   7.173    apply (induct set: Finites, simp_all, clarify)
   7.174    apply (subst card_Un_disjoint)
   7.175 @@ -784,10 +855,6 @@
   7.176    apply (erule finite_induct, auto)
   7.177    done
   7.178  
   7.179 -lemma setsum_eq_0_iff [simp]:
   7.180 -    "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   7.181 -  by (induct set: Finites) auto
   7.182 -
   7.183  lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   7.184    apply (case_tac "finite A")
   7.185     prefer 2 apply (simp add: setsum_def)
   7.186 @@ -825,6 +892,14 @@
   7.187    apply (simp add: setsum_Un_disjoint)
   7.188    done
   7.189  
   7.190 +lemma setsum_Union_disjoint:
   7.191 +  "finite C ==> (ALL A:C. finite A) ==>
   7.192 +        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
   7.193 +      setsum f (Union C) = setsum (setsum f) C"
   7.194 +  apply (frule setsum_UN_disjoint [of C id f])
   7.195 +  apply (unfold Union_def id_def, assumption+)
   7.196 +  done
   7.197 +
   7.198  lemma setsum_addf: "setsum (\<lambda>x. f x + g x) A = (setsum f A + setsum g A)"
   7.199    apply (case_tac "finite A")
   7.200     prefer 2 apply (simp add: setsum_def)
   7.201 @@ -832,21 +907,6 @@
   7.202    apply (simp add: plus_ac0)
   7.203    done
   7.204  
   7.205 -lemma setsum_Un: "finite A ==> finite B ==>
   7.206 -    (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   7.207 -  -- {* For the natural numbers, we have subtraction. *}
   7.208 -  apply (subst setsum_Un_Int [symmetric], auto)
   7.209 -  done
   7.210 -
   7.211 -lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
   7.212 -    (if a:A then setsum f A - f a else setsum f A)"
   7.213 -  apply (case_tac "finite A")
   7.214 -   prefer 2 apply (simp add: setsum_def)
   7.215 -  apply (erule finite_induct)
   7.216 -   apply (auto simp add: insert_Diff_if)
   7.217 -  apply (drule_tac a = a in mk_disjoint_insert, auto)
   7.218 -  done
   7.219 -
   7.220  lemma setsum_cong:
   7.221    "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   7.222    apply (case_tac "finite B")
   7.223 @@ -865,12 +925,356 @@
   7.224    apply (simp add: Ball_def del:insert_Diff_single)
   7.225    done
   7.226  
   7.227 -subsubsection{* Min and Max of finite linearly ordered sets *}
   7.228 +lemma card_UN_disjoint:
   7.229 +  fixes f :: "'a => 'b::plus_ac0"
   7.230 +  shows
   7.231 +    "finite I ==> (ALL i:I. finite (A i)) ==>
   7.232 +        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   7.233 +      card (UNION I A) = setsum (\<lambda>i. card (A i)) I"
   7.234 +  apply (subst card_eq_setsum)
   7.235 +  apply (subst finite_UN, assumption+)
   7.236 +  apply (subgoal_tac "setsum (\<lambda>i. card (A i)) I =
   7.237 +      setsum (%i. (setsum (%x. 1) (A i))) I")
   7.238 +  apply (erule ssubst)
   7.239 +  apply (erule setsum_UN_disjoint, assumption+)
   7.240 +  apply (rule setsum_cong)
   7.241 +  apply (simp, simp add: card_eq_setsum)
   7.242 +  done
   7.243 +
   7.244 +lemma card_Union_disjoint:
   7.245 +  "finite C ==> (ALL A:C. finite A) ==>
   7.246 +        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
   7.247 +      card (Union C) = setsum card C"
   7.248 +  apply (frule card_UN_disjoint [of C id])
   7.249 +  apply (unfold Union_def id_def, assumption+)
   7.250 +  done
   7.251 +
   7.252 +lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
   7.253 +  apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
   7.254 +  apply (erule ssubst, rule setsum_0)
   7.255 +  apply (rule setsum_cong, auto)
   7.256 +  done
   7.257 +
   7.258 +
   7.259 +subsubsection {* Reindexing sums *}
   7.260 +
   7.261 +lemma setsum_reindex [rule_format]: "finite B ==>
   7.262 +                  inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
   7.263 +apply (rule finite_induct, assumption, force)
   7.264 +apply (rule impI, auto)
   7.265 +apply (simp add: inj_on_def)
   7.266 +apply (subgoal_tac "f x \<notin> f ` F")
   7.267 +apply (subgoal_tac "finite (f ` F)")
   7.268 +apply (auto simp add: setsum_insert)
   7.269 +apply (simp add: inj_on_def)
   7.270 +  done
   7.271 +
   7.272 +lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
   7.273 +    setsum f B = setsum id (f ` B)"
   7.274 +by (auto simp add: setsum_reindex id_o)
   7.275 +
   7.276 +
   7.277 +subsubsection {* Properties in more restricted classes of structures *}
   7.278 +
   7.279 +lemma setsum_eq_0_iff [simp]:
   7.280 +    "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   7.281 +  by (induct set: Finites) auto
   7.282 +
   7.283 +lemma setsum_constant_nat:
   7.284 +    "finite A ==> (\<Sum>x: A. y) = (card A) * y"
   7.285 +  -- {* Later generalized to any semiring. *}
   7.286 +  by (erule finite_induct, auto)
   7.287 +
   7.288 +lemma setsum_Un: "finite A ==> finite B ==>
   7.289 +    (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   7.290 +  -- {* For the natural numbers, we have subtraction. *}
   7.291 +  by (subst setsum_Un_Int [symmetric], auto)
   7.292 +
   7.293 +lemma setsum_Un_ring: "finite A ==> finite B ==>
   7.294 +    (setsum f (A Un B) :: 'a :: ring) =
   7.295 +      setsum f A + setsum f B - setsum f (A Int B)"
   7.296 +  apply (subst setsum_Un_Int [symmetric], auto)
   7.297 +  apply (simp add: compare_rls)
   7.298 +  done
   7.299 +
   7.300 +lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
   7.301 +    (if a:A then setsum f A - f a else setsum f A)"
   7.302 +  apply (case_tac "finite A")
   7.303 +   prefer 2 apply (simp add: setsum_def)
   7.304 +  apply (erule finite_induct)
   7.305 +   apply (auto simp add: insert_Diff_if)
   7.306 +  apply (drule_tac a = a in mk_disjoint_insert, auto)
   7.307 +  done
   7.308 +
   7.309 +lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ring) A =
   7.310 +  - setsum f A"
   7.311 +  by (induct set: Finites, auto)
   7.312 +
   7.313 +lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ring) - g x) A =
   7.314 +  setsum f A - setsum g A"
   7.315 +  by (simp add: diff_minus setsum_addf setsum_negf)
   7.316 +
   7.317 +lemma setsum_nonneg: "[| finite A;
   7.318 +    \<forall>x \<in> A. (0::'a::ordered_semiring) \<le> f x |] ==>
   7.319 +    0 \<le>  setsum f A";
   7.320 +  apply (induct set: Finites, auto)
   7.321 +  apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
   7.322 +  apply (blast intro: add_mono)
   7.323 +  done
   7.324 +
   7.325 +subsubsection {* Cardinality of Sigma and Cartesian product *}
   7.326 +
   7.327 +lemma SigmaI_insert: "y \<notin> A ==>
   7.328 +  (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
   7.329 +  by auto
   7.330 +
   7.331 +lemma card_cartesian_product_singleton [simp]: "finite A ==>
   7.332 +    card({x} <*> A) = card(A)"
   7.333 +  apply (subgoal_tac "inj_on (%y .(x,y)) A")
   7.334 +  apply (frule card_image, assumption)
   7.335 +  apply (subgoal_tac "(Pair x ` A) = {x} <*> A")
   7.336 +  apply (auto simp add: inj_on_def)
   7.337 +  done
   7.338 +
   7.339 +lemma card_SigmaI [rule_format,simp]: "finite A ==>
   7.340 +  (ALL a:A. finite (B a)) -->
   7.341 +  card (SIGMA x: A. B x) = (\<Sum>a: A. card (B a))"
   7.342 +  apply (erule finite_induct, auto)
   7.343 +  apply (subst SigmaI_insert, assumption)
   7.344 +  apply (subst card_Un_disjoint)
   7.345 +  apply (auto intro: finite_SigmaI)
   7.346 +  done
   7.347 +
   7.348 +lemma card_cartesian_product [simp]: "[| finite A; finite B |] ==>
   7.349 +  card (A <*> B) = card(A) * card(B)"
   7.350 +  apply (subst card_SigmaI, assumption+)
   7.351 +  apply (simp add: setsum_constant_nat)
   7.352 +  done
   7.353 +
   7.354 +
   7.355 +subsection {* Generalized product over a set *}
   7.356 +
   7.357 +constdefs
   7.358 +  setprod :: "('a => 'b) => 'a set => 'b::times_ac1"
   7.359 +  "setprod f A == if finite A then fold (op * o f) 1 A else 1"
   7.360 +
   7.361 +syntax
   7.362 +  "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
   7.363 +                ("\<Prod>_:_. _" [0, 51, 10] 10)
   7.364 +
   7.365 +syntax (xsymbols)
   7.366 +  "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
   7.367 +                ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
   7.368 +translations
   7.369 +  "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
   7.370 +
   7.371 +
   7.372 +lemma setprod_empty [simp]: "setprod f {} = 1"
   7.373 +  by (auto simp add: setprod_def)
   7.374 +
   7.375 +lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
   7.376 +    setprod f (insert a A) = f a * setprod f A"
   7.377 +  by (auto simp add: setprod_def LC_def LC.fold_insert
   7.378 +      times_ac1_left_commute)
   7.379 +
   7.380 +lemma setprod_1: "setprod (\<lambda>i. 1) A = 1"
   7.381 +  apply (case_tac "finite A")
   7.382 +  apply (erule finite_induct, auto simp add: times_ac1)
   7.383 +  apply (simp add: setprod_def)
   7.384 +  done
   7.385 +
   7.386 +lemma setprod_Un_Int: "finite A ==> finite B
   7.387 +    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
   7.388 +  apply (induct set: Finites, simp)
   7.389 +  apply (simp add: times_ac1 insert_absorb)
   7.390 +  apply (simp add: times_ac1 Int_insert_left insert_absorb)
   7.391 +  done
   7.392 +
   7.393 +lemma setprod_Un_disjoint: "finite A ==> finite B
   7.394 +  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
   7.395 +  apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
   7.396 +  done
   7.397 +
   7.398 +lemma setprod_UN_disjoint:
   7.399 +  fixes f :: "'a => 'b::times_ac1"
   7.400 +  shows
   7.401 +    "finite I ==> (ALL i:I. finite (A i)) ==>
   7.402 +        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   7.403 +      setprod f (UNION I A) = setprod (\<lambda>i. setprod f (A i)) I"
   7.404 +  apply (induct set: Finites, simp, atomize)
   7.405 +  apply (subgoal_tac "ALL i:F. x \<noteq> i")
   7.406 +   prefer 2 apply blast
   7.407 +  apply (subgoal_tac "A x Int UNION F A = {}")
   7.408 +   prefer 2 apply blast
   7.409 +  apply (simp add: setprod_Un_disjoint)
   7.410 +  done
   7.411 +
   7.412 +lemma setprod_Union_disjoint:
   7.413 +  "finite C ==> (ALL A:C. finite A) ==>
   7.414 +        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
   7.415 +      setprod f (Union C) = setprod (setprod f) C"
   7.416 +  apply (frule setprod_UN_disjoint [of C id f])
   7.417 +  apply (unfold Union_def id_def, assumption+)
   7.418 +  done
   7.419 +
   7.420 +lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A =
   7.421 +    (setprod f A * setprod g A)"
   7.422 +  apply (case_tac "finite A")
   7.423 +   prefer 2 apply (simp add: setprod_def times_ac1)
   7.424 +  apply (erule finite_induct, auto)
   7.425 +  apply (simp add: times_ac1)
   7.426 +  apply (simp add: times_ac1)
   7.427 +  done
   7.428 +
   7.429 +lemma setprod_cong:
   7.430 +  "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
   7.431 +  apply (case_tac "finite B")
   7.432 +   prefer 2 apply (simp add: setprod_def, simp)
   7.433 +  apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setprod f C = setprod g C")
   7.434 +   apply simp
   7.435 +  apply (erule finite_induct, simp)
   7.436 +  apply (simp add: subset_insert_iff, clarify)
   7.437 +  apply (subgoal_tac "finite C")
   7.438 +   prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   7.439 +  apply (subgoal_tac "C = insert x (C - {x})")
   7.440 +   prefer 2 apply blast
   7.441 +  apply (erule ssubst)
   7.442 +  apply (drule spec)
   7.443 +  apply (erule (1) notE impE)
   7.444 +  apply (simp add: Ball_def del:insert_Diff_single)
   7.445 +  done
   7.446 +
   7.447 +lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
   7.448 +  apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
   7.449 +  apply (erule ssubst, rule setprod_1)
   7.450 +  apply (rule setprod_cong, auto)
   7.451 +  done
   7.452 +
   7.453 +
   7.454 +subsubsection {* Reindexing products *}
   7.455 +
   7.456 +lemma setprod_reindex [rule_format]: "finite B ==>
   7.457 +                  inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
   7.458 +apply (rule finite_induct, assumption, force)
   7.459 +apply (rule impI, auto)
   7.460 +apply (simp add: inj_on_def)
   7.461 +apply (subgoal_tac "f x \<notin> f ` F")
   7.462 +apply (subgoal_tac "finite (f ` F)")
   7.463 +apply (auto simp add: setprod_insert)
   7.464 +apply (simp add: inj_on_def)
   7.465 +  done
   7.466 +
   7.467 +lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
   7.468 +    setprod f B = setprod id (f ` B)"
   7.469 +by (auto simp add: setprod_reindex id_o)
   7.470 +
   7.471 +
   7.472 +subsubsection {* Properties in more restricted classes of structures *}
   7.473 +
   7.474 +lemma setprod_eq_1_iff [simp]:
   7.475 +    "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
   7.476 +  by (induct set: Finites) auto
   7.477 +
   7.478 +lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::ringpower)) =
   7.479 +    y^(card A)"
   7.480 +  apply (erule finite_induct)
   7.481 +  apply (auto simp add: power_Suc)
   7.482 +  done
   7.483 +
   7.484 +lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::semiring) ==>
   7.485 +    setprod f A = 0"
   7.486 +  apply (induct set: Finites, force, clarsimp)
   7.487 +  apply (erule disjE, auto)
   7.488 +  done
   7.489 +
   7.490 +lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_ring) \<le> f x)
   7.491 +     --> 0 \<le> setprod f A"
   7.492 +  apply (case_tac "finite A")
   7.493 +  apply (induct set: Finites, force, clarsimp)
   7.494 +  apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
   7.495 +  apply (rule mult_mono, assumption+)
   7.496 +  apply (auto simp add: setprod_def)
   7.497 +  done
   7.498 +
   7.499 +lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_ring) < f x)
   7.500 +     --> 0 < setprod f A"
   7.501 +  apply (case_tac "finite A")
   7.502 +  apply (induct set: Finites, force, clarsimp)
   7.503 +  apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
   7.504 +  apply (rule mult_strict_mono, assumption+)
   7.505 +  apply (auto simp add: setprod_def)
   7.506 +  done
   7.507 +
   7.508 +lemma setprod_nonzero [rule_format]:
   7.509 +    "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
   7.510 +      finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
   7.511 +  apply (erule finite_induct, auto)
   7.512 +  done
   7.513 +
   7.514 +lemma setprod_zero_eq:
   7.515 +    "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
   7.516 +     finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
   7.517 +  apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
   7.518 +  done
   7.519 +
   7.520 +lemma setprod_nonzero_field:
   7.521 +    "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
   7.522 +  apply (rule setprod_nonzero, auto)
   7.523 +  done
   7.524 +
   7.525 +lemma setprod_zero_eq_field:
   7.526 +    "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
   7.527 +  apply (rule setprod_zero_eq, auto)
   7.528 +  done
   7.529 +
   7.530 +lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
   7.531 +    (setprod f (A Un B) :: 'a ::{field})
   7.532 +      = setprod f A * setprod f B / setprod f (A Int B)"
   7.533 +  apply (subst setprod_Un_Int [symmetric], auto)
   7.534 +  apply (subgoal_tac "finite (A Int B)")
   7.535 +  apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
   7.536 +  apply (subst times_divide_eq_right [THEN sym], auto)
   7.537 +  done
   7.538 +
   7.539 +lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
   7.540 +    (setprod f (A - {a}) :: 'a :: {field}) =
   7.541 +      (if a:A then setprod f A / f a else setprod f A)"
   7.542 +  apply (erule finite_induct)
   7.543 +   apply (auto simp add: insert_Diff_if)
   7.544 +  apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
   7.545 +  apply (erule ssubst)
   7.546 +  apply (subst times_divide_eq_right [THEN sym])
   7.547 +  apply (auto simp add: mult_ac)
   7.548 +  done
   7.549 +
   7.550 +lemma setprod_inversef: "finite A ==>
   7.551 +    ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
   7.552 +      setprod (inverse \<circ> f) A = inverse (setprod f A)"
   7.553 +  apply (erule finite_induct)
   7.554 +  apply (simp, simp)
   7.555 +  done
   7.556 +
   7.557 +lemma setprod_dividef:
   7.558 +     "[|finite A;
   7.559 +        \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
   7.560 +      ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
   7.561 +  apply (subgoal_tac
   7.562 +         "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
   7.563 +  apply (erule ssubst)
   7.564 +  apply (subst divide_inverse)
   7.565 +  apply (subst setprod_timesf)
   7.566 +  apply (subst setprod_inversef, assumption+, rule refl)
   7.567 +  apply (rule setprod_cong, rule refl)
   7.568 +  apply (subst divide_inverse, auto)
   7.569 +  done
   7.570 +
   7.571 +
   7.572 +subsection{* Min and Max of finite linearly ordered sets *}
   7.573  
   7.574  text{* Seemed easier to define directly than via fold. *}
   7.575  
   7.576  lemma ex_Max: fixes S :: "('a::linorder)set"
   7.577 -  assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
   7.578 +  assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
   7.579  using fin
   7.580  proof (induct)
   7.581    case empty thus ?case by simp
   7.582 @@ -886,14 +1290,14 @@
   7.583      proof (cases)
   7.584        assume "x \<le> m" thus ?thesis using m by blast
   7.585      next
   7.586 -      assume "\<not> x \<le> m" thus ?thesis using m
   7.587 +      assume "~ x \<le> m" thus ?thesis using m
   7.588  	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
   7.589      qed
   7.590    qed
   7.591  qed
   7.592  
   7.593  lemma ex_Min: fixes S :: "('a::linorder)set"
   7.594 -  assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
   7.595 +  assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
   7.596  using fin
   7.597  proof (induct)
   7.598    case empty thus ?case by simp
   7.599 @@ -909,18 +1313,18 @@
   7.600      proof (cases)
   7.601        assume "m \<le> x" thus ?thesis using m by blast
   7.602      next
   7.603 -      assume "\<not> m \<le> x" thus ?thesis using m
   7.604 +      assume "~ m \<le> x" thus ?thesis using m
   7.605  	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
   7.606      qed
   7.607    qed
   7.608  qed
   7.609  
   7.610  constdefs
   7.611 - Min :: "('a::linorder)set \<Rightarrow> 'a"
   7.612 -"Min S  \<equiv>  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
   7.613 + Min :: "('a::linorder)set => 'a"
   7.614 +"Min S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
   7.615  
   7.616 - Max :: "('a::linorder)set \<Rightarrow> 'a"
   7.617 -"Max S  \<equiv>  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
   7.618 + Max :: "('a::linorder)set => 'a"
   7.619 +"Max S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
   7.620  
   7.621  lemma Min[simp]: assumes a: "finite S" "S \<noteq> {}"
   7.622                   shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
   7.623 @@ -946,6 +1350,7 @@
   7.624    qed
   7.625  qed
   7.626  
   7.627 +subsection {* Theorems about @{text "choose"} *}
   7.628  
   7.629  text {*
   7.630    \medskip Basic theorem about @{text "choose"}.  By Florian
   7.631 @@ -965,7 +1370,7 @@
   7.632    apply safe
   7.633     apply (auto intro: finite_subset [THEN card_insert_disjoint])
   7.634    apply (drule_tac x = "xa - {x}" in spec)
   7.635 -  apply (subgoal_tac "x ~: xa", auto)
   7.636 +  apply (subgoal_tac "x \<notin> xa", auto)
   7.637    apply (erule rev_mp, subst card_Diff_singleton)
   7.638    apply (auto intro: finite_subset)
   7.639    done
   7.640 @@ -974,8 +1379,8 @@
   7.641      "[|inj_on f A; f ` A \<subseteq> B; finite A; finite B |] ==> card A <= card B"
   7.642    by (auto intro: card_mono simp add: card_image [symmetric])
   7.643  
   7.644 -lemma card_bij_eq: 
   7.645 -    "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A; 
   7.646 +lemma card_bij_eq:
   7.647 +    "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
   7.648         finite A; finite B |] ==> card A = card B"
   7.649    by (auto intro: le_anti_sym card_inj_on_le)
   7.650  
     8.1 --- a/src/HOL/HOL.thy	Thu Mar 04 10:06:13 2004 +0100
     8.2 +++ b/src/HOL/HOL.thy	Thu Mar 04 12:06:07 2004 +0100
     8.3 @@ -197,11 +197,6 @@
     8.4  syntax (HTML output)
     8.5    abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
     8.6  
     8.7 -axclass plus_ac0 < plus, zero
     8.8 -  commute: "x + y = y + x"
     8.9 -  assoc:   "(x + y) + z = x + (y + z)"
    8.10 -  zero:    "0 + x = x"
    8.11 -
    8.12  
    8.13  subsection {* Theory and package setup *}
    8.14  
     9.1 --- a/src/HOL/HOL_lemmas.ML	Thu Mar 04 10:06:13 2004 +0100
     9.2 +++ b/src/HOL/HOL_lemmas.ML	Thu Mar 04 12:06:07 2004 +0100
     9.3 @@ -446,21 +446,6 @@
     9.4  by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ;
     9.5  qed "exCI";
     9.6  
     9.7 -Goal "x + (y+z) = y + ((x+z)::'a::plus_ac0)";
     9.8 -by (rtac (thm"plus_ac0.commute" RS trans) 1);
     9.9 -by (rtac (thm"plus_ac0.assoc" RS trans) 1);
    9.10 -by (rtac (thm"plus_ac0.commute" RS arg_cong) 1);
    9.11 -qed "plus_ac0_left_commute";
    9.12 -
    9.13 -Goal "x + 0 = (x ::'a::plus_ac0)";
    9.14 -by (rtac (thm"plus_ac0.commute" RS trans) 1);
    9.15 -by (rtac (thm"plus_ac0.zero") 1);
    9.16 -qed "plus_ac0_zero_right";
    9.17 -
    9.18 -bind_thms ("plus_ac0", [thm"plus_ac0.assoc", thm"plus_ac0.commute",
    9.19 -                        plus_ac0_left_commute,
    9.20 -                        thm"plus_ac0.zero", plus_ac0_zero_right]);
    9.21 -
    9.22  (* case distinction *)
    9.23  
    9.24  val [prem1,prem2] = Goal "[| P ==> Q; ~P ==> Q |] ==> Q";
    10.1 --- a/src/HOL/Hyperreal/EvenOdd.ML	Thu Mar 04 10:06:13 2004 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,366 +0,0 @@
    10.4 -(*  Title       : Even.ML
    10.5 -    Author      : Jacques D. Fleuriot  
    10.6 -    Copyright   : 1999  University of Edinburgh
    10.7 -    Description : Even numbers defined
    10.8 -*)
    10.9 -
   10.10 -Goal "even(Suc(Suc n)) = (even(n))";
   10.11 -by (Auto_tac);
   10.12 -qed "even_Suc_Suc";
   10.13 -Addsimps [even_Suc_Suc];
   10.14 -
   10.15 -Goal "(even(n)) = (~odd(n))";
   10.16 -by (induct_tac "n" 1);
   10.17 -by (Auto_tac);
   10.18 -qed "even_not_odd";
   10.19 -
   10.20 -Goal "(odd(n)) = (~even(n))";
   10.21 -by (simp_tac (simpset() addsimps [even_not_odd]) 1);
   10.22 -qed "odd_not_even";
   10.23 -
   10.24 -Goal "even(2*n)";
   10.25 -by (induct_tac "n" 1);
   10.26 -by (Auto_tac);
   10.27 -qed "even_mult_two";
   10.28 -Addsimps [even_mult_two];
   10.29 -
   10.30 -Goal "even(n*2)";
   10.31 -by (induct_tac "n" 1);
   10.32 -by (Auto_tac);
   10.33 -qed "even_mult_two'";
   10.34 -Addsimps [even_mult_two'];
   10.35 -
   10.36 -Goal "even(n + n)";
   10.37 -by (induct_tac "n" 1);
   10.38 -by (Auto_tac);
   10.39 -qed "even_sum_self";
   10.40 -Addsimps [even_sum_self];
   10.41 -
   10.42 -Goal "~odd(2*n)";
   10.43 -by (induct_tac "n" 1);
   10.44 -by Auto_tac;
   10.45 -qed "not_odd_self_mult2";
   10.46 -Addsimps [not_odd_self_mult2];
   10.47 -
   10.48 -Goal "~odd(n + n)";
   10.49 -by (induct_tac "n" 1);
   10.50 -by Auto_tac;
   10.51 -qed "not_odd_sum_self";
   10.52 -Addsimps [not_odd_sum_self];
   10.53 -
   10.54 -Goal "~even(Suc(n + n))";
   10.55 -by (induct_tac "n" 1);
   10.56 -by Auto_tac;
   10.57 -qed "not_even_Suc_sum_self";
   10.58 -Addsimps [not_even_Suc_sum_self];
   10.59 -
   10.60 -Goal "odd(Suc(2*n))";
   10.61 -by (induct_tac "n" 1);
   10.62 -by (Auto_tac);
   10.63 -qed "odd_mult_two_add_one";
   10.64 -Addsimps [odd_mult_two_add_one];
   10.65 -
   10.66 -Goal "odd(Suc(n + n))";
   10.67 -by (induct_tac "n" 1);
   10.68 -by (Auto_tac);
   10.69 -qed "odd_sum_Suc_self";
   10.70 -Addsimps [odd_sum_Suc_self];
   10.71 -
   10.72 -Goal "even(Suc n) = odd(n)";
   10.73 -by (induct_tac "n" 1);
   10.74 -by (Auto_tac);
   10.75 -qed "even_Suc_odd_iff";
   10.76 -
   10.77 -Goal "odd(Suc n) = even(n)";
   10.78 -by (induct_tac "n" 1);
   10.79 -by (Auto_tac);
   10.80 -qed "odd_Suc_even_iff";
   10.81 -
   10.82 -Goal "even n | odd n";
   10.83 -by (simp_tac (simpset() addsimps [even_not_odd]) 1);
   10.84 -qed "even_odd_disj";
   10.85 -
   10.86 -(* could be proved automatically before: spoiled by numeral arith! *)
   10.87 -Goal "EX m. (n = 2*m | n = Suc(2*m))";
   10.88 -by (induct_tac "n" 1 THEN Auto_tac);
   10.89 -by (res_inst_tac [("x","Suc m")] exI 1 THEN Auto_tac);
   10.90 -qed "nat_mult_two_Suc_disj";
   10.91 -
   10.92 -Goal "even(n) = (EX m. n = 2*m)";
   10.93 -by (cut_inst_tac [("n","n")] nat_mult_two_Suc_disj 1);
   10.94 -by (Auto_tac);
   10.95 -qed "even_mult_two_ex";
   10.96 -
   10.97 -Goal "odd(n) = (EX m. n = Suc (2*m))";
   10.98 -by (cut_inst_tac [("n","n")] nat_mult_two_Suc_disj 1);
   10.99 -by (Auto_tac);
  10.100 -qed "odd_Suc_mult_two_ex";
  10.101 -
  10.102 -Goal "even(n) ==> even(m*n)";
  10.103 -by (auto_tac (claset(),
  10.104 -              simpset() addsimps [add_mult_distrib2, even_mult_two_ex]));
  10.105 -qed "even_mult_even";
  10.106 -Addsimps [even_mult_even];
  10.107 -
  10.108 -Goal "(m + m) div 2 = (m::nat)";
  10.109 -by (arith_tac 1);
  10.110 -qed "div_add_self_two_is_m";
  10.111 -Addsimps [div_add_self_two_is_m];
  10.112 -
  10.113 -Goal "Suc(Suc(m*2)) div 2 = Suc m";
  10.114 -by (arith_tac 1);
  10.115 -qed "div_mult_self_Suc_Suc";
  10.116 -Addsimps [div_mult_self_Suc_Suc];
  10.117 -
  10.118 -Goal "Suc(Suc(2*m)) div 2 = Suc m";
  10.119 -by (arith_tac 1);
  10.120 -qed "div_mult_self_Suc_Suc2";
  10.121 -Addsimps [div_mult_self_Suc_Suc2];
  10.122 -
  10.123 -Goal "Suc(Suc(m + m)) div 2 = Suc m";
  10.124 -by (arith_tac 1);
  10.125 -qed "div_add_self_Suc_Suc";
  10.126 -Addsimps [div_add_self_Suc_Suc];
  10.127 -
  10.128 -Goal "~ even n ==> (Suc n) div 2 = Suc((n - 1) div 2)";
  10.129 -by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym,
  10.130 -    odd_Suc_mult_two_ex]));
  10.131 -qed "not_even_imp_Suc_Suc_diff_one_eq";
  10.132 -Addsimps [not_even_imp_Suc_Suc_diff_one_eq];
  10.133 -
  10.134 -Goal "even(m + n) = (even m = even n)";
  10.135 -by (induct_tac "m" 1);
  10.136 -by Auto_tac;
  10.137 -qed "even_add";
  10.138 -AddIffs [even_add];
  10.139 -
  10.140 -Goal "even(m * n) = (even m | even n)";
  10.141 -by (induct_tac "m" 1);
  10.142 -by Auto_tac;
  10.143 -qed "even_mult";
  10.144 -
  10.145 -Goal "even (m ^ n) = (even m & n ~= 0)";
  10.146 -by (induct_tac "n" 1);
  10.147 -by (auto_tac (claset(),simpset() addsimps [even_mult]));
  10.148 -qed "even_pow";
  10.149 -AddIffs [even_pow];
  10.150 -
  10.151 -Goal "odd(m + n) = (odd m ~= odd n)";
  10.152 -by (induct_tac "m" 1);
  10.153 -by Auto_tac;
  10.154 -qed "odd_add";
  10.155 -AddIffs [odd_add];
  10.156 -
  10.157 -Goal "odd(m * n) = (odd m & odd n)";
  10.158 -by (induct_tac "m" 1);
  10.159 -by Auto_tac;
  10.160 -qed "odd_mult";
  10.161 -AddIffs [odd_mult];
  10.162 -
  10.163 -Goal "odd (m ^ n) = (odd m | n = 0)";
  10.164 -by (induct_tac "n" 1);
  10.165 -by Auto_tac;
  10.166 -qed "odd_pow";
  10.167 -
  10.168 -Goal "0 < n --> ~even (n + n - 1)";
  10.169 -by (induct_tac "n" 1);
  10.170 -by Auto_tac;
  10.171 -qed_spec_mp "not_even_2n_minus_1";
  10.172 -Addsimps [not_even_2n_minus_1];
  10.173 -
  10.174 -Goal "Suc (2 * m) mod 2 = 1";
  10.175 -by (induct_tac "m" 1);
  10.176 -by (auto_tac (claset(),simpset() addsimps [mod_Suc]));
  10.177 -qed "mod_two_Suc_2m";
  10.178 -Addsimps [mod_two_Suc_2m];
  10.179 -
  10.180 -Goal "(Suc (Suc (2 * m)) div 2) = Suc m";
  10.181 -by (arith_tac 1);
  10.182 -qed "div_two_Suc_Suc_2m";
  10.183 -Addsimps [div_two_Suc_Suc_2m];
  10.184 -
  10.185 -Goal "even n ==> 2 * ((n + 1) div 2) = n";
  10.186 -by (auto_tac (claset(),simpset() addsimps [mult_div_cancel,
  10.187 -    even_mult_two_ex]));
  10.188 -qed "lemma_even_div";
  10.189 -Addsimps [lemma_even_div];
  10.190 -
  10.191 -Goal "~even n ==> 2 * ((n + 1) div 2) = Suc n";
  10.192 -by (auto_tac (claset(),simpset() addsimps [even_not_odd,
  10.193 -    odd_Suc_mult_two_ex]));
  10.194 -qed "lemma_not_even_div";
  10.195 -Addsimps [lemma_not_even_div];
  10.196 -
  10.197 -Goal "Suc n div 2 <= Suc (Suc n) div 2";
  10.198 -by (arith_tac 1);
  10.199 -qed "Suc_n_le_Suc_Suc_n_div_2";
  10.200 -Addsimps [Suc_n_le_Suc_Suc_n_div_2];
  10.201 -
  10.202 -Goal "(0::nat) < n --> 0 < (n + 1) div 2";
  10.203 -by (arith_tac 1);
  10.204 -qed_spec_mp "Suc_n_div_2_gt_zero";
  10.205 -Addsimps [Suc_n_div_2_gt_zero];
  10.206 -
  10.207 -Goal "0 < n & even n --> 1 < n";
  10.208 -by (induct_tac "n" 1);
  10.209 -by Auto_tac;
  10.210 -qed_spec_mp "even_gt_zero_gt_one_aux";
  10.211 -bind_thm ("even_gt_zero_gt_one",conjI RS even_gt_zero_gt_one_aux);
  10.212 -
  10.213 -(* more general *)
  10.214 -Goal "n div 2 <= (Suc n) div 2";
  10.215 -by (arith_tac 1);
  10.216 -qed "le_Suc_n_div_2";
  10.217 -Addsimps [le_Suc_n_div_2];
  10.218 -
  10.219 -Goal "(1::nat) < n --> 0 < n div 2";
  10.220 -by (arith_tac 1);
  10.221 -qed_spec_mp "div_2_gt_zero";
  10.222 -Addsimps [div_2_gt_zero];
  10.223 -
  10.224 -Goal "even n ==> (n + 1) div 2 = n div 2";
  10.225 -by (rtac (CLAIM "2 * x = 2 * y ==> x = (y::nat)") 1);
  10.226 -by (stac lemma_even_div 1);
  10.227 -by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex]));
  10.228 -qed "lemma_even_div2";
  10.229 -Addsimps [lemma_even_div2];
  10.230 -
  10.231 -Goal "~even n ==> (n + 1) div 2 = Suc (n div 2)";
  10.232 -by (rtac (CLAIM "2 * x = 2 * y ==> x = (y::nat)") 1);
  10.233 -by (stac lemma_not_even_div 1);
  10.234 -by (auto_tac (claset(),simpset() addsimps [even_not_odd,
  10.235 -    odd_Suc_mult_two_ex])); 
  10.236 -by (cut_inst_tac [("m","Suc(2*m)"),("n","2")] mod_div_equality 1); 
  10.237 -by Auto_tac; 
  10.238 -qed "lemma_not_even_div2";
  10.239 -Addsimps [lemma_not_even_div2];
  10.240 -
  10.241 -Goal "(Suc n) div 2 = 0 ==> even n";
  10.242 -by (rtac ccontr 1);
  10.243 -by (dtac lemma_not_even_div2 1 THEN Auto_tac);
  10.244 -qed "Suc_n_div_two_zero_even";
  10.245 -
  10.246 -Goal "0 < n ==> even n = (~ even(n - 1))";
  10.247 -by (case_tac "n" 1);
  10.248 -by Auto_tac;
  10.249 -qed "even_num_iff";
  10.250 -
  10.251 -Goal "0 < n ==> odd n = (~ odd(n - 1))";
  10.252 -by (case_tac "n" 1);
  10.253 -by Auto_tac;
  10.254 -qed "odd_num_iff";
  10.255 -
  10.256 -(* Some mod and div stuff *)
  10.257 -
  10.258 -Goal "n ~= (0::nat) ==> (m = m div n * n + m mod n) & m mod n < n";
  10.259 -by (auto_tac (claset() addIs [mod_less_divisor],simpset()));
  10.260 -qed "mod_div_eq_less";
  10.261 -
  10.262 -Goal "(k*n + m) mod n = m mod (n::nat)";
  10.263 -by (simp_tac (simpset() addsimps mult_ac @ add_ac) 1);
  10.264 -qed "mod_mult_self3";
  10.265 -Addsimps [mod_mult_self3];
  10.266 -
  10.267 -Goal "Suc (k*n + m) mod n = Suc m mod n";
  10.268 -by (rtac (CLAIM "Suc (m + n) = (m + Suc n)" RS ssubst) 1);
  10.269 -by (rtac mod_mult_self3 1);
  10.270 -qed "mod_mult_self4";
  10.271 -Addsimps [mod_mult_self4];
  10.272 -
  10.273 -Goal "Suc m mod n = Suc (m mod n) mod n";
  10.274 -by (cut_inst_tac [("d'","Suc (m mod n) mod n")] (CLAIM "EX d. d' = d") 1);
  10.275 -by (etac exE 1);
  10.276 -by (Asm_simp_tac 1);
  10.277 -by (res_inst_tac [("t","m"),("n1","n")] (mod_div_equality RS subst) 1);
  10.278 -by (auto_tac (claset(),simpset() delsimprocs [cancel_div_mod_proc]));
  10.279 -qed "mod_Suc_eq_Suc_mod";
  10.280 -
  10.281 -Goal "even n = (even (n mod 4))";
  10.282 -by (cut_inst_tac [("d'","(even (n mod 4))")] (CLAIM "EX d. d' = d") 1);
  10.283 -by (etac exE 1);
  10.284 -by (Asm_simp_tac 1);
  10.285 -by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
  10.286 -by (auto_tac (claset(),simpset() addsimps [even_mult,even_num_iff] delsimprocs [cancel_div_mod_proc]));
  10.287 -qed "even_even_mod_4_iff";
  10.288 -
  10.289 -Goal "odd n = (odd (n mod 4))";
  10.290 -by (auto_tac (claset(),simpset() addsimps [odd_not_even,
  10.291 -    even_even_mod_4_iff RS sym]));
  10.292 -qed "odd_odd_mod_4_iff";
  10.293 -
  10.294 -Goal "odd n ==> ((-1) ^ n) = (-1::real)";
  10.295 -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
  10.296 -qed "odd_realpow_minus_one";
  10.297 -Addsimps [odd_realpow_minus_one];
  10.298 -
  10.299 -Goal "even(4*n)";
  10.300 -by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex]));
  10.301 -qed "even_4n";
  10.302 -Addsimps [even_4n];
  10.303 -
  10.304 -Goal "n mod 4 = 0 ==> even(n div 2)";
  10.305 -by Auto_tac;
  10.306 -qed "lemma_even_div_2";
  10.307 -
  10.308 -Goal "n mod 4 = 0 ==> even(n)";
  10.309 -by Auto_tac;
  10.310 -qed "lemma_mod_4_even_n";
  10.311 -
  10.312 -Goal "n mod 4 = 1 ==> odd(n)";
  10.313 -by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
  10.314 -by (auto_tac (claset(),simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]));
  10.315 -qed "lemma_mod_4_odd_n";
  10.316 -
  10.317 -Goal "n mod 4 = 2 ==> even(n)";
  10.318 -by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
  10.319 -by (auto_tac (claset(),simpset() addsimps [even_num_iff] delsimprocs [cancel_div_mod_proc]));
  10.320 -qed "lemma_mod_4_even_n2";
  10.321 -
  10.322 -Goal "n mod 4 = 3 ==> odd(n)";
  10.323 -by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
  10.324 -by (auto_tac (claset(),simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]));
  10.325 -qed "lemma_mod_4_odd_n2";
  10.326 -
  10.327 -Goal "even n ==> ((-1) ^ n) = (1::real)";
  10.328 -by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex]));
  10.329 -qed "even_realpow_minus_one";
  10.330 -Addsimps [even_realpow_minus_one];
  10.331 -
  10.332 -Goal "((4 * n) + 2) div 2 = (2::nat) * n + 1";
  10.333 -by (arith_tac 1);
  10.334 -qed "lemma_4n_add_2_div_2_eq";
  10.335 -Addsimps [lemma_4n_add_2_div_2_eq];
  10.336 -
  10.337 -Goal "(Suc(Suc(4 * n))) div 2 = (2::nat) * n + 1";
  10.338 -by (arith_tac 1);
  10.339 -qed "lemma_Suc_Suc_4n_div_2_eq";
  10.340 -Addsimps [lemma_Suc_Suc_4n_div_2_eq];
  10.341 -
  10.342 -Goal "(Suc(Suc(n * 4))) div 2 = (2::nat) * n + 1";
  10.343 -by (arith_tac 1);
  10.344 -qed "lemma_Suc_Suc_4n_div_2_eq2";
  10.345 -Addsimps [lemma_Suc_Suc_4n_div_2_eq2];
  10.346 -
  10.347 -Goal "n mod 4 = 3 ==> odd((n - 1) div 2)";
  10.348 -by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
  10.349 -by (asm_full_simp_tac (simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]) 1);
  10.350 -val lemma_odd_mod_4_div_2 = result();
  10.351 -
  10.352 -Goal "(4 * n) div 2 = (2::nat) * n";
  10.353 -by (arith_tac 1);
  10.354 -qed "lemma_4n_div_2_eq";
  10.355 -Addsimps [lemma_4n_div_2_eq];
  10.356 -
  10.357 -Goal "(n  * 4) div 2 = (2::nat) * n";
  10.358 -by (arith_tac 1);
  10.359 -qed "lemma_4n_div_2_eq2";
  10.360 -Addsimps [lemma_4n_div_2_eq2];
  10.361 -
  10.362 -Goal "n mod 4 = 1 ==> even ((n - 1) div 2)";
  10.363 -by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
  10.364 -by (dtac ssubst 1 THEN assume_tac 2);
  10.365 -by (rtac ((CLAIM "(n::nat) + 1 - 1 = n") RS ssubst) 1);
  10.366 -by Auto_tac;
  10.367 -val lemma_even_mod_4_div_2 = result();
  10.368 -
  10.369 -
    11.1 --- a/src/HOL/Hyperreal/EvenOdd.thy	Thu Mar 04 10:06:13 2004 +0100
    11.2 +++ b/src/HOL/Hyperreal/EvenOdd.thy	Thu Mar 04 12:06:07 2004 +0100
    11.3 @@ -4,17 +4,163 @@
    11.4      Description : Even and odd numbers defined 
    11.5  *)
    11.6  
    11.7 -EvenOdd = NthRoot +  
    11.8 +header{*Compatibility file from Parity*}
    11.9 +
   11.10 +theory EvenOdd = NthRoot:
   11.11 +
   11.12 +subsection{*General Lemmas About Division*}
   11.13 +
   11.14 +lemma div_add_self_two_is_m: "(m + m) div 2 = (m::nat)"
   11.15 +by arith
   11.16 +declare div_add_self_two_is_m [simp]
   11.17 +
   11.18 +lemma div_mult_self_Suc_Suc: "Suc(Suc(m*2)) div 2 = Suc m"
   11.19 +by arith
   11.20 +declare div_mult_self_Suc_Suc [simp]
   11.21 +
   11.22 +lemma div_mult_self_Suc_Suc2: "Suc(Suc(2*m)) div 2 = Suc m"
   11.23 +by arith
   11.24 +declare div_mult_self_Suc_Suc2 [simp]
   11.25 +
   11.26 +lemma div_add_self_Suc_Suc: "Suc(Suc(m + m)) div 2 = Suc m"
   11.27 +by arith
   11.28 +declare div_add_self_Suc_Suc [simp]
   11.29 +
   11.30 +lemma mod_two_Suc_2m: "Suc (2 * m) mod 2 = 1" 
   11.31 +apply (induct_tac "m")
   11.32 +apply (auto simp add: mod_Suc)
   11.33 +done
   11.34 +declare mod_two_Suc_2m [simp]
   11.35 +
   11.36 +lemma Suc_n_le_Suc_Suc_n_div_2: "Suc n div 2 \<le> Suc (Suc n) div 2"
   11.37 +by arith
   11.38 +declare Suc_n_le_Suc_Suc_n_div_2 [simp]
   11.39 +
   11.40 +lemma Suc_n_div_2_gt_zero: "(0::nat) < n ==> 0 < (n + 1) div 2"
   11.41 +by arith
   11.42 +declare Suc_n_div_2_gt_zero [simp]
   11.43 +
   11.44 +lemma le_Suc_n_div_2: "n div 2 \<le> (Suc n) div 2"
   11.45 +by arith
   11.46 +declare le_Suc_n_div_2 [simp]
   11.47 +
   11.48 +lemma div_2_gt_zero: "(1::nat) < n ==> 0 < n div 2" 
   11.49 +by arith
   11.50 +declare div_2_gt_zero [simp]
   11.51 +
   11.52 +lemma mod_mult_self3: "(k*n + m) mod n = m mod (n::nat)"
   11.53 +by (simp add: mult_ac add_ac)
   11.54 +declare mod_mult_self3 [simp]
   11.55 +
   11.56 +lemma mod_mult_self4: "Suc (k*n + m) mod n = Suc m mod n"
   11.57 +proof -
   11.58 +  have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
   11.59 +  also have "... = Suc m mod n" by (rule mod_mult_self3) 
   11.60 +  finally show ?thesis .
   11.61 +qed
   11.62 +declare mod_mult_self4 [simp]
   11.63 +
   11.64 +lemma nat_mod_idem [simp]: "m mod n mod n = (m mod n :: nat)"
   11.65 +by (case_tac "n=0", auto)
   11.66 +
   11.67 +lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
   11.68 +apply (subst mod_Suc [of m]) 
   11.69 +apply (subst mod_Suc [of "m mod n"], simp) 
   11.70 +done
   11.71 +
   11.72 +lemma lemma_4n_add_2_div_2_eq: "((4 * n) + 2) div 2 = (2::nat) * n + 1"
   11.73 +by arith
   11.74 +declare lemma_4n_add_2_div_2_eq [simp]
   11.75 +
   11.76 +lemma lemma_Suc_Suc_4n_div_2_eq: "(Suc(Suc(4 * n))) div 2 = (2::nat) * n + 1"
   11.77 +by arith
   11.78 +declare lemma_Suc_Suc_4n_div_2_eq [simp]
   11.79 +
   11.80 +lemma lemma_Suc_Suc_4n_div_2_eq2: "(Suc(Suc(n * 4))) div 2 = (2::nat) * n + 1"
   11.81 +by arith
   11.82 +declare lemma_Suc_Suc_4n_div_2_eq2 [simp]
   11.83 +
   11.84  
   11.85 -consts even :: "nat => bool"
   11.86 -primrec 
   11.87 -   even_0   "even 0 = True"
   11.88 -   even_Suc "even (Suc n) = (~ (even n))"    
   11.89 +subsection{*More Even/Odd Results*}
   11.90 + 
   11.91 +lemma even_mult_two_ex: "even(n) = (EX m::nat. n = 2*m)"
   11.92 +by (simp add: even_nat_equiv_def2 numeral_2_eq_2)
   11.93 +
   11.94 +lemma odd_Suc_mult_two_ex: "odd(n) = (EX m. n = Suc (2*m))"
   11.95 +by (simp add: odd_nat_equiv_def2 numeral_2_eq_2)
   11.96 +
   11.97 +lemma even_add: "even(m + n::nat) = (even m = even n)"
   11.98 +by auto
   11.99 +declare even_add [iff]
  11.100 +
  11.101 +lemma odd_add: "odd(m + n::nat) = (odd m ~= odd n)"
  11.102 +by auto
  11.103 +declare odd_add [iff]
  11.104 +
  11.105 +lemma lemma_even_div2: "even (n::nat) ==> (n + 1) div 2 = n div 2"
  11.106 +apply (simp add: numeral_2_eq_2) 
  11.107 +apply (subst div_Suc)  
  11.108 +apply (simp add: even_nat_mod_two_eq_zero) 
  11.109 +done
  11.110 +declare lemma_even_div2 [simp]
  11.111 +
  11.112 +lemma lemma_not_even_div2: "~even n ==> (n + 1) div 2 = Suc (n div 2)"
  11.113 +apply (simp add: numeral_2_eq_2) 
  11.114 +apply (subst div_Suc)  
  11.115 +apply (simp add: odd_nat_mod_two_eq_one) 
  11.116 +done
  11.117 +declare lemma_not_even_div2 [simp]
  11.118 +
  11.119 +lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))" 
  11.120 +by (case_tac "n", auto)
  11.121 +
  11.122 +lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)"
  11.123 +apply (induct n, simp)
  11.124 +apply (subst mod_Suc, simp) 
  11.125 +done
  11.126  
  11.127 -consts odd :: "nat => bool"
  11.128 -primrec 
  11.129 -   odd_0   "odd 0 = False"
  11.130 -   odd_Suc "odd (Suc n) = (~ (odd n))"    
  11.131 +declare neg_one_odd_power [simp]
  11.132 +declare neg_one_even_power [simp]
  11.133 +
  11.134 +lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)"
  11.135 +apply (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst])
  11.136 +apply (simp add: even_num_iff)
  11.137 +done
  11.138 +
  11.139 +lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
  11.140 +by (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst], simp)
  11.141 +
  11.142 +ML
  11.143 +{*
  11.144 +val even_Suc = thm"Parity.even_nat_suc";
  11.145 +
  11.146 +val even_mult_two_ex = thm "even_mult_two_ex";
  11.147 +val odd_Suc_mult_two_ex = thm "odd_Suc_mult_two_ex";
  11.148 +val div_add_self_two_is_m = thm "div_add_self_two_is_m";
  11.149 +val div_mult_self_Suc_Suc = thm "div_mult_self_Suc_Suc";
  11.150 +val div_mult_self_Suc_Suc2 = thm "div_mult_self_Suc_Suc2";
  11.151 +val div_add_self_Suc_Suc = thm "div_add_self_Suc_Suc";
  11.152 +val even_add = thm "even_add";
  11.153 +val odd_add = thm "odd_add";
  11.154 +val mod_two_Suc_2m = thm "mod_two_Suc_2m";
  11.155 +val Suc_n_le_Suc_Suc_n_div_2 = thm "Suc_n_le_Suc_Suc_n_div_2";
  11.156 +val Suc_n_div_2_gt_zero = thm "Suc_n_div_2_gt_zero";
  11.157 +val le_Suc_n_div_2 = thm "le_Suc_n_div_2";
  11.158 +val div_2_gt_zero = thm "div_2_gt_zero";
  11.159 +val lemma_even_div2 = thm "lemma_even_div2";
  11.160 +val lemma_not_even_div2 = thm "lemma_not_even_div2";
  11.161 +val even_num_iff = thm "even_num_iff";
  11.162 +val mod_mult_self3 = thm "mod_mult_self3";
  11.163 +val mod_mult_self4 = thm "mod_mult_self4";
  11.164 +val nat_mod_idem = thm "nat_mod_idem";
  11.165 +val mod_Suc_eq_Suc_mod = thm "mod_Suc_eq_Suc_mod";
  11.166 +val even_even_mod_4_iff = thm "even_even_mod_4_iff";
  11.167 +val lemma_4n_add_2_div_2_eq = thm "lemma_4n_add_2_div_2_eq";
  11.168 +val lemma_Suc_Suc_4n_div_2_eq = thm "lemma_Suc_Suc_4n_div_2_eq";
  11.169 +val lemma_Suc_Suc_4n_div_2_eq2 = thm "lemma_Suc_Suc_4n_div_2_eq2";
  11.170 +val lemma_odd_mod_4_div_2 = thm "lemma_odd_mod_4_div_2";
  11.171 +val lemma_even_mod_4_div_2 = thm "lemma_even_mod_4_div_2";
  11.172 +*}
  11.173  
  11.174  end
  11.175  
    12.1 --- a/src/HOL/Hyperreal/HLog.thy	Thu Mar 04 10:06:13 2004 +0100
    12.2 +++ b/src/HOL/Hyperreal/HLog.thy	Thu Mar 04 12:06:07 2004 +0100
    12.3 @@ -57,7 +57,7 @@
    12.4  lemma hypreal_divide: 
    12.5       "(Abs_hypreal(hyprel `` {X}))/(Abs_hypreal(hyprel `` {Y})) =  
    12.6        (Abs_hypreal(hyprel `` {%n. (X n)/(Y n)}))"
    12.7 -by (simp add: divide_inverse_zero hypreal_zero_num hypreal_inverse hypreal_mult) 
    12.8 +by (simp add: divide_inverse hypreal_zero_num hypreal_inverse hypreal_mult) 
    12.9  
   12.10  lemma powhr_divide:
   12.11       "[| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
   12.12 @@ -96,7 +96,7 @@
   12.13  done
   12.14  
   12.15  lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
   12.16 -by (simp add: divide_inverse_zero powhr_minus)
   12.17 +by (simp add: divide_inverse powhr_minus)
   12.18  
   12.19  lemma powhr_less_mono: "[| a < b; 1 < x |] ==> x powhr a < x powhr b"
   12.20  apply (rule eq_Abs_hypreal [of x])
   12.21 @@ -194,7 +194,7 @@
   12.22  apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
   12.23              HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 
   12.24          simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero 
   12.25 -          hlog_as_starfun hypreal_not_refl2 [THEN not_sym] divide_inverse_zero)
   12.26 +          hlog_as_starfun hypreal_not_refl2 [THEN not_sym] divide_inverse)
   12.27  done
   12.28  
   12.29  lemma hlog_HInfinite_as_starfun:
   12.30 @@ -220,7 +220,7 @@
   12.31  
   12.32  lemma hlog_divide:
   12.33       "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y"
   12.34 -by (simp add: hlog_mult hlog_inverse divide_inverse_zero)
   12.35 +by (simp add: hlog_mult hlog_inverse divide_inverse)
   12.36  
   12.37  lemma hlog_less_cancel_iff [simp]:
   12.38       "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
    13.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Thu Mar 04 10:06:13 2004 +0100
    13.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu Mar 04 12:06:07 2004 +0100
    13.3 @@ -555,13 +555,13 @@
    13.4       "n \<in> HNatInfinite  
    13.5        ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
    13.6  apply (frule lemma_sin_pi)
    13.7 -apply (simp add: divide_inverse_zero)
    13.8 +apply (simp add: divide_inverse)
    13.9  done
   13.10  
   13.11  lemma Infinitesimal_pi_divide_HNatInfinite: 
   13.12       "N \<in> HNatInfinite  
   13.13        ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
   13.14 -apply (simp add: divide_inverse_zero)
   13.15 +apply (simp add: divide_inverse)
   13.16  apply (auto intro: Infinitesimal_HFinite_mult2)
   13.17  done
   13.18  
   13.19 @@ -578,7 +578,7 @@
   13.20                     pi_divide_HNatInfinite_not_zero])
   13.21  apply (auto simp add: hypreal_inverse_distrib)
   13.22  apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
   13.23 -apply (auto intro: SReal_inverse simp add: divide_inverse_zero mult_ac)
   13.24 +apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac)
   13.25  done
   13.26  
   13.27  lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
   13.28 @@ -593,7 +593,7 @@
   13.29  lemma starfunNat_pi_divide_n_Infinitesimal: 
   13.30       "N \<in> HNatInfinite ==> ( *fNat* (%x. pi / real x)) N \<in> Infinitesimal"
   13.31  by (auto intro!: Infinitesimal_HFinite_mult2 
   13.32 -         simp add: starfunNat_mult [symmetric] divide_inverse_zero
   13.33 +         simp add: starfunNat_mult [symmetric] divide_inverse
   13.34                     starfunNat_inverse [symmetric] starfunNat_real_of_nat)
   13.35  
   13.36  lemma STAR_sin_pi_divide_n_approx:
   13.37 @@ -601,16 +601,16 @@
   13.38        ( *f* sin) (( *fNat* (%x. pi / real x)) N) @=  
   13.39        hypreal_of_real pi/(hypreal_of_hypnat N)"
   13.40  by (auto intro!: STAR_sin_Infinitesimal Infinitesimal_HFinite_mult2 
   13.41 -         simp add: starfunNat_mult [symmetric] divide_inverse_zero
   13.42 +         simp add: starfunNat_mult [symmetric] divide_inverse
   13.43                     starfunNat_inverse_real_of_nat_eq)
   13.44  
   13.45  lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi"
   13.46  apply (auto simp add: NSLIMSEQ_def starfunNat_mult [symmetric] starfunNat_real_of_nat)
   13.47  apply (rule_tac f1 = sin in starfun_stafunNat_o2 [THEN subst])
   13.48 -apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse_zero)
   13.49 +apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse)
   13.50  apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
   13.51  apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi 
   13.52 -            simp add: starfunNat_real_of_nat mult_commute divide_inverse_zero)
   13.53 +            simp add: starfunNat_real_of_nat mult_commute divide_inverse)
   13.54  done
   13.55  
   13.56  lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1"
   13.57 @@ -618,7 +618,7 @@
   13.58  apply (rule_tac f1 = cos in starfun_stafunNat_o2 [THEN subst])
   13.59  apply (rule STAR_cos_Infinitesimal)
   13.60  apply (auto intro!: Infinitesimal_HFinite_mult2 
   13.61 -            simp add: starfunNat_mult [symmetric] divide_inverse_zero
   13.62 +            simp add: starfunNat_mult [symmetric] divide_inverse
   13.63                        starfunNat_inverse [symmetric] starfunNat_real_of_nat)
   13.64  done
   13.65  
    14.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Thu Mar 04 10:06:13 2004 +0100
    14.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Mar 04 12:06:07 2004 +0100
    14.3 @@ -476,17 +476,14 @@
    14.4    show "(x + y) * z = x * z + y * z" by (simp add: hypreal_add_mult_distrib)
    14.5    show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
    14.6    show "x \<noteq> 0 ==> inverse x * x = 1" by (simp add: hypreal_mult_inverse_left)
    14.7 -  show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
    14.8 +  show "x / y = x * inverse y" by (simp add: hypreal_divide_def)
    14.9  qed
   14.10  
   14.11  
   14.12  instance hypreal :: division_by_zero
   14.13  proof
   14.14 -  fix x :: hypreal
   14.15 -  show inv: "inverse 0 = (0::hypreal)" 
   14.16 +  show "inverse 0 = (0::hypreal)" 
   14.17      by (simp add: hypreal_inverse hypreal_zero_def)
   14.18 -  show "x/0 = 0" 
   14.19 -    by (simp add: hypreal_divide_def inv hypreal_mult_commute [of a])
   14.20  qed
   14.21  
   14.22  
    15.1 --- a/src/HOL/Hyperreal/Log.thy	Thu Mar 04 10:06:13 2004 +0100
    15.2 +++ b/src/HOL/Hyperreal/Log.thy	Thu Mar 04 12:06:07 2004 +0100
    15.3 @@ -41,7 +41,7 @@
    15.4  
    15.5  lemma powr_divide:
    15.6       "[| 0 < x; 0 < y |] ==> (x / y) powr a = (x powr a)/(y powr a)"
    15.7 -apply (simp add: divide_inverse_zero positive_imp_inverse_positive powr_mult)
    15.8 +apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
    15.9  apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
   15.10  done
   15.11  
   15.12 @@ -58,7 +58,7 @@
   15.13  by (simp add: powr_def exp_minus [symmetric])
   15.14  
   15.15  lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
   15.16 -by (simp add: divide_inverse_zero powr_minus)
   15.17 +by (simp add: divide_inverse powr_minus)
   15.18  
   15.19  lemma powr_less_mono: "[| a < b; 1 < x |] ==> x powr a < x powr b"
   15.20  by (simp add: powr_def)
   15.21 @@ -85,12 +85,12 @@
   15.22  lemma log_mult: 
   15.23       "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]  
   15.24        ==> log a (x * y) = log a x + log a y"
   15.25 -by (simp add: log_def ln_mult divide_inverse_zero left_distrib)
   15.26 +by (simp add: log_def ln_mult divide_inverse left_distrib)
   15.27  
   15.28  lemma log_eq_div_ln_mult_log: 
   15.29       "[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
   15.30        ==> log a x = (ln b/ln a) * log b x"
   15.31 -by (simp add: log_def divide_inverse_zero)
   15.32 +by (simp add: log_def divide_inverse)
   15.33  
   15.34  text{*Base 10 logarithms*}
   15.35  lemma log_base_10_eq1: "0 < x ==> log 10 x = (ln (exp 1) / ln 10) * ln x"
   15.36 @@ -113,7 +113,7 @@
   15.37  
   15.38  lemma log_divide:
   15.39       "[|0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> log a (x/y) = log a x - log a y"
   15.40 -by (simp add: log_mult divide_inverse_zero log_inverse)
   15.41 +by (simp add: log_mult divide_inverse log_inverse)
   15.42  
   15.43  lemma log_less_cancel_iff [simp]:
   15.44       "[| 1 < a; 0 < x; 0 < y |] ==> (log a x < log a y) = (x < y)"
    16.1 --- a/src/HOL/Hyperreal/MacLaurin.ML	Thu Mar 04 10:06:13 2004 +0100
    16.2 +++ b/src/HOL/Hyperreal/MacLaurin.ML	Thu Mar 04 12:06:07 2004 +0100
    16.3 @@ -535,9 +535,9 @@
    16.4  by (res_inst_tac [("x","t")] exI 1);
    16.5  by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
    16.6  by (rtac sumr_fun_eq 1);
    16.7 -by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
    16.8 -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
    16.9 -    even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
   16.10 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
   16.11 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
   16.12 +(*Could sin_zero_iff help?*)
   16.13  qed "Maclaurin_sin_expansion";
   16.14  
   16.15  Goal "EX t. abs t <= abs x &  \
   16.16 @@ -566,9 +566,8 @@
   16.17  by (arith_tac 1);
   16.18  by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
   16.19  by (rtac sumr_fun_eq 1);
   16.20 -by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
   16.21 -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
   16.22 -    even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
   16.23 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
   16.24 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
   16.25  qed "Maclaurin_sin_expansion2";
   16.26  
   16.27  Goal "[| 0 < n; 0 < x |] ==> \
   16.28 @@ -590,9 +589,8 @@
   16.29  by (assume_tac 1 THEN assume_tac 1);
   16.30  by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
   16.31  by (rtac sumr_fun_eq 1);
   16.32 -by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
   16.33 -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
   16.34 -    even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
   16.35 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
   16.36 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
   16.37  qed "Maclaurin_sin_expansion3";
   16.38  
   16.39  Goal "0 < x ==> \
   16.40 @@ -614,9 +612,8 @@
   16.41  by (assume_tac 1 THEN assume_tac 1);
   16.42  by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
   16.43  by (rtac sumr_fun_eq 1);
   16.44 -by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
   16.45 -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
   16.46 -    even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
   16.47 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
   16.48 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
   16.49  qed "Maclaurin_sin_expansion4";
   16.50  
   16.51  (*-----------------------------------------------------------------------------*)
   16.52 @@ -658,9 +655,8 @@
   16.53  by (arith_tac 1);
   16.54  by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
   16.55  by (rtac sumr_fun_eq 1);
   16.56 -by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
   16.57 -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
   16.58 -    even_mult_two_ex,left_distrib,cos_add]  delsimps 
   16.59 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
   16.60 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add]  delsimps 
   16.61      [fact_Suc,realpow_Suc]));
   16.62  by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
   16.63  qed "Maclaurin_cos_expansion";
   16.64 @@ -685,10 +681,8 @@
   16.65  by (assume_tac 1 THEN assume_tac 1);
   16.66  by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
   16.67  by (rtac sumr_fun_eq 1);
   16.68 -by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
   16.69 -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
   16.70 -    even_mult_two_ex,left_distrib,cos_add]  delsimps 
   16.71 -    [fact_Suc,realpow_Suc]));
   16.72 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
   16.73 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add]  delsimps [fact_Suc,realpow_Suc]));
   16.74  by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
   16.75  qed "Maclaurin_cos_expansion2";
   16.76  
   16.77 @@ -712,10 +706,8 @@
   16.78  by (assume_tac 1 THEN assume_tac 1);
   16.79  by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
   16.80  by (rtac sumr_fun_eq 1);
   16.81 -by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
   16.82 -by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
   16.83 -    even_mult_two_ex,left_distrib,cos_add]  delsimps 
   16.84 -    [fact_Suc,realpow_Suc]));
   16.85 +by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
   16.86 +by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add]  delsimps [fact_Suc,realpow_Suc]));
   16.87  by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
   16.88  qed "Maclaurin_minus_cos_expansion";
   16.89  
    17.1 --- a/src/HOL/Hyperreal/NSA.thy	Thu Mar 04 10:06:13 2004 +0100
    17.2 +++ b/src/HOL/Hyperreal/NSA.thy	Thu Mar 04 12:06:07 2004 +0100
    17.3 @@ -914,7 +914,7 @@
    17.4  
    17.5  lemma Infinitesimal_SReal_divide: 
    17.6    "[| x \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal"
    17.7 -apply (simp add: divide_inverse_zero)
    17.8 +apply (simp add: divide_inverse)
    17.9  apply (auto intro!: Infinitesimal_HFinite_mult 
   17.10              dest!: SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   17.11  done
    18.1 --- a/src/HOL/Hyperreal/Transcendental.ML	Thu Mar 04 10:06:13 2004 +0100
    18.2 +++ b/src/HOL/Hyperreal/Transcendental.ML	Thu Mar 04 12:06:07 2004 +0100
    18.3 @@ -830,7 +830,6 @@
    18.4  by Auto_tac;
    18.5  qed "sin_fdiffs2";
    18.6  
    18.7 -(* thms in EvenOdd needed *)
    18.8  Goalw [diffs_def,real_divide_def]
    18.9        "diffs(%n. if even n then \
   18.10  \                (- 1) ^ (n div 2)/(real (fact n)) else 0) \
   18.11 @@ -841,11 +840,11 @@
   18.12  by (stac real_of_nat_mult 1);
   18.13  by (stac even_Suc 1);
   18.14  by (stac inverse_mult_distrib 1);
   18.15 -by (res_inst_tac [("z1","real (Suc n)")] (real_mult_commute RS ssubst) 1);
   18.16 -by (res_inst_tac [("z1","inverse(real (Suc n))")] 
   18.17 -     (real_mult_commute RS ssubst) 1);
   18.18 +by (res_inst_tac [("a1","real (Suc n)")] (mult_commute RS ssubst) 1);
   18.19 +by (res_inst_tac [("a1","inverse(real (Suc n))")] 
   18.20 +     (mult_commute RS ssubst) 1);
   18.21  by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
   18.22 -    odd_not_even RS sym,odd_Suc_mult_two_ex]));
   18.23 +    odd_Suc_mult_two_ex]));
   18.24  qed "cos_fdiffs";
   18.25  
   18.26  
   18.27 @@ -862,7 +861,7 @@
   18.28  by (res_inst_tac [("z1","inverse (real (Suc n))")] 
   18.29       (real_mult_commute RS ssubst) 1);
   18.30  by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
   18.31 -    odd_not_even RS sym,odd_Suc_mult_two_ex]));
   18.32 +    odd_Suc_mult_two_ex]));
   18.33  qed "cos_fdiffs2";
   18.34  
   18.35  (* ------------------------------------------------------------------------ *)
   18.36 @@ -1949,7 +1948,7 @@
   18.37  (* Pre Isabelle99-2 proof was simpler- numerals arithmetic 
   18.38     now causes some unwanted re-arrangements of literals!   *)
   18.39  Goal "[| 0 <= x; cos x = 0 |] ==> \
   18.40 -\     EX n. ~even n & x = real n * (pi/2)";
   18.41 +\     EX n::nat. ~even n & x = real n * (pi/2)";
   18.42  by (dtac (pi_gt_zero RS reals_Archimedean4) 1);
   18.43  by (Step_tac 1);
   18.44  by (subgoal_tac 
   18.45 @@ -1973,7 +1972,7 @@
   18.46  qed "cos_zero_lemma";
   18.47  
   18.48  Goal "[| 0 <= x; sin x = 0 |] ==> \
   18.49 -\     EX n. even n & x = real n * (pi/2)";
   18.50 +\     EX n::nat. even n & x = real n * (pi/2)";
   18.51  by (subgoal_tac 
   18.52      "EX n. ~ even n & x + pi/2  = real n * (pi/2)" 1);
   18.53  by (rtac cos_zero_lemma 2);
   18.54 @@ -1981,15 +1980,15 @@
   18.55  by (res_inst_tac [("x","n - 1")] exI 1);
   18.56  by (rtac (CLAIM "-y <= x ==> -x <= (y::real)") 2);
   18.57  by (rtac real_le_trans 2 THEN assume_tac 3);
   18.58 -by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym,
   18.59 +by (auto_tac (claset(),simpset() addsimps [
   18.60      odd_Suc_mult_two_ex,real_of_nat_Suc,
   18.61      left_distrib,real_mult_assoc RS sym]));
   18.62  qed "sin_zero_lemma";
   18.63  
   18.64  (* also spoilt by numeral arithmetic *)
   18.65  Goal "(cos x = 0) = \
   18.66 -\     ((EX n. ~even n & (x = real n * (pi/2))) |   \
   18.67 -\      (EX n. ~even n & (x = -(real n * (pi/2)))))";
   18.68 +\     ((EX n::nat. ~even n & (x = real n * (pi/2))) |   \
   18.69 +\      (EX n::nat. ~even n & (x = -(real n * (pi/2)))))";
   18.70  by (rtac iffI 1);
   18.71  by (cut_inst_tac [("x","x")] (CLAIM "0 <= (x::real) | x <= 0") 1);
   18.72  by (Step_tac 1);
   18.73 @@ -1998,15 +1997,15 @@
   18.74  by (dtac cos_zero_lemma 3);
   18.75  by (Step_tac 1);
   18.76  by (dtac (CLAIM "-x = y ==> x = -(y::real)") 2);
   18.77 -by (auto_tac (claset(),HOL_ss addsimps [odd_not_even RS sym,
   18.78 +by (auto_tac (claset(),HOL_ss addsimps [
   18.79      odd_Suc_mult_two_ex,real_of_nat_Suc,left_distrib]));
   18.80  by (auto_tac (claset(),simpset() addsimps [cos_add]));
   18.81  qed "cos_zero_iff";
   18.82  
   18.83  (* ditto: but to a lesser extent *)
   18.84  Goal "(sin x = 0) = \
   18.85 -\     ((EX n. even n & (x = real n * (pi/2))) |   \
   18.86 -\      (EX n. even n & (x = -(real n * (pi/2)))))";
   18.87 +\     ((EX n::nat. even n & (x = real n * (pi/2))) |   \
   18.88 +\      (EX n::nat. even n & (x = -(real n * (pi/2)))))";
   18.89  by (rtac iffI 1);
   18.90  by (cut_inst_tac [("x","x")] (CLAIM "0 <= (x::real) | x <= 0") 1);
   18.91  by (Step_tac 1);
    19.1 --- a/src/HOL/Integ/IntDef.thy	Thu Mar 04 10:06:13 2004 +0100
    19.2 +++ b/src/HOL/Integ/IntDef.thy	Thu Mar 04 12:06:07 2004 +0100
    19.3 @@ -369,9 +369,6 @@
    19.4  apply (simp add: zle linorder_linear) 
    19.5  done
    19.6  
    19.7 -instance int :: plus_ac0
    19.8 -proof qed (rule zadd_commute zadd_assoc zadd_0)+
    19.9 -
   19.10  instance int :: linorder
   19.11  proof qed (rule zle_linear)
   19.12  
   19.13 @@ -909,6 +906,63 @@
   19.14  declare le_iff_diff_le_0 [symmetric, simp]
   19.15  
   19.16  
   19.17 +subsection{*More Properties of @{term setsum} and  @{term setprod}*}
   19.18 +
   19.19 +text{*By Jeremy Avigad*}
   19.20 +
   19.21 +
   19.22 +lemma setsum_of_nat: "of_nat (setsum f A) = setsum (of_nat \<circ> f) A"
   19.23 +  apply (case_tac "finite A")
   19.24 +  apply (erule finite_induct, auto)
   19.25 +  apply (simp add: setsum_def)
   19.26 +  done
   19.27 +
   19.28 +lemma setsum_of_int: "of_int (setsum f A) = setsum (of_int \<circ> f) A"
   19.29 +  apply (case_tac "finite A")
   19.30 +  apply (erule finite_induct, auto)
   19.31 +  apply (simp add: setsum_def)
   19.32 +  done
   19.33 +
   19.34 +lemma int_setsum: "int (setsum f A) = setsum (int \<circ> f) A"
   19.35 +  by (subst int_eq_of_nat, rule setsum_of_nat)
   19.36 +
   19.37 +lemma setprod_of_nat: "of_nat (setprod f A) = setprod (of_nat \<circ> f) A"
   19.38 +  apply (case_tac "finite A")
   19.39 +  apply (erule finite_induct, auto)
   19.40 +  apply (simp add: setprod_def)
   19.41 +  done
   19.42 +
   19.43 +lemma setprod_of_int: "of_int (setprod f A) = setprod (of_int \<circ> f) A"
   19.44 +  apply (case_tac "finite A")
   19.45 +  apply (erule finite_induct, auto)
   19.46 +  apply (simp add: setprod_def)
   19.47 +  done
   19.48 +
   19.49 +lemma int_setprod: "int (setprod f A) = setprod (int \<circ> f) A"
   19.50 +  by (subst int_eq_of_nat, rule setprod_of_nat)
   19.51 +
   19.52 +lemma setsum_constant: "finite A ==> (\<Sum>x \<in> A. y) = of_nat(card A) * y"
   19.53 +  apply (erule finite_induct)
   19.54 +  apply (auto simp add: ring_distrib add_ac)
   19.55 +  done
   19.56 +
   19.57 +lemma setprod_nonzero_nat:
   19.58 +    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
   19.59 +  by (rule setprod_nonzero, auto)
   19.60 +
   19.61 +lemma setprod_zero_eq_nat:
   19.62 +    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
   19.63 +  by (rule setprod_zero_eq, auto)
   19.64 +
   19.65 +lemma setprod_nonzero_int:
   19.66 +    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
   19.67 +  by (rule setprod_nonzero, auto)
   19.68 +
   19.69 +lemma setprod_zero_eq_int:
   19.70 +    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
   19.71 +  by (rule setprod_zero_eq, auto)
   19.72 +
   19.73 +
   19.74  (*Legacy ML bindings, but no longer the structure Int.*)
   19.75  ML
   19.76  {*
    20.1 --- a/src/HOL/Integ/NatBin.thy	Thu Mar 04 10:06:13 2004 +0100
    20.2 +++ b/src/HOL/Integ/NatBin.thy	Thu Mar 04 12:06:07 2004 +0100
    20.3 @@ -648,6 +648,12 @@
    20.4            else number_of (bin_add v v') + k)"
    20.5  by simp
    20.6  
    20.7 +lemma nat_number_of_mult_left:
    20.8 +     "number_of v * (number_of v' * (k::nat)) =  
    20.9 +         (if neg (number_of v :: int) then 0
   20.10 +          else number_of (bin_mult v v') * k)"
   20.11 +by simp
   20.12 +
   20.13  
   20.14  subsubsection{*For @{text combine_numerals}*}
   20.15  
   20.16 @@ -776,6 +782,7 @@
   20.17  val nat_number = thms"nat_number";
   20.18  
   20.19  val nat_number_of_add_left = thm"nat_number_of_add_left";
   20.20 +val nat_number_of_mult_left = thm"nat_number_of_mult_left";
   20.21  val left_add_mult_distrib = thm"left_add_mult_distrib";
   20.22  val nat_diff_add_eq1 = thm"nat_diff_add_eq1";
   20.23  val nat_diff_add_eq2 = thm"nat_diff_add_eq2";
    21.1 --- a/src/HOL/Integ/NatSimprocs.thy	Thu Mar 04 10:06:13 2004 +0100
    21.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Thu Mar 04 12:06:07 2004 +0100
    21.3 @@ -204,7 +204,7 @@
    21.4  
    21.5  lemma minus1_divide [simp]:
    21.6       "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
    21.7 -by (simp add: divide_inverse_zero inverse_minus_eq)
    21.8 +by (simp add: divide_inverse inverse_minus_eq)
    21.9  
   21.10  ML
   21.11  {*
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/HOL/Integ/Parity.thy	Thu Mar 04 12:06:07 2004 +0100
    22.3 @@ -0,0 +1,279 @@
    22.4 +(*  Title:      Parity.thy
    22.5 +    Author:     Jeremy Avigad
    22.6 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    22.7 +
    22.8 +    Last modified 2 March 2004
    22.9 +*)
   22.10 +
   22.11 +header {* Parity: Even and Odd for ints and nats*}
   22.12 +
   22.13 +theory Parity = Divides + IntDiv + NatSimprocs:
   22.14 +
   22.15 +axclass even_odd < type
   22.16 +
   22.17 +instance int :: even_odd ..
   22.18 +instance nat :: even_odd ..
   22.19 +
   22.20 +consts
   22.21 +  even :: "'a::even_odd => bool"
   22.22 +
   22.23 +syntax 
   22.24 +  odd :: "'a::even_odd => bool"
   22.25 +
   22.26 +translations 
   22.27 +  "odd x" == "~even x" 
   22.28 +
   22.29 +defs (overloaded)
   22.30 +  even_def: "even (x::int) == x mod 2 = 0"
   22.31 +  even_nat_def: "even (x::nat) == even (int x)"
   22.32 +
   22.33 +
   22.34 +subsection {* Casting a nat power to an integer *}
   22.35 +
   22.36 +lemma zpow_int: "int (x^y) = (int x)^y"
   22.37 +  apply (induct_tac y)
   22.38 +  apply (simp, simp add: zmult_int [THEN sym])
   22.39 +  done
   22.40 +
   22.41 +subsection {* Even and odd are mutually exclusive *}
   22.42 +
   22.43 +lemma int_pos_lt_two_imp_zero_or_one: 
   22.44 +    "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1"
   22.45 +  by auto
   22.46 +
   22.47 +lemma neq_one_mod_two [simp]: "((x::int) mod 2 ~= 0) = (x mod 2 = 1)"
   22.48 +  apply (subgoal_tac "x mod 2 = 0 | x mod 2 = 1", force)
   22.49 +  apply (rule int_pos_lt_two_imp_zero_or_one, auto)
   22.50 +  done
   22.51 +
   22.52 +subsection {* Behavior under integer arithmetic operations *}
   22.53 +
   22.54 +lemma even_times_anything: "even (x::int) ==> even (x * y)"
   22.55 +  by (simp add: even_def zmod_zmult1_eq')
   22.56 +
   22.57 +lemma anything_times_even: "even (y::int) ==> even (x * y)"
   22.58 +  by (simp add: even_def zmod_zmult1_eq)
   22.59 +
   22.60 +lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)"
   22.61 +  by (simp add: even_def zmod_zmult1_eq)
   22.62 +
   22.63 +lemma even_product: "even((x::int) * y) = (even x | even y)"
   22.64 +  apply (auto simp add: even_times_anything anything_times_even) 
   22.65 +  apply (rule ccontr)
   22.66 +  apply (auto simp add: odd_times_odd)
   22.67 +  done
   22.68 +
   22.69 +lemma even_plus_even: "even (x::int) ==> even y ==> even (x + y)"
   22.70 +  by (simp add: even_def zmod_zadd1_eq)
   22.71 +
   22.72 +lemma even_plus_odd: "even (x::int) ==> odd y ==> odd (x + y)"
   22.73 +  by (simp add: even_def zmod_zadd1_eq)
   22.74 +
   22.75 +lemma odd_plus_even: "odd (x::int) ==> even y ==> odd (x + y)"
   22.76 +  by (simp add: even_def zmod_zadd1_eq)
   22.77 +
   22.78 +lemma odd_plus_odd: "odd (x::int) ==> odd y ==> even (x + y)"
   22.79 +  by (simp add: even_def zmod_zadd1_eq)
   22.80 +
   22.81 +lemma even_sum: "even ((x::int) + y) = ((even x & even y) | (odd x & odd y))"
   22.82 +  apply (auto intro: even_plus_even odd_plus_odd)
   22.83 +  apply (rule ccontr, simp add: even_plus_odd)
   22.84 +  apply (rule ccontr, simp add: odd_plus_even)
   22.85 +  done
   22.86 +
   22.87 +lemma even_neg: "even (-(x::int)) = even x"
   22.88 +  by (auto simp add: even_def zmod_zminus1_eq_if)
   22.89 +
   22.90 +lemma even_difference: 
   22.91 +  "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))"
   22.92 +  by (simp only: diff_minus even_sum even_neg)
   22.93 +
   22.94 +lemma even_pow_gt_zero [rule_format]: 
   22.95 +    "even (x::int) ==> 0 < n --> even (x^n)"
   22.96 +  apply (induct_tac n)
   22.97 +  apply (auto simp add: even_product)
   22.98 +  done
   22.99 +
  22.100 +lemma odd_pow: "odd x ==> odd((x::int)^n)"
  22.101 +  apply (induct_tac n)
  22.102 +  apply (simp add: even_def)
  22.103 +  apply (simp add: even_product)
  22.104 +  done
  22.105 +
  22.106 +lemma even_power: "even ((x::int)^n) = (even x & 0 < n)"
  22.107 +  apply (auto simp add: even_pow_gt_zero) 
  22.108 +  apply (erule contrapos_pp, erule odd_pow)
  22.109 +  apply (erule contrapos_pp, simp add: even_def)
  22.110 +  done
  22.111 +
  22.112 +lemma even_zero: "even (0::int)"
  22.113 +  by (simp add: even_def)
  22.114 +
  22.115 +lemma odd_one: "odd (1::int)"
  22.116 +  by (simp add: even_def)
  22.117 +
  22.118 +lemmas even_odd_simps [simp] = even_def[of "number_of v",standard] even_zero 
  22.119 +  odd_one even_product even_sum even_neg even_difference even_power
  22.120 +
  22.121 +
  22.122 +subsection {* Equivalent definitions *}
  22.123 +
  22.124 +lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x" 
  22.125 +  by (auto simp add: even_def)
  22.126 +
  22.127 +lemma two_times_odd_div_two_plus_one: "odd (x::int) ==> 
  22.128 +    2 * (x div 2) + 1 = x"
  22.129 +  apply (insert zmod_zdiv_equality [of x 2, THEN sym])
  22.130 +  by (simp add: even_def)
  22.131 +
  22.132 +lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)"
  22.133 +  apply auto
  22.134 +  apply (rule exI)
  22.135 +  by (erule two_times_even_div_two [THEN sym])
  22.136 +
  22.137 +lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)"
  22.138 +  apply auto
  22.139 +  apply (rule exI)
  22.140 +  by (erule two_times_odd_div_two_plus_one [THEN sym])
  22.141 +
  22.142 +
  22.143 +subsection {* even and odd for nats *}
  22.144 +
  22.145 +lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)"
  22.146 +  by (simp add: even_nat_def)
  22.147 +
  22.148 +lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
  22.149 +  by (simp add: even_nat_def zmult_int [THEN sym])
  22.150 +
  22.151 +lemma even_nat_sum: "even ((x::nat) + y) = 
  22.152 +    ((even x & even y) | (odd x & odd y))"
  22.153 +  by (unfold even_nat_def, simp)
  22.154 +
  22.155 +lemma even_nat_difference: 
  22.156 +    "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
  22.157 +  apply (auto simp add: even_nat_def zdiff_int [THEN sym])
  22.158 +  apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym])
  22.159 +  apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym])
  22.160 +  done
  22.161 +
  22.162 +lemma even_nat_suc: "even (Suc x) = odd x"
  22.163 +  by (simp add: even_nat_def)
  22.164 +
  22.165 +lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
  22.166 +  by (simp add: even_nat_def zpow_int)
  22.167 +
  22.168 +lemma even_nat_zero: "even (0::nat)"
  22.169 +  by (simp add: even_nat_def)
  22.170 +
  22.171 +lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] 
  22.172 +  even_nat_zero even_nat_suc even_nat_product even_nat_sum even_nat_power
  22.173 +
  22.174 +
  22.175 +subsection {* Equivalent definitions *}
  22.176 +
  22.177 +lemma nat_lt_two_imp_zero_or_one: "(x::nat) < Suc (Suc 0) ==> 
  22.178 +    x = 0 | x = Suc 0"
  22.179 +  by auto
  22.180 +
  22.181 +lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0"
  22.182 +  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
  22.183 +  apply (drule subst, assumption)
  22.184 +  apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0")
  22.185 +  apply force
  22.186 +  apply (subgoal_tac "0 < Suc (Suc 0)")
  22.187 +  apply (frule mod_less_divisor [of "Suc (Suc 0)" x])
  22.188 +  apply (erule nat_lt_two_imp_zero_or_one, auto)
  22.189 +  done
  22.190 +
  22.191 +lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0"
  22.192 +  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
  22.193 +  apply (drule subst, assumption)
  22.194 +  apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0")
  22.195 +  apply force 
  22.196 +  apply (subgoal_tac "0 < Suc (Suc 0)")
  22.197 +  apply (frule mod_less_divisor [of "Suc (Suc 0)" x])
  22.198 +  apply (erule nat_lt_two_imp_zero_or_one, auto)
  22.199 +  done
  22.200 +
  22.201 +lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" 
  22.202 +  apply (rule iffI)
  22.203 +  apply (erule even_nat_mod_two_eq_zero)
  22.204 +  apply (insert odd_nat_mod_two_eq_one [of x], auto)
  22.205 +  done
  22.206 +
  22.207 +lemma odd_nat_equiv_def: "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)"
  22.208 +  apply (auto simp add: even_nat_equiv_def)
  22.209 +  apply (subgoal_tac "x mod (Suc (Suc 0)) < Suc (Suc 0)")
  22.210 +  apply (frule nat_lt_two_imp_zero_or_one, auto)
  22.211 +  done
  22.212 +
  22.213 +lemma even_nat_div_two_times_two: "even (x::nat) ==> 
  22.214 +    Suc (Suc 0) * (x div Suc (Suc 0)) = x"
  22.215 +  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
  22.216 +  apply (drule even_nat_mod_two_eq_zero, simp)
  22.217 +  done
  22.218 +
  22.219 +lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> 
  22.220 +    Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x"  
  22.221 +  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
  22.222 +  apply (drule odd_nat_mod_two_eq_one, simp)
  22.223 +  done
  22.224 +
  22.225 +lemma even_nat_equiv_def2: "even (x::nat) = (EX y. x = Suc (Suc 0) * y)"
  22.226 +  apply (rule iffI, rule exI)
  22.227 +  apply (erule even_nat_div_two_times_two [THEN sym], auto)
  22.228 +  done
  22.229 +
  22.230 +lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))"
  22.231 +  apply (rule iffI, rule exI)
  22.232 +  apply (erule odd_nat_div_two_times_two_plus_one [THEN sym], auto)
  22.233 +  done
  22.234 +
  22.235 +subsection {* Powers of negative one *}
  22.236 +
  22.237 +lemma neg_one_even_odd_power:
  22.238 +     "(even x --> (-1::'a::{number_ring,ringpower})^x = 1) & 
  22.239 +      (odd x --> (-1::'a)^x = -1)"
  22.240 +  apply (induct_tac x)
  22.241 +  apply (simp, simp add: power_Suc)
  22.242 +  done
  22.243 +
  22.244 +lemma neg_one_even_power: "even x ==> (-1::'a::{number_ring,ringpower})^x = 1"
  22.245 +  by (rule neg_one_even_odd_power [THEN conjunct1, THEN mp], assumption)
  22.246 +
  22.247 +lemma neg_one_odd_power: "odd x ==> (-1::'a::{number_ring,ringpower})^x = -1"
  22.248 +  by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption)
  22.249 +
  22.250 +
  22.251 +subsection {* Miscellaneous *}
  22.252 +
  22.253 +lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2"
  22.254 +  apply (subst zdiv_zadd1_eq)
  22.255 +  apply (simp add: even_def)
  22.256 +  done
  22.257 +
  22.258 +lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1"
  22.259 +  apply (subst zdiv_zadd1_eq)
  22.260 +  apply (simp add: even_def)
  22.261 +  done
  22.262 +
  22.263 +lemma div_Suc: "Suc a div c = a div c + Suc 0 div c + 
  22.264 +    (a mod c + Suc 0 mod c) div c"
  22.265 +  apply (subgoal_tac "Suc a = a + Suc 0")
  22.266 +  apply (erule ssubst)
  22.267 +  apply (rule div_add1_eq, simp)
  22.268 +  done
  22.269 +
  22.270 +lemma even_nat_plus_one_div_two: "even (x::nat) ==> 
  22.271 +   (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
  22.272 +  apply (subst div_Suc)
  22.273 +  apply (simp add: even_nat_equiv_def)
  22.274 +  done
  22.275 +
  22.276 +lemma odd_nat_plus_one_div_two: "odd (x::nat) ==> 
  22.277 +    (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))"
  22.278 +  apply (subst div_Suc)
  22.279 +  apply (simp add: odd_nat_equiv_def)
  22.280 +  done
  22.281 +
  22.282 +end
    23.1 --- a/src/HOL/Integ/nat_simprocs.ML	Thu Mar 04 10:06:13 2004 +0100
    23.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Thu Mar 04 12:06:07 2004 +0100
    23.3 @@ -6,6 +6,10 @@
    23.4  Simprocs for nat numerals.
    23.5  *)
    23.6  
    23.7 +val Let_number_of = thm"Let_number_of";
    23.8 +val Let_0 = thm"Let_0";
    23.9 +val Let_1 = thm"Let_1";
   23.10 +
   23.11  structure Nat_Numeral_Simprocs =
   23.12  struct
   23.13  
   23.14 @@ -65,12 +69,14 @@
   23.15  
   23.16  val trans_tac = Int_Numeral_Simprocs.trans_tac;
   23.17  
   23.18 -val bin_simps = [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym,
   23.19 -                 add_nat_number_of, nat_number_of_add_left,
   23.20 -                 diff_nat_number_of, le_number_of_eq_not_less,
   23.21 -                 less_nat_number_of, mult_nat_number_of,
   23.22 -                 thm "Let_number_of", nat_number_of] @
   23.23 -                bin_arith_simps @ bin_rel_simps;
   23.24 +val bin_simps =
   23.25 +     [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym,
   23.26 +      add_nat_number_of, nat_number_of_add_left, 
   23.27 +      diff_nat_number_of, le_number_of_eq_not_less,
   23.28 +      mult_nat_number_of, nat_number_of_mult_left, 
   23.29 +      less_nat_number_of, 
   23.30 +      Let_number_of, nat_number_of] @
   23.31 +     bin_arith_simps @ bin_rel_simps;
   23.32  
   23.33  fun prep_simproc (name, pats, proc) =
   23.34    Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
   23.35 @@ -268,7 +274,8 @@
   23.36    val trans_tac         = trans_tac
   23.37    val norm_tac = ALLGOALS
   23.38                      (simp_tac (HOL_ss addsimps [Suc_eq_add_numeral_1]@mult_1s))
   23.39 -                 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_ac))
   23.40 +                 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
   23.41 +                 THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
   23.42    val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
   23.43    val simplify_meta_eq  = simplify_meta_eq
   23.44    end
   23.45 @@ -504,7 +511,7 @@
   23.46  
   23.47  (* reduce contradictory <= to False *)
   23.48  val add_rules =
   23.49 -  [thm "Let_number_of", thm "Let_0", thm "Let_1", nat_0, nat_1,
   23.50 +  [thm "Let_number_of", Let_0, Let_1, nat_0, nat_1,
   23.51     add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
   23.52     eq_nat_number_of, less_nat_number_of, le_number_of_eq_not_less,
   23.53     le_Suc_number_of,le_number_of_Suc,
    24.1 --- a/src/HOL/IsaMakefile	Thu Mar 04 10:06:13 2004 +0100
    24.2 +++ b/src/HOL/IsaMakefile	Thu Mar 04 12:06:07 2004 +0100
    24.3 @@ -87,9 +87,8 @@
    24.4    HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.thy \
    24.5    Integ/cooper_dec.ML Integ/cooper_proof.ML \
    24.6    Integ/Equiv.thy Integ/IntArith.thy Integ/IntDef.thy \
    24.7 -  Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy \
    24.8 -  Integ/int_arith1.ML \
    24.9 -  Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
   24.10 +  Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \
   24.11 +  Integ/int_arith1.ML Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
   24.12    Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
   24.13    Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
   24.14    Nat.thy NatArith.ML NatArith.thy Numeral.thy \
   24.15 @@ -143,7 +142,7 @@
   24.16    Real/Rational.thy Real/PReal.thy Real/RComplete.thy \
   24.17    Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy \
   24.18    Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
   24.19 -  Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
   24.20 +  Hyperreal/EvenOdd.thy\
   24.21    Hyperreal/Fact.ML Hyperreal/Fact.thy Hyperreal/HLog.thy\
   24.22    Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HSeries.thy\
   24.23    Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\
    25.1 --- a/src/HOL/NumberTheory/Finite2.thy	Thu Mar 04 10:06:13 2004 +0100
    25.2 +++ b/src/HOL/NumberTheory/Finite2.thy	Thu Mar 04 12:06:07 2004 +0100
    25.3 @@ -253,12 +253,7 @@
    25.4  lemma cartesian_product_card [simp]: "[| finite A; finite B |] ==> 
    25.5    card (A <*> B) = card(A) * card(B)";
    25.6    apply (rule_tac F = A in finite_induct, auto)
    25.7 -  apply (case_tac "F = {}", force)
    25.8 -  apply (subgoal_tac "card({x} <*> B \<union> F <*> B) = card({x} <*> B) + 
    25.9 -    card(F <*> B)");
   25.10 -  apply simp
   25.11 -  apply (rule card_Un_disjoint)
   25.12 -  by auto
   25.13 +  done
   25.14  
   25.15  (******************************************************************)
   25.16  (*                                                                *)
    26.1 --- a/src/HOL/PreList.thy	Thu Mar 04 10:06:13 2004 +0100
    26.2 +++ b/src/HOL/PreList.thy	Thu Mar 04 12:06:07 2004 +0100
    26.3 @@ -9,7 +9,8 @@
    26.4  (*Is defined separately to serve as a basis for theory ToyList in the
    26.5  documentation.*)
    26.6  
    26.7 -theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power:
    26.8 +theory PreList =
    26.9 +    Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
   26.10  
   26.11  (*belongs to theory Wellfounded_Recursion*)
   26.12  lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
    27.1 --- a/src/HOL/Real/PReal.thy	Thu Mar 04 10:06:13 2004 +0100
    27.2 +++ b/src/HOL/Real/PReal.thy	Thu Mar 04 12:06:07 2004 +0100
    27.3 @@ -296,13 +296,13 @@
    27.4      show "\<exists>y' \<in> B. z = x*?f + y'"
    27.5      proof
    27.6        show "z = x*?f + y*?f"
    27.7 -	by (simp add: left_distrib [symmetric] divide_inverse_zero mult_ac
    27.8 +	by (simp add: left_distrib [symmetric] divide_inverse mult_ac
    27.9  		      order_less_imp_not_eq2)
   27.10      next
   27.11        show "y * ?f \<in> B"
   27.12        proof (rule preal_downwards_closed [OF B y])
   27.13          show "0 < y * ?f"
   27.14 -          by (simp add: divide_inverse_zero zero_less_mult_iff)
   27.15 +          by (simp add: divide_inverse zero_less_mult_iff)
   27.16        next
   27.17          show "y * ?f < y"
   27.18            by (insert mult_strict_left_mono [OF fless ypos], simp)
   27.19 @@ -312,7 +312,7 @@
   27.20      show "x * ?f \<in> A"
   27.21      proof (rule preal_downwards_closed [OF A x])
   27.22        show "0 < x * ?f"
   27.23 -	by (simp add: divide_inverse_zero zero_less_mult_iff)
   27.24 +	by (simp add: divide_inverse zero_less_mult_iff)
   27.25      next
   27.26        show "x * ?f < x"
   27.27  	by (insert mult_strict_left_mono [OF fless xpos], simp)
   27.28 @@ -435,7 +435,7 @@
   27.29      show "\<exists>y'\<in>B. z = (z/y) * y'"
   27.30      proof
   27.31        show "z = (z/y)*y"
   27.32 -	by (simp add: divide_inverse_zero mult_commute [of y] mult_assoc
   27.33 +	by (simp add: divide_inverse mult_commute [of y] mult_assoc
   27.34  		      order_less_imp_not_eq2)
   27.35        show "y \<in> B" .
   27.36      qed
   27.37 @@ -522,7 +522,7 @@
   27.38          show "\<exists>v'\<in>A. x = (x / v) * v'"
   27.39          proof
   27.40            show "x = (x/v)*v"
   27.41 -	    by (simp add: divide_inverse_zero mult_assoc vpos
   27.42 +	    by (simp add: divide_inverse mult_assoc vpos
   27.43                            order_less_imp_not_eq2)
   27.44            show "v \<in> A" .
   27.45          qed
   27.46 @@ -579,7 +579,7 @@
   27.47    have cpos: "0 < ?c"
   27.48      by (simp add: zero_less_divide_iff zero_less_mult_iff pos_add_strict)
   27.49    show "a * d + b * e = ?c * (d + e)"
   27.50 -    by (simp add: divide_inverse_zero mult_assoc order_less_imp_not_eq2)
   27.51 +    by (simp add: divide_inverse mult_assoc order_less_imp_not_eq2)
   27.52    show "?c \<in> Rep_preal w"
   27.53      proof (cases rule: linorder_le_cases)
   27.54        assume "a \<le> b"
   27.55 @@ -808,7 +808,7 @@
   27.56      proof -
   27.57        have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
   27.58        also with ypos have "... = (r/y) * (y + ?d)"
   27.59 -	by (simp only: right_distrib divide_inverse_zero mult_ac, simp)
   27.60 +	by (simp only: right_distrib divide_inverse mult_ac, simp)
   27.61        also have "... = r*x" using ypos
   27.62  	by simp
   27.63        finally show "r + ?d < r*x" .
   27.64 @@ -849,12 +849,12 @@
   27.65      show "0 < x/u" using xpos upos
   27.66        by (simp add: zero_less_divide_iff)  
   27.67      show "x/u < x/r" using xpos upos rpos
   27.68 -      by (simp add: divide_inverse_zero mult_less_cancel_left rless) 
   27.69 +      by (simp add: divide_inverse mult_less_cancel_left rless) 
   27.70      show "inverse (x / r) \<notin> Rep_preal R" using notin
   27.71 -      by (simp add: divide_inverse_zero mult_commute) 
   27.72 +      by (simp add: divide_inverse mult_commute) 
   27.73      show "u \<in> Rep_preal R" by (rule u) 
   27.74      show "x = x / u * u" using upos 
   27.75 -      by (simp add: divide_inverse_zero mult_commute) 
   27.76 +      by (simp add: divide_inverse mult_commute) 
   27.77    qed
   27.78  qed
   27.79  
   27.80 @@ -875,7 +875,7 @@
   27.81    have "q < inverse y" using rpos rless
   27.82      by (simp add: not_in_preal_ub [OF Rep_preal notin] q)
   27.83    hence "r * q < r/y" using rpos
   27.84 -    by (simp add: divide_inverse_zero mult_less_cancel_left)
   27.85 +    by (simp add: divide_inverse mult_less_cancel_left)
   27.86    also have "... \<le> 1" using rpos rless
   27.87      by (simp add: pos_divide_le_eq)
   27.88    finally show ?thesis .
   27.89 @@ -1272,7 +1272,7 @@
   27.90    have "x * z * inverse y * inverse z = x * inverse y * (z * inverse z)"
   27.91      by (simp add: mult_ac)
   27.92    also have "... = x/y" using zpos
   27.93 -    by (simp add: divide_inverse_zero)
   27.94 +    by (simp add: divide_inverse)
   27.95    also have "... < z"
   27.96      by (simp add: pos_divide_less_eq [OF ypos] mult_commute) 
   27.97    finally show ?thesis .
    28.1 --- a/src/HOL/Real/Rational.thy	Thu Mar 04 10:06:13 2004 +0100
    28.2 +++ b/src/HOL/Real/Rational.thy	Thu Mar 04 12:06:07 2004 +0100
    28.3 @@ -511,9 +511,8 @@
    28.4         (simp add: add_rat mult_rat eq_rat int_distrib)
    28.5    show "q \<noteq> 0 ==> inverse q * q = 1"
    28.6      by (induct q) (simp add: inverse_rat mult_rat one_rat zero_rat eq_rat)
    28.7 -  show "r \<noteq> 0 ==> q / r = q * inverse r"
    28.8 -    by (induct q, induct r)
    28.9 -       (simp add: mult_rat divide_rat inverse_rat zero_rat eq_rat)
   28.10 +  show "q / r = q * inverse r"
   28.11 +    by (simp add: divide_rat_def) 
   28.12    show "0 \<noteq> (1::rat)"
   28.13      by (simp add: zero_rat one_rat eq_rat) 
   28.14  qed
   28.15 @@ -632,9 +631,7 @@
   28.16  
   28.17  instance rat :: division_by_zero
   28.18  proof
   28.19 -  fix x :: rat
   28.20    show "inverse 0 = (0::rat)"  by (simp add: inverse_rat_def)
   28.21 -  show "x/0 = 0"   by (simp add: divide_rat_def inverse_rat_def)
   28.22  qed
   28.23  
   28.24  
    29.1 --- a/src/HOL/Real/RealDef.thy	Thu Mar 04 10:06:13 2004 +0100
    29.2 +++ b/src/HOL/Real/RealDef.thy	Thu Mar 04 12:06:07 2004 +0100
    29.3 @@ -351,7 +351,7 @@
    29.4    show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib)
    29.5    show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
    29.6    show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
    29.7 -  show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
    29.8 +  show "x / y = x * inverse y" by (simp add: real_divide_def)
    29.9  qed
   29.10  
   29.11  
   29.12 @@ -365,9 +365,7 @@
   29.13  
   29.14  instance real :: division_by_zero
   29.15  proof
   29.16 -  fix x :: real
   29.17    show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
   29.18 -  show "x/0 = 0" by (simp add: real_divide_def INVERSE_ZERO)
   29.19  qed
   29.20  
   29.21  
    30.1 --- a/src/HOL/Ring_and_Field.thy	Thu Mar 04 10:06:13 2004 +0100
    30.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Mar 04 12:06:07 2004 +0100
    30.3 @@ -59,13 +59,12 @@
    30.4  
    30.5  axclass field \<subseteq> ring, inverse
    30.6    left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
    30.7 -  divide_inverse:      "b \<noteq> 0 ==> a / b = a * inverse b"
    30.8 +  divide_inverse:      "a / b = a * inverse b"
    30.9  
   30.10  axclass ordered_field \<subseteq> ordered_ring, field
   30.11  
   30.12  axclass division_by_zero \<subseteq> zero, inverse
   30.13    inverse_zero [simp]: "inverse 0 = 0"
   30.14 -  divide_zero [simp]: "a / 0 = 0"
   30.15  
   30.16  
   30.17  subsection {* Derived Rules for Addition *}
   30.18 @@ -595,7 +594,7 @@
   30.19  instance ordered_ring \<subseteq> ordered_semiring
   30.20  proof
   30.21    have "(0::'a) \<le> 1*1" by (rule zero_le_square)
   30.22 -  thus "(0::'a) < 1" by (simp add: order_le_less ) 
   30.23 +  thus "(0::'a) < 1" by (simp add: order_le_less) 
   30.24  qed
   30.25  
   30.26  text{*All three types of comparision involving 0 and 1 are covered.*}
   30.27 @@ -650,7 +649,7 @@
   30.28  
   30.29  lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semiring)"
   30.30  apply (insert mult_strict_mono [of 1 m 1 n]) 
   30.31 -apply (simp add:  order_less_trans [OF zero_less_one]); 
   30.32 +apply (simp add:  order_less_trans [OF zero_less_one]) 
   30.33  done
   30.34  
   30.35  
   30.36 @@ -743,24 +742,18 @@
   30.37  lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
   30.38    by (simp add: divide_inverse)
   30.39  
   30.40 -lemma divide_inverse_zero: "a/b = a * inverse(b::'a::{field,division_by_zero})"
   30.41 -apply (case_tac "b = 0")
   30.42 -apply (simp_all add: divide_inverse)
   30.43 -done
   30.44 +lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})"
   30.45 +by (simp add: divide_inverse)
   30.46  
   30.47 -lemma divide_zero_left [simp]: "0/a = (0::'a::{field,division_by_zero})"
   30.48 -by (simp add: divide_inverse_zero)
   30.49 +lemma divide_zero_left [simp]: "0/a = (0::'a::field)"
   30.50 +by (simp add: divide_inverse)
   30.51  
   30.52 -lemma inverse_eq_divide: "inverse (a::'a::{field,division_by_zero}) = 1/a"
   30.53 -by (simp add: divide_inverse_zero)
   30.54 +lemma inverse_eq_divide: "inverse (a::'a::field) = 1/a"
   30.55 +by (simp add: divide_inverse)
   30.56  
   30.57 -lemma nonzero_add_divide_distrib: "c \<noteq> 0 ==> (a+b)/(c::'a::field) = a/c + b/c"
   30.58 +lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c"
   30.59  by (simp add: divide_inverse left_distrib) 
   30.60  
   30.61 -lemma add_divide_distrib: "(a+b)/(c::'a::{field,division_by_zero}) = a/c + b/c"
   30.62 -apply (case_tac "c=0", simp) 
   30.63 -apply (simp add: nonzero_add_divide_distrib) 
   30.64 -done
   30.65  
   30.66  text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
   30.67        of an ordering.*}
   30.68 @@ -935,7 +928,7 @@
   30.69  
   30.70  lemma inverse_divide [simp]:
   30.71        "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
   30.72 -  by (simp add: divide_inverse_zero mult_commute)
   30.73 +  by (simp add: divide_inverse mult_commute)
   30.74  
   30.75  lemma nonzero_mult_divide_cancel_left:
   30.76    assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" 
   30.77 @@ -975,23 +968,21 @@
   30.78    by (simp add: mult_divide_cancel_left)
   30.79  
   30.80  lemma divide_1 [simp]: "a/1 = (a::'a::field)"
   30.81 -  by (simp add: divide_inverse [OF not_sym])
   30.82 +  by (simp add: divide_inverse)
   30.83  
   30.84 -lemma times_divide_eq_right [simp]:
   30.85 -     "a * (b/c) = (a*b) / (c::'a::{field,division_by_zero})"
   30.86 -by (simp add: divide_inverse_zero mult_assoc)
   30.87 +lemma times_divide_eq_right [simp]: "a * (b/c) = (a*b) / (c::'a::field)"
   30.88 +by (simp add: divide_inverse mult_assoc)
   30.89  
   30.90 -lemma times_divide_eq_left [simp]:
   30.91 -     "(b/c) * a = (b*a) / (c::'a::{field,division_by_zero})"
   30.92 -by (simp add: divide_inverse_zero mult_ac)
   30.93 +lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
   30.94 +by (simp add: divide_inverse mult_ac)
   30.95  
   30.96  lemma divide_divide_eq_right [simp]:
   30.97       "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
   30.98 -by (simp add: divide_inverse_zero mult_ac)
   30.99 +by (simp add: divide_inverse mult_ac)
  30.100  
  30.101  lemma divide_divide_eq_left [simp]:
  30.102       "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
  30.103 -by (simp add: divide_inverse_zero mult_assoc)
  30.104 +by (simp add: divide_inverse mult_assoc)
  30.105  
  30.106  
  30.107  subsection {* Division and Unary Minus *}
  30.108 @@ -1005,14 +996,12 @@
  30.109  lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
  30.110  by (simp add: divide_inverse nonzero_inverse_minus_eq)
  30.111  
  30.112 -lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::{field,division_by_zero})"
  30.113 -apply (case_tac "b=0", simp) 
  30.114 -apply (simp add: nonzero_minus_divide_left) 
  30.115 -done
  30.116 +lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
  30.117 +by (simp add: divide_inverse minus_mult_left [symmetric])
  30.118  
  30.119  lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
  30.120 -apply (case_tac "b=0", simp) 
  30.121 -by (rule nonzero_minus_divide_right) 
  30.122 +by (simp add: divide_inverse minus_mult_right [symmetric])
  30.123 +
  30.124  
  30.125  text{*The effect is to extract signs from divisions*}
  30.126  declare minus_divide_left  [symmetric, simp]
  30.127 @@ -1028,8 +1017,7 @@
  30.128  apply (simp add: nonzero_minus_divide_divide) 
  30.129  done
  30.130  
  30.131 -lemma diff_divide_distrib:
  30.132 -     "(a-b)/(c::'a::{field,division_by_zero}) = a/c - b/c"
  30.133 +lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
  30.134  by (simp add: diff_minus add_divide_distrib) 
  30.135  
  30.136  
  30.137 @@ -1236,26 +1224,26 @@
  30.138  
  30.139  lemma zero_less_divide_iff:
  30.140       "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
  30.141 -by (simp add: divide_inverse_zero zero_less_mult_iff)
  30.142 +by (simp add: divide_inverse zero_less_mult_iff)
  30.143  
  30.144  lemma divide_less_0_iff:
  30.145       "(a/b < (0::'a::{ordered_field,division_by_zero})) = 
  30.146        (0 < a & b < 0 | a < 0 & 0 < b)"
  30.147 -by (simp add: divide_inverse_zero mult_less_0_iff)
  30.148 +by (simp add: divide_inverse mult_less_0_iff)
  30.149  
  30.150  lemma zero_le_divide_iff:
  30.151       "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
  30.152        (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
  30.153 -by (simp add: divide_inverse_zero zero_le_mult_iff)
  30.154 +by (simp add: divide_inverse zero_le_mult_iff)
  30.155  
  30.156  lemma divide_le_0_iff:
  30.157       "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
  30.158        (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
  30.159 -by (simp add: divide_inverse_zero mult_le_0_iff)
  30.160 +by (simp add: divide_inverse mult_le_0_iff)
  30.161  
  30.162  lemma divide_eq_0_iff [simp]:
  30.163       "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
  30.164 -by (simp add: divide_inverse_zero field_mult_eq_0_iff)
  30.165 +by (simp add: divide_inverse field_mult_eq_0_iff)
  30.166  
  30.167  
  30.168  subsection{*Simplification of Inequalities Involving Literal Divisors*}
  30.169 @@ -1415,13 +1403,13 @@
  30.170  lemma divide_cancel_right [simp]:
  30.171       "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
  30.172  apply (case_tac "c=0", simp) 
  30.173 -apply (simp add: divide_inverse_zero field_mult_cancel_right) 
  30.174 +apply (simp add: divide_inverse field_mult_cancel_right) 
  30.175  done
  30.176  
  30.177  lemma divide_cancel_left [simp]:
  30.178       "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
  30.179  apply (case_tac "c=0", simp) 
  30.180 -apply (simp add: divide_inverse_zero field_mult_cancel_left) 
  30.181 +apply (simp add: divide_inverse field_mult_cancel_left) 
  30.182  done
  30.183  
  30.184  subsection {* Division and the Number One *}
  30.185 @@ -1669,6 +1657,9 @@
  30.186    thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  30.187  qed
  30.188  
  30.189 +text{*Moving this up spoils many proofs using @{text mult_le_cancel_right}*}
  30.190 +declare times_divide_eq_left [simp]
  30.191 +
  30.192  ML
  30.193  {*
  30.194  val add_assoc = thm"add_assoc";
  30.195 @@ -1809,11 +1800,9 @@
  30.196  val right_inverse_eq = thm"right_inverse_eq";
  30.197  val nonzero_inverse_eq_divide = thm"nonzero_inverse_eq_divide";
  30.198  val divide_self = thm"divide_self";
  30.199 -val divide_inverse_zero = thm"divide_inverse_zero";
  30.200  val inverse_divide = thm"inverse_divide";
  30.201  val divide_zero_left = thm"divide_zero_left";
  30.202  val inverse_eq_divide = thm"inverse_eq_divide";
  30.203 -val nonzero_add_divide_distrib = thm"nonzero_add_divide_distrib";
  30.204  val add_divide_distrib = thm"add_divide_distrib";
  30.205  val field_mult_eq_0_iff = thm"field_mult_eq_0_iff";
  30.206  val field_mult_cancel_right = thm"field_mult_cancel_right";
    31.1 --- a/src/HOL/simpdata.ML	Thu Mar 04 10:06:13 2004 +0100
    31.2 +++ b/src/HOL/simpdata.ML	Thu Mar 04 12:06:07 2004 +0100
    31.3 @@ -246,7 +246,7 @@
    31.4         imp_disjL, conj_assoc, disj_assoc,
    31.5         de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
    31.6         disj_not1, not_all, not_ex, cases_simp,
    31.7 -       thm "the_eq_trivial", the_sym_eq_trivial, thm "plus_ac0.zero", thm "plus_ac0_zero_right"]
    31.8 +       thm "the_eq_trivial", the_sym_eq_trivial]
    31.9       @ ex_simps @ all_simps @ simp_thms)
   31.10       addsimprocs [defALL_regroup,defEX_regroup]
   31.11       addcongs [imp_cong]