(*
Notes on the hypermap chapter.

new type: hypermap

infixes: POWER, belong, iso.

key definitions: orbit_map f x (the orbit of x under f),
  edge x (edge map orbit of x), node x, face x.
  edge_map, face_map, node_map (the permutations)




*)

(*
Notes by Tom Hales in a conversation with TNT on Sep 9, 2010.

  TNT has completed essentially everything up the section with title "transform"
  The main theorem in the "transform" section is called AQIUNPP (markup transform).
  It is a long proof that is  complete except for (flag1) and (flag2).  TNT promises
  to send the completed proof of AQIUNPP on Sep 12, 2010.

  TNT's general naming convention is lemmaABC for the lemma with guid
  ABC.  In particular,
  lemmaZHQCZLX; lemmaFKSNTKR; lemmaHOZKXVW; lemmaTGJISOK; lemmaIUCLZYI;
  lemmaBISHKQW; lemmaFOAGLPA; lemmaSGCOSXK; lemmaQZTPGJV; lemmaKDAEDEX;
  lemmaLIPYTUI; lemmaILTXRQD; lemmaICJHAOQ; lemmaJMKRXLA; 
  lemmaHQYMRTX; lemmaQRDYXYJ.

  [Note: 2/15/2012
  *On HYQMRTX, the furthermore clause in the flypaper hasn't been included in lemmaHQYMRTX.
  *I can't find lemmaQRDYXY. It must not have been uploaded.
  *Also found lemmaSTKBEPH.  This is the algorithm termination; once there are sufficiently many
     loops in a normal family, it must be the collection of faces.  This seems to have been deleted
     from flypaper.pdf.
  ]


  RDW. Reverse double walkup. This is not implemented as of Sep 2010.
  He plans to do it in two cases. The special case that does not add
  any new nodes and the general case.  HLT needs the special case in
  the fans chapter.

*)

(*

  KHGAQRG.  Not done as a separate lemma, but instead it appears many
  times as a subgoal.  If you have a restricted hypermap and and f step,
  then you get a singleton.  compare set_one_point,
  lemma_singleton_atom, .

  YBGABWW. Equivalent but not identical to theorems in TNT.

  PKRQTKP. There are many orbit theorems in hypermap.hl

  ZJIOZB (def of merge and split), ZMFKZNH (merge-split).  Both TNT
  and Gonthier reverse things so that the lemma serves as a definition
  and the def is proved as a lemma.

  ZMFKZNH breaks into several formal lemmas: lemma_face_merge,
  lemma_edge_merge, lemma_node_merge.

  IUCLZYI. This has been formalized, but it is not used directly
  elsewhere.  Instead, a number of smaller preliminary lemmas get
  used.

  EUXPBPO = lemmaThreeDarts //

  WIRLCNL. Something equivalent gets done in lemma_cycle_is_face and
  lemmaQuotientFace.

  UDJNSHH. Not formalized. Instead the proofs that rely on it go back
  to definitions instead.

  KSRDPTZ = lemmaQuotientNoDoubleJoints //

  PYOVATA = lemmaNodalFixedPoint (not exactly the same, the hypotheses
  are different)

  Note May 2012.
  QQYVCFM. Not formalized.  dih2k defined in such a way to avoid lemma.
  WRGCVDR_CIZMRRH.hl defines dih2k in terms of the properties
  of QQYVCHEM.  So it appears that QQYVCFM is not needed.
  cyclic_hypermap.hl and related notions are dead code, never used.

  KHGAQRG. Not formalized because TNT never needs to use it.

*)

