1.1 --- a/test/Tools/isac/Test_Isac.thy Fri Feb 09 11:45:53 2018 +0100
1.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Feb 09 11:57:24 2018 +0100
1.3 @@ -67,8 +67,8 @@
1.4 "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
1.5 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
1.6 "~~/test/Tools/isac/ProgLang/calculate" (* setup for calculate.sml*)
1.7 + "~~/test/Tools/isac/ProgLang/scrtools" (* setup for scrtools.sml *)
1.8 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
1.9 - "~~/test/Tools/isac/ProgLang/scrtools" (* setup for scrtools.sml *)
1.10 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
1.11
1.12 "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
1.13 @@ -127,422 +127,14 @@
1.14
1.15 ML {*
1.16 *} ML {*
1.17 -(* Title: test calculation of values for function constants
1.18 - Author: Walther Neuper 2000
1.19 - (c) copyright due to lincense terms.
1.20 -
1.21 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.22 - 10 20 30 40 50 60 70 80
1.23 -*)
1.24 -
1.25 -"--------------------------------------------------------";
1.26 -"table of contents --------------------------------------";
1.27 -"--------------------------------------------------------";
1.28 -"-calculate.thy: provides 'setup' -----------------------";
1.29 -"----------- fun norm -----------------------------------";
1.30 -"----------- check return value of adhoc_thm ----";
1.31 -"----------- fun calculate_ -----------------------------";
1.32 -"----------- calculate from script --requires 'setup'----";
1.33 -"----------- calculate check test-root-equ --------------";
1.34 -"----------- check calcul,ate bottom up -----------------";
1.35 -"----------- Atools.pow Power.power_class.power ---------";
1.36 -" ================= calculate.sml: calculate_ 2002 ======";
1.37 -"----------- get_pair with 3 args -----------------------";
1.38 -"----------- calculate (2 * x is_const) -----------------";
1.39 -"--------------------------------------------------------";
1.40 -"--------------------------------------------------------";
1.41 -"--------------------------------------------------------";
1.42 -
1.43 -"----------- check return value of adhoc_thm ----";
1.44 -"----------- check return value of adhoc_thm ----";
1.45 -"----------- check return value of adhoc_thm ----";
1.46 -val thy = @{theory "Poly"};
1.47 -val cal = snd (assoc_calc' thy "is_polyexp");
1.48 -val t = @{term "(x / x) is_polyexp"};
1.49 -val SOME (thmID, thm) = adhoc_thm thy cal t;
1.50 -(HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
1.51 -handle TERM _ =>
1.52 - error "calculate.sml: adhoc_thm must return Trueprop";
1.53 -
1.54 -"----------- fun calculate_ -----------------------------";
1.55 -"----------- fun calculate_ -----------------------------";
1.56 -"----------- fun calculate_ -----------------------------";
1.57 -val thy = @{theory "Test"};
1.58 -"===== test 1";
1.59 -val t = (Thm.term_of o the o (parse thy)) "1+2";
1.60 -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
1.61 -term2str (Thm.prop_of thm) = "1 + 2 = 3";
1.62 -
1.63 -"===== test 2";
1.64 -val t = (Thm.term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
1.65 -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
1.66 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.67 -if term2str t = "(3 * 4 / 3) ^^^ 2" then ()
1.68 -else error "calculate.sml: ((1+2)*4/3)^^^2 --> (3 * 4 / 3) ^^^ 2";
1.69 -
1.70 -"===== test 3b -- 2 contiued";
1.71 -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES"))) t;
1.72 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.73 -term2str t;
1.74 -(*val it = "(#12 // #3) ^^^ #2" : string*)
1.75 -
1.76 -"===== test 4";
1.77 -val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"DIVIDE")))t;
1.78 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.79 -term2str t;
1.80 -(*it = "#4 ^^^ #2" : string*)
1.81 -
1.82 -"===== test 5";
1.83 -val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"POWER")))t;
1.84 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.85 -(*show_types := false;*)
1.86 -if term2str t <> "16" then error "calculate.sml: new behaviour in calculate_"
1.87 -else ();
1.88 -
1.89 -
1.90 -val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
1.91 -val (dI',pI',mI') =
1.92 - ("Test",["calculate","test"],["Test","test_calculate"]);
1.93 -
1.94 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.95 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.96 -(*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*)
1.97 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.98 -(*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
1.99 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.100 -(*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
1.101 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.102 -(*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
1.103 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.104 -(*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
1.105 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.106 -(*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
1.107 -
1.108 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.109 -(*nxt = ("Calculate",Calculate "PLUS")*)
1.110 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.111 -(*nxt = ("Calculate",Calculate "TIMES")*)
1.112 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.113 -(*nxt = ("Calculate",Calculate "DIVIDE")*)
1.114 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.115 -(*nxt = ("Calculate",Calculate "POWER")*)
1.116 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.117 -(*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
1.118 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.119 -(*nxt = ("End_Proof'",End_Proof')*)
1.120 -case f of FormKF "16" => () | _ =>
1.121 -error "calculate.sml: script test_calculate changed behaviour";
1.122 -
1.123 -
1.124 -"----------- calculate check test-root-equ --------------";
1.125 -"----------- calculate check test-root-equ --------------";
1.126 -"----------- calculate check test-root-equ --------------";
1.127 -(*(1): 2nd Test_simplify didn't work:
1.128 -val ct =
1.129 - "sqrt (x ^^^ 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
1.130 -> val rls = ("Test_simplify");
1.131 -> val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
1.132 -val ct = "sqrt (x ^^^ 2 + -3 * x) =
1.133 -(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
1.134 -ie. cancel does not work properly
1.135 -*)
1.136 - val thy = "Test";
1.137 - val op_ = "DIVIDE";
1.138 - val ct = "sqrt (x ^^^ 2 + -3 * x) =\
1.139 - \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
1.140 - val SOME (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;
1.141 - writeln ct;
1.142 -(*
1.143 - sqrt (x ^^^ 2 + -3 * x) =\
1.144 - \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))
1.145 -............... does not work *)
1.146 -
1.147 -(*--------------(2): does divide work in Test_simplify ?: ------*)
1.148 - val thy = @{theory Test};
1.149 - val t = (Thm.term_of o the o (parse thy)) "6 / 2";
1.150 - val rls = Test_simplify;
1.151 - val (t,_) = the (rewrite_set_ thy false rls t);
1.152 -(*val t = Free ("3","Real.real") : term*)
1.153 -
1.154 - val thy = "Test";
1.155 - val t = "6 / 2";
1.156 - val rls = "Test_simplify";
1.157 - val (t,_) = the (rewrite_set thy false rls t);
1.158 -(*val t = "3" : string
1.159 - ....... works, thus: which rule in SqRoot_simplify works differently ?*)
1.160 -
1.161 -
1.162 -(*--------------(3): is_const works ?: -------------------------------------*)
1.163 - val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const";
1.164 - atomty t;
1.165 - rewrite_set_ @{theory Test} false tval_rls t;
1.166 -(*val it = SOME (Const ("HOL.True","bool"),[]) ... works*)
1.167 -
1.168 - val t = str2term "2 * x is_const";
1.169 - val SOME (str,t') = eval_const "" "" t (@{theory "Isac"});
1.170 - term2str t';
1.171 -
1.172 -
1.173 -"----------- check calculate bottom up ------------------";
1.174 -"----------- check calculate bottom up ------------------";
1.175 -"----------- check calculate bottom up ------------------";
1.176 -(*-------------- eval_cancel works: *)
1.177 - trace_rewrite:=false;
1.178 - val thy = @{theory Test};
1.179 - val t = (Thm.term_of o the o (parse thy)) "(-4) / 2";
1.180 -
1.181 -val SOME (_, t) = eval_cancel "xxx" "Rings.divide_class.divide" t thy;
1.182 -
1.183 - term2str t;
1.184 -"-4 / 2 = (-2)";
1.185 -(*-------------- but ... *)
1.186 - val ct = "x + (-4) / 2";
1.187 -
1.188 -val thy' = "Test"; (* added AK110727 *)
1.189 - val (ct,_) = the (rewrite_set thy' false rls ct);
1.190 -
1.191 -"(-2) + x";
1.192 -(*-------------- while ... *)
1.193 - val ct = "(-4) / 2";
1.194 -
1.195 - val (ct,_) = the (rewrite_set thy' false rls ct);
1.196 -
1.197 -"-2";
1.198 -*} ML {*
1.199 -
1.200 -(*--------------(5): reproduce (1) with simpler term: ------------*)
1.201 - val thy = "Test";
1.202 - val t = "(3+5)/2";
1.203 - val (t,_) = the (rewrite_set thy false rls t);
1.204 -(*val t = "4" ... works*)
1.205 -
1.206 - val t = "(3+1+2*x)/2";
1.207 - val (t,_) = the (rewrite_set thy false rls t);
1.208 -(*val t = "2 + x" ... works*)
1.209 -
1.210 - trace_rewrite:=false; (*=true3.6.03*)
1.211 -
1.212 - val thy = "Test";
1.213 - val rls = "Test_simplify";
1.214 - val t = "(3+(1+2*x))/2";
1.215 - val (t,_) = the (rewrite_set thy false rls t);
1.216 -(*val t = "2 + x" ... works: give up----------------------------------------*)
1.217 - trace_rewrite:=false;
1.218 -
1.219 - trace_rewrite:=false; (*=true3.6.03*)
1.220 - val thy = @{theory Test};
1.221 - val rls = Test_simplify;
1.222 - val t = str2term "(3+(1+2*x))/2";
1.223 - val SOME (t',asm) = rewrite_set_ thy false rls t;
1.224 - term2str t';
1.225 -(*val t = "2 + x" ... works: give up----------------------------------------*)
1.226 - trace_rewrite:=false;
1.227 -
1.228 -
1.229 -
1.230 -
1.231 -(*--- trace_rewrite before correction of ... --------------------
1.232 - val ct = "(-3 + 2 * x + -1) / 2";
1.233 - val (ct,_) = the (rewrite_set thy' false rls ct);
1.234 -:
1.235 -### trying thm 'root_ge0_2'
1.236 -### rewrite_set_: x + (-1 + -3) / 2
1.237 -### trying thm 'radd_real_const_eq'
1.238 -### trying thm 'radd_real_const'
1.239 -### rewrite_set_: x + (-4) / 2
1.240 -### trying thm 'rcollect_right'
1.241 -:
1.242 -"x + (-4) / 2"
1.243 --------------------------------------while before Isabelle20002:
1.244 - val ct = "(#-3 + #2 * x + #-1) // #2";
1.245 - val (ct,_) = the (rewrite_set thy' false rls ct);
1.246 -:
1.247 -### trying thm 'root_ge0_2'
1.248 -### rewrite_set_: x + (#-1 + #-3) // #2
1.249 -### trying thm 'radd_real_const_eq'
1.250 -### trying thm 'radd_real_const'
1.251 -### rewrite_set_: x + #-4 // #2
1.252 -### rewrite_set_: x + #-2
1.253 -### trying thm 'rcollect_right'
1.254 -:
1.255 -"#-2 + x"
1.256 ------------------------------------------------------------------*)
1.257 -
1.258 -
1.259 -(*===================*)
1.260 - trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
1.261 - val thy' = "Test";
1.262 - val rls = "Test_simplify";
1.263 - val ct = "x + (-1 + -3) / 2";
1.264 - val (ct,_) = the (rewrite_set thy' false rls ct);
1.265 -"x + (-4) / 2";
1.266 -(*
1.267 -### trying calc. 'cancel'
1.268 -@@@ get_pair: binop, t = x + (-4) / 2
1.269 -@@@ get_pair: t else
1.270 -@@@ get_pair: t else -> NONE
1.271 -@@@ get_pair: binop, t = (-4) / 2
1.272 -@@@ get_pair: then 1
1.273 -@@@ get_pair: t -> NONE
1.274 -@@@ get_pair: t1 -> NONE
1.275 -@@@ adhoc_thm': NONE
1.276 -### trying calc. 'pow'
1.277 -*)
1.278 -*} ML {*
1.279 -
1.280 - trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
1.281 - val thy' = "Test";
1.282 - val rls = "Test_simplify";
1.283 - val ct = "x + (-4) / 2";
1.284 - val (ct,_) = the (rewrite_set thy' false rls ct);
1.285 -"(-2) + x";
1.286 -(*
1.287 -### trying calc. 'cancel'
1.288 -@@@ get_pair: binop, t = x + -4 / 2
1.289 -@@@ get_pair: t else
1.290 -@@@ get_pair: t else -> NONE
1.291 -@@@ get_pair: binop, t = -4 / 2
1.292 -@@@ get_pair: then 1
1.293 -@@@ adhoc_thm': SOME #cancel_-4_2
1.294 -### calc. to: x + (-2)
1.295 -### trying calc. 'cancel'
1.296 -*)
1.297 - trace_rewrite:=false;
1.298 -
1.299 -"----------- Atools.pow Power.power_class.power ---------";
1.300 -"----------- Atools.pow Power.power_class.power ---------";
1.301 -"----------- Atools.pow Power.power_class.power ---------";
1.302 -val t = (Thm.term_of o the o (parseold thy)) "1 ^ aaa";
1.303 -atomty t;
1.304 -(*** -------------
1.305 -*** Const ( Nat.power, ['a, nat] => 'a)
1.306 -*** . Free ( 1, 'a)
1.307 -*** . Free ( aaa, nat) *)
1.308 -
1.309 -val t = str2term "1 ^^^ aaa";
1.310 -atomty t;
1.311 -(****
1.312 -*** Const (Atools.pow, real => real => real)
1.313 -*** . Free (1, real)
1.314 -*** . Free (aaa, real)
1.315 -*** *);
1.316 -
1.317 -" ================= calculate.sml: calculate_ 2002 =================== ";
1.318 -" ================= calculate.sml: calculate_ 2002 =================== ";
1.319 -" ================= calculate.sml: calculate_ 2002 =================== ";
1.320 -
1.321 -val thy = @{theory Test};
1.322 -val t = (Thm.term_of o the o (parse thy)) "12 / 3";
1.323 -val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"DIVIDE")))t;
1.324 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.325 -"12 / 3 = 4";
1.326 -val thy = @{theory Test};
1.327 -val t = (Thm.term_of o the o (parse thy)) "4 ^^^ 2";
1.328 -val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"POWER"))) t;
1.329 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.330 -"4 ^ 2 = 16";
1.331 -
1.332 - val t = (Thm.term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
1.333 - val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
1.334 -"1 + 2 = 3";
1.335 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.336 - term2str t;
1.337 -"(3 * 4 / 3) ^^^ 2";
1.338 - val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES")))t;
1.339 -"3 * 4 = 12";
1.340 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.341 - term2str t;
1.342 -"(12 / 3) ^^^ 2";
1.343 - val SOME (thmID,thm) =adhoc_thm thy(the(assoc(calclist,"DIVIDE")))t;
1.344 -"12 / 3 = 4";
1.345 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.346 - term2str t;
1.347 -"4 ^^^ 2";
1.348 - val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"POWER")))t;
1.349 -"4 ^^^ 2 = 16";
1.350 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
1.351 - term2str t;
1.352 -"16";
1.353 - if it <> "16" then error "calculate.sml: new behaviour in calculate_"
1.354 - else ();
1.355 -*} ML {*
1.356 -
1.357 -(*13.9.02 *** calc: operator = pow not defined*)
1.358 - val t = (Thm.term_of o the o (parse thy)) "3^^^2";
1.359 - val SOME (thmID,thm) =
1.360 - adhoc_thm thy (the(assoc(calclist,"POWER"))) t;
1.361 -(*** calc: operator = pow not defined*)
1.362 -
1.363 - val (op_, eval_fn) = the (assoc(calclist,"POWER"));
1.364 - (*
1.365 -val op_ = "Atools.pow" : string
1.366 -val eval_fn = fn : string -> term -> theory -> (string * term) option*)
1.367 -
1.368 - val SOME (thmid,t') = get_pair thy op_ eval_fn t;
1.369 -(*** calc: operator = pow not defined*)
1.370 -
1.371 - val SOME (id,t') = eval_fn op_ t thy;
1.372 -(*** calc: operator = pow not defined*)
1.373 -
1.374 - val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);
1.375 - val SOME (id,t') = eval_binop thmid op_ t thy;
1.376 -(*** calc: operator = pow not defined*)
1.377 -
1.378 -*} ML {*
1.379 -@{theory EqSystem}; (*.., Isac.EqSystem}*)
1.380 -*} ML {*
1.381 -*} ML {*
1.382 -*} ML {*
1.383 -*} ML {*
1.384 -*} ML {*
1.385 -*} ML {*
1.386 -*} ML {* (*Theory loader: undefined entry for theory "EqSystem"*)
1.387 -
1.388 -"----------- get_pair with 3 args --------------------------------";
1.389 -"----------- get_pair with 3 args --------------------------------";
1.390 -"----------- get_pair with 3 args --------------------------------";
1.391 -val (thy, op_, ef, arg) =
1.392 - (thy, "EqSystem.occur'_exactly'_in",
1.393 - assoc_calc' (Thy_Info_get_theory "EqSystem") "occur_exactly_in" |> snd |> snd,
1.394 - str2term
1.395 - "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
1.396 - );
1.397 -val SOME (str, simpl) = get_pair thy op_ ef arg;
1.398 -*} ML {*
1.399 -*} ML {*
1.400 -*} ML {*
1.401 -*} ML {*
1.402 -*} ML {*
1.403 -*} ML {*
1.404 -*} ML {*
1.405 -if str = "2 * x_" then () else writeln "probably WORKS"
1.406 -*} text {*
1.407 -if str =
1.408 -"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
1.409 -then () else error "calculate.sml get_pair with 3 args:occur_exactly_in";
1.410 -*} ML {*
1.411 -
1.412 -
1.413 -"----------- calculate (2 * x is_const) -----------------";
1.414 -"----------- calculate (2 * x is_const) -----------------";
1.415 -"----------- calculate (2 * x is_const) -----------------";
1.416 -val t = str2term "2 * x is_const";
1.417 -val SOME (str, t') = eval_const "" "" t @{theory Test};
1.418 -term2str t';
1.419 -"(2 * x is_const) = False";
1.420 -
1.421 -val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
1.422 -term2str t';
1.423 -"HOL.False";
1.424 -
1.425 *} ML {*
1.426 *}
1.427 -(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
1.428 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
1.429 ML_file "ProgLang/rewrite.sml"
1.430 ML_file "ProgLang/listC.sml"
1.431 ML_file "ProgLang/scrtools.sml"
1.432 ML_file "ProgLang/tools.sml"
1.433 +(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
1.434 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
1.435 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
1.436 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}