1.1 --- a/src/Tools/isac/Scripts/calculate.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,408 +0,0 @@
1.4 -(* calculate values for function constants
1.5 - (c) Walther Neuper 000106
1.6 -
1.7 -use"Scripts/calculate.sml";
1.8 -*)
1.9 -
1.10 -
1.11 -(* dirty type-conversion 30.1.00 for "fixed_values [R=R]" *)
1.12 -
1.13 -val aT = Type ("'a", []);
1.14 -(* isas types for Free, parseold: (1) "R=R" or (2) "R=(R::real)":
1.15 -(1)
1.16 -> val (TFree(ss2,TT2)) = T2;
1.17 -val ss2 = "'a" : string
1.18 -val TT2 = ["term"] : sort
1.19 -(2)
1.20 -> val (Type(ss2',TT2')) = T2';
1.21 -val ss2' = "RealDef.real" : string
1.22 -val TT2' = [] : typ list
1.23 -(3)
1.24 -val realType = TFree ("RealDef.real", HOLogic.termS);
1.25 -is different internally, too;
1.26 -
1.27 -(1) .. (3) are displayed equally !!!
1.28 -*)
1.29 -
1.30 -
1.31 -
1.32 -(* 30.1.00: generating special terms for ME:
1.33 - (1) binary numerals reconverted to Free ("#num",...)
1.34 - by libarary_G.num_str: called from parse (below) and
1.35 - interface_ME_ISA for all thms used
1.36 - (compare HOLogic.dest_binum)
1.37 - (2) 'a types converted to RealDef.real by typ_a2real
1.38 - in parse below
1.39 - (3) binary operators fixed to type real in RatArith.thy
1.40 - (trick by Markus Wenzel)
1.41 -*)
1.42 -
1.43 -
1.44 -
1.45 -
1.46 -(** calculate numerals **)
1.47 -
1.48 -(*27.3.00: problems with patterns below:
1.49 -"Vars (a // #2 = r * xxxxx b)" doesn't work, but
1.50 -"Vars (a // #2 = r * sqrt b)" works
1.51 -*)
1.52 -
1.53 -fun popt2str (SOME (str, term)) = "SOME "^term2str term
1.54 - | popt2str NONE = "NONE";
1.55 -
1.56 -(* scan a term for applying eval_fn ef
1.57 -args
1.58 - thy:
1.59 - op_: operator (as string) selecting the root of the pair
1.60 - ef : fn : (string -> term -> theory -> (string * term) option)
1.61 - ^^^^^^... for creating the string for the resulting theorem
1.62 - t : term to be scanned
1.63 -result:
1.64 - (string * term) option: found by the eval_* -function of type
1.65 - fn : string -> string -> term -> theory -> (string * term) option
1.66 - ^^^^^^... the selecting operator op_ (variable for eval_binop)
1.67 -*)
1.68 -fun get_pair thy op_ (ef:string -> term -> theory -> (string * term) option)
1.69 - (t as (Const(op0,t0) $ arg)) = (* unary fns *)
1.70 -(* val (thy, op_, (ef), (t as (Const(op0,t0) $ arg))) =
1.71 - (thy, op_, eval_fn, ct);
1.72 - *)
1.73 - if op_ = op0 then
1.74 - let val popt = ef op_ t thy
1.75 - in case popt of
1.76 - SOME _ => popt
1.77 - | NONE => get_pair thy op_ ef arg end
1.78 - else get_pair thy op_ ef arg
1.79 -
1.80 - | get_pair thy "Atools.ident" ef (t as (Const("Atools.ident",t0) $ _ $ _ )) =
1.81 -(* val (thy, "Atools.ident", ef, t as (Const(op0,_) $ t1 $ t2)) =
1.82 - (thy, op_, eval_fn, ct);
1.83 - *)
1.84 - ef "Atools.ident" t thy (* not nested *)
1.85 -
1.86 - | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2)) = (* binary funs*)
1.87 -(* val (thy, op_, ef, (t as (Const(op0,_) $ t1 $ t2))) =
1.88 - (thy, op_, eval_fn, ct);
1.89 - *)
1.90 - ((*writeln("1.. get_pair: binop = "^op_);*)
1.91 - if op_ = op0 then
1.92 - let val popt = ef op_ t thy
1.93 - (*val _ = writeln("2.. get_pair: "^term2str t^" -> "^popt2str popt)*)
1.94 - in case popt of
1.95 - SOME (id,_) => popt
1.96 - | NONE =>
1.97 - let val popt = get_pair thy op_ ef t1
1.98 - (*val _ = writeln("3.. get_pair: "^term2str t1^
1.99 - " -> "^popt2str popt)*)
1.100 - in case popt of
1.101 - SOME (id,_) => popt
1.102 - | NONE => get_pair thy op_ ef t2
1.103 - end
1.104 - end
1.105 - else (*search subterms*)
1.106 - let val popt = get_pair thy op_ ef t1
1.107 - (*val _ = writeln("4.. get_pair: "^term2str t^" -> "^popt2str popt)*)
1.108 - in case popt of
1.109 - SOME (id,_) => popt
1.110 - | NONE => get_pair thy op_ ef t2
1.111 - end)
1.112 - | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2 $ t3)) =(* trinary funs*)
1.113 - ((*writeln("### get_pair 4a: t= "^term2str t);
1.114 - writeln("### get_pair 4a: op_= "^op_);
1.115 - writeln("### get_pair 4a: op0= "^op0);*)
1.116 - if op_ = op0 then
1.117 - case ef op_ t thy of
1.118 - SOME tt => SOME tt
1.119 - | NONE => (case get_pair thy op_ ef t2 of
1.120 - SOME tt => SOME tt
1.121 - | NONE => get_pair thy op_ ef t3)
1.122 - else (case get_pair thy op_ ef t1 of
1.123 - SOME tt => SOME tt
1.124 - | NONE => (case get_pair thy op_ ef t2 of
1.125 - SOME tt => SOME tt
1.126 - | NONE => get_pair thy op_ ef t3)))
1.127 - | get_pair thy op_ ef (Const _) = NONE
1.128 - | get_pair thy op_ ef (Free _) = NONE
1.129 - | get_pair thy op_ ef (Var _) = NONE
1.130 - | get_pair thy op_ ef (Bound _) = NONE
1.131 - | get_pair thy op_ ef (Abs(a,T,body)) = get_pair thy op_ ef body
1.132 - | get_pair thy op_ ef (t1$t2) =
1.133 - let(*val _= writeln("5.. get_pair t1 $ t2: "^term2str t1^"
1.134 - $ "^term2str t2)*)
1.135 - val popt = get_pair thy op_ ef t1
1.136 - in case popt of
1.137 - SOME _ => popt
1.138 - | NONE => ((*writeln"### get_pair: t1 $ t2 -> NONE";*)
1.139 - get_pair thy op_ ef t2)
1.140 - end;
1.141 - (*
1.142 -> val t = (term_of o the o (parse thy)) "#3 + #4";
1.143 -> val eval_fn = the (assoc (!eval_list, "op +"));
1.144 -> val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
1.145 -> Syntax.string_of_term (thy2ctxt thy) t';
1.146 -> atomty t';
1.147 ->
1.148 -> val t = (term_of o the o (parse thy)) "(a + #3) + #4";
1.149 -> val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
1.150 -> Syntax.string_of_term (thy2ctxt thy) t';
1.151 ->
1.152 -> val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
1.153 -> val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
1.154 -> Syntax.string_of_term (thy2ctxt thy) t';
1.155 ->
1.156 -> val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
1.157 -> atomty t;
1.158 -> val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
1.159 -> Syntax.string_of_term (thy2ctxt thy) t';
1.160 -> val it = "#3 + (#4 + a) = #7 + a" : string
1.161 ->
1.162 ->
1.163 -> val t = (term_of o the o (parse thy)) "#-4//#-2";
1.164 -> val eval_fn = the (assoc (!eval_list, "cancel"));
1.165 -> val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
1.166 -> Syntax.string_of_term (thy2ctxt thy) t';
1.167 ->
1.168 -> val t = (term_of o the o (parse thy)) "#2^^^#3";
1.169 -> eval_binop "xxx" "pow" t thy;
1.170 -> val eval_fn = (eval_binop "xxx")
1.171 -> : string -> term -> theory -> (string * term) option;
1.172 -> val SOME (id,t') = get_pair thy "pow" eval_fn t;
1.173 -> Syntax.string_of_term (thy2ctxt thy) t';
1.174 -> val eval_fn = the (assoc (!eval_list, "pow"));
1.175 -> val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
1.176 -> Syntax.string_of_term (thy2ctxt thy) t';
1.177 ->
1.178 -> val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
1.179 -> val eval_fn = the (assoc (!eval_list, "op *"));
1.180 -> val (SOME (id,t')) = get_pair thy "op *" eval_fn t;
1.181 -> Syntax.string_of_term (thy2ctxt thy) t';
1.182 ->
1.183 -> val t = (term_of o the o (parse thy)) "#0 < #4";
1.184 -> val eval_fn = the (assoc (!eval_list, "op <"));
1.185 -> val (SOME (id,t')) = get_pair thy "op <" eval_fn t;
1.186 -> Syntax.string_of_term (thy2ctxt thy) t';
1.187 -> val t = (term_of o the o (parse thy)) "#0 < #-4";
1.188 -> val (SOME (id,t')) = get_pair thy "op <" eval_fn t;
1.189 -> Syntax.string_of_term (thy2ctxt thy) t';
1.190 ->
1.191 -> val t = (term_of o the o (parse thy)) "#3 is_const";
1.192 -> val eval_fn = the (assoc (!eval_list, "is'_const"));
1.193 -> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
1.194 -> Syntax.string_of_term (thy2ctxt thy) t';
1.195 -> val t = (term_of o the o (parse thy)) "a is_const";
1.196 -> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
1.197 -> Syntax.string_of_term (thy2ctxt thy) t';
1.198 ->
1.199 -> val t = (term_of o the o (parse thy)) "#6//(#8::real)";
1.200 -> val eval_fn = the (assoc (!eval_list, "cancel"));
1.201 -> val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
1.202 -> Syntax.string_of_term (thy2ctxt thy) t';
1.203 ->
1.204 -> val t = (term_of o the o (parse thy)) "sqrt #12";
1.205 -> val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt"));
1.206 -> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
1.207 -> Syntax.string_of_term (thy2ctxt thy) t';
1.208 -> val it = "sqrt #12 = #2 * sqrt #3 " : string
1.209 ->
1.210 -> val t = (term_of o the o (parse thy)) "sqrt #9";
1.211 -> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
1.212 -> Syntax.string_of_term (thy2ctxt thy) t';
1.213 ->
1.214 -> val t = (term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";
1.215 -> val eval_fn = the (assoc (!eval_list, "Tools.Nth"));
1.216 -> val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;
1.217 -> Syntax.string_of_term (thy2ctxt thy) t';
1.218 -*)
1.219 -
1.220 -(* val ((op_, eval_fn),ct)=(cc,pre);
1.221 - (get_calculation_ Isac.thy (op_, eval_fn) ct) handle e => print_exn e;
1.222 - parse thy ""
1.223 - *)
1.224 -(*.get a thm from an op_ somewhere in the term;
1.225 - apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711).*)
1.226 -fun get_calculation_ thy (op_, eval_fn) ct =
1.227 -(* val (thy, (op_, eval_fn), ct) =
1.228 - (thy, (the (assoc(!calclist',"order_system"))), t);
1.229 - *)
1.230 - case get_pair thy op_ eval_fn ct of
1.231 - NONE => ((*writeln("@@@ get_calculation: NONE, op_="^op_);
1.232 - writeln("@@@ get_calculation: ct= ");atomty ct;*)
1.233 - NONE)
1.234 - | SOME (thmid,t) =>
1.235 - ((*writeln("@@@ get_calculation: NONE, op_="^op_);
1.236 - writeln("@@@ get_calculation: ct= ");atomty ct;*)
1.237 - SOME (thmid, (make_thm o (cterm_of thy)) t));
1.238 -(*
1.239 -> val ct = (the o (parse thy)) "#9 is_const";
1.240 -> get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
1.241 -val it = SOME ("is_const9_","(is_const 9 ) = True [(is_const 9 ) = True]")
1.242 -
1.243 -> val ct = (the o (parse thy)) "sqrt #9";
1.244 -> get_calculation_ thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;
1.245 -val it = SOME ("sqrt_9_","sqrt 9 = 3 [sqrt 9 = 3]") : (string * thm) option
1.246 -
1.247 -> val ct = (the o (parse thy)) "#4<#4";
1.248 -> get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;fun is_no str = (hd o explode) str = "#";
1.249 -
1.250 -val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]")
1.251 -
1.252 -> val ct = (the o (parse thy)) "a<#4";
1.253 -> get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;
1.254 -val it = NONE : (string * thm) option
1.255 -
1.256 -> val ct = (the o (parse thy)) "#5<=#4";
1.257 -> get_calculation_ thy ("op <=",the (assoc(!eval_list,"op <="))) ct;
1.258 -val it = SOME ("less_equal_5_4","(5 <= 4) = False [(5 <= 4) = False]")
1.259 -
1.260 --------------------------------------------------------------------6.8.02:
1.261 - val thy = SqRoot.thy;
1.262 - val t = (term_of o the o (parse thy)) "1+2";
1.263 - get_calculation_ thy (the(assoc(!calc_list,"PLUS"))) t;
1.264 - val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
1.265 --------------------------------------------------------------------6.8.02:
1.266 - val t = (term_of o the o (parse thy)) "-1";
1.267 - atomty t;
1.268 - val t = (term_of o the o (parse thy)) "0";
1.269 - atomty t;
1.270 - val t = (term_of o the o (parse thy)) "1";
1.271 - atomty t;
1.272 - val t = (term_of o the o (parse thy)) "2";
1.273 - atomty t;
1.274 - val t = (term_of o the o (parse thy)) "999999999";
1.275 - atomty t;
1.276 --------------------------------------------------------------------6.8.02:
1.277 -
1.278 -> val ct = (the o (parse thy)) "a+#3+#4";
1.279 -> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
1.280 -val it = SOME ("add_3_4","a + 3 + 4 = a + 7 [a + 3 + 4 = a + 7]")
1.281 -
1.282 -> val ct = (the o (parse thy)) "#3+(#4+a)";
1.283 -> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
1.284 -val it = SOME ("add_3_4","3 + (4 + a) = 7 + a [3 + (4 + a) = 7 + a]")
1.285 -
1.286 -> val ct = (the o (parse thy)) "a+(#3+#4)+#5";
1.287 -> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
1.288 -val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
1.289 -
1.290 -> val ct = (the o (parse thy)) "#3*(#4*a)";
1.291 -> get_calculation_ thy ("op *",the (assoc(!eval_list,"op *"))) ct;
1.292 -val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a [3 * (4 * a) = 12 * a]")
1.293 -
1.294 -> val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";
1.295 -> get_calculation_ thy ("pow",the (assoc(!eval_list,"pow"))) ct;
1.296 -val it = SOME ("4_(+2)","4 ^ 2 = 16 [4 ^ 2 = 16]") : (string * thm) option
1.297 -
1.298 -> val ct = (the o (parse thy)) "#-4//#-2";
1.299 -> get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
1.300 -val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2) [(-4) // (-2) = (+2)]")
1.301 -
1.302 -> val ct = (the o (parse thy)) "#6//#-8";
1.303 -> get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
1.304 -val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4 [6 // (-8) = (-3) // 4]")
1.305 -
1.306 -*)
1.307 -
1.308 -
1.309 -(*
1.310 -> val ct = (the o (parse thy)) "a + 3*4";
1.311 -> applicable "calculate" (Calc("op *", "mult_")) ct;
1.312 -val it = SOME "3 * 4 = 12 [3 * 4 = 12]" : thm option
1.313 -
1.314 ---------------------------
1.315 -> val ct = (the o (parse thy)) "3 =!= 3";
1.316 -> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
1.317 -val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
1.318 -
1.319 -> val ct = (the o (parse thy)) "~ (3 =!= 3)";
1.320 -> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
1.321 -val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
1.322 -
1.323 -> val ct = (the o (parse thy)) "3 =!= 4";
1.324 -> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
1.325 -val thm = "(3 =!= 4) = False [(3 =!= 4) = False]" : thm
1.326 -
1.327 -> val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))";
1.328 -> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
1.329 - "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
1.330 -
1.331 -> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
1.332 -> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
1.333 - "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
1.334 -
1.335 -> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
1.336 -> val rls = eval_rls;
1.337 -> val (ct,_) = the (rewrite_set_ thy false rls ct);
1.338 -val ct = "True" : cterm
1.339 ---------------------------
1.340 -*)
1.341 -
1.342 -
1.343 -(*.get a thm applying an op_ to a term;
1.344 - apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711).*)
1.345 -(* val (thy, (op_, eval_fn), ct) =
1.346 - (thy, ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"), term);
1.347 - *)
1.348 -fun get_calculation1_ thy ((op_, eval_fn):cal) ct =
1.349 - case eval_fn op_ ct thy of
1.350 - NONE => NONE
1.351 - | SOME (thmid,t) =>
1.352 - SOME (thmid, (make_thm o (cterm_of thy)) t);
1.353 -
1.354 -
1.355 -
1.356 -
1.357 -
1.358 -(*.substitute bdv in an rls and leave Calc as they are.(*28.10.02*)
1.359 -fun inst_thm' subs (Thm (id, thm)) =
1.360 - Thm (id, (*read_instantiate throws: *** No such variable in term: ?bdv*)
1.361 - (read_instantiate subs thm) handle _ => thm)
1.362 - | inst_thm' _ calc = calc;
1.363 -fun inst_thm' (subs as (bdv,_)::_) (Thm (id, thm)) =
1.364 - Thm (id, (writeln("@@@ inst_thm': thm= "^(string_of_thmI thm));
1.365 - if bdv mem (vars_str o #prop o rep_thm) thm
1.366 - then (writeln("@@@ inst_thm': read_instantiate, thm="^((string_of_thmI thm)));
1.367 - read_instantiate subs thm)
1.368 - else (writeln("@@@ inst_thm': not mem.. "^bdv);
1.369 - thm)))
1.370 - | inst_thm' _ calc = calc;
1.371 -
1.372 -fun instantiate_rls subs
1.373 - (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca,
1.374 - asm_thm=at,rules=rules,scr=scr}:rls) =
1.375 - (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca,
1.376 - asm_thm=at,scr=scr,
1.377 - rules = map (inst_thm' subs) rules}:rls);---------------------------*)
1.378 -
1.379 -
1.380 -
1.381 -(** rewriting: ordered, conditional **)
1.382 -
1.383 -fun mk_rule (prems,l,r) =
1.384 - Trueprop $ (list_implies (prems, mk_equality (l,r)));
1.385 -
1.386 -(* 'norms' a rule, e.g.
1.387 -(*1*) a = 1 ==> a*(b+c) = b+c
1.388 - => a = 1 ==> a*(b+c) = b+c no change
1.389 -(*2*) t = t => (t=t) = True !!
1.390 -(*3*) [| k < l; m + l = k + n |] ==> m < n
1.391 - => [| k<l; m+l=k+n |] ==> m < n = True !! *)
1.392 -(* val it = fn : term -> term *)
1.393 -fun norm rule =
1.394 - let
1.395 - val (prems,concl)=(map strip_trueprop(Logic.strip_imp_prems rule),
1.396 - (strip_trueprop o Logic.strip_imp_concl)rule)
1.397 - in if is_equality concl then
1.398 - let val (l,r) = dest_equals' concl
1.399 - in if l = r then
1.400 - (*2*) mk_rule(prems,concl,true_as_term)
1.401 - else (*1*) rule end
1.402 - else (*3*) mk_rule(prems,concl,true_as_term)
1.403 - end;
1.404 -
1.405 -
1.406 -
1.407 -
1.408 -
1.409 -
1.410 -
1.411 -