(* 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 Partial_Fractions 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: "c * (z / (z - \<alpha>)) = c * \<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]" (*and

  rule42: "(a * (z/(z-b)) + c * (z/(z-d))) = (a * b^^^n * u [n] + c * d^^^n * u [n])"*)

axiomatization where

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

  ruleYZ: "(a/b + c/d) = (a*(z/b) + c*(z/d))" 

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

consts

  filterExpression  :: "bool => una"

  stepResponse      :: "bool => una"

ML {*

val inverse_z = prep_rls(

  Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 

	  erls = Erls, srls = Erls, calc = [],

	  rules = 

	   [

    Thm ("rule4",num_str @{thm rule4})

	   ], 

	 scr = EmptyScr}:rls);

*}

text {*store the rule set for math engine*}

ML {*

ruleset' := overwritelthy @{theory} (!ruleset',

  [("inverse_z", inverse_z)

   ]);

*}

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 (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)

" (let X = Take X_eq;" ^

"      X' = Rewrite ruleZY False X;" ^ (*z * denominator*)

"      X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)

"      funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*)

"      denom = (Rewrite_Set partial_fraction False) funterm;" ^ (*get_denominator*)

"      equ = (denom = (0::real));" ^

"      fun_arg = Take (lhs X');" ^

"      arg = (Rewrite_Set partial_fraction False) X';" ^ (*get_argument TODO*)

"      (L_L::bool list) =                                    " ^

"            (SubProblem (Test',                            " ^

"                         [linear,univariate,equation,test]," ^

"                         [Test,solve_linear])              " ^

"                        [BOOL equ, REAL z])              " ^

"  in X)"

 ));

*}

end