needs "../formal_lp/hypermap/list_hypermap.hl";;
needs "../formal_lp/hypermap/list_hypermap_iso.hl";;
needs "../formal_lp/hypermap/constants_approx.hl";;

needs "arith/nat.hl";;
needs "misc/vars.hl";;

open Constant_approximations;;
open Misc_vars;;
open Sphere;;



(* Definitions of variables *)


(* Variables for fans *)
(* TODO: these definitions are not necessary *)

let azim2_fan = new_definition `azim2_fan (V,E) (x:real^3#real^3) = azim_dart (V,E) (f_fan_pair (V,E) x)`;;
let azim3_fan = new_definition `azim3_fan (V,E) (x:real^3#real^3) = azim_dart (V,E) (inverse (f_fan_pair_ext (V,E)) x)`;;
let yn_fan = new_definition `yn_fan (n:real^3#real^3->bool) = norm (FST (@x. x IN n))`;;
let ln_fan = new_definition `ln_fan (n:real^3#real^3->bool) = abs (ly (yn_fan n))`;;
let ye_fan = new_definition `ye_fan (x:real^3#real^3) = dist x`;;
let y1_fan = new_definition `y1_fan (x:real^3#real^3) = norm(FST x)`;;
let y2_fan = new_definition `y2_fan (x:real^3#real^3) = norm(SND x)`;;
let y3_fan = new_definition `y3_fan (V,E) (x:real^3#real^3) = norm(sigma_fan (vec 0) V E (FST x) (SND x))`;;
let y4_fan = new_definition `y4_fan (V,E) (x:real^3#real^3) = dist(f_fan_pair (V,E) x)`;;
let y5_fan = new_definition `y5_fan (V,E) (x:real^3#real^3) = dist(inverse (f_fan_pair_ext (V,E)) x)`;;
let y6_fan = new_definition `y6_fan (x:real^3#real^3) = dist x`;;
let y8_fan = new_definition `y8_fan (V,E) (x:real^3#real^3) = y5_fan (V,E) (f_fan_pair_ext (V,E) x)`;;
let y9_fan = new_definition `y9_fan (V,E) (x:real^3#real^3) = dist(f_fan_pair (V,E) x)`;;
let rhazim_fan = new_definition `rhazim_fan (V,E) (x:real^3#real^3) = abs(rho(y1_fan x)) * azim_dart (V,E) x`;;
let rhazim2_fan = new_definition `rhazim2_fan (V,E) (x:real^3#real^3) = rhazim_fan (V,E) (f_fan_pair (V,E) x)`;;
let rhazim3_fan = new_definition `rhazim3_fan (V,E) (x:real^3#real^3) = rhazim_fan (V,E) (inverse (f_fan_pair_ext (V,E)) x)`;;
let rho_fan = new_definition `rho_fan n = abs((&1 + sol0 / pi) - ln_fan n * sol0 / pi)`;;
let sol_fan = new_definition `sol_fan (V,E) f = abs(sum f (\x. azim_dart (V,E) x - pi) + &2 * pi)`;;
let tau_fan = new_definition `tau_fan (V,E) f = abs (tauVEF (V,E,f))`;;

let fan_defs =
[
  azim2_fan; azim3_fan; yn_fan; ln_fan; ye_fan;
  rho_fan; sol_fan; tau_fan; rhazim_fan; rhazim2_fan; rhazim3_fan;
  y1_fan; y2_fan; y3_fan; y4_fan; y5_fan; y6_fan; y8_fan; y9_fan;
]



(* Variables for lists *)


let list_defs = map new_definition
  [
    `azim_list (V,g) = (azim_dart (V,ESTD V) o g):num#num->real`;
    `azim2_list (V,g) = (azim2_fan (V,ESTD V) o g):num#num->real`;
    `azim3_list (V,g) = (azim3_fan (V,ESTD V) o g):num#num->real`;
    `(yn_list g):(num#num->bool)->real = yn_fan o IMAGE g`;
    `(ln_list g):(num#num->bool)->real = ln_fan o IMAGE g`;
    `rhazim_list (V,g) = (rhazim_fan (V,ESTD V) o g):num#num->real`;
    `rhazim2_list (V,g) = (rhazim2_fan (V,ESTD V) o g):num#num->real`;
    `rhazim3_list (V,g) = (rhazim3_fan (V,ESTD V) o g):num#num->real`;
    `(ye_list g):(num#num->real) = ye_fan o g`;
    `(rho_list g):(num#num->bool)->real = rho_fan o IMAGE g`;
    `(sol_list (V,g)):(num#num->bool)->real = sol_fan (V,ESTD V) o IMAGE g`;
    `(tau_list (V,g)):(num#num->bool)->real = tau_fan (V,ESTD V) o IMAGE g`;
    `(y1_list g):(num#num->real) = y1_fan o g`;
    `(y2_list g):(num#num->real) = y2_fan o g`;
    `(y3_list (V,g)):(num#num->real) = y3_fan (V,ESTD V) o g`;
    `(y4_list (V,g)):(num#num->real) = y4_fan (V,ESTD V) o g`;
    `(y5_list (V,g)):(num#num->real) = y5_fan (V,ESTD V) o g`;
    `(y6_list g):(num#num->real) = y6_fan o g`;
    `(y8_list (V,g)):(num#num->real) = y8_fan (V,ESTD V) o g`;
    `(y9_list (V,g)):(num#num->real) = y9_fan (V,ESTD V) o g`;
  ];;


let list_defs2 = map (REWRITE_RULE[FUN_EQ_THM; o_THM]) list_defs;;


let list_var_rewrites =
  map GSYM list_defs @ map GSYM list_defs2;;



(* All variables are nonnegative *)

let AZIM_DART_POS = 
prove(`&0 <= azim_dart (V,E) x`,

   MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
     STRIP_TAC THEN
     ASM_REWRITE_TAC[azim_dart] THEN
     COND_CASES_TAC THENL
     [
       MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC;
       ALL_TAC
     ] THEN
     REWRITE_TAC[Fan_defs.azim_fan] THEN
     COND_CASES_TAC THEN REWRITE_TAC[azim] THEN
     MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC);;

let DIST_POS = 
prove(`!x:(real^3#real^3). &0 <= dist x`,

   GEN_TAC THEN MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
     STRIP_TAC THEN ASM_REWRITE_TAC[dist; NORM_POS_LE]);;

let list_var_pos = map (fun tm -> prove(tm,
                     GEN_TAC THEN REWRITE_TAC list_defs2 THEN REWRITE_TAC fan_defs THEN
                       TRY (MATCH_MP_TAC REAL_LE_MUL) THEN
                       REWRITE_TAC[AZIM_DART_POS; REAL_ABS_POS; NORM_POS_LE; DIST_POS]))
[
  `!x. &0 <= azim_list (V,g) x`;
  `!x. &0 <= azim2_list (V,g) x`;
  `!x. &0 <= azim3_list (V,g) x`;
  `!x. &0 <= rhazim_list (V,g) x`;
  `!x. &0 <= rhazim2_list (V,g) x`;
  `!x. &0 <= rhazim3_list (V,g) x`;
  `!n. &0 <= yn_list g n`;
  `!n. &0 <= ln_list g n`;
  `!e. &0 <= ye_list g e`;
  `!n. &0 <= rho_list g n`;
  `!f. &0 <= sol_list (V,g) f`;
  `!f. &0 <= tau_list (V,g) f`;
  `!x. &0 <= y1_list g x`;
  `!x. &0 <= y2_list g x`;
  `!x. &0 <= y3_list (V,g) x`;
  `!x. &0 <= y4_list (V,g) x`;
  `!x. &0 <= y5_list (V,g) x`;
  `!x. &0 <= y6_list g x`;
  `!x. &0 <= y8_list (V,g) x`;
  `!x. &0 <= y9_list (V,g) x`;
];;



(* mod-file variables and definitions *)

let var_bound_ineqs = Hashtbl.create 40;;

let sets =
  ["dart", `dart H:A->bool`;
   "dart3", `hyp_dart3 H:A->bool`;
   "node", `node_set H:(A->bool)->bool`;
   "face", `face_set H:(A->bool)->bool`;
   "dart_std4", `hyp_dart4 H:A->bool`];;


let define_var var_name set_name low high =
  let var = match set_name with
      "dart" | "dart3" | "dart_std4" -> `d:A`
    | "node" -> `n:A->bool`
    | "face" -> `f:A->bool`
    | _ -> failwith "Undefined set name" in
  let var_ty = snd (dest_var var) in
  let f_ty = mk_type ("fun", [var_ty; `:real`]) in
  let set_ty = mk_type ("fun", [var_ty; `:bool`]) in
  let f = mk_var (var_name^"_mod", f_ty) in
  let set = assoc set_name sets in
  let in_const = mk_mconst ("IN", mk_type ("fun", [var_ty; mk_type ("fun", [set_ty; `:bool`])])) in
  let le = `(<=):real->real->bool` in
  let fvar = mk_comb (f, var) in
  let l, h = mk_binop le low fvar, mk_binop le fvar high in
  let cond = mk_binop in_const var set in

  let ineq_lo = mk_forall(var, mk_imp(cond, l)) in
  let ineq_hi = mk_forall(var, mk_imp(cond, h)) in

  let _ = Hashtbl.add var_bound_ineqs (var_name^"_lo") ineq_lo in
  let _ = Hashtbl.add var_bound_ineqs (var_name^"_hi") ineq_hi in
    f;;




(* Terms for variables in the model file *)
Hashtbl.clear var_bound_ineqs;;

