1 needs "contravening_ineqs.hl";;
2 needs "list_hypermap_computations.hl";;
3 needs "arith/prove_lp.hl";;
6 let plus_op_real = `(+):real->real->real` and
7 mul_op_real = `( * ):real->real->real`;;
10 let REAL_ADD_ASSOC' = (SYM o SPEC_ALL) REAL_ADD_ASSOC;;
11 let x_var_real = `x:real` and
12 y_var_real = `y:real` and
13 z_var_real = `z:real`;;
15 (* Performs the following conversions:
16 (a + ... + c) + d = a + ... + c + d *)
17 let rec plus_assoc_conv tm =
18 if (is_binop plus_op_real tm) then
19 let lhs, rhs = dest_binop plus_op_real tm in
20 if (is_binop plus_op_real lhs) then
21 let x_tm, y_tm = dest_binop plus_op_real lhs in
22 let th0 = INST[x_tm, x_var_real; y_tm, y_var_real; rhs, z_var_real] REAL_ADD_ASSOC' in
23 let ltm, rtm = dest_comb(rand(concl th0)) in
24 TRANS th0 (AP_TERM ltm (plus_assoc_conv rtm))
31 let tm = `(&1 + x + y + &2) + (z + t)`;;
34 test 1000 (REWRITE_CONV[GSYM REAL_ADD_ASSOC]) tm;;
36 test 1000 plus_assoc_conv tm;;
42 let prove_hypermap_lp hyp_str precision constraints target_var_bounds var_bounds =
43 let list_hyp, list_thm, fun_table = compute_all hyp_str in
45 let table_set_rewrites =
46 let hyp = Hashtbl.create 10 in
47 let _ = map (fun set, name -> Hashtbl.add hyp set (Hashtbl.find list_thm name))
49 "list_of_darts", "darts";
50 "list_of_darts3", "darts3";
51 "list_of_darts4", "darts4";
52 "list_of_dartsX", "dartsX";
53 "list_of_nodes", "nodes";
54 "list_of_edges", "edges";
55 "list_of_faces", "faces";
56 "list_of_faces3", "faces3";
57 "list_of_faces4", "faces4";
58 "list_of_faces5", "faces5";
59 "list_of_faces6", "faces6";
63 let l_var_list = `L:((num)list)list` in
65 (* Rewrites subterms in the inequality *)
66 let rewrite_ineq ineq =
67 let rec rewrite_lhs = fun tm ->
68 let rewrite_one = fun tm ->
69 if (is_binop mul_op_real tm) then
70 let mul_tm, var_tm = dest_comb tm in
71 let var_f, arg = dest_comb var_tm in
73 let rec convert_arg = fun arg ->
75 let ltm, sub_arg' = dest_comb arg in
76 let const_name = (fst o dest_const) (if (is_const ltm) then ltm else rator ltm) in
77 if (const_name = "CONS" or const_name = ",") then
81 let sub_arg_th = convert_arg sub_arg' in
82 let th0 = AP_TERM ltm sub_arg_th in
83 let rtm = rand(concl th0) in
85 if (const_name = "set_of_list") then
87 else if (const_name = "FST") then
89 else if (const_name = "SND") then
92 let table = Hashtbl.find fun_table const_name in
93 Hashtbl.find table (rand rtm) in
96 failwith ("convert_arg: "^const_name)
100 let arg_th = convert_arg arg in
101 AP_TERM mul_tm (AP_TERM var_f arg_th)
104 (* tm should be list_sum *)
105 list_sum_conv BETA_CONV tm in
107 if (is_binop plus_op_real tm) then
108 let lhs, rhs = dest_binop plus_op_real tm in
109 let lhs_th = rewrite_one lhs in
110 let rhs_th = rewrite_lhs rhs in
111 let th1 = MK_COMB(AP_TERM plus_op_real lhs_th, rhs_th) in
112 if (is_binop plus_op_real (rand(concl lhs_th))) then
113 let th2 = plus_assoc_conv (rand(concl th1)) in
120 let th0 = BETA_RULE ineq in
121 let ltm, rtm = dest_comb(concl th0) in
122 let op_tm, l_tm = dest_comb ltm in
123 let lhs_th = rewrite_lhs l_tm in
124 EQ_MP (AP_THM (AP_TERM op_tm lhs_th) rtm) th0 in
126 (* This function generates all inequalities from a given base inequality *)
127 let get_ineqs = fun ineq indices ->
128 let t0 = INST[list_hyp, l_var_list] ineq in
129 let t1 = MY_PROVE_HYP (Hashtbl.find list_thm "good_list") t0 in
130 let all_tm, set_tm = dest_comb (concl t1) in
131 let set_th = Hashtbl.find table_set_rewrites ((fst o dest_const o rator) set_tm) in
132 let t2 = EQ_MP (AP_TERM all_tm set_th) t1 in
133 let ths = select_all t2 indices in
134 map rewrite_ineq ths in
137 let precision_constant = Int 10 **/ (Int precision) and
138 target_bound = `&12` in
140 (* This function generates all inequalities with the given name and indices,
141 multiplies these inequalities by given coefficients, and adds up the obtained
143 let sum_step = fun (name, indices, c) ->
145 let ineq = find_ineq precision name in
146 let ineqs = get_ineqs ineq indices in
147 let s1 = map transform_le_ineq (zip ineqs c) in
148 List.fold_left add_step' dummy s1
150 failwith ("Problem: "^name) in
153 let s1' = List.fold_left add_step' dummy (map sum_step constraints) in
154 let s1 = mul_step s1' (mk_real_int precision_constant) in
155 let s2 = List.fold_left add_step' dummy (map sum_step target_var_bounds) in
156 let s3 = List.fold_left add_step' dummy (map sum_step var_bounds) in
157 let s4 = add_step' (add_step' s1 s2) s3 in
159 (* Final transformations *)
160 let r6 = CONV_RULE (DEPTH_CONV NUM_TO_NUMERAL_CONV) s4 in
161 let m = term_of_rat (precision_constant */ precision_constant */ precision_constant) in
162 let r7 = mul_rat_step r6 (mk_comb (`(/) (&1)`, m)) in
163 let r8 = REWRITE_RULE[lin_f; ITLIST; REAL_ADD_RID] r7 in
164 let r9 = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op ((rand o concl) r8) target_bound)) in
165 MATCH_MP REAL_LE_TRANS (CONJ r8 r9);;
170 (*******************************************)
173 needs "test_out.hl";;
174 prove_hypermap_lp hypermap_string precision constraints target_variables variable_bounds;;
178 (prove_hypermap_lp hypermap_string precision constraints target_variables) variable_bounds;;
185 (*************************************)
189 let prove_hypermap_lp hyp_str precision constraints target_var_bounds var_bounds =
190 (* Compute all components of the hypermap *)
191 let list_hyp, list_thm = compute_all hyp_str in
192 let hyp_rewrites1 = map (Hashtbl.find list_thm)
194 "darts"; "darts3"; "darts4"; "dartsX";
196 "faces"; "faces3"; "faces4"; "faces5"; "faces6"
198 let hyp_rewrites2 = map (Hashtbl.find list_thm)
204 let l_var_list = `L:((num)list)list` in
206 (* This function generates all inequalities from a given base inequality *)
207 let get_ineqs = fun ineq indices ->
208 let t0 = INST[list_hyp, l_var_list] ineq in
209 let t1 = MY_PROVE_HYP (Hashtbl.find list_thm "good_list") t0 in
210 let t2 = REWRITE_RULE hyp_rewrites1 t1 in
211 let ths = select_all t2 indices in
212 let ineqs = map (REWRITE_RULE ([list_sum; ITLIST; REAL_ADD_RID; set_of_list; GSYM REAL_ADD_ASSOC] @ hyp_rewrites2)) ths in
215 let precision_constant = Int 10 **/ (Int precision) in
216 let target_bound = `&12` in
218 (* This function generates all inequalities with the given name and indices,
219 multiplies these inequalities by given coefficients, and adds up the obtained
221 let sum_step = fun (name, indices, c) ->
223 let ineq = find_ineq precision name in
224 let ineqs = get_ineqs ineq indices in
225 let s1 = map transform_le_ineq (zip ineqs c) in
226 List.fold_left add_step' dummy s1
228 failwith ("Problem: "^name) in
231 let s1' = List.fold_left add_step' dummy (map sum_step constraints) in
232 let s1 = mul_step s1' (mk_real_int precision_constant) in
233 let s2 = List.fold_left add_step' dummy (map sum_step target_var_bounds) in
234 let s3 = List.fold_left add_step' dummy (map sum_step var_bounds) in
235 let s4 = add_step' (add_step' s1 s2) s3 in
237 (* Final transformations *)
238 let r6 = CONV_RULE (DEPTH_CONV NUM_TO_NUMERAL_CONV) s4 in
239 let m = term_of_rat (precision_constant */ precision_constant */ precision_constant) in
240 let r7 = mul_rat_step r6 (mk_comb (`(/) (&1)`, m)) in
241 let r8 = REWRITE_RULE[lin_f; ITLIST; REAL_ADD_RID] r7 in
242 let r9 = EQT_ELIM (REAL_RAT_LE_CONV (mk_binop le_op ((rand o concl) r8) target_bound)) in
243 MATCH_MP REAL_LE_TRANS (CONJ r8 r9);;
247 (***********************************)
250 needs "test_out.hl";;
254 (prove_hypermap_lp hypermap_string precision constraints target_variables) variable_bounds;;
258 (* Compute all components of the hypermap *)
259 let hyp_str = hypermap_string and
260 target_var_bounds = target_variables and
261 var_bounds = variable_bounds;;
264 test 1 (compute_all) hyp_str;;
267 (**************************)
272 test 10 (get_ineqs ineq) indices;;
275 test 10 (get_ineqs2 ineq) indices;;