# Theory Euler

Up to index of Isabelle/HOL/HOL-Complex/NumberTheory

theory Euler = FiniteLib + QRLib + EvenOdd2:

```(*  Title:      Euler.thy
*)

theory Euler = FiniteLib + QRLib + EvenOdd2:;

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))";

(****************************************************************)
(*                                                              *)
(* Property for MultInvPair                                     *)
(*                                                              *)
(****************************************************************)

lemma MultInvPair_prop1a: "[| p ∈ zprime; 2 < p; ~([a = 0](mod p));
X ∈ (SetS a p); Y ∈ (SetS a p);
~((X ∩ Y) = {}) |] ==>
X = Y";
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 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_prop3, auto simp add: zcong_sym)
done

lemma MultInvPair_prop1b: "[| p ∈ zprime; 2 < p; ~([a = 0](mod p));
X ∈ (SetS a p); Y ∈ (SetS a p);
X ≠ Y |] ==>
X ∩ Y = {}";
apply (rule notnotD)
apply (rule notI)
apply (drule MultInvPair_prop1a, auto)
done

lemma MultInvPair_prop1c: "[| p ∈ zprime; 2 < p; ~([a = 0](mod p)) |] ==>
∀X ∈ SetS a p. ∀Y ∈ SetS a p. X ≠ Y --> X∩Y = {}"

lemma MultInvPair_prop2: "[| p ∈ zprime; 2 < p; ~([a = 0](mod 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)
apply (rule bexI, auto)
done

lemma MultInvPair_distinct: "[| p ∈ zprime; 2 < p; ~([a = 0] (mod p));
~([j = 0] (mod p));
~([j = a * MultInv p j] (mod p))";
apply auto
proof -;
assume "p ∈ zprime" 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)";
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)";
from b a show ?thesis;
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;
qed;

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

(****************************************************************)
(*                                                              *)
(* Properties of SetS                                           *)
(*                                                              *)
(****************************************************************)

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: "∀X ∈ SetS a p. finite X";
by (auto simp add: SetS_def MultInvPair_def)

lemma SetS_elems_card: "[| p ∈ zprime; 2 < p; ~([a = 0] (mod p));
∀X ∈ 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))";
by (auto simp add: SetS_finite SetS_elems_finite
finite_union_finite_subsets);

lemma card_setsum_aux: "[| finite S; ∀X ∈ S. finite (X::int set);
∀X ∈ S. card X = n |] ==> setsum card S = setsum (%x. n) S";
by (induct set: Finites, auto)

lemma SetS_card: "[| p ∈ zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
int(card(SetS a p)) = (p - 1) div 2";
proof -;
assume "p ∈ zprime" 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))";
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))";
apply simp;
apply (rule card_setsum_aux);
apply (rule SetS_finite);
apply (rule prems);
apply (rule SetS_elems_finite);
apply (rule SetS_elems_card);
apply (rule prems)+;
done;
also have "... = 2 * int(card( SetS a p))";
by (auto simp add: prems SetS_finite);
finally show ?thesis .;
qed;
from this show ?thesis;
by auto
qed;

lemma SetS_ssetprod_prop: "[| p ∈ zprime; 2 < p; ~([a = 0] (mod p));
~(QuadRes p a); x ∈ (SetS a p) |] ==>
[ssetprod x = a] (mod p)";
apply (auto simp add: SetS_def MultInvPair_def)
apply (frule StandardRes_SRStar_prop1a)
apply (subgoal_tac "StandardRes p x ≠ 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)");
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);
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 ≠ (a - 1) |] ==> x < a - 1";
by arith

lemma aux2: "[| (a::int) < c; b < c |] ==> (a ≤ b | b ≤ a)";
by auto

lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} ∪
(d22set (p - 1))";
apply (induct p rule: d22set.induct, auto)
apply (simp add: SRStar_def d22set.simps, arith)
apply (simp add: SRStar_def d22set.simps, clarify)
apply (frule aux1)
apply (frule aux2, auto)
apply (frule d22set_le)
apply (frule d22set_g_1, auto)
done

lemma ssetprod_setprod_id: "ssetprod A = setprod id A";
by (auto simp add: ssetprod_def setprod_def)

lemma ssetprod_disj_sets: "[| finite (A::int set set);
∀X ∈ A. finite X;
∀X ∈ A. ∀Y ∈ A. (X ≠ Y --> X ∩ Y = {}) |] ==>
ssetprod (Union A) = setprod (%x. ssetprod x) A";
by (auto simp add: ssetprod_setprod_id setprod_Union_disjoint);

lemma Union_SetS_ssetprod_prop1: "[| p ∈ zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
[ssetprod (Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)";
proof -;
assume "p ∈ zprime" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)";
then have "[ssetprod (Union (SetS a p)) =
setprod ssetprod (SetS a p)] (mod p)";
by (auto simp add: SetS_finite SetS_elems_finite
MultInvPair_prop1c ssetprod_disj_sets)
also; have "[setprod ssetprod (SetS a p) =
setprod (%x. a) (SetS a p)] (mod p)";
apply (rule setprod_same_function_zcong)
by (auto simp add: prems SetS_ssetprod_prop SetS_finite)
also (zcong_trans) have "[setprod (%x. a) (SetS a p) =
a^(card (SetS a p))] (mod p)";
by (auto simp add: prems SetS_finite setprod_constant)
finally (zcong_trans) show ?thesis;
apply (rule zcong_trans)
apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto);
apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force);
apply (auto simp add: prems SetS_card)
done
qed;

lemma Union_SetS_ssetprod_prop2: "[| p ∈ zprime; 2 < p; ~([a = 0](mod p)) |] ==>
ssetprod (Union (SetS a p)) = zfact (p - 1)";
proof -;
assume "p ∈ zprime" and "2 < p" and "~([a = 0](mod p))";
then have "ssetprod (Union (SetS a p)) = ssetprod (SRStar p)";
also have "... = ssetprod ({1} ∪ (d22set (p - 1)))";
by (auto simp add: prems SRStar_d22set_prop)
also have "... = zfact(p - 1)";
proof -;
have "~(1 ∈ d22set (p - 1)) & finite( d22set (p - 1))";
apply (insert prems, auto)
apply (drule d22set_g_1)
done
then have "ssetprod({1} ∪ (d22set (p - 1))) = ssetprod (d22set (p - 1))";
by auto
then show ?thesis
qed;
finally show ?thesis .;
qed;

lemma zfact_prop: "[| p ∈ zprime; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
[zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)";
apply (frule Union_SetS_ssetprod_prop1)
done

(****************************************************************)
(*                                                              *)
(*  Prove the first part of Euler's Criterion:                  *)
(*    ~(QuadRes p x) |] ==>                                     *)
(*                   [x^(nat (((p) - 1) div 2)) = -1](mod p)    *)
(*                                                              *)
(****************************************************************)

lemma Euler_part1: "[| 2 < p; p ∈ zprime; ~([x = 0](mod p));
[x^(nat (((p) - 1) div 2)) = -1](mod p)";
apply (frule zfact_prop, auto)
apply (frule Wilson_Russ)
apply (rule zcong_trans, auto)
done

(********************************************************************)
(*                                                                  *)
(* Prove another part of Euler Criterion:                           *)
(*        [a = 0] (mod p) ==> [0 = a ^ nat ((p - 1) div 2)] (mod p) *)
(*                                                                  *)
(********************************************************************)

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 * a ^ (nat(p) - 1)";
by auto
finally show ?thesis .;
qed;

lemma aux_2: "[| (2::int) < p; p ∈ zOdd |] ==> 0 < ((p - 1) div 2)";
proof -;
assume "2 < p" and "p ∈ 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 "1 < (p - 1)"
by auto
then have " 1 < (2 * ((p - 1) div 2))";
then have "0 < (2 * ((p - 1) div 2)) div 2";
by auto
then show ?thesis by auto
qed;

lemma Euler_part2: "[| 2 < p; p ∈ zprime; [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)
apply (frule zcong_zmult_prop1, auto)
done

(****************************************************************)
(*                                                              *)
(* Prove the final part of Euler's Criterion:                   *)
(*           QuadRes p x |] ==>                                 *)
(*                      [x^(nat (((p) - 1) div 2)) = 1](mod p)  *)
(*                                                              *)
(****************************************************************)

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

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

lemma Euler_part3: "[| 2 < p; p ∈ zprime; ~([x = 0](mod p));
QuadRes p x |] ==> [x^(nat (((p) - 1) div 2)) = 1](mod p)";
apply (subgoal_tac "p ∈ zOdd")
apply (frule aux__1, auto)
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 (frule odd_minus_one_even)
apply (frule even_div_2_prop2)
apply (auto intro: Little_Fermat simp add: zprime_zOdd_eq_grt_2)
done

(********************************************************************)
(*                                                                  *)
(* Finally show Euler's Criterion                                   *)
(*                                                                  *)
(********************************************************************)

theorem Euler_Criterion: "[| 2 < p; p ∈ zprime |] ==> [(Legendre a p) =
a^(nat (((p) - 1) div 2))] (mod p)";
apply (auto simp add: Legendre_def Euler_part2)
apply (frule Euler_part3, auto simp add: zcong_sym)
apply (frule Euler_part1, auto simp add: zcong_sym)
done

end
```

