# HG changeset patch
# User paulson
# Date 1078398367 -3600
# Node ID 5cb24165a2e1f021e0b94ce1fb0a10782ba86f45
# Parent  0fce2d8bce0f34784f5f859fdfb5719fe0c846e9
new material from Avigad, and simplified treatment of division by 0

diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Complex/CLim.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -858,8 +858,7 @@
 apply (simp (no_asm_simp))
 apply (rule capprox_mult_hcomplex_of_complex)
 apply (auto intro!: NSCDERIVD1 intro: capprox_minus_iff [THEN iffD2] 
-            simp add: diff_minus [symmetric] 
-                      divide_inverse_zero [symmetric])
+            simp add: diff_minus [symmetric] divide_inverse [symmetric])
 apply (blast intro: NSCDERIVD2)
 done
 
@@ -968,8 +967,10 @@
 apply (simp add: complex_diff_def)
 apply (drule_tac f = g in CDERIV_inverse_fun)
 apply (drule_tac [2] CDERIV_mult, assumption+)
-apply (simp add: divide_inverse_zero right_distrib power_inverse minus_mult_left mult_ac 
-            del: complexpow_Suc minus_mult_right [symmetric] minus_mult_left [symmetric])
+apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left 
+                 mult_ac 
+            del: minus_mult_right [symmetric] minus_mult_left [symmetric]
+                 complexpow_Suc)
 done
 
 lemma NSCDERIV_quotient:
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Complex/CStar.thy
--- a/src/HOL/Complex/CStar.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Complex/CStar.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -489,18 +489,17 @@
 done
 
 lemma starfunC_divide: "( *fc* f) y  / ( *fc* g) y = ( *fc* (%x. f x / g x)) y"
-by (simp add: divide_inverse_zero)
+by (simp add: divide_inverse)
 declare starfunC_divide [symmetric, simp]
 
 lemma starfunCR_divide:
   "( *fcR* f) y  / ( *fcR* g) y = ( *fcR* (%x. f x / g x)) y"
-by (simp add: divide_inverse_zero)
+by (simp add: divide_inverse)
 declare starfunCR_divide [symmetric, simp]
 
 lemma starfunRC_divide:
   "( *fRc* f) y  / ( *fRc* g) y = ( *fRc* (%x. f x / g x)) y"
-apply (simp add: divide_inverse_zero)
-done
+by (simp add: divide_inverse)
 declare starfunRC_divide [symmetric, simp]
 
 
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Complex/Complex.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -1,4 +1,5 @@
 (*  Title:       Complex.thy
+    ID:      $Id$
     Author:      Jacques D. Fleuriot
     Copyright:   2001 University of Edinburgh
     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
@@ -216,7 +217,7 @@
 apply (induct z)
 apply (rename_tac x y)
 apply (auto simp add: complex_mult complex_inverse complex_one_def
-       complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
+      complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
 apply (drule_tac y = y in real_sum_squares_not_zero)
 apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto)
 done
@@ -248,20 +249,17 @@
   show "(u + v) * w = u * w + v * w"
     by (simp add: complex_mult_def complex_add_def left_distrib 
                   diff_minus add_ac)
-  assume neq: "w \<noteq> 0"
-  thus "z / w = z * inverse w"
+  show "z / w = z * inverse w"
     by (simp add: complex_divide_def)
-  show "inverse w * w = 1"
-    by (simp add: neq complex_mult_inv_left)
+  assume "w \<noteq> 0"
+  thus "inverse w * w = 1"
+    by (simp add: complex_mult_inv_left)
 qed
 
 instance complex :: division_by_zero
 proof
-  show inv: "inverse 0 = (0::complex)"
+  show "inverse 0 = (0::complex)"
     by (simp add: complex_inverse_def complex_zero_def)
-  fix x :: complex
-  show "x/0 = 0"
-    by (simp add: complex_divide_def inv)
 qed
 
 
@@ -789,7 +787,7 @@
               complex_diff_def)
 
 lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
-by (simp add: divide_inverse_zero rcis_def complex_of_real_inverse)
+by (simp add: divide_inverse rcis_def complex_of_real_inverse)
 
 lemma cis_divide: "cis a / cis b = cis (a - b)"
 by (simp add: complex_divide_def cis_mult real_diff_def)
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Complex/NSCA.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -56,7 +56,7 @@
 done
 
 lemma SComplex_divide: "[| x \<in> SComplex;  y \<in> SComplex |] ==> x/y \<in> SComplex"
-by (simp add: SComplex_mult SComplex_inverse divide_inverse_zero)
+by (simp add: SComplex_mult SComplex_inverse divide_inverse)
 
 lemma SComplex_minus: "x \<in> SComplex ==> -x \<in> SComplex"
 apply (simp add: SComplex_def)
@@ -98,7 +98,7 @@
 
 lemma SComplex_divide_number_of:
      "r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex"
-apply (simp only: divide_inverse_zero)
+apply (simp only: divide_inverse)
 apply (blast intro!: SComplex_number_of SComplex_mult SComplex_inverse)
 done
 
@@ -618,7 +618,7 @@
 lemma CInfinitesimal_ratio:
      "[| y \<noteq> 0;  y \<in> CInfinitesimal;  x/y \<in> CFinite |] ==> x \<in> CInfinitesimal"
 apply (drule CInfinitesimal_CFinite_mult2, assumption)
-apply (simp add: divide_inverse_zero hcomplex_mult_assoc)
+apply (simp add: divide_inverse hcomplex_mult_assoc)
 done
 
 lemma SComplex_capprox_iff:
@@ -1126,7 +1126,7 @@
 lemma stc_divide [simp]:
      "[| x \<in> CFinite; y \<in> CFinite; stc y \<noteq> 0 |]  
       ==> stc(x/y) = (stc x) / (stc y)"
-by (simp add: divide_inverse_zero stc_mult stc_not_CInfinitesimal CFinite_inverse stc_inverse)
+by (simp add: divide_inverse stc_mult stc_not_CInfinitesimal CFinite_inverse stc_inverse)
 
 lemma stc_idempotent [simp]: "x \<in> CFinite ==> stc(stc(x)) = stc(x)"
 by (blast intro: stc_CFinite stc_capprox_self capprox_stc_eq)
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -1,9 +1,12 @@
 (*  Title:       NSComplex.thy
+    ID:      $Id$
     Author:      Jacques D. Fleuriot
     Copyright:   2001  University of Edinburgh
-    Description: Nonstandard Complex numbers
+    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
 *)
 
+header{*Nonstandard Complex Numbers*}
+
 theory NSComplex = NSInduct:
 
 constdefs
@@ -394,20 +397,17 @@
     by (rule hcomplex_zero_not_eq_one)
   show "(u + v) * w = u * w + v * w"
     by (simp add: hcomplex_add_mult_distrib)
-  assume neq: "w \<noteq> 0"
-  thus "z / w = z * inverse w"
+  show "z / w = z * inverse w"
     by (simp add: hcomplex_divide_def)
-  show "inverse w * w = 1"
+  assume "w \<noteq> 0"
+  thus "inverse w * w = 1"
     by (rule hcomplex_mult_inv_left)
 qed
 
 instance hcomplex :: division_by_zero
 proof
-  show inv: "inverse 0 = (0::hcomplex)"
+  show "inverse 0 = (0::hcomplex)"
     by (simp add: hcomplex_inverse hcomplex_zero_def)
-  fix x :: hcomplex
-  show "x/0 = 0"
-    by (simp add: hcomplex_divide_def inv)
 qed
 
 
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Divides.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -14,8 +14,6 @@
   div < type
 
 instance  nat :: div ..
-instance  nat :: plus_ac0
-proof qed (rule add_commute add_assoc add_0)+
 
 consts
   div  :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a"          (infixl 70)
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Finite_Set.thy
     ID:         $Id$
     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
+                Additions by Jeremy Avigad in Feb 2004
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
@@ -8,6 +9,65 @@
 
 theory Finite_Set = Divides + Power + Inductive + SetInterval:
 
+subsection {* Types Classes @{text plus_ac0} and @{text times_ac1} *}
+
+axclass plus_ac0 < plus, zero
+  commute:     "x + y = y + x"
+  assoc:       "(x + y) + z = x + (y + z)"
+  zero [simp]: "0 + x = x"
+
+lemma plus_ac0_left_commute: "x + (y+z) = y + ((x+z)::'a::plus_ac0)"
+apply (rule plus_ac0.commute [THEN trans])
+apply (rule plus_ac0.assoc [THEN trans])
+apply (rule plus_ac0.commute [THEN arg_cong])
+done
+
+lemma plus_ac0_zero_right [simp]: "x + 0 = (x ::'a::plus_ac0)"
+apply (rule plus_ac0.commute [THEN trans])
+apply (rule plus_ac0.zero)
+done
+
+lemmas plus_ac0 = plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute
+                  plus_ac0.zero plus_ac0_zero_right
+
+instance semiring < plus_ac0
+proof qed (rule add_commute add_assoc almost_semiring.add_0)+
+
+axclass times_ac1 < times, one
+  commute: "x * y = y * x"
+  assoc:   "(x * y) * z = x * (y * z)"
+  one:    "1 * x = x"
+
+theorem times_ac1_left_commute: "(x::'a::times_ac1) * ((y::'a) * z) =
+  y * (x * z)"
+proof -
+  have "(x::'a::times_ac1) * (y * z) = (x * y) * z"
+    by (rule times_ac1.assoc [THEN sym])
+  also have "x * y = y * x"
+    by (rule times_ac1.commute)
+  also have "(y * x) * z = y * (x * z)"
+    by (rule times_ac1.assoc)
+  finally show ?thesis .
+qed
+
+theorem times_ac1_one_right: "(x::'a::times_ac1) * 1 = x"
+proof -
+  have "x * 1 = 1 * x"
+    by (rule times_ac1.commute)
+  also have "... = x"
+    by (rule times_ac1.one)
+  finally show ?thesis .
+qed
+
+instance semiring < times_ac1
+  apply intro_classes
+  apply (rule mult_commute)
+  apply (rule mult_assoc, simp)
+  done
+
+theorems times_ac1 = times_ac1.assoc times_ac1.commute times_ac1_left_commute
+  times_ac1.one times_ac1_one_right
+
 subsection {* Collection of finite sets *}
 
 consts Finites :: "'a set set"
@@ -25,8 +85,8 @@
   finite: "finite UNIV"
 
 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
- "\<lbrakk> ~finite(UNIV::'a set); finite A \<rbrakk> \<Longrightarrow> \<exists>a::'a. a ~: A"
-by(subgoal_tac "A ~= UNIV", blast, blast)
+ "[| ~finite(UNIV::'a set); finite A  |] ==> \<exists>a::'a. a \<notin> A"
+by(subgoal_tac "A \<noteq> UNIV", blast, blast)
 
 
 lemma finite_induct [case_names empty insert, induct set: Finites]:
@@ -167,6 +227,11 @@
   -- {* The image of a finite set is finite. *}
   by (induct set: Finites) simp_all
 
+lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
+  apply (frule finite_imageI)
+  apply (erule finite_subset, assumption)
+  done
+
 lemma finite_range_imageI:
     "finite (range g) ==> finite (range (%x. f (g x)))"
   apply (drule finite_imageI, simp)
@@ -195,16 +260,16 @@
 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
   -- {* The inverse image of a singleton under an injective function
          is included in a singleton. *}
-  apply (auto simp add: inj_on_def) 
-  apply (blast intro: the_equality [symmetric]) 
+  apply (auto simp add: inj_on_def)
+  apply (blast intro: the_equality [symmetric])
   done
 
 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
   -- {* The inverse image of a finite set under an injective function
          is finite. *}
-  apply (induct set: Finites, simp_all) 
-  apply (subst vimage_insert) 
-  apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
+  apply (induct set: Finites, simp_all)
+  apply (subst vimage_insert)
+  apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
   done
 
 
@@ -215,10 +280,10 @@
 
 text {*
   Strengthen RHS to
-  @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x ~= {}})"}?
+  @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
 
   We'd need to prove
-  @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x ~= {}}"}
+  @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
   by induction. *}
 
 lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
