# HG changeset patch # User Walther Neuper # Date 1519563762 -3600 # Node ID ae0b7006fc28f4651808097755f58d810df356ae # Parent 2f2d25889153e95f057fe5419bac7fe62abb2f22 Calc: cleanup source file diff -r 2f2d25889153 -r ae0b7006fc28 src/Tools/isac/ProgLang/calculate.sml --- a/src/Tools/isac/ProgLang/calculate.sml Sun Feb 25 12:36:23 2018 +0100 +++ b/src/Tools/isac/ProgLang/calculate.sml Sun Feb 25 14:02:42 2018 +0100 @@ -2,9 +2,8 @@ (c) Walther Neuper 000106 *) -signature CALC = +signature NUMERAL_CALCULATION = sig - val aT: typ val adhoc_thm: theory -> string * eval_fn -> term -> (string * thm) option val adhoc_thm1_: theory -> cal -> term -> (string * thm) option val norm: term -> term @@ -18,52 +17,12 @@ end (**) -structure Calc(**): CALC(**) = +structure Calc(**): NUMERAL_CALCULATION(**) = struct (**) -(* 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 (_, term)) = "SOME " ^ term2str term | popt2str NONE = "NONE"; @@ -79,6 +38,17 @@ fn : string -> string -> term -> theory -> (string * term) option ^^^^^^... the selecting operator op_ (variable for eval_binop) *) +fun trace_calc0 str = + if ! trace_calc then writeln ("### " ^ str) else () +fun trace_calc1 str1 str2 = + if ! trace_calc then writeln (str1 ^ str2) else () +fun trace_calc2 str term popt = + if ! trace_calc then writeln (str ^ term2str term ^ " , " ^ popt2str popt) else () +fun trace_calc3 str term = + if ! trace_calc then writeln ("### " ^ str ^ term2str term) else () +fun trace_calc4 str t1 t2 = + if ! trace_calc then writeln ("### " ^ str ^ term2str t1 ^ " $ " ^ term2str t2) else () + fun get_pair thy op_ (ef: eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *) if op_ = op0 then let val popt = ef op_ t thy @@ -87,23 +57,26 @@ | get_pair thy "Atools.ident" ef (t as (Const ("Atools.ident", _) $ _ $ _ )) = ef "Atools.ident" t thy (* not nested *) | get_pair thy op_ ef (t as (Const (op0,_) $ t1 $ t2)) = (* binary funs *) - ((* tracing ("1.. get_pair: binop = "^op_); *) + (trace_calc1 "1.. get_pair: binop = " op_; if op_ = op0 then - let val popt = ef op_ t thy - (* val _ = tracing ("2.. get_pair: " ^ term2str t ^ " -> " ^ popt2str popt) *) + let + val popt = ef op_ t thy + val _ = trace_calc2 "2.. get_pair: " t popt in case popt of SOME _ => popt | NONE => - let val popt = get_pair thy op_ ef t1 - (* val _ = tracing ("3.. get_pair: " ^ term2str t1 ^ " -> "^popt2str popt) *) + let + val popt = get_pair thy op_ ef t1 + val _ = trace_calc2 "3.. get_pair: " t1 popt in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end end else (* search subterms *) - let val popt = get_pair thy op_ ef t1 - (*val _ = tracing("4.. get_pair: "^term2str t^" -> "^popt2str popt)*) + let + val popt = get_pair thy op_ ef t1 + val _ = trace_calc2 "4.. get_pair: " t popt in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end) | get_pair thy op_ ef (t as (Const (op0, _) $ t1 $ t2 $ t3)) = (* ternary funs *) - ((*tracing ("### get_pair 4a: t= " ^ term2str t); - tracing ("### get_pair 4a: op_= " ^ op_); - tracing ("### get_pair 4a: op0= " ^ op0); *) + (trace_calc3 "get_pair 4a: t= "t; + trace_calc1 "get_pair 4a: op_= " op_; + trace_calc1 "get_pair 4a: op0= " op0; if op_ = op0 then case ef op_ t thy of st as SOME _ => st | NONE => (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3) @@ -112,248 +85,30 @@ (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3))) | get_pair thy op_ ef (Abs (_, _, body)) = get_pair thy op_ ef body | get_pair thy op_ ef (t1 $ t2) = - let (* val _= tracing ("5.. get_pair t1 $ t2: " ^ term2str t1 ^ " $ " ^ term2str t2) *) + let + val _ = trace_calc4 "5.. get_pair t1 $ t2: " t1 t2; val popt = get_pair thy op_ ef t1 in case popt of SOME _ => popt - | NONE => ((* tracing "### get_pair: t1 $ t2 -> NONE"; *) get_pair thy op_ ef t2) + | NONE => (trace_calc0 "### get_pair: t1 $ t2 -> NONE"; get_pair thy op_ ef t2) end | get_pair _ _ _ _ = NONE - (* -> val t = (Thm.term_of o the o (parse thy)) "#3 + #4"; -> val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus")); -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; -> term2str t'; -> atomty t'; -> -> val t = (Thm.term_of o the o (parse thy)) "(a + #3) + #4"; -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; -> term2str t'; -> -> val t = (Thm.term_of o the o (parse thy)) "#3 + (#4 + (a::real))"; -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; -> term2str t'; -> -> val t = (Thm.term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))"; -> atomty t; -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; -> term2str t'; -> val it = "#3 + (#4 + a) = #7 + a" : string -> -> -> val t = (Thm.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; -> term2str t'; -> -> val t = (Thm.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; -> term2str t'; -> val eval_fn = the (assoc (!eval_list, "pow")); -> val (SOME (id,t')) = get_pair thy "pow" eval_fn t; -> term2str t'; -> -> val t = (Thm.term_of o the o (parse thy)) "x = #0 + #-1 * #-4"; -> val eval_fn = the (assoc (!eval_list, "Groups.times_class.times")); -> val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t; -> term2str t'; -> -> val t = (Thm.term_of o the o (parse thy)) "#0 < #4"; -> val eval_fn = the (assoc (!eval_list, "Orderings.ord_class.less")); -> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t; -> term2str t'; -> val t = (Thm.term_of o the o (parse thy)) "#0 < #-4"; -> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t; -> term2str t'; -> -> val t = (Thm.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; -> term2str t'; -> val t = (Thm.term_of o the o (parse thy)) "a is_const"; -> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t; -> term2str t'; -> -> val t = (Thm.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; -> term2str t'; -> -> val t = (Thm.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; -> term2str t'; -> val it = "sqrt #12 = #2 * sqrt #3 " : string -> -> val t = (Thm.term_of o the o (parse thy)) "sqrt #9"; -> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t; -> term2str t'; -> -> val t = (Thm.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; -> term2str t'; -*) - -(* val ((op_, eval_fn),ct)=(cc,pre); - (adhoc_thm (Thy_Info_get_theory "Isac") (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).*) +(* get a thm from an op_ somewhere in the term; + apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711) *) fun adhoc_thm thy (op_, eval_fn) ct = case get_pair thy op_ eval_fn ct of - NONE => ((* tracing ("@@@ adhoc_thm: NONE, op_= " ^ op_); - tracing ("@@@ adhoc_thm: ct= "); atomty ct; *) - NONE) + NONE => NONE | SOME (thmid, t) => SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of thy)) t); -(* -> val ct = (the o (parse thy)) "#9 is_const"; -> adhoc_thm 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"; -> adhoc_thm 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"; -> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o Symbol.explode) str = "#"; - -val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]") - -> val ct = (the o (parse thy)) "a<#4"; -> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct; -val it = NONE : (string * thm) option - -> val ct = (the o (parse thy)) "#5<=#4"; -> adhoc_thm thy ("Orderings.ord_class.less_eq",the (assoc(!eval_list,"Orderings.ord_class.less_eq"))) ct; -val it = SOME ("less_equal_5_4","(5 <= 4) = False [(5 <= 4) = False]") - --------------------------------------------------------------------6.8.02: - val thy = SqRoot.thy; - val t = (Thm.term_of o the o (parse thy)) "1+2"; - adhoc_thm 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 = (Thm.term_of o the o (parse thy)) "-1"; - atomty t; - val t = (Thm.term_of o the o (parse thy)) "0"; - atomty t; - val t = (Thm.term_of o the o (parse thy)) "1"; - atomty t; - val t = (Thm.term_of o the o (parse thy)) "2"; - atomty t; - val t = (Thm.term_of o the o (parse thy)) "999999999"; - atomty t; --------------------------------------------------------------------6.8.02: - -> val ct = (the o (parse thy)) "a+#3+#4"; -> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) 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)"; -> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) 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"; -> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) 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)"; -> adhoc_thm thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) 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"; -> adhoc_thm 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"; -> adhoc_thm 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"; -> adhoc_thm 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("Groups.times_class.times", "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 (adhoc_thm 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 (adhoc_thm 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 (adhoc_thm 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 (adhoc_thm 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 (adhoc_thm 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 = "HOL.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 adhoc_thm1_ thy ((op_, eval_fn):cal) ct = +(* get a thm applying an op_ to a term; + apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711) *) +fun adhoc_thm1_ thy (op_, eval_fn) ct = case eval_fn op_ ct thy of NONE => NONE | SOME (thmid,t) => SOME (thmid, (Thm.make_thm o (Thm.global_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, (tracing("@@@ inst_thm': thm= "^(string_of_thmI thm)); - if bdv mem (vars_str o #prop o rep_thm) thm - then (tracing("@@@ inst_thm': read_instantiate, thm="^((string_of_thmI thm))); - read_instantiate subs thm) - else (tracing("@@@ 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 **) +(** for ordered and conditional rewriting **) fun mk_rule (prems,l,r) = Trueprop $ (list_implies (prems, mk_equality (l,r))); diff -r 2f2d25889153 -r ae0b7006fc28 src/Tools/isac/calcelems.sml --- a/src/Tools/isac/calcelems.sml Sun Feb 25 12:36:23 2018 +0100 +++ b/src/Tools/isac/calcelems.sml Sun Feb 25 14:02:42 2018 +0100 @@ -838,6 +838,8 @@ fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1; +(* trace internal steps of isac's numeral calculations *) +val trace_calc = Unsynchronized.ref false; (*.trace internal steps of isac's rewriter*) val trace_rewrite = Unsynchronized.ref false; (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*) diff -r 2f2d25889153 -r ae0b7006fc28 test/Tools/isac/ProgLang/calculate.sml --- a/test/Tools/isac/ProgLang/calculate.sml Sun Feb 25 12:36:23 2018 +0100 +++ b/test/Tools/isac/ProgLang/calculate.sml Sun Feb 25 14:02:42 2018 +0100 @@ -1,9 +1,6 @@ (* Title: test calculation of values for function constants Author: Walther Neuper 2000 (c) copyright due to lincense terms. - -12345678901234567890123456789012345678901234567890123456789012345678901234567890 - 10 20 30 40 50 60 70 80 *) "--------------------------------------------------------"; @@ -20,6 +17,8 @@ " ================= calculate.sml: calculate_ 2002 ======"; "----------- get_pair with 3 args -----------------------"; "----------- calculate (2 * x is_const) -----------------"; +"----------- fun get_pair: examples ------------------------------------------------------------"; +"----------- fun adhoc_thm: examples -----------------------------------------------------------"; "--------------------------------------------------------"; "--------------------------------------------------------"; "--------------------------------------------------------"; @@ -325,3 +324,187 @@ val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t; term2str t'; "HOL.False"; + +"----------- fun get_pair: examples ------------------------------------------------------------"; +"----------- fun get_pair: examples ------------------------------------------------------------"; +"----------- fun get_pair: examples ------------------------------------------------------------"; + (* +> val t = (Thm.term_of o the o (parse thy)) "#3 + #4"; +> val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus")); +> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; +> term2str t'; +> atomty t'; +> +> val t = (Thm.term_of o the o (parse thy)) "(a + #3) + #4"; +> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; +> term2str t'; +> +> val t = (Thm.term_of o the o (parse thy)) "#3 + (#4 + (a::real))"; +> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; +> term2str t'; +> +> val t = (Thm.term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))"; +> atomty t; +> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; +> term2str t'; +> val it = "#3 + (#4 + a) = #7 + a" : string +> +> +> val t = (Thm.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; +> term2str t'; +> +> val t = (Thm.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; +> term2str t'; +> val eval_fn = the (assoc (!eval_list, "pow")); +> val (SOME (id,t')) = get_pair thy "pow" eval_fn t; +> term2str t'; +> +> val t = (Thm.term_of o the o (parse thy)) "x = #0 + #-1 * #-4"; +> val eval_fn = the (assoc (!eval_list, "Groups.times_class.times")); +> val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t; +> term2str t'; +> +> val t = (Thm.term_of o the o (parse thy)) "#0 < #4"; +> val eval_fn = the (assoc (!eval_list, "Orderings.ord_class.less")); +> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t; +> term2str t'; +> val t = (Thm.term_of o the o (parse thy)) "#0 < #-4"; +> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t; +> term2str t'; +> +> val t = (Thm.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; +> term2str t'; +> val t = (Thm.term_of o the o (parse thy)) "a is_const"; +> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t; +> term2str t'; +> +> val t = (Thm.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; +> term2str t'; +> +> val t = (Thm.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; +> term2str t'; +> val it = "sqrt #12 = #2 * sqrt #3 " : string +> +> val t = (Thm.term_of o the o (parse thy)) "sqrt #9"; +> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t; +> term2str t'; +> +> val t = (Thm.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; +> term2str t'; +*) +"----------- fun adhoc_thm: examples -----------------------------------------------------------"; +"----------- fun adhoc_thm: examples -----------------------------------------------------------"; +"----------- fun adhoc_thm: examples -----------------------------------------------------------"; +(* +> val ct = (the o (parse thy)) "#9 is_const"; +> adhoc_thm 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"; +> adhoc_thm 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"; +> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o Symbol.explode) str = "#"; + +val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]") + +> val ct = (the o (parse thy)) "a<#4"; +> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct; +val it = NONE : (string * thm) option + +> val ct = (the o (parse thy)) "#5<=#4"; +> adhoc_thm thy ("Orderings.ord_class.less_eq",the (assoc(!eval_list,"Orderings.ord_class.less_eq"))) ct; +val it = SOME ("less_equal_5_4","(5 <= 4) = False [(5 <= 4) = False]") + +-------------------------------------------------------------------6.8.02: + val thy = SqRoot.thy; + val t = (Thm.term_of o the o (parse thy)) "1+2"; + adhoc_thm 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 = (Thm.term_of o the o (parse thy)) "-1"; + atomty t; + val t = (Thm.term_of o the o (parse thy)) "0"; + atomty t; + val t = (Thm.term_of o the o (parse thy)) "1"; + atomty t; + val t = (Thm.term_of o the o (parse thy)) "2"; + atomty t; + val t = (Thm.term_of o the o (parse thy)) "999999999"; + atomty t; +-------------------------------------------------------------------6.8.02: + +> val ct = (the o (parse thy)) "a+#3+#4"; +> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) 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)"; +> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) 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"; +> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) 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)"; +> adhoc_thm thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) 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"; +> adhoc_thm 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"; +> adhoc_thm 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"; +> adhoc_thm 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)) "3 =!= 3"; +> val (thmid, thm) = the (adhoc_thm 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 (adhoc_thm 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 (adhoc_thm 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 (adhoc_thm 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 (adhoc_thm 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 = "HOL.True" : cterm +-------------------------- +*) +