(* Title:  Test_Z_Transform

   Author: Jan Rocnik

   (c) copyright due to lincense terms.

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

*)

theory Inverse_Z_Transform imports PolyEq DiffApp begin

axiomatization where 

  rule1: "1 = \<delta>[n]" and

  rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and

  rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and 

  rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and

  rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and

  rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"

axiomatization where

  ruleZY: "(X z = a / b) = (X' z = a / (z * b))"

subsection{*Define the Field Descriptions for the specification*}

consts

  filterExpression  :: "bool => una"

  stepResponse      :: "bool => una"

subsection{*Define the Specification*}

ML {*

val thy = @{theory};

store_pbt

 (prep_pbt thy "pbl_SP" [] e_pblID

 (["SignalProcessing"], [], e_rls, NONE, []));

store_pbt

 (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID

 (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));

store_pbt

 (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID

 (["inverse", "Z_Transform", "SignalProcessing"],

  [("#Given" ,["filterExpression (X_eq::bool)"]),

   ("#Find"  ,["stepResponse (n_eq::bool)"])

  ],

  append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 

  [["SignalProcessing","Z_Transform","inverse"]]));

*}

subsection {*Define Name and Signature for the Method*}

consts

  InverseZTransform :: "[bool, bool] => bool"

    ("((Script InverseZTransform (_ =))// (_))" 9)

subsection {*Setup Parent Nodes in Hierarchy of Method*}

ML {*

store_met

 (prep_met thy "met_SP" [] e_metID

 (["SignalProcessing"], [],

   {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,

    crls = e_rls, nrls = e_rls}, "empty_script"));

store_met

 (prep_met thy "met_SP_Ztrans" [] e_metID

 (["SignalProcessing", "Z_Transform"], [],

   {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,

    crls = e_rls, nrls = e_rls}, "empty_script"));

val thy = @{theory}; (*latest version of thy required*)

store_met

 (prep_met thy "met_SP_Ztrans_inv" [] e_metID

 (["SignalProcessing", "Z_Transform", "inverse"], 

  [("#Given" ,["filterExpression (X_eq::bool)"]),

   ("#Find"  ,["stepResponse (n_eq::bool)"])

  ],

   {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,

    crls = e_rls, nrls = e_rls},

  "Script InverseZTransform (Xeq::bool) =" ^

  " (let X = Take Xeq;" ^

  "      X = Rewrite ruleZY False X" ^

  "  in X)"

 ));

*}

end