(*.(c) by Richard Lang, 2003 .*)

 (* defines equation and univariate-equation

    created by: rlang 

          date: 02.09

    changed by: rlang

    last change by: rlang

              date: 02.11.29

 *)

 (* use_thy_only"Knowledge/Equation";

    use_thy"Knowledge/Equation";

    use"Knowledge/Equation.ML";

    use"Equation.ML";

    *)

 theory' := overwritel (!theory', [("Equation.thy",Equation.thy)]);

 val univariate_equation_prls = 

     append_rls "univariate_equation_prls" e_rls 

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

 ruleset' := 

 overwritelthy thy (!ruleset',

 		   [("univariate_equation_prls",

 		     prep_rls univariate_equation_prls)]);

 store_pbt 

  (prep_pbt Equation.thy "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 Equation.thy "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 Equation.thy "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"

 ));