326 *) |
326 *) |
327 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) |
327 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) |
328 "Script Stepwise (t::'z) =\ |
328 "Script Stepwise (t::'z) =\ |
329 \(Repeat\ |
329 \(Repeat\ |
330 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
330 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
331 \ (Try (Repeat (Rewrite real_add_commute False))) @@ \ |
331 \ (Try (Repeat (Rewrite add_commute False))) @@ \ |
332 \ (Try (Repeat (Rewrite real_mult_commute False)))) \ |
332 \ (Try (Repeat (Rewrite real_mult_commute False)))) \ |
333 \ t_t)"; |
333 \ t_t)"; |
334 val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*) |
334 val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*) |
335 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) |
335 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) |
336 "Script Stepwise (t::'z) =\ |
336 "Script Stepwise (t::'z) =\ |
337 \(Repeat\ |
337 \(Repeat\ |
338 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
338 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
339 \ (Try (Repeat (Rewrite real_add_commute False))) @@ \ |
339 \ (Try (Repeat (Rewrite add_commute False))) @@ \ |
340 \ (Try (Repeat (Rewrite real_mult_commute False)))) \ |
340 \ (Try (Repeat (Rewrite real_mult_commute False)))) \ |
341 \ t_t)"; |
341 \ t_t)"; |
342 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body |
342 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body |
343 are inconsistent !!!*) |
343 are inconsistent !!!*) |
344 val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*) |
344 val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*) |
345 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) |
345 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) |
346 "Script Stepwise_inst (t::'z) (v::real) =\ |
346 "Script Stepwise_inst (t::'z) (v::real) =\ |
347 \(Repeat\ |
347 \(Repeat\ |
348 \ ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \ |
348 \ ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \ |
349 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] real_add_commute False))) @@\ |
349 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] add_commute False))) @@\ |
350 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] real_mult_commute False)))) \ |
350 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] real_mult_commute False)))) \ |
351 \ t)"; |
351 \ t)"; |
352 val Repeat $ _ = |
352 val Repeat $ _ = |
353 ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) |
353 ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) |
354 "Repeat (Rewrite real_diff_minus False t)"; |
354 "Repeat (Rewrite real_diff_minus False t)"; |
374 ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) |
374 ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) |
375 "Rewrite_Set_Inst [(bdv,v)] real_diff_minus False"; |
375 "Rewrite_Set_Inst [(bdv,v)] real_diff_minus False"; |
376 val SEq $ _ $ _ $ _ = |
376 val SEq $ _ $ _ $ _ = |
377 ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) |
377 ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) |
378 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
378 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
379 \ (Try (Repeat (Rewrite real_add_commute False))) @@ \ |
379 \ (Try (Repeat (Rewrite add_commute False))) @@ \ |
380 \ (Try (Repeat (Rewrite real_mult_commute False)))) t"; |
380 \ (Try (Repeat (Rewrite real_mult_commute False)))) t"; |
381 |
381 |
382 fun rule2stac _ (Thm (thmID, _)) = |
382 fun rule2stac _ (Thm (thmID, _)) = |
383 Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ HOLogic.false_const)) |
383 Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ HOLogic.false_const)) |
384 | rule2stac calc (Calc (c, _)) = |
384 | rule2stac calc (Calc (c, _)) = |