src/HOL/Old_Number_Theory/WilsonBij.thy
changeset 38159 e9b4835a54ee
parent 35048 82ab78fff970
child 39159 0dec18004e75
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Thu Aug 05 23:43:43 2010 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonBij.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/WilsonBij.thy
     1.6 +    Author:     Thomas M. Rasmussen
     1.7      Copyright   2000  University of Cambridge
     1.8  *)
     1.9  
    1.10  header {* Wilson's Theorem using a more abstract approach *}
    1.11  
    1.12 -theory WilsonBij imports BijectionRel IntFact begin
    1.13 +theory WilsonBij
    1.14 +imports BijectionRel IntFact
    1.15 +begin
    1.16  
    1.17  text {*
    1.18    Wilson's Theorem using a more ``abstract'' approach based on
    1.19 @@ -15,12 +18,10 @@
    1.20  
    1.21  subsection {* Definitions and lemmas *}
    1.22  
    1.23 -definition
    1.24 -  reciR :: "int => int => int => bool" where
    1.25 -  "reciR p = (\<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1)"
    1.26 +definition reciR :: "int => int => int => bool"
    1.27 +  where "reciR p = (\<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1)"
    1.28  
    1.29 -definition
    1.30 -  inv :: "int => int => int" where
    1.31 +definition inv :: "int => int => int" where
    1.32    "inv p a =
    1.33      (if zprime p \<and> 0 < a \<and> a < p then
    1.34        (SOME x. 0 \<le> x \<and> x < p \<and> zcong (a * x) 1 p)