neuper@37906: (* simplification of terms
neuper@37906:    author: Walther Neuper 050912
neuper@37906:    (c) due to copyright terms
neuper@37906: *)
neuper@37906: 
neuper@37950: theory Simplify imports Atools begin
neuper@37906: 
neuper@37906: consts
neuper@37906: 
neuper@37906:   (*descriptions in the related problem*)
neuper@38083:   Term        :: "real => una"
neuper@38083: (*TERM -->   Const ("Pure.term", "RealDef.real => prop")  (*!!!*) $ 
neuper@38083:                Free ("ttt", "RealDef.real")
neuper@38083:   term -->   Free ("term", "RealDef.real => RealDef.real") $
neuper@38083:                Free ("ttt", "RealDef.real")
neuper@38083:     but 'term' is a keyword in *.thy*)
neuper@37950:   normalform  :: "real => una"
neuper@37906: 
neuper@37906:   (*the CAS-command*)
neuper@37906:   Simplify    :: "real => real"  (*"Simplify (1+2a+3+4a)*)
neuper@37906:   Vereinfache :: "real => real"  (*"Vereinfache (1+2a+3+4a)*)
neuper@37906: 
neuper@37906:   (*Script-name*)
neuper@37906:   SimplifyScript      :: "[real,  real] => real"
neuper@37906:                   ("((Script SimplifyScript (_ =))// (_))" 9)
neuper@37906: 
neuper@37950: ML {*
neuper@37972: val thy = @{theory};
s1210629013@55363: *}
neuper@37950: (** problems **)
s1210629013@55359: setup {* KEStore_Elems.add_pbts
s1210629013@55339:   [(prep_pbt thy "pbl_simp" [] e_pblID
s1210629013@55339:       (["simplification"],
s1210629013@55339:         [("#Given" ,["Term t_t"]),
s1210629013@55339:           ("#Find"  ,["normalform n_n"])],
s1210629013@55339:         append_rls "e_rls" e_rls [(*for preds in where_*)], SOME "Simplify t_t", [])),
s1210629013@55339:     (prep_pbt thy "pbl_vereinfache" [] e_pblID
s1210629013@55339:       (["vereinfachen"],
s1210629013@55339:         [("#Given", ["Term t_t"]),
s1210629013@55339:           ("#Find", ["normalform n_n"])],
s1210629013@55339:         append_rls "e_rls" e_rls [(*for preds in where_*)], SOME "Vereinfache t_t", []))] *}
neuper@42425: ML {*
neuper@48763: @{thm mult_commute}
neuper@48763: *}
neuper@48763: ML {*
neuper@37950: 
neuper@37950: (** methods **)
neuper@37950: 
neuper@37950: store_met
neuper@42425:  (prep_met thy "met_tsimp" [] e_metID
neuper@42425: 	   (["simplification"],
neuper@42425: 	    [("#Given" ,["Term t_t"]),
neuper@42425: 		     ("#Find"  ,["normalform n_n"])],
neuper@42425: 	    {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls=e_rls,
neuper@42425: 	     crls = e_rls, errpats = [], nrls = e_rls},
neuper@42425: 	     "empty_script"));
neuper@42425: *}
s1210629013@55373: (** methods **)
s1210629013@55373: setup {* KEStore_Elems.add_mets
s1210629013@55373:   [prep_met thy "met_tsimp" [] e_metID
s1210629013@55373: 	    (["simplification"],
s1210629013@55373: 	      [("#Given" ,["Term t_t"]),
s1210629013@55373: 		      ("#Find"  ,["normalform n_n"])],
s1210629013@55373: 		    {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls=e_rls, crls = e_rls,
s1210629013@55373: 		      errpats = [], nrls = e_rls},
s1210629013@55373: 	      "empty_script")]
s1210629013@55373: *}
s1210629013@55373: 
neuper@42425: ML {*
neuper@37950: 
neuper@37950: (** CAS-command **)
neuper@37950: 
neuper@37950: (*.function for handling the cas-input "Simplify (2*a + 3*a)":
neuper@37950:    make a model which is already in ptree-internal format.*)
neuper@37950: (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
neuper@40836:    val (h,argl) = strip_comb ((term_of o the o (parse (Thy_Info.get_theory "Simplify"))) 
neuper@37950: 				  "Simplify (2*a + 3*a)");
neuper@37950:    *)
neuper@37950: fun argl2dtss t =
neuper@38083:     [((term_of o the o (parse thy)) "Term", t),
neuper@37972:      ((term_of o the o (parse thy)) "normalform", 
neuper@37972:       [(term_of o the o (parse thy)) "N"])
neuper@37950:      ]
s1210629013@52170:   (*| argl2dtss _ = error "Simplify.ML: wrong argument for argl2dtss"*);
neuper@37950: *}
s1210629013@52170: setup {* KEStore_Elems.add_cas
s1210629013@52170:   [((term_of o the o (parse thy)) "Simplify",  
s1210629013@52170:     (("Isac", ["simplification"], ["no_met"]), argl2dtss)),
s1210629013@52170:    ((term_of o the o (parse thy)) "Vereinfache",  
s1210629013@52170:      (("Isac", ["vereinfachen"], ["no_met"]), argl2dtss))]*}
neuper@37906: 
neuper@37906: end