let azim_mod = define_var "azim" "dart" `&0` `pi` and
    azim2_mod = define_var "azim2" "dart3" `&0` `pi` and
    azim3_mod = define_var "azim3" "dart3" `&0` `pi` and
    ln_mod = define_var "ln" "node" `&0` `&1` and
    rhazim_mod = define_var "rhazim" "dart" `&0` `pi + sol0` and
    rhazim2_mod = define_var "rhazim2" "dart3" `&0` `pi + sol0` and
    rhazim3_mod = define_var "rhazim3" "dart3" `&0` `pi + sol0` and
    yn_mod = define_var "yn" "node" `&2` `#2.52`and
    ye_mod = define_var "ye" "dart" `&2` `&3` and
    rho_mod = define_var "rho" "node" `&1` `&1 + sol0 / pi` and
    sol_mod = define_var "sol" "face" `&0` `&4 * pi` and
    tau_mod = define_var "tau" "face" `&0` `tgt` and
    y1_mod = define_var "y1" "dart" `&2` `#2.52` and
    y2_mod = define_var "y2" "dart" `&2` `#2.52` and
    y3_mod = define_var "y3" "dart" `&2` `#2.52` and
    y4_mod = define_var "y4" "dart3" `&2` `&3` and
    y5_mod = define_var "y5" "dart" `&2` `&3` and
    y6_mod = define_var "y6" "dart" `&2` `&3` and
    y8_mod = define_var "y8" "dart_std4" `&2` `#2.52` and
    y9_mod = define_var "y9" "dart_std4" `&2` `#2.52`;;

let var_list =
  let inst_t = inst[`:real^3#real^3`, aty] in
    [
      `hypermap_of_fan (V,E)`, `H:(real^3#real^3)hypermap`;
      `azim_dart (V,E)`, inst_t azim_mod;
      `azim2_fan (V,E)`, inst_t azim2_mod;
      `azim3_fan (V,E)`, inst_t azim3_mod;
      `ln_fan`, inst_t ln_mod;
      `rhazim_fan (V,E)`, inst_t rhazim_mod;
      `rhazim2_fan (V,E)`, inst_t rhazim2_mod;
      `rhazim3_fan (V,E)`, inst_t rhazim3_mod;
      `yn_fan`, inst_t yn_mod;
      `ye_fan`, inst_t ye_mod;
      `rho_fan`, inst_t rho_mod;
      `sol_fan (V,E)`, inst_t sol_mod;
      `tau_fan (V,E)`, inst_t tau_mod;
      `y1_fan`, inst_t y1_mod;
      `y2_fan`, inst_t y2_mod;
      `y3_fan (V,E)`, inst_t y3_mod;
      `y4_fan (V,E)`, inst_t y4_mod;
      `y5_fan (V,E)`, inst_t y5_mod;
      `y6_fan`, inst_t y6_mod;
      `y8_fan (V,E)`, inst_t y8_mod;
      `y9_fan (V,E)`, inst_t y9_mod;
    ];;




(* Declare all inequalities in a format which is close to the mod-file format *)

let constraints = Hashtbl.create 100;;
let add_constraints = map (uncurry (Hashtbl.add constraints));;

(* equality constraints *)

add_constraints
[
  "azim_sum", `!n. n IN node_set (H:(A)hypermap) ==> sum n azim_mod = &2 * pi`;
  "rhazim_sum", `!n. n IN node_set (H:(A)hypermap) ==> sum n rhazim_mod = &2 * pi * rho_mod n`;

  "sol_sum3", `!f. f IN hyp_face3 (H:(A)hypermap) ==> sum f azim_mod = sol_mod f + pi`;
  "tau_sum3", `!f. f IN hyp_face3 (H:(A)hypermap) ==> sum f rhazim_mod = tau_mod f + (pi + sol0)`;
  "sol_sum4", `!f. f IN hyp_face4 (H:(A)hypermap) ==> sum f azim_mod = sol_mod f + &2 * pi`;
  "tau_sum4", `!f. f IN hyp_face4 (H:(A)hypermap) ==> sum f rhazim_mod = tau_mod f + &2 * (pi + sol0)`;
  "sol_sum5", `!f. f IN hyp_face5 (H:(A)hypermap) ==> sum f azim_mod = sol_mod f + &3 * pi`;
  "tau_sum5", `!f. f IN hyp_face5 (H:(A)hypermap) ==> sum f rhazim_mod = tau_mod f + &3 * (pi + sol0)`;
  "sol_sum6", `!f. f IN hyp_face6 (H:(A)hypermap) ==> sum f azim_mod = sol_mod f + &4 * pi`;
  "tau_sum6", `!f. f IN hyp_face6 (H:(A)hypermap) ==> sum f rhazim_mod = tau_mod f + &4 * (pi + sol0)`;

  "ln_def", `!n. n IN node_set (H:(A)hypermap) ==> ln_mod n = (#2.52 - yn_mod n) / #0.52`;
  "rho_def", `!n. n IN node_set (H:(A)hypermap) ==> rho_mod n = (&1 + sol0 / pi) - ln_mod n * sol0 / pi`;

  "edge_sym", `!e. e IN hyp_edge_pairs (H:(A)hypermap) ==> ye_mod (FST e) = ye_mod (SND e):real`;

  "y1_def", `!d. d IN dart (H:(A)hypermap) ==> y1_mod d = yn_mod (node H d):real`;
  "y2_def", `!d. d IN dart (H:(A)hypermap) ==> y2_mod d = yn_mod (node H (face_map H d)):real`;
  "y3_def", `!d. d IN dart (H:(A)hypermap) ==> y3_mod d = yn_mod (node H (inverse (face_map H) d)):real`;
  "y4_def", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> y4_mod d = ye_mod (face_map H d):real`;
  "y5_def", `!d. d IN dart (H:(A)hypermap) ==> y5_mod d = ye_mod (inverse (face_map H) d):real`;
  "y6_def", `!d. d IN dart (H:(A)hypermap) ==> y6_mod d = ye_mod d:real`;
  "y9_def", `!d. d IN hyp_dart4 (H:(A)hypermap) ==> y9_mod d = ye_mod (face_map H d):real`;
  "y8_def", `!d. d IN hyp_dart4 (H:(A)hypermap) ==> y8_mod d = y5_mod (inverse (face_map H) d):real`;

  "azim2c", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> azim2_mod d = azim_mod (face_map H d):real`;
  "azim3c", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> azim3_mod d = azim_mod (inverse (face_map H) d):real`;
  "rhazim2c", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> rhazim2_mod d = rhazim_mod (face_map H d):real`;
  "rhazim3c", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> rhazim3_mod d = rhazim_mod (inverse (face_map H) d):real`;
];;



(* inequality constraints *)

add_constraints
[
  "RHA", `!d. d IN dart (H:(A)hypermap) ==> rhazim_mod d >= azim_mod d:real`;
  "RHB", `!d. d IN dart (H:(A)hypermap) ==> rhazim_mod d <= azim_mod d * (&1 + sol0 / pi)`;
(* "RHBLO"; "RHBHI" *)
];;


(* definitional inequalities *)



(* y bounds *)
add_constraints
[
  "yy10", `!d. (d:A) IN dart (H:(A)hypermap) ==> ye_mod d <= #2.52`;
];;



(* tau tame table D inequality (Main Estimate) *)
add_constraints
[
  "tau3", `!f:A->bool. f IN hyp_face3 (H:(A)hypermap) ==> tau_mod f >= &0`;
  "tau4", `!f:A->bool. f IN hyp_face4 (H:(A)hypermap) ==> tau_mod f >= #0.206`;
  "tau5", `!f:A->bool. f IN hyp_face5 (H:(A)hypermap) ==> tau_mod f >= #0.4819`;
  "tau6", `!f:A->bool. f IN hyp_face6 (H:(A)hypermap) ==> tau_mod f >= #0.7578`;
];;


add_constraints
[
  "ineq105", `!d:A. d IN hyp_dartX H ==>
        ((((azim_mod d) - #1.629) + ((#0.402 * (y2_mod d +
                (y3_mod d + (y5_mod d + (y6_mod d - #8.0))))) -
                        (#0.315 * (y1_mod d - #2.0)))) - #0.0) >= #0.0`;

  "ineq106", `!d:A. d IN hyp_dart3 H ==>
        ((((rhazim_mod d) - #1.2308) + (((#0.3639 * (y2_mod d + (y3_mod d + (y5_mod d + (y6_mod d - #8.0))))) -
                (#0.6 * (y1_mod d - #2.0))) - (#0.685 * (y4_mod d - #2.0)))) - #0.0) >= #0.0`;

  "ineq107", `!d:A. d IN hyp_dart3 H ==>
        (((--(azim_mod d)) + ((#1.231 - (#0.152 * (y2_mod d + (y3_mod d + (y5_mod d + (y6_mod d - #8.0)))))) + ((#0.5 * (y1_mod d - #2.0)) + (#0.773 * (y4_mod d - #2.0))))) - #0.0) >= #0.0`;

  "ineq108", `!d:A. d IN hyp_dart3 H ==>
        ((((azim_mod d) - #1.2308) + (((#0.3639 * (y2_mod d + (y3_mod d + (y5_mod d + (y6_mod d - #8.0))))) - (#0.235 * (y1_mod d - #2.0))) - (#0.685 * (y4_mod d - #2.0)))) - #0.0) >= #0.0`;

  "ineq109", `!d:A. d IN hyp_dart3 H ==>
        (((--(sol_mod (face H d))) + (#0.5513 + ((#0.3232 * (y4_mod d + (y5_mod d + (y6_mod d - #6.0)))) - (#0.151 * (y1_mod d + (y2_mod d + (y3_mod d - #6.0))))))) - #0.0) >= #0.0`;

  "ineq110", `!d:A. d IN hyp_dart3 H ==>
        (((((sol_mod (face H d)) - #0.55125) - (#0.196 * (y4_mod d + (y5_mod d + (y6_mod d - #6.0))))) + (#0.38 * (y1_mod d + (y2_mod d + (y3_mod d - #6.0))))) - #0.0) >= #0.0`;

  "ineq111", `!d:A. d IN hyp_dart3 H ==>
        (((tau_mod (face H d)) + ((#0.001 - (#0.18 * (y1_mod d + (y2_mod d + (y3_mod d - #6.0))))) - (#0.125 * (y4_mod d + (y5_mod d + (y6_mod d - #6.0)))))) - #0.0) >= #0.0`;


  "ineq112", `!d:A. d IN hyp_dart3 H ==>
        ((((tau_mod (face H d)) - (#0.507 * (azim_mod d))) + #0.724) - #0.0) >= #0.0`;

  "ineq113", `!d:A. d IN hyp_dart3 H ==>
        ((((tau_mod (face H d)) - (#0.259 * (azim_mod d))) + #0.32) - #0.0) >= #0.0`;

  "ineq114", `!d:A. d IN hyp_dart3 H ==>
        (((tau_mod (face H d)) + ((#0.626 * (azim_mod d)) - #0.77)) - #0.0) >= #0.0`;

  "ineq115", `!d:A. d IN hyp_dart3 H ==>
        (#1.893 - (azim_mod d)) >= #0.0`;

  "ineq116", `!d:A. d IN hyp_dart3 H ==>
        ((azim_mod d) - #0.852) >= #0.0`;

  "ineq119", `!d:A. d IN hyp_dart4 H ==>
        ((((tau_mod (face H d)) - (#0.453 * (azim_mod d))) + #0.777) - #0.0) >= #0.0`;

  "ineq120", `!d:A. d IN hyp_dart4 H ==>
        (((tau_mod (face H d)) + ((#0.7573 * (azim_mod d)) - #1.433)) - #0.0) >= #0.0`;

  "ineq121", `!d:A. d IN hyp_dart4 H ==>
        (((tau_mod (face H d)) + ((#0.972 * (azim_mod d)) - #1.707)) - #0.0) >= #0.0`;

  "ineq122", `!d:A. d IN hyp_dart4 H ==>
        (((tau_mod (face H d)) + ((#4.72 * (azim_mod d)) - #6.248)) - #0.0) >= #0.0`;
];;


