(* Title:  "Interpret/sub-problem.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";

"----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";

"----------- fun common_sub_thy for Sub_Problem ------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

open Tactic

open Pos

open Test_Code;

"----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";

"----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";

"----------- TODO: make steps around Subproblem more helpful: me' ------------------------------";

(* compare biegelinie-4.sml *)

val (tac as Model_Problem (*["Biegelinien"]*), (pt, p as ([], Pbl))) =

Test_Code.init_calc' @{context} [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

	    "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

(*

  Now follow items for ALL SubProblems,

  since ROOT MethodC must provide values for "actuals" of ALL SubProblems.

  See Biegelinie.thy subsection \<open>Survey on Methods\<close>.

*)

(*

  Items for MethodC "IntegrierenUndKonstanteBestimmen2"

*)

	    "FunktionsVariable x",

    (*"Biegelinie y",          ..already input for Problem above*)

      "AbleitungBiegelinie dy",

      "Biegemoment M_b",

      "Querkraft Q",

(*

  Item for Problem "LINEAR/system", which by [''no_met''] involves refinement

*)

      "GleichungsVariablen [c, c_2, c_3, c_4]"

],

("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]

val (tac as Model_Problem (*["vonBelastungZu", "Biegelinien"]*), (pt, p as ([1], Pbl))) =

  (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'

  |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'

;

"----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";

"----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";

"----------- TODO: make steps around Subproblem more helpful: Step.do_next ---------------------";

val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

	    "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

	    "FunktionsVariable x",

    (*"Biegelinie y",          ..already input for Problem above*)

      "AbleitungBiegelinie dy",

      "Biegemoment M_b",

      "Querkraft Q",

      "GleichungsVariablen [c, c_2, c_3, c_4]"

];

val refs =

  ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);

(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, refs)];

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "Traegerlaenge L" = tac

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "Streckenlast q_0" = tac

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Find "Biegelinie y" = tac

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Relation "Randbedingungen [y 0 = 0]" = tac

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Relation "Randbedingungen [y 0 = 0, y L = 0]" = tac

(*[], 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

(*[], 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

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Theory "Biegelinie" = tac

(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Problem ["Biegelinien"] = tac

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "FunktionsVariable x" = tac

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "AbleitungBiegelinie dy" = tac

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "Biegemoment M_b" = tac

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "Querkraft Q" = tac

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "GleichungsVariablen [c]" = tac

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "GleichungsVariablen [c, c_2]" = tac

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Given "GleichungsVariablen [c, c_2, c_3]" = tac

(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val  Add_Given "GleichungsVariablen [c_2, c, c_3, c_4]" = tac

val Add_Given "GleichungsVariablen [c_2, c, c_3, c_4]" = tac

(*[1], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = tac

            (*INVISIBLE: \<rightarrow>SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)

(*[1], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac

;

"----------- fun common_sub_thy for Sub_Problem ------------------------------------------------";

"----------- fun common_sub_thy for Sub_Problem ------------------------------------------------";

"----------- fun common_sub_thy for Sub_Problem ------------------------------------------------";

val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory Inverse_Z_Transform});

if Context.theory_name (Sub_Problem.common_sub_thy (thy1, thy2)) = "Inverse_Z_Transform"

then () else error "common_sub_thy 1";

val (thy1, thy2) = (@{theory Inverse_Z_Transform}, @{theory Partial_Fractions});

if Context.theory_name (Sub_Problem.common_sub_thy (thy1, thy2)) = "Inverse_Z_Transform"

then () else error "common_sub_thy 2";

val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory PolyEq});

if Context.theory_name (Sub_Problem.common_sub_thy (thy1, thy2)) =

     Context.theory_name (Know_Store.get_ref_last_thy ())

(*   Context.theory_name @{theory} ... would make the test dependent from where the test is run,

                                       e.g. Test_Some.thy or Test_Isac.thy                     *)

then () else error "common_sub_thy 3";

val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory Isac_Knowledge});

if Context.theory_name (Sub_Problem.common_sub_thy (thy1, thy2)) = "Isac_Knowledge"

then () else error "common_sub_thy 4";

val (thy1, thy2) = (@{theory PolyEq}, @{theory Partial_Fractions});

if Context.theory_name (Sub_Problem.common_sub_thy (thy1, thy2)) =

     Context.theory_name (Know_Store.get_ref_last_thy ())

(*   Context.theory_name @{theory} ... would make the test dependent from where the test is run,

                                       e.g. Test_Some.thy or Test_Isac.thy                     *)

then () else error "common_sub_thy 5";

val (thy1, thy2) = (@{theory Isac_Knowledge}, @{theory Partial_Fractions});

if Context.theory_name (Sub_Problem.common_sub_thy (thy1, thy2)) = "Isac_Knowledge"

then () else error "common_sub_thy 6";