(* simplification of terms

    author: Walther Neuper 050912

    (c) due to copyright terms

 *)

 theory Simplify imports Atools begin

 consts

   (*descriptions in the related problem*)

   TERM        :: "real => una"

   normalform  :: "real => una"

   (*the CAS-command*)

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

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

   (*Script-name*)

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

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

 ML {*

 val thy = @{theory};

 (** problems **)

 store_pbt

  (prep_pbt thy "pbl_simp" [] e_pblID

  (["simplification"],

   [("#Given" ,["TERM t_t"]),

    ("#Find"  ,["normalform n_n"])

   ],

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

   SOME "Simplify t_t", 

   []));

 store_pbt

  (prep_pbt thy "pbl_vereinfache" [] e_pblID

  (["vereinfachen"],

   [("#Given" ,["TERM t_t"]),

    ("#Find"  ,["normalform n_n"])

   ],

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

   SOME "Vereinfache t_t", 

   []));

 (** methods **)

 store_met

     (prep_met thy "met_tsimp" [] e_metID

 	      (["simplification"],

 	       [("#Given" ,["TERM t_t"]),

 		("#Find"  ,["normalform n_n"])

 		],

 	       {rew_ord'="tless_true",

 		rls'= e_rls, 

 		calc = [], 

 		srls = e_rls, 

 		prls=e_rls,

 		crls = e_rls, nrls = e_rls},

 	       "empty_script"

 	       ));

 (** CAS-command **)

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

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

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

    val (h,argl) = strip_comb ((term_of o the o (parse (theory "Simplify"))) 

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

    *)

 fun argl2dtss t =

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

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

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

      ]

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

 castab := 

 overwritel (!castab, 

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

 	      (("Isac", ["simplification"], ["no_met"]), 

 	       argl2dtss)),

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

 	      (("Isac", ["vereinfachen"], ["no_met"]), 

 	       argl2dtss))

 	     ]);

 *}

 end