wneuper@59550: (* Title:  Inverse_Z_Transform
neuper@42256:    Author: Jan Rocnik
neuper@42256:    (c) copyright due to lincense terms.
neuper@42256: *)
neuper@42256: 
Walther@60458: theory Inverse_Z_Transform imports PolyEq Diff_App Partial_Fractions begin
neuper@42256: 
wneuper@59550: axiomatization where       \<comment> \<open>TODO: new variables on the rhs enforce replacement by substitution\<close>
neuper@42256:   rule1: "1 = \<delta>[n]" and
neuper@42256:   rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
neuper@42256:   rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and 
walther@60242:   rule4: "c * (z / (z - \<alpha>)) = c * \<alpha> \<up> n * u [n]" and
walther@60242:   rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha> \<up> n) * u [-n - 1]" and
walther@60242:   rule6: "|| z || > 1 ==> z/(z - 1) \<up> 2 = n * u [n]" (*and
walther@60242:   rule42: "(a * (z/(z-b)) + c * (z/(z-d))) = (a * b \<up> n * u [n] + c * d \<up> n * u [n])"*)
neuper@42256: 
neuper@42256: axiomatization where
wneuper@59537: (*ruleZY: "(X z = a / b) = (d_d z X = a / (z * b))"         ..looks better, but types are flawed*)
jan@42367:   ruleZY: "(X z = a / b) = (X' z = a / (z * b))" and
wneuper@59537:   ruleYZ: "a / (z - b) + c / (z - d) = a * (z / (z - b)) + c * (z / (z - d))" and
wneuper@59537:   ruleYZa: "(a / b + c / d) = (a * (z / b) + c * (z / d))"        \<comment> \<open>that is what students learn\<close>
neuper@42256: 
wneuper@59472: subsection\<open>Define the Field Descriptions for the specification\<close>
neuper@42279: consts
neuper@42279:   filterExpression  :: "bool => una"
wneuper@59550:   stepResponse      :: "bool => una"    \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6 above\<close>
neuper@42279: 
wneuper@59472: ML \<open>
s1210629013@55444: val inverse_z = prep_rls'(
Walther@60509:   Rule_Def.Repeat {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
walther@59851: 	  erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
jan@42366: 	  rules = 
jan@42367: 	   [
wenzelm@60298:     \<^rule_thm>\<open>rule4\<close>
jan@42366: 	   ], 
walther@59878: 	 scr = Rule.Empty_Prog});
wneuper@59472: \<close>
jan@42366: 
jan@42366: 
wneuper@59472: text \<open>store the rule set for math engine\<close>
jan@42366: 
wenzelm@60289: rule_set_knowledge inverse_z = inverse_z
jan@42366: 
wneuper@59472: subsection\<open>Define the Specification\<close>
wenzelm@60291: 
wenzelm@60306: problem pbl_SP : "SignalProcessing" = \<open>Rule_Set.empty\<close>
wenzelm@60306: 
wenzelm@60306: problem pbl_SP_Ztrans : "Z_Transform/SignalProcessing" = \<open>Rule_Set.empty\<close>
wenzelm@60306: 
wenzelm@60306: problem pbl_SP_Ztrans_inv : "Inverse/Z_Transform/SignalProcessing" =
wenzelm@60306:   \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
Walther@60449:   Method_Ref: "SignalProcessing/Z_Transform/Inverse"
wenzelm@60306:   Given: "filterExpression X_eq"
wenzelm@60306:   Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
wenzelm@60306: 
neuper@42256: 
walther@60154: subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\<close>
wenzelm@60290: 
wenzelm@60303: method met_SP : "SignalProcessing" =
wenzelm@60303:   \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
wenzelm@60303:     errpats = [], nrls = Rule_Set.empty}\<close>
wenzelm@60303: 
wenzelm@60303: method met_SP_Ztrans : "SignalProcessing/Z_Transform" =
wenzelm@60303:   \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
wenzelm@60303:     errpats = [], nrls = Rule_Set.empty}\<close>
wneuper@59545: 
wneuper@59545: partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
wneuper@59504:   where
walther@59635: "inverse_ztransform X_eq X_z = (
walther@59635:   let
walther@59635:     X = Take X_eq;
walther@59635:     X' = Rewrite ''ruleZY''  X;                                              \<comment> \<open>z * denominator\<close>
walther@59635:     X' = (Rewrite_Set ''norm_Rational'' ) X';                                       \<comment> \<open>simplify\<close>
walther@59635:     funterm = Take (rhs X');                                \<comment> \<open>drop X' z = for equation solving\<close>
walther@59635:     denom = (Rewrite_Set ''partial_fraction'' ) funterm;                     \<comment> \<open>get_denominator\<close>
walther@59635:     equ = (denom = (0::real));
walther@59635:     fun_arg = Take (lhs X');
walther@59635:     arg = (Rewrite_Set ''partial_fraction'' ) X';                          \<comment> \<open>get_argument TODO\<close>
walther@59635:     (L_L::bool list) = \<comment> \<open>'bool list' inhibits:
walther@59635:                 WARNING: Additional type variable(s) in specification of inverse_ztransform: 'a\<close>
walther@59635:       SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''], [''Test'',''solve_linear''])
walther@59635:         [BOOL equ, REAL X_z]
wneuper@59504:   in X) "
wenzelm@60303: 
wenzelm@60303: method met_SP_Ztrans_inv : "SignalProcessing/Z_Transform/Inverse" =
wenzelm@60303:   \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
wenzelm@60303:     errpats = [], nrls = Rule_Set.empty}\<close>
wenzelm@60303:   Program: inverse_ztransform.simps
wenzelm@60303:   Given: "filterExpression X_eq" "functionName X_z"
wenzelm@60303:   Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
wneuper@59538: 
wneuper@59538: partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool"
wneuper@59504:   where
walther@59635: "inverse_ztransform2 X_eq X_z = (
walther@59635:   let
walther@59635:     X = Take X_eq;
walther@59635:     X' = Rewrite ''ruleZY''  X;
walther@60278:     X_z = lhs X';
walther@60278:     zzz = argument_in X_z;
wneuper@59538:     funterm = rhs X';
wneuper@59592:     pbz = SubProblem (''Isac_Knowledge'',
walther@59635:         [''partial_fraction'',''rational'',''simplification''],
walther@59635:         [''simplification'',''of_rationals'',''to_partial_fraction''])
wneuper@59538:       [REAL funterm, REAL zzz];
walther@60278:     pbz_eq = Take (X_z = pbz);
walther@59635:     pbz_eq = Rewrite ''ruleYZ''  pbz_eq;
wneuper@59538:     X_zeq = Take (X_z = rhs pbz_eq);
walther@59635:     n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
wneuper@59538:   in n_eq)"
wenzelm@60303: 
wenzelm@60303: method met_SP_Ztrans_inv_sub : "SignalProcessing/Z_Transform/Inverse_sub" =
wenzelm@60303:   \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
walther@60358:     srls = Rule_Def.Repeat {
walther@60358:       id = "srls_partial_fraction",  preconds = [], rew_ord = ("termlessI",termlessI),
walther@60358:       erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty [
walther@60358:         \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), (* ...for asm in NTH_CONS*)
walther@60358:         (*2nd NTH_CONS pushes n+-1 into asms*)
walther@60358:         \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], 
walther@60358:       srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358:       rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
walther@60358:         \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
walther@60358:         \<^rule_thm>\<open>NTH_NIL\<close>,
walther@60358:         \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
walther@60358:         \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
walther@60358:         \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
walther@60358:         \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"),
walther@60358:         \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"),
walther@60358:         \<^rule_eval>\<open>factors_from_solution\<close> (eval_factors_from_solution "#factors_from_solution")],
walther@60358:       scr = Rule.Empty_Prog},
wenzelm@60303:     prls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], nrls = norm_Rational}\<close>
wenzelm@60303:   Program: inverse_ztransform2.simps
wenzelm@60303:   Given: "filterExpression X_eq" "functionName X_z"
wenzelm@60303:   Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
wenzelm@60303: 
wneuper@59550: ML \<open>
wneuper@59550: \<close> ML \<open>
walther@60278: \<close> ML \<open>
wneuper@59550: \<close>
neuper@42256: 
neuper@42256: end
neuper@42256: