# HG changeset patch
# User nipkow
# Date 1192971224 -7200
# Node ID 3d4953e8844951e995905f4ca80d79840cf3989f
# Parent  b933700f0384ccd5c89dfa4c623d72b3355cd2ea
Eliminated most of the neq0_conv occurrences. As a result, many
theorems had to be rephrased with ~= 0 instead of > 0.

diff -r b933700f0384 -r 3d4953e88449 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -9,9 +9,8 @@
 
 
 section {*The Combinatorial Argument Underlying the First Sylow Theorem*}
-constdefs
-  exponent      :: "[nat, nat] => nat"
-  "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
+definition exponent :: "nat => nat => nat" where
+"exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
 
 
 subsection{*Prime Theorems*}
@@ -20,7 +19,7 @@
 by (unfold prime_def, force)
 
 lemma prime_iff:
-     "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
+  "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
 apply (auto simp add: prime_imp_one_less)
 apply (blast dest!: prime_dvd_mult)
 apply (auto simp add: prime_def)
@@ -40,8 +39,8 @@
 
 
 lemma prime_dvd_cases:
-     "[| p*k dvd m*n;  prime p |]  
-      ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
+  "[| p*k dvd m*n;  prime p |]  
+   ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
 apply (simp add: prime_iff)
 apply (frule dvd_mult_left)
 apply (subgoal_tac "p dvd m | p dvd n")
@@ -55,8 +54,8 @@
 
 
 lemma prime_power_dvd_cases [rule_format (no_asm)]: "prime p
-      ==> \<forall>m n. p^c dvd m*n -->  
-          (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
+  ==> \<forall>m n. p^c dvd m*n -->  
+        (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
 apply (induct_tac "c")
  apply clarify
  apply (case_tac "a")
@@ -85,8 +84,8 @@
 
 (*needed in this form in Sylow.ML*)
 lemma div_combine:
-     "[| prime p; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |]  
-      ==> p ^ a dvd k"
+  "[| prime p; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |]  
+   ==> p ^ a dvd k"
 by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto)
 
 (*Lemma for power_dvd_bound*)
@@ -96,15 +95,12 @@
 apply simp
 apply (subgoal_tac "2 * n + 2 <= p * p^n", simp)
 apply (subgoal_tac "2 * p^n <= p * p^n")
-(*?arith_tac should handle all of this!*)
-apply (rule order_trans)
-prefer 2 apply assumption
+apply arith
 apply (drule_tac k = 2 in mult_le_mono2, simp)
-apply (rule mult_le_mono1, simp)
 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;  0 < a|] ==> n < a"
+lemma power_dvd_bound: "[|p^n dvd a;  Suc 0 < p;  a \<noteq> 0|] ==> n < a"
 apply (drule dvd_imp_le)
 apply (drule_tac [2] n = n in Suc_le_power, auto)
 done
@@ -113,13 +109,13 @@
 subsection{*Exponent Theorems*}
 
 lemma exponent_ge [rule_format]:
-     "[|p^k dvd n;  prime p;  0<n|] ==> k <= exponent p n"
+  "[|p^k dvd n;  prime p;  0<n|] ==> k <= exponent p n"
 apply (simp add: exponent_def)
 apply (erule Greatest_le)
 apply (blast dest: prime_imp_one_less power_dvd_bound)
 done
 
-lemma power_exponent_dvd: "0<s ==> (p ^ exponent p s) dvd s"
+lemma power_exponent_dvd: "s\<noteq>0 ==> (p ^ exponent p s) dvd s"
 apply (simp add: exponent_def)
 apply clarify
 apply (rule_tac k = 0 in GreatestI)
@@ -127,7 +123,7 @@
 done
 
 lemma power_Suc_exponent_Not_dvd:
-     "[|(p * p ^ exponent p s) dvd s;  prime p |] ==> s=0"
+  "[|(p * p ^ exponent p s) dvd s;  prime p |] ==> s=0"
 apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
  prefer 2 apply simp 
 apply (rule ccontr)
@@ -141,7 +137,7 @@
 done
 
 lemma exponent_equalityI:
-     "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
+  "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
 by (simp (no_asm_simp) add: exponent_def)
 
 lemma exponent_eq_0 [simp]: "\<not> prime p ==> exponent p s = 0"
@@ -149,9 +145,8 @@
 
 
 (* exponent_mult_add, easy inclusion.  Could weaken p \<in> prime to Suc 0 < p *)
-lemma exponent_mult_add1:
-     "[| 0 < a; 0 < b |]   
-      ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
+lemma exponent_mult_add1: "[| a \<noteq> 0; b \<noteq> 0 |]
+  ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
 apply (case_tac "prime p")
 apply (rule exponent_ge)
 apply (auto simp add: power_add)
@@ -159,8 +154,8 @@
 done
 
 (* exponent_mult_add, opposite inclusion *)
-lemma exponent_mult_add2: "[| 0 < a; 0 < b |]  
-      ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
+lemma exponent_mult_add2: "[| a \<noteq> 0; b \<noteq> 0 |]  
+  ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
 apply (case_tac "prime p")
 apply (rule leI, clarify)
 apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto)
@@ -173,9 +168,8 @@
 apply (blast dest: power_Suc_exponent_Not_dvd)
 done
 
-lemma exponent_mult_add:
-     "[| 0 < a; 0 < b |]  
-      ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
+lemma exponent_mult_add: "[| a \<noteq> 0; b \<noteq> 0 |]
+   ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
 by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym)
 
 
@@ -194,40 +188,41 @@
 
 subsection{*Main Combinatorial Argument*}
 
-lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
+lemma le_extend_mult: "[| c \<noteq> 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:
-     "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
+  "[| (m::nat) \<noteq> 0; k \<noteq> 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)
 apply (drule less_imp_le [of a])
 apply (drule le_imp_power_dvd)
 apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
-apply (metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less)
+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: "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |]  
-      ==> (p^r) dvd (p^a) - k"
+lemma p_fac_forw: "[| (m::nat) \<noteq> 0; k\<noteq>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")
  prefer 2 apply (blast intro: dvd_mult2)
 apply (drule dvd_diffD1)
   apply assumption
  prefer 2 apply (blast intro: dvd_diff)
-apply (drule less_imp_Suc_add, auto)
+apply (drule not0_implies_Suc, auto)
 done
 
 
-lemma r_le_a_forw: "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a"
+lemma r_le_a_forw:
+  "[| (k::nat) \<noteq> 0; k < p^a; p\<noteq>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: "[| 0<m; 0<k; 0 < (p::nat);  k < p^a;  (p^r) dvd p^a - k |]  
-      ==> (p^r) dvd (p^a)*m - k"
+lemma p_fac_backw: "[| m\<noteq>0; k\<noteq>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")
  prefer 2 apply (blast intro: dvd_mult2)
