1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Aug 03 18:17:27 2022 +0200
1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Thu Aug 04 12:48:37 2022 +0200
1.3 @@ -361,7 +361,7 @@
1.4
1.5 val cancel_leading_coeff = prep_rls'(
1.6 Rule_Def.Repeat {id = "cancel_leading_coeff", preconds = [],
1.7 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
1.8 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
1.9 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.10 rules = [
1.11 \<^rule_thm>\<open>cancel_leading_coeff1\<close>,
1.12 @@ -384,7 +384,7 @@
1.13 ML\<open>
1.14 val complete_square = prep_rls'(
1.15 Rule_Def.Repeat {id = "complete_square", preconds = [],
1.16 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
1.17 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
1.18 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.19 rules = [
1.20 \<^rule_thm>\<open>complete_square1\<close>,
1.21 @@ -427,7 +427,7 @@
1.22 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
1.23 val d0_polyeq_simplify = prep_rls'(
1.24 Rule_Def.Repeat {id = "d0_polyeq_simplify", preconds = [],
1.25 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
1.26 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
1.27 erls = PolyEq_erls,
1.28 srls = Rule_Set.Empty,
1.29 calc = [], errpatts = [],
1.30 @@ -440,7 +440,7 @@
1.31 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
1.32 val d1_polyeq_simplify = prep_rls'(
1.33 Rule_Def.Repeat {id = "d1_polyeq_simplify", preconds = [],
1.34 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
1.35 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
1.36 erls = PolyEq_erls,
1.37 srls = Rule_Set.Empty,
1.38 calc = [], errpatts = [],
1.39 @@ -456,7 +456,7 @@
1.40 (* isolate the bound variable in an d2 equation with bdv only;
1.41 "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *)
1.42 val d2_polyeq_bdv_only_simplify = prep_rls'(
1.43 - Rule_Def.Repeat {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
1.44 + Rule_Def.Repeat {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
1.45 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.46 rules = [
1.47 \<^rule_thm>\<open>d2_prescind1\<close>, (* ax+bx^2=0 -> x(a+bx)=0 *)
1.48 @@ -475,7 +475,7 @@
1.49 'bdv' is a meta-constant*)
1.50 val d2_polyeq_sq_only_simplify = prep_rls'(
1.51 Rule_Def.Repeat {id = "d2_polyeq_sq_only_simplify", preconds = [],
1.52 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
1.53 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
1.54 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.55 rules = [
1.56 \<^rule_thm>\<open>d2_isolate_add1\<close>,(* a+ bx^2=0 -> bx^2=(-1)a*)
1.57 @@ -491,7 +491,7 @@
1.58 'bdv' is a meta-constant*)
1.59 val d2_polyeq_pqFormula_simplify = prep_rls'(
1.60 Rule_Def.Repeat {id = "d2_polyeq_pqFormula_simplify", preconds = [],
1.61 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
1.62 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
1.63 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.64 rules = [
1.65 \<^rule_thm>\<open>d2_pqformula1\<close>, (* q+px+ x^2=0 *)
1.66 @@ -518,7 +518,7 @@
1.67 'bdv' is a meta-constant*)
1.68 val d2_polyeq_abcFormula_simplify = prep_rls'(
1.69 Rule_Def.Repeat {id = "d2_polyeq_abcFormula_simplify", preconds = [],
1.70 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
1.71 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
1.72 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.73 rules = [
1.74 \<^rule_thm>\<open>d2_abcformula1\<close>, (*c+bx+cx^2=0 *)
1.75 @@ -545,7 +545,7 @@
1.76 'bdv' is a meta-constant*)
1.77 val d2_polyeq_simplify = prep_rls'(
1.78 Rule_Def.Repeat {id = "d2_polyeq_simplify", preconds = [],
1.79 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
1.80 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
1.81 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.82 rules = [
1.83 \<^rule_thm>\<open>d2_pqformula1\<close>, (* p+qx+ x^2=0 *)
1.84 @@ -578,7 +578,7 @@
1.85 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
1.86 val d3_polyeq_simplify = prep_rls'(
1.87 Rule_Def.Repeat {id = "d3_polyeq_simplify", preconds = [],
1.88 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
1.89 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
1.90 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.91 rules = [
1.92 \<^rule_thm>\<open>d3_reduce_equation1\<close>, (*a*bdv + b*bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (a + b*bdv + c*bdv \<up> 2=0)*)
1.93 @@ -608,7 +608,7 @@
1.94 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
1.95 val d4_polyeq_simplify = prep_rls'(
1.96 Rule_Def.Repeat {id = "d4_polyeq_simplify", preconds = [],
1.97 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
1.98 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
1.99 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.100 rules = [
1.101 \<^rule_thm>\<open>d4_sub_u1\<close> (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)],
1.102 @@ -1128,7 +1128,7 @@
1.103 ML\<open>
1.104 val collect_bdv = prep_rls'(
1.105 Rule_Def.Repeat{id = "collect_bdv", preconds = [],
1.106 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.107 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.108 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1.109 calc = [], errpatts = [],
1.110 rules = [\<^rule_thm>\<open>bdv_collect_1\<close>,
1.111 @@ -1163,7 +1163,7 @@
1.112 according to knowledge/Poly.sml.*)
1.113 val make_polynomial_in = prep_rls'(
1.114 Rule_Set.Sequence {
1.115 - id = "make_polynomial_in", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.116 + id = "make_polynomial_in", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.117 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.118 rules = [
1.119 Rule.Rls_ expand_poly,
1.120 @@ -1189,7 +1189,7 @@
1.121 ML\<open>
1.122 val make_ratpoly_in = prep_rls'(
1.123 Rule_Set.Sequence {
1.124 - id = "make_ratpoly_in", preconds = []:term list, rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.125 + id = "make_ratpoly_in", preconds = []:term list, rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.126 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.127 rules = [
1.128 Rule.Rls_ norm_Rational,