(* chapter 'Biegelinie' from the textbook: 

   Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271.

   author: Walther Neuper 050826,

   (c) due to copyright terms

*)

theory Biegelinie imports Integrate Equation EqSystem Base_Tools begin

consts

  qq    :: "real => real"             (* Streckenlast               *)

  Q     :: "real => real"             (* Querkraft                  *)

  Q'    :: "real => real"             (* Ableitung der Querkraft    *)

  M'_b  :: "real => real" ("M'_b")    (* Biegemoment                *)

  M'_b' :: "real => real" ("M'_b'")   (* Ableitung des Biegemoments *)

  y''   :: "real => real"             (* 2.Ableitung der Biegeline  *)

  y'    :: "real => real"             (* Neigung der Biegeline      *)

(*y     :: "real => real"             (* Biegeline                  *)*)

  EI    :: "real"                     (* Biegesteifigkeit           *)

  (*new Descriptions in the related problems*)

  Traegerlaenge            :: "real => una"

  Streckenlast             :: "real => una"

  BiegemomentVerlauf       :: "bool => una"

  Biegelinie               :: "(real => real) => una"

  AbleitungBiegelinie      :: "(real => real) => una"

  Randbedingungen          :: "bool list => una"

  RandbedingungenBiegung   :: "bool list => una"

  RandbedingungenNeigung   :: "bool list => una"

  RandbedingungenMoment    :: "bool list => una"

  RandbedingungenQuerkraft :: "bool list => una"

  FunktionsVariable        :: "real => una"

  Funktionen               :: "bool list => una"

  Gleichungen              :: "bool list => una"

  GleichungsVariablen      :: "real list => una"

  (*Script-names*)

  Biegelinie2Script        :: "[real, real, real, real => real, real => real, bool list, real list,

				bool] => bool"	

	("((Script Biegelinie2Script (_ _ _ _ _ _ _=))// (_))" 9)

  Biege1xIntegrierenScript :: 

	            "[real,real,real,real=>real,bool list,bool list,bool list,

		      bool] => bool"	

	("((Script Biege1xIntegrierenScript (_ _ _ _ _ _ _ =))// (_))" 9)

  Belastung2BiegelScript   :: "[real,real,real=>real,real=>real,

	                        bool list] => bool list"	

	("((Script Belastung2BiegelScript (_ _ _ _ =))// (_))" 9)

  SetzeRandbedScript       :: "[bool list,bool list,

	                        bool list] => bool list"	

	("((Script SetzeRandbedScript (_ _ =))// (_))" 9)

axiomatization where

  Querkraft_Belastung:   "Q' x = -qq x" and

  Belastung_Querkraft:   "-qq x = Q' x" and

  Moment_Querkraft:      "M_b' x = Q x" and

  Querkraft_Moment:      "Q x = M_b' x" and

  Neigung_Moment:        "y'' x = -M_b x/ EI" and

  Moment_Neigung:        "M_b x = -EI * y'' x" and

  (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)

  make_fun_explicit:     "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"

setup \<open>

KEStore_Elems.add_thes

  [make_thy @{theory}

    ["Walther Neuper 2005 supported by a grant from NMI Austria"],

  make_isa @{theory} ("IsacKnowledge", "Theorems")

    ["Walther Neuper 2005 supported by a grant from NMI Austria"],

  make_thm @{theory}  "IsacKnowledge" ("Belastung_Querkraft", @{thm Belastung_Querkraft})

	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],

  make_thm @{theory}  "IsacKnowledge" ("Moment_Neigung", @{thm Moment_Neigung})

	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],

  make_thm @{theory}  "IsacKnowledge" ("Moment_Querkraft", @{thm Moment_Querkraft})

	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],

  make_thm @{theory}  "IsacKnowledge" ("Neigung_Moment", @{thm Neigung_Moment})

	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],

  make_thm @{theory}  "IsacKnowledge" ("Querkraft_Belastung", @{thm Querkraft_Belastung})

	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],

  make_thm @{theory}  "IsacKnowledge" ("Querkraft_Moment", @{thm Querkraft_Moment})

	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],

  make_thm @{theory}  "IsacKnowledge" ("make_fun_explicit", @{thm make_fun_explicit})

	  ["Walther Neuper 2005 supported by a grant from NMI Austria"]]

