--- 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) ==
- (\\<forall>a b. <a,b>:r --> (\\<forall>c. <a, c>:s
- --> (\\<exists>x. <b,x>:t & <c,x>:u)))"
+ (\<forall>a b. <a,b> \<in> r --> (\<forall>c. <a, c> \<in> s --> (\<exists>x. <b,x> \<in> t & <c,x> \<in> 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) == (\<forall>x y. <x,y> \<in> (r Un converse(r))^* -->
+ (\<exists>z. <x,z> \<in> r^* & <y,z> \<in> 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 \<subseteq> 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) == (\\<forall>x y. <x,y>: (r Un converse(r))^* -->
- (\\<exists>z. <x,z>:r^* & <y,z>: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 \<subseteq> Sigma(A,B); s \<subseteq> 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 \<subseteq> 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
--- 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 \\<in> A", "l \\<in> llist(A)")
+ "llist(A)" = LNil | LCons ("a \<in> A", "l \<in> 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 "<LNil, LNil> \\<in> lleq(A)"
- LCons "[| a \\<in> A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"
- type_intrs "llist.intrs"
+ intros
+ LNil: "<LNil, LNil> \<in> lleq(A)"
+ LCons: "[| a \<in> A; <l,l'> \<in> lleq(A) |]
+ ==> <LCons(a,l), LCons(a,l')> \<in> 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 \<in> bool; l \<in> 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) \<in> 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 \<subseteq> B ==> llist(A) \<subseteq> 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) ==> \<forall>l \<in> llist(quniv(A)). l Int Vset(i) \<subseteq> 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)) \<subseteq> 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) ==> \<forall>l l'. <l,l'> \<in> lleq(A) --> l Int Vset(i) \<subseteq> 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: "<l,l'> \<in> lleq(A) ==> <l',l> \<in> 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: "<l,l'> \<in> 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 \<in> llist(A) |] ==> <l,l'> \<in> lleq(A)"
+apply (rule_tac X = "{<l,l>. l \<in> 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 \<in> A ==> lconst(a) \<in> 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 \\<in> bool; l \\<in> llist(bool) |] ==>
- flip(LCons(x,l)) = LCons(not(x), flip(l))"
+lemma lconst_type: "a \<in> 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 \<in> bool ==> b Int X \<subseteq> 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) ==> \<forall>l \<in> llist(bool). flip(l) Int Vset(i) \<subseteq> 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 \<in> llist(bool) ==> flip(l) \<in> quniv(bool)"
+apply (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI])
+apply assumption+
+done
+
+lemma flip_type: "l \<in> llist(bool) ==> flip(l): llist(bool)"
+apply (rule_tac X = "{flip (l) . l \<in> 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 \<in> llist(bool) ==> flip(flip(l)) = l"
+apply (rule_tac X1 = "{<flip (flip (l)),l> . l \<in> 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
--- 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 \<in> 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 \<in> 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 \<in> 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 \<in> nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)"
+by (induct_tac "n", auto)
+
+lemma sum_of_squares:
+ "n \<in> nat ==> #6 $* sum (%i. i$*i, succ(n)) =
+ $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)"
+by (induct_tac "n", auto)
+
+lemma sum_of_cubes:
+ "n \<in> 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 \<in> 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
--- 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 \\<in> nat & n \\<in> nat & (\\<exists>k \\<in> nat. n = m#*k)"
+theory Primes = Main:
+constdefs
+ divides :: "[i,i]=>o" (infixl "dvd" 50)
+ "m dvd n == m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
- is_gcd_def "is_gcd(p,m,n) == ((p dvd m) & (p dvd n)) &
- (\\<forall>d\\<in>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)) &
+ (\<forall>d\<in>nat. (d dvd m) & (d dvd n) --> d dvd p)"
- gcd_def "gcd(m,n) ==
- transrec(natify(n),
- %n f. \\<lambda>m \\<in> nat.
+ gcd :: "[i,i]=>i" (* gcd by Euclid's algorithm *)
+ "gcd(m,n) == transrec(natify(n),
+ %n f. \<lambda>m \<in> 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 \\<in> nat. 1<p & (\\<forall>m \\<in> nat. m dvd p --> m=1 | m=p)}"
+ "prime == {p \<in> nat. 1<p & (\<forall>m \<in> nat. m dvd p --> m=1 | m=p)}"
+
+(************************************************)
+(** Divides Relation **)
+(************************************************)
+
+lemma dvdD: "m dvd n ==> m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
+apply (unfold divides_def)
+apply assumption
+done
+
+lemma dvdE:
+ "[|m dvd n; !!k. [|m \<in> nat; n \<in> nat; k \<in> 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 \<in> 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 \<in> 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 \<in> 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 \<in> 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<n; n \<in> 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 \<in> nat; b \<in> 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 \<in> 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 \<in> nat;
+ \<forall>m \<in> nat. P(m,0);
+ \<forall>m \<in> nat. \<forall>n \<in> nat. 0<n --> P(n, m mod n) --> P(m,n) |]
+ ==> \<forall>m \<in> 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 \<in> nat; n \<in> nat;
+ !!m. m \<in> nat ==> P(m,0);
+ !!m n. [|m \<in> nat; n \<in> nat; 0<n; P(n, m mod n)|] ==> P(m,n) |]
+ ==> P (m,n)"
+by (blast intro: gcd_induct_lemma)
+
+
+
+(* gcd type *)
+
+lemma gcd_type [simp,TC]: "gcd(m, n) \<in> nat"
+apply (subgoal_tac "gcd (natify (m) , natify (n)) \<in> 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 \<in> nat; n \<in> 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 \<in> 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 \<in> 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 \<in> nat; n \<in> nat; f \<in> 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 \<in> nat |] ==> f dvd gcd(m,n)"
+apply (rule gcd_greatest_raw)
+apply (auto simp add: divides_def)
+done
+
+lemma gcd_greatest_iff [simp]: "[| k \<in> nat; m \<in> nat; n \<in> 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 \<in> nat; n \<in> 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\<in>nat; n\<in>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 \<in> nat; n \<in> 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 \<in> nat; m \<in> nat; n \<in> 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 \<in> nat; m \<in> nat; n \<in> 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 \<in> 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 \<in> nat |] ==> k dvd (m #* n) <-> k dvd m"
+by (blast intro: dvdI2 relprime_dvd_mult dvd_trans)
+
+lemma prime_imp_relprime:
+ "[| p \<in> prime; ~ (p dvd n); n \<in> 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 \<in> prime ==> p \<in> nat"
+by (unfold prime_def, auto)
+
+lemma prime_nonzero: "p \<in> prime \<Longrightarrow> p\<noteq>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 \<in> prime; m \<in> nat; n \<in> nat |] ==> p dvd m \<or> 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 \<in> 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 \<in> nat; n \<in> 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:
+ "\<lbrakk>n#*n = p#*(k#*k); p \<in> prime; n \<in> nat\<rbrakk> \<Longrightarrow> 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:
+ "\<lbrakk>k#*k = p#*(j#*j); p \<in> prime; 0 < k; j \<in> nat; k \<in> nat\<rbrakk>
+ \<Longrightarrow> 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 \<Longrightarrow> k#*k = p#*(j#*j)"
+by (simp add: mult_ac)
+
+lemma prime_not_square:
+ "\<lbrakk>m \<in> nat; p \<in> prime\<rbrakk> \<Longrightarrow> \<forall>k \<in> nat. 0<k \<longrightarrow> m#*m \<noteq> 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
--- 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) == (\<forall>x y. <x,y>:E --> <y,x>:E)"
+
+ Atleast :: "[i,i]=>o" (*not really necessary: ZF defines cardinality*)
+ "Atleast(n,S) == (\<exists>f. f \<in> inj(n,S))"
+
+ Clique :: "[i,i,i]=>o"
+ "Clique(C,V,E) == (C \<subseteq> V) & (\<forall>x \<in> C. \<forall>y \<in> C. x\<noteq>y --> <x,y> \<in> E)"
+
+ Indept :: "[i,i,i]=>o"
+ "Indept(I,V,E) == (I \<subseteq> V) & (\<forall>x \<in> I. \<forall>y \<in> I. x\<noteq>y --> <x,y> \<notin> E)"
+
+ Ramsey :: "[i,i,i]=>o"
+ "Ramsey(n,i,j) == \<forall>V E. Symmetric(E) & Atleast(n,V) -->
+ (\<exists>C. Clique(C,V,E) & Atleast(i,C)) |
+ (\<exists>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) ==> \<exists>x \<in> 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) == (\\<forall>x y. <x,y>:E --> <y,x>:E)"
+lemma Atleast_superset:
+ "[| Atleast(n,A); A \<subseteq> B |] ==> Atleast(n,B)"
+by (unfold Atleast_def, blast intro: inj_weaken_type)
+
+lemma Atleast_succI:
+ "[| Atleast(m,B); b\<notin> 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 \<in> B |] ==> Atleast(succ(m), B)"
+by (blast intro: Atleast_succI [THEN Atleast_superset])
+
+(*** Main Cardinality Lemma ***)
- Clique_def
- "Clique(C,V,E) == (C \\<subseteq> V) & (\\<forall>x \\<in> C. \\<forall>y \\<in> C. x\\<noteq>y --> <x,y> \\<in> E)"
+(*The #-succ(0) strengthens the original theorem statement, but precisely
+ the same proof could be used!!*)
+lemma pigeon2 [rule_format]:
+ "m \<in> nat ==>
+ \<forall>n \<in> nat. \<forall>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 \<in> B. Instantiate the '\<forall>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 \<in> A. Instantiate the '\<forall>n \<in> nat. \<forall>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 \\<subseteq> V) & (\\<forall>x \\<in> I. \\<forall>y \\<in> I. x\\<noteq>y --> <x,y> \\<notin> 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) == (\\<exists>f. f \\<in> 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 \<in> nat; n \<in> nat |]
+ ==> Atleast(succ(m), {x \<in> A. ~P(x)}) | Atleast(n, {x \<in> A. P(x)})"
+apply (rule nat_succI [THEN pigeon2])
+apply assumption+
+apply (rule Atleast_superset)
+apply auto
+done
+
+(*For the Atleast part, proves ~(a \<in> I) from the second premise!*)
+lemma Indept_succ:
+ "[| Indept(I, {z \<in> V-{a}. <a,z> \<notin> E}, E); Symmetric(E); a \<in> 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 \<in> V-{a}. <a,z>:E}, E); Symmetric(E); a \<in> 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) == \\<forall>V E. Symmetric(E) & Atleast(n,V) -->
- (\\<exists>C. Clique(C,V,E) & Atleast(i,C)) |
- (\\<exists>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 \<in> nat; n \<in> 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.<x,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 \<in> nat ==> \<forall>j \<in> nat. \<exists>n \<in> 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 \<in> nat; j \<in> nat |] ==> \<exists>n \<in> nat. Ramsey(n,i,j)"
+by (blast dest: ramsey_lemma)
end