(* 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"

   oben            :: real

   senkrecht       :: real

   unten           :: real

 ML \<open>

 val thy = @{theory};

 \<close>

 (** problems **)

 setup \<open>KEStore_Elems.add_pbts

   [(Problem.prep_input thy "pbl_algein" [] Problem.id_empty (["Berechnung"], [], Rule_Set.empty, NONE, [])),

     (Problem.prep_input thy "pbl_algein_numsym" [] Problem.id_empty

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

         Rule_Set.empty, NONE, [["Berechnung", "erstNumerisch"], ["Berechnung", "erstSymbolisch"]]))]\<close>

 setup \<open>KEStore_Elems.add_mets

     [MethodC.prep_input thy "met_algein" [] MethodC.id_empty

 	    (["Berechnung"], [],

 	      {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,

           errpats = [], nrls = Rule_Set.Empty},

           @{thm refl}),

     MethodC.prep_input thy "met_algein_numsym" [] MethodC.id_empty

 	    (["Berechnung", "erstNumerisch"], [],

 	      {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,

 	        errpats = [], nrls = Rule_Set.Empty},

 	      @{thm refl})]

 \<close>

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

   where

 "symbolisch_rechnen k_k  q__q  u_u  s_s  o_o  l_l = (

   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'')) 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'')) 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'')) t_t

   in

     Try (Rewrite_Set ''norm_Poly'') t_t)"

 setup \<open>KEStore_Elems.add_mets

     [MethodC.prep_input thy "met_algein_numsym_1num" [] MethodC.id_empty

 	    (["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'= Rule_Set.empty, calc = [],

            srls = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty 

 				       [Rule.Eval ("Prog_Expr.boollist2sum", Prog_Expr.eval_boollist2sum "")], 

 		       prls = Rule_Set.empty, crls =Rule_Set.empty , errpats = [], nrls = norm_Rational},

          @{thm symbolisch_rechnen.simps})]

 \<close>

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

   where 

 "symbolisch_rechnen k_k q__q u_u s_s o_o l_l = (

   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'')) 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'')) 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'')) t_t;

     t_t = Substitute [k_k, q__q] t_t

  in

    (Try (Rewrite_Set ''norm_Poly'')) t_t)"

 setup \<open>KEStore_Elems.add_mets

     [MethodC.prep_input thy "met_algein_symnum" [] MethodC.id_empty

 	    (["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'= Rule_Set.empty, calc = [], 

 	          srls = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty 

 				        [Rule.Eval ("Prog_Expr.boollist2sum", Prog_Expr.eval_boollist2sum "")], 

 				    prls = Rule_Set.empty, crls =Rule_Set.empty , errpats = [], nrls = norm_Rational},

             @{thm symbolisch_rechnen.simps})]

 \<close>

 end