468 \ [BOOL t_t, REAL v_v, REAL_SET itv_v]\ |
468 \ [BOOL t_t, REAL v_v, REAL_SET itv_v]\ |
469 \ in ((SubProblem (Reals_s,[find_values,tool],[Isac,find_values]) \ |
469 \ in ((SubProblem (Reals_s,[find_values,tool],[Isac,find_values]) \ |
470 \ [REAL mx_x, REAL (Rhs t_t), REAL v_v, REAL m_m, \ |
470 \ [REAL mx_x, REAL (Rhs t_t), REAL v_v, REAL m_m, \ |
471 \ BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))"; |
471 \ BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))"; |
472 |
472 |
473 val f_ix = (TermC.str2term "f_ix::bool list", |
473 val f_ix = (TermC.parse_test @{context} "f_ix::bool list", |
474 TermC.str2term "[r=Arbfix]"); |
474 TermC.parse_test @{context} "[r=Arbfix]"); |
475 val m_m = (TermC.str2term "m_m::real", |
475 val m_m = (TermC.parse_test @{context} "m_m::real", |
476 TermC.str2term "A"); |
476 TermC.parse_test @{context} "A"); |
477 val r_s = (TermC.str2term "rs_s::bool list", |
477 val r_s = (TermC.parse_test @{context} "rs_s::bool list", |
478 TermC.str2term "[A = a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"); |
478 TermC.parse_test @{context} "[A = a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"); |
479 val v_v = (TermC.str2term "v_v::real", |
479 val v_v = (TermC.parse_test @{context} "v_v::real", |
480 TermC.str2term "b"); |
480 TermC.parse_test @{context} "b"); |
481 val itv_v = (TermC.str2term "itv_v::real set", |
481 val itv_v = (TermC.parse_test @{context} "itv_v::real set", |
482 TermC.str2term "{x::real. 0 <= x & x <= 2*r}"); |
482 TermC.parse_test @{context} "{x::real. 0 <= x & x <= 2*r}"); |
483 val err_r = (TermC.str2term "err_r::bool", |
483 val err_r = (TermC.parse_test @{context} "err_r::bool", |
484 TermC.str2term "eps=0"); |
484 TermC.parse_test @{context} "eps=0"); |
485 val env = [f_ix, m_m, r_s ,v_v, itv_v, err_r]; |
485 val env = [f_ix, m_m, r_s ,v_v, itv_v, err_r]; |
486 |
486 |
487 (*--- 1.line in script ---*) |
487 (*--- 1.line in script ---*) |
488 val t = TermC.str2term "(hd o (filterVar m_m)) (r_s::bool list)"; |
488 val t = TermC.parse_test @{context} "(hd o (filterVar m_m)) (r_s::bool list)"; |
489 val s = subst_atomic env t; |
489 val s = subst_atomic env t; |
490 UnparseC.term s; |
490 UnparseC.term s; |
491 "(hd o filterVar A) [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"; |
491 "(hd o filterVar A) [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"; |
492 (*=== inhibit exn 110726============================================================= |
492 (*=== inhibit exn 110726============================================================= |
493 val SOME (s',_) = rewrite_set_ thy false prog_expr s; |
493 val SOME (s',_) = rewrite_set_ thy false prog_expr s; |
494 val s'' = UnparseC.term s'; |
494 val s'' = UnparseC.term s'; |
495 if s''="A = a * b" then () else error "new behaviour with prog_expr 1.1."; |
495 if s''="A = a * b" then () else error "new behaviour with prog_expr 1.1."; |
496 === inhibit exn 110726=============================================================*) |
496 === inhibit exn 110726=============================================================*) |
497 val env = env @ [(TermC.str2term "e_e::bool",TermC.str2term "A = a * b")]; |
497 val env = env @ [(TermC.parse_test @{context} "e_e::bool",TermC.parse_test @{context} "A = a * b")]; |
498 |
498 |
499 (*--- 2.line: condition alone ---*) |
499 (*--- 2.line: condition alone ---*) |
500 val t = TermC.str2term "1 < length_h (r_s::bool list)"; |
500 val t = TermC.parse_test @{context} "1 < length_h (r_s::bool list)"; |
501 val s = subst_atomic env t; |
501 val s = subst_atomic env t; |
502 UnparseC.term s; |
502 UnparseC.term s; |
503 "1 < length_h [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"; |
503 "1 < length_h [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"; |
504 (*=== inhibit exn 110726============================================================= |
504 (*=== inhibit exn 110726============================================================= |
505 val SOME (s',_) = rewrite_set_ thy false prog_expr s; |
505 val SOME (s',_) = rewrite_set_ thy false prog_expr s; |
506 val s'' = UnparseC.term s'; |
506 val s'' = UnparseC.term s'; |
507 if s''=\<^const_name>\<open>True\<close> then () else error "new behaviour with prog_expr 1.2."; |
507 if s''=\<^const_name>\<open>True\<close> then () else error "new behaviour with prog_expr 1.2."; |
508 === inhibit exn 110726=============================================================*) |
508 === inhibit exn 110726=============================================================*) |
509 |
509 |
510 (*--- 2.line in script ---*) |
510 (*--- 2.line in script ---*) |
511 val t = TermC.str2term |
511 val t = TermC.parse_test @{context} |
512 "(if 1 < length_h r_s \ |
512 "(if 1 < length_h r_s \ |
513 \ then (SubProblem (Reals_s,[make,function],[no_met])\ |
513 \ then (SubProblem (Reals_s,[make,function],[no_met])\ |
514 \ [REAL m_m, REAL v_v, BOOL_LIST r_s])\ |
514 \ [REAL m_m, REAL v_v, BOOL_LIST r_s])\ |
515 \ else (hd r_s))"; |
515 \ else (hd r_s))"; |
516 val s = subst_atomic env t; |
516 val s = subst_atomic env t; |
527 "SubProblem (Reals_s, [make, function], [no_met])\n\ |
527 "SubProblem (Reals_s, [make, function], [no_met])\n\ |
528 \ [REAL A, REAL b,\n\ |
528 \ [REAL A, REAL b,\n\ |
529 \ BOOL_LIST [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]" then () |
529 \ BOOL_LIST [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]" then () |
530 else error "new behaviour with prog_expr 1.3."; |
530 else error "new behaviour with prog_expr 1.3."; |
531 === inhibit exn 110726=============================================================*) |
531 === inhibit exn 110726=============================================================*) |
532 val env = env @ [(TermC.str2term "t_t::bool", |
532 val env = env @ [(TermC.parse_test @{context} "t_t::bool", |
533 TermC.str2term "A = (2*sqrt(r \<up> 2-(b/2) \<up> 2)) * b")]; |
533 TermC.parse_test @{context} "A = (2*sqrt(r \<up> 2-(b/2) \<up> 2)) * b")]; |
534 |
534 |
535 |
535 |
536 |
536 |
537 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; |
537 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; |
538 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; |
538 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; |
539 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; |
539 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; |
540 TermC.str2term |
540 TermC.parse_test @{context} |
541 "Program Make_fun_by_explicit (f_f::real) (v_v::real) \ |
541 "Program Make_fun_by_explicit (f_f::real) (v_v::real) \ |
542 \ (eqs::bool list) = \ |
542 \ (eqs::bool list) = \ |
543 \ (let h_h = (hd o (filterVar f_f)) eqs; \ |
543 \ (let h_h = (hd o (filterVar f_f)) eqs; \ |
544 \ e_1 = hd (dropWhile (ident h_h) eqs); \ |
544 \ e_1 = hd (dropWhile (ident h_h) eqs); \ |
545 \ v_s = dropWhile (ident f_f) (Vars h_h); \ |
545 \ v_s = dropWhile (ident f_f) (Vars h_h); \ |
546 \ v_1 = hd (dropWhile (ident v_v) v_s); \ |
546 \ v_1 = hd (dropWhile (ident v_v) v_s); \ |
547 \ (s_1::bool list)=(SubProblem(Reals_s,[univar,equation],[no_met])\ |
547 \ (s_1::bool list)=(SubProblem(Reals_s,[univar,equation],[no_met])\ |
548 \ [BOOL e_1, REAL v_1])\ |
548 \ [BOOL e_1, REAL v_1])\ |
549 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_h)"; |
549 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_h)"; |
550 val f_f = (TermC.str2term "f_f::real", |
550 val f_f = (TermC.parse_test @{context} "f_f::real", |
551 TermC.str2term "A"); |
551 TermC.parse_test @{context} "A"); |
552 val v_v = (TermC.str2term "v_v::real", |
552 val v_v = (TermC.parse_test @{context} "v_v::real", |
553 TermC.str2term "b"); |
553 TermC.parse_test @{context} "b"); |
554 val eqs=(TermC.str2term "eqs::bool list", |
554 val eqs=(TermC.parse_test @{context} "eqs::bool list", |
555 TermC.str2term "[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"); |
555 TermC.parse_test @{context} "[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"); |
556 val env = [f_f, v_v, eqs]; |
556 val env = [f_f, v_v, eqs]; |
557 |
557 |
558 (*--- 1.line in script ---*) |
558 (*--- 1.line in script ---*) |
559 val t = TermC.str2term "(hd o (filterVar v_v)) (eqs::bool list)"; |
559 val t = TermC.parse_test @{context} "(hd o (filterVar v_v)) (eqs::bool list)"; |
560 val s = subst_atomic env t; |
560 val s = subst_atomic env t; |
561 UnparseC.term s; |
561 UnparseC.term s; |
562 val t = TermC.str2term |
562 val t = TermC.parse_test @{context} |
563 "(hd o filterVar b) [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"; |
563 "(hd o filterVar b) [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"; |
564 val SOME (t',_) = rewrite_set_ ctxt false prog_expr t; |
564 val SOME (t',_) = rewrite_set_ ctxt false prog_expr t; |
565 val s' = UnparseC.term t'; |
565 val s' = UnparseC.term t'; |
566 (*=== inhibit exn 110726============================================================= |
566 (*=== inhibit exn 110726============================================================= |
567 if s' = "A = a * b" then () else error "new behaviour with prog_expr 2.1"; |
567 if s' = "A = a * b" then () else error "new behaviour with prog_expr 2.1"; |
568 === inhibit exn 110726=============================================================*) |
568 === inhibit exn 110726=============================================================*) |
569 val env = env @ [(TermC.str2term "h_h::bool", TermC.str2term s')]; |
569 val env = env @ [(TermC.parse_test @{context} "h_h::bool", TermC.parse_test @{context} s')]; |
570 |
570 |
571 (*--- 2.line in script ---*) |
571 (*--- 2.line in script ---*) |
572 val t = TermC.str2term "hd (dropWhile (ident h_h) (eqs::bool list))"; |
572 val t = TermC.parse_test @{context} "hd (dropWhile (ident h_h) (eqs::bool list))"; |
573 val s = subst_atomic env t; |
573 val s = subst_atomic env t; |
574 UnparseC.term s; |
574 UnparseC.term s; |
575 val t = TermC.str2term |
575 val t = TermC.parse_test @{context} |
576 "hd (dropWhile (ident (A = a * b))\ |
576 "hd (dropWhile (ident (A = a * b))\ |
577 \ [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2])"; |
577 \ [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2])"; |
578 (*=== inhibit exn 110726============================================================= |
578 (*=== inhibit exn 110726============================================================= |
579 mem_rls "dropWhile_Cons" prog_expr; |
579 mem_rls "dropWhile_Cons" prog_expr; |
580 mem_rls "Prog_Expr.ident" prog_expr; |
580 mem_rls "Prog_Expr.ident" prog_expr; |
581 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
581 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
582 val s' = UnparseC.term t'; |
582 val s' = UnparseC.term t'; |
583 if s' = "(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2" then () |
583 if s' = "(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2" then () |
584 else error "new behaviour with prog_expr 2.2"; |
584 else error "new behaviour with prog_expr 2.2"; |
585 === inhibit exn 110726=============================================================*) |
585 === inhibit exn 110726=============================================================*) |
586 val env = env @ [(TermC.str2term "e_1::bool", TermC.str2term s')]; |
586 val env = env @ [(TermC.parse_test @{context} "e_1::bool", TermC.parse_test @{context} s')]; |
587 |
587 |
588 (*--- 3.line in script ---*) |
588 (*--- 3.line in script ---*) |
589 val t = TermC.str2term "dropWhile (ident f_f) (Vars (h_h::bool))"; |
589 val t = TermC.parse_test @{context} "dropWhile (ident f_f) (Vars (h_h::bool))"; |
590 val s = subst_atomic env t; |
590 val s = subst_atomic env t; |
591 UnparseC.term s; |
591 UnparseC.term s; |
592 val t = TermC.str2term "dropWhile (ident A) (Vars (A = a * b))"; |
592 val t = TermC.parse_test @{context} "dropWhile (ident A) (Vars (A = a * b))"; |
593 (*=== inhibit exn 110726============================================================= |
593 (*=== inhibit exn 110726============================================================= |
594 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
594 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
595 val s' = UnparseC.term t'; |
595 val s' = UnparseC.term t'; |
596 if s' = "[a, b]" then () else error "new behaviour with prog_expr 2.3"; |
596 if s' = "[a, b]" then () else error "new behaviour with prog_expr 2.3"; |
597 === inhibit exn 110726=============================================================*) |
597 === inhibit exn 110726=============================================================*) |
598 val env = env @ [(TermC.str2term "vs_s::real list", TermC.str2term s')]; |
598 val env = env @ [(TermC.parse_test @{context} "vs_s::real list", TermC.parse_test @{context} s')]; |
599 |
599 |
600 (*--- 4.line in script ---*) |
600 (*--- 4.line in script ---*) |
601 val t = TermC.str2term "hd (dropWhile (ident v_v) v_s)"; |
601 val t = TermC.parse_test @{context} "hd (dropWhile (ident v_v) v_s)"; |
602 val s = subst_atomic env t; |
602 val s = subst_atomic env t; |
603 UnparseC.term s; |
603 UnparseC.term s; |
604 val t = TermC.str2term "hd (dropWhile (ident b) [a, b])"; |
604 val t = TermC.parse_test @{context} "hd (dropWhile (ident b) [a, b])"; |
605 (*=== inhibit exn 110726============================================================= |
605 (*=== inhibit exn 110726============================================================= |
606 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
606 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
607 val s' = UnparseC.term t'; |
607 val s' = UnparseC.term t'; |
608 if s' = "a" then () else error "new behaviour with prog_expr 2.4."; |
608 if s' = "a" then () else error "new behaviour with prog_expr 2.4."; |
609 === inhibit exn 110726=============================================================*) |
609 === inhibit exn 110726=============================================================*) |
610 val env = env @ [(TermC.str2term "v_1::real", TermC.str2term s')]; |
610 val env = env @ [(TermC.parse_test @{context} "v_1::real", TermC.parse_test @{context} s')]; |
611 |
611 |
612 (*--- 5.line in script ---*) |
612 (*--- 5.line in script ---*) |
613 val t = TermC.str2term "(SubProblem(Reals_s,[univar,equation],[no_met])\ |
613 val t = TermC.parse_test @{context} "(SubProblem(Reals_s,[univar,equation],[no_met])\ |
614 \ [BOOL e_1, REAL v_1])"; |
614 \ [BOOL e_1, REAL v_1])"; |
615 val s = subst_atomic env t; |
615 val s = subst_atomic env t; |
616 UnparseC.term s; |
616 UnparseC.term s; |
617 "SubProblem (Reals_s, [univar, equation], [no_met])\n\ |
617 "SubProblem (Reals_s, [univar, equation], [no_met])\n\ |
618 \ [BOOL ((a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2), REAL a]"; |
618 \ [BOOL ((a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2), REAL a]"; |
619 val env = env @ [(TermC.str2term "s_1::bool list", |
619 val env = env @ [(TermC.parse_test @{context} "s_1::bool list", |
620 TermC.str2term "[a = 2 * sqrt (r \<up> 2 - (b/2) \<up> 2)]")]; |
620 TermC.parse_test @{context} "[a = 2 * sqrt (r \<up> 2 - (b/2) \<up> 2)]")]; |
621 |
621 |
622 (*--- 6.line in script ---*) |
622 (*--- 6.line in script ---*) |
623 val t = TermC.str2term "Substitute [(v_1 = (rhs o hd) (s_1::bool list))] (h_h::bool)"; |
623 val t = TermC.parse_test @{context} "Substitute [(v_1 = (rhs o hd) (s_1::bool list))] (h_h::bool)"; |
624 val s = subst_atomic env t; |
624 val s = subst_atomic env t; |
625 UnparseC.term s; |
625 UnparseC.term s; |
626 val t = TermC.str2term |
626 val t = TermC.parse_test @{context} |
627 "Substitute [(a = (rhs o hd) [a = 2 * sqrt (r \<up> 2 - (b / 2) \<up> 2)])]\n\ |
627 "Substitute [(a = (rhs o hd) [a = 2 * sqrt (r \<up> 2 - (b / 2) \<up> 2)])]\n\ |
628 \ (A = a * b)"; |
628 \ (A = a * b)"; |
629 (*=== inhibit exn 110726============================================================= |
629 (*=== inhibit exn 110726============================================================= |
630 mem_rls "Prog_Expr.rhs" prog_expr; |
630 mem_rls "Prog_Expr.rhs" prog_expr; |
631 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
631 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
651 \ (s_1::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\ |
651 \ (s_1::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\ |
652 \ [BOOL e_1, REAL v_1]);\ |
652 \ [BOOL e_1, REAL v_1]);\ |
653 \ (s_2::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\ |
653 \ (s_2::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\ |
654 \ [BOOL e_2, REAL v_2])\ |
654 \ [BOOL e_2, REAL v_2])\ |
655 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)"; |
655 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)"; |
656 val f_ = (TermC.str2term "f_f::real", |
656 val f_ = (TermC.parse_test @{context} "f_f::real", |
657 TermC.str2term "A"); |
657 TermC.parse_test @{context} "A"); |
658 val v_v = (TermC.str2term "v_v::real", |
658 val v_v = (TermC.parse_test @{context} "v_v::real", |
659 TermC.str2term "alpha"); |
659 TermC.parse_test @{context} "alpha"); |
660 val eqs=(TermC.str2term "eqs::bool list", |
660 val eqs=(TermC.parse_test @{context} "eqs::bool list", |
661 TermC.str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]"); |
661 TermC.parse_test @{context} "[A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]"); |
662 val env = [f_f, v_v, eqs]; |
662 val env = [f_f, v_v, eqs]; |
663 |
663 |
664 (*--- 1.line in script ---*) |
664 (*--- 1.line in script ---*) |
665 val t = TermC.str2term "(hd o (filterVar (f_f::real))) (eqs::bool list)"; |
665 val t = TermC.parse_test @{context} "(hd o (filterVar (f_f::real))) (eqs::bool list)"; |
666 val s = subst_atomic env t; |
666 val s = subst_atomic env t; |
667 UnparseC.term s; |
667 UnparseC.term s; |
668 val t = TermC.str2term |
668 val t = TermC.parse_test @{context} |
669 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
669 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
670 val SOME (t',_) = rewrite_set_ ctxt false prog_expr t; |
670 val SOME (t',_) = rewrite_set_ ctxt false prog_expr t; |
671 val s' = UnparseC.term t'; |
671 val s' = UnparseC.term t'; |
672 (*=== inhibit exn 110726============================================================= |
672 (*=== inhibit exn 110726============================================================= |
673 if s' = "A = a * b" then() else error "new behaviour with prog_expr 3.1."; |
673 if s' = "A = a * b" then() else error "new behaviour with prog_expr 3.1."; |
674 val env = env @ [(TermC.str2term "h_h::bool", TermC.str2term s')]; |
674 val env = env @ [(TermC.parse_test @{context} "h_h::bool", TermC.parse_test @{context} s')]; |
675 === inhibit exn 110726=============================================================*) |
675 === inhibit exn 110726=============================================================*) |
676 |
676 |
677 (*--- 2.line in script ---*) |
677 (*--- 2.line in script ---*) |
678 val t = TermC.str2term "dropWhile (ident (h_h::bool)) (eqs::bool list)"; |
678 val t = TermC.parse_test @{context} "dropWhile (ident (h_h::bool)) (eqs::bool list)"; |
679 val s = subst_atomic env t; |
679 val s = subst_atomic env t; |
680 UnparseC.term s; |
680 UnparseC.term s; |
681 val t = TermC.str2term |
681 val t = TermC.parse_test @{context} |
682 "dropWhile (ident (A = a * b))\ |
682 "dropWhile (ident (A = a * b))\ |
683 \ [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
683 \ [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
684 (*=== inhibit exn 110726============================================================= |
684 (*=== inhibit exn 110726============================================================= |
685 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
685 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
686 val s' = UnparseC.term t'; |
686 val s' = UnparseC.term t'; |
687 if s' = "[a / 2 = r * sin alpha, b / 2 = r * cos alpha]" |
687 if s' = "[a / 2 = r * sin alpha, b / 2 = r * cos alpha]" |
688 then () else error "new behaviour with prog_expr 3.2."; |
688 then () else error "new behaviour with prog_expr 3.2."; |
689 === inhibit exn 110726=============================================================*) |
689 === inhibit exn 110726=============================================================*) |
690 val env = env @ [(TermC.str2term "es_s::bool list", TermC.str2term s')]; |
690 val env = env @ [(TermC.parse_test @{context} "es_s::bool list", TermC.parse_test @{context} s')]; |
691 |
691 |
692 (*--- 3.line in script ---*) |
692 (*--- 3.line in script ---*) |
693 val t = TermC.str2term "dropWhile (ident (f_f::real)) (Vars (h_h::bool))"; |
693 val t = TermC.parse_test @{context} "dropWhile (ident (f_f::real)) (Vars (h_h::bool))"; |
694 val s = subst_atomic env t; |
694 val s = subst_atomic env t; |
695 UnparseC.term s; |
695 UnparseC.term s; |
696 val t = TermC.str2term "dropWhile (ident A) (Vars (A = a * b))"; |
696 val t = TermC.parse_test @{context} "dropWhile (ident A) (Vars (A = a * b))"; |
697 (*=== inhibit exn 110726============================================================= |
697 (*=== inhibit exn 110726============================================================= |
698 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
698 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
699 val s' = UnparseC.term t'; |
699 val s' = UnparseC.term t'; |
700 if s' = "[a, b]" then () else error "new behaviour with prog_expr 3.3."; |
700 if s' = "[a, b]" then () else error "new behaviour with prog_expr 3.3."; |
701 === inhibit exn 110726=============================================================*) |
701 === inhibit exn 110726=============================================================*) |
702 val env = env @ [(TermC.str2term "vs_s::real list", TermC.str2term s')]; |
702 val env = env @ [(TermC.parse_test @{context} "vs_s::real list", TermC.parse_test @{context} s')]; |
703 |
703 |
704 (*--- 4.line in script ---*) |
704 (*--- 4.line in script ---*) |
705 val t = TermC.str2term "nth_h 1 v_s"; |
705 val t = TermC.parse_test @{context} "nth_h 1 v_s"; |
706 val s = subst_atomic env t; |
706 val s = subst_atomic env t; |
707 UnparseC.term s; |
707 UnparseC.term s; |
708 val t = TermC.str2term "nth_h 1 [a, b]"; |
708 val t = TermC.parse_test @{context} "nth_h 1 [a, b]"; |
709 (*=== inhibit exn 110726============================================================= |
709 (*=== inhibit exn 110726============================================================= |
710 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
710 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
711 val s' = UnparseC.term t'; |
711 val s' = UnparseC.term t'; |
712 if s' = "a" then () else error "new behaviour with prog_expr 3.4."; |
712 if s' = "a" then () else error "new behaviour with prog_expr 3.4."; |
713 === inhibit exn 110726=============================================================*) |
713 === inhibit exn 110726=============================================================*) |
714 val env = env @ [(TermC.str2term "v_1", TermC.str2term s')]; |
714 val env = env @ [(TermC.parse_test @{context} "v_1", TermC.parse_test @{context} s')]; |
715 |
715 |
716 (*--- 5.line in script ---*) |
716 (*--- 5.line in script ---*) |
717 val t = TermC.str2term "nth_h 2 v_s"; |
717 val t = TermC.parse_test @{context} "nth_h 2 v_s"; |
718 val s = subst_atomic env t; |
718 val s = subst_atomic env t; |
719 UnparseC.term s; |
719 UnparseC.term s; |
720 val t = TermC.str2term "nth_h 2 [a, b]"; |
720 val t = TermC.parse_test @{context} "nth_h 2 [a, b]"; |
721 (*=== inhibit exn 110726============================================================= |
721 (*=== inhibit exn 110726============================================================= |
722 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
722 val SOME (t',_) = rewrite_set_ thy false prog_expr t; |
723 val s' = UnparseC.term t'; |
723 val s' = UnparseC.term t'; |
724 if s' = "b" then () else error "new behaviour with prog_expr 3.5."; |
724 if s' = "b" then () else error "new behaviour with prog_expr 3.5."; |
725 === inhibit exn 110726=============================================================*) |
725 === inhibit exn 110726=============================================================*) |
726 val env = env @ [(TermC.str2term "v_2", TermC.str2term s')]; |
726 val env = env @ [(TermC.parse_test @{context} "v_2", TermC.parse_test @{context} s')]; |
727 |
727 |
728 (*--- 6.line in script ---*) |
728 (*--- 6.line in script ---*) |
729 val t = TermC.str2term "(hd o (filterVar v_1)) (es_s::bool list)"; |
729 val t = TermC.parse_test @{context} "(hd o (filterVar v_1)) (es_s::bool list)"; |
730 val s = subst_atomic env t; |
730 val s = subst_atomic env t; |
731 UnparseC.term s; |
731 UnparseC.term s; |
732 val t = TermC.str2term |
732 val t = TermC.parse_test @{context} |
733 "(hd o filterVar a) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
733 "(hd o filterVar a) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
734 val SOME (t',_) = rewrite_set_ ctxt false prog_expr t; |
734 val SOME (t',_) = rewrite_set_ ctxt false prog_expr t; |
735 val s' = UnparseC.term t'; |
735 val s' = UnparseC.term t'; |
736 (*=== inhibit exn 110726============================================================= |
736 (*=== inhibit exn 110726============================================================= |
737 if s' = "a / 2 = r * sin alpha" then () |
737 if s' = "a / 2 = r * sin alpha" then () |
738 else error "new behaviour with prog_expr 3.6."; |
738 else error "new behaviour with prog_expr 3.6."; |
739 === inhibit exn 110726=============================================================*) |
739 === inhibit exn 110726=============================================================*) |
740 val e_1 = TermC.str2term "e_1::bool"; |
740 val e_1 = TermC.parse_test @{context} "e_1::bool"; |
741 val env = env @ [(e_1, TermC.str2term s')]; |
741 val env = env @ [(e_1, TermC.parse_test @{context} s')]; |
742 |
742 |
743 (*--- 7.line in script ---*) |
743 (*--- 7.line in script ---*) |
744 val t = TermC.str2term "(hd o (filterVar v_2)) (es_s::bool list)"; |
744 val t = TermC.parse_test @{context} "(hd o (filterVar v_2)) (es_s::bool list)"; |
745 val s = subst_atomic env t; |
745 val s = subst_atomic env t; |
746 UnparseC.term s; |
746 UnparseC.term s; |
747 val t = TermC.str2term |
747 val t = TermC.parse_test @{context} |
748 "(hd o filterVar b) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
748 "(hd o filterVar b) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
749 val SOME (t',_) = rewrite_set_ ctxt false prog_expr t; |
749 val SOME (t',_) = rewrite_set_ ctxt false prog_expr t; |
750 val s' = UnparseC.term t'; |
750 val s' = UnparseC.term t'; |
751 (*=== inhibit exn 110726============================================================= |
751 (*=== inhibit exn 110726============================================================= |
752 if s' = "b / 2 = r * cos alpha" then () |
752 if s' = "b / 2 = r * cos alpha" then () |
753 else error "new behaviour with prog_expr 3.7."; |
753 else error "new behaviour with prog_expr 3.7."; |
754 === inhibit exn 110726=============================================================*) |
754 === inhibit exn 110726=============================================================*) |
755 val env = env @ [(TermC.str2term "e_2::bool", TermC.str2term s')]; |
755 val env = env @ [(TermC.parse_test @{context} "e_2::bool", TermC.parse_test @{context} s')]; |
756 |
756 |
757 (*--- 8.line in script ---*) |
757 (*--- 8.line in script ---*) |
758 val t = TermC.str2term "(SubProblem (Reals_s,[univar,equation],[no_met])\ |
758 val t = TermC.parse_test @{context} "(SubProblem (Reals_s,[univar,equation],[no_met])\ |
759 \ [BOOL e_1, REAL v_1])"; |
759 \ [BOOL e_1, REAL v_1])"; |
760 val s = subst_atomic env t; |
760 val s = subst_atomic env t; |
761 UnparseC.term s; |
761 UnparseC.term s; |
762 "SubProblem (Reals_s, [univar, equation], [no_met])\ |
762 "SubProblem (Reals_s, [univar, equation], [no_met])\ |
763 \ [BOOL (a / 2 = r * sin alpha), REAL a]"; |
763 \ [BOOL (a / 2 = r * sin alpha), REAL a]"; |
764 val s_1 = TermC.str2term "[a = 2*r*sin alpha]"; |
764 val s_1 = TermC.parse_test @{context} "[a = 2*r*sin alpha]"; |
765 val env = env @ [(TermC.str2term "s_1::bool list", s_1)]; |
765 val env = env @ [(TermC.parse_test @{context} "s_1::bool list", s_1)]; |
766 |
766 |
767 (*--- 9.line in script ---*) |
767 (*--- 9.line in script ---*) |
768 val t = TermC.str2term "(SubProblem (Reals_s,[univar,equation],[no_met])\ |
768 val t = TermC.parse_test @{context} "(SubProblem (Reals_s,[univar,equation],[no_met])\ |
769 \ [BOOL e_2, REAL v_2])"; |
769 \ [BOOL e_2, REAL v_2])"; |
770 val s = subst_atomic env t; |
770 val s = subst_atomic env t; |
771 UnparseC.term s; |
771 UnparseC.term s; |
772 "SubProblem (Reals_s, [univar, equation], [no_met])\ |
772 "SubProblem (Reals_s, [univar, equation], [no_met])\ |
773 \ [BOOL (b / 2 = r * cos alpha), REAL b]"; |
773 \ [BOOL (b / 2 = r * cos alpha), REAL b]"; |
774 val s_2 = TermC.str2term "[b = 2*r*cos alpha]"; |
774 val s_2 = TermC.parse_test @{context} "[b = 2*r*cos alpha]"; |
775 val env = env @ [(TermC.str2term "s_2::bool list", s_2)]; |
775 val env = env @ [(TermC.parse_test @{context} "s_2::bool list", s_2)]; |
776 |
776 |
777 (*--- 10.line in script ---*) |
777 (*--- 10.line in script ---*) |
778 val t = TermC.str2term |
778 val t = TermC.parse_test @{context} |
779 "Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] (h_h::bool)"; |
779 "Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] (h_h::bool)"; |
780 val s = subst_atomic env t; |
780 val s = subst_atomic env t; |
781 UnparseC.term s; |
781 UnparseC.term s; |
782 "Substitute\n [(a = (rhs o hd) [a = 2 * r * sin alpha]),\ |
782 "Substitute\n [(a = (rhs o hd) [a = 2 * r * sin alpha]),\ |
783 \ (b = (rhs o hd) [b = 2 * r * cos alpha])] (A = a * b)"; |
783 \ (b = (rhs o hd) [b = 2 * r * cos alpha])] (A = a * b)"; |