1 (* equations and functions; functions NOT as lambda-terms
2 author: Walther Neuper 2005, 2006
3 (c) due to copyright terms
6 theory Equation imports Atools begin
10 (*descriptions in the related problems TODOshift here from Descriptions.thy*)
11 substitution :: "bool => una"
14 solve :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *)
15 solveTest :: "[bool * 'a] => bool list" (* for test collection *)
18 Function2Equality :: "[bool, bool, bool]
20 ("((Script Function2Equality (_ _ =))// (_))" 9)
22 text {* defines equation and univariate-equation
28 (c) by Richard Lang, 2003 *}
31 val univariate_equation_prls =
32 append_rls "univariate_equation_prls" e_rls
33 [Calc ("Tools.matches",eval_matches "")];
35 overwritelthy thy (!ruleset',
36 [("univariate_equation_prls",
37 prep_rls univariate_equation_prls)]);
41 (prep_pbt (theory "Equation") "pbl_equ" [] e_pblID
43 [("#Given" ,["equality e_","solveFor v_"]),
44 ("#Where" ,["matches (?a = ?b) e_"]),
45 ("#Find" ,["solutions v_i_"])
47 append_rls "equation_prls" e_rls
48 [Calc ("Tools.matches",eval_matches "")],
49 SOME "solve (e_::bool, v_)",
53 (prep_pbt (theory "Equation") "pbl_equ_univ" [] e_pblID
54 (["univariate","equation"],
55 [("#Given" ,["equality e_","solveFor v_"]),
56 ("#Where" ,["matches (?a = ?b) e_"]),
57 ("#Find" ,["solutions v_i_"])
59 univariate_equation_prls,SOME "solve (e_::bool, v_)",[]));
62 (*.function for handling the cas-input "solve (x+1=2, x)":
63 make a model which is already in ptree-internal format.*)
64 (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
65 val (h,argl) = strip_comb ((term_of o the o (parse thy))
66 "solveTest (x+1=2, x)");
68 fun argl2dtss [Const ("Pair", _) $ eq $ bdv] =
69 [((term_of o the o (parse thy)) "equality", [eq]),
70 ((term_of o the o (parse thy)) "solveFor", [bdv]),
71 ((term_of o the o (parse thy)) "solutions",
72 [(term_of o the o (parse thy)) "L"])
74 | argl2dtss _ = raise error "Equation.ML: wrong argument for argl2dtss";
78 [((term_of o the o (parse thy)) "solveTest",
79 (("Test.thy", ["univariate","equation","test"], ["no_met"]),
81 ((term_of o the o (parse thy)) "solve",
82 (("Isac.thy", ["univariate","equation"], ["no_met"]),
89 (prep_met (theory "Equation") "met_equ" [] e_metID
92 {rew_ord'="tless_true", rls'=Erls, calc = [],
95 crls = Atools_erls, nrls = e_rls},