formal_lp/old/ineqs/contravening_ineqs.hl

   1 needs "../formal_lp/ineqs/list_hypermap.hl";;
   2 needs "../formal_lp/ineqs/list_hypermap_iso.hl";;
   3 needs "../formal_lp/ineqs/constants_approx.hl";;
   4
   5
   6 needs "arith/nat.hl";;
   7
   8
   9 open Sphere;;
  10
  11
  12 (* Definitions of variables *)
  13
  14
  15 (* Variables for fans *)
  16 (* TODO: these definitions are not necessary *)
  17
  18
  19 let azim2_fan = new_definition `azim2_fan (V,E) (x:real^3#real^3) = azim_dart (V,E) (f_fan_pair (V,E) x)`;;
  20 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)`;;
  21 let yn_fan = new_definition `yn_fan (n:real^3#real^3->bool) = norm (FST (@x. x IN n))`;;
  22 let ln_fan = new_definition `ln_fan (n:real^3#real^3->bool) = abs (ly (yn_fan n))`;;
  23 let ye_fan = new_definition `ye_fan (x:real^3#real^3) = dist x`;;
  24
  25 let y1_fan = new_definition `y1_fan (x:real^3#real^3) = norm(FST x)`;;
  26 let y2_fan = new_definition `y2_fan (x:real^3#real^3) = norm(SND x)`;;
  27 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))`;;
  28 let y4_fan = new_definition `y4_fan (V,E) (x:real^3#real^3) = dist(f_fan_pair (V,E) x)`;;
  29 let y5_fan = new_definition `y5_fan (V,E) (x:real^3#real^3) = dist(inverse (f_fan_pair_ext (V,E)) x)`;;
  30 let y6_fan = new_definition `y6_fan (x:real^3#real^3) = dist x`;;
  31 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)`;;
  32 let y9_fan = new_definition `y9_fan (V,E) (x:real^3#real^3) = dist(f_fan_pair (V,E) x)`;;
  33
  34 let rhazim_fan = new_definition `rhazim_fan (V,E) (x:real^3#real^3) = abs(rho(y1_fan x)) * azim_dart (V,E) x`;;
  35 let rhazim2_fan = new_definition `rhazim2_fan (V,E) (x:real^3#real^3) = rhazim_fan (V,E) (f_fan_pair (V,E) x)`;;
  36 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)`;;
  37
  38 let rho_fan = new_definition `rho_fan n = abs((&1 + sol0 / pi) - ln_fan n * sol0 / pi)`;;
  39 let sol_fan = new_definition `sol_fan (V,E) f = abs(sum f (\x. azim_dart (V,E) x - pi) + &2 * pi)`;;
  40 let tau_fan = new_definition `tau_fan (V,E) f = abs (tauVEF (V,E,f))`;;
  41
  42
  43 let fan_defs =
  44 [
  45   azim2_fan; azim3_fan; yn_fan; ln_fan; ye_fan;
  46   rho_fan; sol_fan; tau_fan; rhazim_fan; rhazim2_fan; rhazim3_fan;
  47   y1_fan; y2_fan; y3_fan; y4_fan; y5_fan; y6_fan; y8_fan; y9_fan;
  48 ]
  49
  50
  51
  52 (* Variables for lists *)
  53
  54
  55 let list_defs = map new_definition
  56   [
  57     `azim_list (V,g) = (azim_dart (V,ESTD V) o g):num#num->real`;
  58     `azim2_list (V,g) = (azim2_fan (V,ESTD V) o g):num#num->real`;
  59     `azim3_list (V,g) = (azim3_fan (V,ESTD V) o g):num#num->real`;
  60     `(yn_list g):(num#num->bool)->real = yn_fan o IMAGE g`;
  61     `(ln_list g):(num#num->bool)->real = ln_fan o IMAGE g`;
  62     `rhazim_list (V,g) = (rhazim_fan (V,ESTD V) o g):num#num->real`;
  63     `rhazim2_list (V,g) = (rhazim2_fan (V,ESTD V) o g):num#num->real`;
  64     `rhazim3_list (V,g) = (rhazim3_fan (V,ESTD V) o g):num#num->real`;
  65     `(ye_list g):(num#num->real) = ye_fan o g`;
  66     `(rho_list g):(num#num->bool)->real = rho_fan o IMAGE g`;
  67     `(sol_list (V,g)):(num#num->bool)->real = sol_fan (V,ESTD V) o IMAGE g`;
  68     `(tau_list (V,g)):(num#num->bool)->real = tau_fan (V,ESTD V) o IMAGE g`;
  69     `(y1_list g):(num#num->real) = y1_fan o g`;
  70     `(y2_list g):(num#num->real) = y2_fan o g`;
  71     `(y3_list (V,g)):(num#num->real) = y3_fan (V,ESTD V) o g`;
  72     `(y4_list (V,g)):(num#num->real) = y4_fan (V,ESTD V) o g`;
  73     `(y5_list (V,g)):(num#num->real) = y5_fan (V,ESTD V) o g`;
  74     `(y6_list g):(num#num->real) = y6_fan o g`;
  75     `(y8_list (V,g)):(num#num->real) = y8_fan (V,ESTD V) o g`;
  76     `(y9_list (V,g)):(num#num->real) = y9_fan (V,ESTD V) o g`;
  77   ];;
  78
  79
  80 let list_defs2 = map (REWRITE_RULE[FUN_EQ_THM; o_THM]) list_defs;;
  81
  82
  83 let list_var_rewrites =
  84   map GSYM list_defs @ map GSYM list_defs2;;
  85
  86
  87
  88 (* All variables are nonnegative *)
  89
  90
  91
  92 let AZIM_DART_POS = prove(`&0 <= azim_dart (V,E) x`,
  93    MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
  94      STRIP_TAC THEN
  95      ASM_REWRITE_TAC[azim_dart] THEN
  96      COND_CASES_TAC THENL
  97      [
  98        MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC;
  99        ALL_TAC
 100      ] THEN
 101      REWRITE_TAC[Fan_defs.azim_fan] THEN
 102      COND_CASES_TAC THEN REWRITE_TAC[azim] THEN
 103      MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC);;
 104
 105
 106 let DIST_POS = prove(`!x:(real^3#real^3). &0 <= dist x`,
 107    GEN_TAC THEN MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
 108      STRIP_TAC THEN ASM_REWRITE_TAC[dist; NORM_POS_LE]);;
 109
 110
 111 let list_var_pos = map (fun tm -> prove(tm,
 112                      GEN_TAC THEN REWRITE_TAC list_defs2 THEN REWRITE_TAC fan_defs THEN
 113                        TRY (MATCH_MP_TAC REAL_LE_MUL) THEN
 114                        REWRITE_TAC[AZIM_DART_POS; REAL_ABS_POS; NORM_POS_LE; DIST_POS]))
 115 [
 116   `!x. &0 <= azim_list (V,g) x`;
 117   `!x. &0 <= azim2_list (V,g) x`;
 118   `!x. &0 <= azim3_list (V,g) x`;
 119   `!x. &0 <= rhazim_list (V,g) x`;
 120   `!x. &0 <= rhazim2_list (V,g) x`;
 121   `!x. &0 <= rhazim3_list (V,g) x`;
 122   `!n. &0 <= yn_list g n`;
 123   `!n. &0 <= ln_list g n`;
 124   `!e. &0 <= ye_list g e`;
 125   `!n. &0 <= rho_list g n`;
 126   `!f. &0 <= sol_list (V,g) f`;
 127   `!f. &0 <= tau_list (V,g) f`;
 128   `!x. &0 <= y1_list g x`;
 129   `!x. &0 <= y2_list g x`;
 130   `!x. &0 <= y3_list (V,g) x`;
 131   `!x. &0 <= y4_list (V,g) x`;
 132   `!x. &0 <= y5_list (V,g) x`;
 133   `!x. &0 <= y6_list g x`;
 134   `!x. &0 <= y8_list (V,g) x`;
 135   `!x. &0 <= y9_list (V,g) x`;
 136 ];;
 137
 138
 139
 140 (* mod-file variables and definitions *)
 141
 142
 143 let var_bound_ineqs = Hashtbl.create 40;;
 144
 145
 146 let sets =
 147   ["dart", `dart H:A->bool`;
 148    "dart3", `hyp_dart3 H:A->bool`;
 149    "node", `node_set H:(A->bool)->bool`;
 150    "face", `face_set H:(A->bool)->bool`;
 151    "dart_std4", `hyp_dart4 H:A->bool`];;
 152
 153
 154 let define_var var_name set_name low high =
 155   let var = match set_name with
 156       "dart" | "dart3" | "dart_std4" -> `d:A`
 157     | "node" -> `n:A->bool`
 158     | "face" -> `f:A->bool`
 159     | _ -> failwith "Undefined set name" in
 160   let var_ty = snd (dest_var var) in
 161   let f_ty = mk_type ("fun", [var_ty; `:real`]) in
 162   let set_ty = mk_type ("fun", [var_ty; `:bool`]) in
 163   let f = mk_var (var_name^"_mod", f_ty) in
 164   let set = assoc set_name sets in
 165   let in_const = mk_mconst ("IN", mk_type ("fun", [var_ty; mk_type ("fun", [set_ty; `:bool`])])) in
 166   let le = `(<=):real->real->bool` in
 167   let fvar = mk_comb (f, var) in
 168   let l, h = mk_binop le low fvar, mk_binop le fvar high in
 169   let cond = mk_binop in_const var set in
 170
 171   let ineq_lo = mk_forall(var, mk_imp(cond, l)) in
 172   let ineq_hi = mk_forall(var, mk_imp(cond, h)) in
 173
 174   let _ = Hashtbl.add var_bound_ineqs (var_name^"_lo") ineq_lo in
 175   let _ = Hashtbl.add var_bound_ineqs (var_name^"_hi") ineq_hi in
 176     f;;
 177
 178
 179
 180
 181 (* Terms for variables in the model file *)
 182 Hashtbl.clear var_bound_ineqs;;
 183
 184 let azim_mod = define_var "azim" "dart" `&0` `pi` and
 185     azim2_mod = define_var "azim2" "dart3" `&0` `pi` and
 186     azim3_mod = define_var "azim3" "dart3" `&0` `pi` and
 187     ln_mod = define_var "ln" "node" `&0` `&1` and
 188     rhazim_mod = define_var "rhazim" "dart" `&0` `pi + sol0` and
 189     rhazim2_mod = define_var "rhazim2" "dart3" `&0` `pi + sol0` and
 190     rhazim3_mod = define_var "rhazim3" "dart3" `&0` `pi + sol0` and
 191     yn_mod = define_var "yn" "node" `&2` `#2.52`and
 192     ye_mod = define_var "ye" "dart" `&2` `&3` and
 193     rho_mod = define_var "rho" "node" `&1` `&1 + sol0 / pi` and
 194     sol_mod = define_var "sol" "face" `&0` `&4 * pi` and
 195     tau_mod = define_var "tau" "face" `&0` `tgt` and
 196     y1_mod = define_var "y1" "dart" `&2` `#2.52` and
 197     y2_mod = define_var "y2" "dart" `&2` `#2.52` and
 198     y3_mod = define_var "y3" "dart" `&2` `#2.52` and
 199     y4_mod = define_var "y4" "dart3" `&2` `&3` and
 200     y5_mod = define_var "y5" "dart" `&2` `&3` and
 201     y6_mod = define_var "y6" "dart" `&2` `&3` and
 202     y8_mod = define_var "y8" "dart_std4" `&2` `#2.52` and
 203     y9_mod = define_var "y9" "dart_std4" `&2` `#2.52`;;
 204
 205
 206 let var_list =
 207   let inst_t = inst[`:real^3#real^3`, aty] in
 208     [
 209       `hypermap_of_fan (V,E)`, `H:(real^3#real^3)hypermap`;
 210       `azim_dart (V,E)`, inst_t azim_mod;
 211       `azim2_fan (V,E)`, inst_t azim2_mod;
 212       `azim3_fan (V,E)`, inst_t azim3_mod;
 213       `ln_fan`, inst_t ln_mod;
 214       `rhazim_fan (V,E)`, inst_t rhazim_mod;
 215       `rhazim2_fan (V,E)`, inst_t rhazim2_mod;
 216       `rhazim3_fan (V,E)`, inst_t rhazim3_mod;
 217       `yn_fan`, inst_t yn_mod;
 218       `ye_fan`, inst_t ye_mod;
 219       `rho_fan`, inst_t rho_mod;
 220       `sol_fan (V,E)`, inst_t sol_mod;
 221       `tau_fan (V,E)`, inst_t tau_mod;
 222       `y1_fan`, inst_t y1_mod;
 223       `y2_fan`, inst_t y2_mod;
 224       `y3_fan (V,E)`, inst_t y3_mod;
 225       `y4_fan (V,E)`, inst_t y4_mod;
 226       `y5_fan (V,E)`, inst_t y5_mod;
 227       `y6_fan`, inst_t y6_mod;
 228       `y8_fan (V,E)`, inst_t y8_mod;
 229       `y9_fan (V,E)`, inst_t y9_mod;
 230     ];;
 231
 232
 233
 234
 235 (* Declare all inequalities in a format which is close to the mod-file format *)
 236
 237 let constraints = Hashtbl.create 100;;
 238 let add_constraints = map (uncurry (Hashtbl.add constraints));;
 239
 240 (* equality constraints *)
 241
 242 add_constraints
 243 [
 244   "azim_sum", `!n. n IN node_set (H:(A)hypermap) ==> sum n azim_mod = &2 * pi`;
 245   "rhazim_sum", `!n. n IN node_set (H:(A)hypermap) ==> sum n rhazim_mod = &2 * pi * rho_mod n`;
 246
 247   "sol_sum3", `!f. f IN hyp_face3 (H:(A)hypermap) ==> sum f azim_mod = sol_mod f + pi`;
 248   "tau_sum3", `!f. f IN hyp_face3 (H:(A)hypermap) ==> sum f rhazim_mod = tau_mod f + (pi + sol0)`;
 249   "sol_sum4", `!f. f IN hyp_face4 (H:(A)hypermap) ==> sum f azim_mod = sol_mod f + &2 * pi`;
 250   "tau_sum4", `!f. f IN hyp_face4 (H:(A)hypermap) ==> sum f rhazim_mod = tau_mod f + &2 * (pi + sol0)`;
 251   "sol_sum5", `!f. f IN hyp_face5 (H:(A)hypermap) ==> sum f azim_mod = sol_mod f + &3 * pi`;
 252   "tau_sum5", `!f. f IN hyp_face5 (H:(A)hypermap) ==> sum f rhazim_mod = tau_mod f + &3 * (pi + sol0)`;
 253   "sol_sum6", `!f. f IN hyp_face6 (H:(A)hypermap) ==> sum f azim_mod = sol_mod f + &4 * pi`;
 254   "tau_sum6", `!f. f IN hyp_face6 (H:(A)hypermap) ==> sum f rhazim_mod = tau_mod f + &4 * (pi + sol0)`;
 255
 256   "ln_def", `!n. n IN node_set (H:(A)hypermap) ==> ln_mod n = (#2.52 - yn_mod n) / #0.52`;
 257   "rho_def", `!n. n IN node_set (H:(A)hypermap) ==> rho_mod n = (&1 + sol0 / pi) - ln_mod n * sol0 / pi`;
 258
 259   "edge_sym", `!e. e IN hyp_edge_pairs (H:(A)hypermap) ==> ye_mod (FST e) = ye_mod (SND e):real`;
 260
 261   "y1_def", `!d. d IN dart (H:(A)hypermap) ==> y1_mod d = yn_mod (node H d):real`;
 262   "y2_def", `!d. d IN dart (H:(A)hypermap) ==> y2_mod d = yn_mod (node H (face_map H d)):real`;
 263   "y3_def", `!d. d IN dart (H:(A)hypermap) ==> y3_mod d = yn_mod (node H (inverse (face_map H) d)):real`;
 264   "y4_def", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> y4_mod d = ye_mod (face_map H d):real`;
 265   "y5_def", `!d. d IN dart (H:(A)hypermap) ==> y5_mod d = ye_mod (inverse (face_map H) d):real`;
 266   "y6_def", `!d. d IN dart (H:(A)hypermap) ==> y6_mod d = ye_mod d:real`;
 267   "y9_def", `!d. d IN hyp_dart4 (H:(A)hypermap) ==> y9_mod d = ye_mod (face_map H d):real`;
 268   "y8_def", `!d. d IN hyp_dart4 (H:(A)hypermap) ==> y8_mod d = y5_mod (inverse (face_map H) d):real`;
 269
 270   "azim2c", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> azim2_mod d = azim_mod (face_map H d):real`;
 271   "azim3c", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> azim3_mod d = azim_mod (inverse (face_map H) d):real`;
 272   "rhazim2c", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> rhazim2_mod d = rhazim_mod (face_map H d):real`;
 273   "rhazim3c", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> rhazim3_mod d = rhazim_mod (inverse (face_map H) d):real`;
 274 ];;
 275
 276
 277
 278 (* inequality constraints *)
 279
 280 add_constraints
 281 [
 282   "RHA", `!d. d IN dart (H:(A)hypermap) ==> rhazim_mod d >= azim_mod d:real`;
 283   "RHB", `!d. d IN dart (H:(A)hypermap) ==> rhazim_mod d <= azim_mod d * (&1 + sol0 / pi)`;
 284 (* "RHBLO"; "RHBHI" *)
 285 ];;
 286
 287
 288 (* definitional inequalities *)
 289
 290
 291
 292 (* y bounds *)
 293 add_constraints
 294 [
 295   "yy10", `!d. (d:A) IN dart (H:(A)hypermap) ==> ye_mod d <= #2.52`;
 296 ];;
 297
 298
 299
 300 (* tau tame table D inequality (Main Estimate) *)
 301 add_constraints
 302 [
 303   "tau3", `!f:A->bool. f IN hyp_face3 (H:(A)hypermap) ==> tau_mod f >= &0`;
 304   "tau4", `!f:A->bool. f IN hyp_face4 (H:(A)hypermap) ==> tau_mod f >= #0.206`;
 305   "tau5", `!f:A->bool. f IN hyp_face5 (H:(A)hypermap) ==> tau_mod f >= #0.4819`;
 306   "tau6", `!f:A->bool. f IN hyp_face6 (H:(A)hypermap) ==> tau_mod f >= #0.7578`;
 307 ];;
 308
 309
 310 add_constraints
 311 [
 312   "ineq105", `!d:A. d IN hyp_dartX H ==>
 313         ((((azim_mod d) - #1.629) + ((#0.402 * (y2_mod d +
 314                 (y3_mod d + (y5_mod d + (y6_mod d - #8.0))))) -
 315                         (#0.315 * (y1_mod d - #2.0)))) - #0.0) >= #0.0`;
 316
 317   "ineq106", `!d:A. d IN hyp_dart3 H ==>
 318         ((((rhazim_mod d) - #1.2308) + (((#0.3639 * (y2_mod d + (y3_mod d + (y5_mod d + (y6_mod d - #8.0))))) -
 319                 (#0.6 * (y1_mod d - #2.0))) - (#0.685 * (y4_mod d - #2.0)))) - #0.0) >= #0.0`;
 320
 321   "ineq107", `!d:A. d IN hyp_dart3 H ==>
 322         (((--(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`;
 323
 324   "ineq108", `!d:A. d IN hyp_dart3 H ==>
 325         ((((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`;
 326
 327   "ineq109", `!d:A. d IN hyp_dart3 H ==>
 328         (((--(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`;
 329
 330   "ineq110", `!d:A. d IN hyp_dart3 H ==>
 331         (((((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`;
 332
 333   "ineq111", `!d:A. d IN hyp_dart3 H ==>
 334         (((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`;
 335
 336
 337   "ineq112", `!d:A. d IN hyp_dart3 H ==>
 338         ((((tau_mod (face H d)) - (#0.507 * (azim_mod d))) + #0.724) - #0.0) >= #0.0`;
 339
 340   "ineq113", `!d:A. d IN hyp_dart3 H ==>
 341         ((((tau_mod (face H d)) - (#0.259 * (azim_mod d))) + #0.32) - #0.0) >= #0.0`;
 342
 343   "ineq114", `!d:A. d IN hyp_dart3 H ==>
 344         (((tau_mod (face H d)) + ((#0.626 * (azim_mod d)) - #0.77)) - #0.0) >= #0.0`;
 345
 346   "ineq115", `!d:A. d IN hyp_dart3 H ==>
 347         (#1.893 - (azim_mod d)) >= #0.0`;
 348
 349   "ineq116", `!d:A. d IN hyp_dart3 H ==>
 350         ((azim_mod d) - #0.852) >= #0.0`;
 351
 352   "ineq119", `!d:A. d IN hyp_dart4 H ==>
 353         ((((tau_mod (face H d)) - (#0.453 * (azim_mod d))) + #0.777) - #0.0) >= #0.0`;
 354
 355   "ineq120", `!d:A. d IN hyp_dart4 H ==>
 356         (((tau_mod (face H d)) + ((#0.7573 * (azim_mod d)) - #1.433)) - #0.0) >= #0.0`;
 357
 358   "ineq121", `!d:A. d IN hyp_dart4 H ==>
 359         (((tau_mod (face H d)) + ((#0.972 * (azim_mod d)) - #1.707)) - #0.0) >= #0.0`;
 360
 361   "ineq122", `!d:A. d IN hyp_dart4 H ==>
 362         (((tau_mod (face H d)) + ((#4.72 * (azim_mod d)) - #6.248)) - #0.0) >= #0.0`;
 363 ];;
 364
 365
 366 (*
 367 let y1_def = `!d. d IN dart (H:(A)hypermap) ==> y1_mod d = yn_mod (node H d):real`;;
 368 y1_def{(i3,i1,i2,j) in e_dart}: y1[i1,j] = yn[i1];
 369
 370
 371 (* Rename terms and types *)
 372 let s1 = inst [`:real^3#real^3`, aty] im_sum;;
 373 let s2 = subst [`hypermap_of_fan (V,E)`, h_fan_hyp] s1;;
 374 let s3 = subst [`azim_dart (V,E)`, azim_mod] s2;;
 375 *)
 376
 377 (*************************************)
 378
 379 let SUM_ISOMORPHISM = prove(`!G H (g:B->A) (r:A->real). isomorphism g (G,H)
 380                             ==> (!d. d IN dart G ==> sum(node G d) (r o g) = sum(node H (g d)) r)`,
 381    REPEAT STRIP_TAC THEN
 382      SUBGOAL_THEN `sum(node G d) (r o (g:B->A)) = sum(IMAGE g (node G d)) r` (fun th -> REWRITE_TAC[th]) THENL
 383      [
 384        MATCH_MP_TAC (GSYM SUM_IMAGE) THEN
 385          REPEAT STRIP_TAC THEN
 386          UNDISCH_TAC `isomorphism (g:B->A) (G,H)` THEN
 387          REWRITE_TAC[isomorphism; BIJ; INJ] THEN
 388          DISCH_THEN (MP_TAC o CONJUNCT1) THEN
 389          DISCH_THEN (MP_TAC o CONJUNCT1) THEN
 390          DISCH_THEN (MATCH_MP_TAC o CONJUNCT2) THEN
 391          ASM_REWRITE_TAC[] THEN
 392          CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN EXISTS_TAC `node G (d:B)` THEN ASM_SIMP_TAC[Hypermap.lemma_node_subset];
 393        ALL_TAC
 394      ] THEN
 395      MP_TAC (ISPECL [`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `d:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
 396      ASM_REWRITE_TAC[] THEN
 397      DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]));;
 398
 399
 400 let ISO_NODE_INJ = prove(`!G H (g:B->A) n. isomorphism g (G,H) /\ n IN node_set G ==>
 401                            (!x y. x IN n /\ y IN n /\ g x = g y ==> x = y)`,
 402    REPEAT STRIP_TAC THEN
 403      UNDISCH_TAC `isomorphism (g:B->A) (G,H)` THEN
 404      REWRITE_TAC[isomorphism; BIJ; INJ] THEN
 405      DISCH_THEN (MP_TAC o CONJUNCT1) THEN DISCH_THEN (MP_TAC o CONJUNCT1) THEN
 406      DISCH_THEN (MATCH_MP_TAC o CONJUNCT2) THEN
 407      ASM_REWRITE_TAC[] THEN
 408      MP_TAC (ISPECL [`G:(B)hypermap`; `n:B->bool`] Hypermap.lemma_node_representation) THEN
 409      ASM_REWRITE_TAC[] THEN
 410      STRIP_TAC THEN
 411      CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN
 412      EXISTS_TAC `n:B->bool` THEN
 413      ASM_REWRITE_TAC[] THEN
 414      ASM_SIMP_TAC[Hypermap.lemma_node_subset]);;
 415
 416
 417
 418 let COMPONENTS_ISO_IMAGE = prove(`!G H (g:B->A). isomorphism g (G,H)
 419                              ==> (!d. d IN dart G ==>
 420                                     node H (g d) = IMAGE g (node G d) /\
 421                                     face H (g d) = IMAGE g (face G d))`,
 422    REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 423      MP_TAC (ISPECL[`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `d:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
 424      ASM_REWRITE_TAC[] THEN
 425      SIMP_TAC[]);;
 426
 427
 428 let HYPERMAP_MAPS_ISO_COMM = prove(`!G H (g:B->A). isomorphism g (G,H)
 429                              ==> (!d. d IN dart G ==>
 430                                     face_map H (g d) = g (face_map G d) /\
 431                                     node_map H (g d) = g (node_map G d))`,
 432    SIMP_TAC[isomorphism]);;
 433
 434
 435 let HYPERMAP_INV_MAPS = prove(`!(G:(B)hypermap) d. d IN dart G
 436                                 ==> (?k. inverse (face_map G) d = (face_map G POWER k) d)`,
 437    REPEAT STRIP_TAC THEN
 438      ABBREV_TAC `n = CARD (orbit_map (face_map G) (d:B))` THEN
 439      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
 440      ASM_REWRITE_TAC[Hypermap.hypermap_lemma] THEN
 441      ANTS_TAC THENL
 442      [
 443        REWRITE_TAC[ARITH_RULE `1 <= n <=> 0 < n`] THEN
 444          EXPAND_TAC "n" THEN
 445          MATCH_MP_TAC Hypermap_and_fan.ORBIT_MAP_CARD_POS THEN
 446          EXISTS_TAC `dart G:B->bool` THEN
 447          REWRITE_TAC[Hypermap.hypermap_lemma];
 448        ALL_TAC
 449      ] THEN
 450      REWRITE_TAC[Hypermap.POWER_1] THEN
 451      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 452      EXISTS_TAC `n - 1` THEN
 453      REWRITE_TAC[]);;
 454
 455
 456
 457 let HYPERMAP_INV_MAPS_ISO_COMM = prove(`!G H (g:B->A). isomorphism g (G,H)
 458                          ==> (!d. d IN dart G ==>
 459                                 inverse (face_map H) (g d) = g (inverse (face_map G) d) /\
 460                                 inverse (node_map H) (g d) = g (inverse (node_map G) d))`,
 461    REWRITE_TAC[isomorphism] THEN REPEAT STRIP_TAC THEN
 462      MATCH_MP_TAC (GSYM COMM_INVERSE_LEMMA) THEN
 463      MAP_EVERY EXISTS_TAC [`dart G:B->bool`; `dart H:A->bool`] THEN
 464      ASM_SIMP_TAC[Hypermap.hypermap_lemma]);;
 465
 466
 467 let HYPERMAP_INV_MAPS_ISO_IMAGE = prove(`!G H (g:B->A). isomorphism g (G,H)
 468                         ==> (!d. d IN dart G ==>
 469                                face H (inverse (face_map H) (g d)) = IMAGE g (face G (inverse (face_map G) d)) /\
 470                                node H (inverse (face_map H) (g d)) = IMAGE g (node G (inverse (face_map G) d)))`,
 471    REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 472      ASM_SIMP_TAC[HYPERMAP_INV_MAPS_ISO_COMM] THEN
 473      ABBREV_TAC `x = inverse (face_map G) (d:B)` THEN
 474      SUBGOAL_THEN `x:B IN dart G` ASSUME_TAC THENL
 475      [
 476        EXPAND_TAC "x" THEN
 477          ASM_SIMP_TAC[Hypermap.lemma_dart_inveriant_under_inverse_maps];
 478        ALL_TAC
 479      ] THEN
 480      ASM_SIMP_TAC[COMPONENTS_ISO_IMAGE]);;
 481
 482
 483
 484
 485
 486 let HYPERMAP_MAPS_ISO_IMAGE = prove(`!G H (g:B->A). isomorphism g (G,H)
 487                                     ==> (!d. d IN dart G ==>
 488                                            face H (face_map H (g d)) = IMAGE g (face G (face_map G d)) /\
 489                                            face H (node_map H (g d)) = IMAGE g (face G (node_map G d)) /\
 490                                            node H (node_map H (g d)) = IMAGE g (node G (node_map G d)) /\
 491                                            node H (face_map H (g d)) = IMAGE g (node G (face_map G d)))`,
 492    REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 493      ASM_SIMP_TAC[HYPERMAP_MAPS_ISO_COMM] THEN
 494      MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
 495      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 496      REPEAT CONJ_TAC THENL
 497      [
 498        FIRST_X_ASSUM (MP_TAC o SPEC `face_map G (d:B)`);
 499        FIRST_X_ASSUM (MP_TAC o SPEC `node_map G (d:B)`);
 500        FIRST_X_ASSUM (MP_TAC o SPEC `node_map G (d:B)`);
 501        FIRST_X_ASSUM (MP_TAC o SPEC `face_map G (d:B)`)
 502      ] THEN
 503      ASM_SIMP_TAC[Hypermap.lemma_dart_invariant]);;
 504
 505
 506
 507
 508
 509
 510
 511
 512 let SUM_NODE_ISO = prove(`!G H (g:B->A) (r:A->real). isomorphism g (G,H)
 513                            ==> (!n. n IN node_set G ==> sum(IMAGE g n) r = sum n (r o g))`,
 514    REPEAT STRIP_TAC THEN
 515      MATCH_MP_TAC SUM_IMAGE THEN
 516      MATCH_MP_TAC ISO_NODE_INJ THEN
 517      MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
 518      ASM_REWRITE_TAC[]);;
 519
 520
 521
 522 let CARD_NODE_ISO = prove(`!G H (g:B->A). isomorphism g (G,H)
 523                             ==> (!n. n IN node_set G ==> CARD (IMAGE g n) = CARD n)`,
 524    REPEAT STRIP_TAC THEN
 525      MATCH_MP_TAC CARD_IMAGE_INJ THEN
 526      CONJ_TAC THENL
 527      [
 528        MATCH_MP_TAC ISO_NODE_INJ THEN
 529          MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
 530          ASM_REWRITE_TAC[];
 531        ALL_TAC
 532      ] THEN
 533
 534      MP_TAC (ISPECL [`G:(B)hypermap`; `n:B->bool`] Hypermap.lemma_node_representation) THEN
 535      ASM_REWRITE_TAC[] THEN
 536      STRIP_TAC THEN
 537      ASM_REWRITE_TAC[Hypermap.NODE_FINITE]);;
 538
 539
 540 let SUM_NODE_SUB = prove(`!(G:(B)hypermap) r1 r2 n. n IN node_set G
 541                            ==> sum n (\x. r1 x - r2 x) = sum n r1 - sum n r2`,
 542    REPEAT STRIP_TAC THEN
 543      MP_TAC (ISPECL [`G:(B)hypermap`; `n:B->bool`] Hypermap.lemma_node_representation) THEN
 544      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 545      ASM_SIMP_TAC[Hypermap.NODE_FINITE; SUM_SUB]);;
 546
 547
 548 let SUM_NODE_CONST = prove(`!(G:(B)hypermap) c n. n IN node_set G
 549                              ==> sum n (\x. c) = &(CARD n) * c`,
 550    REPEAT STRIP_TAC THEN
 551      MP_TAC (ISPECL [`G:(B)hypermap`; `n:B->bool`] Hypermap.lemma_node_representation) THEN
 552      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 553      ASM_SIMP_TAC[Hypermap.NODE_FINITE; SUM_CONST]);;
 554
 555
 556 let SUM_NODE_SUB_CONST = prove(`!(G:(B)hypermap) r c n. n IN node_set G
 557                                  ==> sum n (\x. r x - c) = sum n r - &(CARD n) * c`,
 558    REPEAT STRIP_TAC THEN
 559      MP_TAC (SPEC_ALL SUM_NODE_CONST) THEN
 560      ASM_REWRITE_TAC[] THEN
 561      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 562      MP_TAC (SPECL [`G:(B)hypermap`; `r:B->real`; `\x:B. c:real`; `n:B->bool`] SUM_NODE_SUB) THEN
 563      ASM_REWRITE_TAC[]);;
 564
 565
 566
 567
 568
 569 let ISO_FACE_INJ = prove(`!G H (g:B->A) f. isomorphism g (G,H) /\ f IN face_set G ==>
 570                            (!x y. x IN f /\ y IN f /\ g x = g y ==> x = y)`,
 571    REPEAT STRIP_TAC THEN
 572      UNDISCH_TAC `isomorphism (g:B->A) (G,H)` THEN
 573      REWRITE_TAC[isomorphism; BIJ; INJ] THEN
 574      DISCH_THEN (MP_TAC o CONJUNCT1) THEN DISCH_THEN (MP_TAC o CONJUNCT1) THEN
 575      DISCH_THEN (MATCH_MP_TAC o CONJUNCT2) THEN
 576      ASM_REWRITE_TAC[] THEN
 577      MP_TAC (ISPECL [`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
 578      ASM_REWRITE_TAC[] THEN
 579      STRIP_TAC THEN
 580      CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN
 581      EXISTS_TAC `f:B->bool` THEN
 582      ASM_REWRITE_TAC[] THEN
 583      ASM_SIMP_TAC[Hypermap.lemma_face_subset]);;
 584
 585
 586 let SUM_FACE_ISO = prove(`!G H (g:B->A) (r:A->real). isomorphism g (G,H)
 587                            ==> (!f. f IN face_set G ==> sum(IMAGE g f) r = sum f (r o g))`,
 588    REPEAT STRIP_TAC THEN
 589      MATCH_MP_TAC SUM_IMAGE THEN
 590      MATCH_MP_TAC ISO_FACE_INJ THEN
 591      MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
 592      ASM_REWRITE_TAC[]);;
 593
 594
 595
 596 let CARD_FACE_ISO = prove(`!G H (g:B->A). isomorphism g (G,H)
 597                             ==> (!f. f IN face_set G ==> CARD (IMAGE g f) = CARD f)`,
 598    REPEAT STRIP_TAC THEN
 599      MATCH_MP_TAC CARD_IMAGE_INJ THEN
 600      CONJ_TAC THENL
 601      [
 602        MATCH_MP_TAC ISO_FACE_INJ THEN
 603          MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
 604          ASM_REWRITE_TAC[];
 605        ALL_TAC
 606      ] THEN
 607
 608      MP_TAC (ISPECL [`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
 609      ASM_REWRITE_TAC[] THEN
 610      STRIP_TAC THEN
 611      ASM_REWRITE_TAC[Hypermap.FACE_FINITE]);;
 612
 613
 614 let SUM_FACE_SUB = prove(`!(G:(B)hypermap) r1 r2 f. f IN face_set G
 615                            ==> sum f (\x. r1 x - r2 x) = sum f r1 - sum f r2`,
 616    REPEAT STRIP_TAC THEN
 617      MP_TAC (ISPECL [`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
 618      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 619      ASM_SIMP_TAC[Hypermap.FACE_FINITE; SUM_SUB]);;
 620
 621
 622 let SUM_FACE_CONST = prove(`!(G:(B)hypermap) c f. f IN face_set G
 623                              ==> sum f (\x. c) = &(CARD f) * c`,
 624    REPEAT STRIP_TAC THEN
 625      MP_TAC (ISPECL [`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
 626      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 627      ASM_SIMP_TAC[Hypermap.FACE_FINITE; SUM_CONST]);;
 628
 629
 630 let SUM_FACE_SUB_CONST = prove(`!(G:(B)hypermap) r c f. f IN face_set G
 631                                  ==> sum f (\x. r x - c) = sum f r - &(CARD f) * c`,
 632    REPEAT STRIP_TAC THEN
 633      MP_TAC (SPEC_ALL SUM_FACE_CONST) THEN
 634      ASM_REWRITE_TAC[] THEN
 635      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
 636      MP_TAC (SPECL [`G:(B)hypermap`; `r:B->real`; `\x:B. c:real`; `f:B->bool`] SUM_FACE_SUB) THEN
 637      ASM_REWRITE_TAC[]);;
 638
 639
 640
 641
 642 let SUM_NODE_LIST = prove(`!L (n:(A#A)list). good_list L /\ MEM n (list_of_nodes L) ==>
 643                             sum (set_of_list n) = list_sum n`,
 644    REPEAT STRIP_TAC THEN
 645      REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `f:(A#A)->real` THEN
 646      MP_TAC (ISPECL [`f:A#A->real`; `n:(A#A)list`] ALL_DISTINCT_SUM) THEN
 647      ANTS_TAC THENL
 648      [
 649        MATCH_MP_TAC ALL_DISTINCT_NODE THEN
 650          EXISTS_TAC `L:((A)list)list` THEN
 651          ASM_REWRITE_TAC[];
 652        ALL_TAC
 653      ] THEN
 654      REWRITE_TAC[]);;
 655
 656
 657
 658 let SUM_NODE_LIST_ALL = prove(`!L (P:(A#A->bool)->((A#A->real)->real)->bool). good_list L /\ good_list_nodes L ==>
 659                             ((!n. n IN node_set (hypermap_of_list L) ==> P n (sum n))
 660                             <=> (!n. MEM n (list_of_nodes L) ==> P (set_of_list n) (list_sum n)))`,
 661    REWRITE_TAC[good_list_nodes] THEN
 662      REPEAT STRIP_TAC THEN
 663      ASM_REWRITE_TAC[IN_SET_OF_LIST; nodes_of_list] THEN
 664      EQ_TAC THEN REPEAT STRIP_TAC THENL
 665      [
 666        FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list n:A#A->bool`) THEN
 667          REWRITE_TAC[MEM_MAP] THEN
 668          ANTS_TAC THENL
 669          [
 670            EXISTS_TAC `n:(A#A)list` THEN
 671              ASM_REWRITE_TAC[];
 672            ALL_TAC
 673          ] THEN
 674
 675          MP_TAC (SPEC_ALL SUM_NODE_LIST) THEN
 676          ASM_REWRITE_TAC[] THEN
 677          DISCH_THEN (fun th -> REWRITE_TAC[th]);
 678        ALL_TAC
 679      ] THEN
 680
 681      POP_ASSUM MP_TAC THEN
 682      REWRITE_TAC[MEM_MAP] THEN
 683      STRIP_TAC THEN
 684      FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
 685      ASM_REWRITE_TAC[] THEN
 686      MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_NODE_LIST) THEN
 687      ASM_REWRITE_TAC[] THEN
 688      DISCH_THEN (fun th -> REWRITE_TAC[th]));;
 689
 690
 691 let CARD_SET_OF_LIST_NODE = prove(`!(L:((A)list)list) n. good_list L /\ MEM n (list_of_nodes L)
 692                                     ==> CARD(set_of_list n) = LENGTH n`,
 693    REPEAT STRIP_TAC THEN
 694      MATCH_MP_TAC CARD_SET_OF_LIST_ALL_DISTINCT THEN
 695      MATCH_MP_TAC ALL_DISTINCT_NODE THEN
 696      EXISTS_TAC `L:((A)list)list` THEN ASM_REWRITE_TAC[]);;
 697
 698
 699
 700
 701
 702 let SUM_FACE_LIST = prove(`!L (f:(A#A)list). good_list L /\ MEM f (list_of_faces L) ==>
 703                             sum (set_of_list f) = list_sum f`,
 704    REPEAT STRIP_TAC THEN
 705      REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `r:(A#A)->real` THEN
 706      MP_TAC (ISPECL [`r:A#A->real`; `f:(A#A)list`] ALL_DISTINCT_SUM) THEN
 707      ANTS_TAC THENL
 708      [
 709        MATCH_MP_TAC ALL_DISTINCT_FACE THEN
 710          EXISTS_TAC `L:((A)list)list` THEN
 711          ASM_REWRITE_TAC[];
 712        ALL_TAC
 713      ] THEN
 714      REWRITE_TAC[]);;
 715
 716
 717
 718 let SUM_FACE_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
 719                             ((!f. f IN face_set (hypermap_of_list L) ==> P f (sum f))
 720                             <=> (!f. MEM f (list_of_faces L) ==> P (set_of_list f) (list_sum f)))`,
 721    REPEAT STRIP_TAC THEN
 722      ASM_SIMP_TAC[FACE_SET_EQ_LIST] THEN
 723      ASM_REWRITE_TAC[IN_SET_OF_LIST; faces_of_list] THEN
 724      EQ_TAC THEN REPEAT STRIP_TAC THENL
 725      [
 726        FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
 727          REWRITE_TAC[MEM_MAP] THEN
 728          ANTS_TAC THENL
 729          [
 730            EXISTS_TAC `f:(A#A)list` THEN
 731              ASM_REWRITE_TAC[];
 732            ALL_TAC
 733          ] THEN
 734
 735          MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
 736          ASM_REWRITE_TAC[] THEN
 737          DISCH_THEN (fun th -> REWRITE_TAC[th]);
 738        ALL_TAC
 739      ] THEN
 740
 741      POP_ASSUM MP_TAC THEN
 742      REWRITE_TAC[MEM_MAP] THEN
 743      STRIP_TAC THEN
 744      FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
 745      ASM_REWRITE_TAC[] THEN
 746      MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
 747      ASM_REWRITE_TAC[] THEN
 748      DISCH_THEN (fun th -> REWRITE_TAC[th]));;
 749
 750
 751
 752 let CARD_SET_OF_LIST_FACE = prove(`!(L:((A)list)list) f. good_list L /\ MEM f (list_of_faces L)
 753                                     ==> CARD(set_of_list f) = LENGTH f`,
 754    REPEAT STRIP_TAC THEN
 755      MATCH_MP_TAC CARD_SET_OF_LIST_ALL_DISTINCT THEN
 756      MATCH_MP_TAC ALL_DISTINCT_FACE THEN
 757      EXISTS_TAC `L:((A)list)list` THEN ASM_REWRITE_TAC[]);;
 758
 759
 760 let IN_DART3_IMP_IN_DART = UNDISCH_ALL (prove(`d:B IN hyp_dart3 G ==> d IN dart G`,
 761                                               SIMP_TAC[hyp_dart3; IN_ELIM_THM]));;
 762 let IN_DART4_IMP_IN_DART = UNDISCH_ALL (prove(`d:B IN hyp_dart4 G ==> d IN dart G`,
 763                                               SIMP_TAC[hyp_dart4; IN_ELIM_THM]));;
 764
 765 let IN_FACE3_IMP_IN_FACE = UNDISCH_ALL (prove(`f IN hyp_face3 (G:(B)hypermap) ==> f IN face_set G`,
 766                                               SIMP_TAC[hyp_face3; IN_ELIM_THM]));;
 767 let IN_FACE4_IMP_IN_FACE = UNDISCH_ALL (prove(`f IN hyp_face4 (G:(B)hypermap) ==> f IN face_set G`,
 768                                               SIMP_TAC[hyp_face4; IN_ELIM_THM]));;
 769 let IN_FACE5_IMP_IN_FACE = UNDISCH_ALL (prove(`f IN hyp_face5 (G:(B)hypermap) ==> f IN face_set G`,
 770                                               SIMP_TAC[hyp_face5; IN_ELIM_THM]));;
 771 let IN_FACE6_IMP_IN_FACE = UNDISCH_ALL (prove(`f IN hyp_face6 (G:(B)hypermap) ==> f IN face_set G`,
 772                                               SIMP_TAC[hyp_face6; IN_ELIM_THM]));;
 773
 774
 775
 776
 777 let DART_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
 778                             ((!d. d IN dart (hypermap_of_list L) ==> P d)
 779                         <=> (!d. MEM d (list_of_darts L) ==> P d))`,
 780    REPEAT STRIP_TAC THEN
 781      ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST; darts_of_list; IN_SET_OF_LIST]);;
 782
 783
 784 let DART3_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
 785                              ((!d. d IN hyp_dart3 (hypermap_of_list L) ==> P d)
 786                                 <=> (!d. MEM d (list_of_darts3 L) ==> P d))`,
 787    REPEAT STRIP_TAC THEN ASM_SIMP_TAC[LIST_OF_DARTS3; IN_SET_OF_LIST]);;
 788
 789
 790
 791 let DART4_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
 792                              ((!d. d IN hyp_dart4 (hypermap_of_list L) ==> P d)
 793                                 <=> (!d. MEM d (list_of_darts4 L) ==> P d))`,
 794    REPEAT STRIP_TAC THEN ASM_SIMP_TAC[LIST_OF_DARTS4; IN_SET_OF_LIST]);;
 795
 796
 797 let DARTX_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
 798                              ((!d. d IN hyp_dartX (hypermap_of_list L) ==> P d)
 799                                 <=> (!d. MEM d (list_of_dartsX L) ==> P d))`,
 800    REPEAT STRIP_TAC THEN ASM_SIMP_TAC[LIST_OF_DARTS_X; IN_SET_OF_LIST]);;
 801
 802
 803
 804 let FACE3_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
 805                              ((!f. f IN hyp_face3 (hypermap_of_list L) ==> P f (sum f))
 806                                 <=> (!f. MEM f (list_of_faces3 L) ==> P (set_of_list f) (list_sum f)))`,
 807    REPEAT STRIP_TAC THEN
 808      ASM_SIMP_TAC[LIST_OF_FACES3] THEN
 809      ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM_MAP] THEN
 810      EQ_TAC THEN REPEAT STRIP_TAC THENL
 811      [
 812        FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
 813          ANTS_TAC THENL
 814          [
 815            EXISTS_TAC `f:(A#A)list` THEN
 816              ASM_REWRITE_TAC[];
 817            ALL_TAC
 818          ] THEN
 819
 820          MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
 821          ANTS_TAC THENL
 822          [
 823            ASM_REWRITE_TAC[] THEN
 824              POP_ASSUM MP_TAC THEN
 825              SIMP_TAC[list_of_faces3; MEM_FILTER];
 826            ALL_TAC
 827          ] THEN
 828          DISCH_THEN (fun th -> REWRITE_TAC[th]);
 829        ALL_TAC
 830      ] THEN
 831
 832      FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
 833      ASM_REWRITE_TAC[] THEN
 834      MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
 835      ANTS_TAC THENL
 836      [
 837        ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 838          SIMP_TAC[list_of_faces3; MEM_FILTER];
 839        ALL_TAC
 840      ] THEN
 841      DISCH_THEN (fun th -> REWRITE_TAC[th]));;
 842
 843
 844
 845 let FACE4_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
 846                              ((!f. f IN hyp_face4 (hypermap_of_list L) ==> P f (sum f))
 847                                 <=> (!f. MEM f (list_of_faces4 L) ==> P (set_of_list f) (list_sum f)))`,
 848    REPEAT STRIP_TAC THEN
 849      ASM_SIMP_TAC[LIST_OF_FACES4] THEN
 850      ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM_MAP] THEN
 851      EQ_TAC THEN REPEAT STRIP_TAC THENL
 852      [
 853        FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
 854          ANTS_TAC THENL
 855          [
 856            EXISTS_TAC `f:(A#A)list` THEN
 857              ASM_REWRITE_TAC[];
 858            ALL_TAC
 859          ] THEN
 860
 861          MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
 862          ANTS_TAC THENL
 863          [
 864            ASM_REWRITE_TAC[] THEN
 865              POP_ASSUM MP_TAC THEN
 866              SIMP_TAC[list_of_faces4; MEM_FILTER];
 867            ALL_TAC
 868          ] THEN
 869          DISCH_THEN (fun th -> REWRITE_TAC[th]);
 870        ALL_TAC
 871      ] THEN
 872
 873      FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
 874      ASM_REWRITE_TAC[] THEN
 875      MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
 876      ANTS_TAC THENL
 877      [
 878        ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 879          SIMP_TAC[list_of_faces4; MEM_FILTER];
 880        ALL_TAC
 881      ] THEN
 882      DISCH_THEN (fun th -> REWRITE_TAC[th]));;
 883
 884
 885 let FACE5_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
 886                              ((!f. f IN hyp_face5 (hypermap_of_list L) ==> P f (sum f))
 887                                 <=> (!f. MEM f (list_of_faces5 L) ==> P (set_of_list f) (list_sum f)))`,
 888    REPEAT STRIP_TAC THEN
 889      ASM_SIMP_TAC[LIST_OF_FACES5] THEN
 890      ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM_MAP] THEN
 891      EQ_TAC THEN REPEAT STRIP_TAC THENL
 892      [
 893        FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
 894          ANTS_TAC THENL
 895          [
 896            EXISTS_TAC `f:(A#A)list` THEN
 897              ASM_REWRITE_TAC[];
 898            ALL_TAC
 899          ] THEN
 900
 901          MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
 902          ANTS_TAC THENL
 903          [
 904            ASM_REWRITE_TAC[] THEN
 905              POP_ASSUM MP_TAC THEN
 906              SIMP_TAC[list_of_faces5; MEM_FILTER];
 907            ALL_TAC
 908          ] THEN
 909          DISCH_THEN (fun th -> REWRITE_TAC[th]);
 910        ALL_TAC
 911      ] THEN
 912
 913      FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
 914      ASM_REWRITE_TAC[] THEN
 915      MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
 916      ANTS_TAC THENL
 917      [
 918        ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 919          SIMP_TAC[list_of_faces5; MEM_FILTER];
 920        ALL_TAC
 921      ] THEN
 922      DISCH_THEN (fun th -> REWRITE_TAC[th]));;
 923
 924
 925 let FACE6_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
 926                              ((!f. f IN hyp_face6 (hypermap_of_list L) ==> P f (sum f))
 927                                 <=> (!f. MEM f (list_of_faces6 L) ==> P (set_of_list f) (list_sum f)))`,
 928    REPEAT STRIP_TAC THEN
 929      ASM_SIMP_TAC[LIST_OF_FACES6] THEN
 930      ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM_MAP] THEN
 931      EQ_TAC THEN REPEAT STRIP_TAC THENL
 932      [
 933        FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
 934          ANTS_TAC THENL
 935          [
 936            EXISTS_TAC `f:(A#A)list` THEN
 937              ASM_REWRITE_TAC[];
 938            ALL_TAC
 939          ] THEN
 940
 941          MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
 942          ANTS_TAC THENL
 943          [
 944            ASM_REWRITE_TAC[] THEN
 945              POP_ASSUM MP_TAC THEN
 946              SIMP_TAC[list_of_faces6; MEM_FILTER];
 947            ALL_TAC
 948          ] THEN
 949          DISCH_THEN (fun th -> REWRITE_TAC[th]);
 950        ALL_TAC
 951      ] THEN
 952
 953      FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
 954      ASM_REWRITE_TAC[] THEN
 955      MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
 956      ANTS_TAC THENL
 957      [
 958        ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
 959          SIMP_TAC[list_of_faces6; MEM_FILTER];
 960        ALL_TAC
 961      ] THEN
 962      DISCH_THEN (fun th -> REWRITE_TAC[th]));;
 963
 964
 965
 966 let EDGE_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
 967                             ((!e. e IN hyp_edge_pairs (hypermap_of_list L) ==> P e)
 968                        <=> (!e. MEM e (list_of_edges L) ==> P e))`,
 969    REPEAT STRIP_TAC THEN
 970      ASM_SIMP_TAC[LIST_OF_EDGES; IN_SET_OF_LIST]);;
 971
 972
 973 let SUB_CONST_o = prove(`!f (c:real) (g:B->A). (\x. f x - c) o g  = (\x. (f o g) x - c)`,
 974    REWRITE_TAC[FUN_EQ_THM; o_THM]);;
 975
 976
 977 (*******************************)
 978
 979
 980 let in_all_rewrites =
 981 [
 982   SUM_NODE_LIST_ALL;
 983   SUM_FACE_LIST_ALL;
 984   EDGE_LIST_ALL;
 985   DART_LIST_ALL;
 986   DART3_LIST_ALL;
 987   DART4_LIST_ALL;
 988   DARTX_LIST_ALL;
 989   FACE3_LIST_ALL;
 990   FACE4_LIST_ALL;
 991   FACE5_LIST_ALL;
 992   FACE6_LIST_ALL;
 993 ];;
 994
 995
 996
 997 let table_set_hyp =
 998   let table = Hashtbl.create 10 in
 999   let _ = map (uncurry (Hashtbl.add table))
1000       [
1001         `hyp_dart3 (G:(B)hypermap)`, IN_DART3_IMP_IN_DART;
1002         `hyp_dart4 (G:(B)hypermap)`, IN_DART4_IMP_IN_DART;
1003         `hyp_face3 (G:(B)hypermap)`, IN_FACE3_IMP_IN_FACE;
1004         `hyp_face4 (G:(B)hypermap)`, IN_FACE4_IMP_IN_FACE;
1005         `hyp_face5 (G:(B)hypermap)`, IN_FACE5_IMP_IN_FACE;
1006         `hyp_face6 (G:(B)hypermap)`, IN_FACE6_IMP_IN_FACE;
1007       ] in
1008     table;;
1009
1010
1011
1012 (*************************************)
1013
1014
1015 let iso_dart_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1016                              ((!d. d IN dart H ==> P d) ==> (!d. d IN dart G ==> P (g d)))`,
1017    REWRITE_TAC[isomorphism; BIJ; SURJ] THEN
1018      REPEAT STRIP_TAC THEN
1019      FIRST_X_ASSUM (MP_TAC o SPEC `d:B`) THEN
1020      FIRST_X_ASSUM (MP_TAC o SPEC `d:B`) THEN
1021      ASM_REWRITE_TAC[] THEN
1022      DISCH_TAC THEN
1023      FIRST_X_ASSUM (MP_TAC o SPEC `(g:B->A) d`) THEN
1024      ASM_SIMP_TAC[]);;
1025
1026
1027 let iso_dart_in = prove(`!(g:B->A) H G d. isomorphism g (G,H) /\ d IN dart G ==>
1028                           g d IN dart H`,
1029    REWRITE_TAC[isomorphism; BIJ; SURJ; INJ] THEN
1030      REPEAT STRIP_TAC THEN
1031      ASM_SIMP_TAC[]);;
1032
1033
1034
1035 let iso_card_eq = prove(`!(g:B->A) H G s. isomorphism g (G,H) /\ s SUBSET dart G
1036                           ==> CARD (IMAGE g s) = CARD s`,
1037    REWRITE_TAC[isomorphism; BIJ; INJ] THEN
1038      REPEAT STRIP_TAC THEN
1039      MATCH_MP_TAC CARD_IMAGE_INJ THEN
1040      CONJ_TAC THENL
1041      [
1042        REPEAT STRIP_TAC THEN
1043          FIRST_X_ASSUM MATCH_MP_TAC THEN
1044          ASM_REWRITE_TAC[] THEN
1045          CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN EXISTS_TAC `s:B->bool` THEN ASM_REWRITE_TAC[];
1046        ALL_TAC
1047      ] THEN
1048      MATCH_MP_TAC FINITE_SUBSET THEN
1049      EXISTS_TAC `dart G:B->bool` THEN
1050      ASM_REWRITE_TAC[Hypermap.hypermap_lemma]);;
1051
1052
1053 let iso_face_card = prove(`!(g:B->A) H G d. isomorphism g (G,H) /\ d IN dart G
1054                                   ==> CARD (face H (g d)) = CARD (face G d)`,
1055    REPEAT STRIP_TAC THEN
1056      MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
1057      ASM_REWRITE_TAC[] THEN
1058      DISCH_THEN (MP_TAC o SPEC `d:B`) THEN
1059      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1060      ASM_REWRITE_TAC[] THEN
1061      MATCH_MP_TAC iso_card_eq THEN
1062      MAP_EVERY EXISTS_TAC [`H:(A)hypermap`; `G:(B)hypermap`] THEN
1063      ASM_SIMP_TAC[Hypermap.lemma_face_subset]);;
1064
1065
1066 let iso_dart3_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1067                 ((!d. d IN hyp_dart3 H ==> P d) ==> (!d. d IN hyp_dart3 G ==> P (g d)))`,
1068    REWRITE_TAC[hyp_dart3; IN_ELIM_THM] THEN
1069      REPEAT STRIP_TAC THEN
1070      FIRST_X_ASSUM MATCH_MP_TAC THEN
1071      MP_TAC (SPEC_ALL iso_dart_in) THEN
1072      ASM_SIMP_TAC[iso_face_card]);;
1073
1074
1075
1076 let iso_dart4_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1077                 ((!d. d IN hyp_dart4 H ==> P d) ==> (!d. d IN hyp_dart4 G ==> P (g d)))`,
1078    REWRITE_TAC[hyp_dart4; IN_ELIM_THM] THEN
1079      REPEAT STRIP_TAC THEN
1080      FIRST_X_ASSUM MATCH_MP_TAC THEN
1081      MP_TAC (SPEC_ALL iso_dart_in) THEN
1082      ASM_SIMP_TAC[iso_face_card]);;
1083
1084
1085
1086 let iso_dartX_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1087                 ((!d. d IN hyp_dartX H ==> P d) ==> (!d. d IN hyp_dartX G ==> P (g d)))`,
1088    REWRITE_TAC[hyp_dartX; IN_ELIM_THM] THEN
1089      REPEAT STRIP_TAC THEN
1090      FIRST_X_ASSUM MATCH_MP_TAC THEN
1091      MP_TAC (SPEC_ALL iso_dart_in) THEN
1092      ASM_SIMP_TAC[iso_face_card]);;
1093
1094
1095
1096
1097 let iso_edge_pairs_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1098                   ((!e. e IN hyp_edge_pairs H ==> P e) ==> (!e. e IN hyp_edge_pairs G ==> P (g (FST e), g (SND e))))`,
1099    REWRITE_TAC[isomorphism; BIJ; SURJ; hyp_edge_pairs; IN_ELIM_THM] THEN
1100      REPEAT STRIP_TAC THEN
1101      ASM_REWRITE_TAC[] THEN
1102      FIRST_X_ASSUM MATCH_MP_TAC THEN
1103      EXISTS_TAC `(g:B->A) x` THEN
1104      ASM_SIMP_TAC[]);;
1105
1106
1107
1108
1109 let iso_node_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1110                              ((!n. n IN node_set H ==> P n) ==> (!n. n IN node_set G ==> P (IMAGE g n)))`,
1111    REPEAT STRIP_TAC THEN
1112      POP_ASSUM (MP_TAC o MATCH_MP Hypermap.lemma_node_representation) THEN
1113      STRIP_TAC THEN
1114      MP_TAC (ISPECL [`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `x:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
1115      ASM_REWRITE_TAC[] THEN
1116      DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
1117      FIRST_X_ASSUM MATCH_MP_TAC THEN
1118      REWRITE_TAC[GSYM Hypermap.lemma_in_node_set] THEN
1119      MATCH_MP_TAC iso_dart_in THEN
1120      EXISTS_TAC `G:(B)hypermap` THEN
1121      ASM_REWRITE_TAC[]);;
1122
1123
1124
1125 let iso_face_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1126                              ((!f. f IN face_set H ==> P f) ==> (!f. f IN face_set G ==> P (IMAGE g f)))`,
1127    REPEAT STRIP_TAC THEN
1128      POP_ASSUM (MP_TAC o MATCH_MP Hypermap.lemma_face_representation) THEN
1129      STRIP_TAC THEN
1130      MP_TAC (ISPECL [`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `x:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
1131      ASM_REWRITE_TAC[] THEN
1132      DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
1133      FIRST_X_ASSUM MATCH_MP_TAC THEN
1134      REWRITE_TAC[GSYM Hypermap.lemma_in_face_set] THEN
1135      MATCH_MP_TAC iso_dart_in THEN
1136      EXISTS_TAC `G:(B)hypermap` THEN
1137      ASM_REWRITE_TAC[]);;
1138
1139
1140 let iso_face3_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1141               ((!f. f IN hyp_face3 H ==> P f) ==> (!f. f IN hyp_face3 G ==> P (IMAGE g f)))`,
1142    REWRITE_TAC[hyp_face3; IN_ELIM_THM] THEN
1143      REPEAT STRIP_TAC THEN
1144      FIRST_X_ASSUM MATCH_MP_TAC THEN
1145      POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1146      MP_TAC (SPECL[`g:B->A`; `H:(A)hypermap`; `G:(B)hypermap`] iso_face_trans) THEN
1147      ASM_REWRITE_TAC[] THEN
1148      REPEAT DISCH_TAC THEN
1149      CONJ_TAC THENL
1150      [
1151        REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
1152          SPEC_TAC (`f:B->bool`, `f:B->bool`) THEN
1153          FIRST_X_ASSUM MATCH_MP_TAC THEN
1154          SIMP_TAC[];
1155        ALL_TAC
1156      ] THEN
1157
1158      MP_TAC (ISPECL[`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
1159      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1160      UNDISCH_TAC `CARD (f:B->bool) = 3` THEN
1161      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1162      ASM_REWRITE_TAC[] THEN
1163
1164      MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
1165      ASM_REWRITE_TAC[] THEN
1166      DISCH_THEN (fun th -> ASM_SIMP_TAC[GSYM th]) THEN
1167      MATCH_MP_TAC iso_face_card THEN
1168      ASM_REWRITE_TAC[]);;
1169
1170
1171 let iso_face4_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1172               ((!f. f IN hyp_face4 H ==> P f) ==> (!f. f IN hyp_face4 G ==> P (IMAGE g f)))`,
1173    REWRITE_TAC[hyp_face4; IN_ELIM_THM] THEN
1174      REPEAT STRIP_TAC THEN
1175      FIRST_X_ASSUM MATCH_MP_TAC THEN
1176      POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1177      MP_TAC (SPECL[`g:B->A`; `H:(A)hypermap`; `G:(B)hypermap`] iso_face_trans) THEN
1178      ASM_REWRITE_TAC[] THEN
1179      REPEAT DISCH_TAC THEN
1180      CONJ_TAC THENL
1181      [
1182        REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
1183          SPEC_TAC (`f:B->bool`, `f:B->bool`) THEN
1184          FIRST_X_ASSUM MATCH_MP_TAC THEN
1185          SIMP_TAC[];
1186        ALL_TAC
1187      ] THEN
1188
1189      MP_TAC (ISPECL[`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
1190      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1191      UNDISCH_TAC `CARD (f:B->bool) = 4` THEN
1192      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1193      ASM_REWRITE_TAC[] THEN
1194
1195      MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
1196      ASM_REWRITE_TAC[] THEN
1197      DISCH_THEN (fun th -> ASM_SIMP_TAC[GSYM th]) THEN
1198      MATCH_MP_TAC iso_face_card THEN
1199      ASM_REWRITE_TAC[]);;
1200
1201
1202 let iso_face5_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1203               ((!f. f IN hyp_face5 H ==> P f) ==> (!f. f IN hyp_face5 G ==> P (IMAGE g f)))`,
1204    REWRITE_TAC[hyp_face5; IN_ELIM_THM] THEN
1205      REPEAT STRIP_TAC THEN
1206      FIRST_X_ASSUM MATCH_MP_TAC THEN
1207      POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1208      MP_TAC (SPECL[`g:B->A`; `H:(A)hypermap`; `G:(B)hypermap`] iso_face_trans) THEN
1209      ASM_REWRITE_TAC[] THEN
1210      REPEAT DISCH_TAC THEN
1211      CONJ_TAC THENL
1212      [
1213        REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
1214          SPEC_TAC (`f:B->bool`, `f:B->bool`) THEN
1215          FIRST_X_ASSUM MATCH_MP_TAC THEN
1216          SIMP_TAC[];
1217        ALL_TAC
1218      ] THEN
1219
1220      MP_TAC (ISPECL[`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
1221      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1222      UNDISCH_TAC `CARD (f:B->bool) = 5` THEN
1223      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1224      ASM_REWRITE_TAC[] THEN
1225
1226      MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
1227      ASM_REWRITE_TAC[] THEN
1228      DISCH_THEN (fun th -> ASM_SIMP_TAC[GSYM th]) THEN
1229      MATCH_MP_TAC iso_face_card THEN
1230      ASM_REWRITE_TAC[]);;
1231
1232
1233 let iso_face6_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1234               ((!f. f IN hyp_face6 H ==> P f) ==> (!f. f IN hyp_face6 G ==> P (IMAGE g f)))`,
1235    REWRITE_TAC[hyp_face6; IN_ELIM_THM] THEN
1236      REPEAT STRIP_TAC THEN
1237      FIRST_X_ASSUM MATCH_MP_TAC THEN
1238      POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1239      MP_TAC (SPECL[`g:B->A`; `H:(A)hypermap`; `G:(B)hypermap`] iso_face_trans) THEN
1240      ASM_REWRITE_TAC[] THEN
1241      REPEAT DISCH_TAC THEN
1242      CONJ_TAC THENL
1243      [
1244        REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
1245          SPEC_TAC (`f:B->bool`, `f:B->bool`) THEN
1246          FIRST_X_ASSUM MATCH_MP_TAC THEN
1247          SIMP_TAC[];
1248        ALL_TAC
1249      ] THEN
1250
1251      MP_TAC (ISPECL[`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
1252      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1253      UNDISCH_TAC `CARD (f:B->bool) = 6` THEN
1254      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1255      ASM_REWRITE_TAC[] THEN
1256
1257      MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
1258      ASM_REWRITE_TAC[] THEN
1259      DISCH_THEN (fun th -> ASM_SIMP_TAC[GSYM th]) THEN
1260      MATCH_MP_TAC iso_face_card THEN
1261      ASM_REWRITE_TAC[]);;
1262
1263
1264
1265
1266 let iso_trans_table =
1267   let table = Hashtbl.create 10 in
1268   let _ = map (uncurry (Hashtbl.add table))
1269     [
1270       `dart H:A->bool`, iso_dart_trans;
1271       `node_set (H:(A)hypermap)`, iso_node_trans;
1272       `face_set (H:(A)hypermap)`, iso_face_trans;
1273       `hyp_edge_pairs (H:(A)hypermap)`, iso_edge_pairs_trans;
1274       `hyp_dart3 (H:(A)hypermap)`, iso_dart3_trans;
1275       `hyp_dart4 (H:(A)hypermap)`, iso_dart4_trans;
1276       `hyp_dartX (H:(A)hypermap)`, iso_dartX_trans;
1277       `hyp_face3 (H:(A)hypermap)`, iso_face3_trans;
1278       `hyp_face4 (H:(A)hypermap)`, iso_face4_trans;
1279       `hyp_face5 (H:(A)hypermap)`, iso_face5_trans;
1280       `hyp_face6 (H:(A)hypermap)`, iso_face6_trans;
1281     ] in
1282     table;;
1283
1284
1285 (**************************)
1286
1287
1288
1289 let gen_iso_thm ineq =
1290   let x_tm, tm = dest_forall ineq in
1291   let set, p_tm' = dest_binary "==>" tm in
1292   let set_th = Hashtbl.find iso_trans_table (rand set) in
1293   let p_tm = mk_abs (x_tm, p_tm') in
1294   let p_var = mk_var ("P", type_of (rand set)) in
1295   let th3 = (SPEC_ALL (REWRITE_RULE[IMP_IMP] set_th)) in
1296     BETA_RULE (INST[p_tm, p_var] th3);;
1297
1298
1299
1300
1301
1302
1303 let gen_general_ineq ineq =
1304   let iso_th = gen_iso_thm ineq in
1305     (* General rewrites before specifying hypermaps *)
1306   let th0 = UNDISCH_ALL (REWRITE_RULE[GSYM IMP_IMP] iso_th) in
1307   let gen_var, rtm = dest_forall(concl th0) in
1308   let ants = lhand rtm in
1309   let set = rand ants in
1310   let th1 = UNDISCH_ALL (SPEC_ALL th0) in
1311
1312   let th_rule th = UNDISCH_ALL (SPEC_ALL (UNDISCH_ALL (SPEC_ALL th))) in
1313
1314   let ths = [
1315     th_rule SUM_NODE_ISO;
1316     th_rule CARD_NODE_ISO;
1317     th_rule SUM_FACE_ISO;
1318     th_rule CARD_FACE_ISO;
1319     th_rule COMPONENTS_ISO_IMAGE;
1320     th_rule HYPERMAP_MAPS_ISO_IMAGE;
1321     th_rule HYPERMAP_INV_MAPS_ISO_IMAGE;
1322     th_rule HYPERMAP_MAPS_ISO_COMM;
1323     th_rule HYPERMAP_INV_MAPS_ISO_COMM;
1324     SUB_CONST_o; ETA_AX;
1325     th_rule SUM_FACE_SUB_CONST;
1326   ] in
1327
1328   let th2' = REWRITE_RULE ths th1 in
1329   let th2 =
1330     if (Hashtbl.mem table_set_hyp set) then
1331       PROVE_HYP (Hashtbl.find table_set_hyp set) th2'
1332     else
1333       th2' in
1334   let th3 = GEN gen_var (DISCH ants th2) in
1335
1336   let s0 = th3 in
1337
1338   (* G -> hypermap_of_list (L:((num)list)list) *)
1339   (* Instantiate correct types *)
1340   let s1 = INST_TYPE [`:real^3#real^3`, aty; `:num#num`, bty] s0 in
1341   let s2 = INST[`hypermap_of_list (L:((num)list)list)`, `G:(num#num)hypermap`] s1 in
1342
1343   let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty] o SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP]) in
1344
1345   let ths = map th_rule in_all_rewrites in
1346   let s3 = REWRITE_RULE ths s2 in
1347
1348   let gen_var2, rtm = dest_forall(concl s3) in
1349   let ants2 = lhand rtm in
1350
1351   let s4 = UNDISCH_ALL (SPEC_ALL s3) in
1352
1353   let ths =
1354     [
1355       th_rule CARD_SET_OF_LIST_FACE;
1356       th_rule CARD_SET_OF_LIST_NODE;
1357     ] in
1358
1359   let s5 = REWRITE_RULE ths s4 in
1360   let s6 = GEN gen_var2 (DISCH ants2 s5) in
1361
1362   (* Deal with basic variables *)
1363   let s7 = INST var_list s6 in
1364   let s8 = INST[`ESTD V`, `E:(real^3->bool)->bool`] s7 in
1365   let s9 = REWRITE_RULE list_var_rewrites s8 in
1366   let r0 = s9 in
1367
1368   (* Basic rewrites *)
1369
1370   let ths =
1371     [
1372       UNDISCH_ALL (INST_TYPE [`:num`, aty] (SPEC_ALL COMPONENTS_HYPERMAP_OF_LIST));
1373     ] in
1374   let r1 = REWRITE_RULE ths r0 in
1375
1376   (* Further rewrites *)
1377   let r2 = REWRITE_RULE[darts_of_list; IN_SET_OF_LIST; ALL_MEM] r1 in
1378     r2;;
1379
1380
1381
1382 (***********************)
1383
1384
1385 (*
1386
1387 let get_ineq str = Hashtbl.find constraints str;;
1388
1389
1390
1391 let th = gen_general_ineq (get_ineq "ineq122");;
1392 let th = gen_general_ineq (get_ineq "sol_sum3");;
1393 let th = gen_general_ineq (get_ineq "tau_sum");;
1394 let th = gen_general_ineq (get_ineq "edge_sym");;
1395 let th = gen_general_ineq (get_ineq "ln_def");;
1396 let th = gen_general_ineq (get_ineq "y1_def");;
1397 let th = gen_general_ineq (get_ineq "y2_def");;
1398 let th = gen_general_ineq (get_ineq "y3_def");;
1399 let th = gen_general_ineq (get_ineq "y4_def");;
1400 let th = gen_general_ineq (get_ineq "y5_def");;
1401 let th = gen_general_ineq (get_ineq "y6_def");;
1402 let th = gen_general_ineq (get_ineq "y8_def");;
1403 let th = gen_general_ineq (get_ineq "y9_def");;
1404 let th = gen_general_ineq (get_ineq "RHB");;
1405
1406
1407
1408 let test_list = ref [];;
1409
1410 let iter_f name ineq =
1411   try
1412     test_list := gen_general_ineq ineq :: !test_list
1413   with x ->
1414     print_string ("problems: "^name^"; ");;
1415
1416
1417 Hashtbl.iter iter_f constraints;;
1418
1419
1420
1421
1422 (********************************)
1423
1424 let ineq = get_ineq "tau_sum3";;
1425
1426 let iso_th = gen_iso_thm ineq;;
1427     (* General rewrites before specifying hypermaps *)
1428 let th0 = UNDISCH_ALL (REWRITE_RULE[GSYM IMP_IMP] iso_th);;
1429 let gen_var, rtm = dest_forall(concl th0);;
1430 let ants = lhand rtm;;
1431 let set = rand ants;;
1432 let th1 = UNDISCH_ALL (SPEC_ALL th0);;
1433
1434 let th_rule th = UNDISCH_ALL (SPEC_ALL (UNDISCH_ALL (SPEC_ALL th)));;
1435
1436 let ths = [
1437     th_rule SUM_NODE_ISO;
1438     th_rule CARD_NODE_ISO;
1439     th_rule SUM_FACE_ISO;
1440     th_rule CARD_FACE_ISO;
1441     th_rule COMPONENTS_ISO_IMAGE;
1442     th_rule HYPERMAP_MAPS_ISO_IMAGE;
1443     th_rule HYPERMAP_INV_MAPS_ISO_IMAGE;
1444     th_rule HYPERMAP_MAPS_ISO_COMM;
1445     th_rule HYPERMAP_INV_MAPS_ISO_COMM;
1446     SUB_CONST_o; ETA_AX;
1447     th_rule SUM_FACE_SUB_CONST;
1448 ];;
1449
1450 let th2' = REWRITE_RULE ths th1;;
1451 let th2 =
1452   if (Hashtbl.mem table_set_hyp set) then
1453     PROVE_HYP (Hashtbl.find table_set_hyp set) th2'
1454   else
1455     th2';;
1456
1457
1458   let th3 = GEN gen_var (DISCH ants th2);;
1459
1460   let s0 = th3;;
1461
1462   (* G -> hypermap_of_list (L:((num)list)list) *)
1463   (* Instantiate correct types *)
1464   let s1 = INST_TYPE [`:real^3#real^3`, aty; `:num#num`, bty] s0;;
1465   let s2 = INST[`hypermap_of_list (L:((num)list)list)`, `G:(num#num)hypermap`] s1;;
1466
1467   let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty] o SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP]);;
1468
1469   let ths = map th_rule in_all_rewrites;;
1470
1471   let s3 = REWRITE_RULE ths s2;;
1472
1473   let gen_var2, rtm = dest_forall(concl s3);;
1474   let ants2 = lhand rtm;;
1475
1476   let s4 = UNDISCH_ALL (SPEC_ALL s3);;
1477
1478   let ths =
1479     [
1480       th_rule CARD_SET_OF_LIST_FACE;
1481       th_rule CARD_SET_OF_LIST_NODE;
1482     ];;
1483
1484   let s5 = REWRITE_RULE ths s4;;
1485   let s6 = GEN gen_var2 (DISCH ants2 s5);;
1486
1487   (* Deal with basic variables *)
1488   let s7 = INST var_list s6;;
1489   let s8 = INST[`ESTD V`, `E:(real^3->bool)->bool`] s7;;
1490   let s9 = REWRITE_RULE list_var_rewrites s8;;
1491   let r0 = s9;;
1492
1493   (* Basic rewrites *)
1494
1495   let ths =
1496     [
1497       UNDISCH_ALL (INST_TYPE [`:num`, aty] (SPEC_ALL COMPONENTS_HYPERMAP_OF_LIST));
1498     ];;
1499   let r1 = REWRITE_RULE ths r0;;
1500
1501   (* Further rewrites *)
1502   let r2 = REWRITE_RULE[darts_of_list; IN_SET_OF_LIST; ALL_MEM] r1
1503     r2;;
1504
1505
1506
1507 *)
1508
1509 (*********************************************************)
1510
1511 (* Integral approximation of inequalities and equalities *)
1512
1513 let neg_op_real = `(--):real->real` and
1514     le_op_real = `(<=):real->real->bool` and
1515     lt_op_real = `(<):real->real->bool` and
1516     ge_op_real = `(>=):real->real->bool` and
1517     plus_op_real = `(+):real->real->real` and
1518     mul_op_real = `( * ):real->real->real`;;
1519
1520 let mk_decimal (n,m) =
1521   let tm = mk_comb(mk_comb(`DECIMAL`, mk_numeral (abs_num n)), mk_numeral m) in
1522     if (n </ Int 0) then mk_comb(neg_op_real, tm) else tm;;
1523
1524
1525 (*
1526 Given a rational number term `r` and a natural number k,
1527 returns a pair of theorems:
1528 |- low <= r, |- r <= high,
1529 with decimal low and high such that
1530 |low - r| <= 10^(-k) and |high - r| <= 10^(-k)
1531 *)
1532 let real_rat_approx tm precision =
1533   let n = rat_of_term tm in
1534   let m = Int 10 **/ (Int precision) in
1535   let n1 = n */ m in
1536   let low, high = floor_num n1, ceiling_num n1 in
1537   let l_tm, h_tm =
1538     if precision = 0 then
1539       term_of_rat low, term_of_rat high
1540     else
1541       mk_decimal (low, m), mk_decimal (high, m) in
1542   let l_th = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op_real l_tm tm)) in
1543   let h_th = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op_real tm h_tm)) in
1544     l_th, h_th;;
1545
1546
1547
1548 (* Split a sum into two parts: with and without free variables *)
1549
1550 let sum_th0 = REAL_ARITH `x = x + &0 + &0` and
1551     sum_th1 = REAL_ARITH `(x + y) + b + c = y + (x + b) + c:real` and
1552     sum_th2 = REAL_ARITH `(x + y) + b + c = y + b + (x + c):real` and
1553     sum_th1' = REAL_ARITH `x + b + c = (x + b) + c:real` and
1554     sum_th2' = REAL_ARITH `x + b + c = b + (x + c):real`;;
1555
1556
1557 let x_var_real = `x:real` and
1558     y_var_real = `y:real` and
1559     b_var_real = `b:real` and
1560     c_var_real = `c:real`;;
1561
1562
1563 let split_sum_conv tm =
1564   let rec split_sum_raw_conv tm =
1565     let xy_tm, bc_tm = dest_binop plus_op_real tm in
1566     let b_tm, c_tm = dest_binop plus_op_real bc_tm in
1567       if (is_binop plus_op_real xy_tm) then
1568         let x_tm, y_tm = dest_binop plus_op_real xy_tm in
1569         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
1570         let th1 = if (frees x_tm <> []) then inst_th sum_th1 else inst_th sum_th2 in
1571         let th2 = split_sum_raw_conv (rand(concl th1)) in
1572           TRANS th1 th2
1573       else
1574         let inst_th = INST[xy_tm, x_var_real; b_tm, b_var_real; c_tm, c_var_real] in
1575           if (frees xy_tm <> []) then inst_th sum_th1' else inst_th sum_th2' in
1576
1577   let th0 = INST[tm, x_var_real] sum_th0 in
1578   let th1 = split_sum_raw_conv (rand(concl th0)) in
1579     TRANS th0 th1;;
1580
1581
1582
1583 let rearrange_mul_conv tm =
1584   let rec dest_mul tm =
1585     if (is_binop mul_op_real tm) then
1586       let lhs, rhs = dest_binop mul_op_real tm in
1587       let cs, vars = dest_mul rhs in
1588         if (frees lhs = []) then
1589           lhs::cs, vars
1590         else
1591           cs, lhs::vars
1592     else
1593       if (frees tm = []) then
1594         [tm], []
1595       else
1596         [], [tm] in
1597   let mk_mul list =
1598     if (list = []) then failwith "rearrange_mul: empty list"
1599     else itlist (fun l r -> mk_binop mul_op_real l r) (tl list) (hd list) in
1600
1601   let cs, vars = dest_mul tm in
1602   let cs_mul, vars_mul = mk_mul cs, mk_mul vars in
1603   let t = mk_eq(tm, mk_binop mul_op_real cs_mul vars_mul) in
1604     EQT_ELIM (REWRITE_CONV[REAL_MUL_AC] t);;
1605
1606
1607
1608 let le_add_th = REAL_ARITH `x + y <= b + c <=> x - b <= c - y:real`;;
1609
1610 (* Moves everything with free variables on the left and performs basic reductions *)
1611 let ineq_rewrite_conv = REWRITE_CONV[real_ge; real_div; DECIMAL] THENC
1612   LAND_CONV REAL_POLY_CONV THENC RAND_CONV REAL_POLY_CONV THENC
1613   LAND_CONV split_sum_conv THENC RAND_CONV split_sum_conv THENC
1614   ONCE_REWRITE_CONV[le_add_th] THENC
1615   LAND_CONV REAL_POLY_CONV THENC RAND_CONV REAL_POLY_CONV THENC
1616   REWRITE_CONV[GSYM real_div] THENC
1617   ONCE_DEPTH_CONV rearrange_mul_conv;;
1618
1619
1620 (* Approximation *)
1621
1622 let le_mul1_th = REAL_ARITH `!x. &1 * x <= x`;;
1623 let ge_mul1_th = REAL_ARITH `!x. x <= &1 * x`;;
1624 let INTERVAL_LO = prove(`interval_arith x (a,b) ==> a <= x`, SIMP_TAC[interval_arith]);;
1625 let INTERVAL_HI = prove(`interval_arith x (a,b) ==> x <= b`, SIMP_TAC[interval_arith]);;
1626
1627 let rec low_approx tm precision =
1628   let low_approx1 tm precision =
1629     if (is_binop mul_op_real tm && frees tm <> []) then
1630       let c, var = dest_binop mul_op_real tm in
1631       let interval_th = approx_interval (create_interval c) precision in
1632       let l_th = MATCH_MP INTERVAL_LO interval_th in
1633       let a, b = dest_binop le_op_real (concl l_th) in
1634         (PROVE_HYP l_th o UNDISCH_ALL o REWRITE_RULE[GSYM IMP_IMP] o SPECL[a; b; var]) REAL_LE_RMUL
1635     else
1636       if (frees tm = []) then
1637         MATCH_MP INTERVAL_LO (approx_interval (create_interval tm) precision)
1638       else
1639         SPEC tm le_mul1_th in
1640
1641   if (is_binop plus_op_real tm && frees tm <> []) then
1642     let lhs, rhs = dest_binop plus_op_real tm in
1643     let l_th = low_approx1 lhs precision in
1644     let r_th = low_approx rhs precision in
1645       MATCH_MP REAL_LE_ADD2 (CONJ l_th r_th)
1646   else
1647     low_approx1 tm precision;;
1648
1649
1650 let rec hi_approx tm precision =
1651   let hi_approx1 tm precision =
1652     if (is_binop mul_op_real tm && frees tm <> []) then
1653       let c, var = dest_binop mul_op_real tm in
1654       let interval_th = approx_interval (create_interval c) precision in
1655       let h_th = MATCH_MP INTERVAL_HI interval_th in
1656       let a, b = dest_binop le_op_real (concl h_th) in
1657         (PROVE_HYP h_th o UNDISCH_ALL o REWRITE_RULE[GSYM IMP_IMP] o SPECL[a; b; var]) REAL_LE_RMUL
1658     else
1659       if (frees tm = []) then
1660         MATCH_MP INTERVAL_HI (approx_interval (create_interval tm) precision)
1661       else
1662         SPEC tm ge_mul1_th in
1663
1664   if (is_binop plus_op_real tm && frees tm <> []) then
1665     let lhs, rhs = dest_binop plus_op_real tm in
1666     let l_th = hi_approx1 lhs precision in
1667     let r_th = hi_approx rhs precision in
1668       MATCH_MP REAL_LE_ADD2 (CONJ l_th r_th)
1669   else
1670     hi_approx1 tm precision;;
1671
1672
1673
1674 let approx_le_ineq precision tm =
1675   let lhs, rhs = dest_binop le_op_real tm in
1676   let lhs_th = low_approx lhs precision in
1677   let rhs_th = hi_approx rhs precision in
1678   let ll, lr = dest_binop le_op_real (concl lhs_th) in
1679   let rl, rr = dest_binop le_op_real (concl rhs_th) in
1680
1681   let th0 = ASSUME tm in
1682   let th1 = SPECL[ll; lr; rhs] REAL_LE_TRANS in
1683   let th2 = SPECL[ll; rhs; rr] REAL_LE_TRANS in
1684   let s1 = MATCH_MP th1 (CONJ lhs_th th0) in
1685     MATCH_MP th2 (CONJ s1 rhs_th);;
1686
1687
1688 let integer_approx_le_ineq precision ineq =
1689   let lhs, rhs = dest_binop le_op_real ineq in
1690   let m = (Int 10 **/ Int precision) in
1691   let m_num, m_real = mk_numeral m, term_of_rat m in
1692   let m_pos = SPEC m_num REAL_POS in
1693   let mul_th = SPECL[m_real; lhs; rhs] REAL_LE_LMUL in
1694   let th0 = MATCH_MP mul_th (CONJ m_pos (ASSUME ineq)) in
1695   let th1 = (CONV_RULE ineq_rewrite_conv) th0 in
1696   let approx = approx_le_ineq 0 (concl th1) in
1697     PROVE_HYP th1 approx;;
1698
1699
1700 let create_approximations precision_list ineq =
1701   let ineq_th = ineq_rewrite_conv ineq in
1702   let rhs = rand(concl ineq_th) in
1703   let th0 = CONV_RULE (LAND_CONV (REWRITE_CONV[DECIMAL] THENC REAL_POLY_CONV))
1704     (approx_le_ineq 8 rhs) in
1705
1706   let int_approx p =
1707     let th1 = integer_approx_le_ineq p (concl th0) in
1708     let th2 = PROVE_HYP th0 th1 in
1709     let th3 = DISCH rhs th2 in
1710       REWRITE_RULE[GSYM ineq_th] th3 in
1711
1712     map int_approx precision_list;;
1713
1714 (**********************************)
1715
1716
1717 (*
1718 let tm = `(&34/ &13 + pi/sol0)* x + &2 + -- &14 / &3 * z <= pi + rho218 + z * sol0 - u / &1000`;;
1719 create_approximations [3;4;5] tm;;
1720 *)
1721
1722
1723 (*************************)
1724
1725 (* Additional step for generalizing hypotheses *)
1726
1727
1728 let LIST_SUM_LMUL = prove(`!(f:A->real) c n. list_sum n (\x. c * f x) = c * list_sum n f`,
1729    GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[list_sum; ITLIST; REAL_MUL_RZERO] THEN
1730      ASM_REWRITE_TAC[GSYM list_sum; REAL_ADD_LDISTRIB]);;
1731
1732
1733 let le_hyp_gen = prove(`!f y. (!x. &0 <= f x) ==> &0 <= f y`, SIMP_TAC[]);;
1734 let le_list_sum_hyp_gen = prove(`!(f:A->real) n. (!x. &0 <= f x) ==> &0 <= list_sum n f`,
1735    REPEAT STRIP_TAC THEN
1736      REWRITE_TAC[list_sum] THEN
1737      SPEC_TAC (`n:(A)list`, `n:(A)list`) THEN
1738      LIST_INDUCT_TAC THEN REWRITE_TAC[ITLIST; REAL_LE_REFL] THEN
1739      MATCH_MP_TAC REAL_LE_ADD THEN
1740      ASM_REWRITE_TAC[]);;
1741
1742
1743
1744 let generalize_hyp th =
1745   let gen_hyp = fun tm ->
1746     let fn, arg = dest_comb (rand tm) in
1747       if (is_comb fn && is_const (rator fn) && (fst o dest_const o rator) fn = "list_sum") then
1748         let f, n = arg, rand fn in
1749           UNDISCH_ALL (ISPECL[f; n] le_list_sum_hyp_gen)
1750       else
1751         UNDISCH_ALL (ISPECL[fn; arg] le_hyp_gen) in
1752
1753   let hyp_ths = map gen_hyp (hyp th) in
1754     itlist PROVE_HYP hyp_ths th;;
1755
1756
1757 (*
1758 let tm = `list_sum n (\x. s x * r) + &1 / &3 * (azim_dart (V,E) o g) x <= pi`;;
1759 let ths = create_approximations [3] tm;;
1760 map generalize_hyp ths;;
1761 *)
1762
1763
1764 (*******************************)
1765
1766
1767 let generate_ineqs precision_list ineq =
1768
1769   let create_approxs original_th precision_list =
1770     let var, ineq = (dest_abs o rand o rator o concl) original_th in
1771     let final_step = fun approx_th ->
1772       let p_tm', q_tm' = dest_imp (concl approx_th) in
1773       let p_tm, q_tm = mk_abs(var, p_tm'), mk_abs(var, q_tm') in
1774       let list_tm = (rand o concl) original_th in
1775       let mono_th = BETA_RULE (ISPECL[p_tm; q_tm; list_tm] (GEN_ALL MONO_ALL)) in
1776       let s1 = MATCH_MP mono_th (GEN var approx_th) in
1777         MATCH_MP s1 original_th in
1778
1779     let approx_ths0 = map generalize_hyp (create_approximations precision_list ineq) in
1780     let approx_ths1 = map (itlist PROVE_HYP list_var_pos) approx_ths0 in
1781     let approx_ths = map (REWRITE_RULE[GSYM LIST_SUM_LMUL]) approx_ths1 in
1782       map final_step approx_ths in
1783
1784
1785   let ineq_th = gen_general_ineq ineq in
1786   let ineq = (snd o dest_abs o rand o rator o concl) ineq_th in
1787     if (is_eq ineq) then
1788       let eq_th = REWRITE_RULE[GSYM REAL_LE_ANTISYM; GSYM AND_ALL] ineq_th in
1789       let ths1 = create_approxs (CONJUNCT1 eq_th) precision_list in
1790       let ths2 = create_approxs (CONJUNCT2 eq_th) precision_list in
1791         ths1, ths2
1792     else
1793       create_approxs ineq_th precision_list, [];;
1794
1795
1796
1797
1798 (*********************************************************************)
1799
1800 (* Table containing all inequalities *)
1801 let ineq_table = Array.init 6 (fun i -> Hashtbl.create 10);;
1802 let ineq_test_table = Array.init 6 (fun i -> Hashtbl.create 10);;
1803
1804
1805
1806 let DECIMAL_INT = prove(`!n. DECIMAL n 1 = &n`, REWRITE_TAC[DECIMAL; REAL_DIV_1]);;
1807
1808
1809 let add_everything_to_table table =
1810   let add_approximations_to_table = fun name ineq ->
1811     let approxs', neg_approxs' = generate_ineqs [3;4;5] ineq in
1812     let approxs = zip (3--5) approxs' in
1813     let neg_approxs = if (neg_approxs' = []) then [] else zip (3--5) neg_approxs' in
1814     let r = CONV_RULE (REWRITE_CONV[DECIMAL_INT] THENC DEPTH_CONV Arith_hash.NUMERAL_TO_NUM_CONV) in
1815     let _ = map (fun (i, t) -> Hashtbl.add (ineq_test_table.(i)) name t;
1816                                Hashtbl.add (ineq_table.(i)) name (r t)) approxs in
1817     let _ = map (fun (i, t) -> Hashtbl.add (ineq_test_table.(i)) (name^"_neg") t;
1818                                Hashtbl.add (ineq_table.(i)) (name^"_neg") (r t)) neg_approxs in
1819       () in
1820
1821     Hashtbl.iter (fun name ineq -> add_approximations_to_table name ineq) table;;
1822
1823
1824 let find_ineq precision name = Hashtbl.find ineq_table.(precision) name;;
1825 let find_test_ineq precision name = Hashtbl.find ineq_test_table.(precision) name;;
1826
1827
1828
1829 (* Generate and add inequalities for constraints *)
1830 add_everything_to_table constraints;;
1831 add_everything_to_table var_bound_ineqs;;
1832
1833
1834 (**************************)
1835
1836
1837 (*
1838 generate_ineqs [4] (get_ineq "ineq112");;
1839
1840 Hashtbl.iter (fun name ineq -> let _ = generate_ineqs[3;4;5] ineq in ()) constraints;;
1841 *)
1842
1843 (***************)
1844 (*********************)
1845