1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,408 @@
1.4 +(* calculate values for function constants
1.5 + (c) Walther Neuper 000106
1.6 +
1.7 +use"ProgLang/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 +