# HG changeset patch
# User nipkow
# Date 1193174843 -7200
# Node ID ad4d5365d9d871a130272101b21fec4fc91e4f5c
# Parent  aa847439803022b7743d0e025a2fe5aa6701a679
went back to >0

diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -100,7 +100,7 @@
 done
 
 (*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
-lemma power_dvd_bound: "[|p^n dvd a;  Suc 0 < p;  a \<noteq> 0|] ==> n < a"
+lemma power_dvd_bound: "[|p^n dvd a;  Suc 0 < p;  a > 0|] ==> n < a"
 apply (drule dvd_imp_le)
 apply (drule_tac [2] n = n in Suc_le_power, auto)
 done
@@ -115,7 +115,7 @@
 apply (blast dest: prime_imp_one_less power_dvd_bound)
 done
 
-lemma power_exponent_dvd: "s\<noteq>0 ==> (p ^ exponent p s) dvd s"
+lemma power_exponent_dvd: "s>0 ==> (p ^ exponent p s) dvd s"
 apply (simp add: exponent_def)
 apply clarify
 apply (rule_tac k = 0 in GreatestI)
@@ -145,7 +145,7 @@
 
 
 (* exponent_mult_add, easy inclusion.  Could weaken p \<in> prime to Suc 0 < p *)
-lemma exponent_mult_add1: "[| a \<noteq> 0; b \<noteq> 0 |]
+lemma exponent_mult_add1: "[| a > 0; b > 0 |]
   ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
 apply (case_tac "prime p")
 apply (rule exponent_ge)
@@ -154,7 +154,7 @@
 done
 
 (* exponent_mult_add, opposite inclusion *)
-lemma exponent_mult_add2: "[| a \<noteq> 0; b \<noteq> 0 |]  
+lemma exponent_mult_add2: "[| a > 0; b > 0 |]  
   ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
 apply (case_tac "prime p")
 apply (rule leI, clarify)
@@ -168,7 +168,7 @@
 apply (blast dest: power_Suc_exponent_Not_dvd)
 done
 
-lemma exponent_mult_add: "[| a \<noteq> 0; b \<noteq> 0 |]
+lemma exponent_mult_add: "[| a > 0; b > 0 |]
    ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
 by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym)
 
@@ -188,14 +188,14 @@
 
 subsection{*Main Combinatorial Argument*}
 
-lemma le_extend_mult: "[| c \<noteq> 0; a <= b |] ==> a <= b * (c::nat)"
+lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)"
 apply (rule_tac P = "%x. x <= b * c" in subst)
 apply (rule mult_1_right)
 apply (rule mult_le_mono, auto)
 done
 
 lemma p_fac_forw_lemma:
-  "[| (m::nat) \<noteq> 0; k \<noteq> 0; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
+  "[| (m::nat) > 0; k > 0; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
 apply (rule notnotD)
 apply (rule notI)
 apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
@@ -205,7 +205,7 @@
 apply(metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less neq0_conv)
 done
 
-lemma p_fac_forw: "[| (m::nat) \<noteq> 0; k\<noteq>0; k < p^a; (p^r) dvd (p^a)* m - k |]  
+lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]  
   ==> (p^r) dvd (p^a) - k"
 apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto)
 apply (subgoal_tac "p^r dvd p^a*m")
@@ -213,15 +213,15 @@
 apply (drule dvd_diffD1)
   apply assumption
  prefer 2 apply (blast intro: dvd_diff)
-apply (drule not0_implies_Suc, auto)
+apply (drule gr0_implies_Suc, auto)
 done
 
 
 lemma r_le_a_forw:
-  "[| (k::nat) \<noteq> 0; k < p^a; p\<noteq>0; (p^r) dvd (p^a) - k |] ==> r <= a"
+  "[| (k::nat) > 0; k < p^a; p>0; (p^r) dvd (p^a) - k |] ==> r <= a"
 by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
 
-lemma p_fac_backw: "[| m\<noteq>0; k\<noteq>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]  
+lemma p_fac_backw: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]  
   ==> (p^r) dvd (p^a)*m - k"
 apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
 apply (subgoal_tac "p^r dvd p^a*m")
@@ -232,7 +232,7 @@
 apply (drule less_imp_Suc_add, auto)
 done
 
-lemma exponent_p_a_m_k_equation: "[| m\<noteq>0; k\<noteq>0; (p::nat)\<noteq>0;  k < p^a |]  
+lemma exponent_p_a_m_k_equation: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a |]  
   ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
 apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
 done
@@ -249,7 +249,7 @@
 apply (induct_tac "k")
 apply (simp (no_asm))
 (*induction step*)
-apply (subgoal_tac "(Suc (j+n) choose Suc n) \<noteq> 0")
+apply (subgoal_tac "(Suc (j+n) choose Suc n) > 0")
  prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
 apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) = 
                     exponent p (Suc n)")
@@ -278,7 +278,7 @@
 
 
 lemma const_p_fac_right:
-  "m\<noteq>0 ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
+  "m>0 ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
 apply (case_tac "prime p")
  prefer 2 apply simp 
 apply (frule_tac a = a in zero_less_prime_power)
@@ -296,7 +296,7 @@
 done
 
 lemma const_p_fac:
-  "m\<noteq>0 ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
+  "m>0 ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
 apply (case_tac "prime p")
  prefer 2 apply simp 
 apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -126,7 +126,7 @@
 apply (blast intro: one_closed zero_less_card_empty)
 done
 
-lemma (in sylow) zero_less_m: "m \<noteq> 0"
+lemma (in sylow) zero_less_m: "m > 0"
 apply (cut_tac zero_less_o_G)
 apply (simp add: order_G)
 done
