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";;
12 (* Definitions of variables *)
15 (* Variables for fans *)
16 (* TODO: these definitions are not necessary *)
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`;;
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)`;;
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)`;;
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))`;;
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;
52 (* Variables for lists *)
55 let list_defs = map new_definition
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`;
80 let list_defs2 = map (REWRITE_RULE[FUN_EQ_THM; o_THM]) list_defs;;
83 let list_var_rewrites =
84 map GSYM list_defs @ map GSYM list_defs2;;
88 (* All variables are nonnegative *)
92 let AZIM_DART_POS = prove(`&0 <= azim_dart (V,E) x`,
93 MP_TAC (ISPEC `x:real^3#real^3` PAIR_SURJECTIVE) THEN
95 ASM_REWRITE_TAC[azim_dart] THEN
98 MP_TAC PI_APPROX_32 THEN REAL_ARITH_TAC;
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);;
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]);;
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]))
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`;
140 (* mod-file variables and definitions *)
143 let var_bound_ineqs = Hashtbl.create 40;;
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`];;
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
171 let ineq_lo = mk_forall(var, mk_imp(cond, l)) in
172 let ineq_hi = mk_forall(var, mk_imp(cond, h)) in
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
181 (* Terms for variables in the model file *)
182 Hashtbl.clear var_bound_ineqs;;
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`;;
207 let inst_t = inst[`:real^3#real^3`, aty] in
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;
235 (* Declare all inequalities in a format which is close to the mod-file format *)
237 let constraints = Hashtbl.create 100;;
238 let add_constraints = map (uncurry (Hashtbl.add constraints));;
240 (* equality constraints *)
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`;
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)`;
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`;
259 "edge_sym", `!e. e IN hyp_edge_pairs (H:(A)hypermap) ==> ye_mod (FST e) = ye_mod (SND e):real`;
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`;
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`;
278 (* inequality constraints *)
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" *)
288 (* definitional inequalities *)
295 "yy10", `!d. (d:A) IN dart (H:(A)hypermap) ==> ye_mod d <= #2.52`;
300 (* tau tame table D inequality (Main Estimate) *)
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`;
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`;
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`;
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`;
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`;
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`;
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`;
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`;
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`;
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`;
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`;
346 "ineq115", `!d:A. d IN hyp_dart3 H ==>
347 (#1.893 - (azim_mod d)) >= #0.0`;
349 "ineq116", `!d:A. d IN hyp_dart3 H ==>
350 ((azim_mod d) - #0.852) >= #0.0`;
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`;
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`;
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`;
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`;
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];
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;;
377 (*************************************)
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
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];
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]));;
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
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]);;
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
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]);;
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
443 REWRITE_TAC[ARITH_RULE `1 <= n <=> 0 < 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];
450 REWRITE_TAC[Hypermap.POWER_1] THEN
451 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
452 EXISTS_TAC `n - 1` THEN
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]);;
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
477 ASM_SIMP_TAC[Hypermap.lemma_dart_inveriant_under_inverse_maps];
480 ASM_SIMP_TAC[COMPONENTS_ISO_IMAGE]);;
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
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)`)
503 ASM_SIMP_TAC[Hypermap.lemma_dart_invariant]);;
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
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
528 MATCH_MP_TAC ISO_NODE_INJ THEN
529 MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
534 MP_TAC (ISPECL [`G:(B)hypermap`; `n:B->bool`] Hypermap.lemma_node_representation) THEN
535 ASM_REWRITE_TAC[] THEN
537 ASM_REWRITE_TAC[Hypermap.NODE_FINITE]);;
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]);;
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]);;
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
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
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]);;
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
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
602 MATCH_MP_TAC ISO_FACE_INJ THEN
603 MAP_EVERY EXISTS_TAC [`G:(B)hypermap`; `H:(A)hypermap`] THEN
608 MP_TAC (ISPECL [`G:(B)hypermap`; `f:B->bool`] Hypermap.lemma_face_representation) THEN
609 ASM_REWRITE_TAC[] THEN
611 ASM_REWRITE_TAC[Hypermap.FACE_FINITE]);;
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]);;
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]);;
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
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
649 MATCH_MP_TAC ALL_DISTINCT_NODE THEN
650 EXISTS_TAC `L:((A)list)list` THEN
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
666 FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list n:A#A->bool`) THEN
667 REWRITE_TAC[MEM_MAP] THEN
670 EXISTS_TAC `n:(A#A)list` THEN
675 MP_TAC (SPEC_ALL SUM_NODE_LIST) THEN
676 ASM_REWRITE_TAC[] THEN
677 DISCH_THEN (fun th -> REWRITE_TAC[th]);
681 POP_ASSUM MP_TAC THEN
682 REWRITE_TAC[MEM_MAP] 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]));;
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[]);;
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
709 MATCH_MP_TAC ALL_DISTINCT_FACE THEN
710 EXISTS_TAC `L:((A)list)list` THEN
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
726 FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
727 REWRITE_TAC[MEM_MAP] THEN
730 EXISTS_TAC `f:(A#A)list` THEN
735 MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
736 ASM_REWRITE_TAC[] THEN
737 DISCH_THEN (fun th -> REWRITE_TAC[th]);
741 POP_ASSUM MP_TAC THEN
742 REWRITE_TAC[MEM_MAP] 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]));;
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[]);;
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]));;
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]));;
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]);;
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]);;
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]);;
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]);;
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
812 FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
815 EXISTS_TAC `f:(A#A)list` THEN
820 MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
823 ASM_REWRITE_TAC[] THEN
824 POP_ASSUM MP_TAC THEN
825 SIMP_TAC[list_of_faces3; MEM_FILTER];
828 DISCH_THEN (fun th -> REWRITE_TAC[th]);
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
837 ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
838 SIMP_TAC[list_of_faces3; MEM_FILTER];
841 DISCH_THEN (fun th -> REWRITE_TAC[th]));;
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
853 FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
856 EXISTS_TAC `f:(A#A)list` THEN
861 MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
864 ASM_REWRITE_TAC[] THEN
865 POP_ASSUM MP_TAC THEN
866 SIMP_TAC[list_of_faces4; MEM_FILTER];
869 DISCH_THEN (fun th -> REWRITE_TAC[th]);
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
878 ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
879 SIMP_TAC[list_of_faces4; MEM_FILTER];
882 DISCH_THEN (fun th -> REWRITE_TAC[th]));;
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
893 FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
896 EXISTS_TAC `f:(A#A)list` THEN
901 MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
904 ASM_REWRITE_TAC[] THEN
905 POP_ASSUM MP_TAC THEN
906 SIMP_TAC[list_of_faces5; MEM_FILTER];
909 DISCH_THEN (fun th -> REWRITE_TAC[th]);
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
918 ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
919 SIMP_TAC[list_of_faces5; MEM_FILTER];
922 DISCH_THEN (fun th -> REWRITE_TAC[th]));;
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
933 FIRST_X_ASSUM (MP_TAC o SPEC `set_of_list f:A#A->bool`) THEN
936 EXISTS_TAC `f:(A#A)list` THEN
941 MP_TAC (SPEC_ALL SUM_FACE_LIST) THEN
944 ASM_REWRITE_TAC[] THEN
945 POP_ASSUM MP_TAC THEN
946 SIMP_TAC[list_of_faces6; MEM_FILTER];
949 DISCH_THEN (fun th -> REWRITE_TAC[th]);
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
958 ASM_REWRITE_TAC[] THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
959 SIMP_TAC[list_of_faces6; MEM_FILTER];
962 DISCH_THEN (fun th -> REWRITE_TAC[th]));;
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]);;
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]);;
977 (*******************************)
980 let in_all_rewrites =
998 let table = Hashtbl.create 10 in
999 let _ = map (uncurry (Hashtbl.add table))
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;
1012 (*************************************)
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
1023 FIRST_X_ASSUM (MP_TAC o SPEC `(g:B->A) d`) THEN
1027 let iso_dart_in = prove(`!(g:B->A) H G d. isomorphism g (G,H) /\ d IN dart G ==>
1029 REWRITE_TAC[isomorphism; BIJ; SURJ; INJ] THEN
1030 REPEAT STRIP_TAC THEN
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
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[];
1048 MATCH_MP_TAC FINITE_SUBSET THEN
1049 EXISTS_TAC `dart G:B->bool` THEN
1050 ASM_REWRITE_TAC[Hypermap.hypermap_lemma]);;
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]);;
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]);;
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]);;
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]);;
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
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
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[]);;
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
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[]);;
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
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
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
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[]);;
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
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
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
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[]);;
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
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
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
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[]);;
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
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
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
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[]);;
1266 let iso_trans_table =
1267 let table = Hashtbl.create 10 in
1268 let _ = map (uncurry (Hashtbl.add table))
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;
1285 (**************************)
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);;
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
1312 let th_rule th = UNDISCH_ALL (SPEC_ALL (UNDISCH_ALL (SPEC_ALL th))) in
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;
1328 let th2' = REWRITE_RULE ths th1 in
1330 if (Hashtbl.mem table_set_hyp set) then
1331 PROVE_HYP (Hashtbl.find table_set_hyp set) th2'
1334 let th3 = GEN gen_var (DISCH ants th2) in
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
1343 let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty] o SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP]) in
1345 let ths = map th_rule in_all_rewrites in
1346 let s3 = REWRITE_RULE ths s2 in
1348 let gen_var2, rtm = dest_forall(concl s3) in
1349 let ants2 = lhand rtm in
1351 let s4 = UNDISCH_ALL (SPEC_ALL s3) in
1355 th_rule CARD_SET_OF_LIST_FACE;
1356 th_rule CARD_SET_OF_LIST_NODE;
1359 let s5 = REWRITE_RULE ths s4 in
1360 let s6 = GEN gen_var2 (DISCH ants2 s5) in
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
1368 (* Basic rewrites *)
1372 UNDISCH_ALL (INST_TYPE [`:num`, aty] (SPEC_ALL COMPONENTS_HYPERMAP_OF_LIST));
1374 let r1 = REWRITE_RULE ths r0 in
1376 (* Further rewrites *)
1377 let r2 = REWRITE_RULE[darts_of_list; IN_SET_OF_LIST; ALL_MEM] r1 in
1382 (***********************)
1387 let get_ineq str = Hashtbl.find constraints str;;
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");;
1408 let test_list = ref [];;
1410 let iter_f name ineq =
1412 test_list := gen_general_ineq ineq :: !test_list
1414 print_string ("problems: "^name^"; ");;
1417 Hashtbl.iter iter_f constraints;;
1422 (********************************)
1424 let ineq = get_ineq "tau_sum3";;
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);;
1434 let th_rule th = UNDISCH_ALL (SPEC_ALL (UNDISCH_ALL (SPEC_ALL th)));;
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;
1450 let th2' = REWRITE_RULE ths th1;;
1452 if (Hashtbl.mem table_set_hyp set) then
1453 PROVE_HYP (Hashtbl.find table_set_hyp set) th2'
1458 let th3 = GEN gen_var (DISCH ants th2);;
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;;
1467 let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty] o SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP]);;
1469 let ths = map th_rule in_all_rewrites;;
1471 let s3 = REWRITE_RULE ths s2;;
1473 let gen_var2, rtm = dest_forall(concl s3);;
1474 let ants2 = lhand rtm;;
1476 let s4 = UNDISCH_ALL (SPEC_ALL s3);;
1480 th_rule CARD_SET_OF_LIST_FACE;
1481 th_rule CARD_SET_OF_LIST_NODE;
1484 let s5 = REWRITE_RULE ths s4;;
1485 let s6 = GEN gen_var2 (DISCH ants2 s5);;
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;;
1493 (* Basic rewrites *)
1497 UNDISCH_ALL (INST_TYPE [`:num`, aty] (SPEC_ALL COMPONENTS_HYPERMAP_OF_LIST));
1499 let r1 = REWRITE_RULE ths r0;;
1501 (* Further rewrites *)
1502 let r2 = REWRITE_RULE[darts_of_list; IN_SET_OF_LIST; ALL_MEM] r1
1509 (*********************************************************)
1511 (* Integral approximation of inequalities and equalities *)
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`;;
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;;
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)
1532 let real_rat_approx tm precision =
1533 let n = rat_of_term tm in
1534 let m = Int 10 **/ (Int precision) in
1536 let low, high = floor_num n1, ceiling_num n1 in
1538 if precision = 0 then
1539 term_of_rat low, term_of_rat high
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
1548 (* Split a sum into two parts: with and without free variables *)
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`;;
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`;;
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
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
1577 let th0 = INST[tm, x_var_real] sum_th0 in
1578 let th1 = split_sum_raw_conv (rand(concl th0)) in
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
1593 if (frees tm = []) then
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
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);;
1608 let le_add_th = REAL_ARITH `x + y <= b + c <=> x - b <= c - y:real`;;
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;;
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]);;
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
1636 if (frees tm = []) then
1637 MATCH_MP INTERVAL_LO (approx_interval (create_interval tm) precision)
1639 SPEC tm le_mul1_th in
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)
1647 low_approx1 tm precision;;
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
1659 if (frees tm = []) then
1660 MATCH_MP INTERVAL_HI (approx_interval (create_interval tm) precision)
1662 SPEC tm ge_mul1_th in
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)
1670 hi_approx1 tm precision;;
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
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);;
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;;
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
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
1712 map int_approx precision_list;;
1714 (**********************************)
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;;
1723 (*************************)
1725 (* Additional step for generalizing hypotheses *)
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]);;
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[]);;
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)
1751 UNDISCH_ALL (ISPECL[fn; arg] le_hyp_gen) in
1753 let hyp_ths = map gen_hyp (hyp th) in
1754 itlist PROVE_HYP hyp_ths th;;
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;;
1764 (*******************************)
1767 let generate_ineqs precision_list ineq =
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
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
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
1793 create_approxs ineq_th precision_list, [];;
1798 (*********************************************************************)
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);;
1806 let DECIMAL_INT = prove(`!n. DECIMAL n 1 = &n`, REWRITE_TAC[DECIMAL; REAL_DIV_1]);;
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
1821 Hashtbl.iter (fun name ineq -> add_approximations_to_table name ineq) table;;
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;;
1829 (* Generate and add inequalities for constraints *)
1830 add_everything_to_table constraints;;
1831 add_everything_to_table var_bound_ineqs;;
1834 (**************************)
1838 generate_ineqs [4] (get_ineq "ineq112");;
1840 Hashtbl.iter (fun name ineq -> let _ = generate_ineqs[3;4;5] ineq in ()) constraints;;
1844 (*********************)