author huffman Sun, 13 Nov 2011 19:26:53 +0100 changeset 45480 a39bb6d42ace parent 45477 11d9c2768729 child 45481 cf937a9ce051
remove unnecessary number-representation-specific rules from metis calls; speed up another proof
```--- a/src/HOL/Old_Number_Theory/Euler.thy	Sat Nov 12 21:10:56 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Euler.thy	Sun Nov 13 19:26:53 2011 +0100
@@ -85,7 +85,7 @@
apply (auto simp add: MultInvPair_def)
apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))")
apply auto
-  apply (metis MultInvPair_distinct Pls_def StandardRes_def aux number_of_is_id one_is_num_one)
+  apply (metis MultInvPair_distinct StandardRes_def aux)
done

@@ -227,7 +227,7 @@
lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p));
~(QuadRes p x) |] ==>
[x^(nat (((p) - 1) div 2)) = -1](mod p)"
-  by (metis Wilson_Russ number_of_is_id zcong_sym zcong_trans zfact_prop)
+  by (metis Wilson_Russ zcong_sym zcong_trans zfact_prop)

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

@@ -280,13 +280,13 @@
apply (subgoal_tac "p \<in> zOdd")
prefer 2
-   apply (metis number_of_is_id numeral_1_eq_1 zprime_zOdd_eq_grt_2)
+   apply (metis 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 (rule zcong_trans)
apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
-  apply (metis Little_Fermat even_div_2_prop2 mult_Bit0 number_of_is_id odd_minus_one_even one_is_num_one mult_1 aux__2)
+  apply (metis Little_Fermat even_div_2_prop2 odd_minus_one_even mult_1 aux__2)
done

```
```--- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Nov 12 21:10:56 2011 +0100
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 13 19:26:53 2011 +0100
@@ -142,7 +142,7 @@
prefer 2
apply (subst zdvd_iff_zgcd [symmetric])
apply (rule_tac [4] zgcd_zcong_zgcd)
-       apply (simp_all add: zcong_sym)
+       apply (simp_all (no_asm_use) add: zcong_sym)
done

```