30 "----------- check return value of get_calculation_ ----"; |
30 "----------- check return value of get_calculation_ ----"; |
31 val thy = @{theory "Poly"}; |
31 val thy = @{theory "Poly"}; |
32 val cal = snd (assoc_calc' thy "is_polyexp"); |
32 val cal = snd (assoc_calc' thy "is_polyexp"); |
33 val t = @{term "(x / x) is_polyexp"}; |
33 val t = @{term "(x / x) is_polyexp"}; |
34 val SOME (thmID, thm) = get_calculation_ thy cal t; |
34 val SOME (thmID, thm) = get_calculation_ thy cal t; |
35 (HOLogic.dest_Trueprop (prop_of thm); writeln "all thms wrapped by Trueprop") |
35 (HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop") |
36 handle TERM _ => |
36 handle TERM _ => |
37 error "calculate.sml: get_calculation_ must return Trueprop"; |
37 error "calculate.sml: get_calculation_ must return Trueprop"; |
38 |
38 |
39 "----------- fun calculate_ -----------------------------"; |
39 "----------- fun calculate_ -----------------------------"; |
40 "----------- fun calculate_ -----------------------------"; |
40 "----------- fun calculate_ -----------------------------"; |
41 "----------- fun calculate_ -----------------------------"; |
41 "----------- fun calculate_ -----------------------------"; |
42 val thy = @{theory "Test"}; |
42 val thy = @{theory "Test"}; |
43 "===== test 1"; |
43 "===== test 1"; |
44 val t = (term_of o the o (parse thy)) "1+2"; |
44 val t = (Thm.term_of o the o (parse thy)) "1+2"; |
45 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; |
45 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; |
46 term2str (prop_of thm) = "1 + 2 = 3"; |
46 term2str (prop_of thm) = "1 + 2 = 3"; |
47 |
47 |
48 "===== test 2"; |
48 "===== test 2"; |
49 val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2"; |
49 val t = (Thm.term_of o the o (parse thy)) "((1+2)*4/3)^^^2"; |
50 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; |
50 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; |
51 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
51 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
52 if term2str t = "(3 * 4 / 3) ^^^ 2" then () |
52 if term2str t = "(3 * 4 / 3) ^^^ 2" then () |
53 else error "calculate.sml: ((1+2)*4/3)^^^2 --> (3 * 4 / 3) ^^^ 2"; |
53 else error "calculate.sml: ((1+2)*4/3)^^^2 --> (3 * 4 / 3) ^^^ 2"; |
54 |
54 |
129 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2)))) |
129 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2)))) |
130 ............... does not work *) |
130 ............... does not work *) |
131 |
131 |
132 (*--------------(2): does divide work in Test_simplify ?: ------*) |
132 (*--------------(2): does divide work in Test_simplify ?: ------*) |
133 val thy = @{theory Test}; |
133 val thy = @{theory Test}; |
134 val t = (term_of o the o (parse thy)) "6 / 2"; |
134 val t = (Thm.term_of o the o (parse thy)) "6 / 2"; |
135 val rls = Test_simplify; |
135 val rls = Test_simplify; |
136 val (t,_) = the (rewrite_set_ thy false rls t); |
136 val (t,_) = the (rewrite_set_ thy false rls t); |
137 (*val t = Free ("3","Real.real") : term*) |
137 (*val t = Free ("3","Real.real") : term*) |
138 |
138 |
139 val thy = "Test"; |
139 val thy = "Test"; |
143 (*val t = "3" : string |
143 (*val t = "3" : string |
144 ....... works, thus: which rule in SqRoot_simplify works differently ?*) |
144 ....... works, thus: which rule in SqRoot_simplify works differently ?*) |
145 |
145 |
146 |
146 |
147 (*--------------(3): is_const works ?: -------------------------------------*) |
147 (*--------------(3): is_const works ?: -------------------------------------*) |
148 val t = (term_of o the o (parse @{theory Test})) "2 is_const"; |
148 val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const"; |
149 atomty t; |
149 atomty t; |
150 rewrite_set_ @{theory Test} false tval_rls t; |
150 rewrite_set_ @{theory Test} false tval_rls t; |
151 (*val it = SOME (Const ("HOL.True","bool"),[]) ... works*) |
151 (*val it = SOME (Const ("HOL.True","bool"),[]) ... works*) |
152 |
152 |
153 val t = str2term "2 * x is_const"; |
153 val t = str2term "2 * x is_const"; |
159 "----------- check calculate bottom up ------------------"; |
159 "----------- check calculate bottom up ------------------"; |
160 "----------- check calculate bottom up ------------------"; |
160 "----------- check calculate bottom up ------------------"; |
161 (*-------------- eval_cancel works: *) |
161 (*-------------- eval_cancel works: *) |
162 trace_rewrite:=false; |
162 trace_rewrite:=false; |
163 val thy = @{theory Test}; |
163 val thy = @{theory Test}; |
164 val t = (term_of o the o (parse thy)) "(-4) / 2"; |
164 val t = (Thm.term_of o the o (parse thy)) "(-4) / 2"; |
165 |
165 |
166 val SOME (_, t) = eval_cancel "xxx" "Fields.inverse_class.divide" t thy; |
166 val SOME (_, t) = eval_cancel "xxx" "Fields.inverse_class.divide" t thy; |
167 |
167 |
168 term2str t; |
168 term2str t; |
169 "-4 / 2 = (-2)"; |
169 "-4 / 2 = (-2)"; |
280 trace_rewrite:=false; |
280 trace_rewrite:=false; |
281 |
281 |
282 "----------- Atools.pow Power.power_class.power ---------"; |
282 "----------- Atools.pow Power.power_class.power ---------"; |
283 "----------- Atools.pow Power.power_class.power ---------"; |
283 "----------- Atools.pow Power.power_class.power ---------"; |
284 "----------- Atools.pow Power.power_class.power ---------"; |
284 "----------- Atools.pow Power.power_class.power ---------"; |
285 val t = (term_of o the o (parseold thy)) "1 ^ aaa"; |
285 val t = (Thm.term_of o the o (parseold thy)) "1 ^ aaa"; |
286 atomty t; |
286 atomty t; |
287 (*** ------------- |
287 (*** ------------- |
288 *** Const ( Nat.power, ['a, nat] => 'a) |
288 *** Const ( Nat.power, ['a, nat] => 'a) |
289 *** . Free ( 1, 'a) |
289 *** . Free ( 1, 'a) |
290 *** . Free ( aaa, nat) *) |
290 *** . Free ( aaa, nat) *) |
300 " ================= calculate.sml: calculate_ 2002 =================== "; |
300 " ================= calculate.sml: calculate_ 2002 =================== "; |
301 " ================= calculate.sml: calculate_ 2002 =================== "; |
301 " ================= calculate.sml: calculate_ 2002 =================== "; |
302 " ================= calculate.sml: calculate_ 2002 =================== "; |
302 " ================= calculate.sml: calculate_ 2002 =================== "; |
303 |
303 |
304 val thy = @{theory Test}; |
304 val thy = @{theory Test}; |
305 val t = (term_of o the o (parse thy)) "12 / 3"; |
305 val t = (Thm.term_of o the o (parse thy)) "12 / 3"; |
306 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t; |
306 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t; |
307 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
307 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
308 "12 / 3 = 4"; |
308 "12 / 3 = 4"; |
309 val thy = @{theory Test}; |
309 val thy = @{theory Test}; |
310 val t = (term_of o the o (parse thy)) "4 ^^^ 2"; |
310 val t = (Thm.term_of o the o (parse thy)) "4 ^^^ 2"; |
311 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER"))) t; |
311 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER"))) t; |
312 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
312 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
313 "4 ^ 2 = 16"; |
313 "4 ^ 2 = 16"; |
314 |
314 |
315 val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2"; |
315 val t = (Thm.term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2"; |
316 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; |
316 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; |
317 "1 + 2 = 3"; |
317 "1 + 2 = 3"; |
318 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
318 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
319 term2str t; |
319 term2str t; |
320 "(3 * 4 / 3) ^^^ 2"; |
320 "(3 * 4 / 3) ^^^ 2"; |
335 "16"; |
335 "16"; |
336 if it <> "16" then error "calculate.sml: new behaviour in calculate_" |
336 if it <> "16" then error "calculate.sml: new behaviour in calculate_" |
337 else (); |
337 else (); |
338 |
338 |
339 (*13.9.02 *** calc: operator = pow not defined*) |
339 (*13.9.02 *** calc: operator = pow not defined*) |
340 val t = (term_of o the o (parse thy)) "3^^^2"; |
340 val t = (Thm.term_of o the o (parse thy)) "3^^^2"; |
341 val SOME (thmID,thm) = |
341 val SOME (thmID,thm) = |
342 get_calculation_ thy (the(assoc(calclist,"POWER"))) t; |
342 get_calculation_ thy (the(assoc(calclist,"POWER"))) t; |
343 (*** calc: operator = pow not defined*) |
343 (*** calc: operator = pow not defined*) |
344 |
344 |
345 val (op_, eval_fn) = the (assoc(calclist,"POWER")); |
345 val (op_, eval_fn) = the (assoc(calclist,"POWER")); |