neuper@37906: (* equations and functions; functions NOT as lambda-terms
neuper@37906:    author: Walther Neuper 2005, 2006
neuper@37906:    (c) due to copyright terms
neuper@37906: *)
neuper@37906: 
neuper@37950: theory Equation imports Atools begin
neuper@37906: 
neuper@37906: consts
neuper@37906: 
neuper@37906:   (*descriptions in the related problems TODOshift here from Descriptions.thy*)
neuper@37950:   substitution      :: "bool => una"
neuper@37906: 
neuper@37906:   (*the CAS-commands*)
neuper@37950:   solve             :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *)
neuper@37950:   solveTest         :: "[bool * 'a] => bool list" (* for test collection *)
neuper@37906:   
neuper@37906:   (*Script-names*)
neuper@37950:   Function2Equality :: "[bool, bool,       bool] 
neuper@37950: 					 => bool"
neuper@37906:                   ("((Script Function2Equality (_ _ =))// (_))" 9)
neuper@37906: 
neuper@37950: text {* defines equation and univariate-equation
neuper@37950:         created by: rlang 
neuper@37950:               date: 02.09
neuper@37950:         changed by: rlang
neuper@37950:         last change by: rlang
neuper@37950:                   date: 02.11.29
neuper@37950:         (c) by Richard Lang, 2003 *}
neuper@37950: 
neuper@37950: ML {*
neuper@37972: val thy = @{theory};
neuper@37972: 
neuper@37950: val univariate_equation_prls = 
neuper@37950:     append_rls "univariate_equation_prls" e_rls 
neuper@37950: 	       [Calc ("Tools.matches",eval_matches "")];
neuper@37950: ruleset' := 
neuper@37967: overwritelthy @{theory} (!ruleset',
neuper@37950: 		   [("univariate_equation_prls",
neuper@37950: 		     prep_rls univariate_equation_prls)]);
neuper@37950: 
neuper@37950: 
neuper@37950: store_pbt 
neuper@37972:  (prep_pbt thy "pbl_equ" [] e_pblID
neuper@37950:  (["equation"],
neuper@37981:   [("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981:    ("#Where" ,["matches (?a = ?b) e_e"]),
neuper@37981:    ("#Find"  ,["solutions v_i"])
neuper@37950:   ],
neuper@37950:   append_rls "equation_prls" e_rls 
neuper@37950: 	     [Calc ("Tools.matches",eval_matches "")],
neuper@37981:   SOME "solve (e_e::bool, v_v)",
neuper@37950:   []));
neuper@37950: 
neuper@37950: store_pbt
neuper@37972:  (prep_pbt thy "pbl_equ_univ" [] e_pblID
neuper@37950:  (["univariate","equation"],
neuper@37981:   [("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981:    ("#Where" ,["matches (?a = ?b) e_e"]),
neuper@37981:    ("#Find"  ,["solutions v_i"])
neuper@37950:   ],
neuper@37981:   univariate_equation_prls,SOME "solve (e_e::bool, v_v)",[]));
neuper@37950: 
neuper@37950: 
neuper@37950: (*.function for handling the cas-input "solve (x+1=2, x)":
neuper@37950:    make a model which is already in ptree-internal format.*)
neuper@37950: (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
neuper@37950:    val (h,argl) = strip_comb ((term_of o the o (parse thy)) 
neuper@37950: 				  "solveTest (x+1=2, x)");
neuper@37950:    *)
neuper@37950: fun argl2dtss [Const ("Pair", _) $ eq $ bdv] =
neuper@37950:     [((term_of o the o (parse thy)) "equality", [eq]),
neuper@37950:      ((term_of o the o (parse thy)) "solveFor", [bdv]),
neuper@37950:      ((term_of o the o (parse thy)) "solutions", 
neuper@37950:       [(term_of o the o (parse thy)) "L"])
neuper@37950:      ]
neuper@37950:   | argl2dtss _ = raise error "Equation.ML: wrong argument for argl2dtss";
neuper@37950: 
neuper@37950: castab := 
neuper@37950: overwritel (!castab, 
neuper@37950: 	    [((term_of o the o (parse thy)) "solveTest", 
neuper@37991: 	      (("Test", ["univariate","equation","test"], ["no_met"]), 
neuper@37950: 	       argl2dtss)),
neuper@37950: 	     ((term_of o the o (parse thy)) "solve",  
neuper@37991: 	      (("Isac", ["univariate","equation"], ["no_met"]), 
neuper@37950: 	       argl2dtss))
neuper@37950: 	     ]);
neuper@37950: 
neuper@37950: 
neuper@37950: 
neuper@37950: store_met
neuper@37972:     (prep_met thy "met_equ" [] e_metID
neuper@37950: 	      (["Equation"],
neuper@37950: 	       [],
neuper@37950: 	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
neuper@37950: 		srls = e_rls, 
neuper@37950: 		prls=e_rls,
neuper@37950: 	     crls = Atools_erls, nrls = e_rls},
neuper@37950: "empty_script"
neuper@37950: ));
neuper@37950: *}
neuper@37950: 
neuper@37906: end