wneuper/isa: test/Tools/isac/Knowledge/eqsystem-2.sml@41abd196342a

     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 "Knowledge/eqsystem-1.sml";

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

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

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

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

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

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

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

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

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

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

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

    20 "Knowledge/eqsystem-1a.sml";

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

    22 "Knowledge/eqsystem-2.sml";

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

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

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

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

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

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

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

    31 val ctxt = Proof_Context.init_global thy;

    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 model = ["equalities " ^

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

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

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

    40 val refs = ("Biegelinie",["LINEAR", "system"], ["no_met"]);

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

    42 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(model, refs)];

    43                                       val Model_Problem = nxt

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

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

    48 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["normalise", "2x2", "LINEAR", "system"] = nxt

    49                                       val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["EqSystem", "normalise", "2x2"] = nxt

    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; val Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"]) = nxt

    56                                       val "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]" = f2str f;

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

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

    59 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c]" = nxt

    60 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c, c_2]" = nxt

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

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

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

    64 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["EqSystem", "top_down_substitution", "2x2"] = nxt

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

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

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

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

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

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

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

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

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

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

    77 case nxt of

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

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

    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;

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

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

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

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

    87 case nxt of

    88     (End_Proof') => ()

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

    92 "----------- all systems from Biegelinie -------------------------";

    93 "----------- all systems from Biegelinie -------------------------";

    94 "----------- all systems from Biegelinie -------------------------";

    95 val thy = @{theory Isac_Knowledge}

    96 val subst =

    97   [(ParseC.parse_test @{context} "bdv_1", ParseC.parse_test @{context} "c"), (ParseC.parse_test @{context} "bdv_2", ParseC.parse_test @{context} "c_2"),

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

   100 "------- Bsp 7.27";

   101 States.reset ();

   102 CalcTree @{context} [(

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

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

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

   106 moveActiveRoot 1;

   107 (*

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

   109 ##7.27##          ordered           substs

   110           c_4       c_2

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

   112   c_2                       c_4

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

   114 val t = ParseC.parse_test @{context}

   115   ("[0 = c_4, " ^

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

   117   "0 = c_2, " ^

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

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

   120 if UnparseC.term @{context} t =

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

   122 then () else error "Bsp 7.27";

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

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

   126 val NONE = rewrite_set_ ctxt false norm_Rational t;

   127 val SOME (t,_) =

   128     rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;

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

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

   132 "--- isolate_bdvs_4x4";

   133 (*

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

   135 UnparseC.term @{context} t;

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

   137 UnparseC.term @{context} t;

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

   139 UnparseC.term @{context} t;

   140 *)

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

   143 States.reset ();

   144 CalcTree @{context} [((*WN130908  <ERROR> error in kernel </ERROR>*)

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

   146 	    "Biegelinie y",

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

   148 	    "FunktionsVariable x"],

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

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

   151 (*

   152 moveActiveRoot 1;

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

   154 *)

   156 "------- Bsp 7.69";

   157 States.reset ();

   158 CalcTree @{context} [(

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

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

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

   162 moveActiveRoot 1;

   163 (*

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

   165 ##7.69##          ordered           subst                   2x2

   166           c_4           c_3

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

   168       c_3                   c_4

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

   170 val t = ParseC.parse_test @{context}

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

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

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

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

   176 "------- Bsp 7.70";

   177 States.reset ();

   178 CalcTree @{context} [(

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

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

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

   182 moveActiveRoot 1;

   183 (*

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

   185 ##7.70##        |subst

   186 c		|

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

   188       c_3	|

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

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

   192 val t = ParseC.parse_test @{context}

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

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

   195   "0 = c_4, " ^

   196   "0 = c_3]");

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

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

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

   200 if UnparseC.term @{context} t =

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

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

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

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

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

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

   209 if UnparseC.term @{context} t =

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

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

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

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

   215 if UnparseC.term @{context} t =

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

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

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

   220 if UnparseC.term @{context} t =

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

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

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

   225 val fmz = ["equalities" ^

   226   "[L * q_0 = c, " ^

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

   228   "0 = c_4, " ^

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

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

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

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

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

   235 /-------------------------------------------------------\

   236 Type unification failed

   237 Type error in application: incompatible operand type

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

   240 Operand:   [c_4] :: 'b list

   241 \-------------------------------------------------------/

   243 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

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

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

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

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

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

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

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

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

   253 (*-----------------------------------vvvWN080102 Exception- Match raised

   254   since associate Rewrite .. Rewrite_Set

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

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

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

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

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

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

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

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

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

   266 --------------------------------------------------------------------------*)

   267 ============ inhibit exn WN120314 ==============================================*)

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

   270 val fmz = [

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

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

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

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

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

   276 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

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

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

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

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

   281 val (p,_,f,nxt,_,pt) = me nxt p c pt; val  Add_Given "solveForVars [c_2, c, c_3, c_4]" = nxt

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

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

   284 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["EqSystem", "top_down_substitution", "4x4"] = nxt

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

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

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

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

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

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

   292 val ([], Res) = p

   293 val "c = L * q_0" = f2str f;

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

   297 "------- Bsp 7.71";

   298 States.reset ();

   299 CalcTree @{context} [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

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

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

   302 	     "AbleitungBiegelinie dy"],

   303 	    ("Biegelinie", ["Biegelinien"],

   304 	     ["IntegrierenUndKonstanteBestimmen2"] ))];

   305 moveActiveRoot 1;

   306 (*

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

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

   309 c c_2          |c c_2	      |1'		      |1': c c_2 |

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

   311 c c_2 c_3 c_4  |          c_4 |3'                     |	         |

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

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

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

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

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

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

   320 States.reset ();

   321 CalcTree @{context} [(["Traegerlaenge L",

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

   323 	    "Biegelinie y",

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

   325 	    "FunktionsVariable x"],

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

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

   328 moveActiveRoot 1;

   329 (*

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

   331 *)

   333 "------- Bsp 7.72b";

   334 States.reset ();

   335 CalcTree @{context} [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",

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

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

   338 	    "AbleitungBiegelinie dy"],

   339 	   ("Biegelinie", ["Biegelinien"],

   340 	    ["IntegrierenUndKonstanteBestimmen2"] ))];

   341 moveActiveRoot 1;

   342 (*

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

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

   345   c_2          |     |			    |c_2

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

   347           c_4  |     |			    |

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

   349 val t = ParseC.parse_test @{context}"[0 = c_2,                                            \

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

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

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

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

   355 States.reset ();

   356 CalcTree @{context} [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)

   357 	    "Biegelinie y",

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

   359 	    "FunktionsVariable x"],

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

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

   362 moveActiveRoot 1;

   363 (*

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

   365 *)

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

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

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

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

   372 "----- Bsp 7.27";

   373 val fmz = ["equalities \

   374 	   \[0 = c_4,                           \

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

   376 	   \ 0 = c_2,                                           \

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

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

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

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

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

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

   383 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

   384 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities [0 = c_4]" = nxt

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

   386 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities\n [0 =\n  c_4 + L * c_3 +\n  (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n  (- 24 * EI),\n  0 = c_4, 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]" = nxt

   387 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c]" = nxt

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

   389 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c_2, c, c_3, c_4]" = nxt

   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 Apply_Method ["EqSystem", "normalise", "4x4"] = nxt

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

   394 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("commute_0_equality", _(*"(0 = ?a) = (?a = 0)"*)) = nxt

   395 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("commute_0_equality", _(*"(0 = ?a) = (?a = 0)"*)) = nxt

   396 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("commute_0_equality", _(*"(0 = ?a) = (?a = 0)"*)) = nxt

   397 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("commute_0_equality", _(*"(0 = ?a) = (?a = 0)"*)) = nxt

   398 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv_1'', c_3)", "(''bdv_2'', c)", "(''bdv_3'', c_2)", "(''bdv_3'', c_4)"], "simplify_System_parenthesized") = nxt

   399 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv_1'', c_3)", "(''bdv_2'', c)", "(''bdv_3'', c_2)", "(''bdv_3'', c_4)"], "isolate_bdvs_4x4") = nxt

   400 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv_1'', c_3)", "(''bdv_2'', c)", "(''bdv_3'', c_2)", "(''bdv_3'', c_4)"], "simplify_System_parenthesized") = nxt

   401 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set "order_system" = nxt

   402 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["normalise", "4x4", "LINEAR", "system"]) = nxt

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

   404 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities [c_2 = 0, c_4 = 0]" = nxt

   405 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities [c_2 = 0, c_4 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = nxt

   406 (*WN231124 -------------------------------strange---^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^*)

   407 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities\n [c_4 = 0, c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2,\n  L \<up> 3 * c / - 6 +\n  (L \<up> 2 * c_2 / - 2 + (- 1 * L * c_3 / - 1 + - 1 * c_4 / - 1)) =\n  q_0 * L \<up> 4 / - 24]" = nxt

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

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

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

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

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

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

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

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

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

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

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

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

   420 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["EqSystem", "normalise", "4x4"] = nxt

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

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

   423   = f2str f;

   424 (*WN231124 probably does not terminate*)

   425 (*old note:*)

   426 "[0 = c_4,                                          " ^

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

   428 " 0 = c_2,                                          " ^

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

author	wneuper <Walther.Neuper@jku.at>
	Mon, 11 Dec 2023 09:24:02 +0100
changeset 60778	41abd196342a
parent 60766	2e0603ca18a4
permissions	-rw-r--r--