@@ -281,6 +346,9 @@
   apply simp
   done
 
+
+subsubsection {* Intervals of nats *}
+
 lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
   by (induct k) (simp_all add: lessThan_Suc)
 
@@ -337,6 +405,10 @@
    apply (auto simp add: finite_Field)
   done
 
+lemma finite_cartesian_product: "[| finite A; finite B |] ==>
+    finite (A <*> B)"
+  by (rule finite_SigmaI)
+
 
 subsection {* Finite cardinality *}
 
@@ -521,8 +593,7 @@
   done
 
 lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
-  apply (induct set: Finites, simp_all, atomize)
-  apply safe
+  apply (induct set: Finites, simp_all, atomize, safe)
    apply (unfold inj_on_def, blast)
   apply (subst card_insert_disjoint)
     apply (erule finite_imageI, blast, blast)
@@ -553,7 +624,7 @@
 lemma dvd_partition:
   "finite C ==> finite (Union C) ==>
     ALL c : C. k dvd card c ==>
-    (ALL c1: C. ALL c2: C. c1 ~= c2 --> c1 Int c2 = {}) ==>
+    (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
   k dvd card (Union C)"
   apply (induct set: Finites, simp_all, clarify)
   apply (subst card_Un_disjoint)
@@ -784,10 +855,6 @@
   apply (erule finite_induct, auto)
   done
 
-lemma setsum_eq_0_iff [simp]:
-    "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
-  by (induct set: Finites) auto
-
 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   apply (case_tac "finite A")
    prefer 2 apply (simp add: setsum_def)
@@ -825,6 +892,14 @@
   apply (simp add: setsum_Un_disjoint)
   done
 
+lemma setsum_Union_disjoint:
+  "finite C ==> (ALL A:C. finite A) ==>
+        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+      setsum f (Union C) = setsum (setsum f) C"
+  apply (frule setsum_UN_disjoint [of C id f])
+  apply (unfold Union_def id_def, assumption+)
+  done
+
 lemma setsum_addf: "setsum (\<lambda>x. f x + g x) A = (setsum f A + setsum g A)"
   apply (case_tac "finite A")
    prefer 2 apply (simp add: setsum_def)
@@ -832,21 +907,6 @@
   apply (simp add: plus_ac0)
   done
 
-lemma setsum_Un: "finite A ==> finite B ==>
-    (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
-  -- {* For the natural numbers, we have subtraction. *}
-  apply (subst setsum_Un_Int [symmetric], auto)
-  done
-
-lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
-    (if a:A then setsum f A - f a else setsum f A)"
-  apply (case_tac "finite A")
-   prefer 2 apply (simp add: setsum_def)
-  apply (erule finite_induct)
-   apply (auto simp add: insert_Diff_if)
-  apply (drule_tac a = a in mk_disjoint_insert, auto)
-  done
-
 lemma setsum_cong:
   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   apply (case_tac "finite B")
@@ -865,12 +925,356 @@
   apply (simp add: Ball_def del:insert_Diff_single)
   done
 
-subsubsection{* Min and Max of finite linearly ordered sets *}
+lemma card_UN_disjoint:
+  fixes f :: "'a => 'b::plus_ac0"
+  shows
+    "finite I ==> (ALL i:I. finite (A i)) ==>
+        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+      card (UNION I A) = setsum (\<lambda>i. card (A i)) I"
+  apply (subst card_eq_setsum)
+  apply (subst finite_UN, assumption+)
+  apply (subgoal_tac "setsum (\<lambda>i. card (A i)) I =
+      setsum (%i. (setsum (%x. 1) (A i))) I")
+  apply (erule ssubst)
+  apply (erule setsum_UN_disjoint, assumption+)
+  apply (rule setsum_cong)
+  apply (simp, simp add: card_eq_setsum)
+  done
+
+lemma card_Union_disjoint:
+  "finite C ==> (ALL A:C. finite A) ==>
+        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+      card (Union C) = setsum card C"
+  apply (frule card_UN_disjoint [of C id])
+  apply (unfold Union_def id_def, assumption+)
+  done
+
+lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
+  apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
+  apply (erule ssubst, rule setsum_0)
+  apply (rule setsum_cong, auto)
+  done
+
+
+subsubsection {* Reindexing sums *}
+
+lemma setsum_reindex [rule_format]: "finite B ==>
+                  inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
+apply (rule finite_induct, assumption, force)
+apply (rule impI, auto)
+apply (simp add: inj_on_def)
+apply (subgoal_tac "f x \<notin> f ` F")
+apply (subgoal_tac "finite (f ` F)")
+apply (auto simp add: setsum_insert)
+apply (simp add: inj_on_def)
+  done
+
+lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
+    setsum f B = setsum id (f ` B)"
+by (auto simp add: setsum_reindex id_o)
+
+
+subsubsection {* Properties in more restricted classes of structures *}
+
+lemma setsum_eq_0_iff [simp]:
+    "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
+  by (induct set: Finites) auto
+
+lemma setsum_constant_nat:
+    "finite A ==> (\<Sum>x: A. y) = (card A) * y"
+  -- {* Later generalized to any semiring. *}
+  by (erule finite_induct, auto)
+
+lemma setsum_Un: "finite A ==> finite B ==>
+    (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
+  -- {* For the natural numbers, we have subtraction. *}
+  by (subst setsum_Un_Int [symmetric], auto)
+
+lemma setsum_Un_ring: "finite A ==> finite B ==>
+    (setsum f (A Un B) :: 'a :: ring) =
+      setsum f A + setsum f B - setsum f (A Int B)"
+  apply (subst setsum_Un_Int [symmetric], auto)
+  apply (simp add: compare_rls)
+  done
+
+lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
+    (if a:A then setsum f A - f a else setsum f A)"
+  apply (case_tac "finite A")
+   prefer 2 apply (simp add: setsum_def)
+  apply (erule finite_induct)
+   apply (auto simp add: insert_Diff_if)
+  apply (drule_tac a = a in mk_disjoint_insert, auto)
+  done
+
+lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ring) A =
+  - setsum f A"
+  by (induct set: Finites, auto)
+
+lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ring) - g x) A =
+  setsum f A - setsum g A"
+  by (simp add: diff_minus setsum_addf setsum_negf)
+
+lemma setsum_nonneg: "[| finite A;
+    \<forall>x \<in> A. (0::'a::ordered_semiring) \<le> f x |] ==>
+    0 \<le>  setsum f A";
+  apply (induct set: Finites, auto)
+  apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
+  apply (blast intro: add_mono)
+  done
+
+subsubsection {* Cardinality of Sigma and Cartesian product *}
+
+lemma SigmaI_insert: "y \<notin> A ==>
+  (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
+  by auto
+
+lemma card_cartesian_product_singleton [simp]: "finite A ==>
+    card({x} <*> A) = card(A)"
+  apply (subgoal_tac "inj_on (%y .(x,y)) A")
+  apply (frule card_image, assumption)
+  apply (subgoal_tac "(Pair x ` A) = {x} <*> A")
+  apply (auto simp add: inj_on_def)
+  done
+
+lemma card_SigmaI [rule_format,simp]: "finite A ==>
+  (ALL a:A. finite (B a)) -->
+  card (SIGMA x: A. B x) = (\<Sum>a: A. card (B a))"
+  apply (erule finite_induct, auto)
+  apply (subst SigmaI_insert, assumption)
+  apply (subst card_Un_disjoint)
+  apply (auto intro: finite_SigmaI)
+  done
+
+lemma card_cartesian_product [simp]: "[| finite A; finite B |] ==>
+  card (A <*> B) = card(A) * card(B)"
+  apply (subst card_SigmaI, assumption+)
+  apply (simp add: setsum_constant_nat)
+  done
+
+
+subsection {* Generalized product over a set *}
+
+constdefs
+  setprod :: "('a => 'b) => 'a set => 'b::times_ac1"
+  "setprod f A == if finite A then fold (op * o f) 1 A else 1"
+
+syntax
+  "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
+                ("\<Prod>_:_. _" [0, 51, 10] 10)
+
+syntax (xsymbols)
+  "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
+                ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
+translations
+  "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
+
+
+lemma setprod_empty [simp]: "setprod f {} = 1"
+  by (auto simp add: setprod_def)
+
+lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
+    setprod f (insert a A) = f a * setprod f A"
+  by (auto simp add: setprod_def LC_def LC.fold_insert
+      times_ac1_left_commute)
+
+lemma setprod_1: "setprod (\<lambda>i. 1) A = 1"
+  apply (case_tac "finite A")
+  apply (erule finite_induct, auto simp add: times_ac1)
+  apply (simp add: setprod_def)
+  done
+
+lemma setprod_Un_Int: "finite A ==> finite B
+    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
+  apply (induct set: Finites, simp)
+  apply (simp add: times_ac1 insert_absorb)
+  apply (simp add: times_ac1 Int_insert_left insert_absorb)
+  done
+
+lemma setprod_Un_disjoint: "finite A ==> finite B
+  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
+  apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
+  done
+
+lemma setprod_UN_disjoint:
+  fixes f :: "'a => 'b::times_ac1"
+  shows
+    "finite I ==> (ALL i:I. finite (A i)) ==>
+        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+      setprod f (UNION I A) = setprod (\<lambda>i. setprod f (A i)) I"
+  apply (induct set: Finites, simp, atomize)
+  apply (subgoal_tac "ALL i:F. x \<noteq> i")
+   prefer 2 apply blast
+  apply (subgoal_tac "A x Int UNION F A = {}")
+   prefer 2 apply blast
+  apply (simp add: setprod_Un_disjoint)
+  done
+
+lemma setprod_Union_disjoint:
+  "finite C ==> (ALL A:C. finite A) ==>
+        (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+      setprod f (Union C) = setprod (setprod f) C"
+  apply (frule setprod_UN_disjoint [of C id f])
+  apply (unfold Union_def id_def, assumption+)
+  done
+
+lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A =
+    (setprod f A * setprod g A)"
+  apply (case_tac "finite A")
+   prefer 2 apply (simp add: setprod_def times_ac1)
+  apply (erule finite_induct, auto)
+  apply (simp add: times_ac1)
+  apply (simp add: times_ac1)
+  done
+
+lemma setprod_cong:
+  "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
+  apply (case_tac "finite B")
+   prefer 2 apply (simp add: setprod_def, simp)
+  apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setprod f C = setprod g C")
+   apply simp
+  apply (erule finite_induct, simp)
+  apply (simp add: subset_insert_iff, clarify)
+  apply (subgoal_tac "finite C")
+   prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
+  apply (subgoal_tac "C = insert x (C - {x})")
+   prefer 2 apply blast
+  apply (erule ssubst)
+  apply (drule spec)
+  apply (erule (1) notE impE)
+  apply (simp add: Ball_def del:insert_Diff_single)
+  done
+
+lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
+  apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
+  apply (erule ssubst, rule setprod_1)
+  apply (rule setprod_cong, auto)
+  done
+
+
+subsubsection {* Reindexing products *}
+
+lemma setprod_reindex [rule_format]: "finite B ==>
+                  inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
+apply (rule finite_induct, assumption, force)
+apply (rule impI, auto)
+apply (simp add: inj_on_def)
+apply (subgoal_tac "f x \<notin> f ` F")
+apply (subgoal_tac "finite (f ` F)")
+apply (auto simp add: setprod_insert)
+apply (simp add: inj_on_def)
+  done
+
+lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
+    setprod f B = setprod id (f ` B)"
+by (auto simp add: setprod_reindex id_o)
+
+
+subsubsection {* Properties in more restricted classes of structures *}
+
+lemma setprod_eq_1_iff [simp]:
+    "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
+  by (induct set: Finites) auto
+
+lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::ringpower)) =
+    y^(card A)"
+  apply (erule finite_induct)
+  apply (auto simp add: power_Suc)
+  done
+
+lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::semiring) ==>
+    setprod f A = 0"
+  apply (induct set: Finites, force, clarsimp)
+  apply (erule disjE, auto)
+  done
+
+lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_ring) \<le> f x)
+     --> 0 \<le> setprod f A"
+  apply (case_tac "finite A")
+  apply (induct set: Finites, force, clarsimp)
+  apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
+  apply (rule mult_mono, assumption+)
+  apply (auto simp add: setprod_def)
+  done
+
+lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_ring) < f x)
+     --> 0 < setprod f A"
+  apply (case_tac "finite A")
+  apply (induct set: Finites, force, clarsimp)
+  apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
+  apply (rule mult_strict_mono, assumption+)
+  apply (auto simp add: setprod_def)
+  done
+
+lemma setprod_nonzero [rule_format]:
+    "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
+      finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
+  apply (erule finite_induct, auto)
+  done
+
+lemma setprod_zero_eq:
+    "(ALL x y. (x::'a::semiring) * y = 0 --> x = 0 | y = 0) ==>
+     finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
+  apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
+  done
+
+lemma setprod_nonzero_field:
+    "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
+  apply (rule setprod_nonzero, auto)
+  done
+
+lemma setprod_zero_eq_field:
+    "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
+  apply (rule setprod_zero_eq, auto)
+  done
+
+lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
+    (setprod f (A Un B) :: 'a ::{field})
+      = setprod f A * setprod f B / setprod f (A Int B)"
+  apply (subst setprod_Un_Int [symmetric], auto)
+  apply (subgoal_tac "finite (A Int B)")
+  apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
+  apply (subst times_divide_eq_right [THEN sym], auto)
+  done
+
+lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
+    (setprod f (A - {a}) :: 'a :: {field}) =
+      (if a:A then setprod f A / f a else setprod f A)"
+  apply (erule finite_induct)
+   apply (auto simp add: insert_Diff_if)
+  apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
+  apply (erule ssubst)
+  apply (subst times_divide_eq_right [THEN sym])
+  apply (auto simp add: mult_ac)
+  done
+
+lemma setprod_inversef: "finite A ==>
+    ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
+      setprod (inverse \<circ> f) A = inverse (setprod f A)"
+  apply (erule finite_induct)
+  apply (simp, simp)
+  done
+
+lemma setprod_dividef:
+     "[|finite A;
+        \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
+      ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
+  apply (subgoal_tac
+         "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
+  apply (erule ssubst)
+  apply (subst divide_inverse)
+  apply (subst setprod_timesf)
+  apply (subst setprod_inversef, assumption+, rule refl)
+  apply (rule setprod_cong, rule refl)
+  apply (subst divide_inverse, auto)
+  done
+
+
+subsection{* Min and Max of finite linearly ordered sets *}
 
 text{* Seemed easier to define directly than via fold. *}
 
 lemma ex_Max: fixes S :: "('a::linorder)set"
-  assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
+  assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
 using fin
 proof (induct)
   case empty thus ?case by simp
@@ -886,14 +1290,14 @@
     proof (cases)
       assume "x \<le> m" thus ?thesis using m by blast
     next
-      assume "\<not> x \<le> m" thus ?thesis using m
+      assume "~ x \<le> m" thus ?thesis using m
 	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
     qed
   qed
 qed
 
 lemma ex_Min: fixes S :: "('a::linorder)set"
-  assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
+  assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
 using fin
 proof (induct)
   case empty thus ?case by simp
@@ -909,18 +1313,18 @@
     proof (cases)
       assume "m \<le> x" thus ?thesis using m by blast
     next
-      assume "\<not> m \<le> x" thus ?thesis using m
+      assume "~ m \<le> x" thus ?thesis using m
 	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
     qed
   qed
 qed
 
 constdefs
- Min :: "('a::linorder)set \<Rightarrow> 'a"
-"Min S  \<equiv>  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
+ Min :: "('a::linorder)set => 'a"
+"Min S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
 
- Max :: "('a::linorder)set \<Rightarrow> 'a"
-"Max S  \<equiv>  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
+ Max :: "('a::linorder)set => 'a"
+"Max S  ==  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
 
 lemma Min[simp]: assumes a: "finite S" "S \<noteq> {}"
                  shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
@@ -946,6 +1350,7 @@
   qed
 qed
 
+subsection {* Theorems about @{text "choose"} *}
 
 text {*
   \medskip Basic theorem about @{text "choose"}.  By Florian
@@ -965,7 +1370,7 @@
   apply safe
    apply (auto intro: finite_subset [THEN card_insert_disjoint])
   apply (drule_tac x = "xa - {x}" in spec)
-  apply (subgoal_tac "x ~: xa", auto)
+  apply (subgoal_tac "x \<notin> xa", auto)
   apply (erule rev_mp, subst card_Diff_singleton)
   apply (auto intro: finite_subset)
   done
@@ -974,8 +1379,8 @@
     "[|inj_on f A; f ` A \<subseteq> B; finite A; finite B |] ==> card A <= card B"
   by (auto intro: card_mono simp add: card_image [symmetric])
 
-lemma card_bij_eq: 
-    "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A; 
+lemma card_bij_eq:
+    "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
        finite A; finite B |] ==> card A = card B"
   by (auto intro: le_anti_sym card_inj_on_le)
 
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/HOL.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -197,11 +197,6 @@
 syntax (HTML output)
   abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
 
-axclass plus_ac0 < plus, zero
-  commute: "x + y = y + x"
-  assoc:   "(x + y) + z = x + (y + z)"
-  zero:    "0 + x = x"
-
 
 subsection {* Theory and package setup *}
 
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/HOL_lemmas.ML	Thu Mar 04 12:06:07 2004 +0100
@@ -446,21 +446,6 @@
 by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ;
 qed "exCI";
 
-Goal "x + (y+z) = y + ((x+z)::'a::plus_ac0)";
-by (rtac (thm"plus_ac0.commute" RS trans) 1);
-by (rtac (thm"plus_ac0.assoc" RS trans) 1);
-by (rtac (thm"plus_ac0.commute" RS arg_cong) 1);
-qed "plus_ac0_left_commute";
-
-Goal "x + 0 = (x ::'a::plus_ac0)";
-by (rtac (thm"plus_ac0.commute" RS trans) 1);
-by (rtac (thm"plus_ac0.zero") 1);
-qed "plus_ac0_zero_right";
-
-bind_thms ("plus_ac0", [thm"plus_ac0.assoc", thm"plus_ac0.commute",
-                        plus_ac0_left_commute,
-                        thm"plus_ac0.zero", plus_ac0_zero_right]);
-
 (* case distinction *)
 
 val [prem1,prem2] = Goal "[| P ==> Q; ~P ==> Q |] ==> Q";
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Hyperreal/EvenOdd.ML
--- a/src/HOL/Hyperreal/EvenOdd.ML	Thu Mar 04 10:06:13 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,366 +0,0 @@
-(*  Title       : Even.ML
-    Author      : Jacques D. Fleuriot  
-    Copyright   : 1999  University of Edinburgh
-    Description : Even numbers defined
-*)
-
-Goal "even(Suc(Suc n)) = (even(n))";
-by (Auto_tac);
-qed "even_Suc_Suc";
-Addsimps [even_Suc_Suc];
-
-Goal "(even(n)) = (~odd(n))";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "even_not_odd";
-
-Goal "(odd(n)) = (~even(n))";
-by (simp_tac (simpset() addsimps [even_not_odd]) 1);
-qed "odd_not_even";
-
-Goal "even(2*n)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "even_mult_two";
-Addsimps [even_mult_two];
-
-Goal "even(n*2)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "even_mult_two'";
-Addsimps [even_mult_two'];
-
-Goal "even(n + n)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "even_sum_self";
-Addsimps [even_sum_self];
-
-Goal "~odd(2*n)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "not_odd_self_mult2";
-Addsimps [not_odd_self_mult2];
-
-Goal "~odd(n + n)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "not_odd_sum_self";
-Addsimps [not_odd_sum_self];
-
-Goal "~even(Suc(n + n))";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "not_even_Suc_sum_self";
-Addsimps [not_even_Suc_sum_self];
-
-Goal "odd(Suc(2*n))";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "odd_mult_two_add_one";
-Addsimps [odd_mult_two_add_one];
-
-Goal "odd(Suc(n + n))";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "odd_sum_Suc_self";
-Addsimps [odd_sum_Suc_self];
-
-Goal "even(Suc n) = odd(n)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "even_Suc_odd_iff";
-
-Goal "odd(Suc n) = even(n)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "odd_Suc_even_iff";
-
-Goal "even n | odd n";
-by (simp_tac (simpset() addsimps [even_not_odd]) 1);
-qed "even_odd_disj";
-
-(* could be proved automatically before: spoiled by numeral arith! *)
-Goal "EX m. (n = 2*m | n = Suc(2*m))";
-by (induct_tac "n" 1 THEN Auto_tac);
-by (res_inst_tac [("x","Suc m")] exI 1 THEN Auto_tac);
-qed "nat_mult_two_Suc_disj";
-
-Goal "even(n) = (EX m. n = 2*m)";
-by (cut_inst_tac [("n","n")] nat_mult_two_Suc_disj 1);
-by (Auto_tac);
-qed "even_mult_two_ex";
-
-Goal "odd(n) = (EX m. n = Suc (2*m))";
-by (cut_inst_tac [("n","n")] nat_mult_two_Suc_disj 1);
-by (Auto_tac);
-qed "odd_Suc_mult_two_ex";
-
-Goal "even(n) ==> even(m*n)";
-by (auto_tac (claset(),
-              simpset() addsimps [add_mult_distrib2, even_mult_two_ex]));
-qed "even_mult_even";
-Addsimps [even_mult_even];
-
-Goal "(m + m) div 2 = (m::nat)";
-by (arith_tac 1);
-qed "div_add_self_two_is_m";
-Addsimps [div_add_self_two_is_m];
-
-Goal "Suc(Suc(m*2)) div 2 = Suc m";
-by (arith_tac 1);
-qed "div_mult_self_Suc_Suc";
-Addsimps [div_mult_self_Suc_Suc];
-
-Goal "Suc(Suc(2*m)) div 2 = Suc m";
-by (arith_tac 1);
-qed "div_mult_self_Suc_Suc2";
-Addsimps [div_mult_self_Suc_Suc2];
-
-Goal "Suc(Suc(m + m)) div 2 = Suc m";
-by (arith_tac 1);
-qed "div_add_self_Suc_Suc";
-Addsimps [div_add_self_Suc_Suc];
-
-Goal "~ even n ==> (Suc n) div 2 = Suc((n - 1) div 2)";
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym,
-    odd_Suc_mult_two_ex]));
-qed "not_even_imp_Suc_Suc_diff_one_eq";
-Addsimps [not_even_imp_Suc_Suc_diff_one_eq];
-
-Goal "even(m + n) = (even m = even n)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "even_add";
-AddIffs [even_add];
-
-Goal "even(m * n) = (even m | even n)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "even_mult";
-
-Goal "even (m ^ n) = (even m & n ~= 0)";
-by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [even_mult]));
-qed "even_pow";
-AddIffs [even_pow];
-
-Goal "odd(m + n) = (odd m ~= odd n)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "odd_add";
-AddIffs [odd_add];
-
-Goal "odd(m * n) = (odd m & odd n)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "odd_mult";
-AddIffs [odd_mult];
-
-Goal "odd (m ^ n) = (odd m | n = 0)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "odd_pow";
-
-Goal "0 < n --> ~even (n + n - 1)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed_spec_mp "not_even_2n_minus_1";
-Addsimps [not_even_2n_minus_1];
-
-Goal "Suc (2 * m) mod 2 = 1";
-by (induct_tac "m" 1);
-by (auto_tac (claset(),simpset() addsimps [mod_Suc]));
-qed "mod_two_Suc_2m";
-Addsimps [mod_two_Suc_2m];
-
-Goal "(Suc (Suc (2 * m)) div 2) = Suc m";
-by (arith_tac 1);
-qed "div_two_Suc_Suc_2m";
-Addsimps [div_two_Suc_Suc_2m];
-
-Goal "even n ==> 2 * ((n + 1) div 2) = n";
-by (auto_tac (claset(),simpset() addsimps [mult_div_cancel,
-    even_mult_two_ex]));
-qed "lemma_even_div";
-Addsimps [lemma_even_div];
-
-Goal "~even n ==> 2 * ((n + 1) div 2) = Suc n";
-by (auto_tac (claset(),simpset() addsimps [even_not_odd,
-    odd_Suc_mult_two_ex]));
-qed "lemma_not_even_div";
-Addsimps [lemma_not_even_div];
-
-Goal "Suc n div 2 <= Suc (Suc n) div 2";
-by (arith_tac 1);
-qed "Suc_n_le_Suc_Suc_n_div_2";
-Addsimps [Suc_n_le_Suc_Suc_n_div_2];
-
-Goal "(0::nat) < n --> 0 < (n + 1) div 2";
-by (arith_tac 1);
-qed_spec_mp "Suc_n_div_2_gt_zero";
-Addsimps [Suc_n_div_2_gt_zero];
-
-Goal "0 < n & even n --> 1 < n";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed_spec_mp "even_gt_zero_gt_one_aux";
-bind_thm ("even_gt_zero_gt_one",conjI RS even_gt_zero_gt_one_aux);
-
-(* more general *)
-Goal "n div 2 <= (Suc n) div 2";
-by (arith_tac 1);
-qed "le_Suc_n_div_2";
-Addsimps [le_Suc_n_div_2];
-
-Goal "(1::nat) < n --> 0 < n div 2";
-by (arith_tac 1);
-qed_spec_mp "div_2_gt_zero";
-Addsimps [div_2_gt_zero];
-
-Goal "even n ==> (n + 1) div 2 = n div 2";
-by (rtac (CLAIM "2 * x = 2 * y ==> x = (y::nat)") 1);
-by (stac lemma_even_div 1);
-by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex]));
-qed "lemma_even_div2";
-Addsimps [lemma_even_div2];
-
-Goal "~even n ==> (n + 1) div 2 = Suc (n div 2)";
-by (rtac (CLAIM "2 * x = 2 * y ==> x = (y::nat)") 1);
-by (stac lemma_not_even_div 1);
-by (auto_tac (claset(),simpset() addsimps [even_not_odd,
-    odd_Suc_mult_two_ex])); 
-by (cut_inst_tac [("m","Suc(2*m)"),("n","2")] mod_div_equality 1); 
-by Auto_tac; 
-qed "lemma_not_even_div2";
-Addsimps [lemma_not_even_div2];
-
-Goal "(Suc n) div 2 = 0 ==> even n";
-by (rtac ccontr 1);
-by (dtac lemma_not_even_div2 1 THEN Auto_tac);
-qed "Suc_n_div_two_zero_even";
-
-Goal "0 < n ==> even n = (~ even(n - 1))";
-by (case_tac "n" 1);
-by Auto_tac;
-qed "even_num_iff";
-
-Goal "0 < n ==> odd n = (~ odd(n - 1))";
-by (case_tac "n" 1);
-by Auto_tac;
-qed "odd_num_iff";
-
-(* Some mod and div stuff *)
-
-Goal "n ~= (0::nat) ==> (m = m div n * n + m mod n) & m mod n < n";
-by (auto_tac (claset() addIs [mod_less_divisor],simpset()));
-qed "mod_div_eq_less";
-
-Goal "(k*n + m) mod n = m mod (n::nat)";
-by (simp_tac (simpset() addsimps mult_ac @ add_ac) 1);
-qed "mod_mult_self3";
-Addsimps [mod_mult_self3];
-
-Goal "Suc (k*n + m) mod n = Suc m mod n";
-by (rtac (CLAIM "Suc (m + n) = (m + Suc n)" RS ssubst) 1);
-by (rtac mod_mult_self3 1);
-qed "mod_mult_self4";
-Addsimps [mod_mult_self4];
-
-Goal "Suc m mod n = Suc (m mod n) mod n";
-by (cut_inst_tac [("d'","Suc (m mod n) mod n")] (CLAIM "EX d. d' = d") 1);
-by (etac exE 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("t","m"),("n1","n")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() delsimprocs [cancel_div_mod_proc]));
-qed "mod_Suc_eq_Suc_mod";
-
-Goal "even n = (even (n mod 4))";
-by (cut_inst_tac [("d'","(even (n mod 4))")] (CLAIM "EX d. d' = d") 1);
-by (etac exE 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [even_mult,even_num_iff] delsimprocs [cancel_div_mod_proc]));
-qed "even_even_mod_4_iff";
-
-Goal "odd n = (odd (n mod 4))";
-by (auto_tac (claset(),simpset() addsimps [odd_not_even,
-    even_even_mod_4_iff RS sym]));
-qed "odd_odd_mod_4_iff";
-
-Goal "odd n ==> ((-1) ^ n) = (-1::real)";
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
-qed "odd_realpow_minus_one";
-Addsimps [odd_realpow_minus_one];
-
-Goal "even(4*n)";
-by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex]));
-qed "even_4n";
-Addsimps [even_4n];
-
-Goal "n mod 4 = 0 ==> even(n div 2)";
-by Auto_tac;
-qed "lemma_even_div_2";
-
-Goal "n mod 4 = 0 ==> even(n)";
-by Auto_tac;
-qed "lemma_mod_4_even_n";
-
-Goal "n mod 4 = 1 ==> odd(n)";
-by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]));
-qed "lemma_mod_4_odd_n";
-
-Goal "n mod 4 = 2 ==> even(n)";
-by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [even_num_iff] delsimprocs [cancel_div_mod_proc]));
-qed "lemma_mod_4_even_n2";
-
-Goal "n mod 4 = 3 ==> odd(n)";
-by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]));
-qed "lemma_mod_4_odd_n2";
-
-Goal "even n ==> ((-1) ^ n) = (1::real)";
-by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex]));
-qed "even_realpow_minus_one";
-Addsimps [even_realpow_minus_one];
-
-Goal "((4 * n) + 2) div 2 = (2::nat) * n + 1";
-by (arith_tac 1);
-qed "lemma_4n_add_2_div_2_eq";
-Addsimps [lemma_4n_add_2_div_2_eq];
-
-Goal "(Suc(Suc(4 * n))) div 2 = (2::nat) * n + 1";
-by (arith_tac 1);
-qed "lemma_Suc_Suc_4n_div_2_eq";
-Addsimps [lemma_Suc_Suc_4n_div_2_eq];
-
-Goal "(Suc(Suc(n * 4))) div 2 = (2::nat) * n + 1";
-by (arith_tac 1);
-qed "lemma_Suc_Suc_4n_div_2_eq2";
-Addsimps [lemma_Suc_Suc_4n_div_2_eq2];
-
-Goal "n mod 4 = 3 ==> odd((n - 1) div 2)";
-by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (asm_full_simp_tac (simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]) 1);
-val lemma_odd_mod_4_div_2 = result();
-
-Goal "(4 * n) div 2 = (2::nat) * n";
-by (arith_tac 1);
-qed "lemma_4n_div_2_eq";
-Addsimps [lemma_4n_div_2_eq];
-
-Goal "(n  * 4) div 2 = (2::nat) * n";
-by (arith_tac 1);
-qed "lemma_4n_div_2_eq2";
-Addsimps [lemma_4n_div_2_eq2];
-
-Goal "n mod 4 = 1 ==> even ((n - 1) div 2)";
-by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (dtac ssubst 1 THEN assume_tac 2);
-by (rtac ((CLAIM "(n::nat) + 1 - 1 = n") RS ssubst) 1);
-by Auto_tac;
-val lemma_even_mod_4_div_2 = result();
-
-
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Hyperreal/EvenOdd.thy
--- a/src/HOL/Hyperreal/EvenOdd.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/EvenOdd.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -4,17 +4,163 @@
     Description : Even and odd numbers defined 
 *)
 
