formal_lp/old/formal_interval/m_verifier.hl

   1 needs "../formal_lp/formal_interval/m_taylor.hl";;
   2 needs "../formal_lp/formal_interval/m_verifier0.hl";;
   3 needs "../formal_lp/arith/informal/informal_m_verifier.hl";;
   4
   5
   6 let mk_real_vars n name = map (fun i -> mk_var (sprintf "%s%d" name i, real_ty)) (1--n);;
   7
   8
   9 (*************************************)
  10
  11 let BOUNDED_INTERVAL_ARITH_IMP_HI' = (MY_RULE o prove)
  12   (`(!x. x IN interval [domain] ==> interval_arith (f x) (lo, hi)) ==>
  13      (!x. x IN interval [domain] ==> f x <= hi)`, SIMP_TAC[interval_arith]);;
  14
  15 let BOUNDED_INTERVAL_ARITH_IMP_LO' = (MY_RULE o prove)
  16   (`(!x. x IN interval [domain] ==> interval_arith (f x) (lo, hi)) ==>
  17      (!x. x IN interval [domain] ==> lo <= f x)`, SIMP_TAC[interval_arith]);;
  18
  19
  20 let eval_interval_arith_hi n bound_th =
  21   let tm0 = (snd o dest_forall o concl) bound_th in
  22   let int_tm, concl_tm = dest_comb tm0 in
  23   let domain_tm = (rand o rator o rand o rand o rand) int_tm in
  24   let ltm, bounds_tm = dest_interval_arith concl_tm in
  25   let f_tm, (lo_tm, hi_tm) = rator ltm, dest_pair bounds_tm in
  26   let f_var = mk_var ("f", type_of f_tm) and
  27       domain_var = mk_var ("domain", type_of domain_tm) in
  28     (MY_PROVE_HYP bound_th o
  29        INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real; lo_tm, lo_var_real] o
  30        inst_first_type_var n_type_array.(n)) BOUNDED_INTERVAL_ARITH_IMP_HI';;
  31
  32
  33 let eval_interval_arith_lo n bound_th =
  34   let tm0 = (snd o dest_forall o concl) bound_th in
  35   let int_tm, concl_tm = dest_comb tm0 in
  36   let domain_tm = (rand o rator o rand o rand o rand) int_tm in
  37   let ltm, bounds_tm = dest_interval_arith concl_tm in
  38   let f_tm, (lo_tm, hi_tm) = rator ltm, dest_pair bounds_tm in
  39   let f_var = mk_var ("f", type_of f_tm) and
  40       domain_var = mk_var ("domain", type_of domain_tm) in
  41     (MY_PROVE_HYP bound_th o
  42        INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real; lo_tm, lo_var_real] o
  43        inst_first_type_var n_type_array.(n)) BOUNDED_INTERVAL_ARITH_IMP_LO';;
  44
  45
  46
  47 (*************************************)
  48 (* subdomains *)
  49
  50 let eval_subset_trans =
  51   let SUBSET_TRANS' = MY_RULE SUBSET_TRANS in
  52     fun st_th tu_th ->
  53       let ltm, t_tm = dest_comb (concl st_th) in
  54       let s_tm = rand ltm and
  55           u_tm = rand (concl tu_th) in
  56       let ty = (hd o snd o dest_type o type_of) s_tm and
  57           s_var = mk_var ("s", type_of s_tm) and
  58           t_var = mk_var ("t", type_of t_tm) and
  59           u_var = mk_var ("u", type_of u_tm) in
  60         (MY_PROVE_HYP st_th o MY_PROVE_HYP tu_th o
  61            INST[s_tm, s_var; t_tm, t_var; u_tm, u_var] o inst_first_type_var ty) SUBSET_TRANS';;
  62
  63 let eval_subset_refl =
  64   let SUBSET_REFL' = MY_RULE SUBSET_REFL in
  65     fun s_tm ->
  66       let ty = (hd o snd o dest_type o type_of) s_tm and
  67           s_var = mk_var ("s", type_of s_tm) in
  68         (INST[s_tm, s_var] o inst_first_type_var ty) SUBSET_REFL';;
  69
  70
  71
  72 let SUBSET_INTERVAL_IMP = prove(`!a b c d. (!i. i IN 1..dimindex (:N) ==> a$i <= c$i /\ d$i <= b$i) ==>
  73                                   interval [c:real^N,d] SUBSET interval [a,b]`,
  74                                 SIMP_TAC[SUBSET_INTERVAL; GSYM IN_NUMSEG]);;
  75
  76
  77 let gen_subset_interval_lemma n =
  78   let a_vars = mk_real_vars n "a" and
  79       b_vars = mk_real_vars n "b" and
  80       c_vars = mk_real_vars n "c" and
  81       d_vars = mk_real_vars n "d" in
  82
  83   let a_tm = mk_vector_list a_vars and
  84       b_tm = mk_vector_list b_vars and
  85       c_tm = mk_vector_list c_vars and
  86       d_tm = mk_vector_list d_vars in
  87
  88   let th0 = (SPEC_ALL o ISPECL [a_tm; b_tm; c_tm; d_tm]) SUBSET_INTERVAL_IMP in
  89   let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
  90   let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
  91     MY_RULE th2;;
  92
  93
  94 let subset_interval_thms_array = Array.init (max_dim + 1)
  95   (fun n -> if n < 1 then TRUTH else gen_subset_interval_lemma n);;
  96
  97
  98
  99 let m_subset_interval n a_tm b_tm c_tm d_tm =
 100   let a_vars = mk_real_vars n "a" and
 101       b_vars = mk_real_vars n "b" and
 102       c_vars = mk_real_vars n "c" and
 103       d_vars = mk_real_vars n "d" in
 104
 105   let a_s = dest_vector a_tm and
 106       b_s = dest_vector b_tm and
 107       c_s = dest_vector c_tm and
 108       d_s = dest_vector d_tm in
 109
 110   let th0 = (INST (zip a_s a_vars) o INST (zip b_s b_vars) o
 111                INST (zip c_s c_vars) o INST (zip d_s d_vars)) subset_interval_thms_array.(n) in
 112   let prove_le tm =
 113     let ltm, rtm = dest_binop le_op_real tm in
 114       EQT_ELIM (float_le ltm rtm) in
 115   let hyp_ths = map prove_le (hyp th0) in
 116     itlist (fun hyp_th th -> MY_PROVE_HYP hyp_th th) hyp_ths th0;;
 117
 118
 119 (*
 120 let pp = 5;;
 121 let n = 2;;
 122
 123 let aa = `[&1; &1]` and bb = `[&3; &2]` and
 124     cc = `[#1.5; &1]` and dd = `[&3; #1.6]`;;
 125 let a_tm = mk_vector (convert_to_float_list pp true aa) and
 126     b_tm = mk_vector (convert_to_float_list pp false bb) and
 127     c_tm = mk_vector (convert_to_float_list pp true cc) and
 128     d_tm = mk_vector (convert_to_float_list pp false dd);;
 129
 130
 131 m_subset_interval n a_tm b_tm c_tm d_tm;;
 132 (* 10: 0.704 *)
 133 test 1000 (m_subset_interval n a_tm b_tm c_tm) d_tm;;
 134 *)
 135
 136 (*************************************)
 137
 138 let M_RESTRICT_RIGHT_LEMMA = prove(`!j x z y w u y' w'. m_cell_domain (x:real^N,z) y w /\
 139                                     (!i. i IN 1..dimindex (:N) ==> ~(i = j) ==>
 140                                        u$i = x$i /\ y'$i = y$i /\ w'$i = w$i) /\
 141                                     u$j = z$j /\ y'$j = z$j /\ w'$j = &0 ==>
 142     m_cell_domain (u,z) y' w' /\ interval [u,z] SUBSET interval [x,z]`,
 143    REWRITE_TAC[m_cell_domain; SUBSET_INTERVAL; GSYM IN_NUMSEG] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
 144      CONJ_TAC THENL
 145      [
 146        GEN_TAC THEN DISCH_TAC THEN
 147          ASM_CASES_TAC `i = j:num` THENL
 148          [
 149            ASM_REWRITE_TAC[REAL_LE_REFL; REAL_SUB_REFL; real_max];
 150            ALL_TAC
 151          ] THEN
 152          REPEAT (FIRST_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[]);
 153        ALL_TAC
 154      ] THEN
 155      DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 156      ASM_CASES_TAC `i = j:num` THENL
 157      [
 158        ASM_REWRITE_TAC[REAL_LE_REFL] THEN
 159          REPEAT (FIRST_X_ASSUM (MP_TAC o SPEC `j:num`)) THEN
 160          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 161          ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
 162        ALL_TAC
 163      ] THEN
 164      REPEAT (FIRST_ASSUM (new_rewrite [] [])) THEN ASM_REWRITE_TAC[REAL_LE_REFL]);;
 165
 166
 167
 168 let M_RESTRICT_LEFT_LEMMA = prove(`!j x z y w u y' w'. m_cell_domain (x:real^N,z) y w /\
 169                                     (!i. i IN 1..dimindex (:N) ==> ~(i = j) ==>
 170                                        u$i = z$i /\ y'$i = y$i /\ w'$i = w$i) /\
 171                                     u$j = x$j /\ y'$j = x$j /\ w'$j = &0 ==>
 172     m_cell_domain (x,u) y' w' /\ interval [x,u] SUBSET interval [x,z]`,
 173    REWRITE_TAC[m_cell_domain; SUBSET_INTERVAL; GSYM IN_NUMSEG] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
 174      CONJ_TAC THENL
 175      [
 176        GEN_TAC THEN DISCH_TAC THEN
 177          ASM_CASES_TAC `i = j:num` THENL
 178          [
 179            ASM_REWRITE_TAC[REAL_LE_REFL; REAL_SUB_REFL; real_max];
 180            ALL_TAC
 181          ] THEN
 182          REPEAT (FIRST_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[]);
 183        ALL_TAC
 184      ] THEN
 185      DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 186      ASM_CASES_TAC `i = j:num` THENL
 187      [
 188        ASM_REWRITE_TAC[REAL_LE_REFL] THEN
 189          REPEAT (FIRST_X_ASSUM (MP_TAC o SPEC `j:num`)) THEN
 190          POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 191          ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
 192        ALL_TAC
 193      ] THEN
 194      REPEAT (FIRST_ASSUM (new_rewrite [] [])) THEN ASM_REWRITE_TAC[REAL_LE_REFL]);;
 195
 196
 197 let gen_restrict_lemma n j left_flag =
 198   let xs = mk_real_vars n "x" and
 199       zs = mk_real_vars n "z" and
 200       ys = mk_real_vars n "y" and
 201       ws = mk_real_vars n "w" and
 202       j_tm = mk_small_numeral j in
 203   let a, b = if left_flag then zs, xs else xs, zs in
 204   let x_tm = mk_vector_list xs and
 205       z_tm = mk_vector_list zs and
 206       y_tm = mk_vector_list ys and
 207       w_tm = mk_vector_list ws and
 208       u_tm = mk_vector_list (map (fun i -> List.nth (if i = j then b else a) (i - 1)) (1--n)) and
 209       y'_tm = mk_vector_list (map (fun i -> List.nth (if i = j then b else ys) (i - 1)) (1--n)) and
 210       w'_tm = mk_vector_list (map (fun i -> if i = j then `&0` else List.nth ws (i - 1)) (1--n)) in
 211
 212   let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; y_tm; w_tm; u_tm; y'_tm; w'_tm])
 213     (if left_flag then M_RESTRICT_LEFT_LEMMA else M_RESTRICT_RIGHT_LEMMA) in
 214   let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
 215   let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
 216     MY_RULE_FLOAT th2;;
 217
 218
 219 let left_restrict_thms_array = Array.init (max_dim + 1)
 220   (fun n -> Array.init (n + 1)
 221      (fun j -> if j < 1 then TRUTH else gen_restrict_lemma n j true));;
 222
 223
 224 let right_restrict_thms_array = Array.init (max_dim + 1)
 225   (fun n -> Array.init (n + 1)
 226      (fun j -> if j < 1 then TRUTH else gen_restrict_lemma n j false));;
 227
 228
 229
 230
 231 (******************************)
 232 (* m_cell_pass *)
 233
 234
 235
 236 let m_cell_pass = new_definition `m_cell_pass f domain <=> (!x. x IN interval [domain] ==> f x < &0)`;;
 237
 238 let dest_m_cell_pass pass_tm =
 239   let ltm, domain = dest_comb pass_tm in
 240     rand ltm, domain;;
 241
 242
 243 (*********************************)
 244
 245 let M_CELL_PASS_LEMMA = prove(`(!x. x IN interval [domain] ==> f x <= hi) /\ (hi < &0 <=> T) ==>
 246                                 m_cell_pass f domain`,
 247                               REWRITE_TAC[m_cell_pass] THEN REPEAT STRIP_TAC THEN
 248                                 MATCH_MP_TAC REAL_LET_TRANS THEN
 249                                 EXISTS_TAC `hi:real` THEN ASM_REWRITE_TAC[] THEN
 250                                 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
 251
 252 let M_CELL_PASS_LEMMA' = MY_RULE M_CELL_PASS_LEMMA;;
 253
 254 let M_CELL_PASS_INTERVAL_LEMMA' = (MY_RULE o prove)
 255   (`(!x. x IN interval [domain] ==> interval_arith (f x) (lo, hi)) /\ hi < &0 ==> m_cell_pass f domain`,
 256    REWRITE_TAC[interval_arith] THEN STRIP_TAC THEN MATCH_MP_TAC M_CELL_PASS_LEMMA THEN
 257      ASM_SIMP_TAC[]);;
 258
 259 let M_CELL_PASS_SUBSET' = (MY_RULE o prove)(`m_cell_pass f domain /\
 260                                               interval [domain2] SUBSET interval [domain] ==>
 261                                               m_cell_pass f domain2`,
 262                                             REWRITE_TAC[m_cell_pass; SUBSET] THEN REPEAT STRIP_TAC THEN
 263                                               REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);;
 264
 265 (* m_cell_pass with taylor_interval *)
 266 let m_taylor_cell_pass n pp m_taylor_th =
 267   let upper_th = eval_m_taylor_upper_bound n pp m_taylor_th in
 268   let tm0 = (snd o dest_forall o concl) upper_th in
 269   let int_tm, concl_tm = dest_comb tm0 in
 270   let domain_tm = (rand o rator o rand o rand o rand) int_tm in
 271   let ltm, hi_tm = dest_comb concl_tm in
 272   let f_tm = (rator o rand) ltm in
 273   let f_var = mk_var ("f", type_of f_tm) and
 274       domain_var = mk_var ("domain", type_of domain_tm) in
 275
 276   let hi_lt0_th = float_lt0 hi_tm in
 277     if (fst o dest_const o rand o concl) hi_lt0_th = "F" then
 278       failwith "m_taylor_cell_pass: hi < &0 <=> F"
 279     else
 280       (MY_PROVE_HYP upper_th o MY_PROVE_HYP hi_lt0_th o
 281          INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real] o
 282          inst_first_type_var n_type_array.(n)) M_CELL_PASS_LEMMA';;
 283
 284
 285 (* m_cell_pass with a raw interval *)
 286 let m_taylor_cell_pass0 n bound_th =
 287   let tm0 = (snd o dest_forall o concl) bound_th in
 288   let int_tm, concl_tm = dest_comb tm0 in
 289   let domain_tm = (rand o rator o rand o rand o rand) int_tm in
 290   let ltm, bounds_tm = dest_interval_arith concl_tm in
 291   let f_tm, (lo_tm, hi_tm) = rator ltm, dest_pair bounds_tm in
 292   let f_var = mk_var ("f", type_of f_tm) and
 293       domain_var = mk_var ("domain", type_of domain_tm) in
 294   let hi_lt0_th = try EQT_ELIM (float_lt0 hi_tm) with Failure _ -> failwith "m_taylor_cell_pass0" in
 295     (MY_PROVE_HYP bound_th o MY_PROVE_HYP hi_lt0_th o
 296        INST[f_tm, f_var; domain_tm, domain_var; hi_tm, hi_var_real; lo_tm, lo_var_real] o
 297        inst_first_type_var n_type_array.(n)) M_CELL_PASS_INTERVAL_LEMMA';;
 298
 299
 300 (**********************)
 301
 302 let M_CELL_PASS_SUBDOMAIN' = (MY_RULE o prove)(`interval [domain2] SUBSET interval [domain] /\
 303                                                  m_cell_pass f domain ==> m_cell_pass f domain2`,
 304    REWRITE_TAC[m_cell_pass; SUBSET] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[]);;
 305
 306
 307 let m_cell_pass_subdomain domain2_tm pass_th =
 308   let f_tm, domain_tm = dest_m_cell_pass (concl pass_th) in
 309   let f_var = mk_var ("f", type_of f_tm) and
 310       domain_var = mk_var ("domain", type_of domain_tm) and
 311       domain2_var = mk_var ("domain2", type_of domain2_tm) in
 312   let a, b = dest_pair domain_tm and
 313       c, d = dest_pair domain2_tm in
 314   let n = get_dim a in
 315   let sub_th = m_subset_interval n a b c d in
 316     (MY_PROVE_HYP sub_th o MY_PROVE_HYP pass_th o
 317        INST[domain_tm, domain_var; domain2_tm, domain2_var; f_tm, f_var] o
 318        inst_first_type_var n_type_array.(n)) M_CELL_PASS_SUBDOMAIN';;
 319
 320
 321
 322
 323
 324 (******************************)
 325
 326 let M_CELL_PASS_GLUE_LEMMA = prove(`!j x z v u f.
 327                                      (!i. 1 <= i /\ i <= dimindex (:N) ==> ~(i = j) ==>
 328                                         u$i = x$i /\ v$i = z$i) ==>
 329                                      v$j = u$j ==>
 330                                          m_cell_pass f (x,v) ==>
 331                                          m_cell_pass f (u,z) ==>
 332                                          m_cell_pass f (x,z:real^N)`,
 333    REWRITE_TAC[m_cell_pass; IN_INTERVAL] THEN REPEAT GEN_TAC THEN
 334      move ["eq1"; "eq_vu"; "cell1"; "cell2"; "y"; "ineq"] THEN
 335      ASM_CASES_TAC `(y:real^N)$j <= (v:real^N)$j` THENL
 336      [
 337        REMOVE_THEN "cell1" MATCH_MP_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 338          USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
 339          ASM_CASES_TAC `i = j:num` THENL
 340          [
 341            REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN SIMP_TAC[];
 342            ALL_TAC
 343          ] THEN
 344          USE_THEN "eq1" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
 345          USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[];
 346        ALL_TAC
 347      ] THEN
 348
 349      POP_ASSUM (ASSUME_TAC o MATCH_MP (REAL_ARITH `~(a <= b) ==> b <= a:real`)) THEN
 350      REMOVE_THEN "cell2" MATCH_MP_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 351      USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
 352      ASM_CASES_TAC `i = j:num` THENL
 353      [
 354        ASM_REWRITE_TAC[] THEN USE_THEN "eq_vu" (fun th -> REWRITE_TAC[SYM th]) THEN
 355          REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN SIMP_TAC[];
 356        ALL_TAC
 357      ] THEN
 358      USE_THEN "eq1" (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THEN
 359      USE_THEN "ineq" (new_rewrite [] []) THEN ASM_REWRITE_TAC[]);;
 360
 361
 362 let gen_glue_lemma n j =
 363   let mk_vars name = map (fun i -> mk_var (sprintf "%s%d" name i, real_ty)) (1--n) in
 364   let xs = mk_vars "x" and
 365       zs = mk_vars "z" and
 366       t_var = mk_var ("t", real_ty) and
 367       j_tm = mk_small_numeral j in
 368   let x_tm = mk_vector_list xs and
 369       z_tm = mk_vector_list zs and
 370       v_tm = mk_vector_list (map (fun i -> if i = j then t_var else List.nth zs (i - 1)) (1--n)) and
 371       u_tm = mk_vector_list (map (fun i -> if i = j then t_var else List.nth xs (i - 1)) (1--n)) in
 372
 373   let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; v_tm; u_tm]) M_CELL_PASS_GLUE_LEMMA in
 374   let th1 = REWRITE_RULE[dimindex_array.(n); gen_in_interval n; ARITH] th0 in
 375   let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
 376     MY_RULE th2;;
 377
 378
 379 let glue_thms_array = Array.init (max_dim + 1)
 380   (fun n -> Array.init (n + 1)
 381      (fun j -> if j < 1 then TRUTH else gen_glue_lemma n j));;
 382
 383
 384
 385 (***************************************)
 386
 387 let M_CELL_SUP = prove(`!f x z. lift o f continuous_on interval [x,z:real^N] /\ m_cell_pass f (x,z) ==>
 388                          ?a. a < &0 /\ !y. y IN interval [x,z] ==> f y <= a`,
 389    REWRITE_TAC[m_cell_pass] THEN REPEAT STRIP_TAC THEN
 390      ASM_CASES_TAC `interval [x:real^N,z] = {}` THENL
 391      [
 392        EXISTS_TAC `-- &1` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN REAL_ARITH_TAC;
 393        ALL_TAC
 394      ] THEN
 395      MP_TAC (SPECL [`f:real^N->real`; `interval [x,z:real^N]`] CONTINUOUS_ATTAINS_SUP) THEN
 396      ASM_REWRITE_TAC[COMPACT_INTERVAL] THEN
 397      DISCH_THEN (X_CHOOSE_THEN `y:real^N` STRIP_ASSUME_TAC) THEN
 398      EXISTS_TAC `(f:real^N->real) y` THEN ASM_REWRITE_TAC[] THEN
 399      FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
 400
 401
 402 let DIFF2_DOMAIN_IMP_CONTINUOUS_ON = prove(`!(f:real^N->real) domain. diff2_domain domain f ==>
 403                                              lift o f continuous_on interval [domain]`,
 404    REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
 405      MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN REPEAT STRIP_TAC THEN
 406      MATCH_MP_TAC DIFFERENTIABLE_IMP_CONTINUOUS_AT THEN
 407      MATCH_MP_TAC diff2_imp_diff THEN
 408      ASM_SIMP_TAC[]);;
 409
 410
 411
 412 let M_CELL_INCREASING_PASS_LEMMA = prove(`!j x z u domain lo f.
 413                                            interval [x,z] SUBSET interval [domain] ==>
 414                                            diff2c_domain domain f ==>
 415                                            (!i. i IN 1..dimindex (:N) ==> ~(i = j) ==> u$i = x$i) ==>
 416                                            u$j = z$j ==>
 417                                                &0 <= lo ==>
 418                                                (!y. y IN interval [domain] ==> lo <= partial j f y) ==>
 419                                                m_cell_pass f (u,z) ==>
 420                                                m_cell_pass f (x,z:real^N)`,
 421    REWRITE_TAC[SUBSET] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[m_cell_pass] THEN
 422      X_GEN_TAC `y:real^N` THEN
 423      ASM_CASES_TAC `~(!i. i IN 1..dimindex (:N) ==> (x:real^N)$i <= (z:real^N)$i)` THENL
 424      [
 425        POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; IN_INTERVAL; GSYM IN_NUMSEG] THEN
 426          DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
 427          DISCH_THEN (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
 428          POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 429        ALL_TAC
 430      ] THEN
 431      POP_ASSUM MP_TAC THEN REWRITE_TAC[negbK] THEN DISCH_TAC THEN
 432      SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL
 433      [
 434        UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN
 435          SIMP_TAC[diff2_domain; diff2c_domain; diff2c];
 436        ALL_TAC
 437      ] THEN
 438      MP_TAC (SPECL [`f:real^N->real`; `u:real^N`; `z:real^N`] M_CELL_SUP) THEN
 439      ANTS_TAC THENL
 440      [
 441        ASM_REWRITE_TAC[] THEN
 442          MATCH_MP_TAC DIFF2_DOMAIN_IMP_CONTINUOUS_ON THEN
 443          UNDISCH_TAC `diff2_domain domain (f:real^N->real)` THEN
 444          REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
 445          REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN
 446          POP_ASSUM MP_TAC THEN
 447          REWRITE_TAC[IN_INTERVAL] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 448          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
 449          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN
 450          ASM_CASES_TAC `i = j:num` THENL [ ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; ALL_TAC] THEN
 451          FIRST_X_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[IN_NUMSEG];
 452        ALL_TAC
 453      ] THEN
 454      DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN DISCH_TAC THEN
 455      MP_TAC (SPECL [`f:real^N->real`; `j:num`; `u:real^N`; `x:real^N`; `z:real^N`; `a:real`] partial_increasing_right) THEN
 456      ASM_REWRITE_TAC[] THEN
 457      ANTS_TAC THENL
 458      [
 459        REPEAT STRIP_TAC THEN
 460          MATCH_MP_TAC diff2_imp_diff THEN
 461          UNDISCH_TAC `diff2_domain domain (f:real^N->real)` THEN REWRITE_TAC[diff2_domain] THEN
 462          DISCH_THEN MATCH_MP_TAC THEN
 463          FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
 464        ALL_TAC
 465      ] THEN
 466      ANTS_TAC THENL
 467      [
 468        REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 469          EXISTS_TAC `lo:real` THEN ASM_REWRITE_TAC[] THEN
 470          REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
 471        ALL_TAC
 472      ] THEN
 473      DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
 474      EXISTS_TAC `a:real` THEN ASM_REWRITE_TAC[] THEN
 475      FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
 476
 477
 478
 479 let M_CELL_DECREASING_PASS_LEMMA = prove(`!j x z u domain hi f.
 480                                            interval [x,z] SUBSET interval [domain] ==>
 481                                            diff2c_domain domain f ==>
 482                                            (!i. i IN 1..dimindex (:N) ==> ~(i = j) ==> u$i = z$i) ==>
 483                                            u$j = x$j ==>
 484                                                hi <= &0 ==>
 485                                                (!y. y IN interval [domain] ==> partial j f y <= hi) ==>
 486                                                m_cell_pass f (x,u) ==>
 487                                                m_cell_pass f (x,z:real^N)`,
 488    REWRITE_TAC[SUBSET] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[m_cell_pass] THEN X_GEN_TAC `y:real^N` THEN
 489      ASM_CASES_TAC `~(!i. i IN 1..dimindex (:N) ==> (x:real^N)$i <= (z:real^N)$i)` THENL
 490      [
 491        POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; IN_INTERVAL; GSYM IN_NUMSEG] THEN
 492          DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
 493          DISCH_THEN (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
 494          POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 495        ALL_TAC
 496      ] THEN
 497      POP_ASSUM MP_TAC THEN REWRITE_TAC[negbK] THEN DISCH_TAC THEN
 498      SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL
 499      [
 500        UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN
 501          SIMP_TAC[diff2_domain; diff2c_domain; diff2c];
 502        ALL_TAC
 503      ] THEN
 504      MP_TAC (SPECL [`f:real^N->real`; `x:real^N`; `u:real^N`] M_CELL_SUP) THEN
 505      ANTS_TAC THENL
 506      [
 507        ASM_REWRITE_TAC[] THEN
 508          MATCH_MP_TAC DIFF2_DOMAIN_IMP_CONTINUOUS_ON THEN
 509          UNDISCH_TAC `diff2_domain domain (f:real^N->real)` THEN
 510          REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
 511          REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN
 512          POP_ASSUM MP_TAC THEN
 513          REWRITE_TAC[IN_INTERVAL] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 514          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
 515          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN
 516          ASM_CASES_TAC `i = j:num` THENL [ ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; ALL_TAC] THEN
 517          FIRST_X_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[IN_NUMSEG];
 518        ALL_TAC
 519      ] THEN
 520      DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN DISCH_TAC THEN
 521      MP_TAC (SPECL [`f:real^N->real`; `j:num`; `u:real^N`; `x:real^N`; `z:real^N`; `a:real`] partial_decreasing_left) THEN
 522      ASM_REWRITE_TAC[] THEN
 523      ANTS_TAC THENL
 524      [
 525        REPEAT STRIP_TAC THEN
 526          MATCH_MP_TAC diff2_imp_diff THEN
 527          UNDISCH_TAC `diff2_domain domain (f:real^N->real)` THEN REWRITE_TAC[diff2_domain] THEN
 528          DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
 529          FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
 530        ALL_TAC
 531      ] THEN
 532      ANTS_TAC THENL
 533      [
 534        REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 535          EXISTS_TAC `hi:real` THEN ASM_REWRITE_TAC[] THEN
 536          REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
 537        ALL_TAC
 538      ] THEN
 539      DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
 540      EXISTS_TAC `a:real` THEN ASM_REWRITE_TAC[] THEN
 541      FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
 542
 543
 544
 545 let M_CELL_CONVEX_PASS_LEMMA = prove(`!j x z u v lo f.
 546                 diff2c_domain (x,z) f ==>
 547                 (!i. i IN 1..dimindex (:N) ==> ~(i = j) ==> u$i = z$i /\ v$i = x$i) ==>
 548                 u$j = x$j ==> v$j = z$j ==>
 549                     &0 <= lo ==>
 550                     (!y. y IN interval [x,z] ==> lo <= partial2 j j f y) ==>
 551                     m_cell_pass f (x,u) ==>
 552                     m_cell_pass f (v,z) ==>
 553                     m_cell_pass f (x:real^N,z)`,
 554    REPEAT STRIP_TAC THEN REWRITE_TAC[m_cell_pass] THEN
 555      X_GEN_TAC `y:real^N` THEN DISCH_TAC THEN
 556      SUBGOAL_THEN `!i. i IN 1..dimindex (:N) ==> (x:real^N)$i <= (z:real^N)$i` ASSUME_TAC THENL
 557      [
 558        POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_INTERVAL] THEN REPEAT STRIP_TAC THEN
 559          MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(y:real^N)$i` THEN
 560          FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[GSYM IN_NUMSEG];
 561        ALL_TAC
 562      ] THEN
 563      SUBGOAL_THEN `diff2_domain (x,z) (f:real^N->real)` ASSUME_TAC THENL
 564      [
 565        UNDISCH_TAC `diff2c_domain (x,z) (f:real^N->real)` THEN
 566          SIMP_TAC[diff2_domain; diff2c_domain; diff2c];
 567        ALL_TAC
 568      ] THEN
 569      MP_TAC (SPECL [`f:real^N->real`; `v:real^N`; `z:real^N`] M_CELL_SUP) THEN
 570      ANTS_TAC THENL
 571      [
 572        ASM_REWRITE_TAC[] THEN
 573          MATCH_MP_TAC DIFF2_DOMAIN_IMP_CONTINUOUS_ON THEN
 574          UNDISCH_TAC `diff2_domain (x,z) (f:real^N->real)` THEN
 575          REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
 576          FIRST_X_ASSUM MATCH_MP_TAC THEN
 577          POP_ASSUM MP_TAC THEN
 578          REWRITE_TAC[IN_INTERVAL] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 579          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
 580          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN
 581          ASM_CASES_TAC `i = j:num` THENL [ ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; ALL_TAC] THEN
 582          FIRST_X_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[IN_NUMSEG];
 583        ALL_TAC
 584      ] THEN
 585      DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
 586
 587      MP_TAC (SPECL [`f:real^N->real`; `x:real^N`; `u:real^N`] M_CELL_SUP) THEN
 588      ANTS_TAC THENL
 589      [
 590        ASM_REWRITE_TAC[] THEN
 591          MATCH_MP_TAC DIFF2_DOMAIN_IMP_CONTINUOUS_ON THEN
 592          UNDISCH_TAC `diff2_domain (x,z) (f:real^N->real)` THEN
 593          REWRITE_TAC[diff2_domain] THEN REPEAT STRIP_TAC THEN
 594          FIRST_X_ASSUM MATCH_MP_TAC THEN
 595          POP_ASSUM MP_TAC THEN
 596          REWRITE_TAC[IN_INTERVAL] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
 597          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
 598          FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN
 599          ASM_CASES_TAC `i = j:num` THENL [ ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; ALL_TAC] THEN
 600          FIRST_X_ASSUM (new_rewrite [] []) THEN ASM_REWRITE_TAC[IN_NUMSEG];
 601        ALL_TAC
 602      ] THEN
 603      DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) THEN
 604
 605      MP_TAC (SPECL [`f:real^N->real`; `j:num`; `x:real^N`; `z:real^N`; `u:real^N`; `v:real^N`; `max a a'`] partial_convex_max) THEN
 606      ASM_REWRITE_TAC[] THEN
 607      ANTS_TAC THENL
 608      [
 609        REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 610          EXISTS_TAC `lo:real` THEN ASM_REWRITE_TAC[] THEN
 611          REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
 612        ALL_TAC
 613      ] THEN
 614      ANTS_TAC THENL
 615      [
 616        REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 617          EXISTS_TAC `a':real` THEN
 618          ASM_SIMP_TAC[] THEN REAL_ARITH_TAC;
 619        ALL_TAC
 620      ] THEN
 621      ANTS_TAC THENL
 622      [
 623        REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 624          EXISTS_TAC `a:real` THEN
 625          ASM_SIMP_TAC[] THEN REAL_ARITH_TAC;
 626        ALL_TAC
 627      ] THEN
 628
 629      DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
 630      EXISTS_TAC `max a a'` THEN
 631      ASM_SIMP_TAC[] THEN
 632      ASM_REAL_ARITH_TAC);;
 633
 634
 635
 636 (*********************)
 637
 638 let ZERO_EQ_ZERO_CONST = prove(`0 = _0`, REWRITE_TAC[NUMERAL]);;
 639
 640 let gen_increasing_lemma n j =
 641   let mk_vars name = map (fun i -> mk_var (sprintf "%s%d" name i, real_ty)) (1--n) in
 642   let xs = mk_vars "x" and
 643       zs = mk_vars "z" and
 644       j_tm = mk_small_numeral j in
 645   let x_tm = mk_vector_list xs and
 646       z_tm = mk_vector_list zs and
 647       u_tm = mk_vector_list (map (fun i -> List.nth (if i = j then zs else xs) (i - 1)) (1--n)) in
 648   let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; u_tm]) M_CELL_INCREASING_PASS_LEMMA in
 649   let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
 650   let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
 651   let th3 = MY_RULE_NUM th2 in
 652     (UNDISCH_ALL o ONCE_REWRITE_RULE[GSYM ZERO_EQ_ZERO_CONST] o DISCH (last (hyp th3))) th3;;
 653
 654
 655 let gen_mono_lemma0 th =
 656   let h2 = List.nth (hyp th) 1 in
 657   let domain_tm = (lhand o rand o lhand) h2 in
 658   let domain_var = mk_var ("domain", type_of domain_tm) in
 659     (UNDISCH_ALL o REWRITE_RULE[SUBSET_REFL] o DISCH_ALL o INST[domain_tm, domain_var]) th;;
 660
 661 let incr_gen_thms_array = Array.init (max_dim + 1)
 662   (fun n -> Array.init (n + 1)
 663      (fun j -> if j < 1 then TRUTH else gen_increasing_lemma n j));;
 664
 665 let incr_thms_array = Array.init (max_dim + 1)
 666   (fun n -> Array.init (n + 1)
 667      (fun j -> if j < 1 then TRUTH else gen_mono_lemma0 incr_gen_thms_array.(n).(j)));;
 668
 669
 670
 671 let gen_decreasing_lemma n j =
 672   let mk_vars name = map (fun i -> mk_var (sprintf "%s%d" name i, real_ty)) (1--n) in
 673   let xs = mk_vars "x" and
 674       zs = mk_vars "z" and
 675       j_tm = mk_small_numeral j in
 676   let x_tm = mk_vector_list xs and
 677       z_tm = mk_vector_list zs and
 678       u_tm = mk_vector_list (map (fun i -> List.nth (if i = j then xs else zs) (i - 1)) (1--n)) in
 679   let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; u_tm]) M_CELL_DECREASING_PASS_LEMMA in
 680   let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
 681   let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
 682   let th3 = MY_RULE_NUM th2 in
 683     (UNDISCH_ALL o ONCE_REWRITE_RULE[GSYM ZERO_EQ_ZERO_CONST] o DISCH (last (hyp th3))) th3;;
 684
 685
 686 let decr_gen_thms_array = Array.init (max_dim + 1)
 687   (fun n -> Array.init (n + 1)
 688      (fun j -> if j < 1 then TRUTH else gen_decreasing_lemma n j));;
 689
 690 let decr_thms_array = Array.init (max_dim + 1)
 691   (fun n -> Array.init (n + 1)
 692      (fun j -> if j < 1 then TRUTH else gen_mono_lemma0 decr_gen_thms_array.(n).(j)));;
 693
 694
 695 (****************************************)
 696
 697 let gen_convex_max_lemma n j =
 698   let xs = mk_real_vars n "x" and
 699       zs = mk_real_vars n "z" and
 700       j_tm = mk_small_numeral j in
 701   let x_tm = mk_vector_list xs and
 702       z_tm = mk_vector_list zs and
 703       u_tm = mk_vector_list (map (fun i -> List.nth (if i = j then xs else zs) (i - 1)) (1--n)) and
 704       v_tm = mk_vector_list (map (fun i -> List.nth (if i = j then zs else xs) (i - 1)) (1--n)) in
 705   let th0 = (SPEC_ALL o ISPECL [j_tm; x_tm; z_tm; u_tm; v_tm]) M_CELL_CONVEX_PASS_LEMMA in
 706   let th1 = REWRITE_RULE[dimindex_array.(n); IN_NUMSEG; gen_in_interval n; ARITH] th0 in
 707   let th2 = REWRITE_RULE (Array.to_list comp_thms_array.(n)) th1 in
 708   let th3 = MY_RULE_NUM th2 in
 709     (UNDISCH_ALL o ONCE_REWRITE_RULE[GSYM ZERO_EQ_ZERO_CONST] o DISCH (last (hyp th3))) th3;;
 710
 711
 712 let convex_thms_array = Array.init (max_dim + 1)
 713   (fun n -> Array.init (n + 1)
 714      (fun j -> if j < 1 then TRUTH else gen_convex_max_lemma n j));;
 715
 716
 717
 718 (******************************************)
 719
 720 let m_glue_cells n j pass_th1 pass_th2 =
 721   let f_tm, domain1 = dest_m_cell_pass (concl pass_th1) and
 722       domain2 = rand (concl pass_th2) in
 723   let x1, z1 = dest_pair domain1 and
 724       x2, z2 = dest_pair domain2 in
 725
 726   let x1s = dest_vector x1 and
 727       x2s = dest_vector x2 and
 728       z2s = dest_vector z2 in
 729
 730   let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
 731       z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
 732       f_var = mk_var ("f", type_of f_tm) and
 733       t_tm = List.nth x2s (j - 1) in
 734
 735   let th0 = (INST[t_tm, t_var_real; f_tm, f_var] o
 736                INST (zip z2s z_vars) o INST (zip x1s x_vars)) glue_thms_array.(n).(j) in
 737     (MY_PROVE_HYP pass_th1 o MY_PROVE_HYP pass_th2) th0;;
 738
 739
 740 (**********************)
 741
 742 let m_mono_pass_gen n j decr_flag diff2_th partial_mono_th sub_th pass_th =
 743   let f_tm, domain0 = dest_m_cell_pass (concl pass_th) and
 744       domain = (rand o rator o concl) diff2_th and
 745       xv, zv = (dest_pair o lhand o rand o lhand o concl) sub_th and
 746       bound_tm = ((if decr_flag then rand else lhand) o rand o snd o dest_forall o concl) partial_mono_th in
 747
 748   let xs = dest_vector xv and
 749       zs = dest_vector zv in
 750
 751   let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
 752       z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
 753       domain_var = mk_var ("domain", type_of domain) and
 754       f_var = mk_var ("f", type_of f_tm) and
 755       bound_var = mk_var ((if decr_flag then "hi" else "lo"), real_ty) in
 756
 757   let le_th0 = (if decr_flag then float_le0 else float_ge0) bound_tm in
 758   let le_th = try EQT_ELIM le_th0 with Failure _ ->
 759     failwith (sprintf "m_mono_pass_gen: j = %d, th = %s" j (string_of_thm le_th0)) in
 760
 761   let th0 = (INST[f_tm, f_var; bound_tm, bound_var; domain, domain_var] o
 762           INST (zip xs x_vars) o INST (zip zs z_vars))
 763     (if decr_flag then decr_gen_thms_array.(n).(j) else incr_gen_thms_array.(n).(j)) in
 764     (MY_PROVE_HYP le_th o MY_PROVE_HYP pass_th o MY_PROVE_HYP diff2_th o
 765        MY_PROVE_HYP sub_th o MY_PROVE_HYP partial_mono_th) th0;;
 766
 767
 768
 769 (* m_incr_pass *)
 770 let m_incr_pass n pp j m_taylor_th pass_th0 =
 771   let _, diff2_th, _, _ = dest_m_taylor_thms n m_taylor_th in
 772   let partial_bound = eval_m_taylor_partial_lower n pp j m_taylor_th in
 773
 774   let f_tm, domain0 = dest_m_cell_pass (concl pass_th0) and
 775       domain = (rand o rator o concl) diff2_th and
 776       lo_tm = (lhand o rand o snd o dest_forall o concl) partial_bound in
 777   let lo_ge0_th = EQT_ELIM (float_ge0 lo_tm) in
 778
 779   let x_tm, z_tm = dest_pair domain in
 780   let xs = dest_vector x_tm and
 781       zs = dest_vector z_tm in
 782
 783   let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
 784       z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
 785       f_var = mk_var ("f", type_of f_tm) in
 786   let th0 = (INST[f_tm, f_var; lo_tm, lo_var_real] o
 787                INST (zip zs z_vars) o INST (zip xs x_vars)) incr_thms_array.(n).(j) in
 788     (MY_PROVE_HYP lo_ge0_th o MY_PROVE_HYP pass_th0 o
 789        MY_PROVE_HYP diff2_th o MY_PROVE_HYP partial_bound) th0;;
 790
 791
 792 (* m_decr_pass *)
 793 let m_decr_pass n pp j m_taylor_th pass_th0 =
 794   let _, diff2_th, _, _ = dest_m_taylor_thms n m_taylor_th in
 795   let partial_bound = eval_m_taylor_partial_upper n pp j m_taylor_th in
 796
 797   let f_tm, domain0 = dest_m_cell_pass (concl pass_th0) and
 798       domain = (rand o rator o concl) diff2_th and
 799       hi_tm = (rand o rand o snd o dest_forall o concl) partial_bound in
 800   let hi_le0_th = EQT_ELIM (float_le0 hi_tm) in
 801
 802   let x_tm, z_tm = dest_pair domain in
 803   let xs = dest_vector x_tm and
 804       zs = dest_vector z_tm in
 805
 806   let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
 807       z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
 808       f_var = mk_var ("f", type_of f_tm) in
 809   let th0 = (INST[f_tm, f_var; hi_tm, hi_var_real] o
 810                INST (zip zs z_vars) o INST (zip xs x_vars)) decr_thms_array.(n).(j) in
 811     (MY_PROVE_HYP hi_le0_th o MY_PROVE_HYP pass_th0 o
 812        MY_PROVE_HYP diff2_th o MY_PROVE_HYP partial_bound) th0;;
 813
 814 (*************************)
 815
 816 (* m_convex_pass *)
 817 let m_convex_pass n j diff2_th partial2_bound_th pass1_th pass2_th =
 818   let f_tm, domain1 = dest_m_cell_pass (concl pass1_th) and
 819       _, domain2 = dest_m_cell_pass (concl pass2_th) in
 820   let x_tm, _ = dest_pair domain1 and
 821       _, z_tm = dest_pair domain2 and
 822       bound_tm = (lhand o rand o snd o dest_forall o concl) partial2_bound_th in
 823
 824   let xs = dest_vector x_tm and
 825       zs = dest_vector z_tm in
 826
 827   let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
 828       z_vars = map (fun i -> z_vars_array.(i)) (1--n) and
 829       f_var = mk_var ("f", type_of f_tm) in
 830
 831   let le_th0 = float_ge0 bound_tm in
 832   let le_th =
 833     try EQT_ELIM le_th0 with Failure _ -> failwith ("m_convex_pass: "^string_of_thm le_th0) in
 834
 835   let th0 = (INST[f_tm, f_var; bound_tm, lo_var_real] o
 836                INST (zip xs x_vars) o INST (zip zs z_vars)) convex_thms_array.(n).(j) in
 837     (MY_PROVE_HYP le_th o MY_PROVE_HYP pass1_th o MY_PROVE_HYP pass2_th o
 838        MY_PROVE_HYP diff2_th o MY_PROVE_HYP partial2_bound_th) th0;;
 839
 840
 841
 842
 843 (***********************)
 844
 845 (* mk_verification_functions *)
 846
 847 type verification_funs =
 848 {
 849   (* p_lin -> p_second -> domain_th -> taylor_th *)
 850   taylor : int -> int -> thm -> thm;
 851   (* pp -> lo -> hi -> interval_th *)
 852   f : int -> term -> term -> thm;
 853   (* i -> pp -> lo -> hi -> interval_th *)
 854   df : int -> int -> term -> term -> thm;
 855   (* i -> j -> pp -> lo -> hi -> interval_th *)
 856   ddf : int -> int -> int -> term -> term -> thm;
 857   (* lo -> hi -> diff2_th *)
 858   diff2_f : term -> term -> thm;
 859 };;
 860
 861
 862 let mk_verification_functions pp0 poly_tm min_flag value_tm =
 863   let x_tm, body_tm = dest_abs poly_tm in
 864   let new_expr =
 865     uncurry (mk_binop sub_op_real) (if min_flag then value_tm, body_tm else body_tm, value_tm) in
 866   let new_f = mk_abs (x_tm, new_expr) in
 867   let n = get_dim x_tm in
 868
 869   let partials = map (fun i ->
 870                         let _ = report (sprintf "Partial %d/%d" i n) in
 871                           gen_partial_poly i new_f) (1--n) in
 872   let get_partial i eq_th =
 873     let partial_i = gen_partial_poly i (rand (concl eq_th)) in
 874     let pi = (rator o lhand o concl) partial_i in
 875       REWRITE_RULE[GSYM partial2] (TRANS (AP_TERM pi eq_th) partial_i) in
 876   let partials2 = map (fun j ->
 877                          let th = List.nth partials (j - 1) in
 878                          let _ = report (sprintf "Partial2 %d/%d" j n) in
 879                            map (fun i -> get_partial i th) (1--j)) (1--n) in
 880
 881   let diff_th = gen_diff_poly new_f in
 882   let lin_th = gen_lin_approx_poly_thm new_f diff_th partials in
 883   let diff2_th = gen_diff2c_domain_poly new_f in
 884   let second_th = gen_second_bounded_poly_thm new_f partials2 in
 885
 886   let replace_numeral i th =
 887     let num_eq = (REWRITE_RULE[Arith_hash.NUM_THM] o NUMERAL_TO_NUM_CONV) (mk_small_numeral i) in
 888       GEN_REWRITE_RULE (LAND_CONV o RATOR_CONV o DEPTH_CONV) [num_eq] th in
 889
 890   let eval0 = mk_eval_function pp0 new_f in
 891   let eval1 = map (fun i ->
 892                      let d_th = List.nth partials (i - 1) in
 893                      let eq_th = replace_numeral i d_th in
 894                        mk_eval_function_eq pp0 eq_th) (1--n) in
 895
 896   let eval2 = map (fun i ->
 897                      map (fun j ->
 898                             let d2_th = List.nth (List.nth partials2 (i - 1)) (j - 1) in
 899                             let eq_th' = replace_numeral i d2_th in
 900                             let eq_th = replace_numeral j eq_th' in
 901                               mk_eval_function_eq pp0 eq_th) (1--i)) (1--n) in
 902
 903   let diff2_f = eval_diff2_poly diff2_th in
 904   let eval_f = eval_m_taylor pp0 diff2_th lin_th second_th in
 905   let taylor_f = build_taylor pp0 lin_th second_th in
 906     {taylor = eval_f;
 907      f = eval0;
 908      df = (fun i -> List.nth eval1 (i - 1));
 909      ddf = (fun i j -> List.nth (List.nth eval2 (j - 1)) (i - 1));
 910      diff2_f = diff2_f;
 911     }, taylor_f, Informal_verifier.mk_verification_functions pp0 new_f partials partials2;;
 912
 913
 914 (* split_domain *)
 915
 916 let split_domain n pp j domain_th =
 917   let domain_tm, y_tm, _ = dest_m_cell_domain (concl domain_th) in
 918   let x_tm, z_tm = dest_pair domain_tm in
 919   let xs = dest_vector x_tm and
 920       zs = dest_vector z_tm and
 921       t = List.nth (dest_vector y_tm) (j - 1) in
 922
 923   let vv = map (fun i -> if i = j then t else List.nth zs (i - 1)) (1--n) and
 924       uu = map (fun i -> if i = j then t else List.nth xs (i - 1)) (1--n) in
 925
 926   let domain1_th = mk_m_center_domain n pp (rand x_tm) (mk_list (vv, real_ty)) and
 927       domain2_th = mk_m_center_domain n pp (mk_list (uu, real_ty)) (rand z_tm) in
 928     domain1_th, domain2_th;;
 929
 930
 931 (* restrict_domain *)
 932
 933 let restrict_domain n j left_flag domain_th =
 934   let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
 935   let x_tm, z_tm = dest_pair domain_tm in
 936   let xs = dest_vector x_tm and
 937       zs = dest_vector z_tm and
 938       ys = dest_vector y_tm and
 939       ws = dest_vector w_tm in
 940
 941   let th0 = (INST (zip xs (mk_real_vars n "x")) o INST (zip zs (mk_real_vars n "z")) o
 942                INST (zip ys (mk_real_vars n "y")) o INST (zip ws (mk_real_vars n "w")))
 943     (if left_flag then left_restrict_thms_array.(n).(j) else right_restrict_thms_array.(n).(j)) in
 944   let ths = CONJUNCTS (MY_PROVE_HYP domain_th th0) in
 945     hd ths, hd (tl ths);;
 946
 947
 948 let convert_to_float_list pp lo_flag list_tm =
 949   let tms = dest_list list_tm in
 950   let i_funs = map build_interval_fun tms in
 951   let ints = map (fun f -> eval_interval_fun pp f [] []) i_funs in
 952   let extract = (if lo_flag then fst else snd) o dest_pair o rand o concl in
 953     mk_list (map extract ints, real_ty);;
 954
 955
 956
 957
 958
 959 (****************************************)
 960
 961 (* time test for domain computations *)
 962 let m_verify_domain_test n pp certificate xx zz =
 963   let r_size = result_size certificate in
 964   let k = ref 0 in
 965   let domain_th = mk_m_center_domain n pp xx zz in
 966
 967   let rec rec_verify domain_th certificate =
 968     match certificate with
 969       | Result_mono (mono, r1) ->
 970           let m = hd mono in
 971           let _ = report (sprintf "Mono: %d (%b)" m.variable m.decr_flag) in
 972           let j, left_flag = m.variable, m.decr_flag in
 973           let domain1_th, _ = restrict_domain n j left_flag domain_th in
 974           let r = if tl mono = [] then r1 else Result_mono (tl mono, r1) in
 975             rec_verify domain1_th r
 976
 977       | Result_pass (f0_flag, xx, zz) ->
 978           let _ = k := !k + 1 in
 979           let _ = report (sprintf "Verifying: %d/%d" !k r_size) in ()
 980
 981       | Result_glue (i, convex_flag, r1, r2) ->
 982           let domain1_th, domain2_th =
 983             if convex_flag then
 984               let d1, _ = restrict_domain n (i + 1) true domain_th and
 985                   d2, _ = restrict_domain n (i + 1) false domain_th in
 986                 d1, d2
 987             else
 988               split_domain n pp (i + 1) domain_th in
 989           let _ = rec_verify domain1_th r1 and
 990               _ = rec_verify domain2_th r2 in ()
 991
 992       | _ -> failwith "False result" in
 993
 994     rec_verify domain_th certificate;;
 995
 996
 997
 998
 999
