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

ML \<open>

val thy = @{theory};

\<close>

(** problems **)

setup \<open>KEStore_Elems.add_pbts

  [(Problem.prep_input thy "pbl_simp" [] Problem.id_empty

      (["simplification"],

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

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

        Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Simplify t_t", [])),

    (Problem.prep_input thy "pbl_vereinfache" [] Problem.id_empty

      (["vereinfachen"],

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

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

        Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Vereinfache t_t", []))]\<close>

(** methods **)

setup \<open>KEStore_Elems.add_mets

    [MethodC.prep_input thy "met_tsimp" [] MethodC.id_empty

	    (["simplification"],

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

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

		    {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},

	      @{thm refl})]

\<close>

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 =

    [((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 _ = raise ERROR "Simplify.ML: wrong argument for argl2dtss"*);

\<close>

setup \<open>KEStore_Elems.add_cas

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

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

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

     (("Isac_Knowledge", ["vereinfachen"], ["no_met"]), argl2dtss))]\<close>

end