1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/IsacKnowledge/Atools.ML Fri Dec 28 14:57:38 2007 +0100
1.3 @@ -0,0 +1,637 @@
1.4 +(* tools for arithmetic
1.5 + WN.8.3.01
1.6 + use"../IsacKnowledge/Atools.ML";
1.7 + use"IsacKnowledge/Atools.ML";
1.8 + use"Atools.ML";
1.9 + *)
1.10 +
1.11 +(*
1.12 +copy from doc/math-eng.tex WN.28.3.03
1.13 +WN071228 extended
1.14 +
1.15 +\section{Coding standards}
1.16 +
1.17 +%WN071228 extended -----vvv
1.18 +\subsection{Identifiers}
1.19 +Naming is particularily crucial, because Isabelles name space is global, and isac does not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc. However, all the cases (1)..(4) require different typing for one and the same identifier {\tt probe} which is impossible, and actually leads to strange errors (for instance (1) is used as string, except in a script addressing a Subproblem).
1.20 +
1.21 +This are the preliminary rules for naming identifiers>
1.22 +\begin{description}
1.23 +\item [elements of a key] into the hierarchy of problems or methods must not contain capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
1.24 +\item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.
1.25 +\item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!
1.26 +\item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}.
1.27 +\item [???] ???
1.28 +\item [???] ???
1.29 +\end{description}
1.30 +%WN071228 extended -----^^^
1.31 +
1.32 +
1.33 +\subsection{Rule sets}
1.34 +The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML where it can be viewed using the knowledge browsers.
1.35 +
1.36 +There are rulesets visible to the student, and there are rulesets visible (in general) only for math authors. There are also rulesets which {\em must} exist for {\em each} theory; these contain the identifier of the respective theory (including all capital letters) as indicated by {\it Thy} below.
1.37 +\begin{description}
1.38 +
1.39 +\item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a normalform for all terms which can be expressed by the definitions of the respective theory (and the respective parents).
1.40 +
1.41 +\item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms which can be expressed by the definitions of the respective theory (and the respective parents) such, that the rewrites can be presented to the student.
1.42 +
1.43 +\item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with numerical constants only (i.e. all terms which can be expressed by the definitions of the respective theory and the respective parent theories). In particular, this ruleset includes evaluating in/equalities with numerical constants only.
1.44 +WN.3.7.03: may be dropped due to more generality: numericals and non-numericals are logically equivalent, where the latter often add to the assumptions (e.g. in Check_elementwise).
1.45 +
1.46 +\end{description}
1.47 +The above rulesets are all visible to the user, and also may be input; thus they must be contained in the global associationlist {\tt ruleset':= }~! All these rulesets must undergo a preparation using the function {\tt prep_rls}, which generates a script for stepwise rewriting etc.
1.48 +The following rulesets are used for internal purposes and usually invisible to the (naive) user:
1.49 +\begin{description}
1.50 +
1.51 +\item [*\_erls]
1.52 +\item [*\_prls]
1.53 +\item [*\_srls]
1.54 +
1.55 +\end{description}
1.56 +{\tt append_rls, merge_rls, remove_rls}
1.57 +*)
1.58 +
1.59 +"******* Atools.ML begin *******";
1.60 +theory' := overwritel (!theory', [("Atools.thy",Atools.thy)]);
1.61 +
1.62 +(** evaluation of numerals and special predicates on the meta-level **)
1.63 +(*-------------------------functions---------------------*)
1.64 +local (* rlang 09.02 *)
1.65 + (*.a 'c is coefficient of v' if v does occur in c.*)
1.66 + fun coeff_in v c = v mem (vars c);
1.67 +in
1.68 + fun occurs_in v t = coeff_in v t;
1.69 +end;
1.70 +
1.71 +(*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
1.72 +fun eval_occurs_in _ "Atools.occurs'_in"
1.73 + (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
1.74 + ((*writeln("@@@ eval_occurs_in: v= "^(term2str v));
1.75 + writeln("@@@ eval_occurs_in: t= "^(term2str t));*)
1.76 + if occurs_in v t
1.77 + then Some ((term2str p) ^ " = True",
1.78 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.79 + else Some ((term2str p) ^ " = False",
1.80 + Trueprop $ (mk_equality (p, HOLogic.false_const))))
1.81 + | eval_occurs_in _ _ _ _ = None;
1.82 +
1.83 +(*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
1.84 +fun some_occur_in vs t =
1.85 + let fun occurs_in' a b = occurs_in b a
1.86 + in foldl or_ (false, map (occurs_in' t) vs) end;
1.87 +
1.88 +(*("some_occur_in", ("Atools.some'_occur'_in",
1.89 + eval_some_occur_in "#eval_some_occur_in_"))*)
1.90 +fun eval_some_occur_in _ "Atools.some'_occur'_in"
1.91 + (p as (Const ("Atools.some'_occur'_in",_)
1.92 + $ vs $ t)) _ =
1.93 + if some_occur_in (isalist2list vs) t
1.94 + then Some ((term2str p) ^ " = True",
1.95 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.96 + else Some ((term2str p) ^ " = False",
1.97 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.98 + | eval_some_occur_in _ _ _ _ = None;
1.99 +
1.100 +
1.101 +
1.102 +
1.103 +(*evaluate 'is_atom'*)
1.104 +(*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
1.105 +fun eval_is_atom (thmid:string) "Atools.is'_atom"
1.106 + (t as (Const(op0,_) $ arg)) thy =
1.107 + (case arg of
1.108 + Free (n,_) => Some (mk_thmid thmid op0 n "",
1.109 + Trueprop $ (mk_equality (t, true_as_term)))
1.110 + | _ => Some (mk_thmid thmid op0 "" "",
1.111 + Trueprop $ (mk_equality (t, false_as_term))))
1.112 + | eval_is_atom _ _ _ _ = None;
1.113 +
1.114 +(*evaluate 'is_even'*)
1.115 +fun even i = (i div 2) * 2 = i;
1.116 +(*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
1.117 +fun eval_is_even (thmid:string) "Atools.is'_even"
1.118 + (t as (Const(op0,_) $ arg)) thy =
1.119 + (case arg of
1.120 + Free (n,_) =>
1.121 + (case int_of_str n of
1.122 + Some i =>
1.123 + if even i then Some (mk_thmid thmid op0 n "",
1.124 + Trueprop $ (mk_equality (t, true_as_term)))
1.125 + else Some (mk_thmid thmid op0 "" "",
1.126 + Trueprop $ (mk_equality (t, false_as_term)))
1.127 + | _ => None)
1.128 + | _ => None)
1.129 + | eval_is_even _ _ _ _ = None;
1.130 +
1.131 +(*evaluate 'is_const'*)
1.132 +(*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
1.133 +fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)
1.134 + (t as (Const(op0,t0) $ arg)) (thy:theory) =
1.135 + (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
1.136 + (case arg of
1.137 + Const (n1,_) =>
1.138 + Some (mk_thmid thmid op0 n1 "",
1.139 + Trueprop $ (mk_equality (t, false_as_term)))
1.140 + | Free (n1,_) =>
1.141 + if is_numeral n1
1.142 + then Some (mk_thmid thmid op0 n1 "",
1.143 + Trueprop $ (mk_equality (t, true_as_term)))
1.144 + else Some (mk_thmid thmid op0 n1 "",
1.145 + Trueprop $ (mk_equality (t, false_as_term)))
1.146 + | Const ("Float.Float",_) =>
1.147 + Some (mk_thmid thmid op0 (term2str arg) "",
1.148 + Trueprop $ (mk_equality (t, true_as_term)))
1.149 + | _ => (*None*)
1.150 + Some (mk_thmid thmid op0 (term2str arg) "",
1.151 + Trueprop $ (mk_equality (t, false_as_term))))
1.152 + | eval_const _ _ _ _ = None;
1.153 +
1.154 +(*. evaluate binary, associative, commutative operators: *,+,^ .*)
1.155 +(*("plus" ,("op +" ,eval_binop "#add_")),
1.156 + ("times" ,("op *" ,eval_binop "#mult_")),
1.157 + ("power_" ,("Atools.pow" ,eval_binop "#power_"))*)
1.158 +
1.159 +(* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
1.160 + ("xxxxxx",op_,t,thy);
1.161 + *)
1.162 +fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) =
1.163 + thmid ^ "Float ((" ^
1.164 + (string_of_int v11)^","^(string_of_int v12)^"), ("^
1.165 + (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
1.166 + (string_of_int v21)^","^(string_of_int v22)^"), ("^
1.167 + (string_of_int p21)^","^(string_of_int p22)^"))";
1.168 +
1.169 +(*.convert int and float to internal floatingpoint prepresentation.*)
1.170 +fun numeral (Free (str, T)) =
1.171 + (case int_of_str str of
1.172 + Some i => Some ((i, 0), (0, 0))
1.173 + | None => None)
1.174 + | numeral (Const ("Float.Float", _) $
1.175 + (Const ("Pair", _) $
1.176 + (Const ("Pair", T) $ Free (v1, _) $ Free (v2,_)) $
1.177 + (Const ("Pair", _) $ Free (p1, _) $ Free (p2,_))))=
1.178 + (case (int_of_str v1, int_of_str v2, int_of_str p1, int_of_str p2) of
1.179 + (Some v1', Some v2', Some p1', Some p2') =>
1.180 + Some ((v1', v2'), (p1', p2'))
1.181 + | _ => None)
1.182 + | numeral _ = None;
1.183 +
1.184 +(*.evaluate binary associative operations.*)
1.185 +fun eval_binop (thmid:string) (op_:string)
1.186 + (t as ( Const(op0,t0) $
1.187 + (Const(op0',t0') $ v $ t1) $ t2))
1.188 + thy = (*binary . (v.n1).n2*)
1.189 + if op0 = op0' then
1.190 + case (numeral t1, numeral t2) of
1.191 + (Some n1, Some n2) =>
1.192 + let val (T1,T2,Trange) = dest_binop_typ t0
1.193 + val res = calc op0 n1 n2
1.194 + val rhs = var_op_float v op_ t0 T1 res
1.195 + val prop = Trueprop $ (mk_equality (t, rhs))
1.196 + in Some (mk_thmid_f thmid n1 n2, prop) end
1.197 + | _ => None
1.198 + else None
1.199 + | eval_binop (thmid:string) (op_:string)
1.200 + (t as
1.201 + (Const (op0, t0) $ t1 $
1.202 + (Const (op0', t0') $ t2 $ v)))
1.203 + thy = (*binary . n1.(n2.v)*)
1.204 + if op0 = op0' then
1.205 + case (numeral t1, numeral t2) of
1.206 + (Some n1, Some n2) =>
1.207 + let val (T1,T2,Trange) = dest_binop_typ t0
1.208 + val res = calc op0 n1 n2
1.209 + val rhs = float_op_var v op_ t0 T1 res
1.210 + val prop = Trueprop $ (mk_equality (t, rhs))
1.211 + in Some (mk_thmid_f thmid n1 n2, prop) end
1.212 + | _ => None
1.213 + else None
1.214 +
1.215 + | eval_binop (thmid:string) (op_:string)
1.216 + (t as (Const (op0,t0) $ t1 $ t2)) thy = (*binary . n1.n2*)
1.217 + (case (numeral t1, numeral t2) of
1.218 + (Some n1, Some n2) =>
1.219 + let val (T1,T2,Trange) = dest_binop_typ t0;
1.220 + val res = calc op0 n1 n2;
1.221 + val rhs = term_of_float Trange res;
1.222 + val prop = Trueprop $ (mk_equality (t, rhs));
1.223 + in Some (mk_thmid_f thmid n1 n2, prop) end
1.224 + | _ => None)
1.225 + | eval_binop _ _ _ _ = None;
1.226 +(*
1.227 +> val Some (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy;
1.228 +> term2str t;
1.229 +val it = "-1 + 2 = 1"
1.230 +> val t = str2term "-1 * (-1 * a)";
1.231 +> val Some (thmid, t) = eval_binop "#mult_" "op *" t thy;
1.232 +> term2str t;
1.233 +val it = "-1 * (-1 * a) = 1 * a"*)
1.234 +
1.235 +
1.236 +
1.237 +(*.evaluate < and <= for numerals.*)
1.238 +(*("le" ,("op <" ,eval_equ "#less_")),
1.239 + ("leq" ,("op <=" ,eval_equ "#less_equal_"))*)
1.240 +fun eval_equ (thmid:string) (op_:string) (t as
1.241 + (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
1.242 + (case (int_of_str n1, int_of_str n2) of
1.243 + (Some n1', Some n2') =>
1.244 + if calc_equ (strip_thy op0) (n1', n2')
1.245 + then Some (mk_thmid thmid op0 n1 n2,
1.246 + Trueprop $ (mk_equality (t, true_as_term)))
1.247 + else Some (mk_thmid thmid op0 n1 n2,
1.248 + Trueprop $ (mk_equality (t, false_as_term)))
1.249 + | _ => None)
1.250 +
1.251 + | eval_equ _ _ _ _ = None;
1.252 +
1.253 +
1.254 +(*evaluate identity
1.255 +> reflI;
1.256 +val it = "(?t = ?t) = True"
1.257 +> val t = str2term "x = 0";
1.258 +> val None = rewrite_ thy dummy_ord e_rls false reflI t;
1.259 +
1.260 +> val t = str2term "1 = 0";
1.261 +> val None = rewrite_ thy dummy_ord e_rls false reflI t;
1.262 +----------- thus needs Calc !
1.263 +> val t = str2term "0 = 0";
1.264 +> val Some (t',_) = rewrite_ thy dummy_ord e_rls false reflI t;
1.265 +> term2str t';
1.266 +val it = "True"
1.267 +
1.268 +val t = str2term "Not (x = 0)";
1.269 +atomt t; term2str t;
1.270 +*** -------------
1.271 +*** Const ( Not)
1.272 +*** . Const ( op =)
1.273 +*** . . Free ( x, )
1.274 +*** . . Free ( 0, )
1.275 +val it = "x ~= 0" : string*)
1.276 +
1.277 +(*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
1.278 + the arguments: thus special handling by 'fun eval_binop'*)
1.279 +(*("ident" ,("Atools.ident",eval_ident "#ident_")):calc*)
1.280 +fun eval_ident (thmid:string) "Atools.ident" (t as
1.281 + (Const (op0,t0) $ t1 $ t2 )) thy =
1.282 + if t1 = t2
1.283 + then Some (mk_thmid thmid op0
1.284 + ("("^(Sign.string_of_term (sign_of thy) t1)^")")
1.285 + ("("^(Sign.string_of_term (sign_of thy) t2)^")"),
1.286 + Trueprop $ (mk_equality (t, true_as_term)))
1.287 + else Some (mk_thmid thmid op0
1.288 + ("("^(Sign.string_of_term (sign_of thy) t1)^")")
1.289 + ("("^(Sign.string_of_term (sign_of thy) t2)^")"),
1.290 + Trueprop $ (mk_equality (t, false_as_term)))
1.291 + | eval_ident _ _ _ _ = None;
1.292 +(* TODO
1.293 +> val t = str2term "x =!= 0";
1.294 +> val Some (str, t') = eval_ident "ident_" "b" t thy;
1.295 +> term2str t';
1.296 +val str = "ident_(x)_(0)" : string
1.297 +val it = "(x =!= 0) = False" : string
1.298 +> val t = str2term "1 =!= 0";
1.299 +> val Some (str, t') = eval_ident "ident_" "b" t thy;
1.300 +> term2str t';
1.301 +val str = "ident_(1)_(0)" : string
1.302 +val it = "(1 =!= 0) = False" : string
1.303 +> val t = str2term "0 =!= 0";
1.304 +> val Some (str, t') = eval_ident "ident_" "b" t thy;
1.305 +> term2str t';
1.306 +val str = "ident_(0)_(0)" : string
1.307 +val it = "(0 =!= 0) = True" : string
1.308 +*)
1.309 +
1.310 +(*.evaluate identity of terms, which stay ready for evaluation in turn;
1.311 + thus returns False only for atoms.*)
1.312 +(*("equal" ,("op =",eval_equal "#equal_")):calc*)
1.313 +fun eval_equal (thmid:string) "op =" (t as
1.314 + (Const (op0,t0) $ t1 $ t2 )) thy =
1.315 + if t1 = t2
1.316 + then ((*writeln"... eval_equal: t1 = t2 --> True";*)
1.317 + Some (mk_thmid thmid op0
1.318 + ("("^(Sign.string_of_term (sign_of thy) t1)^")")
1.319 + ("("^(Sign.string_of_term (sign_of thy) t2)^")"),
1.320 + Trueprop $ (mk_equality (t, true_as_term)))
1.321 + )
1.322 + else (case (is_atom t1, is_atom t2) of
1.323 + (true, true) =>
1.324 + ((*writeln"... eval_equal: t1<>t2, is_atom t1,t2 --> False";*)
1.325 + Some (mk_thmid thmid op0
1.326 + ("("^(term2str t1)^")") ("("^(term2str t2)^")"),
1.327 + Trueprop $ (mk_equality (t, false_as_term)))
1.328 + )
1.329 + | _ => ((*writeln"... eval_equal: t1<>t2, NOT is_atom t1,t2 --> go-on";*)
1.330 + None))
1.331 + | eval_equal _ _ _ _ = (writeln"... eval_equal: error-exit";
1.332 + None);
1.333 +(*
1.334 +val t = str2term "x ~= 0";
1.335 +val None = eval_equal "equal_" "b" t thy;
1.336 +
1.337 +
1.338 +> val t = str2term "(x + 1) = (x + 1)";
1.339 +> val Some (str, t') = eval_equal "equal_" "b" t thy;
1.340 +> term2str t';
1.341 +val str = "equal_(x + 1)_(x + 1)" : string
1.342 +val it = "(x + 1 = x + 1) = True" : string
1.343 +> val t = str2term "x = 0";
1.344 +> val None = eval_equal "equal_" "b" t thy;
1.345 +
1.346 +> val t = str2term "1 = 0";
1.347 +> val Some (str, t') = eval_equal "equal_" "b" t thy;
1.348 +> term2str t';
1.349 +val str = "equal_(1)_(0)" : string
1.350 +val it = "(1 = 0) = False" : string
1.351 +> val t = str2term "0 = 0";
1.352 +> val Some (str, t') = eval_equal "equal_" "b" t thy;
1.353 +> term2str t';
1.354 +val str = "equal_(0)_(0)" : string
1.355 +val it = "(0 = 0) = True" : string
1.356 +*)
1.357 +
1.358 +
1.359 +(** evaluation on the metalevel **)
1.360 +
1.361 +(*. evaluate HOL.divide .*)
1.362 +(*("divide_" ,("HOL.divide" ,eval_cancel "#divide_"))*)
1.363 +fun eval_cancel (thmid:string) "HOL.divide" (t as
1.364 + (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
1.365 + (case (int_of_str n1, int_of_str n2) of
1.366 + (Some n1', Some n2') =>
1.367 + let
1.368 + val sg = sign2 n1' n2';
1.369 + val (T1,T2,Trange) = dest_binop_typ t0;
1.370 + val gcd' = gcd (abs n1') (abs n2');
1.371 + in if gcd' = abs n2'
1.372 + then let val rhs = term_of_num Trange (sg * (abs n1') div gcd')
1.373 + val prop = Trueprop $ (mk_equality (t, rhs))
1.374 + in Some (mk_thmid thmid op0 n1 n2, prop) end
1.375 + else if 0 < n2' andalso gcd' = 1 then None
1.376 + else let val rhs = num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
1.377 + ((abs n2') div gcd')
1.378 + val prop = Trueprop $ (mk_equality (t, rhs))
1.379 + in Some (mk_thmid thmid op0 n1 n2, prop) end
1.380 + end
1.381 + | _ => ((*writeln"@@@ eval_cancel None";*)None))
1.382 +
1.383 + | eval_cancel _ _ _ _ = None;
1.384 +
1.385 +(*. get the argument from a function-definition.*)
1.386 +(*("argument_in" ,("Atools.argument'_in",
1.387 + eval_argument_in "Atools.argument'_in"))*)
1.388 +fun eval_argument_in _ "Atools.argument'_in"
1.389 + (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
1.390 + if is_Free arg (*could be something to be simplified before*)
1.391 + then Some (term2str t ^ " = " ^ term2str arg,
1.392 + Trueprop $ (mk_equality (t, arg)))
1.393 + else None
1.394 + | eval_argument_in _ _ _ _ = None;
1.395 +
1.396 +(*.check if the function-identifier of the first argument matches
1.397 + the function-identifier of the lhs of the second argument.*)
1.398 +(*("sameFunId" ,("Atools.sameFunId",
1.399 + eval_same_funid "Atools.sameFunId"))*)
1.400 +fun eval_sameFunId _ "Atools.sameFunId"
1.401 + (p as Const ("Atools.sameFunId",_) $
1.402 + (f1 $ _) $
1.403 + (Const ("op =", _) $ (f2 $ _) $ _)) _ =
1.404 + if f1 = f2
1.405 + then Some ((term2str p) ^ " = True",
1.406 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.407 + else Some ((term2str p) ^ " = False",
1.408 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.409 +| eval_sameFunId _ _ _ _ = None;
1.410 +
1.411 +
1.412 +(*.from a list of fun-definitions "f x = ..." as 2nd argument
1.413 + filter the elements with the same fun-identfier in "f y"
1.414 + as the fst argument;
1.415 + this is, because Isabelles filter takes more than 1 sec.*)
1.416 +fun same_funid f1 (Const ("op =", _) $ (f2 $ _) $ _) = f1 = f2
1.417 + | same_funid f1 t = raise error ("same_funid called with t = ("
1.418 + ^term2str f1^") ("^term2str t^")");
1.419 +(*("filter_sameFunId" ,("Atools.filter'_sameFunId",
1.420 + eval_filter_sameFunId "Atools.filter'_sameFunId"))*)
1.421 +fun eval_filter_sameFunId _ "Atools.filter'_sameFunId"
1.422 + (p as Const ("Atools.filter'_sameFunId",_) $
1.423 + (fid $ _) $ fs) _ =
1.424 + let val fs' = ((list2isalist HOLogic.boolT) o
1.425 + (filter (same_funid fid))) (isalist2list fs)
1.426 + in Some (term2str (mk_equality (p, fs')),
1.427 + Trueprop $ (mk_equality (p, fs'))) end
1.428 +| eval_filter_sameFunId _ _ _ _ = None;
1.429 +
1.430 +
1.431 +(*make a list of terms to a sum*)
1.432 +fun list2sum [] = error ("list2sum called with []")
1.433 + | list2sum [s] = s
1.434 + | list2sum (s::ss) =
1.435 + let fun sum su [s'] =
1.436 + Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
1.437 + $ su $ s'
1.438 + | sum su (s'::ss') =
1.439 + sum (Const ("op +", [HOLogic.realT,HOLogic.realT]--->HOLogic.realT)
1.440 + $ su $ s') ss'
1.441 + in sum s ss end;
1.442 +
1.443 +(*make a list of equalities to the sum of the lhs*)
1.444 +(*("boollist2sum" ,("Atools.boollist2sum" ,eval_boollist2sum "")):calc*)
1.445 +fun eval_boollist2sum _ "Atools.boollist2sum"
1.446 + (p as Const ("Atools.boollist2sum", _) $
1.447 + (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
1.448 + let val isal = isalist2list l
1.449 + val lhss = map lhs isal
1.450 + val sum = list2sum lhss
1.451 + in Some ((term2str p) ^ " = " ^ (term2str sum),
1.452 + Trueprop $ (mk_equality (p, sum)))
1.453 + end
1.454 +| eval_boollist2sum _ _ _ _ = None;
1.455 +
1.456 +
1.457 +
1.458 +local
1.459 +
1.460 +open Term;
1.461 +
1.462 +in
1.463 +fun termlessI (_:subst) uv = termless uv;
1.464 +fun term_ordI (_:subst) uv = term_ord uv;
1.465 +end;
1.466 +
1.467 +
1.468 +(** rule set, for evaluating list-expressions in scripts 8.01.02 **)
1.469 +
1.470 +
1.471 +val list_rls =
1.472 + append_rls "list_rls" list_rls
1.473 + [Calc ("op *",eval_binop "#mult_"),
1.474 + Calc ("op +", eval_binop "#add_"),
1.475 + Calc ("op <",eval_equ "#less_"),
1.476 + Calc ("op <=",eval_equ "#less_equal_"),
1.477 + Calc ("Atools.ident",eval_ident "#ident_"),
1.478 + Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*)
1.479 +
1.480 + Calc ("Tools.Vars",eval_var "#Vars_"),
1.481 +
1.482 + Thm ("if_True",num_str if_True),
1.483 + Thm ("if_False",num_str if_False)
1.484 + ];
1.485 +
1.486 +ruleset' := overwritelthy thy (!ruleset',
1.487 + [("list_rls",list_rls)
1.488 + ]);
1.489 +
1.490 +(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*)
1.491 +val tless_true = dummy_ord;
1.492 +rew_ord' := overwritel (!rew_ord',
1.493 + [("tless_true", tless_true),
1.494 + ("e_rew_ord'", tless_true),
1.495 + ("dummy_ord", dummy_ord)]);
1.496 +
1.497 +val calculate_Atools =
1.498 + append_rls "calculate_Atools" e_rls
1.499 + [Calc ("op <",eval_equ "#less_"),
1.500 + Calc ("op <=",eval_equ "#less_equal_"),
1.501 + Calc ("op =",eval_equal "#equal_"),
1.502 +
1.503 + Thm ("real_unari_minus",num_str real_unari_minus),
1.504 + Calc ("op +",eval_binop "#add_"),
1.505 + Calc ("op -",eval_binop "#sub_"),
1.506 + Calc ("op *",eval_binop "#mult_")
1.507 + ];
1.508 +
1.509 +val Atools_erls =
1.510 + append_rls "Atools_erls" e_rls
1.511 + [Calc ("op =",eval_equal "#equal_"),
1.512 + Thm ("not_true",num_str not_true),
1.513 + Thm ("not_false",num_str not_false),
1.514 + Thm ("and_true",and_true),
1.515 + Thm ("and_false",and_false),
1.516 + Thm ("or_true",or_true),
1.517 + Thm ("or_false",or_false),
1.518 +
1.519 + Thm ("rat_leq1",rat_leq1),
1.520 + Thm ("rat_leq2",rat_leq2),
1.521 + Thm ("rat_leq3",rat_leq3),
1.522 + Thm ("refl",num_str refl),
1.523 + Thm ("le_refl",num_str le_refl),
1.524 + Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
1.525 +
1.526 + Calc ("op <",eval_equ "#less_"),
1.527 + Calc ("op <=",eval_equ "#less_equal_"),
1.528 +
1.529 + Calc ("Atools.ident",eval_ident "#ident_"),
1.530 + Calc ("Atools.is'_const",eval_const "#is_const_"),
1.531 + Calc ("Atools.occurs'_in",eval_occurs_in ""),
1.532 + Calc ("Tools.matches",eval_matches "")
1.533 + ];
1.534 +
1.535 +val Atools_crls =
1.536 + append_rls "Atools_crls" e_rls
1.537 + [Calc ("op =",eval_equal "#equal_"),
1.538 + Thm ("not_true",num_str not_true),
1.539 + Thm ("not_false",num_str not_false),
1.540 + Thm ("and_true",and_true),
1.541 + Thm ("and_false",and_false),
1.542 + Thm ("or_true",or_true),
1.543 + Thm ("or_false",or_false),
1.544 +
1.545 + Thm ("rat_leq1",rat_leq1),
1.546 + Thm ("rat_leq2",rat_leq2),
1.547 + Thm ("rat_leq3",rat_leq3),
1.548 + Thm ("refl",num_str refl),
1.549 + Thm ("le_refl",num_str le_refl),
1.550 + Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
1.551 +
1.552 + Calc ("op <",eval_equ "#less_"),
1.553 + Calc ("op <=",eval_equ "#less_equal_"),
1.554 +
1.555 + Calc ("Atools.ident",eval_ident "#ident_"),
1.556 + Calc ("Atools.is'_const",eval_const "#is_const_"),
1.557 + Calc ("Atools.occurs'_in",eval_occurs_in ""),
1.558 + Calc ("Tools.matches",eval_matches "")
1.559 + ];
1.560 +
1.561 +(*val atools_erls = ... waere zu testen ...
1.562 + merge_rls calculate_Atools
1.563 + (append_rls Atools_erls (*i.A. zu viele rules*)
1.564 + [Calc ("Atools.ident",eval_ident "#ident_"),
1.565 + Calc ("Atools.is'_const",eval_const "#is_const_"),
1.566 + Calc ("Atools.occurs'_in",
1.567 + eval_occurs_in "#occurs_in"),
1.568 + Calc ("Tools.matches",eval_matches "#matches")
1.569 + ] (*i.A. zu viele rules*)
1.570 + );*)
1.571 +(* val atools_erls = prep_rls(
1.572 + Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
1.573 + erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
1.574 + rules = [Thm ("refl",num_str refl),
1.575 + Thm ("le_refl",num_str le_refl),
1.576 + Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
1.577 + Thm ("not_true",num_str not_true),
1.578 + Thm ("not_false",num_str not_false),
1.579 + Thm ("and_true",and_true),
1.580 + Thm ("and_false",and_false),
1.581 + Thm ("or_true",or_true),
1.582 + Thm ("or_false",or_false),
1.583 + Thm ("and_commute",num_str and_commute),
1.584 + Thm ("or_commute",num_str or_commute),
1.585 +
1.586 + Calc ("op <",eval_equ "#less_"),
1.587 + Calc ("op <=",eval_equ "#less_equal_"),
1.588 +
1.589 + Calc ("Atools.ident",eval_ident "#ident_"),
1.590 + Calc ("Atools.is'_const",eval_const "#is_const_"),
1.591 + Calc ("Atools.occurs'_in",eval_occurs_in ""),
1.592 + Calc ("Tools.matches",eval_matches "")
1.593 + ],
1.594 + scr = Script ((term_of o the o (parse thy))
1.595 + "empty_script")
1.596 + }:rls);
1.597 +ruleset' := overwritelth thy
1.598 + (!ruleset',
1.599 + [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)
1.600 + ]);
1.601 +*)
1.602 +"******* Atools.ML end *******";
1.603 +
1.604 +calclist':= overwritel (!calclist',
1.605 + [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
1.606 + ("some_occur_in",
1.607 + ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
1.608 + ("is_atom" ,("Atools.is'_atom",eval_is_atom "#is_atom_")),
1.609 + ("is_even" ,("Atools.is'_even",eval_is_even "#is_even_")),
1.610 + ("is_const" ,("Atools.is'_const",eval_const "#is_const_")),
1.611 + ("le" ,("op <" ,eval_equ "#less_")),
1.612 + ("leq" ,("op <=" ,eval_equ "#less_equal_")),
1.613 + ("ident" ,("Atools.ident",eval_ident "#ident_")),
1.614 + ("equal" ,("op =",eval_equal "#equal_")),
1.615 + ("plus" ,("op +" ,eval_binop "#add_")),
1.616 + ("minus" ,("op -",eval_binop "#sub_")), (*040207 only for prep_rls
1.617 + no script with "minus"*)
1.618 + ("times" ,("op *" ,eval_binop "#mult_")),
1.619 + ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")),
1.620 + ("power_" ,("Atools.pow" ,eval_binop "#power_")),
1.621 + ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
1.622 + ]);
1.623 +
1.624 +val list_rls = prep_rls(
1.625 + merge_rls "list_erls"
1.626 + (Rls {id="replaced",preconds = [],
1.627 + rew_ord = ("termlessI", termlessI),
1.628 + erls = Rls {id="list_elrs", preconds = [],
1.629 + rew_ord = ("termlessI",termlessI),
1.630 + erls = e_rls,
1.631 + srls = Erls, calc = [], (*asm_thm = [],*)
1.632 + rules = [Calc ("op +", eval_binop "#add_"),
1.633 + Calc ("op <",eval_equ "#less_")
1.634 + (* ~~~~~~ for nth_Cons_*)
1.635 + ],
1.636 + scr = EmptyScr},
1.637 + srls = Erls, calc = [], (*asm_thm = [], *)
1.638 + rules = [], scr = EmptyScr})
1.639 + list_rls);
1.640 +ruleset' := overwritelthy thy (!ruleset', [("list_rls", list_rls)]);
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/sml/IsacKnowledge/Descript.thy Fri Dec 28 14:57:38 2007 +0100
2.3 @@ -0,0 +1,55 @@
2.4 +(* descriptions for items in problem-types
2.5 + WN 1.3.00
2.6 + + see WN, Reactive User-Guidance ... Vers. Oct.2000 p.48 ff
2.7 +*)
2.8 +(* descriptions for items in model-patterns of problems and in method's guards
2.9 + author: Walther Neuper
2.10 + 000301,
2.11 + (c) due to copyright terms
2.12 +
2.13 +remove_thy"Descript";
2.14 +use_thy"IsacKnowledge/Descript";
2.15 +use_thy_only"IsacKnowledge/Descript";
2.16 +
2.17 +remove_thy"Typefix";
2.18 +use_thy"IsacKnowledge/Isac";
2.19 +*)
2.20 +
2.21 +Descript = Script +
2.22 +
2.23 +consts
2.24 +
2.25 + someList :: 'a list => unl (*not for elementwise input, eg. inssort*)
2.26 +
2.27 + additionalRels :: bool list => una
2.28 + boundVariable :: real => una
2.29 +(*derivative :: 'a => toreal 28.11.00*)
2.30 + derivative :: real => una
2.31 + equalities :: bool list => tobooll (*WN071228 see fixedValues*)
2.32 + equality :: bool => una
2.33 + errorBound :: bool => nam
2.34 +
2.35 + fixedValues :: bool list => nam
2.36 + functionEq :: bool => una (*6.5.03: functionTerm -> functionEq*)
2.37 + antiDerivative :: bool => una
2.38 + functionOf :: real => una
2.39 +(*functionTerm :: 'a => toreal 28.11.00*)
2.40 + functionTerm :: real => una (*6.5.03: functionTerm -> functionEq*)
2.41 + interval :: real set => una
2.42 + maxArgument :: bool => toreal
2.43 + maximum :: real => toreal
2.44 +
2.45 + relations :: bool list => una
2.46 + solutions :: bool list => toreall
2.47 +(*solution :: bool => toreal WN0509 bool list=> toreall --->EqSystem*)
2.48 + solveFor :: real => una
2.49 + differentiateFor:: real => una
2.50 + unknown :: 'a => unknow
2.51 + valuesFor :: real list => toreall
2.52 +
2.53 + realTestGiven :: real => una
2.54 + realTestFind :: real => una
2.55 + boolTestGiven :: bool => una
2.56 + boolTestFind :: bool => una
2.57 +
2.58 +end
2.59 \ No newline at end of file
3.1 --- a/src/sml/IsacKnowledge/PolyMinus.ML Fri Dec 28 12:10:09 2007 +0100
3.2 +++ b/src/sml/IsacKnowledge/PolyMinus.ML Fri Dec 28 14:57:38 2007 +0100
3.3 @@ -170,7 +170,7 @@
3.4 (** problems **)
3.5
3.6 store_pbt
3.7 - (prep_pbt Poly.thy "pbl_vereinf_poly" [] e_pblID
3.8 + (prep_pbt PolyMinus.thy "pbl_vereinf_poly" [] e_pblID
3.9 (["polynom","vereinfachen"],
3.10 [("#Given" ,["term t_"]),
3.11 ("#Where" ,["t_ is_polyexp"]),
3.12 @@ -181,12 +181,42 @@
3.13 Some "Vereinfache t_",
3.14 [["simplification","for_polynomials","with_minus"]]));
3.15
3.16 +store_pbt
3.17 + (prep_pbt PolyMinus.thy "pbl_probe" [] e_pblID
3.18 + (["probe"],
3.19 + [], Erls, None, []));
3.20 +
3.21 +store_pbt
3.22 + (prep_pbt PolyMinus.thy "pbl_probe_poly" [] e_pblID
3.23 + (["polynom","probe"],
3.24 + [("#Given" ,["Pruefe e_", "mitWert ws_"]),
3.25 + ("#Where" ,["e_ is_polyexp"]),
3.26 + ("#Find" ,["Geprueft p_"])
3.27 + ],
3.28 + append_rls "prls_pbl_probe_poly"
3.29 + e_rls [(*for preds in where_*)
3.30 + Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
3.31 + Some "Probe e_ ws_",
3.32 + [["probe","fuer_polynom"]]));
3.33 +
3.34 +store_pbt
3.35 + (prep_pbt PolyMinus.thy "pbl_probe_bruch" [] e_pblID
3.36 + (["bruch","probe"],
3.37 + [("#Given" ,["Pruefe e_", "mitWert ws_"]),
3.38 + ("#Where" ,["e_ is_ratpolyexp"]),
3.39 + ("#Find" ,["Geprueft p_"])
3.40 + ],
3.41 + append_rls "prls_pbl_probe_bruch"
3.42 + e_rls [(*for preds in where_*)
3.43 + Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
3.44 + Some "Probe e_ ws_",
3.45 + [["probe","fuer_bruch"]]));
3.46
3.47
3.48 (** methods **)
3.49
3.50 store_met
3.51 - (prep_met Poly.thy "met_simp_poly_minus" [] e_metID
3.52 + (prep_met PolyMinus.thy "met_simp_poly_minus" [] e_metID
3.53 (["simplification","for_polynomials","with_minus"],
3.54 [("#Given" ,["term t_"]),
3.55 ("#Where" ,["t_ is_polyexp"]),
3.56 @@ -202,3 +232,47 @@
3.57 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \
3.58 \ (Try (Rewrite_Set verschoenere False))) t_)"
3.59 ));
3.60 +
3.61 +store_met
3.62 + (prep_met PolyMinus.thy "met_probe" [] e_metID
3.63 + (["probe"],
3.64 + [],
3.65 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
3.66 + prls = Erls, crls = e_rls, nrls = Erls},
3.67 + "empty_script"));
3.68 +
3.69 +store_met
3.70 + (prep_met PolyMinus.thy "met_probe_poly" [] e_metID
3.71 + (["probe","fuer_polynom"],
3.72 + [("#Given" ,["Pruefe e_", "mitWert ws_"]),
3.73 + ("#Where" ,["e_ is_polyexp"]),
3.74 + ("#Find" ,["Geprueft p_"])
3.75 + ],
3.76 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
3.77 + prls = append_rls "prls_met_probe_bruch"
3.78 + e_rls [(*for preds in where_*)
3.79 + Calc ("Rational.is'_ratpolyexp",
3.80 + eval_is_ratpolyexp "")],
3.81 + crls = e_rls, nrls = Erls},
3.82 +"Script ProbeScript (e_::bool) (ws_::bool list) = \
3.83 +\ (let e_ = Take e_; \
3.84 +\ e_ = Substitute ws_ e_ \
3.85 +\ in (Repeat((Try (Repeat (Calculate times))) @@ \
3.86 +\ (Try (Repeat (Calculate plus ))) @@ \
3.87 +\ (Try (Repeat (Calculate minus))))) e_)"
3.88 +));
3.89 +
3.90 +store_met
3.91 + (prep_met PolyMinus.thy "met_probe_bruch" [] e_metID
3.92 + (["probe","fuer_bruch"],
3.93 + [("#Given" ,["Pruefe e_", "mitWert ws_"]),
3.94 + ("#Where" ,["e_ is_ratpolyexp"]),
3.95 + ("#Find" ,["Geprueft p_"])
3.96 + ],
3.97 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
3.98 + prls = append_rls "prls_met_probe_bruch"
3.99 + e_rls [(*for preds in where_*)
3.100 + Calc ("Rational.is'_ratpolyexp",
3.101 + eval_is_ratpolyexp "")],
3.102 + crls = e_rls, nrls = Erls},
3.103 + "empty_script"));
4.1 --- a/src/sml/IsacKnowledge/PolyMinus.thy Fri Dec 28 12:10:09 2007 +0100
4.2 +++ b/src/sml/IsacKnowledge/PolyMinus.thy Fri Dec 28 14:57:38 2007 +0100
4.3 @@ -6,12 +6,27 @@
4.4 use_thy"IsacKnowledge/Isac";
4.5 *)
4.6
4.7 -PolyMinus = Poly +
4.8 +PolyMinus = (*Poly// due to "is_ratpolyexp"..*) Rational +
4.9
4.10 consts
4.11
4.12 - kleiner :: "['a, 'a] => bool" ("_ kleiner _")
4.13 - ist'_monom :: "'a => bool" ("_ ist'_monom")
4.14 + (*predicates for conditions in rewriting*)
4.15 + kleiner :: "['a, 'a] => bool" ("_ kleiner _")
4.16 + ist'_monom :: "'a => bool" ("_ ist'_monom")
4.17 +
4.18 + (*the CAS-command*)
4.19 + Probe :: "[bool, bool list] => bool"
4.20 + (*"Probe (3*a+2*b+a = 4*a+2*b) [a=1,b=2]"*)
4.21 +
4.22 + (*descriptions for the pbl and met*)
4.23 + Pruefe :: bool => una
4.24 + mitWert :: bool list => tobooll
4.25 + Geprueft :: bool => una
4.26 +
4.27 + (*Script-name*)
4.28 + ProbeScript :: "[bool, bool list, bool] \
4.29 + \=> bool"
4.30 + ("((Script ProbeScript (_ _ =))// (_))" 9)
4.31
4.32 rules
4.33
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/sml/Scripts/scrtools.sml Fri Dec 28 14:57:38 2007 +0100
5.3 @@ -0,0 +1,468 @@
5.4 +(* tools which depend on Script.thy and thus are not in term_G.sml
5.5 + (c) Walther Neuper 2000
5.6 +
5.7 +use"Scripts/scrtools.sml";
5.8 +use"scrtools.sml";
5.9 +*)
5.10 +
5.11 +
5.12 +fun is_reall_dsc
5.13 + (Const(_,Type("fun",[Type("List.list",
5.14 + [Type ("real",[])]),_]))) = true
5.15 + | is_reall_dsc
5.16 + (Const(_,Type("fun",[Type("List.list",
5.17 + [Type ("real",[])]),_])) $ t) = true
5.18 + | is_reall_dsc _ = false;
5.19 +fun is_booll_dsc
5.20 + (Const(_,Type("fun",[Type("List.list",
5.21 + [Type ("bool",[])]),_]))) = true
5.22 + | is_booll_dsc
5.23 + (Const(_,Type("fun",[Type("List.list",
5.24 + [Type ("bool",[])]),_])) $ t) = true
5.25 + | is_booll_dsc _ = false;
5.26 +(*
5.27 +> val t = (term_of o the o (parse thy)) "relations";
5.28 +> atomtyp (type_of t);
5.29 +*** Type (fun,[
5.30 +*** Type (List.list,[
5.31 +*** Type (bool,[])
5.32 +*** ]
5.33 +*** Type (Tools.una,[])
5.34 +*** ]
5.35 +> is_booll_dsc t;
5.36 +val it = true : bool
5.37 +> is_reall_dsc t;
5.38 +val it = false : bool
5.39 +*)
5.40 +
5.41 +fun is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_]))) = true
5.42 + | is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_])) $ t) = true
5.43 + (*WN:8.5.03: ??? ~~~~ ???*)
5.44 + | is_list_dsc _ = false;
5.45 +(*
5.46 +> val t = str2term "someList";
5.47 +> is_list_dsc t;
5.48 +val it = true : bool
5.49 +
5.50 +> val t = (term_of o the o (parse thy))
5.51 + "additional_relations [a=b,c=(d::real)]";
5.52 +> is_list_dsc t;
5.53 +val it = true : bool
5.54 +> is_list_dsc (head_of t);
5.55 +val it = true : bool
5.56 +
5.57 +> val t = (term_of o the o (parse thy))"max_relation (A=#2*a*b-a^^^#2)";
5.58 +> is_list_dsc t;
5.59 +val it = false : bool
5.60 +> is_list_dsc (head_of t);
5.61 +val it = false : bool
5.62 +> val t = (term_of o the o (parse thy)) "testdscforlist";
5.63 +> is_list_dsc (head_of t);
5.64 +val it = true : bool
5.65 +*)
5.66 +
5.67 +
5.68 +fun is_unl (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true
5.69 + | is_unl _ = false;
5.70 +(*
5.71 +> val t = str2term "someList"; is_unl t;
5.72 +val it = true : bool
5.73 +> val t = (term_of o the o (parse thy)) "maximum";
5.74 +> is_unl t;
5.75 +val it = false : bool
5.76 +*)
5.77 +
5.78 +fun is_dsc (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) = true
5.79 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.una",_)]))) = true
5.80 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true
5.81 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.str",_)]))) = true
5.82 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) = true
5.83 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))= true
5.84 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.tobooll",_)])))= true
5.85 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.unknow",_)])))= true
5.86 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.cpy",_)])))= true
5.87 + | is_dsc _ = false;
5.88 +fun is_dsc term =
5.89 + (case (range_type o type_of) term of
5.90 + Type("Tools.nam",_) => true
5.91 + | Type("Tools.una",_) => true
5.92 + | Type("Tools.unl",_) => true
5.93 + | Type("Tools.str",_) => true
5.94 + | Type("Tools.toreal",_) => true
5.95 + | Type("Tools.toreall",_) => true
5.96 + | Type("Tools.tobooll",_) => true
5.97 + | Type("Tools.unknow",_) => true
5.98 + | Type("Tools.cpy",_) => true
5.99 + | _ => false)
5.100 + handle Match => false;
5.101 +
5.102 +
5.103 +(*
5.104 +val t as t1 $ t2 = str2term "antiDerivativeName M_b";
5.105 +val Const (_, Type ("fun", [Type ("fun", _), Type ("Tools.una",[])])) $ _ = t;
5.106 +is_dsc t1;
5.107 +
5.108 +> val t = (term_of o the o (parse thy)) "maximum";
5.109 +> is_dsc t;
5.110 +val it = true : bool
5.111 +> val t = (term_of o the o (parse thy)) "testdscforlist";
5.112 +> is_dsc t;
5.113 +val it = true : bool
5.114 +
5.115 +> val t = (head_of o term_of o the o (parse thy)) "maximum A";
5.116 +> is_dsc t;
5.117 +val it = true : bool
5.118 +> val t = (head_of o term_of o the o (parse thy))
5.119 + "fixedValues [R=(R::real)]";
5.120 +> is_dsc t;
5.121 +val it = true : bool
5.122 +*)
5.123 +
5.124 +
5.125 +(*make the term 'Subproblem (domID, pblID)' to a formula for frontend;
5.126 + needs to be here after def. Subproblem in Script.thy*)
5.127 +val t as (subpbl_t $ (pair_t $ Free (domID,_) $ pblID)) =
5.128 + (term_of o the o (parse Script.thy))
5.129 + "Subproblem (Isac,[equation,univar])";
5.130 +val t as (pbl_t $ _) =
5.131 + (term_of o the o (parse Script.thy))
5.132 + "Problem (Isac,[equation,univar])";
5.133 +val Free (_, ID_type) = (term_of o the o (parse Script.thy)) "x::ID";
5.134 +
5.135 +
5.136 +fun subpbl domID pblID =
5.137 + subpbl_t $ (pair_t $ Free (domID,ID_type) $
5.138 + (((list2isalist ID_type) o (map (mk_free ID_type))) pblID));
5.139 +(*> subpbl "Isac" ["equation","univar"] = t;
5.140 +val it = true : bool *)
5.141 +
5.142 +
5.143 +fun pblterm (domID:domID) (pblID:pblID) =
5.144 + pbl_t $ (pair_t $ Free (domID,ID_type) $
5.145 + (((list2isalist ID_type) o (map (mk_free ID_type))) pblID));
5.146 +
5.147 +
5.148 +(**.construct scr-env from scr(created automatically) and Rewrite_Set.**)
5.149 +
5.150 +fun one_scr_arg (Const _ $ arg $ _) = arg
5.151 + | one_scr_arg t = raise error ("one_scr_arg: called by "^(term2str t));
5.152 +fun two_scr_arg (Const _ $ a1 $ a2 $ _) = (a1, a2)
5.153 + | two_scr_arg t = raise error ("two_scr_arg: called by "^(term2str t));
5.154 +
5.155 +
5.156 +(**.generate calc from a script.**)
5.157 +
5.158 +(*.instantiate a stactic or scriptexpr, and ev. attach (curried) argument
5.159 +args:
5.160 + E environment
5.161 + v current value, is attached to curried stactics
5.162 + stac stactic to be instantiated
5.163 +precond:
5.164 + not (a = None) /\ (v = e_term) /\ (stac curried, i.e. without last arg.)
5.165 + this ........................ is the initialization for assy with l=[],
5.166 + but the 1st stac is
5.167 + (a) curried: then (a = Some _), or
5.168 + (b) not curried: then the values of the initialization are not used
5.169 +.*)
5.170 +datatype stacexpr = STac of term | Expr of term
5.171 +fun rep_stacexpr (STac t ) = t
5.172 + | rep_stacexpr (Expr t) =
5.173 + raise error ("rep_stacexpr called with t= "^(term2str t));
5.174 +
5.175 +type env = (term * term) list;
5.176 +
5.177 +(*update environment; t <> empty if coming from listexpr*)
5.178 +fun upd_env (env:env) (v,t) =
5.179 + let val env' = if t = e_term then env else overwrite (env,(v,t));
5.180 + (*val _= writeln("### upd_env: = "^(subst2str env'));*)
5.181 + in env' end;
5.182 +
5.183 +(*.substitute the scripts environment in a leaf of the scripts parse-tree
5.184 + and attach the curried argument of a tactic, if any.
5.185 + a leaf is either a tactic or an 'exp' in 'let v = expr'
5.186 + where 'exp' does not contain a tactic.
5.187 +CAUTION: (1) currying with @@ requires 2 patterns for each tactic
5.188 + (2) the non-curried version must return None for a
5.189 + (3) non-matching patterns become an Expr by fall-through.
5.190 +WN060906 quick and dirty fix: due to (2) a is returned, too.*)
5.191 +fun subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _ ))=
5.192 + (None, STac (subst_atomic E t))
5.193 +
5.194 + | subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ ))=
5.195 + (a, (*in these cases we hope, that a = Some _*)
5.196 + STac (case a of Some a' => (subst_atomic E (t $ a'))
5.197 + | None => ((subst_atomic E t) $ v)))
5.198 +
5.199 + | subst_stacexpr E a v
5.200 + (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ _ )) =
5.201 + (None, STac (subst_atomic E t))
5.202 +
5.203 + | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _))=
5.204 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.205 + | None => ((subst_atomic E t) $ v)))
5.206 +
5.207 + | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ _ ))=
5.208 + (None, STac (subst_atomic E t))
5.209 +
5.210 + | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ )) =
5.211 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.212 + | None => ((subst_atomic E t) $ v)))
5.213 +
5.214 + | subst_stacexpr E a v
5.215 + (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ _ )) =
5.216 + (None, STac (subst_atomic E t))
5.217 +
5.218 + | subst_stacexpr E a v
5.219 + (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ )) =
5.220 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.221 + | None => ((subst_atomic E t) $ v)))
5.222 +
5.223 + | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ $ _ )) =
5.224 + (None, STac (subst_atomic E t))
5.225 +
5.226 + | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ )) =
5.227 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.228 + | None => ((subst_atomic E t) $ v)))
5.229 +
5.230 + | subst_stacexpr E a v
5.231 + (t as (Const("Script.Check'_elementwise",_) $ _ $ _ )) =
5.232 + (None, STac (subst_atomic E t))
5.233 +
5.234 + | subst_stacexpr E a v (t as (Const("Script.Check'_elementwise",_) $ _ )) =
5.235 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.236 + | None => ((subst_atomic E t) $ v)))
5.237 +
5.238 + | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_) $ _ )) =
5.239 + (None, STac (subst_atomic E t))
5.240 +
5.241 + | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_))) = (*t $ v*)
5.242 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.243 + | None => ((subst_atomic E t) $ v)))
5.244 +
5.245 + | subst_stacexpr E a v (t as (Const ("Script.SubProblem",_) $ _ $ _ )) =
5.246 + (None, STac (subst_atomic E t))
5.247 +
5.248 + | subst_stacexpr E a v (t as (Const ("Script.Take",_) $ _ )) =
5.249 + (None, STac (subst_atomic E t))
5.250 +
5.251 + | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ $ _ )) =
5.252 + (None, STac (subst_atomic E t))
5.253 +
5.254 + | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ )) =
5.255 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.256 + | None => ((subst_atomic E t) $ v)))
5.257 +
5.258 + (*now all tactics are matched out and this leaf must be without a tactic*)
5.259 + | subst_stacexpr E a v t =
5.260 + (a, Expr (subst_atomic (case a of Some a => upd_env E (a,v)
5.261 + | None => E) t));
5.262 +(*> val t = str2term "SubProblem(Test_, [linear, univariate, equation, test], [Test, solve_linear]) [bool_ e_, real_ v_]";
5.263 +> subst_stacexpr [] None e_term t;*)
5.264 +
5.265 +
5.266 +fun stacpbls (h $ body) =
5.267 + let
5.268 + fun scan ts (Const ("Let",_) $ e $ (Abs (v,T,b))) =
5.269 + (scan ts e) @ (scan ts b)
5.270 + | scan ts (Const ("If",_) $ c $ e1 $ e2) = (scan ts e1) @ (scan ts e2)
5.271 + | scan ts (Const ("Script.While",_) $ c $ e $ _) = scan ts e
5.272 + | scan ts (Const ("Script.While",_) $ c $ e) = scan ts e
5.273 + | scan ts (Const ("Script.Repeat",_) $ e $ _) = scan ts e
5.274 + | scan ts (Const ("Script.Repeat",_) $ e) = scan ts e
5.275 + | scan ts (Const ("Script.Try",_) $ e $ _) = scan ts e
5.276 + | scan ts (Const ("Script.Try",_) $ e) = scan ts e
5.277 + | scan ts (Const ("Script.Or",_) $e1 $ e2 $ _) =
5.278 + (scan ts e1) @ (scan ts e2)
5.279 + | scan ts (Const ("Script.Or",_) $e1 $ e2) =
5.280 + (scan ts e1) @ (scan ts e2)
5.281 + | scan ts (Const ("Script.Seq",_) $e1 $ e2 $ _) =
5.282 + (scan ts e1) @ (scan ts e2)
5.283 + | scan ts (Const ("Script.Seq",_) $e1 $ e2) =
5.284 + (scan ts e1) @ (scan ts e2)
5.285 + | scan ts t = case subst_stacexpr [] None e_term t of
5.286 + (_, STac _) => [t] | (_, Expr _) => []
5.287 + in (distinct o (scan [])) body end;
5.288 + (*sc = Solve_root_equation ...
5.289 +> val ts = stacpbls sc;
5.290 +> writeln (terms2str thy ts);
5.291 +["Rewrite square_equation_left True e_",
5.292 + "Rewrite_Set SqRoot_simplify False e_",
5.293 + "Rewrite_Set rearrange_assoc False e_",
5.294 + "Rewrite_Set isolate_root False e_",
5.295 + "Rewrite_Set norm_equation False e_",
5.296 + "Rewrite_Set_Inst [(bdv, v_)] isolate_bdv False e_"]
5.297 +*)
5.298 +
5.299 +
5.300 +
5.301 +fun is_calc (Const ("Script.Calculate",_) $ _) = true
5.302 + | is_calc (Const ("Script.Calculate",_) $ _ $ _) = true
5.303 + | is_calc _ = false;
5.304 +fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_
5.305 + | op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_) $ _) = op_
5.306 + | op_of_calc t = raise error ("op_of_calc called with"^term2str t);
5.307 +
5.308 +(*######################################################################
5.309 +
5.310 + val Script sc = (#scr o rep_rls) Test_simplify;
5.311 + val stacs = stacpbls sc;
5.312 +
5.313 + val calcs = filter is_calc stacs;
5.314 + val ids = map op_of_calc calcs;
5.315 + map (curry assoc1 (!calclist')) ids;
5.316 +
5.317 + (((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
5.318 + (filter is_calc) o stacpbls) sc):calc list;
5.319 +
5.320 +######################################################################*)
5.321 +
5.322 +(**.for automatic creation of scripts from rls.**)
5.323 +
5.324 +val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*)
5.325 + ((inst_abs thy) o term_of o the o (parse thy))
5.326 + "Script Stepwise (t_::'z) =\
5.327 + \(Repeat\
5.328 + \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
5.329 + \ (Try (Repeat (Rewrite real_add_commute False))) @@ \
5.330 + \ (Try (Repeat (Rewrite real_mult_commute False)))) \
5.331 + \ t_)";
5.332 +(*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body
5.333 +are inconsistent !!!*)
5.334 +val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*)
5.335 + ((inst_abs thy) o term_of o the o (parse thy))
5.336 + "Script Stepwise_inst (t_::'z) (v_::real) =\
5.337 + \(Repeat\
5.338 + \ ((Try (Repeat (Rewrite_Inst [(bdv,v_)] real_diff_minus False))) @@ \
5.339 + \ (Try (Repeat (Rewrite_Inst [(bdv,v_)] real_add_commute False))) @@\
5.340 + \ (Try (Repeat (Rewrite_Inst [(bdv,v_)] real_mult_commute False)))) \
5.341 + \ t_)";
5.342 +val Repeat $ _ =
5.343 + ((inst_abs thy) o term_of o the o (parseN thy))
5.344 + "Repeat (Rewrite real_diff_minus False t_)";
5.345 +val Try $ _ =
5.346 + ((inst_abs thy) o term_of o the o (parseN thy))
5.347 + "Try (Rewrite real_diff_minus False t_)";
5.348 +val Cal $ _ =
5.349 + ((inst_abs thy) o term_of o the o (parseN thy))
5.350 + "Calculate plus";
5.351 +val Rew $ (Free (_,IDtype)) $ _ $ t_ =
5.352 + ((inst_abs thy) o term_of o the o (parseN thy))
5.353 + "Rewrite real_diff_minus False t_";
5.354 +val Rew_Inst $ Subs $ _ $ _ =
5.355 + ((inst_abs thy) o term_of o the o (parseN thy))
5.356 + "Rewrite_Inst [(bdv,v_)] real_diff_minus False";
5.357 +val Rew_Set $ _ $ _ =
5.358 + ((inst_abs thy) o term_of o the o (parseN thy))
5.359 + "Rewrite_Set real_diff_minus False";
5.360 +val Rew_Set_Inst $ _ $ _ $ _ =
5.361 + ((inst_abs thy) o term_of o the o (parseN thy))
5.362 + "Rewrite_Set_Inst [(bdv,v_)] real_diff_minus False";
5.363 +val SEq $ _ $ _ $ _ =
5.364 + ((inst_abs thy) o term_of o the o (parseN thy))
5.365 + " ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
5.366 + \ (Try (Repeat (Rewrite real_add_commute False))) @@ \
5.367 + \ (Try (Repeat (Rewrite real_mult_commute False)))) t_";
5.368 +
5.369 +fun rule2stac _ (Thm (thmID, _)) =
5.370 + Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ HOLogic.false_const))
5.371 + | rule2stac calc (Calc (c, _)) =
5.372 + Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
5.373 + | rule2stac _ (Rls_ rls) =
5.374 + Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const);
5.375 +(*val t = rule2stac [] (Thm ("real_diff_minus", num_str real_diff_minus));
5.376 +atomt t; term2str t;
5.377 +val t = rule2stac calclist (Calc ("op +", eval_binop "#add_"));
5.378 +atomt t; term2str t;
5.379 +val t = rule2stac [] (Rls_ rearrange_assoc);
5.380 +atomt t; term2str t;
5.381 +*)
5.382 +fun rule2stac_inst _ (Thm (thmID, _)) =
5.383 + Try $ (Repeat $ (Rew_Inst $ Subs $ Free (thmID, IDtype) $
5.384 + HOLogic.false_const))
5.385 + | rule2stac_inst calc (Calc (c, _)) =
5.386 + Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype)))
5.387 + | rule2stac_inst _ (Rls_ rls) =
5.388 + Try $ (Rew_Set_Inst $ Subs $ Free (id_rls rls, IDtype) $
5.389 + HOLogic.false_const);
5.390 +(*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str real_diff_minus));
5.391 +atomt t; term2str t;
5.392 +val t = rule2stac_inst calclist (Calc ("op +", eval_binop "#add_"));
5.393 +atomt t; term2str t;
5.394 +val t = rule2stac_inst [] (Rls_ rearrange_assoc);
5.395 +atomt t; term2str t;
5.396 +*)
5.397 +
5.398 +(*for appropriate nesting take stacs in _reverse_ order*)
5.399 +fun @@@ sts [s] = SEq $ s $ sts
5.400 + | @@@ sts (s::ss) = @@@ (SEq $ s $ sts) ss;
5.401 +fun @@ [stac] = stac
5.402 + | @@ [s1, s2] = SEq $ s1 $ s2 (*---------vvv--*)
5.403 + | @@ stacs =
5.404 + let val s3::s2::ss = rev stacs
5.405 + in @@@ (SEq $ s2 $ s3) ss end;
5.406 +(*
5.407 + val rules = (#rules o rep_rls) isolate_root;
5.408 + val rs = map (rule2stac calclist) rules;
5.409 + val tt = @@ rs;
5.410 + atomt tt; writeln (term2str tt);
5.411 + *)
5.412 +
5.413 +val contains_bdv = (not o null o (filter is_bdv) o ids2str o #prop o rep_thm);
5.414 +
5.415 +(*.does a rule contain a 'bdv'; descend recursively into Rls_.*)
5.416 +fun contain_bdv [] = false
5.417 + | contain_bdv (Thm (_, thm)::rs) =
5.418 + if (not o contains_bdv) thm
5.419 + then contain_bdv rs
5.420 + else true
5.421 + | contain_bdv (Calc _ ::rs) = contain_bdv rs
5.422 + | contain_bdv (Rls_ rls ::rs) =
5.423 + contain_bdv (get_rules rls) orelse contain_bdv rs
5.424 + | contain_bdv (r::_) =
5.425 + raise error ("contain_bdv called with ["^(id_rule r)^",...]");
5.426 +
5.427 +
5.428 +fun rules2scr_Rls calc rules =
5.429 + if contain_bdv rules
5.430 + then ScrStep_inst $ Term $ Bdv $
5.431 + (Repeat $ (((@@ o (map (rule2stac_inst calc))) rules) $ t_))
5.432 + else ScrStep $ Term $
5.433 + (Repeat $ (((@@ o (map (rule2stac calc))) rules) $ t_));
5.434 +fun rules2scr_Seq calc rules =
5.435 + if contain_bdv rules
5.436 + then ScrStep_inst $ Term $ Bdv $
5.437 + (((@@ o (map (rule2stac_inst calc))) rules) $ t_)
5.438 + else ScrStep $ Term $
5.439 + (((@@ o (map (rule2stac calc))) rules) $ t_);
5.440 +
5.441 +(*.prepare the input for an rls for use:
5.442 + # generate a script for stepwise execution of the rls
5.443 + # filter the operators for Calc out of the script
5.444 + !!!use this function in ruleset' := !!! .*)
5.445 +fun prep_rls Erls = raise error "prep_rls not impl. for Erls"
5.446 + | prep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,rules,...}) =
5.447 + let val sc = (rules2scr_Rls (!calclist') rules)
5.448 + in Rls {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
5.449 + srls=srls,
5.450 + calc = (*FIXXXME.040207 use also for met*)
5.451 + ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
5.452 + (filter is_calc) o stacpbls) sc,
5.453 + rules=rules,
5.454 + scr = Script sc} end
5.455 + | prep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,rules,...}) =
5.456 + let val sc = (rules2scr_Seq (!calclist') rules)
5.457 + in Seq {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
5.458 + srls=srls,
5.459 + calc = ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
5.460 + (filter is_calc) o stacpbls) sc,
5.461 + rules=rules,
5.462 + scr = Script sc} end
5.463 + | prep_rls (Rrls {id,...}) =
5.464 + raise error ("prep_rls not required for Rrls \""^id^"\"");
5.465 +(*
5.466 + val Script sc = (#scr o rep_rls o prep_rls) isolate_root;
5.467 + (writeln o term2str) sc;
5.468 + val Script sc = (#scr o rep_rls o prep_rls) isolate_bdv;
5.469 + (writeln o term2str) sc;
5.470 + *)
5.471 +
6.1 --- a/src/smltest/IsacKnowledge/polyminus.sml Fri Dec 28 12:10:09 2007 +0100
6.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml Fri Dec 28 14:57:38 2007 +0100
6.3 @@ -17,6 +17,8 @@
6.4 "----------- build verschoenere ----------------------------------";
6.5 "----------- met simplification for_polynomials with_minus -------";
6.6 "----------- pbl polynom vereinfachen ----------------------------";
6.7 +"----------- met probe fuer_polynom ------------------------------";
6.8 +"----------- pbl polynom probe -----------------------------------";
6.9 "-----------------------------------------------------------------";
6.10 "-----------------------------------------------------------------";
6.11 "-----------------------------------------------------------------";
6.12 @@ -195,12 +197,41 @@
6.13 val ((pt,p),_) = get_calc 1;
6.14 if p = ([], Res) andalso
6.15 term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
6.16 -then () else raise error "biegelinie.sml: 1st biegelin.7.27 changed";
6.17 +then () else raise error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
6.18 show_pt pt;
6.19
6.20
6.21 +"----------- met probe fuer_polynom ------------------------------";
6.22 +"----------- met probe fuer_polynom ------------------------------";
6.23 +"----------- met probe fuer_polynom ------------------------------";
6.24 +val str =
6.25 +"Script ProbeScript (e_::bool) (ws_::bool list) =\
6.26 +\ (let e_ = Take e_; \
6.27 +\ e_ = Substitute ws_ e_ \
6.28 +\ in (Repeat((Try (Repeat (Calculate times))) @@ \
6.29 +\ (Try (Repeat (Calculate plus ))) @@ \
6.30 +\ (Try (Repeat (Calculate minus))))) e_)"
6.31 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
6.32 +atomty sc;
6.33
6.34
6.35 +"----------- pbl polynom probe -----------------------------------";
6.36 +"----------- pbl polynom probe -----------------------------------";
6.37 +"----------- pbl polynom probe -----------------------------------";
6.38 +states:=[];
6.39 +CalcTree [(["Pruefe (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12 =\
6.40 + \3 - 2 * e + 2 * f + 2 * g)",
6.41 + "mitWert [e = 1, f = 2, g = 3]",
6.42 + "Geprueft b"],
6.43 + ("PolyMinus.thy",["polynom","probe"],
6.44 + ["probe","fuer_polynom"]))];
6.45 +moveActiveRoot 1;
6.46 +autoCalculate 1 CompleteCalc;
6.47 +val ((pt,p),_) = get_calc 1;
6.48 +(*if p = ([], Res) andalso
6.49 + term2str (get_obj g_res pt (fst p)) = "11 = 11"
6.50 +then () else raise error "polyminus.sml: Probe 11 = 11";*)
6.51 +show_pt pt;
6.52
6.53
6.54