(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Conclusions *) (* Chapter: Fan *) (* Author: Thomas C. Hales *) (* Date: 2010-05-14 *) (* ========================================================================== *) flyspeck_needs "fan/fan_defs.hl";; module Fan_concl = struct open Fan_defs; let fan_card = new_definition `fan_card (V,E) <=> FINITE V /\ ~(V SUBSET {})`;; let fan_origin = new_definition `fan_origin (V,E) <=> ~(vec 0 IN V)`;; let fan_nonparallel = new_definition `fan_nonparallel (V,E) <=> (!e. (e IN E) ==> ~(collinear ({vec 0} UNION e)))`;; let fan_intersection = new_definition `fan_intersection(V,E):bool<=> (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V}) ==> ((aff_ge {vec 0} e1) INTER (aff_ge {vec 0} e2) = aff_ge {vec 0} (e1 INTER e2)))`;; let fan = new_definition `fan (V,E) <=> ((UNIONS E) SUBSET V) /\ graph(E) /\ fan_card(V,E) /\ fan_origin(V,E)/\ fan_nonparallel(V,E)/\ fan_intersection(V,E)`;; (* move to fan_misc.hl *) let fan_of_FAN = prove(`!V E. FAN((vec 0), V,E) = fan(V,E)`, REWRITE_TAC[fan,fan_origin,fan_card,fan_nonparallel,fan_intersection, FAN, fan1,fan2,fan6,fan7] THEN MESON_TAC[] );; let CTVTAQA_concl = `!V E E'. fan (V,E) /\ (E' SUBSET E) ==> fan (V,E')`;; let XOLHLED_concl = `!V E v. fan (V,E) /\ (v IN V) ==> cyclic_set(set_of_edge v V E) (vec 0) v`;; (* introduction.hl:XOHLED *) let AAUHTVE_concl = `!V E. fan(V,E) ==> (hypermap_of_fan (V,E)) (!d. d IN dart1_of_fan ==> (e_fan_pair (V,E) (e_fan_pair (V,E) d) = d)) /\ (!d. d IN dart1_of_fan ==> (e_fan_pair (V,E) (e_fa let PIIJBJK_concl= `!x V E . FAN (x,V,E) /\ fan81 (x,V,E) ==> conforming_fan (x,V,E)`;; end;;