1 needs "../formal_lp/hypermap/ineqs/lp_gen_ineqs.hl";;
2 needs "../formal_lp/hypermap/ineqs/lp_approx_ineqs.hl";;
3 needs "../formal_lp/hypermap/ineqs/lp_ineqs_defs.hl";;
4 needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs-compiled.hl";;
5 needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs2-compiled.hl";;
6 needs "../formal_lp/hypermap/ineqs/lp_main_estimate-compiled.hl";;
7 needs "../formal_lp/hypermap/arith_link.hl";;
9 module Lp_ineqs = struct
11 open Lp_ineqs_proofs;;
27 let raw_ineq_list, add_raw_ineq, find_raw_ineq =
30 (fun name std tm th ->
31 table := {name = name; tm = tm; proof = th; std_only = std} :: !table),
32 (fun std_flag name -> find (fun x -> x.name = name && x.std_only = std_flag) !table);;
35 (* Combine all nonlinear inequalities related to linear programs into one definition *)
41 | Tablelp :: _ -> true
42 | Lp_aux _ :: _ -> true
45 fun ineq -> check ineq.tags in
46 let ineq_ids = ["6170936724"] in
47 let lp_ineqs = filter (fun ineq -> check_lp_tags ineq or mem ineq.idv ineq_ids) !Ineq.ineqs in
48 let lp_tms = setify (map (fun t -> t.ineq) lp_ineqs) in
49 let lp_tm = end_itlist (curry mk_conj) lp_tms in
50 new_definition (mk_eq (`lp_ineqs:bool`, lp_tm));;
53 let add_lp_ineqs_hyp =
54 let imp_th = (UNDISCH o MATCH_MP EQ_IMP) lp_ineqs_def in
55 let ths = CONJUNCTS imp_th in
57 itlist PROVE_HYP ths th;;
60 (* Replaces all general hypotheses with lp_cond *)
62 let lp_fan_ths = (CONJUNCTS o UNDISCH_ALL o MATCH_MP EQ_IMP o SPEC_ALL) Lp_ineqs_proofs.lp_fan in
63 let lp_cond_ths = (CONJUNCTS o UNDISCH_ALL o MATCH_MP EQ_IMP o SPEC_ALL o INST_TYPE[`:num`, aty]) Lp_ineqs_proofs.lp_cond in
64 let lp_main_estimate_ths = (CONJUNCTS o UNDISCH_ALL o MATCH_MP EQ_IMP o SPEC_ALL) Lp_main_estimate.lp_main_estimate in
65 fun lp_ineq_flag th ->
66 let th' = (UNDISCH_ALL o SPEC_ALL) th in
67 let th0 = if (not lp_ineq_flag) or is_forall (concl th') or is_binary "ALL" (concl th') then th' else th in
68 let th1 = itlist PROVE_HYP lp_fan_ths th0 in
69 let th2 = itlist PROVE_HYP lp_cond_ths th1 in
70 let th3 = itlist PROVE_HYP lp_main_estimate_ths th2 in
71 add_lp_ineqs_hyp th3;;
74 let parse_lp_ineq s type_hints =
75 let hints = map (fun var, ty -> var, pretype_of_type ty) type_hints in
76 let ptm, l = (parse_preterm o lex o explode) s in
78 (term_of_preterm o retypecheck hints) ptm
80 failwith "Unparsed input following term";;
83 let add_lp_ineq_str (name, std_flag, s_tm, th) =
84 let tm = parse_lp_ineq s_tm ["H", `:(A)hypermap`; "V", `:C->bool`; "node_mod", `:A->C`] in
85 let proof = match th with
87 | Some th -> Some (PURE_REWRITE_RULE[GSYM IMP_IMP] (add_lp_hyp true th)) in
88 add_raw_ineq name std_flag tm proof;;
93 `dart (H:(real^3#real^3)hypermap)`, `dart_of_fan (V:real^3->bool,E)`;
94 `H:(real^3#real^3)hypermap`, `hypermap_of_fan (V:real^3->bool,E)`;
95 `face_map (H:(real^3#real^3)hypermap)`, `f_fan_pair_ext (V:real^3->bool,E)`;
96 `azim_mod:real^3#real^3->real`, `azim_dart (V:real^3->bool,E)`;
97 `azim2_mod:real^3#real^3->real`, `azim2_fan (V:real^3->bool,E)`;
98 `azim3_mod:real^3#real^3->real`, `azim3_fan (V:real^3->bool,E)`;
99 `rhazim_mod:real^3#real^3->real`, `rhazim_fan (V:real^3->bool,E)`;
100 `rhazim2_mod:real^3#real^3->real`, `rhazim2_fan (V:real^3->bool,E)`;
101 `rhazim3_mod:real^3#real^3->real`, `rhazim3_fan (V:real^3->bool,E)`;
102 `sol_mod:(real^3#real^3->bool)->real`, `sol_fan (V:real^3->bool,E)`;
103 `tau_mod:(real^3#real^3->bool)->real`, `tau_fan (V:real^3->bool,E)`;
104 `y1_mod:real^3#real^3->real`, `y1_fan`;
105 `y2_mod:real^3#real^3->real`, `y2_fan`;
106 `y3_mod:real^3#real^3->real`, `y3_fan (V,E)`;
107 `y4_mod:real^3#real^3->real`, `y4_fan (V,E)`;
108 `y5_mod:real^3#real^3->real`, `y5_fan (V,E)`;
109 `y6_mod:real^3#real^3->real`, `y6_fan`;
110 `y7_mod:real^3#real^3->real`, `y7_fan (V,E)`;
111 `y8_mod:real^3#real^3->real`, `y8_fan (V,E)`;
112 `y9_mod:real^3#real^3->real`, `y9_fan (V,E)`;
113 `y4'_mod:real^3#real^3->real`, `y4'_fan (V,E)`;
114 `ye_mod:real^3#real^3->real`, `ye_fan`;
115 `yn_mod:real^3->real`, `yn_fan`;
118 let proof = PURE_REWRITE_RULE[GSYM IMP_IMP] (add_lp_hyp true ineq_th) in
119 let tm0 = concl proof in
120 let tm1 = subst subst_list tm0 in
124 let add_lp_ineq_th (name, std_flag, ineq_th) =
125 let tm1, proof = mk_lp_ineq ineq_th in
126 add_raw_ineq name std_flag tm1 (Some proof);;
128 let gen_raw_ineq_data_str name std_flag str =
129 let tm = parse_lp_ineq str ["H", `:(A)hypermap`; "V", `:C->bool`; "node_mod", `:A->C`] in
130 {name = name; tm = tm; proof = None; std_only = std_flag};;
132 let gen_raw_ineq_data name std_flag ineq_th =
133 let tm1, proof = mk_lp_ineq ineq_th in
134 {name = name; tm = tm1; proof = Some proof; std_only = std_flag};;
136 (******************************)
139 (* Generates a general form of an inequality *)
140 let generate_ineq0 ineq =
141 let th0 = Lp_gen_ineqs.generate_ineq ineq.tm in
142 let th1 = add_lp_hyp true th0 in
144 match ineq.proof with
147 PROVE_HYP proof th1;;
151 let power_th = prove(`!f (x:A). (f POWER 2) x = f (f x) /\ (f POWER 3) x = f (f (f x))`,
152 REWRITE_TAC[Hypermap.POWER_2; Hypermap.THREE; Hypermap.POWER; o_THM]) in
155 let tm, proof = mk_lp_ineq th in
156 generate_ineq0 {name = "tmp"; std_only = false; tm = tm; proof = Some proof} in
159 let ltm, set_tm = dest_comb (concl th) in
160 let p_tm = rand ltm in
161 let var_tm, _ = dest_abs p_tm in
162 let th1 = (BETA_RULE o SPEC var_tm o PURE_REWRITE_RULE[GSYM ALL_MEM]) th in
163 let mem_tm = (fst o dest_imp o concl) th1 in
164 UNDISCH th1, (var_tm, mem_tm) in
166 let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty; `:num`, `:D`; `:real^3`, `:C`] o
167 SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP; RIGHT_IMP_FORALL_THM]) in
171 map (fst o strip_ALL o mk_list_th)
172 [y1_def; y2_def; y3_def; y4_def; y5_def; y6_def; y9_def] in
173 let r = (fst o strip_ALL o add_lp_hyp true o REWRITE_RULE[GSYM IMP_IMP]) in
174 let extra_defs = map r
176 y8_list_def; y4'_list_def; y4'_list_f_def;
177 y4'_list_inv_f_def; y4'_list_ff_def; y4'_list_fff_def;
183 `MEM (d:num#num) (list_of_darts3 L)`, th_rule Lp_gen_theory.list_of_darts3_subset;
184 `MEM (d:num#num) (list_of_darts4 L)`, th_rule Lp_gen_theory.list_of_darts4_subset;
185 `MEM (d:num#num) (list_of_darts5 L)`, th_rule Lp_gen_theory.list_of_darts5_subset;
186 `MEM (d:num#num) (list_of_darts6 L)`, th_rule Lp_gen_theory.list_of_darts6_subset;
189 let rec simplify tm =
191 let ltm, q_tm = dest_comb tm in
192 let imp_tm, p_tm = dest_comb ltm in
193 let p_tm, q_tm = dest_imp tm in
194 let p_th = (PURE_REWRITE_CONV def_ths THENC PURE_REWRITE_CONV[power_th]) p_tm in
195 let q_th = simplify q_tm in
196 MK_COMB (AP_TERM imp_tm p_th, q_th)
200 fun simplify_all_flag ineq ->
201 let th1 = generate_ineq0 ineq in
202 let th2, (var_tm, mem_tm) = strip_ALL th1 in
204 if simplify_all_flag then
205 (PURE_REWRITE_CONV def_ths THENC PURE_REWRITE_CONV[power_th]) (concl th2)
207 simplify (concl th2) in
208 let th3 = EQ_MP eq_th th2 in
211 let mem_th = assoc mem_tm mem_ths in
213 with Failure _ -> th3 in
214 let th5 = (GEN var_tm o DISCH mem_tm) th4 in
215 PURE_REWRITE_RULE[ALL_MEM] th5;;
217 let generate_ineq = generate_ineq1 false;;
219 let add_lp_list_ineq, find_ineq =
220 let ineq_table = Array.init 8 (fun i -> Hashtbl.create 10) in
221 let std_ineq_table = Array.init 8 (fun i -> Hashtbl.create 10) in
222 let add std_flag i pair_flag name ineq_th =
223 let table = if std_flag then std_ineq_table.(i) else ineq_table.(i) in
224 Hashtbl.add table name {ineq_th = ineq_th; pair_flag = pair_flag} in
225 let DECIMAL_INT = prove(`!n. DECIMAL n 1 = &n`, REWRITE_TAC[DECIMAL; REAL_DIV_1]) in
228 let inst = INST[`V:real^3->bool,E:(real^3->bool)->bool`, `fan:(real^3->bool)#((real^3->bool)->bool)`] in
229 map inst Lp_ineqs_def.list_var_pos in
231 let rec rewrite_num_conv real_flag tm =
235 | Abs (v_tm, b_tm) ->
236 ABS v_tm (rewrite_num_conv real_flag b_tm)
237 | Comb (Const ("NUMERAL", _), _) ->
238 Arith_nat.NUMERAL_TO_NUM_CONV tm
239 | Comb (Const ("real_of_num", _) as ltm, rtm) ->
241 AP_TERM ltm (rewrite_num_conv real_flag rtm)
244 | Comb (Comb (Const ("DECIMAL", _), _), _) ->
247 MK_COMB (rewrite_num_conv real_flag ltm, rewrite_num_conv real_flag rtm) in
249 let rewrite_num ineq_th =
250 let th1 = PURE_REWRITE_RULE[DECIMAL_INT] ineq_th in
251 let imp_flag = (is_imp o snd o dest_abs o lhand o concl) th1 in
253 let th2 = PURE_REWRITE_RULE[IMP_IMP] th1 in
254 let th3 = CONV_RULE ((LAND_CONV o ABS_CONV o RAND_CONV) (rewrite_num_conv true)) th2 in
255 let th4 = CONV_RULE ((LAND_CONV o ABS_CONV o LAND_CONV) (rewrite_num_conv false)) th3 in
256 PURE_REWRITE_RULE[GSYM IMP_IMP] th4
258 CONV_RULE (rewrite_num_conv true) th1 in
260 (* add_lp_list_ineq *)
261 (fun (name, std_only, list_ineq_th) ->
262 let approx_ths, neg_approx_ths = Lp_approx_ineqs.generate_ineqs pos_thms [3;4;5;6;7] list_ineq_th in
263 let set_name = (fst o dest_const o rator o rand o concl o hd) approx_ths in
264 let pair_flag, approx_ths, neg_approx_ths =
265 if set_name = "list_dart_pairs" then
266 let r = PURE_REWRITE_RULE[Lp_gen_theory.ALL_list_dart_pairs_split; BETA_THM; FST; SND] in
267 true, map r approx_ths, map r neg_approx_ths
269 false, approx_ths, neg_approx_ths in
270 let approx_ths = zip (3--7) approx_ths in
271 let neg_approx_ths = if (neg_approx_ths = []) then [] else zip (3--7) neg_approx_ths in
273 let r = rewrite_num in
275 let _ = map (fun (i, t) -> add true i pair_flag name (r t)) approx_ths in
276 let _ = map (fun (i, t) -> add true i pair_flag (name^"_neg") (r t)) neg_approx_ths in
279 let _ = map (fun (i, t) -> add false i pair_flag name (r t)) approx_ths in
280 let _ = map (fun (i, t) -> add false i pair_flag (name^"_neg") (r t)) neg_approx_ths in
284 (fun std_flag precision name ->
287 Hashtbl.find std_ineq_table.(precision) name
288 with Not_found -> Hashtbl.find ineq_table.(precision) name
290 Hashtbl.find ineq_table.(precision) name);;
293 (* Generates all list inequalities from raw inequalities *)
294 let process_raw_ineqs =
296 Format.print_string s; Format.print_newline(); Format.print_flush() in
297 let counter = ref 0 and
300 let process_ineq ineq =
301 let _ = counter := !counter + 1 in
302 let _ = report (sprintf "Processing: %s (%d / %d)" ineq.name !counter !total) in
303 let th = generate_ineq ineq in
304 add_lp_list_ineq (ineq.name, ineq.std_only, th) in
307 let ineqs = raw_ineq_list() in
308 let _ = counter := 0 in
309 let _ = total := length ineqs in
310 let _ = map process_ineq (raw_ineq_list()) in