1 (* Title: "ProgLang/calculate.sml" |
|
2 test calculation of values for function constants |
|
3 Author: Walther Neuper 2000 |
|
4 (c) copyright due to lincense terms. |
|
5 *) |
|
6 |
|
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 calcul,ate bottom up -----------------"; |
|
18 "----------- Prog_Expr.pow Power.power_class.power ---------"; |
|
19 " ================= calculate.sml: calculate_ 2002 ======"; |
|
20 "----------- get_pair with 3 args -----------------------"; |
|
21 "----------- calculate (2 * x is_const) -----------------"; |
|
22 "----------- fun get_pair: examples ------------------------------------------------------------"; |
|
23 "----------- fun adhoc_thm: examples -----------------------------------------------------------"; |
|
24 "----------- fun power -------------------------------------------------------------------------"; |
|
25 "----------- fun divisors ----------------------------------------------------------------------"; |
|
26 "----------- fun doubles, fun squfact ----------------------------------------------------------"; |
|
27 "--------------------------------------------------------"; |
|
28 "--------------------------------------------------------"; |
|
29 "--------------------------------------------------------"; |
|
30 |
|
31 "----------- check return value of adhoc_thm ----"; |
|
32 "----------- check return value of adhoc_thm ----"; |
|
33 "----------- check return value of adhoc_thm ----"; |
|
34 val thy = @{theory "Poly"}; |
|
35 val cal = snd (assoc_calc' thy "is_polyexp"); |
|
36 val t = @{term "(x / x) is_polyexp"}; |
|
37 val SOME (thmID, thm) = adhoc_thm thy cal t; |
|
38 (HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop") |
|
39 handle TERM _ => |
|
40 error "calculate.sml: adhoc_thm must return Trueprop"; |
|
41 |
|
42 "----------- fun calculate_ --------------------------------------------------------------------"; |
|
43 "----------- fun calculate_ --------------------------------------------------------------------"; |
|
44 "----------- fun calculate_ --------------------------------------------------------------------"; |
|
45 (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *) |
|
46 val t = str2term "((1+2)*4/3)^^^2"; |
|
47 val thy = @{theory}; |
|
48 val times = ("Groups.times_class.times", eval_binop "#mult_") : string * Exec_Def.eval_fn; |
|
49 val plus = ("Groups.plus_class.plus",eval_binop "#add_") : string * Exec_Def.eval_fn; |
|
50 val divide = ("Rings.divide_class.divide" ,eval_cancel "#divide_e") : string * Exec_Def.eval_fn; |
|
51 val pow = ("Prog_Expr.pow" ,eval_binop "#power_") : string * Exec_Def.eval_fn; |
|
52 |
|
53 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t); |
|
54 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t; |
|
55 val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t; |
|
56 if UnparseC.term t' = "(3 * 4 / 3) ^^^ 2" then () else error "calculate_ 1 + 2 = 3 changed"; |
|
57 |
|
58 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t'); |
|
59 val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t'; |
|
60 val SOME (t'', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t; |
|
61 if UnparseC.term t'' = "(12 / 3) ^^^ 2" then () else error "calculate_ 3 * 4 = 12 changed"; |
|
62 |
|
63 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t''); |
|
64 val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t; |
|
65 val SOME (t''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t; |
|
66 if UnparseC.term t''' = "4 ^^^ 2" then () else error "calculate_ 12 / 3 = 4 changed"; |
|
67 |
|
68 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t'''); |
|
69 val SOME ("#: 4 ^^^ 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t; |
|
70 val SOME (t'''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t; |
|
71 if UnparseC.term t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed"; |
|
72 |
|
73 "----------- calculate from Prog --------------------------------- -----------------------------"; |
|
74 "----------- calculate from Prog --------------------------------- -----------------------------"; |
|
75 "----------- calculate from Prog --------------------------------- -----------------------------"; |
|
76 val thy = @{theory "Test"}; |
|
77 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"]; |
|
78 val (dI',pI',mI') = |
|
79 ("Test",["calculate","test"],["Test","test_calculate"]); |
|
80 |
|
81 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
82 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
83 (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*) |
|
84 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
85 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*) |
|
86 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
87 (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*) |
|
88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
89 (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*) |
|
90 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
91 (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*) |
|
92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
93 (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*) |
|
94 |
|
95 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "PLUS")*) |
|
96 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "TIMES")*) |
|
97 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "DIVIDE")*) |
|
98 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "POWER")*) |
|
99 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*) |
|
100 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("End_Proof'",End_Proof')*) |
|
101 case f of FormKF "16" => () | _ => |
|
102 error "calculate.sml: script test_calculate changed behaviour"; |
|
103 |
|
104 |
|
105 "----------- calculate check test-root-equ --------------"; |
|
106 "----------- calculate check test-root-equ --------------"; |
|
107 "----------- calculate check test-root-equ --------------"; |
|
108 (*(1): 2nd Test_simplify didn't work: |
|
109 val ct = |
|
110 "sqrt (x ^^^ 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)" |
|
111 > val rls = ("Test_simplify"); |
|
112 > val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct); |
|
113 val ct = "sqrt (x ^^^ 2 + -3 * x) = |
|
114 (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"; |
|
115 ie. cancel does not work properly |
|
116 *) |
|
117 val thy = @{theory "Test"}; |
|
118 val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE")); |
|
119 val ct = ThmC_Def.num_to_Free @{term |
|
120 "sqrt (x ^^^ 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"}; |
|
121 case calculate_ thy op_ ct of |
|
122 SOME _ => () |
|
123 | NONE => error "calculate_ test-root-equ changed"; |
|
124 (* |
|
125 sqrt (x ^^^ 2 + -3 * x) =\ |
|
126 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2)))) |
|
127 ............... does not work *) |
|
128 |
|
129 (*--------------(2): does divide work in Test_simplify ?: ------*) |
|
130 val thy = @{theory Test}; |
|
131 val t = (Thm.term_of o the o (parse thy)) "6 / 2"; |
|
132 val rls = Test_simplify; |
|
133 val (t,_) = the (rewrite_set_ thy false rls t); |
|
134 (*val t = Free ("3","Real.real") : term*) |
|
135 |
|
136 (*--------------(3): is_const works ?: -------------------------------------*) |
|
137 val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const"; |
|
138 atomty t; |
|
139 rewrite_set_ @{theory Test} false tval_rls t; |
|
140 (*val it = SOME (Const ("HOL.True","bool"),[]) ... works*) |
|
141 |
|
142 val t = str2term "2 * x is_const"; |
|
143 val SOME (str,t') = eval_const "" "" t (@{theory "Isac_Knowledge"}); |
|
144 UnparseC.term t'; |
|
145 |
|
146 |
|
147 "----------- check calculate bottom up ------------------"; |
|
148 "----------- check calculate bottom up ------------------"; |
|
149 "----------- check calculate bottom up ------------------"; |
|
150 (*-------------- eval_cancel works: *) |
|
151 Rewrite.trace_on := false; |
|
152 val thy = @{theory Test}; |
|
153 val rls = Test_simplify; |
|
154 val t = (Thm.term_of o the o (parse thy)) "(-4) / 2"; |
|
155 |
|
156 val SOME (_, t) = eval_cancel "xxx" "Rings.divide_class.divide" t thy; |
|
157 |
|
158 (*--------------(5): reproduce (1) with simpler term: ------------*) |
|
159 val t = (Thm.term_of o the o (parse thy)) "(3+5)/2"; |
|
160 case rewrite_set_ thy false rls t of |
|
161 SOME (Free ("4", _), []) => () |
|
162 | _ => error "rewrite_set_ (3+5)/2 changed"; |
|
163 |
|
164 val t = (Thm.term_of o the o (parse thy)) "(3+1+2*x)/2"; |
|
165 case rewrite_set_ thy false rls t of |
|
166 SOME (Const ("Groups.plus_class.plus", _) $ Free ("2", _) $ Free ("x", _), []) => () |
|
167 | _ => error "rewrite_set_ (3+1+2*x)/2 changed"; |
|
168 |
|
169 Rewrite.trace_on:=false; (*=true3.6.03*) |
|
170 |
|
171 (*--- Rewrite.trace_on before correction of ... -------------------- |
|
172 val ct = "(-3 + 2 * x + -1) / 2"; |
|
173 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
174 : |
|
175 ### trying thm 'root_ge0_2' |
|
176 ### rewrite_set_: x + (-1 + -3) / 2 |
|
177 ### trying thm 'radd_real_const_eq' |
|
178 ### trying thm 'radd_real_const' |
|
179 ### rewrite_set_: x + (-4) / 2 |
|
180 ### trying thm 'rcollect_right' |
|
181 : |
|
182 "x + (-4) / 2" |
|
183 -------------------------------------while before Isabelle20002: |
|
184 val ct = "(#-3 + #2 * x + #-1) // #2"; |
|
185 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
186 : |
|
187 ### trying thm 'root_ge0_2' |
|
188 ### rewrite_set_: x + (#-1 + #-3) // #2 |
|
189 ### trying thm 'radd_real_const_eq' |
|
190 ### trying thm 'radd_real_const' |
|
191 ### rewrite_set_: x + #-4 // #2 |
|
192 ### rewrite_set_: x + #-2 |
|
193 ### trying thm 'rcollect_right' |
|
194 : |
|
195 "#-2 + x" |
|
196 -----------------------------------------------------------------*) |
|
197 |
|
198 |
|
199 (*===================*) |
|
200 Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*) |
|
201 val t = (Thm.term_of o the o (parse thy)) "x + (-1 + -3) / 2"; |
|
202 val SOME (res, []) = rewrite_set_ thy false rls t; |
|
203 if UnparseC.term res = "-2 + x" then () else error "rewrite_set_ x + (-1 + -3) / 2 changed"; |
|
204 "x + (-4) / 2"; |
|
205 (* |
|
206 ### trying calc. 'cancel' |
|
207 @@@ get_pair: binop, t = x + (-4) / 2 |
|
208 @@@ get_pair: t else |
|
209 @@@ get_pair: t else -> NONE |
|
210 @@@ get_pair: binop, t = (-4) / 2 |
|
211 @@@ get_pair: then 1 |
|
212 @@@ get_pair: t -> NONE |
|
213 @@@ get_pair: t1 -> NONE |
|
214 @@@ adhoc_thm': NONE |
|
215 ### trying calc. 'pow' |
|
216 *) |
|
217 |
|
218 Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*) |
|
219 |
|
220 "----------- Prog_Expr.pow Power.power_class.power ---------"; |
|
221 "----------- Prog_Expr.pow Power.power_class.power ---------"; |
|
222 "----------- Prog_Expr.pow Power.power_class.power ---------"; |
|
223 val t = (Thm.term_of o the o (parseold thy)) "1 ^ aaa"; |
|
224 atomty t; |
|
225 (*** ------------- |
|
226 *** Const ( Nat.power, ['a, nat] => 'a) |
|
227 *** . Free ( 1, 'a) |
|
228 *** . Free ( aaa, nat) *) |
|
229 |
|
230 val t = str2term "1 ^^^ aaa"; |
|
231 atomty t; |
|
232 (**** |
|
233 *** Const (Prog_Expr.pow, real => real => real) |
|
234 *** . Free (1, real) |
|
235 *** . Free (aaa, real) |
|
236 *** *); |
|
237 |
|
238 " ================= calculate.sml: calculate_ 2002 =================== "; |
|
239 " ================= calculate.sml: calculate_ 2002 =================== "; |
|
240 " ================= calculate.sml: calculate_ 2002 =================== "; |
|
241 |
|
242 val thy = @{theory Test}; |
|
243 val t = (Thm.term_of o the o (parse thy)) "12 / 3"; |
|
244 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t; |
|
245 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
|
246 "12 / 3 = 4"; |
|
247 val thy = @{theory Test}; |
|
248 val t = (Thm.term_of o the o (parse thy)) "4 ^^^ 2"; |
|
249 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t; |
|
250 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
|
251 "4 ^ 2 = 16"; |
|
252 |
|
253 val t = (Thm.term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2"; |
|
254 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t; |
|
255 "1 + 2 = 3"; |
|
256 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
|
257 UnparseC.term t; |
|
258 "(3 * 4 / 3) ^^^ 2"; |
|
259 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t; |
|
260 "3 * 4 = 12"; |
|
261 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
|
262 UnparseC.term t; |
|
263 "(12 / 3) ^^^ 2"; |
|
264 val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t; |
|
265 "12 / 3 = 4"; |
|
266 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
|
267 UnparseC.term t; |
|
268 "4 ^^^ 2"; |
|
269 val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t; |
|
270 "4 ^^^ 2 = 16"; |
|
271 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
|
272 UnparseC.term t; |
|
273 "16"; |
|
274 if it <> "16" then error "calculate.sml: new behaviour in calculate_" |
|
275 else (); |
|
276 |
|
277 (*13.9.02 *** calc: operator = pow not defined*) |
|
278 val t = (Thm.term_of o the o (parse thy)) "3^^^2"; |
|
279 val SOME (thmID,thm) = |
|
280 adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t; |
|
281 (*** calc: operator = pow not defined*) |
|
282 |
|
283 val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")); |
|
284 (* |
|
285 val op_ = "Prog_Expr.pow" : string |
|
286 val eval_fn = fn : string -> term -> theory -> (string * term) option*) |
|
287 |
|
288 val SOME (thmid,t') = get_pair thy op_ eval_fn t; |
|
289 (*** calc: operator = pow not defined*) |
|
290 |
|
291 val SOME (id,t') = eval_fn op_ t thy; |
|
292 (*** calc: operator = pow not defined*) |
|
293 |
|
294 val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t); |
|
295 val SOME (id,t') = eval_binop thmid op_ t thy; |
|
296 (*** calc: operator = pow not defined*) |
|
297 |
|
298 |
|
299 "----------- get_pair with 3 args --------------------------------"; |
|
300 "----------- get_pair with 3 args --------------------------------"; |
|
301 "----------- get_pair with 3 args --------------------------------"; |
|
302 val (thy, op_, ef, arg) = |
|
303 (thy, "EqSystem.occur'_exactly'_in", |
|
304 assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd, |
|
305 str2term |
|
306 "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2" |
|
307 ); |
|
308 val SOME (str, simpl) = get_pair thy op_ ef arg; |
|
309 if str = |
|
310 "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True" |
|
311 then () else error "calculate.sml get_pair with 3 args:occur_exactly_in"; |
|
312 |
|
313 |
|
314 "----------- calculate (2 * x is_const) -----------------"; |
|
315 "----------- calculate (2 * x is_const) -----------------"; |
|
316 "----------- calculate (2 * x is_const) -----------------"; |
|
317 val t = str2term "2 * x is_const"; |
|
318 val SOME (str, t') = eval_const "" "" t @{theory Test}; |
|
319 UnparseC.term t'; |
|
320 "(2 * x is_const) = False"; |
|
321 |
|
322 val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t; |
|
323 UnparseC.term t'; |
|
324 "HOL.False"; |
|
325 |
|
326 "----------- fun get_pair: examples ------------------------------------------------------------"; |
|
327 "----------- fun get_pair: examples ------------------------------------------------------------"; |
|
328 "----------- fun get_pair: examples ------------------------------------------------------------"; |
|
329 val thy = @{theory}; |
|
330 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS"); |
|
331 |
|
332 val t = (Thm.term_of o the o (parse thy)) "3 + 4"; |
|
333 val SOME (str, term) = get_pair thy isa_str eval_fn t; |
|
334 if str = "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7" |
|
335 then () else error "get_pair 3 + 4 changed"; |
|
336 |
|
337 val t = (Thm.term_of o the o (parse thy)) "(a + 3) + 4"; |
|
338 val SOME (str, term) = get_pair thy isa_str eval_fn t; |
|
339 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7" |
|
340 then () else error "get_pair (a + 3) + 4 changed"; |
|
341 |
|
342 val t = (Thm.term_of o the o (parse thy)) "(a + 3) + 4"; |
|
343 val SOME (str, term) = get_pair thy isa_str eval_fn t; |
|
344 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7" |
|
345 then () else error "get_pair (a + 3) + 4 changed"; |
|
346 |
|
347 val t = (Thm.term_of o the o (parse thy)) "x = 5 * (3 + (4 + a))"; |
|
348 val SOME (str, term) = get_pair thy isa_str eval_fn t; |
|
349 if str = "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a" |
|
350 then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed"; |
|
351 |
|
352 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"); |
|
353 |
|
354 val t = (Thm.term_of o the o (parse thy)) "-4 / -2"; |
|
355 val SOME (str, term) = get_pair thy isa_str eval_fn t; |
|
356 if str = "#divide_e-4_-2" andalso UnparseC.term term = "-4 / -2 = 2" |
|
357 then () else error "get_pair -4 / -2 changed"; |
|
358 |
|
359 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER"); |
|
360 |
|
361 val t = (Thm.term_of o the o (parse thy)) "2 ^^^ 3"; |
|
362 val SOME (str, term) = get_pair thy isa_str eval_fn t; |
|
363 if str = "#: 2 ^^^ 3 = 8" andalso UnparseC.term term = "2 ^^^ 3 = 8" |
|
364 then () else error "get_pair 2 ^^^ 3 changed"; |
|
365 |
|
366 "----------- fun adhoc_thm: examples -----------------------------------------------------------"; |
|
367 "----------- fun adhoc_thm: examples -----------------------------------------------------------"; |
|
368 "----------- fun adhoc_thm: examples -----------------------------------------------------------"; |
|
369 (*--------------------------------------------------------------------vvvvvvvvvv*) |
|
370 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_const"); |
|
371 val SOME t = parseNEW @{context} "9 is_const"; |
|
372 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t; |
|
373 if str = "#is_const_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_const) = True" |
|
374 then () else error "adhoc_thm 9 is_const changed"; |
|
375 |
|
376 |
|
377 case assoc_calc thy "Orderings.ord_class.less" of |
|
378 "le" => () | _ => error "Orderings.ord_class.less <-> le changed"; |
|
379 (*--------------------------------------------------------------------vvvvvvvvvv*) |
|
380 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le"); |
|
381 |
|
382 val SOME t = parseNEW @{context} "4 < 4"; |
|
383 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t; |
|
384 if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False" |
|
385 then () else error "adhoc_thm 4 < 4 changed"; |
|
386 |
|
387 val SOME t = parseNEW @{context} "a < 4"; |
|
388 case adhoc_thm thy (isa_str, eval_fn) t of |
|
389 NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE"; |
|
390 |
|
391 |
|
392 (*--------------------------------------------------------------------vvvvvvvvvv*) |
|
393 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS"); |
|
394 val SOME t = parseNEW @{context} "1 + 2"; |
|
395 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t; |
|
396 if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3" |
|
397 then () else error "adhoc_thm 1 + 2 changed"; |
|
398 |
|
399 (*--------------------------------------------------------------------vvvvvvvvvv*) |
|
400 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"); |
|
401 val SOME t = parseNEW @{context} "6 / -8"; |
|
402 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t; |
|
403 if str = "#divide_e6_-8" andalso ThmC_Def.string_of_thm thm = "6 / -8 = -3 / 4" |
|
404 then () else error "adhoc_thm 1 + 2 changed"; |
|
405 |
|
406 |
|
407 case assoc_calc thy "Prog_Expr.ident" of |
|
408 "ident" => () | _ => error "Prog_Expr.ident <-> ident changed"; |
|
409 (*--------------------------------------------------------------------vvvvvvvvvv*) |
|
410 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident"); |
|
411 |
|
412 val SOME t = parseNEW @{context} "3 =!= 3"; |
|
413 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t; |
|
414 if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True" |
|
415 then () else error "adhoc_thm (3 =!= 3) changed"; |
|
416 |
|
417 val SOME t = parseNEW @{context} "\<not> (4 + (4 * x + x ^ 2) =!= 0)"; |
|
418 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t; |
|
419 if str = "#ident_(4 + (4 * x + x ^ 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x ^ 2) =!= 0) = False" |
|
420 then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed"; |
|
421 |
|
422 "----------- fun power -------------------------------------------------------------------------"; |
|
423 "----------- fun power -------------------------------------------------------------------------"; |
|
424 "----------- fun power -------------------------------------------------------------------------"; |
|
425 if power 2 3 = 8 then () else error "power 2 3 = 8"; |
|
426 if power ~2 3 = ~8 then () else error "power ~2 3 = ~8"; |
|
427 if power ~3 2 = 9 then () else error "power ~3 2 = 9"; |
|
428 (power 3 ~2; error "power 3 ~2: should raise an exn") handle _ => 000; |
|
429 |
|
430 "----------- fun divisors ----------------------------------------------------------------------"; |
|
431 "----------- fun divisors ----------------------------------------------------------------------"; |
|
432 "----------- fun divisors ----------------------------------------------------------------------"; |
|
433 if divisors 30 = [5, 3, 2] then () else error "divisors 30 = [5, 3, 2]"; |
|
434 if divisors 32 = [2, 2, 2, 2, 2] then () else error "divisors 32 = [2, 2, 2, 2, 2]"; |
|
435 if divisors 60 = [5, 3, 2, 2] then () else error "divisors 60 = [5, 3, 2, 2]"; |
|
436 if divisors 11 = [11] then () else error "divisors 11 = [11]"; |
|
437 |
|
438 "----------- fun doubles, fun squfact ----------------------------------------------------------"; |
|
439 "----------- fun doubles, fun squfact ----------------------------------------------------------"; |
|
440 "----------- fun doubles, fun squfact ----------------------------------------------------------"; |
|
441 if doubles [2,3,4] = [] then () else error "doubles [2,3,4] changed"; |
|
442 if doubles [2,3,3,5,5,7] = [5, 3] then () else error "doubles [2,3,3,5,5,7] changed"; |
|
443 |
|
444 if squfact 30 = 1 then () else error "squfact 30 changed"; |
|
445 if squfact 32 = 4 then () else error "squfact 32 changed"; |
|
446 if squfact 60 = 2 then () else error "squfact 60 changed"; |
|
447 if squfact 11 = 1 then () else error "squfact 11 changed"; |
|