@@ -237,8 +232,8 @@
 apply (drule less_imp_Suc_add, auto)
 done
 
-lemma exponent_p_a_m_k_equation: "[| 0<m; 0<k; 0 < (p::nat);  k < p^a |]  
-      ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
+lemma exponent_p_a_m_k_equation: "[| m\<noteq>0; k\<noteq>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
 
@@ -247,14 +242,14 @@
 
 (*The bound K is needed; otherwise it's too weak to be used.*)
 lemma p_not_div_choose_lemma [rule_format]:
-     "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]  
-      ==> k<K --> exponent p ((j+k) choose k) = 0"
+  "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]  
+   ==> k<K --> exponent p ((j+k) choose k) = 0"
 apply (case_tac "prime p")
  prefer 2 apply simp 
 apply (induct_tac "k")
 apply (simp (no_asm))
 (*induction step*)
-apply (subgoal_tac "0 < (Suc (j+n) choose Suc n) ")
+apply (subgoal_tac "(Suc (j+n) choose Suc n) \<noteq> 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)")
@@ -271,9 +266,9 @@
 
 (*The lemma above, with two changes of variables*)
 lemma p_not_div_choose:
-     "[| k<K;  k<=n;   
-       \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]  
-      ==> exponent p (n choose k) = 0"
+  "[| k<K;  k<=n;
+      \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]
+   ==> exponent p (n choose k) = 0"
 apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma)
   prefer 3 apply simp
  prefer 2 apply assumption
@@ -283,7 +278,7 @@
 
 
 lemma const_p_fac_right:
-     "0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
+  "m\<noteq>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)
@@ -301,7 +296,7 @@
 done
 
 lemma const_p_fac:
-     "0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
+  "m\<noteq>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 b933700f0384 -r 3d4953e88449 src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -126,7 +126,7 @@
 apply (blast intro: one_closed zero_less_card_empty)
 done
 
-lemma (in sylow) zero_less_m: "0 < m"
+lemma (in sylow) zero_less_m: "m \<noteq> 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: "0 < card calM"
+lemma (in sylow) zero_less_card_calM: "card calM \<noteq> 0"
 by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)
 
 lemma (in sylow) max_p_div_calM:
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Auth/Guard/Guard.thy
--- a/src/HOL/Auth/Guard/Guard.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Auth/Guard/Guard.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -187,7 +187,7 @@
 
 subsection{*basic facts about @{term crypt_nb}*}
 
-lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> 0 < crypt_nb X"
+lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> crypt_nb X \<noteq> 0"
 by (induct X, simp_all, safe, simp_all)
 
 subsection{*number of Crypt's in a message list*}
@@ -216,7 +216,7 @@
 cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
 by (erule parts.induct, auto simp: in_set_conv_decomp)
 
-lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> 0 < cnb l"
+lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> cnb l \<noteq> 0"
 by (induct l, auto dest: non_empty_crypt_msg parts_insert_substD)
 
 subsection{*list of kparts*}
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Auth/Guard/GuardK.thy
--- a/src/HOL/Auth/Guard/GuardK.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -183,7 +183,7 @@
 
 subsection{*basic facts about @{term crypt_nb}*}
 
-lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> 0 < crypt_nb X"
+lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> crypt_nb X \<noteq> 0"
 by (induct X, simp_all, safe, simp_all)
 
 subsection{*number of Crypt's in a message list*}
@@ -212,7 +212,7 @@
 cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
 by (erule parts.induct, auto simp: in_set_conv_decomp)
 
-lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> 0 < cnb l"
+lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> cnb l \<noteq> 0"
 by (induct l, auto dest: non_empty_crypt_msg parts_insert_substD)
 
 subsection{*list of kparts*}
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Auth/Kerberos_BAN.thy
--- a/src/HOL/Auth/Kerberos_BAN.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -35,7 +35,7 @@
 
 text{*The authenticator only for one journey*}
 specification (authlife)
-  authlife_LB [iff]:    "0 < authlife"
+  authlife_LB [iff]:    "authlife \<noteq> 0"
     by blast
 
 abbreviation
@@ -133,7 +133,7 @@
 apply (rule_tac [2]
            bankerberos.Nil [THEN bankerberos.BK1, THEN bankerberos.BK2,
                              THEN bankerberos.BK3, THEN bankerberos.BK4])
-apply (possibility, simp_all (no_asm_simp) add: used_Cons neq0_conv)
+apply (possibility, simp_all (no_asm_simp) add: used_Cons)
 done
 
 subsection{*Lemmas for reasoning about predicate "Issues"*}
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Complex/ex/MIR.thy
--- a/src/HOL/Complex/ex/MIR.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -268,7 +268,7 @@
 | "fmsize (NDvd i t) = 2"
 | "fmsize p = 1"
   (* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p > 0"	
+lemma fmsize_pos: "fmsize p \<noteq> 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)
+(hints simp add: fmsize_pos neq0_conv[symmetric])
 lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
 by (induct p rule: prep.induct, auto)
 
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Complex/ex/ReflectedFerrack.thy
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -106,7 +106,7 @@
   "fmsize (A p) = 4+ fmsize p"
   "fmsize p = 1"
   (* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p > 0"	
+lemma fmsize_pos: "fmsize p \<noteq> 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)
+(hints simp add: fmsize_pos neq0_conv[symmetric])
 lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
 by (induct p rule: prep.induct, auto)
 
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Divides.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -250,13 +250,13 @@
   apply (simp add: quorem_def)
   done
 
-lemma quorem_div_mod: "0 < b ==> quorem ((a, b), (a div b, a mod b))"
+lemma quorem_div_mod: "b \<noteq> 0 ==> quorem ((a, b), (a div b, a mod b))"
   unfolding quorem_def by simp
 
-lemma quorem_div: "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q"
+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_mod: "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r"
+lemma quorem_mod: "[| quorem((a,b),(q,r));  b \<noteq> 0 |] ==> a mod b = r"
   by (simp add: quorem_div_mod [THEN unique_remainder])
 
 (** A dividend of zero **)
@@ -270,21 +270,19 @@
 (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
 
 lemma quorem_mult1_eq:
-     "[| quorem((b,c),(q,r));  0 < c |]
+     "[| 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)
 
 lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
-  apply (cases "c = 0", simp  add: neq0_conv)
-  using neq0_conv
-  apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
-  done
+apply (cases "c = 0", simp)
+apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
+done
 
 lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
-  apply (cases "c = 0", simp add: neq0_conv)
-  using neq0_conv
-  apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
-  done
+apply (cases "c = 0", simp)
+apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
+done
 
 lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
   apply (rule trans)
@@ -301,23 +299,21 @@
 (** 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));  0 < c |]
+     "[| 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)
 
 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
 lemma div_add1_eq:
-     "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
-  apply (cases "c = 0", simp)
-  using neq0_conv
-  apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
-  done
+  "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
+apply (cases "c = 0", simp)
+apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod)
+done
 
 lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
-  apply (cases "c = 0", simp)
-  using neq0_conv
-  apply (blast intro: quorem_div_mod quorem_div_mod quorem_add1_eq [THEN quorem_mod])
-  done
+apply (cases "c = 0", simp)
+apply (blast intro: quorem_div_mod quorem_add1_eq [THEN quorem_mod])
+done
 
 
 subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Hyperreal/Fact.thy
--- a/src/HOL/Hyperreal/Fact.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Hyperreal/Fact.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -17,60 +17,60 @@
 
 
 lemma fact_gt_zero [simp]: "0 < fact n"
-  by (induct n) auto
+by (induct n) auto
 
 lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
-  by (simp add: neq0_conv)
+by (simp add: neq0_conv)
 
 lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
-  by auto
+by auto
 
 lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
-  by auto
+by auto
 
 lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
-  by simp
+by simp
 
 lemma fact_ge_one [simp]: "1 \<le> fact n"
-  by (induct n) auto
+by (induct n) auto
 
 lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
-  apply (drule le_imp_less_or_eq)
-  apply (auto dest!: less_imp_Suc_add)
-  apply (induct_tac k, auto)
-  done
+apply (drule le_imp_less_or_eq)
+apply (auto dest!: less_imp_Suc_add)
+apply (induct_tac k, auto)
+done
 
 text{*Note that @{term "fact 0 = fact 1"}*}
 lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
-  apply (drule_tac m = m in less_imp_Suc_add, auto)
-  apply (induct_tac k, auto)
-  done
+apply (drule_tac m = m in less_imp_Suc_add, auto)
+apply (induct_tac k, auto)
+done
 
 lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
-  by (auto simp add: positive_imp_inverse_positive)
+by (auto simp add: positive_imp_inverse_positive)
 
 lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
-  by (auto intro: order_less_imp_le)
+by (auto intro: order_less_imp_le)
 
 lemma fact_diff_Suc [rule_format]:
-    "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
-  apply (induct n arbitrary: m)
-  apply auto
-  apply (drule_tac x = "m - 1" in meta_spec, auto)
-  done
+  "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
+apply (induct n arbitrary: m)
+apply auto
+apply (drule_tac x = "m - 1" in meta_spec, auto)
+done
 
 lemma fact_num0 [simp]: "fact 0 = 1"
-  by auto
+by auto
 
 lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
-  by (cases m) auto
+by (cases m) auto
 
 lemma fact_add_num_eq_if:
-    "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
-  by (cases "m + n") auto
+  "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
+by (cases "m + n") auto
 
 lemma fact_add_num_eq_if2:
-    "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
-  by (cases m) auto
+  "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
+by (cases m) auto
 
 end
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -149,14 +149,13 @@
 apply (rule_tac t = a in partition_lhs [THEN subst], assumption)
 apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear)
 apply (frule partition [THEN iffD1], safe)
-using neq0_conv
  apply (blast intro: partition_lt less_le_trans)
 apply (rotate_tac 3)
 apply (drule_tac x = "Suc n" in spec)
 apply (erule impE)
 apply (erule less_imp_le)
-apply (frule partition_rhs, simp only: neq0_conv)
-apply (drule partition_gt, assumption)
+apply (frule partition_rhs)
+apply (drule partition_gt[of _ _ _ 0], arith)
 apply (simp (no_asm_simp))
 done
 
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -114,7 +114,7 @@
 done
 
 lemma Maclaurin:
-   "[| 0 < h; 0 < n; diff 0 = f;
+   "[| 0 < h; n \<noteq> 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,13 +185,11 @@
 done
 
 lemma Maclaurin_objl:
-     "0 < h & 0 < n & 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) +
-              diff n t / real (fact n) * h ^ n)"
+  "0 < h & n\<noteq>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) +
+                  diff n t / real (fact n) * h ^ n)"
 by (blast intro: Maclaurin)
 
 
@@ -220,7 +218,7 @@
 by (blast intro: Maclaurin2)
 
 lemma Maclaurin_minus:
-   "[| h < 0; 0 < n; diff 0 = f;
+   "[| h < 0; n \<noteq> 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 &
@@ -247,7 +245,7 @@
 done
 
 lemma Maclaurin_minus_objl:
-     "(h < 0 & 0 < n & diff 0 = f &
+     "(h < 0 & n \<noteq> 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 &
@@ -263,10 +261,10 @@
 (* not good for PVS sin_approx, cos_approx *)
 
 lemma Maclaurin_bi_le_lemma [rule_format]:
-     "0 < n \<longrightarrow>
-       diff 0 0 =
-       (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
-       diff n 0 * 0 ^ n / real (fact n)"
+  "n\<noteq>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)"
 by (induct "n", auto)
 
 lemma Maclaurin_bi_le:
@@ -278,17 +276,17 @@
               diff n t / real (fact n) * x ^ n"
 apply (case_tac "n = 0", force)
 apply (case_tac "x = 0")
-apply (rule_tac x = 0 in exI)
-apply (force simp add: neq0_conv Maclaurin_bi_le_lemma)
-apply (cut_tac x = x and y = 0 in linorder_less_linear, auto simp add: neq0_conv)
-txt{*Case 1, where @{term "x < 0"}*}
-apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
-apply (simp add: abs_if neq0_conv)
-apply (rule_tac x = t in exI)
-apply (simp add: abs_if)
+ apply (rule_tac x = 0 in exI)
+ apply (force simp add: Maclaurin_bi_le_lemma)
+apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
+ txt{*Case 1, where @{term "x < 0"}*}
+ apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
+  apply (simp add: abs_if)
+ apply (rule_tac x = t in exI)
+ apply (simp add: abs_if)
 txt{*Case 2, where @{term "0 < x"}*}
 apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_objl, safe)
-apply (simp add: abs_if)
+ apply (simp add: abs_if)
 apply (rule_tac x = t in exI)
 apply (simp add: abs_if)
 done
@@ -296,7 +294,7 @@
 lemma Maclaurin_all_lt:
      "[| diff 0 = f;
          \<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
-        x ~= 0; 0 < n
+        x ~= 0; n \<noteq> 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"
@@ -310,7 +308,7 @@
 lemma Maclaurin_all_lt_objl:
      "diff 0 = f &
       (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
-      x ~= 0 & 0 < n
+      x ~= 0 & n \<noteq> 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)"
@@ -318,7 +316,7 @@
 
 lemma Maclaurin_zero [rule_format]:
      "x = (0::real)
