
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@37950: ruleset' := 
neuper@37967: overwritelthy @{theory} (!ruleset',
neuper@37950: 		   [("univariate_equation_prls",
neuper@37950: 		     prep_rls univariate_equation_prls)]);
neuper@37950: 
neuper@37950: 
neuper@37950: store_pbt 
neuper@37972:  (prep_pbt thy "pbl_equ" [] e_pblID
neuper@37950:  (["equation"],
neuper@37981:   [("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981:    ("#Where" ,["matches (?a = ?b) e_e"]),
neuper@38012:    ("#Find"  ,["solutions v_v'i'"])
neuper@37950:   ],
neuper@37950:   append_rls "equation_prls" e_rls 
neuper@37950: 	     [Calc ("Tools.matches",eval_matches "")],
neuper@37981:   SOME "solve (e_e::bool, v_v)",
neuper@37950:   []));
neuper@37950: 
neuper@37950: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equ_univ" [] e_pblID
neuper@37950:  (["univariate","equation"],
neuper@37981:   [("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981:    ("#Where" ,["matches (?a = ?b) e_e"]),
neuper@38012:    ("#Find"  ,["solutions v_v'i'"])
neuper@37950:   ],
neuper@37981:   univariate_equation_prls,SOME "solve (e_e::bool, v_v)",[]));
neuper@37950: 
neuper@37950: 
neuper@37950: (*.function for handling the cas-input "solve (x+1=2, x)":
neuper@37950:    make a model which is already in ptree-internal format.*)
neuper@37950: (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
neuper@37950:    val (h,argl) = strip_comb ((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";
neuper@37950: 
neuper@37950: castab := 
neuper@37950: overwritel (!castab, 
neuper@37950: 	    [((term_of o the o (parse thy)) "solveTest", 
neuper@37991: 	      (("Test", ["univariate","equation","test"], ["no_met"]), 
neuper@37950: 	       argl2dtss)),
neuper@37950: 	     ((term_of o the o (parse thy)) "solve",  
neuper@37991: 	      (("Isac", ["univariate","equation"], ["no_met"]), 
neuper@37950: 	       argl2dtss))
neuper@37950: 	     ]);
neuper@37950: 
neuper@37950: 
neuper@37950: 
neuper@37950: store_met
neuper@37972:     (prep_met thy "met_equ" [] e_metID
neuper@37950: 	      (["Equation"],
neuper@37950: 	       [],
neuper@37950: 	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
neuper@37950: 		srls = e_rls, 
neuper@37950: 		prls=e_rls,
neuper@37950: 	     crls = Atools_erls, nrls = e_rls},
neuper@37950: "empty_script"
neuper@37950: ));
neuper@37950: *}
neuper@37950: 
neuper@37906: end



