author | Jan Rocnik <jan.rocnik@student.tugraz.at> |
Fri, 31 Aug 2012 19:19:07 +0200 | |
changeset 42461 | 94c9a0735e2f |
parent 42444 | 2768aa42a383 |
child 59465 | b33dc41f4350 |
permissions | -rwxr-xr-x |
jan@42443 | 1 |
|
jan@42443 | 2 |
theory example_2 imports Isac |
jan@42443 | 3 |
begin |
jan@42443 | 4 |
|
jan@42444 | 5 |
section{*Symbol Representation*} |
jan@42444 | 6 |
|
jan@42443 | 7 |
ML {* |
jan@42444 | 8 |
(* |
jan@42444 | 9 |
* alpha --> "</alpha>" |
jan@42444 | 10 |
*) |
jan@42443 | 11 |
@{term "\<alpha> "}; |
jan@42443 | 12 |
@{term "\<delta> "}; |
jan@42443 | 13 |
@{term "\<phi> "}; |
jan@42443 | 14 |
@{term "\<rho> "}; |
jan@42443 | 15 |
term2str @{term "\<rho> "}; |
jan@42443 | 16 |
*} |
jan@42443 | 17 |
|
jan@42444 | 18 |
section{*Working with Rulesets*} |
jan@42444 | 19 |
|
jan@42443 | 20 |
axiomatization where |
jan@42443 | 21 |
rule1: "1 = \<delta>[n]" and |
jan@42443 | 22 |
rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and |
jan@42443 | 23 |
rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and |
jan@42443 | 24 |
rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" |
jan@42443 | 25 |
|
jan@42443 | 26 |
ML {* |
jan@42443 | 27 |
@{thm rule1}; |
jan@42443 | 28 |
@{thm rule2}; |
jan@42443 | 29 |
@{thm rule3}; |
jan@42443 | 30 |
@{thm rule4}; |
jan@42443 | 31 |
*} |
jan@42443 | 32 |
|
jan@42444 | 33 |
text{*Create Ruleset and insert rules*} |
jan@42444 | 34 |
|
jan@42443 | 35 |
ML {* |
jan@42444 | 36 |
val transform = append_rls "transform" e_rls |
jan@42443 | 37 |
[ Thm ("rule3",num_str @{thm rule3}), |
jan@42443 | 38 |
Thm ("rule4",num_str @{thm rule4}), |
jan@42443 | 39 |
Thm ("rule1",num_str @{thm rule1}) |
jan@42443 | 40 |
]; |
jan@42443 | 41 |
*} |
jan@42443 | 42 |
|
jan@42444 | 43 |
text{*Apply the Ruleset to a term*} |
jan@42444 | 44 |
|
jan@42443 | 45 |
ML {* |
jan@42444 | 46 |
val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1::real"; |
jan@42444 | 47 |
val SOME (t', asm) = rewrite_set_ thy true transform t; |
jan@42443 | 48 |
*} |
jan@42443 | 49 |
|
jan@42443 | 50 |
ML{* |
jan@42443 | 51 |
term2str t'; |
jan@42443 | 52 |
term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]"; |
jan@42444 | 53 |
term2str t' = "?u [?n] + \<alpha>^^^?n u[n] + ?\<delta> [?n]"; |
jan@42443 | 54 |
*} |
jan@42443 | 55 |
|
jan@42444 | 56 |
text{*Problems: Rule~1 is applied before the expression is checked for Rule~4 |
jan@42444 | 57 |
which would be the correct one. Rule~1 only matches a part of the |
jan@42444 | 58 |
expression.*} |
jan@42443 | 59 |
|
jan@42443 | 60 |
end |