19 (*the CAS-command*) |
19 (*the CAS-command*) |
20 Simplify :: "real => real" (*"Simplify (1+2a+3+4a)*) |
20 Simplify :: "real => real" (*"Simplify (1+2a+3+4a)*) |
21 Vereinfache :: "real => real" (*"Vereinfache (1+2a+3+4a)*) |
21 Vereinfache :: "real => real" (*"Vereinfache (1+2a+3+4a)*) |
22 |
22 |
23 (** problems **) |
23 (** problems **) |
24 setup \<open>KEStore_Elems.add_pbts |
24 |
25 [(Problem.prep_input @{theory} "pbl_simp" [] Problem.id_empty |
25 problem pbl_simp : "simplification" = |
26 (["simplification"], |
26 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close> |
27 [("#Given" ,["Term t_t"]), |
27 CAS: "Simplify t_t" |
28 ("#Find" ,["normalform n_n"])], |
28 Given: "Term t_t" |
29 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Simplify t_t", [])), |
29 Find: "normalform n_n" |
30 (Problem.prep_input @{theory} "pbl_vereinfache" [] Problem.id_empty |
30 |
31 (["vereinfachen"], |
31 problem pbl_vereinfache : "vereinfachen" = |
32 [("#Given", ["Term t_t"]), |
32 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close> |
33 ("#Find", ["normalform n_n"])], |
33 CAS: "Vereinfache t_t" |
34 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Vereinfache t_t", []))]\<close> |
34 Given: "Term t_t" |
|
35 Find: "normalform n_n" |
35 |
36 |
36 (** methods **) |
37 (** methods **) |
37 |
38 |
38 method met_tsimp : "simplification" = |
39 method met_tsimp : "simplification" = |
39 \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Rule_Set.empty, |
40 \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Rule_Set.empty, |