122 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
122 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
123 (*2nd NTH_CONS pushes n+-1 into asms*) |
123 (*2nd NTH_CONS pushes n+-1 into asms*) |
124 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_") |
124 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_") |
125 ], |
125 ], |
126 srls = Rule_Set.Empty, calc = [], errpatts = [], |
126 srls = Rule_Set.Empty, calc = [], errpatts = [], |
127 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), |
127 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}), |
128 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"), |
128 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"), |
129 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}), |
129 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}), |
130 Rule.Num_Calc("Prog_Expr.lhs", Prog_Expr.eval_lhs"eval_lhs_"), |
130 Rule.Num_Calc("Prog_Expr.lhs", Prog_Expr.eval_lhs"eval_lhs_"), |
131 Rule.Num_Calc("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"), |
131 Rule.Num_Calc("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"), |
132 Rule.Num_Calc("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in") |
132 Rule.Num_Calc("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in") |
133 ], |
133 ], |
134 scr = Rule.EmptyScr}; |
134 scr = Rule.EmptyScr}; |
142 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
142 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
143 (*2nd NTH_CONS pushes n+-1 into asms*) |
143 (*2nd NTH_CONS pushes n+-1 into asms*) |
144 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_") |
144 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_") |
145 ], |
145 ], |
146 srls = Rule_Set.Empty, calc = [], errpatts = [], |
146 srls = Rule_Set.Empty, calc = [], errpatts = [], |
147 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), |
147 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}), |
148 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"), |
148 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"), |
149 Rule.Thm ("NTH_NIL", TermC.num_str @{thm NTH_NIL}), |
149 Rule.Thm ("NTH_NIL", ThmC.numerals_to_Free @{thm NTH_NIL}), |
150 Rule.Num_Calc("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"), |
150 Rule.Num_Calc("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"), |
151 Rule.Num_Calc("Prog_Expr.filter'_sameFunId", Prog_Expr.eval_filter_sameFunId "Prog_Expr.filter'_sameFunId"), |
151 Rule.Num_Calc("Prog_Expr.filter'_sameFunId", Prog_Expr.eval_filter_sameFunId "Prog_Expr.filter'_sameFunId"), |
152 (*WN070514 just for smltest/../biegelinie.sml ...*) |
152 (*WN070514 just for smltest/../biegelinie.sml ...*) |
153 Rule.Num_Calc("Prog_Expr.sameFunId", Prog_Expr.eval_sameFunId "Prog_Expr.sameFunId"), |
153 Rule.Num_Calc("Prog_Expr.sameFunId", Prog_Expr.eval_sameFunId "Prog_Expr.sameFunId"), |
154 Rule.Thm ("filter_Cons", TermC.num_str @{thm filter_Cons}), |
154 Rule.Thm ("filter_Cons", ThmC.numerals_to_Free @{thm filter_Cons}), |
155 Rule.Thm ("filter_Nil", TermC.num_str @{thm filter_Nil}), |
155 Rule.Thm ("filter_Nil", ThmC.numerals_to_Free @{thm filter_Nil}), |
156 Rule.Thm ("if_True", TermC.num_str @{thm if_True}), |
156 Rule.Thm ("if_True", ThmC.numerals_to_Free @{thm if_True}), |
157 Rule.Thm ("if_False", TermC.num_str @{thm if_False}), |
157 Rule.Thm ("if_False", ThmC.numerals_to_Free @{thm if_False}), |
158 Rule.Thm ("hd_thm", TermC.num_str @{thm hd_thm}) |
158 Rule.Thm ("hd_thm", ThmC.numerals_to_Free @{thm hd_thm}) |
159 ], |
159 ], |
160 scr = Rule.EmptyScr}; |
160 scr = Rule.EmptyScr}; |
161 \<close> |
161 \<close> |
162 |
162 |
163 section \<open>Methods\<close> |
163 section \<open>Methods\<close> |
194 ("#Find" ,["Biegelinie b"]), |
194 ("#Find" ,["Biegelinie b"]), |
195 ("#Relate",["Randbedingungen s"])], |
195 ("#Relate",["Randbedingungen s"])], |
196 {rew_ord'="tless_true", |
196 {rew_ord'="tless_true", |
197 rls' = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty |
197 rls' = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty |
198 [Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"), |
198 [Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"), |
199 Rule.Thm ("not_true",TermC.num_str @{thm not_true}), |
199 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}), |
200 Rule.Thm ("not_false",TermC.num_str @{thm not_false})], |
200 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})], |
201 calc = [], |
201 calc = [], |
202 srls = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty |
202 srls = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty |
203 [Rule.Num_Calc("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"), |
203 [Rule.Num_Calc("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"), |
204 Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"), |
204 Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"), |
205 Rule.Thm ("last_thmI",TermC.num_str @{thm last_thmI}), |
205 Rule.Thm ("last_thmI",ThmC.numerals_to_Free @{thm last_thmI}), |
206 Rule.Thm ("if_True",TermC.num_str @{thm if_True}), |
206 Rule.Thm ("if_True",ThmC.numerals_to_Free @{thm if_True}), |
207 Rule.Thm ("if_False",TermC.num_str @{thm if_False})], |
207 Rule.Thm ("if_False",ThmC.numerals_to_Free @{thm if_False})], |
208 prls = Rule_Set.Empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.Empty}, |
208 prls = Rule_Set.Empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.Empty}, |
209 @{thm biegelinie.simps})] |
209 @{thm biegelinie.simps})] |
210 \<close> |
210 \<close> |
211 setup \<open>KEStore_Elems.add_mets |
211 setup \<open>KEStore_Elems.add_mets |
212 [Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID |
212 [Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID |
260 "Biegelinie id_fun", "AbleitungBiegelinie id_abl"]), |
260 "Biegelinie id_fun", "AbleitungBiegelinie id_abl"]), |
261 ("#Find" ,["Funktionen fun_s"])], |
261 ("#Find" ,["Funktionen fun_s"])], |
262 {rew_ord'="tless_true", |
262 {rew_ord'="tless_true", |
263 rls' = Rule_Set.append_rules "erls_ausBelastung" Rule_Set.empty |
263 rls' = Rule_Set.append_rules "erls_ausBelastung" Rule_Set.empty |
264 [Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"), |
264 [Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"), |
265 Rule.Thm ("not_true", TermC.num_str @{thm not_true}), |
265 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}), |
266 Rule.Thm ("not_false", TermC.num_str @{thm not_false})], |
266 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})], |
267 calc = [], |
267 calc = [], |
268 srls = Rule_Set.append_rules "srls_ausBelastung" Rule_Set.empty |
268 srls = Rule_Set.append_rules "srls_ausBelastung" Rule_Set.empty |
269 [Rule.Num_Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "eval_rhs_")], |
269 [Rule.Num_Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "eval_rhs_")], |
270 prls = Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}, |
270 prls = Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}, |
271 @{thm belastung_zu_biegelinie.simps})] |
271 @{thm belastung_zu_biegelinie.simps})] |