(*
let y1_def = `!d. d IN dart (H:(A)hypermap) ==> y1_mod d = yn_mod (node H d):real`;;
y1_def{(i3,i1,i2,j) in e_dart}: y1[i1,j] = yn[i1];


(* Rename terms and types *)
let s1 = inst [`:real^3#real^3`, aty] im_sum;;
let s2 = subst [`hypermap_of_fan (V,E)`, h_fan_hyp] s1;;
let s3 = subst [`azim_dart (V,E)`, azim_mod] s2;;
*)

(*************************************)

let SUM_ISOMORPHISM = 
prove(`!G H (g:B->A) (r:A->real). isomorphism g (G,H)
                            ==> (!d. d IN dart G ==> sum(node G d) (r o g) = sum(node H (g d)) r)`,

   REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `sum(node G d) (r o (g:B->A)) = sum(IMAGE g (node G d)) r` (fun th -> REWRITE_TAC[th]) THENL
     [
       MATCH_MP_TAC (GSYM SUM_IMAGE) THEN
         REPEAT STRIP_TAC THEN
         UNDISCH_TAC `isomorphism (g:B->A) (G,H)` THEN
         REWRITE_TAC[isomorphism; BIJ; INJ] THEN
         DISCH_THEN (MP_TAC o CONJUNCT1) THEN
         DISCH_THEN (MP_TAC o CONJUNCT1) THEN
         DISCH_THEN (MATCH_MP_TAC o CONJUNCT2) THEN
         ASM_REWRITE_TAC[] THEN
         CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN EXISTS_TAC `node G (d:B)` THEN ASM_SIMP_TAC[Hypermap.lemma_node_subset];
       ALL_TAC
     ] THEN
     MP_TAC (ISPECL [`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `d:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]));;

let ISO_NODE_INJ = 
prove(`!G H (g:B->A) n. isomorphism g (G,H) /\ n IN node_set G ==>
                           (!x y. x IN n /\ y IN n /\ g x = g y ==> x = y)`,

   REPEAT STRIP_TAC THEN
     UNDISCH_TAC `isomorphism (g:B->A) (G,H)` THEN
     REWRITE_TAC[isomorphism; BIJ; INJ] THEN
     DISCH_THEN (MP_TAC o CONJUNCT1) THEN DISCH_THEN (MP_TAC o CONJUNCT1) THEN
     DISCH_THEN (MATCH_MP_TAC o CONJUNCT2) THEN
     ASM_REWRITE_TAC[] THEN
     MP_TAC (ISPECL [`G:(B)hypermap`; `n:B->bool`] Hypermap.lemma_node_representation) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN
     CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN
     EXISTS_TAC `n:B->bool` THEN
     ASM_REWRITE_TAC[] THEN
     ASM_SIMP_TAC[Hypermap.lemma_node_subset]);;


let COMPONENTS_ISO_IMAGE = 
prove(`!G H (g:B->A). isomorphism g (G,H)
                             ==> (!d. d IN dart G ==>
                                    node H (g d) = IMAGE g (node G d) /\
                                    face H (g d) = IMAGE g (face G d))`,

   REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN DISCH_TAC THEN
     MP_TAC (ISPECL[`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `d:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
     ASM_REWRITE_TAC[] THEN
     SIMP_TAC[]);;

let HYPERMAP_MAPS_ISO_COMM = 
prove(`!G H (g:B->A). isomorphism g (G,H)
                             ==> (!d. d IN dart G ==>
                                    face_map H (g d) = g (face_map G d) /\
                                    node_map H (g d) = g (node_map G d))`,

   SIMP_TAC[isomorphism]);;

let HYPERMAP_INV_MAPS = 
prove(`!(G:(B)hypermap) d. d IN dart G
                                ==> (?k. inverse (face_map G) d = (face_map G POWER k) d)`,

   REPEAT STRIP_TAC THEN
     ABBREV_TAC `n = CARD (orbit_map (face_map G) (d:B))` THEN
     MP_TAC (ISPECL [`face_map G:B->B`; `dart G:B->bool`; `d:B`; `n:num`; `1`] Hypermap_and_fan.FINITE_ORBIT_MAP_INVERSE) THEN
     ASM_REWRITE_TAC[Hypermap.hypermap_lemma] THEN
     ANTS_TAC THENL
     [
       REWRITE_TAC[ARITH_RULE `1 <= n <=> 0 < n`] THEN
         EXPAND_TAC "n" THEN
         MATCH_MP_TAC Hypermap_and_fan.ORBIT_MAP_CARD_POS THEN
         EXISTS_TAC `dart G:B->bool` THEN
         REWRITE_TAC[Hypermap.hypermap_lemma];
       ALL_TAC
     ] THEN
     REWRITE_TAC[Hypermap.POWER_1] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
     EXISTS_TAC `n - 1` THEN
     REWRITE_TAC[]);;


let HYPERMAP_INV_MAPS_ISO_COMM = 
prove(`!G H (g:B->A). isomorphism g (G,H)
                         ==> (!d. d IN dart G ==>
                                inverse (face_map H) (g d) = g (inverse (face_map G) d) /\
                                inverse (node_map H) (g d) = g (inverse (node_map G) d))`,

   REWRITE_TAC[isomorphism] THEN REPEAT STRIP_TAC THEN
     MATCH_MP_TAC (GSYM COMM_INVERSE_LEMMA) THEN
     MAP_EVERY EXISTS_TAC [`dart G:B->bool`; `dart H:A->bool`] THEN
     ASM_SIMP_TAC[Hypermap.hypermap_lemma]);;

let HYPERMAP_INV_MAPS_ISO_IMAGE = 
prove(`!G H (g:B->A). isomorphism g (G,H)
                        ==> (!d. d IN dart G ==>
                               face H (inverse (face_map H) (g d)) = IMAGE g (face G (inverse (face_map G) d)) /\
                               node H (inverse (face_map H) (g d)) = IMAGE g (node G (inverse (face_map G) d)))`,

   REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
     ASM_SIMP_TAC[HYPERMAP_INV_MAPS_ISO_COMM] THEN
     ABBREV_TAC `x = inverse (face_map G) (d:B)` THEN
     SUBGOAL_THEN `x:B IN dart G` ASSUME_TAC THENL
     [
       EXPAND_TAC "x" THEN
         ASM_SIMP_TAC[Hypermap.lemma_dart_inveriant_under_inverse_maps];
       ALL_TAC
     ] THEN
     ASM_SIMP_TAC[COMPONENTS_ISO_IMAGE]);;




let HYPERMAP_MAPS_ISO_IMAGE = 
prove(`!G H (g:B->A). isomorphism g (G,H)
                                    ==> (!d. d IN dart G ==>
                                           face H (face_map H (g d)) = IMAGE g (face G (face_map G d)) /\
                                           face H (node_map H (g d)) = IMAGE g (face G (node_map G d)) /\
                                           node H (node_map H (g d)) = IMAGE g (node G (node_map G d)) /\
                                           node H (face_map H (g d)) = IMAGE g (node G (face_map G d)))`,

   REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
     ASM_SIMP_TAC[HYPERMAP_MAPS_ISO_COMM] THEN
     MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     REPEAT CONJ_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o SPEC `face_map G (d:B)`);
       FIRST_X_ASSUM (MP_TAC o SPEC `node_map G (d:B)`);
       FIRST_X_ASSUM (MP_TAC o SPEC `node_map G (d:B)`);
       FIRST_X_ASSUM (MP_TAC o SPEC `face_map G (d:B)`)
     ] THEN
     ASM_SIMP_TAC[Hypermap.lemma_dart_invariant]);;







let SUM_NODE_ISO = 
prove(`!G H (g:B->A) (r:A->real). isomorphism g (G,H)
                           ==> (!n. n IN node_set G ==> sum(IMAGE g n) r = sum n (r o g))`,

   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC SUM_IMAGE THEN
     MATCH_MP_TAC ISO_NODE_INJ THEN
     MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
     ASM_REWRITE_TAC[]);;


