1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed May 13 12:14:49 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed May 13 16:10:22 2020 +0200
1.3 @@ -46,10 +46,10 @@
1.4 val thy = @{theory};
1.5 \<close>
1.6 setup \<open>KEStore_Elems.add_pbts
1.7 - [(Specify.prep_pbt thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
1.8 - (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Problem.id_empty
1.9 + [(Problem.prep_input thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
1.10 + (Problem.prep_input thy "pbl_SP_Ztrans" [] Problem.id_empty
1.11 (["Z_Transform","SignalProcessing"], [], Rule_Set.empty, NONE, [])),
1.12 - (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
1.13 + (Problem.prep_input thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
1.14 (["Inverse", "Z_Transform", "SignalProcessing"],
1.15 [("#Given" , ["filterExpression X_eq"]),
1.16 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
1.17 @@ -59,11 +59,11 @@
1.18 subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
1.19 ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
1.20 setup \<open>KEStore_Elems.add_mets
1.21 - [Specify.prep_met thy "met_SP" [] Method.id_empty
1.22 + [Method.prep_input thy "met_SP" [] Method.id_empty
1.23 (["SignalProcessing"], [],
1.24 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.25 errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
1.26 - Specify.prep_met thy "met_SP_Ztrans" [] Method.id_empty
1.27 + Method.prep_input thy "met_SP_Ztrans" [] Method.id_empty
1.28 (["SignalProcessing", "Z_Transform"], [],
1.29 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.30 errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
1.31 @@ -87,7 +87,7 @@
1.32 [BOOL equ, REAL X_z]
1.33 in X) "
1.34 setup \<open>KEStore_Elems.add_mets
1.35 - [Specify.prep_met thy "met_SP_Ztrans_inv" [] Method.id_empty
1.36 + [Method.prep_input thy "met_SP_Ztrans_inv" [] Method.id_empty
1.37 (["SignalProcessing", "Z_Transform", "Inverse"],
1.38 [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
1.39 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
1.40 @@ -115,7 +115,7 @@
1.41 n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
1.42 in n_eq)"
1.43 setup \<open>KEStore_Elems.add_mets
1.44 - [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Method.id_empty
1.45 + [Method.prep_input thy "met_SP_Ztrans_inv_sub" [] Method.id_empty
1.46 (["SignalProcessing", "Z_Transform", "Inverse_sub"],
1.47 [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
1.48 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>