|
1 (* simplification of terms |
|
2 author: Walther Neuper 050912 |
|
3 (c) due to copyright terms |
|
4 |
|
5 use"IsacKnowledge/Simplify.ML"; |
|
6 use"Simplify.ML"; |
|
7 *) |
|
8 |
|
9 |
|
10 (** interface isabelle -- isac **) |
|
11 |
|
12 theory' := overwritel (!theory', [("Simplify.thy",Simplify.thy)]); |
|
13 |
|
14 (** problems **) |
|
15 |
|
16 store_pbt |
|
17 (prep_pbt Simplify.thy "pbl_simp" [] e_pblID |
|
18 (["simplification"], |
|
19 [("#Given" ,["term t_"]), |
|
20 ("#Find" ,["normalform n_"]) |
|
21 ], |
|
22 append_rls "e_rls" e_rls [(*for preds in where_*)], |
|
23 Some "Simplify t_", |
|
24 [])); |
|
25 |
|
26 store_pbt |
|
27 (prep_pbt Simplify.thy "pbl_vereinfache" [] e_pblID |
|
28 (["vereinfachen"], |
|
29 [("#Given" ,["term t_"]), |
|
30 ("#Find" ,["normalform n_"]) |
|
31 ], |
|
32 append_rls "e_rls" e_rls [(*for preds in where_*)], |
|
33 Some "Vereinfache t_", |
|
34 [])); |
|
35 |
|
36 (** methods **) |
|
37 |
|
38 store_met |
|
39 (prep_met Simplify.thy "met_simp" [] e_metID |
|
40 (["simplification"], |
|
41 [("#Given" ,["term t_"]), |
|
42 ("#Find" ,["normalform n_"]) |
|
43 ], |
|
44 {rew_ord'="tless_true", |
|
45 rls'= e_rls, |
|
46 calc = [], |
|
47 srls = e_rls, |
|
48 prls=e_rls, |
|
49 crls = e_rls, nrls = e_rls}, |
|
50 "empty_script" |
|
51 )); |
|
52 |
|
53 (** CAS-command **) |
|
54 |
|
55 (*.function for handling the cas-input "Simplify (2*a + 3*a)": |
|
56 make a model which is already in ptree-internal format.*) |
|
57 (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)"); |
|
58 val (h,argl) = strip_comb ((term_of o the o (parse thy)) |
|
59 "Simplify (2*a + 3*a)"); |
|
60 *) |
|
61 fun argl2dtss t = |
|
62 [((term_of o the o (parse thy)) "term", t), |
|
63 ((term_of o the o (parse thy)) "normalform", |
|
64 [(term_of o the o (parse thy)) "N"]) |
|
65 ] |
|
66 | argl2dtss _ = raise error "Simplify.ML: wrong argument for argl2dtss"; |
|
67 |
|
68 castab := |
|
69 overwritel (!castab, |
|
70 [((term_of o the o (parse thy)) "Simplify", |
|
71 (("Isac.thy", ["simplification"], ["no_met"]), |
|
72 argl2dtss)), |
|
73 ((term_of o the o (parse thy)) "Vereinfache", |
|
74 (("Isac.thy", ["vereinfachen"], ["no_met"]), |
|
75 argl2dtss)) |
|
76 ]); |