295 |
295 |
296 datatype con = land | lor; |
296 datatype con = land | lor; |
297 |
297 |
298 |
298 |
299 |
299 |
300 (*.tactics propagate the construction of the calc-tree; |
300 (*.tactics propagate the construction of the calc-tree (as seen by the user); |
301 there are |
301 there are |
302 (a) 'specsteps' for the specify-phase, and others for the solve-phase |
302 (a) 'specsteps' for the specify-phase, and others for the solve-phase |
303 (b) those of the solve-phase are 'initac's and others; |
303 (b) those of the solve-phase are 'initac's and others; |
304 initacs start with a formula different from the preceding formula. |
304 initacs start with a formula different from the preceding formula. |
305 see 'type tac_' for the internal representation of tactics.*) |
305 see 'type tac_' for the internal representation of tactics.*) |
324 Apply_Method also does the 1st step in the script (an 'initac') if there |
324 Apply_Method also does the 1st step in the script (an 'initac') if there |
325 is no 'init_form' .*) |
325 is no 'init_form' .*) |
326 | Check_Postcond of pblID |
326 | Check_Postcond of pblID |
327 | Free_Solve |
327 | Free_Solve |
328 |
328 |
329 | Rewrite_Inst of ( subs * thm') | Rewrite of thm' |
329 | Rewrite_Inst of ( subs * thm'') | Rewrite of thm'' | Rewrite_Asm of thm'' |
330 | Rewrite_Asm of thm' |
|
331 | Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls' |
330 | Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls' |
332 | Detail_Set_Inst of ( subs * rls') | Detail_Set of rls' |
331 | Detail_Set_Inst of ( subs * rls') | Detail_Set of rls' |
333 | End_Detail (*end of script from next_tac, |
332 | End_Detail (*end of script from next_tac, |
334 in solve: switches back to parent script WN0509 drop!*) |
333 in solve: switches back to parent script WN0509 drop!*) |
335 | Derive of rls' (*an input formula using rls WN0509 drop!*) |
334 | Derive of rls' (*an input formula using rls WN0509 drop!*) |
377 | Specify_Method metID => "Specify_Method "^(strs2str metID) |
376 | Specify_Method metID => "Specify_Method "^(strs2str metID) |
378 | Apply_Method metID => "Apply_Method "^(strs2str metID) |
377 | Apply_Method metID => "Apply_Method "^(strs2str metID) |
379 | Check_Postcond pblID => "Check_Postcond "^(strs2str pblID) |
378 | Check_Postcond pblID => "Check_Postcond "^(strs2str pblID) |
380 | Free_Solve => "Free_Solve" |
379 | Free_Solve => "Free_Solve" |
381 |
380 |
382 | Rewrite_Inst (subs,thm')=> |
381 | Rewrite_Inst (subs, (id, term)) => |
383 "Rewrite_Inst "^(pair2str (subs2str subs, spair2str thm')) |
382 "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, term2str term))) |
384 | Rewrite thm' => "Rewrite "^(spair2str thm') |
383 | Rewrite (id, term) => "Rewrite " ^ spair2str (id, term2str term) |
385 | Rewrite_Asm thm' => "Rewrite_Asm "^(spair2str thm') |
384 | Rewrite_Asm (id, term) => "Rewrite_Asm " ^ spair2str (id, term2str term) |
386 | Rewrite_Set_Inst (subs, rls) => |
385 | Rewrite_Set_Inst (subs, rls) => |
387 "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls)) |
386 "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls)) |
388 | Rewrite_Set rls => "Rewrite_Set "^(quote rls ) |
387 | Rewrite_Set rls => "Rewrite_Set "^(quote rls ) |
389 | Detail_Set rls => "Detail_Set "^(quote rls ) |
388 | Detail_Set rls => "Detail_Set "^(quote rls ) |
390 | Detail_Set_Inst (subs, rls) => |
389 | Detail_Set_Inst (subs, rls) => |
486 | rls_of_rewset (Detail_Set rls) = (rls, NONE) |
485 | rls_of_rewset (Detail_Set rls) = (rls, NONE) |
487 | rls_of_rewset (Detail_Set_Inst (subs, rls)) = |
486 | rls_of_rewset (Detail_Set_Inst (subs, rls)) = |
488 (rls, SOME ((subs2subst (assoc_thy "Isac") subs):subst)); |
487 (rls, SOME ((subs2subst (assoc_thy "Isac") subs):subst)); |
489 |
488 |
490 fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID) |
489 fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID) |
491 | rule2tac _ [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm) |
490 | rule2tac _ [] (Thm (thmID, thm)) = Rewrite (thmID, Thm.prop_of thm) |
492 | rule2tac _ subst (Thm (thmID, thm)) = |
491 | rule2tac _ subst (Thm (thmID, thm)) = |
493 Rewrite_Inst (subst2subs subst, (thmID, string_of_thmI thm)) |
492 Rewrite_Inst (subst2subs subst, (thmID, Thm.prop_of thm)) |
494 | rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls) |
493 | rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls) |
495 | rule2tac _ subst (Rls_ rls) = |
494 | rule2tac _ subst (Rls_ rls) = |
496 Rewrite_Set_Inst (subst2subs subst, (id_rls rls)) |
495 Rewrite_Set_Inst (subst2subs subst, (id_rls rls)) |
497 | rule2tac _ _ rule = |
496 | rule2tac _ _ rule = |
498 error ("rule2tac: called with '" ^ rule2str rule ^ "'"); |
497 error ("rule2tac: called with '" ^ rule2str rule ^ "'"); |
557 (term * (*returnvalue of script in solve*) |
556 (term * (*returnvalue of script in solve*) |
558 term list) (*collect by get_assumptions_ in applicable_in, except if |
557 term list) (*collect by get_assumptions_ in applicable_in, except if |
559 butlast tac is Check_elementwise: take only these asms*) |
558 butlast tac is Check_elementwise: take only these asms*) |
560 | Free_Solve' |
559 | Free_Solve' |
561 (* context_thy would be simpler if instead thm' woudl be thm *) |
560 (* context_thy would be simpler if instead thm' woudl be thm *) |
562 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm' * term * (term * term list) |
561 | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm * term * (term * term list) |
563 | Rewrite' of theory' * rew_ord' * rls * bool * thm' * term * (term * term list) |
562 | Rewrite' of theory' * rew_ord' * rls * bool * thm * term * (term * term list) |
564 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' * term * (term * term list) |
563 | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm * term * (term * term list) |
565 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * (term * term list) |
564 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * (term * term list) |
566 | Detail_Set_Inst' of theory' * bool * subst * rls * term * (term * term list) |
565 | Detail_Set_Inst' of theory' * bool * subst * rls * term * (term * term list) |
567 | Rewrite_Set' of theory' * bool * rls * term * (term * term list) |
566 | Rewrite_Set' of theory' * bool * rls * term * (term * term list) |
568 | Detail_Set' of theory' * bool * rls * term * (term * term list) |
567 | Detail_Set' of theory' * bool * rls * term * (term * term list) |
569 | End_Detail' of (term * (term list)) (*see End_Trans'*) |
568 | End_Detail' of (term * (term list)) (*see End_Trans'*) |