\<close>

(** problems **)

setup \<open>KEStore_Elems.add_pbts

  [(Specify.prep_pbt @{theory} "pbl_bieg" [] Celem.e_pblID

      (["Biegelinien"],

        [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),

          (*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)

          ("#Find"  ,["Biegelinie b_b"]),

          ("#Relate",["Randbedingungen r_b"])],

        Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),

    (Specify.prep_pbt @{theory} "pbl_bieg_mom" [] Celem.e_pblID

      (["MomentBestimmte","Biegelinien"],

        [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),

          (*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)

          ("#Find"  ,["Biegelinie b_b"]),

          ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])

        ],

        Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),

    (Specify.prep_pbt @{theory} "pbl_bieg_momg" [] Celem.e_pblID

      (["MomentGegebene","Biegelinien"], [], Rule.append_rls "e_rls" Rule.e_rls [], NONE,

        [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])),

    (Specify.prep_pbt @{theory} "pbl_bieg_einf" [] Celem.e_pblID

      (["einfache","Biegelinien"], [], Rule.append_rls "e_rls" Rule.e_rls [], NONE,

        [["IntegrierenUndKonstanteBestimmen","4x4System"]])),

    (Specify.prep_pbt @{theory} "pbl_bieg_momquer" [] Celem.e_pblID

      (["QuerkraftUndMomentBestimmte","Biegelinien"], [], Rule.append_rls "e_rls" Rule.e_rls [], NONE,

        [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])),

    (Specify.prep_pbt @{theory} "pbl_bieg_vonq" [] Celem.e_pblID

      (["vonBelastungZu","Biegelinien"],

          [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),

            ("#Find"  ,["Funktionen funs'''"])],

        Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["Biegelinien","ausBelastung"]])),

    (Specify.prep_pbt @{theory} "pbl_bieg_randbed" [] Celem.e_pblID

      (["setzeRandbedingungen","Biegelinien"],

          [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),

            ("#Find"  ,["Gleichungen equs'''"])],

        Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),

    (Specify.prep_pbt @{theory} "pbl_equ_fromfun" [] Celem.e_pblID

      (["makeFunctionTo","equation"],

          [("#Given" ,["functionEq fu_n","substitution su_b"]),

            ("#Find"  ,["equality equ'''"])],

        Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["Equation","fromFunction"]]))]\<close>

ML \<open>

(** methods **)

val srls = Rule.Rls {id="srls_IntegrierenUnd..", 

		preconds = [], 

		rew_ord = ("termlessI",termlessI), 

		erls = Rule.append_rls "erls_in_srls_IntegrierenUnd.." Rule.e_rls

				  [(*for asm in NTH_CONS ...*)

				   Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),

				   (*2nd NTH_CONS pushes n+-1 into asms*)

				   Rule.Calc("Groups.plus_class.plus", eval_binop "#add_")

				   ], 

		srls = Rule.Erls, calc = [], errpatts = [],

		rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),

			 Rule.Calc("Groups.plus_class.plus", eval_binop "#add_"),

			 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),

			 Rule.Calc("Tools.lhs", Tools.eval_lhs"eval_lhs_"),

			 Rule.Calc("Tools.rhs", Tools.eval_rhs"eval_rhs_"),

			 Rule.Calc("Atools.argument'_in",

			      eval_argument_in "Atools.argument'_in")

			 ],

		scr = Rule.EmptyScr};

