went back to >0
authornipkow
Tue Oct 23 23:27:23 2007 +0200 (2007-10-23)
changeset 25162ad4d5365d9d8
parent 25161 aa8474398030
child 25163 f737a88a3248
went back to >0
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Complex/ex/HarmonicSeries.thy
src/HOL/Complex/ex/MIR.thy
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/Divides.thy
src/HOL/Finite_Set.thy
src/HOL/Hyperreal/Fact.thy
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/Hyperreal/Taylor.thy
src/HOL/IntArith.thy
src/HOL/Library/Binomial.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Parity.thy
src/HOL/Library/Word.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Power.thy
src/HOL/Real/RComplete.thy
src/HOL/Real/RealDef.thy
src/HOL/ex/Reflected_Presburger.thy
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Tue Oct 23 22:48:25 2007 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Tue Oct 23 23:27:23 2007 +0200
     1.3 @@ -100,7 +100,7 @@
     1.4  done
     1.5  
     1.6  (*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
     1.7 -lemma power_dvd_bound: "[|p^n dvd a;  Suc 0 < p;  a \<noteq> 0|] ==> n < a"
     1.8 +lemma power_dvd_bound: "[|p^n dvd a;  Suc 0 < p;  a > 0|] ==> n < a"
     1.9  apply (drule dvd_imp_le)
    1.10  apply (drule_tac [2] n = n in Suc_le_power, auto)
    1.11  done
    1.12 @@ -115,7 +115,7 @@
    1.13  apply (blast dest: prime_imp_one_less power_dvd_bound)
    1.14  done
    1.15  
    1.16 -lemma power_exponent_dvd: "s\<noteq>0 ==> (p ^ exponent p s) dvd s"
    1.17 +lemma power_exponent_dvd: "s>0 ==> (p ^ exponent p s) dvd s"
    1.18  apply (simp add: exponent_def)
    1.19  apply clarify
    1.20  apply (rule_tac k = 0 in GreatestI)
    1.21 @@ -145,7 +145,7 @@
    1.22  
    1.23  
    1.24  (* exponent_mult_add, easy inclusion.  Could weaken p \<in> prime to Suc 0 < p *)
    1.25 -lemma exponent_mult_add1: "[| a \<noteq> 0; b \<noteq> 0 |]
    1.26 +lemma exponent_mult_add1: "[| a > 0; b > 0 |]
    1.27    ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
    1.28  apply (case_tac "prime p")
    1.29  apply (rule exponent_ge)
    1.30 @@ -154,7 +154,7 @@
    1.31  done
    1.32  
    1.33  (* exponent_mult_add, opposite inclusion *)
    1.34 -lemma exponent_mult_add2: "[| a \<noteq> 0; b \<noteq> 0 |]  
    1.35 +lemma exponent_mult_add2: "[| a > 0; b > 0 |]  
    1.36    ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
    1.37  apply (case_tac "prime p")
    1.38  apply (rule leI, clarify)
    1.39 @@ -168,7 +168,7 @@
    1.40  apply (blast dest: power_Suc_exponent_Not_dvd)
    1.41  done
    1.42  
    1.43 -lemma exponent_mult_add: "[| a \<noteq> 0; b \<noteq> 0 |]
    1.44 +lemma exponent_mult_add: "[| a > 0; b > 0 |]
    1.45     ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
    1.46  by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym)
    1.47  
    1.48 @@ -188,14 +188,14 @@
    1.49  
    1.50  subsection{*Main Combinatorial Argument*}
    1.51  
    1.52 -lemma le_extend_mult: "[| c \<noteq> 0; a <= b |] ==> a <= b * (c::nat)"
    1.53 +lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)"
    1.54  apply (rule_tac P = "%x. x <= b * c" in subst)
    1.55  apply (rule mult_1_right)
    1.56  apply (rule mult_le_mono, auto)
    1.57  done
    1.58  
    1.59  lemma p_fac_forw_lemma:
    1.60 -  "[| (m::nat) \<noteq> 0; k \<noteq> 0; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
    1.61 +  "[| (m::nat) > 0; k > 0; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
    1.62  apply (rule notnotD)
    1.63  apply (rule notI)
    1.64  apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
    1.65 @@ -205,7 +205,7 @@
    1.66  apply(metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less neq0_conv)
    1.67  done
    1.68  
    1.69 -lemma p_fac_forw: "[| (m::nat) \<noteq> 0; k\<noteq>0; k < p^a; (p^r) dvd (p^a)* m - k |]  
    1.70 +lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]  
    1.71    ==> (p^r) dvd (p^a) - k"
    1.72  apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto)
    1.73  apply (subgoal_tac "p^r dvd p^a*m")
    1.74 @@ -213,15 +213,15 @@
    1.75  apply (drule dvd_diffD1)
    1.76    apply assumption
    1.77   prefer 2 apply (blast intro: dvd_diff)
    1.78 -apply (drule not0_implies_Suc, auto)
    1.79 +apply (drule gr0_implies_Suc, auto)
    1.80  done
    1.81  
    1.82  
    1.83  lemma r_le_a_forw:
    1.84 -  "[| (k::nat) \<noteq> 0; k < p^a; p\<noteq>0; (p^r) dvd (p^a) - k |] ==> r <= a"
    1.85 +  "[| (k::nat) > 0; k < p^a; p>0; (p^r) dvd (p^a) - k |] ==> r <= a"
    1.86  by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
    1.87  
    1.88 -lemma p_fac_backw: "[| m\<noteq>0; k\<noteq>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]  
    1.89 +lemma p_fac_backw: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]  
    1.90    ==> (p^r) dvd (p^a)*m - k"
    1.91  apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
    1.92  apply (subgoal_tac "p^r dvd p^a*m")
    1.93 @@ -232,7 +232,7 @@
    1.94  apply (drule less_imp_Suc_add, auto)
    1.95  done
    1.96  
    1.97 -lemma exponent_p_a_m_k_equation: "[| m\<noteq>0; k\<noteq>0; (p::nat)\<noteq>0;  k < p^a |]  
    1.98 +lemma exponent_p_a_m_k_equation: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a |]  
    1.99    ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
   1.100  apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
   1.101  done
   1.102 @@ -249,7 +249,7 @@
   1.103  apply (induct_tac "k")
   1.104  apply (simp (no_asm))
   1.105  (*induction step*)
   1.106 -apply (subgoal_tac "(Suc (j+n) choose Suc n) \<noteq> 0")
   1.107 +apply (subgoal_tac "(Suc (j+n) choose Suc n) > 0")
   1.108   prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
   1.109  apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) = 
   1.110                      exponent p (Suc n)")
   1.111 @@ -278,7 +278,7 @@
   1.112  
   1.113  
   1.114  lemma const_p_fac_right:
   1.115 -  "m\<noteq>0 ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
   1.116 +  "m>0 ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
   1.117  apply (case_tac "prime p")
   1.118   prefer 2 apply simp 
   1.119  apply (frule_tac a = a in zero_less_prime_power)
   1.120 @@ -296,7 +296,7 @@
   1.121  done
   1.122  
   1.123  lemma const_p_fac:
   1.124 -  "m\<noteq>0 ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
   1.125 +  "m>0 ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
   1.126  apply (case_tac "prime p")
   1.127   prefer 2 apply simp 
   1.128  apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
     2.1 --- a/src/HOL/Algebra/Sylow.thy	Tue Oct 23 22:48:25 2007 +0200
     2.2 +++ b/src/HOL/Algebra/Sylow.thy	Tue Oct 23 23:27:23 2007 +0200
     2.3 @@ -126,7 +126,7 @@
     2.4  apply (blast intro: one_closed zero_less_card_empty)
     2.5  done
     2.6  
     2.7 -lemma (in sylow) zero_less_m: "m \<noteq> 0"
     2.8 +lemma (in sylow) zero_less_m: "m > 0"
     2.9  apply (cut_tac zero_less_o_G)
    2.10  apply (simp add: order_G)
    2.11  done
    2.12 @@ -134,7 +134,7 @@
    2.13  lemma (in sylow) card_calM: "card(calM) = (p^a) * m choose p^a"
    2.14  by (simp add: calM_def n_subsets order_G [symmetric] order_def)
    2.15  
    2.16 -lemma (in sylow) zero_less_card_calM: "card calM \<noteq> 0"
    2.17 +lemma (in sylow) zero_less_card_calM: "card calM > 0"
    2.18  by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)
    2.19  
    2.20  lemma (in sylow) max_p_div_calM:
     3.1 --- a/src/HOL/Complex/ex/HarmonicSeries.thy	Tue Oct 23 22:48:25 2007 +0200
     3.2 +++ b/src/HOL/Complex/ex/HarmonicSeries.thy	Tue Oct 23 23:27:23 2007 +0200
     3.3 @@ -80,7 +80,7 @@
     3.4        then have
     3.5          "inverse (real x) = 1 / (real x)"
     3.6          by (rule nonzero_inverse_eq_divide)
     3.7 -      moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef neq0_conv)
     3.8 +      moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef)
     3.9        then have
    3.10          "inverse (real tm) = 1 / (real tm)"
    3.11          by (rule nonzero_inverse_eq_divide)
     4.1 --- a/src/HOL/Complex/ex/MIR.thy	Tue Oct 23 22:48:25 2007 +0200
     4.2 +++ b/src/HOL/Complex/ex/MIR.thy	Tue Oct 23 23:27:23 2007 +0200
     4.3 @@ -268,7 +268,7 @@
     4.4  | "fmsize (NDvd i t) = 2"
     4.5  | "fmsize p = 1"
     4.6    (* several lemmas about fmsize *)
     4.7 -lemma fmsize_pos: "fmsize p \<noteq> 0"	
     4.8 +lemma fmsize_pos: "fmsize p > 0"	
     4.9  by (induct p rule: fmsize.induct) simp_all
    4.10  
    4.11    (* Semantics of formulae (fm) *)
    4.12 @@ -316,7 +316,7 @@
    4.13    "prep (Imp p q) = prep (Or (NOT p) q)"
    4.14    "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
    4.15    "prep p = p"
    4.16 -(hints simp add: fmsize_pos neq0_conv[symmetric])
    4.17 +(hints simp add: fmsize_pos)
    4.18  lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
    4.19  by (induct p rule: prep.induct, auto)
    4.20  
     5.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Tue Oct 23 22:48:25 2007 +0200
     5.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Tue Oct 23 23:27:23 2007 +0200
     5.3 @@ -106,7 +106,7 @@
     5.4    "fmsize (A p) = 4+ fmsize p"
     5.5    "fmsize p = 1"
     5.6    (* several lemmas about fmsize *)
     5.7 -lemma fmsize_pos: "fmsize p \<noteq> 0"
     5.8 +lemma fmsize_pos: "fmsize p > 0"
     5.9  by (induct p rule: fmsize.induct) simp_all
    5.10  
    5.11    (* Semantics of formulae (fm) *)
    5.12 @@ -917,7 +917,7 @@
    5.13    "prep (Imp p q) = prep (Or (NOT p) q)"
    5.14    "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
    5.15    "prep p = p"
    5.16 -(hints simp add: fmsize_pos neq0_conv[symmetric])
    5.17 +(hints simp add: fmsize_pos)
    5.18  lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
    5.19  by (induct p rule: prep.induct, auto)
    5.20  
     6.1 --- a/src/HOL/Divides.thy	Tue Oct 23 22:48:25 2007 +0200
     6.2 +++ b/src/HOL/Divides.thy	Tue Oct 23 23:27:23 2007 +0200
     6.3 @@ -250,14 +250,14 @@
     6.4    apply (simp add: quorem_def)
     6.5    done
     6.6  
     6.7 -lemma quorem_div_mod: "b \<noteq> 0 ==> quorem ((a, b), (a div b, a mod b))"
     6.8 -  unfolding quorem_def by simp
     6.9 +lemma quorem_div_mod: "b > 0 ==> quorem ((a, b), (a div b, a mod b))"
    6.10 +unfolding quorem_def by simp
    6.11  
    6.12 -lemma quorem_div: "[| quorem((a,b),(q,r));  b \<noteq> 0 |] ==> a div b = q"
    6.13 -  by (simp add: quorem_div_mod [THEN unique_quotient])
    6.14 +lemma quorem_div: "[| quorem((a,b),(q,r));  b > 0 |] ==> a div b = q"
    6.15 +by (simp add: quorem_div_mod [THEN unique_quotient])
    6.16  
    6.17 -lemma quorem_mod: "[| quorem((a,b),(q,r));  b \<noteq> 0 |] ==> a mod b = r"
    6.18 -  by (simp add: quorem_div_mod [THEN unique_remainder])
    6.19 +lemma quorem_mod: "[| quorem((a,b),(q,r));  b > 0 |] ==> a mod b = r"
    6.20 +by (simp add: quorem_div_mod [THEN unique_remainder])
    6.21  
    6.22  (** A dividend of zero **)
    6.23  
    6.24 @@ -270,9 +270,9 @@
    6.25  (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
    6.26  
    6.27  lemma quorem_mult1_eq:
    6.28 -     "[| quorem((b,c),(q,r)); c \<noteq> 0 |]
    6.29 -      ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
    6.30 -  by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
    6.31 +  "[| quorem((b,c),(q,r)); c > 0 |]
    6.32 +   ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
    6.33 +by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
    6.34  
    6.35  lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
    6.36  apply (cases "c = 0", simp)
    6.37 @@ -291,17 +291,18 @@
    6.38     apply (simp_all add: mult_commute)
    6.39    done
    6.40  
    6.41 -lemma mod_mult_distrib_mod: "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
    6.42 -  apply (rule mod_mult1_eq' [THEN trans])
    6.43 -  apply (rule mod_mult1_eq)
    6.44 -  done
    6.45 +lemma mod_mult_distrib_mod:
    6.46 +  "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
    6.47 +apply (rule mod_mult1_eq' [THEN trans])
    6.48 +apply (rule mod_mult1_eq)
    6.49 +done
    6.50  
    6.51  (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
    6.52  
    6.53  lemma quorem_add1_eq:
    6.54 -     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c \<noteq> 0 |]
    6.55 -      ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
    6.56 -  by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
    6.57 +  "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c > 0 |]
    6.58 +   ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
    6.59 +by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
    6.60  
    6.61  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
    6.62  lemma div_add1_eq:
    6.63 @@ -621,7 +622,7 @@
    6.64    apply (simp add: power_add)
    6.65    done
    6.66  
    6.67 -lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
    6.68 +lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
    6.69    by (induct n) auto
    6.70  
    6.71  lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
    6.72 @@ -690,19 +691,20 @@
    6.73  
    6.74  lemma split_div_lemma:
    6.75    "0 < n \<Longrightarrow> (n * q \<le> m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
    6.76 -  apply (rule iffI)
    6.77 -  apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
    6.78 -prefer 3; apply assumption
    6.79 -  apply (simp_all add: quorem_def) apply arith
    6.80 -  apply (rule conjI)
    6.81 -  apply (rule_tac P="%x. n * (m div n) \<le> x" in
    6.82 +apply (rule iffI)
    6.83 + apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
    6.84 +   prefer 3; apply assumption
    6.85 +  apply (simp_all add: quorem_def)
    6.86 + apply arith
    6.87 +apply (rule conjI)
    6.88 + apply (rule_tac P="%x. n * (m div n) \<le> x" in
    6.89      subst [OF mod_div_equality [of _ n]])
    6.90 -  apply (simp only: add: mult_ac)
    6.91 -  apply (rule_tac P="%x. x < n + n * (m div n)" in
    6.92 + apply (simp only: add: mult_ac)
    6.93 + apply (rule_tac P="%x. x < n + n * (m div n)" in
    6.94      subst [OF mod_div_equality [of _ n]])
    6.95 -  apply (simp only: add: mult_ac add_ac)
    6.96 -  apply (rule add_less_mono1, simp)
    6.97 -  done
    6.98 +apply (simp only: add: mult_ac add_ac)
    6.99 +apply (rule add_less_mono1, simp)
   6.100 +done
   6.101  
   6.102  theorem split_div':
   6.103    "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
     7.1 --- a/src/HOL/Finite_Set.thy	Tue Oct 23 22:48:25 2007 +0200
     7.2 +++ b/src/HOL/Finite_Set.thy	Tue Oct 23 23:27:23 2007 +0200
     7.3 @@ -1652,16 +1652,6 @@
     7.4  apply(subst card_insert)
     7.5   apply(auto intro:ccontr)
     7.6  done
     7.7 -(*
     7.8 -lemma card_1_eq:
     7.9 -  "(card A = Suc 0) = (\<exists>x. A = {x})"
    7.10 -by (auto dest!: card_eq_SucD)
    7.11 -
    7.12 -lemma card_2_eq:
    7.13 - "(card A = Suc(Suc 0)) = (\<exists>x y. x\<noteq>y & A = {x,y})" 
    7.14 -by (auto dest!: card_eq_SucD)
    7.15 -*)
    7.16 -
    7.17  
    7.18  lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
    7.19  apply (cases "finite A")
    7.20 @@ -1725,7 +1715,7 @@
    7.21  by(simp add:card_def setsum_reindex o_def del:setsum_constant)
    7.22  
    7.23  lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
    7.24 -  by (simp add: card_seteq card_image)
    7.25 +by (simp add: card_seteq card_image)
    7.26  
    7.27  lemma eq_card_imp_inj_on:
    7.28    "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
    7.29 @@ -1806,6 +1796,32 @@
    7.30    done
    7.31  
    7.32  
    7.33 +subsubsection {* Relating injectivity and surjectivity *}
    7.34 +
    7.35 +lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
    7.36 +apply(rule eq_card_imp_inj_on, assumption)
    7.37 +apply(frule finite_imageI)
    7.38 +apply(drule (1) card_seteq)
    7.39 +apply(erule card_image_le)
    7.40 +apply simp
    7.41 +done
    7.42 +
    7.43 +lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
    7.44 +shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
    7.45 +by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
    7.46 +
    7.47 +lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
    7.48 +shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
    7.49 +by(fastsimp simp:surj_def dest!: endo_inj_surj)
    7.50 +
    7.51 +corollary infinite_UNIV_nat: "~finite(UNIV::nat set)"
    7.52 +proof
    7.53 +  assume "finite(UNIV::nat set)"
    7.54 +  with finite_UNIV_inj_surj[of Suc]
    7.55 +  show False by simp (blast dest: Suc_neq_Zero surjD)
    7.56 +qed
    7.57 +
    7.58 +
    7.59  subsection{* A fold functional for non-empty sets *}
    7.60  
    7.61  text{* Does not require start value. *}
     8.1 --- a/src/HOL/Hyperreal/Fact.thy	Tue Oct 23 22:48:25 2007 +0200
     8.2 +++ b/src/HOL/Hyperreal/Fact.thy	Tue Oct 23 23:27:23 2007 +0200
     8.3 @@ -20,7 +20,7 @@
     8.4  by (induct n) auto
     8.5  
     8.6  lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
     8.7 -by (simp add: neq0_conv)
     8.8 +by simp
     8.9  
    8.10  lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
    8.11  by auto
     9.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Tue Oct 23 22:48:25 2007 +0200
     9.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Tue Oct 23 23:27:23 2007 +0200
     9.3 @@ -331,7 +331,7 @@
     9.4       "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
     9.5        ==> {n. N < f n} \<in> FreeUltrafilterNat"
     9.6  apply (induct_tac N)
     9.7 -apply (drule_tac x = 0 in spec, simp add: neq0_conv)
     9.8 +apply (drule_tac x = 0 in spec, simp)
     9.9  apply (drule_tac x = "Suc n" in spec)
    9.10  apply (elim ultra, auto)
    9.11  done
    10.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Oct 23 22:48:25 2007 +0200
    10.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Oct 23 23:27:23 2007 +0200
    10.3 @@ -114,7 +114,7 @@
    10.4  done
    10.5  
    10.6  lemma Maclaurin:
    10.7 -   "[| 0 < h; n \<noteq> 0; diff 0 = f;
    10.8 +   "[| 0 < h; n > 0; diff 0 = f;
    10.9         \<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |]
   10.10      ==> \<exists>t. 0 < t &
   10.11                t < h &
   10.12 @@ -185,7 +185,7 @@
   10.13  done
   10.14  
   10.15  lemma Maclaurin_objl:
   10.16 -  "0 < h & n\<noteq>0 & diff 0 = f &
   10.17 +  "0 < h & n>0 & diff 0 = f &
   10.18    (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
   10.19     --> (\<exists>t. 0 < t & t < h &
   10.20              f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   10.21 @@ -218,7 +218,7 @@
   10.22  by (blast intro: Maclaurin2)
   10.23  
   10.24  lemma Maclaurin_minus:
   10.25 -   "[| h < 0; n \<noteq> 0; diff 0 = f;
   10.26 +   "[| h < 0; n > 0; diff 0 = f;
   10.27         \<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t |]
   10.28      ==> \<exists>t. h < t &
   10.29                t < 0 &
   10.30 @@ -245,7 +245,7 @@
   10.31  done
   10.32  
   10.33  lemma Maclaurin_minus_objl:
   10.34 -     "(h < 0 & n \<noteq> 0 & diff 0 = f &
   10.35 +     "(h < 0 & n > 0 & diff 0 = f &
   10.36         (\<forall>m t.
   10.37            m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t))
   10.38      --> (\<exists>t. h < t &
   10.39 @@ -261,7 +261,7 @@
   10.40  (* not good for PVS sin_approx, cos_approx *)
   10.41  
   10.42  lemma Maclaurin_bi_le_lemma [rule_format]:
   10.43 -  "n\<noteq>0 \<longrightarrow>
   10.44 +  "n>0 \<longrightarrow>
   10.45     diff 0 0 =
   10.46     (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
   10.47     diff n 0 * 0 ^ n / real (fact n)"
   10.48 @@ -294,7 +294,7 @@
   10.49  lemma Maclaurin_all_lt:
   10.50       "[| diff 0 = f;
   10.51           \<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
   10.52 -        x ~= 0; n \<noteq> 0
   10.53 +        x ~= 0; n > 0
   10.54        |] ==> \<exists>t. 0 < abs t & abs t < abs x &
   10.55                 f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   10.56                       (diff n t / real (fact n)) * x ^ n"
   10.57 @@ -308,7 +308,7 @@
   10.58  lemma Maclaurin_all_lt_objl:
   10.59       "diff 0 = f &
   10.60        (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
   10.61 -      x ~= 0 & n \<noteq> 0
   10.62 +      x ~= 0 & n > 0
   10.63        --> (\<exists>t. 0 < abs t & abs t < abs x &
   10.64                 f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   10.65                       (diff n t / real (fact n)) * x ^ n)"
   10.66 @@ -346,7 +346,7 @@
   10.67  
   10.68  subsection{*Version for Exponential Function*}
   10.69  
   10.70 -lemma Maclaurin_exp_lt: "[| x ~= 0; n \<noteq> 0 |]
   10.71 +lemma Maclaurin_exp_lt: "[| x ~= 0; n > 0 |]
   10.72        ==> (\<exists>t. 0 < abs t &
   10.73                  abs t < abs x &
   10.74                  exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
   10.75 @@ -423,9 +423,8 @@
   10.76  done
   10.77  
   10.78  
   10.79 -
   10.80  lemma Maclaurin_sin_expansion3:
   10.81 -     "[| n \<noteq> 0; 0 < x |] ==>
   10.82 +     "[| n > 0; 0 < x |] ==>
   10.83         \<exists>t. 0 < t & t < x &
   10.84         sin x =
   10.85         (\<Sum>m=0..<n. (if even m then 0
   10.86 @@ -491,7 +490,7 @@
   10.87  done
   10.88  
   10.89  lemma Maclaurin_cos_expansion2:
   10.90 -     "[| 0 < x; n \<noteq> 0 |] ==>
   10.91 +     "[| 0 < x; n > 0 |] ==>
   10.92         \<exists>t. 0 < t & t < x &
   10.93         cos x =
   10.94         (\<Sum>m=0..<n. (if even m
   10.95 @@ -510,7 +509,7 @@
   10.96  done
   10.97  
   10.98  lemma Maclaurin_minus_cos_expansion:
   10.99 -     "[| x < 0; n \<noteq> 0 |] ==>
  10.100 +     "[| x < 0; n > 0 |] ==>
  10.101         \<exists>t. x < t & t < 0 &
  10.102         cos x =
  10.103         (\<Sum>m=0..<n. (if even m
    11.1 --- a/src/HOL/Hyperreal/Poly.thy	Tue Oct 23 22:48:25 2007 +0200
    11.2 +++ b/src/HOL/Hyperreal/Poly.thy	Tue Oct 23 23:27:23 2007 +0200
    11.3 @@ -782,7 +782,7 @@
    11.4  declare pexp_one [simp]
    11.5  
    11.6  lemma lemma_order_root [rule_format]:
    11.7 -     "\<forall>p a. n \<noteq> 0 & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
    11.8 +     "\<forall>p a. n > 0 & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
    11.9               --> poly p a = 0"
   11.10  apply (induct "n", blast)
   11.11  apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
   11.12 @@ -792,8 +792,9 @@
   11.13  apply (case_tac "poly p = poly []", auto)
   11.14  apply (simp add: poly_linear_divides del: pmult_Cons, safe)
   11.15  apply (drule_tac [!] a = a in order2)
   11.16 +apply (rule ccontr)
   11.17  apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
   11.18 -apply (metis gr0_conv lemma_order_root)
   11.19 +apply (blast intro: lemma_order_root)
   11.20  done
   11.21  
   11.22  lemma order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
   11.23 @@ -842,7 +843,7 @@
   11.24  
   11.25  (* FIXME: too too long! *)
   11.26  lemma lemma_order_pderiv [rule_format]:
   11.27 -     "\<forall>p q a. n \<noteq> 0 &
   11.28 +     "\<forall>p q a. n > 0 &
   11.29         poly (pderiv p) \<noteq> poly [] &
   11.30         poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q
   11.31         --> n = Suc (order a (pderiv p))"
    12.1 --- a/src/HOL/Hyperreal/Taylor.thy	Tue Oct 23 22:48:25 2007 +0200
    12.2 +++ b/src/HOL/Hyperreal/Taylor.thy	Tue Oct 23 23:27:23 2007 +0200
    12.3 @@ -15,7 +15,7 @@
    12.4  *}
    12.5  
    12.6  lemma taylor_up: 
    12.7 -  assumes INIT: "n\<noteq>0" "diff 0 = f"
    12.8 +  assumes INIT: "n>0" "diff 0 = f"
    12.9    and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
   12.10    and INTERV: "a \<le> c" "c < b" 
   12.11    shows "\<exists> t. c < t & t < b & 
   12.12 @@ -24,9 +24,9 @@
   12.13  proof -
   12.14    from INTERV have "0 < b-c" by arith
   12.15    moreover 
   12.16 -  from INIT have "n\<noteq>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
   12.17 +  from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
   12.18    moreover
   12.19 -  have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"  
   12.20 +  have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
   12.21    proof (intro strip)
   12.22      fix m t
   12.23      assume "m < n & 0 <= t & t <= b - c"
   12.24 @@ -57,7 +57,7 @@
   12.25  qed
   12.26  
   12.27  lemma taylor_down:
   12.28 -  assumes INIT: "n\<noteq>0" "diff 0 = f"
   12.29 +  assumes INIT: "n>0" "diff 0 = f"
   12.30    and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
   12.31    and INTERV: "a < c" "c \<le> b"
   12.32    shows "\<exists> t. a < t & t < c & 
   12.33 @@ -66,7 +66,7 @@
   12.34  proof -
   12.35    from INTERV have "a-c < 0" by arith
   12.36    moreover 
   12.37 -  from INIT have "n\<noteq>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
   12.38 +  from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
   12.39    moreover
   12.40    have "ALL m t. m < n & a-c <= t & t <= 0 --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
   12.41    proof (rule allI impI)+
   12.42 @@ -97,7 +97,7 @@
   12.43  qed
   12.44  
   12.45  lemma taylor:
   12.46 -  assumes INIT: "n\<noteq>0" "diff 0 = f"
   12.47 +  assumes INIT: "n>0" "diff 0 = f"
   12.48    and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
   12.49    and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" 
   12.50    shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
    13.1 --- a/src/HOL/IntArith.thy	Tue Oct 23 22:48:25 2007 +0200
    13.2 +++ b/src/HOL/IntArith.thy	Tue Oct 23 23:27:23 2007 +0200
    13.3 @@ -398,6 +398,15 @@
    13.4   apply (frule pos_zmult_eq_1_iff_lemma, auto) 
    13.5  done
    13.6  
    13.7 +(* Could be simplified but Presburger only becomes available too late *)
    13.8 +lemma infinite_UNIV_int: "~finite(UNIV::int set)"
    13.9 +proof
   13.10 +  assume "finite(UNIV::int set)"
   13.11 +  moreover have "~(EX i::int. 2*i = 1)"
   13.12 +    by (auto simp: pos_zmult_eq_1_iff)
   13.13 +  ultimately show False using finite_UNIV_inj_surj[of "%n::int. n+n"]
   13.14 +    by (simp add:inj_on_def surj_def) (blast intro:sym)
   13.15 +qed
   13.16  
   13.17  subsection {* Legacy ML bindings *}
   13.18  
    14.1 --- a/src/HOL/Library/Binomial.thy	Tue Oct 23 22:48:25 2007 +0200
    14.2 +++ b/src/HOL/Library/Binomial.thy	Tue Oct 23 23:27:23 2007 +0200
    14.3 @@ -44,7 +44,7 @@
    14.4  lemma binomial_1 [simp]: "(n choose Suc 0) = n"
    14.5  by (induct n) simp_all
    14.6  
    14.7 -lemma zero_less_binomial: "k \<le> n ==> (n choose k) \<noteq> 0"
    14.8 +lemma zero_less_binomial: "k \<le> n ==> (n choose k) > 0"
    14.9  by (induct n k rule: diff_induct) simp_all
   14.10  
   14.11  lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
   14.12 @@ -53,8 +53,9 @@
   14.13  apply (simp add: zero_less_binomial)
   14.14  done
   14.15  
   14.16 -lemma zero_less_binomial_iff: "(n choose k \<noteq> 0) = (k\<le>n)"
   14.17 -by (simp add: linorder_not_less binomial_eq_0_iff)
   14.18 +lemma zero_less_binomial_iff: "(n choose k > 0) = (k\<le>n)"
   14.19 +by(simp add: linorder_not_less binomial_eq_0_iff neq0_conv[symmetric]
   14.20 +        del:neq0_conv)
   14.21  
   14.22  (*Might be more useful if re-oriented*)
   14.23  lemma Suc_times_binomial_eq:
    15.1 --- a/src/HOL/Library/Multiset.thy	Tue Oct 23 22:48:25 2007 +0200
    15.2 +++ b/src/HOL/Library/Multiset.thy	Tue Oct 23 23:27:23 2007 +0200
    15.3 @@ -11,7 +11,7 @@
    15.4  
    15.5  subsection {* The type of multisets *}
    15.6  
    15.7 -typedef 'a multiset = "{f::'a => nat. finite {x . f x \<noteq> 0}}"
    15.8 +typedef 'a multiset = "{f::'a => nat. finite {x . f x > 0}}"
    15.9  proof
   15.10    show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp
   15.11  qed
   15.12 @@ -38,7 +38,7 @@
   15.13  
   15.14  abbreviation
   15.15    Melem :: "'a => 'a multiset => bool"  ("(_/ :# _)" [50, 51] 50) where
   15.16 -  "a :# M == count M a \<noteq> 0"
   15.17 +  "a :# M == count M a > 0"
   15.18  
   15.19  syntax
   15.20    "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
   15.21 @@ -309,7 +309,7 @@
   15.22     apply (rule ext, force, clarify)
   15.23    apply (frule setsum_SucD, clarify)
   15.24    apply (rename_tac a)
   15.25 -  apply (subgoal_tac "finite {x. (f (a := f a - 1)) x \<noteq> 0}")
   15.26 +  apply (subgoal_tac "finite {x. (f (a := f a - 1)) x > 0}")
   15.27     prefer 2
   15.28     apply (rule finite_subset)
   15.29      prefer 2
   15.30 @@ -759,7 +759,7 @@
   15.31    apply (rule_tac x = "x # xa" in exI, auto)
   15.32    done
   15.33  
   15.34 -lemma set_count_greater_0: "set x = {a. count (multiset_of x) a \<noteq> 0}"
   15.35 +lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}"
   15.36    by (induct x) auto
   15.37  
   15.38  lemma distinct_count_atmost_1:
    16.1 --- a/src/HOL/Library/Parity.thy	Tue Oct 23 22:48:25 2007 +0200
    16.2 +++ b/src/HOL/Library/Parity.thy	Tue Oct 23 23:27:23 2007 +0200
    16.3 @@ -222,7 +222,7 @@
    16.4    apply (subst power_add)
    16.5    apply (subst zero_le_mult_iff)
    16.6    apply auto
    16.7 -  apply (subgoal_tac "x = 0 & y \<noteq> 0")
    16.8 +  apply (subgoal_tac "x = 0 & y > 0")
    16.9    apply (erule conjE, assumption)
   16.10    apply (subst power_eq_0_iff [symmetric])
   16.11    apply (subgoal_tac "0 <= x^y * x^y")
    17.1 --- a/src/HOL/Library/Word.thy	Tue Oct 23 22:48:25 2007 +0200
    17.2 +++ b/src/HOL/Library/Word.thy	Tue Oct 23 23:27:23 2007 +0200
    17.3 @@ -479,7 +479,7 @@
    17.4          with mod_div_equality [of n 2]
    17.5          show "n div 2 * 2 = n" by simp
    17.6        next
    17.7 -        assume "n mod 2 \<noteq> 0"
    17.8 +        assume "n mod 2 = Suc 0"
    17.9          with mod_div_equality [of n 2]
   17.10          show "Suc (n div 2 * 2) = n" by arith
   17.11        qed
    18.1 --- a/src/HOL/List.thy	Tue Oct 23 22:48:25 2007 +0200
    18.2 +++ b/src/HOL/List.thy	Tue Oct 23 23:27:23 2007 +0200
    18.3 @@ -950,7 +950,7 @@
    18.4    proof (cases)
    18.5      assume "p x"
    18.6      hence eq: "?S' = insert 0 (Suc ` ?S)"
    18.7 -      by(auto simp: nth_Cons image_def split:nat.split dest:not0_implies_Suc)
    18.8 +      by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)
    18.9      have "length (filter p (x # xs)) = Suc(card ?S)"
   18.10        using Cons `p x` by simp
   18.11      also have "\<dots> = Suc(card(Suc ` ?S))" using fin
   18.12 @@ -961,7 +961,7 @@
   18.13    next
   18.14      assume "\<not> p x"
   18.15      hence eq: "?S' = Suc ` ?S"
   18.16 -      by(auto simp add: image_def neq0_conv split:nat.split elim:lessE)
   18.17 +      by(auto simp add: image_def split:nat.split elim:lessE)
   18.18      have "length (filter p (x # xs)) = card ?S"
   18.19        using Cons `\<not> p x` by simp
   18.20      also have "\<dots> = card(Suc ` ?S)" using fin
   18.21 @@ -2456,7 +2456,7 @@
   18.22  
   18.23  lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
   18.24  apply(induct xs arbitrary: I)
   18.25 -apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: not0_implies_Suc)
   18.26 +apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
   18.27  done
   18.28  
   18.29  lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
    19.1 --- a/src/HOL/Nat.thy	Tue Oct 23 22:48:25 2007 +0200
    19.2 +++ b/src/HOL/Nat.thy	Tue Oct 23 23:27:23 2007 +0200
    19.3 @@ -100,22 +100,22 @@
    19.4  text {* Injectiveness and distinctness lemmas *}
    19.5  
    19.6  lemma Suc_neq_Zero: "Suc m = 0 ==> R"
    19.7 -  by (rule notE, rule Suc_not_Zero)
    19.8 +by (rule notE, rule Suc_not_Zero)
    19.9  
   19.10  lemma Zero_neq_Suc: "0 = Suc m ==> R"
   19.11 -  by (rule Suc_neq_Zero, erule sym)
   19.12 +by (rule Suc_neq_Zero, erule sym)
   19.13  
   19.14  lemma Suc_inject: "Suc x = Suc y ==> x = y"
   19.15 -  by (rule inj_Suc [THEN injD])
   19.16 +by (rule inj_Suc [THEN injD])
   19.17  
   19.18  lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
   19.19 -  by auto
   19.20 +by auto
   19.21  
   19.22  lemma n_not_Suc_n: "n \<noteq> Suc n"
   19.23 -  by (induct n) simp_all
   19.24 +by (induct n) simp_all
   19.25  
   19.26  lemma Suc_n_not_n: "Suc t \<noteq> t"
   19.27 -  by (rule not_sym, rule n_not_Suc_n)
   19.28 +by (rule not_sym, rule n_not_Suc_n)
   19.29  
   19.30  
   19.31  text {* A special form of induction for reasoning
   19.32 @@ -221,12 +221,12 @@
   19.33    done
   19.34  
   19.35  lemma less_irrefl [elim!]: "(n::nat) < n ==> R"
   19.36 -  by (rule notE, rule less_not_refl)
   19.37 +by (rule notE, rule less_not_refl)
   19.38  
   19.39  lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)" by blast
   19.40  
   19.41  lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
   19.42 -  by (rule not_sym, rule less_not_refl2)
   19.43 +by (rule not_sym, rule less_not_refl2)
   19.44  
   19.45  lemma lessE:
   19.46    assumes major: "i < k"
   19.47 @@ -239,10 +239,10 @@
   19.48    done
   19.49  
   19.50  lemma not_less0 [iff]: "~ n < (0::nat)"
   19.51 -  by (blast elim: lessE)
   19.52 +by (blast elim: lessE)
   19.53  
   19.54  lemma less_zeroE: "(n::nat) < 0 ==> R"
   19.55 -  by (rule notE, rule not_less0)
   19.56 +by (rule notE, rule not_less0)
   19.57  
   19.58  lemma less_SucE: assumes major: "m < Suc n"
   19.59    and less: "m < n ==> P" and eq: "m = n ==> P" shows P
   19.60 @@ -252,16 +252,16 @@
   19.61    done
   19.62  
   19.63  lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
   19.64 -  by (blast elim!: less_SucE intro: less_trans)
   19.65 +by (blast elim!: less_SucE intro: less_trans)
   19.66  
   19.67  lemma less_one [iff,noatp]: "(n < (1::nat)) = (n = 0)"
   19.68 -  by (simp add: less_Suc_eq)
   19.69 +by (simp add: less_Suc_eq)
   19.70  
   19.71  lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
   19.72 -  by (simp add: less_Suc_eq)
   19.73 +by (simp add: less_Suc_eq)
   19.74  
   19.75  lemma Suc_mono: "m < n ==> Suc m < Suc n"
   19.76 -  by (induct n) (fast elim: less_trans lessE)+
   19.77 +by (induct n) (fast elim: less_trans lessE)+
   19.78  
   19.79  text {* "Less than" is a linear ordering *}
   19.80  lemma less_linear: "m < n | m = n | n < (m::nat)"
   19.81 @@ -312,7 +312,7 @@
   19.82    done
   19.83  
   19.84  lemma Suc_less_SucD: "Suc m < Suc n ==> m < n"
   19.85 -  by (blast elim: lessE dest: Suc_lessD)
   19.86 +by (blast elim: lessE dest: Suc_lessD)
   19.87  
   19.88  lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)"
   19.89    apply (rule iffI)
   19.90 @@ -333,7 +333,7 @@
   19.91  
   19.92  text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
   19.93  lemma not_less_eq: "(~ m < n) = (n < Suc m)"
   19.94 -  by (induct m n rule: diff_induct) simp_all
   19.95 +by (induct m n rule: diff_induct) simp_all
   19.96  
   19.97  text {* Complete induction, aka course-of-values induction *}
   19.98  lemma nat_less_induct:
   19.99 @@ -353,22 +353,22 @@
  19.100    unfolding le_def by (rule not_less_eq [symmetric])
  19.101  
  19.102  lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n"
  19.103 -  by (rule less_Suc_eq_le [THEN iffD2])
  19.104 +by (rule less_Suc_eq_le [THEN iffD2])
  19.105  
  19.106  lemma le0 [iff]: "(0::nat) \<le> n"
  19.107    unfolding le_def by (rule not_less0)
  19.108  
  19.109  lemma Suc_n_not_le_n: "~ Suc n \<le> n"
  19.110 -  by (simp add: le_def)
  19.111 +by (simp add: le_def)
  19.112  
  19.113  lemma le_0_eq [iff]: "((i::nat) \<le> 0) = (i = 0)"
  19.114 -  by (induct i) (simp_all add: le_def)
  19.115 +by (induct i) (simp_all add: le_def)
  19.116  
  19.117  lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)"
  19.118 -  by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
  19.119 +by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
  19.120  
  19.121  lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
  19.122 -  by (drule le_Suc_eq [THEN iffD1], iprover+)
  19.123 +by (drule le_Suc_eq [THEN iffD1], iprover+)
  19.124  
  19.125  lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
  19.126    apply (simp add: le_def less_Suc_eq)
  19.127 @@ -376,7 +376,7 @@
  19.128    done -- {* formerly called lessD *}
  19.129  
  19.130  lemma Suc_leD: "Suc(m) \<le> n ==> m \<le> n"
  19.131 -  by (simp add: le_def less_Suc_eq)
  19.132 +by (simp add: le_def less_Suc_eq)
  19.133  
  19.134  text {* Stronger version of @{text Suc_leD} *}
  19.135  lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
  19.136 @@ -386,13 +386,13 @@
  19.137    done
  19.138  
  19.139  lemma Suc_le_eq: "(Suc m \<le> n) = (m < n)"
  19.140 -  by (blast intro: Suc_leI Suc_le_lessD)
  19.141 +by (blast intro: Suc_leI Suc_le_lessD)
  19.142  
  19.143  lemma le_SucI: "m \<le> n ==> m \<le> Suc n"
  19.144 -  by (unfold le_def) (blast dest: Suc_lessD)
  19.145 +by (unfold le_def) (blast dest: Suc_lessD)
  19.146  
  19.147  lemma less_imp_le: "m < n ==> m \<le> (n::nat)"
  19.148 -  by (unfold le_def) (blast elim: less_asym)
  19.149 +by (unfold le_def) (blast elim: less_asym)
  19.150  
  19.151  text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *}
  19.152  lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq
  19.153 @@ -411,36 +411,36 @@
  19.154    by (blast elim!: less_irrefl elim: less_asym)
  19.155  
  19.156  lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
  19.157 -  by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq)
  19.158 +by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq)
  19.159  
  19.160  text {* Useful with @{text blast}. *}
  19.161  lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
  19.162 -  by (rule less_or_eq_imp_le) (rule disjI2)
  19.163 +by (rule less_or_eq_imp_le) (rule disjI2)
  19.164  
  19.165  lemma le_refl: "n \<le> (n::nat)"
  19.166 -  by (simp add: le_eq_less_or_eq)
  19.167 +by (simp add: le_eq_less_or_eq)
  19.168  
  19.169  lemma le_less_trans: "[| i \<le> j; j < k |] ==> i < (k::nat)"
  19.170 -  by (blast dest!: le_imp_less_or_eq intro: less_trans)
  19.171 +by (blast dest!: le_imp_less_or_eq intro: less_trans)
  19.172  
  19.173  lemma less_le_trans: "[| i < j; j \<le> k |] ==> i < (k::nat)"
  19.174 -  by (blast dest!: le_imp_less_or_eq intro: less_trans)
  19.175 +by (blast dest!: le_imp_less_or_eq intro: less_trans)
  19.176  
  19.177  lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
  19.178 -  by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans)
  19.179 +by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans)
  19.180  
  19.181  lemma le_anti_sym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
  19.182 -  by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym)
  19.183 +by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym)
  19.184  
  19.185  lemma Suc_le_mono [iff]: "(Suc n \<le> Suc m) = (n \<le> m)"
  19.186 -  by (simp add: le_simps)
  19.187 +by (simp add: le_simps)
  19.188  
  19.189  text {* Axiom @{text order_less_le} of class @{text order}: *}
  19.190  lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)"
  19.191 -  by (simp add: le_def nat_neq_iff) (blast elim!: less_asym)
  19.192 +by (simp add: le_def nat_neq_iff) (blast elim!: less_asym)
  19.193  
  19.194  lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n"
  19.195 -  by (rule iffD2, rule nat_less_le, rule conjI)
  19.196 +by (rule iffD2, rule nat_less_le, rule conjI)
  19.197  
  19.198  text {* Axiom @{text linorder_linear} of class @{text linorder}: *}
  19.199  lemma nat_le_linear: "(m::nat) \<le> n | n \<le> m"
  19.200 @@ -457,7 +457,7 @@
  19.201  lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat]
  19.202  
  19.203  lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
  19.204 -  by (blast elim!: less_SucE)
  19.205 +by (blast elim!: less_SucE)
  19.206  
  19.207  text {*
  19.208    Rewrite @{term "n < Suc m"} to @{term "n = m"}
  19.209 @@ -465,7 +465,7 @@
  19.210    Not suitable as default simprules because they often lead to looping
  19.211  *}
  19.212  lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)"
  19.213 -  by (rule not_less_less_Suc_eq, rule leD)
  19.214 +by (rule not_less_less_Suc_eq, rule leD)
  19.215  
  19.216  lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
  19.217  
  19.218 @@ -478,46 +478,47 @@
  19.219  
  19.220  text {* Polymorphic, not just for @{typ nat} *}
  19.221  lemma zero_reorient: "(0 = x) = (x = 0)"
  19.222 -  by auto
  19.223 +by auto
  19.224  
  19.225  lemma one_reorient: "(1 = x) = (x = 1)"
  19.226 -  by auto
  19.227 +by auto
  19.228  
  19.229  text {* These two rules ease the use of primitive recursion.
  19.230  NOTE USE OF @{text "=="} *}
  19.231  lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c"
  19.232 -  by simp
  19.233 +by simp
  19.234  
  19.235  lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)"
  19.236 -  by simp
  19.237 +by simp
  19.238  
  19.239  lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
  19.240 -  by (cases n) simp_all
  19.241 +by (cases n) simp_all
  19.242 +
  19.243 +lemma gr0_implies_Suc: "n > 0 ==> \<exists>m. n = Suc m"
  19.244 +by (cases n) simp_all
  19.245  
  19.246  lemma gr_implies_not0: fixes n :: nat shows "m<n ==> n \<noteq> 0"
  19.247 -  by (cases n) simp_all
  19.248 +by (cases n) simp_all
  19.249  
  19.250 -lemma neq0_conv: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
  19.251 -  by (cases n) simp_all
  19.252 -
  19.253 -lemmas gr0_conv = neq0_conv[symmetric]
  19.254 +lemma neq0_conv[iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
  19.255 +by (cases n) simp_all
  19.256  
  19.257  text {* This theorem is useful with @{text blast} *}
  19.258  lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
  19.259 -  by (rule iffD1, rule neq0_conv, iprover)
  19.260 +by (rule neq0_conv[THEN iffD1], iprover)
  19.261  
  19.262  lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
  19.263 -  by (fast intro: not0_implies_Suc)
  19.264 +by (fast intro: not0_implies_Suc)
  19.265  
  19.266  lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
  19.267  using neq0_conv by blast
  19.268  
  19.269  lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
  19.270 -  by (induct m') simp_all
  19.271 +by (induct m') simp_all
  19.272  
  19.273  text {* Useful in certain inductive arguments *}
  19.274  lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))"
  19.275 -  by (cases m) simp_all
  19.276 +by (cases m) simp_all
  19.277  
  19.278  lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
  19.279    apply (rule nat_less_induct)
  19.280 @@ -542,48 +543,48 @@
  19.281    done
  19.282  
  19.283  lemma Least_Suc2:
  19.284 -     "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
  19.285 -  by (erule (1) Least_Suc [THEN ssubst], simp)
  19.286 +   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
  19.287 +by (erule (1) Least_Suc [THEN ssubst], simp)
  19.288  
  19.289  
  19.290  subsection {* @{term min} and @{term max} *}
  19.291  
  19.292  lemma mono_Suc: "mono Suc"
  19.293 -  by (rule monoI) simp
  19.294 +by (rule monoI) simp
  19.295  
  19.296  lemma min_0L [simp]: "min 0 n = (0::nat)"
  19.297 -  by (rule min_leastL) simp
  19.298 +by (rule min_leastL) simp
  19.299  
  19.300  lemma min_0R [simp]: "min n 0 = (0::nat)"
  19.301 -  by (rule min_leastR) simp
  19.302 +by (rule min_leastR) simp
  19.303  
  19.304  lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
  19.305 -  by (simp add: mono_Suc min_of_mono)
  19.306 +by (simp add: mono_Suc min_of_mono)
  19.307  
  19.308  lemma min_Suc1:
  19.309     "min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
  19.310 -  by (simp split: nat.split)
  19.311 +by (simp split: nat.split)
  19.312  
  19.313  lemma min_Suc2:
  19.314     "min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))"
  19.315 -  by (simp split: nat.split)
  19.316 +by (simp split: nat.split)
  19.317  
  19.318  lemma max_0L [simp]: "max 0 n = (n::nat)"
  19.319 -  by (rule max_leastL) simp
  19.320 +by (rule max_leastL) simp
  19.321  
  19.322  lemma max_0R [simp]: "max n 0 = (n::nat)"
  19.323 -  by (rule max_leastR) simp
  19.324 +by (rule max_leastR) simp
  19.325  
  19.326  lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
  19.327 -  by (simp add: mono_Suc max_of_mono)
  19.328 +by (simp add: mono_Suc max_of_mono)
  19.329  
  19.330  lemma max_Suc1:
  19.331     "max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
  19.332 -  by (simp split: nat.split)
  19.333 +by (simp split: nat.split)
  19.334  
  19.335  lemma max_Suc2:
  19.336     "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
  19.337 -  by (simp split: nat.split)
  19.338 +by (simp split: nat.split)
  19.339  
  19.340  
  19.341  subsection {* Basic rewrite rules for the arithmetic operators *}
  19.342 @@ -591,10 +592,10 @@
  19.343  text {* Difference *}
  19.344  
  19.345  lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
  19.346 -  by (induct n) simp_all
  19.347 +by (induct n) simp_all
  19.348  
  19.349  lemma diff_Suc_Suc [simp, code]: "Suc(m) - Suc(n) = m - n"
  19.350 -  by (induct n) simp_all
  19.351 +by (induct n) simp_all
  19.352  
  19.353  
  19.354  text {*
  19.355 @@ -602,7 +603,7 @@
  19.356    However, none of the generalizations are currently in the simpset,
  19.357    and I dread to think what happens if I put them in
  19.358  *}
  19.359 -lemma Suc_pred [simp]: "0 \<noteq> n ==> Suc (n - Suc 0) = n"
  19.360 +lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
  19.361  by (simp split add: nat.split)
  19.362  
  19.363  declare diff_Suc [simp del, code del]
  19.364 @@ -611,22 +612,22 @@
  19.365  subsection {* Addition *}
  19.366  
  19.367  lemma add_0_right [simp]: "m + 0 = (m::nat)"
  19.368 -  by (induct m) simp_all
  19.369 +by (induct m) simp_all
  19.370  
  19.371  lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
  19.372 -  by (induct m) simp_all
  19.373 +by (induct m) simp_all
  19.374  
  19.375  lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
  19.376 -  by simp
  19.377 +by simp
  19.378  
  19.379  
  19.380  text {* Associative law for addition *}
  19.381  lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)"
  19.382 -  by (induct m) simp_all
  19.383 +by (induct m) simp_all
  19.384  
  19.385  text {* Commutative law for addition *}
  19.386  lemma nat_add_commute: "m + n = n + (m::nat)"
  19.387 -  by (induct m) simp_all
  19.388 +by (induct m) simp_all
  19.389  
  19.390  lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
  19.391    apply (rule mk_left_commute [of "op +"])
  19.392 @@ -635,30 +636,30 @@
  19.393    done
  19.394  
  19.395  lemma nat_add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))"
  19.396 -  by (induct k) simp_all
  19.397 +by (induct k) simp_all
  19.398  
  19.399  lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))"
  19.400 -  by (induct k) simp_all
  19.401 +by (induct k) simp_all
  19.402  
  19.403  lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
  19.404 -  by (induct k) simp_all
  19.405 +by (induct k) simp_all
  19.406  
  19.407  lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"
  19.408 -  by (induct k) simp_all
  19.409 +by (induct k) simp_all
  19.410  
  19.411  text {* Reasoning about @{text "m + 0 = 0"}, etc. *}
  19.412  
  19.413  lemma add_is_0 [iff]: fixes m :: nat shows "(m + n = 0) = (m = 0 & n = 0)"
  19.414 -  by (cases m) simp_all
  19.415 +by (cases m) simp_all
  19.416  
  19.417  lemma add_is_1: "(m+n= Suc 0) = (m= Suc 0 & n=0 | m=0 & n= Suc 0)"
  19.418 -  by (cases m) simp_all
  19.419 +by (cases m) simp_all
  19.420  
  19.421  lemma one_is_add: "(Suc 0 = m + n) = (m = Suc 0 & n = 0 | m = 0 & n = Suc 0)"
  19.422 -  by (rule trans, rule eq_commute, rule add_is_1)
  19.423 +by (rule trans, rule eq_commute, rule add_is_1)
  19.424  
  19.425 -lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m\<noteq>0 | n\<noteq>0)"
  19.426 -by (simp add:gr0_conv)
  19.427 +lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m>0 | n>0)"
  19.428 +by(auto dest:gr0_implies_Suc)
  19.429  
  19.430  lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0"
  19.431    apply (drule add_0_right [THEN ssubst])
  19.432 @@ -677,26 +678,26 @@
  19.433  
  19.434  text {* right annihilation in product *}
  19.435  lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
  19.436 -  by (induct m) simp_all
  19.437 +by (induct m) simp_all
  19.438  
  19.439  text {* right successor law for multiplication *}
  19.440  lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
  19.441 -  by (induct m) (simp_all add: nat_add_left_commute)
  19.442 +by (induct m) (simp_all add: nat_add_left_commute)
  19.443  
  19.444  text {* Commutative law for multiplication *}
  19.445  lemma nat_mult_commute: "m * n = n * (m::nat)"
  19.446 -  by (induct m) simp_all
  19.447 +by (induct m) simp_all
  19.448  
  19.449  text {* addition distributes over multiplication *}
  19.450  lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
  19.451 -  by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute)
  19.452 +by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute)
  19.453  
  19.454  lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
  19.455 -  by (induct m) (simp_all add: nat_add_assoc)
  19.456 +by (induct m) (simp_all add: nat_add_assoc)
  19.457  
  19.458  text {* Associative law for multiplication *}
  19.459  lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
  19.460 -  by (induct m) (simp_all add: add_mult_distrib)
  19.461 +by (induct m) (simp_all add: add_mult_distrib)
  19.462  
  19.463  
  19.464  text{*The naturals form a @{text comm_semiring_1_cancel}*}
  19.465 @@ -725,7 +726,7 @@
  19.466  
  19.467  text {* strict, in 1st argument *}
  19.468  lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
  19.469 -  by (induct k) simp_all
  19.470 +by (induct k) simp_all
  19.471  
  19.472  text {* strict, in both arguments *}
  19.473  lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
  19.474 @@ -759,10 +760,10 @@
  19.475  qed
  19.476  
  19.477  lemma nat_mult_1: "(1::nat) * n = n"
  19.478 -  by simp
  19.479 +by simp
  19.480  
  19.481  lemma nat_mult_1_right: "n * (1::nat) = n"
  19.482 -  by simp
  19.483 +by simp
  19.484  
  19.485  
  19.486  subsection {* Additional theorems about "less than" *}
  19.487 @@ -1083,7 +1084,7 @@
  19.488  by (simp add: linorder_not_less [symmetric], auto)
  19.489  
  19.490  lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
  19.491 -apply (cut_tac less_linear, safe, auto simp add: neq0_conv)
  19.492 +apply (cut_tac less_linear, safe, auto)
  19.493  apply (drule mult_less_mono1, assumption, simp)+
  19.494  done
  19.495  
  19.496 @@ -1105,7 +1106,7 @@
  19.497    apply (rule disjCI)
  19.498    apply (rule nat_less_cases, erule_tac [2] _)
  19.499     apply (drule_tac [2] mult_less_mono2)
  19.500 -    apply (auto simp add: neq0_conv)
  19.501 +    apply (auto)
  19.502    done
  19.503  
  19.504  
  19.505 @@ -1119,7 +1120,7 @@
  19.506  setup Size.setup
  19.507  
  19.508  lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
  19.509 -  by (induct n) simp_all
  19.510 +by (induct n) simp_all
  19.511  
  19.512  lemma size_bool [code func]:
  19.513    "size (b\<Colon>bool) = 0" by (cases b) auto
  19.514 @@ -1136,7 +1137,7 @@
  19.515    "Suc n = Suc m \<longleftrightarrow> n = m"
  19.516    "Suc n = 0 \<longleftrightarrow> False"
  19.517    "0 = Suc m \<longleftrightarrow> False"
  19.518 -  by auto
  19.519 +by auto
  19.520  
  19.521  lemma [code func]:
  19.522    "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
  19.523 @@ -1186,7 +1187,7 @@
  19.524  by (cases "a<b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
  19.525  
  19.526  lemma nat_diff_split_asm:
  19.527 -    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
  19.528 +  "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
  19.529      -- {* elimination of @{text -} on @{text nat} in assumptions *}
  19.530  by (simp split: nat_diff_split)
  19.531  
  19.532 @@ -1378,7 +1379,7 @@
  19.533    done
  19.534  
  19.535  lemma of_nat_less_iff [simp]:
  19.536 -    "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
  19.537 +  "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
  19.538  by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
  19.539  
  19.540  text{*Special cases where either operand is zero*}
  19.541 @@ -1390,7 +1391,7 @@
  19.542  by (rule of_nat_less_iff [of _ 0, simplified])
  19.543  
  19.544  lemma of_nat_le_iff [simp]:
  19.545 -    "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
  19.546 +  "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
  19.547  by (simp add: linorder_not_less [symmetric])
  19.548  
  19.549  text{*Special cases where either operand is zero*}
  19.550 @@ -1420,7 +1421,7 @@
  19.551  by (simp add: inj_on_def)
  19.552  
  19.553  lemma of_nat_diff:
  19.554 -    "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
  19.555 +  "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
  19.556  by (simp del: of_nat_add
  19.557      add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
  19.558  
    20.1 --- a/src/HOL/Power.thy	Tue Oct 23 22:48:25 2007 +0200
    20.2 +++ b/src/HOL/Power.thy	Tue Oct 23 23:27:23 2007 +0200
    20.3 @@ -140,7 +140,7 @@
    20.4  done
    20.5  
    20.6  lemma power_eq_0_iff [simp]:
    20.7 -  "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n\<noteq>0)"
    20.8 +  "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n>0)"
    20.9  apply (induct "n")
   20.10  apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
   20.11  done
   20.12 @@ -342,7 +342,7 @@
   20.13  lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
   20.14  by (insert one_le_power [of i n], simp)
   20.15  
   20.16 -lemma nat_zero_less_power_iff [simp]: "(x^n = 0) = (x = (0::nat) & n\<noteq>0)"
   20.17 +lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
   20.18  by (induct "n", auto)
   20.19  
   20.20  text{*Valid for the naturals, but what if @{text"0<i<1"}?
    21.1 --- a/src/HOL/Real/RComplete.thy	Tue Oct 23 22:48:25 2007 +0200
    21.2 +++ b/src/HOL/Real/RComplete.thy	Tue Oct 23 23:27:23 2007 +0200
    21.3 @@ -1208,10 +1208,10 @@
    21.4    apply simp
    21.5  done
    21.6  
    21.7 -lemma natfloor_div_nat: "1 <= x ==> y \<noteq> 0 ==>
    21.8 +lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
    21.9    natfloor (x / real y) = natfloor x div y"
   21.10  proof -
   21.11 -  assume "1 <= (x::real)" and "(y::nat) \<noteq> 0"
   21.12 +  assume "1 <= (x::real)" and "(y::nat) > 0"
   21.13    have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
   21.14      by simp
   21.15    then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
    22.1 --- a/src/HOL/Real/RealDef.thy	Tue Oct 23 22:48:25 2007 +0200
    22.2 +++ b/src/HOL/Real/RealDef.thy	Tue Oct 23 23:27:23 2007 +0200
    22.3 @@ -746,7 +746,7 @@
    22.4  lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
    22.5  by (simp add: add: real_of_nat_def of_nat_diff)
    22.6  
    22.7 -lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (n \<noteq> 0)"
    22.8 +lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
    22.9  by (auto simp: real_of_nat_def)
   22.10  
   22.11  lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)"
    23.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Tue Oct 23 22:48:25 2007 +0200
    23.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Tue Oct 23 23:27:23 2007 +0200
    23.3 @@ -63,7 +63,7 @@
    23.4    "fmsize (NDvd i t) = 2"
    23.5    "fmsize p = 1"
    23.6    (* several lemmas about fmsize *)
    23.7 -lemma fmsize_pos: "fmsize p \<noteq> 0"	
    23.8 +lemma fmsize_pos: "fmsize p > 0"	
    23.9  by (induct p rule: fmsize.induct) simp_all
   23.10  
   23.11    (* Semantics of formulae (fm) *)
   23.12 @@ -114,7 +114,7 @@
   23.13    "prep (Imp p q) = prep (Or (NOT p) q)"
   23.14    "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   23.15    "prep p = p"
   23.16 -(hints simp add: fmsize_pos neq0_conv[symmetric])
   23.17 +(hints simp add: fmsize_pos)
   23.18  lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
   23.19  by (induct p arbitrary: bs rule: prep.induct, auto)
   23.20  
   23.21 @@ -189,11 +189,11 @@
   23.22  
   23.23  lemma numsubst0_I:
   23.24    "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
   23.25 -by (induct t rule: numsubst0.induct,auto dest: not0_implies_Suc)
   23.26 +by (induct t rule: numsubst0.induct,auto simp:nth_Cons')
   23.27  
   23.28  lemma numsubst0_I':
   23.29    "numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
   23.30 -by (induct t rule: numsubst0.induct, auto dest: not0_implies_Suc simp: numbound0_I[where b="b" and b'="b'"])
   23.31 +by (induct t rule: numsubst0.induct, auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
   23.32  
   23.33  primrec
   23.34    "subst0 t T = T"