638 |
638 |
639 |
639 |
640 "----------- all systems from Biegelinie -------------------------"; |
640 "----------- all systems from Biegelinie -------------------------"; |
641 "----------- all systems from Biegelinie -------------------------"; |
641 "----------- all systems from Biegelinie -------------------------"; |
642 "----------- all systems from Biegelinie -------------------------"; |
642 "----------- all systems from Biegelinie -------------------------"; |
643 val subst = [(str2term "bdv_1", str2term "c"), |
643 val thy = @{theory Isac} |
644 (str2term "bdv_2", str2term "c_2"), |
644 val subst = |
645 (str2term "bdv_3", str2term "c_3"), |
645 [(str2term "bdv_1", str2term "c"), (str2term "bdv_2", str2term "c_2"), |
646 (str2term "bdv_4", str2term "c_4")]; |
646 (str2term "bdv_3", str2term "c_3"), (str2term "bdv_4", str2term "c_4")]; |
|
647 |
647 "------- Bsp 7.27"; |
648 "------- Bsp 7.27"; |
648 states:=[]; |
649 states:=[]; |
649 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y", |
650 CalcTree [( |
650 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]", |
651 ["Traegerlaenge L","Streckenlast q_0","Biegelinie y", |
651 "FunktionsVariable x"], |
652 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"], |
652 ("Biegelinie", ["Biegelinien"], |
653 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]; |
653 ["IntegrierenUndKonstanteBestimmen2"]))]; |
|
654 moveActiveRoot 1; |
654 moveActiveRoot 1; |
655 (* |
655 (* |
656 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
656 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
657 ##7.27## ordered substs |
657 ##7.27## ordered substs |
658 c_4 c_2 |
658 c_4 c_2 |
659 c c_2 c_3 c_4 c c_2 1->2: c |
659 c c_2 c_3 c_4 c c_2 1->2: c |
660 c_2 c_4 |
660 c_2 c_4 |
661 c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*) |
661 c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*) |
662 val t = str2term"[0 = c_4, \ |
662 val t = str2term |
663 \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \ |
663 ("[0 = c_4, " ^ |
664 \ 0 = c_2, \ |
664 "0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), " ^ |
665 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]"; |
665 "0 = c_2, " ^ |
666 val SOME (t',_) = rewrite_set_ thy false isolate_bdvs_4x4 t; |
666 "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]"); |
667 term2str t'; |
667 val SOME (t, _) = rewrite_set_ thy false isolate_bdvs_4x4 t; |
668 "[c_4 = 0,\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI) =\n 0 + -1 * (c_4 + L * c_3),\n c_2 = 0, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0]"; |
668 if term2str t = |
669 |
669 "[c_4 = 0,\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI) =\n -1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0]" |
670 "----- 7.27 go through the rewrites in met_eqsys_norm_4x4"; |
670 then () else error "Bsp 7.27"; |
|
671 |
|
672 "----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4"; |
671 val t = str2term "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"; |
673 val t = str2term "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"; |
672 val NONE = rewrite_set_ thy false norm_Rational t; |
674 val NONE = rewrite_set_ thy false norm_Rational t; |
673 val SOME (t,_) = |
675 val SOME (t,_) = |
674 rewrite_set_inst_ thy false subst simplify_System_parenthesized t; |
676 rewrite_set_inst_ thy false subst simplify_System_parenthesized t; |
675 term2str t = "0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)"; |
677 if term2str t = "0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)" |
|
678 then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4"; |
|
679 |
676 "--- isolate_bdvs_4x4"; |
680 "--- isolate_bdvs_4x4"; |
677 (* |
681 (* |
678 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t; |
682 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t; |
679 term2str t; |
683 term2str t; |
680 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t; |
684 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t; |
683 term2str t; |
687 term2str t; |
684 *) |
688 *) |
685 |
689 |
686 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed"; |
690 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed"; |
687 states:=[]; |
691 states:=[]; |
688 CalcTree [(["Traegerlaenge L","Momentenlinie (-q_0 / L * x^3 / 6)", |
692 CalcTree [((*WN130908 <ERROR> error in kernel </ERROR>*) |
|
693 ["Traegerlaenge L","Momentenlinie (-q_0 / L * x^^^3 / 6)", |
689 "Biegelinie y", |
694 "Biegelinie y", |
690 "Randbedingungen [y L = 0, y' L = 0]", |
695 "Randbedingungen [y L = 0, y' L = 0]", |
691 "FunktionsVariable x"], |
696 "FunktionsVariable x"], |
692 ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"], |
697 ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"], |
693 ["Biegelinien", "AusMomentenlinie"]))]; |
698 ["Biegelinien", "AusMomentenlinie"]))]; |
|
699 (* |
694 moveActiveRoot 1; |
700 moveActiveRoot 1; |
695 (* |
|
696 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
701 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
697 *) |
702 *) |
698 |
703 |
699 "------- Bsp 7.69"; |
704 "------- Bsp 7.69"; |
700 states:=[]; |
705 states:=[]; |
701 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y", |
706 CalcTree [( |
702 "Randbedingungen [y 0 = 0, y L = 0, y' 0 = 0, y' L = 0]", |
707 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y", |
703 "FunktionsVariable x"], |
708 "Randbedingungen [y 0 = 0, y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"], |
704 ("Biegelinie", ["Biegelinien"], |
709 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]; |
705 ["IntegrierenUndKonstanteBestimmen2"] ))]; |
|
706 moveActiveRoot 1; |
710 moveActiveRoot 1; |
707 (* |
711 (* |
708 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
712 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
709 ##7.69## ordered subst 2x2 |
713 ##7.69## ordered subst 2x2 |
710 c_4 c_3 |
714 c_4 c_3 |
711 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2 |
715 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2 |
712 c_3 c_4 |
716 c_3 c_4 |
713 c c_2 c_3 c c_2 c_3 c_4 3:c_4 -> 4:c c_2 c_3 1:c_3 -> 4:c c_2*) |
717 c c_2 c_3 c c_2 c_3 c_4 3:c_4 -> 4:c c_2 c_3 1:c_3 -> 4:c c_2*) |
714 val t = str2term"[0 = c_4 + 0 / (-1 * EI), \ |
718 val t = str2term |
715 \ 0 = c_4 + L * c_3 + (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \ |
719 ("[0 = c_4 + 0 / (-1 * EI), " ^ |
716 \ 0 = c_3 + 0 / (-1 * EI), \ |
720 "0 = c_4 + L * c_3 + (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), " ^ |
717 \ 0 = c_3 + (6 * L * c_2 + 3 * L ^^^ 2 * c + -1 * L ^^^ 3 * q_0) / (-6 * EI)]"; |
721 "0 = c_3 + 0 / (-1 * EI), " ^ |
|
722 "0 = c_3 + (6 * L * c_2 + 3 * L ^^^ 2 * c + -1 * L ^^^ 3 * q_0) / (-6 * EI)]"); |
718 |
723 |
719 "------- Bsp 7.70"; |
724 "------- Bsp 7.70"; |
720 states:=[]; |
725 states:=[]; |
721 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y", |
726 CalcTree [( |
722 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]", |
727 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y", |
723 "FunktionsVariable x"], |
728 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]", "FunktionsVariable x"], |
724 ("Biegelinie", ["Biegelinien"], |
729 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))]; |
725 ["IntegrierenUndKonstanteBestimmen2"] ))]; |
|
726 moveActiveRoot 1; |
730 moveActiveRoot 1; |
727 (* |
731 (* |
728 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
732 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
729 ##7.70## |subst |
733 ##7.70## |subst |
730 c | |
734 c | |
731 c c_2 |1:c -> 2:c_2 |
735 c c_2 |1:c -> 2:c_2 |
732 c_3 | |
736 c_3 | |
733 c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*) |
737 c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*) |
734 |
738 |
735 |
|
736 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4"; |
739 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4"; |
737 val t = str2term"[L * q_0 = c, \ |
740 val t = str2term |
738 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\ |
741 ("[L * q_0 = c, " ^ |
739 \ 0 = c_4, \ |
742 "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, " ^ |
740 \ 0 = c_3]"; |
743 "0 = c_4, " ^ |
741 val SOME (t,_) = |
744 "0 = c_3]"); |
742 rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t; |
745 val SOME (t,_) = rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t; |
743 val SOME (t,_) = |
746 val SOME (t,_) = rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t; |
744 rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t; |
747 val SOME (t,_) = rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t; |
745 val SOME (t,_) = |
748 if term2str t = |
746 rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t; |
749 "[L * q_0 = c, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0, c_4 = 0,\n c_3 = 0]" |
747 term2str t = |
750 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1"; |
748 "[L * q_0 = c, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0, c_4 = 0,\n c_3 = 0]"; |
751 |
749 val SOME (t,_) = |
752 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t; |
750 rewrite_set_inst_ thy false subst simplify_System_parenthesized t; |
753 if term2str t = "[L * q_0 = c, -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2) = 0, c_4 = 0, c_3 = 0]" |
751 term2str t = |
754 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2"; |
752 "[L * q_0 = c, -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2) = 0, c_4 = 0, c_3 = 0]"; |
755 |
753 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t; |
756 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t; |
754 term2str t = |
757 if term2str t = |
755 "[c = (-1 * (L * q_0) + 0) / -1,\n L * c + c_2 = -1 * (-1 * q_0 * L ^^^ 2 / 2) + 0, c_4 = 0, c_3 = 0]"; |
758 "[c = (-1 * (L * q_0) + 0) / -1,\n" ^ |
756 val SOME (t,_) = |
759 " L * c + c_2 = -1 * (-1 * q_0 * L ^^^ 2 / 2) + 0, c_4 = 0, c_3 = 0]" |
757 rewrite_set_inst_ thy false subst simplify_System_parenthesized t; |
760 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3"; |
758 |
761 |
759 term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]"; |
762 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t; |
760 val SOME (t,_) = rewrite_set_ thy false order_system t; |
763 if term2str t = "[c = -1 * L * q_0 / -1, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]" |
761 if term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]" then () |
764 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4"; |
762 else error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed"; |
765 |
763 |
766 val SOME (t, _) = rewrite_set_ thy false order_system t; |
|
767 if term2str t = "[c = -1 * L * q_0 / -1, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]" |
|
768 then () else error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed"; |
764 |
769 |
765 "----- 7.70 with met normalize: "; |
770 "----- 7.70 with met normalize: "; |
766 val fmz = ["equalities \ |
771 val fmz = ["equalities" ^ |
767 \[L * q_0 = c, \ |
772 "[L * q_0 = c, " ^ |
768 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\ |
773 "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, " ^ |
769 \ 0 = c_4, \ |
774 "0 = c_4, " ^ |
770 \ 0 = c_3]", |
775 "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"]; |
771 "solveForVars [c, c_2, c_3, c_4]", "solution LL"]; |
776 val (dI',pI',mI') = ("Biegelinie",["linear", "system"], ["no_met"]); |
772 val (dI',pI',mI') = |
777 val p = e_pos'; val c = []; |
773 ("Biegelinie",["linear", "system"],["no_met"]); |
778 |
774 val p = e_pos'; val c = []; |
|
775 (*============ inhibit exn WN120314 TODO: investigate type error (same as above)== |
779 (*============ inhibit exn WN120314 TODO: investigate type error (same as above)== |
776 in next but one test below the same type error. |
780 in next but one test below the same type error. |
777 /-------------------------------------------------------\ |
781 /-------------------------------------------------------\ |
778 Type unification failed |
782 Type unification failed |
779 Type error in application: incompatible operand type |
783 Type error in application: incompatible operand type |
788 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
792 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
789 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
793 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
790 case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => () |
794 case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => () |
791 | _ => error "eqsystem.sml [EqSystem,normalize,4x4] specify"; |
795 | _ => error "eqsystem.sml [EqSystem,normalize,4x4] specify"; |
792 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
796 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
|
797 |
793 "----- outcommented before Isabelle2002 --> 2011 -------------------------"; |
798 "----- outcommented before Isabelle2002 --> 2011 -------------------------"; |
794 (*vvvWN080102 Exception- Match raised |
799 (*-----------------------------------vvvWN080102 Exception- Match raised |
795 since assod Rewrite .. Rewrite'_Set |
800 since assod Rewrite .. Rewrite'_Set |
796 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
801 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
797 |
802 |
798 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
803 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
799 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
804 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |