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

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", 

  []));

*}

setup {* KEStore_Elems.add_pbts

  [(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", [])),

    (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", []))] *}

ML {*

@{thm mult_commute}

*}

ML {*

(** 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, errpats = [], nrls = 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 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 (Thy_Info.get_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"*);

*}

setup {* KEStore_Elems.add_cas

  [((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