@@ -134,7 +134,7 @@
 lemma (in sylow) card_calM: "card(calM) = (p^a) * m choose p^a"
 by (simp add: calM_def n_subsets order_G [symmetric] order_def)
 
-lemma (in sylow) zero_less_card_calM: "card calM \<noteq> 0"
+lemma (in sylow) zero_less_card_calM: "card calM > 0"
 by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)
 
 lemma (in sylow) max_p_div_calM:
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Complex/ex/HarmonicSeries.thy
--- a/src/HOL/Complex/ex/HarmonicSeries.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Complex/ex/HarmonicSeries.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -80,7 +80,7 @@
       then have
         "inverse (real x) = 1 / (real x)"
         by (rule nonzero_inverse_eq_divide)
-      moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef neq0_conv)
+      moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef)
       then have
         "inverse (real tm) = 1 / (real tm)"
         by (rule nonzero_inverse_eq_divide)
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Complex/ex/MIR.thy
--- a/src/HOL/Complex/ex/MIR.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -268,7 +268,7 @@
 | "fmsize (NDvd i t) = 2"
 | "fmsize p = 1"
   (* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p \<noteq> 0"	
+lemma fmsize_pos: "fmsize p > 0"	
 by (induct p rule: fmsize.induct) simp_all
 
   (* Semantics of formulae (fm) *)
@@ -316,7 +316,7 @@
   "prep (Imp p q) = prep (Or (NOT p) q)"
   "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   "prep p = p"
-(hints simp add: fmsize_pos neq0_conv[symmetric])
+(hints simp add: fmsize_pos)
 lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
 by (induct p rule: prep.induct, auto)
 
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Complex/ex/ReflectedFerrack.thy
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -106,7 +106,7 @@
   "fmsize (A p) = 4+ fmsize p"
   "fmsize p = 1"
   (* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p \<noteq> 0"
+lemma fmsize_pos: "fmsize p > 0"
 by (induct p rule: fmsize.induct) simp_all
 
   (* Semantics of formulae (fm) *)
@@ -917,7 +917,7 @@
   "prep (Imp p q) = prep (Or (NOT p) q)"
   "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   "prep p = p"
-(hints simp add: fmsize_pos neq0_conv[symmetric])
+(hints simp add: fmsize_pos)
 lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
 by (induct p rule: prep.induct, auto)
 
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Divides.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -250,14 +250,14 @@
   apply (simp add: quorem_def)
   done
 
-lemma quorem_div_mod: "b \<noteq> 0 ==> quorem ((a, b), (a div b, a mod b))"
-  unfolding quorem_def by simp
+lemma quorem_div_mod: "b > 0 ==> quorem ((a, b), (a div b, a mod b))"
+unfolding quorem_def by simp
 
-lemma quorem_div: "[| quorem((a,b),(q,r));  b \<noteq> 0 |] ==> a div b = q"
-  by (simp add: quorem_div_mod [THEN unique_quotient])
+lemma quorem_div: "[| quorem((a,b),(q,r));  b > 0 |] ==> a div b = q"
+by (simp add: quorem_div_mod [THEN unique_quotient])
 
-lemma quorem_mod: "[| quorem((a,b),(q,r));  b \<noteq> 0 |] ==> a mod b = r"
-  by (simp add: quorem_div_mod [THEN unique_remainder])
+lemma quorem_mod: "[| quorem((a,b),(q,r));  b > 0 |] ==> a mod b = r"
+by (simp add: quorem_div_mod [THEN unique_remainder])
 
 (** A dividend of zero **)
 
@@ -270,9 +270,9 @@
 (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
 
 lemma quorem_mult1_eq:
-     "[| quorem((b,c),(q,r)); c \<noteq> 0 |]
-      ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
-  by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
+  "[| quorem((b,c),(q,r)); c > 0 |]
+   ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
+by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
 
 lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
 apply (cases "c = 0", simp)
@@ -291,17 +291,18 @@
    apply (simp_all add: mult_commute)
   done
 
-lemma mod_mult_distrib_mod: "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
-  apply (rule mod_mult1_eq' [THEN trans])
-  apply (rule mod_mult1_eq)
-  done
+lemma mod_mult_distrib_mod:
+  "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
+apply (rule mod_mult1_eq' [THEN trans])
+apply (rule mod_mult1_eq)
+done
 
 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
 
 lemma quorem_add1_eq:
-     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c \<noteq> 0 |]
-      ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
-  by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
+  "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c > 0 |]
+   ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
+by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
 
 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
 lemma div_add1_eq:
@@ -621,7 +622,7 @@
   apply (simp add: power_add)
   done
 
-lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
+lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
   by (induct n) auto
 
 lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
@@ -690,19 +691,20 @@
 
 lemma split_div_lemma:
   "0 < n \<Longrightarrow> (n * q \<le> m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
-  apply (rule iffI)
-  apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
-prefer 3; apply assumption
-  apply (simp_all add: quorem_def) apply arith
-  apply (rule conjI)
-  apply (rule_tac P="%x. n * (m div n) \<le> x" in
+apply (rule iffI)
+ apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
+   prefer 3; apply assumption
+  apply (simp_all add: quorem_def)
+ apply arith
+apply (rule conjI)
+ apply (rule_tac P="%x. n * (m div n) \<le> x" in
     subst [OF mod_div_equality [of _ n]])
-  apply (simp only: add: mult_ac)
-  apply (rule_tac P="%x. x < n + n * (m div n)" in
+ apply (simp only: add: mult_ac)
+ apply (rule_tac P="%x. x < n + n * (m div n)" in
     subst [OF mod_div_equality [of _ n]])
-  apply (simp only: add: mult_ac add_ac)
-  apply (rule add_less_mono1, simp)
-  done
+apply (simp only: add: mult_ac add_ac)
+apply (rule add_less_mono1, simp)
+done
 
 theorem split_div':
   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -1652,16 +1652,6 @@
 apply(subst card_insert)
  apply(auto intro:ccontr)
 done
-(*
-lemma card_1_eq:
-  "(card A = Suc 0) = (\<exists>x. A = {x})"
-by (auto dest!: card_eq_SucD)
-
-lemma card_2_eq:
- "(card A = Suc(Suc 0)) = (\<exists>x y. x\<noteq>y & A = {x,y})" 
-by (auto dest!: card_eq_SucD)
-*)
-
 
 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
 apply (cases "finite A")
@@ -1725,7 +1715,7 @@
 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
 
 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
-  by (simp add: card_seteq card_image)
+by (simp add: card_seteq card_image)
 
 lemma eq_card_imp_inj_on:
   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
@@ -1806,6 +1796,32 @@
   done
 
 
+subsubsection {* Relating injectivity and surjectivity *}
+
+lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
+apply(rule eq_card_imp_inj_on, assumption)
+apply(frule finite_imageI)
+apply(drule (1) card_seteq)
+apply(erule card_image_le)
+apply simp
+done
+
+lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
+shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
+by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
+
+lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
+shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
+by(fastsimp simp:surj_def dest!: endo_inj_surj)
+
+corollary infinite_UNIV_nat: "~finite(UNIV::nat set)"
+proof
+  assume "finite(UNIV::nat set)"
+  with finite_UNIV_inj_surj[of Suc]
+  show False by simp (blast dest: Suc_neq_Zero surjD)
+qed
+
+
 subsection{* A fold functional for non-empty sets *}
 
 text{* Does not require start value. *}
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Hyperreal/Fact.thy
--- a/src/HOL/Hyperreal/Fact.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Hyperreal/Fact.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -20,7 +20,7 @@
 by (induct n) auto
 
 lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
-by (simp add: neq0_conv)
+by simp
 
 lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
 by auto
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -331,7 +331,7 @@
      "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
       ==> {n. N < f n} \<in> FreeUltrafilterNat"
 apply (induct_tac N)
-apply (drule_tac x = 0 in spec, simp add: neq0_conv)
+apply (drule_tac x = 0 in spec, simp)
 apply (drule_tac x = "Suc n" in spec)
 apply (elim ultra, auto)
 done
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -114,7 +114,7 @@
 done
 
 lemma Maclaurin:
-   "[| 0 < h; n \<noteq> 0; diff 0 = f;
+   "[| 0 < h; n > 0; diff 0 = f;
        \<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |]
     ==> \<exists>t. 0 < t &
               t < h &
@@ -185,7 +185,7 @@
 done
 
 lemma Maclaurin_objl:
-  "0 < h & n\<noteq>0 & diff 0 = f &
+  "0 < h & n>0 & diff 0 = f &
   (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
    --> (\<exists>t. 0 < t & t < h &
             f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
@@ -218,7 +218,7 @@
 by (blast intro: Maclaurin2)
 
 lemma Maclaurin_minus:
-   "[| h < 0; n \<noteq> 0; diff 0 = f;
+   "[| h < 0; n > 0; diff 0 = f;
        \<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t |]
     ==> \<exists>t. h < t &
               t < 0 &
@@ -245,7 +245,7 @@
 done
 
 lemma Maclaurin_minus_objl:
-     "(h < 0 & n \<noteq> 0 & diff 0 = f &
+     "(h < 0 & n > 0 & diff 0 = f &
        (\<forall>m t.
           m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t))
     --> (\<exists>t. h < t &
@@ -261,7 +261,7 @@
 (* not good for PVS sin_approx, cos_approx *)
 
 lemma Maclaurin_bi_le_lemma [rule_format]:
-  "n\<noteq>0 \<longrightarrow>
+  "n>0 \<longrightarrow>
    diff 0 0 =
    (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
    diff n 0 * 0 ^ n / real (fact n)"
@@ -294,7 +294,7 @@
 lemma Maclaurin_all_lt:
      "[| diff 0 = f;
          \<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
-        x ~= 0; n \<noteq> 0
+        x ~= 0; n > 0
       |] ==> \<exists>t. 0 < abs t & abs t < abs x &
                f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
                      (diff n t / real (fact n)) * x ^ n"
@@ -308,7 +308,7 @@
 lemma Maclaurin_all_lt_objl:
      "diff 0 = f &
       (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
-      x ~= 0 & n \<noteq> 0
+      x ~= 0 & n > 0
       --> (\<exists>t. 0 < abs t & abs t < abs x &
                f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
                      (diff n t / real (fact n)) * x ^ n)"
@@ -346,7 +346,7 @@
 
 subsection{*Version for Exponential Function*}
 
-lemma Maclaurin_exp_lt: "[| x ~= 0; n \<noteq> 0 |]
+lemma Maclaurin_exp_lt: "[| x ~= 0; n > 0 |]
       ==> (\<exists>t. 0 < abs t &
                 abs t < abs x &
                 exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
@@ -423,9 +423,8 @@
 done
 
 
-
 lemma Maclaurin_sin_expansion3:
-     "[| n \<noteq> 0; 0 < x |] ==>
+     "[| n > 0; 0 < x |] ==>
        \<exists>t. 0 < t & t < x &
        sin x =
        (\<Sum>m=0..<n. (if even m then 0
@@ -491,7 +490,7 @@
 done
 
 lemma Maclaurin_cos_expansion2:
-     "[| 0 < x; n \<noteq> 0 |] ==>
+     "[| 0 < x; n > 0 |] ==>
        \<exists>t. 0 < t & t < x &
        cos x =
        (\<Sum>m=0..<n. (if even m
@@ -510,7 +509,7 @@
 done
 
 lemma Maclaurin_minus_cos_expansion:
-     "[| x < 0; n \<noteq> 0 |] ==>
+     "[| x < 0; n > 0 |] ==>
        \<exists>t. x < t & t < 0 &
        cos x =
        (\<Sum>m=0..<n. (if even m
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -782,7 +782,7 @@
 declare pexp_one [simp]
 
 lemma lemma_order_root [rule_format]:
-     "\<forall>p a. n \<noteq> 0 & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
+     "\<forall>p a. n > 0 & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
              --> poly p a = 0"
 apply (induct "n", blast)
 apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
@@ -792,8 +792,9 @@
 apply (case_tac "poly p = poly []", auto)
 apply (simp add: poly_linear_divides del: pmult_Cons, safe)
 apply (drule_tac [!] a = a in order2)
+apply (rule ccontr)
 apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
-apply (metis gr0_conv lemma_order_root)
+apply (blast intro: lemma_order_root)
 done
 
 lemma order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
@@ -842,7 +843,7 @@
 
 (* FIXME: too too long! *)
 lemma lemma_order_pderiv [rule_format]:
-     "\<forall>p q a. n \<noteq> 0 &
+     "\<forall>p q a. n > 0 &
        poly (pderiv p) \<noteq> poly [] &
        poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q
        --> n = Suc (order a (pderiv p))"
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Hyperreal/Taylor.thy
--- a/src/HOL/Hyperreal/Taylor.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Hyperreal/Taylor.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -15,7 +15,7 @@
 *}
 
 lemma taylor_up: 
-  assumes INIT: "n\<noteq>0" "diff 0 = f"
+  assumes INIT: "n>0" "diff 0 = f"
   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
   and INTERV: "a \<le> c" "c < b" 
   shows "\<exists> t. c < t & t < b & 
@@ -24,9 +24,9 @@
 proof -
   from INTERV have "0 < b-c" by arith
   moreover 
-  from INIT have "n\<noteq>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
+  from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
   moreover
-  have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"  
+  have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
   proof (intro strip)
     fix m t
     assume "m < n & 0 <= t & t <= b - c"
@@ -57,7 +57,7 @@
 qed
 
 lemma taylor_down:
-  assumes INIT: "n\<noteq>0" "diff 0 = f"
+  assumes INIT: "n>0" "diff 0 = f"
   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
   and INTERV: "a < c" "c \<le> b"
   shows "\<exists> t. a < t & t < c & 
@@ -66,7 +66,7 @@
 proof -
   from INTERV have "a-c < 0" by arith
   moreover 
-  from INIT have "n\<noteq>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
+  from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
   moreover
   have "ALL m t. m < n & a-c <= t & t <= 0 --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
   proof (rule allI impI)+
@@ -97,7 +97,7 @@
 qed
 
 lemma taylor:
-  assumes INIT: "n\<noteq>0" "diff 0 = f"
+  assumes INIT: "n>0" "diff 0 = f"
   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
   and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" 
   shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/IntArith.thy
--- a/src/HOL/IntArith.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/IntArith.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -398,6 +398,15 @@
  apply (frule pos_zmult_eq_1_iff_lemma, auto) 
 done
 
+(* Could be simplified but Presburger only becomes available too late *)
+lemma infinite_UNIV_int: "~finite(UNIV::int set)"
+proof
+  assume "finite(UNIV::int set)"
+  moreover have "~(EX i::int. 2*i = 1)"
+    by (auto simp: pos_zmult_eq_1_iff)
+  ultimately show False using finite_UNIV_inj_surj[of "%n::int. n+n"]
+    by (simp add:inj_on_def surj_def) (blast intro:sym)
+qed
 
 subsection {* Legacy ML bindings *}
 
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Library/Binomial.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -44,7 +44,7 @@
 lemma binomial_1 [simp]: "(n choose Suc 0) = n"
 by (induct n) simp_all
 
-lemma zero_less_binomial: "k \<le> n ==> (n choose k) \<noteq> 0"
+lemma zero_less_binomial: "k \<le> n ==> (n choose k) > 0"
 by (induct n k rule: diff_induct) simp_all
 
 lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
@@ -53,8 +53,9 @@
 apply (simp add: zero_less_binomial)
 done
 
-lemma zero_less_binomial_iff: "(n choose k \<noteq> 0) = (k\<le>n)"
-by (simp add: linorder_not_less binomial_eq_0_iff)
+lemma zero_less_binomial_iff: "(n choose k > 0) = (k\<le>n)"
+by(simp add: linorder_not_less binomial_eq_0_iff neq0_conv[symmetric]
+        del:neq0_conv)
 
 (*Might be more useful if re-oriented*)
 lemma Suc_times_binomial_eq:
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -11,7 +11,7 @@
 
 subsection {* The type of multisets *}
 
-typedef 'a multiset = "{f::'a => nat. finite {x . f x \<noteq> 0}}"
+typedef 'a multiset = "{f::'a => nat. finite {x . f x > 0}}"
 proof
   show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp
 qed
@@ -38,7 +38,7 @@
 
 abbreviation
   Melem :: "'a => 'a multiset => bool"  ("(_/ :# _)" [50, 51] 50) where
-  "a :# M == count M a \<noteq> 0"
+  "a :# M == count M a > 0"
 
 syntax
   "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
@@ -309,7 +309,7 @@
    apply (rule ext, force, clarify)
   apply (frule setsum_SucD, clarify)
   apply (rename_tac a)
-  apply (subgoal_tac "finite {x. (f (a := f a - 1)) x \<noteq> 0}")
+  apply (subgoal_tac "finite {x. (f (a := f a - 1)) x > 0}")
    prefer 2
    apply (rule finite_subset)
     prefer 2
@@ -759,7 +759,7 @@
   apply (rule_tac x = "x # xa" in exI, auto)
   done
 
-lemma set_count_greater_0: "set x = {a. count (multiset_of x) a \<noteq> 0}"
+lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}"
   by (induct x) auto
 
 lemma distinct_count_atmost_1:
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Library/Parity.thy
--- a/src/HOL/Library/Parity.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Library/Parity.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -222,7 +222,7 @@
   apply (subst power_add)
   apply (subst zero_le_mult_iff)
   apply auto
-  apply (subgoal_tac "x = 0 & y \<noteq> 0")
+  apply (subgoal_tac "x = 0 & y > 0")
   apply (erule conjE, assumption)
   apply (subst power_eq_0_iff [symmetric])
   apply (subgoal_tac "0 <= x^y * x^y")
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Library/Word.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -479,7 +479,7 @@
         with mod_div_equality [of n 2]
         show "n div 2 * 2 = n" by simp
       next
-        assume "n mod 2 \<noteq> 0"
+        assume "n mod 2 = Suc 0"
         with mod_div_equality [of n 2]
         show "Suc (n div 2 * 2) = n" by arith
       qed
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/List.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -950,7 +950,7 @@
   proof (cases)
     assume "p x"
     hence eq: "?S' = insert 0 (Suc ` ?S)"
-      by(auto simp: nth_Cons image_def split:nat.split dest:not0_implies_Suc)
+      by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)
     have "length (filter p (x # xs)) = Suc(card ?S)"
       using Cons `p x` by simp
     also have "\<dots> = Suc(card(Suc ` ?S))" using fin
@@ -961,7 +961,7 @@
   next
     assume "\<not> p x"
     hence eq: "?S' = Suc ` ?S"
-      by(auto simp add: image_def neq0_conv split:nat.split elim:lessE)
+      by(auto simp add: image_def split:nat.split elim:lessE)
     have "length (filter p (x # xs)) = card ?S"
       using Cons `\<not> p x` by simp
     also have "\<dots> = card(Suc ` ?S)" using fin
@@ -2456,7 +2456,7 @@
 
 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
 apply(induct xs arbitrary: I)
-apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: not0_implies_Suc)
+apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
 done
 
 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Nat.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -100,22 +100,22 @@
 text {* Injectiveness and distinctness lemmas *}
 
 lemma Suc_neq_Zero: "Suc m = 0 ==> R"
-  by (rule notE, rule Suc_not_Zero)
+by (rule notE, rule Suc_not_Zero)
 
 lemma Zero_neq_Suc: "0 = Suc m ==> R"
-  by (rule Suc_neq_Zero, erule sym)
+by (rule Suc_neq_Zero, erule sym)
 
 lemma Suc_inject: "Suc x = Suc y ==> x = y"
-  by (rule inj_Suc [THEN injD])
+by (rule inj_Suc [THEN injD])
 
 lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
-  by auto
+by auto
 
 lemma n_not_Suc_n: "n \<noteq> Suc n"
-  by (induct n) simp_all
+by (induct n) simp_all
 
 lemma Suc_n_not_n: "Suc t \<noteq> t"
-  by (rule not_sym, rule n_not_Suc_n)
+by (rule not_sym, rule n_not_Suc_n)
 
 
 text {* A special form of induction for reasoning
@@ -221,12 +221,12 @@
   done
 
 lemma less_irrefl [elim!]: "(n::nat) < n ==> R"
-  by (rule notE, rule less_not_refl)
+by (rule notE, rule less_not_refl)
 
 lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)" by blast
 
 lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
-  by (rule not_sym, rule less_not_refl2)
+by (rule not_sym, rule less_not_refl2)
 
 lemma lessE:
   assumes major: "i < k"
@@ -239,10 +239,10 @@
   done
 
 lemma not_less0 [iff]: "~ n < (0::nat)"
-  by (blast elim: lessE)
+by (blast elim: lessE)
 
 lemma less_zeroE: "(n::nat) < 0 ==> R"
-  by (rule notE, rule not_less0)
+by (rule notE, rule not_less0)
 
 lemma less_SucE: assumes major: "m < Suc n"
   and less: "m < n ==> P" and eq: "m = n ==> P" shows P
@@ -252,16 +252,16 @@
   done
 
 lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
-  by (blast elim!: less_SucE intro: less_trans)
+by (blast elim!: less_SucE intro: less_trans)
 
 lemma less_one [iff,noatp]: "(n < (1::nat)) = (n = 0)"
-  by (simp add: less_Suc_eq)
+by (simp add: less_Suc_eq)
 
 lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
-  by (simp add: less_Suc_eq)
+by (simp add: less_Suc_eq)
 
 lemma Suc_mono: "m < n ==> Suc m < Suc n"
-  by (induct n) (fast elim: less_trans lessE)+
+by (induct n) (fast elim: less_trans lessE)+
 
 text {* "Less than" is a linear ordering *}
 lemma less_linear: "m < n | m = n | n < (m::nat)"
@@ -312,7 +312,7 @@
   done
 
 lemma Suc_less_SucD: "Suc m < Suc n ==> m < n"
-  by (blast elim: lessE dest: Suc_lessD)
+by (blast elim: lessE dest: Suc_lessD)
 
 lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)"
   apply (rule iffI)
@@ -333,7 +333,7 @@
 
 text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
 lemma not_less_eq: "(~ m < n) = (n < Suc m)"
-  by (induct m n rule: diff_induct) simp_all
+by (induct m n rule: diff_induct) simp_all
 
 text {* Complete induction, aka course-of-values induction *}
 lemma nat_less_induct:
@@ -353,22 +353,22 @@
   unfolding le_def by (rule not_less_eq [symmetric])
 
 lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n"
-  by (rule less_Suc_eq_le [THEN iffD2])
+by (rule less_Suc_eq_le [THEN iffD2])
 
 lemma le0 [iff]: "(0::nat) \<le> n"
   unfolding le_def by (rule not_less0)
 
 lemma Suc_n_not_le_n: "~ Suc n \<le> n"
-  by (simp add: le_def)
+by (simp add: le_def)
 
 lemma le_0_eq [iff]: "((i::nat) \<le> 0) = (i = 0)"
-  by (induct i) (simp_all add: le_def)
+by (induct i) (simp_all add: le_def)
 
 lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)"
-  by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
+by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
 
 lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
-  by (drule le_Suc_eq [THEN iffD1], iprover+)
+by (drule le_Suc_eq [THEN iffD1], iprover+)
 
 lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
   apply (simp add: le_def less_Suc_eq)
@@ -376,7 +376,7 @@
   done -- {* formerly called lessD *}
 
 lemma Suc_leD: "Suc(m) \<le> n ==> m \<le> n"
-  by (simp add: le_def less_Suc_eq)
+by (simp add: le_def less_Suc_eq)
 
 text {* Stronger version of @{text Suc_leD} *}
 lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
@@ -386,13 +386,13 @@
   done
 
 lemma Suc_le_eq: "(Suc m \<le> n) = (m < n)"
-  by (blast intro: Suc_leI Suc_le_lessD)
+by (blast intro: Suc_leI Suc_le_lessD)
 
 lemma le_SucI: "m \<le> n ==> m \<le> Suc n"
-  by (unfold le_def) (blast dest: Suc_lessD)
+by (unfold le_def) (blast dest: Suc_lessD)
 
 lemma less_imp_le: "m < n ==> m \<le> (n::nat)"
-  by (unfold le_def) (blast elim: less_asym)
+by (unfold le_def) (blast elim: less_asym)
 
 text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *}
 lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq
@@ -411,36 +411,36 @@
   by (blast elim!: less_irrefl elim: less_asym)
 
 lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
-  by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq)
+by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq)
 
 text {* Useful with @{text blast}. *}
 lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
-  by (rule less_or_eq_imp_le) (rule disjI2)
+by (rule less_or_eq_imp_le) (rule disjI2)
 
 lemma le_refl: "n \<le> (n::nat)"
-  by (simp add: le_eq_less_or_eq)
+by (simp add: le_eq_less_or_eq)
 
 lemma le_less_trans: "[| i \<le> j; j < k |] ==> i < (k::nat)"
-  by (blast dest!: le_imp_less_or_eq intro: less_trans)
+by (blast dest!: le_imp_less_or_eq intro: less_trans)
 
 lemma less_le_trans: "[| i < j; j \<le> k |] ==> i < (k::nat)"
-  by (blast dest!: le_imp_less_or_eq intro: less_trans)
+by (blast dest!: le_imp_less_or_eq intro: less_trans)
 
 lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
-  by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans)
+by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans)
 
 lemma le_anti_sym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
-  by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym)
+by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym)
 
 lemma Suc_le_mono [iff]: "(Suc n \<le> Suc m) = (n \<le> m)"
