# HG changeset patch # User paulson # Date 1012825014 -3600 # Node ID 5c900a821a7c3b72d96110a3a22fa6bc024316f3 # Parent c00df77656561385fda2e131493215ceb479b89a New-style versions of these old examples diff -r c00df7765656 -r 5c900a821a7c src/ZF/ex/Commutation.thy --- a/src/ZF/ex/Commutation.thy Sat Feb 02 13:26:51 2002 +0100 +++ b/src/ZF/ex/Commutation.thy Mon Feb 04 13:16:54 2002 +0100 @@ -7,26 +7,142 @@ ported from Isabelle/HOL by Sidi Ould Ehmety *) -Commutation = Main + +theory Commutation = Main: constdefs - square :: [i, i, i, i] => o + square :: "[i, i, i, i] => o" "square(r,s,t,u) == - (\\a b. :r --> (\\c. :s - --> (\\x. :t & :u)))" + (\a b. \ r --> (\c. \ s --> (\x. \ t & \ u)))" - commute :: [i, i] => o + commute :: "[i, i] => o" "commute(r,s) == square(r,s,s,r)" - diamond :: i=>o - "diamond(r) == commute(r, r)" + diamond :: "i=>o" + "diamond(r) == commute(r, r)" + + strip :: "i=>o" + "strip(r) == commute(r^*, r)" + + Church_Rosser :: "i => o" + "Church_Rosser(r) == (\x y. \ (r Un converse(r))^* --> + (\z. \ r^* & \ r^*))" + confluent :: "i=>o" + "confluent(r) == diamond(r^*)" + + +lemma square_sym: "square(r,s,t,u) ==> square(s,r,u,t)" +by (unfold square_def, blast) + +lemma square_subset: "[| square(r,s,t,u); t \ t' |] ==> square(r,s,t',u)" +by (unfold square_def, blast) + + +lemma square_rtrancl [rule_format]: + "square(r,s,s,t) --> field(s)<=field(t) --> square(r^*,s,s,t^*)" +apply (unfold square_def) +apply clarify +apply (erule rtrancl_induct) +apply (blast intro: rtrancl_refl) +apply (blast intro: rtrancl_into_rtrancl) +done - strip :: i=>o - "strip(r) == commute(r^*, r)" +(* A special case of square_rtrancl_on *) +lemma diamond_strip: + "diamond(r) ==> strip(r)" +apply (unfold diamond_def commute_def strip_def) +apply (rule square_rtrancl) +apply simp_all +done + +(*** commute ***) + +lemma commute_sym: + "commute(r,s) ==> commute(s,r)" +by (unfold commute_def, blast intro: square_sym) + +lemma commute_rtrancl [rule_format]: + "commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)" +apply (unfold commute_def) +apply clarify +apply (rule square_rtrancl) +apply (rule square_sym [THEN square_rtrancl, THEN square_sym]) +apply (simp_all add: rtrancl_field) +done + + +lemma confluentD: "confluent(r) ==> diamond(r^*)" +by (simp add: confluent_def) + +lemma strip_confluent: "strip(r) ==> confluent(r)" +apply (unfold strip_def confluent_def diamond_def) +apply (drule commute_rtrancl) +apply (simp_all add: rtrancl_field) +done + +lemma commute_Un: "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)" +by (unfold commute_def square_def, blast) - Church_Rosser :: i => o - "Church_Rosser(r) == (\\x y. : (r Un converse(r))^* --> - (\\z. :r^* & :r^*))" - confluent :: i=>o - "confluent(r) == diamond(r^*)" +lemma diamond_Un: + "[| diamond(r); diamond(s); commute(r, s) |] ==> diamond(r Un s)" +by (unfold diamond_def, blast intro: commute_Un commute_sym) + +lemma diamond_confluent: + "diamond(r) ==> confluent(r)" +apply (unfold diamond_def confluent_def) +apply (erule commute_rtrancl) +apply simp +done + +lemma confluent_Un: + "[| confluent(r); confluent(s); commute(r^*, s^*); + r \ Sigma(A,B); s \ Sigma(C,D) |] ==> confluent(r Un s)" +apply (unfold confluent_def) +apply (rule rtrancl_Un_rtrancl [THEN subst]) +apply auto +apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD]) +done + + +lemma diamond_to_confluence: + "[| diamond(r); s \ r; r<= s^* |] ==> confluent(s)" +apply (drule rtrancl_subset [symmetric]) +apply assumption +apply (simp_all add: confluent_def) +apply (blast intro: diamond_confluent [THEN confluentD]) +done + + +(*** Church_Rosser ***) + +lemma Church_Rosser1: + "Church_Rosser(r) ==> confluent(r)" +apply (unfold confluent_def Church_Rosser_def square_def + commute_def diamond_def) +apply auto +apply (drule converseI) +apply (simp (no_asm_use) add: rtrancl_converse [symmetric]) +apply (drule_tac x = "b" in spec) +apply (drule_tac x1 = "c" in spec [THEN mp]) +apply (rule_tac b = "a" in rtrancl_trans) +apply (blast intro: rtrancl_mono [THEN subsetD])+ +done + + +lemma Church_Rosser2: + "confluent(r) ==> Church_Rosser(r)" +apply (unfold confluent_def Church_Rosser_def square_def + commute_def diamond_def) +apply auto +apply (frule fieldI1) +apply (simp add: rtrancl_field) +apply (erule rtrancl_induct) +apply auto +apply (blast intro: rtrancl_refl) +apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)+ +done + + +lemma Church_Rosser: "Church_Rosser(r) <-> confluent(r)" +by (blast intro: Church_Rosser1 Church_Rosser2) + end diff -r c00df7765656 -r 5c900a821a7c src/ZF/ex/LList.thy --- a/src/ZF/ex/LList.thy Sat Feb 02 13:26:51 2002 +0100 +++ b/src/ZF/ex/LList.thy Mon Feb 04 13:16:54 2002 +0100 @@ -14,43 +14,242 @@ a typing rule for it, based on some notion of "productivity..." *) -LList = Main + +theory LList = Main: consts - llist :: i=>i + llist :: "i=>i"; codatatype - "llist(A)" = LNil | LCons ("a \\ A", "l \\ llist(A)") + "llist(A)" = LNil | LCons ("a \ A", "l \ llist(A)") (*Coinductive definition of equality*) consts - lleq :: i=>i + lleq :: "i=>i" (*Previously used <*> in the domain and variant pairs as elements. But standard pairs work just as well. To use variant pairs, must change prefix a q/Q to the Sigma, Pair and converse rules.*) coinductive domains "lleq(A)" <= "llist(A) * llist(A)" - intrs - LNil " \\ lleq(A)" - LCons "[| a \\ A; : lleq(A) |] ==> : lleq(A)" - type_intrs "llist.intrs" + intros + LNil: " \ lleq(A)" + LCons: "[| a \ A; \ lleq(A) |] + ==> \ lleq(A)" + type_intros llist.intros (*Lazy list functions; flip is not definitional!*) consts - lconst :: i => i - flip :: i => i + lconst :: "i => i" + flip :: "i => i" defs - lconst_def "lconst(a) == lfp(univ(a), %l. LCons(a,l))" + lconst_def: "lconst(a) == lfp(univ(a), %l. LCons(a,l))" + +axioms + flip_LNil: "flip(LNil) = LNil" + + flip_LCons: "[| x \ bool; l \ llist(bool) |] + ==> flip(LCons(x,l)) = LCons(not(x), flip(l))" + + +(*These commands cause classical reasoning to regard the subset relation + as primitive, not reducing it to membership*) + +declare subsetI [rule del] + subsetCE [rule del] + +declare subset_refl [intro!] + cons_subsetI [intro!] + subset_consI [intro!] + Union_least [intro!] + UN_least [intro!] + Un_least [intro!] + Inter_greatest [intro!] + Int_greatest [intro!] + RepFun_subset [intro!] + Un_upper1 [intro!] + Un_upper2 [intro!] + Int_lower1 [intro!] + Int_lower2 [intro!] + +(*An elimination rule, for type-checking*) +inductive_cases LConsE: "LCons(a,l) \ llist(A)" + +(*Proving freeness results*) +lemma LCons_iff: "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'" +by auto + +lemma LNil_LCons_iff: "~ LNil=LCons(a,l)" +by auto + +(* +lemma llist_unfold: "llist(A) = {0} <+> (A <*> llist(A))"; +let open llist val rew = rewrite_rule con_defs in +by (fast_tac (claset() addSIs (subsetI ::map rew intros) addEs [rew elim]) 1) +end +done +*) + +(*** Lemmas to justify using "llist" in other recursive type definitions ***) + +lemma llist_mono: "A \ B ==> llist(A) \ llist(B)" +apply (unfold llist.defs ) +apply (rule gfp_mono) +apply (rule llist.bnd_mono) +apply (assumption | rule quniv_mono basic_monos)+ +done + +(** Closure of quniv(A) under llist -- why so complex? Its a gfp... **) + +declare QPair_Int_Vset_subset_UN [THEN subset_trans, intro!] + QPair_subset_univ [intro!] + empty_subsetI [intro!] + one_in_quniv [THEN qunivD, intro!] +declare qunivD [dest!] +declare Ord_in_Ord [elim!] + +lemma llist_quniv_lemma [rule_format]: + "Ord(i) ==> \l \ llist(quniv(A)). l Int Vset(i) \ univ(eclose(A))" +apply (erule trans_induct) +apply (rule ballI) +apply (erule llist.cases) +apply (simp_all add: QInl_def QInr_def llist.con_defs) +(*LCons case: I simply can't get rid of the deepen_tac*) +apply (tactic "deepen_tac (claset() addIs [Ord_trans] addIs [Int_lower1 RS subset_trans]) 2 1") +done + +lemma llist_quniv: "llist(quniv(A)) \ quniv(A)" +apply (rule qunivI [THEN subsetI]) +apply (rule Int_Vset_subset) +apply (assumption | rule llist_quniv_lemma)+ +done + +lemmas llist_subset_quniv = + subset_trans [OF llist_mono llist_quniv] + + +(*** Lazy List Equality: lleq ***) + +declare QPair_Int_Vset_subset_UN [THEN subset_trans, intro!] + QPair_mono [intro!] + +declare Ord_in_Ord [elim!] + +(*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*) +lemma lleq_Int_Vset_subset [rule_format]: + "Ord(i) ==> \l l'. \ lleq(A) --> l Int Vset(i) \ l'" +apply (erule trans_induct) +apply (intro allI impI) +apply (erule lleq.cases) +apply (unfold QInr_def llist.con_defs) +apply safe +apply (fast elim!: Ord_trans bspec [elim_format]) +done -rules - flip_LNil "flip(LNil) = LNil" +(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) +lemma lleq_symmetric: " \ lleq(A) ==> \ lleq(A)" +apply (erule lleq.coinduct [OF converseI]) +apply (rule lleq.dom_subset [THEN converse_type]) +apply safe +apply (erule lleq.cases) +apply blast+ +done + +lemma lleq_implies_equal: " \ lleq(A) ==> l=l'" +apply (rule equalityI) +apply (assumption | rule lleq_Int_Vset_subset [THEN Int_Vset_subset] | + erule lleq_symmetric)+ +done + +lemma equal_llist_implies_leq: + "[| l=l'; l \ llist(A) |] ==> \ lleq(A)" +apply (rule_tac X = "{. l \ llist (A) }" in lleq.coinduct) +apply blast +apply safe +apply (erule_tac a="l" in llist.cases) +apply fast+ +done + + +(*** Lazy List Functions ***) + +(*Examples of coinduction for type-checking and to prove llist equations*) + +(*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***) + +lemma lconst_fun_bnd_mono: "bnd_mono(univ(a), %l. LCons(a,l))" +apply (unfold llist.con_defs ) +apply (rule bnd_monoI) +apply (blast intro: A_subset_univ QInr_subset_univ) +apply (blast intro: subset_refl QInr_mono QPair_mono) +done + +(* lconst(a) = LCons(a,lconst(a)) *) +lemmas lconst = def_lfp_unfold [OF lconst_def lconst_fun_bnd_mono] +lemmas lconst_subset = lconst_def [THEN def_lfp_subset] +lemmas member_subset_Union_eclose = arg_into_eclose [THEN Union_upper] + +lemma lconst_in_quniv: "a \ A ==> lconst(a) \ quniv(A)" +apply (rule lconst_subset [THEN subset_trans, THEN qunivI]) +apply (erule arg_into_eclose [THEN eclose_subset, THEN univ_mono]) +done - flip_LCons "[| x \\ bool; l \\ llist(bool) |] ==> - flip(LCons(x,l)) = LCons(not(x), flip(l))" +lemma lconst_type: "a \ A ==> lconst(a): llist(A)" +apply (rule singletonI [THEN llist.coinduct]) +apply (erule lconst_in_quniv [THEN singleton_subsetI]) +apply (fast intro!: lconst) +done + +(*** flip --- equations merely assumed; certain consequences proved ***) + +declare flip_LNil [simp] + flip_LCons [simp] + not_type [simp] + +lemma bool_Int_subset_univ: "b \ bool ==> b Int X \ univ(eclose(A))" +by (fast intro: Int_lower1 [THEN subset_trans] elim!: boolE) + +declare not_type [intro!] +declare bool_Int_subset_univ [intro] + +(*Reasoning borrowed from lleq.ML; a similar proof works for all + "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*) +lemma flip_llist_quniv_lemma [rule_format]: + "Ord(i) ==> \l \ llist(bool). flip(l) Int Vset(i) \ univ(eclose(bool))" +apply (erule trans_induct) +apply (rule ballI) +apply (erule llist.cases) +apply (simp_all) +apply (simp_all add: QInl_def QInr_def llist.con_defs) +(*LCons case: I simply can't get rid of the deepen_tac*) +apply (tactic "deepen_tac (claset() addIs [Ord_trans] addIs [Int_lower1 RS subset_trans]) 2 1") +done + +lemma flip_in_quniv: "l \ llist(bool) ==> flip(l) \ quniv(bool)" +apply (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI]) +apply assumption+ +done + +lemma flip_type: "l \ llist(bool) ==> flip(l): llist(bool)" +apply (rule_tac X = "{flip (l) . l \ llist (bool) }" in llist.coinduct) +apply blast +apply (fast intro!: flip_in_quniv) +apply (erule RepFunE) +apply (erule_tac a="la" in llist.cases) +apply auto +done + +lemma flip_flip: "l \ llist(bool) ==> flip(flip(l)) = l" +apply (rule_tac X1 = "{ . l \ llist (bool) }" in + lleq.coinduct [THEN lleq_implies_equal]) +apply blast +apply (fast intro!: flip_type) +apply (erule RepFunE) +apply (erule_tac a="la" in llist.cases) +apply (simp_all add: flip_type not_not) +done end diff -r c00df7765656 -r 5c900a821a7c src/ZF/ex/NatSum.thy --- a/src/ZF/ex/NatSum.thy Sat Feb 02 13:26:51 2002 +0100 +++ b/src/ZF/ex/NatSum.thy Mon Feb 04 13:16:54 2002 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/ex/Natsum.thy +(* Title: ZF/ex/Natsum.thy ID: $Id$ Author: Tobias Nipkow & Lawrence C Paulson @@ -6,13 +6,65 @@ Note: n is a natural number but the sum is an integer, and f maps integers to integers + +Summing natural numbers, squares, cubes, etc. + +Originally demonstrated permutative rewriting, but add_ac is no longer needed + thanks to new simprocs. + +Thanks to Sloane's On-Line Encyclopedia of Integer Sequences, + http://www.research.att.com/~njas/sequences/ *) -NatSum = Main + -consts sum :: [i=>i, i] => i +theory NatSum = Main: + +consts sum :: "[i=>i, i] => i" primrec "sum (f,0) = #0" "sum (f, succ(n)) = f($#n) $+ sum(f,n)" -end \ No newline at end of file +declare zadd_zmult_distrib [simp] zadd_zmult_distrib2 [simp] +declare zdiff_zmult_distrib [simp] zdiff_zmult_distrib2 [simp] + +(*The sum of the first n odd numbers equals n squared.*) +lemma sum_of_odds: "n \ nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n" +by (induct_tac "n", auto) + +(*The sum of the first n odd squares*) +lemma sum_of_odd_squares: + "n \ nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) = + $#n $* (#4 $* $#n $* $#n $- #1)" +by (induct_tac "n", auto) + +(*The sum of the first n odd cubes*) +lemma sum_of_odd_cubes: + "n \ nat + ==> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) = + $#n $* $#n $* (#2 $* $#n $* $#n $- #1)" +by (induct_tac "n", auto) + +(*The sum of the first n positive integers equals n(n+1)/2.*) +lemma sum_of_naturals: + "n \ nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)" +by (induct_tac "n", auto) + +lemma sum_of_squares: + "n \ nat ==> #6 $* sum (%i. i$*i, succ(n)) = + $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)" +by (induct_tac "n", auto) + +lemma sum_of_cubes: + "n \ nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) = + $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)" +by (induct_tac "n", auto) + +(** Sum of fourth powers **) + +lemma sum_of_fourth_powers: + "n \ nat ==> #30 $* sum (%i. i$*i$*i$*i, succ(n)) = + $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $* + (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)" +by (induct_tac "n", auto) + +end diff -r c00df7765656 -r 5c900a821a7c src/ZF/ex/Primes.thy --- a/src/ZF/ex/Primes.thy Sat Feb 02 13:26:51 2002 +0100 +++ b/src/ZF/ex/Primes.thy Mon Feb 04 13:16:54 2002 +0100 @@ -6,28 +6,432 @@ The "divides" relation, the greatest common divisor and Euclid's algorithm *) -Primes = Main + -consts - dvd :: [i,i]=>o (infixl 50) - is_gcd :: [i,i,i]=>o (* great common divisor *) - gcd :: [i,i]=>i (* gcd by Euclid's algorithm *) - -defs - dvd_def "m dvd n == m \\ nat & n \\ nat & (\\k \\ nat. n = m#*k)" +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_def "is_gcd(p,m,n) == ((p dvd m) & (p dvd n)) & - (\\d\\nat. (d dvd m) & (d dvd n) --> d dvd p)" + is_gcd :: "[i,i,i]=>o" (* 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_def "gcd(m,n) == - transrec(natify(n), - %n f. \\m \\ nat. + gcd :: "[i,i]=>i" (* gcd by Euclid's algorithm *) + "gcd(m,n) == transrec(natify(n), + %n f. \m \ nat. if n=0 then m else f`(m mod n)`n) ` natify(m)" -constdefs - coprime :: [i,i]=>o (* coprime relation *) + coprime :: "[i,i]=>o" (* coprime relation *) "coprime(m,n) == gcd(m,n) = 1" prime :: i (* set of prime numbers *) - "prime == {p \\ nat. 1

