222 (* val Script sc = scr; |
222 (* val Script sc = scr; |
223 *) |
223 *) |
224 fun init_form thy (Script sc) env = |
224 fun init_form thy (Script sc) env = |
225 (case get_stac thy sc of |
225 (case get_stac thy sc of |
226 NONE => NONE (*raise error ("init_form: no 1st stac in "^ |
226 NONE => NONE (*raise error ("init_form: no 1st stac in "^ |
227 (Sign.string_of_term (sign_of thy) sc))*) |
227 (Syntax.string_of_term (thy2ctxt thy) sc))*) |
228 | SOME stac => SOME (subst_atomic env stac)) |
228 | SOME stac => SOME (subst_atomic env stac)) |
229 | init_form _ _ _ = raise error "init_form: no match"; |
229 | init_form _ _ _ = raise error "init_form: no match"; |
230 |
230 |
231 (* use"ME/script.sml"; |
231 (* use"ME/script.sml"; |
232 use"script.sml"; |
232 use"script.sml"; |
299 |
299 |
300 (*.from penv in itm_ make args for script depending on type of description.*) |
300 (*.from penv in itm_ make args for script depending on type of description.*) |
301 (*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv |
301 (*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv |
302 9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*) |
302 9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*) |
303 fun mk_arg thy d [] = raise error ("mk_arg: no data for "^ |
303 fun mk_arg thy d [] = raise error ("mk_arg: no data for "^ |
304 (Sign.string_of_term (sign_of thy) d)) |
304 (Syntax.string_of_term (thy2ctxt thy) d)) |
305 | mk_arg thy d [t] = |
305 | mk_arg thy d [t] = |
306 (case dsc_valT d of |
306 (case dsc_valT d of |
307 "una" => [t] |
307 "una" => [t] |
308 | "nam" => |
308 | "nam" => |
309 [case t of |
309 [case t of |
310 r as (Const ("op =",_) $ _ $ _) => r |
310 r as (Const ("op =",_) $ _ $ _) => r |
311 | _ => raise error |
311 | _ => raise error |
312 ("mk_arg: dsc-typ 'nam' applied to non-equality "^ |
312 ("mk_arg: dsc-typ 'nam' applied to non-equality "^ |
313 (Sign.string_of_term (sign_of thy) t))] |
313 (Syntax.string_of_term (thy2ctxt thy) t))] |
314 | s => raise error ("mk_arg: not impl. for "^s)) |
314 | s => raise error ("mk_arg: not impl. for "^s)) |
315 |
315 |
316 | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts); |
316 | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts); |
317 (* |
317 (* |
318 val d = d_in itm_; |
318 val d = d_in itm_; |
348 (* |
348 (* |
349 > val sc = ... Solve_root_equation ... |
349 > val sc = ... Solve_root_equation ... |
350 > val mI = ("Script.thy","sqrt-equ-test"); |
350 > val mI = ("Script.thy","sqrt-equ-test"); |
351 > val PblObj{meth={ppc=itms,...},...} = get_obj I pt []; |
351 > val PblObj{meth={ppc=itms,...},...} = get_obj I pt []; |
352 > val ts = itms2args thy mI itms; |
352 > val ts = itms2args thy mI itms; |
353 > map (Sign.string_of_term (sign_of thy)) ts; |
353 > map (Syntax.string_of_term (thy2ctxt thy)) ts; |
354 ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list |
354 ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list |
355 *) |
355 *) |
356 |
356 |
357 |
357 |
358 (*["bool_ (1+x=2)","real_ x"] --match_ags--> oris |
358 (*["bool_ (1+x=2)","real_ x"] --match_ags--> oris |
418 *) |
418 *) |
419 |
419 |
420 (*12.1.01.*) |
420 (*12.1.01.*) |
421 | stac2tac_ pt thy (Const("Script.Check'_elementwise",_) $ _ $ |
421 | stac2tac_ pt thy (Const("Script.Check'_elementwise",_) $ _ $ |
422 (set as Const ("Collect",_) $ Abs (_,_,pred))) = |
422 (set as Const ("Collect",_) $ Abs (_,_,pred))) = |
423 (Check_elementwise (Sign.string_of_term (sign_of thy) pred), |
423 (Check_elementwise (Syntax.string_of_term (thy2ctxt thy) pred), |
424 (*set*)Empty_Tac_) |
424 (*set*)Empty_Tac_) |
425 |
425 |
426 | stac2tac_ pt thy (Const("Script.Or'_to'_List",_) $ _ ) = |
426 | stac2tac_ pt thy (Const("Script.Or'_to'_List",_) $ _ ) = |
427 (Or_to_List, Empty_Tac_) |
427 (Or_to_List, Empty_Tac_) |
428 |
428 |
473 Subproblem' ((dI, pI, mI), pors, hdl, fmz_, f)) |
473 Subproblem' ((dI, pI, mI), pors, hdl, fmz_, f)) |
474 end |
474 end |
475 |
475 |
476 | stac2tac_ pt thy t = raise error |
476 | stac2tac_ pt thy t = raise error |
477 ("stac2tac_ TODO: no match for "^ |
477 ("stac2tac_ TODO: no match for "^ |
478 (Sign.string_of_term (sign_of thy) t)); |
478 (Syntax.string_of_term (thy2ctxt thy) t)); |
479 (* |
479 (* |
480 > val t = (term_of o the o (parse thy)) |
480 > val t = (term_of o the o (parse thy)) |
481 "Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False (x=a+#1)"; |
481 "Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False (x=a+#1)"; |
482 > stac2tac_ pt t; |
482 > stac2tac_ pt t; |
483 val it = Rewrite_Set_Inst ([(#,#)],"isolate_bdv") : tac |
483 val it = Rewrite_Set_Inst ([(#,#)],"isolate_bdv") : tac |
539 then pred |
539 then pred |
540 else (mk_and o (map fst)) (get_assumptions_ pt (p,Res)) |
540 else (mk_and o (map fst)) (get_assumptions_ pt (p,Res)) |
541 in (bdv, pred) end |
541 in (bdv, pred) end |
542 | rep_set thy _ _ set = |
542 | rep_set thy _ _ set = |
543 raise error ("check_elementwise: no set "^ (*from script*) |
543 raise error ("check_elementwise: no set "^ (*from script*) |
544 (Sign.string_of_term (sign_of thy) set)); |
544 (Syntax.string_of_term (thy2ctxt thy) set)); |
545 (*> val set = (term_of o the o (parse thy)) "{(x::real). Assumptions}"; |
545 (*> val set = (term_of o the o (parse thy)) "{(x::real). Assumptions}"; |
546 > val p = []; |
546 > val p = []; |
547 > val pt = union_asm pt p [("#0 <= sqrt x + sqrt (#5 + x)",[11]), |
547 > val pt = union_asm pt p [("#0 <= sqrt x + sqrt (#5 + x)",[11]), |
548 ("#0 <= #9 + #4 * x",[22]), |
548 ("#0 <= #9 + #4 * x",[22]), |
549 ("#0 <= x ^^^ #2 + #5 * x",[33]), |
549 ("#0 <= x ^^^ #2 + #5 * x",[33]), |
550 ("#0 <= #2 + x",[44])]; |
550 ("#0 <= #2 + x",[44])]; |
551 > val (bdv,pred) = rep_set thy pt p set; |
551 > val (bdv,pred) = rep_set thy pt p set; |
552 val bdv = Free ("x","RealDef.real") : term |
552 val bdv = Free ("x","RealDef.real") : term |
553 > writeln (Sign.string_of_term (sign_of thy) pred); |
553 > writeln (Syntax.string_of_term (thy2ctxt thy) pred); |
554 ((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & |
554 ((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & |
555 #0 <= x ^^^ #2 + #5 * x) & |
555 #0 <= x ^^^ #2 + #5 * x) & |
556 #0 <= #2 + x |
556 #0 <= #2 + x |
557 *) |
557 *) |
558 --------------------------------------------11.6.03--was unused*) |
558 --------------------------------------------11.6.03--was unused*) |
832 val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,(*fT*)bool,fT] ---> fT) |
832 val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,(*fT*)bool,fT] ---> fT) |
833 $ subs' $ Free (thmID,idT) $ b $ f; |
833 $ subs' $ Free (thmID,idT) $ b $ f; |
834 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end |
834 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end |
835 (*Fehlersuche 25.4.01 |
835 (*Fehlersuche 25.4.01 |
836 (a)----- als String zusammensetzen: |
836 (a)----- als String zusammensetzen: |
837 ML> Sign.string_of_term (sign_of thy)f; |
837 ML> Syntax.string_of_term (thy2ctxt thy)f; |
838 val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string |
838 val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string |
839 ML> Sign.string_of_term (sign_of thy)f'; |
839 ML> Syntax.string_of_term (thy2ctxt thy)f'; |
840 val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string |
840 val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string |
841 ML> subs; |
841 ML> subs; |
842 val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst |
842 val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst |
843 > val tt = (term_of o the o (parse thy)) |
843 > val tt = (term_of o the o (parse thy)) |
844 "(Rewrite_Inst[(bdv,x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))"; |
844 "(Rewrite_Inst[(bdv,x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))"; |
845 > atomty tt; |
845 > atomty tt; |
846 ML> writeln(Sign.string_of_term (sign_of thy)tt); |
846 ML> writeln(Syntax.string_of_term (thy2ctxt thy)tt); |
847 (Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) = |
847 (Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) = |
848 #0 + d_d x (x ^^^ #2 + #3 * x) |
848 #0 + d_d x (x ^^^ #2 + #3 * x) |
849 |
849 |
850 (b)----- laut rep_tac_: |
850 (b)----- laut rep_tac_: |
851 > val ttt=HOLogic.mk_eq (lhs,f'); |
851 > val ttt=HOLogic.mk_eq (lhs,f'); |