1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Sun Mar 25 13:59:57 2018 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Mon Mar 26 07:28:39 2018 +0200
1.3 @@ -100,7 +100,7 @@
1.4 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.5 ("#Find" ,["Biegelinie b_b"]),
1.6 ("#Relate",["Randbedingungen r_b"])],
1.7 - Celem.append_rls "e_rls" Celem.e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),
1.8 + Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),
1.9 (Specify.prep_pbt @{theory} "pbl_bieg_mom" [] Celem.e_pblID
1.10 (["MomentBestimmte","Biegelinien"],
1.11 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
1.12 @@ -108,80 +108,80 @@
1.13 ("#Find" ,["Biegelinie b_b"]),
1.14 ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
1.15 ],
1.16 - Celem.append_rls "e_rls" Celem.e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
1.17 + Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
1.18 (Specify.prep_pbt @{theory} "pbl_bieg_momg" [] Celem.e_pblID
1.19 - (["MomentGegebene","Biegelinien"], [], Celem.append_rls "e_rls" Celem.e_rls [], NONE,
1.20 + (["MomentGegebene","Biegelinien"], [], Rule.append_rls "e_rls" Rule.e_rls [], NONE,
1.21 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])),
1.22 (Specify.prep_pbt @{theory} "pbl_bieg_einf" [] Celem.e_pblID
1.23 - (["einfache","Biegelinien"], [], Celem.append_rls "e_rls" Celem.e_rls [], NONE,
1.24 + (["einfache","Biegelinien"], [], Rule.append_rls "e_rls" Rule.e_rls [], NONE,
1.25 [["IntegrierenUndKonstanteBestimmen","4x4System"]])),
1.26 (Specify.prep_pbt @{theory} "pbl_bieg_momquer" [] Celem.e_pblID
1.27 - (["QuerkraftUndMomentBestimmte","Biegelinien"], [], Celem.append_rls "e_rls" Celem.e_rls [], NONE,
1.28 + (["QuerkraftUndMomentBestimmte","Biegelinien"], [], Rule.append_rls "e_rls" Rule.e_rls [], NONE,
1.29 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])),
1.30 (Specify.prep_pbt @{theory} "pbl_bieg_vonq" [] Celem.e_pblID
1.31 (["vonBelastungZu","Biegelinien"],
1.32 [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
1.33 ("#Find" ,["Funktionen funs'''"])],
1.34 - Celem.append_rls "e_rls" Celem.e_rls [], NONE, [["Biegelinien","ausBelastung"]])),
1.35 + Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["Biegelinien","ausBelastung"]])),
1.36 (Specify.prep_pbt @{theory} "pbl_bieg_randbed" [] Celem.e_pblID
1.37 (["setzeRandbedingungen","Biegelinien"],
1.38 [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
1.39 ("#Find" ,["Gleichungen equs'''"])],
1.40 - Celem.append_rls "e_rls" Celem.e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),
1.41 + Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),
1.42 (Specify.prep_pbt @{theory} "pbl_equ_fromfun" [] Celem.e_pblID
1.43 (["makeFunctionTo","equation"],
1.44 [("#Given" ,["functionEq fu_n","substitution su_b"]),
1.45 ("#Find" ,["equality equ'''"])],
1.46 - Celem.append_rls "e_rls" Celem.e_rls [], NONE, [["Equation","fromFunction"]]))] *}
1.47 + Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["Equation","fromFunction"]]))] *}
1.48 ML {*
1.49 (** methods **)
1.50
1.51 -val srls = Celem.Rls {id="srls_IntegrierenUnd..",
1.52 +val srls = Rule.Rls {id="srls_IntegrierenUnd..",
1.53 preconds = [],
1.54 rew_ord = ("termlessI",termlessI),
1.55 - erls = Celem.append_rls "erls_in_srls_IntegrierenUnd.." Celem.e_rls
1.56 + erls = Rule.append_rls "erls_in_srls_IntegrierenUnd.." Rule.e_rls
1.57 [(*for asm in NTH_CONS ...*)
1.58 - Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.59 + Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.60 (*2nd NTH_CONS pushes n+-1 into asms*)
1.61 - Celem.Calc("Groups.plus_class.plus", eval_binop "#add_")
1.62 + Rule.Calc("Groups.plus_class.plus", eval_binop "#add_")
1.63 ],
1.64 - srls = Celem.Erls, calc = [], errpatts = [],
1.65 - rules = [Celem.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.66 - Celem.Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.67 - Celem.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.68 - Celem.Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.69 - Celem.Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.70 - Celem.Calc("Atools.argument'_in",
1.71 + srls = Rule.Erls, calc = [], errpatts = [],
1.72 + rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.73 + Rule.Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.74 + Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.75 + Rule.Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.76 + Rule.Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.77 + Rule.Calc("Atools.argument'_in",
1.78 eval_argument_in "Atools.argument'_in")
1.79 ],
1.80 - scr = Celem.EmptyScr};
1.81 + scr = Rule.EmptyScr};
1.82
1.83 val srls2 =
1.84 - Celem.Rls {id="srls_IntegrierenUnd..",
1.85 + Rule.Rls {id="srls_IntegrierenUnd..",
1.86 preconds = [],
1.87 rew_ord = ("termlessI",termlessI),
1.88 - erls = Celem.append_rls "erls_in_srls_IntegrierenUnd.." Celem.e_rls
1.89 + erls = Rule.append_rls "erls_in_srls_IntegrierenUnd.." Rule.e_rls
1.90 [(*for asm in NTH_CONS ...*)
1.91 - Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.92 + Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.93 (*2nd NTH_CONS pushes n+-1 into asms*)
1.94 - Celem.Calc("Groups.plus_class.plus", eval_binop "#add_")
1.95 + Rule.Calc("Groups.plus_class.plus", eval_binop "#add_")
1.96 ],
1.97 - srls = Celem.Erls, calc = [], errpatts = [],
1.98 - rules = [Celem.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.99 - Celem.Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.100 - Celem.Thm ("NTH_NIL", TermC.num_str @{thm NTH_NIL}),
1.101 - Celem.Calc("Tools.lhs", eval_lhs "eval_lhs_"),
1.102 - Celem.Calc("Atools.filter'_sameFunId",
1.103 + srls = Rule.Erls, calc = [], errpatts = [],
1.104 + rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.105 + Rule.Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.106 + Rule.Thm ("NTH_NIL", TermC.num_str @{thm NTH_NIL}),
1.107 + Rule.Calc("Tools.lhs", eval_lhs "eval_lhs_"),
1.108 + Rule.Calc("Atools.filter'_sameFunId",
1.109 eval_filter_sameFunId "Atools.filter'_sameFunId"),
1.110 (*WN070514 just for smltest/../biegelinie.sml ...*)
1.111 - Celem.Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),
1.112 - Celem.Thm ("filter_Cons", TermC.num_str @{thm filter_Cons}),
1.113 - Celem.Thm ("filter_Nil", TermC.num_str @{thm filter_Nil}),
1.114 - Celem.Thm ("if_True", TermC.num_str @{thm if_True}),
1.115 - Celem.Thm ("if_False", TermC.num_str @{thm if_False}),
1.116 - Celem.Thm ("hd_thm", TermC.num_str @{thm hd_thm})
1.117 + Rule.Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),
1.118 + Rule.Thm ("filter_Cons", TermC.num_str @{thm filter_Cons}),
1.119 + Rule.Thm ("filter_Nil", TermC.num_str @{thm filter_Nil}),
1.120 + Rule.Thm ("if_True", TermC.num_str @{thm if_True}),
1.121 + Rule.Thm ("if_False", TermC.num_str @{thm if_False}),
1.122 + Rule.Thm ("hd_thm", TermC.num_str @{thm hd_thm})
1.123 ],
1.124 - scr = Celem.EmptyScr};
1.125 + scr = Rule.EmptyScr};
1.126 *}
1.127
1.128 setup {* KEStore_Elems.add_mets
1.129 @@ -192,11 +192,11 @@
1.130 ("#Find" ,["Biegelinie b_b"]),
1.131 ("#Relate",["RandbedingungenBiegung r_b", "RandbedingungenMoment r_m"])],
1.132 {rew_ord'="tless_true",
1.133 - rls' = Celem.append_rls "erls_IntegrierenUndK.." Celem.e_rls
1.134 - [Celem.Calc ("Atools.ident",eval_ident "#ident_"),
1.135 - Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
1.136 - Celem.Thm ("not_false",TermC.num_str @{thm not_false})],
1.137 - calc = [], srls = srls, prls = Celem.Erls, crls = Atools_erls, errpats = [], nrls = Celem.Erls},
1.138 + rls' = Rule.append_rls "erls_IntegrierenUndK.." Rule.e_rls
1.139 + [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
1.140 + Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
1.141 + Rule.Thm ("not_false",TermC.num_str @{thm not_false})],
1.142 + calc = [], srls = srls, prls = Rule.Erls, crls = Atools_erls, errpats = [], nrls = Rule.Erls},
1.143 "Script BiegelinieScript " ^
1.144 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
1.145 "(r_b::bool list) (r_m::bool list) = " ^
1.146 @@ -268,18 +268,18 @@
1.147 ("#Find" ,["Biegelinie b_b"]),
1.148 ("#Relate",["Randbedingungen r_b"])],
1.149 {rew_ord'="tless_true",
1.150 - rls' = Celem.append_rls "erls_IntegrierenUndK.." Celem.e_rls
1.151 - [Celem.Calc ("Atools.ident",eval_ident "#ident_"),
1.152 - Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
1.153 - Celem.Thm ("not_false",TermC.num_str @{thm not_false})],
1.154 + rls' = Rule.append_rls "erls_IntegrierenUndK.." Rule.e_rls
1.155 + [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
1.156 + Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
1.157 + Rule.Thm ("not_false",TermC.num_str @{thm not_false})],
1.158 calc = [],
1.159 - srls = Celem.append_rls "erls_IntegrierenUndK.." Celem.e_rls
1.160 - [Celem.Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.161 - Celem.Calc ("Atools.ident",eval_ident "#ident_"),
1.162 - Celem.Thm ("last_thmI",TermC.num_str @{thm last_thmI}),
1.163 - Celem.Thm ("if_True",TermC.num_str @{thm if_True}),
1.164 - Celem.Thm ("if_False",TermC.num_str @{thm if_False})],
1.165 - prls = Celem.Erls, crls = Atools_erls, errpats = [], nrls = Celem.Erls},
1.166 + srls = Rule.append_rls "erls_IntegrierenUndK.." Rule.e_rls
1.167 + [Rule.Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.168 + Rule.Calc ("Atools.ident",eval_ident "#ident_"),
1.169 + Rule.Thm ("last_thmI",TermC.num_str @{thm last_thmI}),
1.170 + Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
1.171 + Rule.Thm ("if_False",TermC.num_str @{thm if_False})],
1.172 + prls = Rule.Erls, crls = Atools_erls, errpats = [], nrls = Rule.Erls},
1.173 "Script Biegelinie2Script " ^
1.174 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
1.175 " (let " ^
1.176 @@ -300,37 +300,37 @@
1.177 " in B_B)"),
1.178 Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID
1.179 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
1.180 - {rew_ord'="tless_true", rls'=Celem.Erls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls, crls = Atools_erls,
1.181 - errpats = [], nrls = Celem.e_rls},
1.182 + {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
1.183 + errpats = [], nrls = Rule.e_rls},
1.184 "empty_script"),
1.185 Specify.prep_met @{theory} "met_biege_intconst_4" [] Celem.e_metID
1.186 (["IntegrierenUndKonstanteBestimmen","4x4System"], [],
1.187 - {rew_ord'="tless_true", rls'=Celem.Erls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls, crls = Atools_erls,
1.188 - errpats = [], nrls = Celem.e_rls},
1.189 + {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
1.190 + errpats = [], nrls = Rule.e_rls},
1.191 "empty_script"),
1.192 Specify.prep_met @{theory} "met_biege_intconst_1" [] Celem.e_metID
1.193 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], [],
1.194 - {rew_ord'="tless_true", rls'=Celem.Erls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls, crls = Atools_erls,
1.195 - errpats = [], nrls = Celem.e_rls},
1.196 + {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
1.197 + errpats = [], nrls = Rule.e_rls},
1.198 "empty_script"),
1.199 Specify.prep_met @{theory} "met_biege2" [] Celem.e_metID
1.200 (["Biegelinien"], [],
1.201 - {rew_ord'="tless_true", rls'=Celem.Erls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls, crls = Atools_erls,
1.202 - errpats = [], nrls = Celem.e_rls},
1.203 + {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
1.204 + errpats = [], nrls = Rule.e_rls},
1.205 "empty_script"),
1.206 Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
1.207 (["Biegelinien", "ausBelastung"],
1.208 [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
1.209 ("#Find" ,["Funktionen fun_s"])],
1.210 {rew_ord'="tless_true",
1.211 - rls' = Celem.append_rls "erls_ausBelastung" Celem.e_rls
1.212 - [Celem.Calc ("Atools.ident", eval_ident "#ident_"),
1.213 - Celem.Thm ("not_true", TermC.num_str @{thm not_true}),
1.214 - Celem.Thm ("not_false", TermC.num_str @{thm not_false})],
1.215 + rls' = Rule.append_rls "erls_ausBelastung" Rule.e_rls
1.216 + [Rule.Calc ("Atools.ident", eval_ident "#ident_"),
1.217 + Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.218 + Rule.Thm ("not_false", TermC.num_str @{thm not_false})],
1.219 calc = [],
1.220 - srls = Celem.append_rls "srls_ausBelastung" Celem.e_rls
1.221 - [Celem.Calc ("Tools.rhs", eval_rhs "eval_rhs_")],
1.222 - prls = Celem.e_rls, crls = Atools_erls, errpats = [], nrls = Celem.e_rls},
1.223 + srls = Rule.append_rls "srls_ausBelastung" Rule.e_rls
1.224 + [Rule.Calc ("Tools.rhs", eval_rhs "eval_rhs_")],
1.225 + prls = Rule.e_rls, crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
1.226 "Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
1.227 " (let q___q = Take (qq v_v = q__q); " ^
1.228 " q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
1.229 @@ -359,8 +359,8 @@
1.230 (["Biegelinien", "setzeRandbedingungenEin"],
1.231 [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
1.232 ("#Find" , ["Gleichungen equs'''"])],
1.233 - {rew_ord'="tless_true", rls'=Celem.Erls, calc = [], srls = srls2, prls=Celem.e_rls, crls = Atools_erls,
1.234 - errpats = [], nrls = Celem.e_rls},
1.235 + {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = srls2, prls=Rule.e_rls, crls = Atools_erls,
1.236 + errpats = [], nrls = Rule.e_rls},
1.237 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
1.238 " (let b_1 = NTH 1 r_b; " ^
1.239 " f_s = filter_sameFunId (lhs b_1) fun_s; " ^
1.240 @@ -418,11 +418,11 @@
1.241 (["Equation","fromFunction"],
1.242 [("#Given" ,["functionEq fu_n","substitution su_b"]),
1.243 ("#Find" ,["equality equ'''"])],
1.244 - {rew_ord'="tless_true", rls'=Celem.Erls, calc = [],
1.245 - srls = Celem.append_rls "srls_in_EquationfromFunc" Celem.e_rls
1.246 - [Celem.Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.247 - Celem.Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
1.248 - prls=Celem.e_rls, crls = Atools_erls, errpats = [], nrls = Celem.e_rls},
1.249 + {rew_ord'="tless_true", rls'=Rule.Erls, calc = [],
1.250 + srls = Rule.append_rls "srls_in_EquationfromFunc" Rule.e_rls
1.251 + [Rule.Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.252 + Rule.Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
1.253 + prls=Rule.e_rls, crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
1.254 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
1.255 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
1.256 "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^