301 | istates2str (SOME i1, SOME i2) = "(#SOME "^istate2str i1^",\n #SOME "^ |
301 | istates2str (SOME i1, SOME i2) = "(#SOME "^istate2str i1^",\n #SOME "^ |
302 istate2str i2^")"; |
302 istate2str i2^")"; |
303 |
303 |
304 fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) = |
304 fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) = |
305 (ScrState (env, loc_, topt, v, safe, bool)) |
305 (ScrState (env, loc_, topt, v, safe, bool)) |
306 | new_val _ _ = raise error "new_val: only for ScrState"; |
306 | new_val _ _ = error "new_val: only for ScrState"; |
307 |
307 |
308 datatype con = land | lor; |
308 datatype con = land | lor; |
309 |
309 |
310 |
310 |
311 type spec = |
311 type spec = |
498 | End_Proof' => "End_Proof'" |
498 | End_Proof' => "End_Proof'" |
499 | _ => "tac2str not impl. for ?!"; |
499 | _ => "tac2str not impl. for ?!"; |
500 |
500 |
501 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls |
501 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls |
502 | rls_of (Rewrite_Set rls) = rls |
502 | rls_of (Rewrite_Set rls) = rls |
503 | rls_of tac = raise error ("rls_of: called with tac '"^tac2IDstr tac^"'"); |
503 | rls_of tac = error ("rls_of: called with tac '"^tac2IDstr tac^"'"); |
504 |
504 |
505 fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) = |
505 fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) = |
506 (thmID, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst)) |
506 (thmID, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst)) |
507 | thm_of_rew (Rewrite (thmID,_)) = (thmID, NONE) |
507 | thm_of_rew (Rewrite (thmID,_)) = (thmID, NONE) |
508 | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE); |
508 | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE); |
520 Rewrite_Inst (subst2subs subst, (thmID, string_of_thmI thm)) |
520 Rewrite_Inst (subst2subs subst, (thmID, string_of_thmI thm)) |
521 | rule2tac [] (Rls_ rls) = Rewrite_Set (id_rls rls) |
521 | rule2tac [] (Rls_ rls) = Rewrite_Set (id_rls rls) |
522 | rule2tac subst (Rls_ rls) = |
522 | rule2tac subst (Rls_ rls) = |
523 Rewrite_Set_Inst (subst2subs subst, (id_rls rls)) |
523 Rewrite_Set_Inst (subst2subs subst, (id_rls rls)) |
524 | rule2tac _ rule = |
524 | rule2tac _ rule = |
525 raise error ("rule2tac: called with '" ^ rule2str rule ^ "'"); |
525 error ("rule2tac: called with '" ^ rule2str rule ^ "'"); |
526 |
526 |
527 type fmz_ = cterm' list; |
527 type fmz_ = cterm' list; |
528 |
528 |
529 (*.a formalization of an example containing data |
529 (*.a formalization of an example containing data |
530 sufficient for mechanically finding the solution for the example.*) |
530 sufficient for mechanically finding the solution for the example.*) |
832 (*fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used*) |
832 (*fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used*) |
833 fun lev_dnRes ((p,_):pos') = (lev_dn p, Res):pos'; |
833 fun lev_dnRes ((p,_):pos') = (lev_dn p, Res):pos'; |
834 |
834 |
835 (*4.4.00*) |
835 (*4.4.00*) |
836 fun lev_up_ ((p,Res):pos') = (lev_up p,Res):pos' |
836 fun lev_up_ ((p,Res):pos') = (lev_up p,Res):pos' |
837 | lev_up_ p' = raise error ("lev_up_: called for "^(pos'2str p')); |
837 | lev_up_ p' = error ("lev_up_: called for "^(pos'2str p')); |
838 fun lev_dn_ ((p,_):pos') = (lev_dn p,Res):pos' |
838 fun lev_dn_ ((p,_):pos') = (lev_dn p,Res):pos' |
839 fun ind ((p,_):pos') = length p; (*WN050108 deprecated in favour of lev_of*) |
839 fun ind ((p,_):pos') = length p; (*WN050108 deprecated in favour of lev_of*) |
840 fun lev_of ((p,_):pos') = length p; |
840 fun lev_of ((p,_):pos') = length p; |
841 |
841 |
842 |
842 |
1476 |
1476 |
1477 |
1477 |
1478 fun get_somespec ((dI,pI,mI):spec) ((dI',pI',mI'):spec) = |
1478 fun get_somespec ((dI,pI,mI):spec) ((dI',pI',mI'):spec) = |
1479 let val domID = if dI = e_domID |
1479 let val domID = if dI = e_domID |
1480 then if dI' = e_domID |
1480 then if dI' = e_domID |
1481 then raise error"pt_extract: no domID in probl,origin" |
1481 then error"pt_extract: no domID in probl,origin" |
1482 else dI' |
1482 else dI' |
1483 else dI |
1483 else dI |
1484 val pblID = if pI = e_pblID |
1484 val pblID = if pI = e_pblID |
1485 then if pI' = e_pblID |
1485 then if pI' = e_pblID |
1486 then raise error"pt_extract: no pblID in probl,origin" |
1486 then error"pt_extract: no pblID in probl,origin" |
1487 else pI' |
1487 else pI' |
1488 else pI |
1488 else pI |
1489 val metID = if mI = e_metID |
1489 val metID = if mI = e_metID |
1490 then if pI' = e_metID |
1490 then if pI' = e_metID |
1491 then raise error"pt_extract: no metID in probl,origin" |
1491 then error"pt_extract: no metID in probl,origin" |
1492 else mI' |
1492 else mI' |
1493 else mI |
1493 else mI |
1494 in (domID, pblID, metID):spec end; |
1494 in (domID, pblID, metID):spec end; |
1495 fun get_somespec' ((dI,pI,mI):spec) ((dI',pI',mI'):spec) = |
1495 fun get_somespec' ((dI,pI,mI):spec) ((dI',pI',mI'):spec) = |
1496 let val domID = if dI = e_domID then dI' else dI |
1496 let val domID = if dI = e_domID then dI' else dI |
1733 (*.determine the next pos' on the same level.*) |
1733 (*.determine the next pos' on the same level.*) |
1734 fun lev_on' pt (([],Pbl):pos') = ([],Res):pos' |
1734 fun lev_on' pt (([],Pbl):pos') = ([],Res):pos' |
1735 | lev_on' pt (p, Res) = |
1735 | lev_on' pt (p, Res) = |
1736 if get_obj g_res pt p = get_obj g_form pt (lev_on p)(*TransitiveB*) |
1736 if get_obj g_res pt p = get_obj g_form pt (lev_on p)(*TransitiveB*) |
1737 then if existpt' (lev_on p, Res) pt then (lev_on p, Res) |
1737 then if existpt' (lev_on p, Res) pt then (lev_on p, Res) |
1738 else raise error ("lev_on': (p, Res) -> (p, Res) not existent, \ |
1738 else error ("lev_on': (p, Res) -> (p, Res) not existent, \ |
1739 \p = "^ints2str' (lev_on p)) |
1739 \p = "^ints2str' (lev_on p)) |
1740 else (lev_on p, Frm) |
1740 else (lev_on p, Frm) |
1741 | lev_on' pt (p, _) = |
1741 | lev_on' pt (p, _) = |
1742 if existpt' (p, Res) pt then (p, Res) |
1742 if existpt' (p, Res) pt then (p, Res) |
1743 else raise error ("lev_on': (p, Frm) -> (p, Res) not existent, \ |
1743 else error ("lev_on': (p, Frm) -> (p, Res) not existent, \ |
1744 \p = "^ints2str' p); |
1744 \p = "^ints2str' p); |
1745 |
1745 |
1746 fun exist_lev_on' pt p = (lev_on' pt p; true) handle _ => false; |
1746 fun exist_lev_on' pt p = (lev_on' pt p; true) handle _ => false; |
1747 |
1747 |
1748 (*.is the pos' at the last element of a calulation _AND_ can be continued.*) |
1748 (*.is the pos' at the last element of a calulation _AND_ can be continued.*) |
2148 ); |
2148 ); |
2149 |
2149 |
2150 (*.get the theory explicitly specified for the rootpbl; |
2150 (*.get the theory explicitly specified for the rootpbl; |
2151 thus use this function _after_ finishing specification.*) |
2151 thus use this function _after_ finishing specification.*) |
2152 fun rootthy (Nd (PblObj {spec=(thyID, _, _),...}, _)) = assoc_thy thyID |
2152 fun rootthy (Nd (PblObj {spec=(thyID, _, _),...}, _)) = assoc_thy thyID |
2153 | rootthy _ = raise error "rootthy"; |
2153 | rootthy _ = error "rootthy"; |
2154 |
2154 |