--- a/src/HOL/Tools/lin_arith.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Thu Aug 19 11:02:14 2010 +0200
@@ -46,12 +46,12 @@
val mk_Trueprop = HOLogic.mk_Trueprop;
fun atomize thm = case Thm.prop_of thm of
- Const ("Trueprop", _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
+ Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
| _ => [thm];
-fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
- | neg_prop ((TP as Const("Trueprop", _)) $ t) = TP $ (HOLogic.Not $t)
+fun neg_prop ((TP as Const(@{const_name "Trueprop"}, _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
+ | neg_prop ((TP as Const(@{const_name "Trueprop"}, _)) $ t) = TP $ (HOLogic.Not $t)
| neg_prop t = raise TERM ("neg_prop", [t]);
fun is_False thm =
@@ -258,10 +258,10 @@
| negate NONE = NONE;
fun decomp_negation data
- ((Const ("Trueprop", _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
+ ((Const (@{const_name "Trueprop"}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
decomp_typecheck data (T, (rel, lhs, rhs))
- | decomp_negation data ((Const ("Trueprop", _)) $
- (Const ("Not", _) $ (Const (rel, T) $ lhs $ rhs))) =
+ | decomp_negation data ((Const (@{const_name "Trueprop"}, _)) $
+ (Const (@{const_name "Not"}, _) $ (Const (rel, T) $ lhs $ rhs))) =
negate (decomp_typecheck data (T, (rel, lhs, rhs)))
| decomp_negation data _ =
NONE;
@@ -273,7 +273,7 @@
in decomp_negation (thy, discrete, inj_consts) end;
fun domain_is_nat (_ $ (Const (_, T) $ _ $ _)) = nT T
- | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
+ | domain_is_nat (_ $ (Const (@{const_name "Not"}, _) $ (Const (_, T) $ _ $ _))) = nT T
| domain_is_nat _ = false;
@@ -428,7 +428,7 @@
val t2' = incr_boundvars 1 t2
val t1_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
- val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_plus_d = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus},
split_type --> split_type --> split_type) $ t2' $ d)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -448,7 +448,7 @@
(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' $
+ val t1_eq_nat_n = Const (@{const_name "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 Orderings.less},
HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
@@ -472,13 +472,13 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =",
+ val t2_eq_zero = Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val t2_neq_zero = HOLogic.mk_not (Const ("op =",
+ val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
val j_lt_t2 = Const (@{const_name Orderings.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' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -504,13 +504,13 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =",
+ val t2_eq_zero = Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val t2_neq_zero = HOLogic.mk_not (Const ("op =",
+ val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
val j_lt_t2 = Const (@{const_name Orderings.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' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -542,7 +542,7 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =",
+ val t2_eq_zero = Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val zero_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
@@ -556,7 +556,7 @@
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t2_lt_j = Const (@{const_name Orderings.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' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -596,7 +596,7 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =",
+ val t2_eq_zero = Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val zero_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
@@ -610,7 +610,7 @@
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t2_lt_j = Const (@{const_name Orderings.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' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -659,7 +659,7 @@
fun negated_term_occurs_positively (terms : term list) : bool =
List.exists
- (fn (Trueprop $ (Const ("Not", _) $ t)) =>
+ (fn (Trueprop $ (Const (@{const_name "Not"}, _) $ t)) =>
member Pattern.aeconv terms (Trueprop $ t)
| _ => false)
terms;