formal_lp/old/formal_interval/m_taylor_old.hl

   1 needs "../formal_lp/formal_interval/m_taylor.hl";;\r
   2 \r
   3 module M_taylor_old = struct\r
   4 \r
   5 let gen_second_bounded_eq_thm n =\r
   6   let ty, _, x_var, _, _, _, domain_var = get_types_and_vars n in\r
   7   let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(j).(i)) (1--n)) (1--n) in\r
   8   let dd_bounds_list = mk_list (map (fun l -> mk_list (l, real_pair_ty)) dd_vars, real_pair_list_ty) in\r
   9   let th0 = (SPECL[domain_var; dd_bounds_list] o inst_first_type_var ty) second_bounded in\r
  10   let th1 = (CONV_RULE NUM_REDUCE_CONV o REWRITE_RULE[all_n]) th0 in\r
  11     th1;;\r
  12 \r
  13 let gen_second_bounded_poly_thm poly_tm partials2 =\r
  14   let x_var, _ = dest_abs poly_tm in\r
  15   let n = get_dim x_var in\r
  16   let partials2' = List.flatten partials2 in\r
  17   let second_th = (REWRITE_RULE partials2' o SPECL [poly_tm]) (gen_second_bounded_eq_thm n) in\r
  18     second_th;;\r
  19 \r
  20 \r
  21 let gen_second_bounded_poly_thm0 poly_tm =\r
  22   let x_var, _ = dest_abs poly_tm in\r
  23   let n = get_dim x_var in\r
  24   let partials = map (fun i -> gen_partial_poly i poly_tm) (1--n) in\r
  25   let get_partial i eq_th = \r
  26     let partial_i = gen_partial_poly i (rand (concl eq_th)) in\r
  27     let pi = (rator o lhand o concl) partial_i in\r
  28       REWRITE_RULE[GSYM partial2] (TRANS (AP_TERM pi eq_th) partial_i) in\r
  29   let partials2 = map (fun th -> map (fun i -> get_partial i th) (1--n)) partials in\r
  30     gen_second_bounded_poly_thm poly_tm partials2;;\r
  31 \r
  32 \r
  33 (* eval_second_bounded *)\r
  34 let eval_second_bounded pp0 second_bounded_th =\r
  35   let poly_tm = (lhand o rator o lhand o concl) second_bounded_th in\r
  36   let th0 = second_bounded_th in\r
  37   let n = (get_dim o fst o dest_abs) poly_tm in\r
  38   let x_vector = mk_vector_list (map (fun i -> x_vars_array.(i)) (1--n)) and\r
  39       z_vector = mk_vector_list (map (fun i -> z_vars_array.(i)) (1--n)) in\r
  40   let _, _, _, _, _, _, domain_var = get_types_and_vars n in\r
  41 \r
  42   let th1 = INST[mk_pair (x_vector, z_vector), domain_var] th0 in\r
  43   let th2 = REWRITE_RULE[IN_INTERVAL; dimindex_array.(n)] th1 in\r
  44   let th3 = REWRITE_RULE[gen_in_interval n; GSYM interval_arith] th2 in\r
  45   let th4 = (REWRITE_RULE[CONJ_ACI] o REWRITE_RULE (Array.to_list comp_thms_array.(n))) th3 in\r
  46   let final_th0 = (UNDISCH_ALL o MATCH_MP iffRL) th4 in\r
  47 \r
  48   let x_var, h_tm = (dest_forall o hd o hyp) final_th0 in\r
  49   let _, h2 = dest_imp h_tm in\r
  50   let concl_ints = striplist dest_conj h2 in\r
  51 \r
  52   let i_funs = map (fun int -> \r
  53                       let expr, var = dest_interval_arith int in\r
  54                         (eval_constants pp0 o build_interval_fun) expr, var) concl_ints in\r
  55 \r
  56   let rec split_rules i_list =\r
  57     match i_list with\r
  58       | [] -> ([], [])\r
  59       | ((i_fun, var_tm) :: es) -> \r
  60           let th_list, i_list' = split_rules es in\r
  61             match i_fun with\r
  62               | Int_const th -> (var_tm, th) :: th_list, i_list'\r
  63               | _ -> th_list, (var_tm, i_fun) :: i_list' in\r
  64 \r
  65   let const_th_list, i_list0 = split_rules i_funs in\r
  66   let th5 = itlist (fun (var_tm, th) th0 -> \r
  67                       let b_tm = rand (concl th) in\r
  68                         (REWRITE_RULE[th] o INST[b_tm, var_tm]) th0) const_th_list (SYM th4) in\r
  69   let final_th = REWRITE_RULE[GSYM IMP_IMP] th5 in\r
  70   let v_list, i_list' = unzip i_list0 in\r
  71   let i_list = find_and_replace_all i_list' [] in\r
  72 \r
  73     fun pp x_vector_tm z_vector_tm ->\r
  74       let x_vals = dest_vector x_vector_tm and\r
  75           z_vals = dest_vector z_vector_tm in\r
  76         if length x_vals <> n or length z_vals <> n then \r
  77           failwith (sprintf "Wrong vector size; expected size: %d" n)\r
  78         else\r
  79           let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and\r
  80               z_vars = map (fun i -> z_vars_array.(i)) (1--n) in\r
  81 \r
  82           let inst_th = (INST (zip x_vals x_vars) o INST (zip z_vals z_vars)) final_th in\r
  83             if (not o is_eq) (concl inst_th) then inst_th \r
  84             else\r
  85               let x_var, lhs = (dest_forall o lhand o concl) inst_th in\r
  86               let hs = (butlast o striplist dest_imp) lhs in\r
  87               let vars = map (rand o rator) hs in\r
  88               let int_vars = zip vars (map ASSUME hs) in\r
  89 \r
  90               let dd_ints = eval_interval_fun_list pp i_list int_vars in\r
  91               let inst_dd = map2 (fun var th -> (rand o concl) th, var) v_list dd_ints in\r
  92               let inst_th2 = INST inst_dd inst_th in\r
  93 \r
  94               let conj_th = end_itlist CONJ dd_ints in\r
  95               let lhs_th = GEN x_var (itlist DISCH hs conj_th) in\r
  96                 EQ_MP inst_th2 lhs_th;;\r
  97 \r
  98 \r
  99 \r
 100 let eval_second_bounded_poly0 pp0 poly_tm =\r
 101   eval_second_bounded pp0 (gen_second_bounded_poly_thm0 poly_tm);;\r
 102 \r
 103 \r
 104 (*************************************)\r
 105 \r
 106 let eval_m_taylor pp0 diff2c_th lin_th second_th =\r
 107   let poly_tm = (rand o concl) diff2c_th in\r
 108   let n = (get_dim o fst o dest_abs) poly_tm in\r
 109   let eval_lin = eval_lin_approx pp0 lin_th and\r
 110       eval_second = eval_second_bounded pp0 second_th in\r
 111 \r
 112   let ty, _, x_var, f_var, y_var, w_var, domain_var = get_types_and_vars n in\r
 113   let th0 = (SPEC_ALL o inst_first_type_var ty) m_taylor_interval in\r
 114   let th1 = INST[poly_tm, f_var] th0 in\r
 115   let th2 = (UNDISCH_ALL o REWRITE_RULE[GSYM IMP_IMP] o MATCH_MP iffRL o REWRITE_RULE[diff2c_th]) th1 in\r
 116 \r
 117     fun p_lin p_second domain_th ->\r
 118       let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in\r
 119       let x_tm, z_tm = dest_pair domain_tm in\r
 120 \r
 121       let lin_th = eval_lin p_lin y_tm and\r
 122           second_th = eval_second p_second x_tm z_tm in\r
 123 \r
 124       let _, _, f_bounds, df_bounds_list = dest_lin_approx (concl lin_th) in\r
 125       let dd_bounds_list = (rand o concl) second_th in\r
 126       let df_var = mk_var ("d_bounds_list", type_of df_bounds_list) and\r
 127           dd_var = mk_var ("dd_bounds_list", type_of dd_bounds_list) in\r
 128 \r
 129         (MY_PROVE_HYP domain_th o MY_PROVE_HYP lin_th o MY_PROVE_HYP second_th o\r
 130            INST[domain_tm, domain_var; y_tm, y_var; w_tm, w_var;\r
 131                 f_bounds, f_bounds_var; df_bounds_list, df_var; dd_bounds_list, dd_var]) th2;;\r
 132 \r
 133 \r
 134 let eval_m_taylor_poly0 pp0 poly_tm =\r
 135   let diff2_th = gen_diff2c_domain_poly poly_tm in\r
 136   let x_var, _ = dest_abs poly_tm in\r
 137   let n = get_dim x_var in\r
 138   let partials = map (fun i -> gen_partial_poly i poly_tm) (1--n) in\r
 139   let get_partial i eq_th = \r
 140     let partial_i = gen_partial_poly i (rand (concl eq_th)) in\r
 141     let pi = (rator o lhand o concl) partial_i in\r
 142       REWRITE_RULE[GSYM partial2] (TRANS (AP_TERM pi eq_th) partial_i) in\r
 143   let partials2 = map (fun th -> map (fun i -> get_partial i th) (1--n)) partials in\r
 144   let second_th = gen_second_bounded_poly_thm poly_tm partials2 in\r
 145   let diff_th = gen_diff_poly poly_tm in\r
 146   let lin_th = gen_lin_approx_poly_thm poly_tm diff_th partials in\r
 147     eval_m_taylor pp0 diff2_th lin_th second_th;;\r
 148 \r
 149 \r
 150 \r
 151 (********************************)\r
 152 (* m_taylor_error *)\r
 153 \r
 154 \r
 155 (* Sum of the list elements *)\r
 156 \r
 157 let ITLIST2_EQ_SUM = prove(`!(f:A->real) l1 l2. LENGTH l1 = LENGTH l2 ==>\r
 158                                ITLIST2 (\x y z. x * f y + z) l1 l2 (&0) =\r
 159                                sum (1..(LENGTH l1)) (\i. EL (i - 1) l1 * f (EL (i - 1) l2))`,\r
 160    GEN_TAC THEN\r
 161      LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; ITLIST2] THEN TRY ARITH_TAC THENL\r
 162      [\r
 163        REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH];\r
 164        ALL_TAC\r
 165      ] THEN\r
 166      REWRITE_TAC[eqSS] THEN DISCH_TAC THEN\r
 167      FIRST_X_ASSUM (MP_TAC o SPEC `t':(A)list`) THEN ASM_REWRITE_TAC[] THEN\r
 168      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 169      REWRITE_TAC[GSYM add1n] THEN\r
 170      new_rewrite [] [] SUM_ADD_SPLIT THEN REWRITE_TAC[ARITH] THEN\r
 171      REWRITE_TAC[TWO; add1n; SUM_SING_NUMSEG; subnn; EL; HD] THEN\r
 172      REWRITE_TAC[GSYM addn1; SUM_OFFSET; REAL_EQ_ADD_LCANCEL] THEN\r
 173      MATCH_MP_TAC SUM_EQ THEN move ["i"] THEN REWRITE_TAC[IN_NUMSEG] THEN DISCH_TAC THEN\r
 174      ASM_SIMP_TAC[ARITH_RULE `1 <= i ==> (i + 1) - 1 = SUC (i - 1)`; EL; TL]);;\r
 175 \r
 176 \r
 177 \r
 178 let M_TAYLOR_ERROR_ITLIST2 = prove(`!f domain y w dd_bounds_list error. \r
 179              m_cell_domain domain y (vector w) ==>\r
 180              second_bounded (f:real^N->real) domain dd_bounds_list ==>\r
 181              LENGTH w = dimindex (:N) ==>\r
 182                  LENGTH dd_bounds_list = dimindex (:N) ==>\r
 183                  ALL (\list. LENGTH list = dimindex (:N)) dd_bounds_list ==>\r
 184                  ITLIST2 (\x list z. x * ITLIST2 (\a b c. a * iabs b + c) w list (&0) + z) \r
 185                  w dd_bounds_list (&0) <= error ==>\r
 186                  m_taylor_error f domain (vector w) error`,\r
 187    REWRITE_TAC[second_bounded; m_taylor_error] THEN REPEAT GEN_TAC THEN\r
 188      set_tac "s" `ITLIST2 _1 _2 _3 _4` THEN\r
 189      move ["domain"; "second"; "lw"; "ldd"; "ldd_all"; "s_le"; "x"; "x_in"] THEN\r
 190      SUBGOAL_THEN `!i. i IN 1..dimindex (:N) ==> &0 <= EL (i - 1) w` (LABEL_TAC "w_ge0") THENL\r
 191      [\r
 192        GEN_TAC THEN DISCH_TAC THEN REMOVE_THEN "domain" MP_TAC THEN new_rewrite [] [] pair_eq THEN\r
 193          REWRITE_TAC[m_cell_domain] THEN\r
 194          DISCH_THEN (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN\r
 195          ASM_SIMP_TAC[VECTOR_COMPONENT] THEN REAL_ARITH_TAC;\r
 196        ALL_TAC\r
 197      ] THEN\r
 198      MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `s:real` THEN ASM_REWRITE_TAC[] THEN\r
 199      EXPAND_TAC "s" THEN\r
 200      new_rewrite [] [] ITLIST2_EQ_SUM THEN ASM_REWRITE_TAC[] THEN\r
 201      MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[FINITE_NUMSEG] THEN\r
 202      move ["i"; "i_in"] THEN ASM_SIMP_TAC[VECTOR_COMPONENT] THEN\r
 203      USE_THEN "i_in" (ASSUME_TAC o REWRITE_RULE[IN_NUMSEG]) THEN\r
 204      MATCH_MP_TAC REAL_LE_LMUL THEN ASM_SIMP_TAC[] THEN\r
 205      new_rewrite [] [] ITLIST2_EQ_SUM THEN ASM_REWRITE_TAC[] THENL\r
 206      [\r
 207        REMOVE_THEN "ldd_all" MP_TAC THEN REWRITE_TAC[GSYM ALL_EL] THEN\r
 208          DISCH_THEN (MP_TAC o SPEC `i - 1`) THEN\r
 209          ANTS_TAC THENL\r
 210          [\r
 211            ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN ARITH_TAC;\r
 212            ALL_TAC\r
 213          ] THEN\r
 214          DISCH_THEN (fun th -> REWRITE_TAC[th]);\r
 215        ALL_TAC\r
 216      ] THEN\r
 217      MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[FINITE_NUMSEG] THEN\r
 218      move ["j"; "j_in"] THEN ASM_SIMP_TAC[VECTOR_COMPONENT] THEN\r
 219      USE_THEN "j_in" (ASSUME_TAC o REWRITE_RULE[IN_NUMSEG]) THEN\r
 220      MATCH_MP_TAC REAL_LE_LMUL THEN ASM_SIMP_TAC[] THEN\r
 221      FIRST_X_ASSUM (MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[ALL_N_EL] THEN\r
 222      DISCH_THEN (MP_TAC o SPEC `i - 1`) THEN ANTS_TAC THENL\r
 223      [\r
 224        REMOVE_THEN "i_in" MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC;\r
 225        ALL_TAC\r
 226      ] THEN\r
 227      DISCH_THEN (MP_TAC o SPEC `j - 1`) THEN ANTS_TAC THENL\r
 228      [\r
 229        REMOVE_THEN "ldd_all" MP_TAC THEN REWRITE_TAC[GSYM ALL_EL] THEN\r
 230          DISCH_THEN (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THENL\r
 231          [\r
 232            REMOVE_THEN "i_in" MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC;\r
 233            ALL_TAC\r
 234          ] THEN\r
 235          REMOVE_THEN "j_in" MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC;\r
 236        ALL_TAC\r
 237      ] THEN\r
 238      SUBGOAL_THEN `1 + j - 1 = j /\ 1 + i - 1 = i` (fun th -> REWRITE_TAC[th]) THENL\r
 239      [\r
 240        REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN ARITH_TAC;\r
 241        ALL_TAC\r
 242      ] THEN\r
 243      REWRITE_TAC[partial2] THEN\r
 244      DISCH_THEN (MP_TAC o MATCH_MP interval_arith_abs_le) THEN\r
 245      DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[REAL_LE_REFL]);;\r
 246 \r
 247 \r
 248 let M_TAYLOR_ERROR_LIST_SUM2 = prove(`!f domain y w dd_bounds_list error. \r
 249              m_cell_domain domain y (vector w) ==>\r
 250              second_bounded (f:real^N->real) domain dd_bounds_list ==>\r
 251              LENGTH w = dimindex (:N) ==>\r
 252                  LENGTH dd_bounds_list = dimindex (:N) ==>\r
 253                  ALL (\list. LENGTH list = dimindex (:N)) dd_bounds_list ==>\r
 254                  list_sum2 (error_mul_f1 w) w dd_bounds_list <= error ==>\r
 255                  m_taylor_error f domain (vector w) error`,\r
 256   REWRITE_TAC[list_sum2; error_mul_f1; error_mul_f2; M_TAYLOR_ERROR_ITLIST2]);;\r
 257 \r
 258 \r
 259 \r
 260 (**********************************)\r
 261 \r
 262 let m_taylor_error_array = Array.init (max_dim + 1)\r
 263   (fun i -> if i < 1 then TRUTH else\r
 264      (MY_RULE_NUM o REWRITE_RULE[dimindex_array.(i)] o inst_first_type_var (n_type_array.(i)))\r
 265        M_TAYLOR_ERROR_LIST_SUM2);;\r
 266 \r
 267 \r
 268 let REFL_CONV tm = \r
 269   let rhs = rand tm in\r
 270   let th0 = EQT_INTRO (REFL rhs) in\r
 271     th0;;\r
 272 \r
 273 let eval_m_taylor_error n pp m_taylor_th =\r
 274   let domain_th, _, _, second_th = dest_m_taylor_thms n m_taylor_th in\r
 275   let f_tm = (rand o rator o rator o concl) second_th in\r
 276   let domain_tm, y_tm, w_tm = (dest_m_cell_domain o concl) domain_th in\r
 277   let dd_bounds_list = (rand o concl) second_th in\r
 278   let w_list = rand w_tm in\r
 279   let y_var = mk_var ("y", type_of y_tm) and\r
 280       f_var = mk_var ("f", type_of f_tm) and\r
 281       domain_var = mk_var ("domain", type_of domain_tm) in\r
 282 \r
 283   let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP second_th o \r
 284                INST[dd_bounds_list, dd_bounds_list_var; w_list, w_var_list;\r
 285                     domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_error_array.(n) in\r
 286 \r
 287   let len_dd = eval_length dd_bounds_list in\r
 288   let len_w = eval_length w_list in\r
 289 \r
 290   let th1 = (MY_PROVE_HYP len_dd o MY_PROVE_HYP len_w) th0 in\r
 291   let [all_tm; sum2_tm] = hyp th1 in\r
 292   let l_conv = (BETA_CONV THENC LAND_CONV length_conv THENC REFL_CONV) in\r
 293   let all_len = EQT_ELIM (all_conv_univ l_conv all_tm) in\r
 294   let sum2_le_th = list_sum2_le_conv pp (error_mul_f1_le_conv w_list) (lhand sum2_tm) in\r
 295   let error_tm = (rand o concl) sum2_le_th in\r
 296     (MY_PROVE_HYP all_len o MY_PROVE_HYP sum2_le_th o INST[error_tm, error_var]) th1;;\r
 297 \r
 298 \r
 299 (**********************)\r
 300 (* taylor_upper_bound *)\r
 301 \r
 302 \r
 303 (* upper *)\r
 304 let M_TAYLOR_UPPER_BOUND' = prove(`m_cell_domain domain (y:real^N) (vector w) /\\r
 305                                     diff2c_domain domain f /\\r
 306                                     m_lin_approx f y (f_lo, f_hi) d_bounds_list /\\r
 307                                     m_taylor_error f domain (vector w) error /\\r
 308                                     list_sum2 error_mul_f2 w d_bounds_list <= b /\\r
 309                                     b + inv(&2) * error <= a /\\r
 310                                     f_hi + a <= hi /\\r
 311                                     LENGTH w = dimindex (:N) /\ LENGTH d_bounds_list = dimindex (:N) ==>\r
 312                                     (!p. p IN interval [domain] ==> f p <= hi)`,\r
 313    REWRITE_TAC[m_lin_approx; interval_arith; list_sum2; error_mul_f2; ALL_N_EL] THEN\r
 314      set_tac "s" `ITLIST2 _1 _2 _3 _4` THEN STRIP_TAC THEN\r
 315      SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL\r
 316      [\r
 317        UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN\r
 318          SIMP_TAC[diff2_domain; diff2c_domain; diff2c];\r
 319        ALL_TAC\r
 320      ] THEN\r
 321      apply_tac m_taylor_upper_bound THEN\r
 322      MAP_EVERY EXISTS_TAC [`y:real^N`; `vector w:real^N`; `error:real`; `f_hi:real`] THEN\r
 323      ASM_REWRITE_TAC[] THEN \r
 324      MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `f_hi + a:real` THEN\r
 325      ASM_REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN\r
 326      ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN\r
 327      MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `b + inv (&2) * error` THEN\r
 328      ASM_REWRITE_TAC[] THEN\r
 329      MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN\r
 330      MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `s:real` THEN ASM_REWRITE_TAC[] THEN\r
 331      EXPAND_TAC "s" THEN new_rewrite [] [] ITLIST2_EQ_SUM THEN ASM_REWRITE_TAC[] THEN\r
 332      MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[FINITE_NUMSEG] THEN REPEAT STRIP_TAC THEN\r
 333      new_rewrite [] [] REAL_MUL_SYM THEN \r
 334      MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_SIMP_TAC[VECTOR_COMPONENT; REAL_LE_REFL; REAL_ABS_POS] THEN\r
 335      CONJ_TAC THENL\r
 336      [\r
 337        UNDISCH_TAC `m_cell_domain domain (y:real^N) (vector w)` THEN\r
 338          new_rewrite [] [] pair_eq THEN REWRITE_TAC[m_cell_domain] THEN\r
 339          DISCH_THEN (MP_TAC o SPEC `x:num`) THEN ASM_REWRITE_TAC[] THEN\r
 340          ASM_SIMP_TAC[VECTOR_COMPONENT] THEN REAL_ARITH_TAC;\r
 341        ALL_TAC\r
 342      ] THEN\r
 343      FIRST_X_ASSUM (MP_TAC o SPEC `x - 1`) THEN\r
 344      ANTS_TAC THENL\r
 345      [\r
 346        POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC;\r
 347        ALL_TAC\r
 348      ] THEN\r
 349      DISCH_THEN (MP_TAC o MATCH_MP interval_arith_abs_le) THEN\r
 350      SUBGOAL_THEN `1 + x - 1 = x` (fun th -> REWRITE_TAC[th]) THENL\r
 351      [\r
 352        POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC;\r
 353        ALL_TAC\r
 354      ] THEN\r
 355      DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[REAL_LE_REFL]);;\r
 356 \r
 357 \r
 358 (* lower *)\r
 359 let M_TAYLOR_LOWER_BOUND' = prove(`m_cell_domain domain (y:real^N) (vector w) /\\r
 360                                     diff2c_domain domain f /\\r
 361                                     m_lin_approx f y (f_lo, f_hi) d_bounds_list /\\r
 362                                     m_taylor_error f domain (vector w) error /\\r
 363                                     list_sum2 error_mul_f2 w d_bounds_list <= b /\\r
 364                                     b + inv(&2) * error <= a /\\r
 365                                     lo <= f_lo - a /\\r
 366                                     LENGTH w = dimindex (:N) /\ LENGTH d_bounds_list = dimindex (:N) ==>\r
 367                                     (!p. p IN interval [domain] ==> lo <= f p)`,\r
 368    REWRITE_TAC[m_lin_approx; interval_arith; list_sum2; error_mul_f2; ALL_N_EL] THEN\r
 369      set_tac "s" `ITLIST2 _1 _2 _3 _4` THEN STRIP_TAC THEN\r
 370      SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL\r
 371      [\r
 372        UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN\r
 373          SIMP_TAC[diff2_domain; diff2c_domain; diff2c];\r
 374        ALL_TAC\r
 375      ] THEN\r
 376      apply_tac m_taylor_lower_bound THEN\r
 377      MAP_EVERY EXISTS_TAC [`y:real^N`; `vector w:real^N`; `error:real`; `f_lo:real`] THEN\r
 378      ASM_REWRITE_TAC[] THEN \r
 379      MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `f_lo - a:real` THEN\r
 380      ASM_REWRITE_TAC[real_div; real_sub] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN\r
 381      ASM_REWRITE_TAC[REAL_LE_REFL; REAL_LE_NEG] THEN\r
 382      ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN\r
 383      MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `b + inv (&2) * error` THEN\r
 384      ASM_REWRITE_TAC[] THEN\r
 385      MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN\r
 386      MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `s:real` THEN ASM_REWRITE_TAC[] THEN\r
 387      EXPAND_TAC "s" THEN new_rewrite [] [] ITLIST2_EQ_SUM THEN ASM_REWRITE_TAC[] THEN\r
 388      MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[FINITE_NUMSEG] THEN REPEAT STRIP_TAC THEN\r
 389      new_rewrite [] [] REAL_MUL_SYM THEN \r
 390      MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_SIMP_TAC[VECTOR_COMPONENT; REAL_LE_REFL; REAL_ABS_POS] THEN\r
 391      CONJ_TAC THENL\r
 392      [\r
 393        UNDISCH_TAC `m_cell_domain domain (y:real^N) (vector w)` THEN\r
 394          new_rewrite [] [] pair_eq THEN REWRITE_TAC[m_cell_domain] THEN\r
 395          DISCH_THEN (MP_TAC o SPEC `x:num`) THEN ASM_REWRITE_TAC[] THEN\r
 396          ASM_SIMP_TAC[VECTOR_COMPONENT] THEN REAL_ARITH_TAC;\r
 397        ALL_TAC\r
 398      ] THEN\r
 399      FIRST_X_ASSUM (MP_TAC o SPEC `x - 1`) THEN\r
 400      ANTS_TAC THENL\r
 401      [\r
 402        POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC;\r
 403        ALL_TAC\r
 404      ] THEN\r
 405      DISCH_THEN (MP_TAC o MATCH_MP interval_arith_abs_le) THEN\r
 406      SUBGOAL_THEN `1 + x - 1 = x` (fun th -> REWRITE_TAC[th]) THENL\r
 407      [\r
 408        POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC;\r
 409        ALL_TAC\r
 410      ] THEN\r
 411      DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[REAL_LE_REFL]);;\r
 412 \r
 413 \r
 414 (* bound *)\r
 415 let M_TAYLOR_BOUND' = \r
 416   prove(`m_cell_domain domain (y:real^N) (vector w) /\\r
 417           diff2c_domain domain f /\\r
 418           m_lin_approx f y (f_lo, f_hi) d_bounds_list /\\r
 419           m_taylor_error f domain (vector w) error /\\r
 420           list_sum2 error_mul_f2 w d_bounds_list <= b /\\r
 421           b + inv(&2) * error <= a /\\r
 422           lo <= f_lo - a /\\r
 423           f_hi + a <= hi /\\r
 424           LENGTH w = dimindex (:N) /\ LENGTH d_bounds_list = dimindex (:N) ==>\r
 425               (!x. x IN interval [domain] ==> interval_arith (f x) (lo, hi))`,\r
 426         REPEAT STRIP_TAC THEN REWRITE_TAC[interval_arith] THEN\r
 427           MP_TAC M_TAYLOR_UPPER_BOUND' THEN\r
 428           MP_TAC M_TAYLOR_LOWER_BOUND' THEN\r
 429           ASM_REWRITE_TAC[] THEN\r
 430           REPEAT (DISCH_THEN (MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC));;\r
 431 \r
 432 \r
 433 \r
 434 (* arrays *)\r
 435 \r
 436 let m_taylor_upper_array = Array.init (max_dim + 1)\r
 437   (fun i -> if i < 1 then TRUTH else\r
 438      (MY_RULE_NUM o REWRITE_RULE[dimindex_array.(i); float_inv2_th] o inst_first_type_var (n_type_array.(i)))\r
 439        M_TAYLOR_UPPER_BOUND');;\r
 440 \r
 441 \r
 442 let m_taylor_lower_array = Array.init (max_dim + 1)\r
 443   (fun i -> if i < 1 then TRUTH else\r
 444      (MY_RULE_NUM o REWRITE_RULE[dimindex_array.(i); float_inv2_th] o inst_first_type_var (n_type_array.(i)))\r
 445        M_TAYLOR_LOWER_BOUND');;\r
 446 \r
 447 \r
 448 let m_taylor_bound_array = Array.init (max_dim + 1)\r
 449   (fun i -> if i < 1 then TRUTH else\r
 450      (MY_RULE_NUM o REWRITE_RULE[dimindex_array.(i); float_inv2_th] o inst_first_type_var (n_type_array.(i)))\r
 451        M_TAYLOR_BOUND');;\r
 452 \r
 453 \r
 454 \r
 455 (* upper *)\r
 456 let b_var_real = `b:real`;;\r
 457 \r
 458 let eval_m_taylor_upper_bound n pp m_taylor_th =\r
 459   let domain_th, diff_th, lin_th, _ = dest_m_taylor_thms n m_taylor_th in\r
 460   let error_th = eval_m_taylor_error n pp m_taylor_th in\r
 461 \r
 462   let f_tm, _, f_bounds, d_bounds_list = dest_lin_approx (concl lin_th) and\r
 463       domain_tm, y_tm, w_tm = (dest_m_cell_domain o concl) domain_th and\r
 464       error_tm = (rand o concl) error_th in\r
 465   let w_list = rand w_tm and\r
 466       f_lo, f_hi = dest_pair f_bounds in\r
 467   \r
 468   let y_var = mk_var ("y", type_of y_tm) and\r
 469       f_var = mk_var ("f", type_of f_tm) and\r
 470       domain_var = mk_var ("domain", type_of domain_tm) in\r
 471 \r
 472   let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP diff_th o \r
 473                MY_PROVE_HYP lin_th o MY_PROVE_HYP error_th o\r
 474                INST[d_bounds_list, d_bounds_list_var; w_list, w_var_list;\r
 475                     f_lo, f_lo_var; f_hi, f_hi_var; error_tm, error_var;\r
 476                     domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_upper_array.(n) in\r
 477 \r
 478   let len_d_th = eval_length d_bounds_list and\r
 479       len_w_th = eval_length w_list in\r
 480   let th1 = (MY_PROVE_HYP len_d_th o MY_PROVE_HYP len_w_th) th0 in\r
 481 \r
 482   let sum2_tm = (C List.nth 2 o hyp) th1 in\r
 483   let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 (lhand sum2_tm) in\r
 484   let b_tm = (rand o concl) sum2_le_th in\r
 485 \r
 486   let ineq1_th = \r
 487     let ( * ), ( + ) = float_mul_hi pp, add_ineq_hi pp in\r
 488       mk_refl_ineq b_tm + float_inv2 * error_tm in\r
 489 \r
 490   let a_tm = (rand o concl) ineq1_th in\r
 491   let ineq2_th = float_add_hi pp f_hi a_tm in\r
 492   let hi_tm = (rand o concl) ineq2_th in\r
 493     (MY_PROVE_HYP ineq2_th o MY_PROVE_HYP ineq1_th o MY_PROVE_HYP sum2_le_th o\r
 494        INST[a_tm, a_var_real; b_tm, b_var_real; hi_tm, hi_var_real]) th1;;\r
 495 \r
 496 \r
 497 (* lower *)\r
 498 let eval_m_taylor_lower_bound n pp m_taylor_th =\r
 499   let domain_th, diff_th, lin_th, _ = dest_m_taylor_thms n m_taylor_th in\r
 500   let error_th = eval_m_taylor_error n pp m_taylor_th in\r
 501 \r
 502   let f_tm, _, f_bounds, d_bounds_list = dest_lin_approx (concl lin_th) and\r
 503       domain_tm, y_tm, w_tm = (dest_m_cell_domain o concl) domain_th and\r
 504       error_tm = (rand o concl) error_th in\r
 505   let w_list = rand w_tm and\r
 506       f_lo, f_hi = dest_pair f_bounds in\r
 507   \r
 508   let y_var = mk_var ("y", type_of y_tm) and\r
 509       f_var = mk_var ("f", type_of f_tm) and\r
 510       domain_var = mk_var ("domain", type_of domain_tm) in\r
 511 \r
 512   let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP diff_th o \r
 513                MY_PROVE_HYP lin_th o MY_PROVE_HYP error_th o\r
 514                INST[d_bounds_list, d_bounds_list_var; w_list, w_var_list;\r
 515                     f_lo, f_lo_var; f_hi, f_hi_var; error_tm, error_var;\r
 516                     domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_lower_array.(n) in\r
 517 \r
 518   let len_d_th = eval_length d_bounds_list and\r
 519       len_w_th = eval_length w_list in\r
 520   let th1 = (MY_PROVE_HYP len_d_th o MY_PROVE_HYP len_w_th) th0 in\r
 521 \r
 522   let sum2_tm = (C List.nth 2 o hyp) th1 in\r
 523   let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 (lhand sum2_tm) in\r
 524   let b_tm = (rand o concl) sum2_le_th in\r
 525 \r
 526   let ineq1_th = \r
 527     let ( * ), ( + ) = float_mul_hi pp, add_ineq_hi pp in\r
 528       mk_refl_ineq b_tm + float_inv2 * error_tm in\r
 529 \r
 530   let a_tm = (rand o concl) ineq1_th in\r
 531   let ineq2_th = float_sub_lo pp f_lo a_tm in\r
 532   let lo_tm = (lhand o concl) ineq2_th in\r
 533 \r
 534     (MY_PROVE_HYP ineq2_th o MY_PROVE_HYP ineq1_th o MY_PROVE_HYP sum2_le_th o\r
 535        INST[a_tm, a_var_real; b_tm, b_var_real; lo_tm, lo_var_real]) th1;;\r
 536 \r
 537 \r
 538 \r
 539 (* bound *)\r
 540 let eval_m_taylor_bound n pp m_taylor_th =\r
 541   let domain_th, diff_th, lin_th, _ = dest_m_taylor_thms n m_taylor_th in\r
 542   let error_th = eval_m_taylor_error n pp m_taylor_th in\r
 543 \r
 544   let f_tm, _, f_bounds, d_bounds_list = dest_lin_approx (concl lin_th) and\r
 545       domain_tm, y_tm, w_tm = (dest_m_cell_domain o concl) domain_th and\r
 546       error_tm = (rand o concl) error_th in\r
 547   let w_list = rand w_tm and\r
 548       f_lo, f_hi = dest_pair f_bounds in\r
 549   \r
 550   let y_var = mk_var ("y", type_of y_tm) and\r
 551       f_var = mk_var ("f", type_of f_tm) and\r
 552       domain_var = mk_var ("domain", type_of domain_tm) in\r
 553 \r
 554   let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP diff_th o \r
 555                MY_PROVE_HYP lin_th o MY_PROVE_HYP error_th o\r
 556                INST[d_bounds_list, d_bounds_list_var; w_list, w_var_list;\r
 557                     f_lo, f_lo_var; f_hi, f_hi_var; error_tm, error_var;\r
 558                     domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_bound_array.(n) in\r
 559 \r
 560   let len_d_th = eval_length d_bounds_list and\r
 561       len_w_th = eval_length w_list in\r
 562   let th1 = (MY_PROVE_HYP len_d_th o MY_PROVE_HYP len_w_th) th0 in\r
 563 \r
 564   let sum2_tm = (C List.nth 3 o hyp) th1 in\r
 565   let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 (lhand sum2_tm) in\r
 566   let b_tm = (rand o concl) sum2_le_th in\r
 567 \r
 568   let ineq1_th = \r
 569     let ( * ), ( + ) = float_mul_hi pp, add_ineq_hi pp in\r
 570       mk_refl_ineq b_tm + float_inv2 * error_tm in\r
 571 \r
 572   let a_tm = (rand o concl) ineq1_th in\r
 573   let ineq2_th = float_add_hi pp f_hi a_tm in\r
 574   let hi_tm = (rand o concl) ineq2_th in\r
 575 \r
 576   let ineq3_th = float_sub_lo pp f_lo a_tm in\r
 577   let lo_tm = (lhand o concl) ineq3_th in\r
 578 \r
 579     (MY_PROVE_HYP ineq3_th o MY_PROVE_HYP ineq2_th o \r
 580        MY_PROVE_HYP ineq1_th o MY_PROVE_HYP sum2_le_th o\r
 581        INST[a_tm, a_var_real; b_tm, b_var_real; hi_tm, hi_var_real; lo_tm, lo_var_real]) th1;;\r
 582 \r
 583 (******************************)\r
 584 (* taylor_upper_partial_bound *)\r
 585 (* taylor_lower_partial_bound *)\r
 586 \r
 587 \r
 588 (* upper *)\r
 589 let M_TAYLOR_UPPER_PARTIAL_BOUND' = \r
 590   prove(`m_taylor_interval f domain (y:real^N) (vector w) f_bounds d_bounds_list dd_bounds_list /\\r
 591           i IN 1..dimindex (:N) /\\r
 592           EL (i - 1) d_bounds_list = (df_lo, df_hi) /\\r
 593           EL (i - 1) dd_bounds_list = dd_list /\\r
 594           LENGTH d_bounds_list = dimindex (:N) /\ \r
 595           LENGTH dd_bounds_list = dimindex (:N) /\\r
 596           LENGTH dd_list = dimindex (:N) /\ LENGTH w = dimindex (:N) /\\r
 597           list_sum2 error_mul_f2 w dd_list <= error /\\r
 598           df_hi + error <= hi ==>\r
 599           (!p. p IN interval [domain] ==> partial i f p <= hi)`,\r
 600    REWRITE_TAC[m_taylor_interval; m_lin_approx; second_bounded; ALL_N_EL] THEN STRIP_TAC THEN\r
 601      SUBGOAL_THEN `1 <= i /\ i <= dimindex (:N)` (LABEL_TAC "i_in") THENL\r
 602      [\r
 603        ASM_REWRITE_TAC[GSYM IN_NUMSEG];\r
 604        ALL_TAC\r
 605      ] THEN\r
 606      SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL\r
 607      [\r
 608        UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN\r
 609          SIMP_TAC[diff2_domain; diff2c_domain; diff2c];\r
 610        ALL_TAC\r
 611      ] THEN\r
 612      apply_tac m_taylor_upper_partial_bound THEN\r
 613      MAP_EVERY EXISTS_TAC [`y:real^N`; `vector w:real^N`; `error:real`; `df_hi:real`] THEN\r
 614      ASM_REWRITE_TAC[] THEN\r
 615      FIRST_X_ASSUM (MP_TAC o SPEC `i - 1`) THEN\r
 616      ASM_SIMP_TAC[ARITH_RULE `1 <= i /\ i <= n ==> i - 1 < n`] THEN\r
 617      ASM_SIMP_TAC[ARITH_RULE `1 <= i ==> 1 + i - 1 = i`; interval_arith] THEN\r
 618      DISCH_THEN (fun th -> ALL_TAC) THEN\r
 619      REWRITE_TAC[m_taylor_partial_error] THEN REPEAT STRIP_TAC THEN\r
 620      UNDISCH_TAC `list_sum2 error_mul_f2 w dd_list <= error` THEN\r
 621      REWRITE_TAC[list_sum2; error_mul_f2] THEN\r
 622      MATCH_MP_TAC (REWRITE_RULE[GSYM IMP_IMP] REAL_LE_TRANS) THEN\r
 623      new_rewrite [] [] ITLIST2_EQ_SUM THEN ASM_REWRITE_TAC[] THEN\r
 624      MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[FINITE_NUMSEG] THEN\r
 625      move ["j"; "j_in"] THEN\r
 626      ASM_SIMP_TAC[VECTOR_COMPONENT] THEN\r
 627      MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL\r
 628      [\r
 629        UNDISCH_TAC `m_cell_domain domain (y:real^N) (vector w)` THEN\r
 630          new_rewrite [] [] pair_eq THEN REWRITE_TAC[m_cell_domain] THEN\r
 631          DISCH_THEN (MP_TAC o SPEC `j:num`) THEN ASM_REWRITE_TAC[] THEN\r
 632          ASM_SIMP_TAC[VECTOR_COMPONENT] THEN REAL_ARITH_TAC;\r
 633        ALL_TAC\r
 634      ] THEN\r
 635      FIRST_X_ASSUM (MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN\r
 636      DISCH_THEN (MP_TAC o SPEC `i - 1`) THEN\r
 637      ASM_SIMP_TAC[ARITH_RULE `1 <= i /\ i <= n ==> i - 1 < n`] THEN\r
 638      DISCH_THEN (MP_TAC o SPEC `j - 1`) THEN\r
 639      FIRST_ASSUM MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN DISCH_TAC THEN\r
 640      ASM_SIMP_TAC[ARITH_RULE `1 <= j /\ j <= n ==> j - 1 < n`] THEN\r
 641      ASM_SIMP_TAC[ARITH_RULE `!i. 1 <= i ==> 1 + i - 1 = i`; GSYM partial2] THEN\r
 642      DISCH_THEN (MP_TAC o MATCH_MP interval_arith_abs_le) THEN\r
 643      DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[REAL_LE_REFL]);;\r
 644 \r
 645 \r
 646 (* lower *)\r
 647 let M_TAYLOR_LOWER_PARTIAL_BOUND' = \r
 648   prove(`m_taylor_interval f domain (y:real^N) (vector w) f_bounds d_bounds_list dd_bounds_list /\\r
 649           i IN 1..dimindex (:N) /\\r
 650           EL (i - 1) d_bounds_list = (df_lo, df_hi) /\\r
 651           EL (i - 1) dd_bounds_list = dd_list /\\r
 652           LENGTH d_bounds_list = dimindex (:N) /\ \r
 653           LENGTH dd_bounds_list = dimindex (:N) /\\r
 654           LENGTH dd_list = dimindex (:N) /\ LENGTH w = dimindex (:N) /\\r
 655           list_sum2 error_mul_f2 w dd_list <= error /\\r
 656           lo <= df_lo - error ==>\r
 657           (!p. p IN interval [domain] ==> lo <= partial i f p)`,\r
 658    REWRITE_TAC[m_taylor_interval; m_lin_approx; second_bounded; ALL_N_EL] THEN STRIP_TAC THEN\r
 659      SUBGOAL_THEN `1 <= i /\ i <= dimindex (:N)` (LABEL_TAC "i_in") THENL\r
 660      [\r
 661        ASM_REWRITE_TAC[GSYM IN_NUMSEG];\r
 662        ALL_TAC\r
 663      ] THEN\r
 664      SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL\r
 665      [\r
 666        UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN\r
 667          SIMP_TAC[diff2_domain; diff2c_domain; diff2c];\r
 668        ALL_TAC\r
 669      ] THEN\r
 670      apply_tac m_taylor_lower_partial_bound THEN\r
 671      MAP_EVERY EXISTS_TAC [`y:real^N`; `vector w:real^N`; `error:real`; `df_lo:real`] THEN\r
 672      ASM_REWRITE_TAC[] THEN\r
 673      FIRST_X_ASSUM (MP_TAC o SPEC `i - 1`) THEN\r
 674      ASM_SIMP_TAC[ARITH_RULE `1 <= i /\ i <= n ==> i - 1 < n`] THEN\r
 675      ASM_SIMP_TAC[ARITH_RULE `1 <= i ==> 1 + i - 1 = i`; interval_arith] THEN\r
 676      DISCH_THEN (fun th -> ALL_TAC) THEN\r
 677      REWRITE_TAC[m_taylor_partial_error] THEN REPEAT STRIP_TAC THEN\r
 678      UNDISCH_TAC `list_sum2 error_mul_f2 w dd_list <= error` THEN\r
 679      REWRITE_TAC[list_sum2; error_mul_f2] THEN\r
 680      MATCH_MP_TAC (REWRITE_RULE[GSYM IMP_IMP] REAL_LE_TRANS) THEN\r
 681      new_rewrite [] [] ITLIST2_EQ_SUM THEN ASM_REWRITE_TAC[] THEN\r
 682      MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[FINITE_NUMSEG] THEN\r
 683      move ["j"; "j_in"] THEN\r
 684      ASM_SIMP_TAC[VECTOR_COMPONENT] THEN\r
 685      MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL\r
 686      [\r
 687        UNDISCH_TAC `m_cell_domain domain (y:real^N) (vector w)` THEN\r
 688          new_rewrite [] [] pair_eq THEN REWRITE_TAC[m_cell_domain] THEN\r
 689          DISCH_THEN (MP_TAC o SPEC `j:num`) THEN ASM_REWRITE_TAC[] THEN\r
 690          ASM_SIMP_TAC[VECTOR_COMPONENT] THEN REAL_ARITH_TAC;\r
 691        ALL_TAC\r
 692      ] THEN\r
 693      FIRST_X_ASSUM (MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN\r
 694      DISCH_THEN (MP_TAC o SPEC `i - 1`) THEN\r
 695      ASM_SIMP_TAC[ARITH_RULE `1 <= i /\ i <= n ==> i - 1 < n`] THEN\r
 696      DISCH_THEN (MP_TAC o SPEC `j - 1`) THEN\r
 697      FIRST_ASSUM MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN DISCH_TAC THEN\r
 698      ASM_SIMP_TAC[ARITH_RULE `1 <= j /\ j <= n ==> j - 1 < n`] THEN\r
 699      ASM_SIMP_TAC[ARITH_RULE `!i. 1 <= i ==> 1 + i - 1 = i`; GSYM partial2] THEN\r
 700      DISCH_THEN (MP_TAC o MATCH_MP interval_arith_abs_le) THEN\r
 701      DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[REAL_LE_REFL]);;\r
 702 \r
 703 \r
 704 let M_TAYLOR_PARTIAL_BOUND' = \r
 705   prove(`m_taylor_interval f domain (y:real^N) (vector w) f_bounds d_bounds_list dd_bounds_list /\\r
 706           i IN 1..dimindex (:N) /\\r
 707           EL (i - 1) d_bounds_list = (df_lo, df_hi) /\\r
 708           EL (i - 1) dd_bounds_list = dd_list /\\r
 709           LENGTH d_bounds_list = dimindex (:N) /\ \r
 710           LENGTH dd_bounds_list = dimindex (:N) /\\r
 711           LENGTH dd_list = dimindex (:N) /\ LENGTH w = dimindex (:N) /\\r
 712           list_sum2 error_mul_f2 w dd_list <= error /\\r
 713           df_hi + error <= hi ==>\r
 714           lo <= df_lo - error ==>\r
 715           (!x. x IN interval [domain] ==> interval_arith (partial i f x) (lo, hi))`,\r
 716         REPEAT STRIP_TAC THEN\r
 717           REWRITE_TAC[interval_arith] THEN\r
 718           MP_TAC M_TAYLOR_UPPER_PARTIAL_BOUND' THEN \r
 719           MP_TAC M_TAYLOR_LOWER_PARTIAL_BOUND' THEN\r
 720           ASM_REWRITE_TAC[] THEN\r
 721           REPEAT (DISCH_THEN (MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC));;\r
 722 \r
 723 \r
 724 \r
 725 (* The (n, i)-th element is the theorem |- i IN 1..dimindex (:n) *)\r
 726 let i_in_array = Array.init (max_dim + 1)\r
 727   (fun i -> Array.init (i + 1)\r
 728      (fun j ->\r
 729         if j < 1 then TRUTH else\r
 730           let j_tm = mk_small_numeral j in\r
 731           let tm0 = `j IN 1..dimindex (:N)` in\r
 732           let tm1 = (subst [j_tm, `j:num`] o inst [n_type_array.(i), nty]) tm0 in\r
 733             prove(tm1, REWRITE_TAC[dimindex_array.(i); IN_NUMSEG] THEN ARITH_TAC)));;\r
 734 \r
 735 \r
 736 let m_taylor_upper_partial_array = Array.init (max_dim + 1)\r
 737   (fun i -> Array.init (i + 1)\r
 738      (fun j ->\r
 739         if j < 1 then TRUTH else\r
 740           let j_tm = mk_small_numeral j in\r
 741           (MY_RULE_NUM o CONV_RULE NUM_REDUCE_CONV o REWRITE_RULE[dimindex_array.(i); IN_NUMSEG] o \r
 742              INST[j_tm, `i:num`] o inst_first_type_var n_type_array.(i))\r
 743             M_TAYLOR_UPPER_PARTIAL_BOUND'));;\r
 744 \r
 745 \r
 746 let m_taylor_lower_partial_array = Array.init (max_dim + 1)\r
 747   (fun i -> Array.init (i + 1)\r
 748      (fun j ->\r
 749         if j < 1 then TRUTH else\r
 750           let j_tm = mk_small_numeral j in\r
 751           (MY_RULE_NUM o CONV_RULE NUM_REDUCE_CONV o REWRITE_RULE[dimindex_array.(i); IN_NUMSEG] o \r
 752              INST[j_tm, `i:num`] o inst_first_type_var n_type_array.(i))\r
 753             M_TAYLOR_LOWER_PARTIAL_BOUND'));;\r
 754 \r
 755 let m_taylor_interval_partial_array = Array.init (max_dim + 1)\r
 756   (fun i -> Array.init (i + 1)\r
 757      (fun j ->\r
 758         if j < 1 then TRUTH else\r
 759           let j_tm = mk_small_numeral j in\r
 760           (MY_RULE_NUM o CONV_RULE NUM_REDUCE_CONV o REWRITE_RULE[dimindex_array.(i); IN_NUMSEG] o \r
 761              INST[j_tm, `i:num`] o inst_first_type_var n_type_array.(i))\r
 762             M_TAYLOR_PARTIAL_BOUND'));;\r
 763 \r
 764 \r
 765 (* upper_partial *)\r
 766 let eval_m_taylor_upper_partial n pp i m_taylor_th =\r
 767   let f_tm, domain_tm, y_tm, w_tm, f_bounds, d_bounds_list, dd_bounds_list = \r
 768     dest_m_taylor (concl m_taylor_th) in\r
 769   let w_list = rand w_tm in\r
 770   let y_var = mk_var ("y", type_of y_tm) and\r
 771       f_var = mk_var ("f", type_of f_tm) and\r
 772       domain_var = mk_var ("domain", type_of domain_tm) in\r
 773 \r
 774   let th0 = (MY_PROVE_HYP m_taylor_th o\r
 775                INST[dd_bounds_list, dd_bounds_list_var; d_bounds_list, d_bounds_list_var; \r
 776                     w_list, w_var_list; f_bounds, f_bounds_var;\r
 777                     domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_upper_partial_array.(n).(i) in\r
 778 \r
 779   let el_dd_list_tm = (hd o hyp) th0 in\r
 780   let dd_list_th = el_conv (lhand el_dd_list_tm) in\r
 781   let dd_list_tm = (rand o concl) dd_list_th in\r
 782 \r
 783   let len_dd_list_th = eval_length dd_list_tm and\r
 784       len_dd_th = eval_length dd_bounds_list and\r
 785       len_d_th = eval_length d_bounds_list and\r
 786       len_w_th = eval_length w_list in\r
 787   let th1 = (MY_PROVE_HYP len_dd_list_th o MY_PROVE_HYP len_dd_th o MY_PROVE_HYP len_d_th o \r
 788                MY_PROVE_HYP len_w_th o MY_PROVE_HYP dd_list_th o\r
 789                INST[dd_list_tm, dd_list_var]) th0 in\r
 790 \r
 791   let el_d_list_tm = (hd o hyp) th1 in\r
 792   let d_list_th = el_conv (lhand el_d_list_tm) in\r
 793   let df_lo, df_hi = (dest_pair o rand o concl) d_list_th in\r
 794   let th2 = (MY_PROVE_HYP d_list_th o INST[df_lo, df_lo_var; df_hi, df_hi_var]) th1 in\r
 795 \r
 796   let sum2_tm = (C List.nth 1 o hyp) th2 in\r
 797   let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 (lhand sum2_tm) in\r
 798   let error_tm = (rand o concl) sum2_le_th in\r
 799 \r
 800   let ineq1_th = float_add_hi pp df_hi error_tm in\r
 801   let hi_tm = (rand o concl) ineq1_th in\r
 802     (MY_PROVE_HYP ineq1_th o MY_PROVE_HYP sum2_le_th o\r
 803        INST[error_tm, error_var; hi_tm, hi_var_real]) th2;;\r
 804 \r
 805 \r
 806 (* lower_partial *)\r
 807 let eval_m_taylor_lower_partial n pp i m_taylor_th =\r
 808   let f_tm, domain_tm, y_tm, w_tm, f_bounds, d_bounds_list, dd_bounds_list = \r
 809     dest_m_taylor (concl m_taylor_th) in\r
 810   let w_list = rand w_tm in\r
 811   let y_var = mk_var ("y", type_of y_tm) and\r
 812       f_var = mk_var ("f", type_of f_tm) and\r
 813       domain_var = mk_var ("domain", type_of domain_tm) in\r
 814 \r
 815   let th0 = (MY_PROVE_HYP m_taylor_th o\r
 816                INST[dd_bounds_list, dd_bounds_list_var; d_bounds_list, d_bounds_list_var; \r
 817                     w_list, w_var_list; f_bounds, f_bounds_var;\r
 818                     domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_lower_partial_array.(n).(i) in\r
 819 \r
 820   let el_dd_list_tm = (hd o hyp) th0 in\r
 821   let dd_list_th = el_conv (lhand el_dd_list_tm) in\r
 822   let dd_list_tm = (rand o concl) dd_list_th in\r
 823 \r
 824   let len_dd_list_th = eval_length dd_list_tm and\r
 825       len_dd_th = eval_length dd_bounds_list and\r
 826       len_d_th = eval_length d_bounds_list and\r
 827       len_w_th = eval_length w_list in\r
 828   let th1 = (MY_PROVE_HYP len_dd_list_th o MY_PROVE_HYP len_dd_th o MY_PROVE_HYP len_d_th o \r
 829                MY_PROVE_HYP len_w_th o MY_PROVE_HYP dd_list_th o\r
 830                INST[dd_list_tm, dd_list_var]) th0 in\r
 831 \r
 832   let el_d_list_tm = (hd o hyp) th1 in\r
 833   let d_list_th = el_conv (lhand el_d_list_tm) in\r
 834   let df_lo, df_hi = (dest_pair o rand o concl) d_list_th in\r
 835   let th2 = (MY_PROVE_HYP d_list_th o INST[df_lo, df_lo_var; df_hi, df_hi_var]) th1 in\r
 836 \r
 837   let sum2_tm = (C List.nth 1 o hyp) th2 in\r
 838   let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 (lhand sum2_tm) in\r
 839   let error_tm = (rand o concl) sum2_le_th in\r
 840 \r
 841   let ineq1_th = float_sub_lo pp df_lo error_tm in\r
 842   let lo_tm = (lhand o concl) ineq1_th in\r
 843     (MY_PROVE_HYP ineq1_th o MY_PROVE_HYP sum2_le_th o\r
 844        INST[error_tm, error_var; lo_tm, lo_var_real]) th2;;\r
 845 \r
 846 \r
 847 (* interval_partial *)\r
 848 let eval_m_taylor_interval_partial n pp i m_taylor_th =\r
 849   let f_tm, domain_tm, y_tm, w_tm, f_bounds, d_bounds_list, dd_bounds_list = \r
 850     dest_m_taylor (concl m_taylor_th) in\r
 851   let w_list = rand w_tm in\r
 852   let y_var = mk_var ("y", type_of y_tm) and\r
 853       f_var = mk_var ("f", type_of f_tm) and\r
 854       domain_var = mk_var ("domain", type_of domain_tm) in\r
 855 \r
 856   let th0 = (MY_PROVE_HYP m_taylor_th o\r
 857                INST[dd_bounds_list, dd_bounds_list_var; d_bounds_list, d_bounds_list_var; \r
 858                     w_list, w_var_list; f_bounds, f_bounds_var;\r
 859                     domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_interval_partial_array.(n).(i) in\r
 860 \r
 861   let el_dd_list_tm = (hd o hyp) th0 in\r
 862   let dd_list_th = el_conv (lhand el_dd_list_tm) in\r
 863   let dd_list_tm = (rand o concl) dd_list_th in\r
 864 \r
 865   let len_dd_list_th = eval_length dd_list_tm and\r
 866       len_dd_th = eval_length dd_bounds_list and\r
 867       len_d_th = eval_length d_bounds_list and\r
 868       len_w_th = eval_length w_list in\r
 869   let th1 = (MY_PROVE_HYP len_dd_list_th o MY_PROVE_HYP len_dd_th o MY_PROVE_HYP len_d_th o \r
 870                MY_PROVE_HYP len_w_th o MY_PROVE_HYP dd_list_th o\r
 871                INST[dd_list_tm, dd_list_var]) th0 in\r
 872 \r
 873   let el_d_list_tm = (hd o hyp) th1 in\r
 874   let d_list_th = el_conv (lhand el_d_list_tm) in\r
 875   let df_lo, df_hi = (dest_pair o rand o concl) d_list_th in\r
 876   let th2 = (MY_PROVE_HYP d_list_th o INST[df_lo, df_lo_var; df_hi, df_hi_var]) th1 in\r
 877 \r
 878   let sum2_tm = (C List.nth 2 o hyp) th2 in\r
 879   let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 (lhand sum2_tm) in\r
 880   let error_tm = (rand o concl) sum2_le_th in\r
 881 \r
 882   let ineq1_th = float_sub_lo pp df_lo error_tm in\r
 883   let lo_tm = (lhand o concl) ineq1_th in\r
 884   let ineq2_th = float_add_hi pp df_hi error_tm in\r
 885   let hi_tm = (rand o concl) ineq2_th in\r
 886     (MY_PROVE_HYP ineq1_th o MY_PROVE_HYP ineq2_th o MY_PROVE_HYP sum2_le_th o\r
 887        INST[error_tm, error_var; lo_tm, lo_var_real; hi_tm, hi_var_real]) th2;;\r
 888 \r
 889 \r
 890 \r
 891 end;;