(* equations and functions; functions NOT as lambda-terms

    author: Walther Neuper 2005, 2006

    (c) due to copyright terms

 *)

 theory Equation imports Atools begin

 text {* univariate equations over terms :

   In 2003 Richard Lang prototyped ISAC's equation solver while also alpha-testing

   the Lucas-Interpreter's Subproblem mechanism.

   This prototype suffers from the drop-out of Matthias Goldgruber for a year,

   who had started to work on simplification in parallel. So this implementation

   replaced simplifiers by many specific theorems for specific terms in specific

   phases of equation solving; these specific solutions wait for generalisation

   in future improvements of ISAC's equation solver.

 *}

 consts

   (*descriptions in the related problems TODOshift here from Descriptions.thy*)

   substitution      :: "bool => una"

   (*the CAS-commands*)

   solve             :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *)

   solveTest         :: "[bool * 'a] => bool list" (* for test collection *)

   (*Script-names*)

   Function2Equality :: "[bool, bool,       bool] 

 					 => bool"

                   ("((Script Function2Equality (_ _ =))// (_))" 9)

 text {* defines equation and univariate-equation

         created by: rlang 

               date: 02.09

         changed by: rlang

         last change by: rlang

                   date: 02.11.29

         (c) by Richard Lang, 2003 *}

 ML {*

 val thy = @{theory};

 val ctxt = thy2ctxt thy;

 val univariate_equation_prls = 

     append_rls "univariate_equation_prls" e_rls 

 	       [Calc ("Tools.matches",eval_matches "")];

 *}

 setup {* KEStore_Elems.add_rlss [("univariate_equation_prls",

   (Context.theory_name @{theory}, prep_rls univariate_equation_prls))] *}

 setup {* KEStore_Elems.add_pbts

   [(prep_pbt thy "pbl_equ" [] e_pblID

       (["equation"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

           ("#Where" ,["matches (?a = ?b) e_e"]),

           ("#Find"  ,["solutions v_v'i'"])],

         append_rls "equation_prls" e_rls  [Calc ("Tools.matches",eval_matches "")],

         SOME "solve (e_e::bool, v_v)", [])),

     (prep_pbt thy "pbl_equ_univ" [] e_pblID

       (["univariate","equation"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

           ("#Where" ,["matches (?a = ?b) e_e"]),

           ("#Find"  ,["solutions v_v'i'"])],

         univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))] *}

 ML{*

 (*.function for handling the cas-input "solve (x+1=2, x)":

    make a model which is already in ptree-internal format.*)

 (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");

    val (h,argl) = strip_comb ((term_of o the o (parse thy)) 

 				  "solveTest (x+1=2, x)");

    *)

 fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] =

     [((the o (parseNEW ctxt)) "equality", [eq]),

      ((the o (parseNEW ctxt)) "solveFor", [bdv]),

      ((the o (parseNEW ctxt)) "solutions", 

       [(the o (parseNEW ctxt)) "L"])

      ]

   | argl2dtss _ = error "Equation.ML: wrong argument for argl2dtss";

 *}

 setup {* KEStore_Elems.add_cas

   [((term_of o the o (parse thy)) "solveTest", 

       (("Test", ["univariate","equation","test"], ["no_met"]), argl2dtss)),

     ((term_of o the o (parse thy)) "solve",

       (("Isac", ["univariate","equation"], ["no_met"]), argl2dtss))]*}

 ML {*

 store_met

     (prep_met thy "met_equ" [] e_metID

 	      (["Equation"],

 	       [],

 	       {rew_ord'="tless_true", rls'=Erls, calc = [], 

 		srls = e_rls,

 		prls=e_rls,

 	     crls = Atools_erls, errpats = [], nrls = e_rls},

 "empty_script"

 ));

 *}

 setup {* KEStore_Elems.add_mets

   [prep_met thy "met_equ" [] e_metID

 	    (["Equation"], [],

 	      {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,

           errpats = [], nrls = e_rls},

         "empty_script")]

 *}

 end