1.1 --- a/src/HOL/Old_Number_Theory/BijectionRel.thy Thu Aug 05 23:43:43 2010 +0200
1.2 +++ b/src/HOL/Old_Number_Theory/BijectionRel.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/BijectionRel.thy
1.6 + Author: Thomas M. Rasmussen
1.7 Copyright 2000 University of Cambridge
1.8 *)
1.9
1.10 header {* Bijections between sets *}
1.11
1.12 -theory BijectionRel imports Main begin
1.13 +theory BijectionRel
1.14 +imports Main
1.15 +begin
1.16
1.17 text {*
1.18 Inductive definitions of bijections between two different sets and
2.1 --- a/src/HOL/Old_Number_Theory/Chinese.thy Thu Aug 05 23:43:43 2010 +0200
2.2 +++ b/src/HOL/Old_Number_Theory/Chinese.thy Fri Aug 06 12:37:00 2010 +0200
2.3 @@ -1,4 +1,5 @@
2.4 -(* Author: Thomas M. Rasmussen
2.5 +(* Title: HOL/Old_Number_Theory/Chinese.thy
2.6 + Author: Thomas M. Rasmussen
2.7 Copyright 2000 University of Cambridge
2.8 *)
2.9
2.10 @@ -19,17 +20,15 @@
2.11
2.12 subsection {* Definitions *}
2.13
2.14 -consts
2.15 - funprod :: "(nat => int) => nat => nat => int"
2.16 - funsum :: "(nat => int) => nat => nat => int"
2.17 +primrec funprod :: "(nat => int) => nat => nat => int"
2.18 +where
2.19 + "funprod f i 0 = f i"
2.20 +| "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
2.21
2.22 -primrec
2.23 - "funprod f i 0 = f i"
2.24 - "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
2.25 -
2.26 -primrec
2.27 +primrec funsum :: "(nat => int) => nat => nat => int"
2.28 +where
2.29 "funsum f i 0 = f i"
2.30 - "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
2.31 +| "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
2.32
2.33 definition
2.34 m_cond :: "nat => (nat => int) => bool" where
3.1 --- a/src/HOL/Old_Number_Theory/Euler.thy Thu Aug 05 23:43:43 2010 +0200
3.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy Fri Aug 06 12:37:00 2010 +0200
3.3 @@ -1,19 +1,18 @@
3.4 -(* Title: HOL/Quadratic_Reciprocity/Euler.thy
3.5 - ID: $Id$
3.6 +(* Title: HOL/Old_Number_Theory/Euler.thy
3.7 Authors: Jeremy Avigad, David Gray, and Adam Kramer
3.8 *)
3.9
3.10 header {* Euler's criterion *}
3.11
3.12 -theory Euler imports Residues EvenOdd begin
3.13 +theory Euler
3.14 +imports Residues EvenOdd
3.15 +begin
3.16
3.17 -definition
3.18 - MultInvPair :: "int => int => int => int set" where
3.19 - "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
3.20 +definition MultInvPair :: "int => int => int => int set"
3.21 + where "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
3.22
3.23 -definition
3.24 - SetS :: "int => int => int set set" where
3.25 - "SetS a p = (MultInvPair a p ` SRStar p)"
3.26 +definition SetS :: "int => int => int set set"
3.27 + where "SetS a p = MultInvPair a p ` SRStar p"
3.28
3.29
3.30 subsection {* Property for MultInvPair *}
4.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy Thu Aug 05 23:43:43 2010 +0200
4.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Fri Aug 06 12:37:00 2010 +0200
4.3 @@ -1,4 +1,5 @@
4.4 -(* Author: Thomas M. Rasmussen
4.5 +(* Title: HOL/Old_Number_Theory/EulerFermat.thy
4.6 + Author: Thomas M. Rasmussen
4.7 Copyright 2000 University of Cambridge
4.8 *)
4.9
4.10 @@ -17,49 +18,40 @@
4.11
4.12 subsection {* Definitions and lemmas *}
4.13
4.14 -inductive_set
4.15 - RsetR :: "int => int set set"
4.16 - for m :: int
4.17 - where
4.18 - empty [simp]: "{} \<in> RsetR m"
4.19 - | insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
4.20 - \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
4.21 +inductive_set RsetR :: "int => int set set" for m :: int
4.22 +where
4.23 + empty [simp]: "{} \<in> RsetR m"
4.24 +| insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
4.25 + \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
4.26
4.27 -fun
4.28 - BnorRset :: "int \<Rightarrow> int => int set"
4.29 -where
4.30 +fun BnorRset :: "int \<Rightarrow> int => int set" where
4.31 "BnorRset a m =
4.32 (if 0 < a then
4.33 let na = BnorRset (a - 1) m
4.34 in (if zgcd a m = 1 then insert a na else na)
4.35 else {})"
4.36
4.37 -definition
4.38 - norRRset :: "int => int set" where
4.39 - "norRRset m = BnorRset (m - 1) m"
4.40 +definition norRRset :: "int => int set"
4.41 + where "norRRset m = BnorRset (m - 1) m"
4.42
4.43 -definition
4.44 - noXRRset :: "int => int => int set" where
4.45 - "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
4.46 +definition noXRRset :: "int => int => int set"
4.47 + where "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
4.48
4.49 -definition
4.50 - phi :: "int => nat" where
4.51 - "phi m = card (norRRset m)"
4.52 +definition phi :: "int => nat"
4.53 + where "phi m = card (norRRset m)"
4.54
4.55 -definition
4.56 - is_RRset :: "int set => int => bool" where
4.57 - "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
4.58 +definition is_RRset :: "int set => int => bool"
4.59 + where "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
4.60
4.61 -definition
4.62 - RRset2norRR :: "int set => int => int => int" where
4.63 - "RRset2norRR A m a =
4.64 - (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
4.65 - SOME b. zcong a b m \<and> b \<in> norRRset m
4.66 - else 0)"
4.67 +definition RRset2norRR :: "int set => int => int => int"
4.68 + where
4.69 + "RRset2norRR A m a =
4.70 + (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
4.71 + SOME b. zcong a b m \<and> b \<in> norRRset m
4.72 + else 0)"
4.73
4.74 -definition
4.75 - zcongm :: "int => int => int => bool" where
4.76 - "zcongm m = (\<lambda>a b. zcong a b m)"
4.77 +definition zcongm :: "int => int => int => bool"
4.78 + where "zcongm m = (\<lambda>a b. zcong a b m)"
4.79
4.80 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
4.81 -- {* LCP: not sure why this lemma is needed now *}
5.1 --- a/src/HOL/Old_Number_Theory/EvenOdd.thy Thu Aug 05 23:43:43 2010 +0200
5.2 +++ b/src/HOL/Old_Number_Theory/EvenOdd.thy Fri Aug 06 12:37:00 2010 +0200
5.3 @@ -1,4 +1,4 @@
5.4 -(* Title: HOL/Quadratic_Reciprocity/EvenOdd.thy
5.5 +(* Title: HOL/Old_Number_Theory/EvenOdd.thy
5.6 Authors: Jeremy Avigad, David Gray, and Adam Kramer
5.7 *)
5.8
5.9 @@ -8,13 +8,11 @@
5.10 imports Int2
5.11 begin
5.12
5.13 -definition
5.14 - zOdd :: "int set" where
5.15 - "zOdd = {x. \<exists>k. x = 2 * k + 1}"
5.16 +definition zOdd :: "int set"
5.17 + where "zOdd = {x. \<exists>k. x = 2 * k + 1}"
5.18
5.19 -definition
5.20 - zEven :: "int set" where
5.21 - "zEven = {x. \<exists>k. x = 2 * k}"
5.22 +definition zEven :: "int set"
5.23 + where "zEven = {x. \<exists>k. x = 2 * k}"
5.24
5.25 subsection {* Some useful properties about even and odd *}
5.26
6.1 --- a/src/HOL/Old_Number_Theory/Factorization.thy Thu Aug 05 23:43:43 2010 +0200
6.2 +++ b/src/HOL/Old_Number_Theory/Factorization.thy Fri Aug 06 12:37:00 2010 +0200
6.3 @@ -1,41 +1,39 @@
6.4 -(* Author: Thomas Marthedal Rasmussen
6.5 +(* Title: HOL/Old_Number_Theory/Factorization.thy
6.6 + Author: Thomas Marthedal Rasmussen
6.7 Copyright 2000 University of Cambridge
6.8 *)
6.9
6.10 header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
6.11
6.12 theory Factorization
6.13 -imports Main "~~/src/HOL/Old_Number_Theory/Primes" Permutation
6.14 +imports Primes Permutation
6.15 begin
6.16
6.17
6.18 subsection {* Definitions *}
6.19
6.20 -definition
6.21 - primel :: "nat list => bool" where
6.22 - "primel xs = (\<forall>p \<in> set xs. prime p)"
6.23 +definition primel :: "nat list => bool"
6.24 + where "primel xs = (\<forall>p \<in> set xs. prime p)"
6.25
6.26 -consts
6.27 - nondec :: "nat list => bool "
6.28 - prod :: "nat list => nat"
6.29 - oinsert :: "nat => nat list => nat list"
6.30 - sort :: "nat list => nat list"
6.31 +primrec nondec :: "nat list => bool"
6.32 +where
6.33 + "nondec [] = True"
6.34 +| "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
6.35
6.36 -primrec
6.37 - "nondec [] = True"
6.38 - "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
6.39 +primrec prod :: "nat list => nat"
6.40 +where
6.41 + "prod [] = Suc 0"
6.42 +| "prod (x # xs) = x * prod xs"
6.43
6.44 -primrec
6.45 - "prod [] = Suc 0"
6.46 - "prod (x # xs) = x * prod xs"
6.47 +primrec oinsert :: "nat => nat list => nat list"
6.48 +where
6.49 + "oinsert x [] = [x]"
6.50 +| "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)"
6.51
6.52 -primrec
6.53 - "oinsert x [] = [x]"
6.54 - "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)"
6.55 -
6.56 -primrec
6.57 +primrec sort :: "nat list => nat list"
6.58 +where
6.59 "sort [] = []"
6.60 - "sort (x # xs) = oinsert x (sort xs)"
6.61 +| "sort (x # xs) = oinsert x (sort xs)"
6.62
6.63
6.64 subsection {* Arithmetic *}
7.1 --- a/src/HOL/Old_Number_Theory/Fib.thy Thu Aug 05 23:43:43 2010 +0200
7.2 +++ b/src/HOL/Old_Number_Theory/Fib.thy Fri Aug 06 12:37:00 2010 +0200
7.3 @@ -1,4 +1,4 @@
7.4 -(* ID: $Id$
7.5 +(* Title: HOL/Old_Number_Theory/Fib.thy
7.6 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
7.7 Copyright 1997 University of Cambridge
7.8 *)
7.9 @@ -19,8 +19,8 @@
7.10
7.11 fun fib :: "nat \<Rightarrow> nat"
7.12 where
7.13 - "fib 0 = 0"
7.14 -| "fib (Suc 0) = 1"
7.15 + "fib 0 = 0"
7.16 +| "fib (Suc 0) = 1"
7.17 | fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)"
7.18
7.19 text {*
8.1 --- a/src/HOL/Old_Number_Theory/Finite2.thy Thu Aug 05 23:43:43 2010 +0200
8.2 +++ b/src/HOL/Old_Number_Theory/Finite2.thy Fri Aug 06 12:37:00 2010 +0200
8.3 @@ -1,12 +1,11 @@
8.4 -(* Title: HOL/Quadratic_Reciprocity/Finite2.thy
8.5 - ID: $Id$
8.6 +(* Title: HOL/Old_Number_Theory/Finite2.thy
8.7 Authors: Jeremy Avigad, David Gray, and Adam Kramer
8.8 *)
8.9
8.10 header {*Finite Sets and Finite Sums*}
8.11
8.12 theory Finite2
8.13 -imports Main IntFact Infinite_Set
8.14 +imports IntFact Infinite_Set
8.15 begin
8.16
8.17 text{*
9.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy Thu Aug 05 23:43:43 2010 +0200
9.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy Fri Aug 06 12:37:00 2010 +0200
9.3 @@ -1,6 +1,5 @@
9.4 -(* Title: HOL/Quadratic_Reciprocity/Gauss.thy
9.5 - ID: $Id$
9.6 - Authors: Jeremy Avigad, David Gray, and Adam Kramer)
9.7 +(* Title: HOL/Old_Number_Theory/Gauss.thy
9.8 + Authors: Jeremy Avigad, David Gray, and Adam Kramer
9.9 *)
9.10
9.11 header {* Gauss' Lemma *}
9.12 @@ -19,29 +18,12 @@
9.13 assumes a_nonzero: "0 < a"
9.14 begin
9.15
9.16 -definition
9.17 - A :: "int set" where
9.18 - "A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
9.19 -
9.20 -definition
9.21 - B :: "int set" where
9.22 - "B = (%x. x * a) ` A"
9.23 -
9.24 -definition
9.25 - C :: "int set" where
9.26 - "C = StandardRes p ` B"
9.27 -
9.28 -definition
9.29 - D :: "int set" where
9.30 - "D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
9.31 -
9.32 -definition
9.33 - E :: "int set" where
9.34 - "E = C \<inter> {x. ((p - 1) div 2) < x}"
9.35 -
9.36 -definition
9.37 - F :: "int set" where
9.38 - "F = (%x. (p - x)) ` E"
9.39 +definition "A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
9.40 +definition "B = (%x. x * a) ` A"
9.41 +definition "C = StandardRes p ` B"
9.42 +definition "D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
9.43 +definition "E = C \<inter> {x. ((p - 1) div 2) < x}"
9.44 +definition "F = (%x. (p - x)) ` E"
9.45
9.46
9.47 subsection {* Basic properties of p *}
10.1 --- a/src/HOL/Old_Number_Theory/Int2.thy Thu Aug 05 23:43:43 2010 +0200
10.2 +++ b/src/HOL/Old_Number_Theory/Int2.thy Fri Aug 06 12:37:00 2010 +0200
10.3 @@ -1,5 +1,4 @@
10.4 -(* Title: HOL/Quadratic_Reciprocity/Gauss.thy
10.5 - ID: $Id$
10.6 +(* Title: HOL/Old_Number_Theory/Int2.thy
10.7 Authors: Jeremy Avigad, David Gray, and Adam Kramer
10.8 *)
10.9
10.10 @@ -9,9 +8,8 @@
10.11 imports Finite2 WilsonRuss
10.12 begin
10.13
10.14 -definition
10.15 - MultInv :: "int => int => int" where
10.16 - "MultInv p x = x ^ nat (p - 2)"
10.17 +definition MultInv :: "int => int => int"
10.18 + where "MultInv p x = x ^ nat (p - 2)"
10.19
10.20
10.21 subsection {* Useful lemmas about dvd and powers *}
11.1 --- a/src/HOL/Old_Number_Theory/IntFact.thy Thu Aug 05 23:43:43 2010 +0200
11.2 +++ b/src/HOL/Old_Number_Theory/IntFact.thy Fri Aug 06 12:37:00 2010 +0200
11.3 @@ -1,10 +1,13 @@
11.4 -(* Author: Thomas M. Rasmussen
11.5 +(* Title: HOL/Old_Number_Theory/IntFact.thy
11.6 + Author: Thomas M. Rasmussen
11.7 Copyright 2000 University of Cambridge
11.8 *)
11.9
11.10 header {* Factorial on integers *}
11.11
11.12 -theory IntFact imports IntPrimes begin
11.13 +theory IntFact
11.14 +imports IntPrimes
11.15 +begin
11.16
11.17 text {*
11.18 Factorial on integers and recursively defined set including all
11.19 @@ -14,15 +17,11 @@
11.20 \bigskip
11.21 *}
11.22
11.23 -fun
11.24 - zfact :: "int => int"
11.25 -where
11.26 - "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
11.27 +fun zfact :: "int => int"
11.28 + where "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
11.29
11.30 -fun
11.31 - d22set :: "int => int set"
11.32 -where
11.33 - "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
11.34 +fun d22set :: "int => int set"
11.35 + where "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
11.36
11.37
11.38 text {*
12.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy Thu Aug 05 23:43:43 2010 +0200
12.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Fri Aug 06 12:37:00 2010 +0200
12.3 @@ -1,11 +1,12 @@
12.4 -(* Author: Thomas M. Rasmussen
12.5 +(* Title: HOL/Old_Number_Theory/IntPrimes.thy
12.6 + Author: Thomas M. Rasmussen
12.7 Copyright 2000 University of Cambridge
12.8 *)
12.9
12.10 header {* Divisibility and prime numbers (on integers) *}
12.11
12.12 theory IntPrimes
12.13 -imports Main Primes
12.14 +imports Primes
12.15 begin
12.16
12.17 text {*
12.18 @@ -19,8 +20,7 @@
12.19
12.20 subsection {* Definitions *}
12.21
12.22 -fun
12.23 - xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
12.24 +fun xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
12.25 where
12.26 "xzgcda m n r' r s' s t' t =
12.27 (if r \<le> 0 then (r', s', t')
12.28 @@ -28,17 +28,15 @@
12.29 s (s' - (r' div r) * s)
12.30 t (t' - (r' div r) * t))"
12.31
12.32 -definition
12.33 - zprime :: "int \<Rightarrow> bool" where
12.34 - "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
12.35 +definition zprime :: "int \<Rightarrow> bool"
12.36 + where "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
12.37
12.38 -definition
12.39 - xzgcd :: "int => int => int * int * int" where
12.40 - "xzgcd m n = xzgcda m n m n 1 0 0 1"
12.41 +definition xzgcd :: "int => int => int * int * int"
12.42 + where "xzgcd m n = xzgcda m n m n 1 0 0 1"
12.43
12.44 -definition
12.45 - zcong :: "int => int => int => bool" ("(1[_ = _] '(mod _'))") where
12.46 - "[a = b] (mod m) = (m dvd (a - b))"
12.47 +definition zcong :: "int => int => int => bool" ("(1[_ = _] '(mod _'))")
12.48 + where "[a = b] (mod m) = (m dvd (a - b))"
12.49 +
12.50
12.51 subsection {* Euclid's Algorithm and GCD *}
12.52
13.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Aug 05 23:43:43 2010 +0200
13.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Fri Aug 06 12:37:00 2010 +0200
13.3 @@ -38,17 +38,17 @@
13.4
13.5 subsection {* GCD on nat by Euclid's algorithm *}
13.6
13.7 -fun
13.8 - gcd :: "nat => nat => nat"
13.9 -where
13.10 - "gcd m n = (if n = 0 then m else gcd n (m mod n))"
13.11 +fun gcd :: "nat => nat => nat"
13.12 + where "gcd m n = (if n = 0 then m else gcd n (m mod n))"
13.13 +
13.14 lemma gcd_induct [case_names "0" rec]:
13.15 fixes m n :: nat
13.16 assumes "\<And>m. P m 0"
13.17 and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
13.18 shows "P m n"
13.19 proof (induct m n rule: gcd.induct)
13.20 - case (1 m n) with assms show ?case by (cases "n = 0") simp_all
13.21 + case (1 m n)
13.22 + with assms show ?case by (cases "n = 0") simp_all
13.23 qed
13.24
13.25 lemma gcd_0 [simp, algebra]: "gcd m 0 = m"
13.26 @@ -751,22 +751,22 @@
13.27
13.28 lemma lcm_pos:
13.29 assumes mpos: "m > 0"
13.30 - and npos: "n>0"
13.31 + and npos: "n>0"
13.32 shows "lcm m n > 0"
13.33 -proof(rule ccontr, simp add: lcm_def gcd_zero)
13.34 -assume h:"m*n div gcd m n = 0"
13.35 -from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
13.36 -hence gcdp: "gcd m n > 0" by simp
13.37 -with h
13.38 -have "m*n < gcd m n"
13.39 - by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
13.40 -moreover
13.41 -have "gcd m n dvd m" by simp
13.42 - with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
13.43 - with npos have t1:"gcd m n *n \<le> m*n" by simp
13.44 - have "gcd m n \<le> gcd m n*n" using npos by simp
13.45 - with t1 have "gcd m n \<le> m*n" by arith
13.46 -ultimately show "False" by simp
13.47 +proof (rule ccontr, simp add: lcm_def gcd_zero)
13.48 + assume h:"m*n div gcd m n = 0"
13.49 + from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
13.50 + hence gcdp: "gcd m n > 0" by simp
13.51 + with h
13.52 + have "m*n < gcd m n"
13.53 + by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
13.54 + moreover
13.55 + have "gcd m n dvd m" by simp
13.56 + with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
13.57 + with npos have t1:"gcd m n *n \<le> m*n" by simp
13.58 + have "gcd m n \<le> gcd m n*n" using npos by simp
13.59 + with t1 have "gcd m n \<le> m*n" by arith
13.60 + ultimately show "False" by simp
13.61 qed
13.62
13.63 lemma zlcm_pos:
14.1 --- a/src/HOL/Old_Number_Theory/Pocklington.thy Thu Aug 05 23:43:43 2010 +0200
14.2 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy Fri Aug 06 12:37:00 2010 +0200
14.3 @@ -1,11 +1,11 @@
14.4 -(* Title: HOL/Library/Pocklington.thy
14.5 +(* Title: HOL/Old_Number_Theory/Pocklington.thy
14.6 Author: Amine Chaieb
14.7 *)
14.8
14.9 header {* Pocklington's Theorem for Primes *}
14.10
14.11 theory Pocklington
14.12 -imports Main Primes
14.13 +imports Primes
14.14 begin
14.15
14.16 definition modeq:: "nat => nat => nat => bool" ("(1[_ = _] '(mod _'))")
15.1 --- a/src/HOL/Old_Number_Theory/Primes.thy Thu Aug 05 23:43:43 2010 +0200
15.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy Fri Aug 06 12:37:00 2010 +0200
15.3 @@ -1,4 +1,4 @@
15.4 -(* Title: HOL/Library/Primes.thy
15.5 +(* Title: HOL/Old_Number_Theory/Primes.thy
15.6 Author: Amine Chaieb, Christophe Tabacznyj and Lawrence C Paulson
15.7 Copyright 1996 University of Cambridge
15.8 *)
15.9 @@ -9,13 +9,11 @@
15.10 imports Complex_Main Legacy_GCD
15.11 begin
15.12
15.13 -definition
15.14 - coprime :: "nat => nat => bool" where
15.15 - "coprime m n \<longleftrightarrow> gcd m n = 1"
15.16 +definition coprime :: "nat => nat => bool"
15.17 + where "coprime m n \<longleftrightarrow> gcd m n = 1"
15.18
15.19 -definition
15.20 - prime :: "nat \<Rightarrow> bool" where
15.21 - "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
15.22 +definition prime :: "nat \<Rightarrow> bool"
15.23 + where "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
15.24
15.25
15.26 lemma two_is_prime: "prime 2"
16.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Thu Aug 05 23:43:43 2010 +0200
16.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Fri Aug 06 12:37:00 2010 +0200
16.3 @@ -1,4 +1,5 @@
16.4 -(* Authors: Jeremy Avigad, David Gray, and Adam Kramer
16.5 +(* Title: HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
16.6 + Authors: Jeremy Avigad, David Gray, and Adam Kramer
16.7 *)
16.8
16.9 header {* The law of Quadratic reciprocity *}
16.10 @@ -165,33 +166,26 @@
16.11 assumes p_neq_q: "p \<noteq> q"
16.12 begin
16.13
16.14 -definition
16.15 - P_set :: "int set" where
16.16 - "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
16.17 +definition P_set :: "int set"
16.18 + where "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
16.19
16.20 -definition
16.21 - Q_set :: "int set" where
16.22 - "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
16.23 +definition Q_set :: "int set"
16.24 + where "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
16.25
16.26 -definition
16.27 - S :: "(int * int) set" where
16.28 - "S = P_set <*> Q_set"
16.29 +definition S :: "(int * int) set"
16.30 + where "S = P_set <*> Q_set"
16.31
16.32 -definition
16.33 - S1 :: "(int * int) set" where
16.34 - "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
16.35 +definition S1 :: "(int * int) set"
16.36 + where "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
16.37
16.38 -definition
16.39 - S2 :: "(int * int) set" where
16.40 - "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
16.41 +definition S2 :: "(int * int) set"
16.42 + where "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
16.43
16.44 -definition
16.45 - f1 :: "int => (int * int) set" where
16.46 - "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
16.47 +definition f1 :: "int => (int * int) set"
16.48 + where "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
16.49
16.50 -definition
16.51 - f2 :: "int => (int * int) set" where
16.52 - "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
16.53 +definition f2 :: "int => (int * int) set"
16.54 + where "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
16.55
16.56 lemma p_fact: "0 < (p - 1) div 2"
16.57 proof -
17.1 --- a/src/HOL/Old_Number_Theory/Residues.thy Thu Aug 05 23:43:43 2010 +0200
17.2 +++ b/src/HOL/Old_Number_Theory/Residues.thy Fri Aug 06 12:37:00 2010 +0200
17.3 @@ -1,41 +1,36 @@
17.4 -(* Title: HOL/Quadratic_Reciprocity/Residues.thy
17.5 - ID: $Id$
17.6 +(* Title: HOL/Old_Number_Theory/Residues.thy
17.7 Authors: Jeremy Avigad, David Gray, and Adam Kramer
17.8 *)
17.9
17.10 header {* Residue Sets *}
17.11
17.12 -theory Residues imports Int2 begin
17.13 +theory Residues
17.14 +imports Int2
17.15 +begin
17.16
17.17 text {*
17.18 \medskip Define the residue of a set, the standard residue,
17.19 quadratic residues, and prove some basic properties. *}
17.20
17.21 -definition
17.22 - ResSet :: "int => int set => bool" where
17.23 - "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
17.24 +definition ResSet :: "int => int set => bool"
17.25 + where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
17.26
17.27 -definition
17.28 - StandardRes :: "int => int => int" where
17.29 - "StandardRes m x = x mod m"
17.30 +definition StandardRes :: "int => int => int"
17.31 + where "StandardRes m x = x mod m"
17.32
17.33 -definition
17.34 - QuadRes :: "int => int => bool" where
17.35 - "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
17.36 +definition QuadRes :: "int => int => bool"
17.37 + where "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
17.38
17.39 -definition
17.40 - Legendre :: "int => int => int" where
17.41 +definition Legendre :: "int => int => int" where
17.42 "Legendre a p = (if ([a = 0] (mod p)) then 0
17.43 else if (QuadRes p a) then 1
17.44 else -1)"
17.45
17.46 -definition
17.47 - SR :: "int => int set" where
17.48 - "SR p = {x. (0 \<le> x) & (x < p)}"
17.49 +definition SR :: "int => int set"
17.50 + where "SR p = {x. (0 \<le> x) & (x < p)}"
17.51
17.52 -definition
17.53 - SRStar :: "int => int set" where
17.54 - "SRStar p = {x. (0 < x) & (x < p)}"
17.55 +definition SRStar :: "int => int set"
17.56 + where "SRStar p = {x. (0 < x) & (x < p)}"
17.57
17.58
17.59 subsection {* Some useful properties of StandardRes *}
18.1 --- a/src/HOL/Old_Number_Theory/WilsonBij.thy Thu Aug 05 23:43:43 2010 +0200
18.2 +++ b/src/HOL/Old_Number_Theory/WilsonBij.thy Fri Aug 06 12:37:00 2010 +0200
18.3 @@ -1,10 +1,13 @@
18.4 -(* Author: Thomas M. Rasmussen
18.5 +(* Title: HOL/Old_Number_Theory/WilsonBij.thy
18.6 + Author: Thomas M. Rasmussen
18.7 Copyright 2000 University of Cambridge
18.8 *)
18.9
18.10 header {* Wilson's Theorem using a more abstract approach *}
18.11
18.12 -theory WilsonBij imports BijectionRel IntFact begin
18.13 +theory WilsonBij
18.14 +imports BijectionRel IntFact
18.15 +begin
18.16
18.17 text {*
18.18 Wilson's Theorem using a more ``abstract'' approach based on
18.19 @@ -15,12 +18,10 @@
18.20
18.21 subsection {* Definitions and lemmas *}
18.22
18.23 -definition
18.24 - reciR :: "int => int => int => bool" where
18.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)"
18.26 +definition reciR :: "int => int => int => bool"
18.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)"
18.28
18.29 -definition
18.30 - inv :: "int => int => int" where
18.31 +definition inv :: "int => int => int" where
18.32 "inv p a =
18.33 (if zprime p \<and> 0 < a \<and> a < p then
18.34 (SOME x. 0 \<le> x \<and> x < p \<and> zcong (a * x) 1 p)
19.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Thu Aug 05 23:43:43 2010 +0200
19.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Fri Aug 06 12:37:00 2010 +0200
19.3 @@ -1,10 +1,13 @@
19.4 -(* Author: Thomas M. Rasmussen
19.5 +(* Title: HOL/Old_Number_Theory/WilsonRuss.thy
19.6 + Author: Thomas M. Rasmussen
19.7 Copyright 2000 University of Cambridge
19.8 *)
19.9
19.10 header {* Wilson's Theorem according to Russinoff *}
19.11
19.12 -theory WilsonRuss imports EulerFermat begin
19.13 +theory WilsonRuss
19.14 +imports EulerFermat
19.15 +begin
19.16
19.17 text {*
19.18 Wilson's Theorem following quite closely Russinoff's approach
19.19 @@ -13,13 +16,10 @@
19.20
19.21 subsection {* Definitions and lemmas *}
19.22
19.23 -definition
19.24 - inv :: "int => int => int" where
19.25 - "inv p a = (a^(nat (p - 2))) mod p"
19.26 +definition inv :: "int => int => int"
19.27 + where "inv p a = (a^(nat (p - 2))) mod p"
19.28
19.29 -fun
19.30 - wset :: "int \<Rightarrow> int => int set"
19.31 -where
19.32 +fun wset :: "int \<Rightarrow> int => int set" where
19.33 "wset a p =
19.34 (if 1 < a then
19.35 let ws = wset (a - 1) p
19.36 @@ -29,7 +29,7 @@
19.37 text {* \medskip @{term [source] inv} *}
19.38
19.39 lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
19.40 -by (subst int_int_eq [symmetric], auto)
19.41 + by (subst int_int_eq [symmetric]) auto
19.42
19.43 lemma inv_is_inv:
19.44 "zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"