lemma MultInvPair_prop1a:

```  [| p ∈ zprime; 2 < p; ¬ [a = 0] (mod p); X ∈ SetS a p; Y ∈ SetS a p;
X ∩ Y ≠ {} |]
==> X = Y```

lemma MultInvPair_prop1b:

```  [| p ∈ zprime; 2 < p; ¬ [a = 0] (mod p); X ∈ SetS a p; Y ∈ SetS a p; X ≠ Y |]
==> X ∩ Y = {}```

lemma MultInvPair_prop1c:

```  [| p ∈ zprime; 2 < p; ¬ [a = 0] (mod p) |]
==> ∀X∈SetS a p. ∀Y∈SetS a p. X ≠ Y --> X ∩ Y = {}```

lemma MultInvPair_prop2:

`  [| p ∈ zprime; 2 < p; ¬ [a = 0] (mod p) |] ==> Union (SetS a p) = SRStar p`

lemma MultInvPair_distinct:

```  [| p ∈ zprime; 2 < p; ¬ [a = 0] (mod p); ¬ [j = 0] (mod p); ¬ QuadRes p a |]
==> ¬ [j = a * MultInv p j] (mod p)```

lemma MultInvPair_card_two:

```  [| p ∈ zprime; 2 < p; ¬ [a = 0] (mod p); ¬ QuadRes p a; ¬ [j = 0] (mod p) |]
==> card (MultInvPair a p j) = 2```

