66 val i = arg |> HOLogic.dest_number |> snd; |
66 val i = arg |> HOLogic.dest_number |> snd; |
67 (*if*) even i (*then*); |
67 (*if*) even i (*then*); |
68 val SOME ("aaa1_", t') = |
68 val SOME ("aaa1_", t') = |
69 SOME (TermC.mk_thmid thmid (string_of_int n) "", |
69 SOME (TermC.mk_thmid thmid (string_of_int n) "", |
70 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))); |
70 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))); |
71 if UnparseC.term_in_ctxt @{context} t' = "(2 is_even) = True" then () else error "(2 is_even) = True CHANGED"; |
71 if UnparseC.term @{context} t' = "(2 is_even) = True" then () else error "(2 is_even) = True CHANGED"; |
72 |
72 |
73 |
73 |
74 val t = ParseC.parse_test @{context} "3 is_even"; |
74 val t = ParseC.parse_test @{context} "3 is_even"; |
75 case eval_is_even "aaa" "Prog_Expr.is_even" t "ccc" of |
75 case eval_is_even "aaa" "Prog_Expr.is_even" t "ccc" of |
76 SOME (str, t') => |
76 SOME (str, t') => |
77 if str = "aaa_" andalso UnparseC.term_in_ctxt @{context} t' = "(3 is_even) = False" then () |
77 if str = "aaa_" andalso UnparseC.term @{context} t' = "(3 is_even) = False" then () |
78 else error "eval_is_even (3 is_even) CHANGED 1" |
78 else error "eval_is_even (3 is_even) CHANGED 1" |
79 | NONE => error "eval_is_even (3 is_even) CHANGED 2"; |
79 | NONE => error "eval_is_even (3 is_even) CHANGED 2"; |
80 |
80 |
81 val t = ParseC.parse_test @{context} "a ::real"; |
81 val t = ParseC.parse_test @{context} "a ::real"; |
82 val NONE = |
82 val NONE = |
95 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => () |
95 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => () |
96 | _ => error "2 is_num CHANGED"; |
96 | _ => error "2 is_num CHANGED"; |
97 |
97 |
98 val t = ParseC.parse_test @{context} "2 * x is_num"; |
98 val t = ParseC.parse_test @{context} "2 * x is_num"; |
99 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"}); |
99 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"}); |
100 if UnparseC.term_in_ctxt @{context} t' = "(2 * x is_num) = False" then () |
100 if UnparseC.term @{context} t' = "(2 * x is_num) = False" then () |
101 else error "(2 * x is_num) = False CHANGED"; |
101 else error "(2 * x is_num) = False CHANGED"; |
102 |
102 |
103 val t = ParseC.parse_test @{context} "- 2 is_num"; |
103 val t = ParseC.parse_test @{context} "- 2 is_num"; |
104 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"}); |
104 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"}); |
105 if UnparseC.term_in_ctxt @{context} t' = "(- 2 is_num) = True" then () |
105 if UnparseC.term @{context} t' = "(- 2 is_num) = True" then () |
106 else error "(- 2 is_num) = False CHANGED"; |
106 else error "(- 2 is_num) = False CHANGED"; |
107 |
107 |
108 val t = ParseC.parse_test @{context} "- 1 is_num"; |
108 val t = ParseC.parse_test @{context} "- 1 is_num"; |
109 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"}); |
109 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"}); |
110 if UnparseC.term_in_ctxt @{context} t' = "(- 1 is_num) = True" then () |
110 if UnparseC.term @{context} t' = "(- 1 is_num) = True" then () |
111 else error "(- 1 is_num) = False CHANGED"; |
111 else error "(- 1 is_num) = False CHANGED"; |
112 |
112 |
113 val t = ParseC.parse_test @{context} "0 is_num"; |
113 val t = ParseC.parse_test @{context} "0 is_num"; |
114 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"}); |
114 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"}); |
115 if UnparseC.term_in_ctxt @{context} t' = "(0 is_num) = True" then () |
115 if UnparseC.term @{context} t' = "(0 is_num) = True" then () |
116 else error "(0 is_num) = False CHANGED"; |
116 else error "(0 is_num) = False CHANGED"; |
117 |
117 |
118 val t = ParseC.parse_test @{context} "AA is_num"; |
118 val t = ParseC.parse_test @{context} "AA is_num"; |
119 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"}); |
119 val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t (@{theory "Isac_Knowledge"}); |
120 if UnparseC.term_in_ctxt @{context} t' = "(AA is_num) = False" then () |
120 if UnparseC.term @{context} t' = "(AA is_num) = False" then () |
121 else error "(0 is_num) = False CHANGED"; |
121 else error "(0 is_num) = False CHANGED"; |
122 |
122 |
123 |
123 |
124 "-------- fun eval_cancel ----------------------------------------------------------------------"; |
124 "-------- fun eval_cancel ----------------------------------------------------------------------"; |
125 "-------- fun eval_cancel ----------------------------------------------------------------------"; |
125 "-------- fun eval_cancel ----------------------------------------------------------------------"; |
143 val NONE = eval_cancel "cancel_" "Rings.divide_class.divide" t "" |
143 val NONE = eval_cancel "cancel_" "Rings.divide_class.divide" t "" |
144 |
144 |
145 val t = @{term "6 / 4 :: real"}; |
145 val t = @{term "6 / 4 :: real"}; |
146 case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of |
146 case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of |
147 SOME ("cancel_6_4", t') => |
147 SOME ("cancel_6_4", t') => |
148 if UnparseC.term_in_ctxt @{context} t' = "6 / 4 = 3 / 2" then () |
148 if UnparseC.term @{context} t' = "6 / 4 = 3 / 2" then () |
149 else error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 1" |
149 else error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 1" |
150 | _ => error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 2"; |
150 | _ => error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 2"; |
151 |
151 |
152 val t = @{term "- 6 / 4 :: real"}; |
152 val t = @{term "- 6 / 4 :: real"}; |
153 case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of |
153 case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of |
154 SOME ("cancel_~6_4", t') => |
154 SOME ("cancel_~6_4", t') => |
155 if UnparseC.term_in_ctxt @{context} t' = "- 6 / 4 = - 3 / 2" then () |
155 if UnparseC.term @{context} t' = "- 6 / 4 = - 3 / 2" then () |
156 else error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 1" |
156 else error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 1" |
157 | _ => error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 2"; |
157 | _ => error "eval_cancel - 6 / 4 = - 3 / 2 CHANGED 2"; |
158 |
158 |
159 val t = @{term "6 / - 4 :: real"}; |
159 val t = @{term "6 / - 4 :: real"}; |
160 case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of |
160 case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of |
161 SOME ("cancel_6_~4", t') => |
161 SOME ("cancel_6_~4", t') => |
162 if UnparseC.term_in_ctxt @{context} t' = "6 / - 4 = - 3 / 2" then () |
162 if UnparseC.term @{context} t' = "6 / - 4 = - 3 / 2" then () |
163 else error "eval_cancel 6 / - 4 = - 3 / 2 CHANGED 1" |
163 else error "eval_cancel 6 / - 4 = - 3 / 2 CHANGED 1" |
164 | _ => error "eval_cancel 6 / - 4 = - 3 / 2 CHANGED 2"; |
164 | _ => error "eval_cancel 6 / - 4 = - 3 / 2 CHANGED 2"; |
165 |
165 |
166 val t = @{term "- 6 /- 4 :: real"}; |
166 val t = @{term "- 6 /- 4 :: real"}; |
167 case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of |
167 case eval_cancel "cancel_" "Rings.divide_class.divide" t "" of |
168 SOME ("cancel_~6_~4", t') => |
168 SOME ("cancel_~6_~4", t') => |
169 if UnparseC.term_in_ctxt @{context} t' = "- 6 / - 4 = 3 / 2" then () |
169 if UnparseC.term @{context} t' = "- 6 / - 4 = 3 / 2" then () |
170 else error "eval_cancel - 6 / - 4 = 3 / 2 CHANGED 1" |
170 else error "eval_cancel - 6 / - 4 = 3 / 2 CHANGED 1" |
171 | _ => error "eval_cancel - 6 / - 4 = 3 / 2 CHANGED 2"; |
171 | _ => error "eval_cancel - 6 / - 4 = 3 / 2 CHANGED 2"; |
172 |
172 |
173 val t = @{term "- (6 / 4) :: real"}; |
173 val t = @{term "- (6 / 4) :: real"}; |
174 val NONE = eval_cancel "adhoc_thm_cancel" "Rings.divide_class.divide" t ""; |
174 val NONE = eval_cancel "adhoc_thm_cancel" "Rings.divide_class.divide" t ""; |
208 val NONE(*= indetermined*) = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt; |
208 val NONE(*= indetermined*) = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt; |
209 |
209 |
210 val t = ParseC.parse_test @{context} "(x + 1) = (x + 1)"; |
210 val t = ParseC.parse_test @{context} "(x + 1) = (x + 1)"; |
211 val (Const _(*op0,t0*) $ t1 $ t2 ) = t |
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; |
212 val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt; |
213 if UnparseC.term_in_ctxt @{context} t' = "(x + 1 = x + 1) = True" then () else error "(x + 1) = (x + 1) CHANGED"; |
213 if UnparseC.term @{context} t' = "(x + 1 = x + 1) = True" then () else error "(x + 1) = (x + 1) CHANGED"; |
214 |
214 |
215 val t as Const _ $ v $ c = ParseC.parse_test @{context} "1 = 0"; |
215 val t as Const _ $ v $ c = ParseC.parse_test @{context} "1 = 0"; |
216 val false = variable_constant_pair (v, c); |
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; |
217 val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt; |
218 if UnparseC.term_in_ctxt @{context} t' = "(1 = 0) = False" then () else error "1 = 0 CHANGED"; |
218 if UnparseC.term @{context} t' = "(1 = 0) = False" then () else error "1 = 0 CHANGED"; |
219 |
219 |
220 val t = ParseC.parse_test @{context} "0 = 0"; |
220 val t = ParseC.parse_test @{context} "0 = 0"; |
221 val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt; |
221 val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt; |
222 if UnparseC.term_in_ctxt @{context} t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED"; |
222 if UnparseC.term @{context} t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED"; |
223 |
223 |
224 |
224 |
225 "-------- occurs_in ----------------------------------------------------------------------------"; |
225 "-------- occurs_in ----------------------------------------------------------------------------"; |
226 "-------- occurs_in ----------------------------------------------------------------------------"; |
226 "-------- occurs_in ----------------------------------------------------------------------------"; |
227 "-------- occurs_in ----------------------------------------------------------------------------"; |
227 "-------- occurs_in ----------------------------------------------------------------------------"; |
228 val t = @{term "x::real"}; |
228 val t = @{term "x::real"}; |
229 if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed"; |
229 if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed"; |
230 |
230 |
231 val t = ParseC.parse_test @{context} "x occurs_in x"; |
231 val t = ParseC.parse_test @{context} "x occurs_in x"; |
232 val SOME (str, t') = eval_occurs_in 0 "Prog_Expr.occurs_in" t 0; |
232 val SOME (str, t') = eval_occurs_in 0 "Prog_Expr.occurs_in" t 0; |
233 if UnparseC.term_in_ctxt @{context} t' = "x occurs_in x = True" then () |
233 if UnparseC.term @{context} t' = "x occurs_in x = True" then () |
234 else error "x occurs_in x = True ..changed"; |
234 else error "x occurs_in x = True ..changed"; |
235 |
235 |
236 "------- some_occur_in"; |
236 "------- some_occur_in"; |
237 if some_occur_in [@{term "c::real"}, @{term "c_2::real"}] @{term "a + b + c::real"} then () |
237 if some_occur_in [@{term "c::real"}, @{term "c_2::real"}] @{term "a + b + c::real"} then () |
238 else error ""; |
238 else error ""; |
239 |
239 |
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"}; |
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; |
241 val SOME (str, t') = eval_some_occur_in 0 "Prog_Expr.some_occur_in" t 0; |
242 if UnparseC.term_in_ctxt @{context} t' = |
242 if UnparseC.term @{context} 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 () |
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"; |
244 else error "atools.sml: some_occur_in true"; |
245 |
245 |
246 val t = @{term "some_of [c_3, c_4] occur_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2"}; |
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; |
247 val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some_occur_in" t 0; |
248 if UnparseC.term_in_ctxt @{context} t' = |
248 if UnparseC.term @{context} t' = |
249 "some_of [c_3, c_4] occur_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False" then () |
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"; |
250 else error "atools.sml: some_occur_in false"; |
251 |
251 |
252 |
252 |
253 "-------- fun eval_occurs_in -------------------------------------------------------------------"; |
253 "-------- fun eval_occurs_in -------------------------------------------------------------------"; |
337 "---------fun eval_argument_of -----------------------------------------------------------------"; |
337 "---------fun eval_argument_of -----------------------------------------------------------------"; |
338 "---------fun eval_argument_of -----------------------------------------------------------------"; |
338 "---------fun eval_argument_of -----------------------------------------------------------------"; |
339 "---------fun eval_argument_of -----------------------------------------------------------------"; |
339 "---------fun eval_argument_of -----------------------------------------------------------------"; |
340 val t = ParseC.parse_test @{context} "argument_in (M_b x)"; |
340 val t = ParseC.parse_test @{context} "argument_in (M_b x)"; |
341 val SOME (str, t') = eval_argument_in "0" "Prog_Expr.argument_in" t 0; |
341 val SOME (str, t') = eval_argument_in "0" "Prog_Expr.argument_in" t 0; |
342 if UnparseC.term_in_ctxt @{context} t' = "(argument_in M_b x) = x" then () |
342 if UnparseC.term @{context} t' = "(argument_in M_b x) = x" then () |
343 else error "atools.sml:(argument_in M_b x) = x ???"; |
343 else error "atools.sml:(argument_in M_b x) = x ???"; |
344 |
344 |
345 |
345 |
346 "---------fun eval_sameFunId -------------------------------------------------------------------"; |
346 "---------fun eval_sameFunId -------------------------------------------------------------------"; |
347 "---------fun eval_sameFunId -------------------------------------------------------------------"; |
347 "---------fun eval_sameFunId -------------------------------------------------------------------"; |
373 val flhs as (fid $ _) = @{term "y' L"}; |
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]"}; |
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) = |
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]"}; |
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 ""; |
377 val SOME (str, es) = eval_filter_sameFunId "" "Prog_Expr.filter_sameFunId" p ""; |
378 if UnparseC.term_in_ctxt @{context} 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 () |
378 if UnparseC.term @{context} 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"; |
379 else error "atools.slm diff.behav. in filter_sameFunId"; |
380 |
380 |
381 |
381 |
382 "---------fun eval_boollist2sum ----------------------------------------------------------------"; |
382 "---------fun eval_boollist2sum ----------------------------------------------------------------"; |
383 "---------fun eval_boollist2sum ----------------------------------------------------------------"; |
383 "---------fun eval_boollist2sum ----------------------------------------------------------------"; |
384 "---------fun eval_boollist2sum ----------------------------------------------------------------"; |
384 "---------fun eval_boollist2sum ----------------------------------------------------------------"; |
385 fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l |
385 fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l |
386 | lhs t = error("lhs called with (" ^ UnparseC.term_in_ctxt @{context} t ^ ")"); |
386 | lhs t = error("lhs called with (" ^ UnparseC.term @{context} t ^ ")"); |
387 "----------- \<up> redefined due to overwritten identifier -----------"; |
387 "----------- \<up> redefined due to overwritten identifier -----------"; |
388 val u_ = @{term "[]"}; |
388 val u_ = @{term "[]"}; |
389 val u_ = @{term "[b1 = k - 2*q]"}; |
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]"}; |
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_; |
391 val ut_ = isalist2list u_; |
392 val sum_ = map lhs ut_; |
392 val sum_ = map lhs ut_; |
393 val t = list2sum sum_; |
393 val t = list2sum sum_; |
394 UnparseC.term_in_ctxt @{context} t; |
394 UnparseC.term @{context} t; |
395 |
395 |
396 val t = @{term "boollist2sum [b1 = k - 2*(q::real), b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"}; |
396 val t = @{term "boollist2sum [b1 = k - 2*(q::real), b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"}; |
397 case t of |
397 case t of |
398 Const (\<^const_name>\<open>boollist2sum\<close>, _) $ |
398 Const (\<^const_name>\<open>boollist2sum\<close>, _) $ |
399 (Const (\<^const_name>\<open>Cons\<close>, _) $ |
399 (Const (\<^const_name>\<open>Cons\<close>, _) $ |
405 (Const (\<^const_name>\<open>Cons\<close>, _) $ |
405 (Const (\<^const_name>\<open>Cons\<close>, _) $ |
406 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b4", _) $ _ ) $ |
406 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b4", _) $ _ ) $ |
407 Const (\<^const_name>\<open>Nil\<close>, _))))) => () |
407 Const (\<^const_name>\<open>Nil\<close>, _))))) => () |
408 | _ => error "boollist2sum CHANGED"; |
408 | _ => error "boollist2sum CHANGED"; |
409 val SOME (str, pred) = eval_boollist2sum "" "Prog_Expr.boollist2sum" t ""; |
409 val SOME (str, pred) = eval_boollist2sum "" "Prog_Expr.boollist2sum" t ""; |
410 if UnparseC.term_in_ctxt @{context} pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then () |
410 if UnparseC.term @{context} 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"; |
411 else error "atools.sml diff.behav. in eval_boollist2sum"; |
412 |
412 |
413 val srls_ = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty |
413 val srls_ = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty |
414 [Eval ("Prog_Expr.boollist2sum", eval_boollist2sum "")]; |
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]"}; |
415 val t = @{term "boollist2sum [b1 = k - 2*(q::real), b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"}; |
435 val Const (c, _) $ t1 $ t2 = (* binary \<circ> n1 \<circ> n2 *) |
435 val Const (c, _) $ t1 $ t2 = (* binary \<circ> n1 \<circ> n2 *) |
436 (*case*) t (*of*); |
436 (*case*) t (*of*); |
437 (*if*) Calc_Binop.is c andalso is_num t1 andalso is_num t2 (*then*); |
437 (*if*) Calc_Binop.is c andalso is_num t1 andalso is_num t2 (*then*); |
438 val res = Calc_Binop.simplify ctxt t; |
438 val res = Calc_Binop.simplify ctxt t; |
439 val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res)); |
439 val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res)); |
440 SOME ("#: " ^ UnparseC.term_in_ctxt @{context} prop, prop) (*return value*); |
440 SOME ("#: " ^ UnparseC.term @{context} prop, prop) (*return value*); |
441 ; |
441 ; |
442 if "#: " ^ UnparseC.term_in_ctxt @{context} prop = "#: 2 * 3 = 6" andalso UnparseC.term_in_ctxt @{context} prop = "2 * 3 = 6" then () |
442 if "#: " ^ UnparseC.term @{context} prop = "#: 2 * 3 = 6" andalso UnparseC.term @{context} prop = "2 * 3 = 6" then () |
443 else error "eval_binop changed" |
443 else error "eval_binop changed" |
444 ; |
444 ; |
445 val SOME (thmid, tm) = Calc_Binop.numeric "#mult_" op_ t ctxt; |
445 val SOME (thmid, tm) = Calc_Binop.numeric "#mult_" op_ t ctxt; |
446 if thmid = "#: 2 * 3 = 6" andalso UnparseC.term_in_ctxt @{context} prop = "2 * 3 = 6" then () |
446 if thmid = "#: 2 * 3 = 6" andalso UnparseC.term @{context} prop = "2 * 3 = 6" then () |
447 else error "eval_binop changed 2" |
447 else error "eval_binop changed 2" |
448 |
448 |
449 |
449 |
450 "-------- fun matchsub -------------------------------------------------------------------------"; |
450 "-------- fun matchsub -------------------------------------------------------------------------"; |
451 "-------- fun matchsub -------------------------------------------------------------------------"; |
451 "-------- fun matchsub -------------------------------------------------------------------------"; |
464 case or2list @{term True} of Const (\<^const_name>\<open>UniversalList\<close>, _) => () |
464 case or2list @{term True} of Const (\<^const_name>\<open>UniversalList\<close>, _) => () |
465 | _ => error "TermC.UniversalList changed 1"; |
465 | _ => error "TermC.UniversalList changed 1"; |
466 case or2list @{term False} of Const (\<^const_name>\<open>Nil\<close>, _) => () |
466 case or2list @{term False} of Const (\<^const_name>\<open>Nil\<close>, _) => () |
467 | _ => error "TermC.UniversalList changed 2"; |
467 | _ => error "TermC.UniversalList changed 2"; |
468 val t = (ParseC.parse_test @{context} "x=3"); |
468 val t = (ParseC.parse_test @{context} "x=3"); |
469 if UnparseC.term_in_ctxt @{context} (or2list t) = "[x = 3]" then () |
469 if UnparseC.term @{context} (or2list t) = "[x = 3]" then () |
470 else error "or2list changed"; |
470 else error "or2list changed"; |
471 val t = (ParseC.parse_test @{context} "x=3 | x=-3 | x=0"); |
471 val t = (ParseC.parse_test @{context} "x=3 | x=-3 | x=0"); |
472 if UnparseC.term_in_ctxt @{context} (or2list t) = "[x = 3, x = - 3, x = 0]" then () |
472 if UnparseC.term @{context} (or2list t) = "[x = 3, x = - 3, x = 0]" then () |
473 else error "HOL.eq ? HOL.disj ? changed"; |
473 else error "HOL.eq ? HOL.disj ? changed"; |