1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Fri Jun 13 09:55:49 2014 +0200
1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Fri Jun 13 10:29:06 2014 +0200
1.3 @@ -432,7 +432,7 @@
1.4 Thm ("rat_leq3", num_str @{thm rat_leq3})
1.5 ]);
1.6
1.7 -val cancel_leading_coeff = prep_rls(
1.8 +val cancel_leading_coeff = prep_rls'(
1.9 Rls {id = "cancel_leading_coeff", preconds = [],
1.10 rew_ord = ("e_rew_ord",e_rew_ord),
1.11 erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
1.12 @@ -451,9 +451,11 @@
1.13 Thm ("cancel_leading_coeff12",num_str @{thm cancel_leading_coeff12}),
1.14 Thm ("cancel_leading_coeff13",num_str @{thm cancel_leading_coeff13})
1.15 ],scr = Prog ((term_of o the o (parse thy)) "empty_script")}:rls);
1.16 +
1.17 +val prep_rls' = prep_rls @{theory};
1.18 *}
1.19 ML{*
1.20 -val complete_square = prep_rls(
1.21 +val complete_square = prep_rls'(
1.22 Rls {id = "complete_square", preconds = [],
1.23 rew_ord = ("e_rew_ord",e_rew_ord),
1.24 erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
1.25 @@ -466,7 +468,7 @@
1.26 scr = Prog ((term_of o the o (parse thy)) "empty_script")
1.27 }:rls);
1.28
1.29 -val polyeq_simplify = prep_rls(
1.30 +val polyeq_simplify = prep_rls'(
1.31 Rls {id = "polyeq_simplify", preconds = [],
1.32 rew_ord = ("termlessI",termlessI),
1.33 erls = PolyEq_erls,
1.34 @@ -498,7 +500,7 @@
1.35 (* ------------- polySolve ------------------ *)
1.36 (* -- d0 -- *)
1.37 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
1.38 -val d0_polyeq_simplify = prep_rls(
1.39 +val d0_polyeq_simplify = prep_rls'(
1.40 Rls {id = "d0_polyeq_simplify", preconds = [],
1.41 rew_ord = ("e_rew_ord",e_rew_ord),
1.42 erls = PolyEq_erls,
1.43 @@ -512,7 +514,7 @@
1.44
1.45 (* -- d1 -- *)
1.46 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
1.47 -val d1_polyeq_simplify = prep_rls(
1.48 +val d1_polyeq_simplify = prep_rls'(
1.49 Rls {id = "d1_polyeq_simplify", preconds = [],
1.50 rew_ord = ("e_rew_ord",e_rew_ord),
1.51 erls = PolyEq_erls,
1.52 @@ -534,7 +536,7 @@
1.53 ML{*
1.54 (* isolate the bound variable in an d2 equation with bdv only;
1.55 "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *)
1.56 -val d2_polyeq_bdv_only_simplify = prep_rls(
1.57 +val d2_polyeq_bdv_only_simplify = prep_rls'(
1.58 Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
1.59 erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
1.60 rules =
1.61 @@ -555,7 +557,7 @@
1.62 ML{*
1.63 (* isolate the bound variable in an d2 equation with sqrt only;
1.64 'bdv' is a meta-constant*)
1.65 -val d2_polyeq_sq_only_simplify = prep_rls(
1.66 +val d2_polyeq_sq_only_simplify = prep_rls'(
1.67 Rls {id = "d2_polyeq_sq_only_simplify", preconds = [],
1.68 rew_ord = ("e_rew_ord",e_rew_ord),
1.69 erls = PolyEq_erls,
1.70 @@ -582,7 +584,7 @@
1.71 ML{*
1.72 (* isolate the bound variable in an d2 equation with pqFormula;
1.73 'bdv' is a meta-constant*)
1.74 -val d2_polyeq_pqFormula_simplify = prep_rls(
1.75 +val d2_polyeq_pqFormula_simplify = prep_rls'(
1.76 Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],
1.77 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
1.78 srls = Erls, calc = [], errpatts = [],
1.79 @@ -628,7 +630,7 @@
1.80 ML{*
1.81 (* isolate the bound variable in an d2 equation with abcFormula;
1.82 'bdv' is a meta-constant*)
1.83 -val d2_polyeq_abcFormula_simplify = prep_rls(
1.84 +val d2_polyeq_abcFormula_simplify = prep_rls'(
1.85 Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],
1.86 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
1.87 srls = Erls, calc = [], errpatts = [],
1.88 @@ -676,7 +678,7 @@
1.89
1.90 (* isolate the bound variable in an d2 equation;
1.91 'bdv' is a meta-constant*)
1.92 -val d2_polyeq_simplify = prep_rls(
1.93 +val d2_polyeq_simplify = prep_rls'(
1.94 Rls {id = "d2_polyeq_simplify", preconds = [],
1.95 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
1.96 srls = Erls, calc = [], errpatts = [],
1.97 @@ -736,7 +738,7 @@
1.98
1.99 (* -- d3 -- *)
1.100 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
1.101 -val d3_polyeq_simplify = prep_rls(
1.102 +val d3_polyeq_simplify = prep_rls'(
1.103 Rls {id = "d3_polyeq_simplify", preconds = [],
1.104 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
1.105 srls = Erls, calc = [], errpatts = [],
1.106 @@ -809,7 +811,7 @@
1.107
1.108 (* -- d4 -- *)
1.109 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
1.110 -val d4_polyeq_simplify = prep_rls(
1.111 +val d4_polyeq_simplify = prep_rls'(
1.112 Rls {id = "d4_polyeq_simplify", preconds = [],
1.113 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
1.114 srls = Erls, calc = [], errpatts = [],
1.115 @@ -1237,7 +1239,7 @@
1.116
1.117 *}
1.118 ML{*
1.119 -val order_add_mult_in = prep_rls(
1.120 +val order_add_mult_in = prep_rls'(
1.121 Rls{id = "order_add_mult_in", preconds = [],
1.122 rew_ord = ("ord_make_polynomial_in",
1.123 ord_make_polynomial_in false @{theory "Poly"}),
1.124 @@ -1259,7 +1261,7 @@
1.125
1.126 *}
1.127 ML{*
1.128 -val collect_bdv = prep_rls(
1.129 +val collect_bdv = prep_rls'(
1.130 Rls{id = "collect_bdv", preconds = [],
1.131 rew_ord = ("dummy_ord", dummy_ord),
1.132 erls = e_rls,srls = Erls,
1.133 @@ -1294,7 +1296,7 @@
1.134 ML{*
1.135 (*.transforms an arbitrary term without roots to a polynomial [4]
1.136 according to knowledge/Poly.sml.*)
1.137 -val make_polynomial_in = prep_rls(
1.138 +val make_polynomial_in = prep_rls'(
1.139 Seq {id = "make_polynomial_in", preconds = []:term list,
1.140 rew_ord = ("dummy_ord", dummy_ord),
1.141 erls = Atools_erls, srls = Erls,
1.142 @@ -1330,7 +1332,7 @@
1.143 ];
1.144 *}
1.145 ML{*
1.146 -val make_ratpoly_in = prep_rls(
1.147 +val make_ratpoly_in = prep_rls'(
1.148 Seq {id = "make_ratpoly_in", preconds = []:term list,
1.149 rew_ord = ("dummy_ord", dummy_ord),
1.150 erls = Atools_erls, srls = Erls,