-      ==> 0 < n -->
+      ==> n \<noteq> 0 -->
           (\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
           diff 0 0"
 by (induct n, auto)
@@ -328,11 +326,11 @@
       |] ==> \<exists>t. abs t \<le> abs x &
               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
                     (diff n t / real (fact n)) * x ^ n"
-apply (insert linorder_le_less_linear [of n 0])
-apply (erule disjE, force)
+apply(cases "n=0")
+apply (force)
 apply (case_tac "x = 0")
 apply (frule_tac diff = diff and n = n in Maclaurin_zero, assumption)
-apply (drule gr_implies_not0 [THEN not0_implies_Suc])
+apply (drule not0_implies_Suc)
 apply (rule_tac x = 0 in exI, force)
 apply (frule_tac diff = diff and n = n in Maclaurin_all_lt, auto)
 apply (rule_tac x = t in exI, auto)
@@ -348,7 +346,7 @@
 
 subsection{*Version for Exponential Function*}
 
-lemma Maclaurin_exp_lt: "[| x ~= 0; 0 < n |]
+lemma Maclaurin_exp_lt: "[| x ~= 0; n \<noteq> 0 |]
       ==> (\<exists>t. 0 < abs t &
                 abs t < abs x &
                 exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
@@ -375,19 +373,19 @@
 done
 
 lemma mod_exhaust_less_4:
-     "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
+  "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
 by auto
 
 lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
-     "0 < n --> Suc (Suc (2 * n - 2)) = 2*n"
+  "n\<noteq>0 --> Suc (Suc (2 * n - 2)) = 2*n"
 by (induct "n", auto)
 
 lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]:
-     "0 < n --> Suc (Suc (4*n - 2)) = 4*n"
+  "n\<noteq>0 --> Suc (Suc (4*n - 2)) = 4*n"
 by (induct "n", auto)
 
 lemma Suc_mult_two_diff_one [rule_format, simp]:
-      "0 < n --> Suc (2 * n - 1) = 2*n"
+  "n\<noteq>0 --> Suc (2 * n - 1) = 2*n"
 by (induct "n", auto)
 
 
@@ -427,7 +425,7 @@
 
 
 lemma Maclaurin_sin_expansion3:
-     "[| 0 < n; 0 < x |] ==>
+     "[| n \<noteq> 0; 0 < x |] ==>
        \<exists>t. 0 < t & t < x &
        sin x =
        (\<Sum>m=0..<n. (if even m then 0
@@ -493,7 +491,7 @@
 done
 
 lemma Maclaurin_cos_expansion2:
-     "[| 0 < x; 0 < n |] ==>
+     "[| 0 < x; n \<noteq> 0 |] ==>
        \<exists>t. 0 < t & t < x &
        cos x =
        (\<Sum>m=0..<n. (if even m
@@ -512,7 +510,7 @@
 done
 
 lemma Maclaurin_minus_cos_expansion:
-     "[| x < 0; 0 < n |] ==>
+     "[| x < 0; n \<noteq> 0 |] ==>
        \<exists>t. x < t & t < 0 &
        cos x =
        (\<Sum>m=0..<n. (if even m
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -589,15 +589,14 @@
 declare real_mult_zero_disj_iff [simp]
 
 lemma pderiv_aux_iszero [rule_format, simp]:
-    "\<forall>n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p"
+  "\<forall>n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p"
 by (induct "p", auto)
 
 lemma pderiv_aux_iszero_num: "(number_of n :: nat) \<noteq> 0
-      ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) =
+  ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) =
       list_all (%c. c = 0) p)"
-unfolding neq0_conv
-apply (rule_tac n1 = "number_of n" and m1 = 0 in less_imp_Suc_add [THEN exE], force)
-apply (rule_tac n1 = "0 + x" in pderiv_aux_iszero [THEN subst])
+apply(drule  not0_implies_Suc, clarify)
+apply (rule_tac n1 = "m" in pderiv_aux_iszero [THEN subst])
 apply (simp (no_asm_simp) del: pderiv_aux_iszero)
 done
 
@@ -783,7 +782,7 @@
 declare pexp_one [simp]
 
 lemma lemma_order_root [rule_format]:
-     "\<forall>p a. 0 < n & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
+     "\<forall>p a. n \<noteq> 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)
@@ -794,8 +793,7 @@
 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 neq0_conv del: pmult_Cons, blast)
-using neq0_conv 
+apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
 apply (blast intro: lemma_order_root)
 done
 
@@ -845,7 +843,7 @@
 
 (* FIXME: too too long! *)
 lemma lemma_order_pderiv [rule_format]:
-     "\<forall>p q a. 0 < n &
+     "\<forall>p q a. n \<noteq> 0 &
        poly (pderiv p) \<noteq> poly [] &
        poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q
        --> n = Suc (order a (pderiv p))"
@@ -876,7 +874,7 @@
           (poly qa xa + - poly (pderiv q) xa) *
           (poly ([- a, 1] %^ n) xa *
            ((- a + xa) * (inverse (real (Suc n)) * real (Suc n))))")
-apply (simp only: mult_ac)  
+apply (simp only: mult_ac)
 apply (rotate_tac 2)
 apply (drule_tac x = xa in spec)
 apply (simp add: left_distrib mult_ac del: pmult_Cons)
@@ -885,7 +883,7 @@
 lemma order_pderiv: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |]
       ==> (order a p = Suc (order a (pderiv p)))"
 apply (case_tac "poly p = poly []")
-apply (auto simp add: neq0_conv  dest: pderiv_zero)
+apply (auto dest: pderiv_zero)
 apply (drule_tac a = a and p = p in order_decomp)
 apply (blast intro: lemma_order_pderiv)
 done
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Hyperreal/Taylor.thy
--- a/src/HOL/Hyperreal/Taylor.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Hyperreal/Taylor.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -15,7 +15,7 @@
 *}
 
 lemma taylor_up: 
-  assumes INIT: "0 < n" "diff 0 = f"
+  assumes INIT: "n\<noteq>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,7 +24,7 @@
 proof -
   from INTERV have "0 < b-c" by arith
   moreover 
-  from INIT have "0<n" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
+  from INIT have "n\<noteq>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)"  
   proof (intro strip)
@@ -57,7 +57,7 @@
 qed
 
 lemma taylor_down:
-  assumes INIT: "0 < n" "diff 0 = f"
+  assumes INIT: "n\<noteq>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 "0<n" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
+  from INIT have "n\<noteq>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: "0 < n" "diff 0 = f"
+  assumes INIT: "n\<noteq>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 b933700f0384 -r 3d4953e88449 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/IntDiv.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -1316,34 +1316,34 @@
 
 
 theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
