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

   author: Walther Neuper 2005, 2006

   (c) due to copyright terms

*)

theory Equation imports Atools begin

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 univariate_equation_prls = 

    append_rls "univariate_equation_prls" e_rls 

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

ruleset' := 

overwritelthy @{theory} (!ruleset',

		   [("univariate_equation_prls",

		     prep_rls univariate_equation_prls)]);

store_pbt 

 (prep_pbt (theory "Equation") "pbl_equ" [] e_pblID

 (["equation"],

  [("#Given" ,["equality e_","solveFor v_"]),

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

   ("#Find"  ,["solutions v_i_"])

  ],

  append_rls "equation_prls" e_rls 

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

  SOME "solve (e_::bool, v_)",

  []));

store_pbt

 (prep_pbt (theory "Equation") "pbl_equ_univ" [] e_pblID

 (["univariate","equation"],

  [("#Given" ,["equality e_","solveFor v_"]),

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

   ("#Find"  ,["solutions v_i_"])

  ],

  univariate_equation_prls,SOME "solve (e_::bool, v_)",[]));

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

    [((term_of o the o (parse thy)) "equality", [eq]),

     ((term_of o the o (parse thy)) "solveFor", [bdv]),

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

      [(term_of o the o (parse thy)) "L"])

     ]

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

castab := 

overwritel (!castab, 

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

	      (("Test.thy", ["univariate","equation","test"], ["no_met"]), 

	       argl2dtss)),

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

	      (("Isac.thy", ["univariate","equation"], ["no_met"]), 

	       argl2dtss))

	     ]);

store_met

    (prep_met (theory "Equation") "met_equ" [] e_metID

	      (["Equation"],

	       [],

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

		srls = e_rls, 

		prls=e_rls,

	     crls = Atools_erls, nrls = e_rls},

"empty_script"

));

*}

end