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