(* ========================================================================== *)
(* 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`,
(* }}} *)
(* 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`,
(* }}} *)
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_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`,
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
let minn_MIN = prove_by_refinement(
`minn = MIN`,
(* }}} *)
(* }}} *)
(*
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
*)
(* 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`,
let bn_graph_type = new_type_definition
"bn_graph" ("mk_bn_graph","dest_bn_graph") new_graph_th;;
(* 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_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 *)
(* 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_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 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 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 *)
(* 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;;