wneuper/isa: test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z

     1 (* Title:  Build_Inverse_Z_Transform

     2    Author: Jan Rocnik

     3    (c) copyright due to lincense terms.

     4 12345678901234567890123456789012345678901234567890123456789012345678901234567890

     5         10        20        30        40        50        60        70        80

     6 *)

     8 theory Build_Inverse_Z_Transform imports Isac

    10 begin

    12 text{* We stepwise build Inverse_Z_Transform.thy as an exercise.

    13   Because subsection "Stepwise Check the Program" requires

    14   Inverse_Z_Transform.thy as a subtheory of Isac.thy, the setup has been changed

    15   from "theory Inverse_Z_Transform imports Isac begin.." to the above.

    17   ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS:

    18   Here in this theory there are the internal names twice, for instance we have

    19   (Thm.derivation_name @{thm rule1} = "Build_Inverse_Z_Transform.rule1") = true;

    20   but actually in us will be "Inverse_Z_Transform.rule1"

    21 *}

    22 ML {*val thy = @{theory Isac};*}

    25 section {*trials towards Z transform *}

    26 text{*===============================*}

    27 subsection {*terms*}

    28 ML {*

    29 @{term "1 < || z ||"};

    30 @{term "z / (z - 1)"};

    31 @{term "-u -n - 1"};

    32 @{term "-u [-n - 1]"}; (*[ ] denotes lists !!!*)

    33 @{term "z /(z - 1) = -u [-n - 1]"};Isac

    34 @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};

    35 term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};

    36 *}

    37 ML {*

    38 (*alpha -->  "</alpha>" *)

    39 @{term "\<alpha> "};

    40 @{term "\<delta> "};

    41 @{term "\<phi> "};

    42 @{term "\<rho> "};

    43 term2str @{term "\<rho> "};

    44 *}

    46 subsection {*rules*}

    47 (*axiomatization "z / (z - 1) = -u [-n - 1]" Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)

    48 (*definition     "z / (z - 1) = -u [-n - 1]" Bad head of lhs: existing constant "op /"*)

    49 axiomatization where

    50   rule1: "1 = \<delta>[n]" and

    51   rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and

    52   rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and

    53   rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and

    54   rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and

    55   rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"

    56 ML {*

    57 @{thm rule1};

    58 @{thm rule2};

    59 @{thm rule3};

    60 @{thm rule4};

    61 *}

    63 subsection {*apply rules*}

    64 ML {*

    65 val inverse_Z = append_rls "inverse_Z" e_rls

    66   [ Thm  ("rule3",num_str @{thm rule3}),

    67     Thm  ("rule4",num_str @{thm rule4}),

    68     Thm  ("rule1",num_str @{thm rule1})

    69   ];

    71 val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";

    72 val SOME (t', asm) = rewrite_set_ thy true inverse_Z t;

    73 term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]"; (*attention rule1 !!!*)

    74 *}

    75 ML {*

    76 val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls);

    77 *}

    78 ML {*

    79 val SOME (t, asm1) = rewrite_ thy ro er true (num_str @{thm rule3}) t;

    80 term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1"; (*- real *)

    81 term2str t;*}

    82 ML {*

    83 val SOME (t, asm2) = rewrite_ thy ro er true (num_str @{thm rule4}) t;

    84 term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1"; (*- real *)

    85 term2str t;

    86 *}

    87 ML {*

    88 val SOME (t, asm3) = rewrite_ thy ro er true (num_str @{thm rule1}) t;

    89 term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]"; (*- real *)

    90 term2str t;

    91 *}

    92 ML {*

    93 terms2str (asm1 @ asm2 @ asm3);

    94 *}

    96 section {*Prepare steps for CTP-based programming language*}

    97 text{*TODO insert Calculation (Referenz?!)

    99 The goal... realized in sections below, in Sect.\ref{spec-meth} and Sect.\ref{prog-steps}

   101 the reader is advised to jump between the subsequent subsections and the respective steps in Sect.\ref{prog-steps}

   103 *}

   104 subsection {*prepare expression \label{prep-expr}*}

   106 ML {*

   107 val ctxt = ProofContext.init_global @{theory Isac};

   108 val ctxt = declare_constraints' [@{term "z::real"}] ctxt;

   110 val SOME fun1 = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;

   111 val SOME fun1' = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';

   112 *}

   114 subsubsection {*multply with z*}

   116 axiomatization where

   117   ruleZY: "(X z = a / b) = (X' z = a / (z * b))"

   119 ML {*

   120 val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls);

   121 val SOME (fun2, asm1) = rewrite_ thy ro er true  @{thm ruleZY} fun1; term2str fun2;

   122 val SOME (fun2', asm1) = rewrite_ thy ro er true  @{thm ruleZY} fun1'; term2str fun2';

   124 val SOME (fun3,_) = rewrite_set_ @{theory Isac} false norm_Rational fun2;

   125 term2str fun3; (*fails on x^^^(-1) TODO*)

   126 val SOME (fun3',_) = rewrite_set_ @{theory Isac} false norm_Rational fun2';

   127 term2str fun3'; (*OK*)

   128 *}

   130 subsubsection {*get argument of X': z is the variable the equation is solved for*}

   132 text{*grep... Atools.thy, Tools.thy contain general utilities: eval_argument_in, eval_rhs, eval_lhs,...

   134 grep -r "fun eva_" ... shows all functions witch can be used in a script.

   135 lookup this files how to build and handle such functions.

   137 the next section shows how to introduce such a function.

   138 *}

   141 text{*---------------------------begin partial fractions snip--------------------------*}

   143 subsubsection {*get the denominator out of a fraction*}

   145 text {*get denominator should become a constant for the isabelle parser: *}

   147 consts

   149 get_denominator :: "real => real"

   151 text {*Attention Build_Inverse_Z_Transform

   152        works only because definition was copied into Rationals.thy

   153      *}

   155 ML {*

   157 (*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)

   158 fun eval_get_denominator (thmid:string) _

   159 		      (t as Const ("Rational.get_denominator", _) $

   160               (Const ("Rings.inverse_class.divide", _) $ num $

   161                 denom)) thy =

   163     SOME (mk_thmid thmid ""

   164             (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "",

   165 	          Trueprop $ (mk_equality (t, denom)))

   167   | eval_get_denominator _ _ _ _ = NONE;

   169 *}

   171 ML {*

   172 val thy = @{theory Isac};

   173 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));

   174 *}

   175 ML {*

   176 val Const ("Rational.get_denominator", _) $

   177           (Const ("Rings.inverse_class.divide", _) $ numerator $ denominator) = t;

   178 term2str numerator;

   179 term2str denominator

   180 *}

   181 ML {*

   182 val SOME (_, t') = eval_get_denominator "" 0 t thy;

   183 term2str t';

   184 *}

   187 ML {*

   188 (*

   189 if term2s t' = "(argument_in M_b x) = x" then ()

   190 else error "atools.sml:(argument_in M_b x) = x  ???";

   191 *)

   192 *}

   197 subsubsection {*build equation from given term*}

   198 ML {*

   199 val (_, expr) = HOLogic.dest_eq fun3'; term2str expr;

   200 val (_, denom) = HOLogic.dest_bin "Rings.inverse_class.divide" (type_of expr) expr;

   201 term2str denom = "-1 + -2 * z + 8 * z ^^^ 2";

   202 *}

   203 text {*we have rhs in the language, but we need a function

   204   which gets the denominator of a fraction*}

   207 text{*---------------------------end partial fractions snip--------------------------*}

   209 subsection {*solve equation*}

   210 text {*this type of equation if too general for the present program*}

   211 ML {*

   212 "----------- Minisubplb/100-init-rootp (*OK*)bl.sml ---------------------";

   213 val denominator = parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0";

   214 val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))", "solveFor z","solutions L"];

   215 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);

   216 (*                           ^^^^^^^^^^^^^^^^^^^^^^ TODO: ISAC determines type of eq*)

   217 *}

   218 text {*Does the Equation Match the Specification ?*}

   219 ML {*

   220 match_pbl fmz (get_pbt ["univariate","equation"]);

   221 *}

   222 ML {*Context.theory_name thy = "Isac"(*==================================================*)*}

   224 ML {*

   225 val denominator = parseNEW ctxt "-1/8 + -1/4*z + z^^^2 = 0";

   226 val fmz =                                            (*specification*)

   227   ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", (*equality*)

   228    "solveFor z",                                     (*bound variable*)

   229    "solutions L"];                                   (*identifier for solution*)

   231 val (dI',pI',mI') =

   232   ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);

   233 *}

   234 text {*Does the Other Equation Match the Specification ?*}

   235 ML {*

   236 match_pbl fmz (get_pbt ["pqFormula","degree_2","polynomial","univariate","equation"]);

   237 *}

   238 text {*Solve Equation Stepwise*}

   239 ML {*

   240 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   241 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   242 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   243 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   244 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   245 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   246 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   247 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   248 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   249 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   250 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   251 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   252 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)

   253 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   254 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;

   255 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)

   256 show_pt pt;

   257 val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";

   258 *}

   260 subsection {*partial fraction decomposition*}

   261 subsubsection {*solution of the equation*}

   262 ML {*

   263 val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";

   264 term2str solutions;

   265 atomty solutions;

   266 *}

   268 subsubsection {*get solutions out of list*}

   269 text {*in isac's CTP-based programming language: let$ $s_1 = NTH 1$ solutions; $s_2 = NTH 2...$*}

   270 ML {*

   271 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _) $

   272       s_2 $ Const ("List.list.Nil", _)) = solutions;

   273 term2str s_1;

   274 term2str s_2;

   275 *}

   277 ML {* (*Solutions as Denominator --> Denominator1 = z - Zeropoint1, Denominator2 = z-Zeropoint2,...*)

   278 val xx = HOLogic.dest_eq s_1;

   279 val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;

   280 val xx = HOLogic.dest_eq s_2;

   281 val s_2' = HOLogic.mk_binop "Groups.minus_class.minus" xx;

   282 term2str s_1';

   283 term2str s_2';

   284 *}

   286 subsubsection {*build expression*}

   287 text {*in isac's CTP-based programming language: let s_1 = Take numerator / (s_1 * s_2)*}

   288 ML {*

   289 (*The Main Denominator is the multiplikation of the partial fraction denominators*)

   290 val denominator' = HOLogic.mk_binop "Groups.times_class.times" (s_1', s_2') ;

   291 val SOME numerator = parseNEW ctxt "3::real";

   293 val expr' = HOLogic.mk_binop "Rings.inverse_class.divide" (numerator, denominator');

   294 term2str expr';

   295 *}

   297 subsubsection {*Ansatz - create partial fractions out of our expression*}

   298 ML {*Context.theory_name thy = "Isac"(*==================================================*)*}

   300 axiomatization where

   301   ansatz2: "n / (a*b) = A/a + B/(b::real)" and

   302   multiply_eq2: "(n / (a*b) = A/a + B/b) = (a*b*(n  / (a*b)) = a*b*(A/a + B/b))"

   304 ML {*

   305 (*we use our ansatz2 to rewrite our expression and get an equilation with our expression on the left and the partial fractions of it on the right side*)

   306 val SOME (t1,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm ansatz2} expr';

   307 term2str t1; atomty t1;

   308 val eq1 = HOLogic.mk_eq (expr', t1);

   309 term2str eq1;

   310 *}

   311 ML {*

   312 (*eliminate the demoninators by multiplying the left and the right side with the main denominator*)

   313 val SOME (eq2,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm multiply_eq2} eq1;

   314 term2str eq2;

   315 *}

   316 ML {*

   317 (*simplificatoin*)

   318 val SOME (eq3,_) = rewrite_set_ @{theory Isac} false norm_Rational eq2;

   319 term2str eq3; (*?A ?B not simplified*)

   320 *}

   321 ML {*

   322 val SOME fract1 =

   323   parseNEW ctxt "(z - 1 / 2) * (z - -1 / 4) * (A / (z - 1 / 2) + B / (z - -1 / 4))"; (*A B !*)

   324 val SOME (fract2,_) = rewrite_set_ @{theory Isac} false norm_Rational fract1;

   325 term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";

   326 (*term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)" would be more traditional*)

   327 *}

   328 ML {*

   329 val (numerator, denominator) = HOLogic.dest_eq eq3;

   330 val eq3' = HOLogic.mk_eq (numerator, fract1); (*A B !*)

   331 term2str eq3';

   332 (*MANDATORY: simplify (and remove denominator) otherwise 3 = 0*)

   333 val SOME (eq3'' ,_) = rewrite_set_ @{theory Isac} false norm_Rational eq3';

   334 term2str eq3'';

   335 *}

   336 ML {*Context.theory_name thy = "Isac"(*==================================================*)*}

   338 subsubsection {*get first koeffizient*}

   340 ML {*

   341 (*substitude z with the first zeropoint to get A*)

   342 val SOME (eq4_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_1] eq3'';

   343 term2str eq4_1;

   345 val SOME (eq4_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4_1;

   346 term2str eq4_2;

   348 val fmz = ["equality (3 = 3 * A / (4::real))", "solveFor A","solutions L"];

   349 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);

   350 (*solve the simple linear equilation for A TODO: return eq, not list of eq*)

   351 val (p,_,fa,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   352 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   353 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   354 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   355 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   356 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   357 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   358 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   359 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   360 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   361 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   362 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   363 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   364 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   365 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   366 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   367 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   368 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   369 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   370 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   371 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   372 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   373 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   374 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   375 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   376 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   377 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   378 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;

   379 f2str fa;

   380 *}

   382 subsubsection {*get second koeffizient*}

   383 ML {*thy*}

   385 ML {*

   386 (*substitude z with the second zeropoint to get B*)

   387 val SOME (eq4b_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_2] eq3'';

   388 term2str eq4b_1;

   390 val SOME (eq4b_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4b_1;

   391 term2str eq4b_2;

   392 *}

   393 ML {*

   394 (*solve the simple linear equilation for B TODO: return eq, not list of eq*)

   395 val fmz = ["equality (3 = -3 * B / (4::real))", "solveFor B","solutions L"];

   396 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);

   397 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   398 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   399 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   400 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   401 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   402 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   403 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   404 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   405 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   406 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   407 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   408 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   409 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   410 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   411 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   412 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   413 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   414 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   415 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   416 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   417 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   418 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   419 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   420 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   421 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   422 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   423 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   424 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;

   425 f2str fb;

   426 *}

   428 ML {* (*check koeffizients*)

   429 if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";

   430 if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";

   431 *}

   433 subsubsection {*substitute expression with solutions*}

   434 ML {*

   435 *}

   436 ML {*thy*}

   438 section {*Implement the Specification and the Method \label{spec-meth}*}

   439 text{*==============================================*}

   440 subsection{*Define the Field Descriptions for the specification*}

   441 consts

   442   filterExpression  :: "bool => una"

   443   stepResponse      :: "bool => una"

   445 subsection{*Define the Specification*}

   446 ML {*

   447 store_pbt

   448  (prep_pbt thy "pbl_SP" [] e_pblID

   449  (["SignalProcessing"], [], e_rls, NONE, []));

   450 store_pbt

   451  (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID

   452  (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));

   453 *}

   454 ML {*thy*}

   455 ML {*

   456 store_pbt

   457  (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID

   458  (["inverse", "Z_Transform", "SignalProcessing"],

   459   [("#Given" ,["filterExpression X_eq"]),

   460    ("#Find"  ,["stepResponse n_eq"])

   461   ],

   462   append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,

   463   [["SignalProcessing","Z_Transform","inverse"]]));

   465 show_ptyps();

   466 get_pbt ["inverse","Z_Transform","SignalProcessing"];

   467 *}

   469 subsection {*Define Name and Signature for the Method*}

   470 consts

   471   InverseZTransform :: "[bool, bool] => bool"

   472     ("((Script InverseZTransform (_ =))// (_))" 9)

   474 subsection {*Setup Parent Nodes in Hierarchy of Method*}

   475 ML {*

   476 store_met

   477  (prep_met thy "met_SP" [] e_metID

   478  (["SignalProcessing"], [],

   479    {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,

   480     crls = e_rls, nrls = e_rls}, "empty_script"));

   481 store_met

   482  (prep_met thy "met_SP_Ztrans" [] e_metID

   483  (["SignalProcessing", "Z_Transform"], [],

   484    {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,

   485     crls = e_rls, nrls = e_rls}, "empty_script"));

   486 *}

   487 ML {*

   488 store_met

   489  (prep_met thy "met_SP_Ztrans_inv" [] e_metID

   490  (["SignalProcessing", "Z_Transform", "inverse"],

   491   [("#Given" ,["filterExpression X_eq"]),

   492    ("#Find"  ,["stepResponse n_eq"])

   493   ],

   494    {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,

   495     crls = e_rls, nrls = e_rls},

   496   "empty_script"

   497  ));

   498 *}

   499 ML {*

   500 store_met

   501  (prep_met thy "met_SP_Ztrans_inv" [] e_metID

   502  (["SignalProcessing", "Z_Transform", "inverse"],

   503   [("#Given" ,["filterExpression X_eq"]),

   504    ("#Find"  ,["stepResponse n_eq"])

   505   ],

   506    {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,

   507     crls = e_rls, nrls = e_rls},

   508   "Script InverseZTransform (Xeq::bool) =" ^

   509   " (let X = Take Xeq;" ^

   510   "      X = Rewrite ruleZY False X" ^

   511   "  in X)"

   512  ));

   513 *}

   514 ML {*

   515 show_mets();

   516 *}

   517 ML {*

   518 get_met ["SignalProcessing","Z_Transform","inverse"];

   519 *}

   521 section {*Program in CTP-based language \label{prog-steps}*}

   522 text{*=================================*}

   523 subsection {*Stepwise extend Program*}

   524 ML {*

   525 val str =

   526 "Script InverseZTransform (Xeq::bool) =" ^

   527 " Xeq";

   528 *}

   529 ML {*

   530 val str =

   531 "Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)

   532 " (let X = Take Xeq;" ^

   533 "      X' = Rewrite ruleZY False X;" ^ (*z * denominator*)

   534 "      X' = (Rewrite_Set norm_Rational False) X'" ^ (*simplify*)

   535 "  in X)";

   536 (*NONE*)

   537 "Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)

   538 " (let X = Take Xeq;" ^

   539 "      X' = Rewrite ruleZY False X;" ^ (*z * denominator*)

   540 "      X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)

   541 "      X' = (SubProblem (Isac',[pqFormula,degree_2,polynomial,univariate,equation], [no_met])   " ^

   542     "                 [BOOL e_e, REAL v_v])" ^

   543 "  in X)";

   544 *}

   545 ML {*

   546 val str =

   547 "Script InverseZTransform (Xeq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)

   548 " (let X = Take Xeq;" ^

   549 "      X' = Rewrite ruleZY False X;" ^ (*z * denominator*)

   550 "      X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)

   551 "      funterm = rhs X'" ^ (*drop X'= for equation solving*)

   552 "  in X)";

   553 *}

   554 ML {*

   555 val str =

   556 "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)

   557 " (let X = Take X_eq;" ^

   558 "      X' = Rewrite ruleZY False X;" ^ (*z * denominator*)

   559 "      X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)

   560 "      (X'_z::real) = lhs X';" ^

   561 "      (z::real) = argument_in X'_z;" ^

   562 "      (funterm::real) = rhs X';" ^ (*drop X' z = for equation solving*)

   563 "      (denom::real) = get_denominator funterm;" ^ (*get_denominator*)

   564 "      (equ::bool) = (denom = (0::real));" ^

   565 "      (L_L::bool list) =                                    " ^

   566 "            (SubProblem (Test',                            " ^

   567 "                         [linear,univariate,equation,test]," ^

   568 "                         [Test,solve_linear])              " ^

   569 "                        [BOOL equ, REAL z])              " ^

   570 "  in X)"

   571 ;

   573 parse thy str;

   574 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   575 atomty sc;

   577 *}

   579 text {*

   580 This ruleset contains all functions that are in the script;

   581 The evaluation of the functions is done by rewriting using this ruleset.

   582 *}

   584 ML {*

   585 val srls = Rls {id="srls_InverseZTransform",

   586 		  preconds = [], rew_ord = ("termlessI",termlessI),

   587 		  erls = append_rls "erls_in_srls_InverseZTransform" e_rls

   588 				    [(*for asm in NTH_CONS ...*) Calc ("Orderings.ord_class.less",eval_equ "#less_"),

   589 				     (*2nd NTH_CONS pushes n+-1 into asms*) Calc("Groups.plus_class.plus", eval_binop "#add_")

   590 				    ],

   591   srls = Erls, calc = [],

   592 		  rules =

   593     [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),

   594 			     Calc("Groups.plus_class.plus", eval_binop "#add_"),

   595 			     Thm ("NTH_NIL",num_str @{thm NTH_NIL}),

   596 			     Calc("Tools.lhs", eval_lhs"eval_lhs_"), (*<=== ONLY USED*)

   597 			     Calc("Tools.rhs", eval_rhs"eval_rhs_"), (*<=== ONLY USED*)

   598 			     Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),

   599      Calc("Rational.get_denominator",

   600        eval_get_denominator "Rational.get_denominator")

   601 			    ],

   602 		  scr = EmptyScr};

   603 *}

   606 subsection {*Store Final Version of Program for Execution*}

   607 ML {*

   608 store_met

   609  (prep_met thy "met_SP_Ztrans_inv" [] e_metID

   610  (["SignalProcessing", "Z_Transform", "inverse"],

   611   [("#Given" ,["filterExpression X_eq"]),

   612    ("#Find"  ,["stepResponse n_eq"])

   613   ],

   614    {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls,

   615     prls = e_rls,

   616     crls = e_rls, nrls = e_rls},

   617 "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)

   618 " (let X = Take X_eq;" ^

   619 "      X' = Rewrite ruleZY False X;" ^ (*z * denominator*)

   620 "      X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)

   621 "      (X'_z::real) = lhs X';" ^ (**)

   622 "      (z::real) = argument_in X'_z;" ^ (**)

   623 "      (funterm::real) = rhs X';" ^ (*drop X' z = for equation solving*)

   624 "      (denom::real) = get_denominator funterm;" ^ (*get_denominator*)

   625 "      (equ::bool) = (denom = (0::real));" ^

   626 "      (L_L::bool list) =                                    " ^

   627 "            (SubProblem (Test',                            " ^

   628 "                         [linear,univariate,equation,test]," ^

   629 "                         [Test,solve_linear])              " ^

   630 "                        [BOOL equ, REAL z])              " ^

   631 "  in X)"

   632  ));

   633 *}

   634 ML {*

   635 val Script scr = (#scr o get_met) ["SignalProcessing", "Z_Transform", "inverse"];

   636 atomty scr

   637 *}

   638 ML {*

   639 val t = term_of (the (parse thy "get_denominator (24 / (-1 + -2 * z + 8 * z ^^^ 2))"));

   640 atomty t;

   641 *}

   642 ML {*

   643 trace_rewrite := true;

   644 rewrite_set_ thy true srls t;

   645 *}

   647 subsection {*Check the Program*}

   649 subsubsection {*Check the formalization*}

   650 ML {*

   651 val fmz = ["filterExpression (X  = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",

   652   "stepResponse (x[n::real]::bool)"];

   653 val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],

   654   ["SignalProcessing","Z_Transform","inverse"]);

   656 val ([(1, [1], "#Given", Const ("Inverse_Z_Transform.filterExpression", _),

   657             [Const ("HOL.eq", _) $ _ $ _]),

   658            (2, [1], "#Find", Const ("Inverse_Z_Transform.stepResponse", _),

   659             [Free ("x", _) $ _])],

   660           _) = prep_ori fmz thy ((#ppc o get_pbt) pI);

   661 *}

   662 ML {*

   663 val Script sc = (#scr o get_met) ["SignalProcessing","Z_Transform","inverse"];

   664 atomty sc;

   665 *}

   667 subsubsection {*Stepwise check the program*}

   668 ML {*

   669 trace_script := true; print_depth 9;

   670 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",

   671   "stepResponse (x[n::real]::bool)"];

   672 val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],

   673   ["SignalProcessing","Z_Transform","inverse"]);

   674 val (p,_,f,nxt,_,pt)  = CalcTreeTEST [(fmz, (dI,pI,mI))];

   675 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   676 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   677 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   678 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   679 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   680 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";

   681 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))"; (*TODO naming!*)

   682 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";

   683 *}

   684 ML {*

   685 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Subproblem";

   686 *}

   687 ML {*

   688 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Model_Problem";

   689 *}

   690 ML {*

   691 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";

   692 *}

   693 ML {*

   694 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "solveFor z";

   695 *}

   696 ML {*

   697 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Add_Find";

   698 *}

   699 ML {*

   700 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   701 *}

   702 ML {*

   703 show_pt pt;

   704 *}

   705 ML {*

   706 *}

   707 ML {*

   709 *}

   710 ML {*

   712 *}

   713 ML {*

   715 *}

   716 ML {*

   718 *}

   720 ML {*

   722 *}

   723 ML {*

   724 @{theory Isac}

   725 *}

   727 ML {*

   728 *}

   729 ML {*

   730 *}

   731 ML {*

   732 *}

   741 section {*Write Tests for Crucial Details*}

   742 text{*===================================*}

   743 ML {*

   745 *}

   747 section {*Integrate Program into Knowledge*}

   748 ML {*

   749 @{theory Isac}

   750 *}

   752 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 06 Oct 2011 17:43:00 +0200
branch	decompose-isar
changeset 42301	93083d4e05d8
parent 42300	bd8307d618d2
child 42302	2cceae8c18bc
permissions	-rwxr-xr-x