1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Thu Sep 26 17:47:10 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Tue Oct 01 10:47:25 2019 +0200
     1.3 @@ -71,19 +71,20 @@
     1.4  
     1.5  partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
     1.6    where
     1.7 -"inverse_ztransform X_eq X_z =                                       \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
     1.8 - (let X = Take X_eq;
     1.9 -      X' = Rewrite ''ruleZY'' False X;                                         \<comment> \<open>z * denominator\<close>
    1.10 -      X' = (Rewrite_Set ''norm_Rational'' False) X';                                  \<comment> \<open>simplify\<close>
    1.11 -      funterm = Take (rhs X');                                \<comment> \<open>drop X' z = for equation solving\<close>
    1.12 -      denom = (Rewrite_Set ''partial_fraction'' False) funterm;                \<comment> \<open>get_denominator\<close>
    1.13 -      equ = (denom = (0::real));
    1.14 -      fun_arg = Take (lhs X');
    1.15 -      arg = (Rewrite_Set ''partial_fraction'' False) X';                     \<comment> \<open>get_argument TODO\<close>
    1.16 -      (L_L::bool list) = \<comment> \<open>'bool list' inhibits (?!?):
    1.17 -                  WARNING: Additional type variable(s) in specification of inverse_ztransform: 'a\<close>
    1.18 -        SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],
    1.19 -          [''Test'',''solve_linear'']) [BOOL equ, REAL X_z]
    1.20 +"inverse_ztransform X_eq X_z = (
    1.21 +  let
    1.22 +    X = Take X_eq;
    1.23 +    X' = Rewrite ''ruleZY''  X;                                              \<comment> \<open>z * denominator\<close>
    1.24 +    X' = (Rewrite_Set ''norm_Rational'' ) X';                                       \<comment> \<open>simplify\<close>
    1.25 +    funterm = Take (rhs X');                                \<comment> \<open>drop X' z = for equation solving\<close>
    1.26 +    denom = (Rewrite_Set ''partial_fraction'' ) funterm;                     \<comment> \<open>get_denominator\<close>
    1.27 +    equ = (denom = (0::real));
    1.28 +    fun_arg = Take (lhs X');
    1.29 +    arg = (Rewrite_Set ''partial_fraction'' ) X';                          \<comment> \<open>get_argument TODO\<close>
    1.30 +    (L_L::bool list) = \<comment> \<open>'bool list' inhibits:
    1.31 +                WARNING: Additional type variable(s) in specification of inverse_ztransform: 'a\<close>
    1.32 +      SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''], [''Test'',''solve_linear''])
    1.33 +        [BOOL equ, REAL X_z]
    1.34    in X) "
    1.35  setup \<open>KEStore_Elems.add_mets
    1.36      [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
    1.37 @@ -97,20 +98,21 @@
    1.38  
    1.39  partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool"
    1.40    where
    1.41 -"inverse_ztransform2 X_eq X_z =
    1.42 -  (let X = Take X_eq;
    1.43 -    X' = Rewrite ''ruleZY'' False X;
    1.44 +"inverse_ztransform2 X_eq X_z = (
    1.45 +  let
    1.46 +    X = Take X_eq;
    1.47 +    X' = Rewrite ''ruleZY''  X;
    1.48      X'_z = lhs X';
    1.49      zzz = argument_in X'_z;
    1.50      funterm = rhs X';
    1.51      pbz = SubProblem (''Isac_Knowledge'',
    1.52 -      [''partial_fraction'',''rational'',''simplification''],
    1.53 -      [''simplification'',''of_rationals'',''to_partial_fraction''])
    1.54 +        [''partial_fraction'',''rational'',''simplification''],
    1.55 +        [''simplification'',''of_rationals'',''to_partial_fraction''])
    1.56        [REAL funterm, REAL zzz];
    1.57      pbz_eq = Take (X'_z = pbz);
    1.58 -    pbz_eq = Rewrite ''ruleYZ'' False pbz_eq;
    1.59 +    pbz_eq = Rewrite ''ruleYZ''  pbz_eq;
    1.60      X_zeq = Take (X_z = rhs pbz_eq);
    1.61 -    n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq
    1.62 +    n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
    1.63    in n_eq)"
    1.64  setup \<open>KEStore_Elems.add_mets
    1.65      [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID