243 "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; |
243 "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; |
244 "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; |
244 "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; |
245 "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; |
245 "----------- step through 'fun rewrite_terms_' ------------------------------------------------"; |
246 "----- step 0: args for rewrite_terms_, local fun"; |
246 "----- step 0: args for rewrite_terms_, local fun"; |
247 val (thy, ord, erls, equs, t) = |
247 val (thy, ord, erls, equs, t) = |
248 (@{theory "Biegelinie"}, Rewrite_Ord.function_empty, Rule_Set.Empty, [TermC.str2term "x = 0"], |
248 (@{theory "Biegelinie"}, Rewrite_Ord.function_empty, Rule_Set.Empty, [TermC.parse_test @{context} "x = 0"], |
249 TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2"); |
249 TermC.parse_test @{context} "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2"); |
250 "----- step 1: args for rew_"; |
250 "----- step 1: args for rew_"; |
251 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t); |
251 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t); |
252 "----- step 2: rew_sub"; |
252 "----- step 2: rew_sub"; |
253 rew_sub ctxt 1 [] ord erls false [] (HOLogic.Trueprop $ r) t; |
253 rew_sub ctxt 1 [] ord erls false [] (HOLogic.Trueprop $ r) t; |
254 "----- step 3: step through rew_sub -- inefficient: goes into subterms"; |
254 "----- step 3: step through rew_sub -- inefficient: goes into subterms"; |
257 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t; |
257 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t; |
258 writeln "---------- rewrite_terms_ 1---------------------------"; |
258 writeln "---------- rewrite_terms_ 1---------------------------"; |
259 if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then () |
259 if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then () |
260 else error "rewrite.sml rewrite_terms_ [x = 0]"; |
260 else error "rewrite.sml rewrite_terms_ [x = 0]"; |
261 |
261 |
262 val equs = [TermC.str2term "M_b 0 = 0"]; |
262 val equs = [TermC.parse_test @{context} "M_b 0 = 0"]; |
263 val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2"; |
263 val t = TermC.parse_test @{context} "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2"; |
264 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t; |
264 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t; |
265 writeln "---------- rewrite_terms_ 2---------------------------"; |
265 writeln "---------- rewrite_terms_ 2---------------------------"; |
266 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then () |
266 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then () |
267 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]"; |
267 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]"; |
268 |
268 |
269 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"]; |
269 val equs = [TermC.parse_test @{context} "x = 0", TermC.parse_test @{context}"M_b 0 = 0"]; |
270 val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2"; |
270 val t = TermC.parse_test @{context} "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2"; |
271 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t; |
271 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t; |
272 writeln "---------- rewrite_terms_ 3---------------------------"; |
272 writeln "---------- rewrite_terms_ 3---------------------------"; |
273 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then () |
273 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then () |
274 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]"; |
274 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]"; |
275 |
275 |
276 |
276 |
277 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------"; |
277 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------"; |
278 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------"; |
278 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------"; |
279 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------"; |
279 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------"; |
280 (*see smltest/Scripts/term_G.sml: inst_bdv 2*) |
280 (*see smltest/Scripts/term_G.sml: inst_bdv 2*) |
281 val t = TermC.str2term"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0"; |
281 val t = TermC.parse_test @{context}"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0"; |
282 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"), |
282 val bdvs = [(TermC.parse_test @{context}"bdv_1",TermC.parse_test @{context}"c"), |
283 (TermC.str2term"bdv_2",TermC.str2term"c_2"), |
283 (TermC.parse_test @{context}"bdv_2",TermC.parse_test @{context}"c_2"), |
284 (TermC.str2term"bdv_3",TermC.str2term"c_3"), |
284 (TermC.parse_test @{context}"bdv_3",TermC.parse_test @{context}"c_3"), |
285 (TermC.str2term"bdv_4",TermC.str2term"c_4")]; |
285 (TermC.parse_test @{context}"bdv_4",TermC.parse_test @{context}"c_4")]; |
286 (*------------ outcommented WN071210, after inclusion into ROOT.ML |
286 (*------------ outcommented WN071210, after inclusion into ROOT.ML |
287 val SOME (t,_) = |
287 val SOME (t,_) = |
288 rewrite_inst_ thy e_rew_ord |
288 rewrite_inst_ thy e_rew_ord |
289 (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty |
289 (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty |
290 [(Eval ("EqSystem.occur_exactly_in", |
290 [(Eval ("EqSystem.occur_exactly_in", |
315 "===== Rational.thy: cancel ==="; |
315 "===== Rational.thy: cancel ==="; |
316 (* pat matched with the current term gives an environment |
316 (* pat matched with the current term gives an environment |
317 (or not: hen the Rrls not applied); |
317 (or not: hen the Rrls not applied); |
318 if pre1 and pre2 evaluate to @{term True} in this environment, |
318 if pre1 and pre2 evaluate to @{term True} in this environment, |
319 then the Rrls is applied. *) |
319 then the Rrls is applied. *) |
320 val t = TermC.str2term "(a + b) / c ::real"; |
320 val t = TermC.parse_test @{context} "(a + b) / c ::real"; |
321 val pat = TermC.parse_patt thy "?r / ?s ::real"; |
321 val pat = TermC.parse_patt thy "?r / ?s ::real"; |
322 val pres = [TermC.parse_patt thy "?r is_expanded", TermC.parse_patt thy "?s is_expanded"]; |
322 val pres = [TermC.parse_patt thy "?r is_expanded", TermC.parse_patt thy "?s is_expanded"]; |
323 val prepat = [(pres, pat)]; |
323 val prepat = [(pres, pat)]; |
324 val erls = rational_erls; |
324 val erls = rational_erls; |
325 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *) |
325 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *) |
333 then () else error "rewrite.sml: prepat cancel eval__true"; |
333 then () else error "rewrite.sml: prepat cancel eval__true"; |
334 |
334 |
335 "===== Rational.thy: add_fractions_p ==="; |
335 "===== Rational.thy: add_fractions_p ==="; |
336 (* if each pat* TermC.matches with the current term, the Rrls is applied |
336 (* if each pat* TermC.matches with the current term, the Rrls is applied |
337 (there are no preconditions to be checked, they are @{term True}) *) |
337 (there are no preconditions to be checked, they are @{term True}) *) |
338 val t = TermC.str2term "a / b + 1 / 2"; |
338 val t = TermC.parse_test @{context} "a / b + 1 / 2"; |
339 val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v"; |
339 val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v"; |
340 val pres = [@{term True}]; |
340 val pres = [@{term True}]; |
341 val prepat = [(pres, pat)]; |
341 val prepat = [(pres, pat)]; |
342 val erls = rational_erls; |
342 val erls = rational_erls; |
343 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *) |
343 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *) |
347 then () else error "rewrite.sml: prepat add_fractions_p"; |
347 then () else error "rewrite.sml: prepat add_fractions_p"; |
348 |
348 |
349 "===== Poly.thy: order_mult_ ==="; |
349 "===== Poly.thy: order_mult_ ==="; |
350 (* ?p matched with the current term gives an environment, |
350 (* ?p matched with the current term gives an environment, |
351 which evaluates (the instantiated) "p is_multUnordered" to true*) |
351 which evaluates (the instantiated) "p is_multUnordered" to true*) |
352 val t = TermC.str2term "x \<up> 2 * x"; |
352 val t = TermC.parse_test @{context} "x \<up> 2 * x"; |
353 val pat = TermC.parse_patt thy "?p :: real" |
353 val pat = TermC.parse_patt thy "?p :: real" |
354 val pres = [TermC.parse_patt thy "?p is_multUnordered"]; |
354 val pres = [TermC.parse_patt thy "?p is_multUnordered"]; |
355 val prepat = [(pres, pat)]; |
355 val prepat = [(pres, pat)]; |
356 val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty |
356 val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty |
357 [Eval ("Poly.is_multUnordered", |
357 [Eval ("Poly.is_multUnordered", |
367 |
367 |
368 |
368 |
369 "----------- fun app_rev, Rrls, ----------------------------------------------------------------"; |
369 "----------- fun app_rev, Rrls, ----------------------------------------------------------------"; |
370 "----------- fun app_rev, Rrls, ----------------------------------------------------------------"; |
370 "----------- fun app_rev, Rrls, ----------------------------------------------------------------"; |
371 "----------- fun app_rev, Rrls, ----------------------------------------------------------------"; |
371 "----------- fun app_rev, Rrls, ----------------------------------------------------------------"; |
372 val t = TermC.str2term "x \<up> 2 * x"; |
372 val t = TermC.parse_test @{context} "x \<up> 2 * x"; |
373 |
373 |
374 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2"; |
374 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2"; |
375 val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered"; |
375 val tm = TermC.parse_test @{context} "(x \<up> 2 * x) is_multUnordered"; |
376 |
376 |
377 (*+*)case eval_is_multUnordered "testid" "" tm ctxt of |
377 (*+*)case eval_is_multUnordered "testid" "" tm ctxt of |
378 (*+*) SOME |
378 (*+*) SOME |
379 (*+*) ("testidx \<up> 2 * x_", |
379 (*+*) ("testidx \<up> 2 * x_", |
380 (*+*) Const (\<^const_name>\<open>Trueprop\<close>, _) $ |
380 (*+*) Const (\<^const_name>\<open>Trueprop\<close>, _) $ |
451 tracing "=== poly.sml: scan_ chk prepat begin"; |
451 tracing "=== poly.sml: scan_ chk prepat begin"; |
452 scan_ chk prepat; |
452 scan_ chk prepat; |
453 tracing "=== poly.sml: scan_ chk prepat end"; |
453 tracing "=== poly.sml: scan_ chk prepat end"; |
454 |
454 |
455 "----- chk ---"; |
455 "----- chk ---"; |
456 (*reestablish...*) val t = TermC.str2term "x \<up> 2 * x"; |
456 (*reestablish...*) val t = TermC.parse_test @{context} "x \<up> 2 * x"; |
457 val [(pres, pat)] = prepat; |
457 val [(pres, pat)] = prepat; |
458 val subst: Type.tyenv * Envir.tenv = |
458 val subst: Type.tyenv * Envir.tenv = |
459 Pattern.match thy (pat, t) |
459 Pattern.match thy (pat, t) |
460 (Vartab.empty, Vartab.empty); |
460 (Vartab.empty, Vartab.empty); |
461 |
461 |
463 "----- eval__true ---"; |
463 "----- eval__true ---"; |
464 val asms = (map (Envir.subst_term subst) pres); |
464 val asms = (map (Envir.subst_term subst) pres); |
465 if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]" then () |
465 if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]" then () |
466 else error "rewrite.sml: diff. is_multUnordered, asms"; |
466 else error "rewrite.sml: diff. is_multUnordered, asms"; |
467 val (thy, i, asms, bdv, rls) = |
467 val (thy, i, asms, bdv, rls) = |
468 (thy, (i+1), [TermC.str2term "(x \<up> 2 * x) is_multUnordered"], |
468 (thy, (i+1), [TermC.parse_test @{context} "(x \<up> 2 * x) is_multUnordered"], |
469 [] : Subst.T, erls); |
469 [] : Subst.T, erls); |
470 case eval__true ctxt i asms bdv rls of |
470 case eval__true ctxt i asms bdv rls of |
471 ([], true) => () |
471 ([], true) => () |
472 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true"; |
472 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true"; |
473 |
473 |
475 "----------- 2011 thms with axclasses ----------------------------------------------------------"; |
475 "----------- 2011 thms with axclasses ----------------------------------------------------------"; |
476 "----------- 2011 thms with axclasses ----------------------------------------------------------"; |
476 "----------- 2011 thms with axclasses ----------------------------------------------------------"; |
477 val thm = @{thm div_by_1}; |
477 val thm = @{thm div_by_1}; |
478 val prop = Thm.prop_of thm; |
478 val prop = Thm.prop_of thm; |
479 TermC.atomty prop; (*Type 'a*) |
479 TermC.atomty prop; (*Type 'a*) |
480 val t = TermC.str2term "(2*x)/1"; (*Type real*) |
480 val t = TermC.parse_test @{context} "(2*x)/1"; (*Type real*) |
481 |
481 |
482 val (thy, ro, er, inst) = |
482 val (thy, ro, er, inst) = |
483 (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); |
483 (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); |
484 val SOME (t, _) = rewrite_ ctxt ro er true thm t; (*real TermC.matches 'a ?via ring? etc*) |
484 val SOME (t, _) = rewrite_ ctxt ro er true thm t; (*real TermC.matches 'a ?via ring? etc*) |
485 |
485 |
678 "----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------"; |
678 "----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------"; |
679 "----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------"; |
679 "----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------"; |
680 (* norm_equation is defined in Test.thy, other rls see Knowledg/**) |
680 (* norm_equation is defined in Test.thy, other rls see Knowledg/**) |
681 val thy = @{theory}; |
681 val thy = @{theory}; |
682 val rls = norm_equation; |
682 val rls = norm_equation; |
683 val term = TermC.str2term "x + 1 = 2"; |
683 val term = TermC.parse_test @{context} "x + 1 = 2"; |
684 |
684 |
685 (**)val SOME (t, asm) = rewrite_set_ ctxt false rls term; |
685 (**)val SOME (t, asm) = rewrite_set_ ctxt false rls term; |
686 (** )##### try thm: "root_ge0" |
686 (** )##### try thm: "root_ge0" |
687 exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"): |
687 exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"): |
688 dest_eq |
688 dest_eq |