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