1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/Scripts/Tools.thy Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,43 @@
1.4 +(* auxiliary functions used in scripts
1.5 + WN.1.3.00
1.6 +*)
1.7 +(* use_thy"Isa99/Tools";
1.8 + *)
1.9 +
1.10 +
1.11 +Tools = ListG +
1.12 +
1.13 +types (*for Descript.thy*)
1.14 +
1.15 + nam (* named variables *)
1.16 + una (* unnamed variables *)
1.17 + unl (* unnamed variables of type list *)
1.18 + str (* structured variables *)
1.19 + toreal (* var with undef real value *)
1.20 + toreall (* var with undef real list value *)
1.21 + unknow (* input without dsc in fmz=[] *)
1.22 + cpy (* UNUSED: copy-named variables
1.23 + identified by .._0, .._i .._' in pbt *)
1.24 + (* see modspec.sml: fun is_dsc *)
1.25 +
1.26 +arities
1.27 +
1.28 + nam, una, unl, str, toreal, toreall :: type
1.29 +
1.30 +consts
1.31 +
1.32 + UniversalList :: bool list
1.33 +
1.34 + Lhs, Rhs :: bool => real (*of an equality DONT USE*)
1.35 + lhs, rhs :: bool => real (*of an equality*)
1.36 + Var :: 'a => real list (*get the variables of a term *)
1.37 + matches :: ['a, 'a] => bool
1.38 +
1.39 +constdefs
1.40 +
1.41 + Testvar :: "[real, 'a] => bool" (*is a variable in a term ? *)
1.42 + "Testvar v t == v mem (Var t)"
1.43 +
1.44 +(*the other functions are defined on the metalevel, i.e.in Tools.ML*)
1.45 +
1.46 +end
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/sml/Scripts/calculate.sml Thu Apr 17 18:01:03 2003 +0200
2.3 @@ -0,0 +1,382 @@
2.4 +(* use"calculate.sml";
2.5 + use"Isa02/rewrite-parse.sml";
2.6 + use"../Isa02/rewrite-parse.sml";
2.7 + WN.6.1.00
2.8 +
2.9 + both, the rewriter and the parser based on isabelle
2.10 + in one file
2.11 +*)
2.12 +
2.13 +(*val trace_order = ref false; 25.5.02 loeschen !!!*)
2.14 +
2.15 +(*.trace internal steps of isac's rewriter*)
2.16 +val trace_rewrite = ref false;
2.17 +(*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
2.18 +val depth = ref 99999;
2.19 +
2.20 +
2.21 +
2.22 +(* dirty type-conversion 30.1.00 for "fixed_values [R=R]" *)
2.23 +
2.24 +val aT = Type ("'a", []);
2.25 +(* isas types for Free, parseold: (1) "R=R" or (2) "R=(R::real)":
2.26 +(1)
2.27 +> val (TFree(ss2,TT2)) = T2;
2.28 +val ss2 = "'a" : string
2.29 +val TT2 = ["term"] : sort
2.30 +(2)
2.31 +> val (Type(ss2',TT2')) = T2';
2.32 +val ss2' = "RealDef.real" : string
2.33 +val TT2' = [] : typ list
2.34 +(3)
2.35 +val realType = TFree ("RealDef.real", HOLogic.termS);
2.36 +is different internally, too;
2.37 +
2.38 +(1) .. (3) are displayed equally !!!
2.39 +*)
2.40 +
2.41 +
2.42 +
2.43 +(* 30.1.00: generating special terms for ME:
2.44 + (1) binary numerals reconverted to Free ("#num",...)
2.45 + by libarary_G.num_str: called from parse (below) and
2.46 + interface_ME_ISA for all thms used
2.47 + (compare HOLogic.dest_binum)
2.48 + (2) 'a types converted to RealDef.real by typ_a2real
2.49 + in parse below
2.50 + (3) binary operators fixed to type real in RatArith.thy
2.51 + (trick by Markus Wenzel)
2.52 +*)
2.53 +
2.54 +
2.55 +
2.56 +
2.57 +(** calculate numerals **)
2.58 +
2.59 +(*27.3.00: problems with patterns below:
2.60 +"Var (a // #2 = r * xxxxx b)" doesn't work, but
2.61 +"Var (a // #2 = r * sqrt b)" works
2.62 +*)
2.63 +
2.64 +
2.65 +(* scan a term for applying eval_fn ef
2.66 +args
2.67 + thy:
2.68 + op_: operator (as string) selecting the root of the pair
2.69 + ef : fn : (string -> term -> theory -> (string * term) option)
2.70 + ^^^^^^... for creating the string for the resulting theorem
2.71 + t : term to be scanned
2.72 +result:
2.73 + (string * term) option: found by the eval_* -function of type
2.74 + fn : string -> string -> term -> theory -> (string * term) option
2.75 + ^^^^^^... the selecting operator op_ (variable for eval_binop)
2.76 +*)
2.77 +fun get_pair thy op_ (ef:string -> term -> theory -> (string * term) option)
2.78 + (t as (Const(op0,t0) $ arg)) = (* unary fns *)
2.79 + if op_ = (*strip_thy*) op0 then
2.80 + let val popt = ef op_ t thy
2.81 + in case popt of
2.82 + Some _ => popt
2.83 + | None => get_pair thy op_ ef arg end
2.84 + else get_pair thy op_ ef arg
2.85 +
2.86 + | get_pair thy "Atools.ident" ef (t as (Const("Atools.ident",t0) $ _ $ _ )) =
2.87 + ef "Atools.ident" t thy (* not nested *)
2.88 +(* val (thy,op_,ef,t as (Const(op0,_)$t1$t2)) =
2.89 + (thy,op_,eval_fn,ct);
2.90 + *)
2.91 + | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2)) = (* binary funs*)
2.92 + ((*writeln("@@@ get_pair: binop, t = "^
2.93 + (Sign.string_of_term (sign_of thy) t));*)
2.94 + if op_ = op0 then
2.95 + let (*val _=writeln"@@@ get_pair: then 1"*)
2.96 + val popt = ef op_ t thy;
2.97 + in case popt of
2.98 + Some (id,_) => ((*writeln("@@@ get_pair: t -> Some "^id);*)
2.99 + popt)
2.100 + | None =>
2.101 + let (*val _= writeln"@@@ get_pair: t -> None"*)
2.102 + val popt = get_pair thy op_ ef t1
2.103 + in case popt of
2.104 + Some (id,_) =>
2.105 + ((*writeln("@@@ get_pair: t1 -> Some "^id);*)
2.106 + popt)
2.107 + | None => ((*writeln"@@@ get_pair: t1 -> None";*)
2.108 + get_pair thy op_ ef t2)
2.109 + end
2.110 + end
2.111 + else (*search subterms*)
2.112 + let (*val _= writeln"@@@ get_pair: t else"*)
2.113 + val popt = get_pair thy op_ ef t1
2.114 + in case popt of
2.115 + Some (id,_) => ((*writeln("@@@ get_pair: t1 -> Some "^id);*)
2.116 + popt)
2.117 + | None => ((*writeln"@@@ get_pair: t1 else -> None";*)
2.118 + get_pair thy op_ ef t2)
2.119 + end)
2.120 +
2.121 + | get_pair thy op_ ef (Const _) = None
2.122 + | get_pair thy op_ ef (Free _) = None
2.123 + | get_pair thy op_ ef (Var _) = None
2.124 + | get_pair thy op_ ef (Bound _) = None
2.125 + | get_pair thy op_ ef (Abs(a,T,body)) = get_pair thy op_ ef body
2.126 + | get_pair thy op_ ef (t1$t2) =
2.127 + let (*val _= writeln"### get_pair: t1 $ t2"*)
2.128 + val popt = get_pair thy op_ ef t1
2.129 + in case popt of
2.130 + Some _ => popt
2.131 + | None => ((*writeln"### get_pair: t1 $ t2 -> None";*)
2.132 + get_pair thy op_ ef t2)
2.133 + end;
2.134 + (*
2.135 +> val t = (term_of o the o (parse thy)) "#3 + #4";
2.136 +> val eval_fn = the (assoc (!eval_list, "op +"));
2.137 +> val (Some (id,t')) = get_pair thy "op +" eval_fn t;
2.138 +> Sign.string_of_term (sign_of thy) t';
2.139 +> atomty thy t';
2.140 +>
2.141 +> val t = (term_of o the o (parse thy)) "(a + #3) + #4";
2.142 +> val (Some (id,t')) = get_pair thy "op +" eval_fn t;
2.143 +> Sign.string_of_term (sign_of thy) t';
2.144 +>
2.145 +> val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
2.146 +> val (Some (id,t')) = get_pair thy "op +" eval_fn t;
2.147 +> Sign.string_of_term (sign_of thy) t';
2.148 +>
2.149 +> val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
2.150 +> atomty thy t;
2.151 +> val (Some (id,t')) = get_pair thy "op +" eval_fn t;
2.152 +> Sign.string_of_term (sign_of thy) t';
2.153 +> val it = "#3 + (#4 + a) = #7 + a" : string
2.154 +>
2.155 +>
2.156 +> val t = (term_of o the o (parse thy)) "#-4//#-2";
2.157 +> val eval_fn = the (assoc (!eval_list, "cancel"));
2.158 +> val (Some (id,t')) = get_pair thy "cancel" eval_fn t;
2.159 +> Sign.string_of_term (sign_of thy) t';
2.160 +>
2.161 +> val t = (term_of o the o (parse thy)) "#2^^^#3";
2.162 +> eval_binop "xxx" "pow" t thy;
2.163 +> val eval_fn = (eval_binop "xxx")
2.164 +> : string -> term -> theory -> (string * term) option;
2.165 +> val Some (id,t') = get_pair thy "pow" eval_fn t;
2.166 +> Sign.string_of_term (sign_of thy) t';
2.167 +> val eval_fn = the (assoc (!eval_list, "pow"));
2.168 +> val (Some (id,t')) = get_pair thy "pow" eval_fn t;
2.169 +> Sign.string_of_term (sign_of thy) t';
2.170 +>
2.171 +> val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
2.172 +> val eval_fn = the (assoc (!eval_list, "op *"));
2.173 +> val (Some (id,t')) = get_pair thy "op *" eval_fn t;
2.174 +> Sign.string_of_term (sign_of thy) t';
2.175 +>
2.176 +> val t = (term_of o the o (parse thy)) "#0 < #4";
2.177 +> val eval_fn = the (assoc (!eval_list, "op <"));
2.178 +> val (Some (id,t')) = get_pair thy "op <" eval_fn t;
2.179 +> Sign.string_of_term (sign_of thy) t';
2.180 +> val t = (term_of o the o (parse thy)) "#0 < #-4";
2.181 +> val (Some (id,t')) = get_pair thy "op <" eval_fn t;
2.182 +> Sign.string_of_term (sign_of thy) t';
2.183 +>
2.184 +> val t = (term_of o the o (parse thy)) "#3 is_const";
2.185 +> val eval_fn = the (assoc (!eval_list, "is'_const"));
2.186 +> val (Some (id,t')) = get_pair thy "is'_const" eval_fn t;
2.187 +> Sign.string_of_term (sign_of thy) t';
2.188 +> val t = (term_of o the o (parse thy)) "a is_const";
2.189 +> val (Some (id,t')) = get_pair thy "is'_const" eval_fn t;
2.190 +> Sign.string_of_term (sign_of thy) t';
2.191 +>
2.192 +> val t = (term_of o the o (parse thy)) "#6//(#8::real)";
2.193 +> val eval_fn = the (assoc (!eval_list, "cancel"));
2.194 +> val (Some (id,t')) = get_pair thy "cancel" eval_fn t;
2.195 +> Sign.string_of_term (sign_of thy) t';
2.196 +>
2.197 +> val t = (term_of o the o (parse thy)) "sqrt #12";
2.198 +> val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt"));
2.199 +> val (Some (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
2.200 +> Sign.string_of_term (sign_of thy) t';
2.201 +> val it = "sqrt #12 = #2 * sqrt #3 " : string
2.202 +>
2.203 +> val t = (term_of o the o (parse thy)) "sqrt #9";
2.204 +> val (Some (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
2.205 +> Sign.string_of_term (sign_of thy) t';
2.206 +>
2.207 +> val t = (term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";
2.208 +> val eval_fn = the (assoc (!eval_list, "Tools.Nth"));
2.209 +> val (Some (id,t')) = get_pair thy "Tools.Nth" eval_fn t;
2.210 +> Sign.string_of_term (sign_of thy) t';
2.211 +*)
2.212 +
2.213 +(* val ((op_, eval_fn),ct)=(cc,pre);
2.214 + (get_calculation_ Isac.thy (op_, eval_fn) ct) handle e => print_exn e;
2.215 + parse thy ""
2.216 + *)
2.217 +(*.apply ONLY to (app_num_tr'2 term), app_num_tr'2 (- 4711) --> (-4711).*)
2.218 +fun get_calculation_ thy (op_, eval_fn) ct =
2.219 + case get_pair thy op_ eval_fn ct of
2.220 + None => ((*writeln("@@@ get_calculation: None, op_="^op_);
2.221 + writeln("@@@ get_calculation: ct= ");atomty thy ct;*)
2.222 + None)
2.223 + | Some (thmid,t) =>
2.224 + ((*writeln("@@@ get_calculation: None, op_="^op_);
2.225 + writeln("@@@ get_calculation: ct= ");atomty thy ct;*)
2.226 + Some (thmid, (make_thm o (cterm_of (sign_of thy))) t));
2.227 +(*
2.228 +> val ct = (the o (parse thy)) "#9 is_const";
2.229 +> get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
2.230 +val it = Some ("is_const9_","(is_const 9 ) = True [(is_const 9 ) = True]")
2.231 +
2.232 +> val ct = (the o (parse thy)) "sqrt #9";
2.233 +> get_calculation_ thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;
2.234 +val it = Some ("sqrt_9_","sqrt 9 = 3 [sqrt 9 = 3]") : (string * thm) option
2.235 +
2.236 +> val ct = (the o (parse thy)) "#4<#4";
2.237 +> get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;fun is_no str = (hd o explode) str = "#";
2.238 +
2.239 +val it = Some ("less_5_4","(5 < 4) = False [(5 < 4) = False]")
2.240 +
2.241 +> val ct = (the o (parse thy)) "a<#4";
2.242 +> get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;
2.243 +val it = None : (string * thm) option
2.244 +
2.245 +> val ct = (the o (parse thy)) "#5<=#4";
2.246 +> get_calculation_ thy ("op <=",the (assoc(!eval_list,"op <="))) ct;
2.247 +val it = Some ("less_equal_5_4","(5 <= 4) = False [(5 <= 4) = False]")
2.248 +
2.249 +-------------------------------------------------------------------6.8.02:
2.250 + val thy = SqRoot.thy;
2.251 + val t = (term_of o the o (parse thy)) "1+2";
2.252 + get_calculation_ thy (the(assoc(!calc_list,"plus"))) t;
2.253 + val it = Some ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
2.254 +-------------------------------------------------------------------6.8.02:
2.255 + val t = (term_of o the o (parse thy)) "-1";
2.256 + atomty Isac.thy t;
2.257 + val t = (term_of o the o (parse thy)) "0";
2.258 + atomty Isac.thy t;
2.259 + val t = (term_of o the o (parse thy)) "1";
2.260 + atomty Isac.thy t;
2.261 + val t = (term_of o the o (parse thy)) "2";
2.262 + atomty Isac.thy t;
2.263 + val t = (term_of o the o (parse thy)) "999999999";
2.264 + atomty Isac.thy t;
2.265 +-------------------------------------------------------------------6.8.02:
2.266 +
2.267 +> val ct = (the o (parse thy)) "a+#3+#4";
2.268 +> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
2.269 +val it = Some ("add_3_4","a + 3 + 4 = a + 7 [a + 3 + 4 = a + 7]")
2.270 +
2.271 +> val ct = (the o (parse thy)) "#3+(#4+a)";
2.272 +> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
2.273 +val it = Some ("add_3_4","3 + (4 + a) = 7 + a [3 + (4 + a) = 7 + a]")
2.274 +
2.275 +> val ct = (the o (parse thy)) "a+(#3+#4)+#5";
2.276 +> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
2.277 +val it = Some ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
2.278 +
2.279 +> val ct = (the o (parse thy)) "#3*(#4*a)";
2.280 +> get_calculation_ thy ("op *",the (assoc(!eval_list,"op *"))) ct;
2.281 +val it = Some ("mult_3_4","3 * (4 * a) = 12 * a [3 * (4 * a) = 12 * a]")
2.282 +
2.283 +> val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";
2.284 +> get_calculation_ thy ("pow",the (assoc(!eval_list,"pow"))) ct;
2.285 +val it = Some ("4_(+2)","4 ^ 2 = 16 [4 ^ 2 = 16]") : (string * thm) option
2.286 +
2.287 +> val ct = (the o (parse thy)) "#-4//#-2";
2.288 +> get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
2.289 +val it = Some ("cancel_(-4)_(-2)","(-4) // (-2) = (+2) [(-4) // (-2) = (+2)]")
2.290 +
2.291 +> val ct = (the o (parse thy)) "#6//#-8";
2.292 +> get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
2.293 +val it = Some ("cancel_6_(-8)","6 // (-8) = (-3) // 4 [6 // (-8) = (-3) // 4]")
2.294 +
2.295 +*)
2.296 +
2.297 +
2.298 +(*
2.299 +> val ct = (the o (parse thy)) "a + 3*4";
2.300 +> applicable "calculate" (Calc("op *", "mult_")) ct;
2.301 +val it = Some "3 * 4 = 12 [3 * 4 = 12]" : thm option
2.302 +
2.303 +--------------------------
2.304 +> val ct = (the o (parse thy)) "3 =!= 3";
2.305 +> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
2.306 +val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
2.307 +
2.308 +> val ct = (the o (parse thy)) "~ (3 =!= 3)";
2.309 +> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
2.310 +val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
2.311 +
2.312 +> val ct = (the o (parse thy)) "3 =!= 4";
2.313 +> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
2.314 +val thm = "(3 =!= 4) = False [(3 =!= 4) = False]" : thm
2.315 +
2.316 +> val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))";
2.317 +> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
2.318 + "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
2.319 +
2.320 +> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
2.321 +> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
2.322 + "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
2.323 +
2.324 +> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
2.325 +> val rls = eval_rls;
2.326 +> val (ct,_) = the (rewrite_set_ thy false rls ct);
2.327 +val ct = "True" : cterm
2.328 +--------------------------
2.329 +*)
2.330 +
2.331 +
2.332 +(*.substitute bdv in an rls and leave Calc as they are.(*28.10.02*)
2.333 +fun inst_thm' subs (Thm (id, thm)) =
2.334 + Thm (id, (*read_instantiate throws: *** No such variable in term: ?bdv*)
2.335 + (read_instantiate subs thm) handle _ => thm)
2.336 + | inst_thm' _ calc = calc;
2.337 +fun inst_thm' (subs as (bdv,_)::_) (Thm (id, thm)) =
2.338 + Thm (id, (writeln("@@@ inst_thm': thm= "^(string_of_thm thm));
2.339 + if bdv mem (vars_str o #prop o rep_thm) thm
2.340 + then (writeln("@@@ inst_thm': read_instantiate, thm="^((string_of_thm thm)));
2.341 + read_instantiate subs thm)
2.342 + else (writeln("@@@ inst_thm': not mem.. "^bdv);
2.343 + thm)))
2.344 + | inst_thm' _ calc = calc;
2.345 +
2.346 +fun instantiate_rls subs
2.347 + (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca,
2.348 + asm_thm=at,rules=rules,scr=scr}:rls) =
2.349 + (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca,
2.350 + asm_thm=at,scr=scr,
2.351 + rules = map (inst_thm' subs) rules}:rls);---------------------------*)
2.352 +
2.353 +
2.354 +
2.355 +(** rewriting: ordered, conditional **)
2.356 +
2.357 +fun mk_rule (prems,l,r) =
2.358 + Trueprop $ (list_implies (prems, mk_equality (l,r)));
2.359 +
2.360 +(* 'norms' a rule, e.g.
2.361 +(*1*) a = 1 ==> a*(b+c) = b+c
2.362 + => a = 1 ==> a*(b+c) = b+c no change
2.363 +(*2*) t = t => (t=t) = True !!
2.364 +(*3*) [| k < l; m + l = k + n |] ==> m < n
2.365 + => [| k<l; m+l=k+n |] ==> m < n = True !! *)
2.366 +(* val it = fn : term -> term *)
2.367 +fun norm rule =
2.368 + let
2.369 + val (prems,concl)=(map strip_trueprop(Logic.strip_imp_prems rule),
2.370 + (strip_trueprop o Logic.strip_imp_concl)rule)
2.371 + in if is_equality concl then
2.372 + let val (l,r) = dest_equals' concl
2.373 + in if l = r then
2.374 + (*2*) mk_rule(prems,concl,true_as_term)
2.375 + else (*1*) rule end
2.376 + else (*3*) mk_rule(prems,concl,true_as_term)
2.377 + end;
2.378 +
2.379 +
2.380 +
2.381 +
2.382 +
2.383 +
2.384 +
2.385 +
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/sml/Scripts/rewrite.sml Thu Apr 17 18:01:03 2003 +0200
3.3 @@ -0,0 +1,635 @@
3.4 +(* use"../Isa02/rewrite.sml";
3.5 + use"Isa02/rewrite.sml";
3.6 + use"rewrite.sml";
3.7 + *)
3.8 +
3.9 +(*.......................................................................*)
3.10 +
3.11 +
3.12 +exception NO_REWRITE;
3.13 +
3.14 +(*17.6.00: rewrite by going down the term with rew_sub*)
3.15 +(* val (bdv,tless)=(subst,rew_ord);
3.16 + *)
3.17 +fun rewrite__ thy i bdv tless rls put_asm thm ct =
3.18 + let
3.19 + val (t',asms,rew) = rew_sub thy i bdv tless rls put_asm
3.20 + (((inst_bdv bdv(*28.10.02*)) o norm o #prop o rep_thm) thm) ct;
3.21 + in if rew then Some (t', asms)
3.22 + else None end
3.23 +(* val(r,t)=(((inst_bdv bdv) o norm o #prop o rep_thm) thm,ct);
3.24 + val t1 = (#prop o rep_thm) thm;
3.25 + val t2 = norm t1;
3.26 + val t3 = inst_bdv bdv t2;
3.27 +
3.28 + val thm4 = read_instantiate [("bdv","x")] thm;
3.29 + val t4 = (norm o #prop o rep_thm) thm4;
3.30 + *)
3.31 +and rew_sub thy i bdv tless rls put_asm r t =
3.32 + (let (* from Pure/thm.ML: fun rewritec *)
3.33 + val (lhs,rhs) = (dest_equals' o strip_trueprop
3.34 + o Logic.strip_imp_concl) r;
3.35 + (*val _=writeln("@@@ rew_sub: t= "^(term2str t));
3.36 + val _=writeln("@@@ rew_sub: lhs= "^(term2str lhs));*)
3.37 + val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs,t);
3.38 + (*TODOtest: (-"-) handle _ => raise NO_REWRITE; 12.8.02 ???*)
3.39 + (*val _=writeln("@@@ rew_sub: Pattern.match (lhs,t) ");*)
3.40 + val r' = ren_inst (insts, r, lhs, t);
3.41 + val p' = map strip_trueprop (Logic.strip_imp_prems r');
3.42 + val t' = (snd o dest_equals' o strip_trueprop
3.43 + o Logic.strip_imp_concl) r';
3.44 + (*val _=writeln("@@@ rew_sub: t'= "^(term2str t'));*)
3.45 + val _= if ! trace_rewrite andalso i < ! depth andalso p' <> []
3.46 + then writeln((idt"#"(i+1))^" eval prems: "^(term2str r')) else();
3.47 + val (t'',p'') =
3.48 + if eval__true thy (i+1) p' bdv rls
3.49 + then (if ! trace_rewrite andalso i < ! depth andalso p' <> []
3.50 + then writeln((idt"#"(i+1))^" prems true: "^(terms2str p'))else();
3.51 + (t',[])) (* + uncond.rew. *)
3.52 + else if put_asm
3.53 + then (if ! trace_rewrite andalso i < ! depth
3.54 + then writeln((idt"#"(i+1))^" prems to asm: "^(terms2str p'))
3.55 + else();
3.56 + (t',p'))
3.57 + else (if ! trace_rewrite andalso i < ! depth
3.58 + then writeln((idt"#"(i+1))^" prems false: "^(terms2str p'))
3.59 + else();
3.60 + raise NO_REWRITE )
3.61 + in if perm lhs rhs andalso not (tless bdv (t',t))
3.62 + then (if ! trace_rewrite andalso i < ! depth
3.63 + then writeln((idt"#"i)^" not: \""^
3.64 + (Sign.string_of_term (sign_of thy) t)^"\" > \""^
3.65 + (Sign.string_of_term (sign_of thy) t')^"\"") else ();
3.66 + raise NO_REWRITE )
3.67 + else ((*writeln("##@ rew_sub: (t''= "^(term2str t'')^
3.68 + ", p'' ="^(terms2str p'')^", true)");*)
3.69 + (t'',p'',true))
3.70 + end) handle _ (*TODOtest: NO_REWRITE *) =>
3.71 + (case t of
3.72 + Const(s,T) => (Const(s,T),[],false)
3.73 + | Free(s,T) => (Free(s,T),[],false)
3.74 + | Var(n,T) => (Var(n,T),[],false)
3.75 + | Bound i => (Bound i,[],false)
3.76 + | Abs(s,T,body) =>
3.77 + let val (t',asms,rew) = rew_sub thy i bdv tless rls put_asm r body
3.78 + in (Abs(s,T,t'),asms,rew) end
3.79 + | t1 $ t2 =>
3.80 + let val (t2',asm2,rew2) = rew_sub thy i bdv tless rls put_asm r t2
3.81 + in if rew2 then (t1 $ t2',asm2,true)
3.82 + else let val (t1',asm1,rew1) =
3.83 + rew_sub thy i bdv tless rls put_asm r t1
3.84 + in if rew1 then (t1' $ t2,asm1,true)
3.85 + else (t1 $ t2,[],false) end
3.86 + end)
3.87 +(* val (cprems',rls)=([pre],prls);
3.88 + rewrite__set_ thy i false rls pre;
3.89 + *)
3.90 +and eval__true thy i cprems' bdv rls =
3.91 + if cprems' = [HOLogic.true_const] orelse cprems' = [] then true
3.92 + else
3.93 + let
3.94 + fun eval cp = case rewrite__set_ thy (i+1) false bdv rls cp of
3.95 + None => if cp = HOLogic.true_const then true else false
3.96 + | Some (ct,_) => if ct = HOLogic.true_const then true else false
3.97 + (*val _= if not (!trace_rewrite) then ()
3.98 + else writeln ("### --- begin eval. condition(s) ---")
3.99 + val bool = foldr and_ (map eval cprems', true)
3.100 + val _= if not (!trace_rewrite) then ()
3.101 + else writeln "### --- end eval. condition(s) ---"*)
3.102 + in (*bool*) foldr and_ (map eval cprems', true) end
3.103 +
3.104 +and rewrite__set_ thy i _ _ (rrls as Rrls _) t =
3.105 + let val _= if ! trace_rewrite andalso i < ! depth
3.106 + then writeln ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^
3.107 + (term2str t)) else ()
3.108 + val (t', asm, rew) = app_rev thy (i+1) rrls t
3.109 + in if rew then Some (t', asm)
3.110 + else None end
3.111 + | rewrite__set_ thy i put_asm bdv rls ct =
3.112 + let
3.113 + datatype switch = Appl | Noap;
3.114 + fun rew_once ruls asm ct Noap [] = (ct,asm)
3.115 + | rew_once ruls asm ct Appl [] =
3.116 + (case rls of Rls _ => rew_once ruls asm ct Noap ruls
3.117 + | Seq _ => (ct,asm))
3.118 + | rew_once ruls asm ct apno (rul::thms) =
3.119 + case rul of
3.120 + Thm (thmid, thm) =>
3.121 + (if !trace_rewrite andalso i < ! depth
3.122 + then writeln((idt"#"(i+1))^" try thm: "^thmid) else ();
3.123 + case rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
3.124 + ((#erls o rep_rls) rls) put_asm thm ct of
3.125 + None => rew_once ruls asm ct apno thms
3.126 + | Some (ct',asm') => (if ! trace_rewrite andalso i < ! depth
3.127 + then writeln((idt"="(i+1))^" rewrites to: "^
3.128 + (Sign.string_of_term (sign_of thy) ct')) else ();
3.129 + rew_once ruls (asm union asm') ct' Appl (rul::thms)))
3.130 +(* val cc =
3.131 + ("RootEq.is'_rootequation'_in",
3.132 + (eval_is_rootequation_in ""):string -> term ->
3.133 + theory -> (string * term) option);
3.134 + get_calculation_ thy cc pre;
3.135 + *)
3.136 + | Calc (cc as (op_,_)) =>
3.137 + (let val _= if !trace_rewrite andalso i < ! depth then
3.138 + writeln((idt"#"(i+1))^" try calc: "^op_^"'") else ();
3.139 + val ct = app_num_tr'2 ct
3.140 + in case get_calculation_ thy cc ct of
3.141 + None => rew_once ruls asm ct apno thms
3.142 + | Some (thmid, thm') =>
3.143 + let
3.144 + val pairopt =
3.145 + rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
3.146 + ((#erls o rep_rls) rls) put_asm thm' ct;
3.147 + val _ = if pairopt <> None then ()
3.148 + else raise error("rewrite_set_, rewrite_ "^
3.149 + (string_of_thm thm')^" "^(term2str ct)^" = None")
3.150 + val _ = if ! trace_rewrite andalso i < ! depth
3.151 + then writeln((idt"="(i+1))^" calc. to: "^
3.152 + (term2str ((fst o the) pairopt)))
3.153 + else()
3.154 + in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end
3.155 + end)
3.156 + | Rls_ rls' =>
3.157 + (case rewrite__set_ thy (i+1) put_asm bdv rls' ct of
3.158 + Some (t',asm') => rew_once ruls (asm union asm') t' Appl thms
3.159 + | None => rew_once ruls asm ct apno thms);
3.160 +
3.161 + val ruls = (#rules o rep_rls) rls;
3.162 + val _= if ! trace_rewrite andalso i < ! depth
3.163 + then writeln ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^
3.164 + (term2str ct)) else ()
3.165 + val (ct',asm') = rew_once ruls [] ct Noap ruls;
3.166 + in if ct = ct' then None else Some (ct',asm') end
3.167 +
3.168 +and app_rev thy i rrls t =
3.169 + let
3.170 + (*.check a (precond, pattern) of a rev-set; stops with 1st true.*)
3.171 + fun chk_prepat thy erls [] t = true
3.172 + | chk_prepat thy erls prepat t =
3.173 + let fun chk (pres, pat) =
3.174 + let val (_, sbst) =
3.175 + (Pattern.match
3.176 + (Sign.tsig_of (sign_of(assoc_thy "Isac.thy")))
3.177 + (pat, t))
3.178 + handle _ => ([], [])
3.179 + val subst = map mk_subs sbst;
3.180 + (*val _=writeln("### chk_prepat: subst = "^(subst2str subst));*)
3.181 + in if subst = nil then false
3.182 + else
3.183 + ((*writeln("### chk_prepat: (pre,pat) ("^
3.184 + (term2str pre)^", "^(term2str pat)^" = "^(bool2str (
3.185 + eval_true thy [subst_atomic subst pre] (assoc_rls erls))));*)
3.186 + eval__true thy (i+1) (map (subst_atomic subst)pres)
3.187 + [] erls) end
3.188 + fun scan_ f [] = false (*scan_ NEVER called by []*)
3.189 + | scan_ f (pp::pps) = if f pp then true
3.190 + else scan_ f pps;
3.191 + in scan_ chk prepat end;
3.192 +
3.193 + (*.apply the normal_form of a rev-set.*)
3.194 + fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
3.195 + if chk_prepat thy erls prepat t
3.196 + then ((*writeln("### app_rev': t = "^(term2str t));*)
3.197 + normal_form t)
3.198 + else None;
3.199 +
3.200 + val opt = app_rev' thy rrls t
3.201 + in case opt of
3.202 + Some (t', asm) => (t', asm, true)
3.203 + | None => app_sub thy i rrls t
3.204 + end
3.205 +and app_sub thy i rrls t =
3.206 + ((*writeln("### app_sub: subterm = "^(term2str t));*)
3.207 + case t of
3.208 + Const (s, T) => (Const(s, T), [], false)
3.209 + | Free (s, T) => (Free(s, T), [], false)
3.210 + | Var (n, T) => (Var(n, T), [], false)
3.211 + | Bound i => (Bound i, [], false)
3.212 + | Abs (s, T, body) =>
3.213 + let val (t', asm, rew) = app_rev thy i rrls body
3.214 + in (Abs(s, T, t'), asm, rew) end
3.215 + | t1 $ t2 =>
3.216 + let val (t2', asm2, rew2) = app_rev thy i rrls t2
3.217 + in if rew2 then (t1 $ t2', asm2, true)
3.218 + else let val (t1', asm1, rew1) = app_rev thy i rrls t1
3.219 + in if rew1 then (t1' $ t2, asm1, true)
3.220 + else (t1 $ t2, [], false) end
3.221 + end);
3.222 +
3.223 +
3.224 +
3.225 +(*.rewriting without argument [] for rew_ord.*)
3.226 +fun eval_true thy terms rls = eval__true thy 1 terms [] rls;
3.227 +
3.228 +
3.229 +(*.rewriting without internal argument [] for rew_ord.*)
3.230 +fun rewrite_ thy rew_ord erls bool thm term =
3.231 + rewrite__ thy 1 [] rew_ord erls bool thm term;
3.232 +(*.distinguish between (normal) ruleset and reverse-ruleset.*)
3.233 +fun rewrite_set_ thy bool (**)rls(* as Rls _*) term =
3.234 + rewrite__set_ thy 1 bool [] rls term
3.235 +(*| rewrite_set_ thy _ (*Rrls ...*)rrls term = 7.3.03-->rewrite__set_
3.236 + let val (t', asm, rew) = app_rev thy i rrls term
3.237 + in if rew then Some (t', asm)
3.238 + else None end*);
3.239 +
3.240 +
3.241 +fun subs'2subst thy (s:subs') =
3.242 + (((map (apfst (term_of o the o (parse thy))))
3.243 + o (map (apsnd (term_of o the o (parse thy))))) s):subst;
3.244 +
3.245 +(*.variants of rewrite.*)
3.246 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst,
3.247 + thus the argument put_asm IS NOT NECESSARY -- FIXME*)
3.248 +(* val (rew_ord,rls,put_asm,thm,ct)=
3.249 + (e_rew_ord,poly_erls,false,num_str d1_isolate_add2,t);
3.250 + *)
3.251 +fun rewrite_inst_ (thy:theory) rew_ord (rls:rls) (put_asm:bool)
3.252 + (subst:(term * term) list) (thm:thm) (ct:term) =
3.253 + rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
3.254 +
3.255 +fun rewrite_set_inst_ (thy:theory)
3.256 + (put_asm:bool) (subst:(term * term) list) (rls:rls) (ct:term) =
3.257 + (*let
3.258 + val subst = subs'2subst thy subs';
3.259 + val subrls = instantiate_rls subs' rls
3.260 + in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct
3.261 + (*end*);
3.262 +
3.263 +
3.264 +
3.265 +(*. search ct for adjacent numerals and calculate them by operator isa_fn .*)
3.266 +fun calculate_ thy isa_fn ct =
3.267 + let val ct = app_num_tr'2 ct
3.268 + in case get_calculation_ thy isa_fn ct of
3.269 + None => None
3.270 + | Some (thmID, thm) =>
3.271 + (let val Some (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct
3.272 + in Some (rew,(thmID, thm)) end)
3.273 + handle _ => error ("calculate_: "^thmID^" does not rewrite")
3.274 + end;
3.275 +(*
3.276 +> val thy = InsSort.thy;
3.277 +> val op_ = "le"; (* < *)
3.278 +> val ct = (the o (parse thy))
3.279 + "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])";
3.280 +> calculate_ thy op_ ct;
3.281 + Some
3.282 + ("foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])",
3.283 + "(#1 < #3) = True") : (cterm * thm) option *)
3.284 +
3.285 +
3.286 +(* for test-printouts:
3.287 +val _ = writeln("in rew_sub : "^( Sign.string_of_term (sign_of thy) t))
3.288 +val _ = writeln("in eval_true: prems= "^(commas (map (Sign.string_of_term (sign_of thy)) prems')))
3.289 +*)
3.290 +
3.291 +
3.292 +
3.293 +
3.294 +
3.295 +
3.296 +fun get_rls_scr rs' = ((#scr o rep_rls o the o assoc') (!ruleset',rs'))
3.297 + handle _ => raise error ("get_rls_scr: no script for "^rs');
3.298 +
3.299 +
3.300 +(*make_thm added to Pure/thm.ML*)
3.301 +fun mk_thm thy str =
3.302 + let val t = (term_of o the o (parse thy)) str
3.303 + val t' = case t of
3.304 + Const ("==>",_) $ _ $ _ => t
3.305 + | _ => Trueprop $ t
3.306 + in make_thm (cterm_of (sign_of thy) t') end;
3.307 +(*
3.308 + val str = "?r ^^^ 2 = ?r * ?r";
3.309 + val thm = realpow_twoI;
3.310 +
3.311 + val t1 = (#prop o rep_thm) (num_str thm);
3.312 + val t2 = Trueprop $ ((term_of o the o (parse thy)) str);
3.313 + t1 = t2;
3.314 +val it = true : bool ... !!!
3.315 + val th1 = (num_str thm);
3.316 + val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
3.317 + th1 = th2;
3.318 +ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
3.319 +
3.320 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3.321 + val str = "k ~= 0 ==> m * k / (n * k) = m / n";
3.322 + val thm = real_mult_div_cancel2;
3.323 +
3.324 + val t1 = (#prop o rep_thm) (num_str thm);
3.325 + val t2 = ((term_of o the o (parse thy)) str);
3.326 + t1 = t2;
3.327 +val it = false : bool ... Var .. Free
3.328 + val th1 = (num_str thm);
3.329 + val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
3.330 + th1 = th2;
3.331 +ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
3.332 +*)
3.333 +
3.334 +
3.335 +(*prints subgoal etc.
3.336 +((goal thy);(topthm()) o ) str; *)
3.337 +(*assume rejects scheme variables
3.338 + assume (cterm_of (sign_of thy) (Trueprop $
3.339 + (term_of o the o (parse thy)) str)); *)
3.340 +
3.341 +
3.342 +(* outcommented 18.11.xx, xx < 02 -------
3.343 +fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thm thm)
3.344 + | rul2rul' (Calc op_) = Calc' op_;
3.345 +fun rul'2rul thy (Thm'(thmid, ct')) =
3.346 + Thm (thmid, mk_thm thy ct')
3.347 + | rul'2rul thy' (Calc' op_) = Calc op_;
3.348 +
3.349 +
3.350 +fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) =
3.351 + Rls'{preconds'= map string_of_cterm preconds,
3.352 + rew_ord' = fst rew_ord,
3.353 + rules' = map rul2rul' rules}:rlsdat';
3.354 +
3.355 +fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord,
3.356 + rules'=rules}:rlsdat') =
3.357 + let val thy = the (assoc' (theory',thy'))
3.358 + in Rls{preconds = map (the o (parse thy)) preconds,
3.359 + rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))),
3.360 + rules = map (rul'2rul thy) rules}:rls end;
3.361 +
3.362 +fun assoc_rls (thy':theory') ((rlsid, rlsdat'):rls') =
3.363 + if (hd o explode) rlsid = "#"
3.364 + then Some (rls'2rls thy' rlsdat')
3.365 + else assoc (ruleset'(*the global value*), rlsid);
3.366 +------- *)
3.367 +
3.368 +fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
3.369 + (case explode thmid of
3.370 + "s"::"y"::"m"::"_"::id =>
3.371 + if hd id = "#"
3.372 + then mk_thm thy ct'
3.373 + else ((num_str o (get_thm thy)) (implode id)) RS sym
3.374 + | id =>
3.375 + if hd id = "#"
3.376 + then mk_thm thy ct'
3.377 + else (num_str o (get_thm thy)) thmid
3.378 + ) handle _ =>
3.379 + raise error ("assoc_thm': '"^thmid^"' not in '"^
3.380 + (theory2domID thy)^"' (and parents)");
3.381 +(*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3");
3.382 +val it = "6 = 2 * 3" : thm
3.383 +
3.384 +> assoc_thm' Isac.thy ("real_add_zero_left","");
3.385 +val it = "0 + ?z = ?z" : thm
3.386 +
3.387 +> assoc_thm' Isac.thy ("sym_real_add_zero_left","");
3.388 +val it = "?t = 0 + ?t" [.] : thm
3.389 +
3.390 +> assoc_thm' HOL.thy ("sym_real_add_zero_left","");
3.391 +*** Unknown theorem(s) "real_add_zero_left"
3.392 +*** assoc_thm': 'sym_real_add_zero_leftnot in 'HOL.thy' (and parents)
3.393 +
3.394 +uncaught exception ERROR*)
3.395 +
3.396 +(*.only use if assoc_thm' is not possible.
3.397 +fun assoc_thm (thmID:thmID) = ((the o assoc')(!theorem',thmID))
3.398 + handle _ => raise error ("ME_Isa: "^thmID^" not in system");*)
3.399 +
3.400 +
3.401 +fun parse' (thy:theory') (ct:cterm') =
3.402 + case parse ((the o assoc')(!theory',thy)) ct of
3.403 + None => None
3.404 + | Some ct => Some ((string_of_cterm ct):cterm');
3.405 +
3.406 +
3.407 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
3.408 + thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
3.409 +fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls')
3.410 + (put_asm:bool) (thm:thm') (ct:cterm') =
3.411 + let val thy = (the o assoc')(!theory',thy');
3.412 + in
3.413 + case rewrite_ thy
3.414 + ((the o assoc')(!rew_ord',rew_ord)) ((the o assoc')(!ruleset',rls))
3.415 + put_asm ((assoc_thm' thy) thm)
3.416 + ((term_of o the o (parse thy)) ct) of
3.417 + None => None
3.418 + | Some (t, ts) => Some (Sign.string_of_term (sign_of thy) t,
3.419 + map (Sign.string_of_term (sign_of thy)) ts)
3.420 + end;
3.421 +
3.422 +(*
3.423 +val thy = "RatArith.thy";
3.424 +val rew_ord = "dummy_ord";
3.425 +> val rls = "eval_rls";
3.426 +val put_asm = true;
3.427 +val thm = ("square_equation_left","");
3.428 +val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
3.429 +
3.430 +val Zthy = ((the o assoc')(!theory',thy));
3.431 +val Zrew_ord = ((the o assoc')(!rew_ord',rew_ord));
3.432 +val Zrls = ((the o assoc')(!ruleset',rls));
3.433 +val Zput_asm = put_asm;
3.434 +val Zthm = ((the o (assoc'_thm' thy)) thm);
3.435 +val Zct = ((the o (parse ((the o assoc')(!theory',thy)))) ct);
3.436 +
3.437 +rewrite_ Zthy Zrew_ord Zrls Zput_asm Zthm Zct;
3.438 +
3.439 + use"Isa99/interface_ME_ISA.sml";
3.440 +*)
3.441 +
3.442 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
3.443 + thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
3.444 +fun rewrite_set (thy':theory') (put_asm:bool)
3.445 + (rls:rls') (ct:cterm') =
3.446 + let val thy = (the o assoc')(!theory',thy');
3.447 + in
3.448 + case rewrite_set_ thy put_asm ((the o assoc')(!ruleset',rls))
3.449 + ((term_of o the o (parse thy)) ct) of
3.450 + None => None
3.451 + | Some (t, ts) => Some (Sign.string_of_term (sign_of thy) t,
3.452 + map (Sign.string_of_term (sign_of thy)) ts)
3.453 + end;
3.454 +
3.455 +(*evaluate list-expressions
3.456 + should work on term, and stand in Isa99/rewrite-parse.sml,
3.457 + but there list_rls <- eval_binop is not yet defined*)
3.458 +(*fun eval_listexpr' ct =
3.459 + let val rew = rewrite_set "ListG.thy" false "list_rls" ct;
3.460 + in case rew of
3.461 + Some (res,_) => res
3.462 + | None => ct end;-----------------30.9.02---*)
3.463 +fun eval_listexpr_ thy srls t =
3.464 + let val rew = rewrite_set_ thy false srls t;
3.465 + in case rew of
3.466 + Some (res,_) => res
3.467 + | None => t end;
3.468 +
3.469 +
3.470 +fun get_calculation' (thy:theory') op_ (ct:cterm') =
3.471 + case get_calculation_ ((the o assoc')(!theory',thy)) op_
3.472 + ((app_num_tr'2 o term_of o the o
3.473 + (parse ((the o assoc')(!theory',thy)))) ct) of
3.474 + None => None
3.475 + | Some (thmid, thm) =>
3.476 + Some ((thmid, string_of_thm thm):thm');
3.477 +
3.478 +fun calculate (thy':theory') op_ (ct:cterm') =
3.479 + let val thy = (the o assoc')(!theory',thy');
3.480 + in
3.481 + case calculate_ thy op_
3.482 + ((term_of o the o (parse thy)) ct) of
3.483 + None => None
3.484 + | Some (ct,(thmID,thm)) =>
3.485 + Some (Sign.string_of_term (sign_of thy) ct,
3.486 + (thmID, string_of_thm thm):thm')
3.487 + end;
3.488 +(*
3.489 +fun instantiate'' thy' subs ((thmid,ct'):thm') =
3.490 + let val thmid_ = implode ("#"::(explode thmid)) (*see type thm'*)
3.491 + in (thmid_, (string_of_thm o (read_instantiate subs))
3.492 + ((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end;
3.493 +
3.494 +fun instantiate_rls' thy' subs (rls:rls') =
3.495 + rls2rls' (instantiate_rls subs ((the o (assoc_rls thy')) rls)):rlsdat';
3.496 +
3.497 +... problem with these functions:
3.498 +> val thm = mk_thm thy "(bdv + a = b) = (bdv = b - a)";
3.499 +val thm = "(bdv + a = b) = (bdv = b - a)" : thm
3.500 +> show_types:=true; thm;
3.501 +val it = "((bdv::'a) + (a::'a) = (b::'a)) = (bdv = b - a)" : thm
3.502 +... and this doesn't match because of too general typing (?!)
3.503 + and read_insitantiate doesn't instantiate the types (?!)
3.504 +=== solutions:
3.505 +(1) hard-coded type-instantiation ("'a", "RatArith.rat")
3.506 +(2) instantiate', instantiate ... no help by isabelle-users@ !!!
3.507 +=== conclusion:
3.508 + rewrite_inst, rewrite_set_inst circumvent the problem,
3.509 + according functions out-commented with 'instantiate''
3.510 +*)
3.511 +
3.512 +(* instantiate''
3.513 +fun instantiate'' thy' subs ((thmid,ct'):thm') =
3.514 + let
3.515 + val thmid_ = implode ("#"::(explode thmid)); (*see type thm'*)
3.516 + val thy = (the o assoc')(!theory',thy');
3.517 + val typs = map (#T o rep_cterm o the o (parse thy))
3.518 + ((snd o split_list) subs);
3.519 + val ctyps = map
3.520 + ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o (parse thy))
3.521 + ((snd o split_list) subs);
3.522 +
3.523 +> val thy' = "RatArith.thy";
3.524 +> val subs = [("bdv","x::rat"),("zzz","z::nat")];
3.525 +> (the o (parse ((the o assoc')(!theory',thy')))) "x::rat";
3.526 +> (#T o rep_cterm o the o (parse ((the o assoc')(!theory',thy'))));
3.527 +
3.528 +> val ctyp = ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o
3.529 + (parse ((the o assoc')(!theory',thy')))) "x::rat";
3.530 +> val bdv = (the o (parse thy)) "bdv";
3.531 +> val x = (the o (parse thy)) "x";
3.532 +> (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
3.533 + handle e => print_exn e;
3.534 +uncaught exception THM
3.535 + raised at: thm.ML:1085.18-1085.69
3.536 + thm.ML:1092.34
3.537 + goals.ML:536.61
3.538 +
3.539 +> val bdv = (the o (parse thy)) "bdv::nat";
3.540 +> val x = (the o (parse thy)) "x::nat";
3.541 +> (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
3.542 + handle e => print_exn e;
3.543 +uncaught exception THM
3.544 + raised at: thm.ML:1085.18-1085.69
3.545 + thm.ML:1092.34
3.546 + goals.ML:536.61
3.547 +
3.548 +> (instantiate' [Some ctyp] [] isolate_bdv_add)
3.549 + handle e => print_exn e;
3.550 +uncaught exception TYPE
3.551 + raised at: drule.ML:613.13-615.44
3.552 + goals.ML:536.61
3.553 +
3.554 +> val repct = (rep_cterm o the o (parse ((the o assoc')(!theory',thy')))) "x::rat";
3.555 +*)
3.556 +
3.557 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
3.558 + thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
3.559 +fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls')
3.560 + (put_asm:bool) subs (thm:thm') (ct:cterm') =
3.561 + let
3.562 + val thy = (the o assoc')(!theory',thy');
3.563 + val thm = assoc_thm' thy thm; (*28.10.02*)
3.564 + (*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*)
3.565 + in
3.566 + case rewrite_ thy
3.567 + ((the o assoc')(!rew_ord',rew_ord)) ((the o assoc')(!ruleset',rls))
3.568 + put_asm (*sub*)thm ((term_of o the o (parse thy)) ct) of
3.569 + None => None
3.570 + | Some (ctm, ctms) =>
3.571 + Some ((Sign.string_of_term (sign_of thy) ctm):cterm',
3.572 + (map (Sign.string_of_term (sign_of thy)) ctms):cterm' list)
3.573 + end;
3.574 +
3.575 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
3.576 + thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
3.577 +fun rewrite_set_inst (thy':theory') (put_asm:bool)
3.578 + subs' (rls:rls') (ct:cterm') =
3.579 + let
3.580 + val thy = (the o assoc')(!theory',thy');
3.581 + val rls = assoc_rls rls
3.582 + val subst = subs'2subst thy subs'
3.583 + (*val subrls = instantiate_rls subs ((the o assoc')(!ruleset',rls))*)
3.584 + in
3.585 + case rewrite_set_inst_ thy put_asm subst (*sub*)rls
3.586 + ((term_of o the o (parse thy)) ct) of
3.587 + None => None
3.588 + | Some (t, ts) => Some (Sign.string_of_term (sign_of thy) t,
3.589 + map (Sign.string_of_term (sign_of thy)) ts)
3.590 + end;
3.591 +
3.592 +
3.593 +(*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *)
3.594 +fun eval_true' (thy':theory') (rls':rls') (Const ("True",_)) = true
3.595 +
3.596 + | eval_true' (thy':theory') (rls':rls') (t:term) =
3.597 +(* val thy'="Isac.thy"; val rls'="eval_rls"; val t=hd pres';
3.598 + *)
3.599 + let val ct' = Sign.string_of_term (sign_of (assoc_thy thy')) t;
3.600 + in case rewrite_set thy' false rls' ct' of
3.601 + Some ("True",_) => true
3.602 + | _ => false
3.603 + end;
3.604 +fun eval_true_ _ _ (Const ("True",_)) = true
3.605 + | eval_true_ (thy':theory') rls t =
3.606 + case rewrite_set_ (assoc_thy thy') false rls t of
3.607 + Some (Const ("True",_),_) => true
3.608 + | _ => false;
3.609 +
3.610 +(*
3.611 +val test_rls =
3.612 + Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right),
3.613 + rules = [Calc ("matches",eval_matches "")
3.614 + ],
3.615 + scr = Script ((term_of o the o (parse thy))
3.616 + "empty_script")
3.617 + }:rls;
3.618 +
3.619 +
3.620 +
3.621 + rewrite_set_ Isac.thy eval_rls false test_rls
3.622 + ((the o (parse thy)) "matches (?a = ?b) (x = #0)");
3.623 + val xxx = (term_of o the o (parse thy))
3.624 + "matches (?a = ?b) (x = #0)";
3.625 + eval_matches """" xxx thy;
3.626 +Some ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True",
3.627 + Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
3.628 +
3.629 +
3.630 +
3.631 + rewrite_set_ Isac.thy eval_rls false eval_rls
3.632 + ((the o (parse thy)) "contains_root (sqrt #0)");
3.633 +val it = Some ("True",[]) : (cterm * cterm list) option
3.634 +
3.635 +
3.636 +
3.637 +
3.638 +*)
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/sml/Scripts/scrtools.sml Thu Apr 17 18:01:03 2003 +0200
4.3 @@ -0,0 +1,108 @@
4.4 +(* tools which depend on Script.thy and thus are not in term_G.sml
4.5 + *)
4.6 +
4.7 +fun is_reall_dsc
4.8 + (Const(_,Type("fun",[Type("List.list",
4.9 + [Type ("real",[])]),_]))) = true
4.10 + | is_reall_dsc
4.11 + (Const(_,Type("fun",[Type("List.list",
4.12 + [Type ("real",[])]),_])) $ t) = true
4.13 + | is_reall_dsc _ = false;
4.14 +fun is_booll_dsc
4.15 + (Const(_,Type("fun",[Type("List.list",
4.16 + [Type ("bool",[])]),_]))) = true
4.17 + | is_booll_dsc
4.18 + (Const(_,Type("fun",[Type("List.list",
4.19 + [Type ("bool",[])]),_])) $ t) = true
4.20 + | is_booll_dsc _ = false;
4.21 +(*
4.22 +> val t = (term_of o the o (parse thy)) "relations";
4.23 +> atomtyp (type_of t);
4.24 +*** Type (fun,[
4.25 +*** Type (List.list,[
4.26 +*** Type (bool,[])
4.27 +*** ]
4.28 +*** Type (Tools.una,[])
4.29 +*** ]
4.30 +> is_booll_dsc t;
4.31 +val it = true : bool
4.32 +> is_reall_dsc t;
4.33 +val it = false : bool
4.34 +*)
4.35 +
4.36 +fun is_list_dsc (Const(_,Type("fun",[Type("List.list",_),_]))) = true
4.37 + | is_list_dsc (Const(_,Type("fun",[Type("List.list",_),
4.38 + _])) $ t) = true
4.39 + | is_list_dsc _ = false;
4.40 +(*
4.41 +> val t = (term_of o the o (parse thy))
4.42 + "additional_relations [a=b,c=(d::real)]";
4.43 +> is_list_dsc t;
4.44 +val it = true : bool
4.45 +> is_list_dsc (head_of t);
4.46 +val it = true : bool
4.47 +
4.48 +> val t = (term_of o the o (parse thy))"max_relation (A=#2*a*b-a^^^#2)";
4.49 +> is_list_dsc t;
4.50 +val it = false : bool
4.51 +> is_list_dsc (head_of t);
4.52 +val it = false : bool
4.53 +> val t = (term_of o the o (parse thy)) "testdscforlist";
4.54 +> is_list_dsc (head_of t);
4.55 +val it = true : bool
4.56 +*)
4.57 +
4.58 +
4.59 +fun is_dscforlist (Const(_,Type("fun",[_,
4.60 + Type("Tools.unl",_)]))) = true
4.61 + | is_dscforlist _ = false;
4.62 +(*
4.63 +> val t = (term_of o the o (parse thy)) "testdscforlist";
4.64 +> is_dscforlist t;
4.65 +val it = true : bool
4.66 +> val t = (term_of o the o (parse thy)) "maximum";
4.67 +> is_dscforlist t;
4.68 +val it = false : bool
4.69 +*)
4.70 +
4.71 +fun is_dsc (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) = true
4.72 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.una",_)]))) = true
4.73 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true
4.74 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.str",_)]))) = true
4.75 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) = true
4.76 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))= true
4.77 + | is_dsc (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))= true
4.78 + | is_dsc _ = false;
4.79 +(*
4.80 +> val t = (term_of o the o (parse thy)) "maximum";
4.81 +> is_dsc t;
4.82 +val it = true : bool
4.83 +> val t = (term_of o the o (parse thy)) "testdscforlist";
4.84 +> is_dsc t;
4.85 +val it = true : bool
4.86 +
4.87 +> val t = (head_of o term_of o the o (parse thy)) "maximum A";
4.88 +> is_dsc t;
4.89 +val it = true : bool
4.90 +> val t = (head_of o term_of o the o (parse thy))
4.91 + "fixed_values [R=(R::real)]";
4.92 +> is_dsc t;
4.93 +val it = true : bool
4.94 +*)
4.95 +
4.96 +
4.97 +(*make the term 'Subproblem (domID, pblID)' to a formula for frontend;
4.98 + needs to be here after def. Subproblem in Script.thy*)
4.99 +val t as (subpbl_t $ (pair_t $ Free (domID,_) $ pblID)) =
4.100 + (term_of o the o (parse Script.thy))
4.101 + "Subproblem (Isac,[equation,univar])";
4.102 +val Free (_, ID_type) = (term_of o the o (parse Script.thy)) "x::ID";
4.103 +
4.104 +fun subpbl domID pblID =
4.105 + subpbl_t $ (pair_t $ Free (domID,ID_type) $
4.106 + (((list2isalist ID_type) o (map (mk_free ID_type))) pblID));
4.107 +(*> subpbl "Isac" ["equation","univar"] = t;
4.108 +val it = true : bool *)
4.109 +
4.110 +(*6.8.02 ...*)
4.111 +
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/sml/Scripts/term_G.sml Thu Apr 17 18:01:03 2003 +0200
5.3 @@ -0,0 +1,1001 @@
5.4 +(* use"Isa02/term_G.sml";
5.5 + WN.22.10.99
5.6 + functions closely related to original isabelle-98-1 functions,
5.7 + distinguished by ..._G
5.8 + use"term_G.sml";
5.9 +*)
5.10 +
5.11 +(*
5.12 +> cterm_of (sign_of thy) a_term;
5.13 +val it = "empty" : cterm *)
5.14 +
5.15 +
5.16 +
5.17 +fun match thy t pat =
5.18 + (snd (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)))
5.19 + handle _ => [];
5.20 +fun matches thy t pat = if match thy t pat = [] then false else true;
5.21 +(*
5.22 +> val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
5.23 +> val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
5.24 + !^^^^^^^^!... necessary for Pattern.match
5.25 +> val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
5.26 + val insts =
5.27 + ([],
5.28 + [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
5.29 + (("a",0),Free ("3","RealDef.real"))])
5.30 + : (indexname * typ) list * (indexname * term) list*)
5.31 +
5.32 +
5.33 +fun idt str 0 = " "
5.34 + | idt str n = str ^ idt str (n-1);
5.35 +fun indent 0 = ""
5.36 + | indent n = ". " ^ indent(n-1);
5.37 +(*
5.38 + datatype typ =
5.39 + Type of string * typ list |
5.40 + TFree of string * sort |
5.41 + TVar of indexname * sort
5.42 +> ("wer",1):indexname;
5.43 +> ["wer"]:sort;
5.44 +*)
5.45 +fun atomtyp t =
5.46 + let
5.47 + fun ato n (Type (s,[])) =
5.48 + ("\n*** "^indent n^"Type ("^s^",[])")
5.49 + | ato n (Type (s,Ts)) =
5.50 + ("\n*** "^indent n^"Type ("^s^",["^ atol (n+1) Ts)
5.51 +
5.52 + | ato n (TFree (s,sort)) =
5.53 + ("\n*** "^indent n^"TFree ("^s^",["^ strs2str' sort)
5.54 +
5.55 + | ato n (TVar ((s,i),sort)) =
5.56 + ("\n*** "^indent n^"TVar (("^s^","^
5.57 + string_of_int i ^ strs2str' sort)
5.58 + and atol n [] =
5.59 + ("\n*** "^indent n^"]")
5.60 + | atol n (T::Ts) = (ato n T ^ atol n Ts)
5.61 +in print (ato 0 t ^ "\n") end;
5.62 +
5.63 +(*
5.64 +> val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
5.65 +> atomtyp T;
5.66 +*** Type (fun,[
5.67 +*** Type (RealDef.real,[])
5.68 +*** Type (fun,[
5.69 +*** Type (IntDef.int,[])
5.70 +*** Type (nat,[])
5.71 +*** ]
5.72 +*** ]
5.73 +*)
5.74 +fun atomt t =
5.75 + let fun ato (Const(a,T)) n =
5.76 + print("\n*** "^indent n^"Const ( "^a^")")
5.77 + | ato (Free (a,T)) n =
5.78 + print("\n*** "^indent n^"Free ( "^a^", "^")")
5.79 + | ato (Var ((a,ix),T)) n =
5.80 + print("\n*** "^indent n^"Var (("^a^", "^(string_of_int ix)^"), "^")")
5.81 + | ato (Bound ix) n =
5.82 + print("\n*** "^indent n^"Bound "^(string_of_int ix))
5.83 + | ato (Abs(a,T,body)) n =
5.84 + (print("\n*** "^indent n^"Abs( "^a^",..");ato body (n+1))
5.85 + | ato (f$t') n = (ato f n; ato t' (n+1))
5.86 + in print"\n*** -------------"; ato t 0; print"\n" end;
5.87 +
5.88 +fun atomty thy t =
5.89 + let fun ato (Const(a,T)) n =
5.90 + print("\n*** "^indent n^"Const ( "^a^", "^
5.91 + (Sign.string_of_typ (sign_of thy) T)^")")
5.92 + | ato (Free (a,T)) n =
5.93 + print("\n*** "^indent n^"Free ( "^a^", "^
5.94 + (Sign.string_of_typ (sign_of thy) T)^")")
5.95 + | ato (Var ((a,ix),T)) n =
5.96 + print("\n*** "^indent n^"Var (("^a^", "^(string_of_int ix)^"), "^
5.97 + (Sign.string_of_typ (sign_of thy) T)^")")
5.98 + | ato (Bound ix) n =
5.99 + print("\n*** "^indent n^"Bound "^(string_of_int ix))
5.100 + | ato (Abs(a,T,body)) n =
5.101 + (print("\n*** "^indent n^"Abs( "^a^", "^
5.102 + (Sign.string_of_typ (sign_of thy) T)^",..");ato body (n+1))
5.103 + | ato (f$t') n = (ato f n; ato t' (n+1))
5.104 + in print"\n*** -------------"; ato t 0; print"\n" end;
5.105 +
5.106 +fun term_detail2str t =
5.107 + let fun ato (Const(a,T)) n =
5.108 + "\n*** "^indent n^"Const ( "^a^")"
5.109 + | ato (Free (a,T)) n =
5.110 + "\n*** "^indent n^"Free ( "^a^", "^")"
5.111 + | ato (Var ((a,ix),T)) n =
5.112 + "\n*** "^indent n^"Var (("^a^", "^string_of_int ix^"), "^")"
5.113 + | ato (Bound ix) n =
5.114 + "\n*** "^indent n^"Bound "^string_of_int ix
5.115 + | ato (Abs(a,T,body)) n =
5.116 + "\n*** "^indent n^"Abs( "^a^",.."^ato body (n+1)
5.117 + | ato (f$t') n = ato f n^ato t' (n+1)
5.118 + in "\n*** -------------"^ato t 0^"\n" end;
5.119 +fun term_str thy (Const(s,_)) = s
5.120 + | term_str thy (Free(s,_)) = s
5.121 + | term_str thy (Var((s,i),_)) = s^(string_of_int i)
5.122 + | term_str thy (Bound i) = "B."^(string_of_int i)
5.123 + | term_str thy (Abs(s,_,_)) = s
5.124 + | term_str thy t = raise error("term_str not for "^
5.125 + (Sign.string_of_term (sign_of thy) t));
5.126 +
5.127 +
5.128 +
5.129 +fun int_of_str str =
5.130 + let val ss = explode str
5.131 + val str' = case ss of
5.132 + "("::s => drop_last s | _ => ss
5.133 + in case BasisLibrary.Int.fromString (implode str') of
5.134 + SOME i => Some i
5.135 + | NONE => None end;
5.136 +(*
5.137 +> int_of_str "123";
5.138 +val it = Some 123 : int option > int_of_str "(-123)";
5.139 +val it = Some 123 : int option > int_of_str "#123";
5.140 +val it = None : int option > int_of_str "-123";
5.141 +val it = Some ~123 : int option *)
5.142 +fun int_of_str' str =
5.143 + case int_of_str str of
5.144 + Some i => i
5.145 + | None => raise TERM ("int_of_string: no int-string",[]);
5.146 +
5.147 +fun is_numeral str = case int_of_str str of
5.148 + Some _ => true
5.149 + | None => false;
5.150 +val is_no = is_numeral;
5.151 +fun is_num (Free (s,_)) = if is_numeral s then true else false
5.152 + | is_num _ = false;
5.153 +(*>
5.154 +> is_num ((term_of o the o (parse thy)) "#1");
5.155 +val it = true : bool
5.156 +> is_num ((term_of o the o (parse thy)) "#-1");
5.157 +val it = true : bool
5.158 +> is_num ((term_of o the o (parse thy)) "a123");
5.159 +val it = false : bool
5.160 +*)
5.161 +
5.162 +fun vars t =
5.163 + let
5.164 + fun scan vs (Const(s,T)) = vs
5.165 + | scan vs (t as Free(s,T)) = if is_no s then vs else t::vs
5.166 + | scan vs (t as Var((s,i),T)) = t::vs
5.167 + | scan vs (Bound i) = vs
5.168 + | scan vs (Abs(s,T,t)) = scan vs t
5.169 + | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
5.170 + in (distinct o (scan [])) t end;
5.171 +
5.172 +fun vars_str t =
5.173 + let
5.174 + fun scan vs (Const(s,T)) = vs
5.175 + | scan vs (t as Free(s,T)) = if is_no s then vs else s::vs
5.176 + | scan vs (t as Var((s,i),T)) = (s^"_"^(string_of_int i))::vs
5.177 + | scan vs (Bound i) = vs
5.178 + | scan vs (Abs(s,T,t)) = scan vs t
5.179 + | scan vs (t1 $ t2) = (scan vs t1) @ (scan vs t2)
5.180 + in (distinct o (scan [])) t end;
5.181 +
5.182 +fun free2str (Free (s,_)) = s
5.183 + | free2str t = raise error ("free2str not for "^
5.184 + (Sign.string_of_term (sign_of thy) t));
5.185 +fun free2int (t as Free (s, _)) = (((the o int_of_str) s)
5.186 + handle _ => raise error ("free2int: "^term_detail2str t))
5.187 + | free2int t = raise error ("free2int: "^term_detail2str t);
5.188 +
5.189 +(*27.8.01: unused*)
5.190 +fun var2free (t as Const(s,T)) = t
5.191 + | var2free (t as Free(s,T)) = t
5.192 + | var2free (Var((s,i),T)) = Free(s,T)
5.193 + | var2free (t as Bound i) = t
5.194 + | var2free (Abs(s,T,t)) = Abs(s,T,var2free t)
5.195 + | var2free (t1 $ t2) = (var2free t1) $ (var2free t2);
5.196 +
5.197 +(*27.8.01: doesn't find some subterm ???!???*)
5.198 +fun free2var (t as Const(s,T)) = t
5.199 + | free2var (t as Free(s,T)) = if is_no s then t else Var((s,0),T)
5.200 + | free2var (t as Var((s,i),T)) = t
5.201 + | free2var (t as Bound i) = t
5.202 + | free2var (Abs(s,T,t)) = Abs(s,T,free2var t)
5.203 + | free2var (t1 $ t2) = (free2var t1) $ (free2var t2);
5.204 +
5.205 +
5.206 +fun mk_listT T = Type ("List.list", [T]);
5.207 +fun list_const T =
5.208 + Const("List.list.Cons", [T, mk_listT T] ---> mk_listT T);
5.209 +(*28.8.01: TODO: get type from head of list: 1 arg less!!!*)
5.210 +fun list2isalist T [] = Const("List.list.Nil",mk_listT T)
5.211 + | list2isalist T (t::ts) = (list_const T) $ t $ (list2isalist T ts);
5.212 +(*
5.213 +> val tt = (term_of o the o (parse thy)) "R=(R::real)";
5.214 +> val TT = type_of tt;
5.215 +> val ss = list2isalist TT [tt,tt,tt];
5.216 +> cterm_of (sign_of thy) ss;
5.217 +val it = "[R = R, R = R, R = R]" : cterm *)
5.218 +
5.219 +fun isalist2list ls =
5.220 + let
5.221 + fun get es (Const("List.list.Cons",_) $ t $ ls) = get (t::es) ls
5.222 + | get es (Const("List.list.Nil",_)) = es
5.223 + | get _ _ = raise error "Isalist2list applied to NON-list"
5.224 + in (rev o (get [])) ls end;
5.225 +(*
5.226 +> val (Some ct) = parse thy "[a=b,c=d,e=f]";
5.227 +> val ces = map (cterm_of (sign_of thy)) (isalist2list (term_of ct));
5.228 +val it = ["a = b","c = d","e = f"] : cterm list
5.229 +*)
5.230 +
5.231 +
5.232 +
5.233 +val prop = Type ("prop",[]); (* ~/Diss.99/Integers-Isa/tools.sml*)
5.234 +val bool = Type ("bool",[]); (* Integ.int *)
5.235 +val Trueprop = Const("Trueprop",bool-->prop);
5.236 +fun mk_prop t = Trueprop $ t;
5.237 +val true_as_term = Const("True",bool);
5.238 +val false_as_term = Const("False",bool);
5.239 +val true_as_cterm = cterm_of (sign_of thy) true_as_term;
5.240 +val false_as_cterm = cterm_of (sign_of thy) false_as_term;
5.241 +
5.242 +infixr 5 -->; (* /Pure/term.ML *)
5.243 +infixr --->; (* /Pure/term.ML *)
5.244 +fun S --> T = Type("fun",[S,T]); (* /Pure/term.ML *)
5.245 +val op ---> = foldr (op -->); (* /Pure/term.ML *)
5.246 +fun list_implies ([], B) = B : term
5.247 + | list_implies (A::AS, B) = implies $ A $ list_implies(AS,B);(* /term.ML *)
5.248 +
5.249 +
5.250 +
5.251 +(** substitution **)
5.252 +
5.253 +fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = (* = thm.ML *)
5.254 + match_bvs(s, t, if x="" orelse y="" then al
5.255 + else (x,y)::al)
5.256 + | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
5.257 + | match_bvs(_,_,al) = al;
5.258 +fun ren_inst(insts,prop,pat,obj) = (* = thm.ML *)
5.259 + let val ren = match_bvs(pat,obj,[])
5.260 + fun renAbs(Abs(x,T,b)) =
5.261 + Abs(case assoc_string(ren,x) of None => x
5.262 + | Some(y) => y, T, renAbs(b))
5.263 + | renAbs(f$t) = renAbs(f) $ renAbs(t)
5.264 + | renAbs(t) = t
5.265 + in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;
5.266 +
5.267 +
5.268 +
5.269 +
5.270 +
5.271 +
5.272 +fun dest_equals' (Const("op =",_) $ t $ u) = (t,u)(* logic.ML: Const("=="*)
5.273 + | dest_equals' t = raise TERM("dest_equals'", [t]);
5.274 +fun is_equality (Const("op =",_) $ t $ u) = true (* logic.ML: Const("=="*)
5.275 + | is_equality _ = false;
5.276 +fun mk_equality (t,u) = (Const("op =",[type_of t,type_of u]--->bool) $ t $ u);
5.277 +fun is_expliceq (Const("op =",_) $ (Free _) $ u) = true
5.278 + | is_expliceq _ = false;
5.279 +fun strip_trueprop (Const("Trueprop",_) $ t) = t
5.280 + | strip_trueprop t = t;
5.281 +(* | strip_trueprop t = raise TERM("strip_trueprop", [t]);
5.282 +*)
5.283 +
5.284 +(*.(A1==>...An==>B) goes to (A1==>...An==>).*)
5.285 +fun strip_imp_prems' (Const("==>", T) $ A $ t) =
5.286 + let fun coll_prems As (Const("==>", _) $ A $ t) =
5.287 + coll_prems (As $ (implies $ A)) t
5.288 + | coll_prems As _ = Some As
5.289 + in coll_prems (implies $ A) t end
5.290 + | strip_imp_prems' _ = None; (* logic.ML: term -> term list*)
5.291 +(*
5.292 + val thm = real_mult_div_cancel1;
5.293 + val prop = (#prop o rep_thm) thm;
5.294 + atomt prop;
5.295 +*** -------------
5.296 +*** Const ( ==>)
5.297 +*** . Const ( Trueprop)
5.298 +*** . . Const ( Not)
5.299 +*** . . . Const ( op =)
5.300 +*** . . . . Var ((k, 0), )
5.301 +*** . . . . Const ( 0)
5.302 +*** . Const ( Trueprop)
5.303 +*** . . Const ( op =) *** .............
5.304 + val Some t = strip_imp_prems' ((#prop o rep_thm) thm);
5.305 + atomt t;
5.306 +*** -------------
5.307 +*** Const ( ==>)
5.308 +*** . Const ( Trueprop)
5.309 +*** . . Const ( Not)
5.310 +*** . . . Const ( op =)
5.311 +*** . . . . Var ((k, 0), )
5.312 +*** . . . . Const ( 0)
5.313 +
5.314 + val thm = real_le_anti_sym;
5.315 + val prop = (#prop o rep_thm) thm;
5.316 + atomt prop;
5.317 +*** -------------
5.318 +*** Const ( ==>)
5.319 +*** . Const ( Trueprop)
5.320 +*** . . Const ( op <=)
5.321 +*** . . . Var ((z, 0), )
5.322 +*** . . . Var ((w, 0), )
5.323 +*** . Const ( ==>)
5.324 +*** . . Const ( Trueprop)
5.325 +*** . . . Const ( op <=)
5.326 +*** . . . . Var ((w, 0), )
5.327 +*** . . . . Var ((z, 0), )
5.328 +*** . . Const ( Trueprop)
5.329 +*** . . . Const ( op =)
5.330 +*** .............
5.331 + val Some t = strip_imp_prems' ((#prop o rep_thm) thm);
5.332 + atomt t;
5.333 +*** -------------
5.334 +*** Const ( ==>)
5.335 +*** . Const ( Trueprop)
5.336 +*** . . Const ( op <=)
5.337 +*** . . . Var ((z, 0), )
5.338 +*** . . . Var ((w, 0), )
5.339 +*** . Const ( ==>)
5.340 +*** . . Const ( Trueprop)
5.341 +*** . . . Const ( op <=)
5.342 +*** . . . . Var ((w, 0), )
5.343 +*** . . . . Var ((z, 0), )
5.344 +*)
5.345 +
5.346 +(*. (A1==>...An==>) (B) goes to (A1==>...An==>B), where B is lowest branch.*)
5.347 +fun ins_concl (Const("==>", T) $ A $ t) B = implies $ A $ (ins_concl t B)
5.348 + | ins_concl (Const("==>", T) $ A ) B = implies $ A $ B
5.349 + | ins_concl t B = raise TERM("ins_concl", [t, B]);
5.350 +(*
5.351 + val thm = real_le_anti_sym;
5.352 + val prop = (#prop o rep_thm) thm;
5.353 + val concl = Logic.strip_imp_concl prop;
5.354 + val Some prems = strip_imp_prems' prop;
5.355 + val prop' = ins_concl prems concl;
5.356 + prop = prop';
5.357 + atomt prop;
5.358 + atomt prop';
5.359 +*)
5.360 +
5.361 +
5.362 +fun vperm (Var _, Var _) = true (* Pure/thm.ML *)
5.363 + | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
5.364 + | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
5.365 + | vperm (t, u) = (t = u);
5.366 +
5.367 +fun var_perm (t, u) = (* Pure/thm.ML *)
5.368 + vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
5.369 +
5.370 +(* fun decomp_simp, Pure/thm.ML *)
5.371 +fun perm lhs rhs = var_perm (lhs, rhs) andalso not (lhs aconv rhs)
5.372 + andalso not (is_Var lhs);
5.373 +
5.374 +
5.375 +(*---6.1.00: Isa99
5.376 +fun char2int c = ord c - ord "0";
5.377 +
5.378 +fun rev_strl2int [s] = char2int s
5.379 + | rev_strl2int (s::ss) = char2int s + 10*(rev_strl2int ss)
5.380 + | rev_strl2int _ = raise ERROR;
5.381 +
5.382 + fun int_of_str str =
5.383 + let
5.384 + fun scan ("(" :: "+" :: is) =
5.385 + (case rev is of
5.386 + ")" :: si => rev_strl2int si
5.387 + | _ => raise error ("no number: "^str))
5.388 + | scan ("(" :: "-" :: is) =
5.389 + (case rev is of
5.390 + ")" :: si => (~1)*(rev_strl2int si)
5.391 + | _ => raise error ("no number: "^str))
5.392 + | scan ("(" :: is) =
5.393 + (case rev is of
5.394 + ")" :: si => rev_strl2int si
5.395 + | _ => raise error ("no number: "^str))
5.396 + | scan ( "+" :: is) = (rev_strl2int o rev) is
5.397 + | scan ( "-" :: is) = (~1)*((rev_strl2int o rev) is)
5.398 + | scan ( is) = (rev_strl2int o rev) is
5.399 + in (scan o skip_blanks o explode o strip_thy) str
5.400 + handle ERROR => raise error ("no number: "^str) end;
5.401 +---*)
5.402 +
5.403 +
5.404 +fun str_of_int n =
5.405 + if n < 0 then "-"^((string_of_int o abs) n)
5.406 + else string_of_int n;
5.407 +(*
5.408 +> str_of_int 1;
5.409 +val it = "1" : string > str_of_int ~1;
5.410 +val it = "-1" : string
5.411 +*)
5.412 +
5.413 +
5.414 +fun power b 0 = 1
5.415 + | power b n =
5.416 + if n>0 then b*(power b (n-1))
5.417 + else raise error ("power "^(str_of_int b)^" "^(str_of_int n));
5.418 +(*
5.419 +> power 2 3;
5.420 +val it = 8 : int
5.421 +> power ~2 3;
5.422 +val it = ~8 : int
5.423 +> power ~3 2;
5.424 +val it = 9 : int
5.425 +> power 3 ~2;
5.426 +*)
5.427 +fun gcd 0 b = b
5.428 + | gcd a b = if a < b then gcd (b mod a) a
5.429 + else gcd (a mod b) b;
5.430 +fun sign n = if n < 0 then ~1
5.431 + else if n = 0 then 0 else 1;
5.432 +fun sign2 n1 n2 = (sign n1) * (sign n2);
5.433 +
5.434 +infix dvd;
5.435 +fun d dvd n = n mod d = 0;
5.436 +
5.437 +fun divisors n =
5.438 + let fun pdiv ds d n =
5.439 + if d=n then d::ds
5.440 + else if d dvd n then pdiv (d::ds) d (n div d)
5.441 + else pdiv ds (d+1) n
5.442 + in pdiv [] 2 n end;
5.443 +
5.444 +divisors 30;
5.445 +divisors 32;
5.446 +divisors 60;
5.447 +divisors 11;
5.448 +
5.449 +fun doubles ds = (* ds is ordered *)
5.450 + let fun dbls ds [] = ds
5.451 + | dbls ds [i] = ds
5.452 + | dbls ds (i::i'::is) = if i=i' then dbls (i::ds) is
5.453 + else dbls ds (i'::is)
5.454 + in dbls [] ds end;
5.455 +(*> doubles [2,3,4];
5.456 +val it = [] : int list
5.457 +> doubles [2,3,3,5,5,7];
5.458 +val it = [5,3] : int list*)
5.459 +
5.460 +fun squfact 1 = 1
5.461 + | squfact n = foldl op* (1, (doubles o divisors) n);
5.462 +(*> squfact 30;
5.463 +val it = 1 : int
5.464 +> squfact 32;
5.465 +val it = 4 : int
5.466 +> squfact 60;
5.467 +val it = 2 : int
5.468 +> squfact 11;
5.469 +val it = 1 : int*)
5.470 +
5.471 +
5.472 +fun dest_type (Type(T,[])) = T
5.473 + | dest_type T =
5.474 + (atomtyp T;
5.475 + raise error ("... dest_type: not impl. for this type"));
5.476 +
5.477 +fun term_of_num ntyp n = Free (str_of_int n, ntyp);
5.478 +
5.479 +fun pairT T1 T2 = Type ("*", [T1, T2]);
5.480 +(*> val t = str2term "(1,2)";
5.481 +> type_of t = pairT HOLogic.realT HOLogic.realT;
5.482 +val it = true : bool
5.483 +*)
5.484 +fun PairT T1 T2 = ([T1, T2] ---> Type ("*", [T1, T2]));
5.485 +(*> val t = str2term "(1,2)";
5.486 +> val Const ("Pair",pT) $ _ $ _ = t;
5.487 +> pT = PairT HOLogic.realT HOLogic.realT;
5.488 +val it = true : bool
5.489 +*)
5.490 +fun pairt t1 t2 =
5.491 + Const ("Pair", PairT (type_of t1) (type_of t2)) $ t1 $ t2;
5.492 +(*> val t = str2term "(1,2)";
5.493 +> val (t1, t2) = (str2term "1", str2term "2");
5.494 +> t = pairt t1 t2;
5.495 +val it = true : bool*)
5.496 +
5.497 +
5.498 +fun num_of_term (t as Free (s,_)) =
5.499 + (case int_of_str s of
5.500 + Some s' => s'
5.501 + | None => raise error ("num_of_term not for "^
5.502 + (Sign.string_of_term (sign_of thy) t)))
5.503 + | num_of_term t = raise error ("num_of_term not for "^
5.504 + (Sign.string_of_term (sign_of thy) t));
5.505 +
5.506 +fun mk_factroot op_(*=thy.sqrt*) T fact root =
5.507 + Const ("op *", [T, T] ---> T) $ (term_of_num T fact) $
5.508 + (Const (op_, T --> T) $ term_of_num T root);
5.509 +(*
5.510 +val T = (type_of o term_of o the) (parse thy "#12::real");
5.511 +val t = mk_factroot "SqRoot.sqrt" T 2 3;
5.512 +cterm_of (sign_of thy) t;
5.513 +val it = "#2 * sqrt #3 " : cterm
5.514 +*)
5.515 +fun var_op_num v op_ optype ntyp n =
5.516 + Const (op_, optype) $ v $
5.517 + Free (str_of_int n, ntyp);
5.518 +
5.519 +fun num_op_var v op_ optype ntyp n =
5.520 + Const (op_,optype) $
5.521 + Free (str_of_int n, ntyp) $ v;
5.522 +
5.523 +fun num_op_num T1 T2 (op_,Top) n1 n2 =
5.524 + Const (op_,Top) $
5.525 + Free (str_of_int n1, T1) $ Free (str_of_int n2, T2);
5.526 +(*
5.527 +> val t = num_op_num "Int" 3 4;
5.528 +> atomty thy t;
5.529 +> string_of_cterm (cterm_of (sign_of thy) t);
5.530 +*)
5.531 +
5.532 +fun const_in str (Const _) = false
5.533 + | const_in str (Free (s,_)) = if strip_thy s = str then true else false
5.534 + | const_in str (Bound _) = false
5.535 + | const_in str (Var _) = false
5.536 + | const_in str (Abs (_,_,body)) = const_in str body
5.537 + | const_in str (f$u) = const_in str f orelse const_in str u;
5.538 +(*
5.539 +> val t = (term_of o the o (parse thy)) "6 + 5 * sqrt 4 + 3";
5.540 +> const_in "sqrt" t;
5.541 +val it = true : bool
5.542 +> val t = (term_of o the o (parse thy)) "6 + 5 * 4 + 3";
5.543 +> const_in "sqrt" t;
5.544 +val it = false : bool
5.545 +*)
5.546 +
5.547 +(*used for calculating built in binary operations in Isabelle2002->Float.ML
5.548 +fun calc "op +" (n1, n2) = n1+n2
5.549 + | calc "op -" (n1, n2) = n1-n2
5.550 + | calc "op *" (n1, n2) = n1*n2
5.551 + | calc "HOL.divide"(n1, n2) = n1 div n2
5.552 + | calc "Atools.pow"(n1, n2) = power n1 n2
5.553 + | calc op_ _ = raise error ("calc: operator = "^op_^" not defined");-----*)
5.554 +fun calc_equ "op <" (n1, n2) = n1 < n2
5.555 + | calc_equ "op <=" (n1, n2) = n1 <= n2
5.556 + | calc_equ op_ _ =
5.557 + raise error ("calc_equ: operator = "^op_^" not defined");
5.558 +fun sqrt (n:int) = if n < 0 then 0
5.559 + (*FIXME ~~~*) else (trunc o Math.sqrt o BasisLibrary.Real.fromInt) n;
5.560 +
5.561 +fun mk_thmid thmid op_ n1 n2 =
5.562 + thmid ^ (strip_thy n1) ^ "_" ^ (strip_thy n2);
5.563 +
5.564 +fun dest_binop_typ (Type("fun",[range,Type("fun",[arg2,arg1])])) =
5.565 + (arg1,arg2,range)
5.566 + | dest_binop_typ _ = raise error "dest_binop_typ: not binary";
5.567 +(* -----
5.568 +> val t = (term_of o the o (parse thy)) "#3^#4";
5.569 +> val hT = type_of (head_of t);
5.570 +> dest_binop_typ hT;
5.571 +val it = ("'a","nat","'a") : typ * typ * typ
5.572 + ----- *)
5.573 +
5.574 +
5.575 +(** transform binary numerals into
5.576 + Free("#numeral", Type ("polymorph",[])) **)
5.577 +
5.578 +(*5.1.00.: apply_trans in /Pure/Syntax/printer.ML
5.579 + to numeral_tr' in HOL/Tools/numeral_syntax.ML failed:
5.580 +fun pretty ... =
5.581 + val trans = apply_trans "print ast translation";
5.582 + and combT (tup as (c, a, args, p)) =
5.583 + in
5.584 + (case token_trans a args of (*try token translation function*)
5.585 + Some (s, len) => [Pretty.strlen_real s len]
5.586 + | None => (*try print translation functions*)
5.587 + astT (trans a (trf a) args, p) handle Match => prnt ([], tabs))
5.588 +
5.589 + Error: unbound type constructor: ast in path Ast.ast
5.590 +*)
5.591 +
5.592 +fun app_num_tr'1 (Const("0",T)) = Free("0",T)
5.593 + | app_num_tr'1 (Const("1",T)) = Free("1",T)
5.594 +(*| app_num_tr'1 (t as Const("uminus",_) $ Free(s,T)) =
5.595 + (case int_of_str s of Some i =>
5.596 + if i > 0 then Free("-"^s,T) else Free(s,T)
5.597 + | None => t)
5.598 + | app_num_tr'1 (t as Const(s,T)) = t
5.599 +*)| app_num_tr'1 (Const("Numeral.number_of",Type ("fun", [_, T])) $ t) =
5.600 + Free(NumeralSyntax.dest_bin_str t, T)
5.601 +(*| app_num_tr'1 (t as Free(s,T)) = t
5.602 + | app_num_tr'1 (t as Var(n,T)) = t
5.603 + | app_num_tr'1 (t as Bound i) = t*)
5.604 + | app_num_tr'1 (Abs(s,T,body)) = Abs(s,T, app_num_tr'1 body)
5.605 + | app_num_tr'1 (t1 $ t2) = (app_num_tr'1 t1) $ (app_num_tr'1 t2)
5.606 + | app_num_tr'1 t = t;
5.607 +(*.to be used immediately before evaluation of numerals.*)
5.608 +fun(*app_num_tr'2 (Const("0",T)) = Free("0",T)
5.609 + | app_num_tr'2 (Const("1",T)) = Free("1",T)
5.610 + |*)app_num_tr'2 (t as Const("uminus",_) $ Free(s,T)) =
5.611 + (case int_of_str s of Some i =>
5.612 + if i > 0 then Free("-"^s,T) else Free(s,T)
5.613 + | None => t)
5.614 +(*| app_num_tr'2 (t as Const(s,T)) = t
5.615 + | app_num_tr'2 (Const("Numeral.number_of",Type ("fun", [_, T])) $ t) =
5.616 + Free(NumeralSyntax.dest_bin_str t, T)
5.617 + | app_num_tr'2 (t as Free(s,T)) = t
5.618 + | app_num_tr'2 (t as Var(n,T)) = t
5.619 + | app_num_tr'2 (t as Bound i) = t
5.620 +*)| app_num_tr'2 (Abs(s,T,body)) = Abs(s,T, app_num_tr'2 body)
5.621 + | app_num_tr'2 (t1 $ t2) = (app_num_tr'2 t1) $ (app_num_tr'2 t2)
5.622 + | app_num_tr'2 t = t;
5.623 +
5.624 +fun num_str thm =
5.625 + let
5.626 + val {sign_ref = sign_ref, der = der, maxidx = maxidx,
5.627 + shyps = shyps, hyps = hyps, prop = prop} = rep_thm_G thm;
5.628 + val prop' = app_num_tr'1 prop;
5.629 + in assbl_thm sign_ref der maxidx shyps hyps prop' end;
5.630 +
5.631 +
5.632 +(** get types of Free and Abs for parse' **)
5.633 +(*11.1.00: not used, fix-typed +,*,-,^ instead *)
5.634 +
5.635 +val dummyT = Type ("dummy",[]);
5.636 +val dummyT = TVar (("DUMMY",0),[]);
5.637 +
5.638 +(* assumes only 1 type for numerals
5.639 + and different identifiers for Const, Free and Abs *)
5.640 +fun get_types t =
5.641 + let
5.642 + fun get ts (Const(s,T)) = (s,T)::ts
5.643 + | get ts (Free(s,T)) = if is_no s
5.644 + then ("#",T)::ts else (s,T)::ts
5.645 + | get ts (Var(n,T)) = ts
5.646 + | get ts (Bound i) = ts
5.647 + | get ts (Abs(s,T,body)) = get ((s,T)::ts) body
5.648 + | get ts (t1 $ t2) = (get ts t1) @ (get ts t2)
5.649 + in distinct (get [] t) end;
5.650 +(*
5.651 +val t = (term_of o the o (parse thy)) "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
5.652 +get_types t;
5.653 +*)
5.654 +
5.655 +(*11.1.00: not used, fix-typed +,*,-,^ instead *)
5.656 +fun set_types al (Const(s,T)) =
5.657 + (case assoc (al,s) of
5.658 + Some T' => Const(s,T')
5.659 + | None => (warning ("set_types: no type for "^s); Const(s,dummyT)))
5.660 + | set_types al (Free(s,T)) =
5.661 + if is_no s then
5.662 + (case assoc (al,"#") of
5.663 + Some T' => Free(s,T')
5.664 + | None => (warning ("set_types: no type for numerals"); Free(s,T)))
5.665 + else (case assoc (al,s) of
5.666 + Some T' => Free(s,T')
5.667 + | None => (warning ("set_types: no type for "^s); Free(s,T)))
5.668 + | set_types al (Var(n,T)) = Var(n,T)
5.669 + | set_types al (Bound i) = Bound i
5.670 + | set_types al (Abs(s,T,body)) =
5.671 + (case assoc (al,s) of
5.672 + Some T' => Abs(s,T', set_types al body)
5.673 + | None => (warning ("set_types: no type for "^s);
5.674 + Abs(s,T, set_types al body)))
5.675 + | set_types al (t1 $ t2) = (set_types al t1) $ (set_types al t2);
5.676 +(*
5.677 +val t = (term_of o the o (parse thy)) "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
5.678 +val al = get_types t;
5.679 +
5.680 +val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
5.681 +atomty thy t; (* 'a *)
5.682 +val t' = set_types al t;
5.683 +atomty thy t'; (*real*)
5.684 +cterm_of (sign_of thy) t';
5.685 +val it = "x = #0 + #-1 * #-4" : cterm
5.686 +
5.687 +val t = (term_of o the o (parse thy))
5.688 + "#5 * x + x ^^^ #2 = (#2 + x) ^^^ #2";
5.689 +atomty thy t;
5.690 +val t' = set_types al t;
5.691 +atomty thy t';
5.692 +cterm_of (sign_of thy) t';
5.693 +uncaught exception TYPE (*^^^ is new, NOT in al*)
5.694 +*)
5.695 +
5.696 +
5.697 +(** from Descript.ML **)
5.698 +
5.699 +(** decompose an isa-list to an ML-list
5.700 + i.e. [] belong to the meta-language, too **)
5.701 +
5.702 +fun is_list ((Const("List.list.Cons",_)) $ _ $ _) = true
5.703 + | is_list _ = false;
5.704 +(* val (Some ct) = parse thy "lll::real list";
5.705 +> val ty = (#t o rep_cterm) ct;
5.706 +> is_list ty;
5.707 +val it = false : bool
5.708 +> val (Some ct) = parse thy "[lll]";
5.709 +> val ty = (#t o rep_cterm) ct;
5.710 +> is_list ty;
5.711 +val it = true : bool *)
5.712 +
5.713 +
5.714 +
5.715 +fun mk_Free (s,T) = Free(s,T);
5.716 +fun mk_free T s = Free(s,T);
5.717 +
5.718 +
5.719 +(*instantiate let; necessary for ass_up*)
5.720 +fun inst_abs thy (Const sT) = Const sT
5.721 + | inst_abs thy (Free sT) = Free sT
5.722 + | inst_abs thy (Bound n) = Bound n
5.723 + | inst_abs thy (Var iT) = Var iT
5.724 + | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) =
5.725 + let val (v',b') = variant_abs (v,T2,b); (*term.ML*)
5.726 + in Const ("Let",T1) $ inst_abs thy e $ (Abs (v',T2,inst_abs thy b')) end
5.727 + | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
5.728 + | inst_abs thy t =
5.729 + (writeln("inst_abs: unchanged t= "
5.730 + ^(Sign.string_of_term (sign_of thy) t));t);
5.731 +(*val scr as (Script sc) = Script ((term_of o the o (parse thy))
5.732 + "Script Testeq (e_::bool) = \
5.733 + \While (contains_root e_) Do \
5.734 + \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False e_)); \
5.735 + \ e_ = Try (Repeat (Rewrite square_equation_left True e_)) \
5.736 + \ in Try (Repeat (Rewrite radd_0 False e_))) ");
5.737 +ML> atomt sc;
5.738 +*** Const ( Script.Testeq)
5.739 +*** . Free ( e_, )
5.740 +*** . Const ( Script.While)
5.741 +*** . . Const ( RatArith.contains'_root)
5.742 +*** . . . Free ( e_, )
5.743 +*** . . Const ( Let)
5.744 +*** . . . Const ( Script.Try)
5.745 +*** . . . . Const ( Script.Repeat)
5.746 +*** . . . . . Const ( Script.Rewrite)
5.747 +*** . . . . . . Free ( rroot_square_inv, )
5.748 +*** . . . . . . Const ( False)
5.749 +*** . . . . . . Free ( e_, )
5.750 +*** . . . Abs( e_,..
5.751 +*** . . . . Const ( Let)
5.752 +*** . . . . . Const ( Script.Try)
5.753 +*** . . . . . . Const ( Script.Repeat)
5.754 +*** . . . . . . . Const ( Script.Rewrite)
5.755 +*** . . . . . . . . Free ( square_equation_left, )
5.756 +*** . . . . . . . . Const ( True)
5.757 +*** . . . . . . . . Bound 0 <-- !!!
5.758 +*** . . . . . Abs( e_,..
5.759 +*** . . . . . . Const ( Script.Try)
5.760 +*** . . . . . . . Const ( Script.Repeat)
5.761 +*** . . . . . . . . Const ( Script.Rewrite)
5.762 +*** . . . . . . . . . Free ( radd_0, )
5.763 +*** . . . . . . . . . Const ( False)
5.764 +*** . . . . . . . . . Bound 0 <-- !!!
5.765 +val it = () : unit
5.766 +ML> atomt (inst_abs thy sc);
5.767 +*** Const ( Script.Testeq)
5.768 +*** . Free ( e_, )
5.769 +*** . Const ( Script.While)
5.770 +*** . . Const ( RatArith.contains'_root)
5.771 +*** . . . Free ( e_, )
5.772 +*** . . Const ( Let)
5.773 +*** . . . Const ( Script.Try)
5.774 +*** . . . . Const ( Script.Repeat)
5.775 +*** . . . . . Const ( Script.Rewrite)
5.776 +*** . . . . . . Free ( rroot_square_inv, )
5.777 +*** . . . . . . Const ( False)
5.778 +*** . . . . . . Free ( e_, )
5.779 +*** . . . Abs( e_,..
5.780 +*** . . . . Const ( Let)
5.781 +*** . . . . . Const ( Script.Try)
5.782 +*** . . . . . . Const ( Script.Repeat)
5.783 +*** . . . . . . . Const ( Script.Rewrite)
5.784 +*** . . . . . . . . Free ( square_equation_left, )
5.785 +*** . . . . . . . . Const ( True)
5.786 +*** . . . . . . . . Free ( e_, ) <-- !!!
5.787 +*** . . . . . Abs( e_,..
5.788 +*** . . . . . . Const ( Script.Try)
5.789 +*** . . . . . . . Const ( Script.Repeat)
5.790 +*** . . . . . . . . Const ( Script.Rewrite)
5.791 +*** . . . . . . . . . Free ( radd_0, )
5.792 +*** . . . . . . . . . Const ( False)
5.793 +*** . . . . . . . . . Free ( e_, ) <-- !!!
5.794 +val it = () : unit*)
5.795 +
5.796 +
5.797 +
5.798 +fun T_a2real (Type (s, [])) =
5.799 + if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else Type (s, [])
5.800 + | T_a2real (Type (s, Ts)) = Type (s, map T_a2real Ts)
5.801 + | T_a2real (TFree (s, srt)) =
5.802 + if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TFree (s, srt)
5.803 + | T_a2real (TVar (("DUMMY",_),srt)) = HOLogic.realT;
5.804 +
5.805 +(*FIXME .. fixes the type (+see Typefix.thy*)
5.806 +fun typ_a2real (Const( s, T)) = (Const( s, T_a2real T))
5.807 + | typ_a2real (Free( s, T)) = (Free( s, T_a2real T))
5.808 + | typ_a2real (Var( n, T)) = (Var( n, T_a2real T))
5.809 + | typ_a2real (Bound i) = (Bound i)
5.810 + | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t)
5.811 + | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2);
5.812 +(*
5.813 +----------------6.8.02---------------------------------------------------
5.814 + val str = "1";
5.815 + val t = read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
5.816 + atomty thy (term_of t);
5.817 +*** -------------
5.818 +*** Const ( 1, 'a)
5.819 + val t = (app_num_tr' o term_of) t;
5.820 + atomty thy t;
5.821 +*** -------------
5.822 +*** Const ( 1, 'a)
5.823 + val t = typ_a2real t;
5.824 + atomty thy t;
5.825 +*** -------------
5.826 +*** Const ( 1, real)
5.827 +
5.828 + val str = "2";
5.829 + val t = read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
5.830 + atomty thy (term_of t);
5.831 +*** -------------
5.832 +*** Const ( Numeral.number_of, bin => 'a)
5.833 +*** . Const ( Numeral.bin.Bit, [bin, bool] => bin)
5.834 +*** . . Const ( Numeral.bin.Bit, [bin, bool] => bin)
5.835 +*** . . . Const ( Numeral.bin.Pls, bin)
5.836 +*** . . . Const ( True, bool)
5.837 +*** . . Const ( False, bool)
5.838 + val t = (app_num_tr' o term_of) t;
5.839 + atomty thy t;
5.840 +*** -------------
5.841 +*** Free ( 2, 'a)
5.842 + val t = typ_a2real t;
5.843 + atomty thy t;
5.844 +*** -------------
5.845 +*** Free ( 2, real)
5.846 +----------------6.8.02---------------------------------------------------
5.847 +
5.848 +
5.849 +> val str = "R";
5.850 +> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
5.851 +val t = Free ("R","?DUMMY") : term
5.852 +> val t' = typ_a2real t;
5.853 +> cterm_of (sign_of thy) t';
5.854 +val it = "R::RealDef.real" : cterm
5.855 +
5.856 +> val str = "R=R";
5.857 +> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
5.858 +> atomty thy (typ_a2real t);
5.859 +*** -------------
5.860 +*** Const ( op =, [RealDef.real, RealDef.real] => bool)
5.861 +*** Free ( R, RealDef.real)
5.862 +*** Free ( R, RealDef.real)
5.863 +> val t' = typ_a2real t;
5.864 +> cterm_of (sign_of thy) t';
5.865 +val it = "(R::RealDef.real) = R" : cterm
5.866 +
5.867 +> val str = "fixed_values [R=R]";
5.868 +> val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
5.869 +> val t' = typ_a2real t;
5.870 +> cterm_of (sign_of thy) t';
5.871 +val it = "fixed_values [(R::RealDef.real) = R]" : cterm
5.872 +*)
5.873 +
5.874 +fun parseold thy str =
5.875 + (let
5.876 + val sgn = sign_of thy;
5.877 + val t = ((*typ_a2real o*) app_num_tr'1 o term_of)
5.878 + (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
5.879 + in Some (cterm_of sgn t) end)
5.880 + handle _ => None;
5.881 +
5.882 +fun parse thy str =
5.883 + (let
5.884 + val sgn = sign_of thy;
5.885 + val t = (typ_a2real o app_num_tr'1 o term_of)
5.886 + (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
5.887 + in Some (cterm_of sgn t) end) (*FIXXXXME 10.8.02: return term !!!*)
5.888 + handle _ => None;
5.889 +(* 10.8.02: for this reason we still have ^^^--------------------
5.890 + val thy = SqRoot.thy;
5.891 + val str = "(1::real) ^ (2::nat)";
5.892 + val sgn = sign_of thy;
5.893 + val ct = (read_cterm sgn (str,(TVar(("DUMMY",0),[])))) handle e =>print_exn e;
5.894 +(*1*)"(1::real) ^ 2";
5.895 + atomty thy (term_of ct);
5.896 +*** -------------
5.897 +*** Const ( Nat.power, [real, nat] => real)
5.898 +*** . Const ( 1, real)
5.899 +*** . Const ( Numeral.number_of, bin => nat)
5.900 +*** . . Const ( Numeral.bin.Bit, [bin, bool] => bin)
5.901 +*** . . . Const ( Numeral.bin.Bit, [bin, bool] => bin)
5.902 +*** . . . . Const ( Numeral.bin.Pls, bin)
5.903 +*** . . . . Const ( True, bool)
5.904 +*** . . . Const ( False, bool)
5.905 + val t = ((app_num_tr' o term_of)
5.906 + (read_cterm sgn (str,(TVar(("DUMMY",0),[])))))handle e => print_exn e;
5.907 + val ct = (cterm_of sgn t) handle e => print_exn e;
5.908 +(*2*)"(1::real) ^ (2::nat)";
5.909 + atomty thy (term_of ct);
5.910 +*** -------------
5.911 +*** Const ( Nat.power, [real, nat] => real)
5.912 +*** . Free ( 1, real)
5.913 +*** . Free ( 2, nat) (*1*) Const("2",_) (*2*) Free("2",_)
5.914 +
5.915 +
5.916 + val str = "(2::real) ^ (2::nat)";
5.917 + val t = (read_cterm sgn (str,(TVar(("DUMMY",0),[])))) handle e => print_exn e;
5.918 +val t = "(2::real) ^ 2" : cterm
5.919 + val t = ((app_num_tr' o term_of)
5.920 + (read_cterm sgn (str,(TVar(("DUMMY",0),[])))))handle e => print_exn e;
5.921 + val ct = (cterm_of sgn t) handle e => print_exn e;
5.922 +Variable "2" has two distinct types
5.923 +real
5.924 +nat
5.925 +uncaught exception TYPE
5.926 + raised at: sign.ML:672.26-673.56
5.927 + goals.ML:1100.61
5.928 +
5.929 +
5.930 + val str = "(3::real) ^ (2::nat)";
5.931 + val t = (read_cterm sgn (str,(TVar(("DUMMY",0),[])))) handle e => print_exn e;
5.932 +val t = "(3::real) ^ 2" : cterm
5.933 + val t = ((app_num_tr' o term_of)
5.934 + (read_cterm sgn (str,(TVar(("DUMMY",0),[])))))handle e => print_exn e;
5.935 + val ct = (cterm_of sgn t) handle e => print_exn e;
5.936 +val ct = "(3::real) ^ (2::nat)" : cterm
5.937 +
5.938 +
5.939 +Conclusion: The type inference allows different types
5.940 + for one and the same Numeral.number_of
5.941 + BUT the type inference doesn't allow
5.942 + Free ( 2, real) and Free ( 2, nat) within one term
5.943 +--------------- ~~~~ ~~~ *)
5.944 +(*
5.945 +> val (Some ct) = parse thy "(-#5)^^^#3";
5.946 +> atomty thy (term_of ct);
5.947 +*** -------------
5.948 +*** Const ( Nat.op ^, ['a, nat] => 'a)
5.949 +*** Const ( uminus, 'a => 'a)
5.950 +*** Free ( #5, 'a)
5.951 +*** Free ( #3, nat)
5.952 +> val (Some ct) = parse thy "R=R";
5.953 +> atomty thy (term_of ct);
5.954 +*** -------------
5.955 +*** Const ( op =, [real, real] => bool)
5.956 +*** Free ( R, real)
5.957 +*** Free ( R, real)
5.958 +
5.959 +THIS IS THE OUTPUT FOR VERSION (3) above at typ_a2real !!!!!
5.960 +*** -------------
5.961 +*** Const ( op =, [RealDef.real, RealDef.real] => bool)
5.962 +*** Free ( R, RealDef.real)
5.963 +*** Free ( R, RealDef.real) *)
5.964 +
5.965 +fun str2term str = (term_of o the o (parse (assoc_thy "Isac.thy"))) str;
5.966 +
5.967 +(*+ makes a substitution from the output of Pattern.match +*)
5.968 +fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);
5.969 +(*
5.970 + val t = (term_of o the o (parse thy)) "1/a";
5.971 + val pat = (term_of o the o (parse thy)) "?u/?v";
5.972 + val (_,sbst) = (Pattern.match (Sign.tsig_of(sign_of thy)) (pat,t))
5.973 + handle _ => ([],[]);
5.974 + ([],
5.975 + [(("v",0),Free ("a","RealDef.real")),(("u",0),Free ("1","RealDef.real"))])
5.976 + : (indexname * typ) list * (indexname * term) list
5.977 + val subst = map mk_subs sbst;
5.978 + [(Free ("v","RealDef.real"),Free ("a","RealDef.real")),
5.979 + (Free ("u","RealDef.real"),Free ("1","RealDef.real"))] : (term * term) list
5.980 +*)
5.981 +
5.982 +
5.983 +val atomthm = atomt o #prop o rep_thm;
5.984 +
5.985 +(*.instantiate #prop thm with bound variables (as Free).*)
5.986 +fun inst_bdv [] t = t : term
5.987 + | inst_bdv (instl: (term*term) list) t =
5.988 + let fun subst (v as Var((s,_),T)) =
5.989 + (case explode s of
5.990 + "b"::"d"::"v"::_ =>
5.991 + if_none (assoc(instl,Free(s,T))) (Free(s,T))
5.992 + | _ => v)
5.993 + | subst (Abs(a,T,body)) = Abs(a, T, subst body)
5.994 + | subst (f$t') = subst f $ subst t'
5.995 + | subst t = if_none (assoc(instl,t)) t
5.996 + in subst t end;
5.997 +(* num_str d1_isolate_add2;
5.998 + "~ ?a has_bdv_in ?bdv ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)"
5.999 + val subst = [(str2term "bdv", str2term "x")];
5.1000 + val t = (norm o #prop o rep_thm) (num_str d1_isolate_add2);
5.1001 + val t' = inst_bdv subst t;
5.1002 + term2str t';
5.1003 + "~ ?a has_bdv_in x ==> (?a + x = 0) = (x = -1 * ?a)"
5.1004 +*)
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/sml/kbtest/complex.sml Thu Apr 17 18:01:03 2003 +0200
6.3 @@ -0,0 +1,29 @@
6.4 +(* use"kbtest/complex.sml";
6.5 + *)
6.6 +
6.7 + val t = str2term "I__";
6.8 + atomt t;
6.9 + val t = str2term "1 + 2 * I__";
6.10 + atomt t;
6.11 + val t = str2term "1 + 2 * I__ + 3 + 4 * I__ * (5 + 6 * I__) / (7 + 8 * I__)";
6.12 + atomt t;
6.13 +(*andere konkrete Syntax ???*)
6.14 +
6.15 + val t = str2term "Float ((1,2),(0,0)) * I__";
6.16 + atomt t;
6.17 + term2str t;
6.18 + val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__";
6.19 + atomt t;
6.20 + term2str t;
6.21 +
6.22 + (*--- (1.1 + 2.2 I) * (3.3 + 4.4 I) = - 6.05 + 12 I ---*)
6.23 + val t = str2term "(Float ((11,-1),(0,0)) + Float ((22,-1),(0,0)) * I__) *\
6.24 + \(Float ((33,-1),(0,0)) + Float ((44,-1),(0,0)) * I__)";
6.25 + val Some (t',_) =
6.26 + rewrite_set_ thy false
6.27 + (append_rls "simpl_complex" make_polynomial
6.28 + [Thm ("square_I", num_str square_I)]) t;
6.29 + term2str t';
6.30 + "Float ((363, -2), 0, 0) + I__ * Float ((484, -2), 0, 0) +\
6.31 + \I__ * Float ((726, -2), 0, 0) + -1 * Float ((968, -2), 0, 0)"
6.32 + (*--- mit dem rls make_polynomial geht ja schon allerhand !!!---*)
6.33 \ No newline at end of file
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/sml/kbtest/diff.sml Thu Apr 17 18:01:03 2003 +0200
7.3 @@ -0,0 +1,506 @@
7.4 +(* use"kbtest/diff.sml";
7.5 + use"../tests/diff.sml";
7.6 + use"diff.sml";
7.7 + *)
7.8 +
7.9 +" _________________ problemtype _________________ ";
7.10 +" _________________ for correction of diff_const _________________ ";
7.11 +" _________________ for correction of diff_quot _________________ ";
7.12 +" _________________ differentiate by rewrite _________________ ";
7.13 +" ______________ differentiate: me (*+ msteps input*) ______________ ";
7.14 +" ________________ differentiate stdin: student active________________ ";
7.15 +" _________________ differentiate stdin: tutor active_________________ ";
7.16 +"---------------------1.5.02 me from script ---------------------";
7.17 +
7.18 +
7.19 +val thy = Diff.thy;
7.20 +
7.21 +" _________________ problemtype _________________ ";
7.22 +" _________________ problemtype _________________ ";
7.23 +" _________________ problemtype _________________ ";
7.24 +val pbt = {Given =["functionTerm f_", "differentiateFor v_"],
7.25 + Where =[],
7.26 + Find =["derivative f_'_"],
7.27 + With =[],
7.28 + Relate=[]}:string ppc;
7.29 +val chkpbt = ((map (the o (parse Diff.thy))) o ppc2list) pbt;
7.30 +
7.31 +val org = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
7.32 + "differentiateFor x","derivative f_'_"];
7.33 +val chkorg = map (the o (parse Diff.thy)) org;
7.34 +
7.35 +get_pbt ["derivative_of","function"];
7.36 +get_met ("Diff.thy","differentiate_on_R");
7.37 +
7.38 +(*erls should not be in ruleset'! Here only for tests*)
7.39 +ruleset' :=
7.40 +overwritel
7.41 + (!ruleset',
7.42 + [("erls",
7.43 + Rls {id = "erls",preconds = [], rew_ord = ("termlessI",termlessI),
7.44 + erls = e_rls, srls = Erls, calc = [], asm_thm = [],
7.45 + rules = [Thm ("refl",num_str refl),
7.46 + Thm ("le_refl",num_str le_refl),
7.47 + Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
7.48 + Thm ("not_true",num_str not_true),
7.49 + Thm ("not_false",num_str not_false),
7.50 + Thm ("and_true",and_true),
7.51 + Thm ("and_false",and_false),
7.52 + Thm ("or_true",or_true),
7.53 + Thm ("or_false",or_false),
7.54 + Thm ("and_commute",num_str and_commute),
7.55 + Thm ("or_commute",num_str or_commute),
7.56 +
7.57 + Calc ("Atools.is'_const",eval_const "#is_const_"),
7.58 + Calc ("Tools.matches",eval_matches ""),
7.59 +
7.60 + Calc ("op +",eval_binop "#add_"),
7.61 + Calc ("op *",eval_binop "#mult_"),
7.62 + Calc ("Atools.pow" ,eval_binop "#power_"),
7.63 +
7.64 + Calc ("op <",eval_equ "#less_"),
7.65 + Calc ("op <=",eval_equ "#less_equal_"),
7.66 +
7.67 + Calc ("Atools.ident",eval_ident "#ident_")],
7.68 + scr = Script ((term_of o the o (parse thy))
7.69 + "empty_script")
7.70 + }:rls
7.71 + )]);
7.72 +
7.73 +" _________________ for correction of diff_const _________________ ";
7.74 +" _________________ for correction of diff_const _________________ ";
7.75 +" _________________ for correction of diff_const _________________ ";
7.76 +val thy' = "Diff.thy";
7.77 +val ct = "Not (x =!= a)";
7.78 +rewrite_set thy' false "erls" ct;
7.79 +val ct = "2 is_const";
7.80 +rewrite_set thy' false "erls" ct;
7.81 +
7.82 +val thm = ("diff_const","");
7.83 +val ct = "d_d x x";
7.84 +val None =
7.85 + (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
7.86 +val ct = "d_d x 2";
7.87 +val Some (ctt,_) =
7.88 + (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
7.89 +
7.90 +val thm = ("diff_var","");
7.91 +val ct = "d_d x x";
7.92 +val Some (ctt,_) =
7.93 + (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
7.94 +val ct = "d_d x a";
7.95 +val None =
7.96 + (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
7.97 +val ct = "d_d x (x+x)";
7.98 +val None =
7.99 +(rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
7.100 +
7.101 +
7.102 +" _________________ for correction of diff_quot _________________ ";
7.103 +" _________________ for correction of diff_quot _________________ ";
7.104 +" _________________ for correction of diff_quot _________________ ";
7.105 +val thy' = "Diff.thy";
7.106 +val ct = "Not (x = 0)";
7.107 +rewrite_set thy' false "erls" ct;
7.108 +
7.109 +val ct = "d_d x ((x+1) / (x - 1))";
7.110 +val thm = ("diff_quot","");
7.111 +val Some (ctt,_) =
7.112 + (rewrite_inst thy' "tless_true" "erls" true [("bdv","x")] thm ct);
7.113 +
7.114 +
7.115 +
7.116 +
7.117 +
7.118 +
7.119 +
7.120 +" _________________ differentiate by rewrite _________________ ";
7.121 +" _________________ differentiate by rewrite _________________ ";
7.122 +" _________________ differentiate by rewrite _________________ ";
7.123 +val thy' = "Diff.thy";
7.124 +val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
7.125 +"--- 1 ---";
7.126 +val thm = ("diff_sum","");
7.127 +val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
7.128 + [("bdv","x::real")] thm ct);
7.129 +"--- 2 ---";
7.130 +val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
7.131 + [("bdv","x::real")] thm ct);
7.132 +"--- 3 ---";
7.133 +val thm = ("diff_prod_const","");
7.134 +val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
7.135 + [("bdv","x::real")] thm ct);
7.136 +"--- 4 ---";
7.137 +val thm = ("diff_pow","");
7.138 +val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
7.139 + [("bdv","x::real")] thm ct);
7.140 +"--- 5 ---";
7.141 +val thm = ("diff_const","");
7.142 +val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
7.143 + [("bdv","x::real")] thm ct);
7.144 +"--- 6 ---";
7.145 +val thm = ("diff_var","");
7.146 +val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
7.147 + [("bdv","x::real")] thm ct);
7.148 +"2 * x ^^^ (2 - 1) + 3 * 1 + 0";
7.149 +"--- 7 ---";
7.150 +val rls = ("Test_simplify");
7.151 +val (ct,_) = the (rewrite_set thy' false rls ct);
7.152 +if ct="3 + 2 * x" then () else raise error "new behaviour in test-example";
7.153 +
7.154 +val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0";
7.155 +val (ct,_) = the (rewrite_set thy' true rls ct);
7.156 +
7.157 +
7.158 +(*---
7.159 +val t = str2term "x ^^^ (2 - 1)";
7.160 +val Some (t',_) = rewrite_set_ thy false Test_simplify t;
7.161 +term2str t';
7.162 +
7.163 +val t = str2term "-1 * 1";
7.164 +val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
7.165 +*)
7.166 +
7.167 +
7.168 +" ______________ differentiate: me (*+ msteps input*) ______________ ";
7.169 +" ______________ differentiate: me (*+ msteps input*) ______________ ";
7.170 +" ______________ differentiate: me (*+ msteps input*) ______________ ";
7.171 +val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
7.172 + "differentiateFor x","derivative f_'_"];
7.173 +val (dI',pI',mI') =
7.174 + ("Diff.thy",["derivative_of","function"],
7.175 + ("Diff.thy","differentiate_on_R"));
7.176 +val p = e_pos'; val c = [];
7.177 +"--- s1 ---";
7.178 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
7.179 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
7.180 +"--- s2 ---";
7.181 +(*val nxt = ("Add_Given",
7.182 +Add_Given "functionTerm (d_d x (x ^^^ #2 + #3 * x + #4))");*)
7.183 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.184 +"--- s3 ---";
7.185 +(*val nxt = ("Add_Given",Add_Given "differentiateFor x");*)
7.186 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.187 +"--- s4 ---";
7.188 +(*val nxt = ("Add_Find",Add_Find "derivative f_'_");*)
7.189 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.190 +"--- s5 ---";
7.191 +(*val nxt = ("Specify_Domain",Specify_Domain dI');*)
7.192 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.193 +"--- s6 ---";
7.194 +(*val nxt = ("Specify_Problem",Specify_Problem pI');*)
7.195 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.196 +"--- s7 ---";
7.197 +(*val nxt = ("Specify_Method",Specify_Method mI');*)
7.198 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.199 +"--- s8 ---";
7.200 +(*val nxt = ("Apply_Method",Apply_Method mI');*)
7.201 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.202 +"--- 1 ---";
7.203 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_sum","")));*)
7.204 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.205 +"--- 2 ---";
7.206 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_sum","")));*)
7.207 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.208 +"--- 3 ---";
7.209 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_prod_const","")));*)
7.210 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.211 +"--- 4 ---";
7.212 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_pow","")));*)
7.213 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.214 +"--- 5 ---";
7.215 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_const","")));*)
7.216 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.217 +"--- 6 ---";
7.218 +(*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_var","")));*)
7.219 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.220 +"2 * x ^^^ (2 - 1) + 3 * 1 + 0";
7.221 +"--- 7 ---";
7.222 +(*------------------------------11.3.03--------------------
7.223 + trace_rewrite:=true;
7.224 + val (_,_,f,_,_,_) = me nxt p c pt;
7.225 + val Form' (FormKF (_,_,_,_,res)) = f;
7.226 + trace_rewrite:=false;
7.227 +
7.228 + val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0";
7.229 + val Some (ct',_) = rewrite_set "Isac.thy" false "make_polynomial" ct;
7.230 +
7.231 + trace_rewrite:=true;
7.232 + val t = str2term ct;
7.233 + term2str t;
7.234 + val Some (t',_) = rewrite_set_ Isac.thy false make_polynomial t;
7.235 + term2str t';
7.236 + trace_rewrite:=false;
7.237 +
7.238 + val Some (t'',_) = rewrite_set_ Isac.thy false make_polynomial t';
7.239 + term2str t'';
7.240 +
7.241 + val thm = num_str realpow_eq_oneI;
7.242 + case string_of_thm thm of
7.243 +
7.244 +
7.245 + val Rewrite_Set' ("Diff.thy",false,"make_polynomial",ff,(ff',[])) = m;
7.246 + term2str ff; term2str ff';
7.247 +
7.248 +
7.249 +
7.250 +--------------------------------11.3.03--------------------*)
7.251 +
7.252 +(*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial");*)
7.253 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.254 +"--- 8 ---";
7.255 +(*val nxt =
7.256 +("Check_Postcond",Check_Postcond ("Diff.thy","differentiate_on_R"));*)
7.257 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.258 +"--- 9 ---";
7.259 +(*val nxt = ("End_Proof'",End_Proof');*)
7.260 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.261 +if f = EmptyMout then () else raise error "new behaviour in + msteps input";
7.262 +
7.263 +
7.264 +
7.265 +
7.266 +(*---------------- 1.5.02 -----------------------------------------
7.267 +
7.268 +" _________________ script-eval corrected _________________ ";
7.269 +" _________________ script-eval corrected _________________ ";
7.270 +" _________________ script-eval corrected _________________ ";
7.271 +val scr = Script (((inst_abs (assoc_thy "Test.thy")) o
7.272 + term_of o the o (parse Diff.thy))
7.273 + "Script Differentiate (f_::real) (v_::real) = \
7.274 + \(let f_ = Try (Repeat (Rewrite frac_conv False f_)); \
7.275 + \ f_ = Try (Repeat (Rewrite root_conv False f_)); \
7.276 + \ f_ = Repeat \
7.277 + \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False f_)) Or \
7.278 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False f_)) Or \
7.279 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False f_)) Or \
7.280 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot False f_)) Or \
7.281 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False f_)) Or \
7.282 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False f_)) Or \
7.283 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False f_)) Or \
7.284 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False f_)) Or \
7.285 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False f_)) Or \
7.286 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False f_)) Or \
7.287 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False f_)) Or \
7.288 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False f_)) Or \
7.289 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False f_)) Or \
7.290 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False f_)) Or \
7.291 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False f_)) Or \
7.292 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False f_)) Or \
7.293 + \ (Repeat (Rewrite_Set Test_simplify False f_))); \
7.294 + \ f_ = Try (Repeat (Rewrite sym_frac_conv False f_)) \
7.295 + \ in Try (Repeat (Rewrite sym_root_conv False f_)))");
7.296 +val d = e_rls;
7.297 +val (dI',pI',mI') =
7.298 + ("Diff.thy",e_pblID,
7.299 + ("Diff.thy","differentiate_on_R"));
7.300 +val p = e_pos'; val c = [];
7.301 +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
7.302 +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
7.303 +val nxt = ("Specify_Domain",Specify_Domain dI');
7.304 +val (p,_,_,_,_,pt) = me nxt p c pt;
7.305 +val nxt = ("Specify_Method",Specify_Method mI');
7.306 +val (p,_,_,_,_,pt) = me nxt p c pt;
7.307 +val p = ([1],Frm):pos';
7.308 +
7.309 +
7.310 +val parseee = (term_of o the o (parse Diff.thy));
7.311 +val ct = "d_d x (x ^^^ #2 + #3 * x + #4)";
7.312 +val envvv = [(parseee"f_",parseee ct),(parseee"v_",parseee"x")];
7.313 +val ets0=[([],(Mstep'(Script.thy,"BS","",""),envvv,envvv,empty,empty,Safe)),
7.314 + ([],(User', [], [], empty, empty,Sundef))]:ets;
7.315 +val l0 = [];
7.316 +" --------------- 1. ---------------------------------------------";
7.317 +val (pt,_) = cappend_atomic pt[1]e_loc ct (Rewrite("test","")) ct Complete;
7.318 +val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum","")));
7.319 +
7.320 +val NextStep(l1,m') = nxt_tac "Diff.thy" (pt,p) scr ets0 l0;
7.321 +(*("diff_sum","")*)
7.322 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
7.323 + locate_gen "Diff.thy" m' (pt,p) (scr,d) ets0 l0;
7.324 +val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
7.325 +" --------------- 2. ---------------------------------------------";
7.326 +val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum","")));
7.327 +val NextStep(l2,m') = nxt_tac "Diff.thy" (pt,p) scr ets1 l1;
7.328 +(*("diff_sum","")*)
7.329 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
7.330 + locate_gen "Diff.thy" m' (pt,p) (scr,d) ets1 l1;
7.331 +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
7.332 +" --------------- 3. ---------------------------------------------";
7.333 +val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_prod_const","")));
7.334 +val NextStep(l3,m') = nxt_tac "Diff.thy" (pt,p) scr ets2 l2;
7.335 +(*("diff_prod_const","")*)
7.336 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] =
7.337 + locate_gen "Diff.thy" m' (pt,p) (scr,d) ets2 l2;
7.338 +val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
7.339 +" --------------- 4. ---------------------------------------------";
7.340 +val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_pow","")));
7.341 +val NextStep(l4,m') = nxt_tac "Diff.thy" (pt,p) scr ets3 l3;
7.342 +(*("diff_pow","")*)
7.343 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
7.344 + locate_gen "Diff.thy" m' (pt,p) (scr,d) ets3 l3;
7.345 +val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
7.346 +" --------------- 5. ---------------------------------------------";
7.347 +val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_const","")));
7.348 +val NextStep(l5,m') = nxt_tac "Diff.thy" (pt,p) scr ets4 l4;
7.349 +(*("diff_const","")*)
7.350 +val Steps[ (Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets5)] =
7.351 + locate_gen "Diff.thy" m' (pt,p) (scr,d) ets4 l4;
7.352 +val ets5 = (drop_last ets4) @ ets5; val pt = update_ets pt [] [(1,ets5)];
7.353 +" --------------- 6. ---------------------------------------------";
7.354 +val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_var","")));
7.355 +val NextStep(l6,m') = nxt_tac "Diff.thy" (pt,p) scr ets5 l5;
7.356 +(*("diff_var","")ok; here was("diff_const","")because of wrong rule in *.thy*)
7.357 +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets6)] =
7.358 + locate_gen "Diff.thy" m' (pt,p) (scr,d) ets5 l5;
7.359 +val ets6 = (drop_last ets5) @ ets6; val pt = update_ets pt [] [(1,ets6)];
7.360 +" --------------- 7. ---------------------------------------------";
7.361 +val Appl m'=applicable_in p pt (Rewrite_Set "Test_simplify");
7.362 +
7.363 +
7.364 + ---------------- 1.5.02 -----------------------------------------*)
7.365 +
7.366 +
7.367 +
7.368 +
7.369 +" ________________ differentiate stdin: student active________________ ";
7.370 +" ________________ differentiate stdin: student active________________ ";
7.371 +" ________________ differentiate stdin: student active________________ ";
7.372 +proofs:= []; dials:=([],[],[]);
7.373 +StdinSML 0 0 0 0 New_User;
7.374 +set_dstate 1 test_hide 4 1;(*SelRule,St..PutRuleRes,TskipS..*)
7.375 +StdinSML 1 0 0 0 New_Proof;
7.376 +val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
7.377 + "differentiateFor x","derivative f_'_"];
7.378 +val (dI',pI',mI') =
7.379 + ("Diff.thy",["derivative_of","function"],
7.380 + ("Diff.thy","differentiate_on_R"));
7.381 +"--- s1 ---";
7.382 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
7.383 +"--- s2 ---";
7.384 +StdinSML 1 1 ~1 ~1 (RuleFK (Add_Given "functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))"));
7.385 +"--- s3 ---";
7.386 +StdinSML 1 1 ~2 ~2 (RuleFK (Add_Given "differentiateFor x"));
7.387 +"--- s4 ---";
7.388 +StdinSML 1 1 ~3 ~3 (RuleFK (Add_Find "derivative f_'_"));
7.389 +"--- s5 ---";
7.390 +StdinSML 1 1 ~4 ~4 (RuleFK (Specify_Domain dI'));
7.391 +"--- s6 ---";
7.392 +StdinSML 1 1 ~5 ~5 (RuleFK (Specify_Problem pI'));
7.393 +"--- s7 ---";
7.394 +StdinSML 1 1 ~6 ~6 (RuleFK (Specify_Method mI'));
7.395 +"--- s8 ---";
7.396 +StdinSML 1 1 ~7 ~7 (RuleFK (Apply_Method mI'));
7.397 +"--- 1 ---";
7.398 +StdinSML 1 1 ~8 ~8 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_sum",""))));
7.399 +"--- 2 ---";
7.400 +StdinSML 1 1 ~9 ~9 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_sum",""))));
7.401 +"--- 3 ---";
7.402 +StdinSML 1 1 ~10 ~10 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_prod_const",""))));
7.403 +"--- 4 ---";
7.404 +StdinSML 1 1 ~11 ~11 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_pow",""))));
7.405 +"--- 5 ---";
7.406 +StdinSML 1 1 ~12 ~12 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_const",""))));
7.407 +"--- 6 ---";
7.408 +StdinSML 1 1 ~13 ~13 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_var",""))));
7.409 +"--- 7 ---";
7.410 +StdinSML 1 1 ~14 ~14 (RuleFK (Rewrite_Set "Test_simplify"));
7.411 +"--- 8 ---";
7.412 +
7.413 +
7.414 +
7.415 +" _________________ differentiate stdin: tutor active_________________ ";
7.416 +" _________________ differentiate stdin: tutor active_________________ ";
7.417 +" _________________ differentiate stdin: tutor active_________________ ";
7.418 +proofs:= []; dials:=([],[],[]);
7.419 +StdinSML 0 0 0 0 New_User;
7.420 +set_dstate 1 test_hide 0 2;(*PutRule,TskipS..PutRuleRes,Tt..*)
7.421 +StdinSML 1 0 0 0 New_Proof;
7.422 +val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
7.423 + "differentiateFor x","derivative f_'_"];
7.424 +val (dI',pI',mI') =
7.425 + ("Diff.thy",["derivative_of","function"],
7.426 + ("Diff.thy","differentiate_on_R"));
7.427 +"--- s1 ---";
7.428 +val (_,1,1,_,[],[_,_,PpcKF (_,_,_,_,ppc),req],_) =
7.429 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
7.430 +"--- s2 ---";
7.431 +val (_,1,1,_,[],[RuleKF r,PpcKF (_,_,_,_,ppc),req],_) =
7.432 +StdinSML 1 1 ~1 ~1 (Command Accept);
7.433 +"--- s3 ---";
7.434 +val (_,1,1,_,[],[RuleKF r,PpcKF (_,_,_,_,ppc),req],_) =
7.435 +StdinSML 1 1 ~2 ~2 (Command Accept);
7.436 +"--- s4 ---";
7.437 +val (_,1,1,_,[],[RuleKF r,PpcKF (_,_,_,_,ppc),req],_) =
7.438 +StdinSML 1 1 ~3 ~3 (Command Accept);
7.439 +"--- s5 ---";
7.440 +val (_,1,1,_,[],[RuleKF r,PpcKF (_,_,_,_,ppc),req],_) =
7.441 +StdinSML 1 1 ~4 ~4 (Command Accept);
7.442 +"--- s6 ---";
7.443 +val (_,1,1,_,[],[RuleKF r,PpcKF (_,_,_,_,ppc),req],_) =
7.444 +StdinSML 1 1 ~5 ~5 (Command Accept);
7.445 +"--- s7 ---";
7.446 +val (_,1,1,_,[],[RuleKF r,PpcKF (_,_,_,_,ppc),req],_) =
7.447 +StdinSML 1 1 ~6 ~6 (Command Accept);
7.448 +"--- s8 ---";
7.449 +val (_,1,1,_,[],[RuleKF r,FormKF (_,_,_,_,f),req],_) =
7.450 +StdinSML 1 1 ~7 ~7 (Command Accept);
7.451 +"--- 1 ---";
7.452 +val (_,1,1,_,[],[RuleKF r,FormKF (_,_,_,_,f),req],_) =
7.453 +StdinSML 1 1 ~8 ~8 (Command Accept);
7.454 +"--- 2 ---";
7.455 +val (_,1,1,_,[],[RuleKF r,FormKF (_,_,_,_,f),req],_) =
7.456 +StdinSML 1 1 ~9 ~9 (Command Accept);
7.457 +"--- 3 ---";
7.458 +val (_,1,1,_,[],[RuleKF r,FormKF (_,_,_,_,f),req],_) =
7.459 +StdinSML 1 1 ~10 ~10 (Command Accept);
7.460 +"--- 4 ---";
7.461 +val (_,1,1,_,[],[RuleKF r,FormKF (_,_,_,_,f),req],_) =
7.462 +StdinSML 1 1 ~11 ~11 (Command Accept);
7.463 +"--- 5 ---";
7.464 +val (_,1,1,_,[],[RuleKF r,FormKF (_,_,_,_,f),req],_) =
7.465 +StdinSML 1 1 ~12 ~12 (Command Accept);
7.466 +"--- 6 ---";
7.467 +val (_,1,1,_,[],[RuleKF r,FormKF (_,_,_,_,f),req],_) =
7.468 +StdinSML 1 1 ~13 ~13 (Command Accept);
7.469 +"--- 7 ---";
7.470 +val (_,1,1,_,[],[RuleKF r,FormKF (_,_,_,_,f),req],_) =
7.471 +StdinSML 1 1 ~14 ~14 (Command Accept);
7.472 +"--- 8 ---";
7.473 +val (_,1,1,~15,[],
7.474 + [RuleKF (_,Check_Postcond _),FormKF (_,_,_,_,"3 + 2 * x"),
7.475 + Request "Accept ?"],_)
7.476 + = StdinSML 1 1 ~15 ~15 (Command Accept);
7.477 +
7.478 +
7.479 +
7.480 +"---------------------1.5.02 me from script ---------------------";
7.481 +"---------------------1.5.02 me from script ---------------------";
7.482 +"---------------------1.5.02 me from script ---------------------";
7.483 +val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
7.484 + "differentiateFor x","derivative f_'_"];
7.485 +val (dI',pI',mI') =
7.486 + ("Diff.thy",["derivative_of","function"],
7.487 + ("Diff.thy","diff_simpl"));
7.488 +val p = e_pos'; val c = [];
7.489 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
7.490 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
7.491 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.492 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.493 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.494 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.495 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.496 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.497 +(*nxt = ("Apply_Method",Apply_Method ("Diff.thy","differentiate_on_R*)
7.498 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.499 +
7.500 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.501 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.502 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.503 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.504 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.505 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.506 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.507 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.508 +if nxt = ("End_Proof'",End_Proof') then ()
7.509 +else raise error "new behaviour in tests/differentiate, 1.5.02 me from script";
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/sml/kbtest/diffapp.sml Thu Apr 17 18:01:03 2003 +0200
8.3 @@ -0,0 +1,482 @@
8.4 +(* use"tests/test-maximum.sml";
8.5 + use"test-maximum.sml";
8.6 + WW.N.1.3.00
8.7 + + see "test-circle.sml" for pre-, postconditions
8.8 + + see "test-coil-kernel.sml" for variants etc.
8.9 +*)
8.10 +
8.11 +"Contents----------------------------------------------";
8.12 +" Specify_Problem (match_itms_oris) ";
8.13 +" test specify, fmz <> [] ";
8.14 +" test specify, fmz = [] ";
8.15 +" problemtypes + formalizations ";
8.16 +"------------------------------------------------------";
8.17 +
8.18 +
8.19 +
8.20 +" #################################################### ";
8.21 +" Specify_Problem (match_itms_oris) ";
8.22 +" #################################################### ";
8.23 +val fmz =
8.24 + ["fixedValues [r=Arbfix]","maximum A",
8.25 + "valuesFor [a=Undef,b=Undef]",
8.26 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
8.27 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
8.28 + "relations [A=a*b, a=2*r*sin alpha, b=2*r*cos alpha]",
8.29 +
8.30 + "boundVariable a","boundVariable b","boundVariable alpha",
8.31 + "interval {x::real. 0 <= x & x <= 2*r}",
8.32 + "interval {x::real. 0 <= x & x <= 2*r}",
8.33 + "interval {x::real. 0 <= x & x <= pi}",
8.34 + "errorBound (eps=(0::real))"];
8.35 +val (dI',pI',mI') =
8.36 + ("DiffApp.thy",["maximum_of","function"],
8.37 + ("DiffApp.thy","max_by_calculus"));
8.38 +val c = []:cid;
8.39 +
8.40 +val nxt = Init_Proof' (fmz,(dI',pI',mI'));
8.41 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] EmptyPtree;
8.42 +(*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : mstep*)
8.43 +
8.44 +val nxt = mstep2mstep' pt p nxt;
8.45 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.46 +(**)
8.47 +
8.48 +val nxt = mstep2mstep' pt p (Add_Find "valuesFor [(a::real) = Undef]");
8.49 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.50 +(**)
8.51 +
8.52 +if ppc<>(Problem [],
8.53 + {Find=[Incompl "maximum",Incompl "valuesFor [a = Undef]"],
8.54 + Given=[Correct "fixedValues [r = Arbfix]"],
8.55 + Relate=[Incompl "relations []"], Where=[],With=[]})
8.56 +then raise error "test-maximum.sml: model stepwise - different behaviour"
8.57 +else (); (*different with show_types !!!*)
8.58 +
8.59 +(*-----appl_add should not create Error', but accept as Sup,Syn
8.60 +val nxt = mstep2mstep' pt p (Add_Given "boundVariable a");
8.61 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.62 +(**)
8.63 +val nxt = mstep2mstep' pt p (Add_Given "boundVariable a+");
8.64 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.65 +(**)---*)
8.66 +
8.67 +val m = Specify_Problem ["maximum_of","function"];
8.68 +val nxt = mstep2mstep' pt p m;
8.69 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.70 +(**)
8.71 +
8.72 +if ppc<>(Problem ["maximum_of","function"],
8.73 + {Find=[Incompl "maximum",Incompl "valuesFor [a = Undef]"],
8.74 + Given=[Correct "fixedValues [r = Arbfix]"],
8.75 + Relate=[Incompl "relations []"], Where=[],With=[]})
8.76 +then raise error "test-maximum.sml: Specify_Problem different behaviour"
8.77 +else (); (*different with show_types !!!*)
8.78 +
8.79 +val nxt = mstep2mstep' pt p(Specify_Method ("DiffApp.thy","max_by_calculus"));
8.80 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.81 +(**)
8.82 +
8.83 +if ppc<>(Method ("DiffApp.thy","max_by_calculus"),
8.84 + {Find=[Incompl "maximum",Incompl "valuesFor [a = Undef]"],
8.85 + Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_",
8.86 + Missing "interval itv_",Missing "errorBound err_"],
8.87 + Relate=[Incompl "relations []"],Where=[],With=[]})
8.88 +then raise error "test-maximum.sml: Specify_Method different behaviour"
8.89 +else (); (*different with show_types !!!*)
8.90 +
8.91 +
8.92 +
8.93 +
8.94 +
8.95 +
8.96 +
8.97 +
8.98 +" #################################################### ";
8.99 +" test specify, fmz <> [] ";
8.100 +" #################################################### ";
8.101 +val fmz =
8.102 + ["fixedValues [r=Arbfix]","maximum A",
8.103 + "valuesFor [a=Undef,b=Undef]",
8.104 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
8.105 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
8.106 + "relations [A=a*b, a=2*r*sin alpha, b=2*r*cos alpha]",
8.107 +
8.108 + "boundVariable a","boundVariable b","boundVariable alpha",
8.109 + "interval {x::real. 0 <= x & x <= 2*r}",
8.110 + "interval {x::real. 0 <= x & x <= 2*r}",
8.111 + "interval {x::real. 0 <= x & x <= pi}",
8.112 + "errorBound (eps=(0::real))"];
8.113 +val (dI',pI',mI') =
8.114 + ("DiffApp.thy",["maximum_of","function"],
8.115 + ("DiffApp.thy","max_by_calculus"));
8.116 +val c = []:cid;
8.117 +val nxt = Init_Proof' (fmz,(dI',pI',mI'));
8.118 +
8.119 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] EmptyPtree;
8.120 +(*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : mstep*)
8.121 +
8.122 +val nxt = mstep2mstep' pt p nxt;
8.123 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.124 +(*val nxt = Add_Find "maximum (A::bool)" : mstep*)
8.125 +
8.126 +val nxt = mstep2mstep' pt p nxt;
8.127 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.128 +(*val nxt = Add_Find "valuesFor [(a::real) = Undef]" : mstep*)
8.129 +
8.130 +val nxt = mstep2mstep' pt p nxt;
8.131 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.132 +(*val nxt = Add_Find "valuesFor [(b::real) = Undef]" : mstep*)
8.133 +
8.134 +val nxt = mstep2mstep' pt p nxt;
8.135 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.136 +(*val nxt = Add_Relation "relations [A = a * b]" *)
8.137 +
8.138 +val nxt = mstep2mstep' pt p nxt;
8.139 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.140 +(*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
8.141 +
8.142 +if nxt<>(Add_Relation
8.143 + "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
8.144 +then raise error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)
8.145 +
8.146 +val nxt = mstep2mstep' pt p nxt;
8.147 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.148 +(*val nxt = Specify_Domain "DiffApp.thy" : mstep*)
8.149 +
8.150 +val nxt = mstep2mstep' pt p nxt;
8.151 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.152 +(*val nxt = Specify_Problem ["maximum_of","function"]*)
8.153 +
8.154 +val nxt = mstep2mstep' pt p nxt;
8.155 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.156 +(*val nxt = Specify_Method ("DiffApp.thy","max_by_calculus")*)
8.157 +
8.158 +val nxt = mstep2mstep' pt p nxt;
8.159 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.160 +(*val nxt = Add_Given "boundVariable a" : mstep*)
8.161 +
8.162 +val nxt = mstep2mstep' pt p nxt;
8.163 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.164 +(*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)
8.165 +
8.166 +val nxt = mstep2mstep' pt p nxt;
8.167 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.168 +(*val nxt = Add_Given "errorBound (eps = #0)" : mstep*)
8.169 +
8.170 +val nxt = mstep2mstep' pt p nxt;
8.171 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.172 +(*val nxt = Apply_Method ("DiffApp.thy","max_by_calculus") *)
8.173 +if nxt<>(Apply_Method ("DiffApp.thy","max_by_calculus"))
8.174 +then raise error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();
8.175 +
8.176 +
8.177 +" #################################################### ";
8.178 +" test specify, fmz = [] ";
8.179 +" #################################################### ";
8.180 +val fmz = [];
8.181 +val (dI',pI',mI') = empty_spec;
8.182 +val c = []:cid;
8.183 +
8.184 +val nxt = Init_Proof' (fmz,(dI',pI',mI'));
8.185 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' []
8.186 + EmptyPtree;
8.187 +(*val nxt = Specify_Domain "e_domID" : mstep*)
8.188 +
8.189 +val nxt = Specify_Domain "DiffApp.thy";
8.190 +val nxt = mstep2mstep' pt p nxt;
8.191 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.192 +(*val nxt = Specify_Problem ["e_pblID"] : mstep*)
8.193 +
8.194 +val nxt = Specify_Problem ["maximum_of","function"];
8.195 +val nxt = mstep2mstep' pt p nxt;
8.196 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.197 +(*val nxt = Add_Given "fixedValues" : mstep*)
8.198 +
8.199 +val nxt = Add_Given "fixedValues [r=Arbfix]";
8.200 +val nxt = mstep2mstep' pt p nxt;
8.201 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.202 +(*val nxt = Add_Find "maximum" : mstep*)
8.203 +
8.204 +val nxt = Add_Find "maximum A";
8.205 +val nxt = mstep2mstep' pt p nxt;
8.206 +
8.207 +
8.208 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.209 +(*val nxt = Add_Find "valuesFor" : mstep*)
8.210 +
8.211 +val nxt = Add_Find "valuesFor [a=Arbfix]";
8.212 +val nxt = mstep2mstep' pt p nxt;
8.213 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.214 +(*val nxt = Add_Relation "relations" ---
8.215 + --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)
8.216 +
8.217 +(*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
8.218 +if nxt<>(Add_Relation "relations []")
8.219 +then raise error "test specify, fmz <> []: nxt <> Add_Relation.."
8.220 +else (); (*different with show_types !!!*)
8.221 +*)
8.222 +
8.223 +val nxt = Add_Relation "relations [(A=a+b)]";
8.224 +val nxt = mstep2mstep' pt p nxt;
8.225 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.226 +(*val nxt = Specify_Method ("e_domID","e_metID") : mstep*)
8.227 +
8.228 +val nxt = Specify_Method ("DiffApp.thy","max_by_calculus");
8.229 +val nxt = mstep2mstep' pt p nxt;
8.230 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.231 +(*val nxt = Add_Given "boundVariable" : mstep*)
8.232 +
8.233 +val nxt = Add_Given "boundVariable alpha";
8.234 +val nxt = mstep2mstep' pt p nxt;
8.235 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.236 +(*val nxt = Add_Given "interval" : mstep*)
8.237 +
8.238 +val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";
8.239 +val nxt = mstep2mstep' pt p nxt;
8.240 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.241 +(*val nxt = Add_Given "errorBound" : mstep*)
8.242 +
8.243 +val nxt = Add_Given "errorBound (eps=999)";
8.244 +val nxt = mstep2mstep' pt p nxt;
8.245 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
8.246 +(*val nxt = Apply_Method ("DiffApp.thy","max_by_calculus") *)
8.247 +
8.248 +(*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
8.249 +if nxt<>(Apply_Method ("DiffApp.thy","max_by_calculus"))
8.250 +then raise error "test specify, fmz <> []: nxt <> Add_Relation.."
8.251 +else ();
8.252 +*)
8.253 +
8.254 +(* 2.4.00 nach Transfer specify -> hard_gen
8.255 +val nxt = Apply_Method ("DiffApp.thy","max_by_calculus");
8.256 +val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
8.257 +(*val nxt = Empty_Mstep : mstep*)
8.258 +
8.259 +
8.260 +
8.261 +(* use_thy_only"Isa99/knowl-base/Script";
8.262 + *)
8.263 +
8.264 +
8.265 +
8.266 +" #################################################### ";
8.267 +" problemtypes + formalizations ";
8.268 +" #################################################### ";
8.269 +" -------------- [maximum_of,function] --------------- ";
8.270 +val pbt =
8.271 + ["fixedValues fix_","maximum m_","valuesFor vs_","relations rs_"];
8.272 +map (the o (parseold thy)) pbt;
8.273 +val fmz =
8.274 + ["fixedValues [r=Arbfix]","maximum A",
8.275 + "valuesFor [a=Undef,b=Undef]",
8.276 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
8.277 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
8.278 + "relations [A=a*b, a=2*r*sin alpha, b=2*r*cos alpha]",
8.279 +
8.280 + "boundVariable a","boundVariable b","boundVariable alpha",
8.281 + "interval {x::real. 0 <= x & x <= 2*r}",
8.282 + "interval {x::real. 0 <= x & x <= 2*r}",
8.283 + "interval {x::real. 0 <= x & x <= pi}",
8.284 + "errorBound (eps=(0::real))"];
8.285 +map (the o (parseold thy)) fmz;
8.286 +" -------------- [make,function] -------------- ";
8.287 +val pbt =
8.288 + ["functionOf f_","boundVariable v_","equalities eqs_",
8.289 + "functionTerm f_0_"];
8.290 +map (the o (parseold thy)) pbt;
8.291 +val fmz12 =
8.292 + ["functionOf A","boundVariable a","boundVariable b",
8.293 + "equalities [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
8.294 + (*28.11.00: "functionTerm (A_0=Undef)"*)"functionTerm (Undef)"];
8.295 +map (the o (parseold thy)) fmz12;
8.296 +val fmz3 =
8.297 + ["functionOf A","boundVariable a","boundVariable b",
8.298 + "equalities [A=a*b, a=2*R*sin alpha, b=2*R*cos alpha]",
8.299 + (*28.11.00: "functionTerm (A_0=Undef)"*)"functionTerm (Undef)"];
8.300 +map (the o (parseold thy)) fmz3;
8.301 +" --------- [univar,equation] --------- ";
8.302 +val pbt =
8.303 + ["equality e_","solveFor v_","solutions v_i_"];
8.304 +map (the o (parseold thy)) pbt;
8.305 +val fmz =
8.306 + ["equality ((a/2)^^^2 + (b/2)^^^2 = r^^^2)",
8.307 + "solveFor b","solutions b_i"];
8.308 +map (the o (parseold thy)) fmz;
8.309 +" ---- [on_interval,maximum_of,function] ---- ";
8.310 +val pbt =
8.311 + ["functionTerm t_","boundVariable v_","interval itv_",
8.312 + "errorBound err_","maxArgument v_0_"];
8.313 +map (the o (parseold thy)) pbt;
8.314 +val fmz12 =
8.315 + [(*28.11.00: "functionTerm (A_0 = a*sqrt(#4*r^^^#2 - a^^^#2))",*)
8.316 + "functionTerm (a*sqrt(4*r^^^2 - a^^^2))",
8.317 + (*28.11.00: "functionTerm (A_0 = b*sqrt(#4*r^^^#2 - b^^^#2))",*)
8.318 + "functionTerm (b*sqrt(4*r^^^2 - b^^^2))",
8.319 + "boundVariable a","boundVariable b",
8.320 + "interval {x::real. 0 <= x & x <= 2*r}",
8.321 + "errorBound (eps=0)","maxArgument (a_0=Undef)"];
8.322 +map (the o (parseold thy)) fmz12;
8.323 +val fmz3 =
8.324 + [(*28.11.00: "functionTerm (A_0 = (#2*r*sin alpha)*(#2*r*cos alpha))",*)
8.325 + "functionTerm ((2*r*sin alpha)*(2*r*cos alpha))",
8.326 + "boundVariable alpha",
8.327 + "interval {x::real. 0 <= x & x <= pi}",
8.328 + "errorBound (eps=0)","maxArgument (a_0=Undef)"];
8.329 +map (the o (parseold thy)) fmz3;
8.330 +" --------- [derivative_of,function] --------- ";
8.331 +val pbt =
8.332 + ["functionTerm f_","boundVariable v_","derivative f_'_"];
8.333 +map (the o (parseold thy)) pbt;
8.334 +val fmz =
8.335 + [(*28.11.00: "functionTerm (A_0=a*#2*sqrt r^^^#2 - (a//#2)^^^#2)",*)
8.336 + "functionTerm (a*2*sqrt r^^^2 - (a/2)^^^2)",
8.337 + "boundVariable a",
8.338 + (*28.11.00: "derivative (A_0'=Undef)"*)"derivative (Undef)"];
8.339 +map (the o (parseold thy)) fmz;
8.340 +" --------- [find_values,tool] --------- ";
8.341 +val pbt =
8.342 + ["maxArgument ma_","functionTerm f_","boundVariable v_",
8.343 + "valuesFor vls_","additionalRels rs_"];
8.344 +map (the o (parseold thy)) pbt;
8.345 +val fmz1 =
8.346 + ["maxArgument (a_0=(srqt 2)*r)",
8.347 + (*28.11.00: "functionTerm (A_0=a*#2*sqrt r^^^#2 - (a//#2)^^^#2)",*)
8.348 + "functionTerm (a*2*sqrt r^^^2 - (a/2)^^^2)",
8.349 + "boundVariable a",
8.350 + "valuesFor [a=Undef,b=Undef]","maximum A",
8.351 + "additionalRels [(a/2)^^^2 + (b/2)^^^2 = r^^^2]"];
8.352 +map (the o (parseold thy)) fmz1;
8.353 +
8.354 +"---------------------------------------------------------------------";
8.355 +"---------------------------------------------------------------------";
8.356 +"---------------------------------------------------------------------";
8.357 +
8.358 +(* Teil von max-on-surface.sml,
8.359 + der nach Init_Proof -> prep_ori wieder l"auft
8.360 + (f"ur tests mit neuer pos')
8.361 + use"test-max-surf1.sml";
8.362 +
8.363 + Compiler.Control.Print.printDepth:=10; (*4 is default*)
8.364 + Compiler.Control.Print.printDepth:=4; (*4 is default*)
8.365 + *)
8.366 +
8.367 +(* --vvv-- ausgeliehen von test-root-equ/sml *)
8.368 +val loc = e_istate;
8.369 +val (dI',pI',mI') =
8.370 + ("Script.thy",["sqroot-test","univariate","equation"],
8.371 + ("Script.thy","squ-equ-test2"));
8.372 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
8.373 + "solveFor x","errorBound (eps=0)",
8.374 + "solutions L"];
8.375 +(*
8.376 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
8.377 +val ((p,p_),_,_,_,_,(_,pt,_)) = do_ (mI,m) e_pos'[1](e_scr,EmptyPtree,[]);
8.378 + --^^^-- ausgeliehen von test-root-equ/sml *)
8.379 +val (pt,_) =
8.380 + cappend_problem EmptyPtree [] loc ([],(dI',pI',mI'));
8.381 +val pos = (lev_on o lev_dn) [];
8.382 +(* val pos = ([1]) *)
8.383 +val (pt,_) = cappend_parent pt pos loc "{(a,b). is-max ..."
8.384 + Empty_Mstep Transitive;
8.385 +val pos = (lev_on o lev_dn) pos;
8.386 +(*val pos = ([1,1])*)
8.387 +val (pt,_) = cappend_atomic pt pos loc "{(a,b). is-max ..."
8.388 + Empty_Mstep "[1,1]:{(a,b). is-extremum ..." Complete;
8.389 +val pos = lev_on pos;
8.390 +(*val pos = ([1,2])*)
8.391 +val (pt,_) = cappend_atomic pt pos loc "{(a,b). is-extremum ..."
8.392 + Empty_Mstep "[1,2]:{(a,b). f_x(a,b) ..." Complete;
8.393 +val pos = lev_up pos;
8.394 +(*val pos = ([1])*)
8.395 +val (pt,_) = append_result pt pos e_istate "[1#]:{(a,b). f_x(a,b) ..."
8.396 + Complete;
8.397 +
8.398 +val pos = lev_on pos;
8.399 +(*val pos = ([2]) *)
8.400 +val (pt,_) = cappend_atomic pt pos loc "{(a,b). f_x(a,b) ..."
8.401 + Empty_Mstep "[2]:{(a,b). f_x & f_xx &..." Complete;
8.402 +val pos = lev_on pos;
8.403 +(*al pos = [3] : pos*)
8.404 +val (pt,_) = cappend_parent pt pos loc "{(a,b). f_x & f_xx &..."
8.405 + Empty_Mstep Transitive;
8.406 +val pos = (lev_on o lev_dn) pos;
8.407 +(*pos = ([3,1]) *)
8.408 +val (pt,_) = cappend_atomic pt pos loc "{(a,b). f_x & f_xx & ..."
8.409 + Empty_Mstep "[3,1]:{(a,b). f_x & f_xx } cup ..." Complete;
8.410 +val pos = lev_on pos;
8.411 +(*pos = ([3,2]) *)
8.412 +val (pt,_) = cappend_atomic pt pos loc "{(a,b). f_x & f_xx } cup.."
8.413 + Empty_Mstep "[3,2]:{(a,b). f_x ..} cup ..." Complete;
8.414 +
8.415 +val pos = lev_up pos;
8.416 +(*pos = ([3]) *)
8.417 +val (pt,_) = append_result pt pos e_istate "[3#]:{(a,b). f_x ..} cup.."
8.418 + Complete;
8.419 +val pos = lev_on pos;
8.420 +(*val pos = [4] : pos *)
8.421 +val (pt,_) = cappend_parent pt pos loc "{(a,b). f_x ..} cup ..."
8.422 + Empty_Mstep Intersect;
8.423 +val pos = (lev_on o lev_dn) pos;
8.424 +(*val pos = ([4,1]) *)
8.425 +val (pt,_) = cappend_parent pt pos loc "set_1 = ..."
8.426 + Empty_Mstep Sequence;
8.427 +
8.428 +
8.429 +val pos = (lev_on o lev_dn) pos;
8.430 +(*val pos = ([4,1,1]) *)
8.431 +val (pt,_) = cappend_parent(*pbl*) pt pos loc"f_x = d/dx x^3 ..."
8.432 + Empty_Mstep Transitive;
8.433 +val pos = (lev_on o lev_dn) pos;
8.434 +(*val pos = ([4,1,1,1]) *)
8.435 +val (pt,_) = cappend_parent pt pos loc "d/dx x^3 ..."
8.436 + Empty_Mstep Transitive;
8.437 +val pos = (lev_on o lev_dn) pos;
8.438 +(*val pos = ([4,1,1,1,1]) *)
8.439 +val (pt,_) = cappend_atomic pt pos loc "d/dx x^3 ..."
8.440 + Empty_Mstep "[4,1,1,1,1]:3x^2 + d/dx ..." Complete;
8.441 +val pos = lev_on pos;
8.442 +(*val pos = ([4,1,1,1,2]) *)
8.443 +val (pt,_) = cappend_atomic pt pos loc "3x^2 + d/dx ..."
8.444 + Empty_Mstep "[4,1,1,1,2]:3x^2 + 0 + d/dx ..." Complete;
8.445 +val pos = lev_on pos;
8.446 +(*pos = ([4,1,1,1,3]) *)
8.447 +val (pt,_) = cappend_atomic pt pos loc "3x^2 + 0 + d/dx ..."
8.448 + Empty_Mstep "[4,1,1,1,3]:3x^2 + 0 -3 ..." Complete;
8.449 +"--- 1 ---";
8.450 +val pos = lev_up pos;
8.451 +(*pos = ([4,1,1,1]) *)
8.452 +val (pt,_) = append_result pt pos e_istate "[4,1,1,1#]:3x^2 -3."Complete;
8.453 +"--- 2 ---";
8.454 +val pos = lev_up pos;
8.455 +(*val pos = ([4,1,1]) *)
8.456 +val (pt,_) = append_result pt pos e_istate "[4,1,1#]:found 3x^2 -3 ..."
8.457 + Complete;
8.458 +"--- 3 ---";
8.459 +val pos = lev_on pos;
8.460 +(*val pos = ([4,1,2]+) *)
8.461 +val (pt,_) = cappend_parent(*pbl*) pt pos loc "f_y = d/dy x^3 ..."
8.462 + Empty_Mstep Transitive;
8.463 +"--- 4 ---";
8.464 +writeln (pr_ptree pr_short pt);
8.465 +
8.466 +(*
8.467 +. ----- pblobj -----
8.468 +1. {(a,b). is-max ...
8.469 +1.1. {(a,b). is-max ...
8.470 +1.2. {(a,b). is-extremum ...
8.471 +2. {(a,b). f_x(a,b) ...
8.472 +3. {(a,b). f_x & f_xx &...
8.473 +3.1. {(a,b). f_x & f_xx & ...
8.474 +3.2. {(a,b). f_x & f_xx } cup..
8.475 +4. {(a,b). f_x ..} cup ...
8.476 +4.1. set_1 = ...
8.477 +4.1.1. f_x = d/dx x^3 ...
8.478 +4.1.1.1. d/dx x^3 ...
8.479 +4.1.1.1.1. d/dx x^3 ...
8.480 +4.1.1.1.2. 3x^2 + d/dx ...
8.481 +4.1.1.1.3. 3x^2 + 0 + d/dx ...
8.482 +4.1.2. f_y = d/dy x^3 ...
8.483 +
8.484 + use"test-max-surf1.sml";
8.485 + *)
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/sml/kbtest/float.sml Thu Apr 17 18:01:03 2003 +0200
9.3 @@ -0,0 +1,2 @@
9.4 +(* testexamples for Float, floating point numerals
9.5 + *)
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/sml/kbtest/inssort.sml Thu Apr 17 18:01:03 2003 +0200
10.3 @@ -0,0 +1,135 @@
10.4 +(* use"test-inssort.sml";
10.5 + W.N.17.6.00
10.6 +*)
10.7 +
10.8 +"--------------- sort [1,4,3,2] by rewrite_set ----------------";
10.9 +val thy' = "InsSort.thy";
10.10 +val ct = "sort [1,4,3,2]";
10.11 +"--- 1 ---";
10.12 +val rls = "ins_sort";
10.13 +val (ct,_) = the (rewrite_set thy' "eval_rls" false rls ct);
10.14 +if ct="[1, 2, 3, 4]" then "sort [1,4,3,2] OK"
10.15 +else raise error "sort [1,4,3,2] didn't work";
10.16 +
10.17 +
10.18 +"---------------- sort [1,3,2] by rewrite stepwise ----------------";
10.19 +val thy' = "InsSort.thy";
10.20 +val ct = "sort [1,3,2]";
10.21 +"--- 1 ---";
10.22 +val thm = ("sort_def","");
10.23 +val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
10.24 +(*val ct = "foldr ins [#1::real, #3::real, #2::real] []"*)
10.25 +"--- 2 ---";
10.26 +val thm = ("foldr_rec","");
10.27 +val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
10.28 +(*val ct = "foldr ins [#3, #2] (ins [] #1)"*)
10.29 +"--- 3 ---";
10.30 +val thm = ("ins_base","");
10.31 +val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
10.32 +(*val ct = "foldr ins [#3, #2] [#1]"*)
10.33 +"--- 4 ---";
10.34 +val thm = ("foldr_rec","");
10.35 +val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
10.36 +(*val ct = "foldr ins [#2] (ins [#1] #3)"*)
10.37 +"--- 5 ---";
10.38 +val thm = ("ins_rec","");
10.39 +val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
10.40 +(*val ct = "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])"*)
10.41 +"--- 6 ---";
10.42 +val op_ = "le";
10.43 +val (ct,_) = the (calculate thy' op_ ct);
10.44 +(*val ct = "foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])"*)
10.45 +"--- 7 ---";
10.46 +val thm = ("if_True","");
10.47 +val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
10.48 +(*val ct = "foldr ins [#2] (#1 # ins [] #3)"*)
10.49 +"--- 8 ---";
10.50 +val thm = ("ins_base","");
10.51 +val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
10.52 +(*val ct = "foldr ins [#2] [#1, #3]"*)
10.53 +"--- 9 ---";
10.54 +val thm = ("foldr_rec","");
10.55 +val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
10.56 +(*val ct = "foldr ins [] (ins [#1, #3] #2)"*)
10.57 +"--- 10 ---";
10.58 +val thm = ("ins_rec","");
10.59 +val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
10.60 +(*val ct = "foldr ins [] (if #1 < #2 then #1 # ins [#3] #2 else [#2, #1, #3])"*)
10.61 +"--- 11 ---";
10.62 +val op_ = "le";
10.63 +val (ct,_) = the (calculate thy' op_ ct);
10.64 +(*val ct = "foldr ins [] (if True then #1 # ins [#3] #2 else [#2, #1, #3])"*)
10.65 +"--- 12 ---";
10.66 +val thm = ("if_True","");
10.67 +val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
10.68 +(*"foldr ins [] (#1 # ins [#3] #2)"*)
10.69 +"--- 13 ---";
10.70 +val thm = ("ins_rec","");
10.71 +val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
10.72 +(*"foldr ins [] (#1 # (if #3 < #2 then #3 # ins [] #2 else [#2, #3]))"*)
10.73 +"--- 14 ---";
10.74 +val op_ = "le";
10.75 +val (ct,_) = the (calculate thy' op_ ct);
10.76 +(*val ct = "foldr ins [] (#1 # (if False then #3 # ins [] #2 else [#2, #3]))"*)
10.77 +"--- 15 ---";
10.78 +val thm = ("if_False","");
10.79 +val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
10.80 +(*val ct = "foldr ins [] [#1, #2, #3]"*)
10.81 +"--- 16 ---";
10.82 +val thm = ("foldr_base","");
10.83 +val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
10.84 +(*val ct = "[#1, #2, #3]"*)
10.85 +if ct="[1, 2, 3]" then "sort [1,3,2] OK"
10.86 +else raise error "sort [1,3,2] didn't work";
10.87 +
10.88 +
10.89 +"---------------- sort [1,3,2] from script ----------------";
10.90 +val fmz = ["unsorted [1,3,2]", "sorted S"];
10.91 +val (dI',pI',mI') =
10.92 + ("InsSort.thy", ["inssort","functional"], ("InsSort.thy","inssort"));
10.93 +val p = e_pos'; val c = [];
10.94 +
10.95 +
10.96 +
10.97 +(* ------- 17.6.00: mit kleinen problemen aufgegeben
10.98 +val scr=Script ((term_of o the o (parse thy))
10.99 + "Script Sort (u_::'a list) = \
10.100 + \ Rewrite_Set ins_sort False u_");
10.101 +
10.102 +val scr=Script ((term_of o the o (parse thy))
10.103 + "Script Ins_sort (u_::real list) = \
10.104 + \ (let u_ = Rewrite sort_def False u_; \
10.105 + \ u_ = Rewrite foldr_rec False u_; \
10.106 + \ u_ = Rewrite ins_base False u_; \
10.107 + \ u_ = Rewrite foldr_rec False u_; \
10.108 + \ u_ = Rewrite ins_rec False u_; \
10.109 + \ u_ = Calculate le u_; \
10.110 + \ u_ = Rewrite if_True False u_; \
10.111 + \ u_ = Rewrite ins_base False u_; \
10.112 + \ u_ = Rewrite foldr_rec False u_; \
10.113 + \ u_ = Rewrite ins_rec False u_; \
10.114 + \ u_ = Calculate le u_; \
10.115 + \ u_ = Rewrite if_True False u_; \
10.116 + \ u_ = Rewrite ins_rec False u_; \
10.117 + \ u_ = Calculate le u_; \
10.118 + \ u_ = Rewrite if_False False u_; \
10.119 + \ u_ = Rewrite foldr_base False u_ \
10.120 + \ in u_)");
10.121 +val scr=parse thy
10.122 + "Script Ins_sort (u_::real list) = \
10.123 + \ (let u_ = Rewrite sort_def False u_; \
10.124 + \ u_ = Rewrite foldr_rec False u_; \
10.125 + \ u_ = Rewrite ins_base False u_; \
10.126 + \ u_ = Rewrite foldr_rec False u_; \
10.127 + \ u_ = Rewrite ins_rec False u_; \
10.128 + \ u_ = Calculate le u_; \
10.129 + \ u_ = Rewrite if_True False u_; \
10.130 + \ u_ = Rewrite ins_base False u_; \
10.131 + \ u_ = Rewrite foldr_rec False u_; \
10.132 + \ u_ = Rewrite ins_rec False u_; \
10.133 + \ u_ = u_ \
10.134 + \ in u_)";
10.135 +
10.136 +atomty thy (term_of (the scr));
10.137 +
10.138 +------- *)
10.139 \ No newline at end of file