1 needs "../formal_lp/hypermap/list_hypermap.hl";;
2 needs "../formal_lp/hypermap/list_hypermap_iso.hl";;
3 needs "../formal_lp/hypermap/constants_approx.hl";;
8 open Constant_approximations;;
14 (* Definitions of variables *)
17 (* Variables for fans *)
18 (* TODO: these definitions are not necessary *)
20 let azim2_fan = new_definition `azim2_fan (V,E) (x:real^3#real^3) = azim_dart (V,E) (f_fan_pair (V,E) x)`;;
21 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)`;;
22 let yn_fan = new_definition `yn_fan (n:real^3#real^3->bool) = norm (FST (@x. x IN n))`;;
23 let ln_fan = new_definition `ln_fan (n:real^3#real^3->bool) = abs (ly (yn_fan n))`;;
24 let ye_fan = new_definition `ye_fan (x:real^3#real^3) = dist x`;;
26 let y1_fan = new_definition `y1_fan (x:real^3#real^3) = norm(FST x)`;;
27 let y2_fan = new_definition `y2_fan (x:real^3#real^3) = norm(SND x)`;;
28 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))`;;
29 let y4_fan = new_definition `y4_fan (V,E) (x:real^3#real^3) = dist(f_fan_pair (V,E) x)`;;
30 let y5_fan = new_definition `y5_fan (V,E) (x:real^3#real^3) = dist(inverse (f_fan_pair_ext (V,E)) x)`;;
31 let y6_fan = new_definition `y6_fan (x:real^3#real^3) = dist x`;;
32 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)`;;
33 let y9_fan = new_definition `y9_fan (V,E) (x:real^3#real^3) = dist(f_fan_pair (V,E) x)`;;
35 let rhazim_fan = new_definition `rhazim_fan (V,E) (x:real^3#real^3) = abs(rho(y1_fan x)) * azim_dart (V,E) x`;;
36 let rhazim2_fan = new_definition `rhazim2_fan (V,E) (x:real^3#real^3) = rhazim_fan (V,E) (f_fan_pair (V,E) x)`;;
37 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)`;;
39 let rho_fan = new_definition `rho_fan n = abs((&1 + sol0 / pi) - ln_fan n * sol0 / pi)`;;
40 let sol_fan = new_definition `sol_fan (V,E) f = abs(sum f (\x. azim_dart (V,E) x - pi) + &2 * pi)`;;
41 let tau_fan = new_definition `tau_fan (V,E) f = abs (tauVEF (V,E,f))`;;
46 azim2_fan; azim3_fan; yn_fan; ln_fan; ye_fan;
47 rho_fan; sol_fan; tau_fan; rhazim_fan; rhazim2_fan; rhazim3_fan;
48 y1_fan; y2_fan; y3_fan; y4_fan; y5_fan; y6_fan; y8_fan; y9_fan;
53 (* Variables for lists *)
56 let list_defs = map new_definition
58 `azim_list (V,g) = (azim_dart (V,ESTD V) o g):num#num->real`;
59 `azim2_list (V,g) = (azim2_fan (V,ESTD V) o g):num#num->real`;
60 `azim3_list (V,g) = (azim3_fan (V,ESTD V) o g):num#num->real`;
61 `(yn_list g):(num#num->bool)->real = yn_fan o IMAGE g`;
62 `(ln_list g):(num#num->bool)->real = ln_fan o IMAGE g`;
63 `rhazim_list (V,g) = (rhazim_fan (V,ESTD V) o g):num#num->real`;
64 `rhazim2_list (V,g) = (rhazim2_fan (V,ESTD V) o g):num#num->real`;
65 `rhazim3_list (V,g) = (rhazim3_fan (V,ESTD V) o g):num#num->real`;
66 `(ye_list g):(num#num->real) = ye_fan o g`;
67 `(rho_list g):(num#num->bool)->real = rho_fan o IMAGE g`;
68 `(sol_list (V,g)):(num#num->bool)->real = sol_fan (V,ESTD V) o IMAGE g`;
69 `(tau_list (V,g)):(num#num->bool)->real = tau_fan (V,ESTD V) o IMAGE g`;
70 `(y1_list g):(num#num->real) = y1_fan o g`;
71 `(y2_list g):(num#num->real) = y2_fan o g`;
72 `(y3_list (V,g)):(num#num->real) = y3_fan (V,ESTD V) o g`;
73 `(y4_list (V,g)):(num#num->real) = y4_fan (V,ESTD V) o g`;
74 `(y5_list (V,g)):(num#num->real) = y5_fan (V,ESTD V) o g`;
75 `(y6_list g):(num#num->real) = y6_fan o g`;
76 `(y8_list (V,g)):(num#num->real) = y8_fan (V,ESTD V) o g`;
77 `(y9_list (V,g)):(num#num->real) = y9_fan (V,ESTD V) o g`;
81 let list_defs2 = map (REWRITE_RULE[FUN_EQ_THM; o_THM]) list_defs;;
84 let list_var_rewrites =
85 map GSYM list_defs @ map GSYM list_defs2;;
89 (* All variables are nonnegative *)
91 let AZIM_DART_POS = prove(`&0 <= azim_dart (V,E) x`,
92 MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
94 ASM_REWRITE_TAC[azim_dart] THEN
97 MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC;
100 REWRITE_TAC[Fan_defs.azim_fan] THEN
101 COND_CASES_TAC THEN REWRITE_TAC[azim] THEN
102 MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC);;
105 let DIST_POS = prove(`!x:(real^3#real^3). &0 <= dist x`,
106 GEN_TAC THEN MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
107 STRIP_TAC THEN ASM_REWRITE_TAC[dist; NORM_POS_LE]);;
110 let list_var_pos = map (fun tm -> prove(tm,
111 GEN_TAC THEN REWRITE_TAC list_defs2 THEN REWRITE_TAC fan_defs THEN
112 TRY (MATCH_MP_TAC REAL_LE_MUL) THEN
113 REWRITE_TAC[AZIM_DART_POS; REAL_ABS_POS; NORM_POS_LE; DIST_POS]))
115 `!x. &0 <= azim_list (V,g) x`;
116 `!x. &0 <= azim2_list (V,g) x`;
117 `!x. &0 <= azim3_list (V,g) x`;
118 `!x. &0 <= rhazim_list (V,g) x`;
119 `!x. &0 <= rhazim2_list (V,g) x`;
120 `!x. &0 <= rhazim3_list (V,g) x`;
121 `!n. &0 <= yn_list g n`;
122 `!n. &0 <= ln_list g n`;
123 `!e. &0 <= ye_list g e`;
124 `!n. &0 <= rho_list g n`;
125 `!f. &0 <= sol_list (V,g) f`;
126 `!f. &0 <= tau_list (V,g) f`;
127 `!x. &0 <= y1_list g x`;
128 `!x. &0 <= y2_list g x`;
129 `!x. &0 <= y3_list (V,g) x`;
130 `!x. &0 <= y4_list (V,g) x`;
131 `!x. &0 <= y5_list (V,g) x`;
132 `!x. &0 <= y6_list g x`;
133 `!x. &0 <= y8_list (V,g) x`;
134 `!x. &0 <= y9_list (V,g) x`;
139 (* mod-file variables and definitions *)
141 let var_bound_ineqs = Hashtbl.create 40;;
144 ["dart", `dart H:A->bool`;
145 "dart3", `hyp_dart3 H:A->bool`;
146 "node", `node_set H:(A->bool)->bool`;
147 "face", `face_set H:(A->bool)->bool`;
148 "dart_std4", `hyp_dart4 H:A->bool`];;
151 let define_var var_name set_name low high =
152 let var = match set_name with
153 "dart" | "dart3" | "dart_std4" -> `d:A`
154 | "node" -> `n:A->bool`
155 | "face" -> `f:A->bool`
156 | _ -> failwith "Undefined set name" in
157 let var_ty = snd (dest_var var) in
158 let f_ty = mk_type ("fun", [var_ty; `:real`]) in
159 let set_ty = mk_type ("fun", [var_ty; `:bool`]) in
160 let f = mk_var (var_name^"_mod", f_ty) in
161 let set = assoc set_name sets in
162 let in_const = mk_mconst ("IN", mk_type ("fun", [var_ty; mk_type ("fun", [set_ty; `:bool`])])) in
163 let le = `(<=):real->real->bool` in
164 let fvar = mk_comb (f, var) in
165 let l, h = mk_binop le low fvar, mk_binop le fvar high in
166 let cond = mk_binop in_const var set in
168 let ineq_lo = mk_forall(var, mk_imp(cond, l)) in
169 let ineq_hi = mk_forall(var, mk_imp(cond, h)) in
171 let _ = Hashtbl.add var_bound_ineqs (var_name^"_lo") ineq_lo in
172 let _ = Hashtbl.add var_bound_ineqs (var_name^"_hi") ineq_hi in
178 (* Terms for variables in the model file *)
179 Hashtbl.clear var_bound_ineqs;;
181 let azim_mod = define_var "azim" "dart" `&0` `pi` and
182 azim2_mod = define_var "azim2" "dart3" `&0` `pi` and
183 azim3_mod = define_var "azim3" "dart3" `&0` `pi` and
184 ln_mod = define_var "ln" "node" `&0` `&1` and
185 rhazim_mod = define_var "rhazim" "dart" `&0` `pi + sol0` and
186 rhazim2_mod = define_var "rhazim2" "dart3" `&0` `pi + sol0` and
187 rhazim3_mod = define_var "rhazim3" "dart3" `&0` `pi + sol0` and
188 yn_mod = define_var "yn" "node" `&2` `#2.52`and
189 ye_mod = define_var "ye" "dart" `&2` `&3` and
190 rho_mod = define_var "rho" "node" `&1` `&1 + sol0 / pi` and
191 sol_mod = define_var "sol" "face" `&0` `&4 * pi` and
192 tau_mod = define_var "tau" "face" `&0` `tgt` and
193 y1_mod = define_var "y1" "dart" `&2` `#2.52` and
194 y2_mod = define_var "y2" "dart" `&2` `#2.52` and
195 y3_mod = define_var "y3" "dart" `&2` `#2.52` and
196 y4_mod = define_var "y4" "dart3" `&2` `&3` and
197 y5_mod = define_var "y5" "dart" `&2` `&3` and
198 y6_mod = define_var "y6" "dart" `&2` `&3` and
199 y8_mod = define_var "y8" "dart_std4" `&2` `#2.52` and
200 y9_mod = define_var "y9" "dart_std4" `&2` `#2.52`;;
204 let inst_t = inst[`:real^3#real^3`, aty] in
206 `hypermap_of_fan (V,E)`, `H:(real^3#real^3)hypermap`;
207 `azim_dart (V,E)`, inst_t azim_mod;
208 `azim2_fan (V,E)`, inst_t azim2_mod;
209 `azim3_fan (V,E)`, inst_t azim3_mod;
210 `ln_fan`, inst_t ln_mod;
211 `rhazim_fan (V,E)`, inst_t rhazim_mod;
212 `rhazim2_fan (V,E)`, inst_t rhazim2_mod;
213 `rhazim3_fan (V,E)`, inst_t rhazim3_mod;
214 `yn_fan`, inst_t yn_mod;
215 `ye_fan`, inst_t ye_mod;
216 `rho_fan`, inst_t rho_mod;
217 `sol_fan (V,E)`, inst_t sol_mod;
218 `tau_fan (V,E)`, inst_t tau_mod;
219 `y1_fan`, inst_t y1_mod;
220 `y2_fan`, inst_t y2_mod;
221 `y3_fan (V,E)`, inst_t y3_mod;
222 `y4_fan (V,E)`, inst_t y4_mod;
223 `y5_fan (V,E)`, inst_t y5_mod;
224 `y6_fan`, inst_t y6_mod;
225 `y8_fan (V,E)`, inst_t y8_mod;
226 `y9_fan (V,E)`, inst_t y9_mod;
232 (* Declare all inequalities in a format which is close to the mod-file format *)
234 let constraints = Hashtbl.create 100;;
235 let add_constraints = map (uncurry (Hashtbl.add constraints));;
237 (* equality constraints *)
241 "azim_sum", `!n. n IN node_set (H:(A)hypermap) ==> sum n azim_mod = &2 * pi`;
242 "rhazim_sum", `!n. n IN node_set (H:(A)hypermap) ==> sum n rhazim_mod = &2 * pi * rho_mod n`;
244 "sol_sum3", `!f. f IN hyp_face3 (H:(A)hypermap) ==> sum f azim_mod = sol_mod f + pi`;
245 "tau_sum3", `!f. f IN hyp_face3 (H:(A)hypermap) ==> sum f rhazim_mod = tau_mod f + (pi + sol0)`;
246 "sol_sum4", `!f. f IN hyp_face4 (H:(A)hypermap) ==> sum f azim_mod = sol_mod f + &2 * pi`;
247 "tau_sum4", `!f. f IN hyp_face4 (H:(A)hypermap) ==> sum f rhazim_mod = tau_mod f + &2 * (pi + sol0)`;
248 "sol_sum5", `!f. f IN hyp_face5 (H:(A)hypermap) ==> sum f azim_mod = sol_mod f + &3 * pi`;
249 "tau_sum5", `!f. f IN hyp_face5 (H:(A)hypermap) ==> sum f rhazim_mod = tau_mod f + &3 * (pi + sol0)`;
250 "sol_sum6", `!f. f IN hyp_face6 (H:(A)hypermap) ==> sum f azim_mod = sol_mod f + &4 * pi`;
251 "tau_sum6", `!f. f IN hyp_face6 (H:(A)hypermap) ==> sum f rhazim_mod = tau_mod f + &4 * (pi + sol0)`;
253 "ln_def", `!n. n IN node_set (H:(A)hypermap) ==> ln_mod n = (#2.52 - yn_mod n) / #0.52`;
254 "rho_def", `!n. n IN node_set (H:(A)hypermap) ==> rho_mod n = (&1 + sol0 / pi) - ln_mod n * sol0 / pi`;
256 "edge_sym", `!e. e IN hyp_edge_pairs (H:(A)hypermap) ==> ye_mod (FST e) = ye_mod (SND e):real`;
258 "y1_def", `!d. d IN dart (H:(A)hypermap) ==> y1_mod d = yn_mod (node H d):real`;
259 "y2_def", `!d. d IN dart (H:(A)hypermap) ==> y2_mod d = yn_mod (node H (face_map H d)):real`;
260 "y3_def", `!d. d IN dart (H:(A)hypermap) ==> y3_mod d = yn_mod (node H (inverse (face_map H) d)):real`;
261 "y4_def", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> y4_mod d = ye_mod (face_map H d):real`;
262 "y5_def", `!d. d IN dart (H:(A)hypermap) ==> y5_mod d = ye_mod (inverse (face_map H) d):real`;
263 "y6_def", `!d. d IN dart (H:(A)hypermap) ==> y6_mod d = ye_mod d:real`;
264 "y9_def", `!d. d IN hyp_dart4 (H:(A)hypermap) ==> y9_mod d = ye_mod (face_map H d):real`;
265 "y8_def", `!d. d IN hyp_dart4 (H:(A)hypermap) ==> y8_mod d = y5_mod (inverse (face_map H) d):real`;
267 "azim2c", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> azim2_mod d = azim_mod (face_map H d):real`;
268 "azim3c", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> azim3_mod d = azim_mod (inverse (face_map H) d):real`;
269 "rhazim2c", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> rhazim2_mod d = rhazim_mod (face_map H d):real`;
270 "rhazim3c", `!d. d IN hyp_dart3 (H:(A)hypermap) ==> rhazim3_mod d = rhazim_mod (inverse (face_map H) d):real`;
275 (* inequality constraints *)
279 "RHA", `!d. d IN dart (H:(A)hypermap) ==> rhazim_mod d >= azim_mod d:real`;
280 "RHB", `!d. d IN dart (H:(A)hypermap) ==> rhazim_mod d <= azim_mod d * (&1 + sol0 / pi)`;
281 (* "RHBLO"; "RHBHI" *)
285 (* definitional inequalities *)
292 "yy10", `!d. (d:A) IN dart (H:(A)hypermap) ==> ye_mod d <= #2.52`;
297 (* tau tame table D inequality (Main Estimate) *)
300 "tau3", `!f:A->bool. f IN hyp_face3 (H:(A)hypermap) ==> tau_mod f >= &0`;
301 "tau4", `!f:A->bool. f IN hyp_face4 (H:(A)hypermap) ==> tau_mod f >= #0.206`;
302 "tau5", `!f:A->bool. f IN hyp_face5 (H:(A)hypermap) ==> tau_mod f >= #0.4819`;
303 "tau6", `!f:A->bool. f IN hyp_face6 (H:(A)hypermap) ==> tau_mod f >= #0.7578`;
309 "ineq105", `!d:A. d IN hyp_dartX H ==>
310 ((((azim_mod d) - #1.629) + ((#0.402 * (y2_mod d +
311 (y3_mod d + (y5_mod d + (y6_mod d - #8.0))))) -
312 (#0.315 * (y1_mod d - #2.0)))) - #0.0) >= #0.0`;
314 "ineq106", `!d:A. d IN hyp_dart3 H ==>
315 ((((rhazim_mod d) - #1.2308) + (((#0.3639 * (y2_mod d + (y3_mod d + (y5_mod d + (y6_mod d - #8.0))))) -
316 (#0.6 * (y1_mod d - #2.0))) - (#0.685 * (y4_mod d - #2.0)))) - #0.0) >= #0.0`;
318 "ineq107", `!d:A. d IN hyp_dart3 H ==>
319 (((--(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`;
321 "ineq108", `!d:A. d IN hyp_dart3 H ==>
322 ((((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`;
324 "ineq109", `!d:A. d IN hyp_dart3 H ==>
325 (((--(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`;
327 "ineq110", `!d:A. d IN hyp_dart3 H ==>
328 (((((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`;
330 "ineq111", `!d:A. d IN hyp_dart3 H ==>
331 (((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`;
334 "ineq112", `!d:A. d IN hyp_dart3 H ==>
335 ((((tau_mod (face H d)) - (#0.507 * (azim_mod d))) + #0.724) - #0.0) >= #0.0`;
337 "ineq113", `!d:A. d IN hyp_dart3 H ==>
338 ((((tau_mod (face H d)) - (#0.259 * (azim_mod d))) + #0.32) - #0.0) >= #0.0`;
340 "ineq114", `!d:A. d IN hyp_dart3 H ==>
341 (((tau_mod (face H d)) + ((#0.626 * (azim_mod d)) - #0.77)) - #0.0) >= #0.0`;
343 "ineq115", `!d:A. d IN hyp_dart3 H ==>
344 (#1.893 - (azim_mod d)) >= #0.0`;
346 "ineq116", `!d:A. d IN hyp_dart3 H ==>
347 ((azim_mod d) - #0.852) >= #0.0`;
349 "ineq119", `!d:A. d IN hyp_dart4 H ==>
350 ((((tau_mod (face H d)) - (#0.453 * (azim_mod d))) + #0.777) - #0.0) >= #0.0`;
352 "ineq120", `!d:A. d IN hyp_dart4 H ==>
353 (((tau_mod (face H d)) + ((#0.7573 * (azim_mod d)) - #1.433)) - #0.0) >= #0.0`;
355 "ineq121", `!d:A. d IN hyp_dart4 H ==>
356 (((tau_mod (face H d)) + ((#0.972 * (azim_mod d)) - #1.707)) - #0.0) >= #0.0`;
358 "ineq122", `!d:A. d IN hyp_dart4 H ==>
359 (((tau_mod (face H d)) + ((#4.72 * (azim_mod d)) - #6.248)) - #0.0) >= #0.0`;
364 let y1_def = `!d. d IN dart (H:(A)hypermap) ==> y1_mod d = yn_mod (node H d):real`;;
365 y1_def{(i3,i1,i2,j) in e_dart}: y1[i1,j] = yn[i1];
368 (* Rename terms and types *)
369 let s1 = inst [`:real^3#real^3`, aty] im_sum;;
370 let s2 = subst [`hypermap_of_fan (V,E)`, h_fan_hyp] s1;;
371 let s3 = subst [`azim_dart (V,E)`, azim_mod] s2;;
374 (*************************************)
376 let SUM_ISOMORPHISM = prove(`!G H (g:B->A) (r:A->real). isomorphism g (G,H)
377 ==> (!d. d IN dart G ==> sum(node G d) (r o g) = sum(node H (g d)) r)`,
378 REPEAT STRIP_TAC THEN
379 SUBGOAL_THEN `sum(node G d) (r o (g:B->A)) = sum(IMAGE g (node G d)) r` (fun th -> REWRITE_TAC[th]) THENL
381 MATCH_MP_TAC (GSYM SUM_IMAGE) THEN
382 REPEAT STRIP_TAC THEN
383 UNDISCH_TAC `isomorphism (g:B->A) (G,H)` THEN
384 REWRITE_TAC[isomorphism; BIJ; INJ] THEN
385 DISCH_THEN (MP_TAC o CONJUNCT1) THEN
386 DISCH_THEN (MP_TAC o CONJUNCT1) THEN
387 DISCH_THEN (MATCH_MP_TAC o CONJUNCT2) THEN
388 ASM_REWRITE_TAC[] THEN
389 CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN EXISTS_TAC `node G (d:B)` THEN ASM_SIMP_TAC[Hypermap.lemma_node_subset];
392 MP_TAC (ISPECL [`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `d:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
393 ASM_REWRITE_TAC[] THEN
394 DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]));;
397 let ISO_NODE_INJ = prove(`!G H (g:B->A) n. isomorphism g (G,H) /\ n IN node_set G ==>
398 (!x y. x IN n /\ y IN n /\ g x = g y ==> x = y)`,
399 REPEAT STRIP_TAC THEN
400 UNDISCH_TAC `isomorphism (g:B->A) (G,H)` THEN
401 REWRITE_TAC[isomorphism; BIJ; INJ] THEN
402 DISCH_THEN (MP_TAC o CONJUNCT1) THEN DISCH_THEN (MP_TAC o CONJUNCT1) THEN
403 DISCH_THEN (MATCH_MP_TAC o CONJUNCT2) THEN
404 ASM_REWRITE_TAC[] THEN
405 MP_TAC (ISPECL [`G:(B)hypermap`; `n:B->bool`] Hypermap.lemma_node_representation) THEN
406 ASM_REWRITE_TAC[] THEN
408 CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN
409 EXISTS_TAC `n:B->bool` THEN
410 ASM_REWRITE_TAC[] THEN
411 ASM_SIMP_TAC[Hypermap.lemma_node_subset]);;
415 let COMPONENTS_ISO_IMAGE = prove(`!G H (g:B->A). isomorphism g (G,H)
416 ==> (!d. d IN dart G ==>
417 node H (g d) = IMAGE g (node G d) /\
418 face H (g d) = IMAGE g (face G d))`,
419 REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN DISCH_TAC THEN
420 MP_TAC (ISPECL[`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `d:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
421 ASM_REWRITE_TAC[] THEN
425 let HYPERMAP_MAPS_ISO_COMM = prove(`!G H (g:B->A). isomorphism g (G,H)
426 ==> (!d. d IN dart G ==>
427 face_map H (g d) = g (face_map G d) /\
428 node_map H (g d) = g (node_map G d))`,
429 SIMP_TAC[isomorphism]);;
432 let HYPERMAP_INV_MAPS = prove(`!(G:(B)hypermap) d. d IN dart G
433 ==> (?k. inverse (face_map G) d = (face_map G POWER k) d)`,
434 REPEAT STRIP_TAC THEN
435 ABBREV_TAC `n = CARD (orbit_map (face_map G) (d:B))` THEN
436 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
437 ASM_REWRITE_TAC[Hypermap.hypermap_lemma] THEN
440 REWRITE_TAC[ARITH_RULE `1 <= n <=> 0 < n`] THEN
442 MATCH_MP_TAC Hypermap_and_fan.ORBIT_MAP_CARD_POS THEN
443 EXISTS_TAC `dart G:B->bool` THEN
444 REWRITE_TAC[Hypermap.hypermap_lemma];
447 REWRITE_TAC[Hypermap.POWER_1] THEN
448 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
449 EXISTS_TAC `n - 1` THEN
454 let HYPERMAP_INV_MAPS_ISO_COMM = prove(`!G H (g:B->A). isomorphism g (G,H)
455 ==> (!d. d IN dart G ==>
456 inverse (face_map H) (g d) = g (inverse (face_map G) d) /\
457 inverse (node_map H) (g d) = g (inverse (node_map G) d))`,
458 REWRITE_TAC[isomorphism] THEN REPEAT STRIP_TAC THEN
459 MATCH_MP_TAC (GSYM COMM_INVERSE_LEMMA) THEN
460 MAP_EVERY EXISTS_TAC [`dart G:B->bool`; `dart H:A->bool`] THEN
461 ASM_SIMP_TAC[Hypermap.hypermap_lemma]);;
464 let HYPERMAP_INV_MAPS_ISO_IMAGE = prove(`!G H (g:B->A). isomorphism g (G,H)
465 ==> (!d. d IN dart G ==>
466 face H (inverse (face_map H) (g d)) = IMAGE g (face G (inverse (face_map G) d)) /\
467 node H (inverse (face_map H) (g d)) = IMAGE g (node G (inverse (face_map G) d)))`,
468 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
469 ASM_SIMP_TAC[HYPERMAP_INV_MAPS_ISO_COMM] THEN
470 ABBREV_TAC `x = inverse (face_map G) (d:B)` THEN
471 SUBGOAL_THEN `x:B IN dart G` ASSUME_TAC THENL
474 ASM_SIMP_TAC[Hypermap.lemma_dart_inveriant_under_inverse_maps];
477 ASM_SIMP_TAC[COMPONENTS_ISO_IMAGE]);;
483 let HYPERMAP_MAPS_ISO_IMAGE = prove(`!G H (g:B->A). isomorphism g (G,H)
484 ==> (!d. d IN dart G ==>
485 face H (face_map H (g d)) = IMAGE g (face G (face_map G d)) /\
486 face H (node_map H (g d)) = IMAGE g (face G (node_map G d)) /\
487 node H (node_map H (g d)) = IMAGE g (node G (node_map G d)) /\
488 node H (face_map H (g d)) = IMAGE g (node G (face_map G d)))`,
489 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
490 ASM_SIMP_TAC[HYPERMAP_MAPS_ISO_COMM] THEN
491 MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
492 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
493 REPEAT CONJ_TAC THENL
495 FIRST_X_ASSUM (MP_TAC o SPEC `face_map G (d:B)`);
496 FIRST_X_ASSUM (MP_TAC o SPEC `node_map G (d:B)`);
497 FIRST_X_ASSUM (MP_TAC o SPEC `node_map G (d:B)`);
498 FIRST_X_ASSUM (MP_TAC o SPEC `face_map G (d:B)`)
500 ASM_SIMP_TAC[Hypermap.lemma_dart_invariant]);;
509 let SUM_NODE_ISO = prove(`!G H (g:B->A) (r:A->real). isomorphism g (G,H)
510 ==> (!n. n IN node_set G ==> sum(IMAGE g n) r = sum n (r o g))`,
511 REPEAT STRIP_TAC THEN
512 MATCH_MP_TAC SUM_IMAGE THEN
513 MATCH_MP_TAC ISO_NODE_INJ THEN
514 MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
519 let CARD_NODE_ISO = prove(`!G H (g:B->A). isomorphism g (G,H)
520 ==> (!n. n IN node_set G ==> CARD (IMAGE g n) = CARD n)`,
521 REPEAT STRIP_TAC THEN
522 MATCH_MP_TAC CARD_IMAGE_INJ THEN
525 MATCH_MP_TAC ISO_NODE_INJ THEN
526 MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
531 MP_TAC (ISPECL [`G:(B)hypermap`; `n:B->bool`] Hypermap.lemma_node_representation) THEN
532 ASM_REWRITE_TAC[] THEN
534 ASM_REWRITE_TAC[Hypermap.NODE_FINITE]);;
537 let SUM_NODE_SUB = prove(`!(G:(B)hypermap) r1 r2 n. n IN node_set G
538 ==> sum n (\x. r1 x - r2 x) = sum n r1 - sum n r2`,
539 REPEAT STRIP_TAC THEN
540 MP_TAC (ISPECL [`G:(B)hypermap`; `n:B->bool`] Hypermap.lemma_node_representation) THEN
541 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
542 ASM_SIMP_TAC[Hypermap.NODE_FINITE; SUM_SUB]);;
545 let SUM_NODE_CONST = prove(`!(G:(B)hypermap) c n. n IN node_set G
546 ==> sum n (\x. c) = &(CARD n) * c`,
547 REPEAT STRIP_TAC THEN
548 MP_TAC (ISPECL [`G:(B)hypermap`; `n:B->bool`] Hypermap.lemma_node_representation) THEN
549 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
550 ASM_SIMP_TAC[Hypermap.NODE_FINITE; SUM_CONST]);;
553 let SUM_NODE_SUB_CONST = prove(`!(G:(B)hypermap) r c n. n IN node_set G
554 ==> sum n (\x. r x - c) = sum n r - &(CARD n) * c`,
555 REPEAT STRIP_TAC THEN
556 MP_TAC (SPEC_ALL SUM_NODE_CONST) THEN
557 ASM_REWRITE_TAC[] THEN
558 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
559 MP_TAC (SPECL [`G:(B)hypermap`; `r:B->real`; `\x:B. c:real`; `n:B->bool`] SUM_NODE_SUB) THEN
566 let ISO_FACE_INJ = prove(`!G H (g:B->A) f. isomorphism g (G,H) /\ f IN face_set G ==>
567 (!x y. x IN f /\ y IN f /\ g x = g y ==> x = y)`,
568 REPEAT STRIP_TAC THEN
569 UNDISCH_TAC `isomorphism (g:B->A) (G,H)` THEN
570 REWRITE_TAC[isomorphism; BIJ; INJ] THEN
571 DISCH_THEN (MP_TAC o CONJUNCT1) THEN DISCH_THEN (MP_TAC o CONJUNCT1) THEN
572 DISCH_THEN (MATCH_MP_TAC o CONJUNCT2) THEN
573 ASM_REWRITE_TAC[] THEN
574 MP_TAC (ISPECL [`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
575 ASM_REWRITE_TAC[] THEN
577 CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN
578 EXISTS_TAC `f:B->bool` THEN
579 ASM_REWRITE_TAC[] THEN
580 ASM_SIMP_TAC[Hypermap.lemma_face_subset]);;
583 let SUM_FACE_ISO = prove(`!G H (g:B->A) (r:A->real). isomorphism g (G,H)
584 ==> (!f. f IN face_set G ==> sum(IMAGE g f) r = sum f (r o g))`,
585 REPEAT STRIP_TAC THEN
586 MATCH_MP_TAC SUM_IMAGE THEN
587 MATCH_MP_TAC ISO_FACE_INJ THEN
588 MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
593 let CARD_FACE_ISO = prove(`!G H (g:B->A). isomorphism g (G,H)
594 ==> (!f. f IN face_set G ==> CARD (IMAGE g f) = CARD f)`,
595 REPEAT STRIP_TAC THEN
596 MATCH_MP_TAC CARD_IMAGE_INJ THEN
599 MATCH_MP_TAC ISO_FACE_INJ THEN
600 MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
605 MP_TAC (ISPECL [`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
606 ASM_REWRITE_TAC[] THEN
608 ASM_REWRITE_TAC[Hypermap.FACE_FINITE]);;
611 let SUM_FACE_SUB = prove(`!(G:(B)hypermap) r1 r2 f. f IN face_set G
612 ==> sum f (\x. r1 x - r2 x) = sum f r1 - sum f r2`,
613 REPEAT STRIP_TAC THEN
614 MP_TAC (ISPECL [`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
615 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
616 ASM_SIMP_TAC[Hypermap.FACE_FINITE; SUM_SUB]);;
619 let SUM_FACE_CONST = prove(`!(G:(B)hypermap) c f. f IN face_set G
620 ==> sum f (\x. c) = &(CARD f) * c`,
621 REPEAT STRIP_TAC THEN
622 MP_TAC (ISPECL [`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
623 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
624 ASM_SIMP_TAC[Hypermap.FACE_FINITE; SUM_CONST]);;
627 let SUM_FACE_SUB_CONST = prove(`!(G:(B)hypermap) r c f. f IN face_set G
628 ==> sum f (\x. r x - c) = sum f r - &(CARD f) * c`,
629 REPEAT STRIP_TAC THEN
630 MP_TAC (SPEC_ALL SUM_FACE_CONST) THEN
631 ASM_REWRITE_TAC[] THEN
632 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
633 MP_TAC (SPECL [`G:(B)hypermap`; `r:B->real`; `\x:B. c:real`; `f:B->bool`] SUM_FACE_SUB) THEN
639 let SUM_NODE_LIST = prove(`!L (n:(A#A)list). good_list L /\ MEM n (list_of_nodes L) ==>
640 sum (set_of_list n) = list_sum n`,
641 REPEAT STRIP_TAC THEN
642 REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `f:(A#A)->real` THEN
643 MP_TAC (ISPECL [`f:A#A->real`; `n:(A#A)list`] ALL_DISTINCT_SUM) THEN
646 MATCH_MP_TAC ALL_DISTINCT_NODE THEN
647 EXISTS_TAC `L:((A)list)list` THEN
655 let SUM_NODE_LIST_ALL = prove(`!L (P:(A#A->bool)->((A#A->real)->real)->bool). good_list L /\ good_list_nodes L ==>
656 ((!n. n IN node_set (hypermap_of_list L) ==> P n (sum n))
657 <=> (!n. MEM n (list_of_nodes L) ==> P (set_of_list n) (list_sum n)))`,
658 REWRITE_TAC[good_list_nodes] THEN
659 REPEAT STRIP_TAC THEN
660 ASM_REWRITE_TAC[IN_SET_OF_LIST; nodes_of_list] THEN
661 EQ_TAC THEN REPEAT STRIP_TAC THENL
663 FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list n:A#A->bool`) THEN
664 REWRITE_TAC[MEM_MAP] THEN
667 EXISTS_TAC `n:(A#A)list` THEN
672 MP_TAC (SPEC_ALL SUM_NODE_LIST) THEN
673 ASM_REWRITE_TAC[] THEN
674 DISCH_THEN (fun th -> REWRITE_TAC[th]);
678 POP_ASSUM MP_TAC THEN
679 REWRITE_TAC[MEM_MAP] THEN
681 FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
682 ASM_REWRITE_TAC[] THEN
683 MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_NODE_LIST) THEN
684 ASM_REWRITE_TAC[] THEN
685 DISCH_THEN (fun th -> REWRITE_TAC[th]));;
688 let CARD_SET_OF_LIST_NODE = prove(`!(L:((A)list)list) n. good_list L /\ MEM n (list_of_nodes L)
689 ==> CARD(set_of_list n) = LENGTH n`,
690 REPEAT STRIP_TAC THEN
691 MATCH_MP_TAC CARD_SET_OF_LIST_ALL_DISTINCT THEN
692 MATCH_MP_TAC ALL_DISTINCT_NODE THEN
693 EXISTS_TAC `L:((A)list)list` THEN ASM_REWRITE_TAC[]);;
699 let SUM_FACE_LIST = prove(`!L (f:(A#A)list). good_list L /\ MEM f (list_of_faces L) ==>
700 sum (set_of_list f) = list_sum f`,
701 REPEAT STRIP_TAC THEN
702 REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `r:(A#A)->real` THEN
703 MP_TAC (ISPECL [`r:A#A->real`; `f:(A#A)list`] ALL_DISTINCT_SUM) THEN
706 MATCH_MP_TAC ALL_DISTINCT_FACE THEN
707 EXISTS_TAC `L:((A)list)list` THEN
715 let SUM_FACE_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
716 ((!f. f IN face_set (hypermap_of_list L) ==> P f (sum f))
717 <=> (!f. MEM f (list_of_faces L) ==> P (set_of_list f) (list_sum f)))`,
718 REPEAT STRIP_TAC THEN
719 ASM_SIMP_TAC[FACE_SET_EQ_LIST] THEN
720 ASM_REWRITE_TAC[IN_SET_OF_LIST; faces_of_list] THEN
721 EQ_TAC THEN REPEAT STRIP_TAC THENL
723 FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
724 REWRITE_TAC[MEM_MAP] THEN
727 EXISTS_TAC `f:(A#A)list` THEN
732 MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
733 ASM_REWRITE_TAC[] THEN
734 DISCH_THEN (fun th -> REWRITE_TAC[th]);
738 POP_ASSUM MP_TAC THEN
739 REWRITE_TAC[MEM_MAP] THEN
741 FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
742 ASM_REWRITE_TAC[] THEN
743 MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
744 ASM_REWRITE_TAC[] THEN
745 DISCH_THEN (fun th -> REWRITE_TAC[th]));;
749 let CARD_SET_OF_LIST_FACE = prove(`!(L:((A)list)list) f. good_list L /\ MEM f (list_of_faces L)
750 ==> CARD(set_of_list f) = LENGTH f`,
751 REPEAT STRIP_TAC THEN
752 MATCH_MP_TAC CARD_SET_OF_LIST_ALL_DISTINCT THEN
753 MATCH_MP_TAC ALL_DISTINCT_FACE THEN
754 EXISTS_TAC `L:((A)list)list` THEN ASM_REWRITE_TAC[]);;
757 let IN_DART3_IMP_IN_DART = UNDISCH_ALL (prove(`d:B IN hyp_dart3 G ==> d IN dart G`,
758 SIMP_TAC[hyp_dart3; IN_ELIM_THM]));;
759 let IN_DART4_IMP_IN_DART = UNDISCH_ALL (prove(`d:B IN hyp_dart4 G ==> d IN dart G`,
760 SIMP_TAC[hyp_dart4; IN_ELIM_THM]));;
762 let IN_FACE3_IMP_IN_FACE = UNDISCH_ALL (prove(`f IN hyp_face3 (G:(B)hypermap) ==> f IN face_set G`,
763 SIMP_TAC[hyp_face3; IN_ELIM_THM]));;
764 let IN_FACE4_IMP_IN_FACE = UNDISCH_ALL (prove(`f IN hyp_face4 (G:(B)hypermap) ==> f IN face_set G`,
765 SIMP_TAC[hyp_face4; IN_ELIM_THM]));;
766 let IN_FACE5_IMP_IN_FACE = UNDISCH_ALL (prove(`f IN hyp_face5 (G:(B)hypermap) ==> f IN face_set G`,
767 SIMP_TAC[hyp_face5; IN_ELIM_THM]));;
768 let IN_FACE6_IMP_IN_FACE = UNDISCH_ALL (prove(`f IN hyp_face6 (G:(B)hypermap) ==> f IN face_set G`,
769 SIMP_TAC[hyp_face6; IN_ELIM_THM]));;
774 let DART_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
775 ((!d. d IN dart (hypermap_of_list L) ==> P d)
776 <=> (!d. MEM d (list_of_darts L) ==> P d))`,
777 REPEAT STRIP_TAC THEN
778 ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST; darts_of_list; IN_SET_OF_LIST]);;
781 let DART3_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
782 ((!d. d IN hyp_dart3 (hypermap_of_list L) ==> P d)
783 <=> (!d. MEM d (list_of_darts3 L) ==> P d))`,
784 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[LIST_OF_DARTS3; IN_SET_OF_LIST]);;
788 let DART4_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
789 ((!d. d IN hyp_dart4 (hypermap_of_list L) ==> P d)
790 <=> (!d. MEM d (list_of_darts4 L) ==> P d))`,
791 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[LIST_OF_DARTS4; IN_SET_OF_LIST]);;
794 let DARTX_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
795 ((!d. d IN hyp_dartX (hypermap_of_list L) ==> P d)
796 <=> (!d. MEM d (list_of_dartsX L) ==> P d))`,
797 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[LIST_OF_DARTS_X; IN_SET_OF_LIST]);;
801 let FACE3_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
802 ((!f. f IN hyp_face3 (hypermap_of_list L) ==> P f (sum f))
803 <=> (!f. MEM f (list_of_faces3 L) ==> P (set_of_list f) (list_sum f)))`,
804 REPEAT STRIP_TAC THEN
805 ASM_SIMP_TAC[LIST_OF_FACES3] THEN
806 ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM_MAP] THEN
807 EQ_TAC THEN REPEAT STRIP_TAC THENL
809 FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
812 EXISTS_TAC `f:(A#A)list` THEN
817 MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
820 ASM_REWRITE_TAC[] THEN
821 POP_ASSUM MP_TAC THEN
822 SIMP_TAC[list_of_faces3; MEM_FILTER];
825 DISCH_THEN (fun th -> REWRITE_TAC[th]);
829 FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
830 ASM_REWRITE_TAC[] THEN
831 MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
834 ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
835 SIMP_TAC[list_of_faces3; MEM_FILTER];
838 DISCH_THEN (fun th -> REWRITE_TAC[th]));;
842 let FACE4_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
843 ((!f. f IN hyp_face4 (hypermap_of_list L) ==> P f (sum f))
844 <=> (!f. MEM f (list_of_faces4 L) ==> P (set_of_list f) (list_sum f)))`,
845 REPEAT STRIP_TAC THEN
846 ASM_SIMP_TAC[LIST_OF_FACES4] THEN
847 ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM_MAP] THEN
848 EQ_TAC THEN REPEAT STRIP_TAC THENL
850 FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
853 EXISTS_TAC `f:(A#A)list` THEN
858 MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
861 ASM_REWRITE_TAC[] THEN
862 POP_ASSUM MP_TAC THEN
863 SIMP_TAC[list_of_faces4; MEM_FILTER];
866 DISCH_THEN (fun th -> REWRITE_TAC[th]);
870 FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
871 ASM_REWRITE_TAC[] THEN
872 MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
875 ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
876 SIMP_TAC[list_of_faces4; MEM_FILTER];
879 DISCH_THEN (fun th -> REWRITE_TAC[th]));;
882 let FACE5_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
883 ((!f. f IN hyp_face5 (hypermap_of_list L) ==> P f (sum f))
884 <=> (!f. MEM f (list_of_faces5 L) ==> P (set_of_list f) (list_sum f)))`,
885 REPEAT STRIP_TAC THEN
886 ASM_SIMP_TAC[LIST_OF_FACES5] THEN
887 ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM_MAP] THEN
888 EQ_TAC THEN REPEAT STRIP_TAC THENL
890 FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
893 EXISTS_TAC `f:(A#A)list` THEN
898 MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
901 ASM_REWRITE_TAC[] THEN
902 POP_ASSUM MP_TAC THEN
903 SIMP_TAC[list_of_faces5; MEM_FILTER];
906 DISCH_THEN (fun th -> REWRITE_TAC[th]);
910 FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
911 ASM_REWRITE_TAC[] THEN
912 MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
915 ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
916 SIMP_TAC[list_of_faces5; MEM_FILTER];
919 DISCH_THEN (fun th -> REWRITE_TAC[th]));;
922 let FACE6_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
923 ((!f. f IN hyp_face6 (hypermap_of_list L) ==> P f (sum f))
924 <=> (!f. MEM f (list_of_faces6 L) ==> P (set_of_list f) (list_sum f)))`,
925 REPEAT STRIP_TAC THEN
926 ASM_SIMP_TAC[LIST_OF_FACES6] THEN
927 ASM_REWRITE_TAC[IN_SET_OF_LIST; MEM_MAP] THEN
928 EQ_TAC THEN REPEAT STRIP_TAC THENL
930 FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
933 EXISTS_TAC `f:(A#A)list` THEN
938 MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
941 ASM_REWRITE_TAC[] THEN
942 POP_ASSUM MP_TAC THEN
943 SIMP_TAC[list_of_faces6; MEM_FILTER];
946 DISCH_THEN (fun th -> REWRITE_TAC[th]);
950 FIRST_X_ASSUM (MP_TAC o SPEC `x:(A#A)list`) THEN
951 ASM_REWRITE_TAC[] THEN
952 MP_TAC (SPECL[`L:((A)list)list`; `x:(A#A)list`] SUM_FACE_LIST) THEN
955 ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
956 SIMP_TAC[list_of_faces6; MEM_FILTER];
959 DISCH_THEN (fun th -> REWRITE_TAC[th]));;
963 let EDGE_LIST_ALL = prove(`!(L:((A)list)list) P. good_list L ==>
964 ((!e. e IN hyp_edge_pairs (hypermap_of_list L) ==> P e)
965 <=> (!e. MEM e (list_of_edges L) ==> P e))`,
966 REPEAT STRIP_TAC THEN
967 ASM_SIMP_TAC[LIST_OF_EDGES; IN_SET_OF_LIST]);;
970 let SUB_CONST_o = prove(`!f (c:real) (g:B->A). (\x. f x - c) o g = (\x. (f o g) x - c)`,
971 REWRITE_TAC[FUN_EQ_THM; o_THM]);;
974 (*******************************)
977 let in_all_rewrites =
995 let table = Hashtbl.create 10 in
996 let _ = map (uncurry (Hashtbl.add table))
998 `hyp_dart3 (G:(B)hypermap)`, IN_DART3_IMP_IN_DART;
999 `hyp_dart4 (G:(B)hypermap)`, IN_DART4_IMP_IN_DART;
1000 `hyp_face3 (G:(B)hypermap)`, IN_FACE3_IMP_IN_FACE;
1001 `hyp_face4 (G:(B)hypermap)`, IN_FACE4_IMP_IN_FACE;
1002 `hyp_face5 (G:(B)hypermap)`, IN_FACE5_IMP_IN_FACE;
1003 `hyp_face6 (G:(B)hypermap)`, IN_FACE6_IMP_IN_FACE;
1009 (*************************************)
1012 let iso_dart_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1013 ((!d. d IN dart H ==> P d) ==> (!d. d IN dart G ==> P (g d)))`,
1014 REWRITE_TAC[isomorphism; BIJ; SURJ] THEN
1015 REPEAT STRIP_TAC THEN
1016 FIRST_X_ASSUM (MP_TAC o SPEC `d:B`) THEN
1017 FIRST_X_ASSUM (MP_TAC o SPEC `d:B`) THEN
1018 ASM_REWRITE_TAC[] THEN
1020 FIRST_X_ASSUM (MP_TAC o SPEC `(g:B->A) d`) THEN
1024 let iso_dart_in = prove(`!(g:B->A) H G d. isomorphism g (G,H) /\ d IN dart G ==>
1026 REWRITE_TAC[isomorphism; BIJ; SURJ; INJ] THEN
1027 REPEAT STRIP_TAC THEN
1032 let iso_card_eq = prove(`!(g:B->A) H G s. isomorphism g (G,H) /\ s SUBSET dart G
1033 ==> CARD (IMAGE g s) = CARD s`,
1034 REWRITE_TAC[isomorphism; BIJ; INJ] THEN
1035 REPEAT STRIP_TAC THEN
1036 MATCH_MP_TAC CARD_IMAGE_INJ THEN
1039 REPEAT STRIP_TAC THEN
1040 FIRST_X_ASSUM MATCH_MP_TAC THEN
1041 ASM_REWRITE_TAC[] THEN
1042 CONJ_TAC THEN MATCH_MP_TAC IN_TRANS THEN EXISTS_TAC `s:B->bool` THEN ASM_REWRITE_TAC[];
1045 MATCH_MP_TAC FINITE_SUBSET THEN
1046 EXISTS_TAC `dart G:B->bool` THEN
1047 ASM_REWRITE_TAC[Hypermap.hypermap_lemma]);;
1050 let iso_face_card = prove(`!(g:B->A) H G d. isomorphism g (G,H) /\ d IN dart G
1051 ==> CARD (face H (g d)) = CARD (face G d)`,
1052 REPEAT STRIP_TAC THEN
1053 MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
1054 ASM_REWRITE_TAC[] THEN
1055 DISCH_THEN (MP_TAC o SPEC `d:B`) THEN
1056 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1057 ASM_REWRITE_TAC[] THEN
1058 MATCH_MP_TAC iso_card_eq THEN
1059 MAP_EVERY EXISTS_TAC [`H:(A)hypermap`; `G:(B)hypermap`] THEN
1060 ASM_SIMP_TAC[Hypermap.lemma_face_subset]);;
1063 let iso_dart3_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1064 ((!d. d IN hyp_dart3 H ==> P d) ==> (!d. d IN hyp_dart3 G ==> P (g d)))`,
1065 REWRITE_TAC[hyp_dart3; IN_ELIM_THM] THEN
1066 REPEAT STRIP_TAC THEN
1067 FIRST_X_ASSUM MATCH_MP_TAC THEN
1068 MP_TAC (SPEC_ALL iso_dart_in) THEN
1069 ASM_SIMP_TAC[iso_face_card]);;
1073 let iso_dart4_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1074 ((!d. d IN hyp_dart4 H ==> P d) ==> (!d. d IN hyp_dart4 G ==> P (g d)))`,
1075 REWRITE_TAC[hyp_dart4; IN_ELIM_THM] THEN
1076 REPEAT STRIP_TAC THEN
1077 FIRST_X_ASSUM MATCH_MP_TAC THEN
1078 MP_TAC (SPEC_ALL iso_dart_in) THEN
1079 ASM_SIMP_TAC[iso_face_card]);;
1083 let iso_dartX_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1084 ((!d. d IN hyp_dartX H ==> P d) ==> (!d. d IN hyp_dartX G ==> P (g d)))`,
1085 REWRITE_TAC[hyp_dartX; IN_ELIM_THM] THEN
1086 REPEAT STRIP_TAC THEN
1087 FIRST_X_ASSUM MATCH_MP_TAC THEN
1088 MP_TAC (SPEC_ALL iso_dart_in) THEN
1089 ASM_SIMP_TAC[iso_face_card]);;
1094 let iso_edge_pairs_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1095 ((!e. e IN hyp_edge_pairs H ==> P e) ==> (!e. e IN hyp_edge_pairs G ==> P (g (FST e), g (SND e))))`,
1096 REWRITE_TAC[isomorphism; BIJ; SURJ; hyp_edge_pairs; IN_ELIM_THM] THEN
1097 REPEAT STRIP_TAC THEN
1098 ASM_REWRITE_TAC[] THEN
1099 FIRST_X_ASSUM MATCH_MP_TAC THEN
1100 EXISTS_TAC `(g:B->A) x` THEN
1106 let iso_node_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1107 ((!n. n IN node_set H ==> P n) ==> (!n. n IN node_set G ==> P (IMAGE g n)))`,
1108 REPEAT STRIP_TAC THEN
1109 POP_ASSUM (MP_TAC o MATCH_MP Hypermap.lemma_node_representation) THEN
1111 MP_TAC (ISPECL [`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `x:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
1112 ASM_REWRITE_TAC[] THEN
1113 DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
1114 FIRST_X_ASSUM MATCH_MP_TAC THEN
1115 REWRITE_TAC[GSYM Hypermap.lemma_in_node_set] THEN
1116 MATCH_MP_TAC iso_dart_in THEN
1117 EXISTS_TAC `G:(B)hypermap` THEN
1118 ASM_REWRITE_TAC[]);;
1122 let iso_face_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1123 ((!f. f IN face_set H ==> P f) ==> (!f. f IN face_set G ==> P (IMAGE g f)))`,
1124 REPEAT STRIP_TAC THEN
1125 POP_ASSUM (MP_TAC o MATCH_MP Hypermap.lemma_face_representation) THEN
1127 MP_TAC (ISPECL [`g:B->A`; `G:(B)hypermap`; `H:(A)hypermap`; `x:B`] ISOMORPHISM_COMPONENT_IMAGE) THEN
1128 ASM_REWRITE_TAC[] THEN
1129 DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
1130 FIRST_X_ASSUM MATCH_MP_TAC THEN
1131 REWRITE_TAC[GSYM Hypermap.lemma_in_face_set] THEN
1132 MATCH_MP_TAC iso_dart_in THEN
1133 EXISTS_TAC `G:(B)hypermap` THEN
1134 ASM_REWRITE_TAC[]);;
1137 let iso_face3_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1138 ((!f. f IN hyp_face3 H ==> P f) ==> (!f. f IN hyp_face3 G ==> P (IMAGE g f)))`,
1139 REWRITE_TAC[hyp_face3; IN_ELIM_THM] THEN
1140 REPEAT STRIP_TAC THEN
1141 FIRST_X_ASSUM MATCH_MP_TAC THEN
1142 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1143 MP_TAC (SPECL[`g:B->A`; `H:(A)hypermap`; `G:(B)hypermap`] iso_face_trans) THEN
1144 ASM_REWRITE_TAC[] THEN
1145 REPEAT DISCH_TAC THEN
1148 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
1149 SPEC_TAC (`f:B->bool`, `f:B->bool`) THEN
1150 FIRST_X_ASSUM MATCH_MP_TAC THEN
1155 MP_TAC (ISPECL[`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
1156 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1157 UNDISCH_TAC `CARD (f:B->bool) = 3` THEN
1158 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1159 ASM_REWRITE_TAC[] THEN
1161 MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
1162 ASM_REWRITE_TAC[] THEN
1163 DISCH_THEN (fun th -> ASM_SIMP_TAC[GSYM th]) THEN
1164 MATCH_MP_TAC iso_face_card THEN
1165 ASM_REWRITE_TAC[]);;
1168 let iso_face4_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1169 ((!f. f IN hyp_face4 H ==> P f) ==> (!f. f IN hyp_face4 G ==> P (IMAGE g f)))`,
1170 REWRITE_TAC[hyp_face4; IN_ELIM_THM] THEN
1171 REPEAT STRIP_TAC THEN
1172 FIRST_X_ASSUM MATCH_MP_TAC THEN
1173 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1174 MP_TAC (SPECL[`g:B->A`; `H:(A)hypermap`; `G:(B)hypermap`] iso_face_trans) THEN
1175 ASM_REWRITE_TAC[] THEN
1176 REPEAT DISCH_TAC THEN
1179 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
1180 SPEC_TAC (`f:B->bool`, `f:B->bool`) THEN
1181 FIRST_X_ASSUM MATCH_MP_TAC THEN
1186 MP_TAC (ISPECL[`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
1187 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1188 UNDISCH_TAC `CARD (f:B->bool) = 4` THEN
1189 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1190 ASM_REWRITE_TAC[] THEN
1192 MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
1193 ASM_REWRITE_TAC[] THEN
1194 DISCH_THEN (fun th -> ASM_SIMP_TAC[GSYM th]) THEN
1195 MATCH_MP_TAC iso_face_card THEN
1196 ASM_REWRITE_TAC[]);;
1199 let iso_face5_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1200 ((!f. f IN hyp_face5 H ==> P f) ==> (!f. f IN hyp_face5 G ==> P (IMAGE g f)))`,
1201 REWRITE_TAC[hyp_face5; IN_ELIM_THM] THEN
1202 REPEAT STRIP_TAC THEN
1203 FIRST_X_ASSUM MATCH_MP_TAC THEN
1204 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1205 MP_TAC (SPECL[`g:B->A`; `H:(A)hypermap`; `G:(B)hypermap`] iso_face_trans) THEN
1206 ASM_REWRITE_TAC[] THEN
1207 REPEAT DISCH_TAC THEN
1210 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
1211 SPEC_TAC (`f:B->bool`, `f:B->bool`) THEN
1212 FIRST_X_ASSUM MATCH_MP_TAC THEN
1217 MP_TAC (ISPECL[`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
1218 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1219 UNDISCH_TAC `CARD (f:B->bool) = 5` THEN
1220 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1221 ASM_REWRITE_TAC[] THEN
1223 MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
1224 ASM_REWRITE_TAC[] THEN
1225 DISCH_THEN (fun th -> ASM_SIMP_TAC[GSYM th]) THEN
1226 MATCH_MP_TAC iso_face_card THEN
1227 ASM_REWRITE_TAC[]);;
1230 let iso_face6_trans = prove(`!(g:B->A) H G P. isomorphism g (G,H) ==>
1231 ((!f. f IN hyp_face6 H ==> P f) ==> (!f. f IN hyp_face6 G ==> P (IMAGE g f)))`,
1232 REWRITE_TAC[hyp_face6; IN_ELIM_THM] THEN
1233 REPEAT STRIP_TAC THEN
1234 FIRST_X_ASSUM MATCH_MP_TAC THEN
1235 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1236 MP_TAC (SPECL[`g:B->A`; `H:(A)hypermap`; `G:(B)hypermap`] iso_face_trans) THEN
1237 ASM_REWRITE_TAC[] THEN
1238 REPEAT DISCH_TAC THEN
1241 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
1242 SPEC_TAC (`f:B->bool`, `f:B->bool`) THEN
1243 FIRST_X_ASSUM MATCH_MP_TAC THEN
1248 MP_TAC (ISPECL[`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
1249 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1250 UNDISCH_TAC `CARD (f:B->bool) = 6` THEN
1251 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1252 ASM_REWRITE_TAC[] THEN
1254 MP_TAC (SPEC_ALL COMPONENTS_ISO_IMAGE) THEN
1255 ASM_REWRITE_TAC[] THEN
1256 DISCH_THEN (fun th -> ASM_SIMP_TAC[GSYM th]) THEN
1257 MATCH_MP_TAC iso_face_card THEN
1258 ASM_REWRITE_TAC[]);;
1263 let iso_trans_table =
1264 let table = Hashtbl.create 10 in
1265 let _ = map (uncurry (Hashtbl.add table))
1267 `dart H:A->bool`, iso_dart_trans;
1268 `node_set (H:(A)hypermap)`, iso_node_trans;
1269 `face_set (H:(A)hypermap)`, iso_face_trans;
1270 `hyp_edge_pairs (H:(A)hypermap)`, iso_edge_pairs_trans;
1271 `hyp_dart3 (H:(A)hypermap)`, iso_dart3_trans;
1272 `hyp_dart4 (H:(A)hypermap)`, iso_dart4_trans;
1273 `hyp_dartX (H:(A)hypermap)`, iso_dartX_trans;
1274 `hyp_face3 (H:(A)hypermap)`, iso_face3_trans;
1275 `hyp_face4 (H:(A)hypermap)`, iso_face4_trans;
1276 `hyp_face5 (H:(A)hypermap)`, iso_face5_trans;
1277 `hyp_face6 (H:(A)hypermap)`, iso_face6_trans;
1282 (**************************)
1286 let gen_iso_thm ineq =
1287 let x_tm, tm = dest_forall ineq in
1288 let set, p_tm' = dest_binary "==>" tm in
1289 let set_th = Hashtbl.find iso_trans_table (rand set) in
1290 let p_tm = mk_abs (x_tm, p_tm') in
1291 let p_var = mk_var ("P", type_of (rand set)) in
1292 let th3 = (SPEC_ALL (REWRITE_RULE[IMP_IMP] set_th)) in
1293 BETA_RULE (INST[p_tm, p_var] th3);;
1300 let gen_general_ineq ineq =
1301 let iso_th = gen_iso_thm ineq in
1302 (* General rewrites before specifying hypermaps *)
1303 let th0 = UNDISCH_ALL (REWRITE_RULE[GSYM IMP_IMP] iso_th) in
1304 let gen_var, rtm = dest_forall(concl th0) in
1305 let ants = lhand rtm in
1306 let set = rand ants in
1307 let th1 = UNDISCH_ALL (SPEC_ALL th0) in
1309 let th_rule th = UNDISCH_ALL (SPEC_ALL (UNDISCH_ALL (SPEC_ALL th))) in
1312 th_rule SUM_NODE_ISO;
1313 th_rule CARD_NODE_ISO;
1314 th_rule SUM_FACE_ISO;
1315 th_rule CARD_FACE_ISO;
1316 th_rule COMPONENTS_ISO_IMAGE;
1317 th_rule HYPERMAP_MAPS_ISO_IMAGE;
1318 th_rule HYPERMAP_INV_MAPS_ISO_IMAGE;
1319 th_rule HYPERMAP_MAPS_ISO_COMM;
1320 th_rule HYPERMAP_INV_MAPS_ISO_COMM;
1321 SUB_CONST_o; ETA_AX;
1322 th_rule SUM_FACE_SUB_CONST;
1325 let th2' = REWRITE_RULE ths th1 in
1327 if (Hashtbl.mem table_set_hyp set) then
1328 PROVE_HYP (Hashtbl.find table_set_hyp set) th2'
1331 let th3 = GEN gen_var (DISCH ants th2) in
1335 (* G -> hypermap_of_list (L:((num)list)list) *)
1336 (* Instantiate correct types *)
1337 let s1 = INST_TYPE [`:real^3#real^3`, aty; `:num#num`, bty] s0 in
1338 let s2 = INST[`hypermap_of_list (L:((num)list)list)`, `G:(num#num)hypermap`] s1 in
1340 let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty] o SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP]) in
1342 let ths = map th_rule in_all_rewrites in
1343 let s3 = REWRITE_RULE ths s2 in
1345 let gen_var2, rtm = dest_forall(concl s3) in
1346 let ants2 = lhand rtm in
1348 let s4 = UNDISCH_ALL (SPEC_ALL s3) in
1352 th_rule CARD_SET_OF_LIST_FACE;
1353 th_rule CARD_SET_OF_LIST_NODE;
1356 let s5 = REWRITE_RULE ths s4 in
1357 let s6 = GEN gen_var2 (DISCH ants2 s5) in
1359 (* Deal with basic variables *)
1360 let s7 = INST var_list s6 in
1361 let s8 = INST[`ESTD V`, `E:(real^3->bool)->bool`] s7 in
1362 let s9 = REWRITE_RULE list_var_rewrites s8 in
1365 (* Basic rewrites *)
1369 UNDISCH_ALL (INST_TYPE [`:num`, aty] (SPEC_ALL COMPONENTS_HYPERMAP_OF_LIST));
1371 let r1 = REWRITE_RULE ths r0 in
1373 (* Further rewrites *)
1374 let r2 = REWRITE_RULE[darts_of_list; IN_SET_OF_LIST; ALL_MEM] r1 in
1379 (***********************)
1384 let get_ineq str = Hashtbl.find constraints str;;
1388 let th = gen_general_ineq (get_ineq "ineq122");;
1389 let th = gen_general_ineq (get_ineq "sol_sum3");;
1390 let th = gen_general_ineq (get_ineq "tau_sum");;
1391 let th = gen_general_ineq (get_ineq "edge_sym");;
1392 let th = gen_general_ineq (get_ineq "ln_def");;
1393 let th = gen_general_ineq (get_ineq "y1_def");;
1394 let th = gen_general_ineq (get_ineq "y2_def");;
1395 let th = gen_general_ineq (get_ineq "y3_def");;
1396 let th = gen_general_ineq (get_ineq "y4_def");;
1397 let th = gen_general_ineq (get_ineq "y5_def");;
1398 let th = gen_general_ineq (get_ineq "y6_def");;
1399 let th = gen_general_ineq (get_ineq "y8_def");;
1400 let th = gen_general_ineq (get_ineq "y9_def");;
1401 let th = gen_general_ineq (get_ineq "RHB");;
1405 let test_list = ref [];;
1407 let iter_f name ineq =
1409 test_list := gen_general_ineq ineq :: !test_list
1411 print_string ("problems: "^name^"; ");;
1414 Hashtbl.iter iter_f constraints;;
1419 (********************************)
1421 let ineq = get_ineq "tau_sum3";;
1423 let iso_th = gen_iso_thm ineq;;
1424 (* General rewrites before specifying hypermaps *)
1425 let th0 = UNDISCH_ALL (REWRITE_RULE[GSYM IMP_IMP] iso_th);;
1426 let gen_var, rtm = dest_forall(concl th0);;
1427 let ants = lhand rtm;;
1428 let set = rand ants;;
1429 let th1 = UNDISCH_ALL (SPEC_ALL th0);;
1431 let th_rule th = UNDISCH_ALL (SPEC_ALL (UNDISCH_ALL (SPEC_ALL th)));;
1434 th_rule SUM_NODE_ISO;
1435 th_rule CARD_NODE_ISO;
1436 th_rule SUM_FACE_ISO;
1437 th_rule CARD_FACE_ISO;
1438 th_rule COMPONENTS_ISO_IMAGE;
1439 th_rule HYPERMAP_MAPS_ISO_IMAGE;
1440 th_rule HYPERMAP_INV_MAPS_ISO_IMAGE;
1441 th_rule HYPERMAP_MAPS_ISO_COMM;
1442 th_rule HYPERMAP_INV_MAPS_ISO_COMM;
1443 SUB_CONST_o; ETA_AX;
1444 th_rule SUM_FACE_SUB_CONST;
1447 let th2' = REWRITE_RULE ths th1;;
1449 if (Hashtbl.mem table_set_hyp set) then
1450 PROVE_HYP (Hashtbl.find table_set_hyp set) th2'
1455 let th3 = GEN gen_var (DISCH ants th2);;
1459 (* G -> hypermap_of_list (L:((num)list)list) *)
1460 (* Instantiate correct types *)
1461 let s1 = INST_TYPE [`:real^3#real^3`, aty; `:num#num`, bty] s0;;
1462 let s2 = INST[`hypermap_of_list (L:((num)list)list)`, `G:(num#num)hypermap`] s1;;
1464 let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty] o SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP]);;
1466 let ths = map th_rule in_all_rewrites;;
1468 let s3 = REWRITE_RULE ths s2;;
1470 let gen_var2, rtm = dest_forall(concl s3);;
1471 let ants2 = lhand rtm;;
1473 let s4 = UNDISCH_ALL (SPEC_ALL s3);;
1477 th_rule CARD_SET_OF_LIST_FACE;
1478 th_rule CARD_SET_OF_LIST_NODE;
1481 let s5 = REWRITE_RULE ths s4;;
1482 let s6 = GEN gen_var2 (DISCH ants2 s5);;
1484 (* Deal with basic variables *)
1485 let s7 = INST var_list s6;;
1486 let s8 = INST[`ESTD V`, `E:(real^3->bool)->bool`] s7;;
1487 let s9 = REWRITE_RULE list_var_rewrites s8;;
1490 (* Basic rewrites *)
1494 UNDISCH_ALL (INST_TYPE [`:num`, aty] (SPEC_ALL COMPONENTS_HYPERMAP_OF_LIST));
1496 let r1 = REWRITE_RULE ths r0;;
1498 (* Further rewrites *)
1499 let r2 = REWRITE_RULE[darts_of_list; IN_SET_OF_LIST; ALL_MEM] r1
1506 (*********************************************************)
1508 (* Integral approximation of inequalities and equalities *)
1510 let mk_decimal (n,m) =
1511 let tm = mk_comb(mk_comb(`DECIMAL`, mk_numeral (abs_num n)), mk_numeral m) in
1512 if (n </ Int 0) then mk_comb(neg_op_real, tm) else tm;;
1516 Given a rational number term `r` and a natural number k,
1517 returns a pair of theorems:
1518 |- low <= r, |- r <= high,
1519 with decimal low and high such that
1520 |low - r| <= 10^(-k) and |high - r| <= 10^(-k)
1522 let real_rat_approx tm precision =
1523 let n = rat_of_term tm in
1524 let m = Int 10 **/ (Int precision) in
1526 let low, high = floor_num n1, ceiling_num n1 in
1528 if precision = 0 then
1529 term_of_rat low, term_of_rat high
1531 mk_decimal (low, m), mk_decimal (high, m) in
1532 let l_th = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op_real l_tm tm)) in
1533 let h_th = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op_real tm h_tm)) in
1538 (* Split a sum into two parts: with and without free variables *)
1540 let sum_th0 = REAL_ARITH `x = x + &0 + &0` and
1541 sum_th1 = REAL_ARITH `(x + y) + b + c = y + (x + b) + c:real` and
1542 sum_th2 = REAL_ARITH `(x + y) + b + c = y + b + (x + c):real` and
1543 sum_th1' = REAL_ARITH `x + b + c = (x + b) + c:real` and
1544 sum_th2' = REAL_ARITH `x + b + c = b + (x + c):real`;;
1547 let c_var_real = `c:real`;;
1550 let split_sum_conv tm =
1551 let rec split_sum_raw_conv tm =
1552 let xy_tm, bc_tm = dest_binop add_op_real tm in
1553 let b_tm, c_tm = dest_binop add_op_real bc_tm in
1554 if (is_binop add_op_real xy_tm) then
1555 let x_tm, y_tm = dest_binop add_op_real xy_tm in
1556 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
1557 let th1 = if (frees x_tm <> []) then inst_th sum_th1 else inst_th sum_th2 in
1558 let th2 = split_sum_raw_conv (rand(concl th1)) in
1561 let inst_th = INST[xy_tm, x_var_real; b_tm, b_var_real; c_tm, c_var_real] in
1562 if (frees xy_tm <> []) then inst_th sum_th1' else inst_th sum_th2' in
1564 let th0 = INST[tm, x_var_real] sum_th0 in
1565 let th1 = split_sum_raw_conv (rand(concl th0)) in
1570 let rearrange_mul_conv tm =
1571 let rec dest_mul tm =
1572 if (is_binop mul_op_real tm) then
1573 let lhs, rhs = dest_binop mul_op_real tm in
1574 let cs, vars = dest_mul rhs in
1575 if (frees lhs = []) then
1580 if (frees tm = []) then
1585 if (list = []) then failwith "rearrange_mul: empty list"
1586 else itlist (fun l r -> mk_binop mul_op_real l r) (tl list) (hd list) in
1588 let cs, vars = dest_mul tm in
1589 let cs_mul, vars_mul = mk_mul cs, mk_mul vars in
1590 let t = mk_eq(tm, mk_binop mul_op_real cs_mul vars_mul) in
1591 EQT_ELIM (REWRITE_CONV[REAL_MUL_AC] t);;
1595 let le_add_th = REAL_ARITH `x + y <= b + c <=> x - b <= c - y:real`;;
1597 (* Moves everything with free variables on the left and performs basic reductions *)
1598 let ineq_rewrite_conv = REWRITE_CONV[real_ge; real_div; DECIMAL] THENC
1599 LAND_CONV REAL_POLY_CONV THENC RAND_CONV REAL_POLY_CONV THENC
1600 LAND_CONV split_sum_conv THENC RAND_CONV split_sum_conv THENC
1601 ONCE_REWRITE_CONV[le_add_th] THENC
1602 LAND_CONV REAL_POLY_CONV THENC RAND_CONV REAL_POLY_CONV THENC
1603 REWRITE_CONV[GSYM real_div] THENC
1604 ONCE_DEPTH_CONV rearrange_mul_conv;;
1609 let le_mul1_th = REAL_ARITH `!x. &1 * x <= x`;;
1610 let ge_mul1_th = REAL_ARITH `!x. x <= &1 * x`;;
1611 let INTERVAL_LO = prove(`interval_arith x (a,b) ==> a <= x`, SIMP_TAC[interval_arith]);;
1612 let INTERVAL_HI = prove(`interval_arith x (a,b) ==> x <= b`, SIMP_TAC[interval_arith]);;
1614 let rec low_approx tm precision =
1615 let low_approx1 tm precision =
1616 if (is_binop mul_op_real tm && frees tm <> []) then
1617 let c, var = dest_binop mul_op_real tm in
1618 let interval_th = approx_interval (create_interval c) precision in
1619 let l_th = MATCH_MP INTERVAL_LO interval_th in
1620 let a, b = dest_binop le_op_real (concl l_th) in
1621 (PROVE_HYP l_th o UNDISCH_ALL o REWRITE_RULE[GSYM IMP_IMP] o SPECL[a; b; var]) REAL_LE_RMUL
1623 if (frees tm = []) then
1624 MATCH_MP INTERVAL_LO (approx_interval (create_interval tm) precision)
1626 SPEC tm le_mul1_th in
1628 if (is_binop add_op_real tm && frees tm <> []) then
1629 let lhs, rhs = dest_binop add_op_real tm in
1630 let l_th = low_approx1 lhs precision in
1631 let r_th = low_approx rhs precision in
1632 MATCH_MP REAL_LE_ADD2 (CONJ l_th r_th)
1634 low_approx1 tm precision;;
1637 let rec hi_approx tm precision =
1638 let hi_approx1 tm precision =
1639 if (is_binop mul_op_real tm && frees tm <> []) then
1640 let c, var = dest_binop mul_op_real tm in
1641 let interval_th = approx_interval (create_interval c) precision in
1642 let h_th = MATCH_MP INTERVAL_HI interval_th in
1643 let a, b = dest_binop le_op_real (concl h_th) in
1644 (PROVE_HYP h_th o UNDISCH_ALL o REWRITE_RULE[GSYM IMP_IMP] o SPECL[a; b; var]) REAL_LE_RMUL
1646 if (frees tm = []) then
1647 MATCH_MP INTERVAL_HI (approx_interval (create_interval tm) precision)
1649 SPEC tm ge_mul1_th in
1651 if (is_binop add_op_real tm && frees tm <> []) then
1652 let lhs, rhs = dest_binop add_op_real tm in
1653 let l_th = hi_approx1 lhs precision in
1654 let r_th = hi_approx rhs precision in
1655 MATCH_MP REAL_LE_ADD2 (CONJ l_th r_th)
1657 hi_approx1 tm precision;;
1661 let approx_le_ineq precision tm =
1662 let lhs, rhs = dest_binop le_op_real tm in
1663 let lhs_th = low_approx lhs precision in
1664 let rhs_th = hi_approx rhs precision in
1665 let ll, lr = dest_binop le_op_real (concl lhs_th) in
1666 let rl, rr = dest_binop le_op_real (concl rhs_th) in
1668 let th0 = ASSUME tm in
1669 let th1 = SPECL[ll; lr; rhs] REAL_LE_TRANS in
1670 let th2 = SPECL[ll; rhs; rr] REAL_LE_TRANS in
1671 let s1 = MATCH_MP th1 (CONJ lhs_th th0) in
1672 MATCH_MP th2 (CONJ s1 rhs_th);;
1675 let integer_approx_le_ineq precision ineq =
1676 let lhs, rhs = dest_binop le_op_real ineq in
1677 let m = (Int 10 **/ Int precision) in
1678 let m_num, m_real = mk_numeral m, term_of_rat m in
1679 let m_pos = SPEC m_num REAL_POS in
1680 let mul_th = SPECL[m_real; lhs; rhs] REAL_LE_LMUL in
1681 let th0 = MATCH_MP mul_th (CONJ m_pos (ASSUME ineq)) in
1682 let th1 = (CONV_RULE ineq_rewrite_conv) th0 in
1683 let approx = approx_le_ineq 0 (concl th1) in
1684 PROVE_HYP th1 approx;;
1687 let create_approximations precision_list ineq =
1688 let ineq_th = ineq_rewrite_conv ineq in
1689 let rhs = rand(concl ineq_th) in
1690 let th0 = CONV_RULE (LAND_CONV (REWRITE_CONV[DECIMAL] THENC REAL_POLY_CONV))
1691 (approx_le_ineq 8 rhs) in
1694 let th1 = integer_approx_le_ineq p (concl th0) in
1695 let th2 = PROVE_HYP th0 th1 in
1696 let th3 = DISCH rhs th2 in
1697 REWRITE_RULE[GSYM ineq_th] th3 in
1699 map int_approx precision_list;;
1701 (**********************************)
1705 let tm = `(&34/ &13 + pi/sol0)* x + &2 + -- &14 / &3 * z <= pi + rho218 + z * sol0 - u / &1000`;;
1706 create_approximations [3;4;5] tm;;
1710 (*************************)
1712 (* Additional step for generalizing hypotheses *)
1715 let LIST_SUM_LMUL = prove(`!(f:A->real) c n. list_sum n (\x. c * f x) = c * list_sum n f`,
1716 GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[list_sum; ITLIST; REAL_MUL_RZERO] THEN
1717 ASM_REWRITE_TAC[GSYM list_sum; REAL_ADD_LDISTRIB]);;
1720 let le_hyp_gen = prove(`!f y. (!x. &0 <= f x) ==> &0 <= f y`, SIMP_TAC[]);;
1721 let le_list_sum_hyp_gen = prove(`!(f:A->real) n. (!x. &0 <= f x) ==> &0 <= list_sum n f`,
1722 REPEAT STRIP_TAC THEN
1723 REWRITE_TAC[list_sum] THEN
1724 SPEC_TAC (`n:(A)list`, `n:(A)list`) THEN
1725 LIST_INDUCT_TAC THEN REWRITE_TAC[ITLIST; REAL_LE_REFL] THEN
1726 MATCH_MP_TAC REAL_LE_ADD THEN
1727 ASM_REWRITE_TAC[]);;
1731 let generalize_hyp th =
1732 let gen_hyp = fun tm ->
1733 let fn, arg = dest_comb (rand tm) in
1734 if (is_comb fn && is_const (rator fn) && (fst o dest_const o rator) fn = "list_sum") then
1735 let f, n = arg, rand fn in
1736 UNDISCH_ALL (ISPECL[f; n] le_list_sum_hyp_gen)
1738 UNDISCH_ALL (ISPECL[fn; arg] le_hyp_gen) in
1740 let hyp_ths = map gen_hyp (hyp th) in
1741 itlist PROVE_HYP hyp_ths th;;
1745 let tm = `list_sum n (\x. s x * r) + &1 / &3 * (azim_dart (V,E) o g) x <= pi`;;
1746 let ths = create_approximations [3] tm;;
1747 map generalize_hyp ths;;
1751 (*******************************)
1754 let generate_ineqs precision_list ineq =
1756 let create_approxs original_th precision_list =
1757 let var, ineq = (dest_abs o rand o rator o concl) original_th in
1758 let final_step = fun approx_th ->
1759 let p_tm', q_tm' = dest_imp (concl approx_th) in
1760 let p_tm, q_tm = mk_abs(var, p_tm'), mk_abs(var, q_tm') in
1761 let list_tm = (rand o concl) original_th in
1762 let mono_th = BETA_RULE (ISPECL[p_tm; q_tm; list_tm] (GEN_ALL MONO_ALL)) in
1763 let s1 = MATCH_MP mono_th (GEN var approx_th) in
1764 MATCH_MP s1 original_th in
1766 let approx_ths0 = map generalize_hyp (create_approximations precision_list ineq) in
1767 let approx_ths1 = map (itlist PROVE_HYP list_var_pos) approx_ths0 in
1768 let approx_ths = map (REWRITE_RULE[GSYM LIST_SUM_LMUL]) approx_ths1 in
1769 map final_step approx_ths in
1772 let ineq_th = gen_general_ineq ineq in
1773 let ineq = (snd o dest_abs o rand o rator o concl) ineq_th in
1774 if (is_eq ineq) then
1775 let eq_th = REWRITE_RULE[GSYM REAL_LE_ANTISYM; GSYM AND_ALL] ineq_th in
1776 let ths1 = create_approxs (CONJUNCT1 eq_th) precision_list in
1777 let ths2 = create_approxs (CONJUNCT2 eq_th) precision_list in
1780 create_approxs ineq_th precision_list, [];;
1785 (*********************************************************************)
1787 (* Table containing all inequalities *)
1788 let ineq_table = Array.init 6 (fun i -> Hashtbl.create 10);;
1789 let ineq_test_table = Array.init 6 (fun i -> Hashtbl.create 10);;
1793 let DECIMAL_INT = prove(`!n. DECIMAL n 1 = &n`, REWRITE_TAC[DECIMAL; REAL_DIV_1]);;
1796 let add_everything_to_table table =
1797 let add_approximations_to_table = fun name ineq ->
1798 let approxs', neg_approxs' = generate_ineqs [3;4;5] ineq in
1799 let approxs = zip (3--5) approxs' in
1800 let neg_approxs = if (neg_approxs' = []) then [] else zip (3--5) neg_approxs' in
1801 let r = CONV_RULE (REWRITE_CONV[DECIMAL_INT] THENC DEPTH_CONV Arith_hash.NUMERAL_TO_NUM_CONV) in
1802 let _ = map (fun (i, t) -> Hashtbl.add (ineq_test_table.(i)) name t;
1803 Hashtbl.add (ineq_table.(i)) name (r t)) approxs in
1804 let _ = map (fun (i, t) -> Hashtbl.add (ineq_test_table.(i)) (name^"_neg") t;
1805 Hashtbl.add (ineq_table.(i)) (name^"_neg") (r t)) neg_approxs in
1808 Hashtbl.iter (fun name ineq -> add_approximations_to_table name ineq) table;;
1811 let find_ineq precision name = Hashtbl.find ineq_table.(precision) name;;
1812 let find_test_ineq precision name = Hashtbl.find ineq_test_table.(precision) name;;
1816 (* Generate and add inequalities for constraints *)
1817 add_everything_to_table constraints;;
1818 add_everything_to_table var_bound_ineqs;;
1821 (**************************)
1825 generate_ineqs [4] (get_ineq "ineq112");;
1827 Hashtbl.iter (fun name ineq -> let _ = generate_ineqs[3;4;5] ineq in ()) constraints;;
1831 (*********************)