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)"

     2.1 --- a/src/HOL/ex/Sqrt.thy	Thu Sep 12 09:39:02 2013 -0700
     2.2 +++ b/src/HOL/ex/Sqrt.thy	Thu Sep 12 15:08:07 2013 -0700
     2.3 @@ -31,12 +31,12 @@
     2.4    have "p dvd m \<and> p dvd n"
     2.5    proof
     2.6      from eq have "p dvd m\<^sup>2" ..
     2.7 -    with `prime p` pos2 show "p dvd m" by (rule prime_dvd_power_nat)
     2.8 +    with `prime p` show "p dvd m" by (rule prime_dvd_power_nat)
     2.9      then obtain k where "m = p * k" ..
    2.10      with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
    2.11      with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
    2.12      then have "p dvd n\<^sup>2" ..
    2.13 -    with `prime p` pos2 show "p dvd n" by (rule prime_dvd_power_nat)
    2.14 +    with `prime p` show "p dvd n" by (rule prime_dvd_power_nat)
    2.15    qed
    2.16    then have "p dvd gcd m n" ..
    2.17    with gcd have "p dvd 1" by simp
    2.18 @@ -71,12 +71,12 @@
    2.19    also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp
    2.20    finally have eq: "m\<^sup>2 = p * n\<^sup>2" ..
    2.21    then have "p dvd m\<^sup>2" ..
    2.22 -  with `prime p` pos2 have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
    2.23 +  with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
    2.24    then obtain k where "m = p * k" ..
    2.25    with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
    2.26    with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
    2.27    then have "p dvd n\<^sup>2" ..
    2.28 -  with `prime p` pos2 have "p dvd n" by (rule prime_dvd_power_nat)
    2.29 +  with `prime p` have "p dvd n" by (rule prime_dvd_power_nat)
    2.30    with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat)
    2.31    with gcd have "p dvd 1" by simp
    2.32    then have "p \<le> 1" by (simp add: dvd_imp_le)
    2.33 @@ -103,4 +103,3 @@
    2.34  qed
    2.35  
    2.36  end
    2.37 -