--- 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
--- 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);
--- 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
--- 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.