-EvenOdd = NthRoot +  
+header{*Compatibility file from Parity*}
+
+theory EvenOdd = NthRoot:
+
+subsection{*General Lemmas About Division*}
+
+lemma div_add_self_two_is_m: "(m + m) div 2 = (m::nat)"
+by arith
+declare div_add_self_two_is_m [simp]
+
+lemma div_mult_self_Suc_Suc: "Suc(Suc(m*2)) div 2 = Suc m"
+by arith
+declare div_mult_self_Suc_Suc [simp]
+
+lemma div_mult_self_Suc_Suc2: "Suc(Suc(2*m)) div 2 = Suc m"
+by arith
+declare div_mult_self_Suc_Suc2 [simp]
+
+lemma div_add_self_Suc_Suc: "Suc(Suc(m + m)) div 2 = Suc m"
+by arith
+declare div_add_self_Suc_Suc [simp]
+
+lemma mod_two_Suc_2m: "Suc (2 * m) mod 2 = 1" 
+apply (induct_tac "m")
+apply (auto simp add: mod_Suc)
+done
+declare mod_two_Suc_2m [simp]
+
+lemma Suc_n_le_Suc_Suc_n_div_2: "Suc n div 2 \<le> Suc (Suc n) div 2"
+by arith
+declare Suc_n_le_Suc_Suc_n_div_2 [simp]
+
+lemma Suc_n_div_2_gt_zero: "(0::nat) < n ==> 0 < (n + 1) div 2"
+by arith
+declare Suc_n_div_2_gt_zero [simp]
+
+lemma le_Suc_n_div_2: "n div 2 \<le> (Suc n) div 2"
+by arith
+declare le_Suc_n_div_2 [simp]
+
+lemma div_2_gt_zero: "(1::nat) < n ==> 0 < n div 2" 
+by arith
+declare div_2_gt_zero [simp]
+
+lemma mod_mult_self3: "(k*n + m) mod n = m mod (n::nat)"
+by (simp add: mult_ac add_ac)
+declare mod_mult_self3 [simp]
+
+lemma mod_mult_self4: "Suc (k*n + m) mod n = Suc m mod n"
+proof -
+  have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
+  also have "... = Suc m mod n" by (rule mod_mult_self3) 
+  finally show ?thesis .
+qed
+declare mod_mult_self4 [simp]
+
+lemma nat_mod_idem [simp]: "m mod n mod n = (m mod n :: nat)"
+by (case_tac "n=0", auto)
+
+lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
+apply (subst mod_Suc [of m]) 
+apply (subst mod_Suc [of "m mod n"], simp) 
+done
+
+lemma lemma_4n_add_2_div_2_eq: "((4 * n) + 2) div 2 = (2::nat) * n + 1"
+by arith
+declare lemma_4n_add_2_div_2_eq [simp]
+
+lemma lemma_Suc_Suc_4n_div_2_eq: "(Suc(Suc(4 * n))) div 2 = (2::nat) * n + 1"
+by arith
+declare lemma_Suc_Suc_4n_div_2_eq [simp]
+
+lemma lemma_Suc_Suc_4n_div_2_eq2: "(Suc(Suc(n * 4))) div 2 = (2::nat) * n + 1"
+by arith
+declare lemma_Suc_Suc_4n_div_2_eq2 [simp]
+
 