lemma SetS_finite:

`  2 < p ==> finite (SetS a p)`

lemma SetS_elems_finite:

`  ∀X∈SetS a p. finite X`

lemma SetS_elems_card:

```  [| p ∈ zprime; 2 < p; ¬ [a = 0] (mod p); ¬ QuadRes p a |]
==> ∀X∈SetS a p. card X = 2```

lemma Union_SetS_finite:

`  2 < p ==> finite (Union (SetS a p))`

lemma card_setsum_aux:

`  [| finite S; ∀X∈S. finite X; ∀X∈S. card X = n |] ==> setsum card S = (∑x∈S. n)`

lemma SetS_card:

```  [| p ∈ zprime; 2 < p; ¬ [a = 0] (mod p); ¬ QuadRes p a |]
==> int (card (SetS a p)) = (p - 1) div 2```

lemma SetS_ssetprod_prop:

```  [| p ∈ zprime; 2 < p; ¬ [a = 0] (mod p); ¬ QuadRes p a; x ∈ SetS a p |]
==> [ssetprod x = a] (mod p)```

lemma aux1:

`  [| 0 < x; x < a; x ≠ a - 1 |] ==> x < a - 1`

lemma aux2:

`  [| a < c; b < c |] ==> a ≤ b ∨ b ≤ a`

lemma SRStar_d22set_prop:

`  2 < p ==> SRStar p = {1} ∪ d22set (p - 1)`

lemma ssetprod_setprod_id:

`  ssetprod A = setprod id A`

lemma ssetprod_disj_sets:

```  [| finite A; ∀X∈A. finite X; ∀X∈A. ∀Y∈A. X ≠ Y --> X ∩ Y = {} |]
==> ssetprod (Union A) = setprod ssetprod A```

lemma Union_SetS_ssetprod_prop1:

```  [| p ∈ zprime; 2 < p; ¬ [a = 0] (mod p); ¬ QuadRes p a |]
==> [ssetprod (Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)```

lemma Union_SetS_ssetprod_prop2:

```  [| p ∈ zprime; 2 < p; ¬ [a = 0] (mod p) |]
==> ssetprod (Union (SetS a p)) = zfact (p - 1)```

lemma zfact_prop:

```  [| p ∈ zprime; 2 < p; ¬ [a = 0] (mod p); ¬ QuadRes p a |]
==> [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)```

lemma Euler_part1:

```  [| 2 < p; p ∈ zprime; ¬ [x = 0] (mod p); ¬ QuadRes p x |]
==> [x ^ nat ((p - 1) div 2) = -1] (mod p)```

lemma aux_1:

`  0 < p ==> a ^ nat p = a * a ^ (nat p - 1)`

lemma aux_2:

`  [| 2 < p; p ∈ zOdd |] ==> 0 < (p - 1) div 2`

lemma Euler_part2:

```  [| 2 < p; p ∈ zprime; [a = 0] (mod p) |]
==> [0 = a ^ nat ((p - 1) div 2)] (mod p)```

lemma aux__1:

`  [| ¬ [x = 0] (mod p); [y² = x] (mod p) |] ==> ¬ p dvd y`

lemma aux__2:

`  2 * nat ((p - 1) div 2) = nat (2 * ((p - 1) div 2))`

lemma Euler_part3:

```  [| 2 < p; p ∈ zprime; ¬ [x = 0] (mod p); QuadRes p x |]
==> [x ^ nat ((p - 1) div 2) = 1] (mod p)```

theorem Euler_Criterion:

`  [| 2 < p; p ∈ zprime |] ==> [Legendre a p = a ^ nat ((p - 1) div 2)] (mod p)`