1 needs "Library/transc.ml";;
4 let filename = Filename.temp_file "maxima" ".out" in
6 "echo 'linel:10000; display2d:false;" ^ e ^
7 ";' | maxima | grep '^(%o3)' | sed -e 's/^(%o3) //' >" ^
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;;
15 let maxima_ops = ["+",`(+)`; "-",`(-)`; "*",`( * )`; "/",`(/)`; "^",`(pow)`];;
16 let maxima_funs = ["sin",`sin`; "cos",`cos`];;
18 let mk_uneg = curry mk_comb `(--)`;;
22 fun tm -> let op,t = dest_comb tm in
23 if op = ntm then t else failwith "dest_uneg";;
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);;
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 ^ ")";;
38 string_of_hol `(x + sin(-- &2 * x)) pow 2 - cos(x - &22 / &7)`;;
40 let lexe s = map (function Resword s -> s | Ident s -> s) (lex(explode s));;
42 let parse_bracketed prs inp =
44 ast,")"::rst -> ast,rst
45 | _ -> failwith "Closing bracket expected";;
47 let rec parse_ginfix op opup sof prs inp =
49 e1,hop::rst when hop = op -> parse_ginfix op opup (opup sof e1) prs rst
50 | e1,rest -> sof e1,rest;;
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);;
59 let rec parse_atomic_expression inp =
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
72 | "-" :: rest -> let e,rst = parse_neg rest in mk_uneg e,rst
74 and parse_expression inp =
75 itlist parse_general_infix (map fst maxima_ops) parse_neg inp;;
77 let hol_of_string = fst o parse_expression o lexe;;
79 hol_of_string "sin(x) - cos(-(- - 1 + x))";;
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'));;
86 FACTOR_CONV `&1234567890`;;
88 FACTOR_CONV `x pow 6 - &1`;;
90 FACTOR_CONV `r * (r * x * (&1 - x)) * (&1 - r * x * (&1 - x)) - x`;;
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);;
101 ANTIDERIV_CONV `\x. (x + &5) pow 2 + &77 * x`;;
103 ANTIDERIV_CONV `\x. sin(x) + x pow 11`;;
105 (**** This one fails as expected so we need more simplification later
106 ANTIDERIV_CONV `\x. sin(x) pow 3`;;
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);;
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;;
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);;
140 time ANTIDERIV_CONV `\x. sin(x) pow 3`;;
142 time ANTIDERIV_CONV `\x. sin(x) * sin(x) pow 5 * cos(x) pow 4 + cos(x)`;;
144 let FCT1_WEAK = prove
145 (`(!x. (f diffl f'(x)) x) ==> !x. &0 <= x ==> defint(&0,x) f' (f x - f(&0))`,
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;;
154 INTEGRAL_CONV `\x. sin(x) pow 13`;;