# HG changeset patch # User ballarin # Date 1043309813 -3600 # Node ID 3294f727e20d48a9dfada5f6f3e7d97065bf4b0e # Parent 44de406a72732aa0dc0eaedd268d25ffec139ccd Fixed term order for normal form in rings. diff -r 44de406a7273 -r 3294f727e20d src/HOL/Algebra/abstract/Abstract.thy --- a/src/HOL/Algebra/abstract/Abstract.thy Fri Jan 17 23:52:54 2003 +0100 +++ b/src/HOL/Algebra/abstract/Abstract.thy Thu Jan 23 09:16:53 2003 +0100 @@ -4,4 +4,6 @@ Author: Clemens Ballarin, started 17 July 1997 *) -Abstract = RingHomo + Field +theory Abstract = RingHomo + Field: + +end diff -r 44de406a7273 -r 3294f727e20d src/HOL/Algebra/abstract/Ring.ML --- a/src/HOL/Algebra/abstract/Ring.ML Fri Jan 17 23:52:54 2003 +0100 +++ b/src/HOL/Algebra/abstract/Ring.ML Thu Jan 23 09:16:53 2003 +0100 @@ -274,7 +274,8 @@ qed "inverse_unique"; Goal "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"; -by (asm_full_simp_tac (simpset () addsimps [inverse_def, dvd_def]) 1); +by (asm_full_simp_tac (simpset () addsimps [inverse_def, dvd_def] + delsimprocs [ring_simproc]) 1); by (Clarify_tac 1); by (rtac theI 1); by (atac 1); diff -r 44de406a7273 -r 3294f727e20d src/HOL/Algebra/abstract/Ring.thy --- a/src/HOL/Algebra/abstract/Ring.thy Fri Jan 17 23:52:54 2003 +0100 +++ b/src/HOL/Algebra/abstract/Ring.thy Thu Jan 23 09:16:53 2003 +0100 @@ -211,12 +211,12 @@ (* lemma "(a::'a::ring) - (a - b) = b" apply simp -simproc seems to fail on this example + simproc seems to fail on this example (fixed with new term order) *) - +(* lemma bug: "(b::'a::ring) - (b - a) = a" by simp - (* simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" *) - + simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" +*) lemma m_lcancel: assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)" proof @@ -225,7 +225,7 @@ then have "a = 0 | (b - c) = 0" by (simp only: integral_iff) with prem have "b - c = 0" by auto then have "b = b - (b - c)" by simp - also have "b - (b - c) = c" by (rule bug) + also have "b - (b - c) = c" by simp finally show "b = c" . next assume "b = c" then show "a * b = a * c" by simp diff -r 44de406a7273 -r 3294f727e20d src/HOL/Algebra/abstract/RingHomo.ML --- a/src/HOL/Algebra/abstract/RingHomo.ML Fri Jan 17 23:52:54 2003 +0100 +++ b/src/HOL/Algebra/abstract/RingHomo.ML Thu Jan 23 09:16:53 2003 +0100 @@ -51,7 +51,7 @@ by (Asm_simp_tac 1); by (Simp_tac 1); by (dres_inst_tac [("a", "g (Suc n)"), ("b", "setsum g {..n}")] homo_add 1); -by (Asm_simp_tac 1); +by (Asm_full_simp_tac 1); qed "homo_SUM"; Addsimps [homo_add, homo_mult, homo_one, homo_zero, diff -r 44de406a7273 -r 3294f727e20d src/HOL/Algebra/abstract/order.ML --- a/src/HOL/Algebra/abstract/order.ML Fri Jan 17 23:52:54 2003 +0100 +++ b/src/HOL/Algebra/abstract/order.ML Thu Jan 23 09:16:53 2003 +0100 @@ -1,135 +1,78 @@ (* Title: Term order, needed for normal forms in rings Id: $Id$ - Author: Clemens Ballarin and Roland Zumkeller + Author: Clemens Ballarin Copyright: TU Muenchen *) local -(* -An order is a value of type - ('a -> bool, 'a * 'a -> bool). - -The two parts are: - 1) a unary predicate denoting the order's domain - 2) a binary predicate with the semanitcs "greater than" +(*** Lexicographic path order on terms. -If (d, ord) is an order then ord (a,b) is defined if both d a and d b. -*) - -(* -Combines two orders with disjoint domains and returns -another one. -When the compared values are from the same domain, the corresponding -order is used. If not the ones from the first domain are considerer -greater. (If a value is in neither of the two domains, exception -"Domain" is raised.) -*) + See Baader & Nipkow, Term rewriting, CUP 1998. + Without variables. Const, Var, Bound, Free and Abs are treated all as + constants. -fun combineOrd ((d1, ord1), (d2, ord2)) = - (fn x => d1 x orelse d2 x, - fn (a, b) => - if d1 a andalso d1 b then ord1 (a, b) else - if d1 a andalso d2 b then true else - if d2 a andalso d2 b then ord2 (a, b) else - if d2 a andalso d1 b then false else raise Domain) - - -(* Counts the number of function applications + 1. *) -(* ### is there a standard Isabelle function for this? *) - -fun tsize (a $ b) = tsize a + tsize b - | tsize _ = 1; + f_ord maps strings to integers and serves two purposes: + - Predicate on constant symbols. Those that are not recognised by f_ord + must be mapped to ~1. + - Order on the recognised symbols. These must be mapped to distinct + integers >= 0. -(* foldl on non-empty lists *) - -fun foldl2 f (x::xs) = foldl f (x,xs) - - -(* Compares two terms, ignoring type information. *) -infix e; -fun (Const (s1, _)) e (Const (s2, _)) = s1 = s2 - | (Free (s1, _)) e (Free (s2, _)) = s1 = s2 - | (Var (ix1, _)) e (Var (ix2, _)) = ix1 = ix2 - | (Bound i1) e (Bound i2) = i1 = i2 - | (Abs (s1, _, t1)) e (Abs (s2, _, t2)) = s1 = s2 andalso t1 = t2 - | (s1 $ s2) e (t1 $ t2) = s1 = t1 andalso s2 = t2 - | _ e _ = false - - +***) -(* Curried lexicographich path order induced by an order on function symbols. -Its feature include: -- compatibility with Epsilon-operations -- closure under substitutions -- well-foundedness -- subterm-property -- termination -- defined on all terms (not only on ground terms) -- linearity - -The order ignores types. -*) +fun dest_hd f_ord (Const (a, T)) = + let val ord = f_ord a in + if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0) + end + | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0) + | dest_hd _ (Var v) = ((1, v), 1) + | dest_hd _ (Bound i) = ((1, (("", i), Term.dummyT)), 2) + | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3); -infix g; -fun clpo (d, ord) (s,t) = - let val (op g) = clpo (d, ord) in - (s <> t) andalso - if tsize s < tsize t then not (t g s) else - (* improves performance. allowed because clpo is total. *) - #2 (foldl2 combineOrd [ - (fn _ $ _ => true | Abs _ => true | _ => false, - fn (Abs (_, _, s'), t) => s' e t orelse s' g t orelse - (case t of - Abs (_, _, t') => s' g t' - | t1 $ t2 => s g t1 andalso s g t2 - ) - | (s1 $ s2, t) => s1 e t orelse s2 e t orelse - s1 g t orelse s2 g t orelse - (case t of - t1 $ t2 => (s1 e t1 andalso s2 g t2) orelse - (s1 g t1 andalso s g t2) - | _ => false - ) - ), - (fn Free _ => true | _ => false, fn (Free (a,_), Free (b,_)) => a > b), - (fn Bound _ => true | _ => false, fn (Bound a, Bound b) => a > b), - (fn Const (c, _) => not (d c) | _ => false, fn (Const (a, _), Const (b, _)) => a > b), - (fn Const (c, _) => d c | _ => false, fn (Const (a, _), Const (b, _)) => ord (a,b)) - ]) (s,t) - end; - -(* -Open Issues: -- scheme variables have to be ordered (should be simple) -*) - -(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *) - -(* Returns the position of an element in a list. If the -element doesn't occur in the list, a MatchException is raised. *) -fun pos (x::xs) i = if x = i then 0 else 1 + pos xs i; - -(* Generates a finite linear order from a list. -[a, b, c] results in the order "a > b > c". *) -fun linOrd l = fn (a,b) => pos l a < pos l b; - -(* Determines whether an element is contained in a list. *) -fun contains (x::xs) i = (x = i) orelse (contains xs i) | - contains [] i = false; +fun term_lpo f_ord (s, t) = + let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in + if forall (fn si => term_lpo f_ord (si, t) = LESS) ss + then case hd_ord f_ord (f, g) of + GREATER => + if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts + then GREATER else LESS + | EQUAL => + if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts + then list_ord (term_lpo f_ord) (ss, ts) + else LESS + | LESS => LESS + else GREATER + end +and hd_ord f_ord (f, g) = case (f, g) of + (Abs (_, T, t), Abs (_, U, u)) => + (case term_lpo f_ord (t, u) of EQUAL => Term.typ_ord (T, U) | ord => ord) + | (_, _) => prod_ord (prod_ord int_ord + (prod_ord Term.indexname_ord Term.typ_ord)) int_ord + (dest_hd f_ord f, dest_hd f_ord g) in -(* Term order for commutative rings *) +(*** Term order for commutative rings ***) + +fun ring_ord a = + find_index_eq a ["0", "op +", "uminus", "op -", "1", "op *"]; + +fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS); + +(* Some code useful for debugging -fun termless_ring (a, b) = - let - val S = ["op *", "op -", "uminus", "op +", "0"]; - (* Order (decending from left to right) on the constant symbols *) - val baseOrd = (contains S, linOrd S); - in clpo baseOrd (b, a) - end; +val intT = HOLogic.intT; +val a = Free ("a", intT); +val b = Free ("b", intT); +val c = Free ("c", intT); +val plus = Const ("op +", [intT, intT]--->intT); +val mult = Const ("op *", [intT, intT]--->intT); +val uminus = Const ("uminus", intT-->intT); +val one = Const ("1", intT); +val f = Const("f", intT-->intT); + +*) (*** Rewrite rules ***) @@ -233,14 +176,14 @@ val ring_ss = HOL_basic_ss settermless termless_ring addsimps [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def, r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0, - a_lcomm, m_lcomm, r_distr, l_null, r_null, l_minus, r_minus]; + a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus]; + +(* Note: r_one is not necessary in ring_ss *) -val x = bind_thms ("ring_simps", [l_zero, r_zero, l_neg, r_neg, - minus_minus, minus0, +val x = bind_thms ("ring_simps", + [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0, l_one, r_one, l_null, r_null, l_minus, r_minus]); -(* note: r_one added to ring_simp but not ring_ss *) - (* note: not added (and not proved): a_lcancel_eq, a_rcancel_eq, power_one, power_Suc, power_zero, power_one, m_lcancel_eq, m_rcancel_eq, diff -r 44de406a7273 -r 3294f727e20d src/HOL/Algebra/poly/LongDiv.ML --- a/src/HOL/Algebra/poly/LongDiv.ML Fri Jan 17 23:52:54 2003 +0100 +++ b/src/HOL/Algebra/poly/LongDiv.ML Thu Jan 23 09:16:53 2003 +0100 @@ -105,13 +105,13 @@ (* case "x ~= 0 *) by (rotate_tac ~1 1); by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1); -by (Simp_tac 1); +(* by (Simp_tac 1); *) by (rtac impI 1); by (rtac deg_lcoeff_cancel2 1); (* replace by linear arithmetic??? *) - by (rtac le_trans 1); - by (rtac deg_smult_ring 1); - by (Simp_tac 1); + by (rtac le_trans 2); + by (rtac deg_smult_ring 2); + by (Simp_tac 2); by (Simp_tac 1); by (rtac le_trans 1); by (rtac deg_mult_ring 1); @@ -220,9 +220,10 @@ val uminus_zero = result(); Goal "!!a::'a::ring. a - b = 0 ==> a = b"; -br trans 1; -by (res_inst_tac [("b", "a")] (thm "bug") 2); -by (Asm_simp_tac 1); +by (res_inst_tac [("s", "a - (a - b)")] trans 1); +by (asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1); +by (Simp_tac 1); +by (Simp_tac 1); val diff_zero_imp_eq = result(); Goal "!!a::'a::ring. a = b ==> a + (-b) = 0"; diff -r 44de406a7273 -r 3294f727e20d src/HOL/Algebra/poly/UnivPoly.thy --- a/src/HOL/Algebra/poly/UnivPoly.thy Fri Jan 17 23:52:54 2003 +0100 +++ b/src/HOL/Algebra/poly/UnivPoly.thy Thu Jan 23 09:16:53 2003 +0100 @@ -145,10 +145,20 @@ proof (unfold up_one_def) qed simp +(* term order lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n" proof - have "!!f. f : UP ==> (%n. a * f n) : UP" by (unfold UP_def) (force simp add: ring_simps) +*) (* this force step is slow *) +(* then show ?thesis + apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP) +qed +*) +lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n" +proof - + have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP" + by (unfold UP_def) (force simp add: ring_simps) (* this force step is slow *) then show ?thesis by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP) @@ -315,7 +325,7 @@ lemma monom_zero [simp]: "monom 0 n = 0" by (simp add: monom_def up_zero_def) - +(* term order: application of coeff_mult goes wrong: rule not symmetric lemma monom_mult_is_smult: "monom (a::'a::ring) 0 * p = a *s p" proof (rule up_eqI) @@ -327,6 +337,23 @@ case Suc then show ?thesis by simp qed qed +*) +ML_setup {* Delsimprocs [ring_simproc] *} + +lemma monom_mult_is_smult: + "monom (a::'a::ring) 0 * p = a *s p" +proof (rule up_eqI) + fix k + have "coeff (p * monom a 0) k = coeff (a *s p) k" + proof (cases k) + case 0 then show ?thesis by simp ring + next + case Suc then show ?thesis by (simp add: ring_simps) ring + qed + then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring +qed + +ML_setup {* Addsimprocs [ring_simproc] *} lemma monom_add [simp]: "monom (a + b) n = monom (a::'a::ring) n + monom b n" @@ -740,9 +767,13 @@ also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero) finally show ?thesis . qed - +(* term order: makes this simpler!!! lemma smult_integral: "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0" by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast +*) +lemma smult_integral: + "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0" +by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) end \ No newline at end of file