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