1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Apr 06 11:44:36 2020 +0200
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Apr 08 12:32:51 2020 +0200
1.3 @@ -73,7 +73,7 @@
1.4 text\<open>\noindent We try to apply the rules to a given expression.\<close>
1.5
1.6 ML \<open>
1.7 - val inverse_Z = append_rls "inverse_Z" e_rls
1.8 + val inverse_Z = Rule_Set.append_rules "inverse_Z" Rule_Set.empty
1.9 [ Thm ("rule3",TermC.num_str @{thm rule3}),
1.10 Thm ("rule4",TermC.num_str @{thm rule4}),
1.11 Thm ("rule1",TermC.num_str @{thm rule1})
1.12 @@ -616,7 +616,7 @@
1.13
1.14 ML \<open>
1.15 val SOME (t1,_) =
1.16 - rewrite_ @{theory} e_rew_ord e_rls false
1.17 + rewrite_ @{theory} e_rew_ord Rule_Set.empty false
1.18 @{thm ansatz_2nd_order} expr';
1.19 term2str t1; atomty t1;
1.20 val eq1 = HOLogic.mk_eq (expr', t1);
1.21 @@ -631,7 +631,7 @@
1.22
1.23 ML \<open>
1.24 val SOME (eq2,_) =
1.25 - rewrite_ @{theory} e_rew_ord e_rls false
1.26 + rewrite_ @{theory} e_rew_ord Rule_Set.empty false
1.27 @{thm equival_trans_2nd_order} eq1;
1.28 term2str eq2;
1.29 \<close>
1.30 @@ -699,7 +699,7 @@
1.31 ML \<open>
1.32 val ansatz_rls = prep_rls @{theory} (
1.33 Rule_Set.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.34 - erls = e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.35 + erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.36 rules = [
1.37 Thm ("ansatz_2nd_order",num_str @{thm ansatz_2nd_order}),
1.38 Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})
1.39 @@ -732,7 +732,7 @@
1.40
1.41 ML \<open>
1.42 val SOME (eq4_1,_) =
1.43 - rewrite_terms_ @{theory} e_rew_ord e_rls [s_1] eq3'';
1.44 + rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_1] eq3'';
1.45 term2str eq4_1;
1.46 val SOME (eq4_2,_) =
1.47 rewrite_set_ @{theory} false norm_Rational eq4_1;
1.48 @@ -812,7 +812,7 @@
1.49
1.50 ML \<open>
1.51 val SOME (eq4b_1,_) =
1.52 - rewrite_terms_ @{theory} e_rew_ord e_rls [s_2] eq3'';
1.53 + rewrite_terms_ @{theory} e_rew_ord Rule_Set.empty [s_2] eq3'';
1.54 term2str eq4b_1;
1.55 val SOME (eq4b_2,_) =
1.56 rewrite_set_ @{theory} false norm_Rational eq4b_1;
1.57 @@ -883,9 +883,9 @@
1.58 \em Z\_Transform\normalfont.\<close>
1.59
1.60 setup \<open>KEStore_Elems.add_pbts
1.61 - [prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, []),
1.62 + [prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
1.63 prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
1.64 - (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])]\<close>
1.65 + (["Z_Transform","SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
1.66
1.67 text\<open>\noindent For the suddenly created node we have to define the input
1.68 and output parameters. We already prepared their definition in
1.69 @@ -896,7 +896,7 @@
1.70 (["Inverse", "Z_Transform", "SignalProcessing"],
1.71 [("#Given" ,["filterExpression X_eq"]),
1.72 ("#Find", ["stepResponse n_eq"])],
1.73 - append_rls "e_rls" e_rls [(*for preds in where_*)],
1.74 + Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
1.75 NONE,
1.76 [["SignalProcessing","Z_Transform","Inverse"]])]\<close>
1.77 ML \<open>
1.78 @@ -923,13 +923,13 @@
1.79 setup \<open>KEStore_Elems.add_mets
1.80 [prep_met thy "met_SP" [] e_metID
1.81 (["SignalProcessing"], [],
1.82 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.83 - errpats = [], nrls = e_rls},
1.84 + {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.85 + errpats = [], nrls = Rule_Set.empty},
1.86 "empty_script"),
1.87 prep_met thy "met_SP_Ztrans" [] e_metID
1.88 (["SignalProcessing", "Z_Transform"], [],
1.89 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.90 - errpats = [], nrls = e_rls},
1.91 + {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.92 + errpats = [], nrls = Rule_Set.empty},
1.93 "empty_script")]
1.94 \<close>
1.95
1.96 @@ -942,8 +942,8 @@
1.97 (["SignalProcessing", "Z_Transform", "Inverse"],
1.98 [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
1.99 ("#Find", ["stepResponse n_eq"])],
1.100 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.101 - errpats = [], nrls = e_rls},
1.102 + {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.103 + errpats = [], nrls = Rule_Set.empty},
1.104 "empty_script")]
1.105 \<close>
1.106
1.107 @@ -956,8 +956,8 @@
1.108 (["SignalProcessing", "Z_Transform", "Inverse"],
1.109 [("#Given" , ["filterExpression X_eq", "boundVariable X_z"]),
1.110 ("#Find", ["stepResponse n_eq"])],
1.111 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
1.112 - errpats = [], nrls = e_rls},
1.113 + {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.114 + errpats = [], nrls = Rule_Set.empty},
1.115 "Program InverseZTransform (Xeq::bool) =" ^ (*TODO boundVariable X_z*)
1.116 " (let X = Take Xeq;" ^
1.117 " X = Rewrite ruleZY X" ^
1.118 @@ -1088,7 +1088,7 @@
1.119 Rule_Set.Repeat {id="srls_InverseZTransform",
1.120 preconds = [],
1.121 rew_ord = ("termlessI",termlessI),
1.122 - erls = append_rls "erls_in_srls_InverseZTransform" e_rls
1.123 + erls = Rule_Set.append_rules "erls_in_srls_InverseZTransform" Rule_Set.empty
1.124 [(*for asm in NTH_CONS ...*)
1.125 Num_Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.126 (*2nd NTH_CONS pushes n+-1 into asms*)
1.127 @@ -1126,8 +1126,8 @@
1.128 (["SignalProcessing", "Z_Transform", "Inverse"],
1.129 [("#Given" , ["filterExpression X_eq"]), (*TODO boundVariable X_z*)
1.130 ("#Find", ["stepResponse n_eq"])],
1.131 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls, prls = e_rls, crls = e_rls,
1.132 - errpats = [], nrls = e_rls},
1.133 + {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = srls, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.134 + errpats = [], nrls = Rule_Set.empty},
1.135 "Program InverseZTransform (X_eq::bool) = "^
1.136 (*(1/z) instead of z ^^^ -1*)
1.137 "(let X = Take X_eq; "^