let CARD_NODE_ISO = 
prove(`!G H (g:B->A). isomorphism g (G,H)
                            ==> (!n. n IN node_set G ==> CARD (IMAGE g n) = CARD n)`,

   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC CARD_IMAGE_INJ THEN
     CONJ_TAC THENL
     [
       MATCH_MP_TAC ISO_NODE_INJ THEN
         MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     MP_TAC (ISPECL [`G:(B)hypermap`; `n:B->bool`] Hypermap.lemma_node_representation) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN
     ASM_REWRITE_TAC[Hypermap.NODE_FINITE]);;

let SUM_NODE_SUB = 
prove(`!(G:(B)hypermap) r1 r2 n. n IN node_set G
                           ==> sum n (\x. r1 x - r2 x) = sum n r1 - sum n r2`,

   REPEAT STRIP_TAC THEN
     MP_TAC (ISPECL [`G:(B)hypermap`; `n:B->bool`] Hypermap.lemma_node_representation) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     ASM_SIMP_TAC[Hypermap.NODE_FINITE; SUM_SUB]);;

let SUM_NODE_CONST = 
prove(`!(G:(B)hypermap) c n. n IN node_set G
                             ==> sum n (\x. c) = &(CARD n) * c`,

   REPEAT STRIP_TAC THEN
     MP_TAC (ISPECL [`G:(B)hypermap`; `n:B->bool`] Hypermap.lemma_node_representation) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     ASM_SIMP_TAC[Hypermap.NODE_FINITE; SUM_CONST]);;

let SUM_NODE_SUB_CONST = 
prove(`!(G:(B)hypermap) r c n. n IN node_set G
                                 ==> sum n (\x. r x - c) = sum n r - &(CARD n) * c`,

   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC_ALL SUM_NODE_CONST) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
     MP_TAC (SPECL [`G:(B)hypermap`; `r:B->real`; `\x:B. c:real`; `n:B->bool`] SUM_NODE_SUB) THEN
     ASM_REWRITE_TAC[]);;




let ISO_FACE_INJ = 
prove(`!G H (g:B->A) f. isomorphism g (G,H) /\ f IN face_set G ==>
                           (!x y. x IN f /\ y IN f /\ g x = g y ==> x = y)`,

   REPEAT STRIP_TAC THEN
     UNDISCH_TAC `isomorphism (g:B->A) (G,H)` THEN
     REWRITE_TAC[isomorphism; BIJ; INJ] THEN
     DISCH_THEN (MP_TAC o CONJUNCT1) THEN DISCH_THEN (MP_TAC o CONJUNCT1) THEN
     DISCH_THEN (MATCH_MP_TAC o CONJUNCT2) THEN
     ASM_REWRITE_TAC[] THEN
     MP_TAC (ISPECL [`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN
     CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN
     EXISTS_TAC `f:B->bool` THEN
     ASM_REWRITE_TAC[] THEN
     ASM_SIMP_TAC[Hypermap.lemma_face_subset]);;

let SUM_FACE_ISO = 
prove(`!G H (g:B->A) (r:A->real). isomorphism g (G,H)
                           ==> (!f. f IN face_set G ==> sum(IMAGE g f) r = sum f (r o g))`,

   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC SUM_IMAGE THEN
     MATCH_MP_TAC ISO_FACE_INJ THEN
     MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
     ASM_REWRITE_TAC[]);;


let CARD_FACE_ISO = 
prove(`!G H (g:B->A). isomorphism g (G,H)
                            ==> (!f. f IN face_set G ==> CARD (IMAGE g f) = CARD f)`,

   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC CARD_IMAGE_INJ THEN
     CONJ_TAC THENL
     [
       MATCH_MP_TAC ISO_FACE_INJ THEN
         MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN

     MP_TAC (ISPECL [`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN
     ASM_REWRITE_TAC[Hypermap.FACE_FINITE]);;

let SUM_FACE_SUB = 
prove(`!(G:(B)hypermap) r1 r2 f. f IN face_set G
                           ==> sum f (\x. r1 x - r2 x) = sum f r1 - sum f r2`,

   REPEAT STRIP_TAC THEN
     MP_TAC (ISPECL [`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     ASM_SIMP_TAC[Hypermap.FACE_FINITE; SUM_SUB]);;

let SUM_FACE_CONST = 
prove(`!(G:(B)hypermap) c f. f IN face_set G
                             ==> sum f (\x. c) = &(CARD f) * c`,

   REPEAT STRIP_TAC THEN
     MP_TAC (ISPECL [`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     ASM_SIMP_TAC[Hypermap.FACE_FINITE; SUM_CONST]);;

let SUM_FACE_SUB_CONST = 
prove(`!(G:(B)hypermap) r c f. f IN face_set G
                                 ==> sum f (\x. r x - c) = sum f r - &(CARD f) * c`,

   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC_ALL SUM_FACE_CONST) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
     MP_TAC (SPECL [`G:(B)hypermap`; `r:B->real`; `\x:B. c:real`; `f:B->bool`] SUM_FACE_SUB) THEN
     ASM_REWRITE_TAC[]);;



let SUM_NODE_LIST = 
prove(`!L (n:(A#A)list). good_list L /\ MEM n (list_of_nodes L) ==>
                            sum (set_of_list n) = list_sum n`,

   REPEAT STRIP_TAC THEN
     REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `f:(A#A)->real` THEN
     MP_TAC (ISPECL [`f:A#A->real`; `n:(A#A)list`] ALL_DISTINCT_SUM) THEN
     ANTS_TAC THENL
     [
       MATCH_MP_TAC ALL_DISTINCT_NODE THEN
         EXISTS_TAC `L:((A)list)list` THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     REWRITE_TAC[]);;


let SUM_NODE_LIST_ALL = 
prove(`!L (P:(A#A->bool)->((A#A->real)->real)->bool). good_list L /\ good_list_nodes L ==>
                            ((!n. n IN node_set (hypermap_of_list L) ==> P n (sum n))
                            <=> (!n. MEM n (list_of_nodes L) ==> P (set_of_list n) (list_sum n)))`,

   REWRITE_TAC[good_list_nodes] THEN
     REPEAT STRIP_TAC THEN
     ASM_REWRITE_TAC[IN_SET_OF_LIST; nodes_of_list] THEN
     EQ_TAC THEN REPEAT STRIP_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list n:A#A->bool`) THEN
         REWRITE_TAC[MEM_MAP] THEN
         ANTS_TAC THENL
         [
           EXISTS_TAC `n:(A#A)list` THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN

         MP_TAC (SPEC_ALL SUM_NODE_LIST) THEN
         ASM_REWRITE_TAC[] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]);
       ALL_TAC
     ] THEN

     POP_ASSUM MP_TAC THEN
     REWRITE_TAC[MEM_MAP] THEN
     STRIP_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
     ASM_REWRITE_TAC[] THEN
     MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_NODE_LIST) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]));;

let CARD_SET_OF_LIST_NODE = 
prove(`!(L:((A)list)list) n. good_list L /\ MEM n (list_of_nodes L)
                                    ==> CARD(set_of_list n) = LENGTH n`,

   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC CARD_SET_OF_LIST_ALL_DISTINCT THEN
     MATCH_MP_TAC ALL_DISTINCT_NODE THEN
     EXISTS_TAC `L:((A)list)list` THEN ASM_REWRITE_TAC[]);;




let SUM_FACE_LIST = 
prove(`!L (f:(A#A)list). good_list L /\ MEM f (list_of_faces L) ==>
                            sum (set_of_list f) = list_sum f`,

   REPEAT STRIP_TAC THEN
     REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `r:(A#A)->real` THEN
     MP_TAC (ISPECL [`r:A#A->real`; `f:(A#A)list`] ALL_DISTINCT_SUM) THEN
     ANTS_TAC THENL
     [
       MATCH_MP_TAC ALL_DISTINCT_FACE THEN
         EXISTS_TAC `L:((A)list)list` THEN
         ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     REWRITE_TAC[]);;


let SUM_FACE_LIST_ALL = 
prove(`!(L:((A)list)list) P. good_list L ==>
                            ((!f. f IN face_set (hypermap_of_list L) ==> P f (sum f))
                            <=> (!f. MEM f (list_of_faces L) ==> P (set_of_list f) (list_sum f)))`,

   REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[FACE_SET_EQ_LIST] THEN
     ASM_REWRITE_TAC[IN_SET_OF_LIST; faces_of_list] THEN
     EQ_TAC THEN REPEAT STRIP_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
         REWRITE_TAC[MEM_MAP] THEN
         ANTS_TAC THENL
         [
           EXISTS_TAC `f:(A#A)list` THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN

         MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
         ASM_REWRITE_TAC[] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]);
       ALL_TAC
     ] THEN

     POP_ASSUM MP_TAC THEN
     REWRITE_TAC[MEM_MAP] THEN
     STRIP_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
     ASM_REWRITE_TAC[] THEN
     MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]));;


let CARD_SET_OF_LIST_FACE = 
prove(`!(L:((A)list)list) f. good_list L /\ MEM f (list_of_faces L)
                                    ==> CARD(set_of_list f) = LENGTH f`,

   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC CARD_SET_OF_LIST_ALL_DISTINCT THEN
     MATCH_MP_TAC ALL_DISTINCT_FACE THEN
     EXISTS_TAC `L:((A)list)list` THEN ASM_REWRITE_TAC[]);;

let IN_DART3_IMP_IN_DART = UNDISCH_ALL (prove(`d:B IN hyp_dart3 G ==> d IN dart G`,
                                              SIMP_TAC[hyp_dart3; IN_ELIM_THM]));;
let IN_DART4_IMP_IN_DART = UNDISCH_ALL (prove(`d:B IN hyp_dart4 G ==> d IN dart G`,
                                              SIMP_TAC[hyp_dart4; IN_ELIM_THM]));;

let IN_FACE3_IMP_IN_FACE = UNDISCH_ALL (prove(`f IN hyp_face3 (G:(B)hypermap) ==> f IN face_set G`,
                                              SIMP_TAC[hyp_face3; IN_ELIM_THM]));;
let IN_FACE4_IMP_IN_FACE = UNDISCH_ALL (prove(`f IN hyp_face4 (G:(B)hypermap) ==> f IN face_set G`,
                                              SIMP_TAC[hyp_face4; IN_ELIM_THM]));;
let IN_FACE5_IMP_IN_FACE = UNDISCH_ALL (prove(`f IN hyp_face5 (G:(B)hypermap) ==> f IN face_set G`,
                                              SIMP_TAC[hyp_face5; IN_ELIM_THM]));;
let IN_FACE6_IMP_IN_FACE = UNDISCH_ALL (prove(`f IN hyp_face6 (G:(B)hypermap) ==> f IN face_set G`,
                                              SIMP_TAC[hyp_face6; IN_ELIM_THM]));;