-  by (simp add: le_simps)
+by (simp add: le_simps)
 
 text {* Axiom @{text order_less_le} of class @{text order}: *}
 lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)"
-  by (simp add: le_def nat_neq_iff) (blast elim!: less_asym)
+by (simp add: le_def nat_neq_iff) (blast elim!: less_asym)
 
 lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n"
-  by (rule iffD2, rule nat_less_le, rule conjI)
+by (rule iffD2, rule nat_less_le, rule conjI)
 
 text {* Axiom @{text linorder_linear} of class @{text linorder}: *}
 lemma nat_le_linear: "(m::nat) \<le> n | n \<le> m"
@@ -457,7 +457,7 @@
 lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat]
 
 lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
-  by (blast elim!: less_SucE)
+by (blast elim!: less_SucE)
 
 text {*
   Rewrite @{term "n < Suc m"} to @{term "n = m"}
@@ -465,7 +465,7 @@
   Not suitable as default simprules because they often lead to looping
 *}
 lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)"
-  by (rule not_less_less_Suc_eq, rule leD)
+by (rule not_less_less_Suc_eq, rule leD)
 
 lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
 
@@ -478,46 +478,47 @@
 
 text {* Polymorphic, not just for @{typ nat} *}
 lemma zero_reorient: "(0 = x) = (x = 0)"
