# HG changeset patch
# User paulson
# Date 1199272925 -3600
# Node ID 6d947d7a5ae81b38c928ab74552da9e2915a16bb
# Parent  6326138c1bd7bccd1a3760e9f491f6266581b2ab
new metis proofs

diff -r 6326138c1bd7 -r 6d947d7a5ae8 src/HOL/NumberTheory/Euler.thy
--- 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 @@
         by (auto simp add: zcong_zmult_prop2)
     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
     by (simp add: QuadRes_def)
 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)
   apply (auto simp add: zmult_ac)
   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)); 
     ~(QuadRes p x) |] ==> 
       [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))"
   by (auto simp add: nat_mult_distrib)