src/HOL/Old_Number_Theory/EulerFermat.thy

--- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,4 +1,5 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/EulerFermat.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
@@ -17,49 +18,40 @@
 
 subsection {* Definitions and lemmas *}
 
-inductive_set
-  RsetR :: "int => int set set"
-  for m :: int
-  where
-    empty [simp]: "{} \<in> RsetR m"
-  | insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
-      \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
+inductive_set RsetR :: "int => int set set" for m :: int
+where
+  empty [simp]: "{} \<in> RsetR m"
+| insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
+    \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
 
-fun
-  BnorRset :: "int \<Rightarrow> int => int set"
-where
+fun BnorRset :: "int \<Rightarrow> int => int set" where
   "BnorRset a m =
    (if 0 < a then
     let na = BnorRset (a - 1) m
     in (if zgcd a m = 1 then insert a na else na)
     else {})"
 
-definition
-  norRRset :: "int => int set" where
-  "norRRset m = BnorRset (m - 1) m"
+definition norRRset :: "int => int set"
+  where "norRRset m = BnorRset (m - 1) m"
 
-definition
-  noXRRset :: "int => int => int set" where
-  "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
+definition noXRRset :: "int => int => int set"
+  where "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
 
-definition
-  phi :: "int => nat" where
-  "phi m = card (norRRset m)"
+definition phi :: "int => nat"
+  where "phi m = card (norRRset m)"
 
-definition
-  is_RRset :: "int set => int => bool" where
-  "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
+definition is_RRset :: "int set => int => bool"
+  where "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
 
-definition
-  RRset2norRR :: "int set => int => int => int" where
-  "RRset2norRR A m a =
-     (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
-        SOME b. zcong a b m \<and> b \<in> norRRset m
-      else 0)"
+definition RRset2norRR :: "int set => int => int => int"
+  where
+    "RRset2norRR A m a =
+       (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
+          SOME b. zcong a b m \<and> b \<in> norRRset m
+        else 0)"
 
-definition
-  zcongm :: "int => int => int => bool" where
-  "zcongm m = (\<lambda>a b. zcong a b m)"
+definition zcongm :: "int => int => int => bool"
+  where "zcongm m = (\<lambda>a b. zcong a b m)"
 
 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
   -- {* LCP: not sure why this lemma is needed now *}