# HG changeset patch # User nipkow # Date 1119708377 -7200 # Node ID e02fe7ae212b19f7eca407d53728cca8146da289 # Parent 1ff73dc291662f384b03270490384e13c9a2ef0f Changes due to new abel_cancel.ML diff -r 1ff73dc29166 -r e02fe7ae212b src/HOL/Algebra/ringsimp.ML --- a/src/HOL/Algebra/ringsimp.ML Sat Jun 25 12:37:07 2005 +0200 +++ b/src/HOL/Algebra/ringsimp.ML Sat Jun 25 16:06:17 2005 +0200 @@ -5,61 +5,13 @@ Copyright: TU Muenchen *) -local - -(*** Lexicographic path order on terms. - - See Baader & Nipkow, Term rewriting, CUP 1998. - Without variables. Const, Var, Bound, Free and Abs are treated all as - constants. - - 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. - -***) - -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); - -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 ***) fun ring_ord a = find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv", "CRing.minus", "Group.monoid.one", "Group.monoid.mult"]; -fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS); +fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS); val cring_ss = HOL_ss settermless termless_ring; @@ -95,5 +47,3 @@ r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0, a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus]; *) - -end; \ No newline at end of file diff -r 1ff73dc29166 -r e02fe7ae212b src/HOL/OrderedGroup.ML --- a/src/HOL/OrderedGroup.ML Sat Jun 25 12:37:07 2005 +0200 +++ b/src/HOL/OrderedGroup.ML Sat Jun 25 16:06:17 2005 +0200 @@ -1,40 +1,35 @@ (* Title: HOL/OrderedGroup.ML ID: $Id$ - Author: Steven Obua, Technische Universität München + Author: Steven Obua, Tobias Nipkow, Technische Universität München *) structure ab_group_add_cancel_data :> ABEL_CANCEL = struct - val ss = simpset_of HOL.thy + +(*** Term order for abelian groups ***) + +fun agrp_ord a = find_index_eq a ["0", "op +", "uminus", "op -"]; + +fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS); + +val cancel_ss = HOL_basic_ss settermless termless_agrp addsimps + [thm "add_assoc", thm "add_commute", thm "add_left_commute", + thm "add_0", thm "add_0_right", + thm "diff_def", thm "minus_add_distrib", + thm "minus_minus", thm "minus_zero", + thm "right_minus", thm "left_minus", + thm "add_minus_cancel", thm "minus_add_cancel"]; + val eq_reflection = thm "eq_reflection" val thy_ref = Theory.self_ref (theory "OrderedGroup") val T = TFree("'a", ["OrderedGroup.ab_group_add"]) - - val restrict_to_left = thm "restrict_to_left" - val add_cancel_21 = thm "add_cancel_21" - val add_cancel_end = thm "add_cancel_end" - val add_left_cancel = thm "add_left_cancel" - val add_assoc = thm "add_assoc" - val add_commute = thm "add_commute" - val add_left_commute = thm "add_left_commute" - val add_0 = thm "add_0" - val add_0_right = thm "add_0_right" - - val eq_diff_eq = thm "eq_diff_eq" - + val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"] fun dest_eqI th = #1 (HOLogic.dest_bin "op =" HOLogic.boolT (HOLogic.dest_Trueprop (concl_of th))) - - val diff_def = thm "diff_def" - val minus_add_distrib = thm "minus_add_distrib" - val minus_minus = thm "minus_minus" - val minus_0 = thm "minus_zero" - val add_inverses = [thm "right_minus", thm "left_minus"] - val cancel_simps = [thm "add_minus_cancel", thm "minus_add_cancel"] end; structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data); diff -r 1ff73dc29166 -r e02fe7ae212b src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Sat Jun 25 12:37:07 2005 +0200 +++ b/src/HOL/Ring_and_Field.thy Sat Jun 25 16:06:17 2005 +0200 @@ -1555,13 +1555,13 @@ have xy: "- ?x <= ?y" apply (simp) apply (rule_tac y="0::'a" in order_trans) - apply (rule addm2)+ + apply (rule addm2) apply (simp_all add: mult_pos_le mult_neg_le) - apply (rule addm)+ + apply (rule addm) apply (simp_all add: mult_pos_le mult_neg_le) done have yx: "?y <= ?x" - apply (simp add: add_ac) + apply (simp add:diff_def) apply (rule_tac y=0 in order_trans) apply (rule addm2, (simp add: mult_pos_neg_le mult_pos_neg2_le)+) apply (rule addm, (simp add: mult_pos_neg_le mult_pos_neg2_le)+) @@ -1687,7 +1687,7 @@ have 6: "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <= abs (y * (A - A') + (y * A' - c') + (c'-c)) * abs x" by (simp add: abs_le_mult) have 7: "(abs (y * (A - A') + (y * A' - c') + (c'-c))) * abs x <= (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x" - by (simp add: abs_triangle_ineq mult_right_mono) + by(rule abs_triangle_ineq [THEN mult_right_mono]) simp have 8: " (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x <= (abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x" by (simp add: abs_triangle_ineq mult_right_mono) have 9: "(abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x" @@ -1712,7 +1712,7 @@ by (simp) show ?thesis apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"]) - apply (simp_all add: 5 14[simplified abs_of_ge_0[of y, simplified prems]]) + apply (simp_all only: 5 14[simplified abs_of_ge_0[of y, simplified prems]]) done qed diff -r 1ff73dc29166 -r e02fe7ae212b src/HOL/ex/Lagrange.thy --- a/src/HOL/ex/Lagrange.thy Sat Jun 25 12:37:07 2005 +0200 +++ b/src/HOL/ex/Lagrange.thy Sat Jun 25 16:06:17 2005 +0200 @@ -21,6 +21,8 @@ abstract theorem about commutative rings. It has, a priori, nothing to do with nat.*) +ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]" + (*once a slow step, but now (2001) just three seconds!*) lemma Lagrange_lemma: "!!x1::'a::comm_ring.