Update from HH

[Flyspeck/.git] / text_formalization / hypermap / bauer_nipkow.hl

(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: hypermap                                                             *)
(* Author:  Thomas Hales     *)
(* Date: 2011-04-29                                                    *)
(* ========================================================================== *)

(* Port The Bauer-Nipkow completeness theorem from Isabelle,
    based on
   http://afp.sourceforge.net/browser_info/current/HOL/Flyspeck-Tame/outline.pdf

   This is a human-translation of the Isabelle code.  As a correctness
   check, it should be autmatically translated back into Isabelle,
   then checked that the Isabelle thm implies the retranslation of the
   thm here.

   The tame_graph_classification_theorem is the translation into HOL
   Light of the main result of Flyspeck I, Bauer-Nipkow.  To use it,
   we should prove that a (restricted) planar hypermap has a
   face listing that in bn_planar, and a tame hypermap has a
   face listing that is bn_tame.

*)

needs "Library/rstc.ml";; (* for RTC reflexive transitive closure *)

(* flyspeck_needs "../../tame_archive/tame_archive.hl";; *)

module Tame_classification = struct

  open Hales_tactic;;
(*
types: num, (A) list, (A ==> B), (A) Option, A#B, bool.
*)

let translate a = ();;

translate ("#",`CONS`);;
translate ("@",`APPEND`);;
translate ("!",`EL`);;
translate ("length",`LENGTH`);;
translate ("rev",`REVERSE`);;
translate ("?",`ITER`);;

(* List operations in Isabelle-Main:
   op @, concat, filter, length, map, op !, remove1, rev, 
   rotate, rotate1, upto, upt, zip.

   Other things in main:
   the,
   See http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013/doc/main.pdf
*)

(*
(* HOL Light definition from hypermap. Use ITER instead. *)

parse_as_infix("POWER",(24,"right"));;

let POWER = new_recursive_definition num_RECURSION 
  `(!(f:A->A). f POWER 0  = I) /\  
   (!(f:A->A) (n:num). f POWER (SUC n) = (f POWER n) o f)`;;
*)


(* import of 1.1 HOL *)

translate ("the",`the`);;

let the = new_definition `the s = @(x:A). (s = SOME x)`;;

let the_some = prove_by_refinement(
  `!(x:A). the (SOME x) = x`,
  (* {{{ proof *)
  [
  REWRITE_TAC[the];
  GEN_TAC;
  SELECT_TAC;
    INTRO_TAC option_RECURSION [`x`;`I:A->A`];
    REWRITE_TAC[I_THM];
    REPEAT WEAKER_STRIP_TAC;
    BY(ASM_MESON_TAC[]);
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)


(* definition enum :: "nat \<Rightarrow> nat set" where
  [code del]: "enum n = {..<n}" *)

(* let bn_enum  = new_definition `bn_enum (n: num) = { m | m < n } `;; *)

translate ("filter",`filter`);;

(* 1.2 length xs, 1.2.2 filter P xs, 1.2.3 concat,  *)

(*
let filter_liz = prove_by_refinement(
  `filter (f:A->bool) [] = [] /\
    filter f (x:: xs) = if (f x) then (x :: (filter f xs)) else filter f xs`,
  (* {{{ proof *)
  [
    BY(REWRITE_TAC[Seq.filter])
  ]);;
  (* }}} *)

(*
let bn_filter = new_recursive_definition list_RECURSION
  `bn_filter (f:A->bool) [] = [] /\
    bn_filter f ( x:: xs) = if (f x) then (x :: (bn_filter f xs)) else bn_filter f xs`;;

let bn_filter_FILTER = prove_by_refinement (`bn_filter = FILTER`,
  [
  ONCE_REWRITE_TAC[FUN_EQ_THM];
  GEN_TAC;
  ONCE_REWRITE_TAC[FUN_EQ_THM];
  LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[FILTER;bn_filter];
  ]);;
*)


let filter_FILTER = prove_by_refinement(
  `filter = FILTER`,
  (* {{{ proof *)
  [
  ONCE_REWRITE_TAC[FUN_EQ_THM];
  GEN_TAC;
  ONCE_REWRITE_TAC[FUN_EQ_THM];
  BY(LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[Seq.filter;FILTER])
  ]);;
  (* }}} *)

translate ("concat",`concat`);;


let concat = new_recursive_definition list_RECURSION
  `concat ([]:(A list)list) = [] /\
    concat ( (x:A list) :: xs) = APPEND x (concat xs)`;;

(* notation: disjoint_sum { x in xs } f  = concat (MAP (\x. f) xs) *)

(* list_update *)

(* 1.2.3 listProd1, listProd *)

translate ("map",`MAP`);;
translate ("listProd1",`list_prod1`);;
translate ("listProd",`list_prod`);;
translate ("bn_minimal",`bn_minimal`);;

Seq.map_MAP;; (`map = MAP`);;

let list_prod1 = new_definition `list_prod1 (a:A) (b:B list) = 
   MAP(\x. (a,x)) b`;;

let list_prod = new_definition `list_prod (a:A list) (b:B list) =
   concat (MAP (\x. list_prod1 x b) a)`;;

(* 1.2.5 *)

let bn_minimal = new_recursive_definition list_RECURSION
  `(bn_minimal (f:A->num)  [] = CHOICE (UNIV:A->bool)) /\ 
    (bn_minimal (f:A->num) ( (x:A) :: xs) = if (xs= []) then (x:A) else
        (let m = bn_minimal f xs in (if(f x <= f m) then x else m)))`;;

(* benign redefinition from Misc_defs_and_lemmas module *)

translate ("min_list",`min_list`);;

let min_num = new_definition `min_num X = (@m. (m:num) IN X /\ (!n. n IN X ==> m <= n))`;;

let min_list = new_definition `min_list (xs:num list) = min_num (set_of_list xs)`;;

let min_num_single = prove_by_refinement(
  `!x. min_num {x} = x`,
  (* {{{ proof *)
  [
  GEN_TAC;
  TYPIFY `x IN {x} ==> min_num {x} IN {x}` (C SUBGOAL_THEN MP_TAC);
    REWRITE_TAC[IN];
    BY(MESON_TAC[Misc_defs_and_lemmas.min_least ]);
  BY(REWRITE_TAC[IN_SING])
  ]);;
  (* }}} *)

let min_num_in = prove_by_refinement(
  `!X. ~(X = {}) ==> min_num X IN X`,
  (* {{{ proof *)
  [
  REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;NOT_FORALL_THM];
  REWRITE_TAC[IN];
  BY(MESON_TAC[Misc_defs_and_lemmas.min_least ])
  ]);;
  (* }}} *)

let min_num_le = prove_by_refinement(
  `!X c. c IN X ==> min_num X <= c`,
  (* {{{ proof *)
  [
  REWRITE_TAC[IN];
  BY(MESON_TAC[Misc_defs_and_lemmas.min_least ])
  ]);;
  (* }}} *)

let min_num_unique = prove_by_refinement(
  `!X c. c IN X /\ (!c'. c' IN X ==> c <= c') ==> min_num X = c`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC (arith `x <= (c:num) /\ c <= x ==> x = c`);
  CONJ_TAC;
    MATCH_MP_TAC min_num_le;
    BY(ASM_REWRITE_TAC[]);
  FIRST_X_ASSUM MATCH_MP_TAC;
  MATCH_MP_TAC min_num_in;
  BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[])
  ]);;
  (* }}} *)

