# HG changeset patch
# User huffman
# Date 1379023687 25200
# Node ID 2bd8d459ebaea36343213e161877ef78de28b55a
# Parent  ea99a796417417ce34967a3e6c9ce11b49402941
remove unneeded assumption from prime_dvd_power lemmas;
add iff forms of prime_dvd_power lemmas (thanks to Jason Dagit)

diff -r ea99a7964174 -r 2bd8d459ebae src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Thu Sep 12 09:39:02 2013 -0700
+++ b/src/HOL/Number_Theory/Primes.thy	Thu Sep 12 15:08:07 2013 -0700
@@ -167,18 +167,24 @@
   by (metis div_mult_self1_is_id div_mult_self2_is_id
       int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
 
-lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
-    n > 0 --> (p dvd x^n --> p dvd x)"
-  by (induct n rule: nat_induct) auto
+lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
+  by (induct n) auto
 
-lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
-    n > 0 --> (p dvd x^n --> p dvd x)"
-  apply (induct n rule: nat_induct)
-  apply auto
+lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
+  apply (induct n)
   apply (frule prime_ge_0_int)
   apply auto
   done
 
+lemma prime_dvd_power_nat_iff: "prime (p::nat) \<Longrightarrow> n > 0 \<Longrightarrow>
+    p dvd x^n \<longleftrightarrow> p dvd x"
+  by (cases n) (auto elim: prime_dvd_power_nat)
+
+lemma prime_dvd_power_int_iff: "prime (p::int) \<Longrightarrow> n > 0 \<Longrightarrow>
+    p dvd x^n \<longleftrightarrow> p dvd x"
+  by (cases n) (auto elim: prime_dvd_power_int)
+
+
 subsubsection {* Make prime naively executable *}
 
 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
diff -r ea99a7964174 -r 2bd8d459ebae src/HOL/ex/Sqrt.thy
--- a/src/HOL/ex/Sqrt.thy	Thu Sep 12 09:39:02 2013 -0700
+++ b/src/HOL/ex/Sqrt.thy	Thu Sep 12 15:08:07 2013 -0700
@@ -31,12 +31,12 @@
   have "p dvd m \<and> p dvd n"
   proof
     from eq have "p dvd m\<^sup>2" ..
-    with `prime p` pos2 show "p dvd m" by (rule prime_dvd_power_nat)
+    with `prime p` show "p dvd m" by (rule prime_dvd_power_nat)
     then obtain k where "m = p * k" ..
     with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
     with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
     then have "p dvd n\<^sup>2" ..
-    with `prime p` pos2 show "p dvd n" by (rule prime_dvd_power_nat)
+    with `prime p` show "p dvd n" by (rule prime_dvd_power_nat)
   qed
   then have "p dvd gcd m n" ..
   with gcd have "p dvd 1" by simp
@@ -71,12 +71,12 @@
   also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp
   finally have eq: "m\<^sup>2 = p * n\<^sup>2" ..
   then have "p dvd m\<^sup>2" ..
-  with `prime p` pos2 have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
+  with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
   then obtain k where "m = p * k" ..
   with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
   with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
   then have "p dvd n\<^sup>2" ..
-  with `prime p` pos2 have "p dvd n" by (rule prime_dvd_power_nat)
+  with `prime p` have "p dvd n" by (rule prime_dvd_power_nat)
   with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat)
   with gcd have "p dvd 1" by simp
   then have "p \<le> 1" by (simp add: dvd_imp_le)
@@ -103,4 +103,3 @@
 qed
 
 end
-