neuper@37906
|
1 |
(* simplification of terms
|
neuper@37906
|
2 |
author: Walther Neuper 050912
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
*)
|
neuper@37906
|
5 |
|
wneuper@59424
|
6 |
theory Simplify imports Base_Tools begin
|
neuper@37906
|
7 |
|
neuper@37906
|
8 |
consts
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
(*descriptions in the related problem*)
|
walther@60317
|
11 |
Term :: "real => una" (*"term" is a keyword in *.thy*)
|
neuper@37950
|
12 |
normalform :: "real => una"
|
neuper@37906
|
13 |
|
neuper@37906
|
14 |
(*the CAS-command*)
|
neuper@37906
|
15 |
Simplify :: "real => real" (*"Simplify (1+2a+3+4a)*)
|
neuper@37906
|
16 |
Vereinfache :: "real => real" (*"Vereinfache (1+2a+3+4a)*)
|
neuper@37906
|
17 |
|
neuper@37950
|
18 |
(** problems **)
|
wenzelm@60306
|
19 |
|
wenzelm@60306
|
20 |
problem pbl_simp : "simplification" =
|
wenzelm@60306
|
21 |
\<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
|
wenzelm@60306
|
22 |
CAS: "Simplify t_t"
|
wenzelm@60306
|
23 |
Given: "Term t_t"
|
wenzelm@60306
|
24 |
Find: "normalform n_n"
|
wenzelm@60306
|
25 |
|
wenzelm@60306
|
26 |
problem pbl_vereinfache : "vereinfachen" =
|
wenzelm@60306
|
27 |
\<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
|
wenzelm@60306
|
28 |
CAS: "Vereinfache t_t"
|
wenzelm@60306
|
29 |
Given: "Term t_t"
|
wenzelm@60306
|
30 |
Find: "normalform n_n"
|
neuper@37950
|
31 |
|
neuper@37950
|
32 |
(** methods **)
|
wenzelm@60303
|
33 |
|
wenzelm@60303
|
34 |
method met_tsimp : "simplification" =
|
wenzelm@60303
|
35 |
\<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Rule_Set.empty,
|
wenzelm@60303
|
36 |
errpats = [], nrls = Rule_Set.empty}\<close>
|
wenzelm@60303
|
37 |
Given: "Term t_t"
|
wenzelm@60303
|
38 |
Find: "normalform n_n"
|
s1210629013@55373
|
39 |
|
wneuper@59472
|
40 |
ML \<open>
|
neuper@37950
|
41 |
|
neuper@37950
|
42 |
(** CAS-command **)
|
neuper@37950
|
43 |
|
neuper@37950
|
44 |
(*.function for handling the cas-input "Simplify (2*a + 3*a)":
|
wneuper@59279
|
45 |
make a model which is already in ctree-internal format.*)
|
Walther@60567
|
46 |
(* val (h,argl) = strip_comb (TermC.parse_test @{context} "Simplify (2*a + 3*a)");
|
wneuper@59352
|
47 |
val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info_get_theory "Simplify")))
|
neuper@37950
|
48 |
"Simplify (2*a + 3*a)");
|
neuper@37950
|
49 |
*)
|
neuper@37950
|
50 |
fun argl2dtss t =
|
walther@60417
|
51 |
[((TermC.parseNEW''\<^theory>) "Term", t),
|
walther@60417
|
52 |
((TermC.parseNEW''\<^theory>) "normalform",
|
walther@60417
|
53 |
[(TermC.parseNEW''\<^theory>) "N"])
|
neuper@37950
|
54 |
]
|
walther@59962
|
55 |
(*| argl2dtss _ = raise ERROR "Simplify.ML: wrong argument for argl2dtss"*);
|
wneuper@59472
|
56 |
\<close>
|
wenzelm@60314
|
57 |
cas Simplify = \<open>argl2dtss\<close>
|
Walther@60449
|
58 |
Problem_Ref: "simplification"
|
wenzelm@60314
|
59 |
cas Vereinfache = \<open>argl2dtss\<close>
|
Walther@60449
|
60 |
Problem_Ref: "vereinfachen"
|
neuper@37906
|
61 |
|
walther@60269
|
62 |
ML \<open>
|
walther@60269
|
63 |
\<close> ML \<open>
|
walther@60269
|
64 |
\<close> ML \<open>
|
walther@60269
|
65 |
\<close>
|
neuper@37906
|
66 |
end |