src/HOL/Number_Theory/Primes.thy
changeset 53598 2bd8d459ebae
parent 47108 2a1953f0d20d
child 54228 229282d53781
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Thu Sep 12 09:39:02 2013 -0700
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Thu Sep 12 15:08:07 2013 -0700
     1.3 @@ -167,18 +167,24 @@
     1.4    by (metis div_mult_self1_is_id div_mult_self2_is_id
     1.5        int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
     1.6  
     1.7 -lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
     1.8 -    n > 0 --> (p dvd x^n --> p dvd x)"
     1.9 -  by (induct n rule: nat_induct) auto
    1.10 +lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
    1.11 +  by (induct n) auto
    1.12  
    1.13 -lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
    1.14 -    n > 0 --> (p dvd x^n --> p dvd x)"
    1.15 -  apply (induct n rule: nat_induct)
    1.16 -  apply auto
    1.17 +lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
    1.18 +  apply (induct n)
    1.19    apply (frule prime_ge_0_int)
    1.20    apply auto
    1.21    done
    1.22  
    1.23 +lemma prime_dvd_power_nat_iff: "prime (p::nat) \<Longrightarrow> n > 0 \<Longrightarrow>
    1.24 +    p dvd x^n \<longleftrightarrow> p dvd x"
    1.25 +  by (cases n) (auto elim: prime_dvd_power_nat)
    1.26 +
    1.27 +lemma prime_dvd_power_int_iff: "prime (p::int) \<Longrightarrow> n > 0 \<Longrightarrow>
    1.28 +    p dvd x^n \<longleftrightarrow> p dvd x"
    1.29 +  by (cases n) (auto elim: prime_dvd_power_int)
    1.30 +
    1.31 +
    1.32  subsubsection {* Make prime naively executable *}
    1.33  
    1.34  lemma zero_not_prime_nat [simp]: "~prime (0::nat)"