Tutorial/Linking_external_tools.ml

   1 needs "Library/transc.ml";;
   2
   3 let maximas e =
   4   let filename = Filename.temp_file "maxima" ".out" in
   5   let s =
   6     "echo 'linel:10000; display2d:false;" ^ e ^
   7     ";' | maxima | grep '^(%o3)' | sed -e 's/^(%o3) //' >" ^
   8     filename in
   9   if Sys.command s <> 0 then failwith "maxima" else
  10   let fd = Pervasives.open_in filename in
  11   let data = input_line fd in
  12   close_in fd; Sys.remove filename; data;;
  13
  14 prioritize_real();;
  15 let maxima_ops = ["+",`(+)`; "-",`(-)`; "*",`( * )`;  "/",`(/)`; "^",`(pow)`];;
  16 let maxima_funs = ["sin",`sin`; "cos",`cos`];;
  17
  18 let mk_uneg = curry mk_comb `(--)`;;
  19
  20 let dest_uneg =
  21   let ntm = `(--)` in
  22   fun tm -> let op,t = dest_comb tm in
  23             if op = ntm then t else failwith "dest_uneg";;
  24
  25 let mk_pow = let f = mk_binop `(pow)` in fun x y -> f x (rand y);;
  26 let mk_realvar = let real_ty = `:real` in fun x -> mk_var(x,real_ty);;
  27
  28 let rec string_of_hol tm =
  29   if is_ratconst tm then "("^string_of_num(rat_of_term tm)^")"
  30   else if is_numeral tm then string_of_num(dest_numeral tm)
  31   else if is_var tm then fst(dest_var tm)
  32   else if can dest_uneg tm then "-(" ^ string_of_hol(rand tm) ^ ")" else
  33   let lop,r = dest_comb tm in
  34   try let op,l = dest_comb lop in
  35       "("^string_of_hol l^" "^ rev_assoc op maxima_ops^" "^string_of_hol r^")"
  36   with Failure _ -> rev_assoc lop maxima_funs ^ "(" ^ string_of_hol r ^ ")";;
  37
  38 string_of_hol `(x + sin(-- &2 * x)) pow 2 - cos(x - &22 / &7)`;;
  39
  40 let lexe s = map (function Resword s -> s | Ident s -> s) (lex(explode s));;
  41
  42 let parse_bracketed prs inp =
  43   match prs inp with
  44     ast,")"::rst -> ast,rst
  45   | _ -> failwith "Closing bracket expected";;
  46
  47 let rec parse_ginfix op opup sof prs inp =
  48   match prs inp with
  49     e1,hop::rst when hop = op -> parse_ginfix op opup (opup sof e1) prs rst
  50   | e1,rest -> sof e1,rest;;
  51
  52 let parse_general_infix op =
  53   let opcon = if op = "^" then mk_pow else mk_binop (assoc op maxima_ops) in
  54   let constr = if op <> "^" & snd(get_infix_status op) = "right"
  55                then fun f e1 e2 -> f(opcon e1 e2)
  56                else fun f e1 e2 -> opcon(f e1) e2 in
  57   parse_ginfix op constr (fun x -> x);;
  58
  59 let rec parse_atomic_expression inp =
  60   match inp with
  61    [] -> failwith "expression expected"
  62   | "(" :: rest -> parse_bracketed parse_expression rest
  63   | s :: rest when forall isnum (explode s) ->
  64         term_of_rat(num_of_string s),rest
  65   | s :: "(" :: rest when forall isalnum (explode s) ->
  66         let e,rst = parse_bracketed parse_expression rest in
  67         mk_comb(assoc s maxima_funs,e),rst
  68   | s :: rest when forall isalnum (explode s) -> mk_realvar s,rest
  69 and parse_exp inp = parse_general_infix "^" parse_atomic_expression inp
  70 and parse_neg inp =
  71   match inp with
  72    | "-" :: rest -> let e,rst = parse_neg rest in mk_uneg e,rst
  73    | _ -> parse_exp inp
  74 and parse_expression inp =
  75   itlist parse_general_infix (map fst maxima_ops) parse_neg inp;;
  76
  77 let hol_of_string = fst o parse_expression o lexe;;
  78
  79 hol_of_string "sin(x) - cos(-(- - 1 + x))";;
  80
  81 let FACTOR_CONV tm =
  82   let s = "factor("^string_of_hol tm^")" in
  83   let tm' = hol_of_string(maximas s) in
  84   REAL_RING(mk_eq(tm,tm'));;
  85
  86 FACTOR_CONV `&1234567890`;;
  87
  88 FACTOR_CONV `x pow 6 - &1`;;
  89
  90 FACTOR_CONV `r * (r * x * (&1 - x)) * (&1 - r * x * (&1 - x)) - x`;;
  91
  92 let ANTIDERIV_CONV tm =
  93   let x,bod = dest_abs tm in
  94   let s = "integrate("^string_of_hol bod^","^fst(dest_var x)^")" in
  95   let tm' = mk_abs(x,hol_of_string(maximas s)) in
  96   let th1 = CONV_RULE (NUM_REDUCE_CONV THENC REAL_RAT_REDUCE_CONV)
  97                       (SPEC x (DIFF_CONV tm')) in
  98   let th2 = REAL_RING(mk_eq(lhand(concl th1),bod)) in
  99   GEN x (GEN_REWRITE_RULE LAND_CONV [th2] th1);;
 100
 101 ANTIDERIV_CONV `\x. (x + &5) pow 2 + &77 * x`;;
 102
 103 ANTIDERIV_CONV `\x. sin(x) + x pow 11`;;
 104
 105 (**** This one fails as expected so we need more simplification later
 106 ANTIDERIV_CONV `\x. sin(x) pow 3`;;
 107  ****)
 108
 109 let SIN_N_CLAUSES = prove
 110  (`(sin(&(NUMERAL(BIT0 n)) * x) =
 111     &2 * sin(&(NUMERAL n) * x) * cos(&(NUMERAL n) * x)) /\
 112    (sin(&(NUMERAL(BIT1 n)) * x) =
 113         sin(&(NUMERAL(BIT0 n)) * x) * cos(x) +
 114         sin(x) * cos(&(NUMERAL(BIT0 n)) * x)) /\
 115    (cos(&(NUMERAL(BIT0 n)) * x) =
 116         cos(&(NUMERAL n) * x) pow 2 - sin(&(NUMERAL n) * x) pow 2) /\
 117    (cos(&(NUMERAL(BIT1 n)) * x) =
 118         cos(&(NUMERAL(BIT0 n)) * x) * cos(x) -
 119         sin(x) * sin(&(NUMERAL(BIT0 n)) * x))`,
 120   REWRITE_TAC[REAL_MUL_2; REAL_POW_2] THEN
 121   REWRITE_TAC[NUMERAL; BIT0; BIT1] THEN
 122   REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_ADD] THEN
 123   REWRITE_TAC[REAL_ADD_RDISTRIB; SIN_ADD; COS_ADD; REAL_MUL_LID] THEN
 124   CONV_TAC REAL_RING);;
 125
 126 let TRIG_IDENT_TAC x =
 127   REWRITE_TAC[SIN_N_CLAUSES; SIN_ADD; COS_ADD] THEN
 128   REWRITE_TAC[REAL_MUL_LZERO; SIN_0; COS_0; REAL_MUL_RZERO] THEN
 129   MP_TAC(SPEC x SIN_CIRCLE) THEN CONV_TAC REAL_RING;;
 130
 131 let ANTIDERIV_CONV tm =
 132   let x,bod = dest_abs tm in
 133   let s = "expand(integrate("^string_of_hol bod^","^fst(dest_var x)^"))" in
 134   let tm' = mk_abs(x,hol_of_string(maximas s)) in
 135   let th1 = CONV_RULE (NUM_REDUCE_CONV THENC REAL_RAT_REDUCE_CONV)
 136                       (SPEC x (DIFF_CONV tm')) in
 137   let th2 = prove(mk_eq(lhand(concl th1),bod),TRIG_IDENT_TAC x) in
 138   GEN x (GEN_REWRITE_RULE LAND_CONV [th2] th1);;
 139
 140 time ANTIDERIV_CONV `\x. sin(x) pow 3`;;
 141
 142 time ANTIDERIV_CONV `\x. sin(x) * sin(x) pow 5 * cos(x) pow 4 + cos(x)`;;
 143
 144 let FCT1_WEAK = prove
 145  (`(!x. (f diffl f'(x)) x) ==> !x. &0 <= x ==> defint(&0,x) f' (f x - f(&0))`,
 146   MESON_TAC[FTC1]);;
 147
 148 let INTEGRAL_CONV tm =
 149   let th1 = MATCH_MP FCT1_WEAK (ANTIDERIV_CONV tm) in
 150   (CONV_RULE REAL_RAT_REDUCE_CONV o
 151    REWRITE_RULE[SIN_0; COS_0; REAL_MUL_LZERO; REAL_MUL_RZERO] o
 152    CONV_RULE REAL_RAT_REDUCE_CONV o BETA_RULE) th1;;
 153
 154 INTEGRAL_CONV `\x. sin(x) pow 13`;;