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

 (*TERM -->   Const ("Pure.term", "RealDef.real => prop")  (*!!!*) $ 

                Free ("ttt", "RealDef.real")

   term -->   Free ("term", "RealDef.real => RealDef.real") $

                Free ("ttt", "RealDef.real")

     but 'term' is a keyword in *.thy*)

   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 **)

 setup {* KEStore_Elems.add_pbts

   [(Specify.prep_pbt thy "pbl_simp" [] Celem.e_pblID

       (["simplification"],

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

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

         Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], SOME "Simplify t_t", [])),

     (Specify.prep_pbt thy "pbl_vereinfache" [] Celem.e_pblID

       (["vereinfachen"],

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

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

         Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], SOME "Vereinfache t_t", []))] *}

 (** methods **)

 setup {* KEStore_Elems.add_mets

   [Specify.prep_met thy "met_tsimp" [] Celem.e_metID

 	    (["simplification"],

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

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

 		    {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls, crls = Celem.e_rls,

 		      errpats = [], nrls = Celem.e_rls},

 	      "empty_script")]

 *}

 ML {*

 (** CAS-command **)

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

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

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

    val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info_get_theory "Simplify"))) 

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

    *)

 fun argl2dtss t =

     [((Thm.term_of o the o (TermC.parse thy)) "Term", t),

      ((Thm.term_of o the o (TermC.parse thy)) "normalform", 

       [(Thm.term_of o the o (TermC.parse thy)) "N"])

      ]

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

 *}

 setup {* KEStore_Elems.add_cas

   [((Thm.term_of o the o (TermC.parse thy)) "Simplify",  

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

    ((Thm.term_of o the o (TermC.parse thy)) "Vereinfache",  

      (("Isac", ["vereinfachen"], ["no_met"]), argl2dtss))]*}

 end