-  by auto
+by auto
 
 lemma one_reorient: "(1 = x) = (x = 1)"
-  by auto
+by auto
 
 text {* These two rules ease the use of primitive recursion.
 NOTE USE OF @{text "=="} *}
 lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c"
-  by simp
+by simp
 
 lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)"
-  by simp
+by simp
 
 lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
-  by (cases n) simp_all
+by (cases n) simp_all
+
+lemma gr0_implies_Suc: "n > 0 ==> \<exists>m. n = Suc m"
+by (cases n) simp_all
 
 lemma gr_implies_not0: fixes n :: nat shows "m<n ==> n \<noteq> 0"
-  by (cases n) simp_all
+by (cases n) simp_all
 
-lemma neq0_conv: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
-  by (cases n) simp_all
-
-lemmas gr0_conv = neq0_conv[symmetric]
+lemma neq0_conv[iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
+by (cases n) simp_all
 
 text {* This theorem is useful with @{text blast} *}
 lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
-  by (rule iffD1, rule neq0_conv, iprover)
+by (rule neq0_conv[THEN iffD1], iprover)
 
 lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
-  by (fast intro: not0_implies_Suc)
+by (fast intro: not0_implies_Suc)
 
 lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
 using neq0_conv by blast
 
 lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
-  by (induct m') simp_all
+by (induct m') simp_all
 
 text {* Useful in certain inductive arguments *}
 lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))"
-  by (cases m) simp_all
+by (cases m) simp_all
 
 lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
   apply (rule nat_less_induct)
@@ -542,48 +543,48 @@
   done
 
 lemma Least_Suc2:
-     "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
-  by (erule (1) Least_Suc [THEN ssubst], simp)
+   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
+by (erule (1) Least_Suc [THEN ssubst], simp)
 
 
 subsection {* @{term min} and @{term max} *}
 
 lemma mono_Suc: "mono Suc"
-  by (rule monoI) simp
+by (rule monoI) simp
 
 lemma min_0L [simp]: "min 0 n = (0::nat)"
-  by (rule min_leastL) simp
+by (rule min_leastL) simp
 
 lemma min_0R [simp]: "min n 0 = (0::nat)"
-  by (rule min_leastR) simp
+by (rule min_leastR) simp
 
 lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
-  by (simp add: mono_Suc min_of_mono)
+by (simp add: mono_Suc min_of_mono)
 
 lemma min_Suc1:
    "min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
-  by (simp split: nat.split)
+by (simp split: nat.split)
 
 lemma min_Suc2:
    "min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))"
-  by (simp split: nat.split)
+by (simp split: nat.split)
 
 lemma max_0L [simp]: "max 0 n = (n::nat)"
-  by (rule max_leastL) simp
+by (rule max_leastL) simp
 
 lemma max_0R [simp]: "max n 0 = (n::nat)"
-  by (rule max_leastR) simp
+by (rule max_leastR) simp
 
 lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
-  by (simp add: mono_Suc max_of_mono)
+by (simp add: mono_Suc max_of_mono)
 
 lemma max_Suc1:
    "max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
-  by (simp split: nat.split)
+by (simp split: nat.split)
 
 lemma max_Suc2:
    "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
-  by (simp split: nat.split)
+by (simp split: nat.split)
 
 
 subsection {* Basic rewrite rules for the arithmetic operators *}
@@ -591,10 +592,10 @@
 text {* Difference *}
 
 lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
-  by (induct n) simp_all
+by (induct n) simp_all
 
 lemma diff_Suc_Suc [simp, code]: "Suc(m) - Suc(n) = m - n"
-  by (induct n) simp_all
+by (induct n) simp_all
 
 
 text {*
@@ -602,7 +603,7 @@
   However, none of the generalizations are currently in the simpset,
   and I dread to think what happens if I put them in
 *}
-lemma Suc_pred [simp]: "0 \<noteq> n ==> Suc (n - Suc 0) = n"
+lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
 by (simp split add: nat.split)
 
 declare diff_Suc [simp del, code del]
@@ -611,22 +612,22 @@
 subsection {* Addition *}
 
 lemma add_0_right [simp]: "m + 0 = (m::nat)"
-  by (induct m) simp_all
+by (induct m) simp_all
 
 lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
-  by (induct m) simp_all
+by (induct m) simp_all
 
 lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
-  by simp
+by simp
 
 
 text {* Associative law for addition *}
 lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)"