-consts even :: "nat => bool"
-primrec 
-   even_0   "even 0 = True"
-   even_Suc "even (Suc n) = (~ (even n))"    
+subsection{*More Even/Odd Results*}
+ 
+lemma even_mult_two_ex: "even(n) = (EX m::nat. n = 2*m)"
+by (simp add: even_nat_equiv_def2 numeral_2_eq_2)
+
+lemma odd_Suc_mult_two_ex: "odd(n) = (EX m. n = Suc (2*m))"
+by (simp add: odd_nat_equiv_def2 numeral_2_eq_2)
+
+lemma even_add: "even(m + n::nat) = (even m = even n)"
+by auto
+declare even_add [iff]
+
+lemma odd_add: "odd(m + n::nat) = (odd m ~= odd n)"
+by auto
+declare odd_add [iff]
+
+lemma lemma_even_div2: "even (n::nat) ==> (n + 1) div 2 = n div 2"
+apply (simp add: numeral_2_eq_2) 
+apply (subst div_Suc)  
+apply (simp add: even_nat_mod_two_eq_zero) 
+done
+declare lemma_even_div2 [simp]
+
+lemma lemma_not_even_div2: "~even n ==> (n + 1) div 2 = Suc (n div 2)"
+apply (simp add: numeral_2_eq_2) 
+apply (subst div_Suc)  
+apply (simp add: odd_nat_mod_two_eq_one) 
+done
+declare lemma_not_even_div2 [simp]
+
+lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))" 
+by (case_tac "n", auto)
+
+lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)"
+apply (induct n, simp)
+apply (subst mod_Suc, simp) 
+done
 
