1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Thu Aug 26 10:03:53 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Thu Aug 26 18:15:30 2010 +0200
     1.3 @@ -1,29 +1,100 @@
     1.4  (* equations and functions; functions NOT as lambda-terms
     1.5     author: Walther Neuper 2005, 2006
     1.6     (c) due to copyright terms
     1.7 -
     1.8 -remove_thy"Equation";
     1.9 -use_thy"Knowledge/Equation";
    1.10 -use_thy_only"Knowledge/Equation";
    1.11 -
    1.12 -remove_thy"Equation";
    1.13 -use_thy"Knowledge/Isac";
    1.14  *)
    1.15  
    1.16 -Equation = Atools +
    1.17 +theory Equation imports Atools begin
    1.18  
    1.19  consts
    1.20  
    1.21    (*descriptions in the related problems TODOshift here from Descriptions.thy*)
    1.22 -  substitution :: bool => una
    1.23 +  substitution      :: "bool => una"
    1.24  
    1.25    (*the CAS-commands*)
    1.26 -  solve     :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *)
    1.27 -  solveTest :: "[bool * 'a] => bool list" (* for test collection *)
    1.28 +  solve             :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *)
    1.29 +  solveTest         :: "[bool * 'a] => bool list" (* for test collection *)
    1.30    
    1.31    (*Script-names*)
    1.32 -  Function2Equality  :: "[bool, bool,       bool] \
    1.33 -					\=> bool"
    1.34 +  Function2Equality :: "[bool, bool,       bool] 
    1.35 +					 => bool"
    1.36                    ("((Script Function2Equality (_ _ =))// (_))" 9)
    1.37  
    1.38 +text {* defines equation and univariate-equation
    1.39 +        created by: rlang 
    1.40 +              date: 02.09
    1.41 +        changed by: rlang
    1.42 +        last change by: rlang
    1.43 +                  date: 02.11.29
    1.44 +        (c) by Richard Lang, 2003 *}
    1.45 +
    1.46 +ML {*
    1.47 +val univariate_equation_prls = 
    1.48 +    append_rls "univariate_equation_prls" e_rls 
    1.49 +	       [Calc ("Tools.matches",eval_matches "")];
    1.50 +ruleset' := 
    1.51 +overwritelthy thy (!ruleset',
    1.52 +		   [("univariate_equation_prls",
    1.53 +		     prep_rls univariate_equation_prls)]);
    1.54 +
    1.55 +
    1.56 +store_pbt 
    1.57 + (prep_pbt Equation.thy "pbl_equ" [] e_pblID
    1.58 + (["equation"],
    1.59 +  [("#Given" ,["equality e_","solveFor v_"]),
    1.60 +   ("#Where" ,["matches (?a = ?b) e_"]),
    1.61 +   ("#Find"  ,["solutions v_i_"])
    1.62 +  ],
    1.63 +  append_rls "equation_prls" e_rls 
    1.64 +	     [Calc ("Tools.matches",eval_matches "")],
    1.65 +  SOME "solve (e_::bool, v_)",
    1.66 +  []));
    1.67 +
    1.68 +store_pbt
    1.69 + (prep_pbt Equation.thy "pbl_equ_univ" [] e_pblID
    1.70 + (["univariate","equation"],
    1.71 +  [("#Given" ,["equality e_","solveFor v_"]),
    1.72 +   ("#Where" ,["matches (?a = ?b) e_"]),
    1.73 +   ("#Find"  ,["solutions v_i_"])
    1.74 +  ],
    1.75 +  univariate_equation_prls,SOME "solve (e_::bool, v_)",[]));
    1.76 +
    1.77 +
    1.78 +(*.function for handling the cas-input "solve (x+1=2, x)":
    1.79 +   make a model which is already in ptree-internal format.*)
    1.80 +(* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
    1.81 +   val (h,argl) = strip_comb ((term_of o the o (parse thy)) 
    1.82 +				  "solveTest (x+1=2, x)");
    1.83 +   *)
    1.84 +fun argl2dtss [Const ("Pair", _) $ eq $ bdv] =
    1.85 +    [((term_of o the o (parse thy)) "equality", [eq]),
    1.86 +     ((term_of o the o (parse thy)) "solveFor", [bdv]),
    1.87 +     ((term_of o the o (parse thy)) "solutions", 
    1.88 +      [(term_of o the o (parse thy)) "L"])
    1.89 +     ]
    1.90 +  | argl2dtss _ = raise error "Equation.ML: wrong argument for argl2dtss";
    1.91 +
    1.92 +castab := 
    1.93 +overwritel (!castab, 
    1.94 +	    [((term_of o the o (parse thy)) "solveTest", 
    1.95 +	      (("Test.thy", ["univariate","equation","test"], ["no_met"]), 
    1.96 +	       argl2dtss)),
    1.97 +	     ((term_of o the o (parse thy)) "solve",  
    1.98 +	      (("Isac.thy", ["univariate","equation"], ["no_met"]), 
    1.99 +	       argl2dtss))
   1.100 +	     ]);
   1.101 +
   1.102 +
   1.103 +
   1.104 +store_met
   1.105 +    (prep_met Equation.thy "met_equ" [] e_metID
   1.106 +	      (["Equation"],
   1.107 +	       [],
   1.108 +	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
   1.109 +		srls = e_rls, 
   1.110 +		prls=e_rls,
   1.111 +	     crls = Atools_erls, nrls = e_rls},
   1.112 +"empty_script"
   1.113 +));
   1.114 +*}
   1.115 +
   1.116  end
   1.117 \ No newline at end of file