m \\ nat. m dvd p --> m=1 | m=p)}" + "prime == {p \ nat. 1

m \ nat. m dvd p --> m=1 | m=p)}" + +(************************************************) +(** Divides Relation **) +(************************************************) + +lemma dvdD: "m dvd n ==> m \ nat & n \ nat & (\k \ nat. n = m#*k)" +apply (unfold divides_def) +apply assumption +done + +lemma dvdE: + "[|m dvd n; !!k. [|m \ nat; n \ nat; k \ nat; n = m#*k|] ==> P|] ==> P" +by (blast dest!: dvdD) + +lemmas dvd_imp_nat1 = dvdD [THEN conjunct1, standard] +lemmas dvd_imp_nat2 = dvdD [THEN conjunct2, THEN conjunct1, standard] + + +lemma dvd_0_right [simp]: "m \ nat ==> m dvd 0" +apply (unfold 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) + +lemma dvd_refl [simp]: "m \ nat ==> m dvd m" +apply (unfold 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 + +lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m=n" +apply (unfold 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) +apply blast +done + +lemma dvd_mult_right: "[|(i#*j) dvd k; j \ nat|] ==> j dvd k" +apply (unfold divides_def) +apply 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 *) + +lemma gcd_0 [simp]: "gcd(m,0) = natify(m)" +apply (unfold gcd_def) +apply (subst transrec) +apply simp +done + +lemma gcd_natify1 [simp]: "gcd(natify(m),n) = gcd(m,n)" +by (simp add: gcd_def) + +lemma gcd_natify2 [simp]: "gcd(m, natify(n)) = gcd(m,n)" +by (simp add: gcd_def) + +lemma gcd_non_0_raw: + "[| 0 nat |] ==> gcd(m,n) = gcd(n, m mod n)" +apply (unfold 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]) +done + +lemma gcd_non_0: "0 < natify(n) ==> gcd(m,n) = gcd(n, m mod n)" +apply (cut_tac m = "m" and n = "natify (n) " in gcd_non_0_raw) +apply auto +done + +lemma gcd_1 [simp]: "gcd(m,1) = 1" +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 (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 (fast intro: mult_left_commute mult_type) +done + +lemma dvd_mult2: "k dvd m ==> k dvd (m #* n)" +apply (subst mult_commute) +apply (blast intro: dvd_mult) +done + +(* k dvd (m*k) *) +lemmas dvdI1 [simp] = dvd_refl [THEN dvd_mult, standard] +lemmas dvdI2 [simp] = dvd_refl [THEN dvd_mult2, standard] + +lemma dvd_mod_imp_dvd_raw: + "[| a \ nat; b \ nat; k dvd b; k dvd (a mod b) |] ==> k dvd a" +apply (tactic "div_undefined_case_tac \"b=0\" 1") +apply (blast intro: mod_div_equality [THEN subst] + elim: dvdE + intro!: dvd_add dvd_mult mult_type mod_type div_type) +done + +lemma dvd_mod_imp_dvd: "[| k dvd (a mod b); k dvd b; a \ nat |] ==> k dvd a" +apply (cut_tac b = "natify (b) " in dvd_mod_imp_dvd_raw) +apply auto +apply (simp add: divides_def) +done + +(*Imitating TFL*) +lemma gcd_induct_lemma [rule_format (no_asm)]: "[| n \ nat; + \m \ nat. P(m,0); + \m \ nat. \n \ nat. 0 P(n, m mod n) --> P(m,n) |] + ==> \m \ nat. P (m,n)" +apply (erule_tac i = "n" in complete_induct) +apply (case_tac "x=0") +apply (simp (no_asm_simp)) +apply clarify +apply (drule_tac x1 = "m" and x = "x" in bspec [THEN bspec]) +apply (simp_all add: Ord_0_lt_iff) +apply (blast intro: mod_less_divisor [THEN ltD]) +done + +lemma gcd_induct: "!!P. [| m \ nat; n \ nat; + !!m. m \ nat ==> P(m,0); + !!m n. [|m \ nat; n \ nat; 0 P(m,n) |] + ==> P (m,n)" +by (blast intro: gcd_induct_lemma) + + + +(* gcd type *) + +lemma gcd_type [simp,TC]: "gcd(m, n) \ nat" +apply (subgoal_tac "gcd (natify (m) , natify (n)) \ nat") +apply simp +apply (rule_tac m = "natify (m) " and n = "natify (n) " in gcd_induct) +apply auto +apply (simp add: gcd_non_0) +done + + +(* 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" +apply (rule_tac m = "m" and n = "n" in gcd_induct) +apply (simp_all add: gcd_non_0) +apply (blast intro: dvd_mod_imp_dvd_raw nat_into_Ord [THEN Ord_0_lt]) +done + +lemma gcd_dvd1 [simp]: "m \ nat ==> gcd(m,n) dvd m" +apply (cut_tac m = "natify (m) " and n = "natify (n) " in gcd_dvd_both) +apply auto +done + +lemma gcd_dvd2 [simp]: "n \ nat ==> gcd(m,n) dvd n" +apply (cut_tac m = "natify (m) " and n = "natify (n) " in gcd_dvd_both) +apply auto +done + +(* 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 (tactic "div_undefined_case_tac \"b=0\" 1") +apply 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)*) + +lemma gcd_greatest_raw [rule_format]: + "[| m \ nat; n \ nat; f \ nat |] + ==> (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)" +apply (rule_tac m = "m" and n = "n" in gcd_induct) +apply (simp_all add: gcd_non_0 dvd_mod) +done + +lemma gcd_greatest: "[| f dvd m; f dvd n; f \ nat |] ==> f dvd gcd(m,n)" +apply (rule gcd_greatest_raw) +apply (auto simp add: divides_def) +done + +lemma gcd_greatest_iff [simp]: "[| k \ nat; m \ nat; n \ nat |] + ==> (k dvd gcd (m, n)) <-> (k dvd m & k dvd n)" +by (blast intro!: gcd_greatest gcd_dvd1 gcd_dvd2 intro: dvd_trans) + + +(* GCD PROOF: GCD exists and gcd fits the definition *) + +lemma is_gcd: "[| m \ nat; n \ nat |] ==> is_gcd(gcd(m,n), m, n)" +by (simp add: is_gcd_def) + +(* 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 (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) + +lemma gcd_commute_raw: "[| m \ nat; n \ nat |] ==> gcd(m,n) = gcd(n,m)" +apply (rule is_gcd_unique) +apply (rule is_gcd) +apply (rule_tac [3] is_gcd_commute [THEN iffD1]) +apply (rule_tac [3] is_gcd) +apply auto +done + +lemma gcd_commute: "gcd(m,n) = gcd(n,m)" +apply (cut_tac m = "natify (m) " and n = "natify (n) " in gcd_commute_raw) +apply auto +done + +lemma gcd_assoc_raw: "[| k \ nat; m \ nat; n \ nat |] + ==> gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" +apply (rule is_gcd_unique) +apply (rule is_gcd) +apply (simp_all add: is_gcd_def) +apply (blast intro: gcd_dvd1 gcd_dvd2 gcd_type intro: dvd_trans) +done + +lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" +apply (cut_tac k = "natify (k) " and m = "natify (m) " and n = "natify (n) " + in gcd_assoc_raw) +apply auto +done + +lemma gcd_0_left [simp]: "gcd (0, m) = natify(m)" +by (simp add: gcd_commute [of 0]) + +lemma gcd_1_left [simp]: "gcd (1, m) = 1" +by (simp add: gcd_commute [of 1]) + + +(* Multiplication laws *) + +lemma gcd_mult_distrib2_raw: + "[| k \ nat; m \ nat; n \ nat |] + ==> k #* gcd (m, n) = gcd (k #* m, k #* n)" +apply (erule_tac m = "m" and n = "n" in gcd_induct) +apply assumption +apply (simp) +apply (case_tac "k = 0") +apply simp +apply (simp add: mod_geq gcd_non_0 mod_mult_distrib2 Ord_0_lt_iff) +done + +lemma gcd_mult_distrib2: "k #* gcd (m, n) = gcd (k #* m, k #* n)" +apply (cut_tac k = "natify (k) " and m = "natify (m) " and n = "natify (n) " + in gcd_mult_distrib2_raw) +apply auto +done + +lemma gcd_mult [simp]: "gcd (k, k #* n) = natify(k)" +apply (cut_tac k = "k" and m = "1" and n = "n" in gcd_mult_distrib2) +apply auto +done + +lemma gcd_self [simp]: "gcd (k, k) = natify(k)" +apply (cut_tac k = "k" and n = "1" in gcd_mult) +apply auto +done + +lemma relprime_dvd_mult: + "[| gcd (k,n) = 1; k dvd (m #* n); m \ nat |] ==> k dvd m" +apply (cut_tac k = "m" and m = "k" and n = "n" in gcd_mult_distrib2) +apply auto +apply (erule_tac b = "m" in ssubst) +apply (simp add: dvd_imp_nat1) +done + +lemma relprime_dvd_mult_iff: + "[| gcd (k,n) = 1; m \ nat |] ==> k dvd (m #* n) <-> k dvd m" +by (blast intro: dvdI2 relprime_dvd_mult dvd_trans) + +lemma prime_imp_relprime: + "[| p \ prime; ~ (p dvd n); n \ nat |] ==> gcd (p, n) = 1" +apply (unfold prime_def) +apply clarify +apply (drule_tac x = "gcd (p,n) " in bspec) +apply auto +apply (cut_tac m = "p" and n = "n" in gcd_dvd2) +apply auto +done + +lemma prime_into_nat: "p \ prime ==> p \ nat" +by (unfold prime_def, auto) + +lemma prime_nonzero: "p \ prime \ p\0" +by (unfold prime_def, auto) + + +(*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.*) + +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) +apply 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) + apply (rule gcd_greatest) + apply (rule relprime_dvd_mult [of _ k]) +apply (simp add: gcd_assoc) +apply (simp add: gcd_commute) +apply (simp_all add: mult_commute) +apply (blast intro: dvdI1 gcd_dvd1 dvd_trans) +done + +lemma gcd_mult_cancel: "gcd (k,n) = 1 ==> gcd (k #* m, n) = gcd (m, n)" +apply (cut_tac m = "natify (m) " and n = "natify (n) " in gcd_mult_cancel_raw) +apply auto +done + + +(*** 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" +apply (subgoal_tac "p dvd n#*n") + apply (blast dest: prime_dvd_mult) +apply (rule_tac j = "k#*k" in dvd_mult_left) + apply (auto simp add: prime_def) +done + +lemma reduction: + "\k#*k = p#*(j#*j); p \ prime; 0 < k; j \ nat; k \ nat\ + \ k < p#*j & 0 < j" +apply (rule ccontr) +apply (simp add: not_lt_iff_le prime_into_nat) +apply (erule disjE) + apply (frule mult_le_mono, assumption+) +apply (simp add: mult_ac) +apply (auto dest!: natify_eqE + simp add: not_lt_iff_le prime_into_nat mult_le_cancel_le1) +apply (simp add: prime_def) +apply (blast dest: lt_trans1) +done + +lemma rearrange: "j #* (p#*j) = k#*k \ k#*k = p#*(j#*j)" +by (simp add: mult_ac) + +lemma prime_not_square: + "\m \ nat; p \ prime\ \ \k \ nat. 0 m#*m \ p#*(k#*k)" +apply (erule complete_induct) +apply clarify +apply (frule prime_dvd_other_side) +apply assumption +apply assumption +apply (erule dvdE) +apply (simp add: mult_assoc mult_cancel1 prime_nonzero prime_into_nat) +apply (blast dest: rearrange reduction ltD) +done end diff -r c00df7765656 -r 5c900a821a7c src/ZF/ex/Ramsey.thy --- a/src/ZF/ex/Ramsey.thy Sat Feb 02 13:26:51 2002 +0100 +++ b/src/ZF/ex/Ramsey.thy Mon Feb 04 13:16:54 2002 +0100 @@ -9,38 +9,191 @@ D Basin and M Kaufmann, The Boyer-Moore Prover and Nuprl: An Experimental Comparison. In G Huet and G Plotkin, editors, Logical Frameworks. - (CUP, 1991), pages 89--119 + (CUP, 1991), pages 89-119 See also M Kaufmann, An example in NQTHM: Ramsey's Theorem Internal Note, Computational Logic, Inc., Austin, Texas 78703 Available from the author: kaufmann@cli.com + +This function compute Ramsey numbers according to the proof given below +(which, does not constrain the base case values at all. + +fun ram 0 j = 1 + | ram i 0 = 1 + | ram i j = ram (i-1) j + ram i (j-1) + *) -Ramsey = Main + -consts - Symmetric :: i=>o - Atleast :: [i,i]=>o - Clique,Indept,Ramsey :: [i,i,i]=>o +theory Ramsey = Main: +constdefs + Symmetric :: "i=>o" + "Symmetric(E) == (\x y. :E --> :E)" + + Atleast :: "[i,i]=>o" (*not really necessary: ZF defines cardinality*) + "Atleast(n,S) == (\f. f \ inj(n,S))" + + Clique :: "[i,i,i]=>o" + "Clique(C,V,E) == (C \ V) & (\x \ C. \y \ C. x\y --> \ E)" + + Indept :: "[i,i,i]=>o" + "Indept(I,V,E) == (I \ V) & (\x \ I. \y \ I. x\y --> \ E)" + + Ramsey :: "[i,i,i]=>o" + "Ramsey(n,i,j) == \V E. Symmetric(E) & Atleast(n,V) --> + (\C. Clique(C,V,E) & Atleast(i,C)) | + (\I. Indept(I,V,E) & Atleast(j,I))" + +(*** Cliques and Independent sets ***) + +lemma Clique0 [intro]: "Clique(0,V,E)" +by (unfold Clique_def, blast) + +lemma Clique_superset: "[| Clique(C,V',E); V'<=V |] ==> Clique(C,V,E)" +by (unfold Clique_def, blast) + +lemma Indept0 [intro]: "Indept(0,V,E)" +by (unfold Indept_def, blast) -defs +lemma Indept_superset: "[| Indept(I,V',E); V'<=V |] ==> Indept(I,V,E)" +by (unfold Indept_def, blast) + +(*** Atleast ***) + +lemma Atleast0 [intro]: "Atleast(0,A)" +by (unfold Atleast_def inj_def Pi_def function_def, blast) + +lemma Atleast_succD: + "Atleast(succ(m),A) ==> \x \ A. Atleast(m, A-{x})" +apply (unfold Atleast_def) +apply (blast dest: inj_is_fun [THEN apply_type] inj_succ_restrict) +done - Symmetric_def - "Symmetric(E) == (\\x y. :E --> :E)" +lemma Atleast_superset: + "[| Atleast(n,A); A \ B |] ==> Atleast(n,B)" +by (unfold Atleast_def, blast intro: inj_weaken_type) + +lemma Atleast_succI: + "[| Atleast(m,B); b\ B |] ==> Atleast(succ(m), cons(b,B))" +apply (unfold Atleast_def succ_def) +apply (blast intro: inj_extend elim: mem_irrefl) +done + +lemma Atleast_Diff_succI: + "[| Atleast(m, B-{x}); x \ B |] ==> Atleast(succ(m), B)" +by (blast intro: Atleast_succI [THEN Atleast_superset]) + +(*** Main Cardinality Lemma ***) - Clique_def - "Clique(C,V,E) == (C \\ V) & (\\x \\ C. \\y \\ C. x\\y --> \\ E)" +(*The #-succ(0) strengthens the original theorem statement, but precisely + the same proof could be used!!*) +lemma pigeon2 [rule_format]: + "m \ nat ==> + \n \ nat. \A B. Atleast((m#+n) #- succ(0), A Un B) --> + Atleast(m,A) | Atleast(n,B)" +apply (induct_tac "m") +apply (blast intro!: Atleast0) +apply (simp) +apply (rule ballI) +apply (rename_tac m' n) (*simplifier does NOT preserve bound names!*) +apply (induct_tac "n") +apply auto +apply (erule Atleast_succD [THEN bexE]) +apply (rename_tac n' A B z) +apply (erule UnE) +(**case z \ B. Instantiate the '\A B' induction hypothesis. **) +apply (drule_tac [2] x1 = "A" and x = "B-{z}" in spec [THEN spec]) +apply (erule_tac [2] mp [THEN disjE]) +(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*) +apply (erule_tac [3] asm_rl notE Atleast_Diff_succI)+ +(*proving the condition*) +prefer 2 apply (blast intro: Atleast_superset) +(**case z \ A. Instantiate the '\n \ nat. \A B' induction hypothesis. **) +apply (drule_tac x2="succ(n')" and x1="A-{z}" and x="B" + in bspec [THEN spec, THEN spec]) +apply (erule nat_succI) +apply (erule mp [THEN disjE]) +(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*) +apply (erule_tac [2] asm_rl Atleast_Diff_succI notE)+; +(*proving the condition*) +apply simp +apply (blast intro: Atleast_superset) +done - Indept_def - "Indept(I,V,E) == (I \\ V) & (\\x \\ I. \\y \\ I. x\\y --> \\ E)" + +(**** Ramsey's Theorem ****) + +(** Base cases of induction; they now admit ANY Ramsey number **) + +lemma Ramsey0j: "Ramsey(n,0,j)" +by (unfold Ramsey_def, blast) + +lemma Ramseyi0: "Ramsey(n,i,0)" +by (unfold Ramsey_def, blast) + +(** Lemmas for induction step **) - Atleast_def - "Atleast(n,S) == (\\f. f \\ inj(n,S))" +(*The use of succ(m) here, rather than #-succ(0), simplifies the proof of + Ramsey_step_lemma.*) +lemma Atleast_partition: "[| Atleast(m #+ n, A); m \ nat; n \ nat |] + ==> Atleast(succ(m), {x \ A. ~P(x)}) | Atleast(n, {x \ A. P(x)})" +apply (rule nat_succI [THEN pigeon2]) +apply assumption+ +apply (rule Atleast_superset) +apply auto +done + +(*For the Atleast part, proves ~(a \ I) from the second premise!*) +lemma Indept_succ: + "[| Indept(I, {z \ V-{a}. \ E}, E); Symmetric(E); a \ V; + Atleast(j,I) |] ==> + Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))" +apply (unfold Symmetric_def Indept_def) +apply (blast intro!: Atleast_succI) +done + + +lemma Clique_succ: + "[| Clique(C, {z \ V-{a}. :E}, E); Symmetric(E); a \ V; + Atleast(j,C) |] ==> + Clique(cons(a,C), V, E) & Atleast(succ(j), cons(a,C))" +apply (unfold Symmetric_def Clique_def) +apply (blast intro!: Atleast_succI) +done + +(** Induction step **) - Ramsey_def - "Ramsey(n,i,j) == \\V E. Symmetric(E) & Atleast(n,V) --> - (\\C. Clique(C,V,E) & Atleast(i,C)) | - (\\I. Indept(I,V,E) & Atleast(j,I))" +(*Published proofs gloss over the need for Ramsey numbers to be POSITIVE.*) +lemma Ramsey_step_lemma: + "[| Ramsey(succ(m), succ(i), j); Ramsey(n, i, succ(j)); + m \ nat; n \ nat |] ==> Ramsey(succ(m#+n), succ(i), succ(j))" +apply (unfold Ramsey_def) +apply clarify +apply (erule Atleast_succD [THEN bexE]) +apply (erule_tac P1 = "%z.:E" in Atleast_partition [THEN disjE], + assumption+) +(*case m*) +apply (fast dest!: Indept_succ elim: Clique_superset) +(*case n*) +apply (fast dest!: Clique_succ elim: Indept_superset) +done + + +(** The actual proof **) + +(*Again, the induction requires Ramsey numbers to be positive.*) +lemma ramsey_lemma: "i \ nat ==> \j \ nat. \n \ nat. Ramsey(succ(n), i, j)" +apply (induct_tac "i") +apply (blast intro!: Ramsey0j) +apply (rule ballI) +apply (induct_tac "j") +apply (blast intro!: Ramseyi0) +apply (blast intro!: add_type Ramsey_step_lemma) +done + +(*Final statement in a tidy form, without succ(...) *) +lemma ramsey: "[| i \ nat; j \ nat |] ==> \n \ nat. Ramsey(n,i,j)" +by (blast dest: ramsey_lemma) end