Rqe/defs.ml

   1 (* ====================================================================== *)
   2 (*  Signs                                                                 *)
   3 (* ====================================================================== *)
   4
   5 (* ---------------------------------------------------------------------- *)
   6 (*  Datatype                                                              *)
   7 (* ---------------------------------------------------------------------- *)
   8
   9 let sign_INDUCT,sign_RECURSION = define_type
  10   "sign = Zero | Pos | Neg | Nonzero | Unknown";;
  11
  12 let SIGN_CASES = prove_by_refinement(
  13   `!s. (s = Pos) \/ (s = Neg) \/ (s = Zero) \/ (s = Nonzero) \/ (s = Unknown)`,
  14 (* {{{ Proof *)
  15 [
  16   MATCH_MP_TAC sign_INDUCT;
  17   REWRITE_TAC[];
  18 ]);;
  19 (* }}} *)
  20
  21 let szero_tm,spos_tm,sneg_tm,snonz_tm,sunk_tm = `Zero`,`Pos`,`Neg`,`Nonzero`,`Unknown`;;
  22
  23 (* ------------------------------------------------------------------------- *)
  24 (* Intepretation of signs.                                                   *)
  25 (* ------------------------------------------------------------------------- *)
  26
  27 (* An interpretation of the sign of a polynomial over a set. *)
  28 let interpsign = new_recursive_definition sign_RECURSION
  29   `(interpsign set ply Zero = (!x:real. set x ==> (ply x = &0))) /\
  30    (interpsign set ply Pos  = (!x. set x ==> (ply x > &0))) /\
  31    (interpsign set ply Neg  = (!x. set x ==> (ply x < &0))) /\
  32    (interpsign set ply Nonzero  = (!x. set x ==> (ply x <> &0))) /\
  33    (interpsign set ply Unknown = (!x. set x ==> (ply x = ply x)))`;;
  34
  35
  36 let interpsign_tm = `interpsign`;;
  37 let dest_interpsign interpthm =
  38   let int,[set;poly;sign] = strip_ncomb 3 (concl interpthm) in
  39     if not (int = interpsign_tm) then
  40       failwith "not an interpsign"
  41     else
  42       set,poly,sign;;
  43
  44 (*
  45 let k0 = prove_by_refinement(
  46   `interpsign (\x. x = &10) (\x. -- &10 + x * &1) Zero`,[
  47   REWRITE_TAC[interpsign;poly];
  48   REPEAT STRIP_TAC;
  49   POP_ASSUM MP_TAC;
  50   REAL_ARITH_TAC
  51 ]);;
  52
  53 *)
  54
  55 (* A version for one set but multiple polynomials *)
  56 let interpsigns = new_definition
  57   `interpsigns polyl set signl = ALL2 (interpsign set) polyl signl`;;
  58
  59 let t0 = TAUT `a /\ T <=> a`;;
  60 let interpsigns_thms interpthm =
  61   let ret = map BETA_RULE(
  62     CONJUNCTS (PURE_REWRITE_RULE[interpsign;interpsigns;ALL2;t0] interpthm)) in
  63     ret;;
  64
  65 (* keep interpsign *)
  66 let interpsigns_thms2 interpthm =
  67   CONJUNCTS (PURE_REWRITE_RULE[interpsigns;ALL2;t0] interpthm);;
  68
  69 let interpsigns_tm = `interpsigns`;;
  70 let dest_interpsigns interpthm =
  71   let int,[polys;set;signs] = strip_ncomb 3 (concl interpthm) in
  72     if not (int = interpsigns_tm) then
  73       failwith "not an interpsigns"
  74     else
  75       polys,set,signs;;
  76
  77
  78 let interp_sing = prove(
  79   `interpsign set p s = interpsigns [p] set [s]`,
  80   REWRITE_TAC[interpsigns;ALL2]);;
  81
  82 let interp_doub = prove(
  83   `interpsigns [p1] set [s1] ==> interpsigns pl set sl ==>
  84      interpsigns (CONS p1 pl) set (CONS s1 sl)`,
  85   ASM_MESON_TAC[interpsigns;ALL2]);;
  86
  87 let mk_interpsigns thms =
  88   let thms' = map (PURE_REWRITE_RULE[interp_sing]) thms in
  89     end_itlist (fun t1 t2 -> MATCH_MPL [interp_doub;t1;t2]) thms';;
  90
  91
  92 (*
  93
  94 let t0 = ASSUME `interpsign s1 p1 Zero`;;
  95 let t1 = ASSUME `interpsign s1 p2 Pos`;;
  96 let t2 = ASSUME `interpsign s1 p3 Neg`;;
  97
  98 mk_interpsigns [t0;t1;t2];;
  99 map (PURE_REWRITE_RULE[interp_sing])  [t0;t1;t2];;
 100 *)
 101
 102
 103 (*
 104 let k0 = prove_by_refinement(
 105   `interpsigns [(\x. &1 + x * &1); (\x. &2 + x * &3)] (\x. x = (-- &1)) [Zero; Neg]`,
 106 [
 107   REWRITE_TAC[interpsigns;ALL2;interpsign;poly];
 108   REAL_ARITH_TAC
 109 ]);;
 110 *)
 111
 112 (* ---------------------------------------------------------------------- *)
 113 (*  Partition line                                                        *)
 114 (* ---------------------------------------------------------------------- *)
 115
 116
 117 let partition_line = new_recursive_definition list_RECURSION
 118   `(partition_line [] = [(\x. T)]) /\
 119    (partition_line (CONS h t) =
 120       if t = [] then [(\x. x < h); (\x. x = h); (\x. h < x)] else
 121         APPEND [(\x. x < h); (\x. x = h); (\x. h < x /\ x < HD t)]
 122                 (TL (partition_line t)))`;;
 123
 124 (*
 125 let ex0 = prove(
 126   `partition_line [&1] = [(\x. x < &1); (\x. x = &1); (\x. &1 < x)]`,
 127     REWRITE_TAC[partition_line])
 128
 129 let ex1 = prove(
 130   `partition_line [&1; &2] =
 131     [(\x. x < &1); (\x. x = &1); (\x. &1 < x /\ x < &2); (\x. x = &2); (\x. &2 < x)]`,
 132     REWRITE_TAC[partition_line;APPEND;COND_CLAUSES;NOT_CONS_NIL;TL;HD]);;
 133 *)
 134
 135
 136 let make_partition_list =
 137   let lxt = `\x:real. T`
 138   and htm = `h:real`
 139   and h1tm = `h1:real`
 140   and h2tm = `h2:real`
 141   and x_lt_h = `(\x. x < h)`
 142   and x_eq_h = `(\x:real. x = h)`
 143   and h_lt_x = `(\x. h < x)`
 144   and x_lt_h1 = `(\x. x < h1)`
 145   and x_eq_h1 = `(\x:real. x = h1)`
 146   and x_h1_h2 = `(\x. h1 < x /\ x < h2)` in
 147   let rec make_partition_list ps =
 148     match ps with
 149       [] -> [lxt]
 150     | [h] -> map (subst [h,htm]) [x_lt_h; x_eq_h;h_lt_x]
 151     | h1::h2::t -> (map (subst [(h1,h1tm);(h2,h2tm)])
 152        [x_lt_h1; x_eq_h1;x_h1_h2]) @ tl (make_partition_list (h2::t)) in
 153     make_partition_list;;
 154
 155
 156 (*
 157 make_partition_list [`&1`;`&2`]
 158 *)
 159
 160 (* partition a line based on a list of points
 161    this is just a compact representation of a list of terms
 162 *)
 163 let part_line_tm = `partition_line`;;
 164 let real_bool_ty = `:real->bool`;;
 165 let PARTITION_LINE_CONV pts =
 166   let ptm = mk_comb (part_line_tm,pts) in
 167   let ltm = mk_list ((make_partition_list (dest_list pts)),real_bool_ty) in
 168   let tm = mk_eq (ptm,ltm) in
 169     prove(tm,REWRITE_TAC [partition_line;APPEND;COND_CLAUSES;NOT_CONS_NIL;TL;HD]);;
 170
 171 (*
 172 PARTITION_LINE_CONV `[]:real list`
 173 PARTITION_LINE_CONV `[&1; &2]`
 174 PARTITION_LINE_CONV `[&2; &1]`
 175 PARTITION_LINE_CONV `[a:real; b]`
 176 *)
 177
 178
 179 (* an interpretation of a sign matrix
 180    arguments are a list of points, a list of polynomials, and a sign matrix
 181    the points form an ordered list (smallest first),
 182    each zero of each polynomial must appear among the list of points
 183    and finally, the sign matrix corresponds to the correct sign for the polynomial
 184    in the region represented by the set.
 185 *)
 186 let interpmat = new_definition
 187   `interpmat ptl polyl signll <=>
 188     real_ordered_list ptl /\
 189     ALL2 (interpsigns polyl) (partition_line ptl) signll`;;
 190
 191 let interpmat_tm = `interpmat`;;
 192 let dest_interpmat =
 193   let imat_tm = interpmat_tm in
 194   fun tm ->
 195     let sc,args = strip_comb tm in
 196       if not (sc = imat_tm) then failwith "dest_interpmat: not an interpmat term" else
 197       let [ptl;polyl;signll] = args in
 198         ptl,polyl,signll;;
 199
 200 let interpmat_thms thm =
 201   let [rol_thm;interpsigns_thm] = CONJUNCTS (PURE_REWRITE_RULE[interpmat] thm) in
 202     rol_thm,interpsigns_thm;;
 203
 204 let mk_interpmat_thm rol_thm =
 205     fun all_thm ->
 206       let ret = REWRITE_RULE[GSYM interpmat] (CONJ rol_thm all_thm) in
 207       let l,_ = strip_comb (concl ret) in
 208         if not (l = interpmat_tm) then failwith "mk_interpmat" else ret;;
 209
 210 (*
 211 let rol_thm = rol_thm'''
 212 let all_thm = all_thm''
 213 *)
 214
 215 (* {{{ Doc *)
 216
 217 (*
 218 mk_all2_interpsigns
 219
 220 |- partition_line [x1; x2; x3; x4; x5] =
 221      [(\x. x < x1); (\x. x = x1); (\x. x1 < x /\ x < x2); (\x. x = x2);
 222      (\x. x2 < x /\ x < x3); (\x. x = x3); (\x. x3 < x /\ x < x4); (\x. x = x4);
 223      (\x. x4 < x /\ x < x5); (\x. x = x5); (\x. x5 < x)]
 224
 225 [
 226  |- interpsigns
 227       [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 228       (\x. x < x1)
 229       [Unknown; Pos; Pos; Pos]
 230  .
 231  .
 232  .
 233  .
 234
 235  |- interpsigns
 236       [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 237       (\x. x = x5)
 238       [Pos; Pos; Zero; Zero]
 239
 240  |- interpsigns
 241       [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
 242       (\x. x5 < x)
 243       [Unknown; Pos; Pos; Pos]
 244 ]
 245
 246 -->
 247
 248   |- ALL2 (interpsigns [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]])
 249         (partition_line [x1;x2;x3;x4;x5])
 250         [[Unknown; Pos; Pos; Pos];...; [Pos; Pos; Zero; Zero]; [Unknown; Pos; Pos; Pos]]
 251
 252 *)
 253
 254 (* }}} *)
 255
 256 let all2_thm0 = GEN_ALL(EQT_ELIM(hd (CONJUNCTS ALL2)));;
 257 let all2_thm = GEN_ALL (REWRITE_RULE[AND_IMP_THM] (fst (EQ_IMP_RULE (GSYM (last (CONJUNCTS ALL2))))));;
 258
 259 let mk_all2_interpsigns part_thm is_thms =
 260   let is_tm = fst(dest_comb(fst (dest_comb (concl (hd is_thms))))) in
 261   let all2_thm0' = ISPEC is_tm all2_thm0 in (* it`s having trouble matching *)
 262   let ret = itlist (fun x -> fun y -> MATCH_MPL[all2_thm;x;y]) is_thms all2_thm0' in
 263     REWRITE_RULE[GSYM part_thm] ret;;
 264
 265 let dest_all2 tm =
 266   let a2,l = strip_comb tm in
 267     if fst(dest_const a2) = "ALL2" then
 268       let [a1;a2;a3] = l in
 269         a1,a2,a3
 270     else
 271       failwith "dest_all2: not an ALL2";;
 272
 273 (* ---------------------------------------------------------------------- *)
 274 (*  Sets                                                                  *)
 275 (* ---------------------------------------------------------------------- *)
 276
 277 let is_interval set =
 278   try
 279     let x,bod = dest_abs set in
 280     if is_conj bod then
 281       let l,r = dest_conj bod in
 282         can (dest_binop rlt) l & can (dest_binop rlt) r
 283     else can (dest_binop rlt) bod
 284   with _ -> false;;
 285
 286 (*
 287 is_interval `\x. &4 < x /\ x < &5`;;
 288 is_interval `\x. x = &4`;;
 289 *)
 290
 291 let is_point set =
 292   try
 293     let x,bod = dest_abs set in
 294     if is_eq bod then true else false
 295   with _ -> false;;
 296
 297 (*
 298 is_point `\x. x = &5`
 299 is_point `\x. x = y:real`
 300 *)
 301
 302 (* ---------------------------------------------------------------------- *)
 303 (*  We generate new var names                                             *)
 304 (* ---------------------------------------------------------------------- *)
 305
 306 let new_var,reset_vars =
 307   let id = ref 0 in
 308   let pre = "x_" in
 309   let new_var ty =
 310     id := !id + 1;
 311     mk_var (pre ^ (string_of_int !id),ty) in
 312   let reset_vars () =
 313     id := 0 in
 314     new_var,reset_vars;;