--- 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]