Term.term_lpo takes order on terms rather than strings as argument.
authorballarin
Fri Jul 14 14:37:15 2006 +0200 (2006-07-14)
changeset 2012995e84d2c9f2c
parent 20128 8f0e07d7cf92
child 20130 5303e5928285
Term.term_lpo takes order on terms rather than strings as argument.
src/HOL/Algebra/abstract/order.ML
src/HOL/Algebra/ringsimp.ML
src/HOL/OrderedGroup.ML
src/Pure/term.ML
     1.1 --- a/src/HOL/Algebra/abstract/order.ML	Fri Jul 14 14:19:48 2006 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/order.ML	Fri Jul 14 14:37:15 2006 +0200
     1.3 @@ -7,8 +7,9 @@
     1.4  
     1.5  (*** Term order for commutative rings ***)
     1.6  
     1.7 -fun ring_ord a =
     1.8 -  find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus", "1", "HOL.times"];
     1.9 +fun ring_ord (Const (a, _)) =
    1.10 +    find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus", "1", "HOL.times"]
    1.11 +  | ring_ord _ = ~1;
    1.12  
    1.13  fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
    1.14  
     2.1 --- a/src/HOL/Algebra/ringsimp.ML	Fri Jul 14 14:19:48 2006 +0200
     2.2 +++ b/src/HOL/Algebra/ringsimp.ML	Fri Jul 14 14:37:15 2006 +0200
     2.3 @@ -7,9 +7,10 @@
     2.4  
     2.5  (*** Term order for commutative rings ***)
     2.6  
     2.7 -fun ring_ord a =
     2.8 -  find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
     2.9 -  "CRing.minus", "Group.monoid.one", "Group.monoid.mult"];
    2.10 +fun ring_ord (Const (a, _)) =
    2.11 +    find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
    2.12 +      "CRing.minus", "Group.monoid.one", "Group.monoid.mult"]
    2.13 +  | ring_ord _ = ~1;
    2.14  
    2.15  fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
    2.16  
     3.1 --- a/src/HOL/OrderedGroup.ML	Fri Jul 14 14:19:48 2006 +0200
     3.2 +++ b/src/HOL/OrderedGroup.ML	Fri Jul 14 14:37:15 2006 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  (*  Title:      HOL/OrderedGroup.ML
     3.5      ID:         $Id$
     3.6 -    Author:     Steven Obua, Tobias Nipkow, Technische Universitaet Mnchen
     3.7 +    Author:     Steven Obua, Tobias Nipkow, Technische Universitaet Muenchen
     3.8  *)
     3.9  
    3.10  structure ab_group_add_cancel_data :> ABEL_CANCEL  = 
    3.11 @@ -8,7 +8,8 @@
    3.12  
    3.13  (*** Term order for abelian groups ***)
    3.14  
    3.15 -fun agrp_ord a = find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus"];
    3.16 +fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus"]
    3.17 +  | agrp_ord _ = ~1;
    3.18  
    3.19  fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
    3.20  
     4.1 --- a/src/Pure/term.ML	Fri Jul 14 14:19:48 2006 +0200
     4.2 +++ b/src/Pure/term.ML	Fri Jul 14 14:37:15 2006 +0200
     4.3 @@ -172,7 +172,7 @@
     4.4    val term_ord: term * term -> order
     4.5    val hd_ord: term * term -> order
     4.6    val termless: term * term -> bool
     4.7 -  val term_lpo: (string -> int) -> term * term -> order
     4.8 +  val term_lpo: (term -> int) -> term * term -> order
     4.9    val match_bvars: (term * term) * (string * string) list -> (string * string) list
    4.10    val rename_abs: term -> term -> term -> term option
    4.11    val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
    4.12 @@ -646,23 +646,26 @@
    4.13    Without variables.  Const, Var, Bound, Free and Abs are treated all as
    4.14    constants.
    4.15  
    4.16 -  f_ord maps strings to integers and serves two purposes:
    4.17 +  f_ord maps terms to integers and serves two purposes:
    4.18    - Predicate on constant symbols.  Those that are not recognised by f_ord
    4.19      must be mapped to ~1.
    4.20    - Order on the recognised symbols.  These must be mapped to distinct
    4.21      integers >= 0.
    4.22 -
    4.23 +  The argument of f_ord is never an application.
    4.24  *)
    4.25  
    4.26  local
    4.27 -fun dest_hd f_ord (Const (a, T)) =
    4.28 -      let val ord = f_ord a in
    4.29 -        if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
    4.30 +
    4.31 +fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
    4.32 +  | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
    4.33 +  | unrecognized (Var v) = ((1, v), 1)
    4.34 +  | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
    4.35 +  | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
    4.36 +
    4.37 +fun dest_hd f_ord t =
    4.38 +      let val ord = f_ord t in
    4.39 +        if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0)
    4.40        end
    4.41 -  | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
    4.42 -  | dest_hd _ (Var v) = ((1, v), 1)
    4.43 -  | dest_hd _ (Bound i) = ((1, (("", i), dummyT)), 2)
    4.44 -  | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
    4.45  
    4.46  fun term_lpo f_ord (s, t) =
    4.47    let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in