legacy/oldfan/fan_concl.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Conclusions *)
   5 (* Chapter: Fan                                                               *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-05-14                                                           *)
   8 (* ========================================================================== *)
   9
  10 flyspeck_needs "fan/fan_defs.hl";;
  11
  12 module Fan_concl  = struct
  13
  14   open Fan_defs;
  15
  16   let fan_card = new_definition `fan_card (V,E) <=> FINITE V /\ ~(V SUBSET {})`;;
  17
  18   let fan_origin = new_definition `fan_origin (V,E) <=> ~(vec 0 IN V)`;;
  19
  20   let fan_nonparallel = new_definition `fan_nonparallel (V,E) <=> (!e. (e IN E) ==> ~(collinear ({vec 0} UNION e)))`;;
  21
  22   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})
  23 ==> ((aff_ge {vec 0} e1) INTER (aff_ge {vec 0} e2) = aff_ge {vec 0} (e1 INTER e2)))`;;
  24
  25   let fan = new_definition `fan (V,E) <=>  ((UNIONS E) SUBSET V) /\ graph(E) /\ fan_card(V,E) /\ fan_origin(V,E)/\
  26 fan_nonparallel(V,E)/\ fan_intersection(V,E)`;;
  27
  28
  29 (* move to fan_misc.hl *)
  30   let fan_of_FAN = prove(`!V E. FAN((vec 0), V,E) = fan(V,E)`,
  31         REWRITE_TAC[fan,fan_origin,fan_card,fan_nonparallel,fan_intersection,
  32              FAN, fan1,fan2,fan6,fan7] THEN MESON_TAC[]
  33         );;
  34
  35
  36
  37  let CTVTAQA_concl = `!V E E'. fan (V,E) /\ (E' SUBSET E)  ==> fan (V,E')`;;
  38
  39  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 *)
  40
  41  let AAUHTVE_concl = `!V E. fan(V,E) ==>
  42     (hypermap_of_fan (V,E))
  43     (!d. d IN dart1_of_fan ==> (e_fan_pair (V,E) (e_fan_pair (V,E) d) = d)) /\
  44     (!d. d IN dart1_of_fan ==> (e_fan_pair (V,E) (e_fa
  45
  46
  47  let PIIJBJK_concl= `!x V E . FAN (x,V,E) /\ fan81 (x,V,E) ==> conforming_fan (x,V,E)`;;
  48
  49
  50
  51
  52 end;;
  53