src/HOL/Algebra/Exponent.thy
changeset 25162 ad4d5365d9d8
parent 25134 3d4953e88449
child 27105 5f139027c365
     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")