src/HOL/Tools/lin_arith.ML

 
    returns either (SOME term, associated multiplicity) or (NONE, constant)
 *)
 fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
 let
-  fun demult ((mC as Const (@{const_name HOL.times}, _)) $ s $ t, m) =
-      (case s of Const (@{const_name HOL.times}, _) $ s1 $ s2 =>
+  fun demult ((mC as Const (@{const_name Algebras.times}, _)) $ s $ t, m) =
+      (case s of Const (@{const_name Algebras.times}, _) $ s1 $ s2 =>
         (* bracketing to the right: '(s1 * s2) * t' becomes 's1 * (s2 * t)' *)
         demult (mC $ s1 $ (mC $ s2 $ t), m)
       | _ =>
         (* product 's * t', where either factor can be 'NONE' *)
         (case demult (s, m) of
           (SOME s', m') =>
             (case demult (t, m') of
               (SOME t', m'') => (SOME (mC $ s' $ t'), m'')
             | (NONE,    m'') => (SOME s', m''))
         | (NONE,    m') => demult (t, m')))
-    | demult ((mC as Const (@{const_name HOL.divide}, _)) $ s $ t, m) =
+    | demult ((mC as Const (@{const_name Algebras.divide}, _)) $ s $ t, m) =
       (* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could
          become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ?   Note that
          if we choose to do so here, the simpset used by arith must be able to
          perform the same simplifications. *)
       (* FIXME: Currently we treat the numerator as atomic unless the

       (* Note: will raise Rat.DIVZERO iff m' is Rat.zero *)
       (case demult (t, Rat.one) of
         (SOME _, _) => (SOME (mC $ s $ t), m)
       | (NONE,  m') => apsnd (Rat.mult (Rat.inv m')) (demult (s, m)))
     (* terms that evaluate to numeric constants *)
-    | demult (Const (@{const_name HOL.uminus}, _) $ t, m) = demult (t, Rat.neg m)
-    | demult (Const (@{const_name HOL.zero}, _), m) = (NONE, Rat.zero)
-    | demult (Const (@{const_name HOL.one}, _), m) = (NONE, m)
+    | demult (Const (@{const_name Algebras.uminus}, _) $ t, m) = demult (t, Rat.neg m)
+    | demult (Const (@{const_name Algebras.zero}, _), m) = (NONE, Rat.zero)
+    | demult (Const (@{const_name Algebras.one}, _), m) = (NONE, m)
     (*Warning: in rare cases number_of encloses a non-numeral,
       in which case dest_numeral raises TERM; hence all the handles below.
       Same for Suc-terms that turn out not to be numerals -
       although the simplifier should eliminate those anyway ...*)
     | demult (t as Const ("Int.number_class.number_of", _) $ n, m) =

             ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat) option =
 let
   (* Turns a term 'all' and associated multiplicity 'm' into a list 'p' of
      summands and associated multiplicities, plus a constant 'i' (with implicit
      multiplicity 1) *)
-  fun poly (Const (@{const_name HOL.plus}, _) $ s $ t,
+  fun poly (Const (@{const_name Algebras.plus}, _) $ s $ t,
         m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi))
-    | poly (all as Const (@{const_name HOL.minus}, T) $ s $ t, m, pi) =
+    | poly (all as Const (@{const_name Algebras.minus}, T) $ s $ t, m, pi) =
         if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi))
-    | poly (all as Const (@{const_name HOL.uminus}, T) $ t, m, pi) =
+    | poly (all as Const (@{const_name Algebras.uminus}, T) $ t, m, pi) =
         if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
-    | poly (Const (@{const_name HOL.zero}, _), _, pi) =
+    | poly (Const (@{const_name Algebras.zero}, _), _, pi) =
         pi
-    | poly (Const (@{const_name HOL.one}, _), m, (p, i)) =
+    | poly (Const (@{const_name Algebras.one}, _), m, (p, i)) =
         (p, Rat.add i m)
     | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
         poly (t, m, (p, Rat.add i m))
-    | poly (all as Const (@{const_name HOL.times}, _) $ _ $ _, m, pi as (p, i)) =
+    | poly (all as Const (@{const_name Algebras.times}, _) $ _ $ _, m, pi as (p, i)) =
         (case demult inj_consts (all, m) of
            (NONE,   m') => (p, Rat.add i m')
          | (SOME u, m') => add_atom u m' pi)
-    | poly (all as Const (@{const_name HOL.divide}, _) $ _ $ _, m, pi as (p, i)) =
+    | poly (all as Const (@{const_name Algebras.divide}, _) $ _ $ _, m, pi as (p, i)) =
         (case demult inj_consts (all, m) of
            (NONE,   m') => (p, Rat.add i m')
          | (SOME u, m') => add_atom u m' pi)
     | poly (all as Const ("Int.number_class.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
         (let val k = HOLogic.dest_numeral t

         add_atom all m pi
   val (p, i) = poly (lhs, Rat.one, ([], Rat.zero))
   val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
 in
   case rel of
-    @{const_name HOL.less}    => SOME (p, i, "<", q, j)
-  | @{const_name HOL.less_eq} => SOME (p, i, "<=", q, j)
+    @{const_name Algebras.less}    => SOME (p, i, "<", q, j)
+  | @{const_name Algebras.less_eq} => SOME (p, i, "<=", q, j)
   | "op ="              => SOME (p, i, "=", q, j)
   | _                   => NONE
 end handle Rat.DIVZERO => NONE;
 
 fun of_lin_arith_sort thy U =

   case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (
     (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
     case head_of lhs of
       Const (a, _) => member (op =) [@{const_name Orderings.max},
                                     @{const_name Orderings.min},
-                                    @{const_name HOL.abs},
-                                    @{const_name HOL.minus},
-                                    "Int.nat",
-                                    "Divides.div_class.mod",
-                                    "Divides.div_class.div"] a
+                                    @{const_name Algebras.abs},
+                                    @{const_name Algebras.minus},
+                                    "Int.nat" (*DYNAMIC BINDING!*),
+                                    "Divides.div_class.mod" (*DYNAMIC BINDING!*),
+                                    "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
     | _            => (warning ("Lin. Arith.: wrong format for split rule " ^
                                  Display.string_of_thm_without_context thm);
                        false))
   | _ => (warning ("Lin. Arith.: wrong format for split rule " ^
                    Display.string_of_thm_without_context thm);

       (Const (@{const_name Orderings.max}, _), [t1, t2]) =>
       let
         val rev_terms     = rev terms
         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
-        val t1_leq_t2     = Const (@{const_name HOL.less_eq},
+        val t1_leq_t2     = Const (@{const_name Algebras.less_eq},
                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false]
         val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms1 @ [not_false]

     | (Const (@{const_name Orderings.min}, _), [t1, t2]) =>
       let
         val rev_terms     = rev terms
         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
-        val t1_leq_t2     = Const (@{const_name HOL.less_eq},
+        val t1_leq_t2     = Const (@{const_name Algebras.less_eq},
                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false]
         val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms2 @ [not_false]
       in
         SOME [(Ts, subgoal1), (Ts, subgoal2)]
       end
     (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
-    | (Const (@{const_name HOL.abs}, _), [t1]) =>
+    | (Const (@{const_name Algebras.abs}, _), [t1]) =>
       let
         val rev_terms   = rev terms
         val terms1      = map (subst_term [(split_term, t1)]) rev_terms
-        val terms2      = map (subst_term [(split_term, Const (@{const_name HOL.uminus},
+        val terms2      = map (subst_term [(split_term, Const (@{const_name Algebras.uminus},
                             split_type --> split_type) $ t1)]) rev_terms
-        val zero        = Const (@{const_name HOL.zero}, split_type)
-        val zero_leq_t1 = Const (@{const_name HOL.less_eq},
+        val zero        = Const (@{const_name Algebras.zero}, split_type)
+        val zero_leq_t1 = Const (@{const_name Algebras.less_eq},
                             split_type --> split_type --> HOLogic.boolT) $ zero $ t1
-        val t1_lt_zero  = Const (@{const_name HOL.less},
+        val t1_lt_zero  = Const (@{const_name Algebras.less},
                             split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1    = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
         val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
       in
         SOME [(Ts, subgoal1), (Ts, subgoal2)]
       end
     (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
-    | (Const (@{const_name HOL.minus}, _), [t1, t2]) =>
+    | (Const (@{const_name Algebras.minus}, _), [t1, t2]) =>
       let
         (* "d" in the above theorem becomes a new bound variable after NNF   *)
         (* transformation, therefore some adjustment of indices is necessary *)
         val rev_terms       = rev terms
-        val zero            = Const (@{const_name HOL.zero}, split_type)
+        val zero            = Const (@{const_name Algebras.zero}, split_type)
         val d               = Bound 0
         val terms1          = map (subst_term [(split_term, zero)]) rev_terms
         val terms2          = map (subst_term [(incr_boundvars 1 split_term, d)])
                                 (map (incr_boundvars 1) rev_terms)
         val t1'             = incr_boundvars 1 t1
         val t2'             = incr_boundvars 1 t2
-        val t1_lt_t2        = Const (@{const_name HOL.less},
+        val t1_lt_t2        = Const (@{const_name Algebras.less},
                                 split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                (Const (@{const_name HOL.plus},
+                                (Const (@{const_name Algebras.plus},
                                   split_type --> split_type --> split_type) $ t2' $ d)
         val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1        = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
         val subgoal2        = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false]
       in

       end
     (* ?P (nat ?i) = ((ALL n. ?i = of_nat n --> ?P n) & (?i < 0 --> ?P 0)) *)
     | (Const ("Int.nat", _), [t1]) =>
       let
         val rev_terms   = rev terms
-        val zero_int    = Const (@{const_name HOL.zero}, HOLogic.intT)
-        val zero_nat    = Const (@{const_name HOL.zero}, HOLogic.natT)
+        val zero_int    = Const (@{const_name Algebras.zero}, HOLogic.intT)
+        val zero_nat    = Const (@{const_name Algebras.zero}, HOLogic.natT)
         val n           = Bound 0
         val terms1      = map (subst_term [(incr_boundvars 1 split_term, n)])
                             (map (incr_boundvars 1) rev_terms)
         val terms2      = map (subst_term [(split_term, zero_nat)]) rev_terms
         val t1'         = incr_boundvars 1 t1
         val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
                             (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
-        val t1_lt_zero  = Const (@{const_name HOL.less},
+        val t1_lt_zero  = Const (@{const_name Algebras.less},
                             HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1    = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
         val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
       in

          ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) -->
            (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
     | (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
-        val zero                    = Const (@{const_name HOL.zero}, split_type)
+        val zero                    = Const (@{const_name Algebras.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
         val terms2                  = map (subst_term [(incr_boundvars 2 split_term, j)])
                                         (map (incr_boundvars 2) rev_terms)

         val t2'                     = incr_boundvars 2 t2
         val t2_eq_zero              = Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
         val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
-        val j_lt_t2                 = Const (@{const_name HOL.less},
+        val j_lt_t2                 = Const (@{const_name Algebras.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
-                                         (Const (@{const_name HOL.times},
+                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
+                                         (Const (@{const_name Algebras.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
         val subgoal2                = (map HOLogic.mk_Trueprop
                                         [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])

          ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) -->
            (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
     | (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
-        val zero                    = Const (@{const_name HOL.zero}, split_type)
+        val zero                    = Const (@{const_name Algebras.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
         val terms2                  = map (subst_term [(incr_boundvars 2 split_term, i)])
                                         (map (incr_boundvars 2) rev_terms)

         val t2'                     = incr_boundvars 2 t2
         val t2_eq_zero              = Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
         val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
-        val j_lt_t2                 = Const (@{const_name HOL.less},
+        val j_lt_t2                 = Const (@{const_name Algebras.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
-                                         (Const (@{const_name HOL.times},
+                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
+                                         (Const (@{const_name Algebras.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
         val subgoal2                = (map HOLogic.mk_Trueprop
                                         [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])

               number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
     | (Const ("Divides.div_class.mod",
         Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
-        val zero                    = Const (@{const_name HOL.zero}, split_type)
+        val zero                    = Const (@{const_name Algebras.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
         val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, j)])
                                         (map (incr_boundvars 2) rev_terms)
         val t1'                     = incr_boundvars 2 t1
         val t2'                     = incr_boundvars 2 t2
         val t2_eq_zero              = Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
-        val zero_lt_t2              = Const (@{const_name HOL.less},
+        val zero_lt_t2              = Const (@{const_name Algebras.less},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
-        val t2_lt_zero              = Const (@{const_name HOL.less},
+        val t2_lt_zero              = Const (@{const_name Algebras.less},
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
-        val zero_leq_j              = Const (@{const_name HOL.less_eq},
+        val zero_leq_j              = Const (@{const_name Algebras.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
-        val j_leq_zero              = Const (@{const_name HOL.less_eq},
+        val j_leq_zero              = Const (@{const_name Algebras.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
-        val j_lt_t2                 = Const (@{const_name HOL.less},
+        val j_lt_t2                 = Const (@{const_name Algebras.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
-        val t2_lt_j                 = Const (@{const_name HOL.less},
+        val t2_lt_j                 = Const (@{const_name Algebras.less},
                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
-                                         (Const (@{const_name HOL.times},
+                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
+                                         (Const (@{const_name Algebras.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
         val subgoal2                = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
                                         @ hd terms2_3

               number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P i))) *)
     | (Const ("Divides.div_class.div",
         Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
       let
         val rev_terms               = rev terms
-        val zero                    = Const (@{const_name HOL.zero}, split_type)
+        val zero                    = Const (@{const_name Algebras.zero}, split_type)
         val i                       = Bound 1
         val j                       = Bound 0
         val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
         val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, i)])
                                         (map (incr_boundvars 2) rev_terms)
         val t1'                     = incr_boundvars 2 t1
         val t2'                     = incr_boundvars 2 t2
         val t2_eq_zero              = Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
-        val zero_lt_t2              = Const (@{const_name HOL.less},
+        val zero_lt_t2              = Const (@{const_name Algebras.less},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
-        val t2_lt_zero              = Const (@{const_name HOL.less},
+        val t2_lt_zero              = Const (@{const_name Algebras.less},
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
-        val zero_leq_j              = Const (@{const_name HOL.less_eq},
+        val zero_leq_j              = Const (@{const_name Algebras.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
-        val j_leq_zero              = Const (@{const_name HOL.less_eq},
+        val j_leq_zero              = Const (@{const_name Algebras.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
-        val j_lt_t2                 = Const (@{const_name HOL.less},
+        val j_lt_t2                 = Const (@{const_name Algebras.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
-        val t2_lt_j                 = Const (@{const_name HOL.less},
+        val t2_lt_j                 = Const (@{const_name Algebras.less},
                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
-                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
-                                         (Const (@{const_name HOL.times},
+                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
+                                         (Const (@{const_name Algebras.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
         val subgoal2                = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
                                         @ hd terms2_3