517 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
517 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
518 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
518 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
519 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
519 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
520 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
520 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
521 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
521 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
522 case nxt of ("Specify_Method",_) => () |
522 case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => () |
523 | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify"; |
523 | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify"; |
524 |
524 |
525 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
525 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
526 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
526 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
527 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*); |
527 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*); |
528 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
528 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
529 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
529 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
530 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
530 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
531 case nxt of |
531 case nxt of |
532 (_, Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => () |
532 (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => () |
533 | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem"; |
533 | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem"; |
534 |
534 |
535 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
535 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
536 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
536 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
537 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
537 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
538 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
538 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
539 case nxt of |
539 case nxt of |
540 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () |
540 (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () |
541 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution"; |
541 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution"; |
542 |
542 |
543 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
543 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
544 val PblObj {probl,...} = get_obj I pt [5]; |
544 val PblObj {probl,...} = get_obj I pt [5]; |
545 (writeln o (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) probl; |
545 (writeln o (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) probl; |
555 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
555 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
556 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
556 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
557 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
557 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
558 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
558 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
559 case nxt of |
559 case nxt of |
560 (_, Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => () |
560 (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => () |
561 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished"; |
561 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished"; |
562 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
562 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
563 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
563 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
564 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then () |
564 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then () |
565 else error "eqsystem.sml me [EqSys...2x2] finished f2str f"; |
565 else error "eqsystem.sml me [EqSys...2x2] finished f2str f"; |
566 case nxt of |
566 case nxt of |
567 (_, End_Proof') => () |
567 (End_Proof') => () |
568 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'"; |
568 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'"; |
569 |
569 |
570 "----------- me [linear,system] ..normalise..top_down_sub..-------"; |
570 "----------- me [linear,system] ..normalise..top_down_sub..-------"; |
571 "----------- me [linear,system] ..normalise..top_down_sub..-------"; |
571 "----------- me [linear,system] ..normalise..top_down_sub..-------"; |
572 "----------- me [linear,system] ..normalise..top_down_sub..-------"; |
572 "----------- me [linear,system] ..normalise..top_down_sub..-------"; |
583 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
583 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
584 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
584 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
585 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
585 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
586 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
586 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
587 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
587 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
588 case nxt of (_,Specify_Method ["EqSystem", "normalise", "2x2"]) => () |
588 case nxt of (Specify_Method ["EqSystem", "normalise", "2x2"]) => () |
589 | _ => error "eqsystem.sml [linear,system] specify b"; |
589 | _ => error "eqsystem.sml [linear,system] specify b"; |
590 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
590 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
591 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
591 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
592 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
592 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
593 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
593 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
595 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
595 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
596 if f2str f = |
596 if f2str f = |
597 "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]" |
597 "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]" |
598 then () else error "eqsystem.sml me simpl. before SubProblem b"; |
598 then () else error "eqsystem.sml me simpl. before SubProblem b"; |
599 case nxt of |
599 case nxt of |
600 (_, Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => () |
600 (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => () |
601 | _ => error "eqsystem.sml me [linear,system] SubProblem b"; |
601 | _ => error "eqsystem.sml me [linear,system] SubProblem b"; |
602 |
602 |
603 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
603 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
604 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
604 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
605 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
605 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
606 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
606 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
607 case nxt of |
607 case nxt of |
608 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () |
608 (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () |
609 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b"; |
609 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b"; |
610 |
610 |
611 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
611 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
612 val PblObj {probl,...} = get_obj I pt [5]; |
612 val PblObj {probl,...} = get_obj I pt [5]; |
613 (writeln o (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) probl; |
613 (writeln o (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) probl; |
623 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
623 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
624 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
624 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
625 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
625 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
626 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
626 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
627 case nxt of |
627 case nxt of |
628 (_, Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => () |
628 (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => () |
629 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b"; |
629 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b"; |
630 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
630 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
631 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
631 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
632 |
632 |
633 if f2str f = "[c = -1 * q_0 * L ^^^ 3 / (24 * EI), c_2 = 0]" |
633 if f2str f = "[c = -1 * q_0 * L ^^^ 3 / (24 * EI), c_2 = 0]" |
634 then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b"; |
634 then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b"; |
635 case nxt of |
635 case nxt of |
636 (_, End_Proof') => () |
636 (End_Proof') => () |
637 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'"; |
637 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'"; |
638 |
638 |
639 |
639 |
640 "----------- all systems from Biegelinie -------------------------"; |
640 "----------- all systems from Biegelinie -------------------------"; |
641 "----------- all systems from Biegelinie -------------------------"; |
641 "----------- all systems from Biegelinie -------------------------"; |