wneuper/isa: src/Tools/isac/Knowledge/Simplify.thy@bd4f7a35e892

     1 (* simplification of terms

     2    author: Walther Neuper 050912

     3    (c) due to copyright terms

     4 *)

     6 theory Simplify imports Atools begin

     8 consts

    10   (*descriptions in the related problem*)

    11   TERM        :: "real => una"

    12   normalform  :: "real => una"

    14   (*the CAS-command*)

    15   Simplify    :: "real => real"  (*"Simplify (1+2a+3+4a)*)

    16   Vereinfache :: "real => real"  (*"Vereinfache (1+2a+3+4a)*)

    18   (*Script-name*)

    19   SimplifyScript      :: "[real,  real] => real"

    20                   ("((Script SimplifyScript (_ =))// (_))" 9)

    22 ML {*

    24 (** problems **)

    25 store_pbt

    26  (prep_pbt (theory "Simplify") "pbl_simp" [] e_pblID

    27  (["simplification"],

    28   [("#Given" ,["TERM t_"]),

    29    ("#Find"  ,["normalform n_"])

    30   ],

    31   append_rls "e_rls" e_rls [(*for preds in where_*)],

    32   SOME "Simplify t_",

    33   []));

    35 store_pbt

    36  (prep_pbt (theory "Simplify") "pbl_vereinfache" [] e_pblID

    37  (["vereinfachen"],

    38   [("#Given" ,["TERM t_"]),

    39    ("#Find"  ,["normalform n_"])

    40   ],

    41   append_rls "e_rls" e_rls [(*for preds in where_*)],

    42   SOME "Vereinfache t_",

    43   []));

    45 (** methods **)

    47 store_met

    48     (prep_met (theory "Simplify") "met_simp" [] e_metID

    49 	      (["simplification"],

    50 	       [("#Given" ,["TERM t_"]),

    51 		("#Find"  ,["normalform n_"])

    52 		],

    53 	       {rew_ord'="tless_true",

    54 		rls'= e_rls,

    55 		calc = [],

    56 		srls = e_rls,

    57 		prls=e_rls,

    58 		crls = e_rls, nrls = e_rls},

    59 	       "empty_script"

    60 	       ));

    62 (** CAS-command **)

    64 (*.function for handling the cas-input "Simplify (2*a + 3*a)":

    65    make a model which is already in ptree-internal format.*)

    66 (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");

    67    val (h,argl) = strip_comb ((term_of o the o (parse thy))

    68 				  "Simplify (2*a + 3*a)");

    69    *)

    70 fun argl2dtss t =

    71     [((term_of o the o (parse thy)) "TERM", t),

    72      ((term_of o the o (parse thy)) "normalform",

    73       [(term_of o the o (parse thy)) "N"])

    74      ]

    75   | argl2dtss _ = raise error "Simplify.ML: wrong argument for argl2dtss";

    77 castab :=

    78 overwritel (!castab,

    79 	    [((term_of o the o (parse thy)) "Simplify",

    80 	      (("Isac.thy", ["simplification"], ["no_met"]),

    81 	       argl2dtss)),

    82 	     ((term_of o the o (parse thy)) "Vereinfache",

    83 	      (("Isac.thy", ["vereinfachen"], ["no_met"]),

    84 	       argl2dtss))

    85 	     ]);

    86 *}

    88 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 31 Aug 2010 16:38:22 +0200
branch	isac-update-Isa09-2
changeset 37967	bd4f7a35e892
parent 37953	369b3012f6f6
child 37968	e0db2aedf2d4
permissions	-rw-r--r--