1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu Jun 05 15:49:44 2014 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Thu Jun 05 16:41:42 2014 +0200
1.3 @@ -70,31 +70,6 @@
1.4 (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
1.5 make_fun_explicit: "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
1.6
1.7 -ML {*
1.8 -val thy = @{theory};
1.9 -
1.10 -(** theory elements for transfer into html **)
1.11 -store_thes
1.12 - [make_thy @{theory}
1.13 - ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.14 - make_isa @{theory} ("IsacKnowledge", "Theorems")
1.15 - ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.16 - make_thm thy "IsacKnowledge" ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})
1.17 - ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.18 - make_thm thy "IsacKnowledge" ("Moment_Neigung", prop_of @{thm Moment_Neigung})
1.19 - ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.20 - make_thm thy "IsacKnowledge" ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})
1.21 - ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.22 - make_thm thy "IsacKnowledge" ("Neigung_Moment", prop_of @{thm Neigung_Moment})
1.23 - ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.24 - make_thm thy "IsacKnowledge" ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})
1.25 - ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.26 - make_thm thy "IsacKnowledge" ("Querkraft_Moment", prop_of @{thm Querkraft_Moment})
1.27 - ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.28 - make_thm thy "IsacKnowledge" ("make_fun_explicit", prop_of @{thm make_fun_explicit})
1.29 - ["Walther Neuper 2005 supported by a grant from NMI Austria"]
1.30 - ]
1.31 -*}
1.32 setup {*
1.33 KEStore_Elems.add_thes
1.34 [make_thy @{theory}
1.35 @@ -119,14 +94,14 @@
1.36
1.37 (** problems **)
1.38 setup {* KEStore_Elems.add_pbts
1.39 - [(prep_pbt thy "pbl_bieg" [] e_pblID
1.40 + [(prep_pbt @{theory} "pbl_bieg" [] e_pblID
1.41 (["Biegelinien"],
1.42 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
1.43 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.44 ("#Find" ,["Biegelinie b_b"]),
1.45 ("#Relate",["Randbedingungen r_b"])],
1.46 append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),
1.47 - (prep_pbt thy "pbl_bieg_mom" [] e_pblID
1.48 + (prep_pbt @{theory} "pbl_bieg_mom" [] e_pblID
1.49 (["MomentBestimmte","Biegelinien"],
1.50 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
1.51 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.52 @@ -134,26 +109,26 @@
1.53 ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
1.54 ],
1.55 append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
1.56 - (prep_pbt thy "pbl_bieg_momg" [] e_pblID
1.57 + (prep_pbt @{theory} "pbl_bieg_momg" [] e_pblID
1.58 (["MomentGegebene","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
1.59 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])),
1.60 - (prep_pbt thy "pbl_bieg_einf" [] e_pblID
1.61 + (prep_pbt @{theory} "pbl_bieg_einf" [] e_pblID
1.62 (["einfache","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
1.63 [["IntegrierenUndKonstanteBestimmen","4x4System"]])),
1.64 - (prep_pbt thy "pbl_bieg_momquer" [] e_pblID
1.65 + (prep_pbt @{theory} "pbl_bieg_momquer" [] e_pblID
1.66 (["QuerkraftUndMomentBestimmte","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
1.67 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])),
1.68 - (prep_pbt thy "pbl_bieg_vonq" [] e_pblID
1.69 + (prep_pbt @{theory} "pbl_bieg_vonq" [] e_pblID
1.70 (["vonBelastungZu","Biegelinien"],
1.71 [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
1.72 ("#Find" ,["Funktionen funs'''"])],
1.73 append_rls "e_rls" e_rls [], NONE, [["Biegelinien","ausBelastung"]])),
1.74 - (prep_pbt thy "pbl_bieg_randbed" [] e_pblID
1.75 + (prep_pbt @{theory} "pbl_bieg_randbed" [] e_pblID
1.76 (["setzeRandbedingungen","Biegelinien"],
1.77 [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
1.78 ("#Find" ,["Gleichungen equs'''"])],
1.79 append_rls "e_rls" e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),
1.80 - (prep_pbt thy "pbl_equ_fromfun" [] e_pblID
1.81 + (prep_pbt @{theory} "pbl_equ_fromfun" [] e_pblID
1.82 (["makeFunctionTo","equation"],
1.83 [("#Given" ,["functionEq fu_n","substitution su_b"]),
1.84 ("#Find" ,["equality equ'''"])],
1.85 @@ -210,7 +185,7 @@
1.86 *}
1.87
1.88 setup {* KEStore_Elems.add_mets
1.89 - [prep_met thy "met_biege" [] e_metID
1.90 + [prep_met @{theory} "met_biege" [] e_metID
1.91 (["IntegrierenUndKonstanteBestimmen"],
1.92 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
1.93 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.94 @@ -286,7 +261,7 @@
1.95 " B__B = ((Substitute c_1_2) @@ " ^
1.96 " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
1.97 " in B__B)"),
1.98 - prep_met thy "met_biege_2" [] e_metID
1.99 + prep_met @{theory} "met_biege_2" [] e_metID
1.100 (["IntegrierenUndKonstanteBestimmen2"],
1.101 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
1.102 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.103 @@ -323,27 +298,27 @@
1.104 " B_B = ((Substitute con_s) @@ " ^
1.105 " (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
1.106 " in B_B)"),
1.107 - prep_met thy "met_biege_intconst_2" [] e_metID
1.108 + prep_met @{theory} "met_biege_intconst_2" [] e_metID
1.109 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
1.110 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
1.111 errpats = [], nrls = e_rls},
1.112 "empty_script"),
1.113 - prep_met thy "met_biege_intconst_4" [] e_metID
1.114 + prep_met @{theory} "met_biege_intconst_4" [] e_metID
1.115 (["IntegrierenUndKonstanteBestimmen","4x4System"], [],
1.116 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
1.117 errpats = [], nrls = e_rls},
1.118 "empty_script"),
1.119 - prep_met thy "met_biege_intconst_1" [] e_metID
1.120 + prep_met @{theory} "met_biege_intconst_1" [] e_metID
1.121 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], [],
1.122 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
1.123 errpats = [], nrls = e_rls},
1.124 "empty_script"),
1.125 - prep_met thy "met_biege2" [] e_metID
1.126 + prep_met @{theory} "met_biege2" [] e_metID
1.127 (["Biegelinien"], [],
1.128 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
1.129 errpats = [], nrls = e_rls},
1.130 "empty_script"),
1.131 - prep_met thy "met_biege_ausbelast" [] e_metID
1.132 + prep_met @{theory} "met_biege_ausbelast" [] e_metID
1.133 (["Biegelinien", "ausBelastung"],
1.134 [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
1.135 ("#Find" ,["Funktionen fun_s"])],
1.136 @@ -380,7 +355,7 @@
1.137 " [diff,integration,named]) " ^
1.138 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
1.139 " in [Q__Q, M__M, N__N, B__B])"),
1.140 - prep_met thy "met_biege_setzrand" [] e_metID
1.141 + prep_met @{theory} "met_biege_setzrand" [] e_metID
1.142 (["Biegelinien", "setzeRandbedingungenEin"],
1.143 [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
1.144 ("#Find" , ["Gleichungen equs'''"])],
1.145 @@ -439,7 +414,7 @@
1.146 " [Equation,fromFunction]) " ^
1.147 " [BOOL (hd f_s), BOOL b_4]) " ^
1.148 " in [e_1,e_2,e_3,e_4])"*)),
1.149 - prep_met thy "met_equ_fromfun" [] e_metID
1.150 + prep_met @{theory} "met_equ_fromfun" [] e_metID
1.151 (["Equation","fromFunction"],
1.152 [("#Given" ,["functionEq fu_n","substitution su_b"]),
1.153 ("#Find" ,["equality equ'''"])],