1 (* Title: Knowledge/biegelinie-3.sml
2 Author: Walther Neuper 050826
3 (c) due to copyright terms
5 "-----------------------------------------------------------------";
6 "table of contents -----------------------------------------------";
7 "-----------------------------------------------------------------";
8 "----------- auto method [Biegelinien,setzeRandbedingungenEin]--------------------------------";
9 "----------- me method [Biegelinien,setzeRandbedingungenEin]----------------------------------";
10 "---------------------------------------------------------------------------------------------";
11 "---------------------------------------------------------------------------------------------";
12 "---------------------------------------------------------------------------------------------";
15 "----------- auto method [Biegelinien,setzeRandbedingungenEin]--------------------------------";
16 "----------- auto method [Biegelinien,setzeRandbedingungenEin]--------------------------------";
17 "----------- auto method [Biegelinien,setzeRandbedingungenEin]--------------------------------";
18 val fmz = ["Funktionen [Q x = c + - 1 * q_0 * x," ^
19 "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2," ^
20 "y' x = c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)," ^
21 "y x = c_4 + c_3 * x + 1 / (- 1 * EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]",
22 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
24 val (dI',pI',mI') = ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"],
25 ["Biegelinien", "setzeRandbedingungenEin"]);
28 CalcTree [(fmz, (dI',pI',mI'))];
31 autoCalculate 1 CompleteCalc;
33 val ((pt, p),_) = get_calc 1;
34 if p = ([], Res) andalso (get_obj g_res pt (fst p) |> UnparseC.term) =
35 "[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
36 (*"[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 * EI + - 24 * L * c_3 * EI + 12 * L \<up> 2 * c_2 +\n 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n (- 24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
37 ^^^ BEFORE fun calcul IS EVALUATEDO BY Simplifier.rewrite *)
38 then () else error "auto method [Biegelinien,setzeRandbedingungenEin] changed";
41 "----------- me method [Biegelinien,setzeRandbedingungenEin]----------------------------------";
42 "----------- me method [Biegelinien,setzeRandbedingungenEin]----------------------------------";
43 "----------- me method [Biegelinien,setzeRandbedingungenEin]----------------------------------";
44 val fmz = ["Funktionen [Q x = c + - 1 * q_0 * x," ^
45 "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2," ^
46 "y' x = c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)," ^
47 "y x = c_4 + c_3 * x + 1 / (- 1 * EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]",
48 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
50 val (dI',pI',mI') = ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"],
51 ["Biegelinien", "setzeRandbedingungenEin"]);
52 val p = e_pos'; val c = [];
53 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
54 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
56 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
57 val (p,_,f,nxt,_,pt) = me nxt p c pt;
59 "--- before 1.subpbl [Equation, fromFunction]";
60 val (p,_,f,nxt,_,pt) = me nxt p c pt;
61 case nxt of Apply_Method ["Biegelinien", "setzeRandbedingungenEin"] => ()
62 | _ => error "biegelinie.sml: met setzeRandbed*Ein aa";
63 "----- Randbedingung y 0 = 0 in SUBpbl with met [Equation, fromFunction]";
64 val (p,_,f,nxt,_,pt) = me nxt p c pt;
65 if (#1 o (get_obj g_fmz pt)) (fst p) =
66 ["functionEq\n (y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *" ^
67 "\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4))",
68 "substitution (y 0 = 0)", "equality equ'''"] then ()
69 else error "biegelinie.sml met setzeRandbed*Ein bb";
70 (writeln o Istate.string_of) (get_istate_LI pt p);
71 "--- after 1.subpbl [Equation, fromFunction]";
73 val (p,_,f,nxt,_,pt) = me nxt p c pt;
74 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
75 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
76 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
77 case nxt of Apply_Method["Equation", "fromFunction"] => ()
78 | _ => error "biegelinie.sml met2 ff";
79 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
80 "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)";
81 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
82 val (p,_,f,nxt,_,pt) = me nxt p c pt;
83 case nxt of Check_Postcond ["makeFunctionTo", "equation"] => ()
84 | _ => error "biegelinie.sml met2 gg";
86 (*========== inhibit exn WN210927 exception size SINCE BEFORE fun calcul WITH Simplifier.rewrite
87 "--- before 2.subpbl [Equation, fromFunction]";
88 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_4 + 0 / (- 1 * EI)" ;
89 case nxt of Subproblem (_, ["makeFunctionTo", "equation"]) => ()
90 | _ => error "biegelinie.sml met2 hh";
91 "--- after 1st arrival at 2.subpbl [Equation, fromFunction]";
93 val (p,_,f,nxt,_,pt) = me nxt p c pt;
94 if (#1 o (get_obj g_fmz pt)) (fst p) =
95 ["functionEq\n (y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4))",
96 "substitution (y L = 0)", "equality equ'''"] then ()
97 else error "biegelinie.sml metsetzeRandbed*Ein bb ";
98 val (p,_,f,nxt,_,pt) = me nxt p c pt;
99 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
100 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
101 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
102 case nxt of Apply_Method["Equation", "fromFunction"] => ()
103 | _ => error "biegelinie.sml met2 ii";
104 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "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)";
105 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "y L =\nc_4 + c_3 * L +\n1 / (- 1 * EI) *\n(c_2 / 2 * L \<up> 2 + c / 6 * L \<up> 3 + - 1 * q_0 / 24 * L \<up> 4)";
106 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 =\nc_4 + c_3 * L +\n1 / (- 1 * EI) *\n(c_2 / 2 * L \<up> 2 + c / 6 * L \<up> 3 + - 1 * q_0 / 24 * L \<up> 4)";
107 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 =\nc_4 + L * c_3 +\n(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI)" ;
108 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 =\nc_4 + L * c_3 +\n(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI)";
109 case nxt of Subproblem ("Biegelinie", ["makeFunctionTo", "equation"]) => ()
110 | _ => error "biegelinie.sml met2 jj";
111 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
112 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
113 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
114 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
115 case nxt of Apply_Method ["Equation", "fromFunction"] => ()
116 | _ => error "biegelinie.sml met2 kk";
118 val (p,_,f,nxt,_,pt) = me nxt p c pt;
119 if f2str f = "0 = - 1 * c_4 / - 1"
120 (*"M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2" BEFORE fun calcul WITH Simplifier.rewrite*)
121 then () else error "Method fromFunction CHANGED 1";
123 val (p,_,f,nxt,_,pt) = me nxt p c pt;
124 val Test_Out.PpcKF (Test_Out.Problem [], {Find = [], Given = [], Relate = [],
125 Where = [], With = []}) = f;
126 ( *========== inhibit exn WN210927 BEFORE fun calcul WITH Simplifier.rewrite ========
127 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
128 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
129 val (p,_,f,nxt,_,pt) = me nxt p c pt;
130 ( *========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some===
132 case nxt of (_, Subproblem (_, ["makeFunctionTo", "equation"])) => ()
133 | _ => error "biegelinie.sml met2 ll";
135 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
136 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
137 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
138 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
139 case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
140 | _ => error "biegelinie.sml met2 mm";
142 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";
143 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b L = c_2 + c * L + - 1 * q_0 / 2 * L \<up> 2";
144 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * L + - 1 * q_0 / 2 * L \<up> 2";
145 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
146 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
147 case nxt of (_, Check_Postcond ["setzeRandbedingungen", "Biegelinien"]) => ()
148 | _ => error "biegelinie.sml met2 nn";
149 val (p,_,f,nxt,_,pt) = me nxt p c pt;
150 if nxt = ("End_Proof'", End_Proof') andalso f2str f =
151 (* "[0 = c_4,\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) / (- 24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]" *)
152 "[0 = c_4,\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 (- 1 * EI * 24),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
153 then () else error "biegelinie.sml met2 oo";
154 ============ inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=*)