module Work_in_progress = struct
end;;

(* *************************************************************************** *)
(* COMPLETED LEMMAS *)
(* *************************************************************************** *)

(* *************************************************************************** *)
(* WORK IN PROGRESS *)
(* *************************************************************************** *)

(* hypermap liason *)

(* 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)  *)


flyspeck_needs "../tame_archive/tame_archive.hl";;



open Tame_archive;;  (* must open because of reflected references *)
open Hypermap;;
open Tame_classification;;

time Tame_archive.arc3 ();;  (* 0.18 secs *)
List.length !Tame_archive.ref3;;  (* 9 *)
arc3();; (* build data *)

let archive3a = new_definition (mk_eq (`archive3a:((num list)list)list`, hol_of_list3 !ref3));;
let isabelle_graph_class_axiom3 = new_definition
  `isabelle_graph_class_axiom3 = (!g. bn_PlaneGraphs g /\ bn_tame g /\ 
  (!f. bn_Faces g f ==> LENGTH (FST f) = 3) ==>
  bn_iso_in (bn_fgraph g) (set_of_list archive3a))`;;
let isabelle_graph_class_axiom = (* new_definition *) `tame_graph_classification_theorem = (!g. bn_PlaneGraphs g /\ bn_tame g ==> bn_iso_in (bn_fgraph g) (set_of_list tame_archive))`;; let tame_bn_tame = `!H. tame_hypermap (H:(A)hypermap) ==> (?g. bn_PlaneGraphs g /\ bn_tame g /\ iso H (hypermap_of_list (bn_fgraph g)))`;; let tame_not_contravening = `isabelle_graph_classification_theorem ==> (!V. tame_hypermap (hypermap_of_fan (V,ESTD V)) ==> ~contravening V)`;;
let bn_cong_iso_refl = 
prove_by_refinement( `!(g:((A)list)list). bn_cong_iso g g`,
(* {{{ proof *) [ REWRITE_TAC[bn_cong_iso]; REPEAT WEAKER_STRIP_TAC; TYPIFY `I:A->A` EXISTS_TAC; REWRITE_TAC[bn_is_iso;bn_is_Iso;bn_is_pr_Iso;bn_is_Hom;bn_inj_on;I_THM;MAP_I;IMAGE_I]; DISJ1_TAC; BY(MESON_TAC[]) ]);;
(* }}} *)
let rot_bn_rotate = 
prove_by_refinement( `!n s. rot n s = bn_rotate n s`,
(* {{{ proof *) [ rt[Seq.rot;bn_rotate;bn_rotate1] INDUCT_TAC rt[POWER_0] rt[Seq.drop0;Seq.take;I_THM;Seq.cats0] g rt[POWER;o_THM;bn_rotate1] ]);;
(* }}} *)
let perm_eq_bn_cong_iso = 
prove_by_refinement( `!g1 g2. good_list g1 /\ bn_cong_iso g1 g2 ==> perm_eq g1 g2`,
(* {{{ proof *) [ rt[Seq.perm_eq;bn_cong_iso] ]);;
(* }}} *)
let bn_cong_iso = 
prove_by_refinement( `!g1 g2. good_list g1 /\ bn_cong_iso g1 g2 ==> iso (hypermap_of_list g1) (hypermap_of_list g2)`,
(* {{{ proof *) [ g/r rt[bn_cong_iso;bn_is_iso;bn_is_Iso;bn_is_pr_Iso;bn_is_Hom;bn_inj_on] rt[bn_congs;iso] st/r ]);;
(* }}} *) bn_congs;;