Eliminated most of the neq0_conv occurrences. As a result, many
authornipkow
Sun Oct 21 14:53:44 2007 +0200 (2007-10-21)
changeset 251343d4953e88449
parent 25133 b933700f0384
child 25135 4f8176c940cf
Eliminated most of the neq0_conv occurrences. As a result, many
theorems had to be rephrased with ~= 0 instead of > 0.
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Auth/Guard/Guard.thy
src/HOL/Auth/Guard/GuardK.thy
src/HOL/Auth/Kerberos_BAN.thy
src/HOL/Complex/ex/MIR.thy
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/Divides.thy
src/HOL/Hyperreal/Fact.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/Hyperreal/Taylor.thy
src/HOL/IntDiv.thy
src/HOL/Library/Binomial.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Nat_Infinity.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/RealDef.thy
src/HOL/Word/BinBoolList.thy
src/HOL/Word/BinGeneral.thy
src/HOL/Word/WordArith.thy
src/HOL/ex/Reflected_Presburger.thy
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Sun Oct 21 14:21:54 2007 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Sun Oct 21 14:53:44 2007 +0200
     1.3 @@ -9,9 +9,8 @@
     1.4  
     1.5  
     1.6  section {*The Combinatorial Argument Underlying the First Sylow Theorem*}
     1.7 -constdefs
     1.8 -  exponent      :: "[nat, nat] => nat"
     1.9 -  "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
    1.10 +definition exponent :: "nat => nat => nat" where
    1.11 +"exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
    1.12  
    1.13  
    1.14  subsection{*Prime Theorems*}
    1.15 @@ -20,7 +19,7 @@
    1.16  by (unfold prime_def, force)
    1.17  
    1.18  lemma prime_iff:
    1.19 -     "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
    1.20 +  "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
    1.21  apply (auto simp add: prime_imp_one_less)
    1.22  apply (blast dest!: prime_dvd_mult)
    1.23  apply (auto simp add: prime_def)
    1.24 @@ -40,8 +39,8 @@
    1.25  
    1.26  
    1.27  lemma prime_dvd_cases:
    1.28 -     "[| p*k dvd m*n;  prime p |]  
    1.29 -      ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
    1.30 +  "[| p*k dvd m*n;  prime p |]  
    1.31 +   ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
    1.32  apply (simp add: prime_iff)
    1.33  apply (frule dvd_mult_left)
    1.34  apply (subgoal_tac "p dvd m | p dvd n")
    1.35 @@ -55,8 +54,8 @@
    1.36  
    1.37  
    1.38  lemma prime_power_dvd_cases [rule_format (no_asm)]: "prime p
    1.39 -      ==> \<forall>m n. p^c dvd m*n -->  
    1.40 -          (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
    1.41 +  ==> \<forall>m n. p^c dvd m*n -->  
    1.42 +        (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
    1.43  apply (induct_tac "c")
    1.44   apply clarify
    1.45   apply (case_tac "a")
    1.46 @@ -85,8 +84,8 @@
    1.47  
    1.48  (*needed in this form in Sylow.ML*)
    1.49  lemma div_combine:
    1.50 -     "[| prime p; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |]  
    1.51 -      ==> p ^ a dvd k"
    1.52 +  "[| prime p; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |]  
    1.53 +   ==> p ^ a dvd k"
    1.54  by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto)
    1.55  
    1.56  (*Lemma for power_dvd_bound*)
    1.57 @@ -96,15 +95,12 @@
    1.58  apply simp
    1.59  apply (subgoal_tac "2 * n + 2 <= p * p^n", simp)
    1.60  apply (subgoal_tac "2 * p^n <= p * p^n")
    1.61 -(*?arith_tac should handle all of this!*)
    1.62 -apply (rule order_trans)
    1.63 -prefer 2 apply assumption
    1.64 +apply arith
    1.65  apply (drule_tac k = 2 in mult_le_mono2, simp)
    1.66 -apply (rule mult_le_mono1, simp)
    1.67  done
    1.68  
    1.69  (*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
    1.70 -lemma power_dvd_bound: "[|p^n dvd a;  Suc 0 < p;  0 < a|] ==> n < a"
    1.71 +lemma power_dvd_bound: "[|p^n dvd a;  Suc 0 < p;  a \<noteq> 0|] ==> n < a"
    1.72  apply (drule dvd_imp_le)
    1.73  apply (drule_tac [2] n = n in Suc_le_power, auto)
    1.74  done
    1.75 @@ -113,13 +109,13 @@
    1.76  subsection{*Exponent Theorems*}
    1.77  
    1.78  lemma exponent_ge [rule_format]:
    1.79 -     "[|p^k dvd n;  prime p;  0<n|] ==> k <= exponent p n"
    1.80 +  "[|p^k dvd n;  prime p;  0<n|] ==> k <= exponent p n"
    1.81  apply (simp add: exponent_def)
    1.82  apply (erule Greatest_le)
    1.83  apply (blast dest: prime_imp_one_less power_dvd_bound)
    1.84  done
    1.85  
    1.86 -lemma power_exponent_dvd: "0<s ==> (p ^ exponent p s) dvd s"
    1.87 +lemma power_exponent_dvd: "s\<noteq>0 ==> (p ^ exponent p s) dvd s"
    1.88  apply (simp add: exponent_def)
    1.89  apply clarify
    1.90  apply (rule_tac k = 0 in GreatestI)
    1.91 @@ -127,7 +123,7 @@
    1.92  done
    1.93  
    1.94  lemma power_Suc_exponent_Not_dvd:
    1.95 -     "[|(p * p ^ exponent p s) dvd s;  prime p |] ==> s=0"
    1.96 +  "[|(p * p ^ exponent p s) dvd s;  prime p |] ==> s=0"
    1.97  apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
    1.98   prefer 2 apply simp 
    1.99  apply (rule ccontr)
   1.100 @@ -141,7 +137,7 @@
   1.101  done
   1.102  
   1.103  lemma exponent_equalityI:
   1.104 -     "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
   1.105 +  "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
   1.106  by (simp (no_asm_simp) add: exponent_def)
   1.107  
   1.108  lemma exponent_eq_0 [simp]: "\<not> prime p ==> exponent p s = 0"
   1.109 @@ -149,9 +145,8 @@
   1.110  
   1.111  
   1.112  (* exponent_mult_add, easy inclusion.  Could weaken p \<in> prime to Suc 0 < p *)
   1.113 -lemma exponent_mult_add1:
   1.114 -     "[| 0 < a; 0 < b |]   
   1.115 -      ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
   1.116 +lemma exponent_mult_add1: "[| a \<noteq> 0; b \<noteq> 0 |]
   1.117 +  ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
   1.118  apply (case_tac "prime p")
   1.119  apply (rule exponent_ge)
   1.120  apply (auto simp add: power_add)
   1.121 @@ -159,8 +154,8 @@
   1.122  done
   1.123  
   1.124  (* exponent_mult_add, opposite inclusion *)
   1.125 -lemma exponent_mult_add2: "[| 0 < a; 0 < b |]  
   1.126 -      ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
   1.127 +lemma exponent_mult_add2: "[| a \<noteq> 0; b \<noteq> 0 |]  
   1.128 +  ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
   1.129  apply (case_tac "prime p")
   1.130  apply (rule leI, clarify)
   1.131  apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto)
   1.132 @@ -173,9 +168,8 @@
   1.133  apply (blast dest: power_Suc_exponent_Not_dvd)
   1.134  done
   1.135  
   1.136 -lemma exponent_mult_add:
   1.137 -     "[| 0 < a; 0 < b |]  
   1.138 -      ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
   1.139 +lemma exponent_mult_add: "[| a \<noteq> 0; b \<noteq> 0 |]
   1.140 +   ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
   1.141  by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym)
   1.142  
   1.143  
   1.144 @@ -194,40 +188,41 @@
   1.145  
   1.146  subsection{*Main Combinatorial Argument*}
   1.147  
   1.148 -lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
   1.149 +lemma le_extend_mult: "[| c \<noteq> 0; a <= b |] ==> a <= b * (c::nat)"
   1.150  apply (rule_tac P = "%x. x <= b * c" in subst)
   1.151  apply (rule mult_1_right)
   1.152  apply (rule mult_le_mono, auto)
   1.153  done
   1.154  
   1.155  lemma p_fac_forw_lemma:
   1.156 -     "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
   1.157 +  "[| (m::nat) \<noteq> 0; k \<noteq> 0; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
   1.158  apply (rule notnotD)
   1.159  apply (rule notI)
   1.160  apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
   1.161  apply (drule less_imp_le [of a])
   1.162  apply (drule le_imp_power_dvd)
   1.163  apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
   1.164 -apply (metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less)
   1.165 +apply(metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less neq0_conv)
   1.166  done
   1.167  
   1.168 -lemma p_fac_forw: "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |]  
   1.169 -      ==> (p^r) dvd (p^a) - k"
   1.170 +lemma p_fac_forw: "[| (m::nat) \<noteq> 0; k\<noteq>0; k < p^a; (p^r) dvd (p^a)* m - k |]  
   1.171 +  ==> (p^r) dvd (p^a) - k"
   1.172  apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto)
   1.173  apply (subgoal_tac "p^r dvd p^a*m")
   1.174   prefer 2 apply (blast intro: dvd_mult2)
   1.175  apply (drule dvd_diffD1)
   1.176    apply assumption
   1.177   prefer 2 apply (blast intro: dvd_diff)
   1.178 -apply (drule less_imp_Suc_add, auto)
   1.179 +apply (drule not0_implies_Suc, auto)
   1.180  done
   1.181  
   1.182  
   1.183 -lemma r_le_a_forw: "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a"
   1.184 +lemma r_le_a_forw:
   1.185 +  "[| (k::nat) \<noteq> 0; k < p^a; p\<noteq>0; (p^r) dvd (p^a) - k |] ==> r <= a"
   1.186  by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
   1.187  
   1.188 -lemma p_fac_backw: "[| 0<m; 0<k; 0 < (p::nat);  k < p^a;  (p^r) dvd p^a - k |]  
   1.189 -      ==> (p^r) dvd (p^a)*m - k"
   1.190 +lemma p_fac_backw: "[| m\<noteq>0; k\<noteq>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]  
   1.191 +  ==> (p^r) dvd (p^a)*m - k"
   1.192  apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
   1.193  apply (subgoal_tac "p^r dvd p^a*m")
   1.194   prefer 2 apply (blast intro: dvd_mult2)
   1.195 @@ -237,8 +232,8 @@
   1.196  apply (drule less_imp_Suc_add, auto)
   1.197  done
   1.198  
   1.199 -lemma exponent_p_a_m_k_equation: "[| 0<m; 0<k; 0 < (p::nat);  k < p^a |]  
   1.200 -      ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
   1.201 +lemma exponent_p_a_m_k_equation: "[| m\<noteq>0; k\<noteq>0; (p::nat)\<noteq>0;  k < p^a |]  
   1.202 +  ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
   1.203  apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
   1.204  done
   1.205  
   1.206 @@ -247,14 +242,14 @@
   1.207  
   1.208  (*The bound K is needed; otherwise it's too weak to be used.*)
   1.209  lemma p_not_div_choose_lemma [rule_format]:
   1.210 -     "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]  
   1.211 -      ==> k<K --> exponent p ((j+k) choose k) = 0"
   1.212 +  "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]  
   1.213 +   ==> k<K --> exponent p ((j+k) choose k) = 0"
   1.214  apply (case_tac "prime p")
   1.215   prefer 2 apply simp 
   1.216  apply (induct_tac "k")
   1.217  apply (simp (no_asm))
   1.218  (*induction step*)
   1.219 -apply (subgoal_tac "0 < (Suc (j+n) choose Suc n) ")
   1.220 +apply (subgoal_tac "(Suc (j+n) choose Suc n) \<noteq> 0")
   1.221   prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
   1.222  apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) = 
   1.223                      exponent p (Suc n)")
   1.224 @@ -271,9 +266,9 @@
   1.225  
   1.226  (*The lemma above, with two changes of variables*)
   1.227  lemma p_not_div_choose:
   1.228 -     "[| k<K;  k<=n;   
   1.229 -       \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]  
   1.230 -      ==> exponent p (n choose k) = 0"
   1.231 +  "[| k<K;  k<=n;
   1.232 +      \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]
   1.233 +   ==> exponent p (n choose k) = 0"
   1.234  apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma)
   1.235    prefer 3 apply simp
   1.236   prefer 2 apply assumption
   1.237 @@ -283,7 +278,7 @@
   1.238  
   1.239  
   1.240  lemma const_p_fac_right:
   1.241 -     "0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
   1.242 +  "m\<noteq>0 ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
   1.243  apply (case_tac "prime p")
   1.244   prefer 2 apply simp 
   1.245  apply (frule_tac a = a in zero_less_prime_power)
   1.246 @@ -301,7 +296,7 @@
   1.247  done
   1.248  
   1.249  lemma const_p_fac:
   1.250 -     "0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
   1.251 +  "m\<noteq>0 ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
   1.252  apply (case_tac "prime p")
   1.253   prefer 2 apply simp 
   1.254  apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
     2.1 --- a/src/HOL/Algebra/Sylow.thy	Sun Oct 21 14:21:54 2007 +0200
     2.2 +++ b/src/HOL/Algebra/Sylow.thy	Sun Oct 21 14:53:44 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: "0 < m"
     2.8 +lemma (in sylow) zero_less_m: "m \<noteq> 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: "0 < card calM"
    2.17 +lemma (in sylow) zero_less_card_calM: "card calM \<noteq> 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/Auth/Guard/Guard.thy	Sun Oct 21 14:21:54 2007 +0200
     3.2 +++ b/src/HOL/Auth/Guard/Guard.thy	Sun Oct 21 14:53:44 2007 +0200
     3.3 @@ -187,7 +187,7 @@
     3.4  
     3.5  subsection{*basic facts about @{term crypt_nb}*}
     3.6  
     3.7 -lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> 0 < crypt_nb X"
     3.8 +lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> crypt_nb X \<noteq> 0"
     3.9  by (induct X, simp_all, safe, simp_all)
    3.10  
    3.11  subsection{*number of Crypt's in a message list*}
    3.12 @@ -216,7 +216,7 @@
    3.13  cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
    3.14  by (erule parts.induct, auto simp: in_set_conv_decomp)
    3.15  
    3.16 -lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> 0 < cnb l"
    3.17 +lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> cnb l \<noteq> 0"
    3.18  by (induct l, auto dest: non_empty_crypt_msg parts_insert_substD)
    3.19  
    3.20  subsection{*list of kparts*}
     4.1 --- a/src/HOL/Auth/Guard/GuardK.thy	Sun Oct 21 14:21:54 2007 +0200
     4.2 +++ b/src/HOL/Auth/Guard/GuardK.thy	Sun Oct 21 14:53:44 2007 +0200
     4.3 @@ -183,7 +183,7 @@
     4.4  
     4.5  subsection{*basic facts about @{term crypt_nb}*}
     4.6  
     4.7 -lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> 0 < crypt_nb X"
     4.8 +lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> crypt_nb X \<noteq> 0"
     4.9  by (induct X, simp_all, safe, simp_all)
    4.10  
    4.11  subsection{*number of Crypt's in a message list*}
    4.12 @@ -212,7 +212,7 @@
    4.13  cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
    4.14  by (erule parts.induct, auto simp: in_set_conv_decomp)
    4.15  
    4.16 -lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> 0 < cnb l"
    4.17 +lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> cnb l \<noteq> 0"
    4.18  by (induct l, auto dest: non_empty_crypt_msg parts_insert_substD)
    4.19  
    4.20  subsection{*list of kparts*}
     5.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Sun Oct 21 14:21:54 2007 +0200
     5.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Sun Oct 21 14:53:44 2007 +0200
     5.3 @@ -35,7 +35,7 @@
     5.4  
     5.5  text{*The authenticator only for one journey*}
     5.6  specification (authlife)
     5.7 -  authlife_LB [iff]:    "0 < authlife"
     5.8 +  authlife_LB [iff]:    "authlife \<noteq> 0"
     5.9      by blast
    5.10  
    5.11  abbreviation
    5.12 @@ -133,7 +133,7 @@
    5.13  apply (rule_tac [2]
    5.14             bankerberos.Nil [THEN bankerberos.BK1, THEN bankerberos.BK2,
    5.15                               THEN bankerberos.BK3, THEN bankerberos.BK4])
    5.16 -apply (possibility, simp_all (no_asm_simp) add: used_Cons neq0_conv)
    5.17 +apply (possibility, simp_all (no_asm_simp) add: used_Cons)
    5.18  done
    5.19  
    5.20  subsection{*Lemmas for reasoning about predicate "Issues"*}
     6.1 --- a/src/HOL/Complex/ex/MIR.thy	Sun Oct 21 14:21:54 2007 +0200
     6.2 +++ b/src/HOL/Complex/ex/MIR.thy	Sun Oct 21 14:53:44 2007 +0200
     6.3 @@ -268,7 +268,7 @@
     6.4  | "fmsize (NDvd i t) = 2"
     6.5  | "fmsize p = 1"
     6.6    (* several lemmas about fmsize *)
     6.7 -lemma fmsize_pos: "fmsize p > 0"	
     6.8 +lemma fmsize_pos: "fmsize p \<noteq> 0"	
     6.9  by (induct p rule: fmsize.induct) simp_all
    6.10  
    6.11    (* Semantics of formulae (fm) *)
    6.12 @@ -316,7 +316,7 @@
    6.13    "prep (Imp p q) = prep (Or (NOT p) q)"
    6.14    "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
    6.15    "prep p = p"
    6.16 -(hints simp add: fmsize_pos)
    6.17 +(hints simp add: fmsize_pos neq0_conv[symmetric])
    6.18  lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
    6.19  by (induct p rule: prep.induct, auto)
    6.20  
     7.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Sun Oct 21 14:21:54 2007 +0200
     7.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Sun Oct 21 14:53:44 2007 +0200
     7.3 @@ -106,7 +106,7 @@
     7.4    "fmsize (A p) = 4+ fmsize p"
     7.5    "fmsize p = 1"
     7.6    (* several lemmas about fmsize *)
     7.7 -lemma fmsize_pos: "fmsize p > 0"	
     7.8 +lemma fmsize_pos: "fmsize p \<noteq> 0"
     7.9  by (induct p rule: fmsize.induct) simp_all
    7.10  
    7.11    (* Semantics of formulae (fm) *)
    7.12 @@ -917,7 +917,7 @@
    7.13    "prep (Imp p q) = prep (Or (NOT p) q)"
    7.14    "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
    7.15    "prep p = p"
    7.16 -(hints simp add: fmsize_pos)
    7.17 +(hints simp add: fmsize_pos neq0_conv[symmetric])
    7.18  lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
    7.19  by (induct p rule: prep.induct, auto)
    7.20  
     8.1 --- a/src/HOL/Divides.thy	Sun Oct 21 14:21:54 2007 +0200
     8.2 +++ b/src/HOL/Divides.thy	Sun Oct 21 14:53:44 2007 +0200
     8.3 @@ -250,13 +250,13 @@
     8.4    apply (simp add: quorem_def)
     8.5    done
     8.6  
     8.7 -lemma quorem_div_mod: "0 < b ==> quorem ((a, b), (a div b, a mod b))"
     8.8 +lemma quorem_div_mod: "b \<noteq> 0 ==> quorem ((a, b), (a div b, a mod b))"
     8.9    unfolding quorem_def by simp
    8.10  
    8.11 -lemma quorem_div: "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q"
    8.12 +lemma quorem_div: "[| quorem((a,b),(q,r));  b \<noteq> 0 |] ==> a div b = q"
    8.13    by (simp add: quorem_div_mod [THEN unique_quotient])
    8.14  
    8.15 -lemma quorem_mod: "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r"
    8.16 +lemma quorem_mod: "[| quorem((a,b),(q,r));  b \<noteq> 0 |] ==> a mod b = r"
    8.17    by (simp add: quorem_div_mod [THEN unique_remainder])
    8.18  
    8.19  (** A dividend of zero **)
    8.20 @@ -270,21 +270,19 @@
    8.21  (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
    8.22  
    8.23  lemma quorem_mult1_eq:
    8.24 -     "[| quorem((b,c),(q,r));  0 < c |]
    8.25 +     "[| quorem((b,c),(q,r)); c \<noteq> 0 |]
    8.26        ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
    8.27    by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
    8.28  
    8.29  lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
    8.30 -  apply (cases "c = 0", simp  add: neq0_conv)
    8.31 -  using neq0_conv
    8.32 -  apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
    8.33 -  done
    8.34 +apply (cases "c = 0", simp)
    8.35 +apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
    8.36 +done
    8.37  
    8.38  lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
    8.39 -  apply (cases "c = 0", simp add: neq0_conv)
    8.40 -  using neq0_conv
    8.41 -  apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
    8.42 -  done
    8.43 +apply (cases "c = 0", simp)
    8.44 +apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
    8.45 +done
    8.46  
    8.47  lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
    8.48    apply (rule trans)
    8.49 @@ -301,23 +299,21 @@
    8.50  (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
    8.51  
    8.52  lemma quorem_add1_eq:
    8.53 -     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |]
    8.54 +     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c \<noteq> 0 |]
    8.55        ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
    8.56    by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
    8.57  
    8.58  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
    8.59  lemma div_add1_eq:
    8.60 -     "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
    8.61 -  apply (cases "c = 0", simp)
    8.62 -  using neq0_conv
    8.63 -  apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
    8.64 -  done
    8.65 +  "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
    8.66 +apply (cases "c = 0", simp)
    8.67 +apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod)
    8.68 +done
    8.69  
    8.70  lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
    8.71 -  apply (cases "c = 0", simp)
    8.72 -  using neq0_conv
    8.73 -  apply (blast intro: quorem_div_mod quorem_div_mod quorem_add1_eq [THEN quorem_mod])
    8.74 -  done
    8.75 +apply (cases "c = 0", simp)
    8.76 +apply (blast intro: quorem_div_mod quorem_add1_eq [THEN quorem_mod])
    8.77 +done
    8.78  
    8.79  
    8.80  subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}
     9.1 --- a/src/HOL/Hyperreal/Fact.thy	Sun Oct 21 14:21:54 2007 +0200
     9.2 +++ b/src/HOL/Hyperreal/Fact.thy	Sun Oct 21 14:53:44 2007 +0200
     9.3 @@ -17,60 +17,60 @@
     9.4  
     9.5  
     9.6  lemma fact_gt_zero [simp]: "0 < fact n"
     9.7 -  by (induct n) auto
     9.8 +by (induct n) auto
     9.9  
    9.10  lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
    9.11 -  by (simp add: neq0_conv)
    9.12 +by (simp add: neq0_conv)
    9.13  
    9.14  lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
    9.15 -  by auto
    9.16 +by auto
    9.17  
    9.18  lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
    9.19 -  by auto
    9.20 +by auto
    9.21  
    9.22  lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
    9.23 -  by simp
    9.24 +by simp
    9.25  
    9.26  lemma fact_ge_one [simp]: "1 \<le> fact n"
    9.27 -  by (induct n) auto
    9.28 +by (induct n) auto
    9.29  
    9.30  lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
    9.31 -  apply (drule le_imp_less_or_eq)
    9.32 -  apply (auto dest!: less_imp_Suc_add)
    9.33 -  apply (induct_tac k, auto)
    9.34 -  done
    9.35 +apply (drule le_imp_less_or_eq)
    9.36 +apply (auto dest!: less_imp_Suc_add)
    9.37 +apply (induct_tac k, auto)
    9.38 +done
    9.39  
    9.40  text{*Note that @{term "fact 0 = fact 1"}*}
    9.41  lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
    9.42 -  apply (drule_tac m = m in less_imp_Suc_add, auto)
    9.43 -  apply (induct_tac k, auto)
    9.44 -  done
    9.45 +apply (drule_tac m = m in less_imp_Suc_add, auto)
    9.46 +apply (induct_tac k, auto)
    9.47 +done
    9.48  
    9.49  lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
    9.50 -  by (auto simp add: positive_imp_inverse_positive)
    9.51 +by (auto simp add: positive_imp_inverse_positive)
    9.52  
    9.53  lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
    9.54 -  by (auto intro: order_less_imp_le)
    9.55 +by (auto intro: order_less_imp_le)
    9.56  
    9.57  lemma fact_diff_Suc [rule_format]:
    9.58 -    "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
    9.59 -  apply (induct n arbitrary: m)
    9.60 -  apply auto
    9.61 -  apply (drule_tac x = "m - 1" in meta_spec, auto)
    9.62 -  done
    9.63 +  "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
    9.64 +apply (induct n arbitrary: m)
    9.65 +apply auto
    9.66 +apply (drule_tac x = "m - 1" in meta_spec, auto)
    9.67 +done
    9.68  
    9.69  lemma fact_num0 [simp]: "fact 0 = 1"
    9.70 -  by auto
    9.71 +by auto
    9.72  
    9.73  lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
    9.74 -  by (cases m) auto
    9.75 +by (cases m) auto
    9.76  
    9.77  lemma fact_add_num_eq_if:
    9.78 -    "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
    9.79 -  by (cases "m + n") auto
    9.80 +  "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
    9.81 +by (cases "m + n") auto
    9.82  
    9.83  lemma fact_add_num_eq_if2:
    9.84 -    "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
    9.85 -  by (cases m) auto
    9.86 +  "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
    9.87 +by (cases m) auto
    9.88  
    9.89  end
    10.1 --- a/src/HOL/Hyperreal/Integration.thy	Sun Oct 21 14:21:54 2007 +0200
    10.2 +++ b/src/HOL/Hyperreal/Integration.thy	Sun Oct 21 14:53:44 2007 +0200
    10.3 @@ -149,14 +149,13 @@
    10.4  apply (rule_tac t = a in partition_lhs [THEN subst], assumption)
    10.5  apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear)
    10.6  apply (frule partition [THEN iffD1], safe)
    10.7 -using neq0_conv
    10.8   apply (blast intro: partition_lt less_le_trans)
    10.9  apply (rotate_tac 3)
   10.10  apply (drule_tac x = "Suc n" in spec)
   10.11  apply (erule impE)
   10.12  apply (erule less_imp_le)
   10.13 -apply (frule partition_rhs, simp only: neq0_conv)
   10.14 -apply (drule partition_gt, assumption)
   10.15 +apply (frule partition_rhs)
   10.16 +apply (drule partition_gt[of _ _ _ 0], arith)
   10.17  apply (simp (no_asm_simp))
   10.18  done
   10.19  
    11.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Sun Oct 21 14:21:54 2007 +0200
    11.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Sun Oct 21 14:53:44 2007 +0200
    11.3 @@ -114,7 +114,7 @@
    11.4  done
    11.5  
    11.6  lemma Maclaurin:
    11.7 -   "[| 0 < h; 0 < n; diff 0 = f;
    11.8 +   "[| 0 < h; n \<noteq> 0; diff 0 = f;
    11.9         \<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |]
   11.10      ==> \<exists>t. 0 < t &
   11.11                t < h &
   11.12 @@ -185,13 +185,11 @@
   11.13  done
   11.14  
   11.15  lemma Maclaurin_objl:
   11.16 -     "0 < h & 0 < n & diff 0 = f &
   11.17 -       (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
   11.18 -    --> (\<exists>t. 0 < t &
   11.19 -              t < h &
   11.20 -              f h =
   11.21 -              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   11.22 -              diff n t / real (fact n) * h ^ n)"
   11.23 +  "0 < h & n\<noteq>0 & diff 0 = f &
   11.24 +  (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
   11.25 +   --> (\<exists>t. 0 < t & t < h &
   11.26 +            f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   11.27 +                  diff n t / real (fact n) * h ^ n)"
   11.28  by (blast intro: Maclaurin)
   11.29  
   11.30  
   11.31 @@ -220,7 +218,7 @@
   11.32  by (blast intro: Maclaurin2)
   11.33  
   11.34  lemma Maclaurin_minus:
   11.35 -   "[| h < 0; 0 < n; diff 0 = f;
   11.36 +   "[| h < 0; n \<noteq> 0; diff 0 = f;
   11.37         \<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t |]
   11.38      ==> \<exists>t. h < t &
   11.39                t < 0 &
   11.40 @@ -247,7 +245,7 @@
   11.41  done
   11.42  
   11.43  lemma Maclaurin_minus_objl:
   11.44 -     "(h < 0 & 0 < n & diff 0 = f &
   11.45 +     "(h < 0 & n \<noteq> 0 & diff 0 = f &
   11.46         (\<forall>m t.
   11.47            m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t))
   11.48      --> (\<exists>t. h < t &
   11.49 @@ -263,10 +261,10 @@
   11.50  (* not good for PVS sin_approx, cos_approx *)
   11.51  
   11.52  lemma Maclaurin_bi_le_lemma [rule_format]:
   11.53 -     "0 < n \<longrightarrow>
   11.54 -       diff 0 0 =
   11.55 -       (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
   11.56 -       diff n 0 * 0 ^ n / real (fact n)"
   11.57 +  "n\<noteq>0 \<longrightarrow>
   11.58 +   diff 0 0 =
   11.59 +   (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
   11.60 +   diff n 0 * 0 ^ n / real (fact n)"
   11.61  by (induct "n", auto)
   11.62  
   11.63  lemma Maclaurin_bi_le:
   11.64 @@ -278,17 +276,17 @@
   11.65                diff n t / real (fact n) * x ^ n"
   11.66  apply (case_tac "n = 0", force)
   11.67  apply (case_tac "x = 0")
   11.68 -apply (rule_tac x = 0 in exI)
   11.69 -apply (force simp add: neq0_conv Maclaurin_bi_le_lemma)
   11.70 -apply (cut_tac x = x and y = 0 in linorder_less_linear, auto simp add: neq0_conv)
   11.71 -txt{*Case 1, where @{term "x < 0"}*}
   11.72 -apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
   11.73 -apply (simp add: abs_if neq0_conv)
   11.74 -apply (rule_tac x = t in exI)
   11.75 -apply (simp add: abs_if)
   11.76 + apply (rule_tac x = 0 in exI)
   11.77 + apply (force simp add: Maclaurin_bi_le_lemma)
   11.78 +apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
   11.79 + txt{*Case 1, where @{term "x < 0"}*}
   11.80 + apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
   11.81 +  apply (simp add: abs_if)
   11.82 + apply (rule_tac x = t in exI)
   11.83 + apply (simp add: abs_if)
   11.84  txt{*Case 2, where @{term "0 < x"}*}
   11.85  apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_objl, safe)
   11.86 -apply (simp add: abs_if)
   11.87 + apply (simp add: abs_if)
   11.88  apply (rule_tac x = t in exI)
   11.89  apply (simp add: abs_if)
   11.90  done
   11.91 @@ -296,7 +294,7 @@
   11.92  lemma Maclaurin_all_lt:
   11.93       "[| diff 0 = f;
   11.94           \<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
   11.95 -        x ~= 0; 0 < n
   11.96 +        x ~= 0; n \<noteq> 0
   11.97        |] ==> \<exists>t. 0 < abs t & abs t < abs x &
   11.98                 f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   11.99                       (diff n t / real (fact n)) * x ^ n"
  11.100 @@ -310,7 +308,7 @@
  11.101  lemma Maclaurin_all_lt_objl:
  11.102       "diff 0 = f &
  11.103        (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
  11.104 -      x ~= 0 & 0 < n
  11.105 +      x ~= 0 & n \<noteq> 0
  11.106        --> (\<exists>t. 0 < abs t & abs t < abs x &
  11.107                 f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
  11.108                       (diff n t / real (fact n)) * x ^ n)"
  11.109 @@ -318,7 +316,7 @@
  11.110  
  11.111  lemma Maclaurin_zero [rule_format]:
  11.112       "x = (0::real)
  11.113 -      ==> 0 < n -->
  11.114 +      ==> n \<noteq> 0 -->
  11.115            (\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
  11.116            diff 0 0"
  11.117  by (induct n, auto)
  11.118 @@ -328,11 +326,11 @@
  11.119        |] ==> \<exists>t. abs t \<le> abs x &
  11.120                f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
  11.121                      (diff n t / real (fact n)) * x ^ n"
  11.122 -apply (insert linorder_le_less_linear [of n 0])
  11.123 -apply (erule disjE, force)
  11.124 +apply(cases "n=0")
  11.125 +apply (force)
  11.126  apply (case_tac "x = 0")
  11.127  apply (frule_tac diff = diff and n = n in Maclaurin_zero, assumption)
  11.128 -apply (drule gr_implies_not0 [THEN not0_implies_Suc])
  11.129 +apply (drule not0_implies_Suc)
  11.130  apply (rule_tac x = 0 in exI, force)
  11.131  apply (frule_tac diff = diff and n = n in Maclaurin_all_lt, auto)
  11.132  apply (rule_tac x = t in exI, auto)
  11.133 @@ -348,7 +346,7 @@
  11.134  
  11.135  subsection{*Version for Exponential Function*}
  11.136  
  11.137 -lemma Maclaurin_exp_lt: "[| x ~= 0; 0 < n |]
  11.138 +lemma Maclaurin_exp_lt: "[| x ~= 0; n \<noteq> 0 |]
  11.139        ==> (\<exists>t. 0 < abs t &
  11.140                  abs t < abs x &
  11.141                  exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
  11.142 @@ -375,19 +373,19 @@
  11.143  done
  11.144  
  11.145  lemma mod_exhaust_less_4:
  11.146 -     "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
  11.147 +  "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
  11.148  by auto
  11.149  
  11.150  lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
  11.151 -     "0 < n --> Suc (Suc (2 * n - 2)) = 2*n"
  11.152 +  "n\<noteq>0 --> Suc (Suc (2 * n - 2)) = 2*n"
  11.153  by (induct "n", auto)
  11.154  
  11.155  lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]:
  11.156 -     "0 < n --> Suc (Suc (4*n - 2)) = 4*n"
  11.157 +  "n\<noteq>0 --> Suc (Suc (4*n - 2)) = 4*n"
  11.158  by (induct "n", auto)
  11.159  
  11.160  lemma Suc_mult_two_diff_one [rule_format, simp]:
  11.161 -      "0 < n --> Suc (2 * n - 1) = 2*n"
  11.162 +  "n\<noteq>0 --> Suc (2 * n - 1) = 2*n"
  11.163  by (induct "n", auto)
  11.164  
  11.165  
  11.166 @@ -427,7 +425,7 @@
  11.167  
  11.168  
  11.169  lemma Maclaurin_sin_expansion3:
  11.170 -     "[| 0 < n; 0 < x |] ==>
  11.171 +     "[| n \<noteq> 0; 0 < x |] ==>
  11.172         \<exists>t. 0 < t & t < x &
  11.173         sin x =
  11.174         (\<Sum>m=0..<n. (if even m then 0
  11.175 @@ -493,7 +491,7 @@
  11.176  done
  11.177  
  11.178  lemma Maclaurin_cos_expansion2:
  11.179 -     "[| 0 < x; 0 < n |] ==>
  11.180 +     "[| 0 < x; n \<noteq> 0 |] ==>
  11.181         \<exists>t. 0 < t & t < x &
  11.182         cos x =
  11.183         (\<Sum>m=0..<n. (if even m
  11.184 @@ -512,7 +510,7 @@
  11.185  done
  11.186  
  11.187  lemma Maclaurin_minus_cos_expansion:
  11.188 -     "[| x < 0; 0 < n |] ==>
  11.189 +     "[| x < 0; n \<noteq> 0 |] ==>
  11.190         \<exists>t. x < t & t < 0 &
  11.191         cos x =
  11.192         (\<Sum>m=0..<n. (if even m
    12.1 --- a/src/HOL/Hyperreal/Poly.thy	Sun Oct 21 14:21:54 2007 +0200
    12.2 +++ b/src/HOL/Hyperreal/Poly.thy	Sun Oct 21 14:53:44 2007 +0200
    12.3 @@ -589,15 +589,14 @@
    12.4  declare real_mult_zero_disj_iff [simp]
    12.5  
    12.6  lemma pderiv_aux_iszero [rule_format, simp]:
    12.7 -    "\<forall>n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p"
    12.8 +  "\<forall>n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p"
    12.9  by (induct "p", auto)
   12.10  
   12.11  lemma pderiv_aux_iszero_num: "(number_of n :: nat) \<noteq> 0
   12.12 -      ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) =
   12.13 +  ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) =
   12.14        list_all (%c. c = 0) p)"
   12.15 -unfolding neq0_conv
   12.16 -apply (rule_tac n1 = "number_of n" and m1 = 0 in less_imp_Suc_add [THEN exE], force)
   12.17 -apply (rule_tac n1 = "0 + x" in pderiv_aux_iszero [THEN subst])
   12.18 +apply(drule  not0_implies_Suc, clarify)
   12.19 +apply (rule_tac n1 = "m" in pderiv_aux_iszero [THEN subst])
   12.20  apply (simp (no_asm_simp) del: pderiv_aux_iszero)
   12.21  done
   12.22  
   12.23 @@ -783,7 +782,7 @@
   12.24  declare pexp_one [simp]
   12.25  
   12.26  lemma lemma_order_root [rule_format]:
   12.27 -     "\<forall>p a. 0 < n & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
   12.28 +     "\<forall>p a. n \<noteq> 0 & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
   12.29               --> poly p a = 0"
   12.30  apply (induct "n", blast)
   12.31  apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
   12.32 @@ -794,8 +793,7 @@
   12.33  apply (simp add: poly_linear_divides del: pmult_Cons, safe)
   12.34  apply (drule_tac [!] a = a in order2)
   12.35  apply (rule ccontr)
   12.36 -apply (simp add: divides_def poly_mult fun_eq neq0_conv del: pmult_Cons, blast)
   12.37 -using neq0_conv 
   12.38 +apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
   12.39  apply (blast intro: lemma_order_root)
   12.40  done
   12.41  
   12.42 @@ -845,7 +843,7 @@
   12.43  
   12.44  (* FIXME: too too long! *)
   12.45  lemma lemma_order_pderiv [rule_format]:
   12.46 -     "\<forall>p q a. 0 < n &
   12.47 +     "\<forall>p q a. n \<noteq> 0 &
   12.48         poly (pderiv p) \<noteq> poly [] &
   12.49         poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q
   12.50         --> n = Suc (order a (pderiv p))"
   12.51 @@ -876,7 +874,7 @@
   12.52            (poly qa xa + - poly (pderiv q) xa) *
   12.53            (poly ([- a, 1] %^ n) xa *
   12.54             ((- a + xa) * (inverse (real (Suc n)) * real (Suc n))))")
   12.55 -apply (simp only: mult_ac)  
   12.56 +apply (simp only: mult_ac)
   12.57  apply (rotate_tac 2)
   12.58  apply (drule_tac x = xa in spec)
   12.59  apply (simp add: left_distrib mult_ac del: pmult_Cons)
   12.60 @@ -885,7 +883,7 @@
   12.61  lemma order_pderiv: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |]
   12.62        ==> (order a p = Suc (order a (pderiv p)))"
   12.63  apply (case_tac "poly p = poly []")
   12.64 -apply (auto simp add: neq0_conv  dest: pderiv_zero)
   12.65 +apply (auto dest: pderiv_zero)
   12.66  apply (drule_tac a = a and p = p in order_decomp)
   12.67  apply (blast intro: lemma_order_pderiv)
   12.68  done
    13.1 --- a/src/HOL/Hyperreal/Taylor.thy	Sun Oct 21 14:21:54 2007 +0200
    13.2 +++ b/src/HOL/Hyperreal/Taylor.thy	Sun Oct 21 14:53:44 2007 +0200
    13.3 @@ -15,7 +15,7 @@
    13.4  *}
    13.5  
    13.6  lemma taylor_up: 
    13.7 -  assumes INIT: "0 < n" "diff 0 = f"
    13.8 +  assumes INIT: "n\<noteq>0" "diff 0 = f"
    13.9    and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
   13.10    and INTERV: "a \<le> c" "c < b" 
   13.11    shows "\<exists> t. c < t & t < b & 
   13.12 @@ -24,7 +24,7 @@
   13.13  proof -
   13.14    from INTERV have "0 < b-c" by arith
   13.15    moreover 
   13.16 -  from INIT have "0<n" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
   13.17 +  from INIT have "n\<noteq>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
   13.18    moreover
   13.19    have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"  
   13.20    proof (intro strip)
   13.21 @@ -57,7 +57,7 @@
   13.22  qed
   13.23  
   13.24  lemma taylor_down:
   13.25 -  assumes INIT: "0 < n" "diff 0 = f"
   13.26 +  assumes INIT: "n\<noteq>0" "diff 0 = f"
   13.27    and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
   13.28    and INTERV: "a < c" "c \<le> b"
   13.29    shows "\<exists> t. a < t & t < c & 
   13.30 @@ -66,7 +66,7 @@
   13.31  proof -
   13.32    from INTERV have "a-c < 0" by arith
   13.33    moreover 
   13.34 -  from INIT have "0<n" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
   13.35 +  from INIT have "n\<noteq>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
   13.36    moreover
   13.37    have "ALL m t. m < n & a-c <= t & t <= 0 --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
   13.38    proof (rule allI impI)+
   13.39 @@ -97,7 +97,7 @@
   13.40  qed
   13.41  
   13.42  lemma taylor:
   13.43 -  assumes INIT: "0 < n" "diff 0 = f"
   13.44 +  assumes INIT: "n\<noteq>0" "diff 0 = f"
   13.45    and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
   13.46    and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" 
   13.47    shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
    14.1 --- a/src/HOL/IntDiv.thy	Sun Oct 21 14:21:54 2007 +0200
    14.2 +++ b/src/HOL/IntDiv.thy	Sun Oct 21 14:53:44 2007 +0200
    14.3 @@ -1316,34 +1316,34 @@
    14.4  
    14.5  
    14.6  theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
    14.7 -  apply (simp split add: split_nat)
    14.8 -  apply (rule iffI)
    14.9 -  apply (erule exE)
   14.10 -  apply (rule_tac x = "int x" in exI)
   14.11 -  apply simp
   14.12 -  apply (erule exE)
   14.13 -  apply (rule_tac x = "nat x" in exI)
   14.14 -  apply (erule conjE)
   14.15 -  apply (erule_tac x = "nat x" in allE)
   14.16 -  apply simp
   14.17 -  done
   14.18 +apply (simp split add: split_nat)
   14.19 +apply (rule iffI)
   14.20 +apply (erule exE)
   14.21 +apply (rule_tac x = "int x" in exI)
   14.22 +apply simp
   14.23 +apply (erule exE)
   14.24 +apply (rule_tac x = "nat x" in exI)
   14.25 +apply (erule conjE)
   14.26 +apply (erule_tac x = "nat x" in allE)
   14.27 +apply simp
   14.28 +done
   14.29  
   14.30  theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
   14.31 -  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
   14.32 +apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
   14.33      nat_0_le cong add: conj_cong)
   14.34 -  apply (rule iffI)
   14.35 -  apply iprover
   14.36 -  apply (erule exE)
   14.37 -  apply (case_tac "x=0")
   14.38 -  apply (rule_tac x=0 in exI)
   14.39 -  apply simp
   14.40 -  apply (case_tac "0 \<le> k")
   14.41 -  apply iprover
   14.42 -  apply (simp add: neq0_conv linorder_not_le)
   14.43 -  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   14.44 -  apply assumption
   14.45 -  apply (simp add: mult_ac)
   14.46 -  done
   14.47 +apply (rule iffI)
   14.48 +apply iprover
   14.49 +apply (erule exE)
   14.50 +apply (case_tac "x=0")
   14.51 +apply (rule_tac x=0 in exI)
   14.52 +apply simp
   14.53 +apply (case_tac "0 \<le> k")
   14.54 +apply iprover
   14.55 +apply (simp add: neq0_conv linorder_not_le)
   14.56 +apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   14.57 +apply assumption
   14.58 +apply (simp add: mult_ac)
   14.59 +done
   14.60  
   14.61  lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
   14.62  proof
    15.1 --- a/src/HOL/Library/Binomial.thy	Sun Oct 21 14:21:54 2007 +0200
    15.2 +++ b/src/HOL/Library/Binomial.thy	Sun Oct 21 14:53:44 2007 +0200
    15.3 @@ -21,50 +21,50 @@
    15.4                   (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
    15.5  
    15.6  lemma binomial_n_0 [simp]: "(n choose 0) = 1"
    15.7 -  by (cases n) simp_all
    15.8 +by (cases n) simp_all
    15.9  
   15.10  lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
   15.11 -  by simp
   15.12 +by simp
   15.13  
   15.14  lemma binomial_Suc_Suc [simp]:
   15.15 -    "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
   15.16 -  by simp
   15.17 +  "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
   15.18 +by simp
   15.19  
   15.20  lemma binomial_eq_0: "!!k. n < k ==> (n choose k) = 0"
   15.21 -  by (induct n) auto
   15.22 +by (induct n) auto
   15.23  
   15.24  declare binomial_0 [simp del] binomial_Suc [simp del]
   15.25  
   15.26  lemma binomial_n_n [simp]: "(n choose n) = 1"
   15.27 -  by (induct n) (simp_all add: binomial_eq_0)
   15.28 +by (induct n) (simp_all add: binomial_eq_0)
   15.29  
   15.30  lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n"
   15.31 -  by (induct n) simp_all
   15.32 +by (induct n) simp_all
   15.33  
   15.34  lemma binomial_1 [simp]: "(n choose Suc 0) = n"
   15.35 -  by (induct n) simp_all
   15.36 +by (induct n) simp_all
   15.37  
   15.38 -lemma zero_less_binomial: "k \<le> n ==> 0 < (n choose k)"
   15.39 -  by (induct n k rule: diff_induct) simp_all
   15.40 +lemma zero_less_binomial: "k \<le> n ==> (n choose k) \<noteq> 0"
   15.41 +by (induct n k rule: diff_induct) simp_all
   15.42  
   15.43  lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
   15.44 -  apply (safe intro!: binomial_eq_0)
   15.45 -  apply (erule contrapos_pp)
   15.46 -  apply (simp add: neq0_conv zero_less_binomial)
   15.47 -  done
   15.48 +apply (safe intro!: binomial_eq_0)
   15.49 +apply (erule contrapos_pp)
   15.50 +apply (simp add: zero_less_binomial)
   15.51 +done
   15.52  
   15.53 -lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)"
   15.54 -  by (simp add: neq0_conv  linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
   15.55 +lemma zero_less_binomial_iff: "(n choose k \<noteq> 0) = (k\<le>n)"
   15.56 +by (simp add: linorder_not_less binomial_eq_0_iff)
   15.57  
   15.58  (*Might be more useful if re-oriented*)
   15.59  lemma Suc_times_binomial_eq:
   15.60 -    "!!k. k \<le> n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
   15.61 -  apply (induct n)
   15.62 -  apply (simp add: binomial_0)
   15.63 -  apply (case_tac k)
   15.64 -  apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
   15.65 +  "!!k. k \<le> n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
   15.66 +apply (induct n)
   15.67 +apply (simp add: binomial_0)
   15.68 +apply (case_tac k)
   15.69 +apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
   15.70      binomial_eq_0)
   15.71 -  done
   15.72 +done
   15.73  
   15.74  text{*This is the well-known version, but it's harder to use because of the
   15.75    need to reason about division.*}
    16.1 --- a/src/HOL/Library/Multiset.thy	Sun Oct 21 14:21:54 2007 +0200
    16.2 +++ b/src/HOL/Library/Multiset.thy	Sun Oct 21 14:53:44 2007 +0200
    16.3 @@ -11,7 +11,7 @@
    16.4  
    16.5  subsection {* The type of multisets *}
    16.6  
    16.7 -typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}"
    16.8 +typedef 'a multiset = "{f::'a => nat. finite {x . f x \<noteq> 0}}"
    16.9  proof
   16.10    show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp
   16.11  qed
   16.12 @@ -38,7 +38,7 @@
   16.13  
   16.14  abbreviation
   16.15    Melem :: "'a => 'a multiset => bool"  ("(_/ :# _)" [50, 51] 50) where
   16.16 -  "a :# M == 0 < count M a"
   16.17 +  "a :# M == count M a \<noteq> 0"
   16.18  
   16.19  syntax
   16.20    "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
   16.21 @@ -300,7 +300,7 @@
   16.22  lemma rep_multiset_induct_aux:
   16.23    assumes 1: "P (\<lambda>a. (0::nat))"
   16.24      and 2: "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))"
   16.25 -  shows "\<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
   16.26 +  shows "\<forall>f. f \<in> multiset --> setsum f {x. f x \<noteq> 0} = n --> P f"
   16.27    apply (unfold multiset_def)
   16.28    apply (induct_tac n, simp, clarify)
   16.29     apply (subgoal_tac "f = (\<lambda>a.0)")
   16.30 @@ -309,7 +309,7 @@
   16.31     apply (rule ext, force, clarify)
   16.32    apply (frule setsum_SucD, clarify)
   16.33    apply (rename_tac a)
   16.34 -  apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}")
   16.35 +  apply (subgoal_tac "finite {x. (f (a := f a - 1)) x \<noteq> 0}")
   16.36     prefer 2
   16.37     apply (rule finite_subset)
   16.38      prefer 2
   16.39 @@ -323,10 +323,10 @@
   16.40     apply (erule ssubst, rule 2 [unfolded multiset_def], blast)
   16.41    apply (erule allE, erule impE, erule_tac [2] mp, blast)
   16.42    apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
   16.43 -  apply (subgoal_tac "{x. x \<noteq> a --> 0 < f x} = {x. 0 < f x}")
   16.44 +  apply (subgoal_tac "{x. x \<noteq> a --> f x \<noteq> 0} = {x. f x \<noteq> 0}")
   16.45     prefer 2
   16.46     apply blast
   16.47 -  apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x} - {a}")
   16.48 +  apply (subgoal_tac "{x. x \<noteq> a \<and> f x \<noteq> 0} = {x. f x \<noteq> 0} - {a}")
   16.49     prefer 2
   16.50     apply blast
   16.51    apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong)
    17.1 --- a/src/HOL/Library/Nat_Infinity.thy	Sun Oct 21 14:21:54 2007 +0200
    17.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Sun Oct 21 14:53:44 2007 +0200
    17.3 @@ -51,132 +51,132 @@
    17.4  subsection "Constructors"
    17.5  
    17.6  lemma Fin_0: "Fin 0 = 0"
    17.7 -  by (simp add: inat_defs split:inat_splits)
    17.8 +by (simp add: inat_defs split:inat_splits)
    17.9  
   17.10  lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
   17.11 -  by (simp add: inat_defs split:inat_splits)
   17.12 +by (simp add: inat_defs split:inat_splits)
   17.13  
   17.14  lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
   17.15 -  by (simp add: inat_defs split:inat_splits)
   17.16 +by (simp add: inat_defs split:inat_splits)
   17.17  
   17.18  lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)"
   17.19 -  by (simp add: inat_defs split:inat_splits)
   17.20 +by (simp add: inat_defs split:inat_splits)
   17.21  
   17.22  lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
   17.23 -  by (simp add: inat_defs split:inat_splits)
   17.24 +by (simp add: inat_defs split:inat_splits)
   17.25  
   17.26  lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
   17.27 -  by (simp add: inat_defs split:inat_splits)
   17.28 +by (simp add: inat_defs split:inat_splits)
   17.29  
   17.30  lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)"
   17.31 -  by (simp add: inat_defs split:inat_splits)
   17.32 +by (simp add: inat_defs split:inat_splits)
   17.33  
   17.34  
   17.35  subsection "Ordering relations"
   17.36  
   17.37  lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R"
   17.38 -  by (simp add: inat_defs split:inat_splits)
   17.39 +by (simp add: inat_defs split:inat_splits)
   17.40  
   17.41  lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)"
   17.42 -  by (simp add: inat_defs split:inat_splits, arith)
   17.43 +by (simp add: inat_defs split:inat_splits, arith)
   17.44  
   17.45  lemma iless_not_refl [simp]: "\<not> n < (n::inat)"
   17.46 -  by (simp add: inat_defs split:inat_splits)
   17.47 +by (simp add: inat_defs split:inat_splits)
   17.48  
   17.49  lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)"
   17.50 -  by (simp add: inat_defs split:inat_splits)
   17.51 +by (simp add: inat_defs split:inat_splits)
   17.52  
   17.53  lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)"
   17.54 -  by (simp add: inat_defs split:inat_splits)
   17.55 +by (simp add: inat_defs split:inat_splits)
   17.56  
   17.57  lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)"
   17.58 -  by (simp add: inat_defs split:inat_splits)
   17.59 +by (simp add: inat_defs split:inat_splits)
   17.60  
   17.61  lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
   17.62 -  by (simp add: inat_defs split:inat_splits)
   17.63 +by (simp add: inat_defs split:inat_splits)
   17.64  
   17.65  lemma Infty_eq [simp]: "(n < \<infinity>) = (n \<noteq> \<infinity>)"
   17.66 -  by (simp add: inat_defs split:inat_splits)
   17.67 +by (simp add: inat_defs split:inat_splits)
   17.68  
   17.69  lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
   17.70 -  by (simp add: neq0_conv inat_defs split:inat_splits)
   17.71 +by (fastsimp simp: inat_defs split:inat_splits)
   17.72  
   17.73  lemma i0_iless_iSuc [simp]: "0 < iSuc n"
   17.74 -  by (simp add: inat_defs split:inat_splits)
   17.75 +by (simp add: inat_defs split:inat_splits)
   17.76  
   17.77  lemma not_ilessi0 [simp]: "\<not> n < (0::inat)"
   17.78 -  by (simp add: inat_defs split:inat_splits)
   17.79 +by (simp add: inat_defs split:inat_splits)
   17.80  
   17.81  lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
   17.82 -  by (simp add: inat_defs split:inat_splits)
   17.83 +by (simp add: inat_defs split:inat_splits)
   17.84  
   17.85  lemma iSuc_mono [simp]: "(iSuc n < iSuc m) = (n < m)"
   17.86 -  by (simp add: inat_defs split:inat_splits)
   17.87 +by (simp add: inat_defs split:inat_splits)
   17.88  
   17.89  
   17.90  
   17.91  lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
   17.92 -  by (simp add: inat_defs split:inat_splits, arith)
   17.93 +by (simp add: inat_defs split:inat_splits, arith)
   17.94  
   17.95  lemma ile_refl [simp]: "n \<le> (n::inat)"
   17.96 -  by (simp add: inat_defs split:inat_splits)
   17.97 +by (simp add: inat_defs split:inat_splits)
   17.98  
   17.99  lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)"
  17.100 -  by (simp add: inat_defs split:inat_splits)
  17.101 +by (simp add: inat_defs split:inat_splits)
  17.102  
  17.103  lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)"
  17.104 -  by (simp add: inat_defs split:inat_splits)
  17.105 +by (simp add: inat_defs split:inat_splits)
  17.106  
  17.107  lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)"
  17.108 -  by (simp add: inat_defs split:inat_splits)
  17.109 +by (simp add: inat_defs split:inat_splits)
  17.110  
  17.111  lemma Infty_ub [simp]: "n \<le> \<infinity>"
  17.112 -  by (simp add: inat_defs split:inat_splits)
  17.113 +by (simp add: inat_defs split:inat_splits)
  17.114  
  17.115  lemma i0_lb [simp]: "(0::inat) \<le> n"
  17.116 -  by (simp add: inat_defs split:inat_splits)
  17.117 +by (simp add: inat_defs split:inat_splits)
  17.118  
  17.119  lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R"
  17.120 -  by (simp add: inat_defs split:inat_splits)
  17.121 +by (simp add: inat_defs split:inat_splits)
  17.122  
  17.123  lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)"
  17.124 -  by (simp add: inat_defs split:inat_splits, arith)
  17.125 +by (simp add: inat_defs split:inat_splits, arith)
  17.126  
  17.127  lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)"
  17.128 -  by (simp add: inat_defs split:inat_splits)
  17.129 +by (simp add: inat_defs split:inat_splits)
  17.130  
  17.131  lemma ileI1: "m < n ==> iSuc m \<le> n"
  17.132 -  by (simp add: inat_defs split:inat_splits)
  17.133 +by (simp add: inat_defs split:inat_splits)
  17.134  
  17.135  lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)"
  17.136 -  by (simp add: inat_defs split:inat_splits, arith)
  17.137 +by (simp add: inat_defs split:inat_splits, arith)
  17.138  
  17.139  lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)"
  17.140 -  by (simp add: inat_defs split:inat_splits)
  17.141 +by (simp add: inat_defs split:inat_splits)
  17.142  
  17.143  lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)"
  17.144 -  by (simp add: inat_defs split:inat_splits, arith)
  17.145 +by (simp add: inat_defs split:inat_splits, arith)
  17.146  
  17.147  lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
  17.148 -  by (simp add: inat_defs split:inat_splits)
  17.149 +by (simp add: inat_defs split:inat_splits)
  17.150  
  17.151  lemma ile_iSuc [simp]: "n \<le> iSuc n"
  17.152 -  by (simp add: inat_defs split:inat_splits)
  17.153 +by (simp add: inat_defs split:inat_splits)
  17.154  
  17.155  lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k"
  17.156 -  by (simp add: inat_defs split:inat_splits)
  17.157 +by (simp add: inat_defs split:inat_splits)
  17.158  
  17.159  lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
  17.160 -  apply (induct_tac k)
  17.161 -   apply (simp (no_asm) only: Fin_0)
  17.162 -   apply (fast intro: ile_iless_trans i0_lb)
  17.163 -  apply (erule exE)
  17.164 -  apply (drule spec)
  17.165 -  apply (erule exE)
  17.166 -  apply (drule ileI1)
  17.167 -  apply (rule iSuc_Fin [THEN subst])
  17.168 -  apply (rule exI)
  17.169 -  apply (erule (1) ile_iless_trans)
  17.170 -  done
  17.171 +apply (induct_tac k)
  17.172 + apply (simp (no_asm) only: Fin_0)
  17.173 + apply (fast intro: ile_iless_trans i0_lb)
  17.174 +apply (erule exE)
  17.175 +apply (drule spec)
  17.176 +apply (erule exE)
  17.177 +apply (drule ileI1)
  17.178 +apply (rule iSuc_Fin [THEN subst])
  17.179 +apply (rule exI)
  17.180 +apply (erule (1) ile_iless_trans)
  17.181 +done
  17.182  
  17.183  end
    18.1 --- a/src/HOL/Library/Parity.thy	Sun Oct 21 14:21:54 2007 +0200
    18.2 +++ b/src/HOL/Library/Parity.thy	Sun Oct 21 14:53:44 2007 +0200
    18.3 @@ -222,7 +222,7 @@
    18.4    apply (subst power_add)
    18.5    apply (subst zero_le_mult_iff)
    18.6    apply auto
    18.7 -  apply (subgoal_tac "x = 0 & 0 < y")
    18.8 +  apply (subgoal_tac "x = 0 & y \<noteq> 0")
    18.9    apply (erule conjE, assumption)
   18.10    apply (subst power_eq_0_iff [symmetric])
   18.11    apply (subgoal_tac "0 <= x^y * x^y")
    19.1 --- a/src/HOL/Library/Word.thy	Sun Oct 21 14:21:54 2007 +0200
    19.2 +++ b/src/HOL/Library/Word.thy	Sun Oct 21 14:53:44 2007 +0200
    19.3 @@ -412,21 +412,22 @@
    19.4    thus ?thesis ..
    19.5  qed
    19.6  
    19.7 -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>]"
    19.8 +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>]"
    19.9  proof -
   19.10 -  assume [simp]: "0 < n"
   19.11 +  assume [simp]: "n\<noteq>0"
   19.12    show ?thesis
   19.13      apply (subst nat_to_bv_def [of n])
   19.14      apply (simp only: nat_to_bv_helper.simps [of n])
   19.15      apply (subst unfold_nat_to_bv_helper)
   19.16      using prems
   19.17 -    apply (simp add: neq0_conv)
   19.18 +    apply (simp)
   19.19      apply (subst nat_to_bv_def [of "n div 2"])
   19.20      apply auto
   19.21      done
   19.22  qed
   19.23  
   19.24 -lemma bv_to_nat_dist_append: "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
   19.25 +lemma bv_to_nat_dist_append:
   19.26 +  "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
   19.27  proof -
   19.28    have "\<forall>l2. bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
   19.29    proof (induct l1,simp_all)
   19.30 @@ -457,8 +458,7 @@
   19.31    assume ind: "!!j. j < n \<Longrightarrow> bv_to_nat (nat_to_bv j) = j"
   19.32    show "bv_to_nat (nat_to_bv n) = n"
   19.33    proof (rule n_div_2_cases [of n])
   19.34 -    assume "n = 0"
   19.35 -    then show ?thesis by simp
   19.36 +    assume "n = 0" then show ?thesis by simp
   19.37    next
   19.38      assume nn: "n div 2 < n"
   19.39      assume n0: "0 < n"
   19.40 @@ -474,16 +474,14 @@
   19.41        apply (fold nat_to_bv_def)
   19.42        apply (simp add: ind' split del: split_if)
   19.43        apply (cases "n mod 2 = 0")
   19.44 -      proof (simp_all add: neq0_conv)
   19.45 +      proof (simp_all)
   19.46          assume "n mod 2 = 0"
   19.47          with mod_div_equality [of n 2]
   19.48 -        show "n div 2 * 2 = n"
   19.49 -          by simp
   19.50 +        show "n div 2 * 2 = n" by simp
   19.51        next
   19.52 -        assume "n mod 2 = Suc 0"
   19.53 +        assume "n mod 2 \<noteq> 0"
   19.54          with mod_div_equality [of n 2]
   19.55 -        show "Suc (n div 2 * 2) = n"
   19.56 -          by simp
   19.57 +        show "Suc (n div 2 * 2) = n" by arith
   19.58        qed
   19.59    qed
   19.60  qed
   19.61 @@ -536,29 +534,30 @@
   19.62  lemmas [simp del] = nat_to_bv_non0
   19.63  
   19.64  lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) \<le> length w"
   19.65 -  by (subst norm_unsigned_def,rule rem_initial_length)
   19.66 +by (subst norm_unsigned_def,rule rem_initial_length)
   19.67  
   19.68 -lemma norm_unsigned_equal: "length (norm_unsigned w) = length w ==> norm_unsigned w = w"
   19.69 -  by (simp add: norm_unsigned_def,rule rem_initial_equal)
   19.70 +lemma norm_unsigned_equal:
   19.71 +  "length (norm_unsigned w) = length w ==> norm_unsigned w = w"
   19.72 +by (simp add: norm_unsigned_def,rule rem_initial_equal)
   19.73  
   19.74  lemma bv_extend_norm_unsigned: "bv_extend (length w) \<zero> (norm_unsigned w) = w"
   19.75 -  by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)
   19.76 +by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)
   19.77  
   19.78  lemma norm_unsigned_append1 [simp]:
   19.79 -    "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
   19.80 -  by (simp add: norm_unsigned_def,rule rem_initial_append1)
   19.81 +  "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
   19.82 +by (simp add: norm_unsigned_def,rule rem_initial_append1)
   19.83  
   19.84  lemma norm_unsigned_append2 [simp]:
   19.85 -    "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
   19.86 -  by (simp add: norm_unsigned_def,rule rem_initial_append2)
   19.87 +  "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
   19.88 +by (simp add: norm_unsigned_def,rule rem_initial_append2)
   19.89  
   19.90  lemma bv_to_nat_zero_imp_empty:
   19.91 -    "bv_to_nat w = 0 \<Longrightarrow> norm_unsigned w = []"
   19.92 -  by (atomize (full), induct w rule: bit_list_induct) (simp_all add: neq0_conv)
   19.93 +  "bv_to_nat w = 0 \<Longrightarrow> norm_unsigned w = []"
   19.94 +by (atomize (full), induct w rule: bit_list_induct) simp_all
   19.95  
   19.96  lemma bv_to_nat_nzero_imp_nempty:
   19.97    "bv_to_nat w \<noteq> 0 \<Longrightarrow> norm_unsigned w \<noteq> []"
   19.98 -  by (induct w rule: bit_list_induct) simp_all
   19.99 +by (induct w rule: bit_list_induct) simp_all
  19.100  
  19.101  lemma nat_helper1:
  19.102    assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
  19.103 @@ -1855,8 +1854,8 @@
  19.104    qed
  19.105  qed
  19.106  
  19.107 -lemma bv_msb_one: "bv_msb w = \<one> ==> 0 < bv_to_nat w"
  19.108 -  by (cases w) simp_all
  19.109 +lemma bv_msb_one: "bv_msb w = \<one> ==> bv_to_nat w \<noteq> 0"
  19.110 +by (cases w) simp_all
  19.111  
  19.112  lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2"
  19.113  proof -
  19.114 @@ -2064,7 +2063,7 @@
  19.115    by (simp add: length_nat_def Least_equality)
  19.116  
  19.117  lemma length_nat_non0:
  19.118 -  assumes n0: "0 < n"
  19.119 +  assumes n0: "n \<noteq> 0"
  19.120    shows       "length_nat n = Suc (length_nat (n div 2))"
  19.121    apply (simp add: length_nat [symmetric])
  19.122    apply (subst nat_to_bv_non0 [of n])
    20.1 --- a/src/HOL/List.thy	Sun Oct 21 14:21:54 2007 +0200
    20.2 +++ b/src/HOL/List.thy	Sun Oct 21 14:53:44 2007 +0200
    20.3 @@ -950,9 +950,7 @@
    20.4    proof (cases)
    20.5      assume "p x"
    20.6      hence eq: "?S' = insert 0 (Suc ` ?S)"
    20.7 -      apply (auto simp add:  nth_Cons image_def neq0_conv split:nat.split elim:lessE)
    20.8 -      apply (rule_tac x="xa - 1" in exI, auto)
    20.9 -      done
   20.10 +      by(auto simp: nth_Cons image_def split:nat.split dest:not0_implies_Suc)
   20.11      have "length (filter p (x # xs)) = Suc(card ?S)"
   20.12        using Cons `p x` by simp
   20.13      also have "\<dots> = Suc(card(Suc ` ?S))" using fin
   20.14 @@ -2460,12 +2458,7 @@
   20.15  
   20.16  lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
   20.17  apply(induct xs arbitrary: I)
   20.18 - apply simp
   20.19 -apply(auto simp add: neq0_conv sublist_Cons nth_Cons split:nat.split elim: lessE)
   20.20 - apply(erule lessE)
   20.21 -  apply auto
   20.22 -apply(erule lessE)
   20.23 -apply auto
   20.24 +apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: not0_implies_Suc)
   20.25  done
   20.26  
   20.27  lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
    21.1 --- a/src/HOL/Nat.thy	Sun Oct 21 14:21:54 2007 +0200
    21.2 +++ b/src/HOL/Nat.thy	Sun Oct 21 14:53:44 2007 +0200
    21.3 @@ -508,10 +508,7 @@
    21.4    by (fast intro: not0_implies_Suc)
    21.5  
    21.6  lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
    21.7 -  apply (rule iffI)
    21.8 -  apply (rule ccontr)
    21.9 -  apply (simp_all add: neq0_conv)
   21.10 -  done
   21.11 +using neq0_conv by blast
   21.12  
   21.13  lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
   21.14    by (induct m') simp_all
   21.15 @@ -603,8 +600,8 @@
   21.16    However, none of the generalizations are currently in the simpset,
   21.17    and I dread to think what happens if I put them in
   21.18  *}
   21.19 -lemma Suc_pred [simp]: "0 < n ==> Suc (n - Suc 0) = n"
   21.20 -  by (simp add: neq0_conv split add: nat.split)
   21.21 +lemma Suc_pred [simp]: "0 \<noteq> n ==> Suc (n - Suc 0) = n"
   21.22 +by (simp split add: nat.split)
   21.23  
   21.24  declare diff_Suc [simp del, code del]
   21.25  
   21.26 @@ -658,8 +655,8 @@
   21.27  lemma one_is_add: "(Suc 0 = m + n) = (m = Suc 0 & n = 0 | m = 0 & n = Suc 0)"
   21.28    by (rule trans, rule eq_commute, rule add_is_1)
   21.29  
   21.30 -lemma add_gr_0 [iff]: "!!m::nat. (0 < m + n) = (0 < m | 0 < n)"
   21.31 -  by (simp del: neq0_conv add: neq0_conv [symmetric])
   21.32 +lemma add_gr_0 [iff]: "!!m::nat. (m + n \<noteq> 0) = (m\<noteq>0 | n\<noteq>0)"
   21.33 +by simp
   21.34  
   21.35  lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0"
   21.36    apply (drule add_0_right [THEN ssubst])
   21.37 @@ -743,11 +740,11 @@
   21.38    done
   21.39  
   21.40  text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
   21.41 -lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
   21.42 -  apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
   21.43 -  apply (induct_tac x)
   21.44 -  apply (simp_all add: add_less_mono)
   21.45 -  done
   21.46 +lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j"
   21.47 +apply(auto simp: gr0_conv_Suc)
   21.48 +apply (induct_tac m)
   21.49 +apply (simp_all add: add_less_mono)
   21.50 +done
   21.51  
   21.52  
   21.53  text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
   21.54 @@ -1084,9 +1081,9 @@
   21.55  by (simp add: linorder_not_less [symmetric], auto)
   21.56  
   21.57  lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
   21.58 -  apply (cut_tac less_linear, safe, auto simp add: neq0_conv)
   21.59 -  apply (drule mult_less_mono1, assumption, simp)+
   21.60 -  done
   21.61 +apply (cut_tac less_linear, safe, auto simp add: neq0_conv)
   21.62 +apply (drule mult_less_mono1, assumption, simp)+
   21.63 +done
   21.64  
   21.65  lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
   21.66  by (simp add: mult_commute [of k])
   21.67 @@ -1105,8 +1102,8 @@
   21.68    apply (drule sym)
   21.69    apply (rule disjCI)
   21.70    apply (rule nat_less_cases, erule_tac [2] _)
   21.71 -  apply (fastsimp simp add: neq0_conv elim!: less_SucE)
   21.72 -  apply (fastsimp simp add: neq0_conv dest: mult_less_mono2)
   21.73 +  apply (fastsimp elim!: less_SucE)
   21.74 +  apply (auto simp add: neq0_conv dest: mult_less_mono2)
   21.75    done
   21.76  
   21.77  
    22.1 --- a/src/HOL/Power.thy	Sun Oct 21 14:21:54 2007 +0200
    22.2 +++ b/src/HOL/Power.thy	Sun Oct 21 14:53:44 2007 +0200
    22.3 @@ -140,16 +140,13 @@
    22.4  done
    22.5  
    22.6  lemma power_eq_0_iff [simp]:
    22.7 -     "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & 0<n)"
    22.8 +  "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n\<noteq>0)"
    22.9  apply (induct "n")
   22.10  apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
   22.11  done
   22.12  
   22.13 -lemma field_power_eq_0_iff:
   22.14 -     "(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)"
   22.15 -by simp (* TODO: delete *)
   22.16 -
   22.17 -lemma field_power_not_zero: "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
   22.18 +lemma field_power_not_zero:
   22.19 +  "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
   22.20  by force
   22.21  
   22.22  lemma nonzero_power_inverse:
   22.23 @@ -279,26 +276,26 @@
   22.24                   order_less_imp_le)
   22.25  done
   22.26  
   22.27 -lemma power_increasing_iff [simp]: 
   22.28 -     "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
   22.29 -  by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le) 
   22.30 +lemma power_increasing_iff [simp]:
   22.31 +  "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
   22.32 +by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le) 
   22.33  
   22.34  lemma power_strict_increasing_iff [simp]:
   22.35 -     "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
   22.36 -  by (blast intro: power_less_imp_less_exp power_strict_increasing) 
   22.37 +  "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
   22.38 +by (blast intro: power_less_imp_less_exp power_strict_increasing) 
   22.39  
   22.40  lemma power_le_imp_le_base:
   22.41 -  assumes le: "a ^ Suc n \<le> b ^ Suc n"
   22.42 -      and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
   22.43 -  shows "a \<le> b"
   22.44 - proof (rule ccontr)
   22.45 -   assume "~ a \<le> b"
   22.46 -   then have "b < a" by (simp only: linorder_not_le)
   22.47 -   then have "b ^ Suc n < a ^ Suc n"
   22.48 -     by (simp only: prems power_strict_mono)
   22.49 -   from le and this show "False"
   22.50 -      by (simp add: linorder_not_less [symmetric])
   22.51 - qed
   22.52 +assumes le: "a ^ Suc n \<le> b ^ Suc n"
   22.53 +    and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
   22.54 +shows "a \<le> b"
   22.55 +proof (rule ccontr)
   22.56 +  assume "~ a \<le> b"
   22.57 +  then have "b < a" by (simp only: linorder_not_le)
   22.58 +  then have "b ^ Suc n < a ^ Suc n"
   22.59 +    by (simp only: prems power_strict_mono)
   22.60 +  from le and this show "False"
   22.61 +    by (simp add: linorder_not_less [symmetric])
   22.62 +qed
   22.63  
   22.64  lemma power_less_imp_less_base:
   22.65    fixes a b :: "'a::{ordered_semidom,recpower}"
   22.66 @@ -345,7 +342,7 @@
   22.67  lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
   22.68  by (insert one_le_power [of i n], simp)
   22.69  
   22.70 -lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
   22.71 +lemma nat_zero_less_power_iff [simp]: "(x^n = 0) = (x = (0::nat) & n\<noteq>0)"
   22.72  by (induct "n", auto)
   22.73  
   22.74  text{*Valid for the naturals, but what if @{text"0<i<1"}?
   22.75 @@ -393,7 +390,7 @@
   22.76  val power_mono = thm"power_mono";
   22.77  val power_strict_mono = thm"power_strict_mono";
   22.78  val power_eq_0_iff = thm"power_eq_0_iff";
   22.79 -val field_power_eq_0_iff = thm"field_power_eq_0_iff";
   22.80 +val field_power_eq_0_iff = thm"power_eq_0_iff";
   22.81  val field_power_not_zero = thm"field_power_not_zero";
   22.82  val power_inverse = thm"power_inverse";
   22.83  val nonzero_power_divide = thm"nonzero_power_divide";
    23.1 --- a/src/HOL/Real/RealDef.thy	Sun Oct 21 14:21:54 2007 +0200
    23.2 +++ b/src/HOL/Real/RealDef.thy	Sun Oct 21 14:53:44 2007 +0200
    23.3 @@ -794,24 +794,24 @@
    23.4  
    23.5  lemma real_of_nat_div2:
    23.6    "0 <= real (n::nat) / real (x) - real (n div x)"
    23.7 -  apply(case_tac "x = 0")
    23.8 -  apply (simp add: neq0_conv)
    23.9 -  apply (simp add: neq0_conv  compare_rls)
   23.10 -  apply (subst real_of_nat_div_aux)
   23.11 -  apply assumption
   23.12 -  apply simp
   23.13 -  apply (subst zero_le_divide_iff)
   23.14 -  apply simp
   23.15 +apply(case_tac "x = 0")
   23.16 + apply (simp)
   23.17 +apply (simp add: compare_rls)
   23.18 +apply (subst real_of_nat_div_aux)
   23.19 + apply simp
   23.20 +apply simp
   23.21 +apply (subst zero_le_divide_iff)
   23.22 +apply simp
   23.23  done
   23.24  
   23.25  lemma real_of_nat_div3:
   23.26    "real (n::nat) / real (x) - real (n div x) <= 1"
   23.27 -  apply(case_tac "x = 0")
   23.28 -  apply (simp add: neq0_conv )
   23.29 -  apply (simp add: compare_rls neq0_conv )
   23.30 -  apply (subst real_of_nat_div_aux)
   23.31 -  apply assumption
   23.32 -  apply simp
   23.33 +apply(case_tac "x = 0")
   23.34 +apply (simp)
   23.35 +apply (simp add: compare_rls)
   23.36 +apply (subst real_of_nat_div_aux)
   23.37 + apply simp
   23.38 +apply simp
   23.39  done
   23.40  
   23.41  lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x" 
    24.1 --- a/src/HOL/Word/BinBoolList.thy	Sun Oct 21 14:21:54 2007 +0200
    24.2 +++ b/src/HOL/Word/BinBoolList.thy	Sun Oct 21 14:53:44 2007 +0200
    24.3 @@ -1099,20 +1099,19 @@
    24.4    done
    24.5  
    24.6  lemma bin_rsplit_aux_len_le [rule_format] :
    24.7 -  "ALL ws m. n > 0 --> ws = bin_rsplit_aux (n, bs, nw, w) --> 
    24.8 +  "ALL ws m. n \<noteq> 0 --> ws = bin_rsplit_aux (n, bs, nw, w) --> 
    24.9      (length ws <= m) = (nw + length bs * n <= m * n)"
   24.10    apply (rule_tac u=n and v=bs and w=nw and x=w in bin_rsplit_aux.induct)
   24.11    apply (subst bin_rsplit_aux.simps)
   24.12 -  apply (clarsimp simp: Let_def neq0_conv split: ls_splits )
   24.13 -  apply (erule lrlem)
   24.14 +  apply (simp add:lrlem Let_def split: ls_splits )
   24.15    done
   24.16  
   24.17  lemma bin_rsplit_len_le: 
   24.18 -  "n > 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)"
   24.19 +  "n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)"
   24.20    unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le)
   24.21   
   24.22  lemma bin_rsplit_aux_len [rule_format] :
   24.23 -  "0 < n --> length (bin_rsplit_aux (n, cs, nw, w)) = 
   24.24 +  "n\<noteq>0 --> length (bin_rsplit_aux (n, cs, nw, w)) = 
   24.25      (nw + n - 1) div n + length cs"
   24.26    apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct)
   24.27    apply (subst bin_rsplit_aux.simps)
   24.28 @@ -1126,11 +1125,11 @@
   24.29    done
   24.30  
   24.31  lemma bin_rsplit_len: 
   24.32 -  "0 < n ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
   24.33 +  "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
   24.34    unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len)
   24.35  
   24.36  lemma bin_rsplit_aux_len_indep [rule_format] :
   24.37 -  "0 < n ==> (ALL v bs. length bs = length cs --> 
   24.38 +  "n\<noteq>0 ==> (ALL v bs. length bs = length cs --> 
   24.39      length (bin_rsplit_aux (n, bs, nw, v)) = 
   24.40      length (bin_rsplit_aux (n, cs, nw, w)))"
   24.41    apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct)
   24.42 @@ -1148,7 +1147,7 @@
   24.43    done
   24.44  
   24.45  lemma bin_rsplit_len_indep: 
   24.46 -  "0 < n ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
   24.47 +  "n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
   24.48    apply (unfold bin_rsplit_def)
   24.49    apply (erule bin_rsplit_aux_len_indep)
   24.50    apply (rule refl)
    25.1 --- a/src/HOL/Word/BinGeneral.thy	Sun Oct 21 14:21:54 2007 +0200
    25.2 +++ b/src/HOL/Word/BinGeneral.thy	Sun Oct 21 14:53:44 2007 +0200
    25.3 @@ -457,7 +457,7 @@
    25.4    we get a version for when the word length is given literally *)
    25.5  
    25.6  lemmas nat_non0_gr = 
    25.7 -  trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] neq0_conv, standard]
    25.8 +  trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl, standard]
    25.9  
   25.10  lemmas bintrunc_pred_simps [simp] = 
   25.11    bintrunc_minus_simps [of "number_of bin", simplified nobm1, standard]
    26.1 --- a/src/HOL/Word/WordArith.thy	Sun Oct 21 14:21:54 2007 +0200
    26.2 +++ b/src/HOL/Word/WordArith.thy	Sun Oct 21 14:53:44 2007 +0200
    26.3 @@ -117,28 +117,28 @@
    26.4  lemmas unat_eq_zero = unat_0_iff
    26.5  
    26.6  lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"
    26.7 -  by (simp add : neq0_conv unat_0_iff [symmetric])
    26.8 +by (auto simp: unat_0_iff [symmetric])
    26.9  
   26.10  lemma ucast_0 [simp] : "ucast 0 = 0"
   26.11 -  unfolding ucast_def
   26.12 -  by simp (simp add: word_0_wi)
   26.13 +unfolding ucast_def
   26.14 +by simp (simp add: word_0_wi)
   26.15  
   26.16  lemma sint_0 [simp] : "sint 0 = 0"
   26.17 -  unfolding sint_uint
   26.18 -  by (simp add: Pls_def [symmetric])
   26.19 +unfolding sint_uint
   26.20 +by (simp add: Pls_def [symmetric])
   26.21  
   26.22  lemma scast_0 [simp] : "scast 0 = 0"
   26.23 -  apply (unfold scast_def)
   26.24 -  apply simp
   26.25 -  apply (simp add: word_0_wi)
   26.26 -  done
   26.27 +apply (unfold scast_def)
   26.28 +apply simp
   26.29 +apply (simp add: word_0_wi)
   26.30 +done
   26.31  
   26.32  lemma sint_n1 [simp] : "sint -1 = -1"
   26.33 -  apply (unfold word_m1_wi_Min)
   26.34 -  apply (simp add: word_sbin.eq_norm)
   26.35 -  apply (unfold Min_def number_of_eq)
   26.36 -  apply simp
   26.37 -  done
   26.38 +apply (unfold word_m1_wi_Min)
   26.39 +apply (simp add: word_sbin.eq_norm)
   26.40 +apply (unfold Min_def number_of_eq)
   26.41 +apply simp
   26.42 +done
   26.43  
   26.44  lemma scast_n1 [simp] : "scast -1 = -1"
   26.45    apply (unfold scast_def sint_n1)
   26.46 @@ -1242,15 +1242,15 @@
   26.47  lemmas card_word = trans [OF card_eq card_lessThan', standard]
   26.48  
   26.49  lemma finite_word_UNIV: "finite (UNIV :: 'a :: len word set)"
   26.50 -  apply (rule contrapos_np)
   26.51 -   prefer 2
   26.52 -   apply (erule card_infinite)
   26.53 -  apply (simp add : card_word neq0_conv)
   26.54 -  done
   26.55 +apply (rule contrapos_np)
   26.56 + prefer 2
   26.57 + apply (erule card_infinite)
   26.58 +apply (simp add: card_word)
   26.59 +done
   26.60  
   26.61  lemma card_word_size: 
   26.62    "card (UNIV :: 'a :: len word set) = (2 ^ size (x :: 'a word))"
   26.63 -  unfolding word_size by (rule card_word)
   26.64 +unfolding word_size by (rule card_word)
   26.65  
   26.66  end 
   26.67  
    27.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Sun Oct 21 14:21:54 2007 +0200
    27.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Sun Oct 21 14:53:44 2007 +0200
    27.3 @@ -63,7 +63,7 @@
    27.4    "fmsize (NDvd i t) = 2"
    27.5    "fmsize p = 1"
    27.6    (* several lemmas about fmsize *)
    27.7 -lemma fmsize_pos: "fmsize p > 0"	
    27.8 +lemma fmsize_pos: "fmsize p \<noteq> 0"	
    27.9  by (induct p rule: fmsize.induct) simp_all
   27.10  
   27.11    (* Semantics of formulae (fm) *)
   27.12 @@ -114,7 +114,7 @@
   27.13    "prep (Imp p q) = prep (Or (NOT p) q)"
   27.14    "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   27.15    "prep p = p"
   27.16 -(hints simp add: fmsize_pos)
   27.17 +(hints simp add: fmsize_pos neq0_conv[symmetric])
   27.18  lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
   27.19  by (induct p arbitrary: bs rule: prep.induct, auto)
   27.20  
   27.21 @@ -188,14 +188,12 @@
   27.22  | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
   27.23  
   27.24  lemma numsubst0_I:
   27.25 -  shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
   27.26 -  by (induct t rule: numsubst0.induct,auto simp add: gr0_conv_Suc neq0_conv)
   27.27 +  "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
   27.28 +by (induct t rule: numsubst0.induct,auto dest: not0_implies_Suc)
   27.29  
   27.30  lemma numsubst0_I':
   27.31 -  assumes nb: "numbound0 a"
   27.32 -  shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
   27.33 -  using nb
   27.34 -  by (induct t rule: numsubst0.induct, auto simp add: neq0_conv gr0_conv_Suc numbound0_I[where b="b" and b'="b'"])
   27.35 +  "numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
   27.36 +by (induct t rule: numsubst0.induct, auto dest: not0_implies_Suc simp: numbound0_I[where b="b" and b'="b'"])
   27.37  
   27.38  primrec
   27.39    "subst0 t T = T"