1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.ML	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,85 @@
     1.4 +(*.(c) by Richard Lang, 2003 .*)
     1.5 +(* defines equation and univariate-equation
     1.6 +   created by: rlang 
     1.7 +         date: 02.09
     1.8 +   changed by: rlang
     1.9 +   last change by: rlang
    1.10 +             date: 02.11.29
    1.11 +*)
    1.12 +
    1.13 +(* use_thy_only"Knowledge/Equation";
    1.14 +   use_thy"Knowledge/Equation";
    1.15 +   use"Knowledge/Equation.ML";
    1.16 +   use"Equation.ML";
    1.17 +   *)
    1.18 +
    1.19 +theory' := overwritel (!theory', [("Equation.thy",Equation.thy)]);
    1.20 +
    1.21 +val univariate_equation_prls = 
    1.22 +    append_rls "univariate_equation_prls" e_rls 
    1.23 +	       [Calc ("Tools.matches",eval_matches "")];
    1.24 +ruleset' := 
    1.25 +overwritelthy thy (!ruleset',
    1.26 +		   [("univariate_equation_prls",
    1.27 +		     prep_rls univariate_equation_prls)]);
    1.28 +
    1.29 +
    1.30 +store_pbt 
    1.31 + (prep_pbt Equation.thy "pbl_equ" [] e_pblID
    1.32 + (["equation"],
    1.33 +  [("#Given" ,["equality e_","solveFor v_"]),
    1.34 +   ("#Where" ,["matches (?a = ?b) e_"]),
    1.35 +   ("#Find"  ,["solutions v_i_"])
    1.36 +  ],
    1.37 +  append_rls "equation_prls" e_rls 
    1.38 +	     [Calc ("Tools.matches",eval_matches "")],
    1.39 +  SOME "solve (e_::bool, v_)",
    1.40 +  []));
    1.41 +
    1.42 +store_pbt
    1.43 + (prep_pbt Equation.thy "pbl_equ_univ" [] e_pblID
    1.44 + (["univariate","equation"],
    1.45 +  [("#Given" ,["equality e_","solveFor v_"]),
    1.46 +   ("#Where" ,["matches (?a = ?b) e_"]),
    1.47 +   ("#Find"  ,["solutions v_i_"])
    1.48 +  ],
    1.49 +  univariate_equation_prls,SOME "solve (e_::bool, v_)",[]));
    1.50 +
    1.51 +
    1.52 +(*.function for handling the cas-input "solve (x+1=2, x)":
    1.53 +   make a model which is already in ptree-internal format.*)
    1.54 +(* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
    1.55 +   val (h,argl) = strip_comb ((term_of o the o (parse thy)) 
    1.56 +				  "solveTest (x+1=2, x)");
    1.57 +   *)
    1.58 +fun argl2dtss [Const ("Pair", _) $ eq $ bdv] =
    1.59 +    [((term_of o the o (parse thy)) "equality", [eq]),
    1.60 +     ((term_of o the o (parse thy)) "solveFor", [bdv]),
    1.61 +     ((term_of o the o (parse thy)) "solutions", 
    1.62 +      [(term_of o the o (parse thy)) "L"])
    1.63 +     ]
    1.64 +  | argl2dtss _ = raise error "Equation.ML: wrong argument for argl2dtss";
    1.65 +
    1.66 +castab := 
    1.67 +overwritel (!castab, 
    1.68 +	    [((term_of o the o (parse thy)) "solveTest", 
    1.69 +	      (("Test.thy", ["univariate","equation","test"], ["no_met"]), 
    1.70 +	       argl2dtss)),
    1.71 +	     ((term_of o the o (parse thy)) "solve",  
    1.72 +	      (("Isac.thy", ["univariate","equation"], ["no_met"]), 
    1.73 +	       argl2dtss))
    1.74 +	     ]);
    1.75 +
    1.76 +
    1.77 +
    1.78 +store_met
    1.79 +    (prep_met Equation.thy "met_equ" [] e_metID
    1.80 +	      (["Equation"],
    1.81 +	       [],
    1.82 +	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
    1.83 +		srls = e_rls, 
    1.84 +		prls=e_rls,
    1.85 +	     crls = Atools_erls, nrls = e_rls},
    1.86 +"empty_script"
    1.87 +));
    1.88 +