1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed Apr 04 12:41:03 2018 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed Apr 11 14:44:46 2018 +0200
1.3 @@ -184,6 +184,10 @@
1.4 scr = Rule.EmptyScr};
1.5 *}
1.6
1.7 +section \<open>Methods\<close>
1.8 +
1.9 +subsection \<open>Sub-problem "integrate and determine constants", little modularisation\<close>
1.10 +
1.11 setup {* KEStore_Elems.add_mets
1.12 [Specify.prep_met @{theory} "met_biege" [] Celem.e_metID
1.13 (["IntegrierenUndKonstanteBestimmen"],
1.14 @@ -260,13 +264,43 @@
1.15 " B__B = Take B__B; " ^
1.16 " B__B = ((Substitute c_1_2) @@ " ^
1.17 " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
1.18 - " in B__B)"),
1.19 - Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
1.20 + " in B__B)")]
1.21 +*}
1.22 +subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
1.23 +(*------------------------------------------------------------------------------------\\\
1.24 +consts
1.25 + Biegelinie' :: ID vonBelastungZu :: ID Biegelinien :: ID ausBelastung :: ID
1.26 + setzeRandbedingungen :: ID setzeRandbedingungenEin :: ID LINEAR :: ID system :: ID
1.27 + no_met :: ID make_ratpoly_in :: ID
1.28 + bdv :: real c :: real c_2 :: real c_3 :: real c_4 :: real
1.29 +
1.30 +partial_function (tailrec) biegelinie ::
1.31 + "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool"
1.32 +where
1.33 + "biegelinie l q v b s =
1.34 + (let
1.35 + funs = (SubProblem (Biegelinie',
1.36 + [vonBelastungZu, Biegelinien], [Biegelinien, ausBelastung])
1.37 + [REAL q, REAL v]);
1.38 + equs = (SubProblem (Biegelinie',
1.39 + [setzeRandbedingungen, Biegelinien], [Biegelinien, setzeRandbedingungenEin])
1.40 + [BOOL_LIST funs, BOOL_LIST s]);
1.41 + cons = (SubProblem (Biegelinie', [LINEAR, system], [no_met])
1.42 + [BOOL_LIST equs, REAL_LIST [c, c_2, c_3, c_4]]);
1.43 + B = Take (lastI funs);
1.44 + B = ((Substitute cons) @@
1.45 + (Rewrite_Set_Inst [(bdv, v)] make_ratpoly_in False)) B
1.46 + in B) "
1.47 +
1.48 + \\\------------------------------------------------------------------------------------*)
1.49 +
1.50 +setup {* KEStore_Elems.add_mets
1.51 + [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
1.52 (["IntegrierenUndKonstanteBestimmen2"],
1.53 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
1.54 - (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.55 - ("#Find" ,["Biegelinie b_b"]),
1.56 - ("#Relate",["Randbedingungen r_b"])],
1.57 + [("#Given" ,["Traegerlaenge l", "Streckenlast q", "FunktionsVariable v"]),
1.58 + (*("#Where",["0 < l"]), ...wait for < and handling Arbfix*)
1.59 + ("#Find" ,["Biegelinie b"]),
1.60 + ("#Relate",["Randbedingungen s"])],
1.61 {rew_ord'="tless_true",
1.62 rls' = Rule.append_rls "erls_IntegrierenUndK.." Rule.e_rls
1.63 [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
1.64 @@ -280,24 +314,22 @@
1.65 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
1.66 Rule.Thm ("if_False",TermC.num_str @{thm if_False})],
1.67 prls = Rule.Erls, crls = Atools_erls, errpats = [], nrls = Rule.Erls},
1.68 - "Script Biegelinie2Script " ^
1.69 - "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
1.70 - " (let " ^
1.71 - " (fun_s:: bool list) = " ^
1.72 - " (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
1.73 - " [Biegelinien,ausBelastung]) " ^
1.74 - " [REAL q__q, REAL v_v]); " ^
1.75 - " (equ_s::bool list) = " ^
1.76 - " (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien], " ^
1.77 - " [Biegelinien,setzeRandbedingungenEin]) " ^
1.78 - " [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
1.79 - " (con_s::bool list) = " ^
1.80 - " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
1.81 - " [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
1.82 - " B_B = Take (lastI fun_s); " ^
1.83 - " B_B = ((Substitute con_s) @@ " ^
1.84 - " (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
1.85 - " in B_B)"),
1.86 + "Script Biegelinie2Script " ^
1.87 + "(l::real) (q :: real) (v :: real) (b :: real => real) (s :: bool list) = " ^
1.88 + " (let " ^
1.89 + " (funs :: bool list) = (SubProblem (Biegelinie', " ^
1.90 + " [vonBelastungZu, Biegelinien], [Biegelinien, ausBelastung]) " ^
1.91 + " [REAL q, REAL v]); " ^
1.92 + " (equs :: bool list) = (SubProblem (Biegelinie', " ^
1.93 + " [setzeRandbedingungen, Biegelinien], [Biegelinien, setzeRandbedingungenEin]) " ^
1.94 + " [BOOL_LIST funs, BOOL_LIST s]); " ^
1.95 + " (cons :: bool list) = (SubProblem (Biegelinie', " ^
1.96 + " [LINEAR, system], [no_met]) " ^
1.97 + " [BOOL_LIST equs, REAL_LIST [c, c_2, c_3, c_4]]); " ^
1.98 + " B = Take (lastI funs); " ^
1.99 + " B = ((Substitute cons) @@ " ^
1.100 + " (Rewrite_Set_Inst [(bdv, v)] make_ratpoly_in False)) B " ^
1.101 + " in B) "),
1.102 Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID
1.103 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
1.104 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
1.105 @@ -317,8 +349,12 @@
1.106 (["Biegelinien"], [],
1.107 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
1.108 errpats = [], nrls = Rule.e_rls},
1.109 - "empty_script"),
1.110 - Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
1.111 + "empty_script")]
1.112 +*}
1.113 +subsection \<open>Compute the general bending line\<close>
1.114 +
1.115 +setup {* KEStore_Elems.add_mets
1.116 + [Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
1.117 (["Biegelinien", "ausBelastung"],
1.118 [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
1.119 ("#Find" ,["Funktionen fun_s"])],
1.120 @@ -354,8 +390,12 @@
1.121 " (SubProblem (Biegelinie',[named,integrate,function], " ^
1.122 " [diff,integration,named]) " ^
1.123 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
1.124 - " in [Q__Q, M__M, N__N, B__B])"),
1.125 - Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID
1.126 + " in [Q__Q, M__M, N__N, B__B])")]
1.127 +*}
1.128 +subsection \<open>Substitute the constraints into the equations\<close>
1.129 +
1.130 +setup {* KEStore_Elems.add_mets
1.131 + [Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID
1.132 (["Biegelinien", "setzeRandbedingungenEin"],
1.133 [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
1.134 ("#Find" , ["Gleichungen equs'''"])],
1.135 @@ -413,8 +453,12 @@
1.136 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.137 " [Equation,fromFunction]) " ^
1.138 " [BOOL (hd f_s), BOOL b_4]) " ^
1.139 - " in [e_1,e_2,e_3,e_4])"*)),
1.140 - Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID
1.141 + " in [e_1,e_2,e_3,e_4])"*))]
1.142 +*}
1.143 +subsection \<open>Transform an equality into a function\<close>
1.144 +
1.145 +setup {* KEStore_Elems.add_mets
1.146 + [Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID
1.147 (["Equation","fromFunction"],
1.148 [("#Given" ,["functionEq fu_n","substitution su_b"]),
1.149 ("#Find" ,["equality equ'''"])],