-  apply (simp split add: split_nat)
-  apply (rule iffI)
-  apply (erule exE)
-  apply (rule_tac x = "int x" in exI)
-  apply simp
-  apply (erule exE)
-  apply (rule_tac x = "nat x" in exI)
-  apply (erule conjE)
-  apply (erule_tac x = "nat x" in allE)
-  apply simp
-  done
+apply (simp split add: split_nat)
+apply (rule iffI)
+apply (erule exE)
+apply (rule_tac x = "int x" in exI)
+apply simp
+apply (erule exE)
+apply (rule_tac x = "nat x" in exI)
+apply (erule conjE)
+apply (erule_tac x = "nat x" in allE)
+apply simp
+done
 
 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
-  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
+apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
     nat_0_le cong add: conj_cong)
-  apply (rule iffI)
-  apply iprover
-  apply (erule exE)
-  apply (case_tac "x=0")
-  apply (rule_tac x=0 in exI)
-  apply simp
-  apply (case_tac "0 \<le> k")
-  apply iprover
-  apply (simp add: neq0_conv linorder_not_le)
-  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
-  apply assumption
-  apply (simp add: mult_ac)
-  done
+apply (rule iffI)
+apply iprover
+apply (erule exE)
+apply (case_tac "x=0")
+apply (rule_tac x=0 in exI)
+apply simp
+apply (case_tac "0 \<le> k")
+apply iprover
+apply (simp add: neq0_conv linorder_not_le)
+apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
+apply assumption
+apply (simp add: mult_ac)
+done
 
 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
 proof
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Library/Binomial.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -21,50 +21,50 @@
                  (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
 
 lemma binomial_n_0 [simp]: "(n choose 0) = 1"
-  by (cases n) simp_all
+by (cases n) simp_all
 
 lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
-  by simp
+by simp
 
 lemma binomial_Suc_Suc [simp]:
-    "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
-  by simp
+  "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
+by simp
 
 lemma binomial_eq_0: "!!k. n < k ==> (n choose k) = 0"
-  by (induct n) auto
+by (induct n) auto
 
 declare binomial_0 [simp del] binomial_Suc [simp del]
 
 lemma binomial_n_n [simp]: "(n choose n) = 1"
-  by (induct n) (simp_all add: binomial_eq_0)
+by (induct n) (simp_all add: binomial_eq_0)
 
 lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n"
-  by (induct n) simp_all
+by (induct n) simp_all
 
 lemma binomial_1 [simp]: "(n choose Suc 0) = n"
-  by (induct n) simp_all
+by (induct n) simp_all
 
-lemma zero_less_binomial: "k \<le> n ==> 0 < (n choose k)"
-  by (induct n k rule: diff_induct) simp_all
+lemma zero_less_binomial: "k \<le> n ==> (n choose k) \<noteq> 0"
+by (induct n k rule: diff_induct) simp_all
 
 lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
-  apply (safe intro!: binomial_eq_0)
-  apply (erule contrapos_pp)
-  apply (simp add: neq0_conv zero_less_binomial)
-  done
+apply (safe intro!: binomial_eq_0)
+apply (erule contrapos_pp)
+apply (simp add: zero_less_binomial)
+done
 
-lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)"
-  by (simp add: neq0_conv  linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
+lemma zero_less_binomial_iff: "(n choose k \<noteq> 0) = (k\<le>n)"
+by (simp add: linorder_not_less binomial_eq_0_iff)
 
 (*Might be more useful if re-oriented*)
 lemma Suc_times_binomial_eq:
-    "!!k. k \<le> n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
-  apply (induct n)
-  apply (simp add: binomial_0)
-  apply (case_tac k)
-  apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
+  "!!k. k \<le> n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
+apply (induct n)
+apply (simp add: binomial_0)
+apply (case_tac k)
+apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
     binomial_eq_0)
-  done
+done
 
 text{*This is the well-known version, but it's harder to use because of the
   need to reason about division.*}
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Library/Multiset.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -11,7 +11,7 @@
 
 subsection {* The type of multisets *}
 
-typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}"
+typedef 'a multiset = "{f::'a => nat. finite {x . f x \<noteq> 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 == 0 < count M a"
+  "a :# M == count M a \<noteq> 0"
 
 syntax
   "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
@@ -300,7 +300,7 @@
 lemma rep_multiset_induct_aux:
   assumes 1: "P (\<lambda>a. (0::nat))"
     and 2: "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))"
-  shows "\<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
+  shows "\<forall>f. f \<in> multiset --> setsum f {x. f x \<noteq> 0} = n --> P f"
   apply (unfold multiset_def)
   apply (induct_tac n, simp, clarify)
    apply (subgoal_tac "f = (\<lambda>a.0)")
@@ -309,7 +309,7 @@
    apply (rule ext, force, clarify)
   apply (frule setsum_SucD, clarify)
   apply (rename_tac a)
-  apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}")
+  apply (subgoal_tac "finite {x. (f (a := f a - 1)) x \<noteq> 0}")
    prefer 2
    apply (rule finite_subset)
     prefer 2
@@ -323,10 +323,10 @@
    apply (erule ssubst, rule 2 [unfolded multiset_def], blast)
   apply (erule allE, erule impE, erule_tac [2] mp, blast)
   apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
-  apply (subgoal_tac "{x. x \<noteq> a --> 0 < f x} = {x. 0 < f x}")
+  apply (subgoal_tac "{x. x \<noteq> a --> f x \<noteq> 0} = {x. f x \<noteq> 0}")
    prefer 2
    apply blast
-  apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x} - {a}")
+  apply (subgoal_tac "{x. x \<noteq> a \<and> f x \<noteq> 0} = {x. f x \<noteq> 0} - {a}")
    prefer 2
    apply blast
   apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong)
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -51,132 +51,132 @@
 subsection "Constructors"
 
 lemma Fin_0: "Fin 0 = 0"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 
 subsection "Ordering relations"
 
 lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)"
-  by (simp add: inat_defs split:inat_splits, arith)
+by (simp add: inat_defs split:inat_splits, arith)
 
 lemma iless_not_refl [simp]: "\<not> n < (n::inat)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma Infty_eq [simp]: "(n < \<infinity>) = (n \<noteq> \<infinity>)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
-  by (simp add: neq0_conv inat_defs split:inat_splits)
+by (fastsimp simp: inat_defs split:inat_splits)
 
 lemma i0_iless_iSuc [simp]: "0 < iSuc n"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma not_ilessi0 [simp]: "\<not> n < (0::inat)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma iSuc_mono [simp]: "(iSuc n < iSuc m) = (n < m)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 
 
 lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
