1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Apr 05 16:44:21 2012 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Apr 05 16:53:43 2012 +0200
1.3 @@ -58,12 +58,12 @@
1.4 (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
1.5 store_pbt
1.6 (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
1.7 - (["inverse", "Z_Transform", "SignalProcessing"],
1.8 + (["Inverse", "Z_Transform", "SignalProcessing"],
1.9 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.10 ("#Find" ,["stepResponse (n_eq::bool)"])
1.11 ],
1.12 append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
1.13 - [["SignalProcessing","Z_Transform","inverse"]]));
1.14 + [["SignalProcessing","Z_Transform","Inverse"]]));
1.15 *}
1.16
1.17 subsection {*Define Name and Signature for the Method*}
1.18 @@ -86,7 +86,7 @@
1.19 val thy = @{theory}; (*latest version of thy required*)
1.20 store_met
1.21 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.22 - (["SignalProcessing", "Z_Transform", "inverse"],
1.23 + (["SignalProcessing", "Z_Transform", "Inverse"],
1.24 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.25 ("#Find" ,["stepResponse (n_eq::bool)"])
1.26 ],
2.1 --- a/src/Tools/isac/TODO.txt Thu Apr 05 16:44:21 2012 +0200
2.2 +++ b/src/Tools/isac/TODO.txt Thu Apr 05 16:53:43 2012 +0200
2.3 @@ -123,7 +123,7 @@
2.4 ["diff","integration"]
2.5 ["diff","integration","named"]
2.6 Inverse_Z_Transform
2.7 - ["SignalProcessing", "Z_Transform", "inverse"]
2.8 + ["SignalProcessing", "Z_Transform", "Inverse"]
2.9 Isac //
2.10 LinEq //
2.11 LogExp //
3.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Apr 05 16:44:21 2012 +0200
3.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Apr 05 16:53:43 2012 +0200
3.3 @@ -523,7 +523,7 @@
3.4 \begin{verbatim}
3.5 val {srls,...} = get_met ["SignalProcessing",
3.6 "Z_Transform",
3.7 - "inverse"];
3.8 + "Inverse"];
3.9 \end{verbatim}
3.10
3.11 \par \noindent Create 2 good example terms:
3.12 @@ -905,15 +905,15 @@
3.13 ML {*
3.14 store_pbt
3.15 (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
3.16 - (["inverse", "Z_Transform", "SignalProcessing"],
3.17 + (["Inverse", "Z_Transform", "SignalProcessing"],
3.18 [("#Given" ,["filterExpression X_eq"]),
3.19 ("#Find" ,["stepResponse n_eq"])
3.20 ],
3.21 append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
3.22 - [["SignalProcessing","Z_Transform","inverse"]]));
3.23 + [["SignalProcessing","Z_Transform","Inverse"]]));
3.24
3.25 show_ptyps();
3.26 - get_pbt ["inverse","Z_Transform","SignalProcessing"];
3.27 + get_pbt ["Inverse","Z_Transform","SignalProcessing"];
3.28 *}
3.29
3.30 subsection {*Define Name and Signature for the Method*}
3.31 @@ -954,7 +954,7 @@
3.32 ML {*
3.33 store_met
3.34 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
3.35 - (["SignalProcessing", "Z_Transform", "inverse"],
3.36 + (["SignalProcessing", "Z_Transform", "Inverse"],
3.37 [("#Given" ,["filterExpression X_eq"]),
3.38 ("#Find" ,["stepResponse n_eq"])
3.39 ],
3.40 @@ -970,7 +970,7 @@
3.41 ML {*
3.42 store_met
3.43 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
3.44 - (["SignalProcessing", "Z_Transform", "inverse"],
3.45 + (["SignalProcessing", "Z_Transform", "Inverse"],
3.46 [("#Given" ,["filterExpression X_eq"]),
3.47 ("#Find" ,["stepResponse n_eq"])
3.48 ],
3.49 @@ -993,7 +993,7 @@
3.50 the hierarchy.*}
3.51
3.52 ML {*
3.53 - get_met ["SignalProcessing","Z_Transform","inverse"];
3.54 + get_met ["SignalProcessing","Z_Transform","Inverse"];
3.55 *}
3.56
3.57 section {*Program in TP-based language \label{prog-steps}*}
3.58 @@ -1150,7 +1150,7 @@
3.59 prep_met thy "met_SP_Ztrans_inv" [] e_metID
3.60 (["SignalProcessing",
3.61 "Z_Transform",
3.62 - "inverse"],
3.63 + "Inverse"],
3.64 [
3.65 ("#Given" ,["filterExpression X_eq"]),
3.66 ("#Find" ,["stepResponse n_eq"])
3.67 @@ -1245,8 +1245,8 @@
3.68 ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
3.69 "stepResponse (x[n::real]::bool)"];
3.70 val (dI,pI,mI) =
3.71 - ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
3.72 - ["SignalProcessing","Z_Transform","inverse"]);
3.73 + ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
3.74 + ["SignalProcessing","Z_Transform","Inverse"]);
3.75
3.76 val ([
3.77 (
3.78 @@ -1269,7 +1269,7 @@
3.79 val Script sc
3.80 = (#scr o get_met) ["SignalProcessing",
3.81 "Z_Transform",
3.82 - "inverse"];
3.83 + "Inverse"];
3.84 atomty sc;
3.85 *}
3.86
3.87 @@ -1287,8 +1287,8 @@
3.88 "stepResponse (x[n::real]::bool)"];
3.89
3.90 val (dI,pI,mI) =
3.91 - ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
3.92 - ["SignalProcessing","Z_Transform","inverse"]);
3.93 + ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
3.94 + ["SignalProcessing","Z_Transform","Inverse"]);
3.95
3.96 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
3.97 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.98 @@ -1344,7 +1344,7 @@
3.99 val Script s =
3.100 (#scr o get_met) ["SignalProcessing",
3.101 "Z_Transform",
3.102 - "inverse"];
3.103 + "Inverse"];
3.104 writeln (term2str s);
3.105 \end{verbatim}
3.106 \ldots shows the right script. Difference in the arguments.
4.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Thu Apr 05 16:44:21 2012 +0200
4.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Thu Apr 05 16:53:43 2012 +0200
4.3 @@ -1004,7 +1004,7 @@
4.4 \begin{verbatim}
4.5 val {srls,...} = get_met ["SignalProcessing",
4.6 "Z_Transform",
4.7 - "inverse"];
4.8 + "Inverse"];
4.9 \end{verbatim}
4.10
4.11 \par \noindent Create 2 good example terms:
4.12 @@ -2393,7 +2393,7 @@
4.13 val Script s =
4.14 (#scr o get_met) ["SignalProcessing",
4.15 "Z_Transform",
4.16 - "inverse"];
4.17 + "Inverse"];
4.18 writeln (term2str s);
4.19 \end{verbatim}
4.20 \ldots shows the right script. Difference in the arguments.
5.1 --- a/test/Tools/isac/Interpret/mathengine.sml Thu Apr 05 16:44:21 2012 +0200
5.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Thu Apr 05 16:53:43 2012 +0200
5.3 @@ -481,8 +481,8 @@
5.4
5.5 val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
5.6 "stepResponse (x[n::real]::bool)"];
5.7 -val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
5.8 - ["SignalProcessing","Z_Transform","inverse"]);
5.9 +val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
5.10 + ["SignalProcessing","Z_Transform","Inverse"]);
5.11
5.12 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
5.13 (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
6.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Thu Apr 05 16:44:21 2012 +0200
6.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Thu Apr 05 16:53:43 2012 +0200
6.3 @@ -16,16 +16,16 @@
6.4 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
6.5 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
6.6 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
6.7 -get_pbt ["inverse","Z_Transform","SignalProcessing"];
6.8 -get_met ["SignalProcessing","Z_Transform","inverse"];
6.9 +get_pbt ["Inverse","Z_Transform","SignalProcessing"];
6.10 +get_met ["SignalProcessing","Z_Transform","Inverse"];
6.11
6.12 "----------- test [SignalProcessing,Z_Transform,inverse] ---";
6.13 "----------- test [SignalProcessing,Z_Transform,inverse] ---";
6.14 "----------- test [SignalProcessing,Z_Transform,inverse] ---";
6.15 val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
6.16 "stepResponse x[(n::real)]"];
6.17 -val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
6.18 - ["SignalProcessing","Z_Transform","inverse"]);
6.19 +val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
6.20 + ["SignalProcessing","Z_Transform","Inverse"]);
6.21 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
6.22 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
6.23
7.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Thu Apr 05 16:44:21 2012 +0200
7.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Thu Apr 05 16:53:43 2012 +0200
7.3 @@ -24,8 +24,8 @@
7.4 "----------- why helpless here ? ------------------------";
7.5 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
7.6 "stepResponse (x[n::real]::bool)"];
7.7 -val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
7.8 - ["SignalProcessing","Z_Transform","inverse"]);
7.9 +val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
7.10 + ["SignalProcessing","Z_Transform","Inverse"]);
7.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
7.12 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
7.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
7.14 @@ -43,7 +43,7 @@
7.15 val pIopt = get_pblID (pt,ip);
7.16 ip = ([],Res); "false";
7.17 tacis; " = []";
7.18 -pIopt; (* = SOME ["inverse", "Z_Transform", "SignalProcessing"]*)
7.19 +pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*)
7.20 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";
7.21 (*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
7.22 THIS MEANS: replace no_meth by [no_meth] in Script.*)
7.23 @@ -62,7 +62,7 @@
7.24 val pIopt = get_pblID (pt,ip);
7.25 ip = ([],Res); " = false";
7.26 tacis; " = []";
7.27 -pIopt (* = SOME ["inverse", "Z_Transform", "SignalProcessing"]*);
7.28 +pIopt (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*);
7.29 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); " = false";
7.30 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into
7.31 nxt_solve_, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
8.1 --- a/test/Tools/isac/Test_Some.thy Thu Apr 05 16:44:21 2012 +0200
8.2 +++ b/test/Tools/isac/Test_Some.thy Thu Apr 05 16:53:43 2012 +0200
8.3 @@ -33,11 +33,11 @@
8.4 ML {*
8.5 pbl_hierarchy2file (path ^ "pbl/");
8.6 *}
8.7 -text {*
8.8 +ML {*
8.9 pbls2file (path ^ "pbl/");
8.10 *}
8.11 ML {*
8.12 -str2term "inverse" (* = Const ("Rings.inverse_class.inverse", "RealDef.real \<Rightarrow> RealDef.real")*)
8.13 +str2term "Inverse" (* = Const ("Rings.inverse_class.inverse", "RealDef.real \<Rightarrow> RealDef.real")*)
8.14 *}
8.15 ML {*
8.16 met_hierarchy2file (path ^ "met/");