1 (* =========================================================== *)
\r
2 (* Special list conversions *)
\r
3 (* Author: Alexey Solovyev *)
\r
4 (* Date: 2012-10-27 *)
\r
5 (* =========================================================== *)
\r
7 needs "arith/more_float.hl";;
\r
8 needs "list/list_conversions.hl";;
\r
9 needs "misc/vars.hl";;
\r
12 module type List_float_sig = sig
\r
15 val error_mul_f2 : thm
\r
16 val error_mul_f1 : thm
\r
17 val list_sum_conv : (term -> thm) -> term -> thm
\r
18 val list_sum2_le_conv : int -> (int -> term -> term -> thm) -> term -> thm
\r
19 val error_mul_f2_le_conv : int -> term -> term -> thm
\r
20 val error_mul_f2_le_conv2 : int -> term -> term -> thm
\r
21 val error_mul_f1_le_conv : term -> int -> term -> term -> thm
\r
25 module List_float : List_float_sig = struct
\r
32 open List_conversions;;
\r
35 let MY_RULE_FLOAT = UNDISCH_ALL o NUMERALS_TO_NUM o
\r
36 PURE_REWRITE_RULE[FLOAT_OF_NUM; min_exp_def; GSYM IMP_IMP] o SPEC_ALL;;
\r
39 (****************************)
\r
40 (* new definitions *)
\r
42 let list_sum = new_definition `list_sum list f = ITLIST (\t1 t2. f t1 + t2) list (&0)`;;
\r
43 let list_sum2 = new_definition `list_sum2 f l1 l2 = ITLIST2 (\a b c. f a b + c) l1 l2 (&0)`;;
\r
45 let error_mul_f2 = new_definition `error_mul_f2 a int = a * iabs int`;;
\r
46 let error_mul_f1 = new_definition `error_mul_f1 w x list = x * list_sum2 error_mul_f2 w list`;;
\r
48 (*************************************)
\r
49 (* list_sum conversions *)
\r
51 let LIST_SUM_A_EMPTY = prove(`list_sum [] (f:A->real) = &0`, REWRITE_TAC[list_sum; ITLIST]) and
\r
52 LIST_SUM_A_H = prove(`list_sum [h:A] f = f h`, REWRITE_TAC[list_sum; ITLIST; REAL_ADD_RID]) and
\r
53 LIST_SUM_A_CONS = prove(`list_sum (CONS (h:A) t) f = f h + list_sum t f`, REWRITE_TAC[list_sum; ITLIST]);;
\r
56 let list_sum_conv f_conv tm =
\r
57 let ltm, f_tm = dest_comb tm in
\r
58 let list_tm = rand ltm in
\r
59 let list_ty = type_of list_tm in
\r
60 let f_ty = type_of f_tm in
\r
61 let ty = (hd o snd o dest_type) list_ty in
\r
62 let f_var = mk_var("f", f_ty) and
\r
63 h_var = mk_var("h", ty) and
\r
64 t_var = mk_var("t", list_ty) in
\r
65 let inst_t = INST[f_tm, f_var] o INST_TYPE[ty, aty] in
\r
66 let list_sum_h = inst_t LIST_SUM_A_H and
\r
67 list_sum_cons = inst_t LIST_SUM_A_CONS in
\r
69 let rec list_sum_conv_raw = fun h_tm t_tm ->
\r
70 if (is_comb t_tm) then
\r
71 let h_tm', t_tm' = dest_comb t_tm in
\r
72 let th0 = INST[h_tm, h_var; t_tm, t_var] list_sum_cons in
\r
73 let ltm, rtm = dest_comb(rand(concl th0)) in
\r
74 let plus_op, fh_tm = dest_comb ltm in
\r
75 let f_th = f_conv fh_tm in
\r
76 let th1 = list_sum_conv_raw (rand h_tm') t_tm' in
\r
77 let th2 = MK_COMB(AP_TERM plus_op f_th, th1) in
\r
80 let th0 = INST[h_tm, h_var] list_sum_h in
\r
81 let f_th = f_conv (rand(concl th0)) in
\r
84 if (is_comb list_tm) then
\r
85 let h_tm, t_tm = dest_comb list_tm in
\r
86 list_sum_conv_raw (rand h_tm) t_tm
\r
88 inst_t LIST_SUM_A_EMPTY;;
\r
92 (*************************************)
\r
93 (* list_sum2 evaluation *)
\r
95 let LIST_SUM2_0_LE' = (MY_RULE_FLOAT o prove)(`list_sum2 (f:A->B->real) [] [] <= &0`,
\r
96 REWRITE_TAC[list_sum2; ITLIST2; REAL_LE_REFL]);;
\r
97 let LIST_SUM2_1_LE' = (MY_RULE_FLOAT o prove)(`f h1 h2 <= x ==> list_sum2 (f:A->B->real) [h1] [h2] <= x`,
\r
98 REWRITE_TAC[list_sum2; ITLIST2; REAL_ADD_RID]);;
\r
99 let LIST_SUM2_LE' = (MY_RULE_FLOAT o prove)(`f h1 h2 <= x /\ list_sum2 f t1 t2 <= y /\ x + y <= z ==>
\r
100 list_sum2 (f:A->B->real) (CONS h1 t1) (CONS h2 t2) <= z`,
\r
101 REWRITE_TAC[list_sum2; ITLIST2] THEN STRIP_TAC THEN
\r
102 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x + y:real` THEN
\r
103 ASM_SIMP_TAC[REAL_LE_ADD2]);;
\r
106 let list_sum2_le_conv pp f_le_conv tm =
\r
107 let ltm, list2_tm = dest_comb tm in
\r
108 let ltm2, list1_tm = dest_comb ltm in
\r
109 let f_tm = rand ltm2 in
\r
110 let list1_ty = type_of list1_tm and
\r
111 list2_ty = type_of list2_tm and
\r
112 f_ty = type_of f_tm in
\r
113 let ty1 = (hd o snd o dest_type) list1_ty and
\r
114 ty2 = (hd o snd o dest_type) list2_ty in
\r
115 let f_var = mk_var ("f", f_ty) and
\r
116 h1_var, t1_var = mk_var ("h1", ty1), mk_var ("t1", list1_ty) and
\r
117 h2_var, t2_var = mk_var ("h2", ty2), mk_var ("t2", list2_ty) in
\r
118 let inst_t = INST[f_tm, f_var] o INST_TYPE[ty1, aty; ty2, bty] in
\r
119 let list2_0, list2_1, list2_le = inst_t LIST_SUM2_0_LE', inst_t LIST_SUM2_1_LE', inst_t LIST_SUM2_LE' in
\r
121 let rec rec_conv = fun list1_tm list2_tm ->
\r
122 if (is_comb list1_tm) then
\r
123 let h1_tm, t1_tm = dest_cons list1_tm and
\r
124 h2_tm, t2_tm = dest_cons list2_tm in
\r
125 let f_le_th = f_le_conv pp h1_tm h2_tm in
\r
126 let x_tm = (rand o concl) f_le_th in
\r
127 let inst0 = INST[h1_tm, h1_var; h2_tm, h2_var; x_tm, x_var_real] in
\r
128 if is_comb t1_tm then
\r
129 let sum2_t_th = rec_conv t1_tm t2_tm in
\r
130 let y_tm = (rand o concl) sum2_t_th in
\r
131 let xy_th = float_add_hi pp x_tm y_tm in
\r
132 let z_tm = (rand o concl) xy_th in
\r
133 (MY_PROVE_HYP xy_th o MY_PROVE_HYP sum2_t_th o MY_PROVE_HYP f_le_th o
\r
134 INST[y_tm, y_var_real; z_tm, z_var_real; t1_tm, t1_var; t2_tm, t2_var] o
\r
137 if is_comb t2_tm then failwith ("sum2_le_conv: t1 = []; t2 = "^string_of_term t2_tm) else
\r
138 (MY_PROVE_HYP f_le_th o inst0) list2_1
\r
140 if is_comb list2_tm then failwith ("sum2_le_conv: list1 = []; list2 = "^string_of_term list2_tm) else
\r
143 rec_conv list1_tm list2_tm;;
\r
147 (**************************)
\r
148 (* \a b c. a * iabs b + c *)
\r
150 let ERROR_MUL_F2' = (SYM o MY_RULE_FLOAT) error_mul_f2;;
\r
153 (* |- x = a, |- P x y -> P a y *)
\r
154 let rewrite_lhs eq_th th =
\r
155 let ltm, rhs = dest_comb (concl th) in
\r
156 let th0 = AP_THM (AP_TERM (rator ltm) eq_th) rhs in
\r
159 let error_mul_f2_le_conv pp tm1 tm2 =
\r
160 let eq_th = INST[tm1, a_var_real; tm2, int_var] ERROR_MUL_F2' in
\r
161 let iabs_th = float_iabs tm2 in
\r
162 let iabs_tm = (rand o concl) iabs_th in
\r
163 let mul_th = float_mul_hi pp tm1 iabs_tm in
\r
164 let th0 = AP_TERM (mk_comb (mul_op_real, tm1)) iabs_th in
\r
165 let th1 = AP_THM (AP_TERM le_op_real th0) (rand (concl mul_th)) in
\r
166 let le_th = EQ_MP (SYM th1) mul_th in
\r
167 rewrite_lhs eq_th le_th;;
\r
169 let ERROR_MUL_F2_LEMMA' = (MY_RULE_FLOAT o prove)(`iabs int = x /\ a * x <= y ==> error_mul_f2 a int <= y`,
\r
170 REWRITE_TAC[error_mul_f2] THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
\r
172 let error_mul_f2_le_conv2 pp tm1 tm2 =
\r
173 let iabs_th = float_iabs tm2 in
\r
174 let x_tm = (rand o concl) iabs_th in
\r
175 let mul_th = float_mul_hi pp tm1 x_tm in
\r
176 let y_tm = (rand o concl) mul_th in
\r
177 (MY_PROVE_HYP iabs_th o MY_PROVE_HYP mul_th o
\r
178 INST[tm2, int_var; tm1, a_var_real; x_tm, x_var_real; y_tm, y_var_real]) ERROR_MUL_F2_LEMMA';;
\r
182 (**************************)
\r
183 (* \a b c. a * iabs b + c *)
\r
185 let ERROR_MUL_F1_LEMMA' = (MY_RULE_FLOAT o prove)(`x * list_sum2 error_mul_f2 w list <= z ==>
\r
186 error_mul_f1 w x list <= z`, REWRITE_TAC[error_mul_f1]);;
\r
188 let list_sum2_error2_const = `list_sum2 error_mul_f2` and
\r
189 w_var_list = `w:(real)list` and
\r
190 list_var = `list:(real#real)list`;;
\r
192 let error_mul_f1_le_conv w_tm pp x_tm list_tm =
\r
193 (* TODO: if x = 0 then do not need to compute the sum *)
\r
194 let sum2_tm = mk_binop list_sum2_error2_const w_tm list_tm in
\r
195 let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 sum2_tm in
\r
196 let ineq_th = mul_ineq_pos_const_hi pp x_tm sum2_le_th in
\r
197 let z_tm = (rand o concl) ineq_th in
\r
198 (MY_PROVE_HYP ineq_th o
\r
199 INST[x_tm, x_var_real; z_tm, z_var_real; w_tm, w_var_list; list_tm, list_var]) ERROR_MUL_F1_LEMMA';;
\r