let min_num_insert = prove_by_refinement(
  `!x X. ~(X = {}) ==> min_num (x INSERT X) = MIN x (min_num X)`,
  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  TYPIFY `x IN x INSERT X` (C SUBGOAL_THEN ASSUME_TAC);
    BY(SET_TAC[]);
  DISCH_TAC;
  MATCH_MP_TAC min_num_unique;
  CONJ_TAC;
    REWRITE_TAC[MIN];
    COND_CASES_TAC;
      BY(SET_TAC[]);
    TYPIFY `min_num X IN X` ENOUGH_TO_SHOW_TAC;
      BY(SET_TAC[]);
    MATCH_MP_TAC min_num_in;
    BY(ASM_REWRITE_TAC[]);
  REWRITE_TAC[IN_INSERT];
  REPEAT STRIP_TAC;
    ASM_REWRITE_TAC[];
    BY(REWRITE_TAC[MIN] THEN ARITH_TAC);
  MATCH_MP_TAC (arith `m <= min_num X /\ min_num X <= c' ==> m <= c'`);
  CONJ_TAC;
    BY(REWRITE_TAC[MIN] THEN ARITH_TAC);
  MATCH_MP_TAC min_num_le;
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let minn_MIN = prove_by_refinement(
  `minn = MIN`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM];
  REWRITE_TAC[MIN;Ssrnat.minn];
  BY(ARITH_TAC)
  ]);;
  (* }}} *)

