1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Mar 07 14:20:33 2018 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Mar 08 07:28:17 2018 +0100
1.3 @@ -1,8 +1,6 @@
1.4 (* Title: Build_Inverse_Z_Transform
1.5 Author: Jan Rocnik
1.6 (c) copyright due to license terms.
1.7 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.8 - 10 20 30 40 50 60 70 80
1.9 *)
1.10
1.11 theory Build_Inverse_Z_Transform imports Inverse_Z_Transform
1.12 @@ -76,13 +74,13 @@
1.13
1.14 ML {*
1.15 val inverse_Z = append_rls "inverse_Z" e_rls
1.16 - [ Thm ("rule3",num_str @{thm rule3}),
1.17 - Thm ("rule4",num_str @{thm rule4}),
1.18 - Thm ("rule1",num_str @{thm rule1})
1.19 + [ Thm ("rule3",TermC.num_str @{thm rule3}),
1.20 + Thm ("rule4",TermC.num_str @{thm rule4}),
1.21 + Thm ("rule1",TermC.num_str @{thm rule1})
1.22 ];
1.23
1.24 - val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
1.25 - val SOME (t', asm) = rewrite_set_ thy true inverse_Z t;
1.26 + val t = TermC.str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
1.27 + val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t;
1.28 term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
1.29 (*
1.30 * Attention rule1 is applied before the expression is
1.31 @@ -93,19 +91,19 @@
1.32 ML {* val (thy, ro, er) = (@{theory}, tless_true, eval_rls); *}
1.33 ML {*
1.34 val SOME (t, asm1) =
1.35 - rewrite_ thy ro er true (num_str @{thm rule3}) t;
1.36 + Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule3}) t;
1.37 term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1";
1.38 (*- real *)
1.39 term2str t;
1.40
1.41 val SOME (t, asm2) =
1.42 - rewrite_ thy ro er true (num_str @{thm rule4}) t;
1.43 + Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule4}) t;
1.44 term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1";
1.45 (*- real *)
1.46 term2str t;
1.47
1.48 val SOME (t, asm3) =
1.49 - rewrite_ thy ro er true (num_str @{thm rule1}) t;
1.50 + Rewrite.rewrite_ thy ro er true (TermC.num_str @{thm rule1}) t;
1.51 term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]";
1.52 (*- real *)
1.53 term2str t;
1.54 @@ -128,12 +126,12 @@
1.55 Isabelle can handle best.*}
1.56 ML {*
1.57 val ctxt = Proof_Context.init_global @{theory};
1.58 - val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
1.59 + val ctxt = Stool.declare_constraints' [@{term "z::real"}] ctxt;
1.60
1.61 val SOME fun1 =
1.62 - parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
1.63 + TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
1.64 val SOME fun1' =
1.65 - parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
1.66 + TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
1.67 *}
1.68
1.69 subsubsection {*Prepare Numerator and Denominator*}
1.70 @@ -148,19 +146,19 @@
1.71 ML {*
1.72 val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
1.73 val SOME (fun2, asm1) =
1.74 - rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
1.75 + Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
1.76 val SOME (fun2', asm1) =
1.77 - rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
1.78 + Rewrite.rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
1.79
1.80 val SOME (fun3,_) =
1.81 - rewrite_set_ @{theory} false norm_Rational fun2;
1.82 + Rewrite.rewrite_set_ @{theory} false norm_Rational fun2;
1.83 term2str fun3;
1.84 (*
1.85 * Fails on x^^^(-1)
1.86 * We solve this problem by using 1/x as a workaround.
1.87 *)
1.88 val SOME (fun3',_) =
1.89 - rewrite_set_ @{theory} false norm_Rational fun2';
1.90 + Rewrite.rewrite_set_ @{theory} false norm_Rational fun2';
1.91 term2str fun3';
1.92 (*
1.93 * OK - workaround!
1.94 @@ -218,8 +216,8 @@
1.95 (t as Const ("Rational.get_denominator", _) $
1.96 (Const ("Rings.divide_class.divide", _) $num
1.97 $denom)) thy =
1.98 - SOME (mk_thmid thmid "" (term_to_string''' thy denom) "",
1.99 - Trueprop $ (mk_equality (t, denom)))
1.100 + SOME (TermC.mk_thmid thmid (term_to_string''' thy denom) "",
1.101 + HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
1.102 | eval_get_denominator _ _ _ _ = NONE;
1.103 *}
1.104 text {*\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont
1.105 @@ -238,8 +236,8 @@
1.106 (t as Const ("Rational.get_numerator", _) $
1.107 (Const ("Rings.divide_class.divide", _) $num
1.108 $denom )) thy =
1.109 - SOME (mk_thmid thmid "" (term_to_string''' thy num) "",
1.110 - Trueprop $ (mk_equality (t, num)))
1.111 + SOME (TermC.mk_thmid thmid (term_to_string''' thy num) "",
1.112 + HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
1.113 | eval_get_numerator _ _ _ _ = NONE;
1.114 *}
1.115
1.116 @@ -259,7 +257,7 @@
1.117 for this equation type. Later on {\sisac} should determine the type
1.118 of the given equation self.*}
1.119 ML {*
1.120 - val denominator = parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0";
1.121 + val denominator = TermC.parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0";
1.122 val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))",
1.123 "solveFor z",
1.124 "solutions L"];
1.125 @@ -268,7 +266,7 @@
1.126 text {*\noindent Check if the given equation matches the specification of this
1.127 equation type.*}
1.128 ML {*
1.129 - match_pbl fmz (get_pbt ["univariate","equation"]);
1.130 + Specify.match_pbl fmz (Specify.get_pbt ["univariate","equation"]);
1.131 *}
1.132
1.133 text{*\noindent We switch up to the {\sisac} Context and try to solve the
1.134 @@ -276,7 +274,7 @@
1.135
1.136 ML {*
1.137 Context.theory_name thy = "Isac";
1.138 - val denominator = parseNEW ctxt "-1 + -2 * z + 8 * z ^^^ 2 = 0";
1.139 + val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z ^^^ 2 = 0";
1.140 val fmz = (*specification*)
1.141 ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",(*equality*)
1.142 "solveFor z", (*bound variable*)
1.143 @@ -292,7 +290,7 @@
1.144 specification of this equation type.*}
1.145
1.146 ML {*
1.147 - match_pbl fmz (get_pbt
1.148 + Specify.match_pbl fmz (Specify.get_pbt
1.149 ["abcFormula","degree_2","polynomial","univariate","equation"]);
1.150 *}
1.151
1.152 @@ -1076,7 +1074,7 @@
1.153 " in X)";
1.154
1.155 parse thy str;
1.156 - val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
1.157 + val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
1.158 atomty sc;
1.159 *}
1.160