wneuper/isa: src/Tools/isac/Knowledge/AlgEin.thy@73dc85c025ab

     1 (* Algebra Einf"uhrung, Unterrichtsversuch IMST-Projekt

     2    author: Walther Neuper 2007

     3    (c) due to copyright terms

     4 *)

     6 theory AlgEin imports Rational begin

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

     9 consts

    11   (*new Descriptions in the related problems*)

    12   KantenUnten     :: "bool list => una"

    13   KantenSenkrecht :: "bool list => una"

    14   KantenOben      :: "bool list => una"

    15   KantenLaenge    :: "bool => una"

    16   Querschnitt     :: "bool => una"

    17   GesamtLaenge    :: "real => una"

    19   (*Script-names*)

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

    21 				bool] => bool"

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

    24 ML {*

    25 val thy = @{theory};

    27 (** problems **)

    29 store_pbt

    30  (prep_pbt thy "pbl_algein" [] e_pblID

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

    32   []));

    33 (* WN070405

    34 store_pbt

    35  (prep_pbt thy "pbl_algein_num" [] e_pblID

    36  (["numerische", "Berechnung"],

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

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

    39   ],

    40   append_rls "e_rls" e_rls [],

    41   NONE,

    42   []));

    43 *)

    44 store_pbt

    45  (prep_pbt thy "pbl_algein_numsym" [] e_pblID

    46  (["numerischSymbolische", "Berechnung"],

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

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

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

    50   ],

    51   e_rls,

    52   NONE,

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

    55 (* show_ptyps();

    56    *)

    57 *}

    58 setup {* KEStore_Elems.add_pbts

    59   [(prep_pbt thy "pbl_algein" [] e_pblID (["Berechnung"], [], e_rls, NONE, [])),

    60     (prep_pbt thy "pbl_algein_numsym" [] e_pblID

    61       (["numerischSymbolische", "Berechnung"],

    62         [("#Given",

    63             ["KantenLaenge k_k","Querschnitt q__q"(*q_ in Biegelinie.thy*), "KantenUnten u_u",

    64               "KantenSenkrecht s_s", "KantenOben o_o"]),

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

    66         e_rls, NONE, [["Berechnung","erstNumerisch"], ["Berechnung","erstSymbolisch"]]))]; *}

    68 ML {*

    69 (** methods **)

    71 store_met

    72     (prep_met thy "met_algein" [] e_metID

    73 	      (["Berechnung"],

    74 	       [],

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

    76 		srls = Erls, prls = Erls,

    77 		crls =Erls , errpats = [], nrls = Erls},

    78 "empty_script"

    79 ));

    81 store_met

    82     (prep_met thy "met_algein_numsym" [] e_metID

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

    84 	       [],

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

    86 		srls = Erls, prls = Erls,

    87 		crls =Erls , errpats = [], nrls = Erls},

    88 "empty_script"

    89 ));

    91 *}

    92 ML {*

    93 store_met

    94     (prep_met thy "met_algein_numsym" [] e_metID

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

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

    97 			    "KantenUnten u_u", "KantenSenkrecht s_s",

    98 			    "KantenOben o_o"]),

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

   100 		],

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

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

   103 				  [Calc ("Atools.boollist2sum",

   104 					 eval_boollist2sum "")],

   105 		prls = e_rls, crls =e_rls , errpats = [], nrls = norm_Rational},

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

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

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

   109 "      su_m = boollist2sum o_o;                               " ^

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

   111 "      t_t = Substitute o_o t_t;                                " ^

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

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

   114 "      su_m = boollist2sum s_s;                               " ^

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

   116 "      t_t = Substitute s_s t_t;                                " ^

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

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

   119 "      su_m = boollist2sum u_u;                               " ^

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

   121 "      t_t = Substitute u_u t_t;                                " ^

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

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

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

   125 ));

   127 *}

   128 ML {*

   129 store_met

   130     (prep_met thy "met_algein_symnum" [] e_metID

   131 	      (["Berechnung","erstSymbolisch"],

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

   133 			    "KantenUnten u_u", "KantenSenkrecht s_s",

   134 			    "KantenOben o_o"]),

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

   136 		],

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

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

   139 				  [Calc ("Atools.boollist2sum",

   140 					 eval_boollist2sum "")],

   141 		prls = e_rls,

   142 		crls =e_rls , errpats = [], nrls = norm_Rational},

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

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

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

   146 "      su_m = boollist2sum o_o;                               " ^

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

   148 "      t_t = Substitute o_o t_t;                                " ^

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

   150 "      su_m = boollist2sum s_s;                               " ^

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

   152 "      t_t = Substitute s_s t_t;                                " ^

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

   154 "      su_m = boollist2sum u_u;                               " ^

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

   156 "      t_t = Substitute u_u t_t;                                " ^

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

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

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

   160 ));

   161 *}

   163 end

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Mon, 27 Jan 2014 21:49:27 +0100
changeset 55359	73dc85c025ab
parent 55339	cccd24e959ba
child 55363	d78bc1342183
permissions	-rw-r--r--