1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue May 19 12:33:35 2020 +0200
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed May 20 12:52:09 2020 +0200
1.3 @@ -261,12 +261,12 @@
1.4 val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))",
1.5 "solveFor z",
1.6 "solutions L"];
1.7 - val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
1.8 + val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
1.9 \<close>
1.10 text \<open>\noindent Check if the given equation matches the specification of this
1.11 equation type.\<close>
1.12 ML \<open>
1.13 - M_Match.match_pbl fmz (Problem.from_store ["univariate","equation"]);
1.14 + M_Match.match_pbl fmz (Problem.from_store ["univariate", "equation"]);
1.15 \<close>
1.16
1.17 text\<open>\noindent We switch up to the {\sisac} Context and try to solve the
1.18 @@ -282,7 +282,7 @@
1.19 solution*)
1.20 val (dI',pI',mI') =
1.21 ("Isac_Knowledge",
1.22 - ["abcFormula","degree_2","polynomial","univariate","equation"],
1.23 + ["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.24 ["no_met"]);
1.25 \<close>
1.26
1.27 @@ -291,7 +291,7 @@
1.28
1.29 ML \<open>
1.30 M_Match.match_pbl fmz (Problem.from_store
1.31 - ["abcFormula","degree_2","polynomial","univariate","equation"]);
1.32 + ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]);
1.33 \<close>
1.34
1.35 text \<open>\noindent We stepwise solve the equation. This is done by the
1.36 @@ -738,8 +738,8 @@
1.37 rewrite_set_ @{theory} false norm_Rational eq4_1;
1.38 UnparseC.term eq4_2;
1.39
1.40 - val fmz = ["equality (3=3*A/(4::real))", "solveFor A","solutions L"];
1.41 - val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
1.42 + val fmz = ["equality (3=3*A/(4::real))", "solveFor A", "solutions L"];
1.43 + val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
1.44 (*
1.45 * Solve the simple linear equation for A:
1.46 * Return eq, not list of eq's
1.47 @@ -754,14 +754,14 @@
1.48 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.49 (*Specify_Theory "Isac_Knowledge"*)
1.50 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.51 - (*Specify_Problem ["normalise","polynomial",
1.52 - "univariate","equation"])*)
1.53 + (*Specify_Problem ["normalise", "polynomial",
1.54 + "univariate", "equation"])*)
1.55 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.56 - (* Specify_Method["PolyEq","normalise_poly"]*)
1.57 + (* Specify_Method["PolyEq", "normalise_poly"]*)
1.58 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.59 - (*Apply_Method["PolyEq","normalise_poly"]*)
1.60 + (*Apply_Method["PolyEq", "normalise_poly"]*)
1.61 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.62 - (*Rewrite ("all_left","PolyEq.all_left")*)
1.63 + (*Rewrite ("all_left", "PolyEq.all_left")*)
1.64 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.65 (*Rewrite_Set_Inst(["(''bdv'',A)"],"make_ratpoly_in")*)
1.66 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.67 @@ -778,7 +778,7 @@
1.68 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.69 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.70 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.71 - (*Apply_Method ["PolyEq","solve_d1_polyeq_equation"]*)
1.72 + (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
1.73 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.74 (*Rewrite_Set_Inst(["(''bdv'',A)"],"d1_polyeq_simplify")*)
1.75 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.76 @@ -790,11 +790,11 @@
1.77 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.78 (*Check_elementwise "Assumptions"*)
1.79 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.80 - (*Check_Postcond ["degree_1","polynomial",
1.81 - "univariate","equation"]*)
1.82 + (*Check_Postcond ["degree_1", "polynomial",
1.83 + "univariate", "equation"]*)
1.84 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.85 - (*Check_Postcond ["normalise","polynomial",
1.86 - "univariate","equation"]*)
1.87 + (*Check_Postcond ["normalise", "polynomial",
1.88 + "univariate", "equation"]*)
1.89 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.90 (*End_Proof'*)
1.91 f2str fa;
1.92 @@ -818,8 +818,8 @@
1.93 rewrite_set_ @{theory} false norm_Rational eq4b_1;
1.94 UnparseC.term eq4b_2;
1.95
1.96 - val fmz = ["equality (3= -3*B/(4::real))", "solveFor B","solutions L"];
1.97 - val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
1.98 + val fmz = ["equality (3= -3*B/(4::real))", "solveFor B", "solutions L"];
1.99 + val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
1.100 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.101 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.102 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
1.103 @@ -885,7 +885,7 @@
1.104 setup \<open>KEStore_Elems.add_pbts
1.105 [Problem.prep_input thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
1.106 Problem.prep_input thy "pbl_SP_Ztrans" [] Problem.id_empty
1.107 - (["Z_Transform","SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
1.108 + (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
1.109
1.110 text\<open>\noindent For the suddenly created node we have to define the input
1.111 and output parameters. We already prepared their definition in
1.112 @@ -898,10 +898,10 @@
1.113 ("#Find", ["stepResponse n_eq"])],
1.114 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
1.115 NONE,
1.116 - [["SignalProcessing","Z_Transform","Inverse"]])]\<close>
1.117 + [["SignalProcessing", "Z_Transform", "Inverse"]])]\<close>
1.118 ML \<open>
1.119 Test_Tool.show_ptyps() ();
1.120 - Problem.from_store ["Inverse","Z_Transform","SignalProcessing"];
1.121 + Problem.from_store ["Inverse", "Z_Transform", "SignalProcessing"];
1.122 \<close>
1.123
1.124 subsection \<open>Define Name and Signature for the Method\<close>
1.125 @@ -974,7 +974,7 @@
1.126 the hierarchy.\<close>
1.127
1.128 ML \<open>
1.129 - Method.from_store ["SignalProcessing","Z_Transform","Inverse"];
1.130 + Method.from_store ["SignalProcessing", "Z_Transform", "Inverse"];
1.131 \<close>
1.132
1.133 section \<open>Program in TP-based language \label{prog-steps}\<close>
1.134 @@ -1210,7 +1210,7 @@
1.135 "stepResponse (x[n::real]::bool)"];
1.136 val (dI,pI,mI) =
1.137 ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
1.138 - ["SignalProcessing","Z_Transform","Inverse"]);
1.139 + ["SignalProcessing", "Z_Transform", "Inverse"]);
1.140
1.141 val ([
1.142 (
1.143 @@ -1252,7 +1252,7 @@
1.144
1.145 val (dI,pI,mI) =
1.146 ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
1.147 - ["SignalProcessing","Z_Transform","Inverse"]);
1.148 + ["SignalProcessing", "Z_Transform", "Inverse"]);
1.149
1.150 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
1.151 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.152 @@ -1406,7 +1406,7 @@
1.153 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.154 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.155 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.156 - (*Specify_Problem ["normalise","polynomial","univariate","equation"]*)
1.157 + (*Specify_Problem ["normalise", "polynomial", "univariate", "equation"]*)
1.158 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.159 (*Specify_Method ["PolyEq", "normalise_poly"]*)
1.160 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.161 @@ -1418,7 +1418,7 @@
1.162 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.163 (*Rewrite_Set "polyeq_simplify"*)
1.164 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.165 - (*Subproblem("Isac_Knowledge",["degree_1","polynomial","univariate","equation"])*)
1.166 + (*Subproblem("Isac_Knowledge",["degree_1", "polynomial", "univariate", "equation"])*)
1.167 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.168 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.169 val (p,_,f,nxt,_,pt) = me nxt p [] pt;