1.1 --- a/test/Tools/isac/Specify/sub-problem.sml Sun Nov 19 07:51:41 2023 +0100
1.2 +++ b/test/Tools/isac/Specify/sub-problem.sml Mon Nov 20 10:49:54 2023 +0100
1.3 @@ -13,6 +13,9 @@
1.4 "-----------------------------------------------------------------------------------------------";
1.5 "-----------------------------------------------------------------------------------------------";
1.6
1.7 +open Tactic
1.8 +open Pos
1.9 +open Test_Code;
1.10
1.11 "----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";
1.12 "----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";
1.13 @@ -41,13 +44,10 @@
1.14 ],
1.15 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
1.16
1.17 - val (tac as Model_Problem (*["vonBelastungZu", "Biegelinien"]*), (pt, p as ([1], Pbl))) =
1.18 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
1.19 - (*---broken elementwise input to lists---* ) |> me'( *---broken elementwise input to lists---*)
1.20 - (*INVISIBLE: SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
1.21 - |> me'
1.22 - (*with new formal arguments..*) |> me' |> me';
1.23 -
1.24 +val (tac as Model_Problem (*["vonBelastungZu", "Biegelinien"]*), (pt, p as ([1], Pbl))) =
1.25 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
1.26 + |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
1.27 +;
1.28
1.29 "----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";
1.30 "----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";
1.31 @@ -66,17 +66,14 @@
1.32 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
1.33
1.34 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, refs)];
1.35 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Model_Problem*)
1.36 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "Traegerlaenge L"*)
1.37 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "Streckenlast q_0"*)
1.38 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac
1.39 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "Traegerlaenge L" = tac
1.40 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "Streckenlast q_0" = tac
1.41 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Find "Biegelinie y" = tac
1.42 -
1.43 -(*/---broken elementwise input to lists---\* )
1.44 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Relation "Randbedingungen [y 0 = 0]" = tac
1.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
1.46 -( *\---broken elementwise input to lists---/*)
1.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
1.48 -
1.49 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Relation "Randbedingungen [y 0 = 0, y L = 0]" = tac
1.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
1.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
1.52 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Theory "Biegelinie" = tac
1.53 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Problem ["Biegelinien"] = tac
1.54 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac
1.55 @@ -84,7 +81,12 @@
1.56 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "AbleitungBiegelinie dy" = tac
1.57 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "Biegemoment M_b" = tac
1.58 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "Querkraft Q" = tac
1.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
1.60 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "GleichungsVariablen [c]" = tac
1.61 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "GleichungsVariablen [c, c_2]" = tac
1.62 +(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "GleichungsVariablen [c, c_2, c_3]" = tac
1.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
1.64 +
1.65 +val Add_Given "GleichungsVariablen [c_2, c, c_3, c_4]" = tac
1.66 (*[1], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = tac
1.67 (*INVISIBLE: \<rightarrow>SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
1.68 (*[1], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac