src/HOL/Algebra/Exponent.thy
changeset 16663 13e9c402308b
parent 16417 9bc16273c2d4
child 16733 236dfafbeb63
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Fri Jul 01 14:55:05 2005 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Fri Jul 01 17:41:10 2005 +0200
     1.3 @@ -11,15 +11,15 @@
     1.4  
     1.5  constdefs
     1.6    exponent      :: "[nat, nat] => nat"
     1.7 -  "exponent p s == if p \<in> prime then (GREATEST r. p^r dvd s) else 0"
     1.8 +  "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
     1.9  
    1.10  subsection{*Prime Theorems*}
    1.11  
    1.12 -lemma prime_imp_one_less: "p \<in> prime ==> Suc 0 < p"
    1.13 +lemma prime_imp_one_less: "prime p ==> Suc 0 < p"
    1.14  by (unfold prime_def, force)
    1.15  
    1.16  lemma prime_iff:
    1.17 -     "(p \<in> prime) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
    1.18 +     "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
    1.19  apply (auto simp add: prime_imp_one_less)
    1.20  apply (blast dest!: prime_dvd_mult)
    1.21  apply (auto simp add: prime_def)
    1.22 @@ -30,7 +30,7 @@
    1.23  apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2, auto)
    1.24  done
    1.25  
    1.26 -lemma zero_less_prime_power: "p \<in> prime ==> 0 < p^a"
    1.27 +lemma zero_less_prime_power: "prime p ==> 0 < p^a"
    1.28  by (force simp add: prime_iff)
    1.29  
    1.30  
    1.31 @@ -39,7 +39,7 @@
    1.32  
    1.33  
    1.34  lemma prime_dvd_cases:
    1.35 -     "[| p*k dvd m*n;  p \<in> prime |]  
    1.36 +     "[| p*k dvd m*n;  prime p |]  
    1.37        ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
    1.38  apply (simp add: prime_iff)
    1.39  apply (frule dvd_mult_left)
    1.40 @@ -56,7 +56,7 @@
    1.41  done
    1.42  
    1.43  
    1.44 -lemma prime_power_dvd_cases [rule_format (no_asm)]: "p \<in> prime  
    1.45 +lemma prime_power_dvd_cases [rule_format (no_asm)]: "prime p
    1.46        ==> \<forall>m n. p^c dvd m*n -->  
    1.47            (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
    1.48  apply (induct_tac "c")
    1.49 @@ -89,7 +89,7 @@
    1.50  
    1.51  (*needed in this form in Sylow.ML*)
    1.52  lemma div_combine:
    1.53 -     "[| p \<in> prime; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |]  
    1.54 +     "[| prime p; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |]  
    1.55        ==> p ^ a dvd k"
    1.56  by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto)
    1.57  
    1.58 @@ -117,7 +117,7 @@
    1.59  subsection{*Exponent Theorems*}
    1.60  
    1.61  lemma exponent_ge [rule_format]:
    1.62 -     "[|p^k dvd n;  p \<in> prime;  0<n|] ==> k <= exponent p n"
    1.63 +     "[|p^k dvd n;  prime p;  0<n|] ==> k <= exponent p n"
    1.64  apply (simp add: exponent_def)
    1.65  apply (erule Greatest_le)
    1.66  apply (blast dest: prime_imp_one_less power_dvd_bound)
    1.67 @@ -131,14 +131,14 @@
    1.68  done
    1.69  
    1.70  lemma power_Suc_exponent_Not_dvd:
    1.71 -     "[|(p * p ^ exponent p s) dvd s;  p \<in> prime |] ==> s=0"
    1.72 +     "[|(p * p ^ exponent p s) dvd s;  prime p |] ==> s=0"
    1.73  apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
    1.74   prefer 2 apply simp 
    1.75  apply (rule ccontr)
    1.76  apply (drule exponent_ge, auto)
    1.77  done
    1.78  
    1.79 -lemma exponent_power_eq [simp]: "p \<in> prime ==> exponent p (p^a) = a"
    1.80 +lemma exponent_power_eq [simp]: "prime p ==> exponent p (p^a) = a"
    1.81  apply (simp (no_asm_simp) add: exponent_def)
    1.82  apply (rule Greatest_equality, simp)
    1.83  apply (simp (no_asm_simp) add: prime_imp_one_less power_dvd_imp_le)
    1.84 @@ -148,7 +148,7 @@
    1.85       "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
    1.86  by (simp (no_asm_simp) add: exponent_def)
    1.87  
    1.88 -lemma exponent_eq_0 [simp]: "p \<notin> prime ==> exponent p s = 0"
    1.89 +lemma exponent_eq_0 [simp]: "\<not> prime p ==> exponent p s = 0"
    1.90  by (simp (no_asm_simp) add: exponent_def)
    1.91  
    1.92  
    1.93 @@ -156,7 +156,7 @@
    1.94  lemma exponent_mult_add1:
    1.95       "[| 0 < a; 0 < b |]   
    1.96        ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
    1.97 -apply (case_tac "p \<in> prime")
    1.98 +apply (case_tac "prime p")
    1.99  apply (rule exponent_ge)
   1.100  apply (auto simp add: power_add)
   1.101  apply (blast intro: prime_imp_one_less power_exponent_dvd mult_dvd_mono)
   1.102 @@ -165,7 +165,7 @@
   1.103  (* exponent_mult_add, opposite inclusion *)
   1.104  lemma exponent_mult_add2: "[| 0 < a; 0 < b |]  
   1.105        ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
   1.106 -apply (case_tac "p \<in> prime")
   1.107 +apply (case_tac "prime p")
   1.108  apply (rule leI, clarify)
   1.109  apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto)
   1.110  apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b")
   1.111 @@ -191,7 +191,7 @@
   1.112  done
   1.113  
   1.114  lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
   1.115 -apply (case_tac "p \<in> prime")
   1.116 +apply (case_tac "prime p")
   1.117  apply (auto simp add: prime_iff not_divides_exponent_0)
   1.118  done
   1.119  
   1.120 @@ -258,7 +258,7 @@
   1.121  lemma p_not_div_choose_lemma [rule_format]:
   1.122       "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]  
   1.123        ==> k<K --> exponent p ((j+k) choose k) = 0"
   1.124 -apply (case_tac "p \<in> prime")
   1.125 +apply (case_tac "prime p")
   1.126   prefer 2 apply simp 
   1.127  apply (induct_tac "k")
   1.128  apply (simp (no_asm))
   1.129 @@ -293,7 +293,7 @@
   1.130  
   1.131  lemma const_p_fac_right:
   1.132       "0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
   1.133 -apply (case_tac "p \<in> prime")
   1.134 +apply (case_tac "prime p")
   1.135   prefer 2 apply simp 
   1.136  apply (frule_tac a = a in zero_less_prime_power)
   1.137  apply (rule_tac K = "p^a" in p_not_div_choose)
   1.138 @@ -311,7 +311,7 @@
   1.139  
   1.140  lemma const_p_fac:
   1.141       "0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
   1.142 -apply (case_tac "p \<in> prime")
   1.143 +apply (case_tac "prime p")
   1.144   prefer 2 apply simp 
   1.145  apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
   1.146   prefer 2 apply (force simp add: prime_iff)