1 (* Title: ProgLang/program.sml
2 Author: Walther Neuper 190922
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "-----------------------------------------------------------------------------------------------";
8 "table of contents -----------------------------------------------------------------------------";
9 "-----------------------------------------------------------------------------------------------";
10 "-------- fun eval_is_atom ---------------------------------------------------------------------";
11 "-------- fun eval_is_even ---------------------------------------------------------------------";
12 "-------- fun eval_is_num ----------------------------------------------------------------------";
13 "-------- fun eval_cancel ----------------------------------------------------------------------";
14 "-------- fun eval_equ -------------------------------------------------------------------------";
15 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
16 "-------- occurs_in ----------------------------------------------------------------------------";
17 "-------- fun eval_occurs_in -------------------------------------------------------------------";
18 "-------- fun eval_argument_of -----------------------------------------------------------------";
19 "-------- fun eval_sameFunId -------------------------------------------------------------------";
20 "-------- fun eval_filter_sameFunId ------------------------------------------------------------";
21 "-------- fun eval_boollist2sum ----------------------------------------------------------------";
22 "-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
23 "-------- fun matchsub -------------------------------------------------------------------------";
24 "-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
25 "-----------------------------------------------------------------------------------------------";
26 "-----------------------------------------------------------------------------------------------";
27 "-----------------------------------------------------------------------------------------------";
30 "-------- fun eval_is_atom ---------------------------------------------------------------------";
31 "-------- fun eval_is_atom ---------------------------------------------------------------------";
32 "-------- fun eval_is_atom ---------------------------------------------------------------------";
33 if is_atom @{term 0} then () else error "is_atom 0 CHANGED";
34 val eval_t = @{term "0 is_atom"};
35 case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
36 SOME ("#is_atom_0_", _) => ()
37 | _ => error "eval_is_atom 0 CHANGED";
39 if is_atom @{term 1} then () else error "is_atom 1 CHANGED";
40 val eval_t = @{term "1 is_atom"};
41 case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
42 SOME ("#is_atom_1_", _) => ()
43 | _ => error "eval_is_atom 1 CHANGED";
45 if is_atom @{term 123} then () else error "is_atom 123 CHANGED";
46 val eval_t = @{term "123 is_atom"};
47 case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
48 SOME ("#is_atom_123_", _) => ()
49 | _ => error "eval_is_atom 123 CHANGED";
51 if is_atom @{term abc} then () else error "is_atom abc CHANGED";
52 val eval_t = @{term "abc is_atom"};
53 case Prog_Expr.eval_is_atom "#is_atom_" "Prog_Expr.is_atom" eval_t () of
54 SOME ("#is_atom_abc_", _) => ()
55 | _ => error "eval_is_atom abc CHANGED";
58 "-------- fun eval_is_even ---------------------------------------------------------------------";
59 "-------- fun eval_is_even ---------------------------------------------------------------------";
60 "-------- fun eval_is_even ---------------------------------------------------------------------";
61 val t = TermC.parse_test @{context} "2 is_even";
62 eval_is_even "aaa" "Prog_Expr.is_even" t "ccc";
63 "~~~~~ fun eval_is_even , args:"; val ((thmid:string), "Prog_Expr.is_even", (t as (Const _ $ arg)), _) =
64 ("aaa", "Prog_Expr.is_even", t, "ccc");
65 (*if*) TermC.is_num arg (*then*);
66 val i = arg |> HOLogic.dest_number |> snd;
67 (*if*) even i (*then*);
68 val SOME ("aaa1_", t') =
69 SOME (TermC.mk_thmid thmid (string_of_int n) "",
70 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})));
71 if UnparseC.term t' = "(2 is_even) = True" then () else error "(2 is_even) = True CHANGED";
74 val t = TermC.parse_test @{context} "3 is_even";
75 case eval_is_even "aaa" "Prog_Expr.is_even" t "ccc" of
77 if str = "aaa_" andalso UnparseC.term t' = "(3 is_even) = False" then ()
78 else error "eval_is_even (3 is_even) CHANGED 1"
79 | NONE => error "eval_is_even (3 is_even) CHANGED 2";
81 val t = TermC.parse_test @{context} "a ::real";
83 eval_is_even "aaa" "Prog_Expr.is_even" t "ccc";
84 case eval_is_even "aaa" "Prog_Expr.is_even" t "ccc" of
85 SOME _ => error "eval_is_even (a is_even) CHANGED"
89 "-------- fun eval_is_num ----------------------------------------------------------------------";
90 "-------- fun eval_is_num ----------------------------------------------------------------------";
91 "-------- fun eval_is_num ----------------------------------------------------------------------";
92 val ctxt = Proof_Context.init_global @{theory Test}
93 val t = TermC.parseNEW' ctxt "2 is_num";
94 case rewrite_set_ ctxt false tval_rls t of
95 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
96 | _ => error "2 is_num CHANGED";
98 val t = TermC.parse_test @{context} "2 * x is_num";
99 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
100 if UnparseC.term t' = "(2 * x is_num) = False" then ()
101 else error "(2 * x is_num) = False CHANGED";
103 val t = TermC.parse_test @{context} "- 2 is_num";
104 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
105 if UnparseC.term t' = "(- 2 is_num) = True" then ()
106 else error "(- 2 is_num) = False CHANGED";
108 val t = TermC.parse_test @{context} "- 1 is_num";
109 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
110 if UnparseC.term t' = "(- 1 is_num) = True" then ()
111 else error "(- 1 is_num) = False CHANGED";
113 val t = TermC.parse_test @{context} "0 is_num";
114 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
115 if UnparseC.term t' = "(0 is_num) = True" then ()
116 else error "(0 is_num) = False CHANGED";
118 val t = TermC.parse_test @{context} "AA is_num";
119 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"});
120 if UnparseC.term t' = "(AA is_num) = False" then ()
121 else error "(0 is_num) = False CHANGED";
124 "-------- fun eval_cancel ----------------------------------------------------------------------";
125 "-------- fun eval_cancel ----------------------------------------------------------------------";
126 "-------- fun eval_cancel ----------------------------------------------------------------------";
127 val t = @{term "- 1 / 2 :: real"};
128 val NONE = eval_cancel "cancel_" "Rings.divide_class.divide" t "";
129 "~~~~~ fun eval_cancel , args:"; val (thmid, "Rings.divide_class.divide", (t as (Const _ $ t1 $ t2))) =
130 ("xxx", "Rings.divide_class.divide", t);
131 (*if*) TermC.is_num t1 andalso TermC.is_num t2 (*then*);
132 val (T, _) = HOLogic.dest_number t1;
133 val (i1, i2) = (Eval.int_of_numeral t1, Eval.int_of_numeral t2);
134 val res_int as (d, (i1', i2')) = Eval.cancel_int (i1, i2);
136 (*+*)val (~1, (1, 2)) = res_int;
138 (*if*) abs d = 1 andalso (abs i1, abs i2) = (abs i1', abs i2') (*then*);
139 NONE (*return value*);
141 "-------- further examples ";
142 val t = @{term "3 / 2 :: real"};
143 val NONE = eval_cancel "cancel_" "Rings.divide_class.divide" t ""
145 val t = @{term "6 / 4 :: real"};
146 case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of
147 SOME ("cancel_6_4", t') =>
148 if UnparseC.term t' = "6 / 4 = 3 / 2" then ()
149 else error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 1"
150 | _ => error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 2";
152 val t = @{term "- 6 / 4 :: real"};
153 case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of
154 SOME ("cancel_~6_4", t') =>
155 if UnparseC.term t' = "- 6 / 4 = - 3 / 2" then ()
156 else error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 1"
157 | _ => error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 2";
159 val t = @{term "6 / - 4 :: real"};
160 case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of
161 SOME ("cancel_6_~4", t') =>
162 if UnparseC.term t' = "6 / - 4 = - 3 / 2" then ()
163 else error "eval_cancel 6 / - 4 = - 3 / 2 CHANGED 1"
164 | _ => error "eval_cancel 6 / - 4 = - 3 / 2 CHANGED 2";
166 val t = @{term "- 6 /- 4 :: real"};
167 case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of
168 SOME ("cancel_~6_~4", t') =>
169 if UnparseC.term t' = "- 6 / - 4 = 3 / 2" then ()
170 else error "eval_cancel - 6 / - 4 = 3 / 2 CHANGED 1"
171 | _ => error "eval_cancel - 6 / - 4 = 3 / 2 CHANGED 2";
173 val t = @{term "- (6 / 4) :: real"};
174 val NONE = eval_cancel "adhoc_thm_cancel" "Rings.divide_class.divide" t "";
177 "-------- fun eval_equ -------------------------------------------------------------------------";
178 "-------- fun eval_equ -------------------------------------------------------------------------";
179 "-------- fun eval_equ -------------------------------------------------------------------------";
180 eval_equ: string -> string -> term -> 'a -> (string * term) option;
182 case eval_equ "#less_" "Orderings.ord_class.less" @{term "1 < (2::real)"} "" of
185 Const (\<^const_name>\<open>Trueprop\<close>, _) $
186 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
187 (Const (\<^const_name>\<open>ord_class.less\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) $
188 (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) $
189 Const (\<^const_name>\<open>True\<close>, _))) => ()
190 | _ => error "eval_equ 1 < 2 CHANGED";
192 case eval_equ "#less_" "Orderings.ord_class.less" @{term "1 < (1::real)"} "" of
195 Const (\<^const_name>\<open>Trueprop\<close>, _) $
196 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>ord_class.less\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _)) $
197 Const (\<^const_name>\<open>False\<close>, _))) => ()
198 | _ => error "eval_equ 1 < 1 CHANGED";
201 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
202 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
203 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
205 val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge")
207 val t = TermC.parse_test @{context} "x = 0";
208 val NONE(*= indetermined*) = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
210 val t = TermC.parse_test @{context} "(x + 1) = (x + 1)";
211 val (Const _(*op0,t0*) $ t1 $ t2 ) = t
212 val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
213 if UnparseC.term t' = "(x + 1 = x + 1) = True" then () else error "(x + 1) = (x + 1) CHANGED";
215 val t as Const _ $ v $ c = TermC.parse_test @{context} "1 = 0";
216 val false = variable_constant_pair (v, c);
217 val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
218 if UnparseC.term t' = "(1 = 0) = False" then () else error "1 = 0 CHANGED";
220 val t = TermC.parse_test @{context} "0 = 0";
221 val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
222 if UnparseC.term t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED";
225 "-------- occurs_in ----------------------------------------------------------------------------";
226 "-------- occurs_in ----------------------------------------------------------------------------";
227 "-------- occurs_in ----------------------------------------------------------------------------";
228 val t = @{term "x::real"};
229 if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed";
231 val t = TermC.parse_test @{context} "x occurs_in x";
232 val SOME (str, t') = eval_occurs_in 0 "Prog_Expr.occurs_in" t 0;
233 if UnparseC.term t' = "x occurs_in x = True" then ()
234 else error "x occurs_in x = True ..changed";
236 "------- some_occur_in";
237 if some_occur_in [@{term "c::real"}, @{term "c_2::real"}] @{term "a + b + c::real"} then ()
240 val t = @{term "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2"};
241 val SOME (str, t') = eval_some_occur_in 0 "Prog_Expr.some_occur_in" t 0;
242 if UnparseC.term t' =
243 "some_of [c, c_2, c_3,\n c_4] occur_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 =\nTrue" then ()
244 else error "atools.sml: some_occur_in true";
246 val t = @{term "some_of [c_3, c_4] occur_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2"};
247 val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some_occur_in" t 0;
248 if UnparseC.term t' =
249 "some_of [c_3, c_4] occur_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False" then ()
250 else error "atools.sml: some_occur_in false";
253 "-------- fun eval_occurs_in -------------------------------------------------------------------";
254 "-------- fun eval_occurs_in -------------------------------------------------------------------";
255 "-------- fun eval_occurs_in -------------------------------------------------------------------";
256 val v = TermC.parseNEW' ctxt "x";
257 val t = TermC.parseNEW' ctxt "1";
258 if occurs_in v t then error "factor_right_deg (1) x ..changed" else ();
260 val v = TermC.parseNEW' ctxt "AA";
261 val t = TermC.parseNEW' ctxt "1";
262 if occurs_in v t then error "factor_right_deg (1) AA ..changed" else ();
265 val v = TermC.parseNEW' ctxt "x";
266 val t = TermC.parseNEW' ctxt "a*b+c";
267 if occurs_in v t then error "factor_right_deg (a*b+c) x ..changed" else ();
269 val v = TermC.parseNEW' ctxt "AA";
270 val t = TermC.parseNEW' ctxt "a*b+c";
271 if occurs_in v t then error "factor_right_deg (a*b+c) AA ..changed" else ();
274 val v = TermC.parseNEW' ctxt "x";
275 val t = TermC.parseNEW' ctxt "a*x+c";
276 if occurs_in v t then () else error "factor_right_deg (a*x+c) x ..changed";
278 val v = TermC.parseNEW' ctxt "AA";
279 val t = TermC.parseNEW' ctxt "a*AA+c";
280 if occurs_in v t then () else error "factor_right_deg (a*AA+c) AA ..changed";
283 val v = TermC.parseNEW' ctxt "x";
284 val t = TermC.parseNEW' ctxt "(a*b+c)*x \<up> 7";
285 if occurs_in v t then () else error "factor_right_deg (a*b+c)*x \<up> 7) x ..changed";
287 val v = TermC.parseNEW' ctxt "AA";
288 val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
289 if occurs_in v t then () else error "factor_right_deg (a*b+c)*AA \<up> 7) AA ..changed";
292 val v = TermC.parseNEW' ctxt "x";
293 val t = TermC.parseNEW' ctxt "x \<up> 7";
294 if occurs_in v t then () else error "factor_right_deg (x \<up> 7) x ..changed";
296 val v = TermC.parseNEW' ctxt "AA";
297 val t = TermC.parseNEW' ctxt "AA \<up> 7";
298 if occurs_in v t then () else error "factor_right_deg (AA \<up> 7) AA ..changed";
301 val v = TermC.parseNEW' ctxt "x";
302 val t = TermC.parseNEW' ctxt "(a*b+c)*x";
303 if occurs_in v t then () else error "factor_right_deg ((a*b+c)*x) x ..changed";
305 val v = TermC.parseNEW' ctxt "AA";
306 val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
307 if occurs_in v t then () else error "factor_right_deg ((a*b+c)*AA) AA ..changed";
310 val v = TermC.parseNEW' ctxt "x";
311 val t = TermC.parseNEW' ctxt "(a*b+x)*x";
312 if occurs_in v t then () else error "factor_right_deg ((a*b+x)*x) x ..changed";
314 val v = TermC.parseNEW' ctxt "AA";
315 val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
316 if occurs_in v t then () else error "factor_right_deg ((a*b+AA)*AA) AA ..changed";
319 val v = TermC.parseNEW' ctxt "x";
320 val t = TermC.parseNEW' ctxt "x";
321 if occurs_in v t then () else error "factor_right_deg (x) x ..changed";
323 val v = TermC.parseNEW' ctxt "AA";
324 val t = TermC.parseNEW' ctxt "AA";
325 if occurs_in v t then () else error "factor_right_deg (AA) AA ..changed";
328 val v = TermC.parseNEW' ctxt "x";
329 val t = TermC.parseNEW' ctxt "ab - (a*b)*x";
330 if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*x) x ..changed";
332 val v = TermC.parseNEW' ctxt "AA";
333 val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
334 if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*AA) AA ..changed";
337 "---------fun eval_argument_of -----------------------------------------------------------------";
338 "---------fun eval_argument_of -----------------------------------------------------------------";
339 "---------fun eval_argument_of -----------------------------------------------------------------";
340 val t = TermC.parse_test @{context} "argument_in (M_b x)";
341 val SOME (str, t') = eval_argument_in "0" "Prog_Expr.argument_in" t 0;
342 if UnparseC.term t' = "(argument_in M_b x) = x" then ()
343 else error "atools.sml:(argument_in M_b x) = x ???";
346 "---------fun eval_sameFunId -------------------------------------------------------------------";
347 "---------fun eval_sameFunId -------------------------------------------------------------------";
348 "---------fun eval_sameFunId -------------------------------------------------------------------";
349 val t = @{term "M_b L"}; TermC.atom_trace_detail @{context} t;
350 val t as f1 $ _ = @{term "M_b L"};
351 val t as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _ = @{term "M_b x = c + L*x"};
353 val (p as Const (\<^const_name>\<open>sameFunId\<close>, _) $
355 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _)) =
356 @{term "sameFunId (M_b L) (M_b x = c + L*x)"};
358 eval_sameFunId "" "Prog_Expr.sameFunId"
359 (@{term "sameFunId (M_b L) (M_b x = c + L*x)"})""(*true*);
360 eval_sameFunId "" "Prog_Expr.sameFunId"
361 (@{term "sameFunId (M_b L) ( y' x = c + L*x)"})""(*false*);
362 eval_sameFunId "" "Prog_Expr.sameFunId"
363 (@{term "sameFunId (M_b L) ( y x = c + L*x)"})""(*false*);
364 eval_sameFunId "" "Prog_Expr.sameFunId"
365 (@{term "sameFunId ( y L) (M_b x = c + L*x)"})""(*false*);
366 eval_sameFunId "" "Prog_Expr.sameFunId"
367 (@{term "sameFunId ( y L) ( y x = c + L*x)"})""(*true*);
370 "---------fun eval_filter_sameFunId ------------------------------------------------------------";
371 "---------fun eval_filter_sameFunId ------------------------------------------------------------";
372 "---------fun eval_filter_sameFunId ------------------------------------------------------------";
373 val flhs as (fid $ _) = @{term "y' L"};
374 val fs = @{term "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"};
375 val (p as Const (\<^const_name>\<open>filter_sameFunId\<close>,_) $ (fid $ _) $ fs) =
376 @{term "filter_sameFunId (y' L) [M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"};
377 val SOME (str, es) = eval_filter_sameFunId "" "Prog_Expr.filter_sameFunId" p "";
378 if UnparseC.term es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n y x = c + L * x]) =\n[y' x = c + L * x]" then ()
379 else error "atools.slm diff.behav. in filter_sameFunId";
382 "---------fun eval_boollist2sum ----------------------------------------------------------------";
383 "---------fun eval_boollist2sum ----------------------------------------------------------------";
384 "---------fun eval_boollist2sum ----------------------------------------------------------------";
385 fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
386 | lhs t = error("lhs called with (" ^ UnparseC.term t ^ ")");
387 "----------- \<up> redefined due to overwritten identifier -----------";
388 val u_ = @{term "[]"};
389 val u_ = @{term "[b1 = k - 2*q]"};
390 val u_ = @{term "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};
391 val ut_ = isalist2list u_;
392 val sum_ = map lhs ut_;
393 val t = list2sum sum_;
396 val t = @{term "boollist2sum [b1 = k - 2*(q::real), b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};
398 Const (\<^const_name>\<open>boollist2sum\<close>, _) $
399 (Const (\<^const_name>\<open>Cons\<close>, _) $
400 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b1", _) $ _ ) $
401 (Const (\<^const_name>\<open>Cons\<close>, _) $
402 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b2", _) $ _ ) $
403 (Const (\<^const_name>\<open>Cons\<close>, _) $
404 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b3", _) $ _ ) $
405 (Const (\<^const_name>\<open>Cons\<close>, _) $
406 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b4", _) $ _ ) $
407 Const (\<^const_name>\<open>Nil\<close>, _))))) => ()
408 | _ => error "boollist2sum CHANGED";
409 val SOME (str, pred) = eval_boollist2sum "" "Prog_Expr.boollist2sum" t "";
410 if UnparseC.term pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then ()
411 else error "atools.sml diff.behav. in eval_boollist2sum";
413 val srls_ = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty
414 [Eval ("Prog_Expr.boollist2sum", eval_boollist2sum "")];
415 val t = @{term "boollist2sum [b1 = k - 2*(q::real), b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};
416 case rewrite_set_ ctxt false srls_ t of SOME _ => ()
417 | _ => error "atools.sml diff.rewrite boollist2sum";
420 "-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
421 "-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
422 "-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
423 val (op_, ef) = the (LibraryC.assoc (Know_Store.get_calcs @{theory}, "TIMES"));
424 val t = TermC.parseNEW' ctxt "2 * (3::real)";
425 (*val SOME (thmid,t') = *)get_pair ctxt op_ ef t;
427 "~~~~~ fun get_pair, args:"; val(*3*)(thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
429 (*if*) op_ = op0; (*then*)
432 "~~~~~ fun Calc_Binop.numeric , args:"; val ((_ : string), (_: string),
433 (t as (Const (op0, _) $ t1 $ t2)), thy) =
434 ("#mult_", op_, t, thy);
435 val Const (c, _) $ t1 $ t2 = (* binary \<circ> n1 \<circ> n2 *)
437 (*if*) Calc_Binop.is c andalso is_num t1 andalso is_num t2 (*then*);
438 val res = Calc_Binop.simplify ctxt t;
439 val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
440 SOME ("#: " ^ UnparseC.term prop, prop) (*return value*);
442 if "#: " ^ UnparseC.term prop = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()
443 else error "eval_binop changed"
445 val SOME (thmid, tm) = Calc_Binop.numeric "#mult_" op_ t ctxt;
446 if thmid = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()
447 else error "eval_binop changed 2"
450 "-------- fun matchsub -------------------------------------------------------------------------";
451 "-------- fun matchsub -------------------------------------------------------------------------";
452 "-------- fun matchsub -------------------------------------------------------------------------";
453 if matchsub thy (TermC.parse_test @{context} "(a + (b + c))") (TermC.parse_patt_test @{theory} "?x + (?y + ?z)")
454 then () else error "tools.sml matchsub a + (b + c)";
456 if matchsub thy (TermC.parse_test @{context} "(a + (b + c)) + d") (TermC.parse_patt_test @{theory} "?x + (?y + ?z)")
457 then () else error "tools.sml matchsub (a + (b + c)) + d";
460 "-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
461 "-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
462 "-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
463 "see: --------- search for Or_to_List ---";
464 case or2list @{term True} of Const (\<^const_name>\<open>UniversalList\<close>, _) => ()
465 | _ => error "TermC.UniversalList changed 1";
466 case or2list @{term False} of Const (\<^const_name>\<open>Nil\<close>, _) => ()
467 | _ => error "TermC.UniversalList changed 2";
468 val t = (TermC.parse_test @{context} "x=3");
469 if UnparseC.term (or2list t) = "[x = 3]" then ()
470 else error "or2list changed";
471 val t = (TermC.parse_test @{context} "x=3 | x=-3 | x=0");
472 if UnparseC.term (or2list t) = "[x = 3, x = - 3, x = 0]" then ()
473 else error "HOL.eq ? HOL.disj ? changed";