src/HOL/Old_Number_Theory/EulerFermat.thy
changeset 38159 e9b4835a54ee
parent 35440 bdf8ad377877
child 40786 0a54cfc9add3
     1.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Thu Aug 05 23:43:43 2010 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Fri Aug 06 12:37:00 2010 +0200
     1.3 @@ -1,4 +1,5 @@
     1.4 -(*  Author:     Thomas M. Rasmussen
     1.5 +(*  Title:      HOL/Old_Number_Theory/EulerFermat.thy
     1.6 +    Author:     Thomas M. Rasmussen
     1.7      Copyright   2000  University of Cambridge
     1.8  *)
     1.9  
    1.10 @@ -17,49 +18,40 @@
    1.11  
    1.12  subsection {* Definitions and lemmas *}
    1.13  
    1.14 -inductive_set
    1.15 -  RsetR :: "int => int set set"
    1.16 -  for m :: int
    1.17 -  where
    1.18 -    empty [simp]: "{} \<in> RsetR m"
    1.19 -  | insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
    1.20 -      \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
    1.21 +inductive_set RsetR :: "int => int set set" for m :: int
    1.22 +where
    1.23 +  empty [simp]: "{} \<in> RsetR m"
    1.24 +| insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
    1.25 +    \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
    1.26  
    1.27 -fun
    1.28 -  BnorRset :: "int \<Rightarrow> int => int set"
    1.29 -where
    1.30 +fun BnorRset :: "int \<Rightarrow> int => int set" where
    1.31    "BnorRset a m =
    1.32     (if 0 < a then
    1.33      let na = BnorRset (a - 1) m
    1.34      in (if zgcd a m = 1 then insert a na else na)
    1.35      else {})"
    1.36  
    1.37 -definition
    1.38 -  norRRset :: "int => int set" where
    1.39 -  "norRRset m = BnorRset (m - 1) m"
    1.40 +definition norRRset :: "int => int set"
    1.41 +  where "norRRset m = BnorRset (m - 1) m"
    1.42  
    1.43 -definition
    1.44 -  noXRRset :: "int => int => int set" where
    1.45 -  "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
    1.46 +definition noXRRset :: "int => int => int set"
    1.47 +  where "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
    1.48  
    1.49 -definition
    1.50 -  phi :: "int => nat" where
    1.51 -  "phi m = card (norRRset m)"
    1.52 +definition phi :: "int => nat"
    1.53 +  where "phi m = card (norRRset m)"
    1.54  
    1.55 -definition
    1.56 -  is_RRset :: "int set => int => bool" where
    1.57 -  "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
    1.58 +definition is_RRset :: "int set => int => bool"
    1.59 +  where "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
    1.60  
    1.61 -definition
    1.62 -  RRset2norRR :: "int set => int => int => int" where
    1.63 -  "RRset2norRR A m a =
    1.64 -     (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
    1.65 -        SOME b. zcong a b m \<and> b \<in> norRRset m
    1.66 -      else 0)"
    1.67 +definition RRset2norRR :: "int set => int => int => int"
    1.68 +  where
    1.69 +    "RRset2norRR A m a =
    1.70 +       (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
    1.71 +          SOME b. zcong a b m \<and> b \<in> norRRset m
    1.72 +        else 0)"
    1.73  
    1.74 -definition
    1.75 -  zcongm :: "int => int => int => bool" where
    1.76 -  "zcongm m = (\<lambda>a b. zcong a b m)"
    1.77 +definition zcongm :: "int => int => int => bool"
    1.78 +  where "zcongm m = (\<lambda>a b. zcong a b m)"
    1.79  
    1.80  lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
    1.81    -- {* LCP: not sure why this lemma is needed now *}