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

    [((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: "simplification"

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

  Problem: "vereinfachen"

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

end