# HG changeset patch # User paulson # Date 1114612863 -7200 # Node ID 78db9506cc788a9a6e0b841336c32b68260339ca # Parent 67574c1b15a09154a54fff353e523f6926516881 minor tidying diff -r 67574c1b15a0 -r 78db9506cc78 src/ZF/Induct/Comb.thy --- a/src/ZF/Induct/Comb.thy Wed Apr 27 16:40:27 2005 +0200 +++ b/src/ZF/Induct/Comb.thy Wed Apr 27 16:41:03 2005 +0200 @@ -39,7 +39,7 @@ "p ---> q" == " \ contract^*" syntax (xsymbols) - "app" :: "[i, i] => i" (infixl "\" 90) + "comb.app" :: "[i, i] => i" (infixl "\" 90) inductive domains "contract" \ "comb \ comb" @@ -158,8 +158,6 @@ and S_contractE [elim!]: "S -1-> r" and Ap_contractE [elim!]: "p\q -1-> r" -declare contract.Ap1 [intro] contract.Ap2 [intro] - lemma I_contract_E: "I -1-> r ==> P" by (auto simp add: I_def) diff -r 67574c1b15a0 -r 78db9506cc78 src/ZF/ex/Primes.thy --- a/src/ZF/ex/Primes.thy Wed Apr 27 16:40:27 2005 +0200 +++ b/src/ZF/ex/Primes.thy Wed Apr 27 16:41:03 2005 +0200 @@ -2,33 +2,32 @@ ID: $Id$ Author: Christophe Tabacznyj and Lawrence C Paulson Copyright 1996 University of Cambridge +*) -The "divides" relation, the greatest common divisor and Euclid's algorithm -*) +header{*The Divides Relation and Euclid's algorithm for the GCD*} theory Primes = Main: constdefs divides :: "[i,i]=>o" (infixl "dvd" 50) "m dvd n == m \ nat & n \ nat & (\k \ nat. n = m#*k)" - is_gcd :: "[i,i,i]=>o" (* great common divisor *) + is_gcd :: "[i,i,i]=>o" --{*definition of great common divisor*} "is_gcd(p,m,n) == ((p dvd m) & (p dvd n)) & (\d\nat. (d dvd m) & (d dvd n) --> d dvd p)" - gcd :: "[i,i]=>i" (* gcd by Euclid's algorithm *) + gcd :: "[i,i]=>i" --{*Euclid's algorithm for the gcd*} "gcd(m,n) == transrec(natify(n), %n f. \m \ nat. if n=0 then m else f`(m mod n)`n) ` natify(m)" - coprime :: "[i,i]=>o" (* coprime relation *) + coprime :: "[i,i]=>o" --{*the coprime relation*} "coprime(m,n) == gcd(m,n) = 1" - prime :: i (* set of prime numbers *) + prime :: i --{*the set of prime numbers*} "prime == {p \ nat. 1

