1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Jun 21 22:08:01 2021 +0200
1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Sun Jul 18 18:15:27 2021 +0200
1.3 @@ -14,9 +14,10 @@
1.4 "----------- calculate from Prog --------------------------------- -----------------------------";
1.5 "----------- calculate from script --requires 'setup'----";
1.6 "----------- calculate check test-root-equ --------------";
1.7 -"----------- check calcul,ate bottom up -----------------";
1.8 +"----------- check calculate bottom up -----------------";
1.9 "----------- Prog_Expr.pow Power.power_class.power ---------";
1.10 -" ================= evaluate.sml: calculate_ 2002 ======";
1.11 +"----------- fun cancel_int --------------------------------------------------------------------";
1.12 +"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
1.13 "----------- get_pair with 3 args -----------------------";
1.14 "----------- calculate (2 * x is_const) -----------------";
1.15 "----------- fun get_pair: examples ------------------------------------------------------------";
1.16 @@ -45,12 +46,12 @@
1.17 (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
1.18 val t = TermC.str2term "((1+2)*4/3) \<up> 2";
1.19 val thy = @{theory};
1.20 -val times = (\<^const_name>\<open>times\<close>, eval_binop "#mult_") : string * Eval_Def.eval_fn;
1.21 -val plus = (\<^const_name>\<open>plus\<close>,eval_binop "#add_") : string * Eval_Def.eval_fn;
1.22 -val divide = (\<^const_name>\<open>divide\<close> ,eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
1.23 -val pow = (\<^const_name>\<open>powr\<close> ,eval_binop "#power_") : string * Eval_Def.eval_fn;
1.24 +val times = ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
1.25 +val plus = ("Groups.plus_class.plus", eval_binop "#add_") : string * Eval_Def.eval_fn;
1.26 +val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
1.27 +val pow = ("Transcendental.powr", eval_binop "#power_") : string * Eval_Def.eval_fn;
1.28
1.29 -"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t);
1.30 +"~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
1.31 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
1.32 val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
1.33 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_ 1 + 2 = 3 changed";
1.34 @@ -76,7 +77,7 @@
1.35 val thy = @{theory "Test"};
1.36 val fmz = ["realTestGiven (((1+2)*4/3) \<up> 2)", "realTestFind s"];
1.37 val (dI',pI',mI') =
1.38 - ("Test",["calculate", "test"],["Test", "test_calculate"]);
1.39 + ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
1.40
1.41 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.42 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.43 @@ -107,23 +108,23 @@
1.44 "----------- calculate check test-root-equ --------------";
1.45 (*(1): 2nd Test_simplify didn't work:
1.46 val ct =
1.47 - "sqrt (x \<up> 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
1.48 + "sqrt (x \<up> 2 + -3 * x) = (-3 + 2 * x + - 1 * (9 + 4 * x)) / (- 1 * 2)"
1.49 > val rls = ("Test_simplify");
1.50 > val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
1.51 val ct = "sqrt (x \<up> 2 + -3 * x) =
1.52 -(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
1.53 +(-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))";
1.54 ie. cancel does not work properly
1.55 *)
1.56 val thy = @{theory "Test"};
1.57 val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
1.58 val ct = ThmC_Def.num_to_Free @{term
1.59 - "sqrt (x \<up> 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"};
1.60 + "sqrt (x \<up> 2 + -3 * x) = (-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))"};
1.61 case calculate_ thy op_ ct of
1.62 SOME _ => ()
1.63 | NONE => error "calculate_ test-root-equ changed";
1.64 (*
1.65 sqrt (x \<up> 2 + -3 * x) =\
1.66 - \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))
1.67 + \(-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))
1.68 ............... does not work *)
1.69
1.70 (*--------------(2): does divide work in Test_simplify ?: ------*)
1.71 @@ -148,7 +149,7 @@
1.72 "----------- check calculate bottom up ------------------";
1.73 "----------- check calculate bottom up ------------------";
1.74 (*-------------- eval_cancel works: *)
1.75 - Rewrite.trace_on := false;
1.76 + Rewrite.trace_on := false; (*true false*)
1.77 val thy = @{theory Test};
1.78 val rls = Test_simplify;
1.79 val t = (Thm.term_of o the o (TermC.parse thy)) "(-4) / 2";
1.80 @@ -158,22 +159,25 @@
1.81 (*--------------(5): reproduce (1) with simpler term: ------------*)
1.82 val t = (Thm.term_of o the o (TermC.parse thy)) "(3+5)/2";
1.83 case rewrite_set_ thy false rls t of
1.84 - SOME (Free ("4", _), []) => ()
1.85 -| _ => error "rewrite_set_ (3+5)/2 changed";
1.86 + SOME (t', []) =>
1.87 + if UnparseC.term t' = "4" then ()
1.88 + else error "rewrite_set_ (3+5)/2 changed 1"
1.89 +| _ => error "rewrite_set_ (3+5)/2 changed 2";
1.90
1.91 val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
1.92 case rewrite_set_ thy false rls t of
1.93 - SOME (Const (\<^const_name>\<open>plus\<close>, _) $ Free ("2", _) $ Free ("x", _), []) => ()
1.94 -| _ => error "rewrite_set_ (3+1+2*x)/2 changed";
1.95 + SOME (t', _) => (*WAS "x + 2" WITH OLD numerals TOODOO?*)
1.96 + if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
1.97 +| _ => error "rewrite_set_ (3+1+2*x)/2 changed 2";
1.98
1.99 - Rewrite.trace_on:=false; (*=true3.6.03*)
1.100 + Rewrite.trace_on := false; (*true false*)
1.101
1.102 (*--- Rewrite.trace_on before correction of ... --------------------
1.103 - val ct = "(-3 + 2 * x + -1) / 2";
1.104 + val ct = "(-3 + 2 * x + - 1) / 2";
1.105 val (ct,_) = the (rewrite_set thy' false rls ct);
1.106 :
1.107 ### trying thm 'root_ge0_2'
1.108 -### rewrite_set_: x + (-1 + -3) / 2
1.109 +### rewrite_set_: x + (- 1 + -3) / 2
1.110 ### trying thm 'radd_real_const_eq'
1.111 ### trying thm 'radd_real_const'
1.112 ### rewrite_set_: x + (-4) / 2
1.113 @@ -181,26 +185,27 @@
1.114 :
1.115 "x + (-4) / 2"
1.116 -------------------------------------while before Isabelle20002:
1.117 - val ct = "(#-3 + #2 * x + #-1) // #2";
1.118 + val ct = "(#-3 + #2 * x + #- 1) // #2";
1.119 val (ct,_) = the (rewrite_set thy' false rls ct);
1.120 :
1.121 ### trying thm 'root_ge0_2'
1.122 -### rewrite_set_: x + (#-1 + #-3) // #2
1.123 +### rewrite_set_: x + (#- 1 + #-3) // #2
1.124 ### trying thm 'radd_real_const_eq'
1.125 ### trying thm 'radd_real_const'
1.126 ### rewrite_set_: x + #-4 // #2
1.127 -### rewrite_set_: x + #-2
1.128 +### rewrite_set_: x + #- 2
1.129 ### trying thm 'rcollect_right'
1.130 :
1.131 -"#-2 + x"
1.132 +"#- 2 + x"
1.133 -----------------------------------------------------------------*)
1.134
1.135
1.136 (*===================*)
1.137 Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
1.138 - val t = (Thm.term_of o the o (TermC.parse thy)) "x + (-1 + -3) / 2";
1.139 + val t = (Thm.term_of o the o (TermC.parse thy)) "x + (- 1 + -3) / 2";
1.140 val SOME (res, []) = rewrite_set_ thy false rls t;
1.141 -if UnparseC.term res = "-2 + x" then () else error "rewrite_set_ x + (-1 + -3) / 2 changed";
1.142 + (*WAS "x + - 2" WITH OLD numerals TOODOO?*)
1.143 +if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_ x + (- 1 + -3) / 2 changed";
1.144 "x + (-4) / 2";
1.145 (*
1.146 ### trying calc. 'cancel'
1.147 @@ -217,24 +222,6 @@
1.148
1.149 Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
1.150
1.151 -"----------- Prog_Expr.pow Power.power_class.power ---------";
1.152 -"----------- Prog_Expr.pow Power.power_class.power ---------";
1.153 -"----------- Prog_Expr.pow Power.power_class.power ---------";
1.154 -val t = (Thm.term_of o the o (parseold thy)) "1 ^ aaa";
1.155 -TermC.atomty t;
1.156 -(*** -------------
1.157 -*** Const ( Nat.power, ['a, nat] => 'a)
1.158 -*** . Free ( 1, 'a)
1.159 -*** . Free ( aaa, nat) *)
1.160 -
1.161 -val t = TermC.str2term "1 \<up> aaa";
1.162 -TermC.atomty t;
1.163 -(****
1.164 -*** Const (Prog_Expr.pow, real => real => real)
1.165 -*** . Free (1, real)
1.166 -*** . Free (aaa, real)
1.167 -*** *);
1.168 -
1.169 " ================= evaluate.sml: calculate_ 2002 =================== ";
1.170 " ================= evaluate.sml: calculate_ 2002 =================== ";
1.171 " ================= evaluate.sml: calculate_ 2002 =================== ";
1.172 @@ -291,10 +278,64 @@
1.173 val SOME (id,t') = eval_fn op_ t thy;
1.174 (*** calc: operator = pow not defined*)
1.175
1.176 - val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);
1.177 - val SOME (id,t') = eval_binop thmid op_ t thy;
1.178 +case (op_, t) of
1.179 + ("Transcendental.powr",
1.180 + Const ("Transcendental.powr", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $
1.181 + (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))) => ()
1.182 +| _ => error "3 \<up> 2 CHANGED";
1.183 + val SOME (id, t') = eval_binop thmid op_ t thy;
1.184 (*** calc: operator = pow not defined*)
1.185
1.186 +if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop 3 \<up> 2 = 9 CHANGED";
1.187 +
1.188 +
1.189 +"----------- fun cancel_int --------------------------------------------------------------------";
1.190 +"----------- fun cancel_int --------------------------------------------------------------------";
1.191 +"----------- fun cancel_int --------------------------------------------------------------------";
1.192 +if cancel_int (~4, 2) = (~1, (2, 1)) then () else error "cancel_int (~4, 2) CHANGED";
1.193 +if cancel_int (4, ~8) = (~1, (1, 2)) then () else error "cancel_int (4, ~8) CHANGED";
1.194 +if cancel_int (6, 4) = (1, (3, 2)) then () else error "cancel_int (6, 4)CHANGED";
1.195 +
1.196 +
1.197 +"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
1.198 +"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
1.199 +"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
1.200 +val (t1, t2) = (@{term 3}, @{term "2::real"});
1.201 +
1.202 +"~~~~~ fun calcul , args:"; val (op_, (t1, t2)) = ("Groups.plus_class.plus", (t1, t2));
1.203 + val (Const ("Num.numeral_class.numeral", _) $ n1) = t1;
1.204 + val (Const ("Num.numeral_class.numeral", _) $ n2) = t2;
1.205 + val (T, _) = HOLogic.dest_number t1
1.206 + val (i1, i2) = (HOLogic.dest_numeral n1, HOLogic.dest_numeral n2)
1.207 + val result =
1.208 + case op_ of
1.209 + "Groups.plus_class.plus" => i1 + i2
1.210 + | "Groups.minus_class.minus" => i1 - i2
1.211 + | "Groups.times_class.times" => i1 * i2
1.212 + | "Transcendental.powr" => power i1 i2
1.213 + | str => raise ERROR ("calcul not impl.for op_ " ^ str)
1.214 + (*in*)
1.215 + val xxx = HOLogic.mk_number T result;
1.216 + (*end*)
1.217 +case HOLogic.dest_number xxx of
1.218 + (_, 5) => ()
1.219 +| _ => error "calcul + 2 3 CHANGED";
1.220 +
1.221 +case HOLogic.dest_number (calcul "Groups.minus_class.minus" (t1, t2)) of
1.222 + (_, 1) => xxx
1.223 +| _ => error "calcul - 2 3 CHANGED";
1.224 +
1.225 +case HOLogic.dest_number (calcul "Groups.times_class.times" (t1, t2)) of
1.226 + (_, 6) => xxx
1.227 +| _ => error "calcul - 2 3 CHANGED";
1.228 +
1.229 +(* (calcul "Rings.divide_class.divide" (t1, t2)
1.230 +ERROR: calcul not impl.for op_ Rings.divide_class.divide*)
1.231 +
1.232 +case HOLogic.dest_number (calcul "Transcendental.powr" (t1, t2)) of
1.233 + (_, 9) => xxx
1.234 +| _ => error "calcul - 2 3 CHANGED";
1.235 +
1.236
1.237 "----------- get_pair with 3 args --------------------------------";
1.238 "----------- get_pair with 3 args --------------------------------";
1.239 @@ -303,11 +344,11 @@
1.240 (thy, "EqSystem.occur_exactly_in",
1.241 assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd,
1.242 TermC.str2term
1.243 - "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L \<up> 2) / 2"
1.244 + "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2"
1.245 );
1.246 val SOME (str, simpl) = get_pair thy op_ ef arg;
1.247 if str =
1.248 -"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L \<up> 2) / 2 = True"
1.249 +"[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2 = True"
1.250 then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in";
1.251
1.252
1.253 @@ -316,49 +357,50 @@
1.254 "----------- calculate (2 * x is_const) -----------------";
1.255 val t = TermC.str2term "2 * x is_const";
1.256 val SOME (str, t') = eval_const "" "" t @{theory Test};
1.257 -UnparseC.term t';
1.258 -"(2 * x is_const) = False";
1.259 +if UnparseC.term t' = "(2 * x is_const) = False" then ()
1.260 +else error "eval_const 2 * x is_const CHANGED";
1.261
1.262 val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
1.263 -UnparseC.term t';
1.264 -\<^const_name>\<open>False\<close>;
1.265 +if UnparseC.term t' = "False" then ()
1.266 +else error "rewrite_set_ 2 * x is_const CHANGED";
1.267
1.268 "----------- fun get_pair: examples ------------------------------------------------------------";
1.269 "----------- fun get_pair: examples ------------------------------------------------------------";
1.270 "----------- fun get_pair: examples ------------------------------------------------------------";
1.271 val thy = @{theory};
1.272 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
1.273 +if isa_str = "Groups.plus_class.plus" then () else error "eval_fn PLUS changed";
1.274
1.275 -val t = (Thm.term_of o the o (TermC.parse thy)) "3 + 4";
1.276 +val t = @{term "3 + 4 :: real"};
1.277 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.278 -if str = "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7"
1.279 -then () else error "get_pair 3 + 4 changed";
1.280 +(*+*)if str = "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7"
1.281 +(*+*)then () else error "get_pair 3 + 4 changed";
1.282
1.283 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a + 3) + 4";
1.284 +val t = @{term "(a + 3) + 4 :: real"};
1.285 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.286 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
1.287 then () else error "get_pair (a + 3) + 4 changed";
1.288
1.289 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a + 3) + 4";
1.290 +val t = @{term "(a + 3) + 4 :: real"};
1.291 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.292 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
1.293 then () else error "get_pair (a + 3) + 4 changed";
1.294
1.295 -val t = (Thm.term_of o the o (TermC.parse thy)) "x = 5 * (3 + (4 + a))";
1.296 +val t = @{term "x = 5 * (3 + (4 + a) :: real)"};
1.297 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.298 if str = "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a"
1.299 then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed";
1.300
1.301 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
1.302
1.303 -val t = (Thm.term_of o the o (TermC.parse thy)) "-4 / -2";
1.304 +val t = @{term "-4 / - 2 :: real"};
1.305 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.306 -if str = "#divide_e-4_-2" andalso UnparseC.term term = "-4 / -2 = 2"
1.307 -then () else error "get_pair -4 / -2 changed";
1.308 +if str = "#divide_e~4_~2" andalso UnparseC.term term = "- 4 / - 2 = 2"
1.309 +then () else error "get_pair -4 / - 2 changed";
1.310
1.311 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
1.312
1.313 -val t = (Thm.term_of o the o (TermC.parse thy)) "2 \<up> 3";
1.314 +val t = @{term "2 \<up> 3 :: real"};
1.315 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.316 if str = "#: 2 \<up> 3 = 8" andalso UnparseC.term term = "2 \<up> 3 = 8"
1.317 then () else error "get_pair 2 \<up> 3 changed";
1.318 @@ -368,18 +410,17 @@
1.319 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
1.320 (*--------------------------------------------------------------------vvvvvvvvvv*)
1.321 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_const");
1.322 -val SOME t = parseNEW @{context} "9 is_const";
1.323 +val t = @{term "9 is_const"};
1.324 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.325 if str = "#is_const_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_const) = True"
1.326 then () else error "adhoc_thm 9 is_const changed";
1.327
1.328 -
1.329 case assoc_calc thy \<^const_name>\<open>less\<close> of
1.330 "le" => () | _ => error "Orderings.ord_class.less <-> le changed";
1.331 -(*--------------------------------------------------------------------vvvvvvvvvv*)
1.332 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le");
1.333 +if isa_str = "Orderings.ord_class.less" then () else error "adhoc_thm (4 < 4) = False CHANGED";
1.334
1.335 -val SOME t = parseNEW @{context} "4 < 4";
1.336 +val t = @{term "4 < (4 :: real)"};
1.337 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.338 if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"
1.339 then () else error "adhoc_thm 4 < 4 changed";
1.340 @@ -388,37 +429,53 @@
1.341 case adhoc_thm thy (isa_str, eval_fn) t of
1.342 NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE";
1.343
1.344 -
1.345 -(*--------------------------------------------------------------------vvvvvvvvvv*)
1.346 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
1.347 -val SOME t = parseNEW @{context} "1 + 2";
1.348 +val SOME t = parseNEW @{context} "1 + (2::real)";
1.349 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.350 if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
1.351 then () else error "adhoc_thm 1 + 2 changed";
1.352
1.353 -(*--------------------------------------------------------------------vvvvvvvvvv*)
1.354 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
1.355 -val SOME t = parseNEW @{context} "6 / -8";
1.356 +val t = @{term "6 / -8 :: real"};
1.357 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.358 -if str = "#divide_e6_-8" andalso ThmC_Def.string_of_thm thm = "6 / -8 = -3 / 4"
1.359 -then () else error "adhoc_thm 1 + 2 changed";
1.360 -
1.361 +if str = "#divide_e6_~8" andalso ThmC_Def.string_of_thm thm = "6 / - 8 = - 3 / 4"
1.362 +then () else error "adhoc_thm 6 / -8 = - 3 / 4 changed";
1.363
1.364 case assoc_calc thy "Prog_Expr.ident" of
1.365 "ident" => () | _ => error "Prog_Expr.ident <-> ident changed";
1.366 -(*--------------------------------------------------------------------vvvvvvvvvv*)
1.367 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");
1.368
1.369 -val SOME t = parseNEW @{context} "3 =!= 3";
1.370 +val t = @{term "3 =!= (3 :: real)"};
1.371 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.372 if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"
1.373 then () else error "adhoc_thm (3 =!= 3) changed";
1.374
1.375 -val SOME t = parseNEW @{context} "\<not> (4 + (4 * x + x ^ 2) =!= 0)";
1.376 +val t = @{term "\<not> ((4 :: real) + (4 * x + x \<up> 2) =!= 0)"};
1.377 val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
1.378 -if str = "#ident_(4 + (4 * x + x ^ 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x ^ 2) =!= 0) = False"
1.379 +if str = "#ident_(4 + (4 * x + x \<up> 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x \<up> 2) =!= 0) = False"
1.380 then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
1.381
1.382 +"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
1.383 +"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
1.384 +"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
1.385 +val t = TermC.str2term "sqrt 4";
1.386 +
1.387 +(* TOODOO.1: exception TYPE raised by Skip_Proof.make_thm * )
1.388 + exception TYPE raised (line 169 of "consts.ML"): Illegal type
1.389 + for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
1.390 + Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t
1.391 +( **)
1.392 +"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
1.393 + ((ThyC.get_theory "Isac_Knowledge"),
1.394 + ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> theory -> (string * term) option), t);
1.395 +val SOME (thmid, t) =
1.396 + (*case*) get_pair thy op_ eval_fn ct (*of*);
1.397 +(** )
1.398 + exception TYPE raised (line 169 of "consts.ML"): Illegal type
1.399 + for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
1.400 + Skip_Proof.make_thm thy t
1.401 +( **)
1.402 +
1.403 "----------- fun power -------------------------------------------------------------------------";
1.404 "----------- fun power -------------------------------------------------------------------------";
1.405 "----------- fun power -------------------------------------------------------------------------";