# 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