m \ nat. m dvd p --> m=1 | m=p)}" -(************************************************) -(** Divides Relation **) -(************************************************) + +subsection{*The Divides Relation*} lemma dvdD: "m dvd n ==> m \ nat & n \ nat & (\k \ nat. n = m#*k)" by (unfold divides_def, assumption) @@ -42,50 +41,42 @@ lemma dvd_0_right [simp]: "m \ nat ==> m dvd 0" -apply (unfold divides_def) +apply (simp add: divides_def) apply (fast intro: nat_0I mult_0_right [symmetric]) done lemma dvd_0_left: "0 dvd m ==> m = 0" -by (unfold divides_def, force) +by (simp add: divides_def) lemma dvd_refl [simp]: "m \ nat ==> m dvd m" -apply (unfold divides_def) +apply (simp add: divides_def) apply (fast intro: nat_1I mult_1_right [symmetric]) done lemma dvd_trans: "[| m dvd n; n dvd p |] ==> m dvd p" -apply (unfold divides_def) -apply (fast intro: mult_assoc mult_type) -done +by (auto simp add: divides_def intro: mult_assoc mult_type) lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m=n" -apply (unfold divides_def) +apply (simp add: divides_def) apply (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff) done lemma dvd_mult_left: "[|(i#*j) dvd k; i \ nat|] ==> i dvd k" -apply (unfold divides_def) -apply (simp add: mult_assoc, blast) -done +by (auto simp add: divides_def mult_assoc) lemma dvd_mult_right: "[|(i#*j) dvd k; j \ nat|] ==> j dvd k" -apply (unfold divides_def, clarify) +apply (simp add: divides_def, clarify) apply (rule_tac x = "i#*k" in bexI) apply (simp add: mult_ac) apply (rule mult_type) done -(************************************************) -(** Greatest Common Divisor **) -(************************************************) - -(* GCD by Euclid's Algorithm *) +subsection{*Euclid's Algorithm for the GCD*} lemma gcd_0 [simp]: "gcd(m,0) = natify(m)" -apply (unfold gcd_def) +apply (simp add: gcd_def) apply (subst transrec, simp) done @@ -97,7 +88,7 @@ lemma gcd_non_0_raw: "[| 0 nat |] ==> gcd(m,n) = gcd(n, m mod n)" -apply (unfold gcd_def) +apply (simp add: gcd_def) apply (rule_tac P = "%z. ?left (z) = ?right" in transrec [THEN ssubst]) apply (simp add: ltD [THEN mem_imp_not_eq, THEN not_sym] mod_less_divisor [THEN ltD]) @@ -112,12 +103,12 @@ by (simp (no_asm_simp) add: gcd_non_0) lemma dvd_add: "[| k dvd a; k dvd b |] ==> k dvd (a #+ b)" -apply (unfold divides_def) +apply (simp add: divides_def) apply (fast intro: add_mult_distrib_left [symmetric] add_type) done lemma dvd_mult: "k dvd n ==> k dvd (m #* n)" -apply (unfold divides_def) +apply (simp add: divides_def) apply (fast intro: mult_left_commute mult_type) done @@ -132,7 +123,7 @@ lemma dvd_mod_imp_dvd_raw: "[| a \ nat; b \ nat; k dvd b; k dvd (a mod b) |] ==> k dvd a" -apply (case_tac "b=0") +apply (case_tac "b=0") apply (simp add: DIVISION_BY_ZERO_MOD) apply (blast intro: mod_div_equality [THEN subst] elim: dvdE @@ -166,9 +157,9 @@ by (blast intro: gcd_induct_lemma) +subsection{*Basic Properties of @{term gcd}*} -(* gcd type *) - +text{*type of gcd*} lemma gcd_type [simp,TC]: "gcd(m, n) \ nat" apply (subgoal_tac "gcd (natify (m), natify (n)) \ nat") apply simp @@ -178,7 +169,7 @@ done -(* Property 1: gcd(a,b) divides a and b *) +text{* Property 1: gcd(a,b) divides a and b *} lemma gcd_dvd_both: "[| m \ nat; n \ nat |] ==> gcd (m, n) dvd m & gcd (m, n) dvd n" @@ -197,17 +188,17 @@ apply auto done -(* if f divides a and b then f divides gcd(a,b) *) +text{* if f divides a and b then f divides gcd(a,b) *} lemma dvd_mod: "[| f dvd a; f dvd b |] ==> f dvd (a mod b)" -apply (unfold divides_def) +apply (simp add: divides_def) apply (case_tac "b=0") apply (simp add: DIVISION_BY_ZERO_MOD, auto) apply (blast intro: mod_mult_distrib2 [symmetric]) done -(* Property 2: for all a,b,f naturals, - if f divides a and f divides b then f divides gcd(a,b)*) +text{* Property 2: for all a,b,f naturals, + if f divides a and f divides b then f divides gcd(a,b)*} lemma gcd_greatest_raw [rule_format]: "[| m \ nat; n \ nat; f \ nat |] @@ -226,20 +217,22 @@ by (blast intro!: gcd_greatest gcd_dvd1 gcd_dvd2 intro: dvd_trans) -(* GCD PROOF: GCD exists and gcd fits the definition *) +subsection{*The Greatest Common Divisor*} + +text{*The GCD exists and function gcd computes it.*} lemma is_gcd: "[| m \ nat; n \ nat |] ==> is_gcd(gcd(m,n), m, n)" by (simp add: is_gcd_def) -(* GCD is unique *) +text{*The GCD is unique*} lemma is_gcd_unique: "[|is_gcd(m,a,b); is_gcd(n,a,b); m\nat; n\nat|] ==> m=n" -apply (unfold is_gcd_def) +apply (simp add: is_gcd_def) apply (blast intro: dvd_anti_sym) done lemma is_gcd_commute: "is_gcd(k,m,n) <-> is_gcd(k,n,m)" -by (unfold is_gcd_def, blast) +by (simp add: is_gcd_def, blast) lemma gcd_commute_raw: "[| m \ nat; n \ nat |] ==> gcd(m,n) = gcd(n,m)" apply (rule is_gcd_unique) @@ -274,7 +267,36 @@ by (simp add: gcd_commute [of 1]) -(* Multiplication laws *) +subsection{*Addition laws*} + +lemma gcd_add1 [simp]: "gcd (m #+ n, n) = gcd (m, n)" +apply (subgoal_tac "gcd (m #+ natify (n), natify (n)) = gcd (m, natify (n))") +apply simp +apply (case_tac "natify (n) = 0") +apply (auto simp add: Ord_0_lt_iff gcd_non_0) +done + +lemma gcd_add2 [simp]: "gcd (m, m #+ n) = gcd (m, n)" +apply (rule gcd_commute [THEN trans]) +apply (subst add_commute, simp) +apply (rule gcd_commute) +done + +lemma gcd_add2' [simp]: "gcd (m, n #+ m) = gcd (m, n)" +by (subst add_commute, rule gcd_add2) + +lemma gcd_add_mult_raw: "k \ nat ==> gcd (m, k #* m #+ n) = gcd (m, n)" +apply (erule nat_induct) +apply (auto simp add: gcd_add2 add_assoc) +done + +lemma gcd_add_mult: "gcd (m, k #* m #+ n) = gcd (m, n)" +apply (cut_tac k = "natify (k)" in gcd_add_mult_raw) +apply auto +done + + +subsection{* Multiplication Laws*} lemma gcd_mult_distrib2_raw: "[| k \ nat; m \ nat; n \ nat |] @@ -310,59 +332,28 @@ lemma prime_imp_relprime: "[| p \ prime; ~ (p dvd n); n \ nat |] ==> gcd (p, n) = 1" -apply (unfold prime_def, clarify) +apply (simp add: prime_def, clarify) apply (drule_tac x = "gcd (p,n)" in bspec) apply auto apply (cut_tac m = p and n = n in gcd_dvd2, auto) done lemma prime_into_nat: "p \ prime ==> p \ nat" -by (unfold prime_def, auto) +by (simp add: prime_def) lemma prime_nonzero: "p \ prime \ p\0" -by (unfold prime_def, auto) +by (auto simp add: prime_def) -(*This theorem leads immediately to a proof of the uniqueness of - factorization. If p divides a product of primes then it is - one of those primes.*) +text{*This theorem leads immediately to a proof of the uniqueness of + factorization. If @{term p} divides a product of primes then it is + one of those primes.*} lemma prime_dvd_mult: "[|p dvd m #* n; p \ prime; m \ nat; n \ nat |] ==> p dvd m \ p dvd n" by (blast intro: relprime_dvd_mult prime_imp_relprime prime_into_nat) -(** Addition laws **) - -lemma gcd_add1 [simp]: "gcd (m #+ n, n) = gcd (m, n)" -apply (subgoal_tac "gcd (m #+ natify (n), natify (n)) = gcd (m, natify (n))") -apply simp -apply (case_tac "natify (n) = 0") -apply (auto simp add: Ord_0_lt_iff gcd_non_0) -done - -lemma gcd_add2 [simp]: "gcd (m, m #+ n) = gcd (m, n)" -apply (rule gcd_commute [THEN trans]) -apply (subst add_commute, simp) -apply (rule gcd_commute) -done - -lemma gcd_add2' [simp]: "gcd (m, n #+ m) = gcd (m, n)" -by (subst add_commute, rule gcd_add2) - -lemma gcd_add_mult_raw: "k \ nat ==> gcd (m, k #* m #+ n) = gcd (m, n)" -apply (erule nat_induct) -apply (auto simp add: gcd_add2 add_assoc) -done - -lemma gcd_add_mult: "gcd (m, k #* m #+ n) = gcd (m, n)" -apply (cut_tac k = "natify (k)" in gcd_add_mult_raw) -apply auto -done - - -(* More multiplication laws *) - lemma gcd_mult_cancel_raw: "[|gcd (k,n) = 1; m \ nat; n \ nat|] ==> gcd (k #* m, n) = gcd (m, n)" apply (rule dvd_anti_sym) @@ -380,7 +371,7 @@ done -(*** The square root of a prime is irrational: key lemma ***) +subsection{*The Square Root of a Prime is Irrational: Key Lemma*} lemma prime_dvd_other_side: "\n#*n = p#*(k#*k); p \ prime; n \ nat\ \ p dvd n"