1.1 --- a/src/Tools/isac/TODO.thy	Mon Jun 29 17:33:47 2020 +0200
     1.2 +++ b/src/Tools/isac/TODO.thy	Mon Jun 29 18:05:04 2020 +0200
     1.3 @@ -63,6 +63,15 @@
     1.4  text \<open>
     1.5    \begin{itemize}
     1.6    \item xxx
     1.7 +  \item make steps around SubProblem more consistent:
     1.8 +    SubProblem (thy, [pbl]) is bypassed by Model_Problem, if it is 1st Tactic in a Program.
     1.9 +    Design:
    1.10 +    * the Tactic SubProblem (thy, [pbl]) creates the formula SubProblem (thy, [pbl])
    1.11 +      (only the headline !)
    1.12 +    * the Tactic Model_Problem starts Specification
    1.13 +      (with an empty Model)
    1.14 +    see test/../sub-problem.sml
    1.15 +  \item xxx
    1.16    \item Specify_Step.add has dummy argument Istate_Def.Uistate -- remove down to Ctree
    1.17    \item xxx
    1.18    \item Step_Specify.by_tactic (Tactic.Model_Problem' (id, _, met))

     2.1 --- a/test/Tools/isac/Interpret/sub-problem.sml	Mon Jun 29 17:33:47 2020 +0200
     2.2 +++ b/test/Tools/isac/Interpret/sub-problem.sml	Mon Jun 29 18:05:04 2020 +0200
     2.3 @@ -6,12 +6,52 @@
     2.4  "-----------------------------------------------------------------------------------------------";
     2.5  "table of contents -----------------------------------------------------------------------------";
     2.6  "-----------------------------------------------------------------------------------------------";
     2.7 -"----------- TODO ------------------------------------------------------------------------------";
     2.8 +"----------- TODO: make steps around Subproblem more consistent: me' ---------------------------";
     2.9 +"----------- TODO: make steps around Subproblem more consistent: Step.do_next ------------------";
    2.10  "-----------------------------------------------------------------------------------------------";
    2.11  "-----------------------------------------------------------------------------------------------";
    2.12  "-----------------------------------------------------------------------------------------------";
    2.13  
    2.14  
    2.15 -"----------- TODO ------------------------------------------------------------------------------";
    2.16 -"----------- TODO ------------------------------------------------------------------------------";
    2.17 -"----------- TODO ------------------------------------------------------------------------------";
    2.18 +"----------- TODO: make steps around Subproblem more consistent --------------------------------";
    2.19 +"----------- TODO: make steps around Subproblem more consistent --------------------------------";
    2.20 +"----------- TODO: make steps around Subproblem more consistent --------------------------------";
    2.21 +(* compare biegelinie-4.sml *)
    2.22 +val (tac as Model_Problem (*["Biegelinien"]*), (pt, p as ([], Pbl))) =
    2.23 +CalcTreeTEST' [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
    2.24 +	"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",
    2.25 +  "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"],
    2.26 +("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
    2.27 +
    2.28 +  val (tac as Model_Problem (*["vonBelastungZu", "Biegelinien"]*), (pt, p as ([1], Pbl))) =
    2.29 +  (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
    2.30 +    (*INVISIBLE: SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
    2.31 +    |> me';
    2.32 +
    2.33 +
    2.34 +"----------- TODO: make steps around Subproblem more consistent: Step.do_next ------------------";
    2.35 +"----------- TODO: make steps around Subproblem more consistent: Step.do_next ------------------";
    2.36 +"----------- TODO: make steps around Subproblem more consistent: Step.do_next ------------------";
    2.37 +"----------- TODO: make steps around Subproblem more consistent: Step.do_next ------------------";
    2.38 +
    2.39 +val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
    2.40 +	"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",
    2.41 +  "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"];
    2.42 +val refs =
    2.43 +  ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
    2.44 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, refs)];
    2.45 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Model_Problem*)
    2.46 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "Traegerlaenge L"*)
    2.47 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "Streckenlast q_0"*)
    2.48 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Find "Biegelinie y"*)
    2.49 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]"*)
    2.50 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
    2.51 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Theory "Biegelinie"*)
    2.52 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Problem ["Biegelinien"]*)
    2.53 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "FunktionsVariable x"*)
    2.54 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "FunktionsVariable x"*)
    2.55 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
    2.56 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "AbleitungBiegelinie dy"*)
    2.57 +(*[1], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Apply_Method ["IntegrierenUndKonstanteBestimmen2"]*)
    2.58 +            (*INVISIBLE: \<rightarrow>SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
    2.59 +(*[1], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Model_Problem*)

     3.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml	Mon Jun 29 17:33:47 2020 +0200
     3.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml	Mon Jun 29 18:05:04 2020 +0200
     3.3 @@ -85,7 +85,7 @@
     3.4    val (tac as Model_Problem (*["vonBelastungZu", "Biegelinien"]*), (pt, p as ([1], Pbl))) =
     3.5    (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
     3.6      (*INVISIBLE: SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
     3.7 -    |> me'
     3.8 +    |> me';
     3.9      val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 2], Res))) =
    3.10      (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
    3.11        val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 3, 2], Res))) =