let min_list_liz = prove_by_refinement(
  `!x xs. min_list (x :: xs) = if (xs = []) then x else MIN x (min_list xs)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[min_list;set_of_list];
  REPEAT GEN_TAC;
  COND_CASES_TAC;
    BY(ASM_REWRITE_TAC[set_of_list;min_num_single]);
  MATCH_MP_TAC min_num_insert;
  BY(ASM_REWRITE_TAC[SET_OF_LIST_EQ_EMPTY])
  ]);;
  (* }}} *)

(*
let max_num = new_definition `max_num (x:num->bool) = (@m. x m /\ (!n. x n ==> n <= m))`;;

let bn_max_list = new_definition `bn_max_list (xs:num list) = max_num (set_of_list xs)`;;
*)

(* 1.2.6 replace *)

translate ("replace",`replace`);;

let replace = new_recursive_definition list_RECURSION 
   `(replace x ys [] = []) /\
     replace x ys ( (z:A) :: zs) = 
            if (z = x) then APPEND ys zs else z:: (replace x ys zs)`;;

(*
let sub_list = new_recursive_definition list_RECURSION
   `sub_list r n xs [] = REVERSE xs /\
     sub_list r n xs ( (y:A) :: ys) = if (n=0) then (APPEND (REVERSE xs) ( r :: ys)) 
         else (sub_list r (n-1) ( y :: xs) ys)`;;
*)

translate ("mapAt",`bn_mapAt`);;

(* clean this up later.  Isabelle has special notation for (mapAt1 f n [] xs) *)

let mapAt1 = new_recursive_definition list_RECURSION
   `mapAt1 (f:A->A) n xs [] = REVERSE xs /\
     mapAt1 (f:A->A) n xs ((y:A) :: ys) = if (n=0) then (APPEND (REVERSE xs) ( (f y) :: ys)) 
         else (mapAt1 f (n-1) (y :: xs) ys)`;;

let bn_mapAt = new_recursive_definition list_RECURSION 
  `(bn_mapAt [] (f:A->A) (xs:A list) = xs) /\
    (bn_mapAt ((n:num) :: ns) (f:A->A) (xs:A list) = if (n < LENGTH xs) 
       then bn_mapAt ns f (mapAt1 f n [] xs) else bn_mapAt ns f xs)`;;

(* 1.2.9 rotate *)

translate ("rotate1",`rotate1`);;
translate ("rotate",`rotate`);;

(* `rot` is different because rot changes only up to the length of the list *)

let rotate1 = new_recursive_definition list_RECURSION
   `rotate1 ([]:A list) = [] /\
     rotate1 ((x:A) :: xs) = APPEND xs [x]`;;

let rotate = new_definition `rotate (n:num) (xs:A list) = (ITER n rotate1) xs`;;

(* 1.3 splitAt *)

translate ("splitAtRec",`splitAtRec`);;
translate ("splitAt",`splitAt`);;

let splitAtRec = new_recursive_definition list_RECURSION 
 `splitAtRec (c:A) bs [] = (bs,[]) /\
   splitAtRec c bs ((a:A) :: xs) = if (a = c) then (bs,xs) else splitAtRec c (APPEND bs [a]) xs`;;

let splitAt = new_definition `splitAt (c:A) xs = splitAtRec c [] xs`;;

(* 1.4 between *)

translate ("set",`set_of_list`);;
translate ("?",`IN`);;
translate ("between",`between'`);;  (* between is already used in HOL-Light *)

let between' = new_definition `between' (vs:A list) (ram1:A) (ram2:A) = 
    (let (pre1,post1) = splitAt ram1 vs in
       if (ram2 IN set_of_list post1) then
         (let (pre2,post2) = splitAt ram2 post1 in pre2)
       else (let (pre2,post2) = splitAt ram2 pre1 in APPEND post1 pre2))`;;

(* 1.5 Tables *)

(* type (a,b) table is (a#b) list *)

let bn_isTable = new_definition `bn_isTable (f:A->B) vs t =
    !p. (set_of_list t p ==> ((SND p = f (FST p)) /\ set_of_list vs (FST p)))`;;

let bn_removeKey = new_definition `bn_removeKey a (ps:(A#B) list) = 
    FILTER (\p. ~(a = FST p)) ps`;;

let bn_removeKeyList = new_recursive_definition list_RECURSION
  `bn_removeKeyList [] ps = ps /\
    bn_removeKeyList (w :: ws) (ps:(A#B) list) = bn_removeKey w (bn_removeKeyList ws ps)`;;

(*  infixes: =~ (congs) is congruence modulo rotation on lists,  -~ unused on lists.
                  =~ is pr_isomorphism on graphs, -~ isomorphic of graphs.

     {=~} is Isabelle notation for {(f1,f2). f1 =~ f2}.

    type a Fgraph  a list -> bool
            a fgraph a list list
*)

let bn_congs = new_definition `bn_congs (f1:A list) f2 = ?n. f2 = rotate n f1`;;

(* 2.2 homomorphism and isomorphism *)

let bn_is_Hom = new_definition`bn_is_Hom (phi:A->B) Fs1 Fs2 = 
  IMAGE bn_congs (IMAGE (MAP phi) Fs1)
  = IMAGE bn_congs (Fs2)`;;

let bn_inj_on = new_definition 
  `bn_inj_on (f:A->B) s = ( !x y. (s x /\ s y /\ (f x = f y)) ==> (x = y))`;;

let bn_is_pr_Iso = new_definition `bn_is_pr_Iso (phi:A->B) Fs1 Fs2 = 
   (bn_is_Hom phi Fs1 Fs2 /\ bn_inj_on phi (UNIONS (IMAGE set_of_list Fs1)))`;;

let bn_is_hom = new_definition
   `bn_is_hom (phi:A->B) fs1 fs2 = bn_is_Hom phi (set_of_list fs1) (set_of_list fs2)`;;

let bn_is_pr_iso = new_definition
 `bn_is_pr_iso (phi:A->B) fs1 fs2  = bn_is_pr_Iso phi (set_of_list fs1) (set_of_list fs2)`;;

(* 
I don't think I'll need these:
*)

(* bn_pr_iso_test0, bn_pr_iso_test1,  *)

(* 2.3.1 
   def bn_oneone, 
    types (A,B) tester, (A,B) merger.
   def bn_pr_iso_test2
   def bn_test:(A,B) tester
   bn_merge:(A,B) merger
   bn_test2:(A,B) tester
   bn_merge2:(A,B) merger
   bn_pr_iso_test3,
   bn_pr_iso_test,
*)

(* 2.3.2, improper isomorphisms *)

let bn_is_Iso = new_definition `bn_is_Iso (phi:A->B) Fs1 Fs2 = 
   (bn_is_pr_Iso phi Fs1 Fs2 \/ bn_is_pr_Iso phi Fs1 (IMAGE REVERSE Fs2))`;;

let bn_is_iso = new_definition `bn_is_iso (phi:A->B) fs1 fs2 = 
   bn_is_Iso phi (set_of_list fs1) (set_of_list fs2)`;;

let bn_cong_iso = new_definition 
  `bn_cong_iso fs1 fs2 = ?(phi:A->B). bn_is_iso phi fs1 fs2`;;

let bn_cong_pr_iso = new_definition 
  `bn_cong_pr_iso fs1 fs2 = ?(phi:A->B). bn_is_pr_iso phi fs1 fs2`;;

(* -~ abbrev for bn_cong_iso, =~ bn_cong_pr_iso *)

(* bn_iso_test,
*)

(* 2.4 Elementhood *)

(* XX drop primes *)

let bn_pr_iso_in = new_definition
  `bn_pr_iso_in (x:(A list) list) M = ?(y:(B list) list). (bn_cong_pr_iso x y /\ M y)`;;

let bn_pr_iso_subseteq = new_definition
  `bn_pr_iso_subseteq (M:(A list) list -> bool) (N:(B list) list -> bool) 
     = !x. M x ==> bn_pr_iso_in x N`;;

let bn_iso_in = new_definition
  `bn_iso_in (x:(A list) list) M = ?(y:(B list) list). (bn_cong_iso x y /\ M y)`;;

let bn_iso_subseteq = new_definition
  `bn_iso_subseteq (M:(A list) list -> bool) (N:(B list) list -> bool) 
     = !x. M x ==> bn_iso_in x N`;;

(* 3.0 More rotation *)

let rotate_to = new_definition `rotate_to (vs:A list) v = 
    v :: (APPEND (SND (splitAt v vs))  (FST (splitAt v vs)))`;;

let rotate_min = new_definition `rotate_min (vs:num list) = 
  rotate_to vs (min_list vs)`;;  

(* 4.0 Graph

UNION1
INTER1
UNION
INTER

types vertex = nat

const
  vertices
  edges

abbrev vertices_set

4.2 Faces

   facetype = Final | Nonfinal
   datatype face = Face (vertex list) facetype
   consts final:A->bool
        type:A->facetype
   
    final_face = final:face->bool
    type_face = type:face->facetype
    vertices_face = vertices:face -> vertex list


*)

let bn_final_face = new_definition `bn_final_face (vs:A,f:bool) = f`;;

(* bn_type_face  = bn_final_face *)

let bn_vertices_face = new_definition `bn_vertices_face (vs:A,f:B) = vs`;;

let bn_vertices_set = new_definition `bn_vertices_set (fs:A list#B) = 
  set_of_list (bn_vertices_face fs)`;;

(* =~ on faces means =~ on vertex list *)

(* delete:
let bn_set_final = new_definition `bn_set_final (vs:A,f:bool) = (vs,T)`;;
*)

let bn_setFinal = new_definition `bn_setFinal (vs:A,f:bool) = (vs,T)`;;

(* nextVertex written as a dot . *)

let bn_nextElem = new_recursive_definition list_RECURSION 
  `bn_nextElem [] (b:A) x = b /\
    bn_nextElem (a :: aas) b x = 
     if (x=a) then (if (LENGTH aas = 0) then b else HD aas) else bn_nextElem aas b x`;;

let bn_nextVertex = new_definition `bn_nextVertex (vs:A list,f:bool) =
   bn_nextElem vs (HD vs)`;;

let bn_edges = new_definition `bn_edges (fs:A list # bool)  =
   IMAGE (\a. (a, bn_nextVertex fs a)) (bn_vertices_set fs)`;;

let bn_nextVertices = new_definition `bn_nextVertices (vs:A list,f:bool) (n:num) v = 
    (ITER n (bn_nextVertex (vs,f))) v`;;

(* op = REVERSE,  op_graph = Graph.op, op_graph *)

let bn_prevVertex = new_definition `bn_prevVertex (vs:A list,f:bool) v =
   (bn_nextElem (REVERSE vs) (LAST vs) v)`;;

let bn_triangle = new_definition `bn_triangle (vs:A list,f:bool) = (LENGTH vs = 3)`;;

(* 4.3 Graphs *)

(* XX drop primes *)

(*
bn_graph:
list of faces (with boolean marking if each face is final),
number of vertices,
list whose ith entry is the list of faces containing vertex i,
a list of heights.
*)

let new_graph_th = prove(`?(x:((num list # bool) list) #  (num) 
   # (((num list # bool) list) list) # (num list))  . T`,MESON_TAC[]);;

let bn_graph_type = new_type_definition 
  "bn_graph" ("mk_bn_graph","dest_bn_graph") new_graph_th;;

let bn_faces = new_definition `bn_faces g = FST (dest_bn_graph g)`;;

(* abbrev F *)

let bn_Faces = new_definition `bn_Faces g = set_of_list (bn_faces g)`;;

let bn_countVertices = new_definition
  `bn_countVertices g = FST (SND (dest_bn_graph g))`;;

let bn_vertices_graph = new_definition 
 `bn_vertices_graph g = 0.. (bn_countVertices g - 1)`;;

let bn_faceListAt = new_definition
  `bn_faceListAt g = FST (SND (SND (dest_bn_graph g)))`;;

let bn_facesAt = new_definition
  `bn_facesAt g v = EL v (bn_faceListAt g )`;;

let bn_heights = new_definition `bn_heights g = SND(SND(SND(dest_bn_graph g)))`;;

let bn_height = new_definition `bn_height g v = EL v (bn_heights g)`;;

(* seed *)

let LIST_TO = new_recursive_definition num_RECURSION
  `LIST_TO 0 = [] /\ LIST_TO (SUC n) = APPEND (LIST_TO n) [n]`;;

let UPT= new_recursive_definition num_RECURSION
   `UPT m 0 = [] /\ (UPT m (SUC n) = if (n < m) then [] else APPEND (UPT m n) [n]  )`;;

(* notation: [m..<n] = UPT m n *)

(* could replace LIST_TO with UPT 0 *)

let bn_graph = new_definition  `bn_graph n = 
     (let vs = LIST_TO n in
      let fs =  [(vs,T);(vs,F)] in
        mk_bn_graph (    fs , n, REPLICATE n fs, REPLICATE n 0))`;;

(* 4.4 Operations on graphs *)

let bn_finals = new_definition `bn_finals g =
   FILTER bn_final_face (bn_faces g)`;;

let bn_nonFinals = new_definition `bn_nonFinals g = 
   FILTER (\r. ~( bn_final_face r)) (bn_faces g)`;;

let bn_countNonFinals = new_definition `bn_countNonFinals g =
   LENGTH (bn_nonFinals g)`;;

let bn_finalGraph = new_definition `bn_finalGraph g = (bn_countNonFinals g = 0)`;;

let bn_finalVertex = new_definition `bn_finalVertex g v = 
   (!f.  set_of_list(bn_facesAt g v) f ==> bn_final_face f)`;;

let bn_degree = new_definition `bn_degree g v = LENGTH(bn_facesAt g v)`;;

let bn_tri = new_definition  `bn_tri g v =
    LENGTH(FILTER (\f. bn_final_face f /\ LENGTH(bn_vertices_face f)=3) (bn_facesAt g v))`;;

let bn_quad = new_definition  `bn_quad g v =
    LENGTH(FILTER (\f. bn_final_face f /\ LENGTH(bn_vertices_face f)=4) (bn_facesAt g v))`;;

let bn_except = new_definition  `bn_except g v =
    LENGTH(FILTER (\f. bn_final_face f /\ 5 <= LENGTH(bn_vertices_face f)) (bn_facesAt g v))`;;

let bn_vertextype = new_definition `bn_vertextype g v = 
    (bn_tri g v, bn_quad g v, bn_except g v)`;;

let bn_exceptionalVertex = new_definition `bn_exceptionalVertex g v = 
  ~(bn_except g v = 0)`;;

let bn_noExceptionals = new_definition   `bn_noExceptionals g V =
   (!v. V v ==> ~(bn_exceptionalVertex g v))`;;

let bn_edges_graph = new_definition
  `bn_edges_graph g = UNIONS { bn_edges f | bn_Faces g f }`;; 

let bn_neighbors = new_definition
  `bn_neighbors g v = MAP (\f. bn_nextVertex f v )  (bn_facesAt g v)`;;

(* 4.5 Navigation in graphs *)

(* nextFace *)

let bn_directedLength = new_definition `bn_directedLength f (a:A) b =
  if (a=b) then 0 else LENGTH(between'(bn_vertices_face f) a b) + 1`;;

(* 4.6 Code generator setup *)

(* 5 Vector *)

(* vector = list *)

(* 5.1 Tabulation *)

let bn_tabulate0 = new_definition `bn_tabulate0 (p:num# (num->A)) =
    (MAP (SND p) (LIST_TO (FST p)))`;;

let bn_tabulate = new_definition `bn_tabulate n (f:num->A) = bn_tabulate0 (n,f)`;;

let bn_tabulate2 = new_definition `bn_tabulate2 m n (f:num->num->A) =
   bn_tabulate m (\i. bn_tabulate n (f i))`;;

let bn_tabulate3 = new_definition `bn_tabulate3 l m n (f:num->num->num->A) =
   bn_tabulate l (\i. bn_tabulate m (\j. bn_tabulate n (\k. f i j k)))`;;

(*
syntax. [f. x < n], [f. x < m, y < n], [f. x < l, y < m, z < n].
*)

(* 5.2 Access *)

let bn_sub1 = new_definition `bn_sub1 ((xs:A list), (n:num)) = EL n xs`;;
   
let bn_sub = new_definition `bn_sub   (a:A list) n = bn_sub1 (a,n)`;;

(* notaton: a[n] = sub a n, a[m,n] = sub (sub a m) n, a[l,m,n] = sub(sub(sub a l)m)n *)


(* 6 Enumerating Patches  *)

let bn_enumBase = new_definition 
  `bn_enumBase nmax = MAP (\i. [i]) (LIST_TO (SUC nmax))`;;

let bn_enumAppend = new_definition
   `bn_enumAppend nmax iss = 
   concat (MAP (\is.   MAP (\n. APPEND is [n]) (UPT (LAST is) (SUC nmax))) iss)`;;

let bn_enumerator = new_definition
   `bn_enumerator inner outer = 
      (let nmax = outer - 2 in
       let k = inner - 3 in
       (MAP (\is. APPEND [0] (APPEND is [outer -1])) 
          ((bn_enumAppend nmax POWER k) (bn_enumBase nmax))))`;;

let bn_enumTab = new_definition
  `bn_enumTab = bn_tabulate2 9 9 bn_enumerator`;;

(* bn_enum already defined above, call this bn_enumt *)

let bn_enumt = new_definition `bn_enumt inner outer = 
   if (inner < 9 /\ outer < 9) then (bn_sub(bn_sub bn_enumTab inner) outer) else
    bn_enumerator inner outer`;;

let bn_hideDupsRec = new_recursive_definition list_RECURSION 
  `bn_hideDupsRec (a:A) [] = []  /\
    bn_hideDupsRec a (b :: bs) = 
      if (a = b) then NONE :: (bn_hideDupsRec b bs) 
      else  (SOME b) :: (bn_hideDupsRec b bs)`;;

let bn_hideDups = new_recursive_definition list_RECURSION
  `bn_hideDups ([]:A list) = [] /\
    bn_hideDups ((b:A) :: bs) = (SOME b) :: (bn_hideDupsRec b bs)`;;

let bn_indexToVertexList = new_definition `bn_indexToVertexList f v is = 
  bn_hideDups (MAP (\k. bn_nextVertices f k (v:A)) is)`;;

(* 7 Subdividing a Face *)

let bn_split_face = new_definition 
   `bn_split_face f (ram1:A) ram2 newVs = 
      (let vs = bn_vertices_face f in
       let f1 = APPEND [ram1] (APPEND (between' vs ram1 ram2) [ram2]) in
       let f2 = APPEND [ram2] (APPEND (between' vs ram2 ram1) [ram1]) in
         ((APPEND (REVERSE newVs) f1,F), ((APPEND f2 newVs), F)))`;;

let bn_replacefacesAt = new_definition
  `bn_replacefacesAt ns f fs Fs = bn_mapAt ns (replace f fs) Fs`;;

let bn_makeFaceFinalFaceList = new_definition
  `bn_makeFaceFinalFaceList f fs = replace f [bn_setFinal f] fs`;;

let bn_makeFaceFinal = new_definition
  `bn_makeFaceFinal f g = 
      mk_bn_graph (
        bn_makeFaceFinalFaceList f (bn_faces g),
        bn_countVertices g,
        MAP (\fs. bn_makeFaceFinalFaceList f fs) (bn_faceListAt g),
        (bn_heights g)
      )`;;

let bn_heightsNewVertices = new_definition 
  `bn_heightsNewVertices h1 h2 n = 
       MAP (\i. min_num { (h1 + i + 1), (h2 + n -i) } ) (LIST_TO n)`;;

let bn_splitFace = new_definition
  `bn_splitFace g ram1 ram2 oldF newVs = 
     (let fs = bn_faces g in
      let n = bn_countVertices g in
      let Fs = bn_faceListAt g in
      let h = bn_heights g in
      let lVs = LENGTH(newVs) in
      let vs1 = between' (bn_vertices_face oldF) ram1 ram2 in
      let vs2  = between' (bn_vertices_face oldF) ram2 ram1 in
      let (f1,f2) = bn_split_face oldF ram1 ram2 newVs in
      let Fs = bn_replacefacesAt vs1 oldF [f1] Fs in
      let Fs = bn_replacefacesAt vs2 oldF [f2] Fs in
      let Fs = bn_replacefacesAt [ram1] oldF [f2;f1] Fs in
      let Fs = bn_replacefacesAt [ram2] oldF [f1;f2] Fs in
      let Fs = APPEND Fs (REPLICATE lVs [f1;f2]) in
          (f1,f2, mk_bn_graph ((APPEND(replace oldF [f2] fs ) [f1]), (n + lVs),
                                 Fs,(APPEND h (bn_heightsNewVertices (EL ram1 h) (EL ram2 h) lVs)))
        ))`;;

(* XX replaced @ with 'the' vo *)

let bn_subdivFace0 = new_recursive_definition list_RECURSION
  `bn_subdivFace0 g f u n [] = bn_makeFaceFinal f g /\
    bn_subdivFace0 g f u n (vo :: vos) = 
      if (vo = NONE) then bn_subdivFace0 g f u (SUC n) vos else
        (let v = the vo in
           if (bn_nextVertex f u = v /\ n = 0) then bn_subdivFace0 g f v 0 vos
           else 
             (let ws = UPT (bn_countVertices g) (bn_countVertices g + n) in
              let (f1,f2,g') = bn_splitFace g u v f ws in
                bn_subdivFace0 g' f2 v 0 vos))`;;

let bn_subdivFace = new_definition 
  `bn_subdivFace g f vos = bn_subdivFace0 g f (the(HD vos)) 0 (TL vos)`;;


(* 8. Transitive closure *)

(* doing it somewhat differently from the Isabelle since Library/rstc.ml
    already does the reflexive and transitive closure of a relation *)

let bn_RTranCl = new_definition `bn_RTranCl (g:A -> A list) = 
  UNCURRY    (RTC (\x y.  MEM y (g x)))`;;

let bn_invariant = new_definition `bn_invariant (P:A->bool) succs = 
   !g g'. MEM g (succs g) ==> P g ==> P g'`;;

(* notation: g  [s]->*   g'   for (g,g') IN (RTranCl s)  *)

(* 9. Plane Graph Enumeration  *)

let bn_maxGon = new_definition `bn_maxGon (p:num) = p + 3`;;

let bn_duplicateEdge = new_definition `bn_duplicateEdge g f a b =
   (2 <= bn_directedLength f a b /\ 2 <= bn_directedLength f b a /\
    set_of_list (bn_neighbors g a) b)`;;

let bn_containsUnacceptableEdgeSnd = new_recursive_definition list_RECURSION
  `bn_containsUnacceptableEdgeSnd N (v:num) [] = F /\
    bn_containsUnacceptableEdgeSnd N v (w :: ws) = 
  if (LENGTH ws = 0) then F else
    (let w' = HD ws in
     let ws' = TL ws in
  if (v < w /\ w < w' /\ N w w') then T 
  else bn_containsUnacceptableEdgeSnd N w ws)`;;
  
let bn_containsUnacceptableEdge = new_recursive_definition list_RECURSION
  `bn_containsUnacceptableEdge N [] = F /\
  bn_containsUnacceptableEdge N (v :: vs) = 
  if (LENGTH vs = 0) then F else
    (let w = HD vs in
     let ws = TL vs in
       if ((v:num) < w /\ N v w) then T else bn_containsUnacceptableEdgeSnd N v vs)`;;

let bn_containsDuplicateEdge = new_definition
  `bn_containsDuplicateEdge g f v is = bn_containsUnacceptableEdge
    (\i j. bn_duplicateEdge g f (bn_nextVertices f i v ) (bn_nextVertices f j v)) is`;;

(* a lemma in 13.3 proves this to be the same *)

let bn_containsDuplicateEdge0 = new_definition
  `bn_containsDuplicateEdge0 g f v is =
  ((2 <= LENGTH is) /\ 
    ((?k. (k < LENGTH is - 2) /\ 
        (let i0 = EL k is in
         let i1  = EL (k+1) is in
         let i2 = EL (k+2) is in
           (bn_duplicateEdge g f (bn_nextVertices f i1 v) (bn_nextVertices f i2 v) /\
              (i0 < i1 /\ i1 < i2))))
        \/
        (let i0 = EL 0 is in
         let i1 = EL 1 is in
           (bn_duplicateEdge g f (bn_nextVertices f i0 v) (bn_nextVertices f i1 v) /\
              (i0 < i1)))))`;;

let bn_generatePolygon = new_definition 
  `bn_generatePolygon n v f g = 
  (let enumeration = bn_enumerator n (LENGTH (bn_vertices_face f)) in
   let enumeration = FILTER (\is. ~(bn_containsDuplicateEdge g f v is)) enumeration in
   let vertexLists = MAP (\is. bn_indexToVertexList f v is) enumeration in
     MAP (\vs. bn_subdivFace g f vs) vertexLists)`;;

(* concatenated union *)

let c_union = new_definition `c_union xs r = concat (MAP r xs)`;;

let bn_Seed = new_definition
  `bn_Seed p = bn_graph (bn_maxGon p)`;;

(*

let bn_next_plane0 = new_definition
  `bn_next_plane0 p g = if (bn_finalGraph g) then [] else
    c_union (bn_nonFinals g) 
      (\f. c_union (bn_vertices_face f)
         (\v. c_union (UPT 3 (SUC(bn_maxGon p)))
            (\i. bn_generatePolygon i v f g)))`;;


let bn_PlaneGraphs0 = new_definition
 `bn_PlaneGraphs0 = 
   { g | ? p.   bn_RTranCl (bn_next_plane0 p) (bn_Seed p,g) /\ bn_finalGraph g }`;;

*)

(* Plane1 *)

let bn_minimalFace = new_definition 
 `bn_minimalFace = bn_minimal (LENGTH o bn_vertices_face)`;;

let bn_minimalVertex = new_definition
  `bn_minimalVertex g f = bn_minimal (bn_height g) (bn_vertices_face f)`;;

let bn_next_plane = new_definition
  `bn_next_plane p g = 
  (let fs = bn_nonFinals g in
     if (fs = []) then [] else
       (let f = bn_minimalFace fs in
        let v = bn_minimalVertex g f in
          c_union (UPT 3 (SUC (bn_maxGon p))) (\i. bn_generatePolygon i v f g)))`;;

let bn_PlaneGraphsP = new_definition
  `bn_planeGraphsP p = 
   { g | bn_RTranCl (bn_next_plane p) (bn_Seed p,g) /\ bn_finalGraph g} `;;

let bn_PlaneGraphs = new_definition
`bn_PlaneGraphs = UNIONS (IMAGE bn_planeGraphsP (:num))`;;

(* 10 Properties *)

(* 11 Properties of Patch Enumeration *)

(* bn_increasing *)

(* 12 Properties of Face Division *)

(* bn_is_prefix *)

(* bn_is_sublist *)

(* 12.4,  bn_is_nextElem *)
(* 12.6,  bn_before *)
(* 12.7,  bn_pre_between *)
(* 12.8,  bn_pre_split_face *)
(* 12.9, bn_verticesFrom  *)
(* 12.10 bn_pre_splitFace, bn_Edges,  *)
(* 12.11 bn_removeNones *)
(* 12.12 bn_natToVertexListRec, bn_natToVertexList *)
(* 12.13 bn_is_duplicateEdge, bn_invalidVertexList *)
(* 12.14 bn_subdivFace, bn_pre_subdivFace, bn_pre_subdivFace0 *)

(* 13 *)

(* 13.1, bn_minVertex, bn_normFace, bn_normFaces, 
etc. etc.

*)


(* 16 Tameness *)

let bn_squanderTarget = new_definition `bn_squanderTarget = 15410`;;

let bn_excessTCount = new_definition `bn_excessTCount = 6300`;;

let bn_squanderVertex = new_definition `bn_squanderVertex p q = 
  if (p=0 /\ q=3) then 6180 else
    if (p=0 /\ q=4) then 9700 else
      if (p=1 /\ q=2) then 6560 else
        if (p=1 /\ q=3) then 6180 else
          if (p=2 /\ q=1) then 7970 else
            if (p=2 /\ q=2) then 4120 else
              if (p=2 /\ q=3) then 12851 else
                if (p=3 /\ q=1) then 3110 else
                  if (p=3 /\ q=2) then 8170 else
                    if (p=4 /\ q=0) then 3470 else
                      if (p=4 /\ q=1) then 3660 else
                        if (p=5 /\ q=0) then 400 else
                          if (p=5 /\ q=1) then 11360 else
                            if (p=6 /\ q=0) then 6860 else
                              if (p=7 /\ q=0) then 14500 else bn_squanderTarget`;;

let bn_squanderFace = new_definition `bn_squanderFace n = 
  if (n=3) then 0 else
    if (n=4) then 2060 else
      if (n=5) then 4819 else
        if (n=6) then 7120 else bn_squanderTarget`;;
(* tchales, changed n=6 case from 7578, 1/15/2012 to match
    tame_defs.hl, main_estimate_ineq.hl and graph generator *)

(*
let bn_separated2 = new_definition `bn_separated2 g V = 
  !v.  V v ==> ( !f. (MEM f (bn_facesAt g v)) ==> ~(V (bn_nextVertex f v)))`;;

let bn_separated3 = new_definition `bn_separated3 g V = 
  !v. V v ==> (!f. (MEM f (bn_facesAt g v)) ==> LENGTH (bn_vertices_face f)<= 4 ==>
                 (bn_vertices_set f INTER V = { v }) )`;;

let bn_separated = new_definition `bn_separated g V = 
  (bn_separated2 g V /\ bn_separated3 g V)`;;
*)


(* 16.3 Admissible weight assignments *)

let bn_admissible1 = new_definition `bn_admissible1 w g =
  (!f. bn_Faces g f ==> bn_squanderFace (LENGTH (bn_vertices_face f)) <= w f)`;;

let LIST_SUM = new_definition `LIST_SUM xs (f:A->num) = ITLIST (\x y. f x + y) xs 0`;;

let bn_admissible2 = new_definition  `bn_admissible2 w g = 
  (!v. bn_vertices_graph g v ==> (bn_except g v = 0) ==> 
     bn_squanderVertex (bn_tri g v) (bn_quad g v) <= LIST_SUM (bn_facesAt g v) w)`;;

let bn_admissible3 = new_definition `bn_admissible3 w g = 
  (!v. bn_vertices_graph g v ==> (bn_vertextype g v = (5,0,1)) ==>
     (LIST_SUM (FILTER bn_triangle (bn_facesAt g v)) w >= bn_excessTCount))`;;

let bn_admissible = new_definition `bn_admissible w g = 
  (bn_admissible1 w g /\ bn_admissible2 w g /\ bn_admissible3 w g) `;;

(* 16.4 Tameness *)

let bn_tame9a = new_definition `bn_tame9a g = 
  (!f. bn_Faces g f ==> 
     3 <= LENGTH(bn_vertices_face f) /\ LENGTH(bn_vertices_face f) <= 6)`;;

let bn_tame10 = new_definition `bn_tame10 g = 
  (let n = bn_countVertices g in
     13 <= n /\ n <= 15)`;;

let bn_tame11a = new_definition `bn_tame11a g = 
  (!v. bn_vertices_graph g v ==>  3 <= bn_degree g v)`;;

let bn_tame11b = new_definition `bn_tame11b g = 
  (!v. bn_vertices_graph g v ==> 
     bn_degree g v <= (if (bn_except g v = 0) then 7 else 6))`;;

let bn_tame12o = new_definition `bn_tame12o g = 
  (!v. bn_vertices_graph g v ==>
     (~(bn_except g v = 0) /\ bn_degree g v = 6) ==> (bn_vertextype g v = (5,0,1)))`;;

let bn_tame13a = new_definition `bn_tame13a g = 
  (?w. bn_admissible w g /\ LIST_SUM (bn_faces g) w < bn_squanderTarget)`;;

let bn_tame = new_definition `bn_tame g= 
  (bn_tame9a g /\ bn_tame10 g/\ bn_tame11a g/\ 
    bn_tame11b g/\ bn_tame12o g/\ bn_tame13a g)`;;
  
(* 26 *)

let bn_fgraph = new_definition `bn_fgraph g = MAP bn_vertices_face (bn_faces g)`;;

(* the list bn_Archive is the concatenation of bn_Tri, bn_Quad, bn_Pent, and bn_Hex.
    These definitions need to be loaded from the Arch theory (which converts
    them from .ML files)  *)

(*  (* bn_tame_archive is defined in ../../tame_archive/tame_archive.hl *)
let tame_graph_classification_theorem = (* new_definition *)
  `tame_graph_classification_theorem = 
  (!g. bn_PlaneGraphs g /\ bn_tame g ==> bn_iso_in (bn_fgraph g)   bn_tame_archive)`;;

*)


*)


end;;