Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/AlgEin.ML
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 25 Aug 2010 16:20:07 +0200
branchisac-update-Isa09-2
changeset 37947 22235e4dbe5f
parent 37926 src/Tools/isac/IsacKnowledge/AlgEin.ML@e6fc98fbcb85
child 37952 9ddd1000b900
permissions -rw-r--r--
renamed isac's directories and Build_Isac.thy

Scripts --> ProgLang
ME --> Interpret
IsacKnowledge --> Knowledge 
     1 (* Algebra Einf"uhrung, Unterrichtsversuch IMST-Projekt

     2    author: Walther Neuper 2007

     3    (c) due to copyright terms

     4 

     5 use"Knowledge/AlgEin.ML";

     6 use"AlgEin.ML";

     7 

     8 remove_thy"Typefix";

     9 remove_thy"AlgEin";

    10 use_thy"Knowledge/Isac";

    11 *)

    12 

    13 (** interface isabelle -- isac **)

    14 

    15 theory' := overwritel (!theory', [("AlgEin.thy",AlgEin.thy)]);

    16 

    17 (** problems **)

    18 

    19 store_pbt

    20  (prep_pbt AlgEin.thy "pbl_algein" [] e_pblID

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

    22   []));

    23 (* WN070405

    24 store_pbt

    25  (prep_pbt AlgEin.thy "pbl_algein_num" [] e_pblID

    26  (["numerische", "Berechnung"],

    27   [("#Given" ,["KantenUnten u_", "KantenSenkrecht s_", "KantenOben o_"]),

    28    ("#Find"  ,["GesamtLaenge l_"])

    29   ],

    30   append_rls "e_rls" e_rls [], 

    31   NONE, 

    32   []));

    33 *)

    34 store_pbt

    35  (prep_pbt AlgEin.thy "pbl_algein_numsym" [] e_pblID

    36  (["numerischSymbolische", "Berechnung"],

    37   [("#Given" ,["KantenLaenge k_","Querschnitt q__"(*q_ in Biegelinie.thy*),

    38 	       "KantenUnten u_", "KantenSenkrecht s_", "KantenOben o_"]),

    39    ("#Find"  ,["GesamtLaenge l_"])

    40   ],

    41   e_rls, 

    42   NONE, 

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

    44 

    45 (* show_ptyps();

    46    *)

    47 

    48 

    49 (** methods **)

    50 

    51 store_met

    52     (prep_met AlgEin.thy "met_algein" [] e_metID

    53 	      (["Berechnung"],

    54 	       [],

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

    56 		srls = Erls, prls = Erls,

    57 		crls =Erls , nrls = Erls},

    58 "empty_script"

    59 ));

    60 

    61 store_met

    62     (prep_met AlgEin.thy "met_algein_numsym" [] e_metID

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

    64 	       [],

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

    66 		srls = Erls, prls = Erls,

    67 		crls =Erls , nrls = Erls},

    68 "empty_script"

    69 ));

    70 

    71 store_met

    72     (prep_met AlgEin.thy "met_algein_numsym" [] e_metID

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

    74 	       [("#Given" ,["KantenLaenge k_","Querschnitt q__",

    75 			    "KantenUnten u_", "KantenSenkrecht s_", 

    76 			    "KantenOben o_"]),

    77 		("#Find"  ,["GesamtLaenge l_"])

    78 		],

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

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

    81 				  [Calc ("Atools.boollist2sum",

    82 					 eval_boollist2sum "")], 

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

    84 "Script RechnenSymbolScript (k_::bool) (q__::bool)           \

    85 \(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\

    86 \ (let t_ = Take (l_ = oben + senkrecht + unten);            \

    87 \      sum_ = boollist2sum o_;\

    88 \      t_ = Substitute [oben = sum_] t_;\

    89 \      t_ = Substitute o_ t_;\

    90 \      t_ = Substitute [k_, q__] t_;\

    91 \      t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\

    92 \      sum_ = boollist2sum s_;\

    93 \      t_ = Substitute [senkrecht = sum_] t_;\

    94 \      t_ = Substitute s_ t_;\

    95 \      t_ = Substitute [k_, q__] t_;\

    96 \      t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\

    97 \      sum_ = boollist2sum u_;\

    98 \      t_ = Substitute [unten = sum_] t_;\

    99 \      t_ = Substitute u_ t_;\

   100 \      t_ = Substitute [k_, q__] t_;\

   101 \      t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_\

   102 \ in (Try (Rewrite_Set norm_Poly False)) t_)"

   103 ));

   104 

   105 store_met

   106     (prep_met AlgEin.thy "met_algein_symnum" [] e_metID

   107 	      (["Berechnung","erstSymbolisch"],

   108 	       [("#Given" ,["KantenLaenge k_","Querschnitt q__",

   109 			    "KantenUnten u_", "KantenSenkrecht s_", 

   110 			    "KantenOben o_"]),

   111 		("#Find"  ,["GesamtLaenge l_"])

   112 		],

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

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

   115 				  [Calc ("Atools.boollist2sum",

   116 					 eval_boollist2sum "")], 

   117 		prls = e_rls,

   118 		crls =e_rls , nrls = norm_Rational},

   119 "Script RechnenSymbolScript (k_::bool) (q__::bool)           \

   120 \(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\

   121 \ (let t_ = Take (l_ = oben + senkrecht + unten);            \

   122 \      sum_ = boollist2sum o_;\

   123 \      t_ = Substitute [oben = sum_] t_;\

   124 \      t_ = Substitute o_ t_;\

   125 \      t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\

   126 \      sum_ = boollist2sum s_;\

   127 \      t_ = Substitute [senkrecht = sum_] t_;\

   128 \      t_ = Substitute s_ t_;\

   129 \      t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\

   130 \      sum_ = boollist2sum u_;\

   131 \      t_ = Substitute [unten = sum_] t_;\

   132 \      t_ = Substitute u_ t_;\

   133 \      t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\

   134 \      t_ = Substitute [k_, q__] t_\

   135 \ in (Try (Rewrite_Set norm_Poly False)) t_)"

   136 ));

   137 

   138 (* show_mets();

   139    *)

   140 (* use"Knowledge/AlgEin.ML";

   141    *)
wneuper/isa