-consts odd :: "nat => bool"
-primrec 
-   odd_0   "odd 0 = False"
-   odd_Suc "odd (Suc n) = (~ (odd n))"    
+declare neg_one_odd_power [simp]
+declare neg_one_even_power [simp]
+
+lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)"
+apply (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst])
+apply (simp add: even_num_iff)
+done
+
+lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
+by (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst], simp)
+
+ML
+{*
+val even_Suc = thm"Parity.even_nat_suc";
+
+val even_mult_two_ex = thm "even_mult_two_ex";
+val odd_Suc_mult_two_ex = thm "odd_Suc_mult_two_ex";
+val div_add_self_two_is_m = thm "div_add_self_two_is_m";
+val div_mult_self_Suc_Suc = thm "div_mult_self_Suc_Suc";
+val div_mult_self_Suc_Suc2 = thm "div_mult_self_Suc_Suc2";
+val div_add_self_Suc_Suc = thm "div_add_self_Suc_Suc";
+val even_add = thm "even_add";
+val odd_add = thm "odd_add";
+val mod_two_Suc_2m = thm "mod_two_Suc_2m";
+val Suc_n_le_Suc_Suc_n_div_2 = thm "Suc_n_le_Suc_Suc_n_div_2";
+val Suc_n_div_2_gt_zero = thm "Suc_n_div_2_gt_zero";
+val le_Suc_n_div_2 = thm "le_Suc_n_div_2";
+val div_2_gt_zero = thm "div_2_gt_zero";
+val lemma_even_div2 = thm "lemma_even_div2";
+val lemma_not_even_div2 = thm "lemma_not_even_div2";
+val even_num_iff = thm "even_num_iff";
+val mod_mult_self3 = thm "mod_mult_self3";
+val mod_mult_self4 = thm "mod_mult_self4";
+val nat_mod_idem = thm "nat_mod_idem";
+val mod_Suc_eq_Suc_mod = thm "mod_Suc_eq_Suc_mod";
+val even_even_mod_4_iff = thm "even_even_mod_4_iff";
+val lemma_4n_add_2_div_2_eq = thm "lemma_4n_add_2_div_2_eq";
+val lemma_Suc_Suc_4n_div_2_eq = thm "lemma_Suc_Suc_4n_div_2_eq";
+val lemma_Suc_Suc_4n_div_2_eq2 = thm "lemma_Suc_Suc_4n_div_2_eq2";
+val lemma_odd_mod_4_div_2 = thm "lemma_odd_mod_4_div_2";
+val lemma_even_mod_4_div_2 = thm "lemma_even_mod_4_div_2";
+*}
 
 end
 
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Hyperreal/HLog.thy
--- a/src/HOL/Hyperreal/HLog.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/HLog.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -57,7 +57,7 @@
 lemma hypreal_divide: 
      "(Abs_hypreal(hyprel `` {X}))/(Abs_hypreal(hyprel `` {Y})) =  
       (Abs_hypreal(hyprel `` {%n. (X n)/(Y n)}))"
-by (simp add: divide_inverse_zero hypreal_zero_num hypreal_inverse hypreal_mult) 
+by (simp add: divide_inverse hypreal_zero_num hypreal_inverse hypreal_mult) 
 
 lemma powhr_divide:
      "[| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
@@ -96,7 +96,7 @@
 done
 
 lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
-by (simp add: divide_inverse_zero powhr_minus)
+by (simp add: divide_inverse powhr_minus)
 
 lemma powhr_less_mono: "[| a < b; 1 < x |] ==> x powhr a < x powhr b"
 apply (rule eq_Abs_hypreal [of x])
@@ -194,7 +194,7 @@
 apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
             HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 
         simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero 
-          hlog_as_starfun hypreal_not_refl2 [THEN not_sym] divide_inverse_zero)
+          hlog_as_starfun hypreal_not_refl2 [THEN not_sym] divide_inverse)
 done
 
 lemma hlog_HInfinite_as_starfun:
@@ -220,7 +220,7 @@
 
 lemma hlog_divide:
      "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y"
-by (simp add: hlog_mult hlog_inverse divide_inverse_zero)
+by (simp add: hlog_mult hlog_inverse divide_inverse)
 
 lemma hlog_less_cancel_iff [simp]:
      "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -555,13 +555,13 @@
      "n \<in> HNatInfinite  
       ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
 apply (frule lemma_sin_pi)
-apply (simp add: divide_inverse_zero)
+apply (simp add: divide_inverse)
 done
 
 lemma Infinitesimal_pi_divide_HNatInfinite: 
      "N \<in> HNatInfinite  
       ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
-apply (simp add: divide_inverse_zero)
+apply (simp add: divide_inverse)
 apply (auto intro: Infinitesimal_HFinite_mult2)
 done
 
@@ -578,7 +578,7 @@
                    pi_divide_HNatInfinite_not_zero])
 apply (auto simp add: hypreal_inverse_distrib)
 apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
-apply (auto intro: SReal_inverse simp add: divide_inverse_zero mult_ac)
+apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac)
 done
 
 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
@@ -593,7 +593,7 @@
 lemma starfunNat_pi_divide_n_Infinitesimal: 
      "N \<in> HNatInfinite ==> ( *fNat* (%x. pi / real x)) N \<in> Infinitesimal"
 by (auto intro!: Infinitesimal_HFinite_mult2 
-         simp add: starfunNat_mult [symmetric] divide_inverse_zero
+         simp add: starfunNat_mult [symmetric] divide_inverse
                    starfunNat_inverse [symmetric] starfunNat_real_of_nat)
 
 lemma STAR_sin_pi_divide_n_approx:
@@ -601,16 +601,16 @@
       ( *f* sin) (( *fNat* (%x. pi / real x)) N) @=  
       hypreal_of_real pi/(hypreal_of_hypnat N)"
 by (auto intro!: STAR_sin_Infinitesimal Infinitesimal_HFinite_mult2 
-         simp add: starfunNat_mult [symmetric] divide_inverse_zero
+         simp add: starfunNat_mult [symmetric] divide_inverse
                    starfunNat_inverse_real_of_nat_eq)
 
 lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi"
 apply (auto simp add: NSLIMSEQ_def starfunNat_mult [symmetric] starfunNat_real_of_nat)
 apply (rule_tac f1 = sin in starfun_stafunNat_o2 [THEN subst])
-apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse_zero)
+apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse)
 apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
 apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi 
-            simp add: starfunNat_real_of_nat mult_commute divide_inverse_zero)
+            simp add: starfunNat_real_of_nat mult_commute divide_inverse)
 done
 
 lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1"
@@ -618,7 +618,7 @@
 apply (rule_tac f1 = cos in starfun_stafunNat_o2 [THEN subst])
 apply (rule STAR_cos_Infinitesimal)
 apply (auto intro!: Infinitesimal_HFinite_mult2 
-            simp add: starfunNat_mult [symmetric] divide_inverse_zero
+            simp add: starfunNat_mult [symmetric] divide_inverse
                       starfunNat_inverse [symmetric] starfunNat_real_of_nat)
 done
 
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -476,17 +476,14 @@
   show "(x + y) * z = x * z + y * z" by (simp add: hypreal_add_mult_distrib)
   show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
   show "x \<noteq> 0 ==> inverse x * x = 1" by (simp add: hypreal_mult_inverse_left)
-  show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
+  show "x / y = x * inverse y" by (simp add: hypreal_divide_def)
 qed
 
 
 instance hypreal :: division_by_zero
 proof
-  fix x :: hypreal
-  show inv: "inverse 0 = (0::hypreal)" 
+  show "inverse 0 = (0::hypreal)" 
     by (simp add: hypreal_inverse hypreal_zero_def)
-  show "x/0 = 0" 
-    by (simp add: hypreal_divide_def inv hypreal_mult_commute [of a])
 qed
 
 
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Hyperreal/Log.thy
--- a/src/HOL/Hyperreal/Log.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/Log.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -41,7 +41,7 @@
 
 lemma powr_divide:
      "[| 0 < x; 0 < y |] ==> (x / y) powr a = (x powr a)/(y powr a)"
-apply (simp add: divide_inverse_zero positive_imp_inverse_positive powr_mult)
+apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
 apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
 done
 
@@ -58,7 +58,7 @@
 by (simp add: powr_def exp_minus [symmetric])
 
 lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
-by (simp add: divide_inverse_zero powr_minus)
+by (simp add: divide_inverse powr_minus)
 
 lemma powr_less_mono: "[| a < b; 1 < x |] ==> x powr a < x powr b"
 by (simp add: powr_def)
@@ -85,12 +85,12 @@
 lemma log_mult: 
      "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]  
       ==> log a (x * y) = log a x + log a y"
-by (simp add: log_def ln_mult divide_inverse_zero left_distrib)
+by (simp add: log_def ln_mult divide_inverse left_distrib)
 
 lemma log_eq_div_ln_mult_log: 
      "[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
       ==> log a x = (ln b/ln a) * log b x"
-by (simp add: log_def divide_inverse_zero)
+by (simp add: log_def divide_inverse)
 
 text{*Base 10 logarithms*}
 lemma log_base_10_eq1: "0 < x ==> log 10 x = (ln (exp 1) / ln 10) * ln x"
@@ -113,7 +113,7 @@
 
 lemma log_divide:
      "[|0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> log a (x/y) = log a x - log a y"
-by (simp add: log_mult divide_inverse_zero log_inverse)
+by (simp add: log_mult divide_inverse log_inverse)
 
 lemma log_less_cancel_iff [simp]:
      "[| 1 < a; 0 < x; 0 < y |] ==> (log a x < log a y) = (x < y)"
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Hyperreal/MacLaurin.ML
--- a/src/HOL/Hyperreal/MacLaurin.ML	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.ML	Thu Mar 04 12:06:07 2004 +0100
@@ -535,9 +535,9 @@
 by (res_inst_tac [("x","t")] exI 1);
 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
 by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
-    even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+(*Could sin_zero_iff help?*)
 qed "Maclaurin_sin_expansion";
 
 Goal "EX t. abs t <= abs x &  \
@@ -566,9 +566,8 @@
 by (arith_tac 1);
 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
 by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
-    even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
 qed "Maclaurin_sin_expansion2";
 
 Goal "[| 0 < n; 0 < x |] ==> \
@@ -590,9 +589,8 @@
 by (assume_tac 1 THEN assume_tac 1);
 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
 by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
-    even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
 qed "Maclaurin_sin_expansion3";
 
 Goal "0 < x ==> \
@@ -614,9 +612,8 @@
 by (assume_tac 1 THEN assume_tac 1);
 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
 by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
-    even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
 qed "Maclaurin_sin_expansion4";
 
 (*-----------------------------------------------------------------------------*)
@@ -658,9 +655,8 @@
 by (arith_tac 1);
 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
 by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
-    even_mult_two_ex,left_distrib,cos_add]  delsimps 
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add]  delsimps 
     [fact_Suc,realpow_Suc]));
 by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
 qed "Maclaurin_cos_expansion";
@@ -685,10 +681,8 @@
 by (assume_tac 1 THEN assume_tac 1);
 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
 by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
-    even_mult_two_ex,left_distrib,cos_add]  delsimps 
-    [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add]  delsimps [fact_Suc,realpow_Suc]));
 by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
 qed "Maclaurin_cos_expansion2";
 
@@ -712,10 +706,8 @@
 by (assume_tac 1 THEN assume_tac 1);
 by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
 by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
-    even_mult_two_ex,left_distrib,cos_add]  delsimps 
-    [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add]  delsimps [fact_Suc,realpow_Suc]));
 by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
 qed "Maclaurin_minus_cos_expansion";
 
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/NSA.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -914,7 +914,7 @@
 
 lemma Infinitesimal_SReal_divide: 
   "[| x \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal"
