ad 967c8a1eb6b1 (2): for 'ptyps' add functions accessing Theory_Data in parallel to the old ones for 'Unsynchronized.ref'.
- get_ptyps and store_pbts added to KEStore_Elems
- fun merge for Theory_Data
- RootEq and RatEq now necessarily inherit from Equation. ptyps worked previously - Due to fortunate computation order?
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
8 text {* univariate equations over terms :
9 In 2003 Richard Lang prototyped ISAC's equation solver while also alpha-testing
10 the Lucas-Interpreter's Subproblem mechanism.
11 This prototype suffers from the drop-out of Matthias Goldgruber for a year,
12 who had started to work on simplification in parallel. So this implementation
13 replaced simplifiers by many specific theorems for specific terms in specific
14 phases of equation solving; these specific solutions wait for generalisation
15 in future improvements of ISAC's equation solver.
20 (*descriptions in the related problems TODOshift here from Descriptions.thy*)
21 substitution :: "bool => una"
24 solve :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *)
25 solveTest :: "[bool * 'a] => bool list" (* for test collection *)
28 Function2Equality :: "[bool, bool, bool]
30 ("((Script Function2Equality (_ _ =))// (_))" 9)
32 text {* defines equation and univariate-equation
38 (c) by Richard Lang, 2003 *}
42 val ctxt = thy2ctxt thy;
44 val univariate_equation_prls =
45 append_rls "univariate_equation_prls" e_rls
46 [Calc ("Tools.matches",eval_matches "")];
48 setup {* KEStore_Elems.add_rlss [("univariate_equation_prls",
49 (Context.theory_name @{theory}, prep_rls univariate_equation_prls))] *}
52 (prep_pbt thy "pbl_equ" [] e_pblID
54 [("#Given" ,["equality e_e","solveFor v_v"]),
55 ("#Where" ,["matches (?a = ?b) e_e"]),
56 ("#Find" ,["solutions v_v'i'"])
58 append_rls "equation_prls" e_rls
59 [Calc ("Tools.matches",eval_matches "")],
60 SOME "solve (e_e::bool, v_v)",
64 (prep_pbt thy "pbl_equ_univ" [] e_pblID
65 (["univariate","equation"],
66 [("#Given" ,["equality e_e","solveFor v_v"]),
67 ("#Where" ,["matches (?a = ?b) e_e"]),
68 ("#Find" ,["solutions v_v'i'"])
70 univariate_equation_prls,SOME "solve (e_e::bool, v_v)",[]));
72 setup {* KEStore_Elems.store_pbts
73 [(prep_pbt thy "pbl_equ" [] e_pblID
75 [("#Given" ,["equality e_e","solveFor v_v"]),
76 ("#Where" ,["matches (?a = ?b) e_e"]),
77 ("#Find" ,["solutions v_v'i'"])],
78 append_rls "equation_prls" e_rls [Calc ("Tools.matches",eval_matches "")],
79 SOME "solve (e_e::bool, v_v)", [])),
80 (prep_pbt thy "pbl_equ_univ" [] e_pblID
81 (["univariate","equation"],
82 [("#Given" ,["equality e_e","solveFor v_v"]),
83 ("#Where" ,["matches (?a = ?b) e_e"]),
84 ("#Find" ,["solutions v_v'i'"])],
85 univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))] *}
89 (*.function for handling the cas-input "solve (x+1=2, x)":
90 make a model which is already in ptree-internal format.*)
91 (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
92 val (h,argl) = strip_comb ((term_of o the o (parse thy))
93 "solveTest (x+1=2, x)");
95 fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] =
96 [((the o (parseNEW ctxt)) "equality", [eq]),
97 ((the o (parseNEW ctxt)) "solveFor", [bdv]),
98 ((the o (parseNEW ctxt)) "solutions",
99 [(the o (parseNEW ctxt)) "L"])
101 | argl2dtss _ = error "Equation.ML: wrong argument for argl2dtss";
103 setup {* KEStore_Elems.add_cas
104 [((term_of o the o (parse thy)) "solveTest",
105 (("Test", ["univariate","equation","test"], ["no_met"]), argl2dtss)),
106 ((term_of o the o (parse thy)) "solve",
107 (("Isac", ["univariate","equation"], ["no_met"]), argl2dtss))]*}
112 (prep_met thy "met_equ" [] e_metID
115 {rew_ord'="tless_true", rls'=Erls, calc = [],
118 crls = Atools_erls, errpats = [], nrls = e_rls},