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 Base_Tools begin
8 text \<open>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 *)
27 text \<open>defines equation and univariate-equation
33 (c) by Richard Lang, 2003\<close>
37 val ctxt = Rule.thy2ctxt thy;
39 val univariate_equation_prls =
40 Rule.append_rls "univariate_equation_prls" Rule.e_rls
41 [Rule.Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
43 setup \<open>KEStore_Elems.add_rlss [("univariate_equation_prls",
44 (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} univariate_equation_prls))]\<close>
45 setup \<open>KEStore_Elems.add_pbts
46 [(Specify.prep_pbt thy "pbl_equ" [] Celem.e_pblID
48 [("#Given" ,["equality e_e","solveFor v_v"]),
49 ("#Where" ,["matches (?a = ?b) e_e"]),
50 ("#Find" ,["solutions v_v'i'"])],
51 Rule.append_rls "equation_prls" Rule.e_rls [Rule.Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "")],
52 SOME "solve (e_e::bool, v_v)", [])),
53 (Specify.prep_pbt thy "pbl_equ_univ" [] Celem.e_pblID
54 (["univariate","equation"],
55 [("#Given" ,["equality e_e","solveFor v_v"]),
56 ("#Where" ,["matches (?a = ?b) e_e"]),
57 ("#Find" ,["solutions v_v'i'"])],
58 univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))]\<close>
62 (*.function for handling the cas-input "solve (x+1=2, x)":
63 make a model which is already in ctree-internal format.*)
64 (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
65 val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy))
66 "solveTest (x+1=2, x)");
68 fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] =
69 [((the o (TermC.parseNEW ctxt)) "equality", [eq]),
70 ((the o (TermC.parseNEW ctxt)) "solveFor", [bdv]),
71 ((the o (TermC.parseNEW ctxt)) "solutions",
72 [(the o (TermC.parseNEW ctxt)) "L"])
74 | argl2dtss _ = error "Equation.ML: wrong argument for argl2dtss";
76 setup \<open>KEStore_Elems.add_cas
77 [((Thm.term_of o the o (TermC.parse thy)) "solveTest",
78 (("Test", ["univariate","equation","test"], ["no_met"]), argl2dtss)),
79 ((Thm.term_of o the o (TermC.parse thy)) "solve",
80 (("Isac_Knowledge", ["univariate","equation"], ["no_met"]), argl2dtss))]\<close>
83 setup \<open>KEStore_Elems.add_mets
84 [Specify.prep_met thy "met_equ" [] Celem.e_metID
86 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
87 errpats = [], nrls = Rule.e_rls},