-apply (simp add: divide_inverse_zero)
+apply (simp add: divide_inverse)
 apply (auto intro!: Infinitesimal_HFinite_mult 
             dest!: SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
 done
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Hyperreal/Transcendental.ML
--- a/src/HOL/Hyperreal/Transcendental.ML	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML	Thu Mar 04 12:06:07 2004 +0100
@@ -830,7 +830,6 @@
 by Auto_tac;
 qed "sin_fdiffs2";
 
-(* thms in EvenOdd needed *)
 Goalw [diffs_def,real_divide_def]
       "diffs(%n. if even n then \
 \                (- 1) ^ (n div 2)/(real (fact n)) else 0) \
@@ -841,11 +840,11 @@
 by (stac real_of_nat_mult 1);
 by (stac even_Suc 1);
 by (stac inverse_mult_distrib 1);
-by (res_inst_tac [("z1","real (Suc n)")] (real_mult_commute RS ssubst) 1);
-by (res_inst_tac [("z1","inverse(real (Suc n))")] 
-     (real_mult_commute RS ssubst) 1);
+by (res_inst_tac [("a1","real (Suc n)")] (mult_commute RS ssubst) 1);
+by (res_inst_tac [("a1","inverse(real (Suc n))")] 
+     (mult_commute RS ssubst) 1);
 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
-    odd_not_even RS sym,odd_Suc_mult_two_ex]));
+    odd_Suc_mult_two_ex]));
 qed "cos_fdiffs";
 
 
@@ -862,7 +861,7 @@
 by (res_inst_tac [("z1","inverse (real (Suc n))")] 
      (real_mult_commute RS ssubst) 1);
 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
-    odd_not_even RS sym,odd_Suc_mult_two_ex]));
+    odd_Suc_mult_two_ex]));
 qed "cos_fdiffs2";
 
 (* ------------------------------------------------------------------------ *)
@@ -1949,7 +1948,7 @@
 (* Pre Isabelle99-2 proof was simpler- numerals arithmetic 
    now causes some unwanted re-arrangements of literals!   *)
 Goal "[| 0 <= x; cos x = 0 |] ==> \
-\     EX n. ~even n & x = real n * (pi/2)";
+\     EX n::nat. ~even n & x = real n * (pi/2)";
 by (dtac (pi_gt_zero RS reals_Archimedean4) 1);
 by (Step_tac 1);
 by (subgoal_tac 
@@ -1973,7 +1972,7 @@
 qed "cos_zero_lemma";
 
 Goal "[| 0 <= x; sin x = 0 |] ==> \
-\     EX n. even n & x = real n * (pi/2)";
+\     EX n::nat. even n & x = real n * (pi/2)";
 by (subgoal_tac 
     "EX n. ~ even n & x + pi/2  = real n * (pi/2)" 1);
 by (rtac cos_zero_lemma 2);
@@ -1981,15 +1980,15 @@
 by (res_inst_tac [("x","n - 1")] exI 1);
 by (rtac (CLAIM "-y <= x ==> -x <= (y::real)") 2);
 by (rtac real_le_trans 2 THEN assume_tac 3);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym,
+by (auto_tac (claset(),simpset() addsimps [
     odd_Suc_mult_two_ex,real_of_nat_Suc,
     left_distrib,real_mult_assoc RS sym]));
 qed "sin_zero_lemma";
 
 (* also spoilt by numeral arithmetic *)
 Goal "(cos x = 0) = \
-\     ((EX n. ~even n & (x = real n * (pi/2))) |   \
-\      (EX n. ~even n & (x = -(real n * (pi/2)))))";
+\     ((EX n::nat. ~even n & (x = real n * (pi/2))) |   \
+\      (EX n::nat. ~even n & (x = -(real n * (pi/2)))))";
 by (rtac iffI 1);
 by (cut_inst_tac [("x","x")] (CLAIM "0 <= (x::real) | x <= 0") 1);
 by (Step_tac 1);
@@ -1998,15 +1997,15 @@
 by (dtac cos_zero_lemma 3);
 by (Step_tac 1);
 by (dtac (CLAIM "-x = y ==> x = -(y::real)") 2);
-by (auto_tac (claset(),HOL_ss addsimps [odd_not_even RS sym,
+by (auto_tac (claset(),HOL_ss addsimps [
     odd_Suc_mult_two_ex,real_of_nat_Suc,left_distrib]));
 by (auto_tac (claset(),simpset() addsimps [cos_add]));
 qed "cos_zero_iff";
 
 (* ditto: but to a lesser extent *)
 Goal "(sin x = 0) = \
-\     ((EX n. even n & (x = real n * (pi/2))) |   \
-\      (EX n. even n & (x = -(real n * (pi/2)))))";
+\     ((EX n::nat. even n & (x = real n * (pi/2))) |   \
+\      (EX n::nat. even n & (x = -(real n * (pi/2)))))";
 by (rtac iffI 1);
 by (cut_inst_tac [("x","x")] (CLAIM "0 <= (x::real) | x <= 0") 1);
 by (Step_tac 1);
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Integ/IntDef.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -369,9 +369,6 @@
 apply (simp add: zle linorder_linear) 
 done
 
-instance int :: plus_ac0
-proof qed (rule zadd_commute zadd_assoc zadd_0)+
-
 instance int :: linorder
 proof qed (rule zle_linear)
 
@@ -909,6 +906,63 @@
 declare le_iff_diff_le_0 [symmetric, simp]
 
 
+subsection{*More Properties of @{term setsum} and  @{term setprod}*}
+
+text{*By Jeremy Avigad*}
+
+
+lemma setsum_of_nat: "of_nat (setsum f A) = setsum (of_nat \<circ> f) A"
+  apply (case_tac "finite A")
+  apply (erule finite_induct, auto)
+  apply (simp add: setsum_def)
+  done
+
+lemma setsum_of_int: "of_int (setsum f A) = setsum (of_int \<circ> f) A"
+  apply (case_tac "finite A")
+  apply (erule finite_induct, auto)
+  apply (simp add: setsum_def)
+  done
+
+lemma int_setsum: "int (setsum f A) = setsum (int \<circ> f) A"
+  by (subst int_eq_of_nat, rule setsum_of_nat)
+
+lemma setprod_of_nat: "of_nat (setprod f A) = setprod (of_nat \<circ> f) A"
+  apply (case_tac "finite A")
+  apply (erule finite_induct, auto)
+  apply (simp add: setprod_def)
+  done
+
+lemma setprod_of_int: "of_int (setprod f A) = setprod (of_int \<circ> f) A"
+  apply (case_tac "finite A")
+  apply (erule finite_induct, auto)
+  apply (simp add: setprod_def)
+  done
+
+lemma int_setprod: "int (setprod f A) = setprod (int \<circ> f) A"
+  by (subst int_eq_of_nat, rule setprod_of_nat)
+
+lemma setsum_constant: "finite A ==> (\<Sum>x \<in> A. y) = of_nat(card A) * y"
+  apply (erule finite_induct)
+  apply (auto simp add: ring_distrib add_ac)
+  done
+
+lemma setprod_nonzero_nat:
+    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
+  by (rule setprod_nonzero, auto)
+
+lemma setprod_zero_eq_nat:
+    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
+  by (rule setprod_zero_eq, auto)
+
+lemma setprod_nonzero_int:
+    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
+  by (rule setprod_nonzero, auto)
+
+lemma setprod_zero_eq_int:
+    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
+  by (rule setprod_zero_eq, auto)
+
+
 (*Legacy ML bindings, but no longer the structure Int.*)
 ML
 {*
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Integ/NatBin.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -648,6 +648,12 @@
           else number_of (bin_add v v') + k)"
 by simp
 
+lemma nat_number_of_mult_left:
+     "number_of v * (number_of v' * (k::nat)) =  
+         (if neg (number_of v :: int) then 0
+          else number_of (bin_mult v v') * k)"
+by simp
+
 
 subsubsection{*For @{text combine_numerals}*}
 
@@ -776,6 +782,7 @@
 val nat_number = thms"nat_number";
 
 val nat_number_of_add_left = thm"nat_number_of_add_left";
+val nat_number_of_mult_left = thm"nat_number_of_mult_left";
 val left_add_mult_distrib = thm"left_add_mult_distrib";
 val nat_diff_add_eq1 = thm"nat_diff_add_eq1";
 val nat_diff_add_eq2 = thm"nat_diff_add_eq2";
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Integ/NatSimprocs.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -204,7 +204,7 @@
 
 lemma minus1_divide [simp]:
      "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
-by (simp add: divide_inverse_zero inverse_minus_eq)
+by (simp add: divide_inverse inverse_minus_eq)
 
 ML
 {*
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Integ/Parity.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Parity.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -0,0 +1,279 @@
+(*  Title:      Parity.thy
+    Author:     Jeremy Avigad
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+    Last modified 2 March 2004
+*)
+
+header {* Parity: Even and Odd for ints and nats*}
+
+theory Parity = Divides + IntDiv + NatSimprocs:
+
+axclass even_odd < type
+
+instance int :: even_odd ..
+instance nat :: even_odd ..
+
+consts
+  even :: "'a::even_odd => bool"
+
+syntax 
+  odd :: "'a::even_odd => bool"
+
+translations 
+  "odd x" == "~even x" 
+
+defs (overloaded)
+  even_def: "even (x::int) == x mod 2 = 0"
+  even_nat_def: "even (x::nat) == even (int x)"
+
+
+subsection {* Casting a nat power to an integer *}
+
+lemma zpow_int: "int (x^y) = (int x)^y"
+  apply (induct_tac y)
+  apply (simp, simp add: zmult_int [THEN sym])
+  done
+
+subsection {* Even and odd are mutually exclusive *}
+
+lemma int_pos_lt_two_imp_zero_or_one: 
+    "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1"
+  by auto
+
+lemma neq_one_mod_two [simp]: "((x::int) mod 2 ~= 0) = (x mod 2 = 1)"
+  apply (subgoal_tac "x mod 2 = 0 | x mod 2 = 1", force)
+  apply (rule int_pos_lt_two_imp_zero_or_one, auto)
+  done
+
+subsection {* Behavior under integer arithmetic operations *}
+
+lemma even_times_anything: "even (x::int) ==> even (x * y)"
+  by (simp add: even_def zmod_zmult1_eq')
+
+lemma anything_times_even: "even (y::int) ==> even (x * y)"
+  by (simp add: even_def zmod_zmult1_eq)
+
+lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)"
+  by (simp add: even_def zmod_zmult1_eq)
+
+lemma even_product: "even((x::int) * y) = (even x | even y)"
+  apply (auto simp add: even_times_anything anything_times_even) 
+  apply (rule ccontr)
+  apply (auto simp add: odd_times_odd)
+  done
+
+lemma even_plus_even: "even (x::int) ==> even y ==> even (x + y)"
+  by (simp add: even_def zmod_zadd1_eq)
+
+lemma even_plus_odd: "even (x::int) ==> odd y ==> odd (x + y)"
+  by (simp add: even_def zmod_zadd1_eq)
+
+lemma odd_plus_even: "odd (x::int) ==> even y ==> odd (x + y)"
+  by (simp add: even_def zmod_zadd1_eq)
+
+lemma odd_plus_odd: "odd (x::int) ==> odd y ==> even (x + y)"
+  by (simp add: even_def zmod_zadd1_eq)
+
+lemma even_sum: "even ((x::int) + y) = ((even x & even y) | (odd x & odd y))"
+  apply (auto intro: even_plus_even odd_plus_odd)
+  apply (rule ccontr, simp add: even_plus_odd)
+  apply (rule ccontr, simp add: odd_plus_even)
+  done
+
+lemma even_neg: "even (-(x::int)) = even x"
+  by (auto simp add: even_def zmod_zminus1_eq_if)
+
+lemma even_difference: 
+  "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))"
+  by (simp only: diff_minus even_sum even_neg)
+
+lemma even_pow_gt_zero [rule_format]: 
+    "even (x::int) ==> 0 < n --> even (x^n)"
+  apply (induct_tac n)
+  apply (auto simp add: even_product)
+  done
+
+lemma odd_pow: "odd x ==> odd((x::int)^n)"
+  apply (induct_tac n)
+  apply (simp add: even_def)
+  apply (simp add: even_product)
+  done
+
+lemma even_power: "even ((x::int)^n) = (even x & 0 < n)"
+  apply (auto simp add: even_pow_gt_zero) 
+  apply (erule contrapos_pp, erule odd_pow)
+  apply (erule contrapos_pp, simp add: even_def)
+  done
+
+lemma even_zero: "even (0::int)"
+  by (simp add: even_def)
+
+lemma odd_one: "odd (1::int)"
+  by (simp add: even_def)
+
+lemmas even_odd_simps [simp] = even_def[of "number_of v",standard] even_zero 
+  odd_one even_product even_sum even_neg even_difference even_power
+
+
+subsection {* Equivalent definitions *}
+
+lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x" 
+  by (auto simp add: even_def)
+
+lemma two_times_odd_div_two_plus_one: "odd (x::int) ==> 
+    2 * (x div 2) + 1 = x"
+  apply (insert zmod_zdiv_equality [of x 2, THEN sym])
+  by (simp add: even_def)
+
+lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)"
+  apply auto
+  apply (rule exI)
+  by (erule two_times_even_div_two [THEN sym])
+
+lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)"
+  apply auto
+  apply (rule exI)
+  by (erule two_times_odd_div_two_plus_one [THEN sym])
+
+
+subsection {* even and odd for nats *}
+
+lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)"
+  by (simp add: even_nat_def)
+
+lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
+  by (simp add: even_nat_def zmult_int [THEN sym])
+
+lemma even_nat_sum: "even ((x::nat) + y) = 
+    ((even x & even y) | (odd x & odd y))"
+  by (unfold even_nat_def, simp)
+
+lemma even_nat_difference: 
+    "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
+  apply (auto simp add: even_nat_def zdiff_int [THEN sym])
+  apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym])
+  apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym])
+  done
+
+lemma even_nat_suc: "even (Suc x) = odd x"
+  by (simp add: even_nat_def)
+
+lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
+  by (simp add: even_nat_def zpow_int)
+
+lemma even_nat_zero: "even (0::nat)"
+  by (simp add: even_nat_def)
+
+lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] 
+  even_nat_zero even_nat_suc even_nat_product even_nat_sum even_nat_power
+
+
+subsection {* Equivalent definitions *}
+
+lemma nat_lt_two_imp_zero_or_one: "(x::nat) < Suc (Suc 0) ==> 
+    x = 0 | x = Suc 0"
+  by auto
+
+lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0"
+  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
+  apply (drule subst, assumption)
+  apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0")
+  apply force
+  apply (subgoal_tac "0 < Suc (Suc 0)")
+  apply (frule mod_less_divisor [of "Suc (Suc 0)" x])
+  apply (erule nat_lt_two_imp_zero_or_one, auto)
+  done
+
+lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0"
+  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
+  apply (drule subst, assumption)
+  apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0")
+  apply force 
+  apply (subgoal_tac "0 < Suc (Suc 0)")
+  apply (frule mod_less_divisor [of "Suc (Suc 0)" x])
+  apply (erule nat_lt_two_imp_zero_or_one, auto)
+  done
+
+lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" 
+  apply (rule iffI)
+  apply (erule even_nat_mod_two_eq_zero)
+  apply (insert odd_nat_mod_two_eq_one [of x], auto)
+  done
+
+lemma odd_nat_equiv_def: "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)"
+  apply (auto simp add: even_nat_equiv_def)
+  apply (subgoal_tac "x mod (Suc (Suc 0)) < Suc (Suc 0)")
+  apply (frule nat_lt_two_imp_zero_or_one, auto)
+  done
+
+lemma even_nat_div_two_times_two: "even (x::nat) ==> 
+    Suc (Suc 0) * (x div Suc (Suc 0)) = x"
+  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
+  apply (drule even_nat_mod_two_eq_zero, simp)
+  done
+
+lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> 
+    Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x"  
+  apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
+  apply (drule odd_nat_mod_two_eq_one, simp)
+  done
+
+lemma even_nat_equiv_def2: "even (x::nat) = (EX y. x = Suc (Suc 0) * y)"
+  apply (rule iffI, rule exI)
+  apply (erule even_nat_div_two_times_two [THEN sym], auto)
+  done
+
+lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))"
+  apply (rule iffI, rule exI)
+  apply (erule odd_nat_div_two_times_two_plus_one [THEN sym], auto)
+  done
+
+subsection {* Powers of negative one *}
+
+lemma neg_one_even_odd_power:
+     "(even x --> (-1::'a::{number_ring,ringpower})^x = 1) & 
+      (odd x --> (-1::'a)^x = -1)"
+  apply (induct_tac x)
+  apply (simp, simp add: power_Suc)
+  done
+
+lemma neg_one_even_power: "even x ==> (-1::'a::{number_ring,ringpower})^x = 1"
+  by (rule neg_one_even_odd_power [THEN conjunct1, THEN mp], assumption)
+
+lemma neg_one_odd_power: "odd x ==> (-1::'a::{number_ring,ringpower})^x = -1"
+  by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption)
+
+
+subsection {* Miscellaneous *}
+
+lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2"
+  apply (subst zdiv_zadd1_eq)
+  apply (simp add: even_def)
+  done
+
+lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1"
+  apply (subst zdiv_zadd1_eq)
+  apply (simp add: even_def)
+  done
+
+lemma div_Suc: "Suc a div c = a div c + Suc 0 div c + 
+    (a mod c + Suc 0 mod c) div c"
+  apply (subgoal_tac "Suc a = a + Suc 0")
+  apply (erule ssubst)
+  apply (rule div_add1_eq, simp)
+  done
+
+lemma even_nat_plus_one_div_two: "even (x::nat) ==> 
+   (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
+  apply (subst div_Suc)
+  apply (simp add: even_nat_equiv_def)
+  done
+
+lemma odd_nat_plus_one_div_two: "odd (x::nat) ==> 
+    (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))"
+  apply (subst div_Suc)
+  apply (simp add: odd_nat_equiv_def)
+  done
+
+end
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Thu Mar 04 12:06:07 2004 +0100
@@ -6,6 +6,10 @@
 Simprocs for nat numerals.
 *)
 