let DART_LIST_ALL = 
prove(`!(L:((A)list)list) P. good_list L ==>
                            ((!d. d IN dart (hypermap_of_list L) ==> P d)
                        <=> (!d. MEM d (list_of_darts L) ==> P d))`,

   REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST; darts_of_list; IN_SET_OF_LIST]);;

let DART3_LIST_ALL = 
prove(`!(L:((A)list)list) P. good_list L ==>
                             ((!d. d IN hyp_dart3 (hypermap_of_list L) ==> P d)
                                <=> (!d. MEM d (list_of_darts3 L) ==> P d))`,

   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[LIST_OF_DARTS3; IN_SET_OF_LIST]);;


let DART4_LIST_ALL = 
prove(`!(L:((A)list)list) P. good_list L ==>
                             ((!d. d IN hyp_dart4 (hypermap_of_list L) ==> P d)
                                <=> (!d. MEM d (list_of_darts4 L) ==> P d))`,

   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[LIST_OF_DARTS4; IN_SET_OF_LIST]);;

let DARTX_LIST_ALL = 
prove(`!(L:((A)list)list) P. good_list L ==>
                             ((!d. d IN hyp_dartX (hypermap_of_list L) ==> P d)
                                <=> (!d. MEM d (list_of_dartsX L) ==> P d))`,

   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[LIST_OF_DARTS_X; IN_SET_OF_LIST]);;


let FACE3_LIST_ALL = 
prove(`!(L:((A)list)list) P. good_list L ==>
                             ((!f. f IN hyp_face3 (hypermap_of_list L) ==> P f (sum f))
                                <=> (!f. MEM f (list_of_faces3 L) ==> P (set_of_list f) (list_sum f)))`,

   REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[LIST_OF_FACES3] THEN
     ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM_MAP] THEN
     EQ_TAC THEN REPEAT STRIP_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
         ANTS_TAC THENL
         [
           EXISTS_TAC `f:(A#A)list` THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN

         MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
         ANTS_TAC THENL
         [
           ASM_REWRITE_TAC[] THEN
             POP_ASSUM MP_TAC THEN
             SIMP_TAC[list_of_faces3; MEM_FILTER];
           ALL_TAC
         ] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]);
       ALL_TAC
     ] THEN

     FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
     ASM_REWRITE_TAC[] THEN
     MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
     ANTS_TAC THENL
     [
       ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
         SIMP_TAC[list_of_faces3; MEM_FILTER];
       ALL_TAC
     ] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]));;


let FACE4_LIST_ALL = 
prove(`!(L:((A)list)list) P. good_list L ==>
                             ((!f. f IN hyp_face4 (hypermap_of_list L) ==> P f (sum f))
                                <=> (!f. MEM f (list_of_faces4 L) ==> P (set_of_list f) (list_sum f)))`,

   REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[LIST_OF_FACES4] THEN
     ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM_MAP] THEN
     EQ_TAC THEN REPEAT STRIP_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
         ANTS_TAC THENL
         [
           EXISTS_TAC `f:(A#A)list` THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN

         MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
         ANTS_TAC THENL
         [
           ASM_REWRITE_TAC[] THEN
             POP_ASSUM MP_TAC THEN
             SIMP_TAC[list_of_faces4; MEM_FILTER];
           ALL_TAC
         ] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]);
       ALL_TAC
     ] THEN

     FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
     ASM_REWRITE_TAC[] THEN
     MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
     ANTS_TAC THENL
     [
       ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
         SIMP_TAC[list_of_faces4; MEM_FILTER];
       ALL_TAC
     ] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]));;

let FACE5_LIST_ALL = 
prove(`!(L:((A)list)list) P. good_list L ==>
                             ((!f. f IN hyp_face5 (hypermap_of_list L) ==> P f (sum f))
                                <=> (!f. MEM f (list_of_faces5 L) ==> P (set_of_list f) (list_sum f)))`,

   REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[LIST_OF_FACES5] THEN
     ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM_MAP] THEN
     EQ_TAC THEN REPEAT STRIP_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
         ANTS_TAC THENL
         [
           EXISTS_TAC `f:(A#A)list` THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN

         MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
         ANTS_TAC THENL
         [
           ASM_REWRITE_TAC[] THEN
             POP_ASSUM MP_TAC THEN
             SIMP_TAC[list_of_faces5; MEM_FILTER];
           ALL_TAC
         ] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]);
       ALL_TAC
     ] THEN

     FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
     ASM_REWRITE_TAC[] THEN
     MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
     ANTS_TAC THENL
     [
       ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
         SIMP_TAC[list_of_faces5; MEM_FILTER];
       ALL_TAC
     ] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]));;

let FACE6_LIST_ALL = 
prove(`!(L:((A)list)list) P. good_list L ==>
                             ((!f. f IN hyp_face6 (hypermap_of_list L) ==> P f (sum f))
                                <=> (!f. MEM f (list_of_faces6 L) ==> P (set_of_list f) (list_sum f)))`,

   REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[LIST_OF_FACES6] THEN
     ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM_MAP] THEN
     EQ_TAC THEN REPEAT STRIP_TAC THENL
     [
       FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
         ANTS_TAC THENL
         [
           EXISTS_TAC `f:(A#A)list` THEN
             ASM_REWRITE_TAC[];
           ALL_TAC
         ] THEN

         MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
         ANTS_TAC THENL
         [
           ASM_REWRITE_TAC[] THEN
             POP_ASSUM MP_TAC THEN
             SIMP_TAC[list_of_faces6; MEM_FILTER];
           ALL_TAC
         ] THEN
         DISCH_THEN (fun th -> REWRITE_TAC[th]);
       ALL_TAC
     ] THEN

     FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
     ASM_REWRITE_TAC[] THEN
     MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
     ANTS_TAC THENL
     [
       ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
         SIMP_TAC[list_of_faces6; MEM_FILTER];
       ALL_TAC
     ] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[th]));;


let EDGE_LIST_ALL = 
prove(`!(L:((A)list)list) P. good_list L ==>
                            ((!e. e IN hyp_edge_pairs (hypermap_of_list L) ==> P e)
                       <=> (!e. MEM e (list_of_edges L) ==> P e))`,

   REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[LIST_OF_EDGES; IN_SET_OF_LIST]);;

let SUB_CONST_o = 
prove(`!f (c:real) (g:B->A). (\x. f x - c) o g  = (\x. (f o g) x - c)`,

   REWRITE_TAC[FUN_EQ_THM; o_THM]);;

(*******************************)


let in_all_rewrites =
[
  SUM_NODE_LIST_ALL;
  SUM_FACE_LIST_ALL;
  EDGE_LIST_ALL;
  DART_LIST_ALL;
  DART3_LIST_ALL;
  DART4_LIST_ALL;
  DARTX_LIST_ALL;
  FACE3_LIST_ALL;
  FACE4_LIST_ALL;
  FACE5_LIST_ALL;
  FACE6_LIST_ALL;
];;



let table_set_hyp =
  let table = Hashtbl.create 10 in
  let _ = map (uncurry (Hashtbl.add table))
      [
        `hyp_dart3 (G:(B)hypermap)`, IN_DART3_IMP_IN_DART;
        `hyp_dart4 (G:(B)hypermap)`, IN_DART4_IMP_IN_DART;
        `hyp_face3 (G:(B)hypermap)`, IN_FACE3_IMP_IN_FACE;
        `hyp_face4 (G:(B)hypermap)`, IN_FACE4_IMP_IN_FACE;
        `hyp_face5 (G:(B)hypermap)`, IN_FACE5_IMP_IN_FACE;
        `hyp_face6 (G:(B)hypermap)`, IN_FACE6_IMP_IN_FACE;
      ] in
    table;;



(*************************************)


let iso_dart_trans = 
prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
                             ((!d. d IN dart H ==> P d) ==> (!d. d IN dart G ==> P (g d)))`,

   REWRITE_TAC[isomorphism; BIJ; SURJ] THEN
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `d:B`) THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `d:B`) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `(g:B->A) d`) THEN
     ASM_SIMP_TAC[]);;

let iso_dart_in = 
prove(`!(g:B->A) H G d. isomorphism g (G,H) /\ d IN dart G ==>
                          g d IN dart H`,

   REWRITE_TAC[isomorphism; BIJ; SURJ; INJ] THEN
     REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[]);;


let iso_card_eq = 
prove(`!(g:B->A) H G s. isomorphism g (G,H) /\ s SUBSET dart G
                          ==> CARD (IMAGE g s) = CARD s`,

   REWRITE_TAC[isomorphism; BIJ; INJ] THEN
     REPEAT STRIP_TAC THEN
     MATCH_MP_TAC CARD_IMAGE_INJ THEN
     CONJ_TAC THENL
     [
       REPEAT STRIP_TAC THEN
         FIRST_X_ASSUM MATCH_MP_TAC THEN
         ASM_REWRITE_TAC[] THEN
         CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN EXISTS_TAC `s:B->bool` THEN ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     MATCH_MP_TAC FINITE_SUBSET THEN
     EXISTS_TAC `dart G:B->bool` THEN
     ASM_REWRITE_TAC[Hypermap.hypermap_lemma]);;

let iso_face_card = 
prove(`!(g:B->A) H G d. isomorphism g (G,H) /\ d IN dart G
                                  ==> CARD (face H (g d)) = CARD (face G d)`,

   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (MP_TAC o SPEC `d:B`) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     ASM_REWRITE_TAC[] THEN
     MATCH_MP_TAC iso_card_eq THEN
     MAP_EVERY EXISTS_TAC [`H:(A)hypermap`; `G:(B)hypermap`] THEN
     ASM_SIMP_TAC[Hypermap.lemma_face_subset]);;

let iso_dart3_trans = 
prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
                ((!d. d IN hyp_dart3 H ==> P d) ==> (!d. d IN hyp_dart3 G ==> P (g d)))`,

   REWRITE_TAC[hyp_dart3; IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN
     MP_TAC (SPEC_ALL iso_dart_in) THEN
     ASM_SIMP_TAC[iso_face_card]);;


