392 rew_ord' = fst rew_ord, |
392 rew_ord' = fst rew_ord, |
393 rules' = map rul2rul' rules}:rlsdat'; |
393 rules' = map rul2rul' rules}:rlsdat'; |
394 |
394 |
395 fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord, |
395 fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord, |
396 rules'=rules}:rlsdat') = |
396 rules'=rules}:rlsdat') = |
397 let val thy = the (assoc' (theory',thy')) |
397 let val thy = assoc_thy thy'; |
398 in Rls{preconds = map (the o (parse thy)) preconds, |
398 in Rls{preconds = map (the o (parse thy)) preconds, |
399 rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))), |
399 rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))), |
400 rules = map (rul'2rul thy) rules}:rls end; |
400 rules = map (rul'2rul thy) rules}:rls end; |
401 ------- *) |
401 ------- *) |
402 |
402 |
432 *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents) |
432 *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents) |
433 uncaught exception ERROR*) |
433 uncaught exception ERROR*) |
434 |
434 |
435 |
435 |
436 fun parse' (thy:theory') (ct:cterm') = |
436 fun parse' (thy:theory') (ct:cterm') = |
437 case parse ((the o assoc')(!theory',thy)) ct of |
437 case parse (assoc_thy thy) ct of |
438 NONE => NONE |
438 NONE => NONE |
439 | SOME ct => SOME ((term2str (term_of ct)):cterm'); |
439 | SOME ct => SOME ((term2str (term_of ct)):cterm'); |
440 |
440 |
441 |
441 |
442 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst |
442 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst |
443 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) |
443 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) |
444 fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls') |
444 fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls') |
445 (put_asm:bool) (thm:thm') (ct:cterm') = |
445 (put_asm:bool) (thm:thm') (ct:cterm') = |
446 (* val (rew_ord, rls, thm, ct) = (rew_ord', id_rls rls', thm', f); |
446 (* val (rew_ord, rls, thm, ct) = (rew_ord', id_rls rls', thm', f); |
447 *) |
447 *) |
448 let val thy = (the o assoc')(!theory',thy'); |
448 let val thy = assoc_thy thy'; |
449 in |
449 in |
450 case rewrite_ thy |
450 case rewrite_ thy |
451 ((the o assoc')(!rew_ord',rew_ord))((#2 o the o assoc')(!ruleset',rls)) |
451 ((the o assoc')(!rew_ord',rew_ord))((#2 o the o assoc')(!ruleset',rls)) |
452 put_asm ((assoc_thm' thy) thm) |
452 put_asm ((assoc_thm' thy) thm) |
453 ((term_of o the o (parse thy)) ct) of |
453 ((term_of o the o (parse thy)) ct) of |
461 > val rls = "eval_rls"; |
461 > val rls = "eval_rls"; |
462 val put_asm = true; |
462 val put_asm = true; |
463 val thm = ("square_equation_left",""); |
463 val thm = ("square_equation_left",""); |
464 val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)"; |
464 val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)"; |
465 |
465 |
466 val Zthy = ((the o assoc')(!theory',thy)); |
466 val Zthy = assoc_thy thy; |
467 val Zrew_ord = ((the o assoc')(!rew_ord',rew_ord)); |
467 val Zrew_ord = ((the o assoc')(!rew_ord',rew_ord)); |
468 val Zrls = ((the o assoc')(!ruleset',rls)); |
468 val Zrls = ((the o assoc')(!ruleset',rls)); |
469 val Zput_asm = put_asm; |
469 val Zput_asm = put_asm; |
470 val Zthm = ((the o (assoc'_thm' thy)) thm); |
470 val Zthm = ((the o (assoc'_thm' thy)) thm); |
471 val Zct = ((the o (parse ((the o assoc')(!theory',thy)))) ct); |
471 val Zct = ((the o (parse (assoc_thy thy))) ct); |
472 |
472 |
473 rewrite_ Zthy Zrew_ord Zrls Zput_asm Zthm Zct; |
473 rewrite_ Zthy Zrew_ord Zrls Zput_asm Zthm Zct; |
474 |
474 |
475 use"Isa99/interface_ME_ISA.sml"; |
475 use"Isa99/interface_ME_ISA.sml"; |
476 *) |
476 *) |
477 |
477 |
478 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst |
478 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst |
479 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) |
479 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) |
480 fun rewrite_set (thy':theory') (put_asm:bool) |
480 fun rewrite_set (thy':theory') (put_asm:bool) |
481 (rls:rls') (ct:cterm') = |
481 (rls:rls') (ct:cterm') = |
482 let val thy = (the o assoc')(!theory',thy'); |
482 let val thy = (assoc_thy thy'); |
483 in |
483 in |
484 case rewrite_set_ thy put_asm ((#2 o the o assoc')(!ruleset',rls)) |
484 case rewrite_set_ thy put_asm ((#2 o the o assoc')(!ruleset',rls)) |
485 ((term_of o the o (parse thy)) ct) of |
485 ((term_of o the o (parse thy)) ct) of |
486 NONE => NONE |
486 NONE => NONE |
487 | SOME (t, ts) => SOME (term2str t, terms2str ts) |
487 | SOME (t, ts) => SOME (term2str t, terms2str ts) |
504 SOME (res,_) => res |
504 SOME (res,_) => res |
505 | NONE => t end; |
505 | NONE => t end; |
506 |
506 |
507 |
507 |
508 fun get_calculation' (thy:theory') op_ (ct:cterm') = |
508 fun get_calculation' (thy:theory') op_ (ct:cterm') = |
509 case get_calculation_ ((the o assoc')(!theory',thy)) op_ |
509 case get_calculation_ (assoc_thy thy) op_ |
510 ((uminus_to_string o term_of o the o |
510 ((uminus_to_string o term_of o the o |
511 (parse ((the o assoc')(!theory',thy)))) ct) of |
511 (parse (assoc_thy thy))) ct) of |
512 NONE => NONE |
512 NONE => NONE |
513 | SOME (thmid, thm) => |
513 | SOME (thmid, thm) => |
514 SOME ((thmid, string_of_thmI thm):thm'); |
514 SOME ((thmid, string_of_thmI thm):thm'); |
515 |
515 |
516 fun calculate (thy':theory') op_ (ct:cterm') = |
516 fun calculate (thy':theory') op_ (ct:cterm') = |
517 let val thy = (the o assoc')(!theory',thy'); |
517 let val thy = (assoc_thy thy'); |
518 in |
518 in |
519 case calculate_ thy op_ |
519 case calculate_ thy op_ |
520 ((term_of o the o (parse thy)) ct) of |
520 ((term_of o the o (parse thy)) ct) of |
521 NONE => NONE |
521 NONE => NONE |
522 | SOME (ct,(thmID,thm)) => |
522 | SOME (ct,(thmID,thm)) => |
549 |
549 |
550 (* instantiate'' |
550 (* instantiate'' |
551 fun instantiate'' thy' subs ((thmid,ct'):thm') = |
551 fun instantiate'' thy' subs ((thmid,ct'):thm') = |
552 let |
552 let |
553 val thmid_ = implode ("#"::(explode thmid)); (*see type thm'*) |
553 val thmid_ = implode ("#"::(explode thmid)); (*see type thm'*) |
554 val thy = (the o assoc')(!theory',thy'); |
554 val thy = assoc_thy thy'; |
555 val typs = map (#T o rep_cterm o the o (parse thy)) |
555 val typs = map (#T o rep_cterm o the o (parse thy)) |
556 ((snd o split_list) subs); |
556 ((snd o split_list) subs); |
557 val ctyps = map |
557 val ctyps = map |
558 ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o (parse thy)) |
558 ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o (parse thy)) |
559 ((snd o split_list) subs); |
559 ((snd o split_list) subs); |
560 |
560 |
561 > val thy' = "RatArith.thy"; |
561 > val thy' = "RatArith.thy"; |
562 > val subs = [("bdv","x::rat"),("zzz","z::nat")]; |
562 > val subs = [("bdv","x::rat"),("zzz","z::nat")]; |
563 > (the o (parse ((the o assoc')(!theory',thy')))) "x::rat"; |
563 > (the o (parse (assoc_thy thy'))) "x::rat"; |
564 > (#T o rep_cterm o the o (parse ((the o assoc')(!theory',thy')))); |
564 > (#T o rep_cterm o the o (parse (assoc_thy thy'))); |
565 |
565 |
566 > val ctyp = ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o |
566 > val ctyp = ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o |
567 (parse ((the o assoc')(!theory',thy')))) "x::rat"; |
567 (parse (assoc_thy thy'))) "x::rat"; |
568 > val bdv = (the o (parse thy)) "bdv"; |
568 > val bdv = (the o (parse thy)) "bdv"; |
569 > val x = (the o (parse thy)) "x"; |
569 > val x = (the o (parse thy)) "x"; |
570 > (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add) |
570 > (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add) |
571 handle e => print_exn e; |
571 handle e => print_exn e; |
572 uncaught exception THM |
572 uncaught exception THM |
595 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst |
595 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst |
596 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) |
596 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) |
597 fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls') |
597 fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls') |
598 (put_asm:bool) subs (thm:thm') (ct:cterm') = |
598 (put_asm:bool) subs (thm:thm') (ct:cterm') = |
599 let |
599 let |
600 val thy = (the o assoc')(!theory',thy'); |
600 val thy = assoc_thy thy'; |
601 val thm = assoc_thm' thy thm; (*28.10.02*) |
601 val thm = assoc_thm' thy thm; (*28.10.02*) |
602 (*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*) |
602 (*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*) |
603 in |
603 in |
604 case rewrite_ thy |
604 case rewrite_ thy |
605 ((the o assoc')(!rew_ord',rew_ord)) ((#2 o the o assoc')(!ruleset',rls)) |
605 ((the o assoc')(!rew_ord',rew_ord)) ((#2 o the o assoc')(!ruleset',rls)) |
612 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst |
612 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst |
613 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) |
613 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) |
614 fun rewrite_set_inst (thy':theory') (put_asm:bool) |
614 fun rewrite_set_inst (thy':theory') (put_asm:bool) |
615 subs' (rls:rls') (ct:cterm') = |
615 subs' (rls:rls') (ct:cterm') = |
616 let |
616 let |
617 val thy = (the o assoc')(!theory',thy'); |
617 val thy = assoc_thy thy'; |
618 val rls = assoc_rls rls |
618 val rls = assoc_rls rls |
619 val subst = subs'2subst thy subs' |
619 val subst = subs'2subst thy subs' |
620 (*val subrls = instantiate_rls subs ((the o assoc')(!ruleset',rls))*) |
620 (*val subrls = instantiate_rls subs ((the o assoc')(!ruleset',rls))*) |
621 in case rewrite_set_inst_ thy put_asm subst (*sub*)rls |
621 in case rewrite_set_inst_ thy put_asm subst (*sub*)rls |
622 ((term_of o the o (parse thy)) ct) of |
622 ((term_of o the o (parse thy)) ct) of |