Rqe/condense.ml

   1 (* ====================================================================== *)
   2 (*  CONDENSE                                                              *)
   3 (* ====================================================================== *)
   4 (*
   5 let merge_interpsign ord_thm (thm1,thm2,thm3) =
   6   let thm1' = BETA_RULE(PURE_REWRITE_RULE[interpsign] thm1) in
   7   let thm2' = BETA_RULE(PURE_REWRITE_RULE[interpsign] thm2) in
   8   let thm3' = BETA_RULE(PURE_REWRITE_RULE[interpsign] thm3) in
   9   let set1,_,_ = dest_interpsign thm1 in
  10   let _,s1 = dest_abs set1 in
  11   let set3,_,_ = dest_interpsign thm3 in
  12   let _,s3 = dest_abs set3 in
  13   let gthm =
  14     if is_conj s1 && is_conj s3 then gen_thm
  15     else if is_conj s1 && not (is_conj s3) then gen_thm_noright
  16     else if not (is_conj s1) && is_conj s3 then gen_thm_noleft
  17     else gen_thm_noboth in
  18     PURE_REWRITE_RULE[GSYM interpsign] (MATCH_MPL[gthm;ord_thm;thm1';thm2';thm3']);;
  19 *)
  20 (* {{{ Examples *)
  21
  22 (*
  23
  24 length thms
  25 merge_interpsign ord_thm (hd thms)
  26
  27 let thm1,thm2,thm3 = hd thms
  28
  29 let ord_thm = ASSUME `x2 < x3`;;
  30 let thm1 = ASSUME `interpsign (\x. x < x2) [&1; &2; &3] Pos`;;
  31 let thm2 = ASSUME `interpsign (\x. x = x2) [&1; &2; &3] Pos`;;
  32 let thm3 = ASSUME `interpsign (\x. x2 < x /\ x < x3) [&1; &2; &3] Pos`;;
  33 merge_interpsign ord_thm (thm1,thm2,thm3);;
  34
  35 let ord_thm = ASSUME `x1 < x2`;;
  36 let thm1 = ASSUME `interpsign (\x. x1 < x /\ x < x2) [&1; &2; &3] Pos`;;
  37 let thm2 = ASSUME `interpsign (\x. x = x2) [&1; &2; &3] Pos`;;
  38 let thm3 = ASSUME `interpsign (\x. x2 < x) [&1; &2; &3] Pos`;;
  39 merge_interpsign ord_thm (thm1,thm2,thm3);;
  40
  41 let ord_thm = TRUTH;;
  42 let thm1 = ASSUME `interpsign (\x. x < x1) [&1; &2; &3] Pos`;;
  43 let thm2 = ASSUME `interpsign (\x. x = x1) [&1; &2; &3] Pos`;;
  44 let thm3 = ASSUME `interpsign (\x. x1 < x) [&1; &2; &3] Pos`;;
  45 merge_interpsign ord_thm (thm1,thm2,thm3);;
  46
  47 let ord_thm = ASSUME `x1 < x2 /\ x2 < x3`;;
  48 let thm1 = ASSUME `interpsign (\x. x1 < x /\ x < x2) [&1; &2; &3] Pos`;;
  49 let thm2 = ASSUME `interpsign (\x. x = x2) [&1; &2; &3] Pos`;;
  50 let thm3 = ASSUME `interpsign (\x. x2 < x /\ x < x3) [&1; &2; &3] Pos`;;
  51 merge_interpsign ord_thm (thm1,thm2,thm3);;
  52
  53 let ord_thm = ASSUME `x1 < x3`;;
  54 let thm1 = ASSUME `interpsign (\x. x1 < x /\ x < x2) [&1; &2; &3] Neg`;;
  55 let thm2 = ASSUME `interpsign (\x. x = x2) [&1; &2; &3] Neg`;;
  56 let thm3 = ASSUME `interpsign (\x. x2 < x /\ x < x3) [&1; &2; &3] Neg`;;
  57 merge_interpsign ord_thm (thm1,thm2,thm3);;
  58
  59 let ord_thm = ASSUME `x1 < x3`;;
  60 let thm1 = ASSUME `interpsign (\x. x1 < x /\ x < x2) [&1; &2; &3] Zero`;;
  61 let thm2 = ASSUME `interpsign (\x. x = x2) [&1; &2; &3] Zero`;;
  62 let thm3 = ASSUME `interpsign (\x. x2 < x /\ x < x3) [&1; &2; &3] Zero`;;
  63 merge_interpsign ord_thm (thm1,thm2,thm3);;
  64
  65 let ord_thm = ASSUME `x1 < x3`;;
  66 let thm1 = ASSUME `interpsign (\x. x1 < x /\ x < x2) [&1; &2; &3] Nonzero`;;
  67 let thm2 = ASSUME `interpsign (\x. x = x2) [&1; &2; &3] Nonzero`;;
  68 let thm3 = ASSUME `interpsign (\x. x2 < x /\ x < x3) [&1; &2; &3] Nonzero`;;
  69 merge_interpsign ord_thm (thm1,thm2,thm3);;
  70
  71 let ord_thm = ASSUME `x1 < x3`;;
  72 let thm1 = ASSUME `interpsign (\x. x1 < x /\ x < x2) [&1; &2; &3] Unknown`;;
  73 let thm2 = ASSUME `interpsign (\x. x = x2) [&1; &2; &3] Unknown`;;
  74 let thm3 = ASSUME `interpsign (\x. x2 < x /\ x < x3) [&1; &2; &3] Unknown`;;
  75 merge_interpsign ord_thm (thm1,thm2,thm3);;
  76
  77
  78 *)
  79 (* }}} *)
  80 (*
  81 let rec merge_three l1 l2 l3 =
  82   match l1 with
  83       [] -> []
  84     | h::t -> (hd l1,hd l2,hd l3)::merge_three (tl l1) (tl l2) (tl l3);;
  85 *)
  86
  87 (* {{{ Doc *)
  88 (*
  89   combine_interpsigns
  90     |- interpsigns
  91       [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
  92       (\x. x1 < x /\ x < x2)
  93       [Unknown; Pos; Pos; Neg]
  94    |- interpsigns
  95       [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
  96       (\x. x = x2)
  97       [Unknown; Pos; Pos; Neg];
  98    |- interpsigns
  99       [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 100       (\x. x2 < x /\ x < x3)
 101       [Unknown; Pos; Pos; Neg];
 102 -->
 103    |- interpsigns
 104       [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 105       (\x. x1 < x /\ x < x3)
 106       [Unknown; Pos; Pos; Neg];
 107 *)
 108 (* }}} *)
 109 (*
 110 let combine_interpsigns ord_thm thm1 thm2 thm3 =
 111   let _,_,s1 = dest_interpsigns thm1 in
 112   let _,_,s2 = dest_interpsigns thm2 in
 113   let _,_,s3 = dest_interpsigns thm3 in
 114   if not (s1 = s2) or not (s1 = s3) then failwith "combine_interpsigns: signs not equal" else
 115   try
 116     let thms1 = CONJUNCTS(PURE_REWRITE_RULE[interpsigns;ALL2] thm1) in
 117     let thms2 = CONJUNCTS(PURE_REWRITE_RULE[interpsigns;ALL2] thm2) in
 118     let thms3 = CONJUNCTS(PURE_REWRITE_RULE[interpsigns;ALL2] thm3) in
 119     let thms = butlast (merge_three thms1 thms2 thms3) (* ignore the T at end *) in
 120     let thms' = map (merge_interpsign ord_thm) thms in
 121       mk_interpsigns thms'
 122   with Failure s -> failwith ("combine_interpsigns: " ^ s);;
 123 *)
 124 (* {{{ Examples *)
 125
 126 (*
 127 let thm = combine_interpsigns
 128 let ord_thm,thm1,thm2,thm3 = ord_thm5 ,ci1 ,ci2 ,ci3
 129
 130
 131 let h1 = combine_interpsigns ord_thm int1 pt int2 in
 132 let thm1,thm2,thm3 = int1,pt,int2
 133
 134 let tmp = (ith 0 thms)
 135 merge_interpsign ord_thm tmp
 136
 137 let thm1 = ASSUME
 138      `interpsigns
 139       [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 140       (\x. x1 < x /\ x < x2)
 141       [Unknown; Pos; Pos; Neg]`;;
 142
 143 let thm2 = ASSUME
 144    `interpsigns
 145       [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 146       (\x. x = x2)
 147       [Unknown; Pos; Pos; Neg]`;;
 148
 149 let thm3 = ASSUME
 150    `interpsigns
 151      [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 152       (\x. x2 < x /\ x < x3)
 153       [Unknown; Pos; Pos; Neg]`;;
 154
 155 let ord_thm = ASSUME `x1 < x2 /\ x2 < x3`
 156
 157 combine_interpsigns ord_thm thm1 thm2 thm3;;
 158
 159
 160
 161 let thm1 = ASSUME
 162      `interpsigns
 163       [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 164       (\x. x < x5)
 165       [Unknown; Pos; Pos; Neg]`;;
 166
 167 let thm2 = ASSUME
 168    `interpsigns
 169       [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 170       (\x. x = x5)
 171       [Unknown; Pos; Pos; Neg]`;;
 172
 173 let thm3 = ASSUME
 174    `interpsigns
 175      [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 176       (\x. x5 < x /\ x < x6)
 177       [Unknown; Pos; Pos; Neg]`;;
 178
 179 let ord_thm = ASSUME `x5 < x6`;;
 180
 181 combine_interpsigns ord_thm thm1 thm2 thm3;;
 182
 183
 184 let thm1 = ASSUME
 185      `interpsigns
 186       [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 187       (\x. x < x6)
 188       [Unknown; Pos; Pos; Neg]`;;
 189
 190 let thm2 = ASSUME
 191    `interpsigns
 192       [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 193       (\x. x = x6)
 194       [Unknown; Pos; Pos; Neg]`;;
 195
 196 let thm3 = ASSUME
 197    `interpsigns
 198      [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 199       (\x. x6 < x)
 200       [Unknown; Pos; Pos; Neg]`;;
 201
 202 let ord_thm = ASSUME `x5 < x6`;;
 203
 204 combine_interpsigns ord_thm thm1 thm2 thm3;;
 205
 206
 207 *)
 208
 209 (* }}} *)
 210
 211
 212 (* {{{ Doc *)
 213 (*
 214   get_bounds `\x. x < x1` `\x. x1 < x /\ x < x2`
 215    -->
 216    x1 < x2
 217
 218   get_bounds `\x. x0 < x < x1` `\x. x1 < x /\ x < x2`
 219    -->
 220    x0 < x1 /\ x1 < x2
 221
 222   get_bounds `\x. x < x1` `\x. x1 < x`
 223   -->
 224   T
 225
 226 *)
 227 (* }}} *)
 228 (*
 229 let get_bounds set1 set2 =
 230   let _,s1 = dest_abs set1 in
 231   let _,s2 = dest_abs set2 in
 232   let c1 =
 233     if is_conj s1 then
 234       let l,r = dest_conj s1 in
 235       let l1,l2 = dest_binop rlt l in
 236       let l3,l4 = dest_binop rlt r in
 237         mk_binop rlt l1 l4
 238     else t_tm in
 239   let c2 =
 240     if is_conj s2 then
 241       let l,r = dest_conj s2 in
 242       let l1,l2 = dest_binop rlt l in
 243       let l3,l4 = dest_binop rlt r in
 244         mk_binop rlt l1 l4
 245     else t_tm in
 246   if c1 = t_tm then c2
 247   else if c2 = t_tm then c1
 248   else mk_conj (c1,c2);;
 249 *)
 250 (* {{{ Examples *)
 251 (*
 252   get_bounds `\x. x < x1` `\x. x1 < x /\ x < x2`
 253
 254
 255   get_bounds `\x. x0 < x /\ x < x1` `\x. x1 < x /\ x < x2`
 256
 257   get_bounds `\x. x < x1` `\x. x1 < x`
 258 *)
 259 (* }}} *)
 260
 261
 262 (* {{{ Doc *)
 263
 264 (* collect_pts
 265    |- interpsigns ... (\x. x < x1) ...
 266    |- interpsigns ... (\x. x1 < x /\ x < x4) ...
 267    |- interpsigns ... (\x. x4 < x /\ x < x7) ...
 268    |- interpsigns ... (\x. x7 < x) ...
 269
 270  -->
 271   [x1,x4,x7]
 272 *)
 273
 274 (* }}} *)
 275 (*
 276
 277 let rec collect_pts thms =
 278   match thms with
 279       [] -> []
 280     | h::t ->
 281         let rest = collect_pts t in
 282         let _,set,_ = dest_interpsigns h in
 283         let x,b = dest_abs set in
 284         let bds =
 285           if b = t_tm then []
 286           else if is_conj b then
 287             let l,r = dest_conj b in
 288               [fst(dest_binop rlt l);snd(dest_binop rlt r)]
 289           else
 290             let _,l,r = get_binop b in
 291               if x = l then [r] else [l] in
 292         match rest with
 293             [] -> bds
 294           | h::t -> if not (h = (last bds)) then failwith "pts not in order"
 295               else if length bds = 2 then hd bds::rest else rest;;
 296 *)
 297 (* {{{ Examples *)
 298
 299 (*
 300
 301 let thms = [ASSUME `interpsigns [\x. &0 + x * &1; \x. &1] (\x. T) [Unknown; Pos]`]
 302 let h::t = [ASSUME `interpsigns [\x. &0 + x * &1; \x. &1] (\x. T) [Unknown; Pos]`]
 303 collect_pts [ASSUME `interpsigns [\x. &0 + x * &1; \x. &1] (\x. T) [Unknown; Pos]`]
 304
 305 let t1 = ASSUME `interpsigns [[&1]] (\x. x < x1) [Pos]`
 306 let t2 = ASSUME `interpsigns [[&1]] (\x. x1 < x /\ x < x4) [Pos]`
 307 let t3 = ASSUME `interpsigns [[&1]] (\x. x4 < x /\ x < x7) [Pos]`
 308 let t4 = ASSUME `interpsigns [[&1]] (\x. x7 < x) [Pos]`
 309
 310 collect_pts [t1;t2;t3;t4]
 311
 312 let t1 = ASSUME `interpsigns [[&1]] (\x. x0 < x /\ x < x1) [Pos]`
 313 let t2 = ASSUME `interpsigns [[&1]] (\x. x1 < x /\ x < x4) [Pos]`
 314 let t3 = ASSUME `interpsigns [[&1]] (\x. x4 < x /\ x < x7) [Pos]`
 315 let t4 = ASSUME `interpsigns [[&1]] (\x. x7 < x) [Pos]`
 316
 317 collect_pts [t1;t2;t3;t4]
 318
 319 let t1 = ASSUME
 320       `interpsigns
 321         [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0;
 322         &1]]
 323         (\x. x < x1)
 324         [Unknown; Pos; Pos; Pos]`;;
 325
 326 let t2 = ASSUME
 327   `interpsigns
 328          [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0;
 329          &1]]
 330          (\x. x = x1)
 331          [Neg; Pos; Pos; Zero]`;;
 332
 333 let t3 = ASSUME
 334   `interpsigns
 335          [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0;
 336          &1]]
 337          (\x. x1 < x /\ x < x4)
 338          [Unknown; Pos; Pos; Neg]`;;
 339
 340 let t4 = ASSUME
 341   `interpsigns
 342          [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0;
 343          &1]]
 344          (\x. x = x4)
 345          [Pos; Pos; Zero; Neg]`;;
 346
 347 let t5 = ASSUME
 348   `interpsigns
 349          [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0;
 350          &1]]
 351          (\x. x4 < x /\ x < x5)
 352          [Unknown; Pos; Neg; Neg]`;;
 353
 354 let t6 = ASSUME
 355   `interpsigns
 356          [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0;
 357          &1]]
 358          (\x. x = x5)
 359          [Pos; Pos; Zero; Zero]`;;
 360
 361 let t7 = ASSUME
 362   `interpsigns
 363          [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0;
 364          &1]]
 365          (\x. x5 < x)
 366          [Unknown; Pos; Pos; Pos]`;;
 367
 368 let thms = [t1;t2;t3;t4;t5;t6;t7]
 369 collect_pts thms
 370
 371 *)
 372
 373
 374
 375
 376
 377 (*
 378 combine_identical_lines
 379       |- real_ordered_list [x1; x2; x3; x4; x5]
 380       |- ALL2
 381          (interpsigns [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]])
 382          (partition_line [x1; x2; x3; x4; x5])
 383          [[Unknown; Pos; Pos; Pos];
 384 x1        [Neg; Pos; Pos; Zero];
 385           [Unknown; Pos; Pos; Neg];
 386 x2        [Unknown; Pos; Pos; Neg];
 387           [Unknown; Pos; Pos; Neg];
 388 x3        [Unknown; Pos; Pos; Neg];
 389           [Unknown; Pos; Pos; Neg];
 390 x4        [Pos; Pos; Zero; Neg];
 391           [Unknown; Pos; Neg; Neg];
 392 x5        [Pos; Pos; Zero; Zero];
 393           [Unknown; Pos; Pos; Pos]]
 394
 395  -->
 396
 397
 398       |- ALL2
 399          (interpsigns [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]])
 400          (partition_line [x1; x4; x5])
 401          [[Unknown; Pos; Pos; Pos];
 402 x1        [Neg; Pos; Pos; Zero];
 403           [Unknown; Pos; Pos; Neg];
 404 x4        [Pos; Pos; Zero; Neg];
 405           [Unknown; Pos; Neg; Neg];
 406 x5        [Pos; Pos; Zero; Zero];
 407           [Unknown; Pos; Pos; Pos]]
 408
 409 *)
 410
 411 (* }}} *)
 412
 413 (*
 414 let sublist i j l =
 415   let _,r = chop_list i l in
 416   let l2,r2 = chop_list (j-i+1) r in
 417     l2;;
 418 *)
 419 (* {{{ Examples *)
 420 (*
 421 let i,j,l = 1,4,[1;2;3;4;5;6;7]
 422 sublist 1 4 [1;2;3;4;5;6;7]
 423 sublist 2 4 [1;2;3;4;5;6;7]
 424 sublist 1 1 [1;2;3;4;5;6;7]
 425 *)
 426 (* }}} *)
 427
 428 (*
 429 let rec combine ord_thms l =
 430   let lem = REWRITE_RULE[AND_IMP_THM] REAL_LT_TRANS in
 431   match l with
 432       [int] -> [int]
 433     | [int1;int2] -> [int1;int2]
 434     | int1::pt::int2::rest ->
 435         try
 436           let _,set1,_ = dest_interpsigns int1 in
 437           let _,set2,_ = dest_interpsigns int2 in
 438           let ord_tm = get_bounds set1 set2 in
 439           if ord_tm = t_tm then
 440             let h1 = combine_interpsigns TRUTH int1 pt int2 in
 441               combine ord_thms (h1::rest)
 442           else
 443             let lt,rt =
 444               if is_conj ord_tm then
 445                 let c1,c2 = dest_conj ord_tm in
 446                 let l,_ = dest_binop rlt c1 in
 447                 let _,r = dest_binop rlt c2 in
 448                   l,r
 449               else dest_binop rlt ord_tm in
 450             let e1 = find (fun x -> lt = fst(dest_binop rlt (concl x))) ord_thms in
 451             let i1 = index e1 ord_thms in
 452             let e2 = find (fun x -> rt = snd(dest_binop rlt (concl x))) ord_thms in
 453             let i2 = index e2 ord_thms in
 454             let ord_thms' = sublist i1 i2 ord_thms in
 455             let ord_thm = end_itlist (fun x y -> MATCH_MPL[lem;x;y]) ord_thms' in
 456             let h1 = combine_interpsigns ord_thm int1 pt int2 in
 457               combine ord_thms (h1::rest)
 458         with
 459             Failure "combine_interpsigns: signs not equal" ->
 460               int1::pt::(combine ord_thms(int2::rest));;
 461 *)
 462
 463 (*
 464 let combine_identical_lines rol_thm all_thm =
 465   let tmp,mat = dest_comb (concl all_thm) in
 466   let _,line =  dest_comb tmp in
 467   let _,pts = dest_comb line in
 468   let part_thm = PARTITION_LINE_CONV pts in
 469   let thm' = REWRITE_RULE[ALL2;part_thm] all_thm in
 470   let thms = CONJUNCTS thm' in
 471   let ord_thms = rol_thms rol_thm in
 472   let thms' = combine ord_thms thms in
 473   let pts = collect_pts thms' in
 474   let part_thm' = PARTITION_LINE_CONV (mk_list (pts,real_ty)) in
 475     mk_all2_interpsigns part_thm' thms';;
 476 *)
 477 (* {{{ Examples *)
 478
 479 (*
 480 #untrace combine
 481 #trace combine
 482 let int1::pt::int2::rest = snd (chop_list 6 thms)
 483 let int1::pt::int2::rest = snd (chop_list 0 thms)
 484 let int1::pt::int2::rest = snd (chop_list 2 thms)
 485
 486 let l = thms
 487 let int1::pt::int2::rest = l
 488 combine thms
 489 let rol_thm = ASSUME `real_ordered_list [x1; x2; x3; x4; x5]`
 490 let all_thm = ASSUME
 491    `ALL2
 492          (interpsigns [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]])
 493          (partition_line [x1; x2; x3; x4; x5])
 494          [[Unknown; Pos; Pos; Pos];
 495           [Neg; Pos; Pos; Zero];
 496           [Unknown; Pos; Pos; Neg];
 497           [Unknown; Pos; Pos; Neg];
 498           [Unknown; Pos; Pos; Neg];
 499           [Unknown; Pos; Pos; Neg];
 500           [Unknown; Pos; Pos; Neg];
 501           [Pos; Pos; Zero; Neg];
 502           [Unknown; Pos; Neg; Neg];
 503           [Pos; Pos; Zero; Zero];
 504           [Unknown; Pos; Pos; Pos]]`;;
 505
 506 let all_thm' = combine_identical_lines rol_thm all_thm
 507
 508 *)
 509
 510 (* }}} *)
 511
 512 (* {{{ Doc *)
 513 (*
 514 assumes l2 is a sublist of l1
 515
 516 list_diff [1;2;3;4] [2;3] --> [1;4]
 517
 518 *)
 519 (* }}} *)
 520 (*
 521 let rec list_diff l1 l2 =
 522   match l1 with
 523       [] -> if l2 = [] then [] else failwith "l2 not a sublist of l1"
 524     | h::t ->
 525         match l2 with
 526             [] -> l1
 527           | h'::t' -> if h = h' then list_diff t t'
 528               else h::list_diff t l2;;
 529 *)
 530 (* {{{ Examples *)
 531 (*
 532 list_diff [1;2;3;4] [2;3]
 533 list_diff [1;2;3;4] [1;3;4]
 534 *)
 535 (* }}} *)
 536
 537 (*
 538 let CONDENSE mat_thm =
 539   let rol_thm,all_thm = interpmat_thms mat_thm in
 540   let pts = dest_list (snd (dest_comb (concl rol_thm))) in
 541   let all_thm' = combine_identical_lines rol_thm all_thm in
 542   let _,part,_ = dest_all2 (concl all_thm) in
 543   let plist = dest_list (snd (dest_comb part)) in
 544   let _,part',_ = dest_all2 (concl all_thm') in
 545   let plist' = dest_list (snd (dest_comb part')) in
 546   let rol_thm' = itlist ROL_REMOVE (list_diff plist plist') rol_thm in
 547   let mat_thm' = mk_interpmat_thm rol_thm' all_thm' in
 548     mat_thm';;
 549 *)
 550 (* ---------------------------------------------------------------------- *)
 551 (*  OPT                                                                   *)
 552 (* ---------------------------------------------------------------------- *)
 553
 554 let rec triple_index l =
 555   match l with
 556     [] -> failwith "triple_index"
 557   | [x] -> failwith "triple_index"
 558   | [x;y] -> failwith "triple_index"
 559   | x::y::z::rest -> if x = y && y = z then 0 else 1 + triple_index (y::z::rest);;
 560
 561 let tmp = ref TRUTH;;
 562 (*
 563 let
 564 tmp
 565 let mat_thm = !tmp
 566 let mat_thm = mat_thm'
 567 *)
 568 let rec CONDENSE =
 569   let real_app = `APPEND:real list -> real list -> real list` in
 570   let sign_app = `APPEND:(sign list) list -> (sign list) list -> (sign list) list` in
 571   let real_len = `LENGTH:real list -> num` in
 572   let sign_len = `LENGTH:(sign list) list -> num` in
 573   let num_mul = `( * ):num -> num -> num` in
 574   let real_ty = `:real` in
 575   let two = `2` in
 576   let sl_ty = `:sign list` in
 577   fun mat_thm ->
 578     try
 579       tmp := mat_thm;
 580       let pts,_,sgns = dest_interpmat (concl mat_thm) in
 581       let sgnl = dest_list sgns in
 582       let ptl = dest_list pts in
 583       let i = triple_index sgnl (* fail here if fully condensed *) in
 584       if not (i mod 2 = 0) then failwith "misshifted matrix" else
 585       if i = 0 then
 586         if length ptl = 1 then MATCH_MP INTERPMAT_SING mat_thm
 587         else CONDENSE (MATCH_MP INTERPMAT_TRIO mat_thm) else
 588       let l,r = chop_list (i - 2) sgnl in
 589       let sgn1,sgn2 = mk_list(l,sl_ty),mk_list(r,sl_ty) in
 590       let sgns' = mk_comb(mk_comb(sign_app,sgn1),sgn2) in
 591       let sgn_thm = prove(mk_eq(sgns,sgns'),REWRITE_TAC[APPEND]) in
 592       let l',r' = chop_list (i / 2 - 1) ptl (* i always even *) in
 593       let pt1,pt2 = mk_list(l',real_ty),mk_list(r',real_ty) in
 594       let pts' = mk_comb(mk_comb(real_app,pt1),pt2) in
 595       let pt_thm = prove(mk_eq(pts,pts'),REWRITE_TAC[APPEND]) in
 596       let mat_thm' = ONCE_REWRITE_RULE[sgn_thm;pt_thm] mat_thm in
 597       let len_thm = prove((mk_eq(mk_comb(sign_len,sgn1),mk_binop num_mul two (mk_comb(real_len,pt1)))),REWRITE_TAC[LENGTH] THEN ARITH_TAC) in
 598         CONDENSE (REWRITE_RULE[APPEND]
 599          (MATCH_MP (MATCH_MP INTERPMAT_TRIO_INNER mat_thm') len_thm))
 600   with
 601     Failure "triple_index" -> mat_thm
 602   | Failure x -> failwith ("CONDENSE: " ^ x);;
 603
 604
 605 (* {{{ Examples *)
 606
 607 (*
 608
 609 let mat_thm = mat_thm'
 610 CONDENSE mat_thm
 611
 612
 613 let mat_thm = ASSUME
 614   `interpmat [x1; x2; x3; x4; x5]
 615      [\x. &1 + x * (&2 + x * &3); \x. &2 + x * (-- &3 + x * &1); \x. -- &4 + x * (&0 + x * &1);
 616       \x. &8 + x * &4; \x. -- &7 + x * &11; \x. &5 + x * &5]
 617       [
 618       [Pos; Pos; Pos; Neg; Neg; Neg];
 619       [Pos; Pos; Pos; Neg; Neg; Neg];
 620       [Pos; Pos; Pos; Neg; Neg; Neg];
 621       [Pos; Pos; Pos; Neg; Neg; Neg];
 622       [Pos; Pos; Pos; Neg; Neg; Neg];
 623       [Pos; Pos; Pos; Neg; Neg; Neg];
 624       [Pos; Pos; Pos; Neg; Neg; Neg];
 625       [Pos; Pos; Pos; Neg; Neg; Neg];
 626       [Pos; Pos; Pos; Neg; Neg; Neg];
 627       [Zero; Pos; Pos; Neg; Neg; Neg];
 628       [Neg; Pos; Pos; Neg; Neg; Neg]
 629      ]`
 630
 631
 632 let mat_thm = ASSUME
 633   `interpmat [x1; x2; x3; x4; x5]
 634      [\x. &1 + x * (&2 + x * &3); \x. &2 + x * (-- &3 + x * &1); \x. -- &4 + x * (&0 + x * &1);
 635       \x. &8 + x * &4; \x. -- &7 + x * &11; \x. &5 + x * &5]
 636       [[Pos; Pos; Pos; Neg; Neg; Neg];
 637       [Pos; Pos; Zero; Zero; Neg; Neg];
 638       [Pos; Pos; Neg; Pos; Neg; Neg];
 639       [Pos; Pos; Neg; Pos; Neg; Zero];
 640       [Pos; Pos; Neg; Pos; Neg; Pos];
 641       [Pos; Pos; Neg; Pos; Zero; Pos];
 642       [Pos; Pos; Neg; Pos; Pos; Pos];
 643       [Pos; Zero; Neg; Pos; Pos; Pos];
 644       [Pos; Neg; Neg; Pos; Pos; Pos];
 645       [Pos; Zero; Zero; Pos; Pos; Pos];
 646       [Pos; Pos; Pos; Pos; Pos; Pos]]`
 647
 648 let mat_thm' = INFERPSIGN vars sgns mat_thm div_thms
 649
 650 CONDENSE mat_thm
 651
 652
 653
 654 *)
 655
 656 (* }}} *)
 657
 658 (* ---------------------------------------------------------------------- *)
 659 (*  Timing                                                                *)
 660 (* ---------------------------------------------------------------------- *)
 661
 662 let CONDENSE mat_thm =
 663   let start_time = Sys.time() in
 664   let res = CONDENSE mat_thm in
 665     condense_timer +.= (Sys.time() -. start_time);
 666     res;;
 667