let iso_dart4_trans = 
prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
                ((!d. d IN hyp_dart4 H ==> P d) ==> (!d. d IN hyp_dart4 G ==> P (g d)))`,

   REWRITE_TAC[hyp_dart4; IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN
     MP_TAC (SPEC_ALL iso_dart_in) THEN
     ASM_SIMP_TAC[iso_face_card]);;


let iso_dartX_trans = 
prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
                ((!d. d IN hyp_dartX H ==> P d) ==> (!d. d IN hyp_dartX G ==> P (g d)))`,

   REWRITE_TAC[hyp_dartX; IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN
     MP_TAC (SPEC_ALL iso_dart_in) THEN
     ASM_SIMP_TAC[iso_face_card]);;



let iso_edge_pairs_trans = 
prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
                  ((!e. e IN hyp_edge_pairs H ==> P e) ==> (!e. e IN hyp_edge_pairs G ==> P (g (FST e), g (SND e))))`,

   REWRITE_TAC[isomorphism; BIJ; SURJ; hyp_edge_pairs; IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     ASM_REWRITE_TAC[] THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN
     EXISTS_TAC `(g:B->A) x` THEN
     ASM_SIMP_TAC[]);;



let iso_node_trans = 
prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
                             ((!n. n IN node_set H ==> P n) ==> (!n. n IN node_set G ==> P (IMAGE g n)))`,

   REPEAT STRIP_TAC THEN
     POP_ASSUM (MP_TAC o MATCH_MP Hypermap.lemma_node_representation) THEN
     STRIP_TAC THEN
     MP_TAC (ISPECL [`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `x:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN
     REWRITE_TAC[GSYM Hypermap.lemma_in_node_set] THEN
     MATCH_MP_TAC iso_dart_in THEN
     EXISTS_TAC `G:(B)hypermap` THEN
     ASM_REWRITE_TAC[]);;


let iso_face_trans = 
prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
                             ((!f. f IN face_set H ==> P f) ==> (!f. f IN face_set G ==> P (IMAGE g f)))`,

   REPEAT STRIP_TAC THEN
     POP_ASSUM (MP_TAC o MATCH_MP Hypermap.lemma_face_representation) THEN
     STRIP_TAC THEN
     MP_TAC (ISPECL [`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `x:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN
     REWRITE_TAC[GSYM Hypermap.lemma_in_face_set] THEN
     MATCH_MP_TAC iso_dart_in THEN
     EXISTS_TAC `G:(B)hypermap` THEN
     ASM_REWRITE_TAC[]);;

let iso_face3_trans = 
prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
              ((!f. f IN hyp_face3 H ==> P f) ==> (!f. f IN hyp_face3 G ==> P (IMAGE g f)))`,

   REWRITE_TAC[hyp_face3; IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN
     POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
     MP_TAC (SPECL[`g:B->A`; `H:(A)hypermap`; `G:(B)hypermap`] iso_face_trans) THEN
     ASM_REWRITE_TAC[] THEN
     REPEAT DISCH_TAC THEN
     CONJ_TAC THENL
     [
       REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
         SPEC_TAC (`f:B->bool`, `f:B->bool`) THEN
         FIRST_X_ASSUM MATCH_MP_TAC THEN
         SIMP_TAC[];
       ALL_TAC
     ] THEN

     MP_TAC (ISPECL[`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     UNDISCH_TAC `CARD (f:B->bool) = 3` THEN
     DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
     ASM_REWRITE_TAC[] THEN

     MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> ASM_SIMP_TAC[GSYM th]) THEN
     MATCH_MP_TAC iso_face_card THEN
     ASM_REWRITE_TAC[]);;

let iso_face4_trans = 
prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
              ((!f. f IN hyp_face4 H ==> P f) ==> (!f. f IN hyp_face4 G ==> P (IMAGE g f)))`,

   REWRITE_TAC[hyp_face4; IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN
     POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
     MP_TAC (SPECL[`g:B->A`; `H:(A)hypermap`; `G:(B)hypermap`] iso_face_trans) THEN
     ASM_REWRITE_TAC[] THEN
     REPEAT DISCH_TAC THEN
     CONJ_TAC THENL
     [
       REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
         SPEC_TAC (`f:B->bool`, `f:B->bool`) THEN
         FIRST_X_ASSUM MATCH_MP_TAC THEN
         SIMP_TAC[];
       ALL_TAC
     ] THEN

     MP_TAC (ISPECL[`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     UNDISCH_TAC `CARD (f:B->bool) = 4` THEN
     DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
     ASM_REWRITE_TAC[] THEN

     MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> ASM_SIMP_TAC[GSYM th]) THEN
     MATCH_MP_TAC iso_face_card THEN
     ASM_REWRITE_TAC[]);;

let iso_face5_trans = 
prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
              ((!f. f IN hyp_face5 H ==> P f) ==> (!f. f IN hyp_face5 G ==> P (IMAGE g f)))`,

   REWRITE_TAC[hyp_face5; IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN
     POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
     MP_TAC (SPECL[`g:B->A`; `H:(A)hypermap`; `G:(B)hypermap`] iso_face_trans) THEN
     ASM_REWRITE_TAC[] THEN
     REPEAT DISCH_TAC THEN
     CONJ_TAC THENL
     [
       REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
         SPEC_TAC (`f:B->bool`, `f:B->bool`) THEN
         FIRST_X_ASSUM MATCH_MP_TAC THEN
         SIMP_TAC[];
       ALL_TAC
     ] THEN

     MP_TAC (ISPECL[`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     UNDISCH_TAC `CARD (f:B->bool) = 5` THEN
     DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
     ASM_REWRITE_TAC[] THEN

     MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> ASM_SIMP_TAC[GSYM th]) THEN
     MATCH_MP_TAC iso_face_card THEN
     ASM_REWRITE_TAC[]);;

let iso_face6_trans = 
prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
              ((!f. f IN hyp_face6 H ==> P f) ==> (!f. f IN hyp_face6 G ==> P (IMAGE g f)))`,

   REWRITE_TAC[hyp_face6; IN_ELIM_THM] THEN
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN
     POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
     MP_TAC (SPECL[`g:B->A`; `H:(A)hypermap`; `G:(B)hypermap`] iso_face_trans) THEN
     ASM_REWRITE_TAC[] THEN
     REPEAT DISCH_TAC THEN
     CONJ_TAC THENL
     [
       REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
         SPEC_TAC (`f:B->bool`, `f:B->bool`) THEN
         FIRST_X_ASSUM MATCH_MP_TAC THEN
         SIMP_TAC[];
       ALL_TAC
     ] THEN

     MP_TAC (ISPECL[`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     UNDISCH_TAC `CARD (f:B->bool) = 6` THEN
     DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
     ASM_REWRITE_TAC[] THEN

     MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> ASM_SIMP_TAC[GSYM th]) THEN
     MATCH_MP_TAC iso_face_card THEN
     ASM_REWRITE_TAC[]);;



let iso_trans_table =
  let table = Hashtbl.create 10 in
  let _ = map (uncurry (Hashtbl.add table))
    [
      `dart H:A->bool`, iso_dart_trans;
      `node_set (H:(A)hypermap)`, iso_node_trans;
      `face_set (H:(A)hypermap)`, iso_face_trans;
      `hyp_edge_pairs (H:(A)hypermap)`, iso_edge_pairs_trans;
      `hyp_dart3 (H:(A)hypermap)`, iso_dart3_trans;
      `hyp_dart4 (H:(A)hypermap)`, iso_dart4_trans;
      `hyp_dartX (H:(A)hypermap)`, iso_dartX_trans;
      `hyp_face3 (H:(A)hypermap)`, iso_face3_trans;
      `hyp_face4 (H:(A)hypermap)`, iso_face4_trans;
      `hyp_face5 (H:(A)hypermap)`, iso_face5_trans;
      `hyp_face6 (H:(A)hypermap)`, iso_face6_trans;
    ] in
    table;;


(**************************)



let gen_iso_thm ineq =
  let x_tm, tm = dest_forall ineq in
  let set, p_tm' = dest_binary "==>" tm in
  let set_th = Hashtbl.find iso_trans_table (rand set) in
  let p_tm = mk_abs (x_tm, p_tm') in
  let p_var = mk_var ("P", type_of (rand set)) in
  let th3 = (SPEC_ALL (REWRITE_RULE[IMP_IMP] set_th)) in
    BETA_RULE (INST[p_tm, p_var] th3);;






let gen_general_ineq ineq =
  let iso_th = gen_iso_thm ineq in
    (* General rewrites before specifying hypermaps *)
  let th0 = UNDISCH_ALL (REWRITE_RULE[GSYM IMP_IMP] iso_th) in
  let gen_var, rtm = dest_forall(concl th0) in
  let ants = lhand rtm in
  let set = rand ants in
  let th1 = UNDISCH_ALL (SPEC_ALL th0) in

  let th_rule th = UNDISCH_ALL (SPEC_ALL (UNDISCH_ALL (SPEC_ALL th))) in

  let ths = [
    th_rule SUM_NODE_ISO;
    th_rule CARD_NODE_ISO;
    th_rule SUM_FACE_ISO;
    th_rule CARD_FACE_ISO;
    th_rule COMPONENTS_ISO_IMAGE;
    th_rule HYPERMAP_MAPS_ISO_IMAGE;
    th_rule HYPERMAP_INV_MAPS_ISO_IMAGE;
    th_rule HYPERMAP_MAPS_ISO_COMM;
    th_rule HYPERMAP_INV_MAPS_ISO_COMM;
    SUB_CONST_o; ETA_AX;
    th_rule SUM_FACE_SUB_CONST;
  ] in

  let th2' = REWRITE_RULE ths th1 in
  let th2 =
    if (Hashtbl.mem table_set_hyp set) then
      PROVE_HYP (Hashtbl.find table_set_hyp set) th2'
    else
      th2' in
  let th3 = GEN gen_var (DISCH ants th2) in

  let s0 = th3 in

  (* G -> hypermap_of_list (L:((num)list)list) *)
  (* Instantiate correct types *)
  let s1 = INST_TYPE [`:real^3#real^3`, aty; `:num#num`, bty] s0 in
  let s2 = INST[`hypermap_of_list (L:((num)list)list)`, `G:(num#num)hypermap`] s1 in

  let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty] o SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP]) in

  let ths = map th_rule in_all_rewrites in
  let s3 = REWRITE_RULE ths s2 in

  let gen_var2, rtm = dest_forall(concl s3) in
  let ants2 = lhand rtm in

  let s4 = UNDISCH_ALL (SPEC_ALL s3) in

  let ths =
    [
      th_rule CARD_SET_OF_LIST_FACE;
      th_rule CARD_SET_OF_LIST_NODE;
    ] in

  let s5 = REWRITE_RULE ths s4 in
  let s6 = GEN gen_var2 (DISCH ants2 s5) in

  (* Deal with basic variables *)
  let s7 = INST var_list s6 in
  let s8 = INST[`ESTD V`, `E:(real^3->bool)->bool`] s7 in
  let s9 = REWRITE_RULE list_var_rewrites s8 in
  let r0 = s9 in

  (* Basic rewrites *)

  let ths =
    [
      UNDISCH_ALL (INST_TYPE [`:num`, aty] (SPEC_ALL COMPONENTS_HYPERMAP_OF_LIST));
    ] in
  let r1 = REWRITE_RULE ths r0 in

  (* Further rewrites *)
  let r2 = REWRITE_RULE[darts_of_list; IN_SET_OF_LIST; ALL_MEM] r1 in
    r2;;



(***********************)


(*

let get_ineq str = Hashtbl.find constraints str;;



let th = gen_general_ineq (get_ineq "ineq122");;
let th = gen_general_ineq (get_ineq "sol_sum3");;
let th = gen_general_ineq (get_ineq "tau_sum");;
let th = gen_general_ineq (get_ineq "edge_sym");;
let th = gen_general_ineq (get_ineq "ln_def");;
let th = gen_general_ineq (get_ineq "y1_def");;
let th = gen_general_ineq (get_ineq "y2_def");;
let th = gen_general_ineq (get_ineq "y3_def");;
let th = gen_general_ineq (get_ineq "y4_def");;
let th = gen_general_ineq (get_ineq "y5_def");;
let th = gen_general_ineq (get_ineq "y6_def");;
let th = gen_general_ineq (get_ineq "y8_def");;
let th = gen_general_ineq (get_ineq "y9_def");;
let th = gen_general_ineq (get_ineq "RHB");;



let test_list = ref [];;

let iter_f name ineq =
  try
    test_list := gen_general_ineq ineq :: !test_list
  with x ->
    print_string ("problems: "^name^"; ");;


Hashtbl.iter iter_f constraints;;




(********************************)

let ineq = get_ineq "tau_sum3";;

let iso_th = gen_iso_thm ineq;;
    (* General rewrites before specifying hypermaps *)
let th0 = UNDISCH_ALL (REWRITE_RULE[GSYM IMP_IMP] iso_th);;
let gen_var, rtm = dest_forall(concl th0);;
let ants = lhand rtm;;
let set = rand ants;;
let th1 = UNDISCH_ALL (SPEC_ALL th0);;

let th_rule th = UNDISCH_ALL (SPEC_ALL (UNDISCH_ALL (SPEC_ALL th)));;

let ths = [
    th_rule SUM_NODE_ISO;
    th_rule CARD_NODE_ISO;
    th_rule SUM_FACE_ISO;
    th_rule CARD_FACE_ISO;
    th_rule COMPONENTS_ISO_IMAGE;
    th_rule HYPERMAP_MAPS_ISO_IMAGE;
    th_rule HYPERMAP_INV_MAPS_ISO_IMAGE;
    th_rule HYPERMAP_MAPS_ISO_COMM;
    th_rule HYPERMAP_INV_MAPS_ISO_COMM;
    SUB_CONST_o; ETA_AX;
    th_rule SUM_FACE_SUB_CONST;
];;

let th2' = REWRITE_RULE ths th1;;
let th2 =
  if (Hashtbl.mem table_set_hyp set) then
    PROVE_HYP (Hashtbl.find table_set_hyp set) th2'
  else
    th2';;


  let th3 = GEN gen_var (DISCH ants th2);;

  let s0 = th3;;

  (* G -> hypermap_of_list (L:((num)list)list) *)
  (* Instantiate correct types *)
  let s1 = INST_TYPE [`:real^3#real^3`, aty; `:num#num`, bty] s0;;
  let s2 = INST[`hypermap_of_list (L:((num)list)list)`, `G:(num#num)hypermap`] s1;;

  let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty] o SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP]);;

  let ths = map th_rule in_all_rewrites;;

  let s3 = REWRITE_RULE ths s2;;

  let gen_var2, rtm = dest_forall(concl s3);;
  let ants2 = lhand rtm;;

  let s4 = UNDISCH_ALL (SPEC_ALL s3);;

  let ths =
    [
      th_rule CARD_SET_OF_LIST_FACE;
      th_rule CARD_SET_OF_LIST_NODE;
    ];;

  let s5 = REWRITE_RULE ths s4;;
  let s6 = GEN gen_var2 (DISCH ants2 s5);;

  (* Deal with basic variables *)
  let s7 = INST var_list s6;;
  let s8 = INST[`ESTD V`, `E:(real^3->bool)->bool`] s7;;
  let s9 = REWRITE_RULE list_var_rewrites s8;;
  let r0 = s9;;

  (* Basic rewrites *)

  let ths =
    [
      UNDISCH_ALL (INST_TYPE [`:num`, aty] (SPEC_ALL COMPONENTS_HYPERMAP_OF_LIST));
    ];;
  let r1 = REWRITE_RULE ths r0;;

  (* Further rewrites *)
  let r2 = REWRITE_RULE[darts_of_list; IN_SET_OF_LIST; ALL_MEM] r1
    r2;;



*)

(*********************************************************)

(* Integral approximation of inequalities and equalities *)

let mk_decimal (n,m) =
  let tm = mk_comb(mk_comb(`DECIMAL`, mk_numeral (abs_num n)), mk_numeral m) in
    if (n </ Int 0) then mk_comb(neg_op_real, tm) else tm;;


(*
Given a rational number term `r` and a natural number k,
returns a pair of theorems:
|- low <= r, |- r <= high,
with decimal low and high such that
|low - r| <= 10^(-k) and |high - r| <= 10^(-k)
*)
let real_rat_approx tm precision =
  let n = rat_of_term tm in
  let m = Int 10 **/ (Int precision) in
  let n1 = n */ m in
  let low, high = floor_num n1, ceiling_num n1 in
  let l_tm, h_tm =
    if precision = 0 then
      term_of_rat low, term_of_rat high
    else
      mk_decimal (low, m), mk_decimal (high, m) in
  let l_th = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op_real l_tm tm)) in
  let h_th = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op_real tm h_tm)) in
    l_th, h_th;;



(* Split a sum into two parts: with and without free variables *)

let sum_th0 = REAL_ARITH `x = x + &0 + &0` and
    sum_th1 = REAL_ARITH `(x + y) + b + c = y + (x + b) + c:real` and
    sum_th2 = REAL_ARITH `(x + y) + b + c = y + b + (x + c):real` and
    sum_th1' = REAL_ARITH `x + b + c = (x + b) + c:real` and
    sum_th2' = REAL_ARITH `x + b + c = b + (x + c):real`;;


let c_var_real = `c:real`;;


let split_sum_conv tm =
  let rec split_sum_raw_conv tm =
    let xy_tm, bc_tm = dest_binop add_op_real tm in
    let b_tm, c_tm = dest_binop add_op_real bc_tm in
      if (is_binop add_op_real xy_tm) then
        let x_tm, y_tm = dest_binop add_op_real xy_tm in
        let inst_th = INST[x_tm, x_var_real; y_tm, y_var_real; b_tm, b_var_real; c_tm, c_var_real] in
        let th1 = if (frees x_tm <> []) then inst_th sum_th1 else inst_th sum_th2 in
        let th2 = split_sum_raw_conv (rand(concl th1)) in
          TRANS th1 th2
      else
        let inst_th = INST[xy_tm, x_var_real; b_tm, b_var_real; c_tm, c_var_real] in
          if (frees xy_tm <> []) then inst_th sum_th1' else inst_th sum_th2' in

  let th0 = INST[tm, x_var_real] sum_th0 in
  let th1 = split_sum_raw_conv (rand(concl th0)) in
    TRANS th0 th1;;



let rearrange_mul_conv tm =
  let rec dest_mul tm =
    if (is_binop mul_op_real tm) then
      let lhs, rhs = dest_binop mul_op_real tm in
      let cs, vars = dest_mul rhs in
        if (frees lhs = []) then
          lhs::cs, vars
        else
          cs, lhs::vars
    else
      if (frees tm = []) then
        [tm], []
      else
        [], [tm] in
  let mk_mul list =
    if (list = []) then failwith "rearrange_mul: empty list"
    else itlist (fun l r -> mk_binop mul_op_real l r) (tl list) (hd list) in

  let cs, vars = dest_mul tm in
  let cs_mul, vars_mul = mk_mul cs, mk_mul vars in
  let t = mk_eq(tm, mk_binop mul_op_real cs_mul vars_mul) in
    EQT_ELIM (REWRITE_CONV[REAL_MUL_AC] t);;



let le_add_th = REAL_ARITH `x + y <= b + c <=> x - b <= c - y:real`;;

(* Moves everything with free variables on the left and performs basic reductions *)
let ineq_rewrite_conv = REWRITE_CONV[real_ge; real_div; DECIMAL] THENC
  LAND_CONV REAL_POLY_CONV THENC RAND_CONV REAL_POLY_CONV THENC
  LAND_CONV split_sum_conv THENC RAND_CONV split_sum_conv THENC
  ONCE_REWRITE_CONV[le_add_th] THENC
  LAND_CONV REAL_POLY_CONV THENC RAND_CONV REAL_POLY_CONV THENC
  REWRITE_CONV[GSYM real_div] THENC
  ONCE_DEPTH_CONV rearrange_mul_conv;;


(* Approximation *)

let le_mul1_th = REAL_ARITH `!x. &1 * x <= x`;;
let ge_mul1_th = REAL_ARITH `!x. x <= &1 * x`;;
let INTERVAL_LO = 
prove(`interval_arith x (a,b) ==> a <= x`,
 SIMP_TAC[interval_arith]);;
let INTERVAL_HI = 
prove(`interval_arith x (a,b) ==> x <= b`,
 SIMP_TAC[interval_arith]);;
let rec low_approx tm precision =
  let low_approx1 tm precision =
    if (is_binop mul_op_real tm && frees tm <> []) then
      let c, var = dest_binop mul_op_real tm in
      let interval_th = approx_interval (create_interval c) precision in
      let l_th = MATCH_MP INTERVAL_LO interval_th in
      let a, b = dest_binop le_op_real (concl l_th) in
        (PROVE_HYP l_th o UNDISCH_ALL o REWRITE_RULE[GSYM IMP_IMP] o SPECL[a; b; var]) REAL_LE_RMUL
    else
      if (frees tm = []) then
        MATCH_MP INTERVAL_LO (approx_interval (create_interval tm) precision)
      else
        SPEC tm le_mul1_th in

  if (is_binop add_op_real tm && frees tm <> []) then
    let lhs, rhs = dest_binop add_op_real tm in
    let l_th = low_approx1 lhs precision in
    let r_th = low_approx rhs precision in
      MATCH_MP REAL_LE_ADD2 (CONJ l_th r_th)
  else
    low_approx1 tm precision;;


let rec hi_approx tm precision =
  let hi_approx1 tm precision =
    if (is_binop mul_op_real tm && frees tm <> []) then
      let c, var = dest_binop mul_op_real tm in
      let interval_th = approx_interval (create_interval c) precision in
      let h_th = MATCH_MP INTERVAL_HI interval_th in
      let a, b = dest_binop le_op_real (concl h_th) in
        (PROVE_HYP h_th o UNDISCH_ALL o REWRITE_RULE[GSYM IMP_IMP] o SPECL[a; b; var]) REAL_LE_RMUL
    else
      if (frees tm = []) then
        MATCH_MP INTERVAL_HI (approx_interval (create_interval tm) precision)
      else
        SPEC tm ge_mul1_th in

  if (is_binop add_op_real tm && frees tm <> []) then
    let lhs, rhs = dest_binop add_op_real tm in
    let l_th = hi_approx1 lhs precision in
    let r_th = hi_approx rhs precision in
      MATCH_MP REAL_LE_ADD2 (CONJ l_th r_th)
  else
    hi_approx1 tm precision;;



let approx_le_ineq precision tm =
  let lhs, rhs = dest_binop le_op_real tm in
  let lhs_th = low_approx lhs precision in
  let rhs_th = hi_approx rhs precision in
  let ll, lr = dest_binop le_op_real (concl lhs_th) in
  let rl, rr = dest_binop le_op_real (concl rhs_th) in

  let th0 = ASSUME tm in
  let th1 = SPECL[ll; lr; rhs] REAL_LE_TRANS in
  let th2 = SPECL[ll; rhs; rr] REAL_LE_TRANS in
  let s1 = MATCH_MP th1 (CONJ lhs_th th0) in
    MATCH_MP th2 (CONJ s1 rhs_th);;


let integer_approx_le_ineq precision ineq =
  let lhs, rhs = dest_binop le_op_real ineq in
  let m = (Int 10 **/ Int precision) in
  let m_num, m_real = mk_numeral m, term_of_rat m in
  let m_pos = SPEC m_num REAL_POS in
  let mul_th = SPECL[m_real; lhs; rhs] REAL_LE_LMUL in
  let th0 = MATCH_MP mul_th (CONJ m_pos (ASSUME ineq)) in
  let th1 = (CONV_RULE ineq_rewrite_conv) th0 in
  let approx = approx_le_ineq 0 (concl th1) in
    PROVE_HYP th1 approx;;


let create_approximations precision_list ineq =
  let ineq_th = ineq_rewrite_conv ineq in
  let rhs = rand(concl ineq_th) in
  let th0 = CONV_RULE (LAND_CONV (REWRITE_CONV[DECIMAL] THENC REAL_POLY_CONV))
    (approx_le_ineq 8 rhs) in

  let int_approx p =
    let th1 = integer_approx_le_ineq p (concl th0) in
    let th2 = PROVE_HYP th0 th1 in
    let th3 = DISCH rhs th2 in
      REWRITE_RULE[GSYM ineq_th] th3 in

    map int_approx precision_list;;

(**********************************)


(*
let tm = `(&34/ &13 + pi/sol0)* x + &2 + -- &14 / &3 * z <= pi + rho218 + z * sol0 - u / &1000`;;
create_approximations [3;4;5] tm;;
*)


(*************************)

(* Additional step for generalizing hypotheses *)


let LIST_SUM_LMUL = 
prove(`!(f:A->real) c n. list_sum n (\x. c * f x) = c * list_sum n f`,

   GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[list_sum; ITLIST; REAL_MUL_RZERO] THEN
     ASM_REWRITE_TAC[GSYM list_sum; REAL_ADD_LDISTRIB]);;

let le_hyp_gen = 
prove(`!f y. (!x. &0 <= f x) ==> &0 <= f y`,
 SIMP_TAC[]);;
let le_list_sum_hyp_gen = 
prove(`!(f:A->real) n. (!x. &0 <= f x) ==> &0 <= list_sum n f`,

   REPEAT STRIP_TAC THEN
     REWRITE_TAC[list_sum] THEN
     SPEC_TAC (`n:(A)list`, `n:(A)list`) THEN
     LIST_INDUCT_TAC THEN REWRITE_TAC[ITLIST; REAL_LE_REFL] THEN
     MATCH_MP_TAC REAL_LE_ADD THEN
     ASM_REWRITE_TAC[]);;


let generalize_hyp th =
  let gen_hyp = fun tm ->
    let fn, arg = dest_comb (rand tm) in
      if (is_comb fn && is_const (rator fn) && (fst o dest_const o rator) fn = "list_sum") then
        let f, n = arg, rand fn in
          UNDISCH_ALL (ISPECL[f; n] le_list_sum_hyp_gen)
      else
        UNDISCH_ALL (ISPECL[fn; arg] le_hyp_gen) in

  let hyp_ths = map gen_hyp (hyp th) in
    itlist PROVE_HYP hyp_ths th;;


(*
let tm = `list_sum n (\x. s x * r) + &1 / &3 * (azim_dart (V,E) o g) x <= pi`;;
let ths = create_approximations [3] tm;;
map generalize_hyp ths;;
*)


(*******************************)


let generate_ineqs precision_list ineq =

  let create_approxs original_th precision_list =
    let var, ineq = (dest_abs o rand o rator o concl) original_th in
    let final_step = fun approx_th ->
      let p_tm', q_tm' = dest_imp (concl approx_th) in
      let p_tm, q_tm = mk_abs(var, p_tm'), mk_abs(var, q_tm') in
      let list_tm = (rand o concl) original_th in
      let mono_th = BETA_RULE (ISPECL[p_tm; q_tm; list_tm] (GEN_ALL MONO_ALL)) in
      let s1 = MATCH_MP mono_th (GEN var approx_th) in
        MATCH_MP s1 original_th in

    let approx_ths0 = map generalize_hyp (create_approximations precision_list ineq) in
    let approx_ths1 = map (itlist PROVE_HYP list_var_pos) approx_ths0 in
    let approx_ths = map (REWRITE_RULE[GSYM LIST_SUM_LMUL]) approx_ths1 in
      map final_step approx_ths in


  let ineq_th = gen_general_ineq ineq in
  let ineq = (snd o dest_abs o rand o rator o concl) ineq_th in
    if (is_eq ineq) then
      let eq_th = REWRITE_RULE[GSYM REAL_LE_ANTISYM; GSYM AND_ALL] ineq_th in
      let ths1 = create_approxs (CONJUNCT1 eq_th) precision_list in
      let ths2 = create_approxs (CONJUNCT2 eq_th) precision_list in
        ths1, ths2
    else
      create_approxs ineq_th precision_list, [];;




(*********************************************************************)

(* Table containing all inequalities *)
let ineq_table = Array.init 6 (fun i -> Hashtbl.create 10);;
let ineq_test_table = Array.init 6 (fun i -> Hashtbl.create 10);;



let DECIMAL_INT = 
prove(`!n. DECIMAL n 1 = &n`,
 REWRITE_TAC[DECIMAL; REAL_DIV_1]);;

let add_everything_to_table table =
  let add_approximations_to_table = fun name ineq ->
    let approxs', neg_approxs' = generate_ineqs [3;4;5] ineq in
    let approxs = zip (3--5) approxs' in
    let neg_approxs = if (neg_approxs' = []) then [] else zip (3--5) neg_approxs' in
    let r = CONV_RULE (REWRITE_CONV[DECIMAL_INT] THENC DEPTH_CONV Arith_hash.NUMERAL_TO_NUM_CONV) in
    let _ = map (fun (i, t) -> Hashtbl.add (ineq_test_table.(i)) name t;
                               Hashtbl.add (ineq_table.(i)) name (r t)) approxs in
    let _ = map (fun (i, t) -> Hashtbl.add (ineq_test_table.(i)) (name^"_neg") t;
                               Hashtbl.add (ineq_table.(i)) (name^"_neg") (r t)) neg_approxs in
      () in

    Hashtbl.iter (fun name ineq -> add_approximations_to_table name ineq) table;;


let find_ineq precision name = Hashtbl.find ineq_table.(precision) name;;
let find_test_ineq precision name = Hashtbl.find ineq_test_table.(precision) name;;



(* Generate and add inequalities for constraints *)
add_everything_to_table constraints;;
add_everything_to_table var_bound_ineqs;;


(**************************)


(*
generate_ineqs [4] (get_ineq "ineq112");;

Hashtbl.iter (fun name ineq -> let _ = generate_ineqs[3;4;5] ineq in ()) constraints;;
*)

(***************)
(*********************)