walther@60347
|
1 |
(* Title: Knowledge/eqsystem-2.sml
|
walther@60347
|
2 |
author: Walther Neuper 050826,
|
walther@60347
|
3 |
(c) due to copyright terms
|
walther@60347
|
4 |
*)
|
walther@60347
|
5 |
|
walther@60347
|
6 |
"-----------------------------------------------------------------";
|
walther@60347
|
7 |
"table of contents -----------------------------------------------";
|
walther@60347
|
8 |
"-----------------------------------------------------------------";
|
walther@60347
|
9 |
"----------- occur_exactly_in ------------------------------------";
|
walther@60347
|
10 |
"----------- problems --------------------------------------------";
|
walther@60347
|
11 |
"----------- rewrite-order ord_simplify_System -------------------";
|
walther@60347
|
12 |
"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
|
walther@60347
|
13 |
"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
|
walther@60347
|
14 |
"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
|
walther@60347
|
15 |
"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
|
walther@60347
|
16 |
"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
|
walther@60347
|
17 |
"----------- refine [linear,system]-------------------------------";
|
walther@60347
|
18 |
"----------- refine [2x2,linear,system] search error--------------";
|
walther@60347
|
19 |
"----------- me [EqSystem,normalise,2x2] -------------------------";
|
walther@60347
|
20 |
(*^^^--- eqsystem-1.sml ######### together exceed resources here, but not in Test_Isac.thy #####
|
walther@60347
|
21 |
vvv--- eqsystem-2.sml ######### together exceed resources here, but not in Test_Isac.thy #####*)
|
walther@60347
|
22 |
"----------- me [linear,system] ..normalise..top_down_sub..-------";
|
walther@60347
|
23 |
"----------- all systems from Biegelinie -------------------------";
|
walther@60347
|
24 |
"----------- 4x4 systems from Biegelinie -------------------------";
|
walther@60347
|
25 |
"-----------------------------------------------------------------";
|
walther@60347
|
26 |
"-----------------------------------------------------------------";
|
walther@60347
|
27 |
"-----------------------------------------------------------------";
|
walther@60347
|
28 |
|
walther@60347
|
29 |
val thy = @{theory "EqSystem"};
|
walther@60347
|
30 |
val ctxt = Proof_Context.init_global thy;
|
walther@60347
|
31 |
|
walther@60347
|
32 |
"----------- me [linear,system] ..normalise..top_down_sub..-------";
|
walther@60347
|
33 |
"----------- me [linear,system] ..normalise..top_down_sub..-------";
|
walther@60347
|
34 |
"----------- me [linear,system] ..normalise..top_down_sub..-------";
|
walther@60347
|
35 |
val fmz =
|
walther@60347
|
36 |
["equalities\
|
walther@60347
|
37 |
\[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
|
walther@60347
|
38 |
\ - 1 * q_0 / 24 * 0 \<up> 4),\
|
walther@60347
|
39 |
\ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
|
walther@60347
|
40 |
\ - 1 * q_0 / 24 * L \<up> 4)]",
|
walther@60347
|
41 |
"solveForVars [c, c_2]", "solution LL"];
|
walther@60347
|
42 |
val (dI',pI',mI') =
|
walther@60347
|
43 |
("Biegelinie",["LINEAR", "system"], ["no_met"]);
|
walther@60347
|
44 |
val p = e_pos'; val c = [];
|
walther@60347
|
45 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@60347
|
46 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
47 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
48 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
49 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
50 |
case nxt of (Specify_Method ["EqSystem", "normalise", "2x2"]) => ()
|
walther@60347
|
51 |
| _ => error "eqsystem.sml [linear,system] specify b";
|
walther@60347
|
52 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
53 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
54 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
55 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
56 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
57 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
58 |
if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..
|
walther@60347
|
59 |
"[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
|
walther@60347
|
60 |
"[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
|
walther@60347
|
61 |
then () else error "eqsystem.sml me simpl. before SubProblem b";
|
walther@60347
|
62 |
case nxt of
|
walther@60347
|
63 |
(Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
|
walther@60347
|
64 |
| _ => error "eqsystem.sml me [linear,system] SubProblem b";
|
walther@60347
|
65 |
|
walther@60347
|
66 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
67 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
68 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
69 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
70 |
case nxt of
|
walther@60347
|
71 |
(Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
|
walther@60347
|
72 |
| _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
|
walther@60347
|
73 |
|
walther@60347
|
74 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
75 |
val PblObj {probl,...} = get_obj I pt [5];
|
walther@60360
|
76 |
(writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;
|
walther@60347
|
77 |
(*[
|
walther@60347
|
78 |
(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]])),
|
walther@60347
|
79 |
(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
|
walther@60347
|
80 |
(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
|
walther@60347
|
81 |
*)
|
walther@60347
|
82 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
83 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
84 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
85 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
86 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
87 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
88 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
89 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
90 |
case nxt of
|
walther@60347
|
91 |
(Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
|
walther@60347
|
92 |
| _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
|
walther@60347
|
93 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
94 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
95 |
|
walther@60347
|
96 |
if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..
|
walther@60347
|
97 |
"[c = - 1 * q_0 * L \<up> 3 / (24 * EI), c_2 = 0]"*)
|
walther@60347
|
98 |
"[c = - 1 * q_0 * L \<up> 3 / 24, c_2 = 0]"
|
walther@60347
|
99 |
then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
|
walther@60347
|
100 |
case nxt of
|
walther@60347
|
101 |
(End_Proof') => ()
|
walther@60347
|
102 |
| _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
|
walther@60347
|
103 |
|
walther@60347
|
104 |
|
walther@60347
|
105 |
"----------- all systems from Biegelinie -------------------------";
|
walther@60347
|
106 |
"----------- all systems from Biegelinie -------------------------";
|
walther@60347
|
107 |
"----------- all systems from Biegelinie -------------------------";
|
walther@60347
|
108 |
val thy = @{theory Isac_Knowledge}
|
walther@60347
|
109 |
val subst =
|
walther@60347
|
110 |
[(TermC.str2term "bdv_1", TermC.str2term "c"), (TermC.str2term "bdv_2", TermC.str2term "c_2"),
|
walther@60347
|
111 |
(TermC.str2term "bdv_3", TermC.str2term "c_3"), (TermC.str2term "bdv_4", TermC.str2term "c_4")];
|
walther@60347
|
112 |
|
walther@60347
|
113 |
"------- Bsp 7.27";
|
walther@60347
|
114 |
reset_states ();
|
walther@60347
|
115 |
CalcTree [(
|
walther@60347
|
116 |
["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
|
walther@60347
|
117 |
"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],
|
walther@60347
|
118 |
("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
|
walther@60347
|
119 |
moveActiveRoot 1;
|
walther@60347
|
120 |
(*
|
walther@60347
|
121 |
LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
|
walther@60347
|
122 |
##7.27## ordered substs
|
walther@60347
|
123 |
c_4 c_2
|
walther@60347
|
124 |
c c_2 c_3 c_4 c c_2 1->2: c
|
walther@60347
|
125 |
c_2 c_4
|
walther@60347
|
126 |
c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
|
walther@60347
|
127 |
val t = TermC.str2term
|
walther@60347
|
128 |
("[0 = c_4, " ^
|
walther@60347
|
129 |
"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), " ^
|
walther@60347
|
130 |
"0 = c_2, " ^
|
walther@60347
|
131 |
"0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]");
|
Walther@60500
|
132 |
val SOME (t, _) = rewrite_set_ ctxt false isolate_bdvs_4x4 t;
|
walther@60347
|
133 |
if UnparseC.term t =
|
walther@60347
|
134 |
"[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]"
|
walther@60347
|
135 |
then () else error "Bsp 7.27";
|
walther@60347
|
136 |
|
walther@60347
|
137 |
"----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
|
walther@60347
|
138 |
val t = TermC.str2term "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
|
Walther@60500
|
139 |
val NONE = rewrite_set_ ctxt false norm_Rational t;
|
walther@60347
|
140 |
val SOME (t,_) =
|
Walther@60500
|
141 |
rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
|
walther@60347
|
142 |
if UnparseC.term t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)"
|
walther@60347
|
143 |
then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
|
walther@60347
|
144 |
|
walther@60347
|
145 |
"--- isolate_bdvs_4x4";
|
walther@60347
|
146 |
(*
|
Walther@60500
|
147 |
val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;
|
walther@60347
|
148 |
UnparseC.term t;
|
Walther@60500
|
149 |
val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System t;
|
walther@60347
|
150 |
UnparseC.term t;
|
Walther@60500
|
151 |
val SOME (t,_) = rewrite_set_ ctxt false order_system t;
|
walther@60347
|
152 |
UnparseC.term t;
|
walther@60347
|
153 |
*)
|
walther@60347
|
154 |
|
walther@60347
|
155 |
"------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
|
walther@60347
|
156 |
reset_states ();
|
walther@60347
|
157 |
CalcTree [((*WN130908 <ERROR> error in kernel </ERROR>*)
|
walther@60347
|
158 |
["Traegerlaenge L", "Momentenlinie (-q_0 / L * x \<up> 3 / 6)",
|
walther@60347
|
159 |
"Biegelinie y",
|
walther@60347
|
160 |
"Randbedingungen [y L = 0, y' L = 0]",
|
walther@60347
|
161 |
"FunktionsVariable x"],
|
walther@60347
|
162 |
("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
|
walther@60347
|
163 |
["Biegelinien", "AusMomentenlinie"]))];
|
walther@60347
|
164 |
(*
|
walther@60347
|
165 |
moveActiveRoot 1;
|
walther@60347
|
166 |
LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
|
walther@60347
|
167 |
*)
|
walther@60347
|
168 |
|
walther@60347
|
169 |
"------- Bsp 7.69";
|
walther@60347
|
170 |
reset_states ();
|
walther@60347
|
171 |
CalcTree [(
|
walther@60347
|
172 |
["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
|
walther@60347
|
173 |
"Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],
|
walther@60347
|
174 |
("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
|
walther@60347
|
175 |
moveActiveRoot 1;
|
walther@60347
|
176 |
(*
|
walther@60347
|
177 |
LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
|
walther@60347
|
178 |
##7.69## ordered subst 2x2
|
walther@60347
|
179 |
c_4 c_3
|
walther@60347
|
180 |
c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
|
walther@60347
|
181 |
c_3 c_4
|
walther@60347
|
182 |
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*)
|
walther@60347
|
183 |
val t = TermC.str2term
|
walther@60347
|
184 |
("[0 = c_4 + 0 / (- 1 * EI), " ^
|
walther@60347
|
185 |
"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), " ^
|
walther@60347
|
186 |
"0 = c_3 + 0 / (- 1 * EI), " ^
|
walther@60347
|
187 |
"0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]");
|
walther@60347
|
188 |
|
walther@60347
|
189 |
"------- Bsp 7.70";
|
walther@60347
|
190 |
reset_states ();
|
walther@60347
|
191 |
CalcTree [(
|
walther@60347
|
192 |
["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
|
walther@60347
|
193 |
"Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],
|
walther@60347
|
194 |
("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
|
walther@60347
|
195 |
moveActiveRoot 1;
|
walther@60347
|
196 |
(*
|
walther@60347
|
197 |
LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
|
walther@60347
|
198 |
##7.70## |subst
|
walther@60347
|
199 |
c |
|
walther@60347
|
200 |
c c_2 |1:c -> 2:c_2
|
walther@60347
|
201 |
c_3 |
|
walther@60347
|
202 |
c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
|
walther@60347
|
203 |
|
walther@60347
|
204 |
"----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
|
walther@60347
|
205 |
val t = TermC.str2term
|
walther@60347
|
206 |
("[L * q_0 = c, " ^
|
walther@60347
|
207 |
"0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
|
walther@60347
|
208 |
"0 = c_4, " ^
|
walther@60347
|
209 |
"0 = c_3]");
|
Walther@60500
|
210 |
val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
|
Walther@60500
|
211 |
val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
|
Walther@60500
|
212 |
val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
|
walther@60347
|
213 |
if UnparseC.term t =
|
walther@60347
|
214 |
"[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]"
|
walther@60347
|
215 |
then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
|
walther@60347
|
216 |
|
Walther@60500
|
217 |
val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
|
walther@60347
|
218 |
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]"
|
walther@60347
|
219 |
then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";
|
walther@60347
|
220 |
|
Walther@60500
|
221 |
val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;
|
walther@60347
|
222 |
if UnparseC.term t =
|
walther@60347
|
223 |
"[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^
|
walther@60347
|
224 |
" L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]"
|
walther@60347
|
225 |
then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
|
walther@60347
|
226 |
|
Walther@60500
|
227 |
val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
|
walther@60395
|
228 |
if UnparseC.term t =
|
walther@60395
|
229 |
"[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"
|
walther@60347
|
230 |
then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
|
walther@60347
|
231 |
|
Walther@60500
|
232 |
val SOME (t, _) = rewrite_set_ ctxt false order_system t;
|
walther@60395
|
233 |
if UnparseC.term t =
|
walther@60395
|
234 |
"[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"
|
walther@60347
|
235 |
then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";
|
walther@60347
|
236 |
|
walther@60347
|
237 |
"----- 7.70 with met normalise: ";
|
walther@60347
|
238 |
val fmz = ["equalities" ^
|
walther@60347
|
239 |
"[L * q_0 = c, " ^
|
walther@60347
|
240 |
"0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
|
walther@60347
|
241 |
"0 = c_4, " ^
|
walther@60347
|
242 |
"0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
|
walther@60347
|
243 |
val (dI',pI',mI') = ("Biegelinie",["LINEAR", "system"], ["no_met"]);
|
walther@60347
|
244 |
val p = e_pos'; val c = [];
|
walther@60347
|
245 |
|
walther@60347
|
246 |
(*============ inhibit exn WN120314 TODO: investigate type error (same as above)==
|
walther@60347
|
247 |
in next but one test below the same type error.
|
walther@60347
|
248 |
/-------------------------------------------------------\
|
walther@60347
|
249 |
Type unification failed
|
walther@60347
|
250 |
Type error in application: incompatible operand type
|
walther@60347
|
251 |
|
walther@60347
|
252 |
Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
|
walther@60347
|
253 |
Operand: [c_4] :: 'b list
|
walther@60347
|
254 |
\-------------------------------------------------------/
|
walther@60347
|
255 |
|
walther@60347
|
256 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@60347
|
257 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
258 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
259 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
260 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
261 |
case nxt of (_,Apply_Method ["EqSystem", "normalise", "4x4"]) => ()
|
walther@60347
|
262 |
| _ => error "eqsystem.sml [EqSystem,normalise,4x4] specify";
|
walther@60347
|
263 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
264 |
|
walther@60347
|
265 |
"----- outcommented before Isabelle2002 --> 2011 -------------------------";
|
walther@60347
|
266 |
(*-----------------------------------vvvWN080102 Exception- Match raised
|
walther@60347
|
267 |
since associate Rewrite .. Rewrite_Set
|
walther@60347
|
268 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
269 |
|
walther@60347
|
270 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
271 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
272 |
|
walther@60347
|
273 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
274 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
275 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
276 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
277 |
if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"
|
walther@60347
|
278 |
then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";
|
walther@60347
|
279 |
--------------------------------------------------------------------------*)
|
walther@60347
|
280 |
============ inhibit exn WN120314 ==============================================*)
|
walther@60347
|
281 |
|
walther@60347
|
282 |
"----- 7.70 with met top_down_: me";
|
walther@60347
|
283 |
val fmz = [
|
walther@60347
|
284 |
"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]",
|
walther@60347
|
285 |
"solveForVars [(c::real), (c_2::real), (c_3::real), (c_4::real)]", "solution LL"];
|
walther@60347
|
286 |
val (dI',pI',mI') =
|
walther@60347
|
287 |
("Biegelinie",["LINEAR", "system"],["no_met"]);
|
walther@60347
|
288 |
val p = e_pos'; val c = [];
|
walther@60347
|
289 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@60347
|
290 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
291 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
292 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
293 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
294 |
case nxt of Apply_Method ["EqSystem", "top_down_substitution", "4x4"] => ()
|
walther@60347
|
295 |
| _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
|
walther@60347
|
296 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
297 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
298 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
299 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
300 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
301 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
302 |
if p = ([], Res) andalso
|
walther@60347
|
303 |
(* "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"*)
|
walther@60347
|
304 |
f2str f = "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
|
walther@60347
|
305 |
then () else error "eqsystem.sml: 7.70 with met top_down_: me";
|
walther@60347
|
306 |
|
walther@60347
|
307 |
"------- Bsp 7.71";
|
walther@60347
|
308 |
reset_states ();
|
walther@60347
|
309 |
CalcTree [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
|
walther@60347
|
310 |
"Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",
|
walther@60347
|
311 |
"FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
|
walther@60347
|
312 |
"AbleitungBiegelinie dy"],
|
walther@60347
|
313 |
("Biegelinie", ["Biegelinien"],
|
walther@60347
|
314 |
["IntegrierenUndKonstanteBestimmen2"] ))];
|
walther@60347
|
315 |
moveActiveRoot 1;
|
walther@60347
|
316 |
(*
|
walther@60347
|
317 |
LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
|
walther@60347
|
318 |
##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
|
walther@60347
|
319 |
c c_2 |c c_2 |1' |1': c c_2 |
|
walther@60347
|
320 |
c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
|
walther@60347
|
321 |
c c_2 c_3 c_4 | c_4 |3' | |
|
walther@60347
|
322 |
c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *)
|
walther@60347
|
323 |
val t = TermC.str2term"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \
|
walther@60347
|
324 |
\ 0 = c_4 + 0 / (- 1 * EI), \
|
walther@60347
|
325 |
\ 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),\
|
walther@60347
|
326 |
\ 0 = c_3 + 0 / (- 1 * EI)]";
|
walther@60347
|
327 |
|
walther@60347
|
328 |
"------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
|
walther@60347
|
329 |
reset_states ();
|
walther@60347
|
330 |
CalcTree [(["Traegerlaenge L",
|
walther@60347
|
331 |
"Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x \<up> ^3)",
|
walther@60347
|
332 |
"Biegelinie y",
|
walther@60347
|
333 |
"Randbedingungen [y 0 = (0::real), y L = 0]",
|
walther@60347
|
334 |
"FunktionsVariable x"],
|
walther@60347
|
335 |
("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
|
walther@60347
|
336 |
["Biegelinien", "AusMomentenlinie"]))];
|
walther@60347
|
337 |
moveActiveRoot 1;
|
walther@60347
|
338 |
(*
|
walther@60347
|
339 |
LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
|
walther@60347
|
340 |
*)
|
walther@60347
|
341 |
|
walther@60347
|
342 |
"------- Bsp 7.72b";
|
walther@60347
|
343 |
reset_states ();
|
walther@60347
|
344 |
CalcTree [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",
|
walther@60347
|
345 |
"Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",
|
walther@60347
|
346 |
"FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
|
walther@60347
|
347 |
"AbleitungBiegelinie dy"],
|
walther@60347
|
348 |
("Biegelinie", ["Biegelinien"],
|
walther@60347
|
349 |
["IntegrierenUndKonstanteBestimmen2"] ))];
|
walther@60347
|
350 |
moveActiveRoot 1;
|
walther@60347
|
351 |
(*
|
walther@60347
|
352 |
LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
|
walther@60347
|
353 |
##7.72b## |ord. |subst.singles |ord.triang.
|
walther@60347
|
354 |
c_2 | | |c_2
|
walther@60347
|
355 |
c c_2 | |1:c_2 -> 2':c |c_2 c
|
walther@60347
|
356 |
c_4 | | |
|
walther@60347
|
357 |
c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
|
walther@60347
|
358 |
val t = TermC.str2term"[0 = c_2, \
|
walther@60347
|
359 |
\ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \
|
walther@60347
|
360 |
\ 0 = c_4 + 0 / (- 1 * EI), \
|
walther@60347
|
361 |
\ 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)]";
|
walther@60347
|
362 |
|
walther@60347
|
363 |
"------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
|
walther@60347
|
364 |
reset_states ();
|
walther@60347
|
365 |
CalcTree [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)
|
walther@60347
|
366 |
"Biegelinie y",
|
walther@60347
|
367 |
"Randbedingungen [y L = 0, y' L = 0]",
|
walther@60347
|
368 |
"FunktionsVariable x"],
|
walther@60347
|
369 |
("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
|
walther@60347
|
370 |
["Biegelinien", "AusMomentenlinie"]))];
|
walther@60347
|
371 |
moveActiveRoot 1;
|
walther@60347
|
372 |
(*
|
walther@60347
|
373 |
LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
|
walther@60347
|
374 |
*)
|
walther@60347
|
375 |
|
walther@60347
|
376 |
"----------- 4x4 systems from Biegelinie -------------------------";
|
walther@60347
|
377 |
"----------- 4x4 systems from Biegelinie -------------------------";
|
walther@60347
|
378 |
"----------- 4x4 systems from Biegelinie -------------------------";
|
walther@60347
|
379 |
(*STOPPED.WN08?? replace this test with 7.70 *)
|
walther@60347
|
380 |
"----- Bsp 7.27";
|
walther@60347
|
381 |
val fmz = ["equalities \
|
walther@60347
|
382 |
\[0 = c_4, \
|
walther@60347
|
383 |
\ 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), \
|
walther@60347
|
384 |
\ 0 = c_2, \
|
walther@60347
|
385 |
\ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]",
|
walther@60347
|
386 |
"solveForVars [c, c_2, c_3, c_4]", "solution LL"];
|
walther@60347
|
387 |
val (dI',pI',mI') =
|
walther@60347
|
388 |
("Biegelinie",["normalise", "4x4", "LINEAR", "system"],
|
walther@60347
|
389 |
["EqSystem", "normalise", "4x4"]);
|
walther@60347
|
390 |
val p = e_pos'; val c = [];
|
walther@60347
|
391 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@60347
|
392 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
393 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
394 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
395 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
396 |
"------------------------------------------- Apply_Method...";
|
walther@60347
|
397 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
398 |
"[0 = c_4, \
|
walther@60347
|
399 |
\ 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), \
|
walther@60347
|
400 |
\ 0 = c_2, \
|
walther@60347
|
401 |
\ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]";
|
walther@60347
|
402 |
(*vvvWN080102 Exception- Match raised
|
walther@60347
|
403 |
since associate Rewrite .. Rewrite_Set
|
walther@60347
|
404 |
"------------------------------------------- simplify_System_parenthesized...";
|
walther@60347
|
405 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
406 |
"[0 = c_4, \
|
walther@60347
|
407 |
\ 0 = - 1 * q_0 * L \<up> 4 / (- 24 * EI) + \
|
walther@60347
|
408 |
\ (4 * L \<up> 3 * c / (- 24 * EI) + \
|
walther@60347
|
409 |
\ (12 * L \<up> 2 * c_2 / (- 24 * EI) + \
|
walther@60347
|
410 |
\ (L * c_3 + c_4))), \
|
walther@60347
|
411 |
\ 0 = c_2, \
|
walther@60347
|
412 |
\ 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]";
|
walther@60347
|
413 |
(*? "(4 * L \<up> 3 / (- 24 * EI) * c" statt "(4 * L \<up> 3 * c / (- 24 * EI)" ?*)
|
walther@60347
|
414 |
"------------------------------------------- isolate_bdvs...";
|
walther@60347
|
415 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
416 |
"[c_4 = 0,\
|
walther@60347
|
417 |
\ 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),\
|
walther@60347
|
418 |
\ c_2 = 0, \
|
walther@60347
|
419 |
\ c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2) + - 1 * (L * c)]";
|
walther@60347
|
420 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
walther@60347
|
421 |
|
walther@60347
|
422 |
---------------------------------------------------------------------*)
|