1 (* ========================================================================= *)
2 (* Impossibility of Eulerian path for bridges of Koenigsberg. *)
3 (* ========================================================================= *)
5 let edges = new_definition
6 `edges(E:E->bool,V:V->bool,Ter:E->V->bool) = E`;;
8 let vertices = new_definition
9 `vertices(E:E->bool,V:V->bool,Ter:E->V->bool) = V`;;
11 let termini = new_definition
12 `termini(E:E->bool,V:V->bool,Ter:E->V->bool) = Ter`;;
14 (* ------------------------------------------------------------------------- *)
15 (* Definition of an undirected graph. *)
16 (* ------------------------------------------------------------------------- *)
18 let graph = new_definition
21 ==> ?a b. a IN vertices(G) /\ b IN vertices(G) /\
22 termini G e = {a,b}`;;
24 let TERMINI_IN_VERTICES = prove
25 (`!G e v. graph G /\ e IN edges(G) /\ v IN termini G e ==> v IN vertices G`,
26 REWRITE_TAC[graph; EXTENSION; IN_INSERT; NOT_IN_EMPTY] THEN
29 (* ------------------------------------------------------------------------- *)
30 (* Connection in a graph. *)
31 (* ------------------------------------------------------------------------- *)
33 let connects = new_definition
34 `connects G e (a,b) <=> termini G e = {a,b}`;;
36 (* ------------------------------------------------------------------------- *)
37 (* Delete an edge in a graph. *)
38 (* ------------------------------------------------------------------------- *)
40 let delete_edge = new_definition
41 `delete_edge e (E,V,Ter) = (E DELETE e,V,Ter)`;;
43 let DELETE_EDGE_CLAUSES = prove
44 (`(!G. edges(delete_edge e G) = (edges G) DELETE e) /\
45 (!G. vertices(delete_edge e G) = vertices G) /\
46 (!G. termini(delete_edge e G) = termini G)`,
47 REWRITE_TAC[FORALL_PAIR_THM; delete_edge; edges; vertices; termini]);;
49 let GRAPH_DELETE_EDGE = prove
50 (`!G e. graph G ==> graph(delete_edge e G)`,
51 REWRITE_TAC[graph; DELETE_EDGE_CLAUSES; IN_DELETE] THEN MESON_TAC[]);;
53 (* ------------------------------------------------------------------------- *)
54 (* Local finiteness: set of edges with given endpoint is finite. *)
55 (* ------------------------------------------------------------------------- *)
57 let locally_finite = new_definition
59 !v. v IN vertices(G) ==> FINITE {e | e IN edges G /\ v IN termini G e}`;;
61 (* ------------------------------------------------------------------------- *)
62 (* Degree of a vertex. *)
63 (* ------------------------------------------------------------------------- *)
65 let localdegree = new_definition
67 if termini G e = {v} then 2
68 else if v IN termini G e then 1
71 let degree = new_definition
72 `degree G v = nsum {e | e IN edges G /\ v IN termini G e} (localdegree G v)`;;
74 let DEGREE_DELETE_EDGE = prove
76 graph G /\ locally_finite G /\ e IN edges(G)
78 if termini G e = {v} then degree (delete_edge e G) v + 2
79 else if v IN termini G e then degree (delete_edge e G) v + 1
80 else degree (delete_edge e G) v`,
82 REWRITE_TAC[degree; DELETE_EDGE_CLAUSES; IN_DELETE] THEN
84 `{e:E | e IN edges G /\ (v:V) IN termini G e} =
86 then e INSERT {e' | (e' IN edges G /\ ~(e' = e)) /\ v IN termini G e'}
87 else {e' | (e' IN edges G /\ ~(e' = e)) /\ v IN termini G e'}`
89 [REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN COND_CASES_TAC THEN
90 ASM_REWRITE_TAC[IN_ELIM_THM; IN_INSERT] THEN
93 ASM_CASES_TAC `(v:V) IN termini G (e:E)` THEN ASM_REWRITE_TAC[] THENL
95 COND_CASES_TAC THENL [ASM_MESON_TAC[IN_SING; EXTENSION]; ALL_TAC] THEN
96 MATCH_MP_TAC NSUM_EQ THEN REWRITE_TAC[IN_ELIM_THM; localdegree] THEN
97 REWRITE_TAC[DELETE_EDGE_CLAUSES]] THEN
99 `FINITE {e':E | (e' IN edges G /\ ~(e' = e)) /\ (v:V) IN termini G e'}`
100 (fun th -> SIMP_TAC[NSUM_CLAUSES; th])
102 [MATCH_MP_TAC FINITE_SUBSET THEN
103 EXISTS_TAC `{e:E | e IN edges G /\ (v:V) IN termini G e}` THEN
104 SIMP_TAC[IN_ELIM_THM; SUBSET] THEN
105 ASM_MESON_TAC[locally_finite; TERMINI_IN_VERTICES];
107 REWRITE_TAC[IN_ELIM_THM] THEN ASM_REWRITE_TAC[localdegree] THEN
109 `nsum {e':E | (e' IN edges G /\ ~(e' = e)) /\ (v:V) IN termini G e'}
110 (localdegree (delete_edge e G) v) =
111 nsum {e' | (e' IN edges G /\ ~(e' = e)) /\ v IN termini G e'}
114 [ALL_TAC; COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ARITH_TAC] THEN
115 MATCH_MP_TAC NSUM_EQ THEN SIMP_TAC[localdegree; DELETE_EDGE_CLAUSES]);;
117 (* ------------------------------------------------------------------------- *)
118 (* Definition of Eulerian path. *)
119 (* ------------------------------------------------------------------------- *)
121 let eulerian_RULES,eulerian_INDUCT,eulerian_CASES = new_inductive_definition
122 `(!G a. a IN vertices G /\ edges G = {} ==> eulerian G [] (a,a)) /\
123 (!G a b c e es. e IN edges(G) /\ connects G e (a,b) /\
124 eulerian (delete_edge e G) es (b,c)
125 ==> eulerian G (CONS e es) (a,c))`;;
127 let EULERIAN_FINITE = prove
128 (`!G es ab. eulerian G es ab ==> FINITE (edges G)`,
129 MATCH_MP_TAC eulerian_INDUCT THEN
130 SIMP_TAC[DELETE_EDGE_CLAUSES; FINITE_DELETE; FINITE_RULES]);;
132 (* ------------------------------------------------------------------------- *)
133 (* The main result. *)
134 (* ------------------------------------------------------------------------- *)
136 let EULERIAN_ODD_LEMMA = prove
137 (`!G:(E->bool)#(V->bool)#(E->V->bool) es ab.
140 ==> FINITE(edges G) /\
142 ==> (ODD(degree G v) <=>
143 ~(FST ab = SND ab) /\ (v = FST ab \/ v = SND ab))`,
144 MATCH_MP_TAC eulerian_INDUCT THEN CONJ_TAC THENL
145 [SIMP_TAC[degree; NOT_IN_EMPTY; SET_RULE `{x | F} = {}`] THEN
146 SIMP_TAC[NSUM_CLAUSES; FINITE_RULES; ARITH];
148 SIMP_TAC[GRAPH_DELETE_EDGE; FINITE_DELETE; DELETE_EDGE_CLAUSES] THEN
150 DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
151 ASM_SIMP_TAC[GRAPH_DELETE_EDGE] THEN STRIP_TAC THEN
152 X_GEN_TAC `v:V` THEN DISCH_TAC THEN
153 MP_TAC(ISPECL [`G:(E->bool)#(V->bool)#(E->V->bool)`; `e:E`; `v:V`]
154 DEGREE_DELETE_EDGE) THEN
156 [ASM_REWRITE_TAC[locally_finite] THEN GEN_TAC THEN DISCH_TAC THEN
157 MATCH_MP_TAC FINITE_SUBSET THEN
158 EXISTS_TAC `edges(G:(E->bool)#(V->bool)#(E->V->bool))` THEN
159 ASM_SIMP_TAC[SUBSET; IN_ELIM_THM];
161 DISCH_THEN SUBST1_TAC THEN
162 MP_TAC(ISPECL [`G:(E->bool)#(V->bool)#(E->V->bool)`; `e:E`]
163 TERMINI_IN_VERTICES) THEN
164 ASM_REWRITE_TAC[] THEN
165 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [connects]) THEN
166 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
167 ASM_CASES_TAC `b:V = a` THEN ASM_REWRITE_TAC[] THENL
168 [REWRITE_TAC[SET_RULE `{a,a} = {v} <=> v = a`] THEN
169 COND_CASES_TAC THEN ASM_SIMP_TAC[ODD_ADD; ARITH];
171 ASM_REWRITE_TAC[SET_RULE `{a,b} = {v} <=> a = b /\ a = v`] THEN
172 COND_CASES_TAC THEN ASM_SIMP_TAC[ODD_ADD; ARITH] THEN ASM_MESON_TAC[]);;
174 let EULERIAN_ODD = prove
176 graph G /\ eulerian G es (a,b)
177 ==> !v. v IN vertices G
178 ==> (ODD(degree G v) <=> ~(a = b) /\ (v = a \/ v = b))`,
179 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
180 DISCH_THEN(MP_TAC o MATCH_MP EULERIAN_ODD_LEMMA) THEN
181 ASM_SIMP_TAC[FST; SND]);;
183 (* ------------------------------------------------------------------------- *)
184 (* Now the actual Koenigsberg configuration. *)
185 (* ------------------------------------------------------------------------- *)
187 let KOENIGSBERG = prove
188 (`!G. vertices(G) = {0,1,2,3} /\
189 edges(G) = {10,20,30,40,50,60,70} /\
190 termini G (10) = {0,1} /\
191 termini G (20) = {0,2} /\
192 termini G (30) = {0,3} /\
193 termini G (40) = {1,2} /\
194 termini G (50) = {1,2} /\
195 termini G (60) = {2,3} /\
196 termini G (70) = {2,3}
197 ==> ~(?es a b. eulerian G es (a,b))`,
198 GEN_TAC THEN STRIP_TAC THEN
199 MP_TAC(ISPEC `G:(num->bool)#(num->bool)#(num->num->bool)` EULERIAN_ODD) THEN
200 REWRITE_TAC[NOT_EXISTS_THM] THEN
201 REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
202 DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN ANTS_TAC THENL
203 [ASM_REWRITE_TAC[graph] THEN GEN_TAC THEN
204 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN STRIP_TAC THEN
205 ASM_REWRITE_TAC[SET_RULE
206 `{a,b} = {x,y} <=> a = x /\ b = y \/ a = y /\ b = x`] THEN
209 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
210 SIMP_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
211 ASM_REWRITE_TAC[degree; edges] THEN
212 SIMP_TAC[TAUT `a IN s /\ k IN t <=> ~(a IN s ==> ~(k IN t))`] THEN
213 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
214 SIMP_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
215 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH] THEN
216 REWRITE_TAC[DE_MORGAN_THM] THEN
217 REWRITE_TAC[SET_RULE `{x | x = a \/ P(x)} = a INSERT {x | P(x)}`] THEN
218 REWRITE_TAC[SET_RULE `{x | x = a} = {a}`] THEN
219 SIMP_TAC[NSUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN
220 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH] THEN
221 ASM_REWRITE_TAC[localdegree; IN_INSERT; NOT_IN_EMPTY; ARITH] THEN
222 REWRITE_TAC[SET_RULE `{a,b} = {x} <=> x = a /\ a = b`] THEN
224 MP_TAC(SPEC `0` th) THEN MP_TAC(SPEC `1` th) THEN
225 MP_TAC(SPEC `2` th) THEN MP_TAC(SPEC `3` th)) THEN
226 REWRITE_TAC[ARITH] THEN ARITH_TAC);;
230 Maybe for completeness I should show the contrary: existence of Eulerian
231 circuit/walk if we do have the right properties, assuming the graph is
234 http://math.arizona.edu/~lagatta/class/fa05/m105/graphtheorynotes.pdf