legacy/oldlocal/ch_local/local_defs2.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Definitions File *)\r
   5 (* Chapter: Local Fan                                                      *)\r
   6 (* Author: Thomas C. Hales                                                    *)\r
   7 (* Date: 2010-02-25                                                           *)\r
   8 (* ========================================================================== *)\r
   9 \r
  10 \r
  11 \r
  12 \r
  13 module Local_defs  = struct\r
  14 \r
  15 (* the definition of hypermap *)\r
  16 \r
  17 let exist_hypermap = prove(`?H:((A->bool)#(A->A)#(A->A)#(A->A)). FINITE (FST H) /\ (FST(SND H)) permutes (FST H) /\ (FST(SND(SND H))) permutes (FST H) /\ (SND(SND(SND H))) permutes (FST H) /\ (FST(SND H)) o (FST(SND(SND  H))) o (SND(SND(SND H))) = I`,EXISTS_TAC\r
  18 `({},I,I,I):(A->bool)#(A->A)#(A->A)#(A->A)` THEN REWRITE_TAC[FINITE_RULES; PERMUTES_I; I_O_ID]);;\r
  19 \r
  20 let hypermap_tybij = (new_type_definition "hypermap" ("hypermap", "tuple_hypermap")exist_hypermap);;\r
  21 \r
  22 let dart = new_definition `dart (H:(A)hypermap) = FST (tuple_hypermap H)`;;\r
  23 \r
  24 let edge_map = new_definition `edge_map (H:(A)hypermap) = FST(SND(tuple_hypermap H))`;;\r
  25 \r
  26 let node_map = new_definition `node_map (H:(A)hypermap) = FST(SND(SND(tuple_hypermap H)))`;;\r
  27 \r
  28 let face_map = new_definition `face_map (H:(A)hypermap) = SND(SND(SND(tuple_hypermap H)))`;;\r
  29 \r
  30 (* edges, nodes and faces of a hypermap *)\r
  31 \r
  32 parse_as_infix("POWER",(24,"right"));;\r
  33 \r
  34 let POWER = new_recursive_definition num_RECURSION \r
  35   `(!(f:A->A). f POWER 0  = I) /\  \r
  36    (!(f:A->A) (n:num). f POWER (SUC n) = (f POWER n) o f)`;;\r
  37 \r
  38 let orbit_map = new_definition `orbit_map (f:A->A)  (x:A) = {(f POWER n) x | n >= 0}`;;\r
  39 \r
  40 let edge = new_definition `edge (H:(A)hypermap) (x:A) = orbit_map (edge_map H) x`;;\r
  41 \r
  42 let node = new_definition `node (H:(A)hypermap) (x:A) = orbit_map (node_map H) x`;;\r
  43 \r
  44 let face = new_definition `face (H:(A)hypermap) (x:A) = orbit_map (face_map H) x`;;\r
  45 \r
  46 (* some definitions on orbits *)\r
  47 \r
  48 let set_of_orbits = new_definition `set_of_orbits (D:A->bool) (f:A->A) = {orbit_map f x | x IN D}`;;\r
  49 \r
  50 let number_of_orbits = new_definition `number_of_orbits (D:A->bool) (f:A->A) = CARD(set_of_orbits D f)`;;\r
  51 \r
  52 \r
  53 (* the orbits on hypermaps*)\r
  54 \r
  55 let edge_set = new_definition `edge_set (H:(A)hypermap) = set_of_orbits (dart H) (edge_map H)`;;\r
  56 \r
  57 let node_set = new_definition `node_set  (H:(A)hypermap) = set_of_orbits (dart H) (node_map H)`;;\r
  58 \r
  59 let face_set = new_definition `face_set (H:(A)hypermap) = set_of_orbits (dart H) (face_map H)`;;\r
  60 \r
  61 \r
  62 (* some special kinds of hypergraphs *)\r
  63 \r
  64 let plain_hypermap = new_definition `plain_hypermap (H:(A)hypermap) <=> edge_map H o edge_map H = I`;;\r
  65 \r
  66 \r
  67 let simple_hypermap = new_definition `simple_hypermap (H:(A)hypermap) <=>\r
  68     (!x:A. x IN dart H ==> (node H x) INTER (face H x) = {x})`;;\r
  69 \r
  70 (* fan definitions *)\r
  71 \r
  72 let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;\r
  73 \r
  74 let fan1 = new_definition`fan1(x,V,E):bool <=>  FINITE V /\ ~(V SUBSET {}) `;;\r
  75 \r
  76 let fan2 = new_definition`fan2(x,V,E):bool <=>   ~(x IN V)`;;\r
  77 \r
  78 let fan6= new_definition`fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;\r
  79 \r
  80 let fan7= new_definition`fan7(x,V,E):bool<=> (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V})\r
  81 ==> ((aff_ge {x} e1) INTER (aff_ge {x} e2) = aff_ge {x} (e1 INTER e2)))`;;\r
  82 \r
  83 let FAN=new_definition`FAN(x,V,E) <=> ((UNIONS E) SUBSET V) /\ graph(E) /\ fan1(x,V,E) /\ fan2(x,V,E)/\\r
  84 fan6(x,V,E)/\ fan7(x,V,E)`;;\r
  85 \r
  86 \r
  87 let base_point_fan=new_definition`base_point_fan (x,V,E)=x`;;\r
  88 \r
  89 let set_of_edges=new_definition`set_of_edges v E={w|{v,w} IN E}`;;\r
  90 \r
  91 let set_of_edge=new_definition`set_of_edge v V E={w|{v,w} IN E /\ w IN V}`;;\r
  92 \r
  93 (* local fan def. To Here. *)\r
  94 \r
  95 let zfan = new_definition `zfan (V,E) = FAN (vec 0 ,V,E)`;;\r
  96 \r
  97 let hypermap_of_fan = `hypermap_of_zfan\r
  98   (V,E) = `;;\r
  99 \r
 100 let tuple_of_dart = `tuple_of_dart (V,E) \r
 101   (v,w) = \r
 102   (vec 0 , v , w, ...)`;;\r
 103 \r
 104 let azim_fandart = `azim_fandart H (v,w) =\r
 105   (let (v0,v1,v2,v3) = tuple_of_dart H (v,w)\r
 106    in azim v0 v1 v2 v3)  `;;\r
 107 \r
 108 let WRGCVDR1_concl = `!(V,E,f). convex_local_fan (V,E,f) ==> BIJ (\ (v,w). v) f V`;;\r
 109 \r
 110 let WRGCVDR2_concl = `!(V,E,f). convex_local_fan (V,E,f) ==> cyclic_permutation rho_convex_local_fan V`;;\r
 111 \r
 112 (* nd = FST *)\r
 113 \r
 114 \r
 115 let LVDUCXU1_concl = `!V E f. zfan (V,E) /\\r
 116   (f IN face_set(hypermap_of_zfan (V,E))) \r
 117    ==> local_fan (localization(V,E,f))\r
 118    `;;\r
 119 \r
 120 let LVDUCXU2_concl = `!V E f x. zfan (V,E) /\\r
 121   (f IN face_set(hypermap_of_zfan (V,E))) /\\r
 122   (x IN f) \r
 123    ==> (tuple_of_dart H x = tuple_of_dart\r
 124 \r
 125 \r
 126 end;;\r