--- a/src/HOL/Old_Number_Theory/BijectionRel.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/BijectionRel.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,10 +1,13 @@
-(* Author: Thomas M. Rasmussen
+(* Title: HOL/Old_Number_Theory/BijectionRel.thy
+ Author: Thomas M. Rasmussen
Copyright 2000 University of Cambridge
*)
header {* Bijections between sets *}
-theory BijectionRel imports Main begin
+theory BijectionRel
+imports Main
+begin
text {*
Inductive definitions of bijections between two different sets and
--- a/src/HOL/Old_Number_Theory/Chinese.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Chinese.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,4 +1,5 @@
-(* Author: Thomas M. Rasmussen
+(* Title: HOL/Old_Number_Theory/Chinese.thy
+ Author: Thomas M. Rasmussen
Copyright 2000 University of Cambridge
*)
@@ -19,17 +20,15 @@
subsection {* Definitions *}
-consts
- funprod :: "(nat => int) => nat => nat => int"
- funsum :: "(nat => int) => nat => nat => int"
-
-primrec
+primrec funprod :: "(nat => int) => nat => nat => int"
+where
"funprod f i 0 = f i"
- "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
+| "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
-primrec
+primrec funsum :: "(nat => int) => nat => nat => int"
+where
"funsum f i 0 = f i"
- "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
+| "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
definition
m_cond :: "nat => (nat => int) => bool" where
--- a/src/HOL/Old_Number_Theory/Euler.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,19 +1,18 @@
-(* Title: HOL/Quadratic_Reciprocity/Euler.thy
- ID: $Id$
+(* Title: HOL/Old_Number_Theory/Euler.thy
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
header {* Euler's criterion *}
-theory Euler imports Residues EvenOdd begin
+theory Euler
+imports Residues EvenOdd
+begin
-definition
- MultInvPair :: "int => int => int => int set" where
- "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
+definition MultInvPair :: "int => int => int => int set"
+ where "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
-definition
- SetS :: "int => int => int set set" where
- "SetS a p = (MultInvPair a p ` SRStar p)"
+definition SetS :: "int => int => int set set"
+ where "SetS a p = MultInvPair a p ` SRStar p"
subsection {* Property for MultInvPair *}
--- 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 *}
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Quadratic_Reciprocity/EvenOdd.thy
+(* Title: HOL/Old_Number_Theory/EvenOdd.thy
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
@@ -8,13 +8,11 @@
imports Int2
begin
-definition
- zOdd :: "int set" where
- "zOdd = {x. \<exists>k. x = 2 * k + 1}"
+definition zOdd :: "int set"
+ where "zOdd = {x. \<exists>k. x = 2 * k + 1}"
-definition
- zEven :: "int set" where
- "zEven = {x. \<exists>k. x = 2 * k}"
+definition zEven :: "int set"
+ where "zEven = {x. \<exists>k. x = 2 * k}"
subsection {* Some useful properties about even and odd *}
--- a/src/HOL/Old_Number_Theory/Factorization.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Factorization.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,41 +1,39 @@
-(* Author: Thomas Marthedal Rasmussen
+(* Title: HOL/Old_Number_Theory/Factorization.thy
+ Author: Thomas Marthedal Rasmussen
Copyright 2000 University of Cambridge
*)
header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
theory Factorization
-imports Main "~~/src/HOL/Old_Number_Theory/Primes" Permutation
+imports Primes Permutation
begin
subsection {* Definitions *}
-definition
- primel :: "nat list => bool" where
- "primel xs = (\<forall>p \<in> set xs. prime p)"
+definition primel :: "nat list => bool"
+ where "primel xs = (\<forall>p \<in> set xs. prime p)"
-consts
- nondec :: "nat list => bool "
- prod :: "nat list => nat"
- oinsert :: "nat => nat list => nat list"
- sort :: "nat list => nat list"
-
-primrec
+primrec nondec :: "nat list => bool"
+where
"nondec [] = True"
- "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
+| "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
-primrec
+primrec prod :: "nat list => nat"
+where
"prod [] = Suc 0"
- "prod (x # xs) = x * prod xs"
+| "prod (x # xs) = x * prod xs"
-primrec
+primrec oinsert :: "nat => nat list => nat list"
+where
"oinsert x [] = [x]"
- "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)"
+| "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)"
-primrec
+primrec sort :: "nat list => nat list"
+where
"sort [] = []"
- "sort (x # xs) = oinsert x (sort xs)"
+| "sort (x # xs) = oinsert x (sort xs)"
subsection {* Arithmetic *}
--- a/src/HOL/Old_Number_Theory/Fib.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Fib.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,4 +1,4 @@
-(* ID: $Id$
+(* Title: HOL/Old_Number_Theory/Fib.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
*)
@@ -19,8 +19,8 @@
fun fib :: "nat \<Rightarrow> nat"
where
- "fib 0 = 0"
-| "fib (Suc 0) = 1"
+ "fib 0 = 0"
+| "fib (Suc 0) = 1"
| fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)"
text {*
--- a/src/HOL/Old_Number_Theory/Finite2.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Finite2.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,12 +1,11 @@
-(* Title: HOL/Quadratic_Reciprocity/Finite2.thy
- ID: $Id$
+(* Title: HOL/Old_Number_Theory/Finite2.thy
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
header {*Finite Sets and Finite Sums*}
theory Finite2
-imports Main IntFact Infinite_Set
+imports IntFact Infinite_Set
begin
text{*
--- a/src/HOL/Old_Number_Theory/Gauss.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,6 +1,5 @@
-(* Title: HOL/Quadratic_Reciprocity/Gauss.thy
- ID: $Id$
- Authors: Jeremy Avigad, David Gray, and Adam Kramer)
+(* Title: HOL/Old_Number_Theory/Gauss.thy
+ Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
header {* Gauss' Lemma *}
@@ -19,29 +18,12 @@
assumes a_nonzero: "0 < a"
begin
-definition
- A :: "int set" where
- "A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
-
-definition
- B :: "int set" where
- "B = (%x. x * a) ` A"
-
-definition
- C :: "int set" where
- "C = StandardRes p ` B"
-
-definition
- D :: "int set" where
- "D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
-
-definition
- E :: "int set" where
- "E = C \<inter> {x. ((p - 1) div 2) < x}"
-
-definition
- F :: "int set" where
- "F = (%x. (p - x)) ` E"
+definition "A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
+definition "B = (%x. x * a) ` A"
+definition "C = StandardRes p ` B"
+definition "D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
+definition "E = C \<inter> {x. ((p - 1) div 2) < x}"
+definition "F = (%x. (p - x)) ` E"
subsection {* Basic properties of p *}
--- a/src/HOL/Old_Number_Theory/Int2.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Int2.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,5 +1,4 @@
-(* Title: HOL/Quadratic_Reciprocity/Gauss.thy
- ID: $Id$
+(* Title: HOL/Old_Number_Theory/Int2.thy
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
@@ -9,9 +8,8 @@
imports Finite2 WilsonRuss
begin
-definition
- MultInv :: "int => int => int" where
- "MultInv p x = x ^ nat (p - 2)"
+definition MultInv :: "int => int => int"
+ where "MultInv p x = x ^ nat (p - 2)"
subsection {* Useful lemmas about dvd and powers *}
--- a/src/HOL/Old_Number_Theory/IntFact.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/IntFact.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,10 +1,13 @@
-(* Author: Thomas M. Rasmussen
+(* Title: HOL/Old_Number_Theory/IntFact.thy
+ Author: Thomas M. Rasmussen
Copyright 2000 University of Cambridge
*)
header {* Factorial on integers *}
-theory IntFact imports IntPrimes begin
+theory IntFact
+imports IntPrimes
+begin
text {*
Factorial on integers and recursively defined set including all
@@ -14,15 +17,11 @@
\bigskip
*}
-fun
- zfact :: "int => int"
-where
- "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
+fun zfact :: "int => int"
+ where "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
-fun
- d22set :: "int => int set"
-where
- "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
+fun d22set :: "int => int set"
+ where "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
text {*
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,11 +1,12 @@
-(* Author: Thomas M. Rasmussen
+(* Title: HOL/Old_Number_Theory/IntPrimes.thy
+ Author: Thomas M. Rasmussen
Copyright 2000 University of Cambridge
*)
header {* Divisibility and prime numbers (on integers) *}
theory IntPrimes
-imports Main Primes
+imports Primes
begin
text {*
@@ -19,8 +20,7 @@
subsection {* Definitions *}
-fun
- xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
+fun xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
where
"xzgcda m n r' r s' s t' t =
(if r \<le> 0 then (r', s', t')
@@ -28,17 +28,15 @@
s (s' - (r' div r) * s)
t (t' - (r' div r) * t))"
-definition
- zprime :: "int \<Rightarrow> bool" where
- "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
+definition zprime :: "int \<Rightarrow> bool"
+ where "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
-definition
- xzgcd :: "int => int => int * int * int" where
- "xzgcd m n = xzgcda m n m n 1 0 0 1"
+definition xzgcd :: "int => int => int * int * int"
+ where "xzgcd m n = xzgcda m n m n 1 0 0 1"
-definition
- zcong :: "int => int => int => bool" ("(1[_ = _] '(mod _'))") where
- "[a = b] (mod m) = (m dvd (a - b))"
+definition zcong :: "int => int => int => bool" ("(1[_ = _] '(mod _'))")
+ where "[a = b] (mod m) = (m dvd (a - b))"
+
subsection {* Euclid's Algorithm and GCD *}
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Fri Aug 06 12:37:00 2010 +0200
@@ -38,17 +38,17 @@
subsection {* GCD on nat by Euclid's algorithm *}
-fun
- gcd :: "nat => nat => nat"
-where
- "gcd m n = (if n = 0 then m else gcd n (m mod n))"
+fun gcd :: "nat => nat => nat"
+ where "gcd m n = (if n = 0 then m else gcd n (m mod n))"
+
lemma gcd_induct [case_names "0" rec]:
fixes m n :: nat
assumes "\<And>m. P m 0"
and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
shows "P m n"
proof (induct m n rule: gcd.induct)
- case (1 m n) with assms show ?case by (cases "n = 0") simp_all
+ case (1 m n)
+ with assms show ?case by (cases "n = 0") simp_all
qed
lemma gcd_0 [simp, algebra]: "gcd m 0 = m"
@@ -751,22 +751,22 @@
lemma lcm_pos:
assumes mpos: "m > 0"
- and npos: "n>0"
+ and npos: "n>0"
shows "lcm m n > 0"
-proof(rule ccontr, simp add: lcm_def gcd_zero)
-assume h:"m*n div gcd m n = 0"
-from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
-hence gcdp: "gcd m n > 0" by simp
-with h
-have "m*n < gcd m n"
- by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
-moreover
-have "gcd m n dvd m" by simp
- with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
- with npos have t1:"gcd m n *n \<le> m*n" by simp
- have "gcd m n \<le> gcd m n*n" using npos by simp
- with t1 have "gcd m n \<le> m*n" by arith
-ultimately show "False" by simp
+proof (rule ccontr, simp add: lcm_def gcd_zero)
+ assume h:"m*n div gcd m n = 0"
+ from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
+ hence gcdp: "gcd m n > 0" by simp
+ with h
+ have "m*n < gcd m n"
+ by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
+ moreover
+ have "gcd m n dvd m" by simp
+ with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
+ with npos have t1:"gcd m n *n \<le> m*n" by simp
+ have "gcd m n \<le> gcd m n*n" using npos by simp
+ with t1 have "gcd m n \<le> m*n" by arith
+ ultimately show "False" by simp
qed
lemma zlcm_pos:
--- a/src/HOL/Old_Number_Theory/Pocklington.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,11 +1,11 @@
-(* Title: HOL/Library/Pocklington.thy
+(* Title: HOL/Old_Number_Theory/Pocklington.thy
Author: Amine Chaieb
*)
header {* Pocklington's Theorem for Primes *}
theory Pocklington
-imports Main Primes
+imports Primes
begin
definition modeq:: "nat => nat => nat => bool" ("(1[_ = _] '(mod _'))")
--- a/src/HOL/Old_Number_Theory/Primes.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/Primes.thy
+(* Title: HOL/Old_Number_Theory/Primes.thy
Author: Amine Chaieb, Christophe Tabacznyj and Lawrence C Paulson
Copyright 1996 University of Cambridge
*)
@@ -9,13 +9,11 @@
imports Complex_Main Legacy_GCD
begin
-definition
- coprime :: "nat => nat => bool" where
- "coprime m n \<longleftrightarrow> gcd m n = 1"
+definition coprime :: "nat => nat => bool"
+ where "coprime m n \<longleftrightarrow> gcd m n = 1"
-definition
- prime :: "nat \<Rightarrow> bool" where
- "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+definition prime :: "nat \<Rightarrow> bool"
+ where "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
lemma two_is_prime: "prime 2"
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,4 +1,5 @@
-(* Authors: Jeremy Avigad, David Gray, and Adam Kramer
+(* Title: HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
+ Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
header {* The law of Quadratic reciprocity *}
@@ -165,33 +166,26 @@
assumes p_neq_q: "p \<noteq> q"
begin
-definition
- P_set :: "int set" where
- "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
+definition P_set :: "int set"
+ where "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
-definition
- Q_set :: "int set" where
- "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
+definition Q_set :: "int set"
+ where "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
-definition
- S :: "(int * int) set" where
- "S = P_set <*> Q_set"
+definition S :: "(int * int) set"
+ where "S = P_set <*> Q_set"
-definition
- S1 :: "(int * int) set" where
- "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
+definition S1 :: "(int * int) set"
+ where "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
-definition
- S2 :: "(int * int) set" where
- "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
+definition S2 :: "(int * int) set"
+ where "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
-definition
- f1 :: "int => (int * int) set" where
- "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
+definition f1 :: "int => (int * int) set"
+ where "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
-definition
- f2 :: "int => (int * int) set" where
- "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
+definition f2 :: "int => (int * int) set"
+ where "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
lemma p_fact: "0 < (p - 1) div 2"
proof -
--- a/src/HOL/Old_Number_Theory/Residues.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Residues.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,41 +1,36 @@
-(* Title: HOL/Quadratic_Reciprocity/Residues.thy
- ID: $Id$
+(* Title: HOL/Old_Number_Theory/Residues.thy
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
header {* Residue Sets *}
-theory Residues imports Int2 begin
+theory Residues
+imports Int2
+begin
text {*
\medskip Define the residue of a set, the standard residue,
quadratic residues, and prove some basic properties. *}
-definition
- ResSet :: "int => int set => bool" where
- "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
+definition ResSet :: "int => int set => bool"
+ where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
-definition
- StandardRes :: "int => int => int" where
- "StandardRes m x = x mod m"
+definition StandardRes :: "int => int => int"
+ where "StandardRes m x = x mod m"
-definition
- QuadRes :: "int => int => bool" where
- "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
+definition QuadRes :: "int => int => bool"
+ where "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
-definition
- Legendre :: "int => int => int" where
+definition Legendre :: "int => int => int" where
"Legendre a p = (if ([a = 0] (mod p)) then 0
else if (QuadRes p a) then 1
else -1)"
-definition
- SR :: "int => int set" where
- "SR p = {x. (0 \<le> x) & (x < p)}"
+definition SR :: "int => int set"
+ where "SR p = {x. (0 \<le> x) & (x < p)}"
-definition
- SRStar :: "int => int set" where
- "SRStar p = {x. (0 < x) & (x < p)}"
+definition SRStar :: "int => int set"
+ where "SRStar p = {x. (0 < x) & (x < p)}"
subsection {* Some useful properties of StandardRes *}
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,10 +1,13 @@
-(* Author: Thomas M. Rasmussen
+(* Title: HOL/Old_Number_Theory/WilsonBij.thy
+ Author: Thomas M. Rasmussen
Copyright 2000 University of Cambridge
*)
header {* Wilson's Theorem using a more abstract approach *}
-theory WilsonBij imports BijectionRel IntFact begin
+theory WilsonBij
+imports BijectionRel IntFact
+begin
text {*
Wilson's Theorem using a more ``abstract'' approach based on
@@ -15,12 +18,10 @@
subsection {* Definitions and lemmas *}
-definition
- reciR :: "int => int => int => bool" 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)"
+definition reciR :: "int => int => int => bool"
+ 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)"
-definition
- inv :: "int => int => int" where
+definition inv :: "int => int => int" where
"inv p a =
(if zprime p \<and> 0 < a \<and> a < p then
(SOME x. 0 \<le> x \<and> x < p \<and> zcong (a * x) 1 p)
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Fri Aug 06 12:37:00 2010 +0200
@@ -1,10 +1,13 @@
-(* Author: Thomas M. Rasmussen
+(* Title: HOL/Old_Number_Theory/WilsonRuss.thy
+ Author: Thomas M. Rasmussen
Copyright 2000 University of Cambridge
*)
header {* Wilson's Theorem according to Russinoff *}
-theory WilsonRuss imports EulerFermat begin
+theory WilsonRuss
+imports EulerFermat
+begin
text {*
Wilson's Theorem following quite closely Russinoff's approach
@@ -13,13 +16,10 @@
subsection {* Definitions and lemmas *}
-definition
- inv :: "int => int => int" where
- "inv p a = (a^(nat (p - 2))) mod p"
+definition inv :: "int => int => int"
+ where "inv p a = (a^(nat (p - 2))) mod p"
-fun
- wset :: "int \<Rightarrow> int => int set"
-where
+fun wset :: "int \<Rightarrow> int => int set" where
"wset a p =
(if 1 < a then
let ws = wset (a - 1) p
@@ -29,7 +29,7 @@
text {* \medskip @{term [source] inv} *}
lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
-by (subst int_int_eq [symmetric], auto)
+ by (subst int_int_eq [symmetric]) auto
lemma inv_is_inv:
"zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"