1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Mon Apr 06 11:44:36 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 08 12:32:51 2020 +0200
1.3 @@ -173,7 +173,7 @@
1.4 Rule_Def.Repeat{id = "order_add_mult_System", preconds = [],
1.5 rew_ord = ("ord_simplify_System",
1.6 ord_simplify_System false @{theory "Integrate"}),
1.7 - erls = Rule_Set.e_rls,srls = Rule_Set.Empty, calc = [], errpatts = [],
1.8 + erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
1.9 rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1.10 (* z * w = w * z *)
1.11 Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1.12 @@ -281,7 +281,7 @@
1.13 scr = Rule.EmptyScr};
1.14 (*
1.15 val simplify_System =
1.16 - Rule_Set.append_rls "simplify_System" simplify_System_parenthesized
1.17 + Rule_Set.append_rules "simplify_System" simplify_System_parenthesized
1.18 [Rule.Thm ("sym_add_assoc",
1.19 TermC.num_str (@{thm add.assoc} RS @{thm sym}))];
1.20 *)
1.21 @@ -290,7 +290,7 @@
1.22 val isolate_bdvs =
1.23 Rule_Def.Repeat {id="isolate_bdvs", preconds = [],
1.24 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.25 - erls = Rule_Set.append_rls "erls_isolate_bdvs" Rule_Set.e_rls
1.26 + erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
1.27 [(Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.28 eval_occur_exactly_in
1.29 "#eval_occur_exactly_in_"))
1.30 @@ -306,8 +306,8 @@
1.31 val isolate_bdvs_4x4 =
1.32 Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [],
1.33 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.34 - erls = Rule_Set.append_rls
1.35 - "erls_isolate_bdvs_4x4" Rule_Set.e_rls
1.36 + erls = Rule_Set.append_rules
1.37 + "erls_isolate_bdvs_4x4" Rule_Set.empty
1.38 [Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.39 eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.40 Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.41 @@ -410,20 +410,20 @@
1.42 (["system"],
1.43 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.44 ("#Find" ,["solution ss'''"](*''' is copy-named*))],
1.45 - Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.46 + Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.47 (Specify.prep_pbt thy "pbl_equsys_lin" [] Celem.e_pblID
1.48 (["LINEAR", "system"],
1.49 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.50 (*TODO.WN050929 check linearity*)
1.51 ("#Find" ,["solution ss'''"])],
1.52 - Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.53 + Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.54 (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Celem.e_pblID
1.55 (["2x2", "LINEAR", "system"],
1.56 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.57 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.58 ("#Where" ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]),
1.59 ("#Find" ,["solution ss'''"])],
1.60 - Rule_Set.append_rls "prls_2x2_linear_system" Rule_Set.e_rls
1.61 + Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty
1.62 [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.63 Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.64 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.65 @@ -441,7 +441,7 @@
1.66 (["normalise", "2x2", "LINEAR", "system"],
1.67 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.68 ("#Find" ,["solution ss'''"])],
1.69 - Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)],
1.70 + Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
1.71 SOME "solveSystem e_s v_s",
1.72 [["EqSystem","normalise","2x2"]])),
1.73 (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Celem.e_pblID
1.74 @@ -450,7 +450,7 @@
1.75 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.76 ("#Where" ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]),
1.77 ("#Find" ,["solution ss'''"])],
1.78 - Rule_Set.append_rls "prls_3x3_linear_system" Rule_Set.e_rls
1.79 + Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty
1.80 [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.81 Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.82 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.83 @@ -462,7 +462,7 @@
1.84 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.85 ("#Where" ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]),
1.86 ("#Find" ,["solution ss'''"])],
1.87 - Rule_Set.append_rls "prls_4x4_linear_system" Rule_Set.e_rls
1.88 + Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty
1.89 [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.90 Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.91 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.92 @@ -477,7 +477,7 @@
1.93 "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
1.94 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
1.95 ("#Find" ,["solution ss'''"])],
1.96 - Rule_Set.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.97 + Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.98 [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.99 SOME "solveSystem e_s v_s",
1.100 [["EqSystem","top_down_substitution","4x4"]])),
1.101 @@ -486,7 +486,7 @@
1.102 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.103 (*LENGTH is checked 1 level above*)
1.104 ("#Find" ,["solution ss'''"])],
1.105 - Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)],
1.106 + Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
1.107 SOME "solveSystem e_s v_s",
1.108 [["EqSystem","normalise","4x4"]]))]\<close>
1.109
1.110 @@ -495,7 +495,7 @@
1.111 val srls = Rule_Def.Repeat {id="srls_normalise_4x4",
1.112 preconds = [],
1.113 rew_ord = ("termlessI",termlessI),
1.114 - erls = Rule_Set.append_rls "erls_in_srls_IntegrierenUnd.." Rule_Set.e_rls
1.115 + erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty
1.116 [(*for asm in NTH_CONS ...*)
1.117 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.118 (*2nd NTH_CONS pushes n+-1 into asms*)
1.119 @@ -550,7 +550,7 @@
1.120 " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
1.121 ("#Find" ,["solution ss'''"])],
1.122 {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.123 - srls = Rule_Set.append_rls "srls_top_down_2x2" Rule_Set.e_rls
1.124 + srls = Rule_Set.append_rules "srls_top_down_2x2" Rule_Set.empty
1.125 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.126 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.127 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.128 @@ -585,7 +585,7 @@
1.129 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.130 ("#Find" ,["solution ss'''"])],
1.131 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.132 - srls = Rule_Set.append_rls "srls_normalise_2x2" Rule_Set.e_rls
1.133 + srls = Rule_Set.append_rules "srls_normalise_2x2" Rule_Set.empty
1.134 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.135 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.136 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.137 @@ -617,7 +617,7 @@
1.138 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.139 ("#Find" ,["solution ss'''"])],
1.140 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.141 - srls = Rule_Set.append_rls "srls_normalise_4x4" srls
1.142 + srls = Rule_Set.append_rules "srls_normalise_4x4" srls
1.143 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.144 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.145 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.146 @@ -654,8 +654,8 @@
1.147 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
1.148 ("#Find", ["solution ss'''"])],
1.149 {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.150 - srls = Rule_Set.append_rls "srls_top_down_4x4" srls [],
1.151 - prls = Rule_Set.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.152 + srls = Rule_Set.append_rules "srls_top_down_4x4" srls [],
1.153 + prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.154 [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.155 crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.156 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)