author wenzelm Mon, 01 Aug 2005 19:20:28 +0200 changeset 16974 0f8ebabf3163 parent 16973 b2a894562b8f child 16975 34ed8d5d4f16
more zcong_sym;
```--- a/src/HOL/NumberTheory/Euler.thy	Mon Aug 01 19:20:26 2005 +0200
+++ b/src/HOL/NumberTheory/Euler.thy	Mon Aug 01 19:20:28 2005 +0200
@@ -5,13 +5,13 @@

-theory Euler imports Residues EvenOdd begin;
+theory Euler imports Residues EvenOdd begin

constdefs
MultInvPair :: "int => int => int => int set"
"MultInvPair a p j == {StandardRes p j, StandardRes p (a * (MultInv p j))}"
SetS        :: "int => int => int set set"
-  "SetS        a p   ==  ((MultInvPair a p) ` (SRStar p))";
+  "SetS        a p   ==  ((MultInvPair a p) ` (SRStar p))"

(****************************************************************)
(*                                                              *)
@@ -22,25 +22,25 @@
lemma MultInvPair_prop1a: "[| zprime p; 2 < p; ~([a = 0](mod p));
X \<in> (SetS a p); Y \<in> (SetS a p);
~((X \<inter> Y) = {}) |] ==>
-                           X = Y";
+                           X = Y"
-  apply (drule StandardRes_SRStar_prop1a)+; defer 1;
-  apply (drule StandardRes_SRStar_prop1a)+;
+  apply (drule StandardRes_SRStar_prop1a)+ defer 1
+  apply (drule StandardRes_SRStar_prop1a)+
apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym)
apply (drule notE, rule MultInv_zcong_prop1, auto)
-  apply (drule notE, rule MultInv_zcong_prop2, auto)
-  apply (drule MultInv_zcong_prop2, auto)
+  apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym)
+  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
apply (drule MultInv_zcong_prop1, auto)
-  apply (drule MultInv_zcong_prop2, auto)
-  apply (drule MultInv_zcong_prop2, auto)
+  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
+  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
done

lemma MultInvPair_prop1b: "[| zprime p; 2 < p; ~([a = 0](mod p));
X \<in> (SetS a p); Y \<in> (SetS a p);
X \<noteq> Y |] ==>
-                              X \<inter> Y = {}";
+                              X \<inter> Y = {}"
apply (rule notnotD)
apply (rule notI)
apply (drule MultInvPair_prop1a, auto)
@@ -51,7 +51,7 @@

lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>
-                          Union ( SetS a p) = SRStar p";
+                          Union ( SetS a p) = SRStar p"
apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4
SRStar_mult_prop2)
apply (frule StandardRes_SRStar_prop3)
@@ -61,37 +61,37 @@
lemma MultInvPair_distinct: "[| zprime p; 2 < p; ~([a = 0] (mod p));
~([j = 0] (mod p));
-                             ~([j = a * MultInv p j] (mod p))";
+                             ~([j = a * MultInv p j] (mod p))"
apply auto
-proof -;
+proof -
assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
-    "~([j = 0] (mod p))" and "~(QuadRes p a)";
-  assume "[j = a * MultInv p j] (mod p)";
-  then have "[j * j = (a * MultInv p j) * j] (mod p)";
+    "~([j = 0] (mod p))" and "~(QuadRes p a)"
+  assume "[j = a * MultInv p j] (mod p)"
+  then have "[j * j = (a * MultInv p j) * j] (mod p)"
-  then have a:"[j * j = a * (MultInv p j * j)] (mod p)";
+  then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
-  have "[j * j = a] (mod p)";
-    proof -;
-      from prems have b: "[MultInv p j * j = 1] (mod p)";
+  have "[j * j = a] (mod p)"
+    proof -
+      from prems have b: "[MultInv p j * j = 1] (mod p)"
-      from b a show ?thesis;
+      from b a show ?thesis
-    qed;
-  then have "[j^2 = a] (mod p)";
-    apply(subgoal_tac "2 = Suc(Suc(0))");
+    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
-  with prems show False;
+  with prems show False
-qed;
+qed

lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p));
~(QuadRes p a); ~([j = 0] (mod p)) |]  ==>
-                             card (MultInvPair a p j) = 2";
+                             card (MultInvPair a p j) = 2"
-  apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))");
+  apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))")
apply auto
apply (simp only: StandardRes_prop2)
apply (drule MultInvPair_distinct)
@@ -103,77 +103,77 @@
(*                                                              *)
(****************************************************************)

-lemma SetS_finite: "2 < p ==> finite (SetS a p)";
+lemma SetS_finite: "2 < p ==> finite (SetS a p)"
by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI)

-lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X";
+lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X"
by (auto simp add: SetS_def MultInvPair_def)

lemma SetS_elems_card: "[| zprime p; 2 < p; ~([a = 0] (mod p));
-                        \<forall>X \<in> SetS a p. card X = 2";
+                        \<forall>X \<in> SetS a p. card X = 2"
apply (frule StandardRes_SRStar_prop1a)
apply (rule MultInvPair_card_two, auto)
done

-lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))";
+lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
by (auto simp add: SetS_finite SetS_elems_finite finite_Union)

lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set);
-    \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S";
+    \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S"
by (induct set: Finites, auto)

lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
-                  int(card(SetS a p)) = (p - 1) div 2";
-proof -;
-  assume "zprime p" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)";
-  then have "(p - 1) = 2 * int(card(SetS a p))";
-  proof -;
-    have "p - 1 = int(card(Union (SetS a p)))";
+                  int(card(SetS a p)) = (p - 1) div 2"
+proof -
+  assume "zprime p" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)"
+  then have "(p - 1) = 2 * int(card(SetS a p))"
+  proof -
+    have "p - 1 = int(card(Union (SetS a p)))"
by (auto simp add: prems MultInvPair_prop2 SRStar_card)
-    also have "... = int (setsum card (SetS a p))";
+    also have "... = int (setsum card (SetS a p))"
by (auto simp add: prems SetS_finite SetS_elems_finite
MultInvPair_prop1c [of p a] card_Union_disjoint)
-    also have "... = int(setsum (%x.2) (SetS a p))";
+    also have "... = int(setsum (%x.2) (SetS a p))"
apply (insert prems)
apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite
card_setsum_aux simp del: setsum_constant)
done
-    also have "... = 2 * int(card( SetS a p))";
+    also have "... = 2 * int(card( SetS a p))"
by (auto simp add: prems SetS_finite setsum_const2)
-    finally show ?thesis .;
-  qed;
-  from this show ?thesis;
+    finally show ?thesis .
+  qed
+  from this show ?thesis
by auto
-qed;
+qed

lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
~(QuadRes p a); x \<in> (SetS a p) |] ==>
-                          [\<Prod>x = a] (mod p)";
+                          [\<Prod>x = a] (mod p)"
apply (auto simp add: SetS_def MultInvPair_def)
apply (frule StandardRes_SRStar_prop1a)
-  apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)");
+  apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)")
apply (auto simp add: StandardRes_prop2 MultInvPair_distinct)
apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in
-    StandardRes_prop4);
-  apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)");
+    StandardRes_prop4)
+  apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)")
apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and
b = "x * (a * MultInv p x)" and
-                   c = "a * (x * MultInv p x)" in  zcong_trans, force);
+                   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)
done

-lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1";
+lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
by arith

-lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)";
+lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)"
by auto

lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} \<union>
-    (d22set (p - 1))";
+    (d22set (p - 1))"
apply (induct p rule: d22set.induct, auto)
apply (simp add: SRStar_def d22set.simps, clarify)
@@ -209,9 +209,9 @@
qed

lemma Union_SetS_setprod_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>
-                                    \<Prod>(Union (SetS a p)) = zfact (p - 1)";
-proof -;
-  assume "zprime p" and "2 < p" and "~([a = 0](mod p))";
+                                    \<Prod>(Union (SetS a p)) = zfact (p - 1)"
+proof -
+  assume "zprime p" and "2 < p" and "~([a = 0](mod p))"
then have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
@@ -223,16 +223,16 @@
apply (drule d22set_g_1)
done
-     then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))";
+     then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))"
by auto
then show ?thesis
-  qed;
+  qed
finally show ?thesis .
-qed;
+qed

lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
-                   [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)";
+                   [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)"
apply (frule Union_SetS_setprod_prop1)
done
@@ -247,7 +247,7 @@

lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p));
-      [x^(nat (((p) - 1) div 2)) = -1](mod p)";
+      [x^(nat (((p) - 1) div 2)) = -1](mod p)"
apply (frule zfact_prop, auto)
apply (frule Wilson_Russ)
@@ -261,35 +261,35 @@
(*                                                                  *)
(********************************************************************)

-lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)";
-proof -;
-  assume "0 < p";
-  then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))";
+lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
+proof -
+  assume "0 < p"
+  then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))"
-  also have "... = (a ^ 1) * a ^ (nat(p) - 1)";
+  also have "... = (a ^ 1) * a ^ (nat(p) - 1)"
-  also have "... = a * a ^ (nat(p) - 1)";
+  also have "... = a * a ^ (nat(p) - 1)"
by auto
-  finally show ?thesis .;
-qed;
+  finally show ?thesis .
+qed

-lemma aux_2: "[| (2::int) < p; p \<in> zOdd |] ==> 0 < ((p - 1) div 2)";
-proof -;
-  assume "2 < p" and "p \<in> zOdd";
-  then have "(p - 1):zEven";
+lemma aux_2: "[| (2::int) < p; p \<in> zOdd |] ==> 0 < ((p - 1) div 2)"
+proof -
+  assume "2 < p" and "p \<in> zOdd"
+  then have "(p - 1):zEven"
by (auto simp add: zEven_def zOdd_def)
-  then have aux_1: "2 * ((p - 1) div 2) = (p - 1)";
+  then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
then have "1 < (p - 1)"
by auto
-  then have " 1 < (2 * ((p - 1) div 2))";
+  then have " 1 < (2 * ((p - 1) div 2))"
-  then have "0 < (2 * ((p - 1) div 2)) div 2";
+  then have "0 < (2 * ((p - 1) div 2)) div 2"
by auto
then show ?thesis by auto
-qed;
+qed

-lemma Euler_part2: "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)";
+lemma Euler_part2: "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)"
apply (frule zprime_zOdd_eq_grt_2)
apply (frule aux_2, auto)
apply (frule_tac a = a in aux_1, auto)
@@ -304,25 +304,25 @@
(*                                                              *)
(****************************************************************)

-lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)";
+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))");
+    ~([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

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

lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==>
-                      [x^(nat (((p) - 1) div 2)) = 1](mod p)";
+                      [x^(nat (((p) - 1) div 2)) = 1](mod p)"
apply (subgoal_tac "p \<in> zOdd")
apply (frule aux__1, auto)
-  apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower);
+  apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower)
apply (rule zcong_trans)
-  apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"]);
+  apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])