405 |
405 |
406 (*.get the formula f at ptp rewritten by the Rewrite_* already applied to f.*) |
406 (*.get the formula f at ptp rewritten by the Rewrite_* already applied to f.*) |
407 (* val (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) = tac'; |
407 (* val (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) = tac'; |
408 *) |
408 *) |
409 fun context_thy (pt, pos as (p,p_)) (tac as Rewrite (thmID,_)) = |
409 fun context_thy (pt, pos as (p,p_)) (tac as Rewrite (thmID,_)) = |
|
410 let val thm = Global_Theory.get_thm (Isac ()) thmID |
|
411 in |
410 (case applicable_in pos pt tac of |
412 (case applicable_in pos pt tac of |
411 Appl (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) => |
413 Appl (Rewrite' (thy', ord', erls, _, thm, f, (res,asm))) => |
412 let |
414 let |
413 val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID |
|
414 val thm_deriv = Thm.get_name_hint thm |
415 val thm_deriv = Thm.get_name_hint thm |
415 in |
416 in |
416 ContThm |
417 ContThm |
417 {thyID = theory'2thyID thy', |
418 {thyID = theory'2thyID thy', |
418 thm = |
419 thm = |
440 ContNOrew |
441 ContNOrew |
441 {thyID = theory'2thyID thy', |
442 {thyID = theory'2thyID thy', |
442 thm_rls = |
443 thm_rls = |
443 thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv), |
444 thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv), |
444 applto = f} |
445 applto = f} |
445 end) |
446 end) |
|
447 end |
446 | context_thy (pt, pos as (p,p_)) (tac as Rewrite_Inst (subs, (thmID,_))) = |
448 | context_thy (pt, pos as (p,p_)) (tac as Rewrite_Inst (subs, (thmID,_))) = |
|
449 let val thm = Global_Theory.get_thm (Isac ()) thmID |
|
450 in |
447 (case applicable_in pos pt tac of |
451 (case applicable_in pos pt tac of |
448 Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), f, (res, asm))) => |
452 Appl (Rewrite_Inst' (thy', ord', erls, _, subst, thm, f, (res, asm))) => |
449 let |
453 let |
450 val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID |
|
451 val thm_deriv = Thm.get_name_hint thm |
454 val thm_deriv = Thm.get_name_hint thm |
452 val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm) |
455 val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm) |
453 in |
456 in |
454 ContThmInst |
457 ContThmInst |
455 {thyID = theory'2thyID thy', |
458 {thyID = theory'2thyID thy', |
484 thm_rls = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv), |
487 thm_rls = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv), |
485 bdvs = subst, |
488 bdvs = subst, |
486 thminst = thminst, |
489 thminst = thminst, |
487 applto = f} |
490 applto = f} |
488 end) |
491 end) |
|
492 end |
489 | context_thy (pt,p) (tac as Rewrite_Set rls') = |
493 | context_thy (pt,p) (tac as Rewrite_Set rls') = |
490 (case applicable_in p pt tac of |
494 (case applicable_in p pt tac of |
491 Appl (Rewrite_Set' (thy', _, rls, f, (res,asm))) => |
495 Appl (Rewrite_Set' (thy', _, rls, f, (res,asm))) => |
492 ContRls |
496 ContRls |
493 {thyID = theory'2thyID thy', |
497 {thyID = theory'2thyID thy', |
562 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*) |
566 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*) |
563 (* val |
567 (* val |
564 *) |
568 *) |
565 fun atomic_appl_tacs thy _ _ f (Calculate scrID) = |
569 fun atomic_appl_tacs thy _ _ f (Calculate scrID) = |
566 try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' thy scrID |> snd)) |
570 try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' thy scrID |> snd)) |
567 | atomic_appl_tacs thy ro erls f (Rewrite (thm' as (thmID, _))) = |
571 | atomic_appl_tacs thy ro erls f (Rewrite (thm'' as (thmID, _))) = |
568 try_rew thy (ro, assoc_rew_ord ro) erls [] f |
572 try_rew thy (ro, assoc_rew_ord ro) erls [] f |
569 (Thm (thmID, assoc_thm' thy thm')) |
573 (Thm (thmID, assoc_thm'' thy thm'')) |
570 | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm' as (thmID, _))) = |
574 | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm'' as (thmID, _))) = |
571 try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f |
575 try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f |
572 (Thm (thmID, assoc_thm' thy thm')) |
576 (Thm (thmID, assoc_thm'' thy thm'')) |
573 |
577 |
574 | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') = |
578 | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') = |
575 filter_appl_rews thy [] f (assoc_rls rls') |
579 filter_appl_rews thy [] f (assoc_rls rls') |
576 | atomic_appl_tacs thy _ _ f (Rewrite_Set_Inst (subs, rls')) = |
580 | atomic_appl_tacs thy _ _ f (Rewrite_Set_Inst (subs, rls')) = |
577 filter_appl_rews thy (subs2subst thy subs) f (assoc_rls rls') |
581 filter_appl_rews thy (subs2subst thy subs) f (assoc_rls rls') |
634 |
638 |
635 (*..*) |
639 (*..*) |
636 fun guh2rewtac (guh:guh) ([] : subs) = |
640 fun guh2rewtac (guh:guh) ([] : subs) = |
637 let val [isa, thy, sect, xstr] = guh2theID guh |
641 let val [isa, thy, sect, xstr] = guh2theID guh |
638 in case sect of |
642 in case sect of |
639 "Theorems" => Rewrite (xstr, "") |
643 "Theorems" => Rewrite (xstr, (Thm.prop_of o assoc_thm'' (assoc_thy thy)) (xstr, e_term)) |
640 | "Rulesets" => Rewrite_Set xstr |
644 | "Rulesets" => Rewrite_Set xstr |
641 | str => error ("guh2rewtac: not impl. for '"^xstr^"'") |
645 | str => error ("guh2rewtac: not impl. for '"^xstr^"'") |
642 end |
646 end |
643 | guh2rewtac (guh:guh) subs = |
647 | guh2rewtac (guh:guh) subs = |
644 let val [isa, thy, sect, xstr] = guh2theID guh |
648 let val [isa, thy, sect, xstr] = guh2theID guh |
645 in case sect of |
649 in case sect of |
646 "Theorems" => Rewrite_Inst (subs, (xstr, "")) |
650 "Theorems" => |
647 | "Rulesets" => Rewrite_Set_Inst (subs, xstr) |
651 Rewrite_Inst (subs, (xstr, (Thm.prop_of o assoc_thm'' (assoc_thy thy)) (xstr, e_term))) |
648 | str => error ("guh2rewtac: not impl. for '"^xstr^"'") |
652 | "Rulesets" => Rewrite_Set_Inst (subs, xstr) |
|
653 | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'") |
649 end; |
654 end; |
650 (*> guh2rewtac "thy_isac_Test-thm-constant_mult_square" []; |
655 (*> guh2rewtac "thy_isac_Test-thm-constant_mult_square" []; |
651 val it = Rewrite ("constant_mult_square", "") : tac |
656 val it = Rewrite ("constant_mult_square", "") : tac |
652 > guh2rewtac "thy_isac_Test-thm-risolate_bdv_add" ["(bdv, x)"]; |
657 > guh2rewtac "thy_isac_Test-thm-risolate_bdv_add" ["(bdv, x)"]; |
653 val it = Rewrite_Inst (["(bdv, x)"], ("risolate_bdv_add", "")) : tac |
658 val it = Rewrite_Inst (["(bdv, x)"], ("risolate_bdv_add", "")) : tac |