-  by (induct m) simp_all
+by (induct m) simp_all
 
 text {* Commutative law for addition *}
 lemma nat_add_commute: "m + n = n + (m::nat)"
-  by (induct m) simp_all
+by (induct m) simp_all
 
 lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
   apply (rule mk_left_commute [of "op +"])
@@ -635,30 +636,30 @@
   done
 
 lemma nat_add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))"
-  by (induct k) simp_all
+by (induct k) simp_all
 
 lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))"
-  by (induct k) simp_all
+by (induct k) simp_all
 
 lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
-  by (induct k) simp_all
+by (induct k) simp_all
 
 lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"
-  by (induct k) simp_all
+by (induct k) simp_all
 
 text {* Reasoning about @{text "m + 0 = 0"}, etc. *}
 
 lemma add_is_0 [iff]: fixes m :: nat shows "(m + n = 0) = (m = 0 & n = 0)"
-  by (cases m) simp_all
+by (cases m) simp_all
 
 lemma add_is_1: "(m+n= Suc 0) = (m= Suc 0 & n=0 | m=0 & n= Suc 0)"
-  by (cases m) simp_all
+by (cases m) simp_all
 
 lemma one_is_add: "(Suc 0 = m + n) = (m = Suc 0 & n = 0 | m = 0 & n = Suc 0)"
