1.1 --- a/src/HOL/Tools/lin_arith.ML Tue Jan 15 16:19:21 2008 +0100
1.2 +++ b/src/HOL/Tools/lin_arith.ML Tue Jan 15 16:19:23 2008 +0100
1.3 @@ -203,7 +203,7 @@
1.4 in which case dest_numeral raises TERM; hence all the handles below.
1.5 Same for Suc-terms that turn out not to be numerals -
1.6 although the simplifier should eliminate those anyway ...*)
1.7 - | demult (t as Const ("Numeral.number_class.number_of", _) $ n, m) =
1.8 + | demult (t as Const ("Int.number_class.number_of", _) $ n, m) =
1.9 ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n)))
1.10 handle TERM _ => (SOME t, m))
1.11 | demult (t as Const (@{const_name Suc}, _) $ _, m) =
1.12 @@ -242,7 +242,7 @@
1.13 (case demult inj_consts (all, m) of
1.14 (NONE, m') => (p, Rat.add i m')
1.15 | (SOME u, m') => add_atom u m' pi)
1.16 - | poly (all as Const ("Numeral.number_class.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
1.17 + | poly (all as Const ("Int.number_class.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
1.18 (let val k = HOLogic.dest_numeral t
1.19 val k2 = if k < 0 andalso T = HOLogic.natT then 0 else k
1.20 in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k2))) end
1.21 @@ -324,7 +324,7 @@
1.22 @{const_name Orderings.min},
1.23 @{const_name HOL.abs},
1.24 @{const_name HOL.minus},
1.25 - "IntDef.nat",
1.26 + "Int.nat",
1.27 "Divides.div_class.mod",
1.28 "Divides.div_class.div"] a
1.29 | _ => (warning ("Lin. Arith.: wrong format for split rule " ^
1.30 @@ -462,7 +462,7 @@
1.31 SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)]
1.32 end
1.33 (* ?P (nat ?i) = ((ALL n. ?i = int n --> ?P n) & (?i < 0 --> ?P 0)) *)
1.34 - | (Const ("IntDef.nat", _), [t1]) =>
1.35 + | (Const ("Int.nat", _), [t1]) =>
1.36 let
1.37 val rev_terms = rev terms
1.38 val zero_int = Const (@{const_name HOL.zero}, HOLogic.intT)
1.39 @@ -553,7 +553,7 @@
1.40 (neg (number_of ?k) -->
1.41 (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
1.42 | (Const ("Divides.div_class.mod",
1.43 - Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
1.44 + Type ("fun", [Type ("Int.int", []), _])), [t1, t2 as (number_of $ k)]) =>
1.45 let
1.46 val rev_terms = rev terms
1.47 val zero = Const (@{const_name HOL.zero}, split_type)
1.48 @@ -564,8 +564,8 @@
1.49 (map (incr_boundvars 2) rev_terms)
1.50 val t1' = incr_boundvars 2 t1
1.51 val (t2' as (_ $ k')) = incr_boundvars 2 t2
1.52 - val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
1.53 - val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
1.54 + val iszero_t2 = Const ("Int.iszero", split_type --> HOLogic.boolT) $ t2
1.55 + val neg_minus_k = Const ("Int.neg", split_type --> HOLogic.boolT) $
1.56 (number_of $
1.57 (Const (@{const_name HOL.uminus},
1.58 HOLogic.intT --> HOLogic.intT) $ k'))
1.59 @@ -577,7 +577,7 @@
1.60 (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
1.61 (Const (@{const_name HOL.times},
1.62 split_type --> split_type --> split_type) $ t2' $ i) $ j)
1.63 - val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
1.64 + val neg_t2 = Const ("Int.neg", split_type --> HOLogic.boolT) $ t2'
1.65 val t2_lt_j = Const (@{const_name HOL.less},
1.66 split_type --> split_type--> HOLogic.boolT) $ t2' $ j
1.67 val j_leq_zero = Const (@{const_name HOL.less_eq},
1.68 @@ -605,7 +605,7 @@
1.69 (neg (number_of ?k) -->
1.70 (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
1.71 | (Const ("Divides.div_class.div",
1.72 - Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
1.73 + Type ("fun", [Type ("Int.int", []), _])), [t1, t2 as (number_of $ k)]) =>
1.74 let
1.75 val rev_terms = rev terms
1.76 val zero = Const (@{const_name HOL.zero}, split_type)
1.77 @@ -616,8 +616,8 @@
1.78 (map (incr_boundvars 2) rev_terms)
1.79 val t1' = incr_boundvars 2 t1
1.80 val (t2' as (_ $ k')) = incr_boundvars 2 t2
1.81 - val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
1.82 - val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
1.83 + val iszero_t2 = Const ("Int.iszero", split_type --> HOLogic.boolT) $ t2
1.84 + val neg_minus_k = Const ("Int.neg", split_type --> HOLogic.boolT) $
1.85 (number_of $
1.86 (Const (@{const_name HOL.uminus},
1.87 HOLogic.intT --> HOLogic.intT) $ k'))
1.88 @@ -630,7 +630,7 @@
1.89 (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
1.90 (Const (@{const_name HOL.times},
1.91 split_type --> split_type --> split_type) $ t2' $ i) $ j)
1.92 - val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
1.93 + val neg_t2 = Const ("Int.neg", split_type --> HOLogic.boolT) $ t2'
1.94 val t2_lt_j = Const (@{const_name HOL.less},
1.95 split_type --> split_type--> HOLogic.boolT) $ t2' $ j
1.96 val j_leq_zero = Const (@{const_name HOL.less_eq},