src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 38159 e9b4835a54ee
parent 35440 bdf8ad377877
child 39159 0dec18004e75
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Thu Aug 05 23:43:43 2010 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Fri Aug 06 12:37:00 2010 +0200
     1.3 @@ -1,10 +1,13 @@
     1.4 -(*  Author:     Thomas M. Rasmussen
     1.5 +(*  Title:      HOL/Old_Number_Theory/WilsonRuss.thy
     1.6 +    Author:     Thomas M. Rasmussen
     1.7      Copyright   2000  University of Cambridge
     1.8  *)
     1.9  
    1.10  header {* Wilson's Theorem according to Russinoff *}
    1.11  
    1.12 -theory WilsonRuss imports EulerFermat begin
    1.13 +theory WilsonRuss
    1.14 +imports EulerFermat
    1.15 +begin
    1.16  
    1.17  text {*
    1.18    Wilson's Theorem following quite closely Russinoff's approach
    1.19 @@ -13,13 +16,10 @@
    1.20  
    1.21  subsection {* Definitions and lemmas *}
    1.22  
    1.23 -definition
    1.24 -  inv :: "int => int => int" where
    1.25 -  "inv p a = (a^(nat (p - 2))) mod p"
    1.26 +definition inv :: "int => int => int"
    1.27 +  where "inv p a = (a^(nat (p - 2))) mod p"
    1.28  
    1.29 -fun
    1.30 -  wset :: "int \<Rightarrow> int => int set"
    1.31 -where
    1.32 +fun wset :: "int \<Rightarrow> int => int set" where
    1.33    "wset a p =
    1.34      (if 1 < a then
    1.35        let ws = wset (a - 1) p
    1.36 @@ -29,7 +29,7 @@
    1.37  text {* \medskip @{term [source] inv} *}
    1.38  
    1.39  lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
    1.40 -by (subst int_int_eq [symmetric], auto)
    1.41 +  by (subst int_int_eq [symmetric]) auto
    1.42  
    1.43  lemma inv_is_inv:
    1.44      "zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"