author | wneuper <Walther.Neuper@jku.at> |
Sun, 09 Oct 2022 07:44:22 +0200 | |
changeset 60565 | f92963a33fe3 |
parent 60242 | 73ee61385493 |
child 60665 | fad0cbfb586d |
permissions | -rw-r--r-- |
jan@42443 | 1 |
|
wneuper@59592 | 2 |
theory example_2 imports Isac.Isac_Knowledge |
jan@42443 | 3 |
begin |
jan@42443 | 4 |
|
wneuper@59472 | 5 |
section\<open>Symbol Representation\<close> |
jan@42444 | 6 |
|
wneuper@59472 | 7 |
ML \<open> |
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> "}; |
walther@59868 | 15 |
UnparseC.term @{term "\<rho> "}; |
wneuper@59472 | 16 |
\<close> |
jan@42443 | 17 |
|
wneuper@59472 | 18 |
section\<open>Working with Rulesets\<close> |
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 |
walther@60242 | 24 |
rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>\<up>n * u [n]" |
jan@42443 | 25 |
|
wneuper@59472 | 26 |
ML \<open> |
jan@42443 | 27 |
@{thm rule1}; |
jan@42443 | 28 |
@{thm rule2}; |
jan@42443 | 29 |
@{thm rule3}; |
jan@42443 | 30 |
@{thm rule4}; |
wneuper@59472 | 31 |
\<close> |
jan@42443 | 32 |
|
wneuper@59472 | 33 |
text\<open>Create Ruleset and insert rules\<close> |
jan@42444 | 34 |
|
wneuper@59472 | 35 |
ML \<open> |
walther@59852 | 36 |
val transform = Rule_Set.append_rules "transform" Rule_Set.empty |
walther@59871 | 37 |
[ Thm ("rule3",ThmC.numerals_to_Free @{thm rule3}), |
walther@59871 | 38 |
Thm ("rule4",ThmC.numerals_to_Free @{thm rule4}), |
walther@59871 | 39 |
Thm ("rule1",ThmC.numerals_to_Free @{thm rule1}) |
jan@42443 | 40 |
]; |
wneuper@59472 | 41 |
\<close> |
jan@42443 | 42 |
|
wneuper@59472 | 43 |
text\<open>Apply the Ruleset to a term\<close> |
jan@42444 | 44 |
|
wneuper@59472 | 45 |
ML \<open> |
Walther@60565 | 46 |
val t = parse_test @{context} "z / (z - 1) + z / (z - \<alpha>) + 1::real"; |
jan@42444 | 47 |
val SOME (t', asm) = rewrite_set_ thy true transform t; |
wneuper@59472 | 48 |
\<close> |
jan@42443 | 49 |
|
wneuper@59472 | 50 |
ML\<open> |
walther@59868 | 51 |
UnparseC.term t'; |
walther@59868 | 52 |
UnparseC.term t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]"; |
walther@60242 | 53 |
UnparseC.term t' = "?u [?n] + \<alpha>\<up>?n u[n] + ?\<delta> [?n]"; |
wneuper@59472 | 54 |
\<close> |
jan@42443 | 55 |
|
wneuper@59472 | 56 |
text\<open>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 |
wneuper@59472 | 58 |
expression.\<close> |
jan@42443 | 59 |
|
jan@42443 | 60 |
end |