author paulson Wed, 02 Jan 2008 12:22:05 +0100 changeset 25760 6d947d7a5ae8 parent 25759 6326138c1bd7 child 25761 466e714de2fc
new metis proofs
```--- a/src/HOL/NumberTheory/Euler.thy	Wed Jan 02 04:10:47 2008 +0100
+++ b/src/HOL/NumberTheory/Euler.thy	Wed Jan 02 12:22:05 2008 +0100
@@ -77,10 +77,7 @@
qed
then have "[j^2 = a] (mod p)"
-    apply(subgoal_tac "2 = Suc(Suc(0))")
-    apply (erule ssubst)
-    apply (auto simp only: power_Suc power_0)
-    by auto
+    by (metis  number_of_is_id power2_eq_square succ_1 succ_Pls)
with prems show False
qed
@@ -155,7 +152,7 @@
b = "x * (a * MultInv p x)" and
c = "a * (x * MultInv p x)" in  zcong_trans, force)
apply (frule_tac p = p and x = x in MultInv_prop2, auto)
-  apply (drule_tac a = "x * MultInv p x" and b = 1 in zcong_zmult_prop2)
+apply (metis StandardRes_SRStar_prop3 mult_1_right mult_commute zcong_sym zcong_zmult_prop1)
done

@@ -212,10 +209,7 @@
also have "... = zfact(p - 1)"
proof -
have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
-      apply (insert prems, auto)
-      apply (drule d22set_g_1)
-      apply (auto simp add: d22set_fin)
-      done
+      by (metis d22set_fin d22set_g_1 linorder_neq_iff)
then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))"
by auto
then show ?thesis
@@ -235,11 +229,7 @@
lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p));
[x^(nat (((p) - 1) div 2)) = -1](mod p)"
-  apply (frule zfact_prop, auto)
-  apply (frule Wilson_Russ)
-  apply (auto simp add: zcong_sym)
-  apply (rule zcong_trans, auto)
-  done
+  by (metis Wilson_Russ number_of_is_id zcong_sym zcong_trans zfact_prop)

text {* \medskip Prove another part of Euler Criterion: *}

@@ -282,11 +272,7 @@
text {* \medskip Prove the final part of Euler's Criterion: *}

lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
-  apply (subgoal_tac "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==>
-    ~([y ^ 2 = 0] (mod p))")
-  apply (auto simp add: zcong_sym [of "y^2" x p] intro: zcong_trans)
-  apply (auto simp add: zcong_eq_zdvd_prop intro: zpower_zdvd_prop1)
-  done
+  by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div zdvd_trans)

lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))"