1 (* "Knowledge/biegelinie-4.sml"
2 author: Walther Neuper 190515
3 (c) due to copyright terms
5 "table of contents ---------------------------------------------------------------------------";
6 "---------------------------------------------------------------------------------------------";
7 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";
8 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' --------------------------------";
9 "----------- biegel Bsp.7.70. check Problem + MethodC model ----------------------------------";
10 "---------------------------------------------------------------------------------------------";
11 "---------------------------------------------------------------------------------------------";
12 "---------------------------------------------------------------------------------------------";
15 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";
16 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";
17 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";
18 (* the error in this test might be independent from introduction of y, dy
19 as arguments in IntegrierenUndKonstanteBestimmen2,
20 rather due to so far untested use of "auto" *)
21 val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
22 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
23 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
24 "AbleitungBiegelinie dy"];
25 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
28 CalcTree @{context} [(fmz, (dI',pI',mI'))];
31 autoCalculate 1 CompleteCalc;
33 val ((pt, p),_) = States.get_calc 1;
34 if p = ([], Pbl) then () else error ""
35 get_obj I pt (fst p); (*TODO investigate failure*)
37 (* NOTE: \<up> \<up> \<up> \<up> \<up> ^^ no progress already in isabisac15, but not noticed \<up> \<up> \<up> \<up> \<up> ^^ * )
38 (*[], Met*)autoCalculate 1 CompleteCalcHead;
39 (*[1], Pbl*)autoCalculate 1 (Steps 1); (* into SubProblem *)
40 (*[1], Res*)autoCalculate 1 CompleteSubpbl; (**)
41 (*[2], Pbl*)autoCalculate 1 (Steps 1); (* out of SubProblem *)
42 (*[2], Res*)autoCalculate 1 CompleteSubpbl;
43 (*[3], Pbl*)autoCalculate 1 (Steps 1); (* out of SubProblem *)
44 (*[3], Met*)autoCalculate 1 CompleteCalcHead;
45 (*[3, 1], Frm*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
46 (*(**)autoCalculate 1 CompleteSubpbl; error in kernel 4: Step.add: not impl.for Empty_Tac_*)
47 (*[3, 1], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
48 (*[3, 2], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
49 (*[3, 3], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
50 (*[3, 4], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
51 (*[3, 5], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
52 (*[3, 6], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
53 (*[3, 7], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
54 (*[3, 8], Pbl*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
55 (*[3, 8], Met*)autoCalculate 1 CompleteCalcHead;
56 (*[3, 8, 1], Frm*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
57 (*[3, 8, 1], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
58 (*(**)autoCalculate 1 (Steps 1);
59 *** Step.add: not impl.for Empty_Tac_
60 val it = <AUTOCALC><CALCID>1</CALCID><CALCMESSAGE>helpless</CALCMESSAGE></AUTOCALC>: XML.tree *)
62 val ((pt,_),_) = States.get_calc 1;
63 val ip = States.get_pos 1 1;
64 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
66 if ip = ([3, 8, 1], Res) andalso
67 UnparseC.term @{context} f = "[- 1 * c_4 / - 1 = 0,\n (6 * c_4 * EI + 6 * L * c_3 * EI + -3 * L \<up> 2 * c_2 + - 1 * L \<up> 3 * c) /\n (6 * EI) =\n L \<up> 4 * q_0 / (- 24 * EI),\n c_2 = 0, c_2 + L * c = L \<up> 2 * q_0 / 2]"
70 SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => ()
71 | _ => error "ERROR biegel.7.70 changed 1"
72 else error "ERROR biegel.7.70 changed 2";
73 ( * NOTE: \<up> \<up> \<up> \<up> \<up> ^^ no progress already in isabisac15, but not noticed \<up> \<up> \<up> \<up> \<up> ^^ *)
76 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' --------------------------------";
77 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' --------------------------------";
78 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' --------------------------------";
80 val (tac as Model_Problem (*["Biegelinien"]*), (pt, p as ([], Pbl))) =
81 Test_Code.init_calc' @{context} [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
82 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",
83 "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"],
84 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
86 val (tac as Model_Problem (*["vonBelastungZu", "Biegelinien"]*), (pt, p as ([1], Pbl))) =
87 (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
88 (*INVISIBLE: SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
90 val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 2], Res))) =
91 (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
92 val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 3, 2], Res))) =
93 (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
95 val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 4], Res))) =
96 (tac, (pt, p)) |> me' |> me';
97 val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 5, 1], Res))) =
98 (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
100 val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 7], Res))) =
101 (tac, (pt, p)) |> me' |> me' |> me';
102 val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 8, 2], Res))) =
103 (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
105 val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 8], Res))) =
106 (tac, (pt, p)) |> me';
107 val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 9, 1], Res))) =
108 (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
110 val (tac as Check_Postcond ["vonBelastungZu", "Biegelinien"], (pt, p as ([1, 9], Res))) =
111 (tac, (pt, p)) |> me';
113 val (tac as Subproblem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"]), (pt, p as ([1], Res))) =
114 (tac, (pt, p)) |> me';
116 (*INVISIBLE: SubProblem (''Biegelinie'', [''makeFunctionTo'', ''"equation''])*)
117 val (tac as Model_Problem (*[''makeFunctionTo'', ''"equation'']*), (pt, p as ([2], Pbl))) =
118 (tac, (pt, p)) |> me'
120 (*INVISIBLE: SubProblem (''Biegelinie'', [''makeFunctionTo'', ''"equation''])*)
121 val (tac as Model_Problem (*[''makeFunctionTo'', ''"equation'']*), (pt, p as ([2, 1], Pbl))) =
122 (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
123 (* ERROR for a long time -----vvvvvvvvvvvvvvvvvvvvvvvv.. (should be evaluated!) *)
124 val (tac as Substitute ["x = (argument_in lhs (NTH 1 [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]))"], (pt, p as ([2, 1, 1], Frm))) =
125 (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
127 if p = ([2, 1, 1], Frm) andalso (Calc.current_formula (pt, p) |> UnparseC.term @{context}) =
128 "y x =\nc_4 + c_3 * x +\n1 / (- 1 * EI) *\n(c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)"
129 then () else error "";
132 (**** biegel Bsp.7.70. check Problem + MethodC model ##################################### ****)
133 "----------- biegel Bsp.7.70. check Problem + MethodC model ----------------------------------";
134 "----------- biegel Bsp.7.70. check Problem + MethodC model ----------------------------------";
135 (*this formalisation contains no variants, as opposed to maximum example*)
136 val (tac as Model_Problem (*["Biegelinien"]*), ptp as (pt, p as ([], Pbl))) =
137 Test_Code.init_calc' @{context} [([
139 "Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
140 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
142 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"],
143 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
145 (*** stepwise Specification: Problem model================================================= ***)
146 val ("ok", ([(Model_Problem, _, _)], _, ptp))
147 = Step.specify_do_next ptp;
148 val ("ok", ([(Add_Given "Traegerlaenge L", _, _)], _, ptp))
149 = Step.specify_do_next ptp;
150 val ("ok", ([(Add_Given "Streckenlast q_0", _, _)], _, ptp))
151 = Step.specify_do_next ptp;
152 val ("ok", ([(Add_Find "Biegelinie y", _, _)], _, ptp))
153 = Step.specify_do_next ptp;
154 val ("ok", ([(Add_Relation "Randbedingungen [y 0 = 0]", _, _)], _, ptp))
155 = Step.specify_do_next ptp;
156 val ("ok", ([(Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]", _, _)], _, ptp))
157 = Step.specify_do_next ptp;
159 (*** Problem model is complete ============================================================ ***)
160 val PblObj {probl, ...} = get_obj I (fst ptp) [];
161 if I_Model.to_string @{context} probl = "[\n" ^
162 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
163 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
164 "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
165 "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]))]"
166 then () else error "I_Model.to_string probl CHANGED";
168 (*** Specification of References ========================================================== ***)
169 val ("ok", ([(Specify_Theory "Biegelinie", _, _)], _, ptp))
170 = Step.specify_do_next ptp;
171 val ("ok", ([(Specify_Problem ["Biegelinien"], _, _)], _, ptp))
172 = Step.specify_do_next ptp;
173 val ("ok", ([(Specify_Method ["IntegrierenUndKonstanteBestimmen2"], _, _)], _, ptp))
174 = Step.specify_do_next ptp;
176 (*** stepwise Specification: MethodC model ================================================ ***)
177 val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], _, ptp))
178 = Step.specify_do_next ptp;
179 val ("ok", ([(Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]", _, _)], _, ptp))
180 = Step.specify_do_next ptp;
181 val ("ok", ([(Add_Given "AbleitungBiegelinie dy", _, _)], _, ptp))
182 = Step.specify_do_next ptp;
184 (*** Specification of Problem and MethodC model is completes ============================== ***)
185 val PblObj {meth, ...} = get_obj I (fst ptp) [];
186 if I_Model.to_string @{context} meth = "[\n" ^
187 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
188 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
189 "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
190 "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^
191 "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(fun_var, [x])), \n" ^
192 "(6 ,[1] ,true ,#Given ,Cor GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]])), \n" ^
193 "(7 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"
194 then () else error "I_Model.to_string meth CHANGED";
196 (*** Solution starts ====================================================================== ***)
197 val ("ok", ([(Apply_Method ["IntegrierenUndKonstanteBestimmen2"], _, _)], _, ptp))
198 = Step.specify_do_next ptp;