1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Jun 10 17:06:32 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Fri Jun 11 11:49:34 2021 +0200
1.3 @@ -257,7 +257,7 @@
1.4 (*Rule.Rls_ discard_parentheses *3**),
1.5 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.6 Rule.Rls_ separate_bdv2,
1.7 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.8 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
1.9 ],
1.10 scr = Rule.Empty_Prog};
1.11 \<close>
1.12 @@ -275,7 +275,7 @@
1.13 Rule.Rls_ discard_parentheses,
1.14 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.15 Rule.Rls_ separate_bdv2,
1.16 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.17 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
1.18 ],
1.19 scr = Rule.Empty_Prog};
1.20 (*
1.21 @@ -290,10 +290,7 @@
1.22 Rule_Def.Repeat {id="isolate_bdvs", preconds = [],
1.23 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.24 erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
1.25 - [(Rule.Eval ("EqSystem.occur_exactly_in",
1.26 - eval_occur_exactly_in
1.27 - "#eval_occur_exactly_in_"))
1.28 - ],
1.29 + [(\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"))],
1.30 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.31 rules =
1.32 [Rule.Thm ("commute_0_equality", ThmC.numerals_to_Free @{thm commute_0_equality}),
1.33 @@ -307,10 +304,9 @@
1.34 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.35 erls = Rule_Set.append_rules
1.36 "erls_isolate_bdvs_4x4" Rule_Set.empty
1.37 - [Rule.Eval ("EqSystem.occur_exactly_in",
1.38 - eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.39 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.40 - Rule.Eval ("Prog_Expr.some_occur_in", Prog_Expr.eval_some_occur_in "#some_occur_in_"),
1.41 + [\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.42 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.43 + \<^rule_eval>\<open>Prog_Expr.some_occur_in\<close> (Prog_Expr.eval_some_occur_in "#some_occur_in_"),
1.44 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
1.45 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
1.46 ],
1.47 @@ -343,21 +339,19 @@
1.48 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.49 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.50 rules = [(*for precond NTH_CONS ...*)
1.51 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.52 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.53 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.54 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
1.55 (*immediately repeated rewrite pushes
1.56 '+' into precondition !*)
1.57 ],
1.58 scr = Rule.Empty_Prog},
1.59 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.60 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.61 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.62 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.63 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1.64 Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.65 Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
1.66 - Rule.Eval ("EqSystem.occur_exactly_in",
1.67 - eval_occur_exactly_in
1.68 - "#eval_occur_exactly_in_")
1.69 + \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")
1.70 ],
1.71 scr = Rule.Empty_Prog};
1.72 \<close>
1.73 @@ -372,21 +366,19 @@
1.74 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.75 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.76 rules = [(*for precond NTH_CONS ...*)
1.77 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.78 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.79 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.80 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
1.81 (*immediately repeated rewrite pushes
1.82 '+' into precondition !*)
1.83 ],
1.84 scr = Rule.Empty_Prog},
1.85 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.86 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.87 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.88 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.89 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1.90 Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.91 Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
1.92 - Rule.Eval ("EqSystem.occur_exactly_in",
1.93 - eval_occur_exactly_in
1.94 - "#eval_occur_exactly_in_")
1.95 + \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")
1.96 ],
1.97 scr = Rule.Empty_Prog};
1.98 \<close>
1.99 @@ -425,8 +417,8 @@
1.100 Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty
1.101 [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
1.102 Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
1.103 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.104 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.105 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.106 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
1.107 SOME "solveSystem e_s v_s", [])),
1.108 (Problem.prep_input @{theory} "pbl_equsys_lin_2x2_tri" [] Problem.id_empty
1.109 (["triangular", "2x2", "LINEAR", "system"],
1.110 @@ -452,8 +444,8 @@
1.111 Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty
1.112 [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
1.113 Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
1.114 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.115 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.116 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.117 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
1.118 SOME "solveSystem e_s v_s", [])),
1.119 (Problem.prep_input @{theory} "pbl_equsys_lin_4x4" [] Problem.id_empty
1.120 (["4x4", "LINEAR", "system"],
1.121 @@ -464,8 +456,8 @@
1.122 Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty
1.123 [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
1.124 Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
1.125 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.126 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.127 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.128 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
1.129 SOME "solveSystem e_s v_s", [])),
1.130 (Problem.prep_input @{theory} "pbl_equsys_lin_4x4_tri" [] Problem.id_empty
1.131 (["triangular", "4x4", "LINEAR", "system"],
1.132 @@ -477,7 +469,7 @@
1.133 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
1.134 ("#Find" ,["solution ss'''"])],
1.135 Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.136 - [Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "")],
1.137 + [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")],
1.138 SOME "solveSystem e_s v_s",
1.139 [["EqSystem", "top_down_substitution", "4x4"]])),
1.140 (Problem.prep_input @{theory} "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
1.141 @@ -496,13 +488,13 @@
1.142 rew_ord = ("termlessI",termlessI),
1.143 erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty
1.144 [(*for asm in NTH_CONS ...*)
1.145 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.146 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.147 (*2nd NTH_CONS pushes n+-1 into asms*)
1.148 - Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_")
1.149 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
1.150 ],
1.151 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.152 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.153 - Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.154 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.155 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL})],
1.156 scr = Rule.Empty_Prog};
1.157 \<close>
1.158 @@ -656,7 +648,7 @@
1.159 {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.160 srls = Rule_Set.append_rules "srls_top_down_4x4" srls [],
1.161 prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.162 - [Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "")],
1.163 + [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")],
1.164 crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.165 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
1.166 @{thm solve_system4.simps})]