neuper@37906: (* equations and functions; functions NOT as lambda-terms
neuper@37906:    author: Walther Neuper 2005, 2006
neuper@37906:    (c) due to copyright terms
neuper@37906: *)
neuper@37906: 
neuper@37950: theory Equation imports Atools begin
neuper@37906: 
neuper@42398: text {* univariate equations over terms :
neuper@42398:   In 2003 Richard Lang prototyped ISAC's equation solver while also alpha-testing
neuper@42398:   the Lucas-Interpreter's Subproblem mechanism.
neuper@42398:   This prototype suffers from the drop-out of Matthias Goldgruber for a year,
neuper@42398:   who had started to work on simplification in parallel. So this implementation
neuper@42398:   replaced simplifiers by many specific theorems for specific terms in specific
neuper@42398:   phases of equation solving; these specific solutions wait for generalisation
neuper@42398:   in future improvements of ISAC's equation solver.
neuper@42398: *}
neuper@42398: 
neuper@37906: consts
neuper@37906: 
neuper@37906:   (*descriptions in the related problems TODOshift here from Descriptions.thy*)
neuper@37950:   substitution      :: "bool => una"
neuper@37906: 
neuper@37906:   (*the CAS-commands*)
neuper@37950:   solve             :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *)
neuper@37950:   solveTest         :: "[bool * 'a] => bool list" (* for test collection *)
neuper@37906:   
neuper@37906:   (*Script-names*)
neuper@37950:   Function2Equality :: "[bool, bool,       bool] 
neuper@37950: 					 => bool"
neuper@37906:                   ("((Script Function2Equality (_ _ =))// (_))" 9)
neuper@37906: 
neuper@37950: text {* defines equation and univariate-equation
neuper@37950:         created by: rlang 
neuper@37950:               date: 02.09
neuper@37950:         changed by: rlang
neuper@37950:         last change by: rlang
neuper@37950:                   date: 02.11.29
neuper@37950:         (c) by Richard Lang, 2003 *}
neuper@37950: 
neuper@37950: ML {*
neuper@37972: val thy = @{theory};
bonzai@41952: val ctxt = thy2ctxt thy;
neuper@37972: 
neuper@37950: val univariate_equation_prls = 
neuper@37950:     append_rls "univariate_equation_prls" e_rls 
neuper@37950: 	       [Calc ("Tools.matches",eval_matches "")];
neuper@52125: *}
neuper@52125: setup {* KEStore_Elems.add_rlss [("univariate_equation_prls",
s1210629013@55444:   (Context.theory_name @{theory}, prep_rls @{theory} univariate_equation_prls))] *}
s1210629013@55359: setup {* KEStore_Elems.add_pbts
wneuper@59269:   [(Specify.prep_pbt thy "pbl_equ" [] e_pblID
s1210629013@55339:       (["equation"],
s1210629013@55339:         [("#Given" ,["equality e_e","solveFor v_v"]),
s1210629013@55339:           ("#Where" ,["matches (?a = ?b) e_e"]),
s1210629013@55339:           ("#Find"  ,["solutions v_v'i'"])],
s1210629013@55339:         append_rls "equation_prls" e_rls  [Calc ("Tools.matches",eval_matches "")],
s1210629013@55339:         SOME "solve (e_e::bool, v_v)", [])),
wneuper@59269:     (Specify.prep_pbt thy "pbl_equ_univ" [] e_pblID
s1210629013@55339:       (["univariate","equation"],
s1210629013@55339:         [("#Given" ,["equality e_e","solveFor v_v"]),
s1210629013@55339:           ("#Where" ,["matches (?a = ?b) e_e"]),
s1210629013@55339:           ("#Find"  ,["solutions v_v'i'"])],
s1210629013@55339:         univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))] *}
neuper@37950: 
neuper@37950: 
s1210629013@55339: ML{*
neuper@37950: (*.function for handling the cas-input "solve (x+1=2, x)":
wneuper@59279:    make a model which is already in ctree-internal format.*)
neuper@37950: (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
wneuper@59186:    val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy)) 
neuper@37950: 				  "solveTest (x+1=2, x)");
neuper@37950:    *)
neuper@41972: fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] =
bonzai@41952:     [((the o (parseNEW ctxt)) "equality", [eq]),
bonzai@41952:      ((the o (parseNEW ctxt)) "solveFor", [bdv]),
bonzai@41952:      ((the o (parseNEW ctxt)) "solutions", 
bonzai@41952:       [(the o (parseNEW ctxt)) "L"])
neuper@37950:      ]
neuper@38031:   | argl2dtss _ = error "Equation.ML: wrong argument for argl2dtss";
s1210629013@52170: *}
s1210629013@52170: setup {* KEStore_Elems.add_cas
wneuper@59186:   [((Thm.term_of o the o (parse thy)) "solveTest", 
s1210629013@52170:       (("Test", ["univariate","equation","test"], ["no_met"]), argl2dtss)),
wneuper@59186:     ((Thm.term_of o the o (parse thy)) "solve",
s1210629013@52170:       (("Isac", ["univariate","equation"], ["no_met"]), argl2dtss))]*}
neuper@37950: 
neuper@37950: 
s1210629013@55373: setup {* KEStore_Elems.add_mets
wneuper@59269:   [Specify.prep_met thy "met_equ" [] e_metID
s1210629013@55373: 	    (["Equation"], [],
s1210629013@55373: 	      {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
s1210629013@55373:           errpats = [], nrls = e_rls},
s1210629013@55373:         "empty_script")]
s1210629013@55373: *}
neuper@37950: 
neuper@37906: end