src/HOL/Tools/lin_arith.ML
changeset 34974 18b41bba42b5
parent 33728 cb4235333c30
child 35028 108662d50512
--- a/src/HOL/Tools/lin_arith.ML	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Thu Jan 28 11:48:49 2010 +0100
@@ -138,8 +138,8 @@
 *)
 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)
       | _ =>
@@ -150,7 +150,7 @@
               (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
@@ -170,9 +170,9 @@
         (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 -
@@ -196,23 +196,23 @@
   (* 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)
@@ -229,8 +229,8 @@
   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;
@@ -292,11 +292,11 @@
     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))
@@ -372,7 +372,7 @@
         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)
@@ -387,7 +387,7 @@
         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)
@@ -397,16 +397,16 @@
         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]
@@ -415,22 +415,22 @@
         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]
@@ -442,8 +442,8 @@
     | (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)
@@ -451,7 +451,7 @@
         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]
@@ -465,7 +465,7 @@
     | (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
@@ -477,11 +477,11 @@
                                         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]
@@ -497,7 +497,7 @@
     | (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
@@ -509,11 +509,11 @@
                                         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]
@@ -535,7 +535,7 @@
         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
@@ -545,21 +545,21 @@
         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]
@@ -589,7 +589,7 @@
         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
@@ -599,21 +599,21 @@
         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]