(* Algebra Einf"uhrung, Unterrichtsversuch IMST-Projekt

   author: Walther Neuper 2007

   (c) due to copyright terms

*)

theory AlgEin imports Rational begin

(*Poly + ..shouldbe sufficient, but norm_Poly required*)

consts

  (*new Descriptions in the related problems*)

  KantenUnten     :: "bool list => una"

  KantenSenkrecht :: "bool list => una"

  KantenOben      :: "bool list => una"

  KantenLaenge    :: "bool => una"

  Querschnitt     :: "bool => una"

  GesamtLaenge    :: "real => una"

  (*Script-names*)

  RechnenSymbolScript :: "[bool,bool,bool list,bool list,bool list,real,

				bool] => bool"

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

ML {*

val thy = @{theory};

(** problems **)

store_pbt

 (prep_pbt thy "pbl_algein" [] e_pblID

 (["Berechnung"], [], e_rls, NONE, 

  []));

(* WN070405

store_pbt

 (prep_pbt thy "pbl_algein_num" [] e_pblID

 (["numerische", "Berechnung"],

  [("#Given" ,["KantenUnten u_u", "KantenSenkrecht s_s", "KantenOben o_o"]),

   ("#Find"  ,["GesamtLaenge l_l"])

  ],

  append_rls "e_rls" e_rls [], 

  NONE, 

  []));

*)

store_pbt

 (prep_pbt thy "pbl_algein_numsym" [] e_pblID

 (["numerischSymbolische", "Berechnung"],

  [("#Given" ,["KantenLaenge k_k","Querschnitt q__q"(*q_ in Biegelinie.thy*),

	       "KantenUnten u_u", "KantenSenkrecht s_s", "KantenOben o_o"]),

   ("#Find"  ,["GesamtLaenge l_l"])

  ],

  e_rls, 

  NONE, 

  [["Berechnung","erstNumerisch"],["Berechnung","erstSymbolisch"]]));

(* show_ptyps();

   *)

*}

ML {*

(** methods **)

store_met

    (prep_met thy "met_algein" [] e_metID

	      (["Berechnung"],

	       [],

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

		srls = Erls, prls = Erls,

		crls =Erls , nrls = Erls},

"empty_script"

));

store_met

    (prep_met thy "met_algein_numsym" [] e_metID

	      (["Berechnung","erstNumerisch"],

	       [],

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

		srls = Erls, prls = Erls,

		crls =Erls , nrls = Erls},

"empty_script"

));

*}

ML {*

store_met

    (prep_met thy "met_algein_numsym" [] e_metID

	      (["Berechnung","erstNumerisch"],

	       [("#Given" ,["KantenLaenge k_k","Querschnitt q__q",

			    "KantenUnten u_u", "KantenSenkrecht s_s", 

			    "KantenOben o_o"]),

		("#Find"  ,["GesamtLaenge l_l"])

		],

	       {rew_ord'="tless_true", rls'= e_rls, calc = [], 

		srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls 

				  [Calc ("Atools.boollist2sum",

					 eval_boollist2sum "")], 

		prls = e_rls, crls =e_rls , nrls = norm_Rational},

"Script RechnenSymbolScript (k_k::bool) (q__q::bool)           " ^

"(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^

" (let t_t = Take (l_l = oben + senkrecht + unten);            " ^

"      su_m = boollist2sum o_o;                               " ^

"      t_t = Substitute [oben = su_m] t_t;                     " ^

"      t_t = Substitute o_o t_t;                                " ^

"      t_t = Substitute [k_k, q__q] t_t;                         " ^

"      t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^

"      su_m = boollist2sum s_s;                               " ^

"      t_t = Substitute [senkrecht = su_m] t_t;                " ^

"      t_t = Substitute s_s t_t;                                " ^

"      t_t = Substitute [k_k, q__q] t_t;                         " ^

"      t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^

"      su_m = boollist2sum u_u;                               " ^

"      t_t = Substitute [unten = su_m] t_t;                    " ^

"      t_t = Substitute u_u t_t;                                " ^

"      t_t = Substitute [k_k, q__q] t_t;                         " ^

"      t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t  " ^

" in (Try (Rewrite_Set norm_Poly False)) t_t)                  "

));

*}

ML {*

store_met

    (prep_met thy "met_algein_symnum" [] e_metID

	      (["Berechnung","erstSymbolisch"],

	       [("#Given" ,["KantenLaenge k_k","Querschnitt q__q",

			    "KantenUnten u_u", "KantenSenkrecht s_s", 

			    "KantenOben o_o"]),

		("#Find"  ,["GesamtLaenge l_l"])

		],

	       {rew_ord'="tless_true", rls'= e_rls, calc = [], 

		srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls 

				  [Calc ("Atools.boollist2sum",

					 eval_boollist2sum "")], 

		prls = e_rls,

		crls =e_rls , nrls = norm_Rational},

"Script RechnenSymbolScript (k_k::bool) (q__q::bool)           " ^

"(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^

" (let t_t = Take (l_l = oben + senkrecht + unten);            " ^

"      su_m = boollist2sum o_o;                               " ^

"      t_t = Substitute [oben = su_m] t_t;                     " ^

"      t_t = Substitute o_o t_t;                                " ^

"      t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^

"      su_m = boollist2sum s_s;                               " ^

"      t_t = Substitute [senkrecht = su_m] t_t;                " ^

"      t_t = Substitute s_s t_t;                                " ^

"      t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^

"      su_m = boollist2sum u_u;                               " ^

"      t_t = Substitute [unten = su_m] t_t;                    " ^

"      t_t = Substitute u_u t_t;                                " ^

"      t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^

"      t_t = Substitute [k_k, q__q] t_t                          " ^

" in (Try (Rewrite_Set norm_Poly False)) t_t)                 "

));

*}

end