(* 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 thy = @{theory};

val ctxt = ThyC.to_ctxt thy;

val univariate_equation_prls = 

    Rule_Set.append_rules "univariate_equation_prls" Rule_Set.empty 

	       [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];

\<close>

setup \<open>KEStore_Elems.add_rlss [("univariate_equation_prls",

  (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} univariate_equation_prls))]\<close>

setup \<open>KEStore_Elems.add_pbts

  [(Specify.prep_pbt thy "pbl_equ" [] Spec.e_pblID

      (["equation"],

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

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

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

        Rule_Set.append_rules "equation_prls" Rule_Set.empty  [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")],

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

    (Specify.prep_pbt thy "pbl_equ_univ" [] Spec.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)", []))]\<close>

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 ("Product_Type.Pair", _) $ eq $ bdv] =

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

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

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

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

     ]

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

\<close>

setup \<open>KEStore_Elems.add_cas

  [((Thm.term_of o the o (TermC.parse thy)) "solveTest", 

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

    ((Thm.term_of o the o (TermC.parse thy)) "solve",

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

setup \<open>KEStore_Elems.add_mets

    [Specify.prep_met thy "met_equ" [] Spec.e_metID

	    (["Equation"], [],

	      {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},

        @{thm refl})]

\<close>

end