1.1 --- a/test/Tools/isac/ProgLang/calculate.sml Sun Feb 25 14:02:42 2018 +0100
1.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Sun Feb 25 16:31:17 2018 +0100
1.3 @@ -328,183 +328,95 @@
1.4 "----------- fun get_pair: examples ------------------------------------------------------------";
1.5 "----------- fun get_pair: examples ------------------------------------------------------------";
1.6 "----------- fun get_pair: examples ------------------------------------------------------------";
1.7 - (*
1.8 -> val t = (Thm.term_of o the o (parse thy)) "#3 + #4";
1.9 -> val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));
1.10 -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
1.11 -> term2str t';
1.12 -> atomty t';
1.13 ->
1.14 -> val t = (Thm.term_of o the o (parse thy)) "(a + #3) + #4";
1.15 -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
1.16 -> term2str t';
1.17 ->
1.18 -> val t = (Thm.term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
1.19 -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
1.20 -> term2str t';
1.21 ->
1.22 -> val t = (Thm.term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
1.23 -> atomty t;
1.24 -> val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
1.25 -> term2str t';
1.26 -> val it = "#3 + (#4 + a) = #7 + a" : string
1.27 ->
1.28 ->
1.29 -> val t = (Thm.term_of o the o (parse thy)) "#-4//#-2";
1.30 -> val eval_fn = the (assoc (!eval_list, "cancel"));
1.31 -> val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
1.32 -> term2str t';
1.33 ->
1.34 -> val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
1.35 -> eval_binop "xxx" "pow" t thy;
1.36 -> val eval_fn = (eval_binop "xxx")
1.37 -> : string -> term -> theory -> (string * term) option;
1.38 -> val SOME (id,t') = get_pair thy "pow" eval_fn t;
1.39 -> term2str t';
1.40 -> val eval_fn = the (assoc (!eval_list, "pow"));
1.41 -> val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
1.42 -> term2str t';
1.43 ->
1.44 -> val t = (Thm.term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
1.45 -> val eval_fn = the (assoc (!eval_list, "Groups.times_class.times"));
1.46 -> val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t;
1.47 -> term2str t';
1.48 ->
1.49 -> val t = (Thm.term_of o the o (parse thy)) "#0 < #4";
1.50 -> val eval_fn = the (assoc (!eval_list, "Orderings.ord_class.less"));
1.51 -> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
1.52 -> term2str t';
1.53 -> val t = (Thm.term_of o the o (parse thy)) "#0 < #-4";
1.54 -> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
1.55 -> term2str t';
1.56 ->
1.57 -> val t = (Thm.term_of o the o (parse thy)) "#3 is_const";
1.58 -> val eval_fn = the (assoc (!eval_list, "is'_const"));
1.59 -> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
1.60 -> term2str t';
1.61 -> val t = (Thm.term_of o the o (parse thy)) "a is_const";
1.62 -> val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
1.63 -> term2str t';
1.64 ->
1.65 -> val t = (Thm.term_of o the o (parse thy)) "#6//(#8::real)";
1.66 -> val eval_fn = the (assoc (!eval_list, "cancel"));
1.67 -> val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
1.68 -> term2str t';
1.69 ->
1.70 -> val t = (Thm.term_of o the o (parse thy)) "sqrt #12";
1.71 -> val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt"));
1.72 -> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
1.73 -> term2str t';
1.74 -> val it = "sqrt #12 = #2 * sqrt #3 " : string
1.75 ->
1.76 -> val t = (Thm.term_of o the o (parse thy)) "sqrt #9";
1.77 -> val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
1.78 -> term2str t';
1.79 ->
1.80 -> val t = (Thm.term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";
1.81 -> val eval_fn = the (assoc (!eval_list, "Tools.Nth"));
1.82 -> val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;
1.83 -> term2str t';
1.84 -*)
1.85 +val thy = @{theory};
1.86 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
1.87 +
1.88 +val t = (Thm.term_of o the o (parse thy)) "3 + 4";
1.89 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.90 +if str = "#: 3 + 4 = 7" andalso term2str term = "3 + 4 = 7"
1.91 +then () else error "get_pair 3 + 4 changed";
1.92 +
1.93 +val t = (Thm.term_of o the o (parse thy)) "(a + 3) + 4";
1.94 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.95 +if str = "#: a + 3 + 4 = a + 7" andalso term2str term = "a + 3 + 4 = a + 7"
1.96 +then () else error "get_pair (a + 3) + 4 changed";
1.97 +
1.98 +val t = (Thm.term_of o the o (parse thy)) "(a + 3) + 4";
1.99 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.100 +if str = "#: a + 3 + 4 = a + 7" andalso term2str term = "a + 3 + 4 = a + 7"
1.101 +then () else error "get_pair (a + 3) + 4 changed";
1.102 +
1.103 +val t = (Thm.term_of o the o (parse thy)) "x = 5 * (3 + (4 + a))";
1.104 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.105 +if str = "#: 3 + (4 + a) = 7 + a" andalso term2str term = "3 + (4 + a) = 7 + a"
1.106 +then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed";
1.107 +
1.108 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
1.109 +
1.110 +val t = (Thm.term_of o the o (parse thy)) "-4 / -2";
1.111 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.112 +if str = "#divide_e-4_-2" andalso term2str term = "-4 / -2 = 2"
1.113 +then () else error "get_pair -4 / -2 changed";
1.114 +
1.115 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
1.116 +
1.117 +val t = (Thm.term_of o the o (parse thy)) "2 ^^^ 3";
1.118 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.119 +if str = "#: 2 ^^^ 3 = 8" andalso term2str term = "2 ^^^ 3 = 8"
1.120 +then () else error "get_pair 2 ^^^ 3 changed";
1.121 +
1.122 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
1.123 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
1.124 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
1.125 -(*
1.126 -> val ct = (the o (parse thy)) "#9 is_const";
1.127 -> adhoc_thm thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
1.128 -val it = SOME ("is_const9_","(is_const 9 ) = True [(is_const 9 ) = True]")
1.129 +(*--------------------------------------------------------------------vvvvvvvvvv*)
1.130 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "is_const");
1.131 +val SOME t = parseNEW @{context} "9 is_const";
1.132 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.133 +if str = "#is_const_9_" andalso thm2str thm = "(9 is_const) = True"
1.134 +then () else error "adhoc_thm 9 is_const changed";
1.135
1.136 -> val ct = (the o (parse thy)) "sqrt #9";
1.137 -> adhoc_thm thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;
1.138 -val it = SOME ("sqrt_9_","sqrt 9 = 3 [sqrt 9 = 3]") : (string * thm) option
1.139
1.140 -> val ct = (the o (parse thy)) "#4<#4";
1.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 = "#";
1.142 +case assoc_calc thy "Orderings.ord_class.less" of
1.143 + "le" => () | _ => error "Orderings.ord_class.less <-> le changed";
1.144 +(*--------------------------------------------------------------------vvvvvvvvvv*)
1.145 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "le");
1.146
1.147 -val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]")
1.148 +val SOME t = parseNEW @{context} "4 < 4";
1.149 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.150 +if str = "#less_4_4" andalso thm2str thm = "(4 < 4) = False"
1.151 +then () else error "adhoc_thm 4 < 4 changed";
1.152
1.153 -> val ct = (the o (parse thy)) "a<#4";
1.154 -> adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;
1.155 -val it = NONE : (string * thm) option
1.156 +val SOME t = parseNEW @{context} "a < 4";
1.157 +case adhoc_thm thy (isa_str, eval_fn) t of
1.158 +NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE";
1.159
1.160 -> val ct = (the o (parse thy)) "#5<=#4";
1.161 -> adhoc_thm thy ("Orderings.ord_class.less_eq",the (assoc(!eval_list,"Orderings.ord_class.less_eq"))) ct;
1.162 -val it = SOME ("less_equal_5_4","(5 <= 4) = False [(5 <= 4) = False]")
1.163
1.164 --------------------------------------------------------------------6.8.02:
1.165 - val thy = SqRoot.thy;
1.166 - val t = (Thm.term_of o the o (parse thy)) "1+2";
1.167 - adhoc_thm thy (the(assoc(!calc_list,"PLUS"))) t;
1.168 - val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
1.169 --------------------------------------------------------------------6.8.02:
1.170 - val t = (Thm.term_of o the o (parse thy)) "-1";
1.171 - atomty t;
1.172 - val t = (Thm.term_of o the o (parse thy)) "0";
1.173 - atomty t;
1.174 - val t = (Thm.term_of o the o (parse thy)) "1";
1.175 - atomty t;
1.176 - val t = (Thm.term_of o the o (parse thy)) "2";
1.177 - atomty t;
1.178 - val t = (Thm.term_of o the o (parse thy)) "999999999";
1.179 - atomty t;
1.180 --------------------------------------------------------------------6.8.02:
1.181 +(*--------------------------------------------------------------------vvvvvvvvvv*)
1.182 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
1.183 +val SOME t = parseNEW @{context} "1 + 2";
1.184 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.185 +if str = "#: 1 + 2 = 3" andalso thm2str thm = "1 + 2 = 3"
1.186 +then () else error "adhoc_thm 1 + 2 changed";
1.187
1.188 -> val ct = (the o (parse thy)) "a+#3+#4";
1.189 -> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
1.190 -val it = SOME ("add_3_4","a + 3 + 4 = a + 7 [a + 3 + 4 = a + 7]")
1.191 -
1.192 -> val ct = (the o (parse thy)) "#3+(#4+a)";
1.193 -> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
1.194 -val it = SOME ("add_3_4","3 + (4 + a) = 7 + a [3 + (4 + a) = 7 + a]")
1.195 -
1.196 -> val ct = (the o (parse thy)) "a+(#3+#4)+#5";
1.197 -> adhoc_thm thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
1.198 -val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
1.199 +(*--------------------------------------------------------------------vvvvvvvvvv*)
1.200 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
1.201 +val SOME t = parseNEW @{context} "6 / -8";
1.202 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.203 +if str = "#divide_e6_-8" andalso thm2str thm = "6 / -8 = -3 / 4"
1.204 +then () else error "adhoc_thm 1 + 2 changed";
1.205
1.206 -> val ct = (the o (parse thy)) "#3*(#4*a)";
1.207 -> adhoc_thm thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) ct;
1.208 -val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a [3 * (4 * a) = 12 * a]")
1.209
1.210 -> val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";
1.211 -> adhoc_thm thy ("pow",the (assoc(!eval_list,"pow"))) ct;
1.212 -val it = SOME ("4_(+2)","4 ^ 2 = 16 [4 ^ 2 = 16]") : (string * thm) option
1.213 +case assoc_calc thy "Atools.ident" of
1.214 + "ident" => () | _ => error "Atools.ident <-> ident changed";
1.215 +(*--------------------------------------------------------------------vvvvvvvvvv*)
1.216 +val SOME (isa_str, eval_fn) = assoc (KEStore_Elems.get_calcs @{theory}, "ident");
1.217
1.218 -> val ct = (the o (parse thy)) "#-4//#-2";
1.219 -> adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
1.220 -val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2) [(-4) // (-2) = (+2)]")
1.221 +val SOME t = parseNEW @{context} "3 =!= 3";
1.222 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.223 +if str = "#ident_(3)_(3)" andalso thm2str thm = "(3 =!= 3) = True"
1.224 +then () else error "adhoc_thm (3 =!= 3) changed";
1.225
1.226 -> val ct = (the o (parse thy)) "#6//#-8";
1.227 -> adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
1.228 -val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4 [6 // (-8) = (-3) // 4]")
1.229 -
1.230 -*)
1.231 -
1.232 -(*
1.233 ---------------------------
1.234 -> val ct = (the o (parse thy)) "3 =!= 3";
1.235 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
1.236 -val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
1.237 -
1.238 -> val ct = (the o (parse thy)) "~ (3 =!= 3)";
1.239 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
1.240 -val thm = "(3 =!= 3) = True [(3 =!= 3) = True]" : thm
1.241 -
1.242 -> val ct = (the o (parse thy)) "3 =!= 4";
1.243 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
1.244 -val thm = "(3 =!= 4) = False [(3 =!= 4) = False]" : thm
1.245 -
1.246 -> val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))";
1.247 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
1.248 - "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
1.249 -
1.250 -> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
1.251 -> val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
1.252 - "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
1.253 -
1.254 -> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
1.255 -> val rls = eval_rls;
1.256 -> val (ct,_) = the (rewrite_set_ thy false rls ct);
1.257 -val ct = "HOL.True" : cterm
1.258 ---------------------------
1.259 -*)
1.260 -
1.261 +val SOME t = parseNEW @{context} "\<not> (4 + (4 * x + x ^ 2) =!= 0)";
1.262 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.263 +if str = "#ident_(4 + (4 * x + x ^ 2))_(0)" andalso thm2str thm = "(4 + (4 * x + x ^ 2) =!= 0) = False"
1.264 +then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";