26 |
26 |
27 theory Ramsey imports Main begin |
27 theory Ramsey imports Main begin |
28 |
28 |
29 definition |
29 definition |
30 Symmetric :: "i=>o" where |
30 Symmetric :: "i=>o" where |
31 "Symmetric(E) == (\<forall>x y. <x,y>:E --> <y,x>:E)" |
31 "Symmetric(E) == (\<forall>x y. <x,y>:E \<longrightarrow> <y,x>:E)" |
32 |
32 |
33 definition |
33 definition |
34 Atleast :: "[i,i]=>o" where -- "not really necessary: ZF defines cardinality" |
34 Atleast :: "[i,i]=>o" where -- "not really necessary: ZF defines cardinality" |
35 "Atleast(n,S) == (\<exists>f. f \<in> inj(n,S))" |
35 "Atleast(n,S) == (\<exists>f. f \<in> inj(n,S))" |
36 |
36 |
37 definition |
37 definition |
38 Clique :: "[i,i,i]=>o" where |
38 Clique :: "[i,i,i]=>o" where |
39 "Clique(C,V,E) == (C \<subseteq> V) & (\<forall>x \<in> C. \<forall>y \<in> C. x\<noteq>y --> <x,y> \<in> E)" |
39 "Clique(C,V,E) == (C \<subseteq> V) & (\<forall>x \<in> C. \<forall>y \<in> C. x\<noteq>y \<longrightarrow> <x,y> \<in> E)" |
40 |
40 |
41 definition |
41 definition |
42 Indept :: "[i,i,i]=>o" where |
42 Indept :: "[i,i,i]=>o" where |
43 "Indept(I,V,E) == (I \<subseteq> V) & (\<forall>x \<in> I. \<forall>y \<in> I. x\<noteq>y --> <x,y> \<notin> E)" |
43 "Indept(I,V,E) == (I \<subseteq> V) & (\<forall>x \<in> I. \<forall>y \<in> I. x\<noteq>y \<longrightarrow> <x,y> \<notin> E)" |
44 |
44 |
45 definition |
45 definition |
46 Ramsey :: "[i,i,i]=>o" where |
46 Ramsey :: "[i,i,i]=>o" where |
47 "Ramsey(n,i,j) == \<forall>V E. Symmetric(E) & Atleast(n,V) --> |
47 "Ramsey(n,i,j) == \<forall>V E. Symmetric(E) & Atleast(n,V) \<longrightarrow> |
48 (\<exists>C. Clique(C,V,E) & Atleast(i,C)) | |
48 (\<exists>C. Clique(C,V,E) & Atleast(i,C)) | |
49 (\<exists>I. Indept(I,V,E) & Atleast(j,I))" |
49 (\<exists>I. Indept(I,V,E) & Atleast(j,I))" |
50 |
50 |
51 (*** Cliques and Independent sets ***) |
51 (*** Cliques and Independent sets ***) |
52 |
52 |
91 |
91 |
92 (*The #-succ(0) strengthens the original theorem statement, but precisely |
92 (*The #-succ(0) strengthens the original theorem statement, but precisely |
93 the same proof could be used!!*) |
93 the same proof could be used!!*) |
94 lemma pigeon2 [rule_format]: |
94 lemma pigeon2 [rule_format]: |
95 "m \<in> nat ==> |
95 "m \<in> nat ==> |
96 \<forall>n \<in> nat. \<forall>A B. Atleast((m#+n) #- succ(0), A Un B) --> |
96 \<forall>n \<in> nat. \<forall>A B. Atleast((m#+n) #- succ(0), A \<union> B) \<longrightarrow> |
97 Atleast(m,A) | Atleast(n,B)" |
97 Atleast(m,A) | Atleast(n,B)" |
98 apply (induct_tac "m") |
98 apply (induct_tac "m") |
99 apply (blast intro!: Atleast0, simp) |
99 apply (blast intro!: Atleast0, simp) |
100 apply (rule ballI) |
100 apply (rule ballI) |
101 apply (rename_tac m' n) (*simplifier does NOT preserve bound names!*) |
101 apply (rename_tac m' n) (*simplifier does NOT preserve bound names!*) |