1.1 --- a/TODO.md Sun Nov 19 07:51:41 2023 +0100
1.2 +++ b/TODO.md Mon Nov 20 10:49:54 2023 +0100
1.3 @@ -53,6 +53,7 @@
1.4 ***** priority of WN items is top down, most urgent/simple on top
1.5
1.6 * WN:
1.7 +* WN: rename pat2str --> single_to_string
1.8 * WN: emergency-CS "prepare 14: improved item_to_add"
1.9 * no code cleanup
1.10 * ERROR in test/../biegelinie-3.sml outcommented
1.11 @@ -63,24 +64,16 @@
1.12 locate SOMEWHERE BEFORE Model_Def (+ needed in Model_Pattern ??!?)
1.13 <-?-> Input_Descript.thy
1.14 * WN: thy --> ctxt in by_Add_, ? I_Model.T_TEST ?
1.15 + try to do the same in as many functions as possible
1.16 * WN: use fn in add_single
1.17 -* WN: rename pat2str --> single_to_string
1.18 -* WN: introduce typedecl toreallNOpar, toboollNOpar
1.19 +* WN: comment design of list-elements in values
1.20 and remove HACK: before introduction typedecl toreallNOpar, toboollNOpar
1.21 * WN: reconsider design max_variants/_TEST
1.22 -* WN: (*/---with M_Model.match_itms_oris broken elementwise input to lists---\*)
1.23 - (*\---with M_Model.match_itms_oris broken elementwise input to lists---/*)
1.24 - several tests marked in Test_Isac.thy, which have out-comments.
1.25 - * repair them together with all <broken elementwise input to lists>
1.26 - * repair together with O_Model.to_string "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"])"
1.27 +* WN: simplify "" in O_Model.to_string "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"])"
1.28 * WN: review PblObh {meth, ...}
1.29 * fill early (Model_Problem?) with Inc [] presents input-templates
1.30 * try to minimise user's contact with Method:
1.31 * M_Model.match_itms_oris can probably be replaced by i_Model.s_make_complete and Pre_Conds.check(?_*)
1.32 -* WN: uncomment: I_Model.check_internal (*filter (fn (_, _, _, m_field ,_) ..*)
1.33 - after I_Model.s_make_complete does NOT create m_field #undef, "i_model_empty";
1.34 - see test/../i-model.sml --- setup test data for I_Model.s_make_complete ---
1.35 -* WN: ---broken elementwise input to lists---
1.36 * WN: undetected ERROR in autoCalculate --- due to Post_Conds.check? (_OLD .. dispels ?)
1.37 * WN: "review (descriptor, ts)"; ts : term list, because this supports element-wise input of lists.
1.38 ts = [_] is determined by <Pre_Conds.is_list_descr descriptor>.
2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Sun Nov 19 07:51:41 2023 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Mon Nov 20 10:49:54 2023 +0100
2.3 @@ -104,6 +104,7 @@
2.4 val string_of_detail: Proof.context -> term -> string
2.5 (*from isac_test for Minisubpbl*)
2.6 val atom_typ: Proof.context -> typ -> unit
2.7 + val atom_trace_detail: Proof.context -> term -> unit
2.8
2.9 \<^isac_test>\<open>
2.10 val mk_negative: typ -> term -> term
2.11 @@ -114,7 +115,7 @@
2.12 val atom_trace: Proof.context -> term -> unit
2.13
2.14 val atom_write_detail: Proof.context -> term -> unit
2.15 - val atom_trace_detail: Proof.context -> term -> unit
2.16 +(*val atom_trace_detail: Proof.context -> term -> unit*)
2.17 \<close>
2.18 end
2.19
2.20 @@ -221,8 +222,8 @@
2.21 end;
2.22
2.23 fun atom_write_detail ctxt t = (writeln o (string_of_detail ctxt)) t;
2.24 +\<close>
2.25 fun atom_trace_detail ctxt t = (tracing o (string_of_detail ctxt)) t;
2.26 -\<close>
2.27
2.28 (* contains the term a VAR(("*",_),_) ? *)
2.29 fun contains_Var (Abs(_,_,body)) = contains_Var body
3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Sun Nov 19 07:51:41 2023 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Mon Nov 20 10:49:54 2023 +0100
3.3 @@ -295,7 +295,7 @@
3.4
3.5 Problem ["LINEAR", "system"]
3.6 MethodC ["no_met"]
3.7 - ^^^^^^--- thus automatied refinement to appropriate Problem
3.8 + ^^^^^^--- thus automatic refinement to appropriate type of equational system
3.9 \<close>
3.10
3.11 subsection \<open>Compute the general bending line\<close>
4.1 --- a/test/Tools/isac/Specify/sub-problem.sml Sun Nov 19 07:51:41 2023 +0100
4.2 +++ b/test/Tools/isac/Specify/sub-problem.sml Mon Nov 20 10:49:54 2023 +0100
4.3 @@ -13,6 +13,9 @@
4.4 "-----------------------------------------------------------------------------------------------";
4.5 "-----------------------------------------------------------------------------------------------";
4.6
4.7 +open Tactic
4.8 +open Pos
4.9 +open Test_Code;
4.10
4.11 "----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";
4.12 "----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";
4.13 @@ -41,13 +44,10 @@
4.14 ],
4.15 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
4.16
4.17 - val (tac as Model_Problem (*["vonBelastungZu", "Biegelinien"]*), (pt, p as ([1], Pbl))) =
4.18 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
4.19 - (*---broken elementwise input to lists---* ) |> me'( *---broken elementwise input to lists---*)
4.20 - (*INVISIBLE: SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
4.21 - |> me'
4.22 - (*with new formal arguments..*) |> me' |> me';
4.23 -
4.24 +val (tac as Model_Problem (*["vonBelastungZu", "Biegelinien"]*), (pt, p as ([1], Pbl))) =
4.25 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
4.26 + |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
4.27 +;
4.28
4.29 "----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";
4.30 "----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";
4.31 @@ -66,17 +66,14 @@
4.32 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
4.33
4.34 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, refs)];
4.35 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Model_Problem*)
4.36 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "Traegerlaenge L"*)
4.37 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "Streckenlast q_0"*)
4.38 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac
4.39 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "Traegerlaenge L" = tac
4.40 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "Streckenlast q_0" = tac
4.41 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Find "Biegelinie y" = tac
4.42 -
4.43 -(*/---broken elementwise input to lists---\* )
4.44 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Relation "Randbedingungen [y 0 = 0]" = tac
4.45 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]" = tac
4.46 -( *\---broken elementwise input to lists---/*)
4.47 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = tac
4.48 -
4.49 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Relation "Randbedingungen [y 0 = 0, y L = 0]" = tac
4.50 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0]" = tac
4.51 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Relation "Randbedingungen [y L = 0, y 0 = 0, M_b 0 = 0, M_b L = 0]" = tac
4.52 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Theory "Biegelinie" = tac
4.53 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Problem ["Biegelinien"] = tac
4.54 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac
4.55 @@ -84,7 +81,12 @@
4.56 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "AbleitungBiegelinie dy" = tac
4.57 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "Biegemoment M_b" = tac
4.58 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "Querkraft Q" = tac
4.59 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = tac
4.60 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "GleichungsVariablen [c]" = tac
4.61 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "GleichungsVariablen [c, c_2]" = tac
4.62 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "GleichungsVariablen [c, c_2, c_3]" = tac
4.63 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "GleichungsVariablen [c_2, c, c_3, c_4]" = tac
4.64 +
4.65 +val Add_Given "GleichungsVariablen [c_2, c, c_3, c_4]" = tac
4.66 (*[1], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = tac
4.67 (*INVISIBLE: \<rightarrow>SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
4.68 (*[1], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac
5.1 --- a/test/Tools/isac/Test_Isac.thy Sun Nov 19 07:51:41 2023 +0100
5.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Nov 20 10:49:54 2023 +0100
5.3 @@ -276,8 +276,8 @@
5.4 ML_file "Specify/specification.sml"
5.5 ML_file "Specify/cas-command.sml"
5.6 ML_file "Specify/p-spec.sml"
5.7 -(*ML_file "Specify/specify.sml ---with M_Model.match_itms_oris broken elementwise input to lists---*)
5.8 -(*ML_file "Specify/sub-problem.sml" biegel, |> me' with M_Model.match_itms_oris broken*)
5.9 +(*ML_file "Specify/specify.sml" ---with M_Model.match_itms_oris broken elementwise input to lists*)
5.10 + ML_file "Specify/sub-problem.sml"
5.11 ML_file "Specify/step-specify.sml"
5.12
5.13 ML_file "Interpret/istate.sml"
5.14 @@ -384,7 +384,7 @@
5.15 ^^^ BEFORE fun Calc_Binop.simplify IS EVALUATEDO BY Simplifier.rewrite *)
5.16 then () else error "auto method [Biegelinien,setzeRandbedingungenEin] changed";
5.17
5.18 -
5.19 +
5.20 "----------- SubProblem: me method [Biegelinien,setzeRandbedingungenEin]----------------------";
5.21 "----------- SubProblem: me method [Biegelinien,setzeRandbedingungenEin]----------------------";
5.22 "----------- SubProblem: me method [Biegelinien,setzeRandbedingungenEin]----------------------";
6.1 --- a/test/Tools/isac/Test_Theory.thy Sun Nov 19 07:51:41 2023 +0100
6.2 +++ b/test/Tools/isac/Test_Theory.thy Mon Nov 20 10:49:54 2023 +0100
6.3 @@ -101,11 +101,2440 @@
6.4 \<close> ML \<open>
6.5 \<close>
6.6
6.7 -(** )ML_file "Minisubpbl/100a-init-rootpbl-Maximum.sml"( **)
6.8 +(** )ML_file "Knowledge/eqsystem-1.sml"( **)
6.9 section \<open>===================================================================================\<close>
6.10 -section \<open>===== ============================================================================\<close>
6.11 +section \<open>===== Knowledge/eqsystem-1.sml ====================================================\<close>
6.12 +section \<open>===== (*ERROR type_of: type mismatch in application * real * real list (#) [c]*) ==\<close>
6.13 ML \<open>
6.14 +(* Title: Knowledge/eqsystem-1.sml
6.15 + author: Walther Neuper 050826,
6.16 + (c) due to copyright terms
6.17 +*)
6.18 +
6.19 +"-----------------------------------------------------------------------------------------------";
6.20 +"table of contents -----------------------------------------------------------------------------";
6.21 +"-----------------------------------------------------------------------------------------------";
6.22 +"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
6.23 +"----------- problems -----------------------------------------------------------equsystem-1.sml";
6.24 +"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
6.25 +"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
6.26 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
6.27 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
6.28 +"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
6.29 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
6.30 +"----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
6.31 +"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
6.32 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
6.33 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
6.34 +"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
6.35 +"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
6.36 +"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
6.37 +"-----------------------------------------------------------------------------------------------";
6.38 +"-----------------------------------------------------------------------------------------------";
6.39 +"-----------------------------------------------------------------------------------------------";
6.40 +
6.41 +val thy = @{theory "EqSystem"};
6.42 +val ctxt = Proof_Context.init_global thy;
6.43 +
6.44 +open Kernel
6.45 +open Tactic
6.46 +open Test_Code
6.47 +open Pos
6.48 +open P_Model
6.49 +open Rewrite;
6.50 +open Prog_Expr;
6.51 +
6.52 +"----------- occur_exactly_in ------------------------------------";
6.53 +"----------- occur_exactly_in ------------------------------------";
6.54 +"----------- occur_exactly_in ------------------------------------";
6.55 +val all = [ParseC.parse_test @{context}"c", ParseC.parse_test @{context}"c_2", ParseC.parse_test @{context}"c_3"];
6.56 +val t = ParseC.parse_test @{context}"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
6.57 +
6.58 +if occur_exactly_in [ParseC.parse_test @{context}"c", ParseC.parse_test @{context}"c_2"] all t
6.59 +then () else error "eqsystem.sml occur_exactly_in 1";
6.60 +
6.61 +if not (occur_exactly_in [ParseC.parse_test @{context}"c", ParseC.parse_test @{context}"c_2", ParseC.parse_test @{context}"c_3"] all t)
6.62 +then () else error "eqsystem.sml occur_exactly_in 2";
6.63 +
6.64 +if not (occur_exactly_in [ParseC.parse_test @{context}"c_2"] all t)
6.65 +then () else error "eqsystem.sml occur_exactly_in 3";
6.66 +
6.67 +val t = ParseC.parse_test @{context}"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
6.68 +eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
6.69 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
6.70 +if str = "[c, c_2] from [c, c_2,\n" ^
6.71 + " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
6.72 +then () else error "eval_occur_exactly_in [c, c_2]";
6.73 +
6.74 +val t = ParseC.parse_test @{context} ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
6.75 + "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
6.76 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
6.77 +if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
6.78 +" c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
6.79 +then () else error "eval_occur_exactly_in [c, c_2, c_3]";
6.80 +
6.81 +val t = ParseC.parse_test @{context}"[c_2] from [c,c_2,c_3] occur_exactly_in \
6.82 + \- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
6.83 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
6.84 +if str = "[c_2] from [c, c_2,\n" ^
6.85 + " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
6.86 +then () else error "eval_occur_exactly_in [c, c_2, c_3]";
6.87 +
6.88 +val t = ParseC.parse_test @{context}"[] from [c,c_2,c_3] occur_exactly_in 0";
6.89 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
6.90 +if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
6.91 +else error "eval_occur_exactly_in [c, c_2, c_3]";
6.92 +
6.93 +val t =
6.94 + ParseC.parse_test @{context}
6.95 + "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
6.96 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
6.97 +if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
6.98 + \- 1 * (q_0 * L \<up> 2) / 2 = True" then ()
6.99 +else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
6.100 +
6.101 +
6.102 +"----------- problems --------------------------------------------";
6.103 +"----------- problems --------------------------------------------";
6.104 +"----------- problems --------------------------------------------";
6.105 +val t = ParseC.parse_test @{context} "Length [x+y=1,y=2] = 2";
6.106 +val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
6.107 + [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
6.108 + (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
6.109 + Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
6.110 + Eval (\<^const_name>\<open>HOL.eq\<close>, eval_equal "#equal_")
6.111 + ];
6.112 +val SOME (t',_) = rewrite_set_ ctxt false testrls t;
6.113 +if UnparseC.term @{context} t' = "True" then ()
6.114 +else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
6.115 +
6.116 +val SOME t = ParseC.term_opt ctxt "solution LL";
6.117 +TermC.atom_trace_detail @{context} t;
6.118 +val SOME t = ParseC.term_opt ctxt "solution LL";
6.119 +TermC.atom_trace_detail @{context} t;
6.120 +
6.121 +val t = ParseC.parse_test @{context}
6.122 +"(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
6.123 +TermC.atom_trace_detail @{context} t;
6.124 +val t = ParseC.parse_test @{context} ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
6.125 + "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
6.126 +(*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
6.127 + assume flawed test setup hidden by "handle _ => ..."
6.128 + ERROR rewrite__set_ called with 'Erls' for '1 < 1'
6.129 +val SOME (t,_) =
6.130 + rewrite_set_ ctxt true
6.131 + (Rule_Set.append_rules "prls_" Rule_Set.empty
6.132 + [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
6.133 + Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
6.134 + Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),
6.135 + Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),
6.136 + Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
6.137 + ]) t;
6.138 +if t = @{term True} then ()
6.139 +else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
6.140 + broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)
6.141 +
6.142 +
6.143 +"----------- rewrite-order ord_simplify_System -------------------";
6.144 +"----------- rewrite-order ord_simplify_System -------------------";
6.145 +"----------- rewrite-order ord_simplify_System -------------------";
6.146 +"M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
6.147 +"--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
6.148 +if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
6.149 + ParseC.parse_test @{context}"c * x") then ()
6.150 +else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
6.151 +
6.152 +if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
6.153 + ParseC.parse_test @{context}"c_2") then ()
6.154 +else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
6.155 +
6.156 +if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"c * x",
6.157 + ParseC.parse_test @{context}"c_2") then ()
6.158 +else error "integrate.sml, (c * x) < (c_2) not#3";
6.159 +
6.160 +"--- mult.commute ---";
6.161 +if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"x * c",
6.162 + ParseC.parse_test @{context}"c * x") then ()
6.163 +else error "integrate.sml, (x * c) < (c * x) not#4";
6.164 +
6.165 +if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
6.166 + ParseC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)")
6.167 +then () else error "integrate.sml, (. * .) < (. * .) not#5";
6.168 +
6.169 +if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
6.170 + ParseC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)")
6.171 +then () else error "integrate.sml, (. * .) < (. * .) not#6";
6.172 +
6.173 +
6.174 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
6.175 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
6.176 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
6.177 +val t = ParseC.parse_test @{context}"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
6.178 + \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
6.179 +val bdvs = [(ParseC.parse_test @{context}"bdv_1",ParseC.parse_test @{context}"c"),
6.180 + (ParseC.parse_test @{context}"bdv_2",ParseC.parse_test @{context}"c_2")];
6.181 +val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
6.182 +if UnparseC.term @{context} t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
6.183 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
6.184 +
6.185 +val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
6.186 +if UnparseC.term @{context} t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"
6.187 +then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
6.188 +
6.189 +val SOME (t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
6.190 +if UnparseC.term @{context} t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
6.191 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
6.192 +
6.193 +"--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";
6.194 +val SOME (t,_) = rewrite_set_ ctxt true order_system t;
6.195 +if UnparseC.term @{context} t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
6.196 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
6.197 +
6.198 +
6.199 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
6.200 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
6.201 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
6.202 +val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
6.203 +val ctxt = Proof_Context.init_global thy;
6.204 +val t =
6.205 + ParseC.parse_test @{context}"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
6.206 + \ - 1 * q_0 / 24 * 0 \<up> 4),\
6.207 + \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
6.208 + \ - 1 * q_0 / 24 * L \<up> 4)]";
6.209 +val SOME (t, _) = rewrite_set_ ctxt true norm_Rational t;
6.210 +if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
6.211 + "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
6.212 + "[0 = c_2, 0 = (24 * c_2 + 24 * L * c + L \<up> 4 * q_0) / 24]"
6.213 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
6.214 +
6.215 +val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
6.216 +if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
6.217 + "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
6.218 + "[0 = c_2, 0 = q_0 * L \<up> 4 / 24 + (L * c + c_2)]"
6.219 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
6.220 +
6.221 +val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
6.222 +if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
6.223 + "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)
6.224 + "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / 24)]"
6.225 +then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
6.226 +
6.227 +val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
6.228 +if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
6.229 + "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
6.230 + "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
6.231 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
6.232 +
6.233 +val xxx = rewrite_set_ ctxt true order_system t;
6.234 +if is_none xxx
6.235 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
6.236 +
6.237 +
6.238 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
6.239 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
6.240 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
6.241 +val e1__ = ParseC.parse_test @{context} "c_2 = 77";
6.242 +val e2__ = ParseC.parse_test @{context} "L * c + c_2 = q_0 * L \<up> 2 / 2";
6.243 +val bdvs = [(ParseC.parse_test @{context}"bdv_1",ParseC.parse_test @{context}"c"),
6.244 + (ParseC.parse_test @{context}"bdv_2",ParseC.parse_test @{context}"c_2")];
6.245 +val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;
6.246 +if UnparseC.term @{context} e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
6.247 +else error "eqsystem.sml top_down_substitution,2x2] subst";
6.248 +
6.249 +val SOME (e2__,_) =
6.250 + rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized e2__;
6.251 +if UnparseC.term @{context} e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()
6.252 +else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
6.253 +
6.254 +val SOME (e2__,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs e2__;
6.255 +if UnparseC.term @{context} e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
6.256 +else error "eqsystem.sml top_down_substitution,2x2] isolate";
6.257 +
6.258 +val t = ParseC.parse_test @{context} "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
6.259 +val SOME (t,_) = rewrite_set_ ctxt true order_system t;
6.260 +if UnparseC.term @{context} t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
6.261 +else error "eqsystem.sml top_down_substitution,2x2] order_system";
6.262 +
6.263 +if not (ord_simplify_System
6.264 + false ctxt []
6.265 + (ParseC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
6.266 + ParseC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
6.267 +then () else error "eqsystem.sml, order_result rew_ord";
6.268 +
6.269 +
6.270 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
6.271 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
6.272 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
6.273 +(*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
6.274 +val t = ParseC.parse_test @{context} (
6.275 + "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^
6.276 + "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^
6.277 + "c + c_2 + c_3 + c_4 = 0, " ^
6.278 + "c_2 + c_3 + c_4 = 0]");
6.279 +val bdvs = [(ParseC.parse_test @{context}"bdv_1::real",ParseC.parse_test @{context}"c::real"),
6.280 + (ParseC.parse_test @{context}"bdv_2::real",ParseC.parse_test @{context}"c_2::real"),
6.281 + (ParseC.parse_test @{context}"bdv_3::real",ParseC.parse_test @{context}"c_3::real"),
6.282 + (ParseC.parse_test @{context}"bdv_4::real",ParseC.parse_test @{context}"c_4::real")];
6.283 +val SOME (t, _) =
6.284 + rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
6.285 +if UnparseC.term @{context} t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
6.286 +then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
6.287 +
6.288 +val SOME (t, _) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
6.289 +if UnparseC.term @{context} t = "[c_4 = 0, \
6.290 + \L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \
6.291 + \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
6.292 +then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
6.293 +
6.294 +val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
6.295 +if UnparseC.term @{context} t = "[c_4 = 0,\
6.296 + \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
6.297 + \ c + (c_2 + (c_3 + c_4)) = 0,\n\
6.298 + \ c_2 + (c_3 + c_4) = 0]"
6.299 +then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
6.300 +
6.301 +val SOME (t, _) = rewrite_set_ ctxt true order_system t;
6.302 +if UnparseC.term @{context} t = "[c_4 = 0,\
6.303 + \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
6.304 + \ c_2 + (c_3 + c_4) = 0,\n\
6.305 + \ c + (c_2 + (c_3 + c_4)) = 0]"
6.306 +then () else error "eqsystem.sml rewrite in 4x4 order_system";
6.307 +
6.308 +
6.309 +"----------- refine [linear,system]-------------------------------";
6.310 +"----------- refine [linear,system]-------------------------------";
6.311 +"----------- refine [linear,system]-------------------------------";
6.312 +val fmz =
6.313 + ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
6.314 + "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]",
6.315 + "solveForVars [c, c_2]", "solution LL"];
6.316 +
6.317 +(*WN120313 in "solution L" above "Refine.by_formalise @{context} fmz ["LINEAR", "system"]" caused an error...*)
6.318 +"~~~~~ fun Refine.refine , args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
6.319 +"~~~~~ fun check_match' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
6.320 + ((rev o tl) pblID, fmz, [(*match list*)],
6.321 + ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
6.322 + val {thy, model, where_, where_rls, ...} = py ;
6.323 +"~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, model);
6.324 + val (ts, ctxt) = ContextC.init_while_parsing fmz thy;
6.325 +"~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
6.326 + fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
6.327 + (_, _::_) => (Free (v,T)::get_vars vs)
6.328 + | (_, [] ) => get_vars vs) (*filter out nums as long as
6.329 + we have Free ("123",_)*)
6.330 + | get_vars [] = [];
6.331 + t = "equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^
6.332 + "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";
6.333 + val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
6.334 +val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
6.335 +val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;
6.336 +val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;
6.337 +val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;
6.338 + val t = nth 2 fmz; t = "solveForVars [c, c_2]";
6.339 + val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
6.340 +val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
6.341 + val t = nth 3 fmz; t = "solution LL";
6.342 + (*(Syntax.read_term ctxt t);
6.343 +Type unification failed: Clash of types "real" and "_ list"
6.344 +Type error in application: incompatible operand type
6.345 +
6.346 +Operator: solution :: bool list \<Rightarrow> toreall
6.347 +Operand: L :: real ========== L was already present in equalities ========== *)
6.348 +
6.349 +"===== case 1 =====";
6.350 +val matches = Refine.by_formalise @{context} fmz ["LINEAR", "system"];
6.351 +case matches of
6.352 + [M_Match.Matches (["LINEAR", "system"], _), (*Matches*)
6.353 + M_Match.Matches (["2x2", "LINEAR", "system"], _), (*NoMatch !--> continue search !*)
6.354 + M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _), (**)
6.355 + M_Match.Matches (["normalise", "2x2", "LINEAR", "system"], (**)
6.356 + {Find = [Correct "solution LL"], With = [], (**)
6.357 + Given = [Correct "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
6.358 + Correct "solveForVars [c, c_2]"],
6.359 + Where = [],
6.360 + Relate = []})] => ()
6.361 +| _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";
6.362 +
6.363 +"===== case 2 =====";
6.364 +val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
6.365 + "solveForVars [c, c_2]", "solution LL"];
6.366 +val matches = Refine.by_formalise @{context} fmz ["LINEAR", "system"];
6.367 +case matches of [_,_,
6.368 + M_Match.Matches
6.369 + (["triangular", "2x2", "LINEAR", "system"],
6.370 + {Find = [Correct "solution LL"],
6.371 + With = [],
6.372 + Given =
6.373 + [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
6.374 + Correct "solveForVars [c, c_2]"],
6.375 + Where = [Correct
6.376 + "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
6.377 + Correct
6.378 + "[c, c_2] from [c, c_2] occur_exactly_in NTH 2\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"],
6.379 + Relate = []})] => ()
6.380 +| _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
6.381 +
6.382 +(*WN051014-----------------------------------------------------------------------------------\\
6.383 + the above 'val matches = Refine.by_formalise @{context} fmz ["LINEAR", "system"]'
6.384 + didn't work anymore; we investigated in these steps:*)
6.385 +val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
6.386 + "solveForVars [c, c_2]", "solution LL"];
6.387 +val matches = Refine.by_formalise @{context} fmz ["triangular", "2x2", "LINEAR", "system"];
6.388 +(*... resulted in
6.389 + False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
6.390 + [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
6.391 +val t = ParseC.parse_test @{context} ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
6.392 + "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
6.393 +
6.394 +val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;
6.395 +(*found:...
6.396 +## try thm: NTH_CONS
6.397 +### eval asms: 1 < 2 + - 1
6.398 +==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =
6.399 + nth_ (2 + - 1 + - 1) []
6.400 +#### rls: erls_prls_triangular on: 1 < 2 + - 1
6.401 +##### try calc: op <'
6.402 +### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + - 1"]
6.403 +
6.404 +... i.e Eval ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") was missing in erls_prls_triangular*)
6.405 +(*--------------------------------------------------------------------------------------------//*)
6.406 +
6.407 +
6.408 +"===== case 3: relaxed preconditions for triangular system =====";
6.409 +val fmz = ["equalities [L * q_0 = c, \
6.410 + \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
6.411 + \ 0 = c_4, \
6.412 + \ 0 = c_3]",
6.413 + "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
6.414 +(*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:
6.415 +probably exn thrown by fun declare_constraints
6.416 +/-------------------------------------------------------\
6.417 +Type unification failed
6.418 +Type error in application: incompatible operand type
6.419 +
6.420 +Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
6.421 +Operand: [c_4] :: 'b list
6.422 +\-------------------------------------------------------/
6.423 +val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
6.424 +case TermC.matches of
6.425 + [M_Match.Matches (["LINEAR", "system"], _),
6.426 + M_Match.NoMatch (["2x2", "LINEAR", "system"], _),
6.427 + M_Match.NoMatch (["3x3", "LINEAR", "system"], _),
6.428 + M_Match.Matches (["4x4", "LINEAR", "system"], _),
6.429 + M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
6.430 + M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
6.431 + | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
6.432 +(*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
6.433 +
6.434 +"===== case 4 =====";
6.435 +val fmz = ["equalities [L * q_0 = c, \
6.436 + \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
6.437 + \ 0 = c_3, \
6.438 + \ 0 = c_4]",
6.439 + "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
6.440 +val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];
6.441 +case TermC.matches of
6.442 + [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
6.443 + | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
6.444 +val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
6.445 +============ inhibit exn WN120314 ==============================================*)
6.446 +
6.447 +
6.448 +"----------- Refine.refine [2x2,linear,system] search error--------------";
6.449 +"----------- Refine.refine [2x2,linear,system] search error--------------";
6.450 +"----------- Refine.refine [2x2,linear,system] search error--------------";
6.451 +(*didn't go into ["2x2", "LINEAR", "system"];
6.452 + we investigated in these steps:*)
6.453 +val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
6.454 + \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
6.455 + "solveForVars [c, c_2]", "solution LL"];
6.456 +val matches = Refine.by_formalise @{context} fmz ["2x2", "LINEAR", "system"];
6.457 +(*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
6.458 +(*brought: 'False "length_ es_ = 2"'*)
6.459 +
6.460 +(*-----fun check_match' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
6.461 +(* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
6.462 + (rev ["LINEAR", "system"], fmz, [(*match list*)],
6.463 + ((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));
6.464 + *)
6.465 +> show_types:=true; UnparseC.term @{context} (hd where_); show_types:=false;
6.466 +val it = "length_ (es_::real list) = (2::real)" : string
6.467 +
6.468 +=========================================================================\
6.469 +-------fun Problem.prep_input
6.470 +(* val (thy, (pblID, dsc_dats: (string * (string list)) list,
6.471 + ev:rls, ca: string option, metIDs:metID list)) =
6.472 + (EqSystem.thy, (["system"],
6.473 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
6.474 + ("#Find" ,["solution ss___"](*___ is copy-named*))
6.475 + ],
6.476 + Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
6.477 + SOME "solveSystem es_ v_s",
6.478 + []));
6.479 + *)
6.480 +> val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
6.481 +val equalities_es_ = "equalities es_" : string
6.482 +> val (dd, ii) = ((Model_Pattern.split_descriptor ctxt) o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
6.483 +> show_types:=true; UnparseC.term @{context} ii; show_types:=false;
6.484 +val it = "es_::bool list" : string
6.485 +~~~~~~~~~~~~~~~ \<up> \<up> \<up> OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
6.486 +
6.487 +> val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];
6.488 +> show_types:=true; UnparseC.term @{context} (hd where_); show_types:=false;
6.489 +
6.490 +=========================================================================/
6.491 +
6.492 +-----fun check_match' ff:
6.493 +> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
6.494 +[
6.495 +(1 ,[1] ,true ,#Given ,Cor equalities
6.496 + [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
6.497 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2] ,(es_, [[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
6.498 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),
6.499 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
6.500 +(3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
6.501 +
6.502 +> (writeln o pres2str) pre';
6.503 +[
6.504 +(false, length_ es_ = 2),
6.505 +(true, length_ [c, c_2] = 2)]
6.506 +
6.507 +----- fun match_oris':
6.508 +> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
6.509 +> (writeln o pres2str) pre';
6.510 +..as in check_match'
6.511 +
6.512 +----- fun check in Pre_Conds.
6.513 +> (writeln o env2str) env;
6.514 +["
6.515 +(es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
6.516 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "
6.517 +(v_s, [c, c_2])", "
6.518 +(ss___, L)"]
6.519 +
6.520 +> val es_ = (fst o hd) env;
6.521 +val es_ = Free ("es_", "bool List.list") : Term.term
6.522 +
6.523 +> val pre1 = hd pres;
6.524 +TermC.atom_trace_detail @{context} pre1;
6.525 +***
6.526 +*** Const (op =, [real, real] => bool)
6.527 +*** . Const (ListG.length_, real list => real)
6.528 +*** . . Free (es_, real list)
6.529 +~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up> should be bool list~~~~~~~~~~~~~~~~~~~
6.530 +*** . Free (2, real)
6.531 +***
6.532 +
6.533 +THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
6.534 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
6.535 +*)
6.536 +
6.537 +
6.538 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
6.539 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
6.540 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
6.541 +(*this test fails, see TODO WN230404*)
6.542 +val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
6.543 + "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
6.544 + "solveForVars [c, c_2]", "solution LL"];
6.545 +val (dI',pI',mI') =
6.546 + ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
6.547 + ["EqSystem", "normalise", "2x2"]);
6.548 +val p = e_pos'; val c = [];
6.549 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
6.550 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.551 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.552 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.553 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.554 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["EqSystem", "normalise", "2x2"] = nxt
6.555 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.556 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.557 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.558 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.559 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.560 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.561 +case nxt of
6.562 + (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
6.563 + | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
6.564 +
6.565 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
6.566 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities [c_2 = 0]" = nxt
6.567 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = nxt
6.568 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c]" = nxt
6.569 +\<close> ML \<open>(*ERROR type_of: type mismatch in application * real * real list (#) [c]*)
6.570 +(*//################## @ {context} within fun XXXXX ---------------------------------------\\* )
6.571 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.572 +
6.573 +val xxx = nxt
6.574 +
6.575 +val Add_Given "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = nxt;
6.576 +
6.577 +(*ERROR WN230404: mk_env not reasonable for "Cor_TEST equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(e_s, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])"*)
6.578 +(** )val return_Add_Given_equ
6.579 + = me nxt p c pt;( **)
6.580 +(*//------------------ step into Add_Given_equ ---------------------------------------------\\*);
6.581 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
6.582 + val ctxt = Ctree.get_ctxt pt p
6.583 +val ("ok", (_, _, (pt, p))) =
6.584 + (*case*) Step.by_tactic tac (pt, p) (*of*);
6.585 +
6.586 +(** ) (*case*)
6.587 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);( **)
6.588 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
6.589 + (p, ((pt, Pos.e_pos'), []));
6.590 + (*if*) Pos.on_calc_end ip (*else*);
6.591 + val (_, probl_id, _) = Calc.references (pt, p);
6.592 +val _ =
6.593 + (*case*) tacis (*of*);
6.594 + (*if*) probl_id = Problem.id_empty (*else*);
6.595 +
6.596 +(** ) switch_specify_solve p_ (pt, ip);( **)
6.597 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
6.598 + (*if*) Pos.on_specification ([], state_pos) (*then*);
6.599 +
6.600 +(** ) specify_do_next (pt, input_pos);( **)
6.601 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
6.602 +
6.603 +(** )val (_, (p_', tac)) =
6.604 + Specify.find_next_step ptp;( **)
6.605 +"~~~~~ fun find_next_step , args:"; val (ptp as (pt, (p, p_))) = (ptp);
6.606 +
6.607 +(** )val (_, (p_', tac)) =
6.608 + Specify.find_next_step ptp;( **);
6.609 +"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
6.610 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
6.611 + spec = refs, ...} = Calc.specify_data (pt, pos);
6.612 + val ctxt = Ctree.get_ctxt pt pos;
6.613 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
6.614 + (*if*) p_ = Pos.Pbl (*then*);
6.615 +
6.616 +(** )Specify.for_problem ctxt oris (o_refs, refs) (pbl, met); ( **)
6.617 +"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
6.618 + (ctxt, oris, (o_refs, refs), (pbl, met));
6.619 + val cpI = if pI = Problem.id_empty then pI' else pI;
6.620 + val cmI = if mI = MethodC.id_empty then mI' else mI;
6.621 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
6.622 + val {model = mpc, ...} = MethodC.from_store ctxt cmI
6.623 +
6.624 +(** )val (preok, _) =
6.625 + Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl); ( **);
6.626 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
6.627 + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
6.628 +
6.629 +(*WN230827: REPLACE WITH I_Model.of_max_variant* )val (env_subst, env_eval) =
6.630 + sep_variants_envs_OLD model_patt i_model ( **)
6.631 +"~~~~~ fun sep_variants_envs_OLD , args:"; val (model_patt, i_model) = (model_patt, i_model);
6.632 + val equal_descr_pairs =
6.633 + map (get_equal_descr i_model) model_patt
6.634 + |> flat
6.635 + val all_variants =
6.636 + map (fn (_, (_, variants, _, _, _)) => variants) equal_descr_pairs
6.637 + |> flat
6.638 + |> distinct op =
6.639 + val variants_separated = map (filter_variants equal_descr_pairs) all_variants
6.640 + val restricted_to_given = map (filter (fn ((m_field, (_, _)), (_, _, _, _, (_, _))) =>
6.641 + m_field = "#Given")) variants_separated;
6.642 +
6.643 +(** )val envs_subst = map
6.644 + mk_env_subst restricted_to_given ( **)
6.645 +"~~~~~ fun mk_env_subst , args:"; val (equal_descr_pairs) = (nth 1 (nth 1 restricted_to_given));
6.646 +
6.647 +val xxx =
6.648 +(*+*)(fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
6.649 + => (mk_env feedb) |> map fst (*dummy rhs dropped*)|> map (pair id))
6.650 + : Model_Pattern.single * I_Model.single_TEST -> Pre_Conds.env_subst;
6.651 +(*+*)equal_descr_pairs: Model_Pattern.single * I_Model.single_TEST;
6.652 +
6.653 +(** ) xxx equal_descr_pairs ( **)
6.654 +"~~~~~ fun xxx , args:"; val (((_, (_, id)), (_, _, _, _, (feedb, _)))) = (equal_descr_pairs);
6.655 +(*ERROR WN230404 (see TODO.md:
6.656 +mk_env not reasonable for "Cor_TEST equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(e_s, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])" (**)
6.657 + (mk_env feedb) *)
6.658 +
6.659 +(*+*)feedb: Model_Def.i_model_feedback_TEST;
6.660 +(*+*)(*----^^^^^^^^^^^^^^^^^^*)
6.661 +(*+*) I_Model.Cor_TEST: (descriptor * term list) * (term * term list) -> feedback_TEST;
6.662 +(*+*)Model_Def.Cor_TEST: (descriptor * term list) * (term * term list) -> Model_Def.i_model_feedback_TEST;
6.663 +(*\\------------------ step into Add_Given_equ ---------------------------------------------//*)
6.664 +
6.665 +
6.666 +val (p,_,f,nxt,_,pt) = return_Add_Given_equ; (**)val Add_Given "solveForVars [c]" = nxt;(**)
6.667 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c_2]" = nxt;
6.668 +
6.669 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.670 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.671 +case nxt of
6.672 + (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
6.673 + | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
6.674 +
6.675 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.676 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.677 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.678 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.679 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.680 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.681 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.682 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.683 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.684 +case nxt of
6.685 + (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
6.686 + | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
6.687 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.688 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.689 +(* final test ... ----------------------------------------------------------------------------*)
6.690 +if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
6.691 +else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
6.692 +
6.693 +case nxt of
6.694 + (End_Proof') => ()
6.695 + | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
6.696 +
6.697 +Test_Tool.show_pt pt (*[
6.698 +(([], Frm), solveSystem
6.699 + [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],
6.700 + [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]
6.701 + [[c], [c_2]]),
6.702 +(([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
6.703 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]),
6.704 +(([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]),
6.705 +(([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]),
6.706 +(([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]),
6.707 +(([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]),
6.708 +(([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]),
6.709 +(([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2),
6.710 +(([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2),
6.711 +(([5, 2], Res), L * c = q_0 * L \<up> 2 / 2),
6.712 +(([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L),
6.713 +(([5, 4], Res), c = L * q_0 / 2),
6.714 +(([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]),
6.715 +(([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]),
6.716 +(([5], Res), [c = L * q_0 / 2, c_2 = 0]),
6.717 +(([], Res), [c = L * q_0 / 2, c_2 = 0])]
6.718 +*)
6.719 +( *\\################# @ {context} within fun XXXXX ----------------------------------------//*)
6.720 +
6.721 \<close> ML \<open>
6.722 +\<close>
6.723 +
6.724 +section \<open>===================================================================================\<close>
6.725 +section \<open>===== Knowledge/eqsystem-1a.sml ===================================================\<close>
6.726 +section \<open>===== (*ERROR type_of: type mismatch in application * real * real list (#) [c]*) ==\<close>
6.727 +ML \<open>
6.728 +(* Title: Knowledge/eqsystem-1a.sml
6.729 + author: Walther Neuper 050826,
6.730 +*)
6.731 +
6.732 +"-----------------------------------------------------------------------------------------------";
6.733 +"table of contents -----------------------------------------------------------------------------";
6.734 +"-----------------------------------------------------------------------------------------------";
6.735 +"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
6.736 +"----------- problems -----------------------------------------------------------equsystem-1.sml";
6.737 +"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
6.738 +"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
6.739 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
6.740 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
6.741 +"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
6.742 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
6.743 +"----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
6.744 +"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
6.745 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
6.746 +(*========== ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^--vvvvvvvvvvvvvvvv ==================*)
6.747 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
6.748 +"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
6.749 +"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
6.750 +"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
6.751 +"-----------------------------------------------------------------------------------------------";
6.752 +"-----------------------------------------------------------------------------------------------";
6.753 +"-----------------------------------------------------------------------------------------------";
6.754 +
6.755 +
6.756 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
6.757 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
6.758 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
6.759 +val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
6.760 + "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
6.761 + "solveForVars [c, c_2]", "solution LL"];
6.762 +val (dI',pI',mI') =
6.763 + ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
6.764 + ["EqSystem", "normalise", "2x2"]);
6.765 +val p = e_pos'; val c = [];
6.766 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
6.767 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.768 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.769 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.770 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.771 +case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
6.772 + | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
6.773 +
6.774 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.775 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.776 +
6.777 +(*+*)if f2str f =
6.778 + "[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n" ^
6.779 + " 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]" then () else error "";
6.780 +(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt) =
6.781 + "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)";
6.782 +
6.783 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.784 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.785 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.786 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"]) = nxt
6.787 + val "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = f2str f;
6.788 +(*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [R, L, R, L, R, R, R, L, R, R], srls_normalise_2x2, SOME e_s, \n[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2], ORundef, true, false)"
6.789 + = (Ctree.get_istate_LI pt p |> Istate.string_of ctxt)
6.790 +
6.791 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.792 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.793 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c]" = nxt
6.794 +\<close> ML \<open>(*ERROR type_of: type mismatch in application * real * real list (#) [c]*)
6.795 +(*//################## @ {context} within fun XXXXX ---------------------------------------\\* )
6.796 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.797 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.798 +case nxt of
6.799 + (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
6.800 + | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
6.801 +
6.802 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.803 +
6.804 + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
6.805 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);
6.806 +
6.807 +val (p''',_,f,nxt''',_,pt''') = me nxt p c pt;f2str f;
6.808 +(*/------------------- step into me Apply_Method -------------------------------------------\*)
6.809 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
6.810 + val (pt'''', p'''') = (* keep for continuation*)
6.811 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
6.812 +
6.813 + case Step.by_tactic tac (pt, p) of
6.814 + ("ok", (_, _, ptp)) => ptp;
6.815 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
6.816 +
6.817 +(*+isa==isa2*)val ([5], Met) = p;
6.818 +(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt (fst p);
6.819 + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
6.820 +(*+isa==isa2*)is1 |> Istate.string_of ctxt;
6.821 + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
6.822 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);
6.823 +
6.824 + (*case*)
6.825 + Step.check tac (pt, p) (*of*);
6.826 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p) );
6.827 +
6.828 +(*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
6.829 +(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of ctxt);
6.830 +
6.831 + (*if*) Tactic.for_specify tac (*else*);
6.832 +val Applicable.Yes xxx =
6.833 +
6.834 +Solve_Step.check tac (ctree, pos);
6.835 +
6.836 +(*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
6.837 +(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of ctxt);
6.838 +
6.839 +"~~~~~ from Step.check to Step.by_tactic return val:"; val (Applicable.Yes tac') = (Applicable.Yes xxx);
6.840 + (*if*) Tactic.for_specify' tac' (*else*);
6.841 +
6.842 +Step_Solve.by_tactic tac' ptp;;
6.843 +"~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Apply_Method' _), (ptp as (pt, p)))
6.844 + = (tac', ptp);
6.845 +
6.846 +(*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
6.847 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);
6.848 +
6.849 + LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;
6.850 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))
6.851 + = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);
6.852 + val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
6.853 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
6.854 + val {model, ...} = MethodC.from_store ctxt mI;
6.855 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
6.856 + val (is, env, ctxt, prog) = case
6.857 + LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
6.858 + (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
6.859 +
6.860 +(*+*)val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)" =
6.861 +(*+isa==isa2*)is |> Istate.string_of ctxt
6.862 +
6.863 + val ini = LItool.implicit_take ctxt prog env;
6.864 + val pos = start_new_level pos
6.865 +val NONE =
6.866 + (*case*) ini (*of*);
6.867 + val (tac''', ist''', ctxt''') =
6.868 + case LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt of
6.869 + Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
6.870 +
6.871 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
6.872 +(*+isa==isa2*)ist''' |> Istate.string_of ctxt;
6.873 +
6.874 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
6.875 + = (prog ,(pt, (lev_dn p, Res)), is, ctxt);
6.876 +val Accept_Tac
6.877 + (Take' ttt, iii, _) =
6.878 + (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
6.879 +
6.880 +(*+isa==isa2*)val "c_2 = 0" = (ttt |> UnparseC.term @{context});
6.881 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
6.882 +(*+isa==isa2*)(Pstate iii |> Istate.string_of ctxt);
6.883 +
6.884 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
6.885 + = ((prog, (ptp, ctxt)), (Pstate ist));
6.886 + (*if*) path = [] (*then*);
6.887 +
6.888 + scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
6.889 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
6.890 + = (cc, (trans_scan_dn ist), (Program.body_of prog));
6.891 +
6.892 + (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
6.893 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
6.894 + = (cc ,(ist |> path_down [L, R]), e);
6.895 +
6.896 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" =
6.897 +(*+isa==isa2*)(Pstate ist |> Istate.string_of ctxt);
6.898 +
6.899 + (*if*) Tactical.contained_in t (*else*);
6.900 +
6.901 + (*case*)
6.902 + LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
6.903 +"~~~~~ fun check_leaf , args:"; val (call, ctxt, prog_rls, (E, (a, v)), t)
6.904 + = ("next ", ctxt, eval, (get_subst ist), t);
6.905 +
6.906 + (*case*)
6.907 + Prog_Tac.eval_leaf E a v t (*of*);
6.908 +"~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)))
6.909 + = (E, a, v, t);
6.910 +
6.911 +val return =
6.912 + (Program.Tac (subst_atomic E t), NONE:term option);
6.913 +"~~~~~ from fun eval_leaf \<longrightarrow>fun check_leaf , return:"; val (Program.Tac stac, a') = return;
6.914 + val stac' = Rewrite.eval_prog_expr ctxt prog_rls
6.915 + (subst_atomic (Env.update_opt E (a, v)) stac)
6.916 +
6.917 +val return =
6.918 + (Program.Tac stac', a');
6.919 +"~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val (Program.Tac prog_tac, form_arg) = return;
6.920 +
6.921 + check_tac cc ist (prog_tac, form_arg);
6.922 +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
6.923 + = (cc, ist, (prog_tac, form_arg));
6.924 + val m = LItool.tac_from_prog (pt, p) prog_tac
6.925 +val _ =
6.926 + (*case*) m (*of*); (*tac as string/input*)
6.927 +
6.928 + (*case*)
6.929 +Solve_Step.check m (pt, p) (*of*);
6.930 +"~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos)) = (m, (pt, p));
6.931 +
6.932 +val return =
6.933 + check_tac cc ist (prog_tac, form_arg)
6.934 +
6.935 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" =
6.936 +(*+isa==isa2*)(Pstate ist |> Istate.string_of ctxt);
6.937 +
6.938 +"~~~~~ from fun scan_dn \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:";
6.939 + val (Accept_Tac (tac, ist, ctxt)) = return;
6.940 +
6.941 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
6.942 +(*+isa==isa2*)(Pstate ist |> Istate.string_of ctxt)
6.943 +
6.944 +val return =
6.945 + Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac);
6.946 +"~~~~~ from fun find_next_step \<longrightarrow>fun by_tactic , return:"; val Next_Step (ist, ctxt, tac) = return;
6.947 + val (tac', ist', ctxt') = (tac, ist, ctxt)
6.948 +val Tactic.Take' t =
6.949 + (*case*) tac' (*of*);
6.950 + val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');
6.951 +
6.952 +(*+isa==isa2*)pos; (*from check_tac*)
6.953 +(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt [5];
6.954 + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
6.955 +(*+isa==isa2*)is1 |> Istate.string_of ctxt;
6.956 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
6.957 +(*+isa==isa2*)(ist' |> Istate.string_of ctxt)
6.958 +(*-------------------- stop step into me Apply_Method ----------------------------------------*)
6.959 +(*+isa==isa2*)val "c_2 = 0" = f2str f;
6.960 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
6.961 +(*+isa==isa2*)(Ctree.get_istate_LI pt''' p''' |> Istate.string_of ctxt)
6.962 +(*\\------------------- step into me Apply_Method ------------------------------------------//*)
6.963 +
6.964 +val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' c pt''';f2str f;
6.965 +
6.966 +(*+isa==isa2*)val ([5, 1], Frm) = p'''';
6.967 +(*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f2str f;
6.968 +(*+isa<>isa2*)val (** )Check_Postcond ["triangular", "2x2", "LINEAR", "system"]( **)
6.969 + Substitute ["c_2 = 0"](**) = nxt'''';
6.970 +(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt'''' (fst p'''');
6.971 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
6.972 +(*+isa==isa2*)is1 |> Istate.string_of ctxt;
6.973 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
6.974 +(*+isa==isa2*)Ctree.get_istate_LI pt'''' p'''' |> Istate.string_of ctxt;
6.975 +
6.976 +(*//------------------ step into me Take ---------------------------------------------------\\*)
6.977 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');
6.978 +
6.979 + val (pt, p) = (* keep for continuation*)
6.980 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
6.981 +
6.982 + case Step.by_tactic tac (pt, p) of
6.983 + ("ok", (_, _, ptp)) => ptp;
6.984 +
6.985 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
6.986 +(*isa==isa2*)Ctree.get_istate_LI pt p |> Istate.string_of ctxt;
6.987 +
6.988 + (*case*)
6.989 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
6.990 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
6.991 + (*if*) Pos.on_calc_end ip (*else*);
6.992 + val (_, probl_id, _) = Calc.references (pt, p);
6.993 +val _ =
6.994 + (*case*) tacis (*of*);
6.995 + (*if*) probl_id = Problem.id_empty (*else*);
6.996 +
6.997 + switch_specify_solve p_ (pt, ip);
6.998 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
6.999 + (*if*) Pos.on_specification ([], state_pos) (*else*);
6.1000 +
6.1001 + LI.do_next (pt, input_pos);
6.1002 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
6.1003 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
6.1004 + val thy' = get_obj g_domID pt (par_pblobj pt p);
6.1005 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
6.1006 +
6.1007 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
6.1008 +(*+isa==isa2*)ist |> Istate.string_of ctxt;
6.1009 +
6.1010 + (*case*)
6.1011 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
6.1012 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
6.1013 + = (sc, (pt, pos), ist, ctxt);
6.1014 +
6.1015 + (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
6.1016 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
6.1017 + = ((prog, (ptp, ctxt)), (Pstate ist));
6.1018 + (*if*) path = [] (*else*);
6.1019 +
6.1020 + go_scan_up (prog, cc) (trans_scan_up ist);
6.1021 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
6.1022 + = ((prog, cc), (trans_scan_up ist));
6.1023 +
6.1024 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, false)" =
6.1025 +(*+isa==isa2*)Pstate ist |> Istate.string_of ctxt;
6.1026 +(*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = act_arg |> UnparseC.term @{context};
6.1027 +
6.1028 + (*if*) path = [R] (*root of the program body*) (*else*);
6.1029 +
6.1030 + scan_up pcc (ist |> path_up) (go_up ctxt path sc);
6.1031 +"~~~~~ and scan_up , args:"; val ((pcc as (sc, cc)), ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))
6.1032 + = (pcc, (ist |> path_up), (go_up ctxt path sc));
6.1033 + val (i, body) = check_Let_up ctxt ist sc;
6.1034 +
6.1035 + (*case*) scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
6.1036 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
6.1037 + = (cc, (ist |> path_up_down [R, D] |> upd_env i), body);
6.1038 +
6.1039 +val goback =
6.1040 + (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
6.1041 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ e1 $ e2 $ a))
6.1042 + = (cc, (ist |> path_down [L, R]), e);
6.1043 +
6.1044 + (*case*) scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
6.1045 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
6.1046 + = (cc, (ist |> path_down_form ([L, L, R], a)), e1);
6.1047 + (*if*) Tactical.contained_in t (*else*);
6.1048 +
6.1049 + (*case*)
6.1050 + LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
6.1051 +"~~~~~ fun check_leaf , args:"; val (call, ctxt, prog_rls, (E, (a, v)), t)
6.1052 + = ("next ", ctxt, eval, (get_subst ist), t);
6.1053 +val (Program.Tac stac, a') =
6.1054 + (*case*) Prog_Tac.eval_leaf E a v t (*of*);
6.1055 + val stac' = Rewrite.eval_prog_expr ctxt prog_rls
6.1056 + (subst_atomic (Env.update_opt E (a, v)) stac)
6.1057 +
6.1058 +(*+*)val "Substitute [c_2 = 0] (L * c + c_2 = q_0 * L \<up> 2 / 2)" = stac' |> UnparseC.term @{context};
6.1059 +
6.1060 +val return =
6.1061 + (Program.Tac stac', a');
6.1062 +"~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val ((Program.Tac prog_tac, form_arg))
6.1063 + = (return);
6.1064 +
6.1065 + check_tac cc ist (prog_tac, form_arg);
6.1066 +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
6.1067 + = (cc, ist, (prog_tac, form_arg));
6.1068 + val m = LItool.tac_from_prog (pt, p) prog_tac
6.1069 +val _ =
6.1070 + (*case*) m (*of*);
6.1071 +
6.1072 + (*case*)
6.1073 +Solve_Step.check m (pt, p) (*of*);
6.1074 +"~~~~~ fun check , args:"; val ((Tactic.Substitute sube), (cs as (pt, pos as (p, _))))
6.1075 + = (m, (pt, p));
6.1076 + val pp = Ctree.par_pblobj pt p
6.1077 + val ctxt = Ctree.get_loc pt pos |> snd
6.1078 + val thy = Proof_Context.theory_of ctxt
6.1079 + val f = Calc.current_formula cs;
6.1080 + val {rew_ord, asm_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp)
6.1081 + val subte = Prog_Tac.Substitute_adapt_to_type' ctxt sube
6.1082 + val ro = get_rew_ord ctxt rew_ord;
6.1083 + (*if*) foldl and_ (true, map TermC.contains_Var subte) (*else*);
6.1084 +
6.1085 +(*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f |> UnparseC.term @{context}
6.1086 +(*+isa<>isa2*)val (** )["c_2 = (0::'a)"]( **)["c_2 = 0"](**) = subte |> map (UnparseC.term @{context})
6.1087 +
6.1088 +val SOME ttt =
6.1089 + (*case*) Rewrite.rewrite_terms_ ctxt ro asm_rls subte f (*of*);
6.1090 +(*-------------------- stop step into me Take ------------------------------------------------*)
6.1091 +(*\\------------------ step into me Take ---------------------------------------------------//*)
6.1092 +
6.1093 +val (p,_,f,nxt,_,pt) = me nxt'''' p'''' c pt'''';f2str f;
6.1094 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1095 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1096 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1097 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1098 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1099 +
6.1100 +(*+*)val (** )"L * c + c_2 = q_0 * L \<up> 2 / 2"( **)
6.1101 + "[c = L * q_0 / 2, c_2 = 0]"(**) = f2str f;
6.1102 +(*val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =*)
6.1103 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\", \"\n(e_2, c = L * q_0 / 2)\", \"\n(e__s, [c_2 = 0, c = L * q_0 / 2])\"], [R, R, D, R, D, R, D, R, D, R, D, L, R], srls_top_down_2x2, SOME e__s, \n[c = L * q_0 / 2, c_2 = 0], ORundef, true, true)" =
6.1104 +(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of ctxt);
6.1105 +
6.1106 +case nxt of
6.1107 + (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
6.1108 + | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
6.1109 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1110 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1111 +
6.1112 +(* final test ... ----------------------------------------------------------------------------*)
6.1113 +if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
6.1114 +else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
6.1115 +
6.1116 +case nxt of
6.1117 + (End_Proof') => ()
6.1118 + | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
6.1119 +
6.1120 +Test_Tool.show_pt pt (*[
6.1121 +(([], Frm), solveSystem
6.1122 + [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],
6.1123 + [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]
6.1124 + [[c], [c_2]]),
6.1125 +(([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
6.1126 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]),
6.1127 +(([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]),
6.1128 +(([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]),
6.1129 +(([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]),
6.1130 +(([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]),
6.1131 +(([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]),
6.1132 +(([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2),
6.1133 +
6.1134 +(([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2),
6.1135 +(([5, 2], Res), L * c = q_0 * L \<up> 2 / 2),
6.1136 +(([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L),
6.1137 +(([5, 4], Res), c = L * q_0 / 2),
6.1138 +(([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]),
6.1139 +(([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]),
6.1140 +(([5], Res), [c = L * q_0 / 2, c_2 = 0]),
6.1141 +(([], Res), [c = L * q_0 / 2, c_2 = 0])]
6.1142 +*)
6.1143 +( *\\################# @ {context} within fun XXXXX ----------------------------------------//*)
6.1144 +
6.1145 +\<close> ML \<open>
6.1146 +\<close>
6.1147 +
6.1148 +section \<open>===================================================================================\<close>
6.1149 +section \<open>===== Knowledge/eqsystem-2.sml ====================================================\<close>
6.1150 +section \<open>===== (*ERROR type_of: type mismatch in application * real * real list (#) [c]*) ==\<close>
6.1151 +ML \<open>
6.1152 +(* Title: Knowledge/eqsystem-2.sml
6.1153 + author: Walther Neuper 050826,
6.1154 + (c) due to copyright terms
6.1155 +*)
6.1156 +"-----------------------------------------------------------------------------------------------";
6.1157 +"table of contents -----------------------------------------------------------------------------";
6.1158 +"-----------------------------------------------------------------------------------------------";
6.1159 +"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
6.1160 +"----------- problems -----------------------------------------------------------equsystem-1.sml";
6.1161 +"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
6.1162 +"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
6.1163 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
6.1164 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
6.1165 +"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
6.1166 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
6.1167 +"----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
6.1168 +"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
6.1169 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
6.1170 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
6.1171 +"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
6.1172 +"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
6.1173 +"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
6.1174 +"-----------------------------------------------------------------------------------------------";
6.1175 +"-----------------------------------------------------------------------------------------------";
6.1176 +"-----------------------------------------------------------------------------------------------";
6.1177 +
6.1178 +val thy = @{theory "EqSystem"};
6.1179 +val ctxt = Proof_Context.init_global thy;
6.1180 +
6.1181 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
6.1182 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
6.1183 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
6.1184 +val fmz =
6.1185 + ["equalities\
6.1186 + \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
6.1187 + \ - 1 * q_0 / 24 * 0 \<up> 4),\
6.1188 + \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
6.1189 + \ - 1 * q_0 / 24 * L \<up> 4)]",
6.1190 + "solveForVars [c, c_2]", "solution LL"];
6.1191 +val (dI',pI',mI') =
6.1192 + ("Biegelinie",["LINEAR", "system"], ["no_met"]);
6.1193 +val p = e_pos'; val c = [];
6.1194 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
6.1195 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1196 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1197 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1198 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["normalise", "2x2", "LINEAR", "system"] = nxt
6.1199 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["EqSystem", "normalise", "2x2"] = nxt
6.1200 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1201 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1202 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1203 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1204 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1205 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"]) = nxt
6.1206 + val "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]" = f2str f;
6.1207 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1208 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1209 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c]" = nxt
6.1210 +\<close> ML \<open>(*ERROR type_of: type mismatch in application * real * real list (#) [c]*)
6.1211 +(*//################## @ {context} within fun XXXXX ---------------------------------------\\* )
6.1212 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1213 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1214 +
6.1215 +case nxt of
6.1216 + (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
6.1217 + | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
6.1218 +
6.1219 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1220 +val PblObj {probl,...} = get_obj I pt [5];
6.1221 + (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;
6.1222 +(*[
6.1223 +(1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
6.1224 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
6.1225 +(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
6.1226 +*)
6.1227 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1228 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1229 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1230 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1231 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1232 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1233 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1234 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1235 +case nxt of
6.1236 + (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
6.1237 + | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
6.1238 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1239 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
6.1240 +
6.1241 +if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..
6.1242 + "[c = - 1 * q_0 * L \<up> 3 / (24 * EI), c_2 = 0]"*)
6.1243 + "[c = - 1 * q_0 * L \<up> 3 / 24, c_2 = 0]"
6.1244 +then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
6.1245 +case nxt of
6.1246 + (End_Proof') => ()
6.1247 + | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
6.1248 +( *\\################# @ {context} within fun XXXXX ----------------------------------------//*)
6.1249 +
6.1250 +
6.1251 +\<close> ML \<open>
6.1252 +"----------- all systems from Biegelinie -------------------------";
6.1253 +"----------- all systems from Biegelinie -------------------------";
6.1254 +"----------- all systems from Biegelinie -------------------------";
6.1255 +val thy = @{theory Isac_Knowledge}
6.1256 +val subst =
6.1257 + [(ParseC.parse_test @{context} "bdv_1", ParseC.parse_test @{context} "c"), (ParseC.parse_test @{context} "bdv_2", ParseC.parse_test @{context} "c_2"),
6.1258 + (ParseC.parse_test @{context} "bdv_3", ParseC.parse_test @{context} "c_3"), (ParseC.parse_test @{context} "bdv_4", ParseC.parse_test @{context} "c_4")];
6.1259 +
6.1260 +"------- Bsp 7.27";
6.1261 +States.reset ();
6.1262 +CalcTree @{context} [(
6.1263 + ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
6.1264 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],
6.1265 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
6.1266 +\<close> ML \<open>(*ERROR type_of: type mismatch in application, real, real list, occurs_in [c]*)
6.1267 +(*//################## @ {context} within fun XXXXX ---------------------------------------\\* )
6.1268 +moveActiveRoot 1;
6.1269 +(*
6.1270 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
6.1271 +##7.27## ordered substs
6.1272 + c_4 c_2
6.1273 +c c_2 c_3 c_4 c c_2 1->2: c
6.1274 + c_2 c_4
6.1275 +c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
6.1276 +val t = ParseC.parse_test @{context}
6.1277 + ("[0 = c_4, " ^
6.1278 + "0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
6.1279 + "0 = c_2, " ^
6.1280 + "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]");
6.1281 +val SOME (t, _) = rewrite_set_ ctxt false isolate_bdvs_4x4 t;
6.1282 +if UnparseC.term @{context} t =
6.1283 +"[c_4 = 0,\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n (- 24 * EI) =\n - 1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0]"
6.1284 +then () else error "Bsp 7.27";
6.1285 +
6.1286 +"----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
6.1287 +val t = ParseC.parse_test @{context} "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
6.1288 +val NONE = rewrite_set_ ctxt false norm_Rational t;
6.1289 +val SOME (t,_) =
6.1290 + rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
6.1291 +if UnparseC.term @{context} t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)"
6.1292 +then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
6.1293 +
6.1294 +"--- isolate_bdvs_4x4";
6.1295 +(*
6.1296 +val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;
6.1297 +UnparseC.term @{context} t;
6.1298 +val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System t;
6.1299 +UnparseC.term @{context} t;
6.1300 +val SOME (t,_) = rewrite_set_ ctxt false order_system t;
6.1301 +UnparseC.term @{context} t;
6.1302 +*)
6.1303 +
6.1304 +"------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
6.1305 +States.reset ();
6.1306 +CalcTree @{context} [((*WN130908 <ERROR> error in kernel </ERROR>*)
6.1307 + ["Traegerlaenge L", "Momentenlinie (-q_0 / L * x \<up> 3 / 6)",
6.1308 + "Biegelinie y",
6.1309 + "Randbedingungen [y L = 0, y' L = 0]",
6.1310 + "FunktionsVariable x"],
6.1311 + ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
6.1312 + ["Biegelinien", "AusMomentenlinie"]))];
6.1313 +(*
6.1314 +moveActiveRoot 1;
6.1315 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
6.1316 +*)
6.1317 +
6.1318 +"------- Bsp 7.69";
6.1319 +States.reset ();
6.1320 +CalcTree @{context} [(
6.1321 + ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
6.1322 + "Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],
6.1323 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
6.1324 +moveActiveRoot 1;
6.1325 +(*
6.1326 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
6.1327 +##7.69## ordered subst 2x2
6.1328 + c_4 c_3
6.1329 +c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
6.1330 + c_3 c_4
6.1331 +c c_2 c_3 c c_2 c_3 c_4 3:c_4 -> 4:c c_2 c_3 1:c_3 -> 4:c c_2*)
6.1332 +val t = ParseC.parse_test @{context}
6.1333 + ("[0 = c_4 + 0 / (- 1 * EI), " ^
6.1334 + "0 = c_4 + L * c_3 + (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
6.1335 + "0 = c_3 + 0 / (- 1 * EI), " ^
6.1336 + "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]");
6.1337 +
6.1338 +"------- Bsp 7.70";
6.1339 +States.reset ();
6.1340 +CalcTree @{context} [(
6.1341 + ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
6.1342 + "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],
6.1343 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
6.1344 +moveActiveRoot 1;
6.1345 +(*
6.1346 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
6.1347 +##7.70## |subst
6.1348 +c |
6.1349 +c c_2 |1:c -> 2:c_2
6.1350 + c_3 |
6.1351 + c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
6.1352 +
6.1353 +"----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
6.1354 +val t = ParseC.parse_test @{context}
6.1355 + ("[L * q_0 = c, " ^
6.1356 + "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
6.1357 + "0 = c_4, " ^
6.1358 + "0 = c_3]");
6.1359 +val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
6.1360 +val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
6.1361 +val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
6.1362 +if UnparseC.term @{context} t =
6.1363 + "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"
6.1364 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
6.1365 +
6.1366 +val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
6.1367 +if UnparseC.term @{context} t = "[L * q_0 = c, - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2) = 0, c_4 = 0,\n c_3 = 0]"
6.1368 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";
6.1369 +
6.1370 +val SOME (t,_) = rewrite_set_inst_ ctxt false subst isolate_bdvs_4x4 t;
6.1371 +if UnparseC.term @{context} t =
6.1372 + "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^
6.1373 + " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]"
6.1374 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
6.1375 +
6.1376 +val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t;
6.1377 +if UnparseC.term @{context} t =
6.1378 + "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"
6.1379 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
6.1380 +
6.1381 +val SOME (t, _) = rewrite_set_ ctxt false order_system t;
6.1382 +if UnparseC.term @{context} t =
6.1383 + "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"
6.1384 +then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";
6.1385 +
6.1386 +"----- 7.70 with met normalise: ";
6.1387 +val fmz = ["equalities" ^
6.1388 + "[L * q_0 = c, " ^
6.1389 + "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
6.1390 + "0 = c_4, " ^
6.1391 + "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
6.1392 +val (dI',pI',mI') = ("Biegelinie",["LINEAR", "system"], ["no_met"]);
6.1393 +val p = e_pos'; val c = [];
6.1394 +
6.1395 +(*============ inhibit exn WN120314 TODO: investigate type error (same as above)==
6.1396 + in next but one test below the same type error.
6.1397 +/-------------------------------------------------------\
6.1398 +Type unification failed
6.1399 +Type error in application: incompatible operand type
6.1400 +
6.1401 +Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
6.1402 +Operand: [c_4] :: 'b list
6.1403 +\-------------------------------------------------------/
6.1404 +
6.1405 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
6.1406 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1407 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1408 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1409 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1410 +case nxt of (_,Apply_Method ["EqSystem", "normalise", "4x4"]) => ()
6.1411 + | _ => error "eqsystem.sml [EqSystem,normalise,4x4] specify";
6.1412 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1413 +
6.1414 +"----- outcommented before Isabelle2002 --> 2011 -------------------------";
6.1415 +(*-----------------------------------vvvWN080102 Exception- Match raised
6.1416 + since associate Rewrite .. Rewrite_Set
6.1417 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1418 +
6.1419 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1420 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1421 +
6.1422 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1423 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1424 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1425 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1426 +if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"
6.1427 +then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";
6.1428 +--------------------------------------------------------------------------*)
6.1429 +============ inhibit exn WN120314 ==============================================*)
6.1430 +
6.1431 +"----- 7.70 with met top_down_: me";
6.1432 +val fmz = [
6.1433 + "equalities [(c::real) = L * q_0, L * c + (c_2::real) = q_0 * L \<up> 2 / 2, (c_3::real) = 0, (c_4::real) = 0]",
6.1434 + "solveForVars [(c::real), (c_2::real), (c_3::real), (c_4::real)]", "solution LL"];
6.1435 +val (dI',pI',mI') =
6.1436 + ("Biegelinie",["LINEAR", "system"],["no_met"]);
6.1437 +val p = e_pos'; val c = [];
6.1438 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
6.1439 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1440 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1441 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1442 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1443 +case nxt of Apply_Method ["EqSystem", "top_down_substitution", "4x4"] => ()
6.1444 + | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
6.1445 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1446 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1447 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1448 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1449 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1450 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1451 +if p = ([], Res) andalso
6.1452 +(* "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"*)
6.1453 + f2str f = "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
6.1454 +then () else error "eqsystem.sml: 7.70 with met top_down_: me";
6.1455 +
6.1456 +"------- Bsp 7.71";
6.1457 +States.reset ();
6.1458 +CalcTree @{context} [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
6.1459 + "Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",
6.1460 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
6.1461 + "AbleitungBiegelinie dy"],
6.1462 + ("Biegelinie", ["Biegelinien"],
6.1463 + ["IntegrierenUndKonstanteBestimmen2"] ))];
6.1464 +moveActiveRoot 1;
6.1465 +(*
6.1466 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
6.1467 +##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
6.1468 +c c_2 |c c_2 |1' |1': c c_2 |
6.1469 + c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
6.1470 +c c_2 c_3 c_4 | c_4 |3' | |
6.1471 + c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *)
6.1472 +val t = ParseC.parse_test @{context}"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \
6.1473 +\ 0 = c_4 + 0 / (- 1 * EI), \
6.1474 +\ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /(- 24 * EI),\
6.1475 +\ 0 = c_3 + 0 / (- 1 * EI)]";
6.1476 +
6.1477 +"------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
6.1478 +States.reset ();
6.1479 +CalcTree @{context} [(["Traegerlaenge L",
6.1480 + "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x \<up> ^3)",
6.1481 + "Biegelinie y",
6.1482 + "Randbedingungen [y 0 = (0::real), y L = 0]",
6.1483 + "FunktionsVariable x"],
6.1484 + ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
6.1485 + ["Biegelinien", "AusMomentenlinie"]))];
6.1486 +moveActiveRoot 1;
6.1487 +(*
6.1488 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
6.1489 +*)
6.1490 +
6.1491 +"------- Bsp 7.72b";
6.1492 +States.reset ();
6.1493 +CalcTree @{context} [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",
6.1494 + "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",
6.1495 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
6.1496 + "AbleitungBiegelinie dy"],
6.1497 + ("Biegelinie", ["Biegelinien"],
6.1498 + ["IntegrierenUndKonstanteBestimmen2"] ))];
6.1499 +moveActiveRoot 1;
6.1500 +(*
6.1501 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
6.1502 +##7.72b## |ord. |subst.singles |ord.triang.
6.1503 + c_2 | | |c_2
6.1504 +c c_2 | |1:c_2 -> 2':c |c_2 c
6.1505 + c_4 | | |
6.1506 +c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
6.1507 +val t = ParseC.parse_test @{context}"[0 = c_2, \
6.1508 +\ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \
6.1509 +\ 0 = c_4 + 0 / (- 1 * EI), \
6.1510 +\ 0 = c_4 + L * c_3 + (60 * L \<up> 2 * c_2 + 20 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 120 * EI)]";
6.1511 +
6.1512 +"------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
6.1513 +States.reset ();
6.1514 +CalcTree @{context} [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)
6.1515 + "Biegelinie y",
6.1516 + "Randbedingungen [y L = 0, y' L = 0]",
6.1517 + "FunktionsVariable x"],
6.1518 + ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
6.1519 + ["Biegelinien", "AusMomentenlinie"]))];
6.1520 +moveActiveRoot 1;
6.1521 +(*
6.1522 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
6.1523 +*)
6.1524 +
6.1525 +"----------- 4x4 systems from Biegelinie -------------------------";
6.1526 +"----------- 4x4 systems from Biegelinie -------------------------";
6.1527 +"----------- 4x4 systems from Biegelinie -------------------------";
6.1528 +(*STOPPED.WN08?? replace this test with 7.70 *)
6.1529 +"----- Bsp 7.27";
6.1530 +val fmz = ["equalities \
6.1531 + \[0 = c_4, \
6.1532 + \ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
6.1533 + \ 0 = c_2, \
6.1534 + \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]",
6.1535 + "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
6.1536 +val (dI',pI',mI') =
6.1537 + ("Biegelinie",["normalise", "4x4", "LINEAR", "system"],
6.1538 + ["EqSystem", "normalise", "4x4"]);
6.1539 +val p = e_pos'; val c = [];
6.1540 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
6.1541 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1542 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1543 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1544 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1545 +"------------------------------------------- Apply_Method...";
6.1546 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1547 +"[0 = c_4, \
6.1548 +\ 0 = c_4 + L * c_3 +\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
6.1549 +\ 0 = c_2, \
6.1550 +\ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]";
6.1551 +(*vvvWN080102 Exception- Match raised
6.1552 + since associate Rewrite .. Rewrite_Set
6.1553 +"------------------------------------------- simplify_System_parenthesized...";
6.1554 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1555 +"[0 = c_4, \
6.1556 +\ 0 = - 1 * q_0 * L \<up> 4 / (- 24 * EI) + \
6.1557 +\ (4 * L \<up> 3 * c / (- 24 * EI) + \
6.1558 +\ (12 * L \<up> 2 * c_2 / (- 24 * EI) + \
6.1559 +\ (L * c_3 + c_4))), \
6.1560 +\ 0 = c_2, \
6.1561 +\ 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]";
6.1562 +(*? "(4 * L \<up> 3 / (- 24 * EI) * c" statt "(4 * L \<up> 3 * c / (- 24 * EI)" ?*)
6.1563 +"------------------------------------------- isolate_bdvs...";
6.1564 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1565 +"[c_4 = 0,\
6.1566 +\ c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 4 / (- 24 * EI)) + - 1 * (4 * L \<up> 3 * c / (- 24 * EI)) + - 1 * (12 * L \<up> 2 * c_2 / (- 24 * EI)) + - 1 * (L * c_3),\
6.1567 +\ c_2 = 0, \
6.1568 +\ c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2) + - 1 * (L * c)]";
6.1569 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.1570 +
6.1571 +---------------------------------------------------------------------*)
6.1572 +( *\\################# @ {context} within fun XXXXX ----------------------------------------//*)
6.1573 +
6.1574 +\<close> ML \<open>
6.1575 +\<close>
6.1576 +
6.1577 +(** )ML_file "Specify/specify.sml"( **)
6.1578 +section \<open>===================================================================================\<close>
6.1579 +section \<open>===== Specify/specify.sml =========================================================\<close>
6.1580 +section \<open>===== (*ERROR isalist2list applied to NON-list: funs'''*) =========================\<close>
6.1581 +ML \<open>
6.1582 +(* Title: "Specify/specify.sml"
6.1583 + Author: Walther Neuper
6.1584 + (c) due to copyright terms
6.1585 +*)
6.1586 +
6.1587 +"-----------------------------------------------------------------------------------------------";
6.1588 +"table of contents -----------------------------------------------------------------------------";
6.1589 +"-----------------------------------------------------------------------------------------------";
6.1590 +"-----------------------------------------------------------------------------------------------";
6.1591 +"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
6.1592 +"----------- revise Specify.do_all -------------------------------------------------------------";
6.1593 +"----------- specify-phase: low level functions for Biegelinie ---------------------------------";
6.1594 +"-----------------------------------------------------------------------------------------------";
6.1595 +"-----------------------------------------------------------------------------------------------";
6.1596 +"-----------------------------------------------------------------------------------------------";
6.1597 +open Pos;
6.1598 +open Ctree;
6.1599 +open Test_Code;
6.1600 +open Tactic;
6.1601 +open Specify;
6.1602 +open Step;
6.1603 +
6.1604 +open O_Model;
6.1605 +open I_Model;
6.1606 +open P_Model;
6.1607 +open Specify_Step;
6.1608 +open Test_Code;
6.1609 +
6.1610 +(**** maximum-example: Specify.finish_phase ############################################# ****)
6.1611 +"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
6.1612 +"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
6.1613 +(*//-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --\\* )
6.1614 + val (p,_,f,nxt,_,pt) =
6.1615 + Test_Code.init_calc @{context}
6.1616 + [(["fixedValues [r=Arbfix]", "maximum A",
6.1617 + "valuesFor [a,b]",
6.1618 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
6.1619 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
6.1620 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
6.1621 +
6.1622 + "boundVariable a", "boundVariable b", "boundVariable alpha",
6.1623 + "interval {x::real. 0 <= x & x <= 2*r}",
6.1624 + "interval {x::real. 0 <= x & x <= 2*r}",
6.1625 + "interval {x::real. 0 <= x & x <= pi}",
6.1626 + "errorBound (eps=(0::real))"],
6.1627 + ("Diff_App",["maximum_of", "function"],["Diff_App", "max_by_calculus"])
6.1628 + )];
6.1629 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1630 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1631 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1632 + (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
6.1633 + val pits = get_obj g_pbl pt (fst p);
6.1634 + writeln (I_Model.to_string ctxt pits);
6.1635 +(*[
6.1636 +(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
6.1637 +(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
6.1638 +(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
6.1639 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
6.1640 + val (pt,p) = Specify.finish_phase (pt,p);
6.1641 + val pits = get_obj g_pbl pt (fst p);
6.1642 + if I_Model.to_string ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]"
6.1643 + then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
6.1644 + writeln (I_Model.to_string ctxt pits);
6.1645 +(*[
6.1646 +(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
6.1647 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
6.1648 +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
6.1649 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
6.1650 +2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]*)
6.1651 + val mits = get_obj g_met pt (fst p);
6.1652 + if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"
6.1653 + then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
6.1654 + writeln (I_Model.to_string ctxt mits);
6.1655 +(*[
6.1656 +(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
6.1657 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
6.1658 +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
6.1659 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
6.1660 +2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),
6.1661 +(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
6.1662 +(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
6.1663 +0 <= x & x <= 2 * r}])),
6.1664 +(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
6.1665 +( *\\-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --//*)
6.1666 +
6.1667 +
6.1668 +(**** revise Specify.do_all ############################################################## ****);
6.1669 +"----------- revise Specify.do_all -------------------------------------------------------------";
6.1670 +"----------- revise Specify.do_all -------------------------------------------------------------";
6.1671 +(* from Minisubplb/100-init-rootpbl.sml:
6.1672 +val (_(*example text*),
6.1673 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
6.1674 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
6.1675 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
6.1676 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
6.1677 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
6.1678 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
6.1679 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
6.1680 + "ErrorBound (\<epsilon> = (0::real))" :: []),
6.1681 + refs as ("Diff_App",
6.1682 + ["univariate_calculus", "Optimisation"],
6.1683 + ["Optimisation", "by_univariate_calculus"])))
6.1684 + = Store.get (Know_Store.get_expls @ {theory Know_Store}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
6.1685 +*)
6.1686 +val model = ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
6.1687 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
6.1688 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
6.1689 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
6.1690 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
6.1691 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
6.1692 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
6.1693 + "ErrorBound (\<epsilon> = (0::real))" :: [])
6.1694 +val refs = ("Diff_App",
6.1695 + ["univariate_calculus", "Optimisation"],
6.1696 + ["Optimisation", "by_univariate_calculus"])
6.1697 +
6.1698 +val (p,_,f,nxt,_,pt) =
6.1699 + Test_Code.init_calc @{context} [(model, refs)];
6.1700 +"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
6.1701 + = (@{context}, [(model, refs)]);
6.1702 +
6.1703 + Specify.do_all (pt, p);
6.1704 +(*//------------------ step into do_all ----------------------------------------------------\\*)
6.1705 +"~~~~~ fun do_all , args:"; val (pt, (*old* )pos as( *old*) (p, _)) = (pt, p);
6.1706 + val (itms, oris, probl, o_refs, spec, ctxt) = case Ctree.get_obj I pt p of
6.1707 + Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
6.1708 + => (itms, oris, probl, o_spec, spec, ctxt)
6.1709 + | _ => raise ERROR "LI.by_tactic: no PblObj"
6.1710 + val (_, pbl_id', met_id') = References.select_input o_refs spec
6.1711 + val (pbl_imod, met_imod) = I_Model.s_make_complete ctxt oris
6.1712 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_id', met_id')
6.1713 +;
6.1714 +(*-------------------- stop step into do_all -------------------------------------------------*)
6.1715 +(*/------------------- check result of I_Model.complete' ------------------------------------\*)
6.1716 +(*+*)if Model_Pattern.to_string @{context} (#model (MethodC.from_store ctxt met_id')) = "[\"" ^
6.1717 + "(#Given, (Constants, fixes))\", \"" ^
6.1718 + "(#Given, (Maximum, maxx))\", \"" ^
6.1719 + "(#Given, (Extremum, extr))\", \"" ^
6.1720 + "(#Given, (SideConditions, sideconds))\", \"" ^
6.1721 + "(#Given, (FunctionVariable, funvar))\", \"" ^
6.1722 + "(#Given, (Input_Descript.Domain, doma))\", \"" ^
6.1723 + "(#Given, (ErrorBound, err))\", \"" ^
6.1724 + "(#Find, (AdditionalValues, vals))\"]"
6.1725 +(*+*)then () else error "mod_pat CHANGED";
6.1726 +(*+*)if I_Model.to_string_TEST @{context} met_imod = "[\n" ^
6.1727 + "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
6.1728 + "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
6.1729 + "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
6.1730 + "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
6.1731 + "(7, [1], true ,#undef, (Cor_TEST FunctionVariable a , pen2str, Position.T)), \n" ^
6.1732 + "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
6.1733 + "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
6.1734 + "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
6.1735 +(*+*)then () else error "met_imod CHANGED";
6.1736 +(*\------------------- check result of I_Model.complete' ------------------------------------/*)
6.1737 +(*\\------------------ step into do_all ----------------------------------------------------//*)
6.1738 +
6.1739 +(*-------------------- continuing do_all -----------------------------------------------------*)
6.1740 + val (pt, _) = Ctree.cupdate_problem pt p
6.1741 + (o_refs, I_Model.TEST_to_OLD pbl_imod, I_Model.TEST_to_OLD met_imod, ctxt)
6.1742 +;
6.1743 +
6.1744 +
6.1745 +(**** specify-phase: low level functions for Biegelinie #################################### ****)
6.1746 +"----------- specify-phase: low level functions for Biegelinie ---------------------------------";
6.1747 +"----------- specify-phase: low level functions for Biegelinie ---------------------------------";
6.1748 +open Pos;
6.1749 +open Ctree;
6.1750 +open Test_Code;
6.1751 +open Tactic;
6.1752 +open Specify;
6.1753 +open Step;
6.1754 +
6.1755 +open O_Model;
6.1756 +open I_Model;
6.1757 +open P_Model;
6.1758 +open Specify_Step;
6.1759 +
6.1760 +val formalise = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
6.1761 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
6.1762 +(*
6.1763 + Now follow items for ALL SubProblems,
6.1764 + since ROOT MethodC must provide values for "actuals" of ALL SubProblems.
6.1765 + See Biegelinie.thy subsection \<open>Survey on Methods\<close>.
6.1766 +*)
6.1767 +(*
6.1768 + Items for MethodC "IntegrierenUndKonstanteBestimmen2"
6.1769 +*)
6.1770 + "FunktionsVariable x",
6.1771 + (*"Biegelinie y", ..already input for Problem above*)
6.1772 + "AbleitungBiegelinie dy",
6.1773 + "Biegemoment M_b",
6.1774 + "Querkraft Q",
6.1775 +(*
6.1776 + Item for Problem "LINEAR/system", which by [''no_met''] involves refinement
6.1777 +*)
6.1778 + "GleichungsVariablen [c, c_2, c_3, c_4]"
6.1779 +];
6.1780 +(*
6.1781 + Note: the above sequence of items follows the sequence of formal arguments (and of model items)
6.1782 + of MethodC "IntegrierenUndKonstanteBestimmen2"
6.1783 +*)
6.1784 +val references = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
6.1785 +val p = e_pos'; val c = [];
6.1786 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(formalise, references)]; (*nxt = Model_Problem*)
6.1787 +
6.1788 +(*/------------------- check result of Test_Code.init_calc @{context} ----------------------------------------\*)
6.1789 +(*+*)val (o_model, ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]), _) =
6.1790 + get_obj g_origin pt (fst p);
6.1791 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
6.1792 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
6.1793 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
6.1794 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
6.1795 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
6.1796 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
6.1797 + "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
6.1798 + "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
6.1799 + "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
6.1800 + "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
6.1801 +then () else error "[IntegrierenUndKonstanteBestimmen2] O_Model CHANGED";
6.1802 +(*\------------------- check result of Test_Code.init_calc @{context} ----------------------------------------/*)
6.1803 +
6.1804 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt
6.1805 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
6.1806 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt
6.1807 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Randbedingungen [y 0 = 0]" = nxt
6.1808 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Randbedingungen [y 0 = 0, y L = 0]" = nxt
6.1809 +(*[], 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]" = nxt
6.1810 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Randbedingungen [y L = 0, y 0 = 0, M_b 0 = 0, M_b L = 0]" = nxt
6.1811 +
6.1812 +val return_me_Add_Relation_Randbedingungen = me nxt p c pt; (*\<rightarrow>Specify_Problem ["Biegelinien"]*)
6.1813 +(*/------------------- step into me_Add_Relation_Randbedingungen ---------------------------\\*)
6.1814 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
6.1815 + val ctxt = Ctree.get_ctxt pt p
6.1816 + val (pt, p) =
6.1817 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
6.1818 + case Step.by_tactic tac (pt, p) of
6.1819 + ("ok", (_, _, ptp)) => ptp
6.1820 +
6.1821 +val ("ok", ([(Specify_Theory "Biegelinie", _, _)], _, _)) =
6.1822 + (*case*)
6.1823 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
6.1824 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
6.1825 + (p, ((pt, Pos.e_pos'), []));
6.1826 + (*if*) Pos.on_calc_end ip (*else*);
6.1827 + val (_, probl_id, _) = Calc.references (pt, p);
6.1828 +val _ =
6.1829 + (*case*) tacis (*of*);
6.1830 + (*if*) probl_id = Problem.id_empty (*else*);
6.1831 +
6.1832 + switch_specify_solve p_ (pt, ip);
6.1833 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
6.1834 + (*if*) Pos.on_specification ([], state_pos) (*then*);
6.1835 +
6.1836 + specify_do_next (pt, input_pos);
6.1837 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
6.1838 + val (_, (p_', tac)) = Specify.find_next_step ptp
6.1839 + val ist_ctxt = Ctree.get_loc pt (p, p_)
6.1840 +val Specify_Theory "Biegelinie" =
6.1841 + (*case*) tac (*of*);
6.1842 +
6.1843 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
6.1844 +
6.1845 +(*|------------------- contine me_Add_Relation_Randbedingungen -------------------------------*)
6.1846 +(*\------------------- step into me_Add_Relation_Randbedingungen ---------------------------//*)
6.1847 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = return_me_Add_Relation_Randbedingungen;
6.1848 + val Specify_Theory "Biegelinie" = nxt
6.1849 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt
6.1850 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
6.1851 +
6.1852 +(*[], Met*)val return_me_Specify_Method_IntegrierenUndKonstanteBestimmen2
6.1853 + = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
6.1854 +\<close> ML \<open>(*/------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2--------\*)
6.1855 +(*/------------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2--------\*)
6.1856 +
6.1857 +(*/------------------- initial check for whole me ------------------------------------------\*)
6.1858 +(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt;
6.1859 +
6.1860 +(*+*)val {origin = (o_model, o_refs, _), probl = i_pbl, meth = i_met, spec, ...} =
6.1861 + Calc.specify_data (pt, p);
6.1862 +(*+*)if o_refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])
6.1863 +(*+*)then () else error "initial o_refs CHANGED";
6.1864 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
6.1865 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
6.1866 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
6.1867 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
6.1868 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
6.1869 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
6.1870 + "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
6.1871 + "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
6.1872 + "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
6.1873 + "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
6.1874 +(*+*)then () else error "initial o_model CHANGED";
6.1875 +(*+*)val "[\n(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [M_b 0 = 0, y 0 = 0, y L = 0, M_b L = 0] , pen2str)]"
6.1876 + = I_Model.to_string @{context} i_pbl
6.1877 +(*+*)val "[]" = I_Model.to_string @{context} i_met
6.1878 +(*+*)val (_, ["Biegelinien"], _) = spec;
6.1879 +(*\------------------- initial check for whole me ------------------------------------------/*)
6.1880 +
6.1881 +\<close> ML \<open>(*//------------ step into Step.by_tactic -------------------------------------------\\*)
6.1882 +(*//------------------ step into Step.by_tactic -------------------------------------------\\*)
6.1883 +"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
6.1884 + val (pt'''''_', p'''''_') = case
6.1885 + Step.by_tactic tac (pt, p) of ("ok", (_, _, ptp)) => ptp;
6.1886 +(*/------------------- check for entry to Step.by_tactic -----------------------------------\*)
6.1887 +(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac;
6.1888 +(*+*)val {origin = (o_model, _, _), ...} = Calc.specify_data (pt, p);
6.1889 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
6.1890 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
6.1891 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
6.1892 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
6.1893 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
6.1894 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
6.1895 + "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
6.1896 + "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
6.1897 + "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
6.1898 + "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
6.1899 +(*+*)then () else error "o_model AFTER Specify_Method NOTok CHANGED";
6.1900 +(*\------------------- check for Step.by_tactic --------------------------------------------/*)
6.1901 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
6.1902 + val Applicable.Yes (tac' as Specify_Method' (["IntegrierenUndKonstanteBestimmen2"], o_model, i_model)) =(*case*)
6.1903 + Step.check tac (pt, p) (*of*);
6.1904 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
6.1905 + (*if*) Tactic.for_specify tac (*then*);
6.1906 +
6.1907 +Specify_Step.check tac (ctree, pos);
6.1908 +"~~~~~ fun check , args:"; val ((Tactic.Specify_Method mID), (ctree, pos)) = (tac, (ctree, pos));
6.1909 +
6.1910 + val (o_model''''', _, i_model''''') =
6.1911 + Specify_Step.complete_for mID (ctree, pos);
6.1912 +"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (mID, (ctree, pos));
6.1913 + val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = met_imod, ctxt,
6.1914 + ...} = Calc.specify_data (ctree, pos);
6.1915 + val ctxt = Ctree.get_ctxt ctree pos
6.1916 + val (dI, _, _) = References.select_input o_refs refs;
6.1917 + val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
6.1918 + val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
6.1919 +
6.1920 + val (o_model', ctxt') =
6.1921 + O_Model.complete_for m_patt root_model (o_model, ctxt);
6.1922 +(*/------------------- check entry to O_Model.complete_for -----------------------------------------\*)
6.1923 +(*+*)Model_Pattern.to_string @{context} m_patt = "[\"" ^
6.1924 + "(#Given, (Traegerlaenge, l))\", \"" ^
6.1925 + "(#Given, (Streckenlast, q))\", \"" ^
6.1926 + "(#Given, (FunktionsVariable, v))\", \"" ^
6.1927 + "(#Given, (GleichungsVariablen, vs))\", \"" ^
6.1928 + "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
6.1929 + "(#Find, (Biegelinie, b))\", \"" ^
6.1930 + "(#Relate, (Randbedingungen, s))\"]";
6.1931 +(*+*) O_Model.to_string @{context} root_model;
6.1932 +(*\------------------- check entry to O_Model.complete_for -----------------------------------------/*)
6.1933 +"~~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) = (m_patt, root_model, (o_model, ctxt));
6.1934 + val missing = m_patt |> filter_out
6.1935 + (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor))
6.1936 +\<close> ML \<open>
6.1937 +(*ERROR?*)val [] = missing
6.1938 +\<close> ML \<open>
6.1939 + val add = (root_model
6.1940 + |> filter
6.1941 + (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor))
6.1942 +;
6.1943 +val return_complete_for =
6.1944 + ((o_model @ add)
6.1945 + |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
6.1946 + |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
6.1947 + |> add_enumerate (* for correct enumeration *)
6.1948 + |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
6.1949 + ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from O_Model.complete_for*);
6.1950 +"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.complete_for , return:"; val (o_model', ctxt') =
6.1951 + ((o_model @ add)
6.1952 + |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
6.1953 + |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
6.1954 + |> add_enumerate (* for correct enumeration *)
6.1955 + |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
6.1956 + ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));
6.1957 +(*+*)val "[\n(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n(4, [\"1\"], #Given, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n(6, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"]), \n(7, [\"1\"], #Given, Biegemoment, [\"M_b\"]), \n(8, [\"1\"], #Given, Querkraft, [\"Q\"]), \n(9, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
6.1958 + = O_Model.to_string @{context} o_model';
6.1959 +
6.1960 + val thy = ThyC.get_theory @{context} dI
6.1961 + val (_, (i_model, _)) = M_Match.match_itms_oris ctxt o_model'
6.1962 + (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST met_imod) (m_patt, where_, where_rls) ;
6.1963 +
6.1964 +val return_Specify_Step_complete_for =
6.1965 + (o_model', ctxt', i_model);
6.1966 +
6.1967 +"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.check , return:"; val (o_model, _, i_model) =
6.1968 + (o_model', ctxt', i_model);
6.1969 +
6.1970 +val return_Specify_Step_check =
6.1971 + Applicable.Yes (Tactic.Specify_Method' (mID, o_model, I_Model.TEST_to_OLD i_model));
6.1972 +"~~~~~ fun Specify_Step.check \<longrightarrow>fun Step.check \<longrightarrow>fun Step.by_tactic , return:"; val (Applicable.Yes tac') =
6.1973 + (Applicable.Yes (Tactic.Specify_Method' (mID, o_model, I_Model.TEST_to_OLD i_model)));
6.1974 + (*if*) Tactic.for_specify' tac' (*then*);
6.1975 + val ("ok", ([], [], (_, _))) =
6.1976 +
6.1977 +Step_Specify.by_tactic tac' ptp;
6.1978 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =
6.1979 + (tac', ptp);
6.1980 + val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
6.1981 + ...} = Calc.specify_data (pt, pos);
6.1982 + val (dI, _, mID) = References.select_input o_refs refs;
6.1983 + val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
6.1984 + val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
6.1985 + val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
6.1986 + val thy = ThyC.get_theory @{context} dI
6.1987 + val (_, (i_model, _)) = M_Match.match_itms_oris ctxt o_model'
6.1988 + (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_meth) (m_patt, where_, where_rls);
6.1989 + val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', I_Model.TEST_to_OLD i_model))
6.1990 + (Istate_Def.Uistate, ctxt') (pt, pos)
6.1991 +
6.1992 +(*/------------------- check result of Step_Specify.by_tactic ------------------------------\*)
6.1993 +(*+*)val {origin = (o_model, _, _), meth, ...} = Calc.specify_data (pt, pos);
6.1994 +(*+*)O_Model.to_string @{context} o_model;
6.1995 +(*+*)val "[\n(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [M_b 0 = 0, y 0 = 0, y L = 0, M_b L = 0] , pen2str), \n(0 ,[1] ,false ,i_model_empty ,Sup FunktionsVariable), \n(0 ,[1] ,false ,i_model_empty ,Sup AbleitungBiegelinie), \n(0 ,[1] ,false ,i_model_empty ,Sup Biegemoment), \n(0 ,[1] ,false ,i_model_empty ,Sup Querkraft), \n(0 ,[1] ,false ,i_model_empty ,Sup GleichungsVariablen []), \n(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str)]"
6.1996 + = I_Model.to_string @{context} meth
6.1997 +(*\------------------- check result of Step_Specify.by_tactic ------------------------------/*)
6.1998 +(*\------------------- step into Step.by_tactic /////////////////////////////////////////////*)
6.1999 +
6.2000 +val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
6.2001 + Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []) (*of*);
6.2002 +(*/------------------- step into Step.do_next \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)
6.2003 +"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
6.2004 + (p'''''_', ((pt'''''_', Pos.e_pos'), []));
6.2005 + (*if*) Pos.on_calc_end ip (*else*);
6.2006 + val (_, probl_id, _) = Calc.references (pt, p);
6.2007 + val _ = (*case*) tacis (*of*);
6.2008 + (*if*) probl_id = Problem.id_empty (*else*);
6.2009 +
6.2010 +val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
6.2011 + switch_specify_solve p_ (pt, ip);
6.2012 +"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
6.2013 + (*if*) Pos.on_specification ([], state_pos) (*then*);
6.2014 +
6.2015 +val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], [], (pt'''''_'', p'''''_''))) =
6.2016 + Step.specify_do_next (pt, input_pos);
6.2017 +(*/------------------- check result of specify_do_next -------------------------------------\*)
6.2018 +(*+*)val {origin = (ooo_mod, _, _), meth, ...} = Calc.specify_data (pt'''''_'', p'''''_'');
6.2019 +(*+*) O_Model.to_string @{context} ooo_mod; "result of Step_Specify.by_tactic o_model CHANGED";
6.2020 +(*+*)val "[\n(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [M_b 0 = 0, y 0 = 0, y L = 0, M_b L = 0] , pen2str), \n(0 ,[1] ,false ,i_model_empty ,Sup AbleitungBiegelinie), \n(0 ,[1] ,false ,i_model_empty ,Sup Biegemoment), \n(0 ,[1] ,false ,i_model_empty ,Sup Querkraft), \n(0 ,[1] ,false ,i_model_empty ,Sup GleichungsVariablen []), \n(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x , pen2str)]"
6.2021 + = I_Model.to_string @{context} meth;
6.2022 +(*\------------------- check result of specify_do_next -------------------------------------/*)
6.2023 +"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
6.2024 +
6.2025 +(**)val (_, (p_', Add_Given "FunktionsVariable x")) =(**)
6.2026 + Specify.find_next_step ptp;
6.2027 +"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
6.2028 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
6.2029 + spec = refs, ...} = Calc.specify_data (pt, pos);
6.2030 + val ctxt = Ctree.get_ctxt pt pos;
6.2031 + (*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);
6.2032 + (*if*) p_ = Pos.Pbl (*else*);
6.2033 +
6.2034 +val return_XXX = for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to_TEST met);
6.2035 +"~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
6.2036 + (oris, (o_refs, refs), (pbl, met));
6.2037 + val cmI = if mI = MethodC.id_empty then mI' else mI;
6.2038 + val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
6.2039 + val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
6.2040 +"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return_XXX);
6.2041 +(*/------------------- check within find_next_step -----------------------------------------\*)
6.2042 +(*+*)Model_Pattern.to_string @{context} (MethodC.from_store ctxt mI' |> #model) = "[\"" ^
6.2043 + "(#Given, (Traegerlaenge, l))\", \"" ^
6.2044 + "(#Given, (Streckenlast, q))\", \"" ^
6.2045 + "(#Given, (FunktionsVariable, v))\", \"" ^ (* <---------- take m_field from here !!!*)
6.2046 + "(#Given, (GleichungsVariablen, vs))\", \"" ^
6.2047 + "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
6.2048 + "(#Find, (Biegelinie, b))\", \"" ^
6.2049 + "(#Relate, (Randbedingungen, s))\"]";
6.2050 +(*\------------------- check within find_next_step -----------------------------------------/*)
6.2051 +
6.2052 +val return_item_to_add as SOME ("#Given", "FunktionsVariable x") =
6.2053 + (*case*) item_to_add ctxt oris (I_Model.OLD_to_TEST met) (*of*);
6.2054 +"~~~~~ ~ fun item_to_add , args:"; val (thy, oris, _, itms) =
6.2055 + (ctxt, oris, mpc, I_Model.OLD_to_TEST met);
6.2056 +val SOME (fd, ct') = return_item_to_add
6.2057 +
6.2058 +(*+*)val Add_Given "FunktionsVariable x" = P_Model.mk_additem fd ct';
6.2059 +
6.2060 +"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =
6.2061 + ("dummy", (Pos.Met, P_Model.mk_additem fd ct'));
6.2062 + val ist_ctxt = Ctree.get_loc pt (p, p_)
6.2063 + val _ = (*case*) tac (*of*);
6.2064 +
6.2065 + ("dummy",
6.2066 +Step_Specify.by_tactic_input tac (pt, (p, p_'))) (*return from specify_do_next*);
6.2067 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
6.2068 + (tac, (pt, (p, p_')));
6.2069 +
6.2070 + val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
6.2071 + Specify.by_Add_ "#Given" ct ptp (*return from by_tactic_input*);
6.2072 +"~~~~~ ~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
6.2073 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
6.2074 + (*if*) p_ = Pos.Met (*then*);
6.2075 + val (i_model, m_patt) = (met,
6.2076 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
6.2077 +
6.2078 +val Add (5, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =
6.2079 + (*case*)
6.2080 + I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
6.2081 +"~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
6.2082 + (ctxt, m_field, oris, i_model, m_patt, ct);
6.2083 +(*.NEW*) val SOME (t as (descriptor $ _)) = (*case*) ParseC.term_opt ctxt str (*of*);
6.2084 +(*.NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
6.2085 +
6.2086 +val ("", (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), [Free ("x", _)]) =
6.2087 + (*case*)
6.2088 + O_Model.contains ctxt m_field o_model t (*of*);
6.2089 +"~~~~~ ~~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
6.2090 + val ots = ((distinct op =) o flat o (map #5)) ori
6.2091 + val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
6.2092 + val (d, ts) = Input_Descript.split t
6.2093 + val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
6.2094 + (*if*) (subtract op = oids ids) <> [] (*else*);
6.2095 + (*if*) d = TermC.empty (*else*);
6.2096 + (*if*) member op = (map #4 ori) d (*then*);
6.2097 +
6.2098 + associate_input ctxt sel (d, ts) ori;
6.2099 +"~~~~~ ~~~~ fun associate_input , args:"; val (ctxt, m_field, (descript, vals), ((id, vat, m_field', descript', vals') :: oris)) =
6.2100 + (ctxt, sel, (d, ts), ori);
6.2101 +
6.2102 +(*/------------------- check within associate_input ------------------------------------------\*)
6.2103 +(*+*)val Add_Given "FunktionsVariable x" = tac;
6.2104 +(*+*)m_field = "#Given";
6.2105 +(*+*)val Const (\<^const_name>\<open>FunktionsVariable\<close>, _) = descript;
6.2106 +(*+*)val [Free ("x", _)] = vals;
6.2107 +(*+*)O_Model.to_string @{context} ori = "[\n" ^
6.2108 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
6.2109 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
6.2110 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
6.2111 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
6.2112 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
6.2113 + "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
6.2114 + "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";
6.2115 +(*+*)val (id, vat, m_field', descript', vals') = nth 5 ori
6.2116 +(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) =
6.2117 + (id, vat, m_field', descript', vals')
6.2118 +(*\------------------- check within associate_input ----------------------------------------/*)
6.2119 +\<close> ML \<open>(*\\------------ step into Step.by_tactic -------------------------------------------//*)
6.2120 +(*\\------------------ step into Step.by_tactic -------------------------------------------//*)
6.2121 +\<close> ML \<open>(*\------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2-------//*)
6.2122 +(*\------------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2-------//*)
6.2123 +(*[], Met*)val (p,_,f,nxt,_,pt) = return_me_Specify_Method_IntegrierenUndKonstanteBestimmen2
6.2124 + val Add_Given "FunktionsVariable x" = nxt;
6.2125 +
6.2126 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
6.2127 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt
6.2128 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt
6.2129 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c]" = nxt
6.2130 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2]" = nxt
6.2131 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3]" = nxt
6.2132 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c_2, c, c_3, c_4]" = nxt
6.2133 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
6.2134 +
6.2135 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
6.2136 +(*/------------------- check entry to me Model_Problem -------------------------------------\*)
6.2137 +(*+*)val ([1], Pbl) = p;
6.2138 +(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
6.2139 + get_obj g_origin pt (fst p);
6.2140 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
6.2141 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
6.2142 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
6.2143 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
6.2144 +(*
6.2145 +.. here the O_Model does NOT know, which MethodC will be chosen,
6.2146 +so "belastung_zu_biegelinie q__q v_v b_b id_abl" is NOT known,
6.2147 +"b_b" and "id_abl" are NOT missing.
6.2148 +*)
6.2149 +then () else error "[Biegelinien, ausBelastung] initial O_Model CHANGED";
6.2150 +(*\------------------- check entry to me Model_Problem -------------------------------------/*)
6.2151 +
6.2152 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
6.2153 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
6.2154 +\<close> ML \<open>
6.2155 +\<close> ML \<open>(*ERROR isalist2list applied to NON-list: funs'''*)
6.2156 +(*//################## @ {context} within fun XXXXX ---------------------------------------\\* )
6.2157 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Funktionen funs'''":*)
6.2158 +
6.2159 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
6.2160 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
6.2161 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["Biegelinien", "ausBelastung"]*)
6.2162 +
6.2163 +(*[1], Met*)val return_me_Specify_Method_ausBelastung = me nxt p c pt; (*\<rightarrow>Add_Given "Biegelinie y"*)
6.2164 +(*//------------------ step into me_Specify_Method_ausBelastung ----------------------------\\*)
6.2165 +(*+*)val Specify_Method ["Biegelinien", "ausBelastung"] = nxt;
6.2166 +(*+*)(* by \<up> \<up> \<up> \<up> "b_b" and "id_abl" must be requested: PUT THEM INTO O_Model*)
6.2167 +
6.2168 +"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
6.2169 +
6.2170 + val ("ok", ([], [], (_, _))) = (*case*)
6.2171 + Step.by_tactic tac (pt, p) (*of*);
6.2172 +"~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
6.2173 + val Applicable.Yes tac' = (*case*) check tac (pt, p) (*of*);
6.2174 + (*if*) Tactic.for_specify' tac' (*then*);
6.2175 +
6.2176 + val ("ok", ([], [], (_, _))) =
6.2177 +Step_Specify.by_tactic tac' ptp;
6.2178 +(*/------------------- initial check for Step_Specify.by_tactic ----------------------------\*)
6.2179 +(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
6.2180 + get_obj g_origin pt (fst p);
6.2181 +(*+*)if O_Model.to_string ctxt o_model = "[\n" ^
6.2182 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
6.2183 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
6.2184 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
6.2185 +(*
6.2186 +.. here the MethodC has been determined by the user,
6.2187 +so "belastung_zu_biegelinie q__q v_v b_b id_abl" IS KNOWN and,
6.2188 +"b_b" and "id_abl" WOULD BE missing (added by O_Model.).
6.2189 +*)
6.2190 +then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC";
6.2191 +(*\------------------- initial check for Step_Specify.by_tactic ----------------------------/*)
6.2192 +"~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =
6.2193 + (tac', ptp);
6.2194 +(*.NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
6.2195 +(*.NEW*) ...} =Calc.specify_data (pt, pos);
6.2196 +(*.NEW*) val (dI, _, mID) = References.select_input o_refs refs;
6.2197 +(*.NEW*) val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
6.2198 +(*.NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
6.2199 +(*.NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt);
6.2200 +
6.2201 +(*/------------------- check for entry to O_Model.complete_for -----------------------------\*)
6.2202 +(*+*)if mID = ["Biegelinien", "ausBelastung"]
6.2203 +(*+*)then () else error "MethodC [Biegelinien, ausBelastung] CHANGED";
6.2204 +(*+*)if Model_Pattern.to_string ctxt m_patt = "[\"" ^
6.2205 + "(#Given, (Streckenlast, q__q))\", \"" ^
6.2206 + "(#Given, (FunktionsVariable, v_v))\", \"" ^
6.2207 + "(#Given, (Biegelinie, b_b))\", \"" ^
6.2208 + "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
6.2209 + "(#Given, (Biegemoment, id_momentum))\", \"" ^
6.2210 + "(#Given, (Querkraft, id_lat_force))\", \"" ^
6.2211 + "(#Find, (Funktionen, fun_s))\"]"
6.2212 +(*+*)then () else error "[Biegelinien, ausBelastung] Model_Pattern CHANGED";
6.2213 +(*+*)if O_Model.to_string ctxt o_model = "[\n" ^
6.2214 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
6.2215 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
6.2216 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
6.2217 +(*+*)then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC CHANGED";
6.2218 +(*+*) O_Model.to_string ctxt root_model;
6.2219 +(*+*) O_Model.to_string ctxt o_model';
6.2220 + "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
6.2221 +(*\------------------- check for entry to O_Model.complete_for -----------------------------/*)
6.2222 +
6.2223 + O_Model.complete_for m_patt root_model (o_model, ctxt);
6.2224 +"~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) =
6.2225 + (m_patt, root_model, (o_model, ctxt));
6.2226 + val missing = m_patt |> filter_out
6.2227 + (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor))
6.2228 +;
6.2229 + val add = root_model
6.2230 + |> filter
6.2231 + (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor)
6.2232 +;
6.2233 + (o_model @ add
6.2234 +(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
6.2235 +(*NEW*)
6.2236 + |> map (fn (_, b, c, d, e) => (b, c, d, e))
6.2237 + |> add_enumerate
6.2238 + |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
6.2239 + ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from O_Model.complete_for*);
6.2240 +"~~~~ from fun O_Model.complete_for \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =
6.2241 + ((o_model @ add)
6.2242 +(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
6.2243 +(*NEW*)
6.2244 + |> map (fn (_, b, c, d, e) => (b, c, d, e))
6.2245 + |> add_enumerate
6.2246 + |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
6.2247 + ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));
6.2248 +
6.2249 +(*/------------------- check within O_Model.complete_for -------------------------------------------\*)
6.2250 +(*+*) O_Model.to_string ctxt o_model';
6.2251 + "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
6.2252 +(*\------------------- check within O_Model.complete_for -------------------------------------------/*)
6.2253 +
6.2254 +(*.NEW*) val thy = ThyC.get_theory ctxt dI
6.2255 +(*.NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
6.2256 +(*.NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
6.2257 +(*.NEW*) (Istate_Def.Uistate, ctxt') (pt, pos)
6.2258 +;
6.2259 +(*+*) I_Model.to_string ctxt i_model; "[Biegelinien, ausBelastung] I_Model CHANGED 1";
6.2260 +(*+*)val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt, ...} =
6.2261 +(*+*) Calc.specify_data (pt, pos);
6.2262 +(*+*)pos = ([1], Met);
6.2263 +
6.2264 + ("ok", ([], [], (pt, pos))) (*return from Step_Specify.by_tactic*);
6.2265 +"~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =
6.2266 + ("ok", ([], [], (pt, pos)));
6.2267 +(* val ("helpless", ([(xxxxx, _, _)], _, _)) = (*case*)*)
6.2268 + (* SHOULD BE \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> Add_Given "Biegelinie y" | Add_Given "AbleitungBiegelinie dy"*)
6.2269 +
6.2270 +val ("ok", ([( Add_Given "Biegelinie y", _, _)], [], _)) =
6.2271 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
6.2272 +"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
6.2273 +(*.NEW*)(*if*) on_calc_end ip (*else*);
6.2274 +(*.NEW*) val (_, probl_id, _) = Calc.references (pt, p);
6.2275 +(*-"-*) val _ = (*case*) tacis (*of*);
6.2276 +(*.NEW*) (*if*) probl_id = Problem.id_empty (*else*);
6.2277 +
6.2278 +(*.NEW*)val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
6.2279 + switch_specify_solve p_ (pt, ip);
6.2280 +"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
6.2281 + (*if*) Pos.on_specification ([], state_pos) (*then*);
6.2282 +
6.2283 + val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
6.2284 + specify_do_next (pt, input_pos);
6.2285 +"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
6.2286 +
6.2287 + val (_, (p_', tac)) =
6.2288 + Specify.find_next_step ptp;
6.2289 +"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
6.2290 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
6.2291 + spec = refs, ...} = Calc.specify_data (pt, pos);
6.2292 + val ctxt = Ctree.get_ctxt pt pos
6.2293 +;
6.2294 +(*+*)O_Model.to_string ctxt oris = "[\n" ^
6.2295 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
6.2296 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
6.2297 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
6.2298 + "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
6.2299 + "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
6.2300 +(*+*)val (true, []) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_TEST pbl) (Pos.Met, mI');
6.2301 +(*+*)I_Model.to_string ctxt met = "[\n" ^
6.2302 + "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
6.2303 + "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
6.2304 + "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
6.2305 + "(4 ,[1] ,false ,#Given ,Mis Biegelinie b_b), \n" ^
6.2306 + "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
6.2307 +
6.2308 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
6.2309 + (*if*) p_ = Pos.Pbl (*else*);
6.2310 +val return = for_method ctxt oris (o_refs, refs) (pbl, met);
6.2311 +"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
6.2312 +
6.2313 + val ist_ctxt = Ctree.get_loc pt (p, p_)
6.2314 + val Add_Given "Biegelinie y" = (*case*) tac (*of*);
6.2315 +val return = Step_Specify.by_tactic_input tac (pt, (p, p_'));
6.2316 +(*+*)val Add_Given "Biegelinie y" = tac;
6.2317 + val ist_ctxt = Ctree.get_loc pt (p, p_)
6.2318 + val _ = (*case*) tac (*of*);
6.2319 +
6.2320 + val (_, ([(Add_Given "Biegelinie y", _, _)], _, (p'''''_'', ([1], Met)))) =
6.2321 +Step_Specify.by_tactic_input tac (pt, (p, p_'))
6.2322 +(*/------------------- check result of Step_Specify.by_tactic_input ------------------------\*)
6.2323 +(*+*)val {meth, ...} = Calc.specify_data (p'''''_'', ([1], Met));
6.2324 +(*+*)I_Model.to_string ctxt meth = "[\n" ^ (* result does NOT show Add_Given "Biegelinie y" *)
6.2325 + "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
6.2326 + "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
6.2327 + "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
6.2328 + "(4 ,[1] ,false ,#Given ,Mis Biegelinie b_b), \n" ^
6.2329 + "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
6.2330 +(*\------------------- check result of Step_Specify.by_tactic_input ------------------------/*)
6.2331 +"~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) = (tac, (pt, (p, p_')));
6.2332 +
6.2333 + Specify.by_Add_ "#Given" ct ptp;
6.2334 +"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
6.2335 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
6.2336 + (*if*) p_ = Pos.Met (*then*);
6.2337 + val (i_model, m_patt) = (met,
6.2338 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
6.2339 +val Add (4, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]), (Free ("b_b", _), [Free ("y", _)]))) =
6.2340 + (*case*)
6.2341 + check_single ctxt m_field oris i_model m_patt ct (*of*);
6.2342 +
6.2343 +(*/------------------- check for entry to check_single -------------------------------------\*)
6.2344 +(*+*) O_Model.to_string @{context} oris; "[Biegelinien, ausBelastung] O_Model CHANGED for entry";
6.2345 +(*+*) I_Model.to_string ctxt met; "[Biegelinien, ausBelastung] I_Model CHANGED for entry";
6.2346 +(*\------------------- check for entry to check_single -------------------------------------/*)
6.2347 +
6.2348 +"~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
6.2349 + (ctxt, sel, oris, met, ((#model o MethodC.from_store ctxt) cmI), ct);
6.2350 + val SOME t = (*case*) ParseC.term_opt ctxt str (*of*);
6.2351 +
6.2352 +(*+*)val Const (\<^const_name>\<open>Biegelinie\<close>, _) $ Free ("y", _) = t;
6.2353 +(*("associate_input: input ('Biegelinie y') not found in oris (typed)", (0, [], "#Given", Const (\<^const_name>\<open>Biegelinie\<close>, "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]), [])*)
6.2354 +
6.2355 + (*case*)
6.2356 + contains ctxt m_field o_model t (*of*);
6.2357 +"~~~~~ ~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
6.2358 + val ots = ((distinct op =) o flat o (map #5)) ori
6.2359 + val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
6.2360 + val (d, ts) = Input_Descript.split t
6.2361 + val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
6.2362 + (*if*) (subtract op = oids ids) <> [] (*else*);
6.2363 + (*if*) d = TermC.empty (*else*);
6.2364 + (*if*) not (subset op = (map make_typeless ts, map make_typeless ots)) (*else*);
6.2365 +
6.2366 + (*case*) O_Model.associate_input' ctxt sel ts ori (*of*);
6.2367 +"~~~~~ ~~~ fun associate_input' , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);
6.2368 +
6.2369 +(*+/---------------- bypass recursion of associate_input' ----------------\*)
6.2370 +(*+*)O_Model.to_string ctxt oris = "[\n" ^
6.2371 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
6.2372 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
6.2373 + "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
6.2374 + "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
6.2375 +(*+*)val (id, vat, sel', d, ts') = nth 3 oris; (* 3rd iteration *)
6.2376 +(*+\---------------- bypass recursion of associate_input' ----------------/*)
6.2377 +
6.2378 + (*if*) sel = sel' andalso (inter op = ts ts') <> [] (*else*);
6.2379 +
6.2380 +(*/------------------- check within associate_input' -------------------------------\*)
6.2381 +(*+*)if sel = "#Given" andalso sel' = "#Given"
6.2382 +(*+*)then () else error "associate_input' Model_Pattern CHANGED";
6.2383 +(*BUT: m_field can change from root-Problem to sub-MethodC --------------------vvv*)
6.2384 +(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
6.2385 +(*+*)if (Problem.from_store ctxt ["vonBelastungZu", "Biegelinien"] |> #model |> Model_Pattern.to_string ctxt) = "[\"" ^
6.2386 + "(#Given, (Streckenlast, q_q))\", \"" ^
6.2387 + "(#Given, (FunktionsVariable, v_v))\", \"" ^
6.2388 + "(#Find, (Funktionen, funs'''))\"]"
6.2389 +(*+*)then () else error "associate_input' Model_Pattern of Subproblem CHANGED";
6.2390 +(* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv ------------------------------------- \<up>*)
6.2391 +(*+*)if (Problem.from_store ctxt ["Biegelinien"] |> #model |> Model_Pattern.to_string ctxt) = "[\"" ^
6.2392 + "(#Given, (Traegerlaenge, l_l))\", \"" ^
6.2393 + "(#Given, (Streckenlast, q_q))\", \"" ^
6.2394 + "(#Find, (Biegelinie, b_b))\", \"" ^ (*------------------------------------- \<up> *)
6.2395 + "(#Relate, (Randbedingungen, r_b))\"]"
6.2396 +(*+*)then () else error "associate_input' Model_Pattern root-problem CHANGED";
6.2397 +(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
6.2398 +(*+*)if (MethodC.from_store ctxt ["Biegelinien", "ausBelastung"] |> #model |> Model_Pattern.to_string ctxt) = "[\"" ^
6.2399 + "(#Given, (Streckenlast, q__q))\", \"" ^
6.2400 + "(#Given, (FunktionsVariable, v_v))\", \"" ^
6.2401 + "(#Given, (Biegelinie, b_b))\", \"" ^
6.2402 + "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
6.2403 + "(#Given, (Biegemoment, id_momentum))\", \"" ^
6.2404 + "(#Given, (Querkraft, id_lat_force))\", \"" ^
6.2405 + "(#Find, (Funktionen, fun_s))\"]"
6.2406 +(*+*)then () else error "associate_input' Model_Pattern CHANGED";
6.2407 +(*+*)if UnparseC.term ctxt d = "Biegelinie" andalso UnparseC.terms ctxt ts = "[y]"
6.2408 +(*+*) andalso UnparseC.terms ctxt ts' = "[y]"
6.2409 +(*+*)then
6.2410 +(*+*) (case (inter op = ts ts') of [Free ("y", _(*"real \<Rightarrow> real"*))] => ()
6.2411 +(*+*) | _ => error "check within associate_input' CHANGED 1")
6.2412 +(*+*)else error "check within associate_input' CHANGED 2";
6.2413 +(*\------------------- check within associate_input' -------------------------------/*)
6.2414 +
6.2415 +(*|------------------- contine me_Specify_Method_ausBelastung --------------------------------*)
6.2416 +(*\------------------- step into me_Specify_Method_ausBelastung ----------------------------//*)
6.2417 +(*[1], Met*)val (p,_,f,nxt,_,pt) = return_me_Specify_Method_ausBelastung;
6.2418 + val Add_Given "Biegelinie y" = nxt
6.2419 +
6.2420 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy"= nxt
6.2421 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt
6.2422 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt
6.2423 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Biegelinien", "ausBelastung"] = nxt
6.2424 +
6.2425 +(*[1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("sym_neg_equal_iff_equal", _)= nxt
6.2426 +(*[1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("Belastung_Querkraft", _)= nxt
6.2427 +(*[1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"])= nxt
6.2428 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Model_Problem= nxt
6.2429 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "functionTerm (- q_0)"= nxt
6.2430 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "integrateBy x"= nxt
6.2431 +;
6.2432 +(*/------------------- check result of Add_Given "functionTerm (- q_0)" --------------------\*)
6.2433 +if p = ([1, 3], Pbl) andalso
6.2434 + f = Test_Out.PpcKF (Test_Out.Problem [], {Find = [Incompl "antiDerivativeName"],
6.2435 + Given = [Correct "functionTerm (- q_0)", Incompl "integrateBy"],
6.2436 + Relate = [], Where = [], With = []})
6.2437 +then
6.2438 + (case nxt of Add_Given "integrateBy x" => () | _ => error "specify-phase: low level CHANGED 1")
6.2439 +else error "specify-phase: low level CHANGED 2";
6.2440 +(*\------------------- check result of Add_Given "functionTerm (- q_0)" --------------------/*)
6.2441 +( *\\################# @ {context} within fun XXXXX ----------------------------------------//*)
6.2442 +
6.2443
6.2444 \<close> ML \<open>
6.2445 \<close>