+val Let_number_of = thm"Let_number_of";
+val Let_0 = thm"Let_0";
+val Let_1 = thm"Let_1";
+
 structure Nat_Numeral_Simprocs =
 struct
 
@@ -65,12 +69,14 @@
 
 val trans_tac = Int_Numeral_Simprocs.trans_tac;
 
-val bin_simps = [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym,
-                 add_nat_number_of, nat_number_of_add_left,
-                 diff_nat_number_of, le_number_of_eq_not_less,
-                 less_nat_number_of, mult_nat_number_of,
-                 thm "Let_number_of", nat_number_of] @
-                bin_arith_simps @ bin_rel_simps;
+val bin_simps =
+     [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym,
+      add_nat_number_of, nat_number_of_add_left, 
+      diff_nat_number_of, le_number_of_eq_not_less,
+      mult_nat_number_of, nat_number_of_mult_left, 
+      less_nat_number_of, 
+      Let_number_of, nat_number_of] @
+     bin_arith_simps @ bin_rel_simps;
 
 fun prep_simproc (name, pats, proc) =
   Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
@@ -268,7 +274,8 @@
   val trans_tac         = trans_tac
   val norm_tac = ALLGOALS
                     (simp_tac (HOL_ss addsimps [Suc_eq_add_numeral_1]@mult_1s))
-                 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_ac))
+                 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
+                 THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
   val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
   val simplify_meta_eq  = simplify_meta_eq
   end
@@ -504,7 +511,7 @@
 
 (* reduce contradictory <= to False *)
 val add_rules =