val srls2 = 

    Rule.Rls {id="srls_IntegrierenUnd..", 

	 preconds = [], 

	 rew_ord = ("termlessI",termlessI), 

	 erls = Rule.append_rls "erls_in_srls_IntegrierenUnd.." Rule.e_rls

			   [(*for asm in NTH_CONS ...*)

			    Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),

			    (*2nd NTH_CONS pushes n+-1 into asms*)

			    Rule.Calc("Groups.plus_class.plus", eval_binop "#add_")

			    ], 

	 srls = Rule.Erls, calc = [], errpatts = [],

	 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),

		  Rule.Calc("Groups.plus_class.plus", eval_binop "#add_"),

		  Rule.Thm ("NTH_NIL", TermC.num_str @{thm NTH_NIL}),

		  Rule.Calc("Tools.lhs", Tools.eval_lhs "eval_lhs_"),

		  Rule.Calc("Atools.filter'_sameFunId",

		       eval_filter_sameFunId "Atools.filter'_sameFunId"),

		  (*WN070514 just for smltest/../biegelinie.sml ...*)

		  Rule.Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),

		  Rule.Thm ("filter_Cons", TermC.num_str @{thm filter_Cons}),

		  Rule.Thm ("filter_Nil", TermC.num_str @{thm filter_Nil}),

		  Rule.Thm ("if_True", TermC.num_str @{thm if_True}),

		  Rule.Thm ("if_False", TermC.num_str @{thm if_False}),

		  Rule.Thm ("hd_thm", TermC.num_str @{thm hd_thm})

		  ],

	 scr = Rule.EmptyScr};

\<close>

section \<open>Methods\<close>

(* setup parent directory *)

setup \<open>KEStore_Elems.add_mets

    [Specify.prep_met @{theory} "met_biege" [] Celem.e_metID 

	    (["IntegrierenUndKonstanteBestimmen"], [],

	    {rew_ord'="tless_true", rls'= Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls =Rule.Erls,

          errpats = [], nrls = Rule.Erls},

      @{thm refl})]

\<close>

subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>

partial_function (tailrec) biegelinie :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> real list \<Rightarrow> bool"

  where

"biegelinie l q v b s vs =

  (let

    funs = SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],

             [''Biegelinien'', ''ausBelastung'']) [REAL q, REAL v];                \<comment> \<open>PROG +args\<close>

    equs = SubProblem (''Biegelinie'', [''setzeRandbedingungen'', ''Biegelinien''],

             [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST s];

    cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''], [''no_met''])

             [BOOL_LIST equs, REAL_LIST vs];     \<comment> \<open>PROG consts\<close>

    B = Take (lastI funs);

    B = ((Substitute cons) @@ (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B                         

  in B)"

setup \<open>KEStore_Elems.add_mets

    [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID

	    (["IntegrierenUndKonstanteBestimmen2"],

	      [("#Given" ,["Traegerlaenge l", "Streckenlast q",

              "FunktionsVariable v", "GleichungsVariablen vs", "AbleitungBiegelinie id_abl"]),

		      (*("#Where",["0 < l"]), ...wait for &lt; and handling Arbfix*)

		      ("#Find"  ,["Biegelinie b"]),

		      ("#Relate",["Randbedingungen s"])],

	      {rew_ord'="tless_true", 

	        rls' = Rule.append_rls "erls_IntegrierenUndK.." Rule.e_rls 

				      [Rule.Calc ("Atools.ident",eval_ident "#ident_"),

				        Rule.Thm ("not_true",TermC.num_str @{thm not_true}),

				        Rule.Thm ("not_false",TermC.num_str @{thm not_false})], 

				  calc = [], 

				  srls = Rule.append_rls "erls_IntegrierenUndK.." Rule.e_rls 

				      [Rule.Calc("Tools.rhs", Tools.eval_rhs"eval_rhs_"),

				        Rule.Calc ("Atools.ident",eval_ident "#ident_"),

				        Rule.Thm ("last_thmI",TermC.num_str @{thm last_thmI}),

				        Rule.Thm ("if_True",TermC.num_str @{thm if_True}),

				        Rule.Thm ("if_False",TermC.num_str @{thm if_False})],

				  prls = Rule.Erls, crls = Atools_erls, errpats = [], nrls = Rule.Erls},

        @{thm biegelinie.simps}

	    (*""Script Biegelinie2Script                                                                           " ^

        "(l::real) (q :: real) (v :: real) (id_abl::real\<Rightarrow>real) (b :: real => real) (s :: bool list) (vs :: real list) = " ^

        "  (let                                                                                             " ^

        "    (funs :: bool list) = (SubProblem (''Biegelinie'',                                             " ^

        "      [''vonBelastungZu'', ''Biegelinien''], [''Biegelinien'', ''ausBelastung''])                  " ^

        "      [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]);                                            " ^

        "    (equs :: bool list) = (SubProblem (''Biegelinie'',                                             " ^

        "      [''setzeRandbedingungen'', ''Biegelinien''], [''Biegelinien'', ''setzeRandbedingungenEin'']) " ^

        "      [BOOL_LIST funs, BOOL_LIST s]);                                                              " ^

        "    (cons :: bool list) = (SubProblem (''Biegelinie'',                                             " ^

        "      [''LINEAR'', ''system''], [''no_met''])                                                      " ^

        "      [BOOL_LIST equs, REAL_LIST vs]);                                                             " ^

        "    B = Take (lastI funs);                                                                         " ^

        "    B = ((Substitute cons) @@                                                                      " ^

        "           (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B                          " ^

        "  in B)                                                                                            "*))]

\<close>

setup \<open>KEStore_Elems.add_mets

    [Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID

	    (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],

	      {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,

          errpats = [], nrls = Rule.e_rls},

        @{thm refl}),

    Specify.prep_met @{theory} "met_biege_intconst_4" [] Celem.e_metID

	    (["IntegrierenUndKonstanteBestimmen","4x4System"], [],

	      {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,

          errpats = [], nrls = Rule.e_rls},

        @{thm refl}),

    Specify.prep_met @{theory} "met_biege_intconst_1" [] Celem.e_metID

	    (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], [],

        {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,

          errpats = [], nrls = Rule.e_rls},

        @{thm refl}),

    Specify.prep_met @{theory} "met_biege2" [] Celem.e_metID

	    (["Biegelinien"], [],

	      {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,

          errpats = [], nrls = Rule.e_rls},

        @{thm refl})]

