1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Mon Apr 08 16:10:07 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Tue Apr 09 11:38:26 2019 +0200
1.3 @@ -17,8 +17,10 @@
1.4 rule42: "(a * (z/(z-b)) + c * (z/(z-d))) = (a * b^^^n * u [n] + c * d^^^n * u [n])"*)
1.5
1.6 axiomatization where
1.7 +(*ruleZY: "(X z = a / b) = (d_d z X = a / (z * b))" ..looks better, but types are flawed*)
1.8 ruleZY: "(X z = a / b) = (X' z = a / (z * b))" and
1.9 - ruleYZ: "(a/b + c/d) = (a*(z/b) + c*(z/d))"
1.10 + ruleYZ: "a / (z - b) + c / (z - d) = a * (z / (z - b)) + c * (z / (z - d))" and
1.11 + ruleYZa: "(a / b + c / d) = (a * (z / b) + c * (z / d))" \<comment> \<open>that is what students learn\<close>
1.12
1.13 subsection\<open>Define the Field Descriptions for the specification\<close>
1.14 consts
1.15 @@ -95,7 +97,7 @@
1.16 fun_arg = Take (lhs X');
1.17 arg = (Rewrite_Set ''partial_fraction'' False) X'; \<comment> \<open>get_argument TODO\<close>
1.18 L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],
1.19 - [''Test'',''solve_linear'']) [BOOL equ, STRING ''z''] \<comment> \<open>PROG string\<close>
1.20 + [''Test'',''solve_linear'']) [BOOL equ, REAL z] \<comment> \<open>PROG --> as arg\<close>
1.21 in X) "
1.22 *)
1.23 setup \<open>KEStore_Elems.add_mets
2.1 --- a/src/Tools/isac/TODO.thy Mon Apr 08 16:10:07 2019 +0200
2.2 +++ b/src/Tools/isac/TODO.thy Tue Apr 09 11:38:26 2019 +0200
2.3 @@ -13,21 +13,13 @@
2.4 String constants have already bee introduced to old string-programs.
2.5 Shifting this program code into partial_function reveals further issues:
2.6 \begin{itemize}
2.7 -\item "partial_function xxx .." introduces a constant "xxx" (see xxx.simps), might break tests
2.8 \item Diff.thy
2.9 \begin{itemize}
2.10 \item differentiateX --> differentiate after removal of script-constant
2.11 \end{itemize}
2.12 -\item Inverse_Z_Transform.thy:
2.13 - \begin{itemize}
2.14 - \item inverse_ztransform2, inverse_ztransform3 --- what can be dropped?
2.15 - Type unification failed: Clash of types "bool" and "_ itself"
2.16 - Type error in application: incompatible operand type
2.17 - Operator: Let (Take X_eq) :: (??'a itself \<Rightarrow> ??'b) \<Rightarrow> ??'b
2.18 - Operand:
2.19 - \<lambda>X. let X' = Rewrite ''ruleZY'' ...
2.20 - \item ''z''] \<comment> \<open>PROG string\<close>
2.21 - \end{itemize}
2.22 +\item Inverse_Z_Transform.thy: thm ruleZY introduces a new variable on the rhs of the rewrite-rule.
2.23 + The problem is related to the decision of typing for "d_d" and making bound variables free (while
2.24 + shifting specific handling in equation solving etc. to the metalogic.
2.25 \item Test.thy: met_test_sqrt2: deleted?!
2.26 \item
2.27 \begin{itemize}
3.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Mon Apr 08 16:10:07 2019 +0200
3.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Tue Apr 09 11:38:26 2019 +0200
3.3 @@ -1,17 +1,15 @@
3.4 (* Title: Knowledge/Inverse_Z_Transform/inverse_z_transform.sml
3.5 Author: Jan Rocnik
3.6 (c) copyright due to lincense terms.
3.7 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
3.8 - 10 20 30 40 50 60 70 80
3.9 *)
3.10
3.11 "-----------------------------------------------------------------";
3.12 "table of contents -----------------------------------------------";
3.13 "-----------------------------------------------------------------";
3.14 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
3.15 -"----------- syntax [SignalProcessing,Z_Transform,inverse_sub] ---";
3.16 -"----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
3.17 -"----------- test [SignalProcessing,Z_Transform,inverse_sub] autoc";
3.18 +"----------- syntax [SignalProcessing,Z_Transform,Inverse_sub] ---";
3.19 +"----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
3.20 +"----------- test [SignalProcessing,Z_Transform,Inverse_sub] autoc";
3.21 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
3.22 "----------- [Signal..,inverse] (Step 1): <ISA> rhs (?X' z = ... -";
3.23 "-----------------------------------------------------------------";
3.24 @@ -23,9 +21,9 @@
3.25 get_pbt ["Inverse","Z_Transform","SignalProcessing"];
3.26 get_met ["SignalProcessing","Z_Transform","Inverse"];
3.27
3.28 -"----------- syntax [SignalProcessing,Z_Transform,inverse_sub] ---";
3.29 -"----------- syntax [SignalProcessing,Z_Transform,inverse_sub] ---";
3.30 -"----------- syntax [SignalProcessing,Z_Transform,inverse_sub] ---";
3.31 +"----------- syntax [SignalProcessing,Z_Transform,Inverse_sub] ---";
3.32 +"----------- syntax [SignalProcessing,Z_Transform,Inverse_sub] ---";
3.33 +"----------- syntax [SignalProcessing,Z_Transform,Inverse_sub] ---";
3.34 val str =
3.35 "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
3.36 "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
3.37 @@ -77,7 +75,7 @@
3.38
3.39 (*[2,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.40 if p = ([2, 1], Frm) andalso f2str fb = "3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))"
3.41 -then () else error "Z_Transform,inverse_sub] me 1"; (*Rewrite_Set "norm_Rational"*)
3.42 +then () else error "Z_Transform,Inverse_sub] me 1"; (*Rewrite_Set "norm_Rational"*)
3.43
3.44 (*[2, 1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac", ["abcFormula", "degree_2", "po...a*)
3.45 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.46 @@ -90,7 +88,7 @@
3.47 (*[2,2], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"*)
3.48 (*[2,2,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.49 if p = ([2, 2, 1], Frm) andalso f2str fb = "-1 + -2 * z + 8 * z ^^^ 2 = 0"
3.50 -then () else error "Z_Transform,inverse_sub] me 2";
3.51 +then () else error "Z_Transform,Inverse_sub] me 2";
3.52
3.53 (*[2,2,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.54 (*[2,2,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.55 @@ -104,7 +102,7 @@
3.56 (*[2,5], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*"Substitute ["z = 1 / 2"]*)
3.57 (*[2,5], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.58 if p = ([2, 5], Res) andalso f2str fb = "3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2)"
3.59 -then () else error "Z_Transform,inverse_sub] me 3"; (*Rewrite_Set "norm_Rational"*)
3.60 +then () else error "Z_Transform,Inverse_sub] me 3"; (*Rewrite_Set "norm_Rational"*)
3.61
3.62 (*[2, 6], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem (Isac, ["normalise","polynomial","univariate","equation"]*)
3.63 (*[2,7], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.64 @@ -119,7 +117,7 @@
3.65 (*[2,7,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.66 (*[2,7,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.67 if p = ([2, 7, 2], Res) andalso f2str fb = "3 / 1 + -3 / 4 * AA = 0"
3.68 -then () else error "Z_Transform,inverse_sub] me 5";
3.69 +then () else error "Z_Transform,Inverse_sub] me 5";
3.70
3.71 (*[2,7,3], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem*)
3.72 (*[2,7,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.73 @@ -132,7 +130,7 @@
3.74 (*[2,7,4], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
3.75 (*[2,7,4,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.76 if p = ([2, 7, 4, 1], Frm) andalso f2str fb = "3 + -3 / 4 * AA = 0"
3.77 -then () else error "Z_Transform,inverse_sub] me 6";
3.78 +then () else error "Z_Transform,Inverse_sub] me 6";
3.79
3.80 (*[2,7,4,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.81 (*[2,7,4,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.82 @@ -144,7 +142,7 @@
3.83 (*[2,8], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.84 (*[2,8], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.85 if p = ([2, 8], Res) andalso f2str fb = "3 = AA * (-1 / 4 - -1 / 4) + BB * (-1 / 4 - 1 / 2)"
3.86 -then () else error "Z_Transform,inverse_sub] me 7";
3.87 +then () else error "Z_Transform,Inverse_sub] me 7";
3.88
3.89 (*[2,9], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem*)
3.90 (*[2,10], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.91 @@ -157,12 +155,12 @@
3.92 (*[2,10], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "normalise_poly"]*)
3.93 (*[2,10,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.94 if p = ([2, 10, 1], Frm) andalso f2str fb = "3 = -3 * BB / 4"
3.95 -then () else error "Z_Transform,inverse_sub] me 8";
3.96 +then () else error "Z_Transform,Inverse_sub] me 8";
3.97
3.98 (*[2,10,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.99 (*[2,10,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.100 if p = ([2, 10, 2], Res) andalso f2str fb = "3 / 1 + 3 / 4 * BB = 0"
3.101 -then () else error "Z_Transform,inverse_sub] me 9";
3.102 +then () else error "Z_Transform,Inverse_sub] me 9";
3.103
3.104 (*[2,10,3], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem*)
3.105 (*[2,10,4], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.106 @@ -176,7 +174,7 @@
3.107 (*[2,10,4], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
3.108 (*[2,10,4,1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.109 if p = ([2, 10, 4, 1], Frm) andalso f2str fb = "3 + 3 / 4 * BB = 0"
3.110 -then () else error "Z_Transform,inverse_sub] me 10";
3.111 +then () else error "Z_Transform,Inverse_sub] me 10";
3.112
3.113 (*[2,10,4,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.114 (*[2,10,4,2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.115 @@ -188,29 +186,25 @@
3.116 (*[2,11], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
3.117 (*[2,11], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond ["partial_fraction","rational","simplification"]*)
3.118 (*[2], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.119 -f2str fb = "X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))"; (*old*)(*Take "?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)"*)
3.120 +f2str fb = "X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))"; (*Take "?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)"*)
3.121
3.122 -(*[3], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Rewrite ("ruleYZ", "?a / ?b + ?c / ?d = ?a * (?z / ?b) + ?c * (?z / ?d)")*)
3.123 -f2str fb = "?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)"; (*new = old*)
3.124 +(*[3], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.125 +f2str fb = "?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)"; (*Rewrite ("ruleYZ", "?a / ?b + ?c / ?d = ?a * (?z / ?b) + ?c * (?z / ?d)")*)
3.126
3.127 -(*[3], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Take "X_z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))"*)
3.128 -f2str fb = "?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))"; (*new = old*)
3.129 +(*[3], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.130 +f2str fb = "?X' z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))";(*Take "X_z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))"*)
3.131
3.132 -(*//----------------------------- first correct "free variables on rhs" ----------------------\\
3.133 -(*[4], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Empty_Tac new*)
3.134 -(*f2str fb new*)
3.135 -f2str fb = "X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))"; (*Rewrite_Set "inverse_z" old*)
3.136 -(*[4], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Check_Postcond ["Inverse", "Z_Transform", "SignalProcessing"]*)
3.137 -(*f2str fb /// new*)
3.138 -f2str fb = "X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]"; (*old*)
3.139 -(*[], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*End_Proof*)
3.140 -f2str fb = "X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]" (*old*)
3.141 +(*[4], Frm)*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.142 +(*[4], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.143 +(*[], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
3.144
3.145 -if p = ([], Res) andalso f2str fb = "X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]"
3.146 -then () else error "z-trans (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real)))) changed";
3.147 - \\----------------------------- first correct "free variables on rhs" ----------------------//*)
3.148 -show_pt_tac pt;
3.149 -(* [
3.150 +case nxt of (_, End_Proof') =>
3.151 + if p = ([], Res) andalso
3.152 + f2str fb = "X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]"
3.153 + then () else error "[SignalProcessing,Z_Transform,Inverse_sub] changed 1"
3.154 +| _ => error "[SignalProcessing,Z_Transform,Inverse_sub] changed 2"
3.155 +
3.156 +(* show_pt_tac pt; [
3.157 ([], Frm), Problem
3.158 (''Isac'',
3.159 String.char.Char ''Inverse'' ''Z_Transform''
3.160 @@ -338,9 +332,9 @@
3.161 ([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n])]
3.162 val it = (): unit*)
3.163
3.164 -"----------- test [SignalProcessing,Z_Transform,inverse_sub] autoc";
3.165 -"----------- test [SignalProcessing,Z_Transform,inverse_sub] autoc";
3.166 -"----------- test [SignalProcessing,Z_Transform,inverse_sub] autoc";
3.167 +"----------- test [SignalProcessing,Z_Transform,Inverse_sub] autoc";
3.168 +"----------- test [SignalProcessing,Z_Transform,Inverse_sub] autoc";
3.169 +"----------- test [SignalProcessing,Z_Transform,Inverse_sub] autoc";
3.170 reset_states ();
3.171 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
3.172 "stepResponse (x[n::real]::bool)"];
3.173 @@ -352,13 +346,10 @@
3.174 autoCalculate 1 CompleteCalc;
3.175
3.176 val ((pt,_),_) = get_calc 1; val p = get_pos 1 1;
3.177 -(*//----------------------------- first correct "free variables on rhs" ----------------------\\
3.178 val (Form f, tac, asms) = pt_extract (pt, p);
3.179 -if term2str f = "X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]"
3.180 +if term2str f = "X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]"
3.181 andalso p = ([], Res) then ()
3.182 - else error "inv Z, exp 1 autoCalculate changed"
3.183 - \\----------------------------- first correct "free variables on rhs" ----------------------//*)
3.184 -
3.185 + else error "inv Z, exp 1 autoCalculate changed";
3.186
3.187 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
3.188 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
3.189 @@ -367,22 +358,19 @@
3.190 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
3.191 "stepResponse (x[n::real]::bool)"];
3.192 val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
3.193 - ["SignalProcessing", "Z_Transform", "Inverse"]);
3.194 + ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
3.195 CalcTree [(fmz, (dI,pI,mI))];
3.196 Iterator 1;
3.197 moveActiveRoot 1;
3.198 autoCalculate 1 CompleteCalc;
3.199
3.200 val ((pt,_),_) = get_calc 1; val p = get_pos 1 1;
3.201 -(*//----------------------------- first correct "free variables on rhs" ----------------------\\
3.202 val (Form f, tac, asms) = pt_extract (pt, p);
3.203 -if term2str f = "X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]"
3.204 +if term2str f = "X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]"
3.205 andalso p = ([], Res) then ()
3.206 - else error "inv Z, exp 1 autoCalculate changed"
3.207 - \\----------------------------- first correct "free variables on rhs" ----------------------//*)
3.208 + else error "inv Z, exp 1 autoCalculate changed";
3.209
3.210 -show_pt pt;
3.211 -(*[
3.212 +(*show_pt pt;[
3.213 (([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])),
3.214 (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
3.215 (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),