2 theory example_2 imports Isac
5 section{*Symbol Representation*}
15 term2str @{term "\<rho> "};
18 section{*Working with Rulesets*}
21 rule1: "1 = \<delta>[n]" and
22 rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
23 rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and
24 rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]"
33 text{*Create Ruleset and insert rules*}
36 val transform = append_rls "transform" e_rls
37 [ Thm ("rule3",num_str @{thm rule3}),
38 Thm ("rule4",num_str @{thm rule4}),
39 Thm ("rule1",num_str @{thm rule1})
43 text{*Apply the Ruleset to a term*}
46 val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1::real";
47 val SOME (t', asm) = rewrite_set_ thy true transform t;
52 term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
53 term2str t' = "?u [?n] + \<alpha>^^^?n u[n] + ?\<delta> [?n]";
56 text{*Problems: Rule~1 is applied before the expression is checked for Rule~4
57 which would be the correct one. Rule~1 only matches a part of the