eqsystem 4x4, intermediate state start_Take
authorwneuper
Thu, 14 Sep 2006 15:29:45 +0200
branchstart_Take
changeset 660c58b3d2ee7a9
parent 659 d2b8b9b91d9c
child 661 dfcdcbd43ab2
eqsystem 4x4, intermediate state
src/sml/IsacKnowledge/EqSystem.ML
src/sml/IsacKnowledge/Poly.ML
src/sml/IsacKnowledge/Rational.ML
src/smltest/IsacKnowledge/biegelinie.sml
src/smltest/IsacKnowledge/eqsystem.sml
     1.1 --- a/src/sml/IsacKnowledge/EqSystem.ML	Thu Sep 14 09:27:48 2006 +0200
     1.2 +++ b/src/sml/IsacKnowledge/EqSystem.ML	Thu Sep 14 15:29:45 2006 +0200
     1.3 @@ -431,7 +431,7 @@
     1.4   (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_tri" [] e_pblID
     1.5   (["triangular", "4x4", "linear", "system"],
     1.6    [("#Given" ,["equalities es_", "solveForVars vs_"]),
     1.7 -   ("#Where"  ,
     1.8 +   ("#Where" , (*analoguous to 2x2*)
     1.9      ["(tl (tl (tl vs_))) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))",
    1.10       "    (tl (tl vs_))  from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))",
    1.11       "        (tl vs_)   from_ vs_ occur_exactly_in (nth_ 3 (es_::bool list))",
    1.12 @@ -442,6 +442,24 @@
    1.13    prls_triangular, 
    1.14    Some "solveSystem es_ vs_", 
    1.15    [(*["EqSystem","triangular","4x4"]*)]));
    1.16 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ pbl @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
    1.17 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ pbl @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
    1.18 +store_pbt
    1.19 + (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_tri" [] e_pblID
    1.20 + (["triangular", "4x4", "linear", "system"],
    1.21 +  [("#Given" ,["equalities es_", "solveForVars vs_"]),
    1.22 +   ("#Where" , (*accepts missing*)
    1.23 +    ["(tl (tl (tl vs_))) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))",
    1.24 +     "    (tl (tl vs_))  from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))",
    1.25 +     "        (tl vs_)   from_ vs_ occur_exactly_in (nth_ 3 (es_::bool list))",
    1.26 +     "            vs_    from_ vs_ occur_exactly_in (nth_ 4 (es_::bool list))"
    1.27 +     ]),
    1.28 +   ("#Find"  ,["solution ss___"])
    1.29 +  ],
    1.30 +  prls_triangular, 
    1.31 +  Some "solveSystem es_ vs_", 
    1.32 +  [(*["EqSystem","triangular","4x4"]*)]));
    1.33 +@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ pbl @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
    1.34  store_pbt
    1.35   (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_norm" [] e_pblID
    1.36   (["normalize", "4x4", "linear", "system"],
    1.37 @@ -494,18 +512,18 @@
    1.38  "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \
    1.39  \  (let e1__ = Take (hd es_);                                                \
    1.40  \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
    1.41 -\                                      isolate_bdvs False)) @@               \
    1.42 +\                                  isolate_bdvs False))     @@               \
    1.43  \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
    1.44 -\                                  simplify_System False))) e1__;           \
    1.45 +\                                  simplify_System False))) e1__;            \
    1.46  \       e2__ = Take (hd (tl es_));                                           \
    1.47  \       e2__ = ((Substitute [e1__]) @@                                       \
    1.48  \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
    1.49 -\                                  simplify_System_parenthesized False)) @@ \
    1.50 +\                                  simplify_System_parenthesized False)) @@  \
    1.51  \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
    1.52 -\                                      isolate_bdvs False)) @@               \
    1.53 +\                                  isolate_bdvs False))     @@               \
    1.54  \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
    1.55 -\                                  simplify_System False))) e2__;           \
    1.56 -\       es__ = Take [e1__, e2__]\
    1.57 +\                                  simplify_System False))) e2__;            \
    1.58 +\       es__ = Take [e1__, e2__]                                             \
    1.59  \   in (Try (Rewrite_Set order_system False)) es__)"
    1.60  (*---------------------------------------------------------------------------
    1.61    this script does NOT separate the equations as abolve, 
    1.62 @@ -601,8 +619,41 @@
    1.63  \   in (SubProblem (EqSystem_,[linear,system],[no_met])                      \
    1.64  \                  [bool_list_ es__, real_list_ vs_]))"
    1.65  ));
    1.66 -
    1.67 -
    1.68 +store_met
    1.69 +    (prep_met EqSystem.thy "met_eqsys_topdown_4x4" [] e_metID
    1.70 +	 (["EqSystem","top_down_substitution","4x4"],
    1.71 +	  [("#Given" ,["equalities es_", "solveForVars vs_"]),
    1.72 +	   ("#Where"  ,
    1.73 +	    ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))",
    1.74 +	     "    vs_  from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]),
    1.75 +	   ("#Find"  ,["solution ss___"])
    1.76 +	   ],
    1.77 +	  {rew_ord'="ord_simplify_System", rls' = Erls, calc = [], 
    1.78 +	   srls = append_rls "srls_top_down_4x4" e_rls
    1.79 +				  [Thm ("hd_thm",num_str hd_thm),
    1.80 +				   Thm ("tl_Cons",num_str tl_Cons),
    1.81 +				   Thm ("tl_Nil",num_str tl_Nil)
    1.82 +				   ], 
    1.83 +	   prls = prls_triangular, crls = Erls, nrls = Erls},
    1.84 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ met @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
    1.85 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ met @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
    1.86 +"Script SolveSystemScript (es_::bool list) (vs_::real list) =                \
    1.87 +\  (let e1__ = Take (hd es_);                                                \
    1.88 +\       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
    1.89 +\                                  isolate_bdvs False))     @@               \
    1.90 +\               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
    1.91 +\                                  simplify_System False))) e1__;            \
    1.92 +\       e2__ = Take (hd (tl es_));                                           \
    1.93 +\       e2__ = ((Substitute [e1__]) @@                                       \
    1.94 +\               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
    1.95 +\                                  simplify_System_parenthesized False)) @@  \
    1.96 +\               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
    1.97 +\                                  isolate_bdvs False))     @@               \
    1.98 +\               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
    1.99 +\                                  simplify_System False))) e2__;            \
   1.100 +\       es__ = Take [e1__, e2__]                                             \
   1.101 +\   in (Try (Rewrite_Set order_system False)) es__)"
   1.102 +));
   1.103  
   1.104  show_mets();
   1.105  
     2.1 --- a/src/sml/IsacKnowledge/Poly.ML	Thu Sep 14 09:27:48 2006 +0200
     2.2 +++ b/src/sml/IsacKnowledge/Poly.ML	Thu Sep 14 15:29:45 2006 +0200
     2.3 @@ -592,10 +592,13 @@
     2.4  	       (*"0 * z = 0"*)
     2.5  	       Thm ("real_add_zero_left",num_str real_add_zero_left),
     2.6  	       (*"0 + z = z"*)
     2.7 -	       Thm ("real_add_zero_right",num_str real_add_zero_right)
     2.8 +	       Thm ("real_add_zero_right",num_str real_add_zero_right),
     2.9  	       (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
    2.10 +
    2.11  	       (*Thm ("realpow_oneI",num_str realpow_oneI)*)
    2.12  	       (*"?r ^^^ 1 = ?r"*)
    2.13 +	       Thm ("real_0_divide",num_str real_0_divide)(*WN060914*)
    2.14 +	       (*"0 / ?x = 0"*)
    2.15  	       ], scr = EmptyScr}:rls;
    2.16  
    2.17  (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
     3.1 --- a/src/sml/IsacKnowledge/Rational.ML	Thu Sep 14 09:27:48 2006 +0200
     3.2 +++ b/src/sml/IsacKnowledge/Rational.ML	Thu Sep 14 15:29:45 2006 +0200
     3.3 @@ -3505,7 +3505,8 @@
     3.4        }:rls);
     3.5  (*.consists of rls containing the absolute minimum of thms.*)
     3.6  (*040209: this version has been used by RL for his equations,
     3.7 -which is now replaced by MGs version below*)
     3.8 +which is now replaced by MGs version below
     3.9 +vvv OLD VERSION !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
    3.10  val norm_Rational = prep_rls(
    3.11    Rls {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
    3.12        erls = norm_rat_erls, srls = Erls, calc = [], (*asm_thm = [],*)
    3.13 @@ -3515,6 +3516,7 @@
    3.14  	       Rls_ rat_mult_divide,
    3.15  	       Rls_ expand,
    3.16  	       Rls_ reduce_0_1_2,
    3.17 +	       (*^^^^^^^^^ from RL -- not the latest one vvvvvvvvv*)
    3.18  	       Rls_ order_add_mult,
    3.19  	       Rls_ collect_numerals,
    3.20  	       Rls_ add_fractions_p,
    3.21 @@ -3523,18 +3525,18 @@
    3.22        scr = Script ((term_of o the o (parse thy)) 
    3.23        "empty_script")
    3.24        }:rls);
    3.25 -
    3.26  val norm_Rational_parenthesized = prep_rls(
    3.27    Seq {id = "norm_Rational_parenthesized", preconds = []:term list, 
    3.28         rew_ord = ("dummy_ord", dummy_ord),
    3.29        erls = Atools_erls, srls = Erls,
    3.30        calc = [], (*asm_thm = [],*)
    3.31 -      rules = [Rls_  norm_Rational,
    3.32 +      rules = [Rls_  norm_Rational, (*from RL -- not the latest one*)
    3.33  	       Rls_ discard_parentheses
    3.34  	       ],
    3.35        scr = EmptyScr
    3.36        }:rls);      
    3.37  
    3.38 +
    3.39  (*-------------------18.3.03 --> struct <-----------^^^--*)
    3.40  
    3.41  
    3.42 @@ -3651,14 +3653,14 @@
    3.43  val rat_reduce_1 = prep_rls(
    3.44    Rls {id = "rat_reduce_1", preconds = [], 
    3.45         rew_ord = ("dummy_ord",dummy_ord), 
    3.46 -      erls = e_rls, srls = Erls, calc = [], 
    3.47 -      rules = [Thm ("real_divide_1",num_str real_divide_1),
    3.48 -		 (*"?x / 1 = ?x"*)
    3.49 -		Thm ("real_mult_1",num_str real_mult_1)                 
    3.50 +       erls = e_rls, srls = Erls, calc = [], 
    3.51 +       rules = [Thm ("real_divide_1",num_str real_divide_1),
    3.52 +		(*"?x / 1 = ?x"*)
    3.53 +		Thm ("real_mult_1",num_str real_mult_1)           
    3.54  		(*"1 * z = z"*)
    3.55 -	       ],
    3.56 -      scr = Script ((term_of o the o (parse thy)) "empty_script")
    3.57 -      }:rls);
    3.58 +		],
    3.59 +       scr = Script ((term_of o the o (parse thy)) "empty_script")
    3.60 +       }:rls);
    3.61  (* ------------------------------------------------------------------ *)
    3.62  (*. looping part of norm_Rational(*_mg*) .*)
    3.63  val norm_Rational_rls = prep_rls(
    3.64 @@ -3691,6 +3693,7 @@
    3.65         }:rls);
    3.66  (* ------------------------------------------------------------------ *)
    3.67  
    3.68 +
    3.69  ruleset' := overwritelthy thy (!ruleset',
    3.70    [("calculate_Rational", calculate_Rational),
    3.71     ("calc_rat_erls",calc_rat_erls),
     4.1 --- a/src/smltest/IsacKnowledge/biegelinie.sml	Thu Sep 14 09:27:48 2006 +0200
     4.2 +++ b/src/smltest/IsacKnowledge/biegelinie.sml	Thu Sep 14 15:29:45 2006 +0200
     4.3 @@ -833,7 +833,7 @@
     4.4  | _ => raise error "biegelinie.sml met2 nn";
     4.5  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
     4.6  if nxt = ("End_Proof'", End_Proof') andalso f2str f =
     4.7 -   "[0 = c_4 + 0 / (-1 * EI),\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]" then ()
     4.8 +   "[0 = c_4,\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]" then ()
     4.9  else raise error "biegelinie.sml met2 oo";
    4.10  
    4.11  (*
     5.1 --- a/src/smltest/IsacKnowledge/eqsystem.sml	Thu Sep 14 09:27:48 2006 +0200
     5.2 +++ b/src/smltest/IsacKnowledge/eqsystem.sml	Thu Sep 14 15:29:45 2006 +0200
     5.3 @@ -186,7 +186,7 @@
     5.4  	    \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 +         \
     5.5  	    \                                     -1 * q_0 / 24 * L ^^^ 4)]";
     5.6  val Some (t,_) = rewrite_set_ thy true norm_Rational t;
     5.7 -if term2str t="[0 = c_2 + 0 / EI, 0 = c_2 + L * c + L ^^^ 4 * q_0 / (24 * EI)]"
     5.8 +if term2str t="[0 = c_2, 0 = c_2 + L * c + L ^^^ 4 * q_0 / (24 * EI)]"
     5.9  then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
    5.10  
    5.11  val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
    5.12 @@ -963,7 +963,7 @@
    5.13  	     (str2term "bdv_2", str2term "c_2"),
    5.14  	     (str2term "bdv_3", str2term "c_3"),
    5.15  	     (str2term "bdv_4", str2term "c_4")]; 
    5.16 -"----- Bsp 7.27";
    5.17 +"------- Bsp 7.27";
    5.18  states:=[];
    5.19  CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
    5.20  	     "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
    5.21 @@ -973,7 +973,11 @@
    5.22  moveActiveRoot 1;
    5.23  (*
    5.24  trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
    5.25 -##7.27##*)
    5.26 +##7.27##          ordered           substs
    5.27 +          c_4       c_2           
    5.28 +c c_2 c_3 c_4     c c_2             1->2: c
    5.29 +  c_2                       c_4	  
    5.30 +c c_2             c c_2 c_3 c_4     [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
    5.31  val t = str2term"[0 = c_4,                           \
    5.32  \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),                                       \
    5.33  \ 0 = c_2,                                           \
    5.34 @@ -983,13 +987,14 @@
    5.35  "[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]";
    5.36  
    5.37  
    5.38 -"--- go through the rewrites in met_eqsys_norm_4x4";
    5.39 +"----- go through the rewrites in met_eqsys_norm_4x4";
    5.40  val t = str2term "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";
    5.41  val None = rewrite_set_ thy false norm_Rational t;
    5.42  val Some (t,_) = 
    5.43      rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
    5.44 -term2str t;
    5.45 -(*
    5.46 +term2str t = "0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)";
    5.47 +"--- isolate_bdvs_4x4";
    5.48 +(*@@@@@
    5.49  val Some (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
    5.50  term2str t;
    5.51  val Some (t,_) = rewrite_set_inst_ thy false subst simplify_System t;
    5.52 @@ -998,7 +1003,7 @@
    5.53  term2str t;
    5.54  *)
    5.55  
    5.56 -"----- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
    5.57 +"------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
    5.58  states:=[];
    5.59  CalcTree [(["Traegerlaenge L","Momentenlinie (-q_0 / L * x^3 / 6)",
    5.60  	    "Biegelinie y",
    5.61 @@ -1011,7 +1016,7 @@
    5.62  trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
    5.63  *)
    5.64  
    5.65 -"----- Bsp 7.69";
    5.66 +"------- Bsp 7.69";
    5.67  states:=[];
    5.68  CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
    5.69  	     "Randbedingungen [y 0 = 0, y L = 0, y' 0 = 0, y' L = 0]",
    5.70 @@ -1021,13 +1026,17 @@
    5.71  moveActiveRoot 1;
    5.72  (*
    5.73  trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
    5.74 -##7.69##*)
    5.75 -val t = str2term"[0 = c_4 + 0 / (-1 * EI),                                                   \
    5.76 +##7.69##          ordered           subst                   2x2
    5.77 +          c_4           c_3         
    5.78 +c c_2 c_3 c_4     c c_2 c_3	    1:c_3 -> 2:c c_2        2:         c c_2
    5.79 +      c_3                   c_4	 			   
    5.80 +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*)
    5.81 +val t = str2term"[0 = c_4 + 0 / (-1 * EI),                                   \
    5.82  \ 0 = c_4 + L * c_3 + (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),                                                              \
    5.83  \ 0 = c_3 + 0 / (-1 * EI),                                                   \
    5.84  \ 0 = c_3 + (6 * L * c_2 + 3 * L ^^^ 2 * c + -1 * L ^^^ 3 * q_0) / (-6 * EI)]";
    5.85  
    5.86 -"----- Bsp 7.70";
    5.87 +"------- Bsp 7.70";
    5.88  states:=[];
    5.89  CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
    5.90  	     "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
    5.91 @@ -1037,13 +1046,46 @@
    5.92  moveActiveRoot 1;
    5.93  (*
    5.94  trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
    5.95 -##7.70##*)
    5.96 -val t = str2term"[L * q_0 = c,                                       \
    5.97 +##7.70##        |subst
    5.98 +c		|
    5.99 +c c_2           |1:c -> 2:c_2
   5.100 +      c_3	|
   5.101 +          c_4   |            @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
   5.102 +
   5.103 +"----- go through the rewrites in met_eqsys_norm_4x4";
   5.104 +val t = str2term"[L * q_0 = c,                       \
   5.105  \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
   5.106  \ 0 = c_4 + 0 / (-1 * EI),                           \
   5.107  \ 0 = c_3 + 0 / (-1 * EI)]";
   5.108 +val Some (t,_) =
   5.109 +    rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
   5.110 +val Some (t,_) =
   5.111 +    rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
   5.112 +val Some (t,_) =
   5.113 +    rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
   5.114 +term2str t;
   5.115  
   5.116 -"----- Bsp 7.71";
   5.117 +
   5.118 +val Some (t,_) = 
   5.119 +    rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
   5.120 +term2str t;
   5.121 +val Some (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
   5.122 +term2str t;
   5.123 +
   5.124 +val Some (t',_) = rewrite_set_ thy false order_system t;
   5.125 +term2str t';
   5.126 +
   5.127 +val t = str2term"c_3 + 0 / (-1 * EI)";
   5.128 +val Some (t',_) = rewrite_set_ Isac.thy false reduce_0_1_2 t;
   5.129 +term2str t';
   5.130 +rewrite_set_ Isac.thy false norm_Rational t;
   5.131 +term2str t';
   5.132 +trace_rewrite := true;
   5.133 +trace_rewrite := false;
   5.134 +
   5.135 +
   5.136 +
   5.137 +"------- Bsp 7.71";
   5.138  states:=[];
   5.139  CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
   5.140  	     "Randbedingungen [M_b L = 0, y 0 = 0, y L = 0, y' 0 = 0]",
   5.141 @@ -1053,13 +1095,17 @@
   5.142  moveActiveRoot 1;
   5.143  (*
   5.144  trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
   5.145 -##7.71##*)
   5.146 +##7.71##       |ordered       |subst.singles (recurs) |2x2       |diagonal
   5.147 +c c_2          |c c_2	      |1'		      |1': c c_2 |
   5.148 +          c_4  |      c_3     |2:c_3 -> 4' :c c_2 c_4 |	         |
   5.149 +c c_2 c_3 c_4  |          c_4 |3'                     |	         |
   5.150 +      c_3      |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2     |4'':c c_2 |      *)
   5.151  val t = str2term"[0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, \
   5.152  \ 0 = c_4 + 0 / (-1 * EI),                            \
   5.153  \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) /(-24 * EI),\
   5.154  \ 0 = c_3 + 0 / (-1 * EI)]";
   5.155  
   5.156 -"----- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
   5.157 +"------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
   5.158  states:=[];
   5.159  CalcTree [(["Traegerlaenge L",
   5.160  	    "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x^3)",
   5.161 @@ -1073,7 +1119,7 @@
   5.162  trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
   5.163  *)
   5.164  
   5.165 -"----- Bsp 7.72b";
   5.166 +"------- Bsp 7.72b";
   5.167  states:=[];
   5.168  CalcTree [(["Traegerlaenge L","Streckenlast (q_0 / L * x)","Biegelinie y",
   5.169  	    "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = 0, y L = 0]",
   5.170 @@ -1083,13 +1129,17 @@
   5.171  moveActiveRoot 1;
   5.172  (*
   5.173  trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
   5.174 -##7.72b##*)
   5.175 +##7.72b##      |ord. |subst.singles         |ord.triang.
   5.176 +  c_2          |     |			    |c_2  
   5.177 +c c_2	       |     |1:c_2 -> 2':c	    |c_2 c
   5.178 +          c_4  |     |			    |
   5.179 +c c_2 c_3 c_4  |     |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
   5.180  val t = str2term"[0 = c_2,                                            \
   5.181  \ 0 = (6 * c_2 + 6 * L * c + -1 * L ^^^ 2 * q_0) / 6, \
   5.182  \ 0 = c_4 + 0 / (-1 * EI),                            \
   5.183  \ 0 = c_4 + L * c_3 + (60 * L ^^^ 2 * c_2 + 20 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-120 * EI)]";
   5.184  
   5.185 -"----- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
   5.186 +"------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
   5.187  states:=[];
   5.188  CalcTree [(["Traegerlaenge L","Momentenlinie ???",(*description unclear*)
   5.189  	    "Biegelinie y",