walther@59902
|
1 |
(* Title: "ProgLang/evaluate.sml"
|
walther@60278
|
2 |
test calculation of values for function constants
|
neuper@38022
|
3 |
Author: Walther Neuper 2000
|
neuper@38022
|
4 |
(c) copyright due to lincense terms.
|
neuper@37906
|
5 |
*)
|
neuper@37906
|
6 |
|
neuper@38022
|
7 |
"--------------------------------------------------------";
|
neuper@38022
|
8 |
"table of contents --------------------------------------";
|
neuper@38022
|
9 |
"--------------------------------------------------------";
|
neuper@55366
|
10 |
"-calculate.thy: provides 'setup' -----------------------";
|
neuper@41924
|
11 |
"----------- fun norm -----------------------------------";
|
wneuper@59255
|
12 |
"----------- check return value of adhoc_thm ----";
|
wneuper@59411
|
13 |
"----------- fun calculate_ --------------------------------------------------------------------";
|
wneuper@59411
|
14 |
"----------- calculate from Prog --------------------------------- -----------------------------";
|
neuper@55366
|
15 |
"----------- calculate from script --requires 'setup'----";
|
neuper@38032
|
16 |
"----------- calculate check test-root-equ --------------";
|
walther@60317
|
17 |
"----------- check calculate bottom up -----------------";
|
walther@59603
|
18 |
"----------- Prog_Expr.pow Power.power_class.power ---------";
|
walther@60317
|
19 |
"----------- fun cancel_int --------------------------------------------------------------------";
|
Walther@60516
|
20 |
"----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
|
neuper@38032
|
21 |
"----------- get_pair with 3 args -----------------------";
|
walther@60387
|
22 |
"----------- calculate (2 * x is_num) -------------------";
|
wneuper@59387
|
23 |
"----------- fun get_pair: examples ------------------------------------------------------------";
|
wneuper@59387
|
24 |
"----------- fun adhoc_thm: examples -----------------------------------------------------------";
|
walther@60391
|
25 |
"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
|
walther@60357
|
26 |
"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
|
wneuper@59403
|
27 |
"----------- fun power -------------------------------------------------------------------------";
|
wneuper@59403
|
28 |
"----------- fun divisors ----------------------------------------------------------------------";
|
wneuper@59403
|
29 |
"----------- fun doubles, fun squfact ----------------------------------------------------------";
|
neuper@38022
|
30 |
"--------------------------------------------------------";
|
neuper@38022
|
31 |
"--------------------------------------------------------";
|
neuper@38022
|
32 |
"--------------------------------------------------------";
|
neuper@37906
|
33 |
|
wneuper@59255
|
34 |
"----------- check return value of adhoc_thm ----";
|
wneuper@59255
|
35 |
"----------- check return value of adhoc_thm ----";
|
wneuper@59255
|
36 |
"----------- check return value of adhoc_thm ----";
|
neuper@41924
|
37 |
val thy = @{theory "Poly"};
|
Walther@60550
|
38 |
val ctxt = Proof_Context.init_global thy;
|
Walther@60550
|
39 |
val cal = snd (get_calc ctxt "is_polyexp");
|
neuper@38022
|
40 |
val t = @{term "(x / x) is_polyexp"};
|
Walther@60519
|
41 |
val SOME (thmID, thm) = adhoc_thm ctxt cal t;
|
wneuper@59188
|
42 |
(HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
|
neuper@38022
|
43 |
handle TERM _ =>
|
walther@59902
|
44 |
error "evaluate.sml: adhoc_thm must return Trueprop";
|
neuper@38022
|
45 |
|
wneuper@59411
|
46 |
"----------- fun calculate_ --------------------------------------------------------------------";
|
wneuper@59411
|
47 |
"----------- fun calculate_ --------------------------------------------------------------------";
|
wneuper@59411
|
48 |
"----------- fun calculate_ --------------------------------------------------------------------";
|
wneuper@59411
|
49 |
(* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
|
Walther@60565
|
50 |
val t = TermC.parse_test @{context} "((1+2)*4/3) \<up> 2";
|
wneuper@59411
|
51 |
val thy = @{theory};
|
Walther@60500
|
52 |
val ctxt = Proof_Context.init_global @{theory}
|
Walther@60539
|
53 |
val times = ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval.ml_fun;
|
Walther@60539
|
54 |
val plus = ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval.ml_fun;
|
Walther@60539
|
55 |
val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval.ml_fun;
|
Walther@60539
|
56 |
val pow = (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval.ml_fun;
|
wneuper@59411
|
57 |
|
walther@60317
|
58 |
"~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
|
Walther@60519
|
59 |
val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{context} isa_fn t;
|
Walther@60509
|
60 |
val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
|
walther@60242
|
61 |
if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_ 1 + 2 = 3 changed";
|
wneuper@59411
|
62 |
|
wneuper@59411
|
63 |
"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
|
Walther@60519
|
64 |
val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{context} isa_fn t';
|
Walther@60509
|
65 |
val SOME (t'', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
|
walther@60242
|
66 |
if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_ 3 * 4 = 12 changed";
|
wneuper@59411
|
67 |
|
wneuper@59411
|
68 |
"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
|
Walther@60519
|
69 |
val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{context} isa_fn t;
|
Walther@60509
|
70 |
val SOME (t''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
|
walther@60242
|
71 |
if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_ 12 / 3 = 4 changed";
|
wneuper@59411
|
72 |
|
wneuper@59411
|
73 |
"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
|
Walther@60519
|
74 |
val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{context} isa_fn t;
|
Walther@60509
|
75 |
val SOME (t'''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
|
walther@59868
|
76 |
if UnparseC.term t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed";
|
wneuper@59411
|
77 |
|
wneuper@59411
|
78 |
"----------- calculate from Prog --------------------------------- -----------------------------";
|
wneuper@59411
|
79 |
"----------- calculate from Prog --------------------------------- -----------------------------";
|
wneuper@59411
|
80 |
"----------- calculate from Prog --------------------------------- -----------------------------";
|
neuper@41924
|
81 |
val thy = @{theory "Test"};
|
walther@60242
|
82 |
val fmz = ["realTestGiven (((1+2)*4/3) \<up> 2)", "realTestFind s"];
|
neuper@37906
|
83 |
val (dI',pI',mI') =
|
walther@60317
|
84 |
("Test", ["calculate", "test"], ["Test", "test_calculate"]);
|
neuper@38035
|
85 |
|
Walther@60571
|
86 |
val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
87 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@60242
|
88 |
(*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) \<up> #2)")*)
|
neuper@37906
|
89 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
90 |
(*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
|
neuper@37906
|
91 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@38035
|
92 |
(*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
|
neuper@37906
|
93 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59997
|
94 |
(*nxt = ("Specify_Problem",Specify_Problem ["calculate", "test"])*)
|
neuper@37906
|
95 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59997
|
96 |
(*nxt = ("Specify_Method",Specify_Method ("Test", "test_calculate"))*)
|
neuper@37906
|
97 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
walther@59997
|
98 |
(*nxt = ("Apply_Method",Apply_Method ("Test", "test_calculate"))*)
|
neuper@37906
|
99 |
|
walther@59713
|
100 |
(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "PLUS")*)
|
walther@59713
|
101 |
(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "TIMES")*)
|
walther@59713
|
102 |
(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "DIVIDE")*)
|
walther@59713
|
103 |
(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "POWER")*)
|
walther@59997
|
104 |
(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Check_Postcond",Check_Postcond ["calculate", "test"])*)
|
walther@59713
|
105 |
(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("End_Proof'",End_Proof')*)
|
walther@59959
|
106 |
case f of Test_Out.FormKF "16" => () | _ =>
|
walther@59902
|
107 |
error "evaluate.sml: script test_calculate changed behaviour";
|
neuper@37906
|
108 |
|
neuper@37906
|
109 |
|
neuper@38032
|
110 |
"----------- calculate check test-root-equ --------------";
|
neuper@38032
|
111 |
"----------- calculate check test-root-equ --------------";
|
neuper@38032
|
112 |
"----------- calculate check test-root-equ --------------";
|
neuper@37906
|
113 |
(*(1): 2nd Test_simplify didn't work:
|
neuper@37906
|
114 |
val ct =
|
walther@60329
|
115 |
"sqrt (x \<up> 2 + -3 * x) = (-3 + 2 * x + - 1 * (9 + 4 * x)) / (- 1 * 2)"
|
neuper@37906
|
116 |
> val rls = ("Test_simplify");
|
neuper@37906
|
117 |
> val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
|
walther@60242
|
118 |
val ct = "sqrt (x \<up> 2 + -3 * x) =
|
walther@60329
|
119 |
(-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))";
|
neuper@37906
|
120 |
ie. cancel does not work properly
|
neuper@37906
|
121 |
*)
|
wneuper@59382
|
122 |
val thy = @{theory "Test"};
|
walther@59686
|
123 |
val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
|
walther@60337
|
124 |
val ct = @{term
|
walther@60329
|
125 |
"sqrt (x \<up> 2 + -3 * x) = (-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))"};
|
Walther@60500
|
126 |
case calculate_ ctxt op_ ct of
|
wneuper@59382
|
127 |
SOME _ => ()
|
wneuper@59382
|
128 |
| NONE => error "calculate_ test-root-equ changed";
|
neuper@37906
|
129 |
(*
|
walther@60242
|
130 |
sqrt (x \<up> 2 + -3 * x) =\
|
walther@60329
|
131 |
\(-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))
|
neuper@37906
|
132 |
............... does not work *)
|
neuper@37906
|
133 |
|
neuper@37906
|
134 |
(*--------------(2): does divide work in Test_simplify ?: ------*)
|
akargl@42188
|
135 |
val thy = @{theory Test};
|
Walther@60424
|
136 |
val ctxt = (ThyC.id_to_ctxt "Test")
|
Walther@60424
|
137 |
val t = TermC.parseNEW' ctxt "6 / 2";
|
neuper@37906
|
138 |
val rls = Test_simplify;
|
Walther@60500
|
139 |
val (t,_) = the (rewrite_set_ ctxt false rls t);
|
walther@59997
|
140 |
(*val t = Free ("3", "Real.real") : term*)
|
neuper@37906
|
141 |
|
walther@60387
|
142 |
(*--------------(3): is_num works ?: -------------------------------------*)
|
Walther@60424
|
143 |
val t = TermC.parseNEW' ctxt "2 is_num";
|
walther@60230
|
144 |
TermC.atomty t;
|
Walther@60500
|
145 |
rewrite_set_ ctxt false tval_rls t;
|
wenzelm@60309
|
146 |
(*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
|
neuper@37906
|
147 |
|
Walther@60565
|
148 |
val t = TermC.parse_test @{context} "2 * x is_num";
|
walther@60387
|
149 |
val NONE = eval_is_num "" "" t (@{theory "Isac_Knowledge"});
|
neuper@37906
|
150 |
|
neuper@37906
|
151 |
|
neuper@38032
|
152 |
"----------- check calculate bottom up ------------------";
|
neuper@38032
|
153 |
"----------- check calculate bottom up ------------------";
|
neuper@38032
|
154 |
"----------- check calculate bottom up ------------------";
|
neuper@37906
|
155 |
(*-------------- eval_cancel works: *)
|
akargl@42188
|
156 |
val thy = @{theory Test};
|
wneuper@59384
|
157 |
val rls = Test_simplify;
|
Walther@60424
|
158 |
val t = TermC.parseNEW' ctxt "(-4) / 2";
|
akargl@42188
|
159 |
|
wenzelm@60309
|
160 |
val SOME (_, t) = eval_cancel "xxx" \<^const_name>\<open>divide\<close> t thy;
|
akargl@42188
|
161 |
|
neuper@37906
|
162 |
(*--------------(5): reproduce (1) with simpler term: ------------*)
|
Walther@60424
|
163 |
val t = TermC.parseNEW' ctxt "(3+5)/(2::real)";
|
Walther@60500
|
164 |
case rewrite_set_ ctxt false rls t of
|
walther@60317
|
165 |
SOME (t', []) =>
|
walther@60317
|
166 |
if UnparseC.term t' = "4" then ()
|
walther@60317
|
167 |
else error "rewrite_set_ (3+5)/2 changed 1"
|
walther@60317
|
168 |
| _ => error "rewrite_set_ (3+5)/2 changed 2";
|
neuper@37906
|
169 |
|
Walther@60424
|
170 |
val t = TermC.parseNEW' ctxt "(3+1+2*x)/(2::real)";
|
Walther@60500
|
171 |
case rewrite_set_ ctxt false rls t of
|
walther@60356
|
172 |
SOME (t', _) =>
|
walther@60324
|
173 |
if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
|
walther@60317
|
174 |
| _ => error "rewrite_set_ (3+1+2*x)/2 changed 2";
|
neuper@37906
|
175 |
|
Walther@60500
|
176 |
(*--- trace_rewrite before correction of ... --------------------
|
walther@60329
|
177 |
val ct = "(-3 + 2 * x + - 1) / 2";
|
neuper@37906
|
178 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
neuper@37906
|
179 |
:
|
neuper@37906
|
180 |
### trying thm 'root_ge0_2'
|
walther@60329
|
181 |
### rewrite_set_: x + (- 1 + -3) / 2
|
neuper@37906
|
182 |
### trying thm 'radd_real_const_eq'
|
neuper@37906
|
183 |
### trying thm 'radd_real_const'
|
neuper@37906
|
184 |
### rewrite_set_: x + (-4) / 2
|
neuper@37906
|
185 |
### trying thm 'rcollect_right'
|
neuper@37906
|
186 |
:
|
neuper@37906
|
187 |
"x + (-4) / 2"
|
neuper@37906
|
188 |
-------------------------------------while before Isabelle20002:
|
walther@60329
|
189 |
val ct = "(#-3 + #2 * x + #- 1) // #2";
|
neuper@37906
|
190 |
val (ct,_) = the (rewrite_set thy' false rls ct);
|
neuper@37906
|
191 |
:
|
neuper@37906
|
192 |
### trying thm 'root_ge0_2'
|
walther@60329
|
193 |
### rewrite_set_: x + (#- 1 + #-3) // #2
|
neuper@37906
|
194 |
### trying thm 'radd_real_const_eq'
|
neuper@37906
|
195 |
### trying thm 'radd_real_const'
|
neuper@37906
|
196 |
### rewrite_set_: x + #-4 // #2
|
walther@60329
|
197 |
### rewrite_set_: x + #- 2
|
neuper@37906
|
198 |
### trying thm 'rcollect_right'
|
neuper@37906
|
199 |
:
|
walther@60329
|
200 |
"#- 2 + x"
|
neuper@37906
|
201 |
-----------------------------------------------------------------*)
|
neuper@37906
|
202 |
|
neuper@37906
|
203 |
|
neuper@37906
|
204 |
(*===================*)
|
Walther@60424
|
205 |
val t = TermC.parseNEW' ctxt "x + (- 1 + -3) / (2::real)";
|
Walther@60500
|
206 |
val SOME (res, []) = rewrite_set_ ctxt false rls t;
|
walther@60329
|
207 |
if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_ x + (- 1 + -3) / 2 changed";
|
neuper@37906
|
208 |
"x + (-4) / 2";
|
neuper@37906
|
209 |
(*
|
neuper@37906
|
210 |
### trying calc. 'cancel'
|
neuper@37906
|
211 |
@@@ get_pair: binop, t = x + (-4) / 2
|
neuper@37906
|
212 |
@@@ get_pair: t else
|
neuper@38032
|
213 |
@@@ get_pair: t else -> NONE
|
neuper@37906
|
214 |
@@@ get_pair: binop, t = (-4) / 2
|
neuper@37906
|
215 |
@@@ get_pair: then 1
|
neuper@38032
|
216 |
@@@ get_pair: t -> NONE
|
neuper@38032
|
217 |
@@@ get_pair: t1 -> NONE
|
wneuper@59255
|
218 |
@@@ adhoc_thm': NONE
|
neuper@37906
|
219 |
### trying calc. 'pow'
|
neuper@37906
|
220 |
*)
|
neuper@37906
|
221 |
|
walther@59902
|
222 |
" ================= evaluate.sml: calculate_ 2002 =================== ";
|
walther@59902
|
223 |
" ================= evaluate.sml: calculate_ 2002 =================== ";
|
walther@59902
|
224 |
" ================= evaluate.sml: calculate_ 2002 =================== ";
|
neuper@37906
|
225 |
|
akargl@42188
|
226 |
val thy = @{theory Test};
|
Walther@60424
|
227 |
val t = TermC.parseNEW' ctxt "12 / 3";
|
Walther@60519
|
228 |
val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
|
Walther@60500
|
229 |
val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
|
neuper@37906
|
230 |
"12 / 3 = 4";
|
akargl@42188
|
231 |
val thy = @{theory Test};
|
Walther@60424
|
232 |
val t = TermC.parseNEW' ctxt "4 \<up> 2";
|
Walther@60519
|
233 |
val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
|
Walther@60500
|
234 |
val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
|
neuper@37906
|
235 |
"4 ^ 2 = 16";
|
neuper@37906
|
236 |
|
Walther@60424
|
237 |
val t = TermC.parseNEW' ctxt "((1 + 2) * 4 / 3) \<up> 2";
|
Walther@60519
|
238 |
val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
|
neuper@37906
|
239 |
"1 + 2 = 3";
|
Walther@60500
|
240 |
val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
|
walther@59868
|
241 |
UnparseC.term t;
|
walther@60242
|
242 |
"(3 * 4 / 3) \<up> 2";
|
Walther@60519
|
243 |
val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
|
neuper@37906
|
244 |
"3 * 4 = 12";
|
Walther@60500
|
245 |
val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
|
walther@59868
|
246 |
UnparseC.term t;
|
walther@60242
|
247 |
"(12 / 3) \<up> 2";
|
Walther@60519
|
248 |
val SOME (thmID,thm) =adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
|
neuper@37906
|
249 |
"12 / 3 = 4";
|
Walther@60500
|
250 |
val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
|
walther@59868
|
251 |
UnparseC.term t;
|
walther@60242
|
252 |
"4 \<up> 2";
|
Walther@60519
|
253 |
val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
|
walther@60242
|
254 |
"4 \<up> 2 = 16";
|
Walther@60500
|
255 |
val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
|
walther@59868
|
256 |
UnparseC.term t;
|
neuper@37906
|
257 |
"16";
|
walther@59902
|
258 |
if it <> "16" then error "evaluate.sml: new behaviour in calculate_"
|
neuper@37906
|
259 |
else ();
|
neuper@37906
|
260 |
|
neuper@37906
|
261 |
(*13.9.02 *** calc: operator = pow not defined*)
|
Walther@60424
|
262 |
val t = TermC.parseNEW' ctxt "3 \<up> 2";
|
neuper@38032
|
263 |
val SOME (thmID,thm) =
|
Walther@60519
|
264 |
adhoc_thm ctxt (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
|
neuper@37906
|
265 |
(*** calc: operator = pow not defined*)
|
neuper@37906
|
266 |
|
walther@59686
|
267 |
val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
|
neuper@37906
|
268 |
(*
|
wenzelm@60405
|
269 |
val op_ = \<^const_name>\<open>realpow\<close> : string
|
neuper@37906
|
270 |
val eval_fn = fn : string -> term -> theory -> (string * term) option*)
|
neuper@37906
|
271 |
|
Walther@60504
|
272 |
val SOME (thmid,t') = get_pair ctxt op_ eval_fn t;
|
neuper@37906
|
273 |
(*** calc: operator = pow not defined*)
|
neuper@37906
|
274 |
|
Walther@60504
|
275 |
val SOME (id,t') = eval_fn op_ t ctxt;
|
neuper@37906
|
276 |
(*** calc: operator = pow not defined*)
|
neuper@37906
|
277 |
|
walther@60317
|
278 |
case (op_, t) of
|
wenzelm@60405
|
279 |
(\<^const_name>\<open>realpow\<close>,
|
wenzelm@60405
|
280 |
Const (\<^const_name>\<open>realpow\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
|
walther@60336
|
281 |
(Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
|
walther@60317
|
282 |
| _ => error "3 \<up> 2 CHANGED";
|
Walther@60516
|
283 |
val SOME (id, t') = Calc_Binop.numeric thmid op_ t ctxt;
|
neuper@37906
|
284 |
(*** calc: operator = pow not defined*)
|
neuper@37906
|
285 |
|
walther@60317
|
286 |
if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop 3 \<up> 2 = 9 CHANGED";
|
walther@60317
|
287 |
|
walther@60317
|
288 |
|
walther@60317
|
289 |
"----------- fun cancel_int --------------------------------------------------------------------";
|
walther@60317
|
290 |
"----------- fun cancel_int --------------------------------------------------------------------";
|
walther@60317
|
291 |
"----------- fun cancel_int --------------------------------------------------------------------";
|
walther@60317
|
292 |
if cancel_int (~4, 2) = (~1, (2, 1)) then () else error "cancel_int (~4, 2) CHANGED";
|
walther@60317
|
293 |
if cancel_int (4, ~8) = (~1, (1, 2)) then () else error "cancel_int (4, ~8) CHANGED";
|
walther@60317
|
294 |
if cancel_int (6, 4) = (1, (3, 2)) then () else error "cancel_int (6, 4)CHANGED";
|
walther@60317
|
295 |
|
walther@60317
|
296 |
|
Walther@60516
|
297 |
"----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
|
Walther@60516
|
298 |
"----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
|
Walther@60516
|
299 |
"----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
|
walther@60401
|
300 |
val t = @{term "2 + 3 ::real"};
|
walther@60317
|
301 |
|
Walther@60516
|
302 |
"~~~~~ fun Calc_Binop.simplify , args:"; val (thy, lhs) = (@{theory}, t);
|
walther@60401
|
303 |
val simp_ctxt =
|
walther@60401
|
304 |
Proof_Context.init_global thy
|
wenzelm@60407
|
305 |
|> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
|
walther@60401
|
306 |
val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);
|
walther@60317
|
307 |
|
walther@60401
|
308 |
if ThmC.string_of_thm eq = "2 + 3 \<equiv> 5" then () else error "calcul 1";
|
walther@60317
|
309 |
|
walther@60401
|
310 |
val rhs = Thm.term_of (Thm.rhs_of eq);
|
walther@60401
|
311 |
val _ = \<^assert> (is_num rhs);
|
walther@60317
|
312 |
|
walther@60401
|
313 |
(*return value*) rhs;
|
walther@60401
|
314 |
if TermC.to_string rhs = "5" then () else error "calcul 2";
|
walther@60317
|
315 |
|
akargl@42188
|
316 |
|
neuper@37906
|
317 |
"----------- get_pair with 3 args --------------------------------";
|
neuper@37906
|
318 |
"----------- get_pair with 3 args --------------------------------";
|
neuper@37906
|
319 |
"----------- get_pair with 3 args --------------------------------";
|
neuper@37906
|
320 |
val (thy, op_, ef, arg) =
|
walther@60278
|
321 |
(thy, "EqSystem.occur_exactly_in",
|
Walther@60550
|
322 |
get_calc (@{theory "EqSystem"} |> Proof_Context.init_global) "occur_exactly_in" |> snd |> snd,
|
Walther@60565
|
323 |
TermC.parse_test @{context}
|
walther@60329
|
324 |
"[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2"
|
neuper@37906
|
325 |
);
|
Walther@60504
|
326 |
val SOME (str, simpl) = get_pair ctxt op_ ef arg;
|
neuper@37906
|
327 |
if str =
|
walther@60317
|
328 |
"[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2 = True"
|
walther@59902
|
329 |
then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in";
|
neuper@37906
|
330 |
|
neuper@37906
|
331 |
|
walther@60387
|
332 |
"----------- calculate (2 * x is_num) -------------------";
|
walther@60387
|
333 |
"----------- calculate (2 * x is_num) -------------------";
|
walther@60387
|
334 |
"----------- calculate (2 * x is_num) -------------------";
|
Walther@60565
|
335 |
val t = TermC.parse_test @{context} "(2::real) * x is_num";
|
walther@60387
|
336 |
|
walther@60387
|
337 |
val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t @{theory Test};
|
walther@60387
|
338 |
if UnparseC.term t' = "(2 * x is_num) = False" then ()
|
walther@60387
|
339 |
else error "is_num 2 * x is_num CHANGED";
|
neuper@37906
|
340 |
|
Walther@60500
|
341 |
val SOME (t',_) = rewrite_set_ ctxt false tval_rls t;
|
walther@60317
|
342 |
if UnparseC.term t' = "False" then ()
|
walther@60387
|
343 |
else error "rewrite_set_ 2 * x is_num CHANGED";
|
wneuper@59387
|
344 |
|
wneuper@59387
|
345 |
"----------- fun get_pair: examples ------------------------------------------------------------";
|
wneuper@59387
|
346 |
"----------- fun get_pair: examples ------------------------------------------------------------";
|
wneuper@59387
|
347 |
"----------- fun get_pair: examples ------------------------------------------------------------";
|
wneuper@59388
|
348 |
val thy = @{theory};
|
Walther@60550
|
349 |
val ctxt = @{context};
|
walther@59686
|
350 |
val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
|
walther@60317
|
351 |
if isa_str = "Groups.plus_class.plus" then () else error "eval_fn PLUS changed";
|
wneuper@59388
|
352 |
|
walther@60317
|
353 |
val t = @{term "3 + 4 :: real"};
|
Walther@60504
|
354 |
val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
|
walther@60317
|
355 |
(*+*)if str = "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7"
|
walther@60317
|
356 |
(*+*)then () else error "get_pair 3 + 4 changed";
|
wneuper@59388
|
357 |
|
walther@60317
|
358 |
val t = @{term "(a + 3) + 4 :: real"};
|
Walther@60504
|
359 |
val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
|
walther@59868
|
360 |
if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
|
wneuper@59388
|
361 |
then () else error "get_pair (a + 3) + 4 changed";
|
wneuper@59388
|
362 |
|
walther@60317
|
363 |
val t = @{term "(a + 3) + 4 :: real"};
|
Walther@60504
|
364 |
val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
|
walther@59868
|
365 |
if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
|
wneuper@59388
|
366 |
then () else error "get_pair (a + 3) + 4 changed";
|
wneuper@59388
|
367 |
|
walther@60317
|
368 |
val t = @{term "x = 5 * (3 + (4 + a) :: real)"};
|
Walther@60504
|
369 |
val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
|
walther@59868
|
370 |
if str = "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a"
|
wneuper@59388
|
371 |
then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed";
|
wneuper@59388
|
372 |
|
walther@59686
|
373 |
val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
|
wneuper@59388
|
374 |
|
walther@60329
|
375 |
val t = @{term "-4 / - 2 :: real"};
|
Walther@60504
|
376 |
val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
|
walther@60317
|
377 |
if str = "#divide_e~4_~2" andalso UnparseC.term term = "- 4 / - 2 = 2"
|
walther@60329
|
378 |
then () else error "get_pair -4 / - 2 changed";
|
wneuper@59388
|
379 |
|
walther@59686
|
380 |
val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
|
wneuper@59388
|
381 |
|
walther@60317
|
382 |
val t = @{term "2 \<up> 3 :: real"};
|
Walther@60504
|
383 |
val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
|
walther@60242
|
384 |
if str = "#: 2 \<up> 3 = 8" andalso UnparseC.term term = "2 \<up> 3 = 8"
|
walther@60242
|
385 |
then () else error "get_pair 2 \<up> 3 changed";
|
wneuper@59388
|
386 |
|
wneuper@59387
|
387 |
"----------- fun adhoc_thm: examples -----------------------------------------------------------";
|
wneuper@59387
|
388 |
"----------- fun adhoc_thm: examples -----------------------------------------------------------";
|
wneuper@59387
|
389 |
"----------- fun adhoc_thm: examples -----------------------------------------------------------";
|
wneuper@59388
|
390 |
(*--------------------------------------------------------------------vvvvvvvvvv*)
|
walther@60387
|
391 |
val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_num");
|
walther@60387
|
392 |
val t = @{term "9 is_num"};
|
Walther@60519
|
393 |
val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
|
walther@60387
|
394 |
if str = "#is_num_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_num) = True"
|
walther@60387
|
395 |
then () else error "adhoc_thm 9 is_num changed";
|
wneuper@59387
|
396 |
|
Walther@60550
|
397 |
case get_calc_prog_id ctxt \<^const_name>\<open>less\<close> of
|
wneuper@59388
|
398 |
"le" => () | _ => error "Orderings.ord_class.less <-> le changed";
|
walther@59686
|
399 |
val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le");
|
walther@60317
|
400 |
if isa_str = "Orderings.ord_class.less" then () else error "adhoc_thm (4 < 4) = False CHANGED";
|
wneuper@59387
|
401 |
|
walther@60317
|
402 |
val t = @{term "4 < (4 :: real)"};
|
Walther@60519
|
403 |
val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
|
walther@59876
|
404 |
if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"
|
wneuper@59388
|
405 |
then () else error "adhoc_thm 4 < 4 changed";
|
wneuper@59387
|
406 |
|
wneuper@59388
|
407 |
val SOME t = parseNEW @{context} "a < 4";
|
Walther@60519
|
408 |
case adhoc_thm ctxt (isa_str, eval_fn) t of
|
wneuper@59388
|
409 |
NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE";
|
wneuper@59387
|
410 |
|
walther@59686
|
411 |
val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
|
walther@60317
|
412 |
val SOME t = parseNEW @{context} "1 + (2::real)";
|
Walther@60519
|
413 |
val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
|
walther@59876
|
414 |
if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
|
wneuper@59388
|
415 |
then () else error "adhoc_thm 1 + 2 changed";
|
wneuper@59387
|
416 |
|
walther@59686
|
417 |
val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
|
walther@60317
|
418 |
val t = @{term "6 / -8 :: real"};
|
Walther@60519
|
419 |
val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
|
walther@60317
|
420 |
if str = "#divide_e6_~8" andalso ThmC_Def.string_of_thm thm = "6 / - 8 = - 3 / 4"
|
walther@60317
|
421 |
then () else error "adhoc_thm 6 / -8 = - 3 / 4 changed";
|
wneuper@59387
|
422 |
|
Walther@60550
|
423 |
case get_calc_prog_id ctxt "Prog_Expr.ident" of
|
walther@59603
|
424 |
"ident" => () | _ => error "Prog_Expr.ident <-> ident changed";
|
walther@59686
|
425 |
val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");
|
wneuper@59387
|
426 |
|
walther@60317
|
427 |
val t = @{term "3 =!= (3 :: real)"};
|
Walther@60519
|
428 |
val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
|
walther@59876
|
429 |
if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"
|
wneuper@59388
|
430 |
then () else error "adhoc_thm (3 =!= 3) changed";
|
wneuper@59387
|
431 |
|
walther@60317
|
432 |
val t = @{term "\<not> ((4 :: real) + (4 * x + x \<up> 2) =!= 0)"};
|
Walther@60519
|
433 |
val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
|
walther@60317
|
434 |
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"
|
wneuper@59388
|
435 |
then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
|
wneuper@59403
|
436 |
|
walther@60391
|
437 |
"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
|
walther@60391
|
438 |
"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
|
walther@60391
|
439 |
"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
|
Walther@60538
|
440 |
val eval_ = ("Rings.divide_class.divide", eval_cancel "#divide_e" : Eval.ml_fun): Eval.ml;
|
walther@60391
|
441 |
val t = @{term "- 1 / 2 ::real"};
|
walther@60391
|
442 |
(*
|
walther@60391
|
443 |
ML\<open>Eval.adhoc_thm\<close> is called while searching terms for adjacent numerals
|
walther@60391
|
444 |
given a certain ML_type\<open>eval_fn\<close> and a certain ML\<open>term\<close> ..
|
walther@60391
|
445 |
|
walther@60391
|
446 |
THE ERROR WAS:
|
walther@60391
|
447 |
rew_once:
|
walther@60391
|
448 |
Eval.get_pair for \<^const_name>\<open>divide\<close> \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2")
|
walther@60391
|
449 |
but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE
|
walther@60391
|
450 |
|
walther@60391
|
451 |
STEP-INTO BEVORE REMOVING THE ERROR:
|
walther@60391
|
452 |
val SOME ("#divide_e~1_2", adhoc_thm) =
|
Walther@60519
|
453 |
Eval.adhoc_thm @{context} eval_ t;
|
walther@60391
|
454 |
"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
|
walther@60391
|
455 |
val SOME
|
walther@60391
|
456 |
("#divide_e~1_2", t'') =
|
Walther@60504
|
457 |
(*case*) get_pair ctxt op_ eval_fn t (*of*);
|
walther@60391
|
458 |
(*
|
walther@60391
|
459 |
get_pair finds two adjacent numerals and does NOT distinguish between different kinds of
|
walther@60391
|
460 |
\<^ML_type>\<open>eval_fn\<close>. In case of \<^ML>\<open>eval_cancel\<close> the return value WAS the same as the input..
|
walther@60391
|
461 |
*)
|
walther@60391
|
462 |
(*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2"
|
walther@60391
|
463 |
*)
|
walther@60391
|
464 |
|
Walther@60519
|
465 |
val NONE = adhoc_thm @{context} eval_ t;
|
walther@60393
|
466 |
"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
|
walther@60391
|
467 |
val NONE =
|
Walther@60504
|
468 |
(*case*) get_pair ctxt op_ eval_fn t (*of*);
|
walther@60391
|
469 |
|
walther@60391
|
470 |
|
walther@60329
|
471 |
"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
|
walther@60329
|
472 |
"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
|
walther@60329
|
473 |
"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
|
Walther@60565
|
474 |
val t = TermC.parse_test @{context} "sqrt 4";
|
Walther@60519
|
475 |
Eval.adhoc_thm @{context} ("NthRoot.sqrt", eval_sqrt "#sqrt_") t;
|
walther@60329
|
476 |
|
walther@60329
|
477 |
"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
|
walther@60329
|
478 |
((ThyC.get_theory "Isac_Knowledge"),
|
Walther@60504
|
479 |
("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> Proof.context -> (string * term) option), t);
|
walther@60356
|
480 |
|
walther@60329
|
481 |
val SOME (thmid, t) =
|
Walther@60504
|
482 |
(*case*) get_pair ctxt op_ eval_fn ct (*of*);
|
walther@60356
|
483 |
(*+*)val "sqrt 4 = 2" = UnparseC.term t;
|
walther@60356
|
484 |
|
walther@60329
|
485 |
(** )
|
walther@60356
|
486 |
Skip_Proof.make_thm thy t;
|
walther@60356
|
487 |
|
walther@60329
|
488 |
exception TYPE raised (line 169 of "consts.ML"): Illegal type
|
walther@60329
|
489 |
for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
|
walther@60329
|
490 |
( **)
|
walther@60329
|
491 |
|
wneuper@59403
|
492 |
"----------- fun power -------------------------------------------------------------------------";
|
wneuper@59403
|
493 |
"----------- fun power -------------------------------------------------------------------------";
|
wneuper@59403
|
494 |
"----------- fun power -------------------------------------------------------------------------";
|
wneuper@59403
|
495 |
if power 2 3 = 8 then () else error "power 2 3 = 8";
|
wneuper@59403
|
496 |
if power ~2 3 = ~8 then () else error "power ~2 3 = ~8";
|
wneuper@59403
|
497 |
if power ~3 2 = 9 then () else error "power ~3 2 = 9";
|
walther@60270
|
498 |
case \<^try>\<open> power 3 ~2 \<close> of
|
walther@60270
|
499 |
SOME _ => raise error "power 3 ~2: should raise an exn 1"
|
walther@60271
|
500 |
| NONE => ();
|
wneuper@59403
|
501 |
|
wneuper@59403
|
502 |
"----------- fun divisors ----------------------------------------------------------------------";
|
wneuper@59403
|
503 |
"----------- fun divisors ----------------------------------------------------------------------";
|
wneuper@59403
|
504 |
"----------- fun divisors ----------------------------------------------------------------------";
|
wneuper@59403
|
505 |
if divisors 30 = [5, 3, 2] then () else error "divisors 30 = [5, 3, 2]";
|
wneuper@59403
|
506 |
if divisors 32 = [2, 2, 2, 2, 2] then () else error "divisors 32 = [2, 2, 2, 2, 2]";
|
wneuper@59403
|
507 |
if divisors 60 = [5, 3, 2, 2] then () else error "divisors 60 = [5, 3, 2, 2]";
|
wneuper@59403
|
508 |
if divisors 11 = [11] then () else error "divisors 11 = [11]";
|
wneuper@59403
|
509 |
|
wneuper@59403
|
510 |
"----------- fun doubles, fun squfact ----------------------------------------------------------";
|
wneuper@59403
|
511 |
"----------- fun doubles, fun squfact ----------------------------------------------------------";
|
wneuper@59403
|
512 |
"----------- fun doubles, fun squfact ----------------------------------------------------------";
|
wneuper@59403
|
513 |
if doubles [2,3,4] = [] then () else error "doubles [2,3,4] changed";
|
wneuper@59403
|
514 |
if doubles [2,3,3,5,5,7] = [5, 3] then () else error "doubles [2,3,3,5,5,7] changed";
|
wneuper@59403
|
515 |
|
wneuper@59403
|
516 |
if squfact 30 = 1 then () else error "squfact 30 changed";
|
wneuper@59403
|
517 |
if squfact 32 = 4 then () else error "squfact 32 changed";
|
wneuper@59403
|
518 |
if squfact 60 = 2 then () else error "squfact 60 changed";
|
wneuper@59403
|
519 |
if squfact 11 = 1 then () else error "squfact 11 changed";
|