1000 (***************************)
1001
1002 let m_verify_raw n pp fs certificate domain_th0 th_list =
1003   let r_size = result_size certificate in
1004   let k = ref 0 in
1005
1006   let rec rec_verify =
1007     let rec apply_trans sub_ths th0 acc =
1008       match sub_ths with
1009         | [] -> rev acc
1010         | th :: ths ->
1011             let th' = eval_subset_trans th th0 in
1012               apply_trans ths th' (th' :: acc) in
1013
1014     let rec mk_domains mono th0 acc =
1015       match mono with
1016         | [] -> rev acc
1017         | m :: ms ->
1018             let j, flag = m.variable, m.decr_flag in
1019             let ths = restrict_domain n j flag th0 in
1020               mk_domains ms (fst ths) (ths :: acc) in
1021
1022     let verify_mono mono domain_th certificate =
1023       let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1024       let xx, zz = dest_pair domain in
1025       let df0_flags = itlist (fun m b -> m.df0_flag & b) mono true in
1026       let _ = report (sprintf "df0_flags = %b" df0_flags) in
1027       let taylor_th, diff2_th =
1028         if df0_flags then
1029           TRUTH, fs.diff2_f xx zz
1030         else
1031           let t_th = fs.taylor pp pp domain_th in
1032           let _, d_th, _, _ = dest_m_taylor_thms n t_th in
1033             t_th, d_th in
1034
1035       let domain_ths = mk_domains mono domain_th [] in
1036 (*      let domains = domain_th :: map fst (butlast domain_ths) in *)
1037
1038 (*      let gen_mono (m, domain_th) = *)
1039       let gen_mono m =
1040         if m.df0_flag then
1041           if m.decr_flag then
1042             eval_interval_arith_hi n (fs.df m.variable pp xx zz)
1043           else
1044             eval_interval_arith_lo n (fs.df m.variable pp xx zz)
1045         else
1046           if m.decr_flag then
1047             eval_m_taylor_partial_upper n pp m.variable taylor_th
1048           else
1049             eval_m_taylor_partial_lower n pp m.variable taylor_th in
1050
1051 (*      let mono_ths = map gen_mono (zip mono domains) in *)
1052       let mono_ths = map gen_mono mono in
1053       let pass_th0 = rec_verify ((fst o last) domain_ths) certificate in
1054       let sub_th0 = (eval_subset_refl o rand o concl o snd o hd) domain_ths in
1055       let sub_ths = apply_trans (sub_th0 :: map snd (butlast domain_ths)) sub_th0 [] in
1056       let th = rev_itlist (fun ((m, mono_th), sub_th) pass_th ->
1057                              let j, flag = m.variable, m.decr_flag in
1058                                m_mono_pass_gen n j flag diff2_th mono_th sub_th pass_th)
1059         (rev (zip (zip mono mono_ths) sub_ths)) pass_th0 in
1060         if hyp th <> [] then failwith ("hyp <> []: "^string_of_thm th) else th in
1061
1062
1063
1064       fun domain_th certificate ->
1065         match certificate with
1066           | Result_mono (mono, r1) ->
1067               let mono_strs =
1068                 map (fun m -> sprintf "%s%d (%b)" (if m.decr_flag then "-" else "")
1069                        m.variable m.df0_flag) mono in
1070               let _ = report (sprintf "Mono: [%s]" (String.concat ";" mono_strs)) in
1071                 verify_mono mono domain_th r1
1072
1073           | Result_pass (f0_flag, xx, zz) ->
1074               let _ = k := !k + 1 in
1075               let _ = report (sprintf "Verifying: %d/%d (f0_flag = %b)" !k r_size f0_flag) in
1076                 if f0_flag then
1077                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1078                   let xx, zz = dest_pair domain in
1079                     m_taylor_cell_pass0 n (fs.f pp xx zz)
1080                 else
1081                   let taylor_th = fs.taylor pp pp domain_th in
1082                     m_taylor_cell_pass n pp taylor_th
1083
1084           | Result_glue (i, convex_flag, r1, r2) ->
1085               let domain1_th, domain2_th =
1086                 if convex_flag then
1087                   let d1, _ = restrict_domain n (i + 1) true domain_th in
1088                   let d2, _ = restrict_domain n (i + 1) false domain_th in
1089                     d1, d2
1090                 else
1091                   split_domain n pp (i + 1) domain_th in
1092               let th1 = rec_verify domain1_th r1 in
1093               let th2 = rec_verify domain2_th r2 in
1094                 if convex_flag then
1095                   let _ = report (sprintf "GlueConvex: %d" (i + 1)) in
1096                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1097                   let xx, zz = dest_pair domain in
1098                   let diff2_th = fs.diff2_f xx zz in
1099                   let partial2_th = fs.ddf (i + 1) (i + 1) pp xx zz in
1100                   let lo_partial2_th = eval_interval_arith_lo n partial2_th in
1101                     m_convex_pass n (i + 1) diff2_th lo_partial2_th th1 th2
1102                 else
1103                   m_glue_cells n (i + 1) th1 th2
1104
1105           | Result_pass_ref i ->
1106               let _ = report (sprintf "Ref: %d" i) in
1107                 if i > 0 then
1108                   List.nth th_list (i - 1)
1109                 else
1110                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1111                   let pass_th = List.nth th_list (-i - 1) in
1112                     m_cell_pass_subdomain domain pass_th
1113
1114           | _ -> failwith "False result" in
1115
1116     rec_verify domain_th0 certificate;;
1117
1118
1119 (*****************)
1120
1121
1122 let m_verify_raw0 n pp fs certificate xx zz =
1123   m_verify_raw n pp fs certificate (mk_m_center_domain n pp xx zz) [];;
1124
1125
1126
1127 let m_verify_list n pp fs certificate_list xx zz =
1128   let domain_hash = Hashtbl.create (length certificate_list * 10) in
1129   let mem, find, add = Hashtbl.mem domain_hash,
1130     Hashtbl.find domain_hash, Hashtbl.add domain_hash in
1131
1132   let get_m_cell_domain n pp domain0 path =
1133     let rec get_rec domain_th path hash =
1134       match path with
1135         | [] -> domain_th
1136         | (s, j) :: ps ->
1137             let hash' = hash^s^(string_of_int j) in
1138               if mem hash' then
1139                 get_rec (find hash') ps hash'
1140               else
1141                 if s = "l" or s = "r" then
1142                   let domain1_th, domain2_th = split_domain n pp j domain_th in
1143                   let hash1 = hash^"l"^(string_of_int j) and
1144                       hash2 = hash^"r"^(string_of_int j) in
1145                   let _ = add hash1 domain1_th; add hash2 domain2_th in
1146                     if s = "l" then
1147                       get_rec domain1_th ps hash'
1148                     else
1149                       get_rec domain2_th ps hash'
1150                 else
1151                   let l_flag = (s = "ml") in
1152                   let domain_th', _ = restrict_domain n j l_flag domain_th in
1153                   let _ = add hash' domain_th' in
1154                     get_rec domain_th' ps hash' in
1155       get_rec domain0 path "" in
1156
1157   let domain_th0 = mk_m_center_domain n pp xx zz in
1158   let size = length certificate_list in
1159   let k = ref 0 in
1160   let rec rec_verify certificate_list th_list =
1161     match certificate_list with
1162       | [] -> last th_list
1163       | (path, certificate) :: cs ->
1164           let _ = k := !k + 1; report (sprintf "List: %d/%d" !k size) in
1165           let domain_th = get_m_cell_domain n pp domain_th0 path in
1166           let th = m_verify_raw n pp fs certificate domain_th th_list in
1167             rec_verify cs (th_list @ [th]) in
1168     rec_verify certificate_list [];;
1169
1170
1171 (***************************)
1172 (* Verification based on a p_result_tree *)
1173
1174 let m_p_verify_raw n p_split fs certificate domain_th0 th_list =
1175   let r_size = p_result_size certificate in
1176   let k = ref 0 in
1177
1178   let rec rec_verify =
1179     let rec apply_trans sub_ths th0 acc =
1180       match sub_ths with
1181         | [] -> rev acc
1182         | th :: ths ->
1183             let th' = eval_subset_trans th th0 in
1184               apply_trans ths th' (th' :: acc) in
1185
1186     let rec mk_domains mono th0 acc =
1187       match mono with
1188         | [] -> rev acc
1189         | m :: ms ->
1190             let j, flag = m.variable, m.decr_flag in
1191             let ths = restrict_domain n j flag th0 in
1192               mk_domains ms (fst ths) (ths :: acc) in
1193
1194     let verify_mono p_stat mono domain_th certificate =
1195       let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1196       let xx, zz = dest_pair domain in
1197       let df0_flags = itlist (fun m b -> m.df0_flag & b) mono true in
1198       let _ = report (sprintf "df0_flags = %b" df0_flags) in
1199       let taylor_th, diff2_th =
1200         if df0_flags then
1201           TRUTH, fs.diff2_f xx zz
1202         else
1203           let t_th = fs.taylor p_stat.pp p_stat.pp domain_th in
1204           let _, d_th, _, _ = dest_m_taylor_thms n t_th in
1205             t_th, d_th in
1206
1207       let domain_ths = mk_domains mono domain_th [] in
1208       let gen_mono m =
1209         if m.df0_flag then
1210           if m.decr_flag then
1211             eval_interval_arith_hi n (fs.df m.variable p_stat.pp xx zz)
1212           else
1213             eval_interval_arith_lo n (fs.df m.variable p_stat.pp xx zz)
1214         else
1215           if m.decr_flag then
1216             eval_m_taylor_partial_upper n p_stat.pp m.variable taylor_th
1217           else
1218             eval_m_taylor_partial_lower n p_stat.pp m.variable taylor_th in
1219       let mono_ths = map gen_mono mono in
1220       let pass_th0 = rec_verify ((fst o last) domain_ths) certificate in
1221       let sub_th0 = (eval_subset_refl o rand o concl o snd o hd) domain_ths in
1222       let sub_ths = apply_trans (sub_th0 :: map snd (butlast domain_ths)) sub_th0 [] in
1223       let th = rev_itlist (fun ((m, mono_th), sub_th) pass_th ->
1224                              let j, flag = m.variable, m.decr_flag in
1225                                m_mono_pass_gen n j flag diff2_th mono_th sub_th pass_th)
1226         (rev (zip (zip mono mono_ths) sub_ths)) pass_th0 in
1227         if hyp th <> [] then failwith ("hyp <> []: "^string_of_thm th) else th in
1228
1229
1230
1231       fun domain_th certificate ->
1232         match certificate with
1233           | P_result_mono (p_stat, mono, r1) ->
1234               let mono_strs =
1235                 map (fun m -> sprintf "%s%d (%b)" (if m.decr_flag then "-" else "")
1236                        m.variable m.df0_flag) mono in
1237               let _ = report (sprintf "Mono: [%s]" (String.concat ";" mono_strs)) in
1238                 verify_mono p_stat mono domain_th r1
1239
1240           | P_result_pass (p_stat, f0_flag) ->
1241               let _ = k := !k + 1 in
1242               let _ = report (sprintf "Verifying: %d/%d (f0_flag = %b)" !k r_size f0_flag) in
1243                 if f0_flag then
1244                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1245                   let xx, zz = dest_pair domain in
1246                     m_taylor_cell_pass0 n (fs.f p_stat.pp xx zz)
1247                 else
1248                   let taylor_th = fs.taylor p_stat.pp p_stat.pp domain_th in
1249                     m_taylor_cell_pass n p_stat.pp taylor_th
1250
1251           | P_result_glue (p_stat, i, convex_flag, r1, r2) ->
1252               let domain1_th, domain2_th =
1253                 if convex_flag then
1254                   let d1, _ = restrict_domain n (i + 1) true domain_th in
1255                   let d2, _ = restrict_domain n (i + 1) false domain_th in
1256                     d1, d2
1257                 else
1258                   split_domain n p_split (i + 1) domain_th in
1259               let th1 = rec_verify domain1_th r1 in
1260               let th2 = rec_verify domain2_th r2 in
1261                 if convex_flag then
1262                   let _ = report (sprintf "GlueConvex: %d" (i + 1)) in
1263                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1264                   let xx, zz = dest_pair domain in
1265                   let diff2_th = fs.diff2_f xx zz in
1266                   let partial2_th = fs.ddf (i + 1) (i + 1) p_stat.pp xx zz in
1267                   let lo_partial2_th = eval_interval_arith_lo n partial2_th in
1268                     m_convex_pass n (i + 1) diff2_th lo_partial2_th th1 th2
1269                 else
1270                   m_glue_cells n (i + 1) th1 th2
1271
1272           | P_result_ref i ->
1273               let _ = report (sprintf "Ref: %d" i) in
1274                 if i > 0 then
1275                   List.nth th_list (i - 1)
1276                 else
1277                   let domain, _, _ = (dest_m_cell_domain o concl) domain_th in
1278                   let pass_th = List.nth th_list (-i - 1) in
1279                     m_cell_pass_subdomain domain pass_th in
1280
1281     rec_verify domain_th0 certificate;;
1282
1283 (*****************)
1284
1285 let m_p_verify_raw0 n p_split fs certificate xx zz =
1286   m_p_verify_raw n p_split fs certificate (mk_m_center_domain n p_split xx zz) [];;
1287
1288
1289
1290 let m_p_verify_list n p_split fs certificate_list xx zz =
1291   let domain_hash = Hashtbl.create (length certificate_list * 10) in
1292   let mem, find, add = Hashtbl.mem domain_hash,
1293     Hashtbl.find domain_hash, Hashtbl.add domain_hash in
1294
1295   let get_m_cell_domain n pp domain0 path =
1296     let rec get_rec domain_th path hash =
1297       match path with
1298         | [] -> domain_th
1299         | (s, j) :: ps ->
1300             let hash' = hash^s^(string_of_int j) in
1301               if mem hash' then
1302                 get_rec (find hash') ps hash'
1303               else
1304                 if s = "l" or s = "r" then
1305                   let domain1_th, domain2_th = split_domain n pp j domain_th in
1306                   let hash1 = hash^"l"^(string_of_int j) and
1307                       hash2 = hash^"r"^(string_of_int j) in
1308                   let _ = add hash1 domain1_th; add hash2 domain2_th in
1309                     if s = "l" then
1310                       get_rec domain1_th ps hash'
1311                     else
1312                       get_rec domain2_th ps hash'
1313                 else
1314                   let l_flag = (s = "ml") in
1315                   let domain_th', _ = restrict_domain n j l_flag domain_th in
1316                   let _ = add hash' domain_th' in
1317                     get_rec domain_th' ps hash' in
1318       get_rec domain0 path "" in
1319
1320   let domain_th0 = mk_m_center_domain n p_split xx zz in
1321   let size = length certificate_list in
1322   let k = ref 0 in
1323   let rec rec_verify certificate_list th_list =
1324     match certificate_list with
1325       | [] -> last th_list
1326       | (path, certificate) :: cs ->
1327           let _ = k := !k + 1; report (sprintf "List: %d/%d" !k size) in
1328           let domain_th = get_m_cell_domain n p_split domain_th0 path in
1329           let th = m_p_verify_raw n p_split fs certificate domain_th th_list in
1330             rec_verify cs (th_list @ [th]) in
1331     rec_verify certificate_list [];;