1.1 --- a/src/Tools/isac/Build_Isac.thy Sun Feb 25 14:02:42 2018 +0100
1.2 +++ b/src/Tools/isac/Build_Isac.thy Sun Feb 25 16:31:17 2018 +0100
1.3 @@ -103,6 +103,7 @@
1.4 *}
1.5 (*==============================================================================================*)
1.6
1.7 +ML {* Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *) *}
1.8 ML {* Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *) *}
1.9 ML {* LTool.is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
1.10 ML {* Math_Engine.me; (*from "Interpret/mathengine.sml"*) *}
2.1 --- a/src/Tools/isac/calcelems.sml Sun Feb 25 14:02:42 2018 +0100
2.2 +++ b/src/Tools/isac/calcelems.sml Sun Feb 25 16:31:17 2018 +0100
2.3 @@ -242,6 +242,13 @@
2.4 However, we leave theory identifiers short, in particular in use as keys into KEStore. *)
2.5 fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)
2.6
2.7 +fun thm2str thm =
2.8 + let
2.9 + val t = Thm.prop_of thm
2.10 + val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac"))
2.11 + val ctxt' = Config.put show_markup false ctxt
2.12 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
2.13 +
2.14 fun term_to_string' ctxt t =
2.15 let
2.16 val ctxt' = Config.put show_markup false ctxt
3.1 --- a/test/Tools/isac/ProgLang/calculate.sml Sun Feb 25 14:02:42 2018 +0100
3.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Sun Feb 25 16:31:17 2018 +0100
3.3 @@ -328,183 +328,95 @@
3.4 "----------- fun get_pair: examples ------------------------------------------------------------";
3.5 "----------- fun get_pair: examples ------------------------------------------------------------";
3.6 "----------- fun get_pair: examples ------------------------------------------------------------";
3.7 - (*
3.8 -> val t = (Thm.term_of o the o (parse thy)) "#3 + #4";
3.9 -> val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));
3.10 -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
3.11 -> term2str t';
3.12 -> atomty t';
3.13 ->
3.14 -> val t = (Thm.term_of o the o (parse thy)) "(a + #3) + #4";
3.15 -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
3.16 -> term2str t';
3.17 ->
3.18 -> val t = (Thm.term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
3.19 -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
3.20 -> term2str t';
3.21 ->
3.22 -> val t = (Thm.term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
3.23 -> atomty t;
3.24 -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
3.25 -> term2str t';
3.26 -> val it = "#3 + (#4 + a) = #7 + a" : string
3.27 ->
3.28 ->
3.29 -> val t = (Thm.term_of o the o (parse thy)) "#-4//#-2";
3.30 -> val eval_fn = the (assoc (!eval_list, "cancel"));
3.31 -> val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
3.32 -> term2str t';
3.33 ->
3.34 -> val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
3.35 -> eval_binop "xxx" "pow" t thy;
3.36 -> val eval_fn = (eval_binop "xxx")
3.37 -> : string -> term -> theory -> (string * term) option;
3.38 -> val SOME (id,t') = get_pair thy "pow" eval_fn t;
3.39 -> term2str t';
3.40 -> val eval_fn = the (assoc (!eval_list, "pow"));
3.41 -> val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
3.42 -> term2str t';
3.43 ->
3.44 -> val t = (Thm.term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
3.45 -> val eval_fn = the (assoc (!eval_list, "Groups.times_class.times"));
3.46 -> val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t;
3.47 -> term2str t';
3.48 ->
3.49 -> val t = (Thm.term_of o the o (parse thy)) "#0 < #4";
3.50 -> val eval_fn = the (assoc (!eval_list, "Orderings.ord_class.less"));
3.51 -> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
3.52 -> term2str t';
3.53 -> val t = (Thm.term_of o the o (parse thy)) "#0 < #-4";
3.54 -> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
3.55 -> term2str t';
3.56 ->
3.57 -> val t = (Thm.term_of o the o (parse thy)) "#3 is_const";
3.58 -> val eval_fn = the (assoc (!eval_list, "is'_const"));
3.59 -> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
3.60 -> term2str t';
3.61 -> val t = (Thm.term_of o the o (parse thy)) "a is_const";
3.62 -> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
3.63 -> term2str t';
3.64 ->
3.65 -> val t = (Thm.term_of o the o (parse thy)) "#6//(#8::real)";
3.66 -> val eval_fn = the (assoc (!eval_list, "cancel"));
3.67 -> val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
3.68 -> term2str t';
3.69 ->
3.70 -> val t = (Thm.term_of o the o (parse thy)) "sqrt #12";
3.71 -> val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt"));
3.72 -> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
3.73 -> term2str t';
3.74 -> val it = "sqrt #12 = #2 * sqrt #3 " : string
3.75 ->
3.76 -> val t = (Thm.term_of o the o (parse thy)) "sqrt #9";
3.77 -> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
3.78 -> term2str t';
3.79 ->
3.80 -> val t = (Thm.term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";
3.81 -> val eval_fn = the (assoc (!eval_list, "Tools.Nth"));
3.82 -> val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;
3.83 -> term2str t';
3.84 -*)
3.85 +val thy = @{theory};
3.86 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
3.87 +
3.88 +val t = (Thm.term_of o the o (parse thy)) "3 + 4";
3.89 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
3.90 +if str = "#: 3 + 4 = 7" andalso term2str term = "3 + 4 = 7"
3.91 +then () else error "get_pair 3 + 4 changed";
3.92 +
3.93 +val t = (Thm.term_of o the o (parse thy)) "(a + 3) + 4";
3.94 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
3.95 +if str = "#: a + 3 + 4 = a + 7" andalso term2str term = "a + 3 + 4 = a + 7"
3.96 +then () else error "get_pair (a + 3) + 4 changed";
3.97 +
3.98 +val t = (Thm.term_of o the o (parse thy)) "(a + 3) + 4";
3.99 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
3.100 +if str = "#: a + 3 + 4 = a + 7" andalso term2str term = "a + 3 + 4 = a + 7"
3.101 +then () else error "get_pair (a + 3) + 4 changed";
3.102 +
3.103 +val t = (Thm.term_of o the o (parse thy)) "x = 5 * (3 + (4 + a))";
3.104 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
3.105 +if str = "#: 3 + (4 + a) = 7 + a" andalso term2str term = "3 + (4 + a) = 7 + a"
3.106 +then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed";
3.107 +
3.108 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
3.109 +
3.110 +val t = (Thm.term_of o the o (parse thy)) "-4 / -2";
3.111 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
3.112 +if str = "#divide_e-4_-2" andalso term2str term = "-4 / -2 = 2"
3.113 +then () else error "get_pair -4 / -2 changed";
3.114 +
3.115 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
3.116 +
3.117 +val t = (Thm.term_of o the o (parse thy)) "2 ^^^ 3";
3.118 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
3.119 +if str = "#: 2 ^^^ 3 = 8" andalso term2str term = "2 ^^^ 3 = 8"
3.120 +then () else error "get_pair 2 ^^^ 3 changed";
3.121 +
3.122 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
3.123 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
3.124 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
3.125 -(*
3.126 -> val ct = (the o (parse thy)) "#9 is_const";
3.127 -> adhoc_thm thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
3.128 -val it = SOME ("is_const9_","(is_const 9 ) = True [(is_const 9 ) = True]")
3.129 +(*--------------------------------------------------------------------vvvvvvvvvv*)
3.130 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "is_const");
3.131 +val SOME t = parseNEW @{context} "9 is_const";
3.132 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
3.133 +if str = "#is_const_9_" andalso thm2str thm = "(9 is_const) = True"
3.134 +then () else error "adhoc_thm 9 is_const changed";
3.135
3.136 -> val ct = (the o (parse thy)) "sqrt #9";
3.137 -> adhoc_thm thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;
3.138 -val it = SOME ("sqrt_9_","sqrt 9 = 3 [sqrt 9 = 3]") : (string * thm) option
3.139
3.140 -> val ct = (the o (parse thy)) "#4<#4";
3.141 -> 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.142 +case assoc_calc thy "Orderings.ord_class.less" of
3.143 + "le" => () | _ => error "Orderings.ord_class.less <-> le changed";
3.144 +(*--------------------------------------------------------------------vvvvvvvvvv*)
3.145 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "le");
3.146
3.147 -val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]")
3.148 +val SOME t = parseNEW @{context} "4 < 4";
3.149 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
3.150 +if str = "#less_4_4" andalso thm2str thm = "(4 < 4) = False"
3.151 +then () else error "adhoc_thm 4 < 4 changed";
3.152
3.153 -> val ct = (the o (parse thy)) "a<#4";
3.154 -> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;
3.155 -val it = NONE : (string * thm) option
3.156 +val SOME t = parseNEW @{context} "a < 4";
3.157 +case adhoc_thm thy (isa_str, eval_fn) t of
3.158 +NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE";
3.159
3.160 -> val ct = (the o (parse thy)) "#5<=#4";
3.161 -> adhoc_thm thy ("Orderings.ord_class.less_eq",the (assoc(!eval_list,"Orderings.ord_class.less_eq"))) ct;
3.162 -val it = SOME ("less_equal_5_4","(5 <= 4) = False [(5 <= 4) = False]")
3.163
3.164 --------------------------------------------------------------------6.8.02:
3.165 - val thy = SqRoot.thy;
3.166 - val t = (Thm.term_of o the o (parse thy)) "1+2";
3.167 - adhoc_thm thy (the(assoc(!calc_list,"PLUS"))) t;
3.168 - val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
3.169 --------------------------------------------------------------------6.8.02:
3.170 - val t = (Thm.term_of o the o (parse thy)) "-1";
3.171 - atomty t;
3.172 - val t = (Thm.term_of o the o (parse thy)) "0";
3.173 - atomty t;
3.174 - val t = (Thm.term_of o the o (parse thy)) "1";
3.175 - atomty t;
3.176 - val t = (Thm.term_of o the o (parse thy)) "2";
3.177 - atomty t;
3.178 - val t = (Thm.term_of o the o (parse thy)) "999999999";
3.179 - atomty t;
3.180 --------------------------------------------------------------------6.8.02:
3.181 +(*--------------------------------------------------------------------vvvvvvvvvv*)
3.182 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
3.183 +val SOME t = parseNEW @{context} "1 + 2";
3.184 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
3.185 +if str = "#: 1 + 2 = 3" andalso thm2str thm = "1 + 2 = 3"
3.186 +then () else error "adhoc_thm 1 + 2 changed";
3.187
3.188 -> val ct = (the o (parse thy)) "a+#3+#4";
3.189 -> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
3.190 -val it = SOME ("add_3_4","a + 3 + 4 = a + 7 [a + 3 + 4 = a + 7]")
3.191 -
3.192 -> val ct = (the o (parse thy)) "#3+(#4+a)";
3.193 -> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
3.194 -val it = SOME ("add_3_4","3 + (4 + a) = 7 + a [3 + (4 + a) = 7 + a]")
3.195 -
3.196 -> val ct = (the o (parse thy)) "a+(#3+#4)+#5";
3.197 -> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
3.198 -val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
3.199 +(*--------------------------------------------------------------------vvvvvvvvvv*)
3.200 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
3.201 +val SOME t = parseNEW @{context} "6 / -8";
3.202 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
3.203 +if str = "#divide_e6_-8" andalso thm2str thm = "6 / -8 = -3 / 4"
3.204 +then () else error "adhoc_thm 1 + 2 changed";
3.205
3.206 -> val ct = (the o (parse thy)) "#3*(#4*a)";
3.207 -> adhoc_thm thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) ct;
3.208 -val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a [3 * (4 * a) = 12 * a]")
3.209
3.210 -> val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";
3.211 -> adhoc_thm thy ("pow",the (assoc(!eval_list,"pow"))) ct;
3.212 -val it = SOME ("4_(+2)","4 ^ 2 = 16 [4 ^ 2 = 16]") : (string * thm) option
3.213 +case assoc_calc thy "Atools.ident" of
3.214 + "ident" => () | _ => error "Atools.ident <-> ident changed";
3.215 +(*--------------------------------------------------------------------vvvvvvvvvv*)
3.216 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "ident");
3.217
3.218 -> val ct = (the o (parse thy)) "#-4//#-2";
3.219 -> adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
3.220 -val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2) [(-4) // (-2) = (+2)]")
3.221 +val SOME t = parseNEW @{context} "3 =!= 3";
3.222 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
3.223 +if str = "#ident_(3)_(3)" andalso thm2str thm = "(3 =!= 3) = True"
3.224 +then () else error "adhoc_thm (3 =!= 3) changed";
3.225
3.226 -> val ct = (the o (parse thy)) "#6//#-8";
3.227 -> adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
3.228 -val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4 [6 // (-8) = (-3) // 4]")
3.229 -
3.230 -*)
3.231 -
3.232 -(*
3.233 ---------------------------
3.234 -> val ct = (the o (parse thy)) "3 =!= 3";
3.235 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.236 -val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
3.237 -
3.238 -> val ct = (the o (parse thy)) "~ (3 =!= 3)";
3.239 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.240 -val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
3.241 -
3.242 -> val ct = (the o (parse thy)) "3 =!= 4";
3.243 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.244 -val thm = "(3 =!= 4) = False [(3 =!= 4) = False]" : thm
3.245 -
3.246 -> val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))";
3.247 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.248 - "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
3.249 -
3.250 -> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
3.251 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
3.252 - "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
3.253 -
3.254 -> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
3.255 -> val rls = eval_rls;
3.256 -> val (ct,_) = the (rewrite_set_ thy false rls ct);
3.257 -val ct = "HOL.True" : cterm
3.258 ---------------------------
3.259 -*)
3.260 -
3.261 +val SOME t = parseNEW @{context} "\<not> (4 + (4 * x + x ^ 2) =!= 0)";
3.262 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
3.263 +if str = "#ident_(4 + (4 * x + x ^ 2))_(0)" andalso thm2str thm = "(4 + (4 * x + x ^ 2) =!= 0) = False"
3.264 +then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
4.1 --- a/test/Tools/isac/Test_Isac.thy Sun Feb 25 14:02:42 2018 +0100
4.2 +++ b/test/Tools/isac/Test_Isac.thy Sun Feb 25 16:31:17 2018 +0100
4.3 @@ -74,6 +74,9 @@
4.4 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
4.5 "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
4.6 "~~/test/Tools/isac/ProgLang/calculate" (* setup for calculate.sml*)
4.7 +
4.8 +
4.9 +
4.10 "~~/test/Tools/isac/ProgLang/scrtools" (* setup for scrtools.sml *)
4.11 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
4.12 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
4.13 @@ -104,6 +107,7 @@
4.14 open Model; (* NONE *)
4.15 open LTool; rule2stac;
4.16 open Rewrite; mk_thm;
4.17 + open Calc; get_pair;
4.18 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.19 *}
4.20
4.21 @@ -133,8 +137,8 @@
4.22 ML_file "library.sml"
4.23 ML_file "calcelems.sml"
4.24 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
4.25 + ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
4.26 ML_file "kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
4.27 - ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
4.28 ML_file "ProgLang/termC.sml"
4.29 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
4.30 ML_file "ProgLang/rewrite.sml"