1.1 --- a/src/Tools/isac/Interpret/rewtools.sml Thu Oct 27 09:53:54 2016 +0200
1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Oct 27 10:48:10 2016 +0200
1.3 @@ -135,7 +135,7 @@
1.4 val _ = if not (! trace_rewrite) then () else tracing ("### trying calc. \"" ^ op_^"\"")
1.5 val t = uminus_to_string t
1.6 in
1.7 - case get_calculation_ thy c t of
1.8 + case adhoc_thm thy c t of
1.9 NONE => rew_once lim rts t apno rs'
1.10 | SOME (thmid, tm) =>
1.11 (let
1.12 @@ -545,11 +545,11 @@
1.13 SOME (f',_) => [rule2tac thy [] thm']
1.14 | NONE => [])
1.15 | try_rew thy _ _ _ f (cal as Calc c) =
1.16 - (case get_calculation_ thy c f of
1.17 + (case adhoc_thm thy c f of
1.18 SOME (str, _) => [rule2tac thy [] cal]
1.19 | NONE => [])
1.20 | try_rew thy _ _ _ f (cal as Cal1 c) =
1.21 - (case get_calculation_ thy c f of
1.22 + (case adhoc_thm thy c f of
1.23 SOME (str, _) => [rule2tac thy [] cal]
1.24 | NONE => [])
1.25 | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
2.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Thu Oct 27 09:53:54 2016 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Thu Oct 27 10:48:10 2016 +0200
2.3 @@ -200,7 +200,7 @@
2.4 | SOME (ct',asm') =>
2.5 rew_once ruls (asm union asm') ct' Appl (rul::thms))
2.6 | Calc (cc as (op_,_)) =>
2.7 - (case get_calculation_ thy cc ct of
2.8 + (case adhoc_thm thy cc ct of
2.9 NONE => rew_once ruls asm ct apno thms
2.10 | SOME (thmid, thm') =>
2.11 let
2.12 @@ -236,7 +236,7 @@
2.13 | SOME (ct',asm') =>
2.14 rew_once ruls (asm union asm') ct' Appl (rul::thms))
2.15 | Calc (cc as (op_,_)) =>
2.16 - (case get_calculation_ thy cc ct of
2.17 + (case adhoc_thm thy cc ct of
2.18 NONE => rew_once ruls asm ct apno thms
2.19 | SOME (thmid, thm') =>
2.20 let
3.1 --- a/src/Tools/isac/ProgLang/calculate.sml Thu Oct 27 09:53:54 2016 +0200
3.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Thu Oct 27 10:48:10 2016 +0200
3.3 @@ -182,43 +182,43 @@
3.4 *)
3.5
3.6 (* val ((op_, eval_fn),ct)=(cc,pre);
3.7 - (get_calculation_ (Thy_Info.get_theory "Isac") (op_, eval_fn) ct) handle e => print_exn e;
3.8 + (adhoc_thm (Thy_Info.get_theory "Isac") (op_, eval_fn) ct) handle e => print_exn e;
3.9 parse thy ""
3.10 *)
3.11 (*.get a thm from an op_ somewhere in the term;
3.12 apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711).*)
3.13 -fun get_calculation_ thy (op_, eval_fn) ct =
3.14 +fun adhoc_thm thy (op_, eval_fn) ct =
3.15 case get_pair thy op_ eval_fn ct of
3.16 - NONE => ((* tracing ("@@@ get_calculation: NONE, op_= " ^ op_);
3.17 - tracing ("@@@ get_calculation: ct= "); atomty ct; *)
3.18 + NONE => ((* tracing ("@@@ adhoc_thm: NONE, op_= " ^ op_);
3.19 + tracing ("@@@ adhoc_thm: ct= "); atomty ct; *)
3.20 NONE)
3.21 | SOME (thmid, t) => SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of thy)) t);
3.22 (*
3.23 > val ct = (the o (parse thy)) "#9 is_const";
3.24 -> get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
3.25 +> adhoc_thm thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
3.26 val it = SOME ("is_const9_","(is_const 9 ) = True [(is_const 9 ) = True]")
3.27
3.28 > val ct = (the o (parse thy)) "sqrt #9";
3.29 -> get_calculation_ thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;
3.30 +> adhoc_thm thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;
3.31 val it = SOME ("sqrt_9_","sqrt 9 = 3 [sqrt 9 = 3]") : (string * thm) option
3.32
3.33 > val ct = (the o (parse thy)) "#4<#4";
3.34 -> get_calculation_ thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o Symbol.explode) str = "#";
3.35 +> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o Symbol.explode) str = "#";
3.36
3.37 val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]")
3.38
3.39 > val ct = (the o (parse thy)) "a<#4";
3.40 -> get_calculation_ thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;
3.41 +> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;
3.42 val it = NONE : (string * thm) option
3.43
3.44 > val ct = (the o (parse thy)) "#5<=#4";
3.45 -> get_calculation_ thy ("Orderings.ord_class.less_eq",the (assoc(!eval_list,"Orderings.ord_class.less_eq"))) ct;
3.46 +> adhoc_thm thy ("Orderings.ord_class.less_eq",the (assoc(!eval_list,"Orderings.ord_class.less_eq"))) ct;
3.47 val it = SOME ("less_equal_5_4","(5 <= 4) = False [(5 <= 4) = False]")
3.48
3.49 -------------------------------------------------------------------6.8.02:
3.50 val thy = SqRoot.thy;
3.51 val t = (Thm.term_of o the o (parse thy)) "1+2";
3.52 - get_calculation_ thy (the(assoc(!calc_list,"PLUS"))) t;
3.53 + adhoc_thm thy (the(assoc(!calc_list,"PLUS"))) t;
3.54 val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
3.55 -------------------------------------------------------------------6.8.02:
3.56 val t = (Thm.term_of o the o (parse thy)) "-1";
3.57 @@ -234,31 +234,31 @@
3.58 -------------------------------------------------------------------6.8.02:
3.59
3.60 > val ct = (the o (parse thy)) "a+#3+#4";
3.61 -> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
3.62 +> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
3.63 val it = SOME ("add_3_4","a + 3 + 4 = a + 7 [a + 3 + 4 = a + 7]")
3.64
3.65 > val ct = (the o (parse thy)) "#3+(#4+a)";
3.66 -> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
3.67 +> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
3.68 val it = SOME ("add_3_4","3 + (4 + a) = 7 + a [3 + (4 + a) = 7 + a]")
3.69
3.70 > val ct = (the o (parse thy)) "a+(#3+#4)+#5";
3.71 -> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
3.72 +> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
3.73 val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
3.74
3.75 > val ct = (the o (parse thy)) "#3*(#4*a)";
3.76 -> get_calculation_ thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) ct;
3.77 +> adhoc_thm thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) ct;
3.78 val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a [3 * (4 * a) = 12 * a]")
3.79
3.80 > val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";
3.81 -> get_calculation_ thy ("pow",the (assoc(!eval_list,"pow"))) ct;
3.82 +> adhoc_thm thy ("pow",the (assoc(!eval_list,"pow"))) ct;
3.83 val it = SOME ("4_(+2)","4 ^ 2 = 16 [4 ^ 2 = 16]") : (string * thm) option
3.84
3.85 > val ct = (the o (parse thy)) "#-4//#-2";
3.86 -> get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
3.87 +> adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
3.88 val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2) [(-4) // (-2) = (+2)]")
3.89
3.90 > val ct = (the o (parse thy)) "#6//#-8";
3.91 -> get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
3.92 +> adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
3.93 val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4 [6 // (-8) = (-3) // 4]")
3.94
3.95 *)
3.96 @@ -271,23 +271,23 @@
3.97
3.98 --------------------------
3.99 > val ct = (the o (parse thy)) "3 =!= 3";
3.100 -> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
3.101 +> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.102 val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
3.103
3.104 > val ct = (the o (parse thy)) "~ (3 =!= 3)";
3.105 -> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
3.106 +> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.107 val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
3.108
3.109 > val ct = (the o (parse thy)) "3 =!= 4";
3.110 -> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
3.111 +> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.112 val thm = "(3 =!= 4) = False [(3 =!= 4) = False]" : thm
3.113
3.114 > val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))";
3.115 -> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
3.116 +> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.117 "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
3.118
3.119 > val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
3.120 -> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
3.121 +> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.122 "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
3.123
3.124 > val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
3.125 @@ -303,7 +303,7 @@
3.126 (* val (thy, (op_, eval_fn), ct) =
3.127 (thy, ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"), term);
3.128 *)
3.129 -fun get_calculation1_ thy ((op_, eval_fn):cal) ct =
3.130 +fun adhoc_thm1_ thy ((op_, eval_fn):cal) ct =
3.131 case eval_fn op_ ct thy of
3.132 NONE => NONE
3.133 | SOME (thmid,t) =>
4.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Thu Oct 27 09:53:54 2016 +0200
4.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Thu Oct 27 10:48:10 2016 +0200
4.3 @@ -161,7 +161,7 @@
4.4 | Calc (cc as (op_, _)) =>
4.5 let val _= trace1 i (" try calc: " ^ op_ ^ "'")
4.6 val ct = uminus_to_string ct
4.7 - in case get_calculation_ thy cc ct of
4.8 + in case adhoc_thm thy cc ct of
4.9 NONE => rew_once ruls asm ct apno thms
4.10 | SOME (thmid, thm') =>
4.11 let
4.12 @@ -175,7 +175,7 @@
4.13 | Cal1 (cc as (op_, _)) =>
4.14 let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
4.15 val ct = uminus_to_string ct
4.16 - in case get_calculation1_ thy cc ct of
4.17 + in case adhoc_thm1_ thy cc ct of
4.18 NONE => (ct, asm)
4.19 | SOME (thmid, thm') =>
4.20 let
4.21 @@ -297,7 +297,7 @@
4.22 (*. search ct for adjacent numerals and calculate them by operator isa_fn .*)
4.23 fun calculate_ thy isa_fn ct =
4.24 let val ct = uminus_to_string ct
4.25 - in case get_calculation_ thy isa_fn ct of
4.26 + in case adhoc_thm thy isa_fn ct of
4.27 NONE => NONE
4.28 | SOME (thmID, thm) =>
4.29 (let val SOME (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct
4.30 @@ -465,8 +465,8 @@
4.31 let val rew = rewrite_set_ thy false srls t;
4.32 in case rew of SOME (res,_) => res | NONE => t end;
4.33
4.34 -fun get_calculation' (thy:theory') op_ (ct:cterm') =
4.35 - case get_calculation_ (assoc_thy thy) op_
4.36 +fun adhoc_thm' (thy:theory') op_ (ct:cterm') =
4.37 + case adhoc_thm (assoc_thy thy) op_
4.38 ((uminus_to_string o Thm.term_of o the o
4.39 (parse (assoc_thy thy))) ct) of
4.40 NONE => NONE
5.1 --- a/src/Tools/isac/calcelems.sml Thu Oct 27 09:53:54 2016 +0200
5.2 +++ b/src/Tools/isac/calcelems.sml Thu Oct 27 10:48:10 2016 +0200
5.3 @@ -42,7 +42,7 @@
5.4 by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid.
5.5 * case 2 "sym_..": Global_Theory.get_thm..RS sym
5.6 * case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_:
5.7 - from applicable_in..Calculate: opstr --calculate_/get_calculation_--> (thmID, thm)
5.8 + from applicable_in..Calculate: opstr --calculate_/adhoc_thm--> (thmID, thm)
5.9 *)
5.10 type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *)
5.11 type rls' = string;
6.1 --- a/test/Tools/isac/Knowledge/diff.sml Thu Oct 27 09:53:54 2016 +0200
6.2 +++ b/test/Tools/isac/Knowledge/diff.sml Thu Oct 27 10:48:10 2016 +0200
6.3 @@ -144,7 +144,7 @@
6.4 term2str t';
6.5
6.6 val t = str2term "-1 * 1";
6.7 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
6.8 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"times"))) t;
6.9 *)
6.10
6.11 "----------- differentiate: me (*+ tacs input*) ---------";
7.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Thu Oct 27 09:53:54 2016 +0200
7.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Thu Oct 27 10:48:10 2016 +0200
7.3 @@ -36,10 +36,10 @@
7.4 val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst
7.5 (num_str @{thm "int_isolate_add"}) t; term2str t;
7.6
7.7 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;
7.8 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES"))) t;
7.9 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
7.10
7.11 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
7.12 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
7.13 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
7.14
7.15 "----------- mathengine with usecase1 -------------------";
7.16 @@ -71,10 +71,10 @@
7.17 SOME t' => t'
7.18 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
7.19
7.20 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;
7.21 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES"))) t;
7.22 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
7.23
7.24 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
7.25 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
7.26 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
7.27
7.28
8.1 --- a/test/Tools/isac/Knowledge/integrate.sml Thu Oct 27 09:53:54 2016 +0200
8.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Thu Oct 27 10:48:10 2016 +0200
8.3 @@ -107,7 +107,7 @@
8.4 else error "intergrate.sml: diff. eval_add_new_c";
8.5
8.6 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
8.7 -val SOME (thmstr, thm) = get_calculation1_ thy cc term;
8.8 +val SOME (thmstr, thm) = adhoc_thm1_ thy cc term;
8.9
8.10 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
8.11 if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then ()
9.1 --- a/test/Tools/isac/ProgLang/calculate.sml Thu Oct 27 09:53:54 2016 +0200
9.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Thu Oct 27 10:48:10 2016 +0200
9.3 @@ -11,7 +11,7 @@
9.4 "--------------------------------------------------------";
9.5 "-calculate.thy: provides 'setup' -----------------------";
9.6 "----------- fun norm -----------------------------------";
9.7 -"----------- check return value of get_calculation_ ----";
9.8 +"----------- check return value of adhoc_thm ----";
9.9 "----------- fun calculate_ -----------------------------";
9.10 "----------- fun calculate_ -----------------------------";
9.11 "----------- calculate from script --requires 'setup'----";
9.12 @@ -25,16 +25,16 @@
9.13 "--------------------------------------------------------";
9.14 "--------------------------------------------------------";
9.15
9.16 -"----------- check return value of get_calculation_ ----";
9.17 -"----------- check return value of get_calculation_ ----";
9.18 -"----------- check return value of get_calculation_ ----";
9.19 +"----------- check return value of adhoc_thm ----";
9.20 +"----------- check return value of adhoc_thm ----";
9.21 +"----------- check return value of adhoc_thm ----";
9.22 val thy = @{theory "Poly"};
9.23 val cal = snd (assoc_calc' thy "is_polyexp");
9.24 val t = @{term "(x / x) is_polyexp"};
9.25 -val SOME (thmID, thm) = get_calculation_ thy cal t;
9.26 +val SOME (thmID, thm) = adhoc_thm thy cal t;
9.27 (HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
9.28 handle TERM _ =>
9.29 - error "calculate.sml: get_calculation_ must return Trueprop";
9.30 + error "calculate.sml: adhoc_thm must return Trueprop";
9.31
9.32 "----------- fun calculate_ -----------------------------";
9.33 "----------- fun calculate_ -----------------------------";
9.34 @@ -42,30 +42,30 @@
9.35 val thy = @{theory "Test"};
9.36 "===== test 1";
9.37 val t = (Thm.term_of o the o (parse thy)) "1+2";
9.38 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
9.39 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
9.40 term2str (Thm.prop_of thm) = "1 + 2 = 3";
9.41
9.42 "===== test 2";
9.43 val t = (Thm.term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
9.44 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
9.45 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
9.46 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
9.47 if term2str t = "(3 * 4 / 3) ^^^ 2" then ()
9.48 else error "calculate.sml: ((1+2)*4/3)^^^2 --> (3 * 4 / 3) ^^^ 2";
9.49
9.50 "===== test 3b -- 2 contiued";
9.51 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;
9.52 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES"))) t;
9.53 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
9.54 term2str t;
9.55 (*val it = "(#12 // #3) ^^^ #2" : string*)
9.56
9.57 "===== test 4";
9.58 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
9.59 +val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"DIVIDE")))t;
9.60 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
9.61 term2str t;
9.62 (*it = "#4 ^^^ #2" : string*)
9.63
9.64 "===== test 5";
9.65 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER")))t;
9.66 +val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"POWER")))t;
9.67 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
9.68 (*show_types := false;*)
9.69 if term2str t <> "16" then error "calculate.sml: new behaviour in calculate_"
9.70 @@ -256,7 +256,7 @@
9.71 @@@ get_pair: then 1
9.72 @@@ get_pair: t -> NONE
9.73 @@@ get_pair: t1 -> NONE
9.74 -@@@ get_calculation: NONE
9.75 +@@@ adhoc_thm': NONE
9.76 ### trying calc. 'pow'
9.77 *)
9.78
9.79 @@ -273,7 +273,7 @@
9.80 @@@ get_pair: t else -> NONE
9.81 @@@ get_pair: binop, t = -4 / 2
9.82 @@@ get_pair: then 1
9.83 -@@@ get_calculation: SOME #cancel_-4_2
9.84 +@@@ adhoc_thm': SOME #cancel_-4_2
9.85 ### calc. to: x + (-2)
9.86 ### trying calc. 'cancel'
9.87 *)
9.88 @@ -303,32 +303,32 @@
9.89
9.90 val thy = @{theory Test};
9.91 val t = (Thm.term_of o the o (parse thy)) "12 / 3";
9.92 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
9.93 +val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"DIVIDE")))t;
9.94 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
9.95 "12 / 3 = 4";
9.96 val thy = @{theory Test};
9.97 val t = (Thm.term_of o the o (parse thy)) "4 ^^^ 2";
9.98 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER"))) t;
9.99 +val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"POWER"))) t;
9.100 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
9.101 "4 ^ 2 = 16";
9.102
9.103 val t = (Thm.term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
9.104 - val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
9.105 + val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
9.106 "1 + 2 = 3";
9.107 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
9.108 term2str t;
9.109 "(3 * 4 / 3) ^^^ 2";
9.110 - val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES")))t;
9.111 + val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES")))t;
9.112 "3 * 4 = 12";
9.113 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
9.114 term2str t;
9.115 "(12 / 3) ^^^ 2";
9.116 - val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
9.117 + val SOME (thmID,thm) =adhoc_thm thy(the(assoc(calclist,"DIVIDE")))t;
9.118 "12 / 3 = 4";
9.119 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
9.120 term2str t;
9.121 "4 ^^^ 2";
9.122 - val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER")))t;
9.123 + val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"POWER")))t;
9.124 "4 ^^^ 2 = 16";
9.125 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
9.126 term2str t;
9.127 @@ -339,7 +339,7 @@
9.128 (*13.9.02 *** calc: operator = pow not defined*)
9.129 val t = (Thm.term_of o the o (parse thy)) "3^^^2";
9.130 val SOME (thmID,thm) =
9.131 - get_calculation_ thy (the(assoc(calclist,"POWER"))) t;
9.132 + adhoc_thm thy (the(assoc(calclist,"POWER"))) t;
9.133 (*** calc: operator = pow not defined*)
9.134
9.135 val (op_, eval_fn) = the (assoc(calclist,"POWER"));