src/HOL/Old_Number_Theory/Euler.thy
changeset 61382 efac889fccbc
parent 58889 5b7a9633cfa8
child 61649 268d88ec9087
     1.1 --- a/src/HOL/Old_Number_Theory/Euler.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     1.5  *)
     1.6  
     1.7 -section {* Euler's criterion *}
     1.8 +section \<open>Euler's criterion\<close>
     1.9  
    1.10  theory Euler
    1.11  imports Residues EvenOdd
    1.12 @@ -15,7 +15,7 @@
    1.13    where "SetS a p = MultInvPair a p ` SRStar p"
    1.14  
    1.15  
    1.16 -subsection {* Property for MultInvPair *}
    1.17 +subsection \<open>Property for MultInvPair\<close>
    1.18  
    1.19  lemma MultInvPair_prop1a:
    1.20    "[| zprime p; 2 < p; ~([a = 0](mod p));
    1.21 @@ -89,7 +89,7 @@
    1.22    done
    1.23  
    1.24  
    1.25 -subsection {* Properties of SetS *}
    1.26 +subsection \<open>Properties of SetS\<close>
    1.27  
    1.28  lemma SetS_finite: "2 < p ==> finite (SetS a p)"
    1.29    by (auto simp add: SetS_def SRStar_finite [of p])
    1.30 @@ -223,14 +223,14 @@
    1.31    apply (auto simp add: Union_SetS_setprod_prop2)
    1.32    done
    1.33  
    1.34 -text {* \medskip Prove the first part of Euler's Criterion: *}
    1.35 +text \<open>\medskip Prove the first part of Euler's Criterion:\<close>
    1.36  
    1.37  lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
    1.38      ~(QuadRes p x) |] ==> 
    1.39        [x^(nat (((p) - 1) div 2)) = -1](mod p)"
    1.40    by (metis Wilson_Russ zcong_sym zcong_trans zfact_prop)
    1.41  
    1.42 -text {* \medskip Prove another part of Euler Criterion: *}
    1.43 +text \<open>\medskip Prove another part of Euler Criterion:\<close>
    1.44  
    1.45  lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
    1.46  proof -
    1.47 @@ -251,7 +251,7 @@
    1.48      by (auto simp add: zEven_def zOdd_def)
    1.49    then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
    1.50      by (auto simp add: even_div_2_prop2)
    1.51 -  with `2 < p` have "1 < (p - 1)"
    1.52 +  with \<open>2 < p\<close> have "1 < (p - 1)"
    1.53      by auto
    1.54    then have " 1 < (2 * ((p - 1) div 2))"
    1.55      by (auto simp add: aux_1)
    1.56 @@ -268,7 +268,7 @@
    1.57    apply (frule zcong_zmult_prop1, auto)
    1.58    done
    1.59  
    1.60 -text {* \medskip Prove the final part of Euler's Criterion: *}
    1.61 +text \<open>\medskip Prove the final part of Euler's Criterion:\<close>
    1.62  
    1.63  lemma aux__1: "[| ~([x = 0] (mod p)); [y\<^sup>2 = x] (mod p)|] ==> ~(p dvd y)"
    1.64    by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
    1.65 @@ -291,7 +291,7 @@
    1.66    done
    1.67  
    1.68  
    1.69 -text {* \medskip Finally show Euler's Criterion: *}
    1.70 +text \<open>\medskip Finally show Euler's Criterion:\<close>
    1.71  
    1.72  theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
    1.73      a^(nat (((p) - 1) div 2))] (mod p)"