\<close>

subsection \<open>Compute the general bending line\<close>

partial_function (tailrec) belastung_zu_biegelinie :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list"

  where

"belastung_zu_biegelinie q__q v_v id_fun id_abl =

  (let q___q = Take (qq v_v = q__q);

       q___q = ((Rewrite ''sym_neg_equal_iff_equal'' True) @@

              (Rewrite ''Belastung_Querkraft'' True)) q___q;

       Q__Q = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],

                [''diff'', ''integration'', ''named'']) [REAL (rhs q___q), REAL v_v, REAL_REAL Q];

       M__M = Rewrite ''Querkraft_Moment'' True Q__Q;

       M__M = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],

                [''diff'', ''integration'', ''named'']) [REAL (rhs M__M), REAL v_v, REAL_REAL M_b];

       N__N = ((Rewrite ''Moment_Neigung'' False) @@

               (Rewrite ''make_fun_explicit'' False)) M__M;

       N__N = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],

                  [''diff'', ''integration'', ''named''])

                [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl];                        \<comment> \<open>PROG string\<close>

       B__B = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],

                  [''diff'', ''integration'', ''named'']) 

                [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]                          \<comment> \<open>PROG string\<close>

 in [Q__Q, M__M, N__N, B__B])"

setup \<open>KEStore_Elems.add_mets

    [Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID

	    (["Biegelinien", "ausBelastung"],

	      [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v",

            "Biegelinie id_fun", "AbleitungBiegelinie id_abl"]),

	       ("#Find"  ,["Funktionen fun_s"])],

	      {rew_ord'="tless_true", 

	        rls' = Rule.append_rls "erls_ausBelastung" Rule.e_rls 

				      [Rule.Calc ("Atools.ident", eval_ident "#ident_"),

				        Rule.Thm ("not_true", TermC.num_str @{thm not_true}),

				        Rule.Thm ("not_false", TermC.num_str @{thm not_false})], 

				  calc = [], 

				  srls = Rule.append_rls "srls_ausBelastung" Rule.e_rls 

				      [Rule.Calc ("Tools.rhs", Tools.eval_rhs "eval_rhs_")], 

				  prls = Rule.e_rls, crls = Atools_erls, errpats = [], nrls = Rule.e_rls},

        @{thm belastung_zu_biegelinie.simps}

	    (*"Script Belastung2BiegelScript (q__q::real) (v_v::real) (id_fun::real\<Rightarrow>real) (id_abl::real\<Rightarrow>real) = " ^

          "  (let q___q = Take (qq v_v = q__q);                                                " ^

          "       q___q = ((Rewrite ''sym_neg_equal_iff_equal'' True) @@                       " ^

          "              (Rewrite ''Belastung_Querkraft'' True)) q___q;                        " ^

          "      (Q__Q:: bool) =                                                               " ^

          "             (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''],    " ^

          "                          [''diff'',''integration'',''named''])                     " ^

          "                          [REAL (rhs q___q), REAL v_v, REAL_REAL Q]);               " ^

          "       M__M = Rewrite ''Querkraft_Moment'' True Q__Q;                               " ^

          "      (M__M::bool) =                                                                " ^

          "             (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''],    " ^

          "                          [''diff'',''integration'',''named''])                     " ^

          "                          [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]);              " ^

          "       N__N = ((Rewrite ''Moment_Neigung'' False) @@                                " ^

          "              (Rewrite ''make_fun_explicit'' False)) M__M;                          " ^

          "      (N__N:: bool) =                                                               " ^

          "             (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''],    " ^

          "                          [''diff'',''integration'', ''named''])                    " ^

          "                          [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl]);           " ^

          "      (B__B:: bool) =                                                               " ^

          "             (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''],    " ^

          "                          [''diff'',''integration'',''named''])                     " ^

          "                          [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun])            " ^

          " in [Q__Q, M__M, N__N, B__B])                                                       "*))]

