(* simplification of terms

    author: Walther Neuper 050912

    (c) due to copyright terms

 *)

 theory Simplify imports Base_Tools begin

 consts

   (*descriptions in the related problem*)

   Term        :: "real => una"   (*"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)*)

 (** problems **)

 problem pbl_simp : "simplification" =

   \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>

   CAS: "Simplify t_t"

   Given: "Term t_t"

   Find: "normalform n_n"

 problem pbl_vereinfache : "vereinfachen" =

   \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>

   CAS: "Vereinfache t_t"

   Given: "Term t_t"

   Find: "normalform n_n"

 (** methods **)

 method met_tsimp : "simplification" =

   \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Rule_Set.empty,

     errpats = [], nrls = Rule_Set.empty}\<close>

   Given: "Term t_t"

   Find: "normalform n_n"

 ML \<open>

 (** 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 (TermC.parse_test @{context} "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 =

     [((TermC.parseNEW''\<^theory>) "Term", t),

      ((TermC.parseNEW''\<^theory>) "normalform", 

      [(TermC.parseNEW''\<^theory>) "N"])

      ]

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

 \<close>

 cas Simplify = \<open>argl2dtss\<close>

   Problem_Ref: "simplification"

 cas Vereinfache = \<open>argl2dtss\<close>

   Problem_Ref: "vereinfachen"

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end