-  by (simp add: inat_defs split:inat_splits, arith)
+by (simp add: inat_defs split:inat_splits, arith)
 
 lemma ile_refl [simp]: "n \<le> (n::inat)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma Infty_ub [simp]: "n \<le> \<infinity>"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma i0_lb [simp]: "(0::inat) \<le> n"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)"
-  by (simp add: inat_defs split:inat_splits, arith)
+by (simp add: inat_defs split:inat_splits, arith)
 
 lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma ileI1: "m < n ==> iSuc m \<le> n"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)"
-  by (simp add: inat_defs split:inat_splits, arith)
+by (simp add: inat_defs split:inat_splits, arith)
 
 lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)"
-  by (simp add: inat_defs split:inat_splits, arith)
+by (simp add: inat_defs split:inat_splits, arith)
 
 lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma ile_iSuc [simp]: "n \<le> iSuc n"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k"
-  by (simp add: inat_defs split:inat_splits)
+by (simp add: inat_defs split:inat_splits)
 
 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
-  apply (induct_tac k)
-   apply (simp (no_asm) only: Fin_0)
-   apply (fast intro: ile_iless_trans i0_lb)
-  apply (erule exE)
-  apply (drule spec)
-  apply (erule exE)
-  apply (drule ileI1)
-  apply (rule iSuc_Fin [THEN subst])
-  apply (rule exI)
-  apply (erule (1) ile_iless_trans)
-  done
+apply (induct_tac k)
+ apply (simp (no_asm) only: Fin_0)
+ apply (fast intro: ile_iless_trans i0_lb)
+apply (erule exE)
+apply (drule spec)
+apply (erule exE)
+apply (drule ileI1)
+apply (rule iSuc_Fin [THEN subst])
+apply (rule exI)
+apply (erule (1) ile_iless_trans)
+done
 
 end
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Library/Parity.thy
--- a/src/HOL/Library/Parity.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Library/Parity.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -222,7 +222,7 @@
   apply (subst power_add)
   apply (subst zero_le_mult_iff)
   apply auto
-  apply (subgoal_tac "x = 0 & 0 < y")
+  apply (subgoal_tac "x = 0 & y \<noteq> 0")
   apply (erule conjE, assumption)
   apply (subst power_eq_0_iff [symmetric])
   apply (subgoal_tac "0 <= x^y * x^y")
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Library/Word.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -412,21 +412,22 @@
   thus ?thesis ..
 qed
 
-lemma nat_to_bv_non0 [simp]: "0 < n ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then \<zero> else \<one>]"
+lemma nat_to_bv_non0 [simp]: "n\<noteq>0 ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then \<zero> else \<one>]"
 proof -
-  assume [simp]: "0 < n"
+  assume [simp]: "n\<noteq>0"
   show ?thesis
     apply (subst nat_to_bv_def [of n])
     apply (simp only: nat_to_bv_helper.simps [of n])
     apply (subst unfold_nat_to_bv_helper)
     using prems
-    apply (simp add: neq0_conv)
+    apply (simp)
     apply (subst nat_to_bv_def [of "n div 2"])
     apply auto
     done
 qed
 
-lemma bv_to_nat_dist_append: "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
+lemma bv_to_nat_dist_append:
+  "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
 proof -
   have "\<forall>l2. bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
   proof (induct l1,simp_all)
@@ -457,8 +458,7 @@
   assume ind: "!!j. j < n \<Longrightarrow> bv_to_nat (nat_to_bv j) = j"
   show "bv_to_nat (nat_to_bv n) = n"
   proof (rule n_div_2_cases [of n])
-    assume "n = 0"
-    then show ?thesis by simp
+    assume "n = 0" then show ?thesis by simp
   next
     assume nn: "n div 2 < n"
     assume n0: "0 < n"
@@ -474,16 +474,14 @@
       apply (fold nat_to_bv_def)
       apply (simp add: ind' split del: split_if)
       apply (cases "n mod 2 = 0")
-      proof (simp_all add: neq0_conv)
+      proof (simp_all)
         assume "n mod 2 = 0"
         with mod_div_equality [of n 2]
-        show "n div 2 * 2 = n"
-          by simp
+        show "n div 2 * 2 = n" by simp
       next
-        assume "n mod 2 = Suc 0"
+        assume "n mod 2 \<noteq> 0"
         with mod_div_equality [of n 2]
-        show "Suc (n div 2 * 2) = n"
-          by simp
+        show "Suc (n div 2 * 2) = n" by arith
       qed
   qed
 qed
@@ -536,29 +534,30 @@
 lemmas [simp del] = nat_to_bv_non0
 
 lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) \<le> length w"
-  by (subst norm_unsigned_def,rule rem_initial_length)
+by (subst norm_unsigned_def,rule rem_initial_length)
 
-lemma norm_unsigned_equal: "length (norm_unsigned w) = length w ==> norm_unsigned w = w"
-  by (simp add: norm_unsigned_def,rule rem_initial_equal)
+lemma norm_unsigned_equal:
+  "length (norm_unsigned w) = length w ==> norm_unsigned w = w"
+by (simp add: norm_unsigned_def,rule rem_initial_equal)
 
 lemma bv_extend_norm_unsigned: "bv_extend (length w) \<zero> (norm_unsigned w) = w"
-  by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)
+by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)
 
 lemma norm_unsigned_append1 [simp]:
-    "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
-  by (simp add: norm_unsigned_def,rule rem_initial_append1)
+  "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
+by (simp add: norm_unsigned_def,rule rem_initial_append1)
 
 lemma norm_unsigned_append2 [simp]:
-    "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
-  by (simp add: norm_unsigned_def,rule rem_initial_append2)
+  "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
+by (simp add: norm_unsigned_def,rule rem_initial_append2)
 
 lemma bv_to_nat_zero_imp_empty:
-    "bv_to_nat w = 0 \<Longrightarrow> norm_unsigned w = []"
-  by (atomize (full), induct w rule: bit_list_induct) (simp_all add: neq0_conv)
+  "bv_to_nat w = 0 \<Longrightarrow> norm_unsigned w = []"
+by (atomize (full), induct w rule: bit_list_induct) simp_all
 
 lemma bv_to_nat_nzero_imp_nempty:
   "bv_to_nat w \<noteq> 0 \<Longrightarrow> norm_unsigned w \<noteq> []"
-  by (induct w rule: bit_list_induct) simp_all
+by (induct w rule: bit_list_induct) simp_all
 
 lemma nat_helper1:
   assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
@@ -1855,8 +1854,8 @@
   qed
 qed
 