-  by (rule trans, rule eq_commute, rule add_is_1)
+by (rule trans, rule eq_commute, rule add_is_1)
 
-lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m\<noteq>0 | n\<noteq>0)"
-by (simp add:gr0_conv)
+lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m>0 | n>0)"
+by(auto dest:gr0_implies_Suc)
 
 lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0"
   apply (drule add_0_right [THEN ssubst])
@@ -677,26 +678,26 @@
 
 text {* right annihilation in product *}
 lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
-  by (induct m) simp_all
+by (induct m) simp_all
 
 text {* right successor law for multiplication *}
 lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
-  by (induct m) (simp_all add: nat_add_left_commute)
+by (induct m) (simp_all add: nat_add_left_commute)
 
 text {* Commutative law for multiplication *}
 lemma nat_mult_commute: "m * n = n * (m::nat)"
-  by (induct m) simp_all
+by (induct m) simp_all
 
 text {* addition distributes over multiplication *}
 lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
-  by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute)
+by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute)
 
 lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
-  by (induct m) (simp_all add: nat_add_assoc)
+by (induct m) (simp_all add: nat_add_assoc)
 
 text {* Associative law for multiplication *}
 lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
-  by (induct m) (simp_all add: add_mult_distrib)
+by (induct m) (simp_all add: add_mult_distrib)
 
 
 text{*The naturals form a @{text comm_semiring_1_cancel}*}
