(* 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 * real] => bool list"(*solveFor ::"real => una"; eg.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 *)

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

    [(ParseC.term_opt \<^context> "equality" |> the, [eq]),

     (ParseC.term_opt \<^context> "solveFor" |> the, [bdv]),

     (ParseC.term_opt \<^context> "solutions" |> the, 

      [ParseC.term_opt\<^context> "L" |> the])

     ]

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

\<close>

cas solveTest = \<open>argl2dtss\<close>

  Theory_Ref: Test

  Problem_Ref: "univariate/equation/test"

cas solve = \<open>argl2dtss\<close>

  Problem_Ref: "univariate/equation"

method met_equ : "Equation" =

  \<open>{rew_ord = "tless_true", rls' = Rule_Set.Empty, calc = [], prog_rls = Rule_Set.empty, 

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

ML \<open>

\<close> ML \<open>

\<close>

end