equal
deleted
inserted
replaced
1 (* Title: Inverse_Z_Transform |
1 (* Title: Inverse_Z_Transform |
2 Author: Jan Rocnik |
2 Author: Jan Rocnik |
3 (c) copyright due to lincense terms. |
3 (c) copyright due to lincense terms. |
4 *) |
4 *) |
5 |
5 |
6 theory Inverse_Z_Transform imports PolyEq DiffApp Partial_Fractions begin |
6 theory Inverse_Z_Transform imports PolyEq Diff_App Partial_Fractions begin |
7 |
7 |
8 axiomatization where \<comment> \<open>TODO: new variables on the rhs enforce replacement by substitution\<close> |
8 axiomatization where \<comment> \<open>TODO: new variables on the rhs enforce replacement by substitution\<close> |
9 rule1: "1 = \<delta>[n]" and |
9 rule1: "1 = \<delta>[n]" and |
10 rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and |
10 rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and |
11 rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and |
11 rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and |