@@ -725,7 +726,7 @@
 
 text {* strict, in 1st argument *}
 lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
-  by (induct k) simp_all
+by (induct k) simp_all
 
 text {* strict, in both arguments *}
 lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
@@ -759,10 +760,10 @@
 qed
 
 lemma nat_mult_1: "(1::nat) * n = n"
-  by simp
+by simp
 
 lemma nat_mult_1_right: "n * (1::nat) = n"
-  by simp
+by simp
 
 
 subsection {* Additional theorems about "less than" *}
@@ -1083,7 +1084,7 @@
 by (simp add: linorder_not_less [symmetric], auto)
 
 lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
-apply (cut_tac less_linear, safe, auto simp add: neq0_conv)
+apply (cut_tac less_linear, safe, auto)
 apply (drule mult_less_mono1, assumption, simp)+
 done
 
@@ -1105,7 +1106,7 @@
   apply (rule disjCI)
   apply (rule nat_less_cases, erule_tac [2] _)
    apply (drule_tac [2] mult_less_mono2)
-    apply (auto simp add: neq0_conv)
+    apply (auto)
   done
 
 
@@ -1119,7 +1120,7 @@
 setup Size.setup
 
 lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
-  by (induct n) simp_all
+by (induct n) simp_all
 
 lemma size_bool [code func]:
   "size (b\<Colon>bool) = 0" by (cases b) auto
