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>
Wed, 19 Oct 2022 10:43:04 +0200
changeset 60567 bb3140a02f3d
parent 60565 f92963a33fe3
child 60571 19a172de0bb5
permissions -rw-r--r--
eliminate term2str in src, Prog_Tac.*_adapt_to_type 
     1 (* Title: Knowledge/eqsystem-2.sml

     2    author: Walther Neuper 050826,

     3    (c) due to copyright terms

     4 *)

     5 "-----------------------------------------------------------------------------------------------";

     6 "table of contents -----------------------------------------------------------------------------";

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

     8 "----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";

     9 "----------- problems -----------------------------------------------------------equsystem-1.sml";

    10 "----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";

    11 "----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";

    12 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";

    13 "----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";

    14 "----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";

    15 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";

    16 "----------- refine [linear,system]----------------------------------------------equsystem-1.sml";

    17 "----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";

    18 "----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";

    19 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

    20 "----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";

    21 "----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";

    22 "----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";

    23 "-----------------------------------------------------------------------------------------------";

    24 "-----------------------------------------------------------------------------------------------";

    25 "-----------------------------------------------------------------------------------------------";

    26 

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

    28 val ctxt = Proof_Context.init_global thy;

    29 

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

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

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

    33 val fmz = 

    34     ["equalities\

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    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 if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..

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

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

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

    60 case nxt of

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

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

    63 

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

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

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

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

    68 case nxt of

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

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

    71 

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

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

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

    75 (*[

    76 (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]])),

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

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

    79 *)

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

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

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

    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 case nxt of

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

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

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

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

    93 

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

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

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

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

    98 case nxt of

    99     (End_Proof') => ()

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

   101 

   102 

   103 "----------- all systems from Biegelinie -------------------------";

   104 "----------- all systems from Biegelinie -------------------------";

   105 "----------- all systems from Biegelinie -------------------------";

   106 val thy = @{theory Isac_Knowledge}

   107 val subst = 

   108   [(TermC.parse_test @{context} "bdv_1", TermC.parse_test @{context} "c"), (TermC.parse_test @{context} "bdv_2", TermC.parse_test @{context} "c_2"),

   109 	(TermC.parse_test @{context} "bdv_3", TermC.parse_test @{context} "c_3"), (TermC.parse_test @{context} "bdv_4", TermC.parse_test @{context} "c_4")]; 

   110 

   111 "------- Bsp 7.27";

   112 States.reset ();

   113 CalcTree [(

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

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

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

   117 moveActiveRoot 1;

   118 (*

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

   120 ##7.27##          ordered           substs

   121           c_4       c_2           

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

   123   c_2                       c_4	  

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

   125 val t = TermC.parse_test @{context}

   126   ("[0 = c_4, " ^

   127   "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), " ^

   128   "0 = c_2, " ^

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

   130 val SOME (t, _) = rewrite_set_ ctxt false isolate_bdvs_4x4 t;

   131 if UnparseC.term t =

   132 "[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]"

   133 then () else error "Bsp 7.27";

   134 

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

   136 val t = TermC.parse_test @{context} "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";

   137 val NONE = rewrite_set_ ctxt false norm_Rational t;

   138 val SOME (t,_) = 

   139     rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;

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

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

   142 

   143 "--- isolate_bdvs_4x4";

   144 (*

   145 val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;

   146 UnparseC.term t;

   147 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System t;

   148 UnparseC.term t;

   149 val SOME (t,_) = rewrite_set_ ctxt false order_system t;

   150 UnparseC.term t;

   151 *)

   152 

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

   154 States.reset ();

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

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

   157 	    "Biegelinie y",

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

   159 	    "FunktionsVariable x"],

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

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

   162 (*

   163 moveActiveRoot 1;

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

   165 *)

   166 

   167 "------- Bsp 7.69";

   168 States.reset ();

   169 CalcTree [(

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

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

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

   173 moveActiveRoot 1;

   174 (*

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

   176 ##7.69##          ordered           subst                   2x2

   177           c_4           c_3         

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

   179       c_3                   c_4	 			   

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

   181 val t = TermC.parse_test @{context} 

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

   183   "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), " ^

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

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

   186 

   187 "------- Bsp 7.70";

   188 States.reset ();

   189 CalcTree [(

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

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

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

   193 moveActiveRoot 1;

   194 (*

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

   196 ##7.70##        |subst

   197 c		|

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

   199       c_3	|

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

   201 

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

   203 val t = TermC.parse_test @{context}

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

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

   206   "0 = c_4, " ^

   207   "0 = c_3]");

   208 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;

   209 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;

   210 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;

   211 if UnparseC.term t = 

   212   "[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]"

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

   214 

   215 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;

   216 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]"

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

   218 

   219 val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;

   220 if UnparseC.term t =

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

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

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

   224 

   225 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;

   226 if UnparseC.term t =

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

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

   229 

   230 val SOME (t, _) = rewrite_set_ ctxt false order_system t;

   231 if UnparseC.term t =

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

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

   234 

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

   236 val fmz = ["equalities" ^

   237   "[L * q_0 = c, " ^

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

   239   "0 = c_4, " ^

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

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

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

   243 

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

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

   246 /-------------------------------------------------------\

   247 Type unification failed

   248 Type error in application: incompatible operand type

   249 

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

   251 Operand:   [c_4] :: 'b list

   252 \-------------------------------------------------------/

   253 

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

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

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

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

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

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

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

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

   262 

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

   264 (*-----------------------------------vvvWN080102 Exception- Match raised 

   265   since associate Rewrite .. Rewrite_Set

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

   267 

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

   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 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

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

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

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

   277 --------------------------------------------------------------------------*)

   278 ============ inhibit exn WN120314 ==============================================*)

   279 

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

   281 val fmz = [

   282   "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]",

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   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 if p = ([], Res) andalso

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

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

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

   304 

   305 "------- Bsp 7.71";

   306 States.reset ();

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

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

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

   310 	     "AbleitungBiegelinie dy"],

   311 	    ("Biegelinie", ["Biegelinien"],

   312 	     ["IntegrierenUndKonstanteBestimmen2"] ))];

   313 moveActiveRoot 1;

   314 (*

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

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

   317 c c_2          |c c_2	      |1'		      |1': c c_2 |

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

   319 c c_2 c_3 c_4  |          c_4 |3'                     |	         |

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

   321 val t = TermC.parse_test @{context}"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \

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

   323 \ 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),\

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

   325 

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

   327 States.reset ();

   328 CalcTree [(["Traegerlaenge L",

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

   330 	    "Biegelinie y",

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

   332 	    "FunktionsVariable x"],

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

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

   335 moveActiveRoot 1;

   336 (*

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

   338 *)

   339 

   340 "------- Bsp 7.72b";

   341 States.reset ();

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

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

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

   345 	    "AbleitungBiegelinie dy"],

   346 	   ("Biegelinie", ["Biegelinien"],

   347 	    ["IntegrierenUndKonstanteBestimmen2"] ))];

   348 moveActiveRoot 1;

   349 (*

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

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

   352   c_2          |     |			    |c_2  

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

   354           c_4  |     |			    |

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

   356 val t = TermC.parse_test @{context}"[0 = c_2,                                            \

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

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

   359 \ 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)]";

   360 

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

   362 States.reset ();

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

   364 	    "Biegelinie y",

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

   366 	    "FunktionsVariable x"],

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

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

   369 moveActiveRoot 1;

   370 (*

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

   372 *)

   373 

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

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

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

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

   378 "----- Bsp 7.27";

   379 val fmz = ["equalities \

   380 	   \[0 = c_4,                           \

   381 	   \ 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),                                       \

   382 	   \ 0 = c_2,                                           \

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

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

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

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

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

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

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

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

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

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

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

   394 "------------------------------------------- Apply_Method...";

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

   396 "[0 = c_4,                                          \

   397 \ 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),                                   \

   398 \ 0 = c_2,                                          \

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

   400 (*vvvWN080102 Exception- Match raised 

   401   since associate Rewrite .. Rewrite_Set

   402 "------------------------------------------- simplify_System_parenthesized...";

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

   404 "[0 = c_4,                                  \

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

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

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

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

   409 \ 0 = c_2,                                  \

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

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

   412 "------------------------------------------- isolate_bdvs...";

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

   414 "[c_4 = 0,\

   415 \ 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),\

   416 \ c_2 = 0, \

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

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

   419 

   420 ---------------------------------------------------------------------*)
wneuper/isa