\<close>

subsection \<open>Substitute the constraints into the equations\<close>

partial_function (tailrec) setzte_randbedingungen :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"

  where 

"setzte_randbedingungen fun_s r_b =

 (let b_1 = NTH 1 r_b;

      f_s = filter_sameFunId (lhs b_1) fun_s;

      e_1 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],

              [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_1];

      b_2 = NTH 2 r_b;

      f_s = filter_sameFunId (lhs b_2) fun_s;

      e_2 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],

               [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_2];

      b_3 = NTH 3 r_b;

      f_s = filter_sameFunId (lhs b_3) fun_s;

      e_3 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],

               [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_3];

      b_4 = NTH 4 r_b;

      f_s = filter_sameFunId (lhs b_4) fun_s;

      e_4 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],

               [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_4]

 in [e_1, e_2, e_3, e_4])"

setup \<open>KEStore_Elems.add_mets

    [Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID

	    (["Biegelinien", "setzeRandbedingungenEin"],

	      [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),

	        ("#Find"  , ["Gleichungen equs'''"])],

	      {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = srls2, prls=Rule.e_rls, crls = Atools_erls,

          errpats = [], nrls = Rule.e_rls},

        @{thm setzte_randbedingungen.simps}

	    (*"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^

          " (let b_1 = NTH 1 r_b;                                         " ^

          "      f_s = filter_sameFunId (lhs b_1) fun_s;                   " ^

          "      (e_1::bool) =                                             " ^

          "             (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^

          "                          [''Equation'',''fromFunction''])              " ^

          "                          [BOOL (hd f_s), BOOL b_1]);         " ^

          "      b_2 = NTH 2 r_b;                                         " ^

          "      f_s = filter_sameFunId (lhs b_2) fun_s;                   " ^

          "      (e_2::bool) =                                             " ^

          "             (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^

          "                          [''Equation'',''fromFunction''])              " ^

          "                          [BOOL (hd f_s), BOOL b_2]);         " ^

          "      b_3 = NTH 3 r_b;                                         " ^

          "      f_s = filter_sameFunId (lhs b_3) fun_s;                   " ^

          "      (e_3::bool) =                                             " ^

          "             (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^

          "                          [''Equation'',''fromFunction''])              " ^

          "                          [BOOL (hd f_s), BOOL b_3]);         " ^

          "      b_4 = NTH 4 r_b;                                         " ^

          "      f_s = filter_sameFunId (lhs b_4) fun_s;                   " ^

          "      (e_4::bool) =                                             " ^

          "             (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^

          "                          [''Equation'',''fromFunction''])              " ^

          "                          [BOOL (hd f_s), BOOL b_4])          " ^

          " in [e_1, e_2, e_3, e_4])"*)

          (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

          "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^

          " (let b_1 = NTH 1 r_b;                                         " ^

          "      f_s = filter (sameFunId (lhs b_1)) fun_s;                 " ^

          "      (e_1::bool) =                                             " ^

          "             (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^

          "                          [''Equation'',''fromFunction''])              " ^

          "                          [BOOL (hd f_s), BOOL b_1]);         " ^

          "      b_2 = NTH 2 r_b;                                         " ^

          "      f_s = filter (sameFunId (lhs b_2)) fun_s;                 " ^

          "      (e_2::bool) =                                             " ^

          "             (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^

          "                          [''Equation'',''fromFunction''])              " ^

          "                          [BOOL (hd f_s), BOOL b_2]);         " ^

          "      b_3 = NTH 3 r_b;                                         " ^

          "      f_s = filter (sameFunId (lhs b_3)) fun_s;                 " ^

          "      (e_3::bool) =                                             " ^

          "             (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^

          "                          [''Equation'',''fromFunction''])              " ^

          "                          [BOOL (hd f_s), BOOL b_3]);         " ^

          "      b_4 = NTH 4 r_b;                                         " ^

          "      f_s = filter (sameFunId (lhs b_4)) fun_s;                 " ^

          "      (e_4::bool) =                                             " ^

          "             (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^

          "                          [''Equation'',''fromFunction''])              " ^

          "                          [BOOL (hd f_s), BOOL b_4])          " ^

          " in [e_1,e_2,e_3,e_4])"*))]

