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

    author: Walther Neuper 2005, 2006

    (c) due to copyright terms

 *)

 theory Equation imports Base_Tools begin

 text \<open>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.

 \<close>

 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 *)

 text \<open>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\<close>

 ML \<open>

 val univariate_equation_prls = 

     Rule_Set.append_rules "univariate_equation_prls" Rule_Set.empty 

 	       [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];

 \<close>

 rule_set_knowledge univariate_equation_prls = \<open>Auto_Prog.prep_rls @{theory} univariate_equation_prls\<close>

 problem pbl_equ : "equation" =

   \<open>Rule_Set.append_rules "equation_prls" Rule_Set.empty

     [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")]\<close>

   CAS: "solve (e_e::bool, v_v)"

   Given: "equality e_e" "solveFor v_v"

   Where: "matches (?a = ?b) e_e"

   Find: "solutions v_v'i'"

 problem pbl_equ_univ : "univariate/equation" =

   \<open>univariate_equation_prls\<close>

   CAS: "solve (e_e::bool, v_v)"

   Given: "equality e_e" "solveFor v_v"

   Where: "matches (?a = ?b) e_e"

   Find: "solutions v_v'i'"

 ML\<open>

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

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

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

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

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

    *)

 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ eq $ bdv] =

     [((the o (TermC.parseNEW \<^context>)) "equality", [eq]),

      ((the o (TermC.parseNEW \<^context>)) "solveFor", [bdv]),

      ((the o (TermC.parseNEW \<^context>)) "solutions", 

       [(the o (TermC.parseNEW \<^context>)) "L"])

      ]

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

 \<close>

 setup \<open>KEStore_Elems.add_cas

   [((Thm.term_of o the o (TermC.parse @{theory})) "solveTest", 

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

     ((Thm.term_of o the o (TermC.parse @{theory})) "solve",

       (("Isac_Knowledge", ["univariate", "equation"], ["no_met"]), argl2dtss))]\<close>

 method met_equ : "Equation" =

   \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,

           errpats = [], nrls = Rule_Set.empty}\<close>

 ML \<open>

 \<close> ML \<open>

 \<close>

 end