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