# HG changeset patch
# User paulson
# Date 1197912468 -3600
# Node ID 2488fc510178b73c8b887b89b27cd2a8698229ae
# Parent  b04508c59b9d382f4287b9ae6968e421e0bd4bca
tidied some messy proofs

diff -r b04508c59b9d -r 2488fc510178 src/HOL/NumberTheory/Euler.thy
--- a/src/HOL/NumberTheory/Euler.thy	Mon Dec 17 18:24:44 2007 +0100
+++ b/src/HOL/NumberTheory/Euler.thy	Mon Dec 17 18:27:48 2007 +0100
@@ -91,9 +91,7 @@
   apply (auto simp add: MultInvPair_def)
   apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))")
   apply auto
-  apply (simp only: StandardRes_prop2)
-  apply (drule MultInvPair_distinct)
-  apply auto back
+  apply (metis MultInvPair_distinct Pls_def StandardRes_prop2 int_0_less_1 less_Pls_Bit0 number_of_is_id one_is_num_one order_less_trans)
   done
 
 
@@ -297,15 +295,14 @@
                       [x^(nat (((p) - 1) div 2)) = 1](mod p)"
   apply (subgoal_tac "p \<in> zOdd")
   apply (auto simp add: QuadRes_def)
+   prefer 2 
+   apply (metis number_of_is_id numeral_1_eq_1 zprime_zOdd_eq_grt_2)
   apply (frule aux__1, auto)
   apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower)
-  apply (auto simp add: zpower_zpower)
+  apply (auto simp add: zpower_zpower) 
   apply (rule zcong_trans)
   apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
-  apply (simp add: aux__2)
-  apply (frule odd_minus_one_even)
-  apply (frule even_div_2_prop2)
-  apply (auto intro: Little_Fermat simp add: zprime_zOdd_eq_grt_2)
+  apply (metis Little_Fermat even_div_2_prop2 mult_num0 number_of_is_id odd_minus_one_even one_is_num_one zmult_1 aux__2)
   done
 
 
diff -r b04508c59b9d -r 2488fc510178 src/HOL/NumberTheory/Int2.thy
--- a/src/HOL/NumberTheory/Int2.thy	Mon Dec 17 18:24:44 2007 +0100
+++ b/src/HOL/NumberTheory/Int2.thy	Mon Dec 17 18:27:48 2007 +0100
@@ -124,13 +124,7 @@
 
 lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m);
     x < m; y < m |] ==> x = y"
-  apply (simp add: zcong_zmod_eq)
-  apply (subgoal_tac "(x mod m) = x")
-  apply (subgoal_tac "(y mod m) = y")
-  apply simp
-  apply (rule_tac [1-2] mod_pos_pos_trivial)
-  apply auto
-  done
+  by (metis zcong_not zcong_sym zless_linear)
 
 lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==>
     ~([x = 1] (mod p))"