neuper@37906: (* simplification of terms
neuper@37906:    author: Walther Neuper 050912
neuper@37906:    (c) due to copyright terms
neuper@37906: *)
neuper@37906: 
wneuper@59424: theory Simplify imports Base_Tools 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: 
wneuper@59472: ML \<open>
neuper@37972: val thy = @{theory};
wneuper@59472: \<close>
neuper@37950: (** problems **)
wneuper@59472: setup \<open>KEStore_Elems.add_pbts
walther@59973:   [(Problem.prep_input thy "pbl_simp" [] Problem.id_empty
s1210629013@55339:       (["simplification"],
s1210629013@55339:         [("#Given" ,["Term t_t"]),
s1210629013@55339:           ("#Find"  ,["normalform n_n"])],
walther@59852:         Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Simplify t_t", [])),
walther@59973:     (Problem.prep_input thy "pbl_vereinfache" [] Problem.id_empty
s1210629013@55339:       (["vereinfachen"],
s1210629013@55339:         [("#Given", ["Term t_t"]),
s1210629013@55339:           ("#Find", ["normalform n_n"])],
walther@59852:         Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Vereinfache t_t", []))]\<close>
neuper@37950: 
neuper@37950: (** methods **)
wneuper@59472: setup \<open>KEStore_Elems.add_mets
walther@60154:     [MethodC.prep_input thy "met_tsimp" [] MethodC.id_empty
s1210629013@55373: 	    (["simplification"],
s1210629013@55373: 	      [("#Given" ,["Term t_t"]),
s1210629013@55373: 		      ("#Find"  ,["normalform n_n"])],
walther@59852: 		    {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Rule_Set.empty,
walther@59852: 		      errpats = [], nrls = Rule_Set.empty},
wneuper@59545: 	      @{thm refl})]
wneuper@59472: \<close>
s1210629013@55373: 
wneuper@59472: ML \<open>
neuper@37950: 
neuper@37950: (** CAS-command **)
neuper@37950: 
neuper@37950: (*.function for handling the cas-input "Simplify (2*a + 3*a)":
wneuper@59279:    make a model which is already in ctree-internal format.*)
neuper@37950: (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
wneuper@59352:    val (h,argl) = strip_comb ((Thm.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 =
wneuper@59389:     [((Thm.term_of o the o (TermC.parse thy)) "Term", t),
wneuper@59389:      ((Thm.term_of o the o (TermC.parse thy)) "normalform", 
wneuper@59389:       [(Thm.term_of o the o (TermC.parse thy)) "N"])
neuper@37950:      ]
walther@59962:   (*| argl2dtss _ = raise ERROR "Simplify.ML: wrong argument for argl2dtss"*);
wneuper@59472: \<close>
wneuper@59472: setup \<open>KEStore_Elems.add_cas
wneuper@59389:   [((Thm.term_of o the o (TermC.parse thy)) "Simplify",  
wneuper@59592:     (("Isac_Knowledge", ["simplification"], ["no_met"]), argl2dtss)),
wneuper@59389:    ((Thm.term_of o the o (TermC.parse thy)) "Vereinfache",  
wneuper@59592:      (("Isac_Knowledge", ["vereinfachen"], ["no_met"]), argl2dtss))]\<close>
neuper@37906: 
neuper@37906: end