266 val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")); |
266 val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")); |
267 (* |
267 (* |
268 val op_ = \<^const_name>\<open>realpow\<close> : string |
268 val op_ = \<^const_name>\<open>realpow\<close> : string |
269 val eval_fn = fn : string -> term -> theory -> (string * term) option*) |
269 val eval_fn = fn : string -> term -> theory -> (string * term) option*) |
270 |
270 |
271 val SOME (thmid,t') = get_pair thy op_ eval_fn t; |
271 val SOME (thmid,t') = get_pair ctxt op_ eval_fn t; |
272 (*** calc: operator = pow not defined*) |
272 (*** calc: operator = pow not defined*) |
273 |
273 |
274 val SOME (id,t') = eval_fn op_ t thy; |
274 val SOME (id,t') = eval_fn op_ t ctxt; |
275 (*** calc: operator = pow not defined*) |
275 (*** calc: operator = pow not defined*) |
276 |
276 |
277 case (op_, t) of |
277 case (op_, t) of |
278 (\<^const_name>\<open>realpow\<close>, |
278 (\<^const_name>\<open>realpow\<close>, |
279 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>, _))) $ |
279 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>, _))) $ |
280 (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => () |
280 (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => () |
281 | _ => error "3 \<up> 2 CHANGED"; |
281 | _ => error "3 \<up> 2 CHANGED"; |
282 val SOME (id, t') = eval_binop thmid op_ t thy; |
282 val SOME (id, t') = eval_binop thmid op_ t ctxt; |
283 (*** calc: operator = pow not defined*) |
283 (*** calc: operator = pow not defined*) |
284 |
284 |
285 if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop 3 \<up> 2 = 9 CHANGED"; |
285 if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop 3 \<up> 2 = 9 CHANGED"; |
286 |
286 |
287 |
287 |
320 (thy, "EqSystem.occur_exactly_in", |
320 (thy, "EqSystem.occur_exactly_in", |
321 assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd, |
321 assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd, |
322 TermC.str2term |
322 TermC.str2term |
323 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2" |
323 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2" |
324 ); |
324 ); |
325 val SOME (str, simpl) = get_pair thy op_ ef arg; |
325 val SOME (str, simpl) = get_pair ctxt op_ ef arg; |
326 if str = |
326 if str = |
327 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2 = True" |
327 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2 = True" |
328 then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in"; |
328 then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in"; |
329 |
329 |
330 |
330 |
347 val thy = @{theory}; |
347 val thy = @{theory}; |
348 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS"); |
348 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS"); |
349 if isa_str = "Groups.plus_class.plus" then () else error "eval_fn PLUS changed"; |
349 if isa_str = "Groups.plus_class.plus" then () else error "eval_fn PLUS changed"; |
350 |
350 |
351 val t = @{term "3 + 4 :: real"}; |
351 val t = @{term "3 + 4 :: real"}; |
352 val SOME (str, term) = get_pair thy isa_str eval_fn t; |
352 val SOME (str, term) = get_pair ctxt isa_str eval_fn t; |
353 (*+*)if str = "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7" |
353 (*+*)if str = "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7" |
354 (*+*)then () else error "get_pair 3 + 4 changed"; |
354 (*+*)then () else error "get_pair 3 + 4 changed"; |
355 |
355 |
356 val t = @{term "(a + 3) + 4 :: real"}; |
356 val t = @{term "(a + 3) + 4 :: real"}; |
357 val SOME (str, term) = get_pair thy isa_str eval_fn t; |
357 val SOME (str, term) = get_pair ctxt isa_str eval_fn t; |
358 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7" |
358 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7" |
359 then () else error "get_pair (a + 3) + 4 changed"; |
359 then () else error "get_pair (a + 3) + 4 changed"; |
360 |
360 |
361 val t = @{term "(a + 3) + 4 :: real"}; |
361 val t = @{term "(a + 3) + 4 :: real"}; |
362 val SOME (str, term) = get_pair thy isa_str eval_fn t; |
362 val SOME (str, term) = get_pair ctxt isa_str eval_fn t; |
363 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7" |
363 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7" |
364 then () else error "get_pair (a + 3) + 4 changed"; |
364 then () else error "get_pair (a + 3) + 4 changed"; |
365 |
365 |
366 val t = @{term "x = 5 * (3 + (4 + a) :: real)"}; |
366 val t = @{term "x = 5 * (3 + (4 + a) :: real)"}; |
367 val SOME (str, term) = get_pair thy isa_str eval_fn t; |
367 val SOME (str, term) = get_pair ctxt isa_str eval_fn t; |
368 if str = "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a" |
368 if str = "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a" |
369 then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed"; |
369 then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed"; |
370 |
370 |
371 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"); |
371 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"); |
372 |
372 |
373 val t = @{term "-4 / - 2 :: real"}; |
373 val t = @{term "-4 / - 2 :: real"}; |
374 val SOME (str, term) = get_pair thy isa_str eval_fn t; |
374 val SOME (str, term) = get_pair ctxt isa_str eval_fn t; |
375 if str = "#divide_e~4_~2" andalso UnparseC.term term = "- 4 / - 2 = 2" |
375 if str = "#divide_e~4_~2" andalso UnparseC.term term = "- 4 / - 2 = 2" |
376 then () else error "get_pair -4 / - 2 changed"; |
376 then () else error "get_pair -4 / - 2 changed"; |
377 |
377 |
378 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER"); |
378 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER"); |
379 |
379 |
380 val t = @{term "2 \<up> 3 :: real"}; |
380 val t = @{term "2 \<up> 3 :: real"}; |
381 val SOME (str, term) = get_pair thy isa_str eval_fn t; |
381 val SOME (str, term) = get_pair ctxt isa_str eval_fn t; |
382 if str = "#: 2 \<up> 3 = 8" andalso UnparseC.term term = "2 \<up> 3 = 8" |
382 if str = "#: 2 \<up> 3 = 8" andalso UnparseC.term term = "2 \<up> 3 = 8" |
383 then () else error "get_pair 2 \<up> 3 changed"; |
383 then () else error "get_pair 2 \<up> 3 changed"; |
384 |
384 |
385 "----------- fun adhoc_thm: examples -----------------------------------------------------------"; |
385 "----------- fun adhoc_thm: examples -----------------------------------------------------------"; |
386 "----------- fun adhoc_thm: examples -----------------------------------------------------------"; |
386 "----------- fun adhoc_thm: examples -----------------------------------------------------------"; |
450 val SOME ("#divide_e~1_2", adhoc_thm) = |
450 val SOME ("#divide_e~1_2", adhoc_thm) = |
451 Eval.adhoc_thm @{theory} eval_ t; |
451 Eval.adhoc_thm @{theory} eval_ t; |
452 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t); |
452 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t); |
453 val SOME |
453 val SOME |
454 ("#divide_e~1_2", t'') = |
454 ("#divide_e~1_2", t'') = |
455 (*case*) get_pair thy op_ eval_fn t (*of*); |
455 (*case*) get_pair ctxt op_ eval_fn t (*of*); |
456 (* |
456 (* |
457 get_pair finds two adjacent numerals and does NOT distinguish between different kinds of |
457 get_pair finds two adjacent numerals and does NOT distinguish between different kinds of |
458 \<^ML_type>\<open>eval_fn\<close>. In case of \<^ML>\<open>eval_cancel\<close> the return value WAS the same as the input.. |
458 \<^ML_type>\<open>eval_fn\<close>. In case of \<^ML>\<open>eval_cancel\<close> the return value WAS the same as the input.. |
459 *) |
459 *) |
460 (*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2" |
460 (*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2" |
461 *) |
461 *) |
462 |
462 |
463 val NONE = adhoc_thm @{theory} eval_ t; |
463 val NONE = adhoc_thm @{theory} eval_ t; |
464 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t); |
464 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t); |
465 val NONE = |
465 val NONE = |
466 (*case*) get_pair thy op_ eval_fn t (*of*); |
466 (*case*) get_pair ctxt op_ eval_fn t (*of*); |
467 |
467 |
468 |
468 |
469 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------"; |
469 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------"; |
470 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------"; |
470 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------"; |
471 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------"; |
471 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------"; |
472 val t = TermC.str2term "sqrt 4"; |
472 val t = TermC.str2term "sqrt 4"; |
473 Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t; |
473 Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t; |
474 |
474 |
475 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) = |
475 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) = |
476 ((ThyC.get_theory "Isac_Knowledge"), |
476 ((ThyC.get_theory "Isac_Knowledge"), |
477 ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> theory -> (string * term) option), t); |
477 ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> Proof.context -> (string * term) option), t); |
478 |
478 |
479 val SOME (thmid, t) = |
479 val SOME (thmid, t) = |
480 (*case*) get_pair thy op_ eval_fn ct (*of*); |
480 (*case*) get_pair ctxt op_ eval_fn ct (*of*); |
481 (*+*)val "sqrt 4 = 2" = UnparseC.term t; |
481 (*+*)val "sqrt 4 = 2" = UnparseC.term t; |
482 |
482 |
483 (** ) |
483 (** ) |
484 Skip_Proof.make_thm thy t; |
484 Skip_Proof.make_thm thy t; |
485 |
485 |