1 (* Title: "ProgLang/evaluate.sml"
2 test calculation of values for function constants
3 Author: Walther Neuper 2000
4 (c) copyright due to lincense terms.
7 "--------------------------------------------------------";
8 "table of contents --------------------------------------";
9 "--------------------------------------------------------";
10 "-calculate.thy: provides 'setup' -----------------------";
11 "----------- fun norm -----------------------------------";
12 "----------- check return value of adhoc_thm ----";
13 "----------- fun calculate_ --------------------------------------------------------------------";
14 "----------- calculate from Prog --------------------------------- -----------------------------";
15 "----------- calculate from script --requires 'setup'----";
16 "----------- calculate check test-root-equ --------------";
17 "----------- check calculate bottom up -----------------";
18 "----------- Prog_Expr.pow Power.power_class.power ---------";
19 "----------- fun cancel_int --------------------------------------------------------------------";
20 "----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
21 "----------- get_pair with 3 args -----------------------";
22 "----------- calculate (2 * x is_num) -------------------";
23 "----------- fun get_pair: examples ------------------------------------------------------------";
24 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
25 "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
26 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
27 "----------- fun power -------------------------------------------------------------------------";
28 "----------- fun divisors ----------------------------------------------------------------------";
29 "----------- fun doubles, fun squfact ----------------------------------------------------------";
30 "--------------------------------------------------------";
31 "--------------------------------------------------------";
32 "--------------------------------------------------------";
34 "----------- check return value of adhoc_thm ----";
35 "----------- check return value of adhoc_thm ----";
36 "----------- check return value of adhoc_thm ----";
37 val thy = @{theory "Poly"};
38 val ctxt = Proof_Context.init_global thy;
39 val cal = snd (get_calc ctxt "is_polyexp");
40 val t = @{term "(x / x) is_polyexp"};
41 val SOME (thmID, thm) = adhoc_thm ctxt cal t;
42 (HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
44 error "evaluate.sml: adhoc_thm must return Trueprop";
46 "----------- fun calculate_ --------------------------------------------------------------------";
47 "----------- fun calculate_ --------------------------------------------------------------------";
48 "----------- fun calculate_ --------------------------------------------------------------------";
49 (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
50 val t = TermC.str2term "((1+2)*4/3) \<up> 2";
52 val ctxt = Proof_Context.init_global @{theory}
53 val times = ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval.ml_fun;
54 val plus = ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval.ml_fun;
55 val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval.ml_fun;
56 val pow = (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval.ml_fun;
58 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
59 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{context} isa_fn t;
60 val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
61 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_ 1 + 2 = 3 changed";
63 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
64 val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{context} isa_fn t';
65 val SOME (t'', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
66 if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_ 3 * 4 = 12 changed";
68 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
69 val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{context} isa_fn t;
70 val SOME (t''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
71 if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_ 12 / 3 = 4 changed";
73 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
74 val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{context} isa_fn t;
75 val SOME (t'''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
76 if UnparseC.term t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed";
78 "----------- calculate from Prog --------------------------------- -----------------------------";
79 "----------- calculate from Prog --------------------------------- -----------------------------";
80 "----------- calculate from Prog --------------------------------- -----------------------------";
81 val thy = @{theory "Test"};
82 val fmz = ["realTestGiven (((1+2)*4/3) \<up> 2)", "realTestFind s"];
84 ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
86 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
87 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
88 (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) \<up> #2)")*)
89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
90 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
92 (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
93 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
94 (*nxt = ("Specify_Problem",Specify_Problem ["calculate", "test"])*)
95 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
96 (*nxt = ("Specify_Method",Specify_Method ("Test", "test_calculate"))*)
97 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
98 (*nxt = ("Apply_Method",Apply_Method ("Test", "test_calculate"))*)
100 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "PLUS")*)
101 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "TIMES")*)
102 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "DIVIDE")*)
103 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "POWER")*)
104 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Check_Postcond",Check_Postcond ["calculate", "test"])*)
105 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("End_Proof'",End_Proof')*)
106 case f of Test_Out.FormKF "16" => () | _ =>
107 error "evaluate.sml: script test_calculate changed behaviour";
110 "----------- calculate check test-root-equ --------------";
111 "----------- calculate check test-root-equ --------------";
112 "----------- calculate check test-root-equ --------------";
113 (*(1): 2nd Test_simplify didn't work:
115 "sqrt (x \<up> 2 + -3 * x) = (-3 + 2 * x + - 1 * (9 + 4 * x)) / (- 1 * 2)"
116 > val rls = ("Test_simplify");
117 > val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
118 val ct = "sqrt (x \<up> 2 + -3 * x) =
119 (-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))";
120 ie. cancel does not work properly
122 val thy = @{theory "Test"};
123 val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
125 "sqrt (x \<up> 2 + -3 * x) = (-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))"};
126 case calculate_ ctxt op_ ct of
128 | NONE => error "calculate_ test-root-equ changed";
130 sqrt (x \<up> 2 + -3 * x) =\
131 \(-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))
132 ............... does not work *)
134 (*--------------(2): does divide work in Test_simplify ?: ------*)
135 val thy = @{theory Test};
136 val ctxt = (ThyC.id_to_ctxt "Test")
137 val t = TermC.parseNEW' ctxt "6 / 2";
138 val rls = Test_simplify;
139 val (t,_) = the (rewrite_set_ ctxt false rls t);
140 (*val t = Free ("3", "Real.real") : term*)
142 (*--------------(3): is_num works ?: -------------------------------------*)
143 val t = TermC.parseNEW' ctxt "2 is_num";
145 rewrite_set_ ctxt false tval_rls t;
146 (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
148 val t = TermC.str2term "2 * x is_num";
149 val NONE = eval_is_num "" "" t (@{theory "Isac_Knowledge"});
152 "----------- check calculate bottom up ------------------";
153 "----------- check calculate bottom up ------------------";
154 "----------- check calculate bottom up ------------------";
155 (*-------------- eval_cancel works: *)
156 val thy = @{theory Test};
157 val rls = Test_simplify;
158 val t = TermC.parseNEW' ctxt "(-4) / 2";
160 val SOME (_, t) = eval_cancel "xxx" \<^const_name>\<open>divide\<close> t thy;
162 (*--------------(5): reproduce (1) with simpler term: ------------*)
163 val t = TermC.parseNEW' ctxt "(3+5)/(2::real)";
164 case rewrite_set_ ctxt false rls t of
166 if UnparseC.term t' = "4" then ()
167 else error "rewrite_set_ (3+5)/2 changed 1"
168 | _ => error "rewrite_set_ (3+5)/2 changed 2";
170 val t = TermC.parseNEW' ctxt "(3+1+2*x)/(2::real)";
171 case rewrite_set_ ctxt false rls t of
173 if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
174 | _ => error "rewrite_set_ (3+1+2*x)/2 changed 2";
176 (*--- trace_rewrite before correction of ... --------------------
177 val ct = "(-3 + 2 * x + - 1) / 2";
178 val (ct,_) = the (rewrite_set thy' false rls ct);
180 ### trying thm 'root_ge0_2'
181 ### rewrite_set_: x + (- 1 + -3) / 2
182 ### trying thm 'radd_real_const_eq'
183 ### trying thm 'radd_real_const'
184 ### rewrite_set_: x + (-4) / 2
185 ### trying thm 'rcollect_right'
188 -------------------------------------while before Isabelle20002:
189 val ct = "(#-3 + #2 * x + #- 1) // #2";
190 val (ct,_) = the (rewrite_set thy' false rls ct);
192 ### trying thm 'root_ge0_2'
193 ### rewrite_set_: x + (#- 1 + #-3) // #2
194 ### trying thm 'radd_real_const_eq'
195 ### trying thm 'radd_real_const'
196 ### rewrite_set_: x + #-4 // #2
197 ### rewrite_set_: x + #- 2
198 ### trying thm 'rcollect_right'
201 -----------------------------------------------------------------*)
204 (*===================*)
205 val t = TermC.parseNEW' ctxt "x + (- 1 + -3) / (2::real)";
206 val SOME (res, []) = rewrite_set_ ctxt false rls t;
207 if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_ x + (- 1 + -3) / 2 changed";
210 ### trying calc. 'cancel'
211 @@@ get_pair: binop, t = x + (-4) / 2
213 @@@ get_pair: t else -> NONE
214 @@@ get_pair: binop, t = (-4) / 2
216 @@@ get_pair: t -> NONE
217 @@@ get_pair: t1 -> NONE
219 ### trying calc. 'pow'
222 " ================= evaluate.sml: calculate_ 2002 =================== ";
223 " ================= evaluate.sml: calculate_ 2002 =================== ";
224 " ================= evaluate.sml: calculate_ 2002 =================== ";
226 val thy = @{theory Test};
227 val t = TermC.parseNEW' ctxt "12 / 3";
228 val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
229 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
231 val thy = @{theory Test};
232 val t = TermC.parseNEW' ctxt "4 \<up> 2";
233 val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
234 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
237 val t = TermC.parseNEW' ctxt "((1 + 2) * 4 / 3) \<up> 2";
238 val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
240 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
242 "(3 * 4 / 3) \<up> 2";
243 val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
245 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
248 val SOME (thmID,thm) =adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
250 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
253 val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
255 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
258 if it <> "16" then error "evaluate.sml: new behaviour in calculate_"
261 (*13.9.02 *** calc: operator = pow not defined*)
262 val t = TermC.parseNEW' ctxt "3 \<up> 2";
263 val SOME (thmID,thm) =
264 adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
265 (*** calc: operator = pow not defined*)
267 val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
269 val op_ = \<^const_name>\<open>realpow\<close> : string
270 val eval_fn = fn : string -> term -> theory -> (string * term) option*)
272 val SOME (thmid,t') = get_pair ctxt op_ eval_fn t;
273 (*** calc: operator = pow not defined*)
275 val SOME (id,t') = eval_fn op_ t ctxt;
276 (*** calc: operator = pow not defined*)
279 (\<^const_name>\<open>realpow\<close>,
280 Const (\<^const_name>\<open>realpow\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
281 (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
282 | _ => error "3 \<up> 2 CHANGED";
283 val SOME (id, t') = Calc_Binop.numeric thmid op_ t ctxt;
284 (*** calc: operator = pow not defined*)
286 if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop 3 \<up> 2 = 9 CHANGED";
289 "----------- fun cancel_int --------------------------------------------------------------------";
290 "----------- fun cancel_int --------------------------------------------------------------------";
291 "----------- fun cancel_int --------------------------------------------------------------------";
292 if cancel_int (~4, 2) = (~1, (2, 1)) then () else error "cancel_int (~4, 2) CHANGED";
293 if cancel_int (4, ~8) = (~1, (1, 2)) then () else error "cancel_int (4, ~8) CHANGED";
294 if cancel_int (6, 4) = (1, (3, 2)) then () else error "cancel_int (6, 4)CHANGED";
297 "----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
298 "----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
299 "----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
300 val t = @{term "2 + 3 ::real"};
302 "~~~~~ fun Calc_Binop.simplify , args:"; val (thy, lhs) = (@{theory}, t);
304 Proof_Context.init_global thy
305 |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
306 val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);
308 if ThmC.string_of_thm eq = "2 + 3 \<equiv> 5" then () else error "calcul 1";
310 val rhs = Thm.term_of (Thm.rhs_of eq);
311 val _ = \<^assert> (is_num rhs);
313 (*return value*) rhs;
314 if TermC.to_string rhs = "5" then () else error "calcul 2";
317 "----------- get_pair with 3 args --------------------------------";
318 "----------- get_pair with 3 args --------------------------------";
319 "----------- get_pair with 3 args --------------------------------";
320 val (thy, op_, ef, arg) =
321 (thy, "EqSystem.occur_exactly_in",
322 get_calc (@{theory "EqSystem"} |> Proof_Context.init_global) "occur_exactly_in" |> snd |> snd,
324 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2"
326 val SOME (str, simpl) = get_pair ctxt op_ ef arg;
328 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2 = True"
329 then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in";
332 "----------- calculate (2 * x is_num) -------------------";
333 "----------- calculate (2 * x is_num) -------------------";
334 "----------- calculate (2 * x is_num) -------------------";
335 val t = TermC.str2term "(2::real) * x is_num";
337 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t @{theory Test};
338 if UnparseC.term t' = "(2 * x is_num) = False" then ()
339 else error "is_num 2 * x is_num CHANGED";
341 val SOME (t',_) = rewrite_set_ ctxt false tval_rls t;
342 if UnparseC.term t' = "False" then ()
343 else error "rewrite_set_ 2 * x is_num CHANGED";
345 "----------- fun get_pair: examples ------------------------------------------------------------";
346 "----------- fun get_pair: examples ------------------------------------------------------------";
347 "----------- fun get_pair: examples ------------------------------------------------------------";
349 val ctxt = @{context};
350 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
351 if isa_str = "Groups.plus_class.plus" then () else error "eval_fn PLUS changed";
353 val t = @{term "3 + 4 :: real"};
354 val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
355 (*+*)if str = "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7"
356 (*+*)then () else error "get_pair 3 + 4 changed";
358 val t = @{term "(a + 3) + 4 :: real"};
359 val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
360 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
361 then () else error "get_pair (a + 3) + 4 changed";
363 val t = @{term "(a + 3) + 4 :: real"};
364 val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
365 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
366 then () else error "get_pair (a + 3) + 4 changed";
368 val t = @{term "x = 5 * (3 + (4 + a) :: real)"};
369 val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
370 if str = "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a"
371 then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed";
373 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
375 val t = @{term "-4 / - 2 :: real"};
376 val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
377 if str = "#divide_e~4_~2" andalso UnparseC.term term = "- 4 / - 2 = 2"
378 then () else error "get_pair -4 / - 2 changed";
380 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
382 val t = @{term "2 \<up> 3 :: real"};
383 val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
384 if str = "#: 2 \<up> 3 = 8" andalso UnparseC.term term = "2 \<up> 3 = 8"
385 then () else error "get_pair 2 \<up> 3 changed";
387 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
388 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
389 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
390 (*--------------------------------------------------------------------vvvvvvvvvv*)
391 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_num");
392 val t = @{term "9 is_num"};
393 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
394 if str = "#is_num_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_num) = True"
395 then () else error "adhoc_thm 9 is_num changed";
397 case get_calc_prog_id ctxt \<^const_name>\<open>less\<close> of
398 "le" => () | _ => error "Orderings.ord_class.less <-> le changed";
399 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le");
400 if isa_str = "Orderings.ord_class.less" then () else error "adhoc_thm (4 < 4) = False CHANGED";
402 val t = @{term "4 < (4 :: real)"};
403 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
404 if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"
405 then () else error "adhoc_thm 4 < 4 changed";
407 val SOME t = parseNEW @{context} "a < 4";
408 case adhoc_thm ctxt (isa_str, eval_fn) t of
409 NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE";
411 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
412 val SOME t = parseNEW @{context} "1 + (2::real)";
413 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
414 if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
415 then () else error "adhoc_thm 1 + 2 changed";
417 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
418 val t = @{term "6 / -8 :: real"};
419 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
420 if str = "#divide_e6_~8" andalso ThmC_Def.string_of_thm thm = "6 / - 8 = - 3 / 4"
421 then () else error "adhoc_thm 6 / -8 = - 3 / 4 changed";
423 case get_calc_prog_id ctxt "Prog_Expr.ident" of
424 "ident" => () | _ => error "Prog_Expr.ident <-> ident changed";
425 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");
427 val t = @{term "3 =!= (3 :: real)"};
428 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
429 if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"
430 then () else error "adhoc_thm (3 =!= 3) changed";
432 val t = @{term "\<not> ((4 :: real) + (4 * x + x \<up> 2) =!= 0)"};
433 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
434 if str = "#ident_(4 + (4 * x + x \<up> 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x \<up> 2) =!= 0) = False"
435 then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
437 "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
438 "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
439 "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
440 val eval_ = ("Rings.divide_class.divide", eval_cancel "#divide_e" : Eval.ml_fun): Eval.ml;
441 val t = @{term "- 1 / 2 ::real"};
443 ML\<open>Eval.adhoc_thm\<close> is called while searching terms for adjacent numerals
444 given a certain ML_type\<open>eval_fn\<close> and a certain ML\<open>term\<close> ..
448 Eval.get_pair for \<^const_name>\<open>divide\<close> \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2")
449 but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE
451 STEP-INTO BEVORE REMOVING THE ERROR:
452 val SOME ("#divide_e~1_2", adhoc_thm) =
453 Eval.adhoc_thm @{context} eval_ t;
454 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
456 ("#divide_e~1_2", t'') =
457 (*case*) get_pair ctxt op_ eval_fn t (*of*);
459 get_pair finds two adjacent numerals and does NOT distinguish between different kinds of
460 \<^ML_type>\<open>eval_fn\<close>. In case of \<^ML>\<open>eval_cancel\<close> the return value WAS the same as the input..
462 (*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2"
465 val NONE = adhoc_thm @{context} eval_ t;
466 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
468 (*case*) get_pair ctxt op_ eval_fn t (*of*);
471 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
472 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
473 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
474 val t = TermC.str2term "sqrt 4";
475 Eval.adhoc_thm @{context} ("NthRoot.sqrt", eval_sqrt "#sqrt_") t;
477 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
478 ((ThyC.get_theory "Isac_Knowledge"),
479 ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> Proof.context -> (string * term) option), t);
481 val SOME (thmid, t) =
482 (*case*) get_pair ctxt op_ eval_fn ct (*of*);
483 (*+*)val "sqrt 4 = 2" = UnparseC.term t;
486 Skip_Proof.make_thm thy t;
488 exception TYPE raised (line 169 of "consts.ML"): Illegal type
489 for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
492 "----------- fun power -------------------------------------------------------------------------";
493 "----------- fun power -------------------------------------------------------------------------";
494 "----------- fun power -------------------------------------------------------------------------";
495 if power 2 3 = 8 then () else error "power 2 3 = 8";
496 if power ~2 3 = ~8 then () else error "power ~2 3 = ~8";
497 if power ~3 2 = 9 then () else error "power ~3 2 = 9";
498 case \<^try>\<open> power 3 ~2 \<close> of
499 SOME _ => raise error "power 3 ~2: should raise an exn 1"
502 "----------- fun divisors ----------------------------------------------------------------------";
503 "----------- fun divisors ----------------------------------------------------------------------";
504 "----------- fun divisors ----------------------------------------------------------------------";
505 if divisors 30 = [5, 3, 2] then () else error "divisors 30 = [5, 3, 2]";
506 if divisors 32 = [2, 2, 2, 2, 2] then () else error "divisors 32 = [2, 2, 2, 2, 2]";
507 if divisors 60 = [5, 3, 2, 2] then () else error "divisors 60 = [5, 3, 2, 2]";
508 if divisors 11 = [11] then () else error "divisors 11 = [11]";
510 "----------- fun doubles, fun squfact ----------------------------------------------------------";
511 "----------- fun doubles, fun squfact ----------------------------------------------------------";
512 "----------- fun doubles, fun squfact ----------------------------------------------------------";
513 if doubles [2,3,4] = [] then () else error "doubles [2,3,4] changed";
514 if doubles [2,3,3,5,5,7] = [5, 3] then () else error "doubles [2,3,3,5,5,7] changed";
516 if squfact 30 = 1 then () else error "squfact 30 changed";
517 if squfact 32 = 4 then () else error "squfact 32 changed";
518 if squfact 60 = 2 then () else error "squfact 60 changed";
519 if squfact 11 = 1 then () else error "squfact 11 changed";