1.1 --- a/src/Tools/isac/Interpret/li-tool.sml Sat Aug 19 05:06:55 2023 +0200
1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Sun Aug 20 08:54:01 2023 +0200
1.3 @@ -296,21 +296,25 @@
1.4 if Config.get ctxt LI_trace
1.5 then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
1.6 else ();
1.7 -
1.8 fun assoc_by_type ctxt f aa prog met_id formals actuals =
1.9 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
1.10 [] => raise ERROR (msg_miss_type ctxt prog met_id f formals actuals)
1.11 | [a] => (f, a)
1.12 | aas as (a :: _) => (writeln (msg_ambiguous ctxt prog met_id f aas formals actuals); (f, a));
1.13 +
1.14 fun relate_args _ (f::_) [] ctxt prog met_id formals actuals =
1.15 raise ERROR (msg_miss ctxt prog met_id "relate_args" f formals actuals)
1.16 | relate_args env [] _ _ _ _ _ _ = env (*may drop Find?*)
1.17 | relate_args env (f::ff) (aas as (a::aa)) ctxt prog met_id formals actuals =
1.18 if type_of f = type_of a
1.19 - then relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals
1.20 + then
1.21 + relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals
1.22 else
1.23 - let val (f, a) = assoc_by_type ctxt f aas prog met_id formals actuals
1.24 - in relate_args (env @ [(f, a)]) ff (remove op = a aas) ctxt prog met_id formals actuals end
1.25 + let
1.26 + val (f, a) = assoc_by_type ctxt f aas prog met_id formals actuals
1.27 + in
1.28 + relate_args (env @ [(f, a)]) ff (remove op = a aas) ctxt prog met_id formals actuals
1.29 + end
1.30 (** )in( **)
1.31 fun init_pstate ctxt i_model met_id =
1.32 let
2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Sat Aug 19 05:06:55 2023 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Sun Aug 20 08:54:01 2023 +0200
2.3 @@ -352,6 +352,9 @@
2.4 (* Streckenlast Biegelinie Funktionen
2.5 FunktionsVariable AbleitungBiegelinie *)
2.6 "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list"
2.7 +(* q__q----v_v------b_b--------------id_der------*)
2.8 +(*NEW id_lateral_f
2.9 + id_momentum*)
2.10 where
2.11 "belastung_zu_biegelinie q__q v_v b_b id_der = (
2.12 let
3.1 --- a/src/Tools/isac/MathEngBasic/specification-def.sml Sat Aug 19 05:06:55 2023 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/specification-def.sml Sun Aug 20 08:54:01 2023 +0200
3.3 @@ -15,7 +15,7 @@
3.4 struct
3.5 (**)
3.6
3.7 -type T = (* NOTES AT START PIDE-ADAPTATION*)
3.8 +type T = (* NOTES AT START PIDE-ADAPTATION..*)
3.9 bool * (* I_Model.T andalso Pre_Conds.T ELIMINATE*)
3.10 Pos.pos_ * (* model belongs to Problem or MethodC *)
3.11 term * (* the headline shown on Calc.T NOT SPECIFIC FOR Pbl | Met*)
4.1 --- a/test/Tools/isac/Test_Isac.thy Sat Aug 19 05:06:55 2023 +0200
4.2 +++ b/test/Tools/isac/Test_Isac.thy Sun Aug 20 08:54:01 2023 +0200
4.3 @@ -138,6 +138,7 @@
4.4 \<close>
4.5
4.6 ML \<open>
4.7 +\<close> ML \<open>
4.8 "~~~~~ fun xxx , args:"; val () = ();
4.9 "~~~~~ and xxx , args:"; val () = ();
4.10 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
4.11 @@ -146,7 +147,7 @@
4.12 "xx"
4.13 ^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
4.14 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
4.15 - (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
4.16 +(*//------------------ adhoc inserted n ----------------------------------------------------\\*)
4.17 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)
4.18 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
4.19
4.20 @@ -181,8 +182,7 @@
4.21 \<close>
4.22 ML \<open>
4.23 \<close> ML \<open>
4.24 -\<close> ML \<open>
4.25 -\<close> ML \<open>
4.26 +
4.27 \<close> ML \<open>
4.28 \<close>
4.29
4.30 @@ -346,7 +346,17 @@
4.31 ML_file "Knowledge/diff-app.sml" (* postponed to dev. specification | TP-prog. *)
4.32 ML_file "Knowledge/biegelinie-1.sml"
4.33 ML_file "Knowledge/biegelinie-2.sml" (*Test_Isac_Short*)
4.34 +ML \<open> (* \<longrightarrow> Test_Some.thy *)
4.35 +\<close> ML \<open>
4.36 +
4.37 +\<close> ML \<open>
4.38 +\<close>
4.39 ML_file "Knowledge/biegelinie-3.sml" (*Test_Isac_Short*)
4.40 +ML \<open>
4.41 +\<close> ML \<open>
4.42 +
4.43 +\<close> ML \<open>
4.44 +\<close>
4.45 ML_file "Knowledge/biegelinie-4.sml"
4.46 ML_file "Knowledge/algein.sml"
4.47 ML_file "Knowledge/diophanteq.sml"
4.48 @@ -364,8 +374,7 @@
4.49 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
4.50 ML \<open>
4.51 \<close> ML \<open>
4.52 -\<close> ML \<open>
4.53 -\<close> ML \<open>
4.54 +
4.55 \<close> ML \<open>
4.56 \<close>
4.57
5.1 --- a/test/Tools/isac/Test_Some.thy Sat Aug 19 05:06:55 2023 +0200
5.2 +++ b/test/Tools/isac/Test_Some.thy Sun Aug 20 08:54:01 2023 +0200
5.3 @@ -70,20 +70,12 @@
5.4 val return_XXXXX = "XXXXX"
5.5 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
5.6 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
5.7 -\<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)
5.8 -(*-------------------- continuing XXXXX ------------------------------------------------------*)
5.9 +\<close> ML \<open> (*||----------- continuing XXXXX ------------------------------------------------------*)
5.10 +(*||------------------ continuing XXXXX ------------------------------------------------------*)
5.11 (*\\------------------ step into XXXXX -----------------------------------------------------//*)
5.12 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
5.13 val "XXXXX" = return_XXXXX;
5.14
5.15 -(*/------------------- check entry to XXXXX -------------------------------------------------\*)
5.16 -(*\------------------- check entry to XXXXX -------------------------------------------------/*)
5.17 -(*/------------------- check within XXXXX ---------------------------------------------------\*)
5.18 -(*\------------------- check within XXXXX ---------------------------------------------------/*)
5.19 -(*/------------------- check result of XXXXX ------------------------------------------------\*)
5.20 -(*\------------------- check result of XXXXX ------------------------------------------------/*)
5.21 -(* final test ... ----------------------------------------------------------------------------*)
5.22 -
5.23 \<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)
5.24 (*//------------------ inserted hidden code ------------------------------------------------\\*)
5.25 (*\\------------------ inserted hidden code ------------------------------------------------//*)
5.26 @@ -116,426 +108,539 @@
5.27 section \<open>===== ============================================================================\<close>
5.28 ML \<open>
5.29 \<close> ML \<open>
5.30 -\<close> ML \<open>
5.31 +
5.32 \<close> ML \<open>
5.33 \<close>
5.34
5.35 section \<open>===================================================================================\<close>
5.36 -section \<open>===== simplify.sml ================================================================\<close>
5.37 +section \<open>===== biegelinie-2.sml ============================================================\<close>
5.38 ML \<open>
5.39 \<close> ML \<open>
5.40 +(* Title: Knowledge/biegelinie-2.sml
5.41 + author: Walther Neuper 190515
5.42 + (c) due to copyright terms
5.43 +*)
5.44 +"table of contents -----------------------------------------------";
5.45 +"-----------------------------------------------------------------";
5.46 +"----------- auto SubProblem (_,[vonBelastungZu,Biegelinien] -----";
5.47 +"----------- me SubProblem (_,[vonBelastungZu,Biegelinien] -------";
5.48 +"-----------------------------------------------------------------";
5.49 +"-----------------------------------------------------------------";
5.50 +"-----------------------------------------------------------------";
5.51 +
5.52 +
5.53 +"----------- auto SubProblem (_,[vonBelastungZu,Biegelinien] -----";
5.54 +"----------- auto SubProblem (_,[vonBelastungZu,Biegelinien] -----";
5.55 +"----------- auto SubProblem (_,[vonBelastungZu,Biegelinien] -----";
5.56 +val fmz =
5.57 + ["Streckenlast q_0", "FunktionsVariable x",
5.58 + "Funktionen [Q x = c + - 1 * q_0 * x, \
5.59 + \M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\
5.60 + \ y' x = c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\
5.61 + \ y x = c_4 + c_3 * x + 1 / (- 1 * EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]",
5.62 + "AbleitungBiegelinie dy"];
5.63 +val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu", "Biegelinien"],
5.64 + ["Biegelinien", "ausBelastung"]);
5.65 +
5.66 +States.reset ();
5.67 +CalcTree @{context} [(fmz, (dI',pI',mI'))];
5.68 +Iterator 1;
5.69 +moveActiveRoot 1;
5.70 +autoCalculate 1 CompleteCalc;
5.71 +
5.72 +val ((pt, p),_) = States.get_calc 1;
5.73 +(* ERROR: THIS TEST WAS BROKEN BEFORE CS "eliminate ThmC.numerals_to_Free",
5.74 + UNDETECTED BY Test_Isac_Short.thy ===========================================================\\
5.75 +if p = ([], Res) andalso (get_obj g_res pt (fst p) |> UnparseC.term @{context}) =
5.76 + "[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n dy x =\n c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]"
5.77 +then () else error "auto SubProblem (_,[vonBelastungZu,Biegelinien] changed";
5.78 +===============================================================================================//*)
5.79 +
5.80
5.81 \<close> ML \<open>
5.82 -\<close> ML \<open>
5.83 -\<close>
5.84 -
5.85 -section \<open>===================================================================================\<close>
5.86 -section \<open>===== Interpret/li-tool.sml =======================================================\<close>
5.87 -ML \<open>
5.88 -\<close> ML \<open>
5.89 -(* Title: Interpret/li-tool.sml
5.90 - Author: Walther Neuper 050908
5.91 - (c) copyright due to lincense terms.
5.92 -*)
5.93 -"-----------------------------------------------------------------";
5.94 -"table of contents -----------------------------------------------";
5.95 -"-----------------------------------------------------------------";
5.96 -"----------- fun implicit_take, fun get_first_argument -------------------------";
5.97 -"----------- fun from_prog ---------------------------------------";
5.98 -"----------- fun specific_from_prog ----------------------------";
5.99 -"----------- fun de_esc_underscore -------------------------------";
5.100 -"----------- fun go ----------------------------------------------";
5.101 -"----------- fun formal_args -------------------------------------";
5.102 -"----------- fun dsc_valT ----------------------------------------";
5.103 -"----------- fun arguments_from_model ---------------------------------------";
5.104 -"----------- fun init_pstate -----------------------------------------------------------------";
5.105 -"-----------------------------------------------------------------";
5.106 -"-----------------------------------------------------------------";
5.107 -"-----------------------------------------------------------------";
5.108 -
5.109 -val thy = @{theory Isac_Knowledge};
5.110 -
5.111 -\<close> ML \<open>
5.112 -"----------- fun init_pstate -----------------------------------------------------------------";
5.113 -"----------- fun init_pstate -----------------------------------------------------------------";
5.114 -"----------- fun init_pstate -----------------------------------------------------------------";
5.115 -(*
5.116 - This test is deeply nested (down into details of creating environments).
5.117 - In order to make Sidekick show the structure add to each
5.118 - * (*/...\*) and (*\.../*)
5.119 - * a companion > ML < (*/...\*) and > ML < (*\.../*)
5.120 - Note the wrong ^----^ delimiters.
5.121 -*)
5.122 -val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
5.123 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
5.124 - "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
5.125 - "AbleitungBiegelinie dy"];
5.126 -val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
5.127 - ["IntegrierenUndKonstanteBestimmen2"]);
5.128 +"----------- me SubProblem (_,[vonBelastungZu,Biegelinien] -------";
5.129 +"----------- me SubProblem (_,[vonBelastungZu,Biegelinien] -------";
5.130 +"----------- me SubProblem (_,[vonBelastungZu,Biegelinien] -------";
5.131 +val fmz =
5.132 + ["Streckenlast q_0", "FunktionsVariable x",
5.133 + "Funktionen [Q x = c + - 1 * q_0 * x, \
5.134 + \M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\
5.135 + \ y' x = c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\
5.136 + \ y x = c_4 + c_3 * x + 1 / (- 1 * EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]",
5.137 + "AbleitungBiegelinie dy"];
5.138 +val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu", "Biegelinien"],
5.139 + ["Biegelinien", "ausBelastung"]);
5.140 val p = e_pos'; val c = [];
5.141 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; val Model_Problem = nxt
5.142 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt
5.143 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
5.144 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt
5.145 -\<close> ML \<open>
5.146 -(*/---broken elementwise input to lists---\* )
5.147 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
5.148 - (*isa* ) val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt
5.149 - ( *isa2*) val Add_Relation "Randbedingungen [y 0 = 0]" = nxt
5.150 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
5.151 - (*isa*) val Specify_Theory "Biegelinie" = nxt
5.152 - (*isa2* ) val Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]" = nxt( **)
5.153 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; val Model_Problem = nxt
5.154 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
5.155 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "FunktionsVariable x" = nxt
5.156 +\<close> ML \<open> (*isa*)
5.157 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) *\n (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]" = nxt
5.158 +\<close> text \<open> (*isa2* )
5.159 +(*/---broken elementwise input to lists---\*)
5.160 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Funktionen [Q x = c + - 1 * q_0 * x]" = nxt
5.161 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Funktionen\n [M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) *\n (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]" = nxt
5.162 ( *\---broken elementwise input to lists---/*)
5.163 \<close> ML \<open>
5.164 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt
5.165 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
5.166 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt
5.167 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
5.168 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "FunktionsVariable x" = nxt
5.169 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = nxt
5.170 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
5.171 -
5.172 -\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
5.173 -(*[], Met*)val return_Add_Given_AbleitungBieg
5.174 - = me nxt p c pt;
5.175 -\<close> ML \<open> (*/------------ step into me_Add_Given_AbleitungBieg --------------------------------\\*)
5.176 -(*/------------------- step into me_Add_Given_AbleitungBieg --------------------------------\\*)
5.177 -
5.178 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
5.179 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["vonBelastungZu", "Biegelinien"] = nxt
5.180 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Biegelinien", "ausBelastung"] = nxt
5.181 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
5.182 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.183 +val return_me_Add_Given_AbleitungBiegelinie
5.184 + = me nxt p c pt;
5.185 +\<close> ML \<open> (*//----------- step into me_Add_Given_AbleitungBiegelinie --------------------------\\*)
5.186 +(*//------------------ step into me_Add_Given_AbleitungBiegelinie --------------------------\\*)
5.187 +\<close> ML \<open>
5.188 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
5.189 +\<close> ML \<open>
5.190 val ctxt = Ctree.get_ctxt pt p
5.191 -val ("ok", (_, _, ptp as (pt, p))) =
5.192 - (*case*) Step.by_tactic tac (pt, p) (*of*);
5.193 -
5.194 -\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
5.195 - (*case*)
5.196 + val (pt, p) =
5.197 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
5.198 + case Step.by_tactic tac (pt, p) of
5.199 + ("ok", (_, _, ptp)) => ptp
5.200 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.201 + (*case*)
5.202 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
5.203 \<close> ML \<open>
5.204 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
5.205 - (p, ((pt, Pos.e_pos'), []) );
5.206 + (p, ((pt, Pos.e_pos'), []));
5.207 +\<close> ML \<open>
5.208 + (*if*) Pos.on_calc_end ip (*else*);
5.209 +\<close> ML \<open>
5.210 + val (_, probl_id, _) = Calc.references (pt, p);
5.211 +\<close> ML \<open>
5.212 +val _ =
5.213 + (*case*) tacis (*of*);
5.214 +\<close> ML \<open>
5.215 + (*if*) probl_id = Problem.id_empty (*else*);
5.216 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.217 + switch_specify_solve p_ (pt, ip);
5.218 +\<close> ML \<open>
5.219 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.220 +\<close> ML \<open>
5.221 + (*if*) Pos.on_specification ([], state_pos) (*then*);
5.222 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.223 + specify_do_next (pt, input_pos);
5.224 +\<close> ML \<open>
5.225 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
5.226 +\<close> ML \<open>
5.227 + val (_, (p_', tac)) = Specify.find_next_step ptp
5.228 + val ist_ctxt = Ctree.get_loc pt (p, p_)
5.229 +\<close> ML \<open>
5.230 +val Tactic.Apply_Method mI =
5.231 + (*case*) tac (*of*);
5.232 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.233 + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
5.234 + ist_ctxt (pt, (p, p_'));
5.235 +\<close> ML \<open>
5.236 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
5.237 + ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
5.238 +\<close> ML \<open>
5.239 + val (itms, oris, probl) = case get_obj I pt p of
5.240 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
5.241 + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
5.242 + val {model, ...} = MethodC.from_store ctxt mI;
5.243 +\<close> ML \<open>
5.244 +(*+*)val "Biegelinien/ausBelastung" = mI |> References.implode_id
5.245 +\<close> ML \<open>
5.246 +(*+* ===== current MethodC i_model ==============================================================*)
5.247 +(*+*)if (itms |> I_Model.to_string @{context}) = "[\n" ^
5.248 + "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.249 + "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
5.250 + "(3 ,[1] ,true ,#Find ,Cor Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) *\n (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)] ,(funs''', [[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]])), \n" ^
5.251 +(* ...................... Cor Biegemoment M_b,
5.252 + ...................... Cor Querkraft Q , *)
5.253 + "(4 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"
5.254 +(* ...................... Cor Biegelinie y , *)
5.255 +then () else error "by_tactic: parent "
5.256 +\<close> ML \<open>
5.257 +(*+* ===== current o_model created from Formalise.model of SubProblem ===========================*)
5.258 +(*+*)(oris |> O_Model.to_string @{context}) = "[\n" ^
5.259 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.260 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
5.261 + "(3, [\"1\"], #Find, Funktionen, [\"[Q x = c + - 1 * q_0 * x]\", \"[M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2]\", \"[y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)]\", \"[y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]\"]), \n" ^
5.262 + "(4, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
5.263 +\<close> ML \<open>
5.264 +(*+* ===== parent Problem i_model ===============================================================*)
5.265 +(*+*)(probl |> I_Model.to_string @{context}) = "[\n" ^
5.266 + "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.267 + "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
5.268 + "(3 ,[1] ,true ,#Find ,Cor Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) *\n (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)] ,(funs''', [[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]))]"
5.269 +\<close> ML \<open>
5.270 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
5.271 +\<close> ML \<open>
5.272 +(*+* ===== current MethodC i_model complete'd ===================================================*)
5.273 +(*+*)(itms |> I_Model.to_string @{context}) = "[\n" ^
5.274 + "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.275 + "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
5.276 + "(3 ,[1] ,true ,#Find ,Cor Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) *\n (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)] ,(funs''', [[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]])), \n" ^
5.277 + "(4 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"
5.278 +\<close> ML \<open>
5.279 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.280 + val (is, env, ctxt, prog) = case
5.281 + LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
5.282 + (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
5.283 +\<close> ML \<open>
5.284 +"~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) = (ctxt, (I_Model.OLD_to_TEST itms), mI);
5.285 +\<close> ML \<open>
5.286 + val (model_patt, program, prog, prog_rls, where_, where_rls) =
5.287 + case MethodC.from_store ctxt met_id of
5.288 + {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>
5.289 + (model_patt, program, prog, prog_rls, where_, where_rls)
5.290 +\<close> ML \<open>
5.291 +(*+* ===== MethodC model_patt ===================================================================*)
5.292 +(*+*)if (model_patt |> Model_Pattern.to_string @{context}) = "[\"" ^
5.293 + (*5 elements ------------------------------------------ ERROR: -------------CORRECT: *)
5.294 + "(#Given, (Streckenlast, q__q))\", \"" ^
5.295 + "(#Given, (FunktionsVariable, v_v))\", \"" ^
5.296 + "(#Given, (Biegelinie, b_b))\", \"" ^ (*\<longrightarrow> (b_b, dy) (b_b, y) *)
5.297 + "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^ (*\<longrightarrow> (id_der, [Q x =..]) (id_der, dy) *)
5.298 + "(#Find, (Funktionen, fun_s))\"]" (* (fun_s, [Q x =..])*)
5.299 +then () else error "init_pstate initial model_patt CHANGED"
5.300 +\<close> ML \<open>
5.301 +(*+*)if (i_model |> I_Model.to_string_TEST @{context}) = "[\n" ^
5.302 + "(1, [1], true ,#Given, (Cor_TEST Streckenlast q_0 , pen2str, Position.T)), \n" ^
5.303 + "(2, [1], true ,#Given, (Cor_TEST FunktionsVariable x , pen2str, Position.T)), \n" ^
5.304 + "(3, [1], true ,#Find, (Cor_TEST Funktionen\n [" ^
5.305 + "Q x = c + - 1 * q_0 * x, " ^
5.306 + "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n " ^
5.307 + "y' x =\n c_3 +\n 1 / (- 1 * EI) *\n (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n " ^
5.308 + "y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)] , pen2str, Position.T)), \n" ^
5.309 + "(4, [1], true ,#Given, (Cor_TEST AbleitungBiegelinie dy , pen2str, Position.T))]"
5.310 +(*MISSING: ------------------------------------------------------------------- (b_b, y) *)
5.311 +then () else error "init_pstate initial i_model CHANGED";
5.312 +\<close> ML \<open> (*isa*)
5.313 + val (_, env_model, (env_subst, env_eval)) = I_Model.of_max_variant model_patt i_model;
5.314 +(*?! complete with Met.i_model ?!*)
5.315 +\<close> ML \<open> (*isa*)
5.316 +(*+*)if (env_model |> Subst.to_string @{context}) = "[\"\n" ^
5.317 + "(q__q, q_0)\", \"\n" ^
5.318 + "(v_v, x)\", \"\n" ^
5.319 + "(id_der, dy)\", \"\n" ^
5.320 + "(fun_s, [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)])\"]"
5.321 +then () else error "init_pstate: env_model CHANGED";
5.322 +\<close> ML \<open> (*isa*)
5.323 + val actuals = map snd env_model
5.324 +\<close> text \<open> (*isa2*)
5.325 + val (_, env_subst, env_eval) = I_Model.of_max_variant model_patt i_model;
5.326 + val actuals = map snd env_subst
5.327 +\<close> ML \<open> (*isa==isa2*)
5.328 +(*+*)val "[q_0, x, dy, [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]"
5.329 + = actuals |> UnparseC.terms @{context}
5.330 +\<close> ML \<open> (*isa==isa2*)
5.331 + val formals = Program.formal_args prog
5.332 +\<close> ML \<open> (*isa==isa2*)
5.333 +(*+*)val "[q__q, v_v, b_b, id_der]" = formals |> UnparseC.terms @{context} (*From fun. belastung_zu_biegelinie*)
5.334 +\<close> ML \<open> (*isa*)
5.335 + val preconds = Pre_Conds.check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval))
5.336 + val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
5.337 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.338 + val ist = Istate.e_pstate
5.339 + |> Istate.set_eval prog_rls
5.340 + |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals)
5.341 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.342 + (relate_args [] formals actuals ctxt prog met_id formals actuals);
5.343 +\<close> ML \<open>
5.344 +"~~~~~ fun relate_args , args:"; val (env, (f::ff), (aas as (a::aa)), ctxt, prog, met_id, formals, actuals) =
5.345 + ([], formals, actuals, ctxt, prog, met_id, formals, actuals);
5.346 +
5.347 + (*if*) type_of f = type_of a (*then*);
5.348 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.349 + relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals;
5.350 +\<close> ML \<open>
5.351 +(*+*)val "q__q" = f |> UnparseC.term @{context}
5.352 +(*+*)val "q_0" = a |> UnparseC.term @{context};
5.353 +\<close> ML \<open>
5.354 + (*if*) type_of f = type_of a (*then*);
5.355 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.356 + relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals;
5.357 +\<close> ML \<open>
5.358 +"~~~~~ fun relate_args , args:"; val (env, (f::ff), (aas as (a::aa)), ctxt, prog, met_id, formals, actuals) =
5.359 + ((env @ [(f, a)]), ff, aa, ctxt, prog, met_id, formals, actuals)
5.360 +\<close> ML \<open>
5.361 +(*+*)val "v_v" = f |> UnparseC.term @{context}
5.362 +(*+*)val "x" = a |> UnparseC.term @{context}
5.363 +\<close> ML \<open>
5.364 + (*if*) type_of f = type_of a (*then*);
5.365 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.366 + relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals;
5.367 +\<close> ML \<open>
5.368 +"~~~~~ fun relate_args , args:"; val (env, (f::ff), (aas as (a::aa)), ctxt, prog, met_id, formals, actuals) =
5.369 + ((env @ [(f, a)]), ff, aa, ctxt, prog, met_id, formals, actuals)
5.370 +\<close> ML \<open>
5.371 +(*+*)val "b_b" = f |> UnparseC.term @{context} (*ERROR: IS Biegelinie*)
5.372 +(*+*)val "dy" = a |> UnparseC.term @{context} (*ERROR: IS AbleitungBiegelinie*)
5.373 +(*CONCLUSION: if the type is equal, then the sequence decides the pairing for env
5.374 + (q__q, q_0)
5.375 + (v_v, x)
5.376 +*)
5.377 +\<close> ML \<open>
5.378 + (*if*) type_of f = type_of a (*then*);
5.379 +\<close> ML \<open>
5.380 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.381 + relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals;
5.382 +\<close> ML \<open>
5.383 +"~~~~~ fun relate_args , args:"; val (env, (f::ff), (aas as (a::aa)), ctxt, prog, met_id, formals, actuals) =
5.384 + ((env @ [(f, a)]), ff, aa, ctxt, prog, met_id, formals, actuals)
5.385 +\<close> ML \<open>
5.386 +(*+*)val "id_der" = f |> UnparseC.term @{context} (*ERROR IS AbleitungBiegelinie*)
5.387 +(*+*)val "[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n y' x =\n c_3 +\n 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]"
5.388 + = a |> UnparseC.term @{context} (*ERROR IS FROM Pbl.i_model*)
5.389 +\<close> ML \<open>
5.390 + (*if*) type_of f = type_of a (*else*);
5.391 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.392 + val (f, a) =
5.393 + assoc_by_type ctxt f aas prog met_id formals actuals;
5.394 +\<close> ML \<open>
5.395 +"~~~~~ fun assoc_by_type , args:"; val (ctxt, f, aa, prog, met_id, formals, actuals) =
5.396 + (ctxt, f, aas, prog, met_id, formals, actuals);
5.397 +\<close> ML \<open>
5.398 +val [] =
5.399 + (*case*) filter (curry (fn (f, a) => type_of f = type_of a) f) aa (*of*);
5.400 +\<close> ML \<open>
5.401 +(*+*)val Free ("id_der", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])) = f
5.402 +\<close> ML \<open>
5.403 +(*+*)val [Const ("List.list.Cons", _) $ _ $
5.404 + (Const ("List.list.Cons", _) $ _ $
5.405 + (Const ("List.list.Cons", _) $ _ $
5.406 + (Const ("List.list.Cons", _) $ _ $
5.407 + Const ("List.list.Nil", list_elem_type))))] = aa
5.408 +(*+*)val Type ("List.list", [Type ("HOL.bool", [])]) = list_elem_type
5.409 +\<close> ML \<open>
5.410 +\<close> ML \<open>
5.411 +\<close> ML \<open>
5.412 +\<close> ML \<open>
5.413 +\<close> ML \<open>
5.414 +\<close> ML \<open>
5.415 +\<close> ML \<open>
5.416 +\<close> ML \<open>
5.417 +\<close> ML \<open>
5.418 +\<close> ML \<open> (*||----------- continuing me_Add_Given_AbleitungBiegelinie ---------------------------*)
5.419 +(*||------------------ continuing me_Add_Given_AbleitungBiegelinie ---------------------------*)
5.420 +(*\\------------------ step into XXXXX -----------------------------------------------------//*)
5.421 +\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
5.422 +\<close> text \<open> (*ERROR in creating the environment from formal args*)
5.423 +val (p,_,f,nxt,_,pt) = return_me_Add_Given_AbleitungBiegelinie;
5.424 +\<close> ML \<open>
5.425 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)
5.426 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.427 +*)
5.428 +(* ERROR: THIS TEST WAS BROKEN BEFORE CS "eliminate ThmC.numerals_to_Free",
5.429 + UNDETECTED BY Test_Isac_Short.thy
5.430 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5.431 +arguments_from_model: 'Biegelinie' not in itms:
5.432 +itms:
5.433 +[
5.434 +(1 ,[1] ,true ,#Given ,Cor ??.Biegelinie.Streckenlast q_0 ,(q_q, [q_0])),
5.435 +(2 ,[1] ,true ,#Given ,Cor ??.Biegelinie.FunktionsVariable x ,(v_v, [x])),
5.436 +(3 ,[1] ,true ,#Find ,Cor ??.Biegelinie.Funktionen [
5.437 + ??.Biegelinie.Q x = c + - 1 * q_0 * x,
5.438 + ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,
5.439 + ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),
5.440 + y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)],
5.441 + (funs''', [[
5.442 + ??.Biegelinie.Q x = c + - 1 * q_0 * x,
5.443 + ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,
5.444 + ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),
5.445 + y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]) ),
5.446 +(4 ,[1] ,true ,#Given ,Cor ??.Biegelinie.AbleitungBiegelinie dy ,(id_der, [dy]))]
5.447 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5.448 +CORRECTION:
5.449 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5.450 +Const ("Biegelinie.Biegelinie", _) MUST BE IN itms OF THE model,
5.451 +BECAUSE REQUIRED BY GUARD OF MethodC.
5.452 +*)
5.453 +(*//---------------- adhoc inserted ------------------------------------------------\\*)
5.454 +\<close> ML \<open>
5.455 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
5.456 + val (pt, p) =
5.457 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
5.458 + case Step.by_tactic tac (pt, p) of
5.459 + ("ok", (_, _, ptp)) => ptp
5.460 + | ("unsafe-ok", (_, _, ptp)) => ptp
5.461 + | ("not-applicable",_) => (pt, p)
5.462 + | ("end-of-calculation", (_, _, ptp)) => ptp
5.463 + | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
5.464 + | _ => raise ERROR "me: uncovered case Step.by_tactic";
5.465 +\<close> ML \<open>
5.466 +
5.467 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)
5.468 + (*case*)
5.469 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
5.470 +*)
5.471 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
5.472 + (p, ((pt, Pos.e_pos'), []));
5.473 (*if*) Pos.on_calc_end ip (*else*);
5.474 val (_, probl_id, _) = Calc.references (pt, p);
5.475 val _ =
5.476 (*case*) tacis (*of*);
5.477 (*if*) probl_id = Problem.id_empty (*else*);
5.478
5.479 -\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
5.480 - switch_specify_solve p_ (pt, ip);
5.481 -\<close> ML \<open>
5.482 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)
5.483 + switch_specify_solve p_ (pt, ip)
5.484 +*)
5.485 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.486 - (*if*) Pos.on_specification ([], state_pos) (*then*);
5.487 + (*if*) Pos.on_specification ([], state_pos) (*then*);
5.488
5.489 -\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
5.490 - specify_do_next (pt, input_pos);
5.491 -\<close> ML \<open>
5.492 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)
5.493 + specify_do_next (pt, input_pos)
5.494 +*)
5.495 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
5.496 val (_, (p_', tac)) = Specify.find_next_step ptp
5.497 val ist_ctxt = Ctree.get_loc pt (p, p_)
5.498 val Tactic.Apply_Method mI =
5.499 (*case*) tac (*of*);
5.500
5.501 -\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
5.502 - LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
5.503 - ist_ctxt (pt, (p, p_'));
5.504 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)
5.505 + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt (pt, (p, p_'))
5.506 +*)
5.507 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
5.508 +((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
5.509 + val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
5.510 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
5.511 + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
5.512 + val {model, ...} = MethodC.from_store ctxt mI;
5.513 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
5.514 + val prog_rls = LItool.get_simplifier (pt, pos);
5.515 +
5.516 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)
5.517 + (*case*)
5.518 + LItool.init_pstate prog_rls ctxt itms mI (*of*);
5.519 +*)
5.520 +"~~~~~ fun init_pstate , args:"; val (prog_rls, ctxt, itms, metID) = (prog_rls, ctxt, itms, mI);
5.521 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ... (**)
5.522 + val actuals =
5.523 + arguments_from_model metID itms
5.524 +*)
5.525 \<close> ML \<open>
5.526 -"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
5.527 - ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
5.528 - val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
5.529 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
5.530 - | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
5.531 - val {model, ...} = MethodC.from_store ctxt mI;
5.532 - val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
5.533 -;
5.534 -(*+*)if (itms |> I_Model.to_string @{context}) = "[\n" ^
5.535 - "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
5.536 - "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.537 - "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
5.538 - "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^
5.539 - "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(fun_var, [x])), \n" ^
5.540 - "(6 ,[1] ,true ,#Given ,Cor GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]])), \n" ^
5.541 - "(7 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"
5.542 -(*+*)then () else error "init_pstate: initial i_model changed";
5.543 -(*+*)if (itms |> I_Model.penv_to_string @{context}) = "[" ^ (*to be eliminated*)
5.544 -(*1*)"(l_l, [L]), " ^
5.545 -(*2*)"(q_q, [q_0]), " ^
5.546 -(*3*)"(b_b, [y]), " ^
5.547 -(*4*)"(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), " ^
5.548 -(*5*)"(fun_var, [x]), " ^
5.549 -(*6*)"(vs, [[c, c_2, c_3, c_4]]), " ^
5.550 -(*7*)"(id_der, [dy])]"
5.551 -(*+*)then () else error "init_pstate: initial penv changed";
5.552 +"~~~~~ fun arguments_from_model , args:"; val (mI, itms) = (metID, itms);
5.553 + val mvat = Pre_Conds.max_variant itms
5.554 + fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
5.555 + val itms = filter (okv mvat) itms;
5.556
5.557 -\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
5.558 - (*case*)
5.559 - LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI (*of*);
5.560 -\<close> ML \<open>(*//------------ step into init_pstate -----------------------------------------------\\*)
5.561 -(*//------------------ step into init_pstate -----------------------------------------------\\*)
5.562 -"~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) = (ctxt, (I_Model.OLD_to_TEST itms), mI);
5.563 - val (model_patt, program, prog, prog_rls, where_, where_rls) =
5.564 - case MethodC.from_store ctxt met_id of
5.565 - {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>
5.566 - (model_patt, program, prog, prog_rls, where_, where_rls)
5.567 +I_Model.to_string @{context} itms |> writeln;
5.568 +(*[
5.569 +(1 ,[1] ,true ,#Given ,Cor ??.Biegelinie.Streckenlast q_0 ,(q_q, [q_0])),
5.570 +(2 ,[1] ,true ,#Given ,Cor ??.Biegelinie.FunktionsVariable x ,(v_v, [x])),
5.571 +(3 ,[1] ,true ,#Find ,Cor ??.Biegelinie.Funktionen [
5.572 + ??.Biegelinie.Q x = c + - 1 * q_0 * x,
5.573 + ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,
5.574 + ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),
5.575 + y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)],
5.576 + (funs''', [[
5.577 + ??.Biegelinie.Q x = c + - 1 * q_0 * x,
5.578 + ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,
5.579 + ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),
5.580 + y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]) ),
5.581 +(4 ,[1] ,true ,#Given ,Cor ??.Biegelinie.AbleitungBiegelinie dy ,(id_der, [dy]))]
5.582 +*)
5.583 + fun test_dsc d (_, _, _, _, itm_) = (d = I_Model.descriptor itm_)
5.584 + fun itm2arg itms (_, (d, _)) =
5.585 + case find_first (test_dsc d) itms of
5.586 + NONE => raise ERROR "arguments_from_model ..."(*error_msg_2 d itms*)
5.587 + | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_
5.588
5.589 + val pats = (#model o MethodC.from_store ctxt) mI;
5.590 +(*[("#Given", (Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), Free ("q__q", "real"))),
5.591 + ("#Given", (Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), Free ("v_v", "real"))),
5.592 + ("#Given", (Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), Free ("b_b", "real \<Rightarrow> real"))),
5.593 + ("#Given", (Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), Free ("id_der", "real \<Rightarrow> real"))),
5.594 + ("#Find", (Const ("Biegelinie.Funktionen", "bool list \<Rightarrow> una"), Free ("fun_s", "bool list")))]:
5.595 + Model_Pattern.T*)
5.596 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ... (**)
5.597 + (flat o (map (
5.598 + itm2arg itms))) pats
5.599 +*)
5.600 +"~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 1 pats);
5.601 +val SOME (1, [1], true, "#Given", Cor ((Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)]))) =
5.602 + find_first (test_dsc d) itms;
5.603 +
5.604 +"~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 2 pats);
5.605 +val SOME (2, [1], true, "#Given", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("v_v", _), [Free ("x", _)]))) =
5.606 + find_first (test_dsc d) itms;
5.607 +
5.608 +"~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 3 pats);
5.609 +val Const ("Biegelinie.Biegelinie", _) = d
5.610 +val NONE =
5.611 + find_first (test_dsc d) itms;
5.612 +
5.613 +"~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 4 pats);
5.614 +val SOME (4, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", _), [Free ("dy", _)]), (Free ("id_der", _), [Free ("dy", _)]))) =
5.615 + find_first (test_dsc d) itms;
5.616 +
5.617 +"~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 5 pats);
5.618 +val SOME (3, [1], true, "#Find", Cor ((Const ("Biegelinie.Funktionen", _), _), (Free ("funs'''", _), _))) =
5.619 + find_first (test_dsc d) itms
5.620 +
5.621 +(*\\---------------- adhoc inserted ------------------------------------------------//*)
5.622 \<close> ML \<open>
5.623 - val return_of_max_variant =
5.624 - I_Model.of_max_variant model_patt i_model;
5.625 -\<close> ML \<open>(*///----------- step into of_max_variant --------------------------------------------\\*)
5.626 -(*///----------------- step into of_max_variant --------------------------------------------\\*)
5.627 -"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
5.628 - val all_variants =
5.629 - map (fn (_, variants, _, _, _) => variants) i_model
5.630 - |> flat
5.631 - |> distinct op =
5.632 - val variants_separated = map (filter_variants' i_model) all_variants
5.633 - val sums_corr = map (cnt_corrects) variants_separated
5.634 - val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
5.635 - val (_, max_variant) = hd (*..crude decision, up to improvement *)
5.636 - (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
5.637 - val i_model_max =
5.638 - filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
5.639 - val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
5.640 -;
5.641 -(*+*)if (equal_descr_pairs |> descr_pairs_to_string @{context}) = "[" ^
5.642 -(*defined: in program+model--vvvv--,----------------------------------------- in problem ---vvv*)
5.643 - "((#Given, (Traegerlaenge, l_l)), (1, [1], true ,#Given, " ^ "(Cor_TEST Traegerlaenge L ,(l_l, [L]), Position.T))), " ^
5.644 - "((#Given, (Streckenlast, q_q)), (2, [1], true ,#Given, " ^
5.645 - "(Cor_TEST Streckenlast q_0 ,(q_q, [q_0]), Position.T))), " ^
5.646 - "((#Given, (FunktionsVariable, fun_var)), (5, [1], true ,#Given, " ^
5.647 - "(Cor_TEST FunktionsVariable x ,(fun_var, [x]), Position.T))), " ^
5.648 - "((#Given, (GleichungsVariablen, vs)), (6, [1], true ,#Given, " ^
5.649 - "(Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]]), Position.T))), " ^
5.650 - "((#Given, (AbleitungBiegelinie, id_der)), (7, [1], true ,#Given, " ^
5.651 - "(Cor_TEST AbleitungBiegelinie dy ,(id_der, [dy]), Position.T))), " ^
5.652 - "((#Find, (Biegelinie, b_b)), (3, [1], true ,#Find, (Cor_TEST Biegelinie y ,(b_b, [y]), Position.T))), " ^
5.653 - "((#Relate, (Randbedingungen, r_b)), (4, [1], true ,#Relate, " ^
5.654 - "(Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), Position.T)))]"
5.655 -then () else error "of_max_variant: equal_descr_pairs CHANGED";
5.656 -(*/////############### old test code ##################################################\\\\\\* )
5.657 +(* ERROR: THIS TEST WAS BROKEN BEFORE CS "eliminate ThmC.numerals_to_Free",
5.658 + UNDETECTED BY Test_Isac_Short.thy ===========================================================\\
5.659 +case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
5.660 +| _ => error "biegelinie.sml met2 b";
5.661
5.662 - val env_subst =
5.663 - mk_env_subst_DEL equal_descr_pairs;
5.664 -(*/------------------- ERRORs to remove in CS subsequent to "prepare 1 PIDE turn 11"-000----\* )
5.665 -(*+*)if ( env_subst |> Subst.to_string @{context}) = "[\"\n" ^
5.666 -(*ERRORs------^^^^^^^^^----------isa2: penv ---vvv----------------------..isa2, thus "correct"*)
5.667 -(*1*)"(l_l, L)\", \"\n" ^ (* (l_l, [L]) *)
5.668 -(*2*)"(q_q, q_0)\", \"\n" ^ (* (q_q, [q_0]) *)
5.669 -(*3*)"(fun_var, x)\", \"\n" ^ (* (fun_var, [x]) *)
5.670 -(*4*)"(vs, GleichungsVariablen)\", \"\n" ^ (* (vs, [[c, c_2, c_3, c_4]]) *)
5.671 -(*5*)"(id_der, dy)\", \"\n" ^ (* (id_der, [dy]) *)
5.672 -(*6*)"(b_b, y)\"]" (* (b_b, [y]) *)
5.673 -(*7 missing*) (* (r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]) *)
5.674 -(*+*)then () else error "of_max_variant: env_subst BETTER ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? "
5.675 -( *\------------------- ERRORs to remove ..--------------------------------------------------/*)
5.676 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
5.677 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
5.678 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
5.679 +case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
5.680 +| _ => error "biegelinie.sml met2 c";
5.681
5.682 -(*///----------------- step into mk_env_subst_DEL ------------------------------------------\\*)
5.683 -"~~~~~ fun mk_env_subst_DEL , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
5.684 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.685 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.686 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.687 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.688 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.689
5.690 -(*///################# nth 1 equal_descr_pairs ############################################=\\*)
5.691 - val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
5.692 - => (Pre_Conds.discern_feedback_subst id feedb) (*|> map fst (*rhs dropped*)|> map (pair id)*) ) (nth 1 equal_descr_pairs);
5.693 -"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 1 equal_descr_pairs);
5.694 -(*--------------------------------------------------------------------------^^^----------------*)
5.695 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + - 1 * q_0 * x";
5.696 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + - 1 * q_0 * x";
5.697 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + - 1 * q_0 * x";
5.698 +case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
5.699 +| _ => error "biegelinie.sml met2 d";
5.700
5.701 - Pre_Conds.discern_feedback_subst id feedb;
5.702 -"~~~~~ fun discern_feedback_subst , args:"; val (id, Cor_TEST ((descr, [ts]), _)) = (id, feedb);
5.703 - (*if*) TermC.is_list ts (*else*);
5.704 - val ts = [ts]
5.705 -;
5.706 - Pre_Conds.discern_type_subst (descr, id) ts;
5.707 -"~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), ts);
5.708 -val _(*"real \<Rightarrow> una"*) =
5.709 - (*case*) type_of descr (*of*);
5.710 -val return_discern_type_subst_1 = [(id, Library.the_single ts)]
5.711 -(*\\\################# nth 1 equal_descr_pairs ############################################=//*)
5.712 -
5.713 -(*///################# nth 4 equal_descr_pairs ############################################=\\*)
5.714 - val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
5.715 - => (discern_feedback_subst id feedb) (*|> map fst (*rhs dropped*)|> map (pair id)*) ) (nth 1 equal_descr_pairs);
5.716 -"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 4 equal_descr_pairs);
5.717 -(*--------------------------------------------------------------------------^^^----------------*)
5.718 -
5.719 - Pre_Conds.discern_feedback_subst id feedb;
5.720 -"~~~~~ fun discern_feedback_subst , args:"; val (id, Cor_TEST ((descr, (*[*)ts(*]*)), _)) = (id, feedb);
5.721 -(*+*)val (Free ("vs", _), "[[c], [c_2], [c_3], [c_4]]")
5.722 - = (id, ts |> UnparseC.terms @{context});
5.723 -
5.724 - (*if*) fold (curry and_) (map TermC.is_list ts) true (*then*);
5.725 - val ts = ts;
5.726 -
5.727 - discern_type_subst (descr, id) ts;
5.728 -"~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), ts);
5.729 -val (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) =
5.730 - (*case*) type_of descr (*of*);
5.731 - (*if*) TermC.is_list (hd ts) (*then*);
5.732 -
5.733 -val return_discern_type_subst_4 =
5.734 -(* if TermC.is_list (hd ts)
5.735 - then*) [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.realT)]
5.736 -(* else []*)
5.737 -(*+*)val "[\"\n(vs, [c, c_2, c_3, c_4])\"]"
5.738 - = return_discern_type_subst_4 |> Subst.to_string @{context}
5.739 -
5.740 -(*-------------------- contine discern_feedback_subst ----------------------------------------*)
5.741 -val return_discern_feedback_subst_4 = return_discern_type_subst_4
5.742 -(*-------------------- contine mk_env_subst_DEL ----------------------------------------------*)
5.743 -val return_mk_env_subst_DEL_4 = return_discern_feedback_subst_4
5.744 -(*+*)val "[\"\n(vs, [c, c_2, c_3, c_4])\"]"
5.745 - = return_mk_env_subst_DEL_4 |> Subst.to_string @{context}
5.746 -(*\\\################# nth 4 equal_descr_pairs ############################################=//*)
5.747 -
5.748 -(*///################# nth 7 equal_descr_pairs ############################################=\\*)
5.749 - val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
5.750 - => (discern_feedback_subst id feedb) (*|> map fst (*rhs dropped*)|> map (pair id)*) ) (nth 7 equal_descr_pairs);
5.751 -"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 7 equal_descr_pairs);
5.752 -(*--------------------------------------------------------------------------^^^----------------*)
5.753 -
5.754 - Pre_Conds.discern_feedback_subst id feedb;
5.755 -"~~~~~ fun discern_feedback_subst , args:"; val (id, Cor_TEST ((descr, (*[*)ts(*]*)), _)) = (id, feedb);
5.756 -(*+*)val (Free ("r_b", _), "[[y 0 = 0], [y L = 0], [M_b 0 = 0], [M_b L = 0]]")
5.757 - = (id, ts |> UnparseC.terms @{context});
5.758 -
5.759 - (*if*) fold (curry and_) (map TermC.is_list ts) true (*then*);
5.760 - val ts = ts;
5.761 -
5.762 - discern_type_subst (descr, id) ts;
5.763 -"~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), ts);
5.764 -val (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) =
5.765 - (*case*) type_of descr (*of*);
5.766 - (*if*) TermC.is_list (hd ts) (*then*);
5.767 -
5.768 -val return_discern_type_subst_7 =
5.769 -(* if TermC.is_list (hd ts)
5.770 - then*) [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.boolT)]
5.771 -(* else []*)
5.772 -(*+*)val "[\"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"
5.773 - = return_discern_type_subst_7 |> Subst.to_string @{context}
5.774 -
5.775 -(*-------------------- contine discern_feedback_subst ----------------------------------------*)
5.776 -val return_discern_feedback_subst_7 = return_discern_type_subst_7
5.777 -(*-------------------- contine mk_env_subst_DEL ----------------------------------------------*)
5.778 -val return_mk_env_subst_DEL_7 = return_discern_type_subst_7
5.779 -(*+*)val "[\"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"
5.780 - = return_mk_env_subst_DEL_7 |> Subst.to_string @{context};
5.781 -(*\\\################# nth 7 equal_descr_pairs ############################################=//*)
5.782 -
5.783 -(*BEFORE correct (vs, [c, c_2, c_3, c_4])* )
5.784 -(*+*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(vs, vs)\", \"\n(id_der, dy)\", \"\n(b_b, y)\"]"
5.785 -(*ERRORs still -----------------------------------------------------------^^^-------------------------------------, r_b*)
5.786 - = (env_subst |> Subst.to_string @{context})
5.787 -*)
5.788 -(*NOW only nth 7 is missing.. (but mk_env_eval_DEL completely broken)* )
5.789 -(*+*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(id_der, dy)\", \"\n(b_b, y)\"]"
5.790 -(*ERRORs still ---------------------------------------------------------------------------------------------------------------------, r_b*)
5.791 - = (env_subst |> Subst.to_string @ {context})
5.792 -*)
5.793 -(*+*)if (env_subst |> Subst.to_string @{context}) = "[\"\n" ^
5.794 -(*1*)"(l_l, L)\", \"\n" ^
5.795 -(*2*)"(q_q, q_0)\", \"\n" ^
5.796 -(*3*)"(fun_var, x)\", \"\n" ^
5.797 -(*4*)"(vs, [c, c_2, c_3, c_4])\", \"\n" ^
5.798 -(*5*)"(id_der, dy)\", \"\n" ^
5.799 -(*6*)"(b_b, y)\", \"\n" ^
5.800 -(*7*)"(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"
5.801 -(*+*)then () else error "env_subst CHANGED";
5.802 -
5.803 -
5.804 -(*+*)if (i_model_max |> I_Model.to_string_TEST @{context}) = "[\n" ^
5.805 - "(1, [1], true ,#Given, (Cor_TEST Traegerlaenge L ,(l_l, [L]), Position.T)), \n" ^
5.806 - "(2, [1], true ,#Given, (Cor_TEST Streckenlast q_0 ,(q_q, [q_0]), Position.T)), \n" ^
5.807 - "(3, [1], true ,#Find, (Cor_TEST Biegelinie y ,(b_b, [y]), Position.T)), \n" ^
5.808 - "(4, [1], true ,#Relate, (Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), Position.T)), \n" ^
5.809 - "(5, [1], true ,#Given, (Cor_TEST FunktionsVariable x ,(fun_var, [x]), Position.T)), \n" ^
5.810 - "(6, [1], true ,#Given, (Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]]), Position.T)), \n" ^
5.811 - "(7, [1], true ,#Given, (Cor_TEST AbleitungBiegelinie dy ,(id_der, [dy]), Position.T))]"
5.812 -(*+*)then () else error "i_model_max CHANGED";
5.813 -
5.814 -(*||------------------ continue of_max_variant ---------------------------------------------\\*)
5.815 -
5.816 - mk_env_eval_DEL i_model_max;
5.817 -(*///----------------- step into mk_env_eval_DEL -------------------------------------------\\*)
5.818 -"~~~~~ fun mk_env_eval_DEL , args:"; val (i_singles) = (i_model_max);
5.819 - val xxx = (fn (_, _, _, _, (feedb, _)) => discern_feedback_subst id feedb);
5.820 -
5.821 -(*///################# nth 1 i_model_max \<longrightarrow>[], <>[] only in maximum-example ##############=\\*)
5.822 -"~~~~~ fun xxx , args:"; val (_, _, _, _, (feedb, _)) = nth 1 i_model_max;
5.823 -(*---------------------------------------------------------^^^------------*)
5.824 -(*+*)val "Cor_TEST Traegerlaenge L ,(l_l, [L])"
5.825 - = feedb |> I_Model.feedback_to_string'_TEST @{context};
5.826 -
5.827 - discern_feedback_subst id feedb;
5.828 -"~~~~~ fun discern_feedback_subst , args:"; val (Model_Def.Cor_TEST ((descr, [ts]), _)) = (feedb);
5.829 - (*if*) TermC.is_list ts (*else*);
5.830 - val ts = (*if TermC.is_list ts then TermC.isalist2list ts else*) [ts];
5.831 -
5.832 - Pre_Conds.discern_type_eval descr ts;
5.833 -"~~~~~ fun discern_type_eval , args:"; val (descr, ts) = (descr, ts);
5.834 -val _(*"real \<Rightarrow> una"*) =
5.835 - (*case*) type_of descr (*of*)
5.836 -;
5.837 - Pre_Conds.discern_atoms ts;
5.838 -"~~~~~ fun discern_atoms , args:"; val (ts) = (ts);
5.839 - (*if*) all_atoms ts (*then*);
5.840 -
5.841 -val return_distinguish_ts_eval_1 =
5.842 - map (rpair TermC.empty (*dummy rhs*)) ts
5.843 -(*-------------------- contine discern_type_subst --------------------------------------------*)
5.844 -(*-------------------- contine discern_feedback_subst ----------------------------------------*)
5.845 -(*-------------------- contine mk_env_eval_DEL -----------------------------------------------*)
5.846 -val return_mk_env_subst_DEL_1
5.847 - = filter_out (fn (_, b) => b = TermC.empty) return_distinguish_ts_eval_1
5.848 -(*+*)val [] = return_mk_env_subst_DEL_1
5.849 -(*\\\################# nth 1 i_model_max \<longrightarrow>[], <>[] only in maximum-example ##############=//*)
5.850 -(*\\\----------------- step into mk_env_eval_DEL -------------------------------------------//*)
5.851 -
5.852 -(*|||----------------- contine of_max_variant ------------------------------------------------*)
5.853 -
5.854 -(* val env_eval = mk_env_eval_DEL i_model_max*)
5.855 - val env_eval = mk_env_eval_DEL i_model_max
5.856 -(*+*)val [] = env_eval
5.857 -val return_of_max_variant_step = (i_model_max, env_model, (env_subst, env_eval))
5.858 -;
5.859 -return_of_max_variant_step = return_of_max_variant
5.860 -( *\\\\\############### old test code ##################################################//////*)
5.861 -\<close> ML \<open>
5.862 -(*\\\----------------- step into of_max_variant --------------------------------------------//*)
5.863 - val (_, env_model, (env_subst, env_eval)) = return_of_max_variant
5.864 -
5.865 -(*|------------------- contine init_pstate ---------------------------------------------------*)
5.866 - val actuals = map snd env_model
5.867 -(*+* )val "[L, q_0, x, [c, c_2, c_3, c_4], dy, y, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]"
5.868 - = actuals |> UnparseC.terms @{context}(**)
5.869 -(*+*)val 7 = length actuals( **)
5.870 -(*WRONG ----------------v-v--v---v--v---v--v---v-----------v-------v--v-------v--v---------v--v---------v*)
5.871 -(*+*) val "[L, q_0, x, [[c], [c_2], [c_3], [c_4]], dy, y, [[y 0 = 0], [y L = 0], [M_b 0 = 0], [M_b L = 0]]]"
5.872 - = actuals |> UnparseC.terms @{context}
5.873 -\<close> ML \<open>
5.874 - val formals = Program.formal_args prog
5.875 -(*+*)val "[l_l, q_q, fun_var, b_b, r_b, vs, id_der]"
5.876 - = formals |> UnparseC.terms @{context}
5.877 -(*+*)val 7 = length formals
5.878 -
5.879 -\<close> ML \<open>
5.880 - val preconds = Pre_Conds.check_from_store ctxt where_rls where_ env_subst env_eval
5.881 -\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
5.882 - val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
5.883 - val ist = Istate.e_pstate
5.884 - |> Istate.set_eval prog_rls
5.885 - |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals)
5.886 -\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
5.887 -(*+*)(relate_args [] formals actuals ctxt prog met_id formals actuals)
5.888 -\<close> text \<open>
5.889 -val return_init_pstate = (Istate.Pstate ist, ctxt, program)
5.890 -\<close> ML \<open>(*\\------------ step into init_pstate -----------------------------------------------//*)
5.891 -(*\\------------------ step into init_pstate -----------------------------------------------//*)
5.892 -\<close> ML \<open>(*\------------- step into me_Add_Given_AbleitungBieg --------------------------------//*)
5.893 -(*\------------------- step into me_Add_Given_AbleitungBieg --------------------------------//*)
5.894 -\<close> text \<open> (*\------------ step into me_Add_Given_AbleitungBieg --------------------------------//*)
5.895 -val (p,_,f,nxt,_,pt) = return_Add_Given_AbleitungBieg;
5.896 - val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
5.897 -
5.898 -\<close> text \<open>
5.899 -(* final test ... ----------------------------------------------------------------------------*)
5.900 -(*+*)val ([], Met) = p
5.901 -(*+*)val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
5.902 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.903 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.904 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.905 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.906 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
5.907 + "M_b x = Integral c + - 1 * q_0 * x D x";
5.908 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
5.909 + "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";
5.910 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
5.911 + "M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";
5.912 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
5.913 + "- EI * y'' x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2";
5.914 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
5.915 + "y'' x = 1 / - EI * (c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2)";
5.916 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.917 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.918 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.919 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.920 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
5.921 + "y' x = Integral 1 / - EI * (c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2) D x";
5.922 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
5.923 +"y' x = Integral 1 / (- 1 * EI) * (c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2) D x";
5.924 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
5.925 +"y' x =\nc_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)";
5.926 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
5.927 +"y' x =\nc_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)";
5.928 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.929 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.930 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.931 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.932 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
5.933 +"y x =\nIntegral c_3 +\n 1 / (- 1 * EI) *\n (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3) D x";
5.934 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
5.935 +"y x =\nc_4 + c_3 * x +\n1 / (- 1 * EI) *\n(c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)";
5.936 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
5.937 + "y x =\nc_4 + c_3 * x +\n1 / (- 1 * EI) *\n(c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)";
5.938 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.939 +if f2str f =
5.940 + "[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n dy x =\n c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]"
5.941 +then case nxt of ("End_Proof'", End_Proof') => ()
5.942 + | _ => error "biegelinie.sml met2 e 1"
5.943 +else error "biegelinie.sml met2 e 2";
5.944 +=============================================================================================//*)
5.945
5.946 \<close> ML \<open>
5.947 \<close>
5.948 @@ -544,7 +649,7 @@
5.949 section \<open>===== ============================================================================\<close>
5.950 ML \<open>
5.951 \<close> ML \<open>
5.952 -\<close> ML \<open>
5.953 +
5.954 \<close> ML \<open>
5.955 \<close>
5.956