27 "-----------------------------------------------------------------"; |
27 "-----------------------------------------------------------------"; |
28 "-----------------------------------------------------------------"; |
28 "-----------------------------------------------------------------"; |
29 |
29 |
30 val thy = @{theory "Biegelinie"}; |
30 val thy = @{theory "Biegelinie"}; |
31 val ctxt = ThyC.id_to_ctxt "Biegelinie"; |
31 val ctxt = ThyC.id_to_ctxt "Biegelinie"; |
32 fun str2term str = TermC.parseNEW' ctxt str; |
|
33 fun term2s t = UnparseC.term_by_thyID "Biegelinie" t; |
32 fun term2s t = UnparseC.term_by_thyID "Biegelinie" t; |
34 fun rewrit thm str = fst (the (rewrite_ ctxt tless_true Rule_Set.empty true thm str)); |
33 fun rewrit thm str = fst (the (rewrite_ ctxt tless_true Rule_Set.empty true thm str)); |
35 |
34 |
36 "----------- the rules -------------------------------------------"; |
35 "----------- the rules -------------------------------------------"; |
37 "----------- the rules -------------------------------------------"; |
36 "----------- the rules -------------------------------------------"; |
38 "----------- the rules -------------------------------------------"; |
37 "----------- the rules -------------------------------------------"; |
39 val t = rewrit @{thm Belastung_Querkraft} (TermC.str2term "- qq x = - q_0"); term2s t; |
38 val t = rewrit @{thm Belastung_Querkraft} (TermC.parse_test @{context} "- qq x = - q_0"); term2s t; |
40 if term2s t = "Q' x = - q_0" then () |
39 if term2s t = "Q' x = - q_0" then () |
41 else error "/biegelinie.sml: Belastung_Querkraft"; |
40 else error "/biegelinie.sml: Belastung_Querkraft"; |
42 |
41 |
43 val t = rewrit @{thm Querkraft_Moment} (TermC.str2term "Q x = - q_0 * x + c"); term2s t; |
42 val t = rewrit @{thm Querkraft_Moment} (TermC.parse_test @{context} "Q x = - q_0 * x + c"); term2s t; |
44 if term2s t = "?M_b' x = - q_0 * x + c" then () |
43 if term2s t = "?M_b' x = - q_0 * x + c" then () |
45 (*if term2s t = "M_b' x = - q_0 * x + c" then () cf.fbe1652b0df8 new handling of quotes in mixfix*) |
44 (*if term2s t = "M_b' x = - q_0 * x + c" then () cf.fbe1652b0df8 new handling of quotes in mixfix*) |
46 else error "/biegelinie.sml: Querkraft_Moment"; |
45 else error "/biegelinie.sml: Querkraft_Moment"; |
47 |
46 |
48 val t = rewrit @{thm Moment_Neigung} (TermC.str2term "M_b x = -q_0 * x \<up> 2/2 + q_0/2 *L*x"); |
47 val t = rewrit @{thm Moment_Neigung} (TermC.parse_test @{context} "M_b x = -q_0 * x \<up> 2/2 + q_0/2 *L*x"); |
49 term2s t; |
48 term2s t; |
50 if term2s t = "- EI * y'' x = - q_0 * x \<up> 2 / 2 + q_0 / 2 * L * x" then () |
49 if term2s t = "- EI * y'' x = - q_0 * x \<up> 2 / 2 + q_0 / 2 * L * x" then () |
51 else error "biegelinie.sml: Moment_Neigung"; |
50 else error "biegelinie.sml: Moment_Neigung"; |
52 |
51 |
53 "----------- simplify_leaf for this script -----------------------"; |
52 "----------- simplify_leaf for this script -----------------------"; |
69 Eval("Prog_Expr.lhs", eval_lhs "eval_lhs_"), |
68 Eval("Prog_Expr.lhs", eval_lhs "eval_lhs_"), |
70 Eval("Prog_Expr.rhs", eval_rhs "eval_rhs_"), |
69 Eval("Prog_Expr.rhs", eval_rhs "eval_rhs_"), |
71 Eval("Prog_Expr.argument_in", eval_argument_in "Prog_Expr.argument_in") |
70 Eval("Prog_Expr.argument_in", eval_argument_in "Prog_Expr.argument_in") |
72 ], |
71 ], |
73 scr = Empty_Prog}; |
72 scr = Empty_Prog}; |
74 val rm_ = TermC.str2term"[M_b 0 = 0, M_b L = 0]"; |
73 val rm_ = TermC.parse_test @{context}"[M_b 0 = 0, M_b L = 0]"; |
75 val M__ = TermC.str2term"M_b x = - 1 * x \<up> 2 / 2 + x * c + c_2"; |
74 val M__ = TermC.parse_test @{context}"M_b x = - 1 * x \<up> 2 / 2 + x * c + c_2"; |
76 val SOME (e1__,_) = rewrite_set_ ctxt false srls |
75 val SOME (e1__,_) = rewrite_set_ ctxt false srls |
77 (TermC.str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_); |
76 (TermC.parse_test @{context} "(NTH::[real,bool list]=>bool) 1 " $ rm_); |
78 if UnparseC.term e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_"; |
77 if UnparseC.term e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_"; |
79 |
78 |
80 val SOME (x1__,_) = rewrite_set_ ctxt false srls (TermC.str2term "argument_in (lhs (M_b 0 = 0))"); |
79 val SOME (x1__,_) = rewrite_set_ ctxt false srls (TermC.parse_test @{context} "argument_in (lhs (M_b 0 = 0))"); |
81 if UnparseC.term x1__ = "0" then () |
80 if UnparseC.term x1__ = "0" then () |
82 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)"; |
81 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)"; |
83 |
82 |
84 |
83 |
85 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----"; |
84 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----"; |
113 |
112 |
114 "----------- investigate normalforms in biegelinien --------------"; |
113 "----------- investigate normalforms in biegelinien --------------"; |
115 "----------- investigate normalforms in biegelinien --------------"; |
114 "----------- investigate normalforms in biegelinien --------------"; |
116 "----------- investigate normalforms in biegelinien --------------"; |
115 "----------- investigate normalforms in biegelinien --------------"; |
117 "----- coming from integration, kept for later improvements:"; |
116 "----- coming from integration, kept for later improvements:"; |
118 val Q = TermC.str2term "Q x = c + - 1 * q_0 * x"; |
117 val Q = TermC.parse_test @{context} "Q x = c + - 1 * q_0 * x"; |
119 val M_b = TermC.str2term "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2"; |
118 val M_b = TermC.parse_test @{context} "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2"; |
120 val y' = TermC.str2term "y' x = c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"; |
119 val y' = TermC.parse_test @{context} "y' x = c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"; |
121 val y = TermC.str2term "y x = c_4 + c_3 * x +\n1 / (- 1 * EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)"; |
120 val y = TermC.parse_test @{context} "y x = c_4 + c_3 * x +\n1 / (- 1 * EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)"; |
122 (* \<up> 1 / (- 1 * EI) NOT distributed - ok! \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^^*) |
121 (* \<up> 1 / (- 1 * EI) NOT distributed - ok! \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^^*) |