Rqe/matinsert.ml

   1
   2 let ROWINSERT =
   3   let lxt = `\x:real. T` in
   4   fun i const_thm interpsigns_thm ->
   5     let isigns_thms = interpsigns_thms2 interpsigns_thm in
   6     let isigns_thm = hd isigns_thms in
   7     let set,_,_ =
   8       if concl isigns_thm = t_tm then lxt,t_tm,t_tm else
   9         dest_interpsign (hd isigns_thms) in
  10     let const_thm' = MATCH_MP (ISPEC set matinsert_lem0) const_thm in
  11     let const_thm'' = PURE_REWRITE_RULE[GSYM interpsign] const_thm' in
  12     let isigns_thms' = insertat i const_thm'' isigns_thms in
  13     let isigns_thms'' = if isigns_thm = TRUTH then butlast isigns_thms' else isigns_thms' in
  14       mk_interpsigns isigns_thms'';;
  15
  16 let MATINSERT vars i const_thm cont mat_thm =
  17   let const_thm' = GEN (hd vars) const_thm in
  18   let rol_thm,all2_thm = interpmat_thms mat_thm in
  19   let part_thm = PARTITION_LINE_CONV (snd (dest_comb (concl rol_thm))) in
  20   let isigns_thms = CONJUNCTS(REWRITE_RULE[ALL2;part_thm] all2_thm) in
  21   let isigns_thms' = map (ROWINSERT i const_thm') isigns_thms in
  22   let all2_thm' = mk_all2_interpsigns part_thm isigns_thms' in
  23   let mat_thm' = mk_interpmat_thm rol_thm all2_thm' in
  24     cont mat_thm';;
  25
  26
  27
  28 (* ---------------------------------------------------------------------- *)
  29 (*  Opt                                                                   *)
  30 (* ---------------------------------------------------------------------- *)
  31
  32 (* OPT FAILED... slightly slower, even with hashtables *)
  33
  34 let rec mk_suc =
  35   let zero = `0` in
  36   let suc = `SUC` in
  37   fun n ->
  38     match n with
  39       0 -> zero
  40     | n -> mk_comb(suc,mk_suc (n-1));;
  41
  42 let rec MK_SUC =
  43   let f n = prove(mk_eq(mk_small_numeral n,mk_suc n),ARITH_TAC) in
  44   let size = 100 in
  45   let range = 0--size in
  46   let suc_tbl = Hashtbl.create size in
  47   map2 (Hashtbl.add suc_tbl) range (map f range);
  48   fun n ->
  49     try Hashtbl.find suc_tbl n with _ -> f n;;
  50
  51 let PL_LENGTH =
  52   let pl_tm = `partition_line` in
  53   let len_tm = `LENGTH:(real -> bool) list -> num` in
  54   fun pts ->
  55     let lpts = mk_comb(len_tm,mk_comb(pl_tm,pts)) in
  56     let lthm = ARITH_SIMP_CONV[PARTITION_LINE_LENGTH;LENGTH] lpts in
  57     let pts' = snd(dest_eq(concl lthm)) in
  58     let n = dest_small_numeral pts' in
  59     let suc_thm = MK_SUC n in
  60       TRANS lthm suc_thm;;
  61
  62
  63 let rec MK_LT =
  64   let f(n1,n2) = prove(mk_binop nle (mk_suc n1) (mk_suc n2),ARITH_TAC) in
  65   let size1 = 20 in
  66   let size2 = 20 in
  67   let range1 = 0--size1 in
  68   let range2 = 0--size2 in
  69   let range = filter (fun (x,y) -> x <= y) (allpairs (fun x y -> x,y) range1 range2) in
  70   let suc_tbl = Hashtbl.create (size1 * size2) in
  71   map2 (Hashtbl.add suc_tbl) range (map f range);
  72   fun (n1,n2) ->
  73     try Hashtbl.find suc_tbl (n1,n2) with _ -> f(n1,n2);;
  74
  75
  76 (*
  77 let vars,i,const_thm,mat_thm = !ti,!tconst,!tmat
  78 #trace MATINSERT
  79 *)
  80
  81
  82 (* ---------------------------------------------------------------------- *)
  83 (*  Timing                                                                *)
  84 (* ---------------------------------------------------------------------- *)
  85
  86 let MATINSERT vars i const_thm cont mat_thm =
  87   let start_time = Sys.time() in
  88   let res = MATINSERT vars i const_thm cont mat_thm in
  89     matinsert_timer +.= (Sys.time() -. start_time);
  90     res;;
  91
  92
  93
  94 (*
  95
  96 let vars,i,const_thm, cont,mat_thm =
  97 [ry;rx],
  98 0,
  99 ASSUME `-- &1 < &0`,
 100 I,
 101 ASSUME `interpmat [x_24] [\x. &0 + x * &1] [[Neg]; [Zero]; [Pos]]`
 102
 103 MATINSERT vars i const_thm cont mat_thm
 104
 105
 106 let vars,i,const_thm, cont,mat_thm =
 107 [ry;rx],
 108 0,
 109 ASSUME `&0 + x * &1 < &0`,
 110 I,
 111 ASSUME `interpmat [] [\y. &1] [[Pos]]`
 112
 113 MATINSERT vars i const_thm cont mat_thm
 114
 115
 116 let vars,i,const_thm, cont,mat_thm =
 117 [`x:real`; `a:real`; `b:real`; `c:real`],
 118 0,
 119 ASSUME `&0 + a * &2 < &0`,
 120 I,
 121 ASSUME `interpmat [x_408] [\x. (&0 + b * &1) + x * (&0 + a * &2)] [[Pos]; [Zero]; [Neg]]`
 122
 123 MATINSERT vars i const_thm cont mat_thm
 124
 125 *)