1.1 --- a/src/ZF/Induct/Comb.thy Wed Apr 27 16:40:27 2005 +0200
1.2 +++ b/src/ZF/Induct/Comb.thy Wed Apr 27 16:41:03 2005 +0200
1.3 @@ -39,7 +39,7 @@
1.4 "p ---> q" == "<p,q> \<in> contract^*"
1.5
1.6 syntax (xsymbols)
1.7 - "app" :: "[i, i] => i" (infixl "\<bullet>" 90)
1.8 + "comb.app" :: "[i, i] => i" (infixl "\<bullet>" 90)
1.9
1.10 inductive
1.11 domains "contract" \<subseteq> "comb \<times> comb"
1.12 @@ -158,8 +158,6 @@
1.13 and S_contractE [elim!]: "S -1-> r"
1.14 and Ap_contractE [elim!]: "p\<bullet>q -1-> r"
1.15
1.16 -declare contract.Ap1 [intro] contract.Ap2 [intro]
1.17 -
1.18 lemma I_contract_E: "I -1-> r ==> P"
1.19 by (auto simp add: I_def)
1.20
2.1 --- a/src/ZF/ex/Primes.thy Wed Apr 27 16:40:27 2005 +0200
2.2 +++ b/src/ZF/ex/Primes.thy Wed Apr 27 16:41:03 2005 +0200
2.3 @@ -2,33 +2,32 @@
2.4 ID: $Id$
2.5 Author: Christophe Tabacznyj and Lawrence C Paulson
2.6 Copyright 1996 University of Cambridge
2.7 +*)
2.8
2.9 -The "divides" relation, the greatest common divisor and Euclid's algorithm
2.10 -*)
2.11 +header{*The Divides Relation and Euclid's algorithm for the GCD*}
2.12
2.13 theory Primes = Main:
2.14 constdefs
2.15 divides :: "[i,i]=>o" (infixl "dvd" 50)
2.16 "m dvd n == m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
2.17
2.18 - is_gcd :: "[i,i,i]=>o" (* great common divisor *)
2.19 + is_gcd :: "[i,i,i]=>o" --{*definition of great common divisor*}
2.20 "is_gcd(p,m,n) == ((p dvd m) & (p dvd n)) &
2.21 (\<forall>d\<in>nat. (d dvd m) & (d dvd n) --> d dvd p)"
2.22
2.23 - gcd :: "[i,i]=>i" (* gcd by Euclid's algorithm *)
2.24 + gcd :: "[i,i]=>i" --{*Euclid's algorithm for the gcd*}
2.25 "gcd(m,n) == transrec(natify(n),
2.26 %n f. \<lambda>m \<in> nat.
2.27 if n=0 then m else f`(m mod n)`n) ` natify(m)"
2.28
2.29 - coprime :: "[i,i]=>o" (* coprime relation *)
2.30 + coprime :: "[i,i]=>o" --{*the coprime relation*}
2.31 "coprime(m,n) == gcd(m,n) = 1"
2.32
2.33 - prime :: i (* set of prime numbers *)
2.34 + prime :: i --{*the set of prime numbers*}
2.35 "prime == {p \<in> nat. 1<p & (\<forall>m \<in> nat. m dvd p --> m=1 | m=p)}"
2.36
2.37 -(************************************************)
2.38 -(** Divides Relation **)
2.39 -(************************************************)
2.40 +
2.41 +subsection{*The Divides Relation*}
2.42
2.43 lemma dvdD: "m dvd n ==> m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
2.44 by (unfold divides_def, assumption)
2.45 @@ -42,50 +41,42 @@
2.46
2.47
2.48 lemma dvd_0_right [simp]: "m \<in> nat ==> m dvd 0"
2.49 -apply (unfold divides_def)
2.50 +apply (simp add: divides_def)
2.51 apply (fast intro: nat_0I mult_0_right [symmetric])
2.52 done
2.53
2.54 lemma dvd_0_left: "0 dvd m ==> m = 0"
2.55 -by (unfold divides_def, force)
2.56 +by (simp add: divides_def)
2.57
2.58 lemma dvd_refl [simp]: "m \<in> nat ==> m dvd m"
2.59 -apply (unfold divides_def)
2.60 +apply (simp add: divides_def)
2.61 apply (fast intro: nat_1I mult_1_right [symmetric])
2.62 done
2.63
2.64 lemma dvd_trans: "[| m dvd n; n dvd p |] ==> m dvd p"
2.65 -apply (unfold divides_def)
2.66 -apply (fast intro: mult_assoc mult_type)
2.67 -done
2.68 +by (auto simp add: divides_def intro: mult_assoc mult_type)
2.69
2.70 lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m=n"
2.71 -apply (unfold divides_def)
2.72 +apply (simp add: divides_def)
2.73 apply (force dest: mult_eq_self_implies_10
2.74 simp add: mult_assoc mult_eq_1_iff)
2.75 done
2.76
2.77 lemma dvd_mult_left: "[|(i#*j) dvd k; i \<in> nat|] ==> i dvd k"
2.78 -apply (unfold divides_def)
2.79 -apply (simp add: mult_assoc, blast)
2.80 -done
2.81 +by (auto simp add: divides_def mult_assoc)
2.82
2.83 lemma dvd_mult_right: "[|(i#*j) dvd k; j \<in> nat|] ==> j dvd k"
2.84 -apply (unfold divides_def, clarify)
2.85 +apply (simp add: divides_def, clarify)
2.86 apply (rule_tac x = "i#*k" in bexI)
2.87 apply (simp add: mult_ac)
2.88 apply (rule mult_type)
2.89 done
2.90
2.91
2.92 -(************************************************)
2.93 -(** Greatest Common Divisor **)
2.94 -(************************************************)
2.95 -
2.96 -(* GCD by Euclid's Algorithm *)
2.97 +subsection{*Euclid's Algorithm for the GCD*}
2.98
2.99 lemma gcd_0 [simp]: "gcd(m,0) = natify(m)"
2.100 -apply (unfold gcd_def)
2.101 +apply (simp add: gcd_def)
2.102 apply (subst transrec, simp)
2.103 done
2.104
2.105 @@ -97,7 +88,7 @@
2.106
2.107 lemma gcd_non_0_raw:
2.108 "[| 0<n; n \<in> nat |] ==> gcd(m,n) = gcd(n, m mod n)"
2.109 -apply (unfold gcd_def)
2.110 +apply (simp add: gcd_def)
2.111 apply (rule_tac P = "%z. ?left (z) = ?right" in transrec [THEN ssubst])
2.112 apply (simp add: ltD [THEN mem_imp_not_eq, THEN not_sym]
2.113 mod_less_divisor [THEN ltD])
2.114 @@ -112,12 +103,12 @@
2.115 by (simp (no_asm_simp) add: gcd_non_0)
2.116
2.117 lemma dvd_add: "[| k dvd a; k dvd b |] ==> k dvd (a #+ b)"
2.118 -apply (unfold divides_def)
2.119 +apply (simp add: divides_def)
2.120 apply (fast intro: add_mult_distrib_left [symmetric] add_type)
2.121 done
2.122
2.123 lemma dvd_mult: "k dvd n ==> k dvd (m #* n)"
2.124 -apply (unfold divides_def)
2.125 +apply (simp add: divides_def)
2.126 apply (fast intro: mult_left_commute mult_type)
2.127 done
2.128
2.129 @@ -132,7 +123,7 @@
2.130
2.131 lemma dvd_mod_imp_dvd_raw:
2.132 "[| a \<in> nat; b \<in> nat; k dvd b; k dvd (a mod b) |] ==> k dvd a"
2.133 -apply (case_tac "b=0")
2.134 +apply (case_tac "b=0")
2.135 apply (simp add: DIVISION_BY_ZERO_MOD)
2.136 apply (blast intro: mod_div_equality [THEN subst]
2.137 elim: dvdE
2.138 @@ -166,9 +157,9 @@
2.139 by (blast intro: gcd_induct_lemma)
2.140
2.141
2.142 +subsection{*Basic Properties of @{term gcd}*}
2.143
2.144 -(* gcd type *)
2.145 -
2.146 +text{*type of gcd*}
2.147 lemma gcd_type [simp,TC]: "gcd(m, n) \<in> nat"
2.148 apply (subgoal_tac "gcd (natify (m), natify (n)) \<in> nat")
2.149 apply simp
2.150 @@ -178,7 +169,7 @@
2.151 done
2.152
2.153
2.154 -(* Property 1: gcd(a,b) divides a and b *)
2.155 +text{* Property 1: gcd(a,b) divides a and b *}
2.156
2.157 lemma gcd_dvd_both:
2.158 "[| m \<in> nat; n \<in> nat |] ==> gcd (m, n) dvd m & gcd (m, n) dvd n"
2.159 @@ -197,17 +188,17 @@
2.160 apply auto
2.161 done
2.162
2.163 -(* if f divides a and b then f divides gcd(a,b) *)
2.164 +text{* if f divides a and b then f divides gcd(a,b) *}
2.165
2.166 lemma dvd_mod: "[| f dvd a; f dvd b |] ==> f dvd (a mod b)"
2.167 -apply (unfold divides_def)
2.168 +apply (simp add: divides_def)
2.169 apply (case_tac "b=0")
2.170 apply (simp add: DIVISION_BY_ZERO_MOD, auto)
2.171 apply (blast intro: mod_mult_distrib2 [symmetric])
2.172 done
2.173
2.174 -(* Property 2: for all a,b,f naturals,
2.175 - if f divides a and f divides b then f divides gcd(a,b)*)
2.176 +text{* Property 2: for all a,b,f naturals,
2.177 + if f divides a and f divides b then f divides gcd(a,b)*}
2.178
2.179 lemma gcd_greatest_raw [rule_format]:
2.180 "[| m \<in> nat; n \<in> nat; f \<in> nat |]
2.181 @@ -226,20 +217,22 @@
2.182 by (blast intro!: gcd_greatest gcd_dvd1 gcd_dvd2 intro: dvd_trans)
2.183
2.184
2.185 -(* GCD PROOF: GCD exists and gcd fits the definition *)
2.186 +subsection{*The Greatest Common Divisor*}
2.187 +
2.188 +text{*The GCD exists and function gcd computes it.*}
2.189
2.190 lemma is_gcd: "[| m \<in> nat; n \<in> nat |] ==> is_gcd(gcd(m,n), m, n)"
2.191 by (simp add: is_gcd_def)
2.192
2.193 -(* GCD is unique *)
2.194 +text{*The GCD is unique*}
2.195
2.196 lemma is_gcd_unique: "[|is_gcd(m,a,b); is_gcd(n,a,b); m\<in>nat; n\<in>nat|] ==> m=n"
2.197 -apply (unfold is_gcd_def)
2.198 +apply (simp add: is_gcd_def)
2.199 apply (blast intro: dvd_anti_sym)
2.200 done
2.201
2.202 lemma is_gcd_commute: "is_gcd(k,m,n) <-> is_gcd(k,n,m)"
2.203 -by (unfold is_gcd_def, blast)
2.204 +by (simp add: is_gcd_def, blast)
2.205
2.206 lemma gcd_commute_raw: "[| m \<in> nat; n \<in> nat |] ==> gcd(m,n) = gcd(n,m)"
2.207 apply (rule is_gcd_unique)
2.208 @@ -274,7 +267,36 @@
2.209 by (simp add: gcd_commute [of 1])
2.210
2.211
2.212 -(* Multiplication laws *)
2.213 +subsection{*Addition laws*}
2.214 +
2.215 +lemma gcd_add1 [simp]: "gcd (m #+ n, n) = gcd (m, n)"
2.216 +apply (subgoal_tac "gcd (m #+ natify (n), natify (n)) = gcd (m, natify (n))")
2.217 +apply simp
2.218 +apply (case_tac "natify (n) = 0")
2.219 +apply (auto simp add: Ord_0_lt_iff gcd_non_0)
2.220 +done
2.221 +
2.222 +lemma gcd_add2 [simp]: "gcd (m, m #+ n) = gcd (m, n)"
2.223 +apply (rule gcd_commute [THEN trans])
2.224 +apply (subst add_commute, simp)
2.225 +apply (rule gcd_commute)
2.226 +done
2.227 +
2.228 +lemma gcd_add2' [simp]: "gcd (m, n #+ m) = gcd (m, n)"
2.229 +by (subst add_commute, rule gcd_add2)
2.230 +
2.231 +lemma gcd_add_mult_raw: "k \<in> nat ==> gcd (m, k #* m #+ n) = gcd (m, n)"
2.232 +apply (erule nat_induct)
2.233 +apply (auto simp add: gcd_add2 add_assoc)
2.234 +done
2.235 +
2.236 +lemma gcd_add_mult: "gcd (m, k #* m #+ n) = gcd (m, n)"
2.237 +apply (cut_tac k = "natify (k)" in gcd_add_mult_raw)
2.238 +apply auto
2.239 +done
2.240 +
2.241 +
2.242 +subsection{* Multiplication Laws*}
2.243
2.244 lemma gcd_mult_distrib2_raw:
2.245 "[| k \<in> nat; m \<in> nat; n \<in> nat |]
2.246 @@ -310,59 +332,28 @@
2.247
2.248 lemma prime_imp_relprime:
2.249 "[| p \<in> prime; ~ (p dvd n); n \<in> nat |] ==> gcd (p, n) = 1"
2.250 -apply (unfold prime_def, clarify)
2.251 +apply (simp add: prime_def, clarify)
2.252 apply (drule_tac x = "gcd (p,n)" in bspec)
2.253 apply auto
2.254 apply (cut_tac m = p and n = n in gcd_dvd2, auto)
2.255 done
2.256
2.257 lemma prime_into_nat: "p \<in> prime ==> p \<in> nat"
2.258 -by (unfold prime_def, auto)
2.259 +by (simp add: prime_def)
2.260
2.261 lemma prime_nonzero: "p \<in> prime \<Longrightarrow> p\<noteq>0"
2.262 -by (unfold prime_def, auto)
2.263 +by (auto simp add: prime_def)
2.264
2.265
2.266 -(*This theorem leads immediately to a proof of the uniqueness of
2.267 - factorization. If p divides a product of primes then it is
2.268 - one of those primes.*)
2.269 +text{*This theorem leads immediately to a proof of the uniqueness of
2.270 + factorization. If @{term p} divides a product of primes then it is
2.271 + one of those primes.*}
2.272
2.273 lemma prime_dvd_mult:
2.274 "[|p dvd m #* n; p \<in> prime; m \<in> nat; n \<in> nat |] ==> p dvd m \<or> p dvd n"
2.275 by (blast intro: relprime_dvd_mult prime_imp_relprime prime_into_nat)
2.276
2.277
2.278 -(** Addition laws **)
2.279 -
2.280 -lemma gcd_add1 [simp]: "gcd (m #+ n, n) = gcd (m, n)"
2.281 -apply (subgoal_tac "gcd (m #+ natify (n), natify (n)) = gcd (m, natify (n))")
2.282 -apply simp
2.283 -apply (case_tac "natify (n) = 0")
2.284 -apply (auto simp add: Ord_0_lt_iff gcd_non_0)
2.285 -done
2.286 -
2.287 -lemma gcd_add2 [simp]: "gcd (m, m #+ n) = gcd (m, n)"
2.288 -apply (rule gcd_commute [THEN trans])
2.289 -apply (subst add_commute, simp)
2.290 -apply (rule gcd_commute)
2.291 -done
2.292 -
2.293 -lemma gcd_add2' [simp]: "gcd (m, n #+ m) = gcd (m, n)"
2.294 -by (subst add_commute, rule gcd_add2)
2.295 -
2.296 -lemma gcd_add_mult_raw: "k \<in> nat ==> gcd (m, k #* m #+ n) = gcd (m, n)"
2.297 -apply (erule nat_induct)
2.298 -apply (auto simp add: gcd_add2 add_assoc)
2.299 -done
2.300 -
2.301 -lemma gcd_add_mult: "gcd (m, k #* m #+ n) = gcd (m, n)"
2.302 -apply (cut_tac k = "natify (k)" in gcd_add_mult_raw)
2.303 -apply auto
2.304 -done
2.305 -
2.306 -
2.307 -(* More multiplication laws *)
2.308 -
2.309 lemma gcd_mult_cancel_raw:
2.310 "[|gcd (k,n) = 1; m \<in> nat; n \<in> nat|] ==> gcd (k #* m, n) = gcd (m, n)"
2.311 apply (rule dvd_anti_sym)
2.312 @@ -380,7 +371,7 @@
2.313 done
2.314
2.315
2.316 -(*** The square root of a prime is irrational: key lemma ***)
2.317 +subsection{*The Square Root of a Prime is Irrational: Key Lemma*}
2.318
2.319 lemma prime_dvd_other_side:
2.320 "\<lbrakk>n#*n = p#*(k#*k); p \<in> prime; n \<in> nat\<rbrakk> \<Longrightarrow> p dvd n"