(* ========================================================================== *) (* 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 \ nat set" where [code del]: "enum n = {..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.. 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;;