@@ -1136,7 +1137,7 @@
   "Suc n = Suc m \<longleftrightarrow> n = m"
   "Suc n = 0 \<longleftrightarrow> False"
   "0 = Suc m \<longleftrightarrow> False"
-  by auto
+by auto
 
 lemma [code func]:
   "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
@@ -1186,7 +1187,7 @@
 by (cases "a<b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
 
 lemma nat_diff_split_asm:
-    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
+  "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
     -- {* elimination of @{text -} on @{text nat} in assumptions *}
 by (simp split: nat_diff_split)
 
@@ -1378,7 +1379,7 @@
   done
 
 lemma of_nat_less_iff [simp]:
-    "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
+  "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
 by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
 
 text{*Special cases where either operand is zero*}
@@ -1390,7 +1391,7 @@
 by (rule of_nat_less_iff [of _ 0, simplified])
 
 lemma of_nat_le_iff [simp]:
-    "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
+  "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
 by (simp add: linorder_not_less [symmetric])
 
 text{*Special cases where either operand is zero*}
@@ -1420,7 +1421,7 @@
 by (simp add: inj_on_def)
 
 lemma of_nat_diff:
-    "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
+  "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
 by (simp del: of_nat_add
     add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
 
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Power.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -140,7 +140,7 @@
 done
 
 lemma power_eq_0_iff [simp]:
-  "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n\<noteq>0)"
+  "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n>0)"
 apply (induct "n")
 apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
 done
@@ -342,7 +342,7 @@
 lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
 by (insert one_le_power [of i n], simp)
 
-lemma nat_zero_less_power_iff [simp]: "(x^n = 0) = (x = (0::nat) & n\<noteq>0)"
+lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
 by (induct "n", auto)
 
 text{*Valid for the naturals, but what if @{text"0<i<1"}?
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Real/RComplete.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -1208,10 +1208,10 @@
   apply simp
 done
 
-lemma natfloor_div_nat: "1 <= x ==> y \<noteq> 0 ==>
+lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
   natfloor (x / real y) = natfloor x div y"
 proof -
-  assume "1 <= (x::real)" and "(y::nat) \<noteq> 0"
+  assume "1 <= (x::real)" and "(y::nat) > 0"
   have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
     by simp
   then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -746,7 +746,7 @@
 lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
 by (simp add: add: real_of_nat_def of_nat_diff)
 
-lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (n \<noteq> 0)"
+lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
 by (auto simp: real_of_nat_def)
 
 lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)"
diff -r aa8474398030 -r ad4d5365d9d8 src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -63,7 +63,7 @@
   "fmsize (NDvd i t) = 2"
   "fmsize p = 1"
   (* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p \<noteq> 0"	
+lemma fmsize_pos: "fmsize p > 0"	
 by (induct p rule: fmsize.induct) simp_all
 
   (* Semantics of formulae (fm) *)
@@ -114,7 +114,7 @@
   "prep (Imp p q) = prep (Or (NOT p) q)"
   "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   "prep p = p"
-(hints simp add: fmsize_pos neq0_conv[symmetric])
+(hints simp add: fmsize_pos)
 lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
 by (induct p arbitrary: bs rule: prep.induct, auto)
 
@@ -189,11 +189,11 @@
 
 lemma numsubst0_I:
   "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
-by (induct t rule: numsubst0.induct,auto dest: not0_implies_Suc)
+by (induct t rule: numsubst0.induct,auto simp:nth_Cons')
 
 lemma numsubst0_I':
   "numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
-by (induct t rule: numsubst0.induct, auto dest: not0_implies_Suc simp: numbound0_I[where b="b" and b'="b'"])
+by (induct t rule: numsubst0.induct, auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
 
 primrec
   "subst0 t T = T"