legacy/oldfan/ch_fan/FAN_DEF.ml

   1
   2 (* definition of fan as ordered pairs *)
   3 (* This is the correct definition to use!! *)
   4
   5 let CASE_FAN_FINITE = new_definition `CASE_FAN_FINITE (V,E):bool  <=> FINITE V /\ ~(V SUBSET {})`;;
   6
   7 let CASE_FAN_ORIGIN = new_definition `CASE_FAN_ORIGIN (V,E) <=> ~((vec 0) IN (V:real^3 -> bool))`;;
   8
   9 let CASE_FAN_INDEPENDENCE =
  10   new_definition `CASE_FAN_INDEPENDENCE (V,E) <=>
  11   (!e.  e IN E ==> ~collinear ({vec 0} UNION e))`;;
  12
  13 let CASE_FAN_INTERSECTION =
  14   new_definition`CASE_FAN_INTERSECTION(V,E):bool<=>
  15   (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V})
  16   ==> ((aff_ge {vec 0 } e1) INTER (aff_ge {vec 0} e2) = aff_ge {vec 0} (e1 INTER e2)))`;;
  17
  18
  19 let FANO=new_definition`FANO(V,E) <=>
  20   ((UNIONS E) SUBSET V) /\ graph(E) /\ CASE_FAN_FINITE(V,E) /\ CASE_FAN_ORIGIN(V,E)/\
  21   CASE_FAN_INDEPENDENCE(V,E)/\ CASE_FAN_INTERSECTION(V,E)`;;
  22
  23 let FANO_OF_FAN = prove( `!V E. (FAN(vec 0 , V , E) <=> FANO(V,E))`,
  24   REWRITE_TAC[FAN;FANO;CASE_FAN_FINITE;CASE_FAN_ORIGIN;CASE_FAN_INDEPENDENCE;CASE_FAN_INTERSECTION;fan1;fan2;fan6;fan7]);;