development/thales/session/work_in_progress.hl

   1
   2 module Work_in_progress = struct
   3 end;;
   4
   5 (* *************************************************************************** *)
   6 (* COMPLETED LEMMAS *)
   7 (* *************************************************************************** *)
   8
   9 (* *************************************************************************** *)
  10 (* WORK IN PROGRESS *)
  11 (* *************************************************************************** *)
  12
  13 (* hypermap liason *)
  14
  15 (* the list bn_Archive is the concatenation of bn_Tri, bn_Quad, bn_Pent, and bn_Hex.
  16     These definitions need to be loaded from the Arch theory (which converts
  17     them from .ML files)  *)
  18
  19
  20 flyspeck_needs "../tame_archive/tame_archive.hl";;
  21
  22
  23
  24 open Tame_archive;;  (* must open because of reflected references *)
  25 open Hypermap;;
  26 open Tame_classification;;
  27
  28 time Tame_archive.arc3 ();;  (* 0.18 secs *)
  29 List.length !Tame_archive.ref3;;  (* 9 *)
  30 arc3();; (* build data *)
  31
  32 let archive3a = new_definition (mk_eq (`archive3a:((num list)list)list`, hol_of_list3 !ref3));;
  33
  34 let isabelle_graph_class_axiom3 = new_definition
  35   `isabelle_graph_class_axiom3 = (!g. bn_PlaneGraphs g /\ bn_tame g /\
  36   (!f. bn_Faces g f ==> LENGTH (FST f) = 3) ==>
  37   bn_iso_in (bn_fgraph g) (set_of_list archive3a))`;;
  38
  39 let isabelle_graph_class_axiom = (* new_definition *)
  40   `tame_graph_classification_theorem =
  41   (!g. bn_PlaneGraphs g /\ bn_tame g ==> bn_iso_in (bn_fgraph g) (set_of_list tame_archive))`;;
  42
  43 let tame_bn_tame = `!H. tame_hypermap (H:(A)hypermap)
  44   ==> (?g. bn_PlaneGraphs g /\ bn_tame g /\
  45          iso H (hypermap_of_list (bn_fgraph g)))`;;
  46
  47 let tame_not_contravening = `isabelle_graph_classification_theorem
  48   ==> (!V. tame_hypermap (hypermap_of_fan (V,ESTD V)) ==> ~contravening V)`;;
  49
  50 let bn_cong_iso_refl = prove_by_refinement(
  51   `!(g:((A)list)list). bn_cong_iso g g`,
  52   (* {{{ proof *)
  53   [
  54   REWRITE_TAC[bn_cong_iso];
  55   REPEAT WEAKER_STRIP_TAC;
  56   TYPIFY `I:A->A` EXISTS_TAC;
  57   REWRITE_TAC[bn_is_iso;bn_is_Iso;bn_is_pr_Iso;bn_is_Hom;bn_inj_on;I_THM;MAP_I;IMAGE_I];
  58   DISJ1_TAC;
  59   BY(MESON_TAC[])
  60   ]);;
  61   (* }}} *)
  62
  63 let rot_bn_rotate = prove_by_refinement(
  64   `!n s. rot n s = bn_rotate n s`,
  65   (* {{{ proof *)
  66   [
  67   rt[Seq.rot;bn_rotate;bn_rotate1]
  68     INDUCT_TAC
  69     rt[POWER_0]
  70   rt[Seq.drop0;Seq.take;I_THM;Seq.cats0]
  71 g
  72 rt[POWER;o_THM;bn_rotate1]
  73   ]);;
  74   (* }}} *)
  75
  76
  77 let perm_eq_bn_cong_iso = prove_by_refinement(
  78   `!g1 g2. good_list g1 /\ bn_cong_iso g1 g2 ==> perm_eq g1 g2`,
  79   (* {{{ proof *)
  80   [
  81   rt[Seq.perm_eq;bn_cong_iso]
  82   ]);;
  83   (* }}} *)
  84
  85
  86 let bn_cong_iso = prove_by_refinement(
  87   `!g1 g2. good_list g1 /\ bn_cong_iso g1 g2 ==> iso (hypermap_of_list g1) (hypermap_of_list g2)`,
  88   (* {{{ proof *)
  89   [
  90 g/r
  91       rt[bn_cong_iso;bn_is_iso;bn_is_Iso;bn_is_pr_Iso;bn_is_Hom;bn_inj_on]
  92         rt[bn_congs;iso]
  93 st/r
  94   ]);;
  95   (* }}} *)
  96
  97
  98 bn_congs;;
  99