src/Tools/isac/Knowledge/Inverse_Z_Transform.thy
changeset 59473 28b67cae58c3
parent 59472 3e904f8ec16c
child 59489 cfcbcac0bae8
     1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Nov 21 12:32:54 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Nov 28 11:46:00 2018 +0100
     1.3 @@ -73,15 +73,17 @@
     1.4  subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
     1.5  ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
     1.6  setup \<open>KEStore_Elems.add_mets
     1.7 -  [Specify.prep_met thy "met_SP" [] Celem.e_metID
     1.8 +    [Specify.prep_met thy "met_SP" [] Celem.e_metID
     1.9        (["SignalProcessing"], [],
    1.10          {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
    1.11            errpats = [], nrls = Rule.e_rls}, "empty_script"),
    1.12      Specify.prep_met thy "met_SP_Ztrans" [] Celem.e_metID
    1.13        (["SignalProcessing", "Z_Transform"], [],
    1.14          {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
    1.15 -          errpats = [], nrls = Rule.e_rls}, "empty_script"),
    1.16 -    Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
    1.17 +          errpats = [], nrls = Rule.e_rls}, "empty_script")]
    1.18 +\<close>
    1.19 +setup \<open>KEStore_Elems.add_mets
    1.20 +    [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
    1.21        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.22          [("#Given" ,["filterExpression (X_eq::bool)"]),
    1.23            ("#Find"  ,["stepResponse (n_eq::bool)"])],
    1.24 @@ -101,8 +103,10 @@
    1.25            "                         [LINEAR,univariate,equation,test]," ^
    1.26            "                         [Test,solve_linear])              " ^
    1.27            "                        [BOOL equ, REAL z])              " ^
    1.28 -          "  in X)"),
    1.29 -    Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
    1.30 +          "  in X)")]
    1.31 +\<close>
    1.32 +setup \<open>KEStore_Elems.add_mets
    1.33 +    [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
    1.34        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.35          [("#Given" ,["filterExpression X_eq"]),
    1.36            ("#Find"  ,["stepResponse n_eq"])],
    1.37 @@ -174,8 +178,10 @@
    1.38             "      (X_z::bool) = Take (X_z = pbz);                          "^
    1.39             "      (n_eq::bool) = (Rewrite_Set inverse_z False) X_z;        "^
    1.40             "      n_eq = drop_questionmarks n_eq                           "^
    1.41 -           "in n_eq)"),
    1.42 -    Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
    1.43 +           "in n_eq)")]
    1.44 +\<close>
    1.45 +setup \<open>KEStore_Elems.add_mets
    1.46 +    [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
    1.47        (["SignalProcessing", "Z_Transform", "Inverse_sub"], 
    1.48          [("#Given" ,["filterExpression X_eq"]),
    1.49            ("#Find"  ,["stepResponse n_eq"])],