src/HOL/Old_Number_Theory/EulerFermat.thy
```     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 *}
```