-lemma bv_msb_one: "bv_msb w = \<one> ==> 0 < bv_to_nat w"
-  by (cases w) simp_all
+lemma bv_msb_one: "bv_msb w = \<one> ==> bv_to_nat w \<noteq> 0"
+by (cases w) simp_all
 
 lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2"
 proof -
@@ -2064,7 +2063,7 @@
   by (simp add: length_nat_def Least_equality)
 
 lemma length_nat_non0:
-  assumes n0: "0 < n"
+  assumes n0: "n \<noteq> 0"
   shows       "length_nat n = Suc (length_nat (n div 2))"
   apply (simp add: length_nat [symmetric])
   apply (subst nat_to_bv_non0 [of n])
diff -r b933700f0384 -r 3d4953e88449 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/List.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -950,9 +950,7 @@
   proof (cases)
     assume "p x"
     hence eq: "?S' = insert 0 (Suc ` ?S)"
-      apply (auto simp add:  nth_Cons image_def neq0_conv split:nat.split elim:lessE)
-      apply (rule_tac x="xa - 1" in exI, auto)
-      done
+      by(auto simp: nth_Cons image_def split:nat.split dest:not0_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
@@ -2460,12 +2458,7 @@
 
 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
 apply(induct xs arbitrary: I)
- apply simp
-apply(auto simp add: neq0_conv sublist_Cons nth_Cons split:nat.split elim: lessE)
- apply(erule lessE)
-  apply auto
-apply(erule lessE)
-apply auto
+apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: not0_implies_Suc)
 done
 
 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Nat.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -508,10 +508,7 @@
   by (fast intro: not0_implies_Suc)
 
 lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
-  apply (rule iffI)
-  apply (rule ccontr)
-  apply (simp_all add: neq0_conv)
-  done
+using neq0_conv by blast
 
 lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
   by (induct m') simp_all
@@ -603,8 +600,8 @@
   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 < n ==> Suc (n - Suc 0) = n"
-  by (simp add: neq0_conv split add: nat.split)
+lemma Suc_pred [simp]: "0 \<noteq> n ==> Suc (n - Suc 0) = n"
+by (simp split add: nat.split)
 
 declare diff_Suc [simp del, code del]
 
@@ -658,8 +655,8 @@
 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)
 
-lemma add_gr_0 [iff]: "!!m::nat. (0 < m + n) = (0 < m | 0 < n)"
-  by (simp del: neq0_conv add: neq0_conv [symmetric])
+lemma add_gr_0 [iff]: "!!m::nat. (m + n \<noteq> 0) = (m\<noteq>0 | n\<noteq>0)"
+by simp
 
 lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0"
   apply (drule add_0_right [THEN ssubst])
@@ -743,11 +740,11 @@
   done
 
 text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
-lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
-  apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
-  apply (induct_tac x)
-  apply (simp_all add: add_less_mono)
-  done
+lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j"
+apply(auto simp: gr0_conv_Suc)
+apply (induct_tac m)
+apply (simp_all add: add_less_mono)
+done
 
 
 text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
@@ -1084,9 +1081,9 @@
 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 (drule mult_less_mono1, assumption, simp)+
-  done
+apply (cut_tac less_linear, safe, auto simp add: neq0_conv)
+apply (drule mult_less_mono1, assumption, simp)+
+done
 
 lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
 by (simp add: mult_commute [of k])
@@ -1105,8 +1102,8 @@
   apply (drule sym)
   apply (rule disjCI)
   apply (rule nat_less_cases, erule_tac [2] _)
-  apply (fastsimp simp add: neq0_conv elim!: less_SucE)
-  apply (fastsimp simp add: neq0_conv dest: mult_less_mono2)
+  apply (fastsimp elim!: less_SucE)
+  apply (auto simp add: neq0_conv dest: mult_less_mono2)
   done
 
 
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Power.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -140,16 +140,13 @@
 done
 
 lemma power_eq_0_iff [simp]:
-     "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & 0<n)"
+  "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n\<noteq>0)"
 apply (induct "n")
 apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
 done
 
-lemma field_power_eq_0_iff:
-     "(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)"
-by simp (* TODO: delete *)
-
-lemma field_power_not_zero: "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
+lemma field_power_not_zero:
+  "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
 by force
 
 lemma nonzero_power_inverse:
@@ -279,26 +276,26 @@
                  order_less_imp_le)
 done
 
-lemma power_increasing_iff [simp]: 
-     "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
-  by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le) 
+lemma power_increasing_iff [simp]:
+  "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
+by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le) 
 
 lemma power_strict_increasing_iff [simp]:
-     "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
-  by (blast intro: power_less_imp_less_exp power_strict_increasing) 
+  "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
+by (blast intro: power_less_imp_less_exp power_strict_increasing) 
 
 lemma power_le_imp_le_base:
-  assumes le: "a ^ Suc n \<le> b ^ Suc n"
-      and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
-  shows "a \<le> b"
- proof (rule ccontr)
-   assume "~ a \<le> b"
-   then have "b < a" by (simp only: linorder_not_le)
-   then have "b ^ Suc n < a ^ Suc n"
-     by (simp only: prems power_strict_mono)
-   from le and this show "False"
-      by (simp add: linorder_not_less [symmetric])
- qed
+assumes le: "a ^ Suc n \<le> b ^ Suc n"
+    and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
+shows "a \<le> b"
+proof (rule ccontr)
+  assume "~ a \<le> b"
+  then have "b < a" by (simp only: linorder_not_le)
+  then have "b ^ Suc n < a ^ Suc n"
+    by (simp only: prems power_strict_mono)
+  from le and this show "False"
+    by (simp add: linorder_not_less [symmetric])
+qed
 
 lemma power_less_imp_less_base:
   fixes a b :: "'a::{ordered_semidom,recpower}"
