1.1 --- a/src/Tools/isac/ProgLang/calculate.sml Sun Feb 25 12:36:23 2018 +0100
1.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Sun Feb 25 14:02:42 2018 +0100
1.3 @@ -2,9 +2,8 @@
1.4 (c) Walther Neuper 000106
1.5 *)
1.6
1.7 -signature CALC =
1.8 +signature NUMERAL_CALCULATION =
1.9 sig
1.10 - val aT: typ
1.11 val adhoc_thm: theory -> string * eval_fn -> term -> (string * thm) option
1.12 val adhoc_thm1_: theory -> cal -> term -> (string * thm) option
1.13 val norm: term -> term
1.14 @@ -18,52 +17,12 @@
1.15 end
1.16
1.17 (**)
1.18 -structure Calc(**): CALC(**) =
1.19 +structure Calc(**): NUMERAL_CALCULATION(**) =
1.20 struct
1.21 (**)
1.22
1.23 -(* dirty type-conversion 30.1.00 for "fixed_values [R=R]" *)
1.24 -
1.25 -val aT = Type ("'a", []);
1.26 -(* isas types for Free, parseold: (1) "R=R" or (2) "R=(R::real)":
1.27 -(1)
1.28 -> val (TFree(ss2,TT2)) = T2;
1.29 -val ss2 = "'a" : string
1.30 -val TT2 = ["term"] : sort
1.31 -(2)
1.32 -> val (Type(ss2',TT2')) = T2';
1.33 -val ss2' = "RealDef.real" : string
1.34 -val TT2' = [] : typ list
1.35 -(3)
1.36 -val realType = TFree ("RealDef.real", HOLogic.termS);
1.37 -is different internally, too;
1.38 -
1.39 -(1) .. (3) are displayed equally !!!
1.40 -*)
1.41 -
1.42 -
1.43 -
1.44 -(* 30.1.00: generating special terms for ME:
1.45 - (1) binary numerals reconverted to Free ("#num",...)
1.46 - by libarary_G.num_str: called from parse (below) and
1.47 - interface_ME_ISA for all thms used
1.48 - (compare HOLogic.dest_binum)
1.49 - (2) 'a types converted to RealDef.real by typ_a2real
1.50 - in parse below
1.51 - (3) binary operators fixed to type real in RatArith.thy
1.52 - (trick by Markus Wenzel)
1.53 -*)
1.54 -
1.55 -
1.56 -
1.57 -
1.58 (** calculate numerals **)
1.59
1.60 -(*27.3.00: problems with patterns below:
1.61 -"Vars (a // #2 = r * xxxxx b)" doesn't work, but
1.62 -"Vars (a // #2 = r * sqrt b)" works
1.63 -*)
1.64 -
1.65 fun popt2str (SOME (_, term)) = "SOME " ^ term2str term
1.66 | popt2str NONE = "NONE";
1.67
1.68 @@ -79,6 +38,17 @@
1.69 fn : string -> string -> term -> theory -> (string * term) option
1.70 ^^^^^^... the selecting operator op_ (variable for eval_binop)
1.71 *)
1.72 +fun trace_calc0 str =
1.73 + if ! trace_calc then writeln ("### " ^ str) else ()
1.74 +fun trace_calc1 str1 str2 =
1.75 + if ! trace_calc then writeln (str1 ^ str2) else ()
1.76 +fun trace_calc2 str term popt =
1.77 + if ! trace_calc then writeln (str ^ term2str term ^ " , " ^ popt2str popt) else ()
1.78 +fun trace_calc3 str term =
1.79 + if ! trace_calc then writeln ("### " ^ str ^ term2str term) else ()
1.80 +fun trace_calc4 str t1 t2 =
1.81 + if ! trace_calc then writeln ("### " ^ str ^ term2str t1 ^ " $ " ^ term2str t2) else ()
1.82 +
1.83 fun get_pair thy op_ (ef: eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
1.84 if op_ = op0 then
1.85 let val popt = ef op_ t thy
1.86 @@ -87,23 +57,26 @@
1.87 | get_pair thy "Atools.ident" ef (t as (Const ("Atools.ident", _) $ _ $ _ )) =
1.88 ef "Atools.ident" t thy (* not nested *)
1.89 | get_pair thy op_ ef (t as (Const (op0,_) $ t1 $ t2)) = (* binary funs *)
1.90 - ((* tracing ("1.. get_pair: binop = "^op_); *)
1.91 + (trace_calc1 "1.. get_pair: binop = " op_;
1.92 if op_ = op0 then
1.93 - let val popt = ef op_ t thy
1.94 - (* val _ = tracing ("2.. get_pair: " ^ term2str t ^ " -> " ^ popt2str popt) *)
1.95 + let
1.96 + val popt = ef op_ t thy
1.97 + val _ = trace_calc2 "2.. get_pair: " t popt
1.98 in case popt of SOME _ => popt | NONE =>
1.99 - let val popt = get_pair thy op_ ef t1
1.100 - (* val _ = tracing ("3.. get_pair: " ^ term2str t1 ^ " -> "^popt2str popt) *)
1.101 + let
1.102 + val popt = get_pair thy op_ ef t1
1.103 + val _ = trace_calc2 "3.. get_pair: " t1 popt
1.104 in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end
1.105 end
1.106 else (* search subterms *)
1.107 - let val popt = get_pair thy op_ ef t1
1.108 - (*val _ = tracing("4.. get_pair: "^term2str t^" -> "^popt2str popt)*)
1.109 + let
1.110 + val popt = get_pair thy op_ ef t1
1.111 + val _ = trace_calc2 "4.. get_pair: " t popt
1.112 in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end)
1.113 | get_pair thy op_ ef (t as (Const (op0, _) $ t1 $ t2 $ t3)) = (* ternary funs *)
1.114 - ((*tracing ("### get_pair 4a: t= " ^ term2str t);
1.115 - tracing ("### get_pair 4a: op_= " ^ op_);
1.116 - tracing ("### get_pair 4a: op0= " ^ op0); *)
1.117 + (trace_calc3 "get_pair 4a: t= "t;
1.118 + trace_calc1 "get_pair 4a: op_= " op_;
1.119 + trace_calc1 "get_pair 4a: op0= " op0;
1.120 if op_ = op0 then
1.121 case ef op_ t thy of st as SOME _ => st | NONE =>
1.122 (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)
1.123 @@ -112,248 +85,30 @@
1.124 (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)))
1.125 | get_pair thy op_ ef (Abs (_, _, body)) = get_pair thy op_ ef body
1.126 | get_pair thy op_ ef (t1 $ t2) =
1.127 - let (* val _= tracing ("5.. get_pair t1 $ t2: " ^ term2str t1 ^ " $ " ^ term2str t2) *)
1.128 + let
1.129 + val _ = trace_calc4 "5.. get_pair t1 $ t2: " t1 t2;
1.130 val popt = get_pair thy op_ ef t1
1.131 in case popt of SOME _ => popt
1.132 - | NONE => ((* tracing "### get_pair: t1 $ t2 -> NONE"; *) get_pair thy op_ ef t2)
1.133 + | NONE => (trace_calc0 "### get_pair: t1 $ t2 -> NONE"; get_pair thy op_ ef t2)
1.134 end
1.135 | get_pair _ _ _ _ = NONE
1.136
1.137 - (*
1.138 -> val t = (Thm.term_of o the o (parse thy)) "#3 + #4";
1.139 -> val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));
1.140 -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
1.141 -> term2str t';
1.142 -> atomty t';
1.143 ->
1.144 -> val t = (Thm.term_of o the o (parse thy)) "(a + #3) + #4";
1.145 -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
1.146 -> term2str t';
1.147 ->
1.148 -> val t = (Thm.term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
1.149 -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
1.150 -> term2str t';
1.151 ->
1.152 -> val t = (Thm.term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
1.153 -> atomty t;
1.154 -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
1.155 -> term2str t';
1.156 -> val it = "#3 + (#4 + a) = #7 + a" : string
1.157 ->
1.158 ->
1.159 -> val t = (Thm.term_of o the o (parse thy)) "#-4//#-2";
1.160 -> val eval_fn = the (assoc (!eval_list, "cancel"));
1.161 -> val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
1.162 -> term2str t';
1.163 ->
1.164 -> val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
1.165 -> eval_binop "xxx" "pow" t thy;
1.166 -> val eval_fn = (eval_binop "xxx")
1.167 -> : string -> term -> theory -> (string * term) option;
1.168 -> val SOME (id,t') = get_pair thy "pow" eval_fn t;
1.169 -> term2str t';
1.170 -> val eval_fn = the (assoc (!eval_list, "pow"));
1.171 -> val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
1.172 -> term2str t';
1.173 ->
1.174 -> val t = (Thm.term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
1.175 -> val eval_fn = the (assoc (!eval_list, "Groups.times_class.times"));
1.176 -> val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t;
1.177 -> term2str t';
1.178 ->
1.179 -> val t = (Thm.term_of o the o (parse thy)) "#0 < #4";
1.180 -> val eval_fn = the (assoc (!eval_list, "Orderings.ord_class.less"));
1.181 -> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
1.182 -> term2str t';
1.183 -> val t = (Thm.term_of o the o (parse thy)) "#0 < #-4";
1.184 -> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
1.185 -> term2str t';
1.186 ->
1.187 -> val t = (Thm.term_of o the o (parse thy)) "#3 is_const";
1.188 -> val eval_fn = the (assoc (!eval_list, "is'_const"));
1.189 -> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
1.190 -> term2str t';
1.191 -> val t = (Thm.term_of o the o (parse thy)) "a is_const";
1.192 -> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
1.193 -> term2str t';
1.194 ->
1.195 -> val t = (Thm.term_of o the o (parse thy)) "#6//(#8::real)";
1.196 -> val eval_fn = the (assoc (!eval_list, "cancel"));
1.197 -> val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
1.198 -> term2str t';
1.199 ->
1.200 -> val t = (Thm.term_of o the o (parse thy)) "sqrt #12";
1.201 -> val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt"));
1.202 -> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
1.203 -> term2str t';
1.204 -> val it = "sqrt #12 = #2 * sqrt #3 " : string
1.205 ->
1.206 -> val t = (Thm.term_of o the o (parse thy)) "sqrt #9";
1.207 -> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
1.208 -> term2str t';
1.209 ->
1.210 -> val t = (Thm.term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";
1.211 -> val eval_fn = the (assoc (!eval_list, "Tools.Nth"));
1.212 -> val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;
1.213 -> term2str t';
1.214 -*)
1.215 -
1.216 -(* val ((op_, eval_fn),ct)=(cc,pre);
1.217 - (adhoc_thm (Thy_Info_get_theory "Isac") (op_, eval_fn) ct) handle e => print_exn e;
1.218 - parse thy ""
1.219 - *)
1.220 -(*.get a thm from an op_ somewhere in the term;
1.221 - apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711).*)
1.222 +(* get a thm from an op_ somewhere in the term;
1.223 + apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711) *)
1.224 fun adhoc_thm thy (op_, eval_fn) ct =
1.225 case get_pair thy op_ eval_fn ct of
1.226 - NONE => ((* tracing ("@@@ adhoc_thm: NONE, op_= " ^ op_);
1.227 - tracing ("@@@ adhoc_thm: ct= "); atomty ct; *)
1.228 - NONE)
1.229 + NONE => NONE
1.230 | SOME (thmid, t) => SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of thy)) t);
1.231 -(*
1.232 -> val ct = (the o (parse thy)) "#9 is_const";
1.233 -> adhoc_thm thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
1.234 -val it = SOME ("is_const9_","(is_const 9 ) = True [(is_const 9 ) = True]")
1.235
1.236 -> val ct = (the o (parse thy)) "sqrt #9";
1.237 -> adhoc_thm thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;
1.238 -val it = SOME ("sqrt_9_","sqrt 9 = 3 [sqrt 9 = 3]") : (string * thm) option
1.239 -
1.240 -> val ct = (the o (parse thy)) "#4<#4";
1.241 -> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o Symbol.explode) str = "#";
1.242 -
1.243 -val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]")
1.244 -
1.245 -> val ct = (the o (parse thy)) "a<#4";
1.246 -> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;
1.247 -val it = NONE : (string * thm) option
1.248 -
1.249 -> val ct = (the o (parse thy)) "#5<=#4";
1.250 -> adhoc_thm thy ("Orderings.ord_class.less_eq",the (assoc(!eval_list,"Orderings.ord_class.less_eq"))) ct;
1.251 -val it = SOME ("less_equal_5_4","(5 <= 4) = False [(5 <= 4) = False]")
1.252 -
1.253 --------------------------------------------------------------------6.8.02:
1.254 - val thy = SqRoot.thy;
1.255 - val t = (Thm.term_of o the o (parse thy)) "1+2";
1.256 - adhoc_thm thy (the(assoc(!calc_list,"PLUS"))) t;
1.257 - val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
1.258 --------------------------------------------------------------------6.8.02:
1.259 - val t = (Thm.term_of o the o (parse thy)) "-1";
1.260 - atomty t;
1.261 - val t = (Thm.term_of o the o (parse thy)) "0";
1.262 - atomty t;
1.263 - val t = (Thm.term_of o the o (parse thy)) "1";
1.264 - atomty t;
1.265 - val t = (Thm.term_of o the o (parse thy)) "2";
1.266 - atomty t;
1.267 - val t = (Thm.term_of o the o (parse thy)) "999999999";
1.268 - atomty t;
1.269 --------------------------------------------------------------------6.8.02:
1.270 -
1.271 -> val ct = (the o (parse thy)) "a+#3+#4";
1.272 -> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
1.273 -val it = SOME ("add_3_4","a + 3 + 4 = a + 7 [a + 3 + 4 = a + 7]")
1.274 -
1.275 -> val ct = (the o (parse thy)) "#3+(#4+a)";
1.276 -> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
1.277 -val it = SOME ("add_3_4","3 + (4 + a) = 7 + a [3 + (4 + a) = 7 + a]")
1.278 -
1.279 -> val ct = (the o (parse thy)) "a+(#3+#4)+#5";
1.280 -> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
1.281 -val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
1.282 -
1.283 -> val ct = (the o (parse thy)) "#3*(#4*a)";
1.284 -> adhoc_thm thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) ct;
1.285 -val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a [3 * (4 * a) = 12 * a]")
1.286 -
1.287 -> val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";
1.288 -> adhoc_thm thy ("pow",the (assoc(!eval_list,"pow"))) ct;
1.289 -val it = SOME ("4_(+2)","4 ^ 2 = 16 [4 ^ 2 = 16]") : (string * thm) option
1.290 -
1.291 -> val ct = (the o (parse thy)) "#-4//#-2";
1.292 -> adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
1.293 -val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2) [(-4) // (-2) = (+2)]")
1.294 -
1.295 -> val ct = (the o (parse thy)) "#6//#-8";
1.296 -> adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
1.297 -val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4 [6 // (-8) = (-3) // 4]")
1.298 -
1.299 -*)
1.300 -
1.301 -
1.302 -(*
1.303 -> val ct = (the o (parse thy)) "a + 3*4";
1.304 -> applicable "calculate" (Calc("Groups.times_class.times", "mult_")) ct;
1.305 -val it = SOME "3 * 4 = 12 [3 * 4 = 12]" : thm option
1.306 -
1.307 ---------------------------
1.308 -> val ct = (the o (parse thy)) "3 =!= 3";
1.309 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
1.310 -val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
1.311 -
1.312 -> val ct = (the o (parse thy)) "~ (3 =!= 3)";
1.313 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
1.314 -val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
1.315 -
1.316 -> val ct = (the o (parse thy)) "3 =!= 4";
1.317 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
1.318 -val thm = "(3 =!= 4) = False [(3 =!= 4) = False]" : thm
1.319 -
1.320 -> val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))";
1.321 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
1.322 - "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
1.323 -
1.324 -> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
1.325 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
1.326 - "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
1.327 -
1.328 -> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
1.329 -> val rls = eval_rls;
1.330 -> val (ct,_) = the (rewrite_set_ thy false rls ct);
1.331 -val ct = "HOL.True" : cterm
1.332 ---------------------------
1.333 -*)
1.334 -
1.335 -
1.336 -(*.get a thm applying an op_ to a term;
1.337 - apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711).*)
1.338 -(* val (thy, (op_, eval_fn), ct) =
1.339 - (thy, ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"), term);
1.340 - *)
1.341 -fun adhoc_thm1_ thy ((op_, eval_fn):cal) ct =
1.342 +(* get a thm applying an op_ to a term;
1.343 + apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711) *)
1.344 +fun adhoc_thm1_ thy (op_, eval_fn) ct =
1.345 case eval_fn op_ ct thy of
1.346 NONE => NONE
1.347 | SOME (thmid,t) =>
1.348 SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of thy)) t);
1.349
1.350 -
1.351 -
1.352 -
1.353 -
1.354 -(*.substitute bdv in an rls and leave Calc as they are.(*28.10.02*)
1.355 -fun inst_thm' subs (Thm (id, thm)) =
1.356 - Thm (id, (*read_instantiate throws: *** No such variable in term: ?bdv*)
1.357 - (read_instantiate subs thm) handle _ => thm)
1.358 - | inst_thm' _ calc = calc;
1.359 -fun inst_thm' (subs as (bdv,_)::_) (Thm (id, thm)) =
1.360 - Thm (id, (tracing("@@@ inst_thm': thm= "^(string_of_thmI thm));
1.361 - if bdv mem (vars_str o #prop o rep_thm) thm
1.362 - then (tracing("@@@ inst_thm': read_instantiate, thm="^((string_of_thmI thm)));
1.363 - read_instantiate subs thm)
1.364 - else (tracing("@@@ inst_thm': not mem.. "^bdv);
1.365 - thm)))
1.366 - | inst_thm' _ calc = calc;
1.367 -
1.368 -fun instantiate_rls subs
1.369 - (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca,
1.370 - asm_thm=at,rules=rules,scr=scr}:rls) =
1.371 - (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca,
1.372 - asm_thm=at,scr=scr,
1.373 - rules = map (inst_thm' subs) rules}:rls);---------------------------*)
1.374 -
1.375 -
1.376 -
1.377 -(** rewriting: ordered, conditional **)
1.378 +(** for ordered and conditional rewriting **)
1.379
1.380 fun mk_rule (prems,l,r) =
1.381 Trueprop $ (list_implies (prems, mk_equality (l,r)));
2.1 --- a/src/Tools/isac/calcelems.sml Sun Feb 25 12:36:23 2018 +0100
2.2 +++ b/src/Tools/isac/calcelems.sml Sun Feb 25 14:02:42 2018 +0100
2.3 @@ -838,6 +838,8 @@
2.4 fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
2.5
2.6
2.7 +(* trace internal steps of isac's numeral calculations *)
2.8 +val trace_calc = Unsynchronized.ref false;
2.9 (*.trace internal steps of isac's rewriter*)
2.10 val trace_rewrite = Unsynchronized.ref false;
2.11 (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
3.1 --- a/test/Tools/isac/ProgLang/calculate.sml Sun Feb 25 12:36:23 2018 +0100
3.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Sun Feb 25 14:02:42 2018 +0100
3.3 @@ -1,9 +1,6 @@
3.4 (* Title: test calculation of values for function constants
3.5 Author: Walther Neuper 2000
3.6 (c) copyright due to lincense terms.
3.7 -
3.8 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
3.9 - 10 20 30 40 50 60 70 80
3.10 *)
3.11
3.12 "--------------------------------------------------------";
3.13 @@ -20,6 +17,8 @@
3.14 " ================= calculate.sml: calculate_ 2002 ======";
3.15 "----------- get_pair with 3 args -----------------------";
3.16 "----------- calculate (2 * x is_const) -----------------";
3.17 +"----------- fun get_pair: examples ------------------------------------------------------------";
3.18 +"----------- fun adhoc_thm: examples -----------------------------------------------------------";
3.19 "--------------------------------------------------------";
3.20 "--------------------------------------------------------";
3.21 "--------------------------------------------------------";
3.22 @@ -325,3 +324,187 @@
3.23 val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
3.24 term2str t';
3.25 "HOL.False";
3.26 +
3.27 +"----------- fun get_pair: examples ------------------------------------------------------------";
3.28 +"----------- fun get_pair: examples ------------------------------------------------------------";
3.29 +"----------- fun get_pair: examples ------------------------------------------------------------";
3.30 + (*
3.31 +> val t = (Thm.term_of o the o (parse thy)) "#3 + #4";
3.32 +> val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));
3.33 +> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
3.34 +> term2str t';
3.35 +> atomty t';
3.36 +>
3.37 +> val t = (Thm.term_of o the o (parse thy)) "(a + #3) + #4";
3.38 +> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
3.39 +> term2str t';
3.40 +>
3.41 +> val t = (Thm.term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
3.42 +> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
3.43 +> term2str t';
3.44 +>
3.45 +> val t = (Thm.term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
3.46 +> atomty t;
3.47 +> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
3.48 +> term2str t';
3.49 +> val it = "#3 + (#4 + a) = #7 + a" : string
3.50 +>
3.51 +>
3.52 +> val t = (Thm.term_of o the o (parse thy)) "#-4//#-2";
3.53 +> val eval_fn = the (assoc (!eval_list, "cancel"));
3.54 +> val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
3.55 +> term2str t';
3.56 +>
3.57 +> val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
3.58 +> eval_binop "xxx" "pow" t thy;
3.59 +> val eval_fn = (eval_binop "xxx")
3.60 +> : string -> term -> theory -> (string * term) option;
3.61 +> val SOME (id,t') = get_pair thy "pow" eval_fn t;
3.62 +> term2str t';
3.63 +> val eval_fn = the (assoc (!eval_list, "pow"));
3.64 +> val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
3.65 +> term2str t';
3.66 +>
3.67 +> val t = (Thm.term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
3.68 +> val eval_fn = the (assoc (!eval_list, "Groups.times_class.times"));
3.69 +> val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t;
3.70 +> term2str t';
3.71 +>
3.72 +> val t = (Thm.term_of o the o (parse thy)) "#0 < #4";
3.73 +> val eval_fn = the (assoc (!eval_list, "Orderings.ord_class.less"));
3.74 +> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
3.75 +> term2str t';
3.76 +> val t = (Thm.term_of o the o (parse thy)) "#0 < #-4";
3.77 +> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
3.78 +> term2str t';
3.79 +>
3.80 +> val t = (Thm.term_of o the o (parse thy)) "#3 is_const";
3.81 +> val eval_fn = the (assoc (!eval_list, "is'_const"));
3.82 +> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
3.83 +> term2str t';
3.84 +> val t = (Thm.term_of o the o (parse thy)) "a is_const";
3.85 +> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
3.86 +> term2str t';
3.87 +>
3.88 +> val t = (Thm.term_of o the o (parse thy)) "#6//(#8::real)";
3.89 +> val eval_fn = the (assoc (!eval_list, "cancel"));
3.90 +> val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
3.91 +> term2str t';
3.92 +>
3.93 +> val t = (Thm.term_of o the o (parse thy)) "sqrt #12";
3.94 +> val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt"));
3.95 +> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
3.96 +> term2str t';
3.97 +> val it = "sqrt #12 = #2 * sqrt #3 " : string
3.98 +>
3.99 +> val t = (Thm.term_of o the o (parse thy)) "sqrt #9";
3.100 +> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
3.101 +> term2str t';
3.102 +>
3.103 +> val t = (Thm.term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";
3.104 +> val eval_fn = the (assoc (!eval_list, "Tools.Nth"));
3.105 +> val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;
3.106 +> term2str t';
3.107 +*)
3.108 +"----------- fun adhoc_thm: examples -----------------------------------------------------------";
3.109 +"----------- fun adhoc_thm: examples -----------------------------------------------------------";
3.110 +"----------- fun adhoc_thm: examples -----------------------------------------------------------";
3.111 +(*
3.112 +> val ct = (the o (parse thy)) "#9 is_const";
3.113 +> adhoc_thm thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
3.114 +val it = SOME ("is_const9_","(is_const 9 ) = True [(is_const 9 ) = True]")
3.115 +
3.116 +> val ct = (the o (parse thy)) "sqrt #9";
3.117 +> adhoc_thm thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;
3.118 +val it = SOME ("sqrt_9_","sqrt 9 = 3 [sqrt 9 = 3]") : (string * thm) option
3.119 +
3.120 +> val ct = (the o (parse thy)) "#4<#4";
3.121 +> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o Symbol.explode) str = "#";
3.122 +
3.123 +val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]")
3.124 +
3.125 +> val ct = (the o (parse thy)) "a<#4";
3.126 +> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;
3.127 +val it = NONE : (string * thm) option
3.128 +
3.129 +> val ct = (the o (parse thy)) "#5<=#4";
3.130 +> adhoc_thm thy ("Orderings.ord_class.less_eq",the (assoc(!eval_list,"Orderings.ord_class.less_eq"))) ct;
3.131 +val it = SOME ("less_equal_5_4","(5 <= 4) = False [(5 <= 4) = False]")
3.132 +
3.133 +-------------------------------------------------------------------6.8.02:
3.134 + val thy = SqRoot.thy;
3.135 + val t = (Thm.term_of o the o (parse thy)) "1+2";
3.136 + adhoc_thm thy (the(assoc(!calc_list,"PLUS"))) t;
3.137 + val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
3.138 +-------------------------------------------------------------------6.8.02:
3.139 + val t = (Thm.term_of o the o (parse thy)) "-1";
3.140 + atomty t;
3.141 + val t = (Thm.term_of o the o (parse thy)) "0";
3.142 + atomty t;
3.143 + val t = (Thm.term_of o the o (parse thy)) "1";
3.144 + atomty t;
3.145 + val t = (Thm.term_of o the o (parse thy)) "2";
3.146 + atomty t;
3.147 + val t = (Thm.term_of o the o (parse thy)) "999999999";
3.148 + atomty t;
3.149 +-------------------------------------------------------------------6.8.02:
3.150 +
3.151 +> val ct = (the o (parse thy)) "a+#3+#4";
3.152 +> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
3.153 +val it = SOME ("add_3_4","a + 3 + 4 = a + 7 [a + 3 + 4 = a + 7]")
3.154 +
3.155 +> val ct = (the o (parse thy)) "#3+(#4+a)";
3.156 +> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
3.157 +val it = SOME ("add_3_4","3 + (4 + a) = 7 + a [3 + (4 + a) = 7 + a]")
3.158 +
3.159 +> val ct = (the o (parse thy)) "a+(#3+#4)+#5";
3.160 +> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
3.161 +val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
3.162 +
3.163 +> val ct = (the o (parse thy)) "#3*(#4*a)";
3.164 +> adhoc_thm thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) ct;
3.165 +val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a [3 * (4 * a) = 12 * a]")
3.166 +
3.167 +> val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";
3.168 +> adhoc_thm thy ("pow",the (assoc(!eval_list,"pow"))) ct;
3.169 +val it = SOME ("4_(+2)","4 ^ 2 = 16 [4 ^ 2 = 16]") : (string * thm) option
3.170 +
3.171 +> val ct = (the o (parse thy)) "#-4//#-2";
3.172 +> adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
3.173 +val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2) [(-4) // (-2) = (+2)]")
3.174 +
3.175 +> val ct = (the o (parse thy)) "#6//#-8";
3.176 +> adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
3.177 +val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4 [6 // (-8) = (-3) // 4]")
3.178 +
3.179 +*)
3.180 +
3.181 +(*
3.182 +--------------------------
3.183 +> val ct = (the o (parse thy)) "3 =!= 3";
3.184 +> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.185 +val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
3.186 +
3.187 +> val ct = (the o (parse thy)) "~ (3 =!= 3)";
3.188 +> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.189 +val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
3.190 +
3.191 +> val ct = (the o (parse thy)) "3 =!= 4";
3.192 +> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.193 +val thm = "(3 =!= 4) = False [(3 =!= 4) = False]" : thm
3.194 +
3.195 +> val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))";
3.196 +> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.197 + "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
3.198 +
3.199 +> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
3.200 +> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.201 + "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
3.202 +
3.203 +> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
3.204 +> val rls = eval_rls;
3.205 +> val (ct,_) = the (rewrite_set_ thy false rls ct);
3.206 +val ct = "HOL.True" : cterm
3.207 +--------------------------
3.208 +*)
3.209 +