(* Notes by Hales Feb 12, 2012.

   There are over 600 lemmas in the file.

   TNT has 108 definitions in his file, which makes it hard to
   understand the statements and how they related to the
   flypaper. Here is an informal summary of definitions.

   infixes: POWER, belong, iso

   Types:
   (A)hypermap  with extraction functions
   dart (H:(A)hypermap -> 
   edge_map
   node_map
   face_map
   
   edge H x ; edge orbit of dart x
   node H x ; node orbit of dart x
   face H x ; face orbit of dart x

   (A)loop with extraction functions.  A loop is an unordered set (of darts) together with a permutation
   that acts transitively on he set.  (This is what gets called torsor in flypaper.pdf.)
   dart_of ; dart set of loop
   next ; successor function
   back ; inverse of successor function
   belong ; in dart set
   size ; card of dart set
   top ; PRE(CARD dart_of L)
   is_loop H L ; x IN L ==>one_step_contour H x (next L x)
   loop_path L x k ;  ((next L) POWER k) x; path out of loop starting at x.
   index L x y ; (specification) smallest i such that y = next^i x.

   Informal definitions:
   POWER : nth iterate of a function.
   orbit_map (f:A->A)  (x:A)         orbit of x under f
   go_one_step H x y <=> y is the image of dart x under e,n, or f.
   is_path H (p:num->A) (n:num) ;  (p 0) ... (p n) is a dart path in H.
   is_in_component H x y ; darts x and y are in the same path component of H
   comb_component H x ; (same as is_in_component H x)
   set_of_orbits D f = set of orbits in D of f
   number_of_orbits D f = card of set_of_orbits
   
   edge_set H = set_of_orbits (dart H) (edge_map H)
   node_set H = set_of_orbits (dart H) (node_map H)
   face_set H = set_of_orbits (dart H) (face_map H)
   set_components H D = set of combinatorial components of all darts x in D
   set_part_components H D = same as set_components H D
   set_of_components H = set_components H (dart H)

   number_of_edges H = Klar
   number_of_nodes H = Klar
   number_of_faces H = Klar
   number_of_components H = Klar
   connected_hypermpa H = Klar

   plain_hypermap H
   planar_hypermap H
   simple_hypermap H
   is_no_double_joins H

   dart_degenerate H x;  the dart x is fixed by e,n, or f.
   dart_nondegenerate H x; negation
   is_edge_nondegenerate
   is_node_nondegenerate
   is_face_nondegenerate
   isolated_dart ; x = f x = n x = e x.
   is_edge_degenerate ; x = e x but x != n x, x != f x.
   is_node_degenerate
   is_face_degenerae

   ***
   **   lists as functions p:num->A: ** :

   is_inj_list (p:num->A) n ;  (p is 1-1 on 0..n)
   support_list (p:num->A) n ; { p i | i <= n}
   in_list p n ; i IN (support_list p n)
   is_disjoint p q
   glue p q n ; list concatenation.
   is_glueing p q n m ;  This states roughly that no member of (q,m) is in (p,n), except (p n = q 0).
   Used to concatenate injective lists (p,n) @ (q,m).
   join p q n ; list concatenation, swallowing head of q.

   edge_path H x i   =  ((edge_map H) POWER i) x
   node_path H x i  =  similar
   face_path H x i =  similar

   samsara  p n x = the successor to x in list (p,n), wrapping to the beginning if necessary.
   
   *** contours

   one_step_contour H x y ;   y = f x or n^{-1} x
   is_contour H p n ; (p,n) is a contour path
   node_contour H x i ;  ((inverse (node_map H)) POWER i) x
   face_contour H x i ; ((face_map H) POWER i) x
   is_inj_contour H p n ; (p,n) is an injective contour path
   
   
   *** walkup

   shift H ; rotates (e,n,f) -> (n,f,e) triality of H.
   edge_walkup H x ; new hypermap after edge_walkup of H at x.
   node_walkup H x
   face_walkup H x
   double_edge_walkup H x y
   double_node_walkup H x y
   double_face_walkup H x y
   
   *** more on orbits

   power_list f x = \i. (f POWER i) x
   inj_orbit f x n ; the power_list of f x is an inj list (p,n)

   order_permutation ; the order of a permutation of finite order.
   
   *** merge

   is_edge_merge H x.
   is_node_merge
   is_face_merge
   is_edge_split
   is_node_split
   is_face_split

   is_splitting_component H x ;  n x and e^{-1} x are in the same comb component of (edge_walkup H x)
   is_Moebius_contour H p k ; (p,k) is an (injective) Moebius contour

   shift_path p i ; \j. p (j + i)
   
   *** complements

   ind H x n ; 
   mirror H x k n ; 
   complement H x n  =mirror H x n n ; implements complementary loop of  face contour

   *** misc

   res (f:A->A) s ; restriction of function f to s, extension by identity.

   planar_ind H ; planar index iota

   iso H H' ; isomorphism of hypermap

   *** cyclic hypermap

   cyclic_hypermap ;  darts two sets of k, cyc_emap, cyc_nmap, cyc_fmap.

   cyc_emap
   cyc_nmap
   cyc_fmap  face map on cyclic hypermap

   
   *** quotients

   is_node_going H L x y ;  n^{-1} steps from dart x to y in loop L
   atom H L x = the "atom" [ .... x;n^{-1} x ....] of x in loop L
   is_normal H NF ; NF is a normal family of loops.
   quotient_darts H NF ; set of atoms from loops in NF.
   support_darts NF ; darts visiting NF
   fmap ; face map on atoms
   emap ; edge map on atoms
   nmap ;  node map on atoms
   quotient H NF ; quotient hypermap by a normal family NF.
   cycle H L ; set of atoms of L 
   support_node H NF a ; set of darts of H at the node containing the atom a

   choice H NF x ; the atom containing x in the normal family.
   head H NF x; head of  atom containing dart x.
   tail ; tail of a atom containing dart x


   face_loop H x ;  returns the loop on the face of x.
   face_collection H ; the set of face loops.

   canon_loop H NF ;  this says that every atom in NF has size 1.
   canon H NF ; the set of loops that are canonical
   canon_darts ; the set of darts of loops that are canonical
   
   canon_flag H NF ; this is not quite the way it is presented in flypaper.
   flag H NF L x ;

   *** m,p,q,x,y,z:

   minside H L x ; specification m st.  next^i x = f^i x.
   mAdd H L x ; specification p st.  f^{p+1} in support of NF.
   mRoute H L x ; specification q st ...

   dart_inside H NF L x.   { f^i x | 1<= i <= m}
   heading H NF L x ; I think this is the dart y = f^{m+1} x.
   attach H NF L x ; I think this is the dart z = f^{p+1} y.
   
   *** restricted hypermaps
   
   is_restricted H

   is_split_condition H NF L x ; long list of hypotheses; needed to split a loop into two

   is_marked H NF L x; defines marked hypermap

   *** transform of hypermap

   genex H NF L x;   glues "attach" dart to "heading" dart
   tpx H NF L x;  I think this is the size of the new face?
   geney  NF L x; glues "heading" dart to "attach" dart
   tpy H NF L x; again size of new face?
   dnax H NF L x ; new loop X
   dnay H NF L x = new loop Y

   genesis H NF L x = new set of loops, deleting L, adding two new loops.
   
*)