\<close>

subsection \<open>Transform an equality into a function\<close>

        (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->

               0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)

partial_function (tailrec) function_to_equality :: "bool \<Rightarrow> bool \<Rightarrow> bool"

  where

"function_to_equality fu_n su_b =

 (let fu_n = Take fu_n;

      bd_v = argument_in (lhs fu_n);

      va_l = argument_in (lhs su_b);

      eq_u = Substitute [bd_v = va_l] fu_n;

                                     \<comment> \<open>([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2\<close>

      eq_u = Substitute [su_b] eq_u

 in (Rewrite_Set ''norm_Rational'' False) eq_u)"

setup \<open>KEStore_Elems.add_mets

    [Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID

	    (["Equation","fromFunction"],

	      [("#Given" ,["functionEq fu_n","substitution su_b"]),

	        ("#Find"  ,["equality equ'''"])],

	      {rew_ord'="tless_true", rls'=Rule.Erls, calc = [],

          srls = Rule.append_rls "srls_in_EquationfromFunc" Rule.e_rls

				      [Rule.Calc("Tools.lhs", Tools.eval_lhs "eval_lhs_"),

				        Rule.Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")], 

				  prls=Rule.e_rls, crls = Atools_erls, errpats = [], nrls = Rule.e_rls},

        (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->

               0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)

        @{thm function_to_equality.simps}

	    (*"Script Function2Equality (fu_n::bool) (su_b::bool) =" ^

        " (let fu_n = Take fu_n;                             " ^

        "      bd_v = argument_in (lhs fu_n);                " ^

        "      va_l = argument_in (lhs su_b);                " ^

        "      eq_u = (Substitute [bd_v = va_l]) fu_n;       " ^

                                        (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)

        "      eq_u = (Substitute [su_b]) eq_u               " ^

        " in (Rewrite_Set ''norm_Rational'' False) eq_u)         "*))]

\<close>

end