@@ -345,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]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
+lemma nat_zero_less_power_iff [simp]: "(x^n = 0) = (x = (0::nat) & n\<noteq>0)"
 by (induct "n", auto)
 
 text{*Valid for the naturals, but what if @{text"0<i<1"}?
@@ -393,7 +390,7 @@
 val power_mono = thm"power_mono";
 val power_strict_mono = thm"power_strict_mono";
 val power_eq_0_iff = thm"power_eq_0_iff";
-val field_power_eq_0_iff = thm"field_power_eq_0_iff";
+val field_power_eq_0_iff = thm"power_eq_0_iff";
 val field_power_not_zero = thm"field_power_not_zero";
 val power_inverse = thm"power_inverse";
 val nonzero_power_divide = thm"nonzero_power_divide";
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -794,24 +794,24 @@
 
 lemma real_of_nat_div2:
   "0 <= real (n::nat) / real (x) - real (n div x)"
-  apply(case_tac "x = 0")
-  apply (simp add: neq0_conv)
-  apply (simp add: neq0_conv  compare_rls)
-  apply (subst real_of_nat_div_aux)
-  apply assumption
-  apply simp
-  apply (subst zero_le_divide_iff)
-  apply simp
+apply(case_tac "x = 0")
+ apply (simp)
+apply (simp add: compare_rls)
+apply (subst real_of_nat_div_aux)
+ apply simp
+apply simp
+apply (subst zero_le_divide_iff)
+apply simp
 done
 
 lemma real_of_nat_div3:
   "real (n::nat) / real (x) - real (n div x) <= 1"
-  apply(case_tac "x = 0")
-  apply (simp add: neq0_conv )
-  apply (simp add: compare_rls neq0_conv )
-  apply (subst real_of_nat_div_aux)
-  apply assumption
-  apply simp
+apply(case_tac "x = 0")
+apply (simp)
+apply (simp add: compare_rls)
+apply (subst real_of_nat_div_aux)
+ apply simp
+apply simp
 done
 
 lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x" 
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -1099,20 +1099,19 @@
   done
 
 lemma bin_rsplit_aux_len_le [rule_format] :
-  "ALL ws m. n > 0 --> ws = bin_rsplit_aux (n, bs, nw, w) --> 
+  "ALL ws m. n \<noteq> 0 --> ws = bin_rsplit_aux (n, bs, nw, w) --> 
     (length ws <= m) = (nw + length bs * n <= m * n)"
   apply (rule_tac u=n and v=bs and w=nw and x=w in bin_rsplit_aux.induct)
   apply (subst bin_rsplit_aux.simps)
-  apply (clarsimp simp: Let_def neq0_conv split: ls_splits )
-  apply (erule lrlem)
+  apply (simp add:lrlem Let_def split: ls_splits )
   done
 
 lemma bin_rsplit_len_le: 
-  "n > 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)"
+  "n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)"
   unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le)
  
 lemma bin_rsplit_aux_len [rule_format] :
-  "0 < n --> length (bin_rsplit_aux (n, cs, nw, w)) = 
+  "n\<noteq>0 --> length (bin_rsplit_aux (n, cs, nw, w)) = 
     (nw + n - 1) div n + length cs"
   apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct)
   apply (subst bin_rsplit_aux.simps)
@@ -1126,11 +1125,11 @@
   done
 
 lemma bin_rsplit_len: 
-  "0 < n ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
+  "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
   unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len)
 
 lemma bin_rsplit_aux_len_indep [rule_format] :
-  "0 < n ==> (ALL v bs. length bs = length cs --> 
+  "n\<noteq>0 ==> (ALL v bs. length bs = length cs --> 
     length (bin_rsplit_aux (n, bs, nw, v)) = 
     length (bin_rsplit_aux (n, cs, nw, w)))"
   apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct)
@@ -1148,7 +1147,7 @@
   done
 
 lemma bin_rsplit_len_indep: 
-  "0 < n ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
+  "n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
   apply (unfold bin_rsplit_def)
   apply (erule bin_rsplit_aux_len_indep)
   apply (rule refl)
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -457,7 +457,7 @@
   we get a version for when the word length is given literally *)
 
 lemmas nat_non0_gr = 
-  trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] neq0_conv, standard]
+  trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl, standard]
 
 lemmas bintrunc_pred_simps [simp] = 
   bintrunc_minus_simps [of "number_of bin", simplified nobm1, standard]
diff -r b933700f0384 -r 3d4953e88449 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Word/WordArith.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -117,28 +117,28 @@
 lemmas unat_eq_zero = unat_0_iff
 
 lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"
-  by (simp add : neq0_conv unat_0_iff [symmetric])
+by (auto simp: unat_0_iff [symmetric])
 
 lemma ucast_0 [simp] : "ucast 0 = 0"
-  unfolding ucast_def
-  by simp (simp add: word_0_wi)
+unfolding ucast_def
+by simp (simp add: word_0_wi)
 
 lemma sint_0 [simp] : "sint 0 = 0"
-  unfolding sint_uint
-  by (simp add: Pls_def [symmetric])
+unfolding sint_uint
+by (simp add: Pls_def [symmetric])
 
 lemma scast_0 [simp] : "scast 0 = 0"
-  apply (unfold scast_def)
-  apply simp
-  apply (simp add: word_0_wi)
-  done
+apply (unfold scast_def)
+apply simp
+apply (simp add: word_0_wi)
+done
 
 lemma sint_n1 [simp] : "sint -1 = -1"
-  apply (unfold word_m1_wi_Min)
-  apply (simp add: word_sbin.eq_norm)
-  apply (unfold Min_def number_of_eq)
-  apply simp
-  done
+apply (unfold word_m1_wi_Min)
+apply (simp add: word_sbin.eq_norm)
+apply (unfold Min_def number_of_eq)
+apply simp
+done
 
 lemma scast_n1 [simp] : "scast -1 = -1"
   apply (unfold scast_def sint_n1)
@@ -1242,15 +1242,15 @@
 lemmas card_word = trans [OF card_eq card_lessThan', standard]
 
 lemma finite_word_UNIV: "finite (UNIV :: 'a :: len word set)"
-  apply (rule contrapos_np)
-   prefer 2
-   apply (erule card_infinite)
-  apply (simp add : card_word neq0_conv)
-  done
+apply (rule contrapos_np)
+ prefer 2
+ apply (erule card_infinite)
+apply (simp add: card_word)
+done
 
 lemma card_word_size: 
   "card (UNIV :: 'a :: len word set) = (2 ^ size (x :: 'a word))"
-  unfolding word_size by (rule card_word)
+unfolding word_size by (rule card_word)
 
 end 
 
diff -r b933700f0384 -r 3d4953e88449 src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -63,7 +63,7 @@
   "fmsize (NDvd i t) = 2"
   "fmsize p = 1"
   (* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p > 0"	
+lemma fmsize_pos: "fmsize p \<noteq> 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)
+(hints simp add: fmsize_pos neq0_conv[symmetric])
 lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
 by (induct p arbitrary: bs rule: prep.induct, auto)
 
@@ -188,14 +188,12 @@
 | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
 
 lemma numsubst0_I:
-  shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
-  by (induct t rule: numsubst0.induct,auto simp add: gr0_conv_Suc neq0_conv)
+  "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
+by (induct t rule: numsubst0.induct,auto dest: not0_implies_Suc)
 
 lemma numsubst0_I':
-  assumes nb: "numbound0 a"
-  shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
-  using nb
-  by (induct t rule: numsubst0.induct, auto simp add: neq0_conv gr0_conv_Suc numbound0_I[where b="b" and b'="b'"])
+  "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'"])
 
 primrec
   "subst0 t T = T"