Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/eqsystem-2.sml
author wneuper <walther.neuper@jku.at>
Sun, 12 Sep 2021 15:53:36 +0200
changeset 60395 f2e6a3bf46de
parent 60360 49680d595342
child 60500 59a3af532717
permissions -rw-r--r--
cleanup test/../eqsystem-2.sml 
     1 (* Title: Knowledge/eqsystem-2.sml

     2    author: Walther Neuper 050826,

     3    (c) due to copyright terms

     4 *)

     5 

     6 Rewrite.trace_on := false; (*true false*)

     7 "-----------------------------------------------------------------";

     8 "table of contents -----------------------------------------------";

     9 "-----------------------------------------------------------------";

    10 "----------- occur_exactly_in ------------------------------------";

    11 "----------- problems --------------------------------------------";

    12 "----------- rewrite-order ord_simplify_System -------------------";

    13 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";

    14 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";

    15 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";

    16 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";

    17 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";

    18 "----------- refine [linear,system]-------------------------------";

    19 "----------- refine [2x2,linear,system] search error--------------";

    20 "----------- me [EqSystem,normalise,2x2] -------------------------";

    21 (*^^^--- eqsystem-1.sml ######### together exceed resources here, but not in Test_Isac.thy #####

    22   vvv--- eqsystem-2.sml ######### together exceed resources here, but not in Test_Isac.thy #####*)

    23 "----------- me [linear,system] ..normalise..top_down_sub..-------";

    24 "----------- all systems from Biegelinie -------------------------";

    25 "----------- 4x4 systems from Biegelinie -------------------------";

    26 "-----------------------------------------------------------------";

    27 "-----------------------------------------------------------------";

    28 "-----------------------------------------------------------------";

    29 

    30 val thy = @{theory "EqSystem"};

    31 val ctxt = Proof_Context.init_global thy;

    32 

    33 "----------- me [linear,system] ..normalise..top_down_sub..-------";

    34 "----------- me [linear,system] ..normalise..top_down_sub..-------";

    35 "----------- me [linear,system] ..normalise..top_down_sub..-------";

    36 val fmz = 

    37     ["equalities\

    38      \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 +                \

    39      \                                            - 1 * q_0 / 24 * 0 \<up> 4),\

    40      \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 +                \

    41      \                                            - 1 * q_0 / 24 * L \<up> 4)]",

    42      "solveForVars [c, c_2]", "solution LL"];

    43 val (dI',pI',mI') =

    44   ("Biegelinie",["LINEAR", "system"], ["no_met"]);

    45 val p = e_pos'; val c = []; 

    46 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

    47 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

    48 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

    49 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

    50 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    51 case nxt of (Specify_Method ["EqSystem", "normalise", "2x2"]) => ()

    52 	  | _ => error "eqsystem.sml [linear,system] specify b";

    53 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    54 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    55 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    56 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    57 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    58 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    59 if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..

    60   "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)

    61   "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"

    62 then () else error "eqsystem.sml me simpl. before SubProblem b";

    63 case nxt of

    64     (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()

    65   | _ => error "eqsystem.sml me [linear,system] SubProblem b";

    66 

    67 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

    68 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

    69 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

    70 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

    71 case nxt of

    72     (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()

    73   | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";

    74 

    75 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    76 val PblObj {probl,...} = get_obj I pt [5];

    77     (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;

    78 (*[

    79 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),

    80 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),

    81 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]

    82 *)

    83 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    84 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    85 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    86 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    87 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    88 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    89 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    90 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    91 case nxt of

    92     (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()

    93   | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";

    94 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    95 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    96 

    97 if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..

    98   "[c = - 1 * q_0 * L \<up> 3 / (24 * EI), c_2 = 0]"*)

    99   "[c = - 1 * q_0 * L \<up> 3 / 24, c_2 = 0]"

   100 then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";

   101 case nxt of

   102     (End_Proof') => ()

   103   | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";

   104 

   105 

   106 "----------- all systems from Biegelinie -------------------------";

   107 "----------- all systems from Biegelinie -------------------------";

   108 "----------- all systems from Biegelinie -------------------------";

   109 val thy = @{theory Isac_Knowledge}

   110 val subst = 

   111   [(TermC.str2term "bdv_1", TermC.str2term "c"), (TermC.str2term "bdv_2", TermC.str2term "c_2"),

   112 	(TermC.str2term "bdv_3", TermC.str2term "c_3"), (TermC.str2term "bdv_4", TermC.str2term "c_4")]; 

   113 

   114 "------- Bsp 7.27";

   115 reset_states ();

   116 CalcTree [(

   117   ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

   118 	  "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],

   119 	("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];

   120 moveActiveRoot 1;

   121 (*

   122 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

   123 ##7.27##          ordered           substs

   124           c_4       c_2           

   125 c c_2 c_3 c_4     c c_2             1->2: c

   126   c_2                       c_4	  

   127 c c_2             c c_2 c_3 c_4     [2':c, 1:c_2, 3:c_4] -> 4:c_3*)

   128 val t = TermC.str2term

   129   ("[0 = c_4, " ^

   130   "0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^

   131   "0 = c_2, " ^

   132   "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]");

   133 val SOME (t, _) = rewrite_set_ thy false isolate_bdvs_4x4 t;

   134 if UnparseC.term t =

   135 "[c_4 = 0,\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n (- 24 * EI) =\n - 1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0]"

   136 then () else error "Bsp 7.27";

   137 

   138 "----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";

   139 val t = TermC.str2term "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";

   140 val NONE = rewrite_set_ thy false norm_Rational t;

   141 val SOME (t,_) = 

   142     rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

   143 if UnparseC.term t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)"

   144 then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";

   145 

   146 "--- isolate_bdvs_4x4";

   147 (*

   148 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;

   149 UnparseC.term t;

   150 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t;

   151 UnparseC.term t;

   152 val SOME (t,_) = rewrite_set_ thy false order_system t;

   153 UnparseC.term t;

   154 *)

   155 

   156 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";

   157 reset_states ();

   158 CalcTree [((*WN130908  <ERROR> error in kernel </ERROR>*)

   159   ["Traegerlaenge L", "Momentenlinie (-q_0 / L * x \<up> 3 / 6)",

   160 	    "Biegelinie y",

   161 	    "Randbedingungen [y L = 0, y' L = 0]",

   162 	    "FunktionsVariable x"],

   163 	   ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],

   164 	    ["Biegelinien", "AusMomentenlinie"]))];

   165 (*

   166 moveActiveRoot 1;

   167 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

   168 *)

   169 

   170 "------- Bsp 7.69";

   171 reset_states ();

   172 CalcTree [(

   173   ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

   174 	  "Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],

   175 	("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];

   176 moveActiveRoot 1;

   177 (*

   178 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

   179 ##7.69##          ordered           subst                   2x2

   180           c_4           c_3         

   181 c c_2 c_3 c_4     c c_2 c_3	    1:c_3 -> 2:c c_2        2:         c c_2

   182       c_3                   c_4	 			   

   183 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*)

   184 val t = TermC.str2term 

   185   ("[0 = c_4 + 0 / (- 1 * EI), " ^

   186   "0 = c_4 + L * c_3 + (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^

   187   "0 = c_3 + 0 / (- 1 * EI), " ^

   188   "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]");

   189 

   190 "------- Bsp 7.70";

   191 reset_states ();

   192 CalcTree [(

   193   ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

   194 	  "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],

   195 	("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];

   196 moveActiveRoot 1;

   197 (*

   198 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

   199 ##7.70##        |subst

   200 c		|

   201 c c_2           |1:c -> 2:c_2

   202       c_3	|

   203           c_4   |            STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)

   204 

   205 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4";

   206 val t = TermC.str2term

   207   ("[L * q_0 = c, " ^

   208   "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^

   209   "0 = c_4, " ^

   210   "0 = c_3]");

   211 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;

   212 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;

   213 val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;

   214 if UnparseC.term t = 

   215   "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"

   216 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";

   217 

   218 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

   219 if UnparseC.term t = "[L * q_0 = c, - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2) = 0, c_4 = 0,\n c_3 = 0]"

   220 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";

   221 

   222 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;

   223 if UnparseC.term t =

   224    "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^ 

   225    " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]"

   226 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";

   227 

   228 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

   229 if UnparseC.term t =

   230   "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"

   231 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";

   232 

   233 val SOME (t, _) = rewrite_set_ thy false order_system t;

   234 if UnparseC.term t =

   235   "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"

   236 then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";

   237 

   238 "----- 7.70 with met normalise: ";

   239 val fmz = ["equalities" ^

   240   "[L * q_0 = c, " ^

   241   "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^

   242   "0 = c_4, " ^

   243   "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];

   244 val (dI',pI',mI') = ("Biegelinie",["LINEAR", "system"], ["no_met"]);

   245 val p = e_pos'; val c = [];

   246 

   247 (*============ inhibit exn WN120314 TODO: investigate type error (same as above)==

   248   in next but one test below the same type error.

   249 /-------------------------------------------------------\

   250 Type unification failed

   251 Type error in application: incompatible operand type

   252 

   253 Operator:  op # c_3 :: 'a list \<Rightarrow> 'a list

   254 Operand:   [c_4] :: 'b list

   255 \-------------------------------------------------------/

   256 

   257 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   258 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   259 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   260 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   261 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   262 case nxt of (_,Apply_Method ["EqSystem", "normalise", "4x4"]) => ()

   263 	  | _ => error "eqsystem.sml [EqSystem,normalise,4x4] specify";

   264 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   265 

   266 "----- outcommented before Isabelle2002 --> 2011 -------------------------";

   267 (*-----------------------------------vvvWN080102 Exception- Match raised 

   268   since associate Rewrite .. Rewrite_Set

   269 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   270 

   271 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   272 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   273 

   274 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   275 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   276 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   277 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   278 if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]" 

   279 then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";

   280 --------------------------------------------------------------------------*)

   281 ============ inhibit exn WN120314 ==============================================*)

   282 

   283 "----- 7.70 with met top_down_: me";

   284 val fmz = [

   285   "equalities [(c::real) = L * q_0, L * c + (c_2::real) = q_0 * L \<up> 2 / 2, (c_3::real) = 0, (c_4::real) = 0]",

   286 	"solveForVars [(c::real), (c_2::real), (c_3::real), (c_4::real)]", "solution LL"];

   287 val (dI',pI',mI') =

   288   ("Biegelinie",["LINEAR", "system"],["no_met"]);

   289 val p = e_pos'; val c = []; 

   290 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   291 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   292 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   293 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   294 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   295 case nxt of Apply_Method ["EqSystem", "top_down_substitution", "4x4"] => ()

   296 	  | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";

   297 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   298 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   299 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   300 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   301 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   302 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   303 if p = ([], Res) andalso

   304 (*           "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"*)

   305    f2str f = "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"

   306 then () else error "eqsystem.sml: 7.70 with met top_down_: me";

   307 

   308 "------- Bsp 7.71";

   309 reset_states ();

   310 CalcTree [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

   311 	     "Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",

   312 	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

   313 	     "AbleitungBiegelinie dy"],

   314 	    ("Biegelinie", ["Biegelinien"],

   315 	     ["IntegrierenUndKonstanteBestimmen2"] ))];

   316 moveActiveRoot 1;

   317 (*

   318 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

   319 ##7.71##       |ordered       |subst.singles (recurs) |2x2       |diagonal

   320 c c_2          |c c_2	      |1'		      |1': c c_2 |

   321           c_4  |      c_3     |2:c_3 -> 4' :c c_2 c_4 |	         |

   322 c c_2 c_3 c_4  |          c_4 |3'                     |	         |

   323       c_3      |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2     |4'':c c_2 |      *)

   324 val t = TermC.str2term"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \

   325 \ 0 = c_4 + 0 / (- 1 * EI),                            \

   326 \ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /(- 24 * EI),\

   327 \ 0 = c_3 + 0 / (- 1 * EI)]";

   328 

   329 "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";

   330 reset_states ();

   331 CalcTree [(["Traegerlaenge L",

   332 	    "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x \<up> ^3)",

   333 	    "Biegelinie y",

   334 	    "Randbedingungen [y 0 = (0::real), y L = 0]",

   335 	    "FunktionsVariable x"],

   336 	   ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],

   337 	    ["Biegelinien", "AusMomentenlinie"]))];

   338 moveActiveRoot 1;

   339 (*

   340 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

   341 *)

   342 

   343 "------- Bsp 7.72b";

   344 reset_states ();

   345 CalcTree [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",

   346 	    "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",

   347 	    "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

   348 	    "AbleitungBiegelinie dy"],

   349 	   ("Biegelinie", ["Biegelinien"],

   350 	    ["IntegrierenUndKonstanteBestimmen2"] ))];

   351 moveActiveRoot 1;

   352 (*

   353 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

   354 ##7.72b##      |ord. |subst.singles         |ord.triang.

   355   c_2          |     |			    |c_2  

   356 c c_2	       |     |1:c_2 -> 2':c	    |c_2 c

   357           c_4  |     |			    |

   358 c c_2 c_3 c_4  |     |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)

   359 val t = TermC.str2term"[0 = c_2,                                            \

   360 \ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \

   361 \ 0 = c_4 + 0 / (- 1 * EI),                            \

   362 \ 0 = c_4 + L * c_3 + (60 * L \<up> 2 * c_2 + 20 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 120 * EI)]";

   363 

   364 "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";

   365 reset_states ();

   366 CalcTree [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)

   367 	    "Biegelinie y",

   368 	    "Randbedingungen [y L = 0, y' L = 0]",

   369 	    "FunktionsVariable x"],

   370 	   ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],

   371 	    ["Biegelinien", "AusMomentenlinie"]))];

   372 moveActiveRoot 1;

   373 (*

   374 LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;

   375 *)

   376 

   377 "----------- 4x4 systems from Biegelinie -------------------------";

   378 "----------- 4x4 systems from Biegelinie -------------------------";

   379 "----------- 4x4 systems from Biegelinie -------------------------";

   380 (*STOPPED.WN08?? replace this test with 7.70 *)

   381 "----- Bsp 7.27";

   382 val fmz = ["equalities \

   383 	   \[0 = c_4,                           \

   384 	   \ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI),                                       \

   385 	   \ 0 = c_2,                                           \

   386 	   \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]", 

   387 	   "solveForVars [c, c_2, c_3, c_4]", "solution LL"];

   388 val (dI',pI',mI') =

   389   ("Biegelinie",["normalise", "4x4", "LINEAR", "system"],

   390    ["EqSystem", "normalise", "4x4"]);

   391 val p = e_pos'; val c = []; 

   392 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   393 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;

   394 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;

   395 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;

   396 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;

   397 "------------------------------------------- Apply_Method...";

   398 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   399 "[0 = c_4,                                          \

   400 \ 0 = c_4 + L * c_3 +\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI),                                   \

   401 \ 0 = c_2,                                          \

   402 \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]";

   403 (*vvvWN080102 Exception- Match raised 

   404   since associate Rewrite .. Rewrite_Set

   405 "------------------------------------------- simplify_System_parenthesized...";

   406 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   407 "[0 = c_4,                                  \

   408 \ 0 = - 1 * q_0 * L \<up> 4 / (- 24 * EI) +     \

   409 \     (4 * L \<up> 3 * c / (- 24 * EI) +       \

   410 \     (12 * L \<up> 2 * c_2 / (- 24 * EI) +    \

   411 \     (L * c_3 + c_4))),                    \

   412 \ 0 = c_2,                                  \

   413 \ 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]";

   414 (*? "(4 * L \<up> 3 / (- 24 * EI) * c" statt "(4 * L \<up> 3 * c / (- 24 * EI)" ?*)

   415 "------------------------------------------- isolate_bdvs...";

   416 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   417 "[c_4 = 0,\

   418 \ c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 4 / (- 24 * EI)) + - 1 * (4 * L \<up> 3 * c / (- 24 * EI)) + - 1 * (12 * L \<up> 2 * c_2 / (- 24 * EI)) + - 1 * (L * c_3),\

   419 \ c_2 = 0, \

   420 \ c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2) + - 1 * (L * c)]";

   421 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   422 

   423 ---------------------------------------------------------------------*)
wneuper/isa