1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Mon Aug 09 14:20:20 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue Aug 10 09:43:07 2021 +0200
1.3 @@ -24,22 +24,21 @@
1.4
1.5 ML \<open>
1.6 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
1.7 - Rule_Set.append_rules "LinEq_prls" Rule_Set.empty
1.8 - [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.9 - \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
1.10 - \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
1.11 - \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
1.12 - \<^rule_eval>\<open>has_degree_in\<close> (eval_has_degree_in ""),
1.13 - \<^rule_eval>\<open>is_polyrat_in\<close> (eval_is_polyrat_in ""),
1.14 - \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
1.15 - \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.16 - \<^rule_thm>\<open>not_true\<close>,
1.17 - \<^rule_thm>\<open>not_false\<close>,
1.18 - \<^rule_thm>\<open>and_true\<close>,
1.19 - \<^rule_thm>\<open>and_false\<close>,
1.20 - \<^rule_thm>\<open>or_true\<close>,
1.21 - \<^rule_thm>\<open>or_false\<close>
1.22 - ];
1.23 + Rule_Set.append_rules "LinEq_prls" Rule_Set.empty [
1.24 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.25 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
1.26 + \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
1.27 + \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
1.28 + \<^rule_eval>\<open>has_degree_in\<close> (eval_has_degree_in ""),
1.29 + \<^rule_eval>\<open>is_polyrat_in\<close> (eval_is_polyrat_in ""),
1.30 + \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
1.31 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.32 + \<^rule_thm>\<open>not_true\<close>,
1.33 + \<^rule_thm>\<open>not_false\<close>,
1.34 + \<^rule_thm>\<open>and_true\<close>,
1.35 + \<^rule_thm>\<open>and_false\<close>,
1.36 + \<^rule_thm>\<open>or_true\<close>,
1.37 + \<^rule_thm>\<open>or_false\<close>];
1.38 (* ----- erls ----- *)
1.39 val LinEq_crls =
1.40 Rule_Set.append_rules "LinEq_crls" poly_crls
1.41 @@ -53,8 +52,8 @@
1.42
1.43 (* ----- crls ----- *)
1.44 val LinEq_erls =
1.45 - Rule_Set.append_rules "LinEq_erls" Poly_erls
1.46 - [\<^rule_thm>\<open>real_assoc_1\<close>
1.47 + Rule_Set.append_rules "LinEq_erls" Poly_erls [
1.48 + \<^rule_thm>\<open>real_assoc_1\<close>
1.49 (*
1.50 Don't use
1.51 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.52 @@ -67,42 +66,37 @@
1.53
1.54 val LinPoly_simplify = prep_rls'(
1.55 Rule_Def.Repeat {id = "LinPoly_simplify", preconds = [],
1.56 - rew_ord = ("termlessI",termlessI),
1.57 - erls = LinEq_erls,
1.58 - srls = Rule_Set.Empty,
1.59 - calc = [], errpatts = [],
1.60 - rules = [
1.61 - \<^rule_thm>\<open>real_assoc_1\<close>,
1.62 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.63 - \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
1.64 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.65 - (* Don't use
1.66 - \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.67 - \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
1.68 - *)
1.69 - \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")
1.70 - ],
1.71 - scr = Rule.Empty_Prog});
1.72 + rew_ord = ("termlessI",termlessI),
1.73 + erls = LinEq_erls,
1.74 + srls = Rule_Set.Empty,
1.75 + calc = [], errpatts = [],
1.76 + rules = [
1.77 + \<^rule_thm>\<open>real_assoc_1\<close>,
1.78 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.79 + \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
1.80 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.81 + (* Don't use
1.82 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.83 + \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
1.84 + *)
1.85 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")],
1.86 + scr = Rule.Empty_Prog});
1.87 \<close>
1.88 rule_set_knowledge LinPoly_simplify = LinPoly_simplify
1.89 ML \<open>
1.90
1.91 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
1.92 val LinEq_simplify = prep_rls'(
1.93 -Rule_Def.Repeat {id = "LinEq_simplify", preconds = [],
1.94 - rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.95 - erls = LinEq_erls,
1.96 - srls = Rule_Set.Empty,
1.97 - calc = [], errpatts = [],
1.98 - rules = [
1.99 - \<^rule_thm>\<open>lin_isolate_add1\<close>,
1.100 - (* a+bx=0 -> bx=-a *)
1.101 - \<^rule_thm>\<open>lin_isolate_add2\<close>,
1.102 - (* a+ x=0 -> x=-a *)
1.103 - \<^rule_thm>\<open>lin_isolate_div\<close>
1.104 - (* bx=c -> x=c/b *)
1.105 - ],
1.106 - scr = Rule.Empty_Prog});
1.107 + Rule_Def.Repeat {id = "LinEq_simplify", preconds = [],
1.108 + rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.109 + erls = LinEq_erls,
1.110 + srls = Rule_Set.Empty,
1.111 + calc = [], errpatts = [],
1.112 + rules = [
1.113 + \<^rule_thm>\<open>lin_isolate_add1\<close>, (* a+bx=0 -> bx=-a *)
1.114 + \<^rule_thm>\<open>lin_isolate_add2\<close>, (* a+ x=0 -> x=-a *)
1.115 + \<^rule_thm>\<open>lin_isolate_div\<close> (* bx=c -> x=c/b *)],
1.116 + scr = Rule.Empty_Prog});
1.117 \<close>
1.118 rule_set_knowledge LinEq_simplify = LinEq_simplify
1.119