diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/ProgLang/calculate.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/ProgLang/calculate.sml Wed Aug 25 16:20:07 2010 +0200 @@ -0,0 +1,408 @@ +(* calculate values for function constants + (c) Walther Neuper 000106 + +use"ProgLang/calculate.sml"; +*) + + +(* dirty type-conversion 30.1.00 for "fixed_values [R=R]" *) + +val aT = Type ("'a", []); +(* isas types for Free, parseold: (1) "R=R" or (2) "R=(R::real)": +(1) +> val (TFree(ss2,TT2)) = T2; +val ss2 = "'a" : string +val TT2 = ["term"] : sort +(2) +> val (Type(ss2',TT2')) = T2'; +val ss2' = "RealDef.real" : string +val TT2' = [] : typ list +(3) +val realType = TFree ("RealDef.real", HOLogic.termS); +is different internally, too; + +(1) .. (3) are displayed equally !!! +*) + + + +(* 30.1.00: generating special terms for ME: + (1) binary numerals reconverted to Free ("#num",...) + by libarary_G.num_str: called from parse (below) and + interface_ME_ISA for all thms used + (compare HOLogic.dest_binum) + (2) 'a types converted to RealDef.real by typ_a2real + in parse below + (3) binary operators fixed to type real in RatArith.thy + (trick by Markus Wenzel) +*) + + + + +(** calculate numerals **) + +(*27.3.00: problems with patterns below: +"Vars (a // #2 = r * xxxxx b)" doesn't work, but +"Vars (a // #2 = r * sqrt b)" works +*) + +fun popt2str (SOME (str, term)) = "SOME "^term2str term + | popt2str NONE = "NONE"; + +(* scan a term for applying eval_fn ef +args + thy: + op_: operator (as string) selecting the root of the pair + ef : fn : (string -> term -> theory -> (string * term) option) + ^^^^^^... for creating the string for the resulting theorem + t : term to be scanned +result: + (string * term) option: found by the eval_* -function of type + fn : string -> string -> term -> theory -> (string * term) option + ^^^^^^... the selecting operator op_ (variable for eval_binop) +*) +fun get_pair thy op_ (ef:string -> term -> theory -> (string * term) option) + (t as (Const(op0,t0) $ arg)) = (* unary fns *) +(* val (thy, op_, (ef), (t as (Const(op0,t0) $ arg))) = + (thy, op_, eval_fn, ct); + *) + if op_ = op0 then + let val popt = ef op_ t thy + in case popt of + SOME _ => popt + | NONE => get_pair thy op_ ef arg end + else get_pair thy op_ ef arg + + | get_pair thy "Atools.ident" ef (t as (Const("Atools.ident",t0) $ _ $ _ )) = +(* val (thy, "Atools.ident", ef, t as (Const(op0,_) $ t1 $ t2)) = + (thy, op_, eval_fn, ct); + *) + ef "Atools.ident" t thy (* not nested *) + + | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2)) = (* binary funs*) +(* val (thy, op_, ef, (t as (Const(op0,_) $ t1 $ t2))) = + (thy, op_, eval_fn, ct); + *) + ((*writeln("1.. get_pair: binop = "^op_);*) + if op_ = op0 then + let val popt = ef op_ t thy + (*val _ = writeln("2.. get_pair: "^term2str t^" -> "^popt2str popt)*) + in case popt of + SOME (id,_) => popt + | NONE => + let val popt = get_pair thy op_ ef t1 + (*val _ = writeln("3.. get_pair: "^term2str t1^ + " -> "^popt2str popt)*) + in case popt of + SOME (id,_) => popt + | NONE => get_pair thy op_ ef t2 + end + end + else (*search subterms*) + let val popt = get_pair thy op_ ef t1 + (*val _ = writeln("4.. get_pair: "^term2str t^" -> "^popt2str popt)*) + in case popt of + SOME (id,_) => popt + | NONE => get_pair thy op_ ef t2 + end) + | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2 $ t3)) =(* trinary funs*) + ((*writeln("### get_pair 4a: t= "^term2str t); + writeln("### get_pair 4a: op_= "^op_); + writeln("### get_pair 4a: op0= "^op0);*) + if op_ = op0 then + case ef op_ t thy of + SOME tt => SOME tt + | NONE => (case get_pair thy op_ ef t2 of + SOME tt => SOME tt + | NONE => get_pair thy op_ ef t3) + else (case get_pair thy op_ ef t1 of + SOME tt => SOME tt + | NONE => (case get_pair thy op_ ef t2 of + SOME tt => SOME tt + | NONE => get_pair thy op_ ef t3))) + | get_pair thy op_ ef (Const _) = NONE + | get_pair thy op_ ef (Free _) = NONE + | get_pair thy op_ ef (Var _) = NONE + | get_pair thy op_ ef (Bound _) = NONE + | get_pair thy op_ ef (Abs(a,T,body)) = get_pair thy op_ ef body + | get_pair thy op_ ef (t1$t2) = + let(*val _= writeln("5.. get_pair t1 $ t2: "^term2str t1^" + $ "^term2str t2)*) + val popt = get_pair thy op_ ef t1 + in case popt of + SOME _ => popt + | NONE => ((*writeln"### get_pair: t1 $ t2 -> NONE";*) + get_pair thy op_ ef t2) + end; + (* +> val t = (term_of o the o (parse thy)) "#3 + #4"; +> val eval_fn = the (assoc (!eval_list, "op +")); +> val (SOME (id,t')) = get_pair thy "op +" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> atomty t'; +> +> val t = (term_of o the o (parse thy)) "(a + #3) + #4"; +> val (SOME (id,t')) = get_pair thy "op +" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> +> val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))"; +> val (SOME (id,t')) = get_pair thy "op +" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> +> val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))"; +> atomty t; +> val (SOME (id,t')) = get_pair thy "op +" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> val it = "#3 + (#4 + a) = #7 + a" : string +> +> +> val t = (term_of o the o (parse thy)) "#-4//#-2"; +> val eval_fn = the (assoc (!eval_list, "cancel")); +> val (SOME (id,t')) = get_pair thy "cancel" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> +> val t = (term_of o the o (parse thy)) "#2^^^#3"; +> eval_binop "xxx" "pow" t thy; +> val eval_fn = (eval_binop "xxx") +> : string -> term -> theory -> (string * term) option; +> val SOME (id,t') = get_pair thy "pow" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> val eval_fn = the (assoc (!eval_list, "pow")); +> val (SOME (id,t')) = get_pair thy "pow" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> +> val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4"; +> val eval_fn = the (assoc (!eval_list, "op *")); +> val (SOME (id,t')) = get_pair thy "op *" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> +> val t = (term_of o the o (parse thy)) "#0 < #4"; +> val eval_fn = the (assoc (!eval_list, "op <")); +> val (SOME (id,t')) = get_pair thy "op <" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> val t = (term_of o the o (parse thy)) "#0 < #-4"; +> val (SOME (id,t')) = get_pair thy "op <" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> +> val t = (term_of o the o (parse thy)) "#3 is_const"; +> val eval_fn = the (assoc (!eval_list, "is'_const")); +> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> val t = (term_of o the o (parse thy)) "a is_const"; +> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> +> val t = (term_of o the o (parse thy)) "#6//(#8::real)"; +> val eval_fn = the (assoc (!eval_list, "cancel")); +> val (SOME (id,t')) = get_pair thy "cancel" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> +> val t = (term_of o the o (parse thy)) "sqrt #12"; +> val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt")); +> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> val it = "sqrt #12 = #2 * sqrt #3 " : string +> +> val t = (term_of o the o (parse thy)) "sqrt #9"; +> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +> +> val t = (term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]"; +> val eval_fn = the (assoc (!eval_list, "Tools.Nth")); +> val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t; +> Syntax.string_of_term (thy2ctxt thy) t'; +*) + +(* val ((op_, eval_fn),ct)=(cc,pre); + (get_calculation_ Isac.thy (op_, eval_fn) ct) handle e => print_exn e; + parse thy "" + *) +(*.get a thm from an op_ somewhere in the term; + apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711).*) +fun get_calculation_ thy (op_, eval_fn) ct = +(* val (thy, (op_, eval_fn), ct) = + (thy, (the (assoc(!calclist',"order_system"))), t); + *) + case get_pair thy op_ eval_fn ct of + NONE => ((*writeln("@@@ get_calculation: NONE, op_="^op_); + writeln("@@@ get_calculation: ct= ");atomty ct;*) + NONE) + | SOME (thmid,t) => + ((*writeln("@@@ get_calculation: NONE, op_="^op_); + writeln("@@@ get_calculation: ct= ");atomty ct;*) + SOME (thmid, (make_thm o (cterm_of thy)) t)); +(* +> val ct = (the o (parse thy)) "#9 is_const"; +> get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct; +val it = SOME ("is_const9_","(is_const 9 ) = True [(is_const 9 ) = True]") + +> val ct = (the o (parse thy)) "sqrt #9"; +> get_calculation_ thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct; +val it = SOME ("sqrt_9_","sqrt 9 = 3 [sqrt 9 = 3]") : (string * thm) option + +> val ct = (the o (parse thy)) "#4<#4"; +> get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;fun is_no str = (hd o explode) str = "#"; + +val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]") + +> val ct = (the o (parse thy)) "a<#4"; +> get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct; +val it = NONE : (string * thm) option + +> val ct = (the o (parse thy)) "#5<=#4"; +> get_calculation_ thy ("op <=",the (assoc(!eval_list,"op <="))) ct; +val it = SOME ("less_equal_5_4","(5 <= 4) = False [(5 <= 4) = False]") + +-------------------------------------------------------------------6.8.02: + val thy = SqRoot.thy; + val t = (term_of o the o (parse thy)) "1+2"; + get_calculation_ thy (the(assoc(!calc_list,"PLUS"))) t; + val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option +-------------------------------------------------------------------6.8.02: + val t = (term_of o the o (parse thy)) "-1"; + atomty t; + val t = (term_of o the o (parse thy)) "0"; + atomty t; + val t = (term_of o the o (parse thy)) "1"; + atomty t; + val t = (term_of o the o (parse thy)) "2"; + atomty t; + val t = (term_of o the o (parse thy)) "999999999"; + atomty t; +-------------------------------------------------------------------6.8.02: + +> val ct = (the o (parse thy)) "a+#3+#4"; +> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct; +val it = SOME ("add_3_4","a + 3 + 4 = a + 7 [a + 3 + 4 = a + 7]") + +> val ct = (the o (parse thy)) "#3+(#4+a)"; +> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct; +val it = SOME ("add_3_4","3 + (4 + a) = 7 + a [3 + (4 + a) = 7 + a]") + +> val ct = (the o (parse thy)) "a+(#3+#4)+#5"; +> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct; +val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option + +> val ct = (the o (parse thy)) "#3*(#4*a)"; +> get_calculation_ thy ("op *",the (assoc(!eval_list,"op *"))) ct; +val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a [3 * (4 * a) = 12 * a]") + +> val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5"; +> get_calculation_ thy ("pow",the (assoc(!eval_list,"pow"))) ct; +val it = SOME ("4_(+2)","4 ^ 2 = 16 [4 ^ 2 = 16]") : (string * thm) option + +> val ct = (the o (parse thy)) "#-4//#-2"; +> get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct; +val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2) [(-4) // (-2) = (+2)]") + +> val ct = (the o (parse thy)) "#6//#-8"; +> get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct; +val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4 [6 // (-8) = (-3) // 4]") + +*) + + +(* +> val ct = (the o (parse thy)) "a + 3*4"; +> applicable "calculate" (Calc("op *", "mult_")) ct; +val it = SOME "3 * 4 = 12 [3 * 4 = 12]" : thm option + +-------------------------- +> val ct = (the o (parse thy)) "3 =!= 3"; +> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct); +val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm + +> val ct = (the o (parse thy)) "~ (3 =!= 3)"; +> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct); +val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm + +> val ct = (the o (parse thy)) "3 =!= 4"; +> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct); +val thm = "(3 =!= 4) = False [(3 =!= 4) = False]" : thm + +> val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))"; +> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct); + "(4 + (4 * x + x ^ 2) =!= (+0)) = False" + +> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))"; +> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct); + "(4 + (4 * x + x ^ 2) =!= (+0)) = False" + +> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))"; +> val rls = eval_rls; +> val (ct,_) = the (rewrite_set_ thy false rls ct); +val ct = "True" : cterm +-------------------------- +*) + + +(*.get a thm applying an op_ to a term; + apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711).*) +(* val (thy, (op_, eval_fn), ct) = + (thy, ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"), term); + *) +fun get_calculation1_ thy ((op_, eval_fn):cal) ct = + case eval_fn op_ ct thy of + NONE => NONE + | SOME (thmid,t) => + SOME (thmid, (make_thm o (cterm_of thy)) t); + + + + + +(*.substitute bdv in an rls and leave Calc as they are.(*28.10.02*) +fun inst_thm' subs (Thm (id, thm)) = + Thm (id, (*read_instantiate throws: *** No such variable in term: ?bdv*) + (read_instantiate subs thm) handle _ => thm) + | inst_thm' _ calc = calc; +fun inst_thm' (subs as (bdv,_)::_) (Thm (id, thm)) = + Thm (id, (writeln("@@@ inst_thm': thm= "^(string_of_thmI thm)); + if bdv mem (vars_str o #prop o rep_thm) thm + then (writeln("@@@ inst_thm': read_instantiate, thm="^((string_of_thmI thm))); + read_instantiate subs thm) + else (writeln("@@@ inst_thm': not mem.. "^bdv); + thm))) + | inst_thm' _ calc = calc; + +fun instantiate_rls subs + (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca, + asm_thm=at,rules=rules,scr=scr}:rls) = + (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca, + asm_thm=at,scr=scr, + rules = map (inst_thm' subs) rules}:rls);---------------------------*) + + + +(** rewriting: ordered, conditional **) + +fun mk_rule (prems,l,r) = + Trueprop $ (list_implies (prems, mk_equality (l,r))); + +(* 'norms' a rule, e.g. +(*1*) a = 1 ==> a*(b+c) = b+c + => a = 1 ==> a*(b+c) = b+c no change +(*2*) t = t => (t=t) = True !! +(*3*) [| k < l; m + l = k + n |] ==> m < n + => [| k m < n = True !! *) +(* val it = fn : term -> term *) +fun norm rule = + let + val (prems,concl)=(map strip_trueprop(Logic.strip_imp_prems rule), + (strip_trueprop o Logic.strip_imp_concl)rule) + in if is_equality concl then + let val (l,r) = dest_equals' concl + in if l = r then + (*2*) mk_rule(prems,concl,true_as_term) + else (*1*) rule end + else (*3*) mk_rule(prems,concl,true_as_term) + end; + + + + + + + +