-  [thm "Let_number_of", thm "Let_0", thm "Let_1", nat_0, nat_1,
+  [thm "Let_number_of", Let_0, Let_1, nat_0, nat_1,
    add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
    eq_nat_number_of, less_nat_number_of, le_number_of_eq_not_less,
    le_Suc_number_of,le_number_of_Suc,
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/IsaMakefile	Thu Mar 04 12:06:07 2004 +0100
@@ -87,9 +87,8 @@
   HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.thy \
   Integ/cooper_dec.ML Integ/cooper_proof.ML \
   Integ/Equiv.thy Integ/IntArith.thy Integ/IntDef.thy \
-  Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy \
-  Integ/int_arith1.ML \
-  Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
+  Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \
+  Integ/int_arith1.ML Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
   Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
   Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
   Nat.thy NatArith.ML NatArith.thy Numeral.thy \
@@ -143,7 +142,7 @@
   Real/Rational.thy Real/PReal.thy Real/RComplete.thy \
   Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy \
   Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
-  Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
+  Hyperreal/EvenOdd.thy\
   Hyperreal/Fact.ML Hyperreal/Fact.thy Hyperreal/HLog.thy\
   Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HSeries.thy\
   Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/NumberTheory/Finite2.thy
--- a/src/HOL/NumberTheory/Finite2.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/NumberTheory/Finite2.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -253,12 +253,7 @@
 lemma cartesian_product_card [simp]: "[| finite A; finite B |] ==> 
   card (A <*> B) = card(A) * card(B)";
   apply (rule_tac F = A in finite_induct, auto)
-  apply (case_tac "F = {}", force)
-  apply (subgoal_tac "card({x} <*> B \<union> F <*> B) = card({x} <*> B) + 
-    card(F <*> B)");
-  apply simp
-  apply (rule card_Un_disjoint)
-  by auto
+  done
 
 (******************************************************************)
 (*                                                                *)
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/PreList.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -9,7 +9,8 @@
 (*Is defined separately to serve as a basis for theory ToyList in the
 documentation.*)
 
-theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power:
+theory PreList =
+    Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
 
 (*belongs to theory Wellfounded_Recursion*)
 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Real/PReal.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -296,13 +296,13 @@
     show "\<exists>y' \<in> B. z = x*?f + y'"
     proof
       show "z = x*?f + y*?f"
-	by (simp add: left_distrib [symmetric] divide_inverse_zero mult_ac
+	by (simp add: left_distrib [symmetric] divide_inverse mult_ac
 		      order_less_imp_not_eq2)
     next
       show "y * ?f \<in> B"
       proof (rule preal_downwards_closed [OF B y])
         show "0 < y * ?f"
-          by (simp add: divide_inverse_zero zero_less_mult_iff)
+          by (simp add: divide_inverse zero_less_mult_iff)
       next
         show "y * ?f < y"
           by (insert mult_strict_left_mono [OF fless ypos], simp)
@@ -312,7 +312,7 @@
     show "x * ?f \<in> A"
     proof (rule preal_downwards_closed [OF A x])
       show "0 < x * ?f"
-	by (simp add: divide_inverse_zero zero_less_mult_iff)
+	by (simp add: divide_inverse zero_less_mult_iff)
     next
       show "x * ?f < x"
 	by (insert mult_strict_left_mono [OF fless xpos], simp)
@@ -435,7 +435,7 @@
     show "\<exists>y'\<in>B. z = (z/y) * y'"
     proof
       show "z = (z/y)*y"
-	by (simp add: divide_inverse_zero mult_commute [of y] mult_assoc
+	by (simp add: divide_inverse mult_commute [of y] mult_assoc
 		      order_less_imp_not_eq2)
       show "y \<in> B" .
     qed
@@ -522,7 +522,7 @@
         show "\<exists>v'\<in>A. x = (x / v) * v'"
         proof
           show "x = (x/v)*v"
-	    by (simp add: divide_inverse_zero mult_assoc vpos
+	    by (simp add: divide_inverse mult_assoc vpos
                           order_less_imp_not_eq2)
           show "v \<in> A" .
         qed
@@ -579,7 +579,7 @@
   have cpos: "0 < ?c"
     by (simp add: zero_less_divide_iff zero_less_mult_iff pos_add_strict)
   show "a * d + b * e = ?c * (d + e)"
-    by (simp add: divide_inverse_zero mult_assoc order_less_imp_not_eq2)
+    by (simp add: divide_inverse mult_assoc order_less_imp_not_eq2)
   show "?c \<in> Rep_preal w"
     proof (cases rule: linorder_le_cases)
       assume "a \<le> b"
@@ -808,7 +808,7 @@
     proof -
       have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
       also with ypos have "... = (r/y) * (y + ?d)"
-	by (simp only: right_distrib divide_inverse_zero mult_ac, simp)
+	by (simp only: right_distrib divide_inverse mult_ac, simp)
       also have "... = r*x" using ypos
 	by simp
       finally show "r + ?d < r*x" .
@@ -849,12 +849,12 @@
     show "0 < x/u" using xpos upos
       by (simp add: zero_less_divide_iff)  
     show "x/u < x/r" using xpos upos rpos
-      by (simp add: divide_inverse_zero mult_less_cancel_left rless) 
+      by (simp add: divide_inverse mult_less_cancel_left rless) 
     show "inverse (x / r) \<notin> Rep_preal R" using notin
-      by (simp add: divide_inverse_zero mult_commute) 
+      by (simp add: divide_inverse mult_commute) 
     show "u \<in> Rep_preal R" by (rule u) 
     show "x = x / u * u" using upos 
-      by (simp add: divide_inverse_zero mult_commute) 
+      by (simp add: divide_inverse mult_commute) 
   qed
 qed
 
@@ -875,7 +875,7 @@
   have "q < inverse y" using rpos rless
     by (simp add: not_in_preal_ub [OF Rep_preal notin] q)
   hence "r * q < r/y" using rpos
-    by (simp add: divide_inverse_zero mult_less_cancel_left)
+    by (simp add: divide_inverse mult_less_cancel_left)
   also have "... \<le> 1" using rpos rless
     by (simp add: pos_divide_le_eq)
   finally show ?thesis .
@@ -1272,7 +1272,7 @@
   have "x * z * inverse y * inverse z = x * inverse y * (z * inverse z)"
     by (simp add: mult_ac)
   also have "... = x/y" using zpos
-    by (simp add: divide_inverse_zero)
+    by (simp add: divide_inverse)
   also have "... < z"
     by (simp add: pos_divide_less_eq [OF ypos] mult_commute) 
   finally show ?thesis .
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Real/Rational.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -511,9 +511,8 @@
        (simp add: add_rat mult_rat eq_rat int_distrib)
   show "q \<noteq> 0 ==> inverse q * q = 1"
     by (induct q) (simp add: inverse_rat mult_rat one_rat zero_rat eq_rat)
-  show "r \<noteq> 0 ==> q / r = q * inverse r"
-    by (induct q, induct r)
-       (simp add: mult_rat divide_rat inverse_rat zero_rat eq_rat)
+  show "q / r = q * inverse r"
+    by (simp add: divide_rat_def) 
   show "0 \<noteq> (1::rat)"
     by (simp add: zero_rat one_rat eq_rat) 
 qed
@@ -632,9 +631,7 @@
 
 instance rat :: division_by_zero
 proof
-  fix x :: rat
   show "inverse 0 = (0::rat)"  by (simp add: inverse_rat_def)
-  show "x/0 = 0"   by (simp add: divide_rat_def inverse_rat_def)
 qed
 
 
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Real/RealDef.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -351,7 +351,7 @@
   show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib)
   show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
   show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
-  show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
+  show "x / y = x * inverse y" by (simp add: real_divide_def)
 qed
 
 
@@ -365,9 +365,7 @@
 
 instance real :: division_by_zero
 proof
-  fix x :: real
   show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
-  show "x/0 = 0" by (simp add: real_divide_def INVERSE_ZERO)
 qed
 
 
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -59,13 +59,12 @@
 
 axclass field \<subseteq> ring, inverse
   left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
-  divide_inverse:      "b \<noteq> 0 ==> a / b = a * inverse b"
+  divide_inverse:      "a / b = a * inverse b"
 
 axclass ordered_field \<subseteq> ordered_ring, field
 
 axclass division_by_zero \<subseteq> zero, inverse
   inverse_zero [simp]: "inverse 0 = 0"
-  divide_zero [simp]: "a / 0 = 0"
 
 
 subsection {* Derived Rules for Addition *}
@@ -595,7 +594,7 @@
 instance ordered_ring \<subseteq> ordered_semiring
 proof
   have "(0::'a) \<le> 1*1" by (rule zero_le_square)
-  thus "(0::'a) < 1" by (simp add: order_le_less ) 
+  thus "(0::'a) < 1" by (simp add: order_le_less) 
 qed
 
 text{*All three types of comparision involving 0 and 1 are covered.*}
@@ -650,7 +649,7 @@
 
 lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semiring)"
 apply (insert mult_strict_mono [of 1 m 1 n]) 
-apply (simp add:  order_less_trans [OF zero_less_one]); 
+apply (simp add:  order_less_trans [OF zero_less_one]) 
 done
 
 
@@ -743,24 +742,18 @@
 lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
   by (simp add: divide_inverse)
 
-lemma divide_inverse_zero: "a/b = a * inverse(b::'a::{field,division_by_zero})"
-apply (case_tac "b = 0")
-apply (simp_all add: divide_inverse)
-done
+lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})"
+by (simp add: divide_inverse)
 
-lemma divide_zero_left [simp]: "0/a = (0::'a::{field,division_by_zero})"
-by (simp add: divide_inverse_zero)
+lemma divide_zero_left [simp]: "0/a = (0::'a::field)"
+by (simp add: divide_inverse)
 
-lemma inverse_eq_divide: "inverse (a::'a::{field,division_by_zero}) = 1/a"
-by (simp add: divide_inverse_zero)
+lemma inverse_eq_divide: "inverse (a::'a::field) = 1/a"
+by (simp add: divide_inverse)
 
-lemma nonzero_add_divide_distrib: "c \<noteq> 0 ==> (a+b)/(c::'a::field) = a/c + b/c"
+lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c"
 by (simp add: divide_inverse left_distrib) 
 
-lemma add_divide_distrib: "(a+b)/(c::'a::{field,division_by_zero}) = a/c + b/c"
-apply (case_tac "c=0", simp) 
-apply (simp add: nonzero_add_divide_distrib) 
-done
 
 text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
       of an ordering.*}
@@ -935,7 +928,7 @@
 
 lemma inverse_divide [simp]:
       "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
-  by (simp add: divide_inverse_zero mult_commute)
+  by (simp add: divide_inverse mult_commute)
 
 lemma nonzero_mult_divide_cancel_left:
   assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" 
@@ -975,23 +968,21 @@
   by (simp add: mult_divide_cancel_left)
 
 lemma divide_1 [simp]: "a/1 = (a::'a::field)"
-  by (simp add: divide_inverse [OF not_sym])
+  by (simp add: divide_inverse)
 
-lemma times_divide_eq_right [simp]:
-     "a * (b/c) = (a*b) / (c::'a::{field,division_by_zero})"
-by (simp add: divide_inverse_zero mult_assoc)
+lemma times_divide_eq_right [simp]: "a * (b/c) = (a*b) / (c::'a::field)"
+by (simp add: divide_inverse mult_assoc)
 
-lemma times_divide_eq_left [simp]:
-     "(b/c) * a = (b*a) / (c::'a::{field,division_by_zero})"
-by (simp add: divide_inverse_zero mult_ac)
+lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
+by (simp add: divide_inverse mult_ac)
 
 lemma divide_divide_eq_right [simp]:
      "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
-by (simp add: divide_inverse_zero mult_ac)
+by (simp add: divide_inverse mult_ac)
 
 lemma divide_divide_eq_left [simp]:
      "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
-by (simp add: divide_inverse_zero mult_assoc)
+by (simp add: divide_inverse mult_assoc)
 
 
 subsection {* Division and Unary Minus *}
@@ -1005,14 +996,12 @@
 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
 by (simp add: divide_inverse nonzero_inverse_minus_eq)
 
-lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::{field,division_by_zero})"
-apply (case_tac "b=0", simp) 
-apply (simp add: nonzero_minus_divide_left) 
-done
+lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
+by (simp add: divide_inverse minus_mult_left [symmetric])
 
 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
-apply (case_tac "b=0", simp) 
-by (rule nonzero_minus_divide_right) 
+by (simp add: divide_inverse minus_mult_right [symmetric])
+
 
 text{*The effect is to extract signs from divisions*}
 declare minus_divide_left  [symmetric, simp]
@@ -1028,8 +1017,7 @@
 apply (simp add: nonzero_minus_divide_divide) 
 done
 
-lemma diff_divide_distrib:
-     "(a-b)/(c::'a::{field,division_by_zero}) = a/c - b/c"
+lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
 by (simp add: diff_minus add_divide_distrib) 
 
 
@@ -1236,26 +1224,26 @@
 
 lemma zero_less_divide_iff:
      "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
-by (simp add: divide_inverse_zero zero_less_mult_iff)
+by (simp add: divide_inverse zero_less_mult_iff)
 
 lemma divide_less_0_iff:
      "(a/b < (0::'a::{ordered_field,division_by_zero})) = 
       (0 < a & b < 0 | a < 0 & 0 < b)"
-by (simp add: divide_inverse_zero mult_less_0_iff)
+by (simp add: divide_inverse mult_less_0_iff)
 
 lemma zero_le_divide_iff:
      "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
       (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
-by (simp add: divide_inverse_zero zero_le_mult_iff)
+by (simp add: divide_inverse zero_le_mult_iff)
 
 lemma divide_le_0_iff:
      "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
       (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
-by (simp add: divide_inverse_zero mult_le_0_iff)
+by (simp add: divide_inverse mult_le_0_iff)
 
 lemma divide_eq_0_iff [simp]:
      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
-by (simp add: divide_inverse_zero field_mult_eq_0_iff)
+by (simp add: divide_inverse field_mult_eq_0_iff)
 
 
 subsection{*Simplification of Inequalities Involving Literal Divisors*}
@@ -1415,13 +1403,13 @@
 lemma divide_cancel_right [simp]:
      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
 apply (case_tac "c=0", simp) 
-apply (simp add: divide_inverse_zero field_mult_cancel_right) 
+apply (simp add: divide_inverse field_mult_cancel_right) 
 done
 
 lemma divide_cancel_left [simp]:
      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
 apply (case_tac "c=0", simp) 
-apply (simp add: divide_inverse_zero field_mult_cancel_left) 
+apply (simp add: divide_inverse field_mult_cancel_left) 
 done
 
 subsection {* Division and the Number One *}
@@ -1669,6 +1657,9 @@
   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
 qed
 
+text{*Moving this up spoils many proofs using @{text mult_le_cancel_right}*}
+declare times_divide_eq_left [simp]
+
 ML
 {*
 val add_assoc = thm"add_assoc";
@@ -1809,11 +1800,9 @@
 val right_inverse_eq = thm"right_inverse_eq";
 val nonzero_inverse_eq_divide = thm"nonzero_inverse_eq_divide";
 val divide_self = thm"divide_self";
-val divide_inverse_zero = thm"divide_inverse_zero";
 val inverse_divide = thm"inverse_divide";
 val divide_zero_left = thm"divide_zero_left";
 val inverse_eq_divide = thm"inverse_eq_divide";
-val nonzero_add_divide_distrib = thm"nonzero_add_divide_distrib";
 val add_divide_distrib = thm"add_divide_distrib";
 val field_mult_eq_0_iff = thm"field_mult_eq_0_iff";
 val field_mult_cancel_right = thm"field_mult_cancel_right";
diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/simpdata.ML	Thu Mar 04 12:06:07 2004 +0100
@@ -246,7 +246,7 @@
        imp_disjL, conj_assoc, disj_assoc,
        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
        disj_not1, not_all, not_ex, cases_simp,
-       thm "the_eq_trivial", the_sym_eq_trivial, thm "plus_ac0.zero", thm "plus_ac0_zero_right"]
+       thm "the_eq_trivial", the_sym_eq_trivial]
      @ ex_simps @ all_simps @ simp_thms)
      addsimprocs [defALL_regroup,defEX_regroup]
      addcongs [imp_cong]