--- a/NEWS Thu Mar 16 20:19:25 2006 +0100
+++ b/NEWS Fri Mar 17 09:34:23 2006 +0100
@@ -346,19 +346,21 @@
25 like -->); output depends on the "iff" print_mode, the default is
"A = B" (with priority 50).
-* Renamed some (legacy-named) constants in HOL.thy:
+* Renamed some (legacy-named) constants in HOL.thy and Orderings.thy:
op + ~> HOL.plus
op - ~> HOL.minus
uminus ~> HOL.uminus
op * ~> HOL.times
+ op < ~> Orderings.less
+ op <= ~> Orderings.less_eq
Adaptions may be required in the following cases:
-a) User-defined constants using any of the names "plus", "minus", or "times"
-The standard syntax translations for "+", "-" and "*" may go wrong.
+a) User-defined constants using any of the names "plus", "minus", "times", "less"
+or "less_eq". The standard syntax translations for "+", "-" and "*" may go wrong.
INCOMPATIBILITY: use more specific names.
-b) Variables named "plus", "minus", or "times"
+b) Variables named "plus", "minus", "times", "less", "less_eq"
INCOMPATIBILITY: use more specific names.
c) Commutative equations theorems (e. g. "a + b = b + a")
--- a/src/HOL/Hoare/hoare.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Hoare/hoare.ML Fri Mar 17 09:34:23 2006 +0100
@@ -65,7 +65,7 @@
fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm
in Collect_const t $ trm end;
-fun inclt ty = Const ("op <=", [ty,ty] ---> boolT);
+fun inclt ty = Const ("Orderings.less_eq", [ty,ty] ---> boolT);
(** Makes "Mset <= t" **)
fun Mset_incl t = let val MsetT = fastype_of t
--- a/src/HOL/Hoare/hoareAbort.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Hoare/hoareAbort.ML Fri Mar 17 09:34:23 2006 +0100
@@ -66,7 +66,7 @@
fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm
in Collect_const t $ trm end;
-fun inclt ty = Const ("op <=", [ty,ty] ---> boolT);
+fun inclt ty = Const ("Orderings.less_eq", [ty,ty] ---> boolT);
(** Makes "Mset <= t" **)
fun Mset_incl t = let val MsetT = fastype_of t
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Mar 17 09:34:23 2006 +0100
@@ -166,7 +166,7 @@
import_theory prim_rec;
const_maps
- "<" > "op <" :: "[nat,nat]=>bool";
+ "<" > "Orderings.less" :: "[nat,nat]=>bool";
end_import;
@@ -181,7 +181,7 @@
">" > HOL4Compat.nat_gt
">=" > HOL4Compat.nat_ge
FUNPOW > HOL4Compat.FUNPOW
- "<=" > "op <=" :: "[nat,nat]=>bool"
+ "<=" > "Orderings.less_eq" :: "[nat,nat]=>bool"
"+" > "HOL.plus" :: "[nat,nat]=>nat"
"*" > "HOL.times" :: "[nat,nat]=>nat"
"-" > "HOL.minus" :: "[nat,nat]=>nat"
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Mar 17 09:34:23 2006 +0100
@@ -23,7 +23,7 @@
inv > HOL.inverse :: "real => real"
real_add > HOL.plus :: "[real,real] => real"
real_mul > HOL.times :: "[real,real] => real"
- real_lt > "op <" :: "[real,real] => bool";
+ real_lt > "Orderings.less" :: "[real,real] => bool";
ignore_thms
real_TY_DEF
@@ -51,7 +51,7 @@
const_maps
real_gt > HOL4Compat.real_gt
real_ge > HOL4Compat.real_ge
- real_lte > "op <=" :: "[real,real] => bool"
+ real_lte > Orderings.less_eq :: "[real,real] => bool"
real_sub > HOL.minus :: "[real,real] => real"
"/" > HOL.divide :: "[real,real] => real"
pow > Nat.power :: "[real,nat] => real"
--- a/src/HOL/Import/HOL/arithmetic.imp Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp Fri Mar 17 09:34:23 2006 +0100
@@ -23,7 +23,7 @@
"ALT_ZERO" > "HOL4Compat.ALT_ZERO"
">=" > "HOL4Compat.nat_ge"
">" > "HOL4Compat.nat_gt"
- "<=" > "op <=" :: "nat => nat => bool"
+ "<=" > "Orderings.less_eq" :: "nat => nat => bool"
"-" > "HOL.minus" :: "nat => nat => nat"
"+" > "HOL.plus" :: "nat => nat => nat"
"*" > "HOL.times" :: "nat => nat => nat"
--- a/src/HOL/Import/HOL/prim_rec.imp Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Import/HOL/prim_rec.imp Fri Mar 17 09:34:23 2006 +0100
@@ -18,7 +18,7 @@
"PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
"PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
"PRE" > "HOL4Base.prim_rec.PRE"
- "<" > "op <" :: "nat => nat => bool"
+ "<" > "Orderings.less" :: "nat => nat => bool"
thm_maps
"wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
--- a/src/HOL/Import/HOL/real.imp Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Import/HOL/real.imp Fri Mar 17 09:34:23 2006 +0100
@@ -12,7 +12,7 @@
"sum" > "HOL4Real.real.sum"
"real_sub" > "HOL.minus" :: "real => real => real"
"real_of_num" > "RealDef.real" :: "nat => real"
- "real_lte" > "op <=" :: "real => real => bool"
+ "real_lte" > "Orderings.less_eq" :: "real => real => bool"
"real_gt" > "HOL4Compat.real_gt"
"real_ge" > "HOL4Compat.real_ge"
"pow" > "Nat.power" :: "real => nat => real"
--- a/src/HOL/Import/HOL/realax.imp Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Import/HOL/realax.imp Fri Mar 17 09:34:23 2006 +0100
@@ -29,7 +29,7 @@
"treal_0" > "HOL4Real.realax.treal_0"
"real_neg" > "HOL.uminus" :: "real => real"
"real_mul" > "HOL.times" :: "real => real => real"
- "real_lt" > "op <" :: "real => real => bool"
+ "real_lt" > "Orderings.less" :: "real => real => bool"
"real_add" > "HOL.plus" :: "real => real => real"
"real_1" > "1" :: "real"
"real_0" > "0" :: "real"
--- a/src/HOL/Integ/IntDef.thy Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy Fri Mar 17 09:34:23 2006 +0100
@@ -891,8 +891,8 @@
"HOL.uminus" :: "int => int" ("~")
"HOL.plus" :: "int => int => int" ("(_ +/ _)")
"HOL.times" :: "int => int => int" ("(_ */ _)")
- "op <" :: "int => int => bool" ("(_ </ _)")
- "op <=" :: "int => int => bool" ("(_ <=/ _)")
+ "Orderings.less" :: "int => int => bool" ("(_ </ _)")
+ "Orderings.less_eq" :: "int => int => bool" ("(_ <=/ _)")
"neg" ("(_ < 0)")
code_syntax_tyco int
--- a/src/HOL/Integ/cooper_dec.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Integ/cooper_dec.ML Fri Mar 17 09:34:23 2006 +0100
@@ -213,12 +213,12 @@
else (warning "Nonlinear term --- Non numeral leftside at dvd"
;raise COOPER)
|linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) )
- |linform vars (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
- |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
- |linform vars (Const("op <=",_)$ s $ t ) =
- (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s))
+ |linform vars (Const("Orderings.less",_)$ s $t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
+ |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
+ |linform vars (Const("Orderings.less_eq",_)$ s $ t ) =
+ (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s))
|linform vars (Const("op >=",_)$ s $ t ) =
- (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT -->
+ (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT -->
HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT -->
HOLogic.intT) $s $(mk_numeral 1)) $ t))
@@ -229,8 +229,8 @@
(* ------------------------------------------------------------------------- *)
fun posineq fm = case fm of
- (Const ("Not",_)$(Const("op <",_)$ c $ t)) =>
- (HOLogic.mk_binrel "op <" (zero , (linear_sub [] (mk_numeral 1) (linear_add [] c t ) )))
+ (Const ("Not",_)$(Const("Orderings.less",_)$ c $ t)) =>
+ (HOLogic.mk_binrel "Orderings.less" (zero , (linear_sub [] (mk_numeral 1) (linear_add [] c t ) )))
| ( Const ("op &",_) $ p $ q) => HOLogic.mk_conj (posineq p,posineq q)
| ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q)
| _ => fm;
@@ -262,7 +262,7 @@
(Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
let val m = l div (dest_numeral c)
- val n = (if p = "op <" then abs(m) else m)
+ val n = (if p = "Orderings.less" then abs(m) else m)
val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x)
in
(HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
@@ -297,7 +297,7 @@
(Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
let val m = l div (dest_numeral c)
- val n = (if p = "op <" then abs(m) else m)
+ val n = (if p = "Orderings.less" then abs(m) else m)
val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
end
@@ -319,7 +319,7 @@
if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
else fm
- |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
+ |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
)) => if (x = y)
then if (pm1 = one) andalso (c = zero) then HOLogic.false_const
else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const
@@ -340,7 +340,7 @@
if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
else fm
- |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
+ |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
)) => if (x = y)
then if (pm1 = one) andalso (c = zero) then HOLogic.true_const
else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
@@ -378,7 +378,7 @@
else bset x p
|(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))] else []
- |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
+ |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
|(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q)
|(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q)
|_ => [];
@@ -398,7 +398,7 @@
else aset x p
|(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a] else []
- |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
+ |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
|(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
|(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
|_ => [];
@@ -450,7 +450,7 @@
val operations =
- [("op =",op=), ("op <",IntInf.<), ("op >",IntInf.>), ("op <=",IntInf.<=) ,
+ [("op =",op=), ("Orderings.less",IntInf.<), ("op >",IntInf.>), ("Orderings.less_eq",IntInf.<=) ,
("op >=",IntInf.>=),
("Divides.op dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))];
--- a/src/HOL/Integ/cooper_proof.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Integ/cooper_proof.ML Fri Mar 17 09:34:23 2006 +0100
@@ -255,20 +255,20 @@
(*==================================================*)
fun decomp_adjustcoeffeq sg x l fm = case fm of
- (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
+ (Const("Not",_)$(Const("Orderings.less",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
let
val m = l div (dest_numeral c)
val n = if (x = y) then abs (m) else 1
val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
val rs = if (x = y)
- then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
- else HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )
+ then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
+ else HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] one rt )
val ck = cterm_of sg (mk_numeral n)
val cc = cterm_of sg c
val ct = cterm_of sg z
val cx = cterm_of sg y
val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral n)))
+ (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral n)))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
@@ -278,7 +278,7 @@
if (is_arith_rel fm) andalso (x = y)
then
let val m = l div (dest_numeral c)
- val k = (if p = "op <" then abs(m) else m)
+ val k = (if p = "Orderings.less" then abs(m) else m)
val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div k)*l) ), x))
val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) ))))
@@ -290,9 +290,9 @@
in
case p of
- "op <" =>
+ "Orderings.less" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
+ (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral k)))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
@@ -344,7 +344,7 @@
then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 = zero) then
if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
(instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
@@ -383,7 +383,7 @@
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
@@ -441,7 +441,7 @@
then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if ((y=x) andalso (c1 = zero)) then
if (pm1 = one)
then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
@@ -482,7 +482,7 @@
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
@@ -571,7 +571,7 @@
if (x=y) andalso (c1=zero) andalso (c2=one)
then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
@@ -581,20 +581,20 @@
then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
end
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = one then
let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
in (instantiate' [] [SOME cfma, SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
end
- else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
+ else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
in (instantiate' [] [SOME cfma, SOME cB,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
@@ -662,7 +662,7 @@
if (x=y) andalso (c1=zero) andalso (c2=one)
then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
@@ -672,19 +672,19 @@
then let val ast_z = norm_zero_one (linear_sub [] one z )
val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = (mk_numeral ~1) then
let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm))
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm))
in (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
end
- else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
+ else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
in (instantiate' [] [SOME cfma, SOME cA,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
@@ -790,7 +790,7 @@
fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm =
(* Get the Bset thm*)
let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm
- val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
+ val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm));
val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm
in (dpos,minf_eqth,nbstpthm,minf_moddth)
end;
@@ -800,7 +800,7 @@
(* ------------------------------------------------------------------------- *)
fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm =
let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm
- val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
+ val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm));
val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm
in (dpos,pinf_eqth,nastpthm,pinf_moddth)
end;
--- a/src/HOL/Integ/int_arith1.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Integ/int_arith1.ML Fri Mar 17 09:34:23 2006 +0100
@@ -348,8 +348,8 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <"
- val dest_bal = HOLogic.dest_bin "op <" Term.dummyT
+ val mk_bal = HOLogic.mk_binrel "Orderings.less"
+ val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
val bal_add1 = less_add_iff1 RS trans
val bal_add2 = less_add_iff2 RS trans
);
@@ -357,8 +357,8 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <="
- val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT
+ val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
+ val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
val bal_add1 = le_add_iff1 RS trans
val bal_add2 = le_add_iff2 RS trans
);
--- a/src/HOL/Integ/int_factor_simprocs.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Integ/int_factor_simprocs.ML Fri Mar 17 09:34:23 2006 +0100
@@ -103,8 +103,8 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <"
- val dest_bal = HOLogic.dest_bin "op <" Term.dummyT
+ val mk_bal = HOLogic.mk_binrel "Orderings.less"
+ val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
val cancel = mult_less_cancel_left RS trans
val neg_exchanges = true
)
@@ -112,8 +112,8 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <="
- val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT
+ val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
+ val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
val cancel = mult_le_cancel_left RS trans
val neg_exchanges = true
)
--- a/src/HOL/Integ/nat_simprocs.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML Fri Mar 17 09:34:23 2006 +0100
@@ -195,8 +195,8 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <"
- val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel "Orderings.less"
+ val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
val bal_add1 = nat_less_add_iff1 RS trans
val bal_add2 = nat_less_add_iff2 RS trans
);
@@ -204,8 +204,8 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <="
- val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
+ val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
val bal_add1 = nat_le_add_iff1 RS trans
val bal_add2 = nat_le_add_iff2 RS trans
);
@@ -315,8 +315,8 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <"
- val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel "Orderings.less"
+ val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
val cancel = nat_mult_less_cancel1 RS trans
val neg_exchanges = true
)
@@ -324,8 +324,8 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <="
- val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
+ val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
val cancel = nat_mult_le_cancel1 RS trans
val neg_exchanges = true
)
@@ -391,16 +391,16 @@
structure LessCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <"
- val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel "Orderings.less"
+ val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_less_cancel_disj
);
structure LeCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <="
- val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel "Orderings.less_eq"
+ val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_le_cancel_disj
);
--- a/src/HOL/Integ/presburger.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Integ/presburger.ML Fri Mar 17 09:34:23 2006 +0100
@@ -133,9 +133,9 @@
("op =", bT --> bT --> bT),
("Not", bT --> bT),
- ("op <=", iT --> iT --> bT),
+ ("Orderings.less_eq", iT --> iT --> bT),
("op =", iT --> iT --> bT),
- ("op <", iT --> iT --> bT),
+ ("Orderings.less", iT --> iT --> bT),
("Divides.op dvd", iT --> iT --> bT),
("Divides.op div", iT --> iT --> iT),
("Divides.op mod", iT --> iT --> iT),
@@ -147,9 +147,9 @@
("HOL.max", iT --> iT --> iT),
("HOL.min", iT --> iT --> iT),
- ("op <=", nT --> nT --> bT),
+ ("Orderings.less_eq", nT --> nT --> bT),
("op =", nT --> nT --> bT),
- ("op <", nT --> nT --> bT),
+ ("Orderings.less", nT --> nT --> bT),
("Divides.op dvd", nT --> nT --> bT),
("Divides.op div", nT --> nT --> nT),
("Divides.op mod", nT --> nT --> nT),
--- a/src/HOL/Integ/reflected_cooper.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Integ/reflected_cooper.ML Fri Mar 17 09:34:23 2006 +0100
@@ -29,8 +29,8 @@
case t of
Const("True",_) => T
| Const("False",_) => F
- | Const("op <",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
- | Const("op <=",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
+ | Const("Orderings.less",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
+ | Const("Orderings.less_eq",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
| Const ("Divides.op dvd",_)$t1$t2 =>
Divides(i_of_term vs t1,i_of_term vs t2)
| Const("op =",eqT)$t1$t2 =>
@@ -89,13 +89,13 @@
case t of
T => HOLogic.true_const
| F => HOLogic.false_const
- | Lt(t1,t2) => Const("op <",[iT,iT] ---> bT)$
+ | Lt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Le(t1,t2) => Const("op <=",[iT,iT] ---> bT)$
+ | Le(t1,t2) => Const("Orderings.less_equal",[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Gt(t1,t2) => Const("op <",[iT,iT] ---> bT)$
+ | Gt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
(term_of_i vs t2)$(term_of_i vs t1)
- | Ge(t1,t2) => Const("op <=",[iT,iT] ---> bT)$
+ | Ge(t1,t2) => Const("Orderings.less_equal",[iT,iT] ---> bT)$
(term_of_i vs t2)$(term_of_i vs t1)
| Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
--- a/src/HOL/Orderings.thy Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Orderings.thy Fri Mar 17 09:34:23 2006 +0100
@@ -18,24 +18,20 @@
ord < type
syntax
- "op <" :: "['a::ord, 'a] => bool" ("op <")
- "op <=" :: "['a::ord, 'a] => bool" ("op <=")
-
-global
+ "less" :: "['a::ord, 'a] => bool" ("op <")
+ "less_eq" :: "['a::ord, 'a] => bool" ("op <=")
consts
- "op <" :: "['a::ord, 'a] => bool" ("(_/ < _)" [50, 51] 50)
- "op <=" :: "['a::ord, 'a] => bool" ("(_/ <= _)" [50, 51] 50)
-
-local
+ "less" :: "['a::ord, 'a] => bool" ("(_/ < _)" [50, 51] 50)
+ "less_eq" :: "['a::ord, 'a] => bool" ("(_/ <= _)" [50, 51] 50)
syntax (xsymbols)
- "op <=" :: "['a::ord, 'a] => bool" ("op \<le>")
- "op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50)
+ "less_eq" :: "['a::ord, 'a] => bool" ("op \<le>")
+ "less_eq" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50)
syntax (HTML output)
- "op <=" :: "['a::ord, 'a] => bool" ("op \<le>")
- "op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50)
+ "less_eq" :: "['a::ord, 'a] => bool" ("op \<le>")
+ "less_eq" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50)
text{* Syntactic sugar: *}
@@ -310,11 +306,11 @@
if of_sort t1
then SOME (t1, "=", t2)
else NONE
- | dec (Const ("op <=", _) $ t1 $ t2) =
+ | dec (Const ("Orderings.less_eq", _) $ t1 $ t2) =
if of_sort t1
then SOME (t1, "<=", t2)
else NONE
- | dec (Const ("op <", _) $ t1 $ t2) =
+ | dec (Const ("Orderings.less", _) $ t1 $ t2) =
if of_sort t1
then SOME (t1, "<", t2)
else NONE
@@ -548,35 +544,35 @@
if v=v' andalso not (v mem (map fst (Term.add_frees n [])))
then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match;
fun all_tr' [Const ("_bound",_) $ Free (v,_),
- Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+ Const("op -->",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
mk v v' "_lessAll" n P
| all_tr' [Const ("_bound",_) $ Free (v,_),
- Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+ Const("op -->",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
mk v v' "_leAll" n P
| all_tr' [Const ("_bound",_) $ Free (v,_),
- Const("op -->",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
+ Const("op -->",_) $ (Const ("Orderings.less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
mk v v' "_gtAll" n P
| all_tr' [Const ("_bound",_) $ Free (v,_),
- Const("op -->",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
+ Const("op -->",_) $ (Const ("Orderings.less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
mk v v' "_geAll" n P;
fun ex_tr' [Const ("_bound",_) $ Free (v,_),
- Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+ Const("op &",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
mk v v' "_lessEx" n P
| ex_tr' [Const ("_bound",_) $ Free (v,_),
- Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+ Const("op &",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
mk v v' "_leEx" n P
| ex_tr' [Const ("_bound",_) $ Free (v,_),
- Const("op &",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
+ Const("op &",_) $ (Const ("Orderings.less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
mk v v' "_gtEx" n P
| ex_tr' [Const ("_bound",_) $ Free (v,_),
- Const("op &",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
+ Const("op &",_) $ (Const ("Orderings.less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
mk v v' "_geEx" n P
in
[("ALL ", all_tr'), ("EX ", ex_tr')]
@@ -703,10 +699,4 @@
leave out the "(xtrans)" above.
*)
-subsection {* Code generator setup *}
-
-code_alias
- "op <=" "Orderings.op_le"
- "op <" "Orderings.op_lt"
-
end
--- a/src/HOL/Real/Float.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Real/Float.ML Fri Mar 17 09:34:23 2006 +0100
@@ -335,12 +335,12 @@
val float_mult_const = Const ("HOL.times", HOLogic.realT --> HOLogic.realT --> HOLogic.realT)
val float_uminus_const = Const ("HOL.uminus", HOLogic.realT --> HOLogic.realT)
val float_abs_const = Const ("HOL.abs", HOLogic.realT --> HOLogic.realT)
-val float_le_const = Const ("op <=", HOLogic.realT --> HOLogic.realT --> HOLogic.boolT)
+val float_le_const = Const ("Orderings.less_eq", HOLogic.realT --> HOLogic.realT --> HOLogic.boolT)
val float_pprt_const = Const ("OrderedGroup.pprt", HOLogic.realT --> HOLogic.realT)
val float_nprt_const = Const ("OrderedGroup.nprt", HOLogic.realT --> HOLogic.realT)
-val nat_le_const = Const ("op <=", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
-val nat_less_const = Const ("op <", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+val nat_le_const = Const ("Orderings.less_eq", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+val nat_less_const = Const ("Orderings.less", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
val nat_eq_const = Const ("op =", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
val zero = FloatArith.izero
--- a/src/HOL/Set.thy Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Set.thy Fri Mar 17 09:34:23 2006 +0100
@@ -168,7 +168,7 @@
fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
list_comb (Syntax.const "_setless", ts)
| less_tr' _ _ _ = raise Match;
- in [("op <=", le_tr'), ("op <", less_tr')] end
+ in [("Orderings.less_eq", le_tr'), ("Orderings.less", less_tr')] end
*}
@@ -208,26 +208,26 @@
let
fun
all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)),
- Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+ Const("op -->",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
(if v=v' andalso T="set"
then Syntax.const "_setlessAll" $ Syntax.mark_bound v' $ n $ P
else raise Match)
| all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)),
- Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+ Const("op -->",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
(if v=v' andalso T="set"
then Syntax.const "_setleAll" $ Syntax.mark_bound v' $ n $ P
else raise Match);
fun
ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)),
- Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+ Const("op &",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
(if v=v' andalso T="set"
then Syntax.const "_setlessEx" $ Syntax.mark_bound v' $ n $ P
else raise Match)
| ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)),
- Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
+ Const("op &",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
(if v=v' andalso T="set"
then Syntax.const "_setleEx" $ Syntax.mark_bound v' $ n $ P
else raise Match)
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Fri Mar 17 09:34:23 2006 +0100
@@ -213,12 +213,12 @@
else (warning "Nonlinear term --- Non numeral leftside at dvd"
;raise COOPER)
|linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) )
- |linform vars (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
- |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
- |linform vars (Const("op <=",_)$ s $ t ) =
- (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s))
+ |linform vars (Const("Orderings.less",_)$ s $t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
+ |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t))
+ |linform vars (Const("Orderings.less_eq",_)$ s $ t ) =
+ (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s))
|linform vars (Const("op >=",_)$ s $ t ) =
- (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT -->
+ (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT -->
HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT -->
HOLogic.intT) $s $(mk_numeral 1)) $ t))
@@ -229,8 +229,8 @@
(* ------------------------------------------------------------------------- *)
fun posineq fm = case fm of
- (Const ("Not",_)$(Const("op <",_)$ c $ t)) =>
- (HOLogic.mk_binrel "op <" (zero , (linear_sub [] (mk_numeral 1) (linear_add [] c t ) )))
+ (Const ("Not",_)$(Const("Orderings.less",_)$ c $ t)) =>
+ (HOLogic.mk_binrel "Orderings.less" (zero , (linear_sub [] (mk_numeral 1) (linear_add [] c t ) )))
| ( Const ("op &",_) $ p $ q) => HOLogic.mk_conj (posineq p,posineq q)
| ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q)
| _ => fm;
@@ -262,7 +262,7 @@
(Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
let val m = l div (dest_numeral c)
- val n = (if p = "op <" then abs(m) else m)
+ val n = (if p = "Orderings.less" then abs(m) else m)
val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x)
in
(HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
@@ -297,7 +297,7 @@
(Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $
c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
let val m = l div (dest_numeral c)
- val n = (if p = "op <" then abs(m) else m)
+ val n = (if p = "Orderings.less" then abs(m) else m)
val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
end
@@ -319,7 +319,7 @@
if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
else fm
- |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
+ |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
)) => if (x = y)
then if (pm1 = one) andalso (c = zero) then HOLogic.false_const
else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const
@@ -340,7 +340,7 @@
if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const
else fm
- |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
+ |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z
)) => if (x = y)
then if (pm1 = one) andalso (c = zero) then HOLogic.true_const
else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
@@ -378,7 +378,7 @@
else bset x p
|(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))] else []
- |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
+ |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else []
|(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q)
|(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q)
|_ => [];
@@ -398,7 +398,7 @@
else aset x p
|(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a] else []
- |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
+ |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else []
|(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q)
|(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q)
|_ => [];
@@ -450,7 +450,7 @@
val operations =
- [("op =",op=), ("op <",IntInf.<), ("op >",IntInf.>), ("op <=",IntInf.<=) ,
+ [("op =",op=), ("Orderings.less",IntInf.<), ("op >",IntInf.>), ("Orderings.less_eq",IntInf.<=) ,
("op >=",IntInf.>=),
("Divides.op dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))];
--- a/src/HOL/Tools/Presburger/cooper_proof.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML Fri Mar 17 09:34:23 2006 +0100
@@ -255,20 +255,20 @@
(*==================================================*)
fun decomp_adjustcoeffeq sg x l fm = case fm of
- (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
+ (Const("Not",_)$(Const("Orderings.less",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) =>
let
val m = l div (dest_numeral c)
val n = if (x = y) then abs (m) else 1
val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x))
val rs = if (x = y)
- then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
- else HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )
+ then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) ))))
+ else HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] one rt )
val ck = cterm_of sg (mk_numeral n)
val cc = cterm_of sg c
val ct = cterm_of sg z
val cx = cterm_of sg y
val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral n)))
+ (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral n)))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
@@ -278,7 +278,7 @@
if (is_arith_rel fm) andalso (x = y)
then
let val m = l div (dest_numeral c)
- val k = (if p = "op <" then abs(m) else m)
+ val k = (if p = "Orderings.less" then abs(m) else m)
val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div k)*l) ), x))
val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) ))))
@@ -290,9 +290,9 @@
in
case p of
- "op <" =>
+ "Orderings.less" =>
let val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
+ (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral k)))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
@@ -344,7 +344,7 @@
then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 = zero) then
if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
(instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
@@ -383,7 +383,7 @@
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
@@ -441,7 +441,7 @@
then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if ((y=x) andalso (c1 = zero)) then
if (pm1 = one)
then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
@@ -482,7 +482,7 @@
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
@@ -571,7 +571,7 @@
if (x=y) andalso (c1=zero) andalso (c2=one)
then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
@@ -581,20 +581,20 @@
then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1)))
in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
end
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = one then
let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
in (instantiate' [] [SOME cfma, SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
end
- else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
+ else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
in (instantiate' [] [SOME cfma, SOME cB,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
@@ -662,7 +662,7 @@
if (x=y) andalso (c1=zero) andalso (c2=one)
then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
@@ -672,19 +672,19 @@
then let val ast_z = norm_zero_one (linear_sub [] one z )
val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
- val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
+ val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |(Const("op <",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
+ |(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) =>
if (y=x) andalso (c1 =zero) then
if pm1 = (mk_numeral ~1) then
let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
- val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm))
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm))
in (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
end
- else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
+ else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm))
in (instantiate' [] [SOME cfma, SOME cA,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
@@ -790,7 +790,7 @@
fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm =
(* Get the Bset thm*)
let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm
- val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
+ val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm));
val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm
in (dpos,minf_eqth,nbstpthm,minf_moddth)
end;
@@ -800,7 +800,7 @@
(* ------------------------------------------------------------------------- *)
fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm =
let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm
- val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
+ val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm));
val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm
in (dpos,pinf_eqth,nastpthm,pinf_moddth)
end;
--- a/src/HOL/Tools/Presburger/presburger.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML Fri Mar 17 09:34:23 2006 +0100
@@ -133,9 +133,9 @@
("op =", bT --> bT --> bT),
("Not", bT --> bT),
- ("op <=", iT --> iT --> bT),
+ ("Orderings.less_eq", iT --> iT --> bT),
("op =", iT --> iT --> bT),
- ("op <", iT --> iT --> bT),
+ ("Orderings.less", iT --> iT --> bT),
("Divides.op dvd", iT --> iT --> bT),
("Divides.op div", iT --> iT --> iT),
("Divides.op mod", iT --> iT --> iT),
@@ -147,9 +147,9 @@
("HOL.max", iT --> iT --> iT),
("HOL.min", iT --> iT --> iT),
- ("op <=", nT --> nT --> bT),
+ ("Orderings.less_eq", nT --> nT --> bT),
("op =", nT --> nT --> bT),
- ("op <", nT --> nT --> bT),
+ ("Orderings.less", nT --> nT --> bT),
("Divides.op dvd", nT --> nT --> bT),
("Divides.op div", nT --> nT --> nT),
("Divides.op mod", nT --> nT --> nT),
--- a/src/HOL/Tools/Presburger/reflected_cooper.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML Fri Mar 17 09:34:23 2006 +0100
@@ -29,8 +29,8 @@
case t of
Const("True",_) => T
| Const("False",_) => F
- | Const("op <",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
- | Const("op <=",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
+ | Const("Orderings.less",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
+ | Const("Orderings.less_eq",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
| Const ("Divides.op dvd",_)$t1$t2 =>
Divides(i_of_term vs t1,i_of_term vs t2)
| Const("op =",eqT)$t1$t2 =>
@@ -89,13 +89,13 @@
case t of
T => HOLogic.true_const
| F => HOLogic.false_const
- | Lt(t1,t2) => Const("op <",[iT,iT] ---> bT)$
+ | Lt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Le(t1,t2) => Const("op <=",[iT,iT] ---> bT)$
+ | Le(t1,t2) => Const("Orderings.less_equal",[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Gt(t1,t2) => Const("op <",[iT,iT] ---> bT)$
+ | Gt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
(term_of_i vs t2)$(term_of_i vs t1)
- | Ge(t1,t2) => Const("op <=",[iT,iT] ---> bT)$
+ | Ge(t1,t2) => Const("Orderings.less_equal",[iT,iT] ---> bT)$
(term_of_i vs t2)$(term_of_i vs t1)
| Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
--- a/src/HOL/Tools/refute.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Tools/refute.ML Fri Mar 17 09:34:23 2006 +0100
@@ -621,7 +621,7 @@
(* other optimizations *)
| Const ("Finite_Set.card", T) => collect_type_axioms (axs, T)
| Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
- | Const ("op <", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms (axs, T)
+ | Const ("Orderings.less", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms (axs, T)
| Const ("HOL.plus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
| Const ("HOL.minus", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
| Const ("HOL.times", T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T)
@@ -2146,7 +2146,7 @@
fun Nat_less_interpreter thy model args t =
case t of
- Const ("op <", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
+ Const ("Orderings.less", Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
let
val (i_nat, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", Type ("nat", [])))
val size_nat = size_of_type i_nat
--- a/src/HOL/Tools/res_clause.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML Fri Mar 17 09:34:23 2006 +0100
@@ -90,8 +90,8 @@
(*Provide readable names for the more common symbolic functions*)
val const_trans_table =
Symtab.make [("op =", "equal"),
- ("op <=", "lessequals"),
- ("op <", "less"),
+ ("Orderings.less_eq", "lessequals"),
+ ("Orderings.less", "less"),
("op &", "and"),
("op |", "or"),
("HOL.plus", "plus"),
--- a/src/HOL/antisym_setup.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/antisym_setup.ML Fri Mar 17 09:34:23 2006 +0100
@@ -12,7 +12,7 @@
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
let val prems = prems_of_ss ss;
- val less = Const("op <",T);
+ val less = Const("Orderings.less",T);
val t = HOLogic.mk_Trueprop(le $ s $ r);
in case Library.find_first (prp t) prems of
NONE =>
@@ -27,7 +27,7 @@
fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
let val prems = prems_of_ss ss;
- val le = Const("op <=",T);
+ val le = Const("Orderings.less_eq",T);
val t = HOLogic.mk_Trueprop(le $ r $ s);
in case Library.find_first (prp t) prems of
NONE =>
--- a/src/HOL/arith_data.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/arith_data.ML Fri Mar 17 09:34:23 2006 +0100
@@ -115,8 +115,8 @@
structure LessCancelSums = CancelSumsFun
(struct
open Sum;
- val mk_bal = HOLogic.mk_binrel "op <";
- val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
+ val mk_bal = HOLogic.mk_binrel "Orderings.less";
+ val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT;
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_less;
end);
@@ -126,8 +126,8 @@
structure LeCancelSums = CancelSumsFun
(struct
open Sum;
- val mk_bal = HOLogic.mk_binrel "op <=";
- val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
+ val mk_bal = HOLogic.mk_binrel "Orderings.less_eq";
+ val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT;
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_le;
end);
@@ -330,8 +330,8 @@
and (q,j) = poly(rhs,Rat.rat_of_int 1,([],Rat.rat_of_int 0))
in case rel of
- "op <" => SOME(p,i,"<",q,j)
- | "op <=" => SOME(p,i,"<=",q,j)
+ "Orderings.less" => SOME(p,i,"<",q,j)
+ | "Orderings.less_eq" => SOME(p,i,"<=",q,j)
| "op =" => SOME(p,i,"=",q,j)
| _ => NONE
end handle Zero => NONE;
@@ -544,24 +544,24 @@
val r = #prop(rep_thm thm);
in
case r of
- Tr $ ((c as Const("op <=",T)) $ s $ t) =>
+ Tr $ ((c as Const("Orderings.less_eq",T)) $ s $ t) =>
let val r' = Tr $ (c $ t $ s)
in
case Library.find_first (prp r') prems of
NONE =>
- let val r' = Tr $ (HOLogic.Not $ (Const("op <",T) $ s $ t))
+ let val r' = Tr $ (HOLogic.Not $ (Const("Orderings.less",T) $ s $ t))
in case Library.find_first (prp r') prems of
NONE => []
| SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)]
end
| SOME thm' => [thm' RS (thm RS antisym)]
end
- | Tr $ (Const("Not",_) $ (Const("op <",T) $ s $ t)) =>
- let val r' = Tr $ (Const("op <=",T) $ s $ t)
+ | Tr $ (Const("Not",_) $ (Const("Orderings.less",T) $ s $ t)) =>
+ let val r' = Tr $ (Const("Orderings.less_eq",T) $ s $ t)
in
case Library.find_first (prp r') prems of
NONE =>
- let val r' = Tr $ (HOLogic.Not $ (Const("op <",T) $ t $ s))
+ let val r' = Tr $ (HOLogic.Not $ (Const("Orderings.less",T) $ t $ s))
in case Library.find_first (prp r') prems of
NONE => []
| SOME thm' =>
--- a/src/HOL/ex/SVC_Oracle.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/ex/SVC_Oracle.ML Fri Mar 17 09:34:23 2006 +0100
@@ -78,8 +78,8 @@
| fm ((c as Const("True", _))) = c
| fm ((c as Const("False", _))) = c
| fm (t as Const("op =", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
- | fm (t as Const("op <", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
- | fm (t as Const("op <=", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const("Orderings.less", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const("Orderings.less_eq", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm t = replace t
(*entry point, and abstraction of a meta-formula*)
fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
--- a/src/HOL/ex/mesontest2.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/ex/mesontest2.ML Fri Mar 17 09:34:23 2006 +0100
@@ -985,19 +985,19 @@
meson_tac 1);
val HEN002_0_ax =
- "(\\<forall>X Y. less_equal(X::'a,Y) --> equal(Divide(X::'a,Y),zero)) & \
-\ (\\<forall>X Y. equal(Divide(X::'a,Y),zero) --> less_equal(X::'a,Y)) & \
-\ (\\<forall>Y X. less_equal(Divide(X::'a,Y),X)) & \
-\ (\\<forall>X Y Z. less_equal(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z))) & \
-\ (\\<forall>X. less_equal(zero::'a,X)) & \
-\ (\\<forall>X Y. less_equal(X::'a,Y) & less_equal(Y::'a,X) --> equal(X::'a,Y)) & \
-\ (\\<forall>X. less_equal(X::'a,identity))";
+ "(\\<forall>X Y. mless_equal(X::'a,Y) --> equal(Divide(X::'a,Y),zero)) & \
+\ (\\<forall>X Y. equal(Divide(X::'a,Y),zero) --> mless_equal(X::'a,Y)) & \
+\ (\\<forall>Y X. mless_equal(Divide(X::'a,Y),X)) & \
+\ (\\<forall>X Y Z. mless_equal(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z))) & \
+\ (\\<forall>X. mless_equal(zero::'a,X)) & \
+\ (\\<forall>X Y. mless_equal(X::'a,Y) & mless_equal(Y::'a,X) --> equal(X::'a,Y)) & \
+\ (\\<forall>X. mless_equal(X::'a,identity))";
val HEN002_0_eq =
"(\\<forall>A B C. equal(A::'a,B) --> equal(Divide(A::'a,C),Divide(B::'a,C))) & \
\ (\\<forall>D F' E. equal(D::'a,E) --> equal(Divide(F'::'a,D),Divide(F'::'a,E))) & \
-\ (\\<forall>G H I'. equal(G::'a,H) & less_equal(G::'a,I') --> less_equal(H::'a,I')) & \
-\ (\\<forall>J L K'. equal(J::'a,K') & less_equal(L::'a,J) --> less_equal(L::'a,K'))";
+\ (\\<forall>G H I'. equal(G::'a,H) & mless_equal(G::'a,I') --> mless_equal(H::'a,I')) & \
+\ (\\<forall>J L K'. equal(J::'a,K') & mless_equal(L::'a,J) --> mless_equal(L::'a,K'))";
(*250258 inferences so far. Searching to depth 16. 406.2 secs*)
val HEN003_3 = prove_hard
@@ -1009,32 +1009,32 @@
(*202177 inferences so far. Searching to depth 14. 451 secs*)
val HEN007_2 = prove_hard
(EQU001_0_ax ^ " & \
-\ (\\<forall>X Y. less_equal(X::'a,Y) --> quotient(X::'a,Y,zero)) & \
-\ (\\<forall>X Y. quotient(X::'a,Y,zero) --> less_equal(X::'a,Y)) & \
-\ (\\<forall>Y Z X. quotient(X::'a,Y,Z) --> less_equal(Z::'a,X)) & \
-\ (\\<forall>Y X V3 V2 V1 Z V4 V5. quotient(X::'a,Y,V1) & quotient(Y::'a,Z,V2) & quotient(X::'a,Z,V3) & quotient(V3::'a,V2,V4) & quotient(V1::'a,Z,V5) --> less_equal(V4::'a,V5)) & \
-\ (\\<forall>X. less_equal(zero::'a,X)) & \
-\ (\\<forall>X Y. less_equal(X::'a,Y) & less_equal(Y::'a,X) --> equal(X::'a,Y)) & \
-\ (\\<forall>X. less_equal(X::'a,identity)) & \
+\ (\\<forall>X Y. mless_equal(X::'a,Y) --> quotient(X::'a,Y,zero)) & \
+\ (\\<forall>X Y. quotient(X::'a,Y,zero) --> mless_equal(X::'a,Y)) & \
+\ (\\<forall>Y Z X. quotient(X::'a,Y,Z) --> mless_equal(Z::'a,X)) & \
+\ (\\<forall>Y X V3 V2 V1 Z V4 V5. quotient(X::'a,Y,V1) & quotient(Y::'a,Z,V2) & quotient(X::'a,Z,V3) & quotient(V3::'a,V2,V4) & quotient(V1::'a,Z,V5) --> mless_equal(V4::'a,V5)) & \
+\ (\\<forall>X. mless_equal(zero::'a,X)) & \
+\ (\\<forall>X Y. mless_equal(X::'a,Y) & mless_equal(Y::'a,X) --> equal(X::'a,Y)) & \
+\ (\\<forall>X. mless_equal(X::'a,identity)) & \
\ (\\<forall>X Y. quotient(X::'a,Y,Divide(X::'a,Y))) & \
\ (\\<forall>X Y Z W. quotient(X::'a,Y,Z) & quotient(X::'a,Y,W) --> equal(Z::'a,W)) & \
\ (\\<forall>X Y W Z. equal(X::'a,Y) & quotient(X::'a,W,Z) --> quotient(Y::'a,W,Z)) & \
\ (\\<forall>X W Y Z. equal(X::'a,Y) & quotient(W::'a,X,Z) --> quotient(W::'a,Y,Z)) & \
\ (\\<forall>X W Z Y. equal(X::'a,Y) & quotient(W::'a,Z,X) --> quotient(W::'a,Z,Y)) & \
-\ (\\<forall>X Z Y. equal(X::'a,Y) & less_equal(Z::'a,X) --> less_equal(Z::'a,Y)) & \
-\ (\\<forall>X Y Z. equal(X::'a,Y) & less_equal(X::'a,Z) --> less_equal(Y::'a,Z)) & \
+\ (\\<forall>X Z Y. equal(X::'a,Y) & mless_equal(Z::'a,X) --> mless_equal(Z::'a,Y)) & \
+\ (\\<forall>X Y Z. equal(X::'a,Y) & mless_equal(X::'a,Z) --> mless_equal(Y::'a,Z)) & \
\ (\\<forall>X Y W. equal(X::'a,Y) --> equal(Divide(X::'a,W),Divide(Y::'a,W))) & \
\ (\\<forall>X W Y. equal(X::'a,Y) --> equal(Divide(W::'a,X),Divide(W::'a,Y))) & \
\ (\\<forall>X. quotient(X::'a,identity,zero)) & \
\ (\\<forall>X. quotient(zero::'a,X,zero)) & \
\ (\\<forall>X. quotient(X::'a,X,zero)) & \
\ (\\<forall>X. quotient(X::'a,zero,X)) & \
-\ (\\<forall>Y X Z. less_equal(X::'a,Y) & less_equal(Y::'a,Z) --> less_equal(X::'a,Z)) & \
-\ (\\<forall>W1 X Z W2 Y. quotient(X::'a,Y,W1) & less_equal(W1::'a,Z) & quotient(X::'a,Z,W2) --> less_equal(W2::'a,Y)) & \
-\ (less_equal(x::'a,y)) & \
+\ (\\<forall>Y X Z. mless_equal(X::'a,Y) & mless_equal(Y::'a,Z) --> mless_equal(X::'a,Z)) & \
+\ (\\<forall>W1 X Z W2 Y. quotient(X::'a,Y,W1) & mless_equal(W1::'a,Z) & quotient(X::'a,Z,W2) --> mless_equal(W2::'a,Y)) & \
+\ (mless_equal(x::'a,y)) & \
\ (quotient(z::'a,y,zQy)) & \
\ (quotient(z::'a,x,zQx)) & \
-\ (~less_equal(zQy::'a,zQx)) --> False",
+\ (~mless_equal(zQy::'a,zQx)) --> False",
meson_tac 1);
(*60026 inferences so far. Searching to depth 12. 42.2 secs*)
@@ -1044,11 +1044,11 @@
\ (\\<forall>X. equal(Divide(zero::'a,X),zero)) & \
\ (\\<forall>X. equal(Divide(X::'a,X),zero)) & \
\ (equal(Divide(a::'a,zero),a)) & \
-\ (\\<forall>Y X Z. less_equal(X::'a,Y) & less_equal(Y::'a,Z) --> less_equal(X::'a,Z)) & \
-\ (\\<forall>X Z Y. less_equal(Divide(X::'a,Y),Z) --> less_equal(Divide(X::'a,Z),Y)) & \
-\ (\\<forall>Y Z X. less_equal(X::'a,Y) --> less_equal(Divide(Z::'a,Y),Divide(Z::'a,X))) & \
-\ (less_equal(a::'a,b)) & \
-\ (~less_equal(Divide(a::'a,c),Divide(b::'a,c))) --> False",
+\ (\\<forall>Y X Z. mless_equal(X::'a,Y) & mless_equal(Y::'a,Z) --> mless_equal(X::'a,Z)) & \
+\ (\\<forall>X Z Y. mless_equal(Divide(X::'a,Y),Z) --> mless_equal(Divide(X::'a,Z),Y)) & \
+\ (\\<forall>Y Z X. mless_equal(X::'a,Y) --> mless_equal(Divide(Z::'a,Y),Divide(Z::'a,X))) & \
+\ (mless_equal(a::'a,b)) & \
+\ (~mless_equal(Divide(a::'a,c),Divide(b::'a,c))) --> False",
meson_tac 1);
@@ -1075,7 +1075,7 @@
(*970373 inferences so far. Searching to depth 17. 890.0 secs*)
val HEN012_3 = prove_hard
(EQU001_0_ax ^ "&" ^ HEN002_0_ax ^ "&" ^ HEN002_0_eq ^ " & \
-\ (~less_equal(a::'a,a)) --> False",
+\ (~mless_equal(a::'a,a)) --> False",
meson_tac 1);
@@ -1292,20 +1292,20 @@
\ (\\<forall>A B. equal(A::'a,B) --> equal(successor(A),successor(B)))";
val NUM001_1_ax =
- "(\\<forall>A C B. less(A::'a,B) & less(C::'a,A) --> less(C::'a,B)) & \
-\ (\\<forall>A B C. equal(add(successor(A),B),C) --> less(B::'a,C)) & \
-\ (\\<forall>A B. less(A::'a,B) --> equal(add(successor(predecessor_of_1st_minus_2nd(B::'a,A)),A),B))";
+ "(\\<forall>A C B. mless(A::'a,B) & mless(C::'a,A) --> mless(C::'a,B)) & \
+\ (\\<forall>A B C. equal(add(successor(A),B),C) --> mless(B::'a,C)) & \
+\ (\\<forall>A B. mless(A::'a,B) --> equal(add(successor(predecessor_of_1st_minus_2nd(B::'a,A)),A),B))";
val NUM001_2_ax =
- "(\\<forall>A B. divides(A::'a,B) --> less(A::'a,B) | equal(A::'a,B)) & \
-\ (\\<forall>A B. less(A::'a,B) --> divides(A::'a,B)) & \
+ "(\\<forall>A B. divides(A::'a,B) --> mless(A::'a,B) | equal(A::'a,B)) & \
+\ (\\<forall>A B. mless(A::'a,B) --> divides(A::'a,B)) & \
\ (\\<forall>A B. equal(A::'a,B) --> divides(A::'a,B))";
(*20717 inferences so far. Searching to depth 11. 13.7 secs*)
val NUM021_1 = prove
(EQU001_0_ax ^ "&" ^ NUM001_0_ax ^ "&" ^ NUM001_1_ax ^ "&" ^ NUM001_2_ax ^
- "& (less(b::'a,c)) & \
-\ (~less(b::'a,a)) & \
+ "& (mless(b::'a,c)) & \
+\ (~mless(b::'a,a)) & \
\ (divides(c::'a,a)) & \
\ (\\<forall>A. ~equal(successor(A),num0)) --> False",
meson_tac 1);
@@ -1315,7 +1315,7 @@
(EQU001_0_ax ^ "&" ^ NUM001_0_ax ^ "&" ^ NUM001_1_ax ^ " & \
\ (\\<forall>B A. equal(add(A::'a,B),add(B::'a,A))) & \
\ (\\<forall>B A C. equal(add(A::'a,B),add(C::'a,B)) --> equal(A::'a,C)) & \
-\ (less(a::'a,a)) & \
+\ (mless(a::'a,a)) & \
\ (\\<forall>A. ~equal(successor(A),num0)) --> False",
meson_tac 1);
@@ -1690,20 +1690,20 @@
(*948 inferences so far. Searching to depth 18. 1.1 secs*)
val PRV001_1 = prove
- ("(\\<forall>X Y Z. q1(X::'a,Y,Z) & less_or_equal(X::'a,Y) --> q2(X::'a,Y,Z)) & \
-\ (\\<forall>X Y Z. q1(X::'a,Y,Z) --> less_or_equal(X::'a,Y) | q3(X::'a,Y,Z)) & \
+ ("(\\<forall>X Y Z. q1(X::'a,Y,Z) & mless_or_equal(X::'a,Y) --> q2(X::'a,Y,Z)) & \
+\ (\\<forall>X Y Z. q1(X::'a,Y,Z) --> mless_or_equal(X::'a,Y) | q3(X::'a,Y,Z)) & \
\ (\\<forall>Z X Y. q2(X::'a,Y,Z) --> q4(X::'a,Y,Y)) & \
\ (\\<forall>Z Y X. q3(X::'a,Y,Z) --> q4(X::'a,Y,X)) & \
-\ (\\<forall>X. less_or_equal(X::'a,X)) & \
-\ (\\<forall>X Y. less_or_equal(X::'a,Y) & less_or_equal(Y::'a,X) --> equal(X::'a,Y)) & \
-\ (\\<forall>Y X Z. less_or_equal(X::'a,Y) & less_or_equal(Y::'a,Z) --> less_or_equal(X::'a,Z)) & \
-\ (\\<forall>Y X. less_or_equal(X::'a,Y) | less_or_equal(Y::'a,X)) & \
-\ (\\<forall>X Y. equal(X::'a,Y) --> less_or_equal(X::'a,Y)) & \
-\ (\\<forall>X Y Z. equal(X::'a,Y) & less_or_equal(X::'a,Z) --> less_or_equal(Y::'a,Z)) & \
-\ (\\<forall>X Z Y. equal(X::'a,Y) & less_or_equal(Z::'a,X) --> less_or_equal(Z::'a,Y)) & \
+\ (\\<forall>X. mless_or_equal(X::'a,X)) & \
+\ (\\<forall>X Y. mless_or_equal(X::'a,Y) & mless_or_equal(Y::'a,X) --> equal(X::'a,Y)) & \
+\ (\\<forall>Y X Z. mless_or_equal(X::'a,Y) & mless_or_equal(Y::'a,Z) --> mless_or_equal(X::'a,Z)) & \
+\ (\\<forall>Y X. mless_or_equal(X::'a,Y) | mless_or_equal(Y::'a,X)) & \
+\ (\\<forall>X Y. equal(X::'a,Y) --> mless_or_equal(X::'a,Y)) & \
+\ (\\<forall>X Y Z. equal(X::'a,Y) & mless_or_equal(X::'a,Z) --> mless_or_equal(Y::'a,Z)) & \
+\ (\\<forall>X Z Y. equal(X::'a,Y) & mless_or_equal(Z::'a,X) --> mless_or_equal(Z::'a,Y)) & \
\ (q1(a::'a,b,c)) & \
-\ (\\<forall>W. ~(q4(a::'a,b,W) & less_or_equal(a::'a,W) & less_or_equal(b::'a,W) & less_or_equal(W::'a,a))) & \
-\ (\\<forall>W. ~(q4(a::'a,b,W) & less_or_equal(a::'a,W) & less_or_equal(b::'a,W) & less_or_equal(W::'a,b))) --> False",
+\ (\\<forall>W. ~(q4(a::'a,b,W) & mless_or_equal(a::'a,W) & mless_or_equal(b::'a,W) & mless_or_equal(W::'a,a))) & \
+\ (\\<forall>W. ~(q4(a::'a,b,W) & mless_or_equal(a::'a,W) & mless_or_equal(b::'a,W) & mless_or_equal(W::'a,b))) --> False",
meson_tac 1);
(*PRV is now called SWV (software verification) *)
@@ -1712,14 +1712,14 @@
\ (\\<forall>X. equal(successor(predecessor(X)),X)) & \
\ (\\<forall>X Y. equal(predecessor(X),predecessor(Y)) --> equal(X::'a,Y)) & \
\ (\\<forall>X Y. equal(successor(X),successor(Y)) --> equal(X::'a,Y)) & \
-\ (\\<forall>X. LESS_THAN(predecessor(X),X)) & \
-\ (\\<forall>X. LESS_THAN(X::'a,successor(X))) & \
-\ (\\<forall>X Y Z. LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,Z) --> LESS_THAN(X::'a,Z)) & \
-\ (\\<forall>X Y. LESS_THAN(X::'a,Y) | LESS_THAN(Y::'a,X) | equal(X::'a,Y)) & \
-\ (\\<forall>X. ~LESS_THAN(X::'a,X)) & \
-\ (\\<forall>Y X. ~(LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,X))) & \
-\ (\\<forall>Y X Z. equal(X::'a,Y) & LESS_THAN(X::'a,Z) --> LESS_THAN(Y::'a,Z)) & \
-\ (\\<forall>Y Z X. equal(X::'a,Y) & LESS_THAN(Z::'a,X) --> LESS_THAN(Z::'a,Y))";
+\ (\\<forall>X. mless_THAN(predecessor(X),X)) & \
+\ (\\<forall>X. mless_THAN(X::'a,successor(X))) & \
+\ (\\<forall>X Y Z. mless_THAN(X::'a,Y) & mless_THAN(Y::'a,Z) --> mless_THAN(X::'a,Z)) & \
+\ (\\<forall>X Y. mless_THAN(X::'a,Y) | mless_THAN(Y::'a,X) | equal(X::'a,Y)) & \
+\ (\\<forall>X. ~mless_THAN(X::'a,X)) & \
+\ (\\<forall>Y X. ~(mless_THAN(X::'a,Y) & mless_THAN(Y::'a,X))) & \
+\ (\\<forall>Y X Z. equal(X::'a,Y) & mless_THAN(X::'a,Z) --> mless_THAN(Y::'a,Z)) & \
+\ (\\<forall>Y Z X. equal(X::'a,Y) & mless_THAN(Z::'a,X) --> mless_THAN(Z::'a,Y))";
val SWV001_0_eq =
"(\\<forall>X Y. equal(X::'a,Y) --> equal(predecessor(X),predecessor(Y))) & \
@@ -1729,55 +1729,55 @@
(*21 inferences so far. Searching to depth 5. 0.4 secs*)
val PRV003_1 = prove
(EQU001_0_ax ^ "&" ^ SWV001_1_ax ^ "&" ^ SWV001_0_eq ^ " & \
-\ (~LESS_THAN(n::'a,j)) & \
-\ (LESS_THAN(k::'a,j)) & \
-\ (~LESS_THAN(k::'a,i)) & \
-\ (LESS_THAN(i::'a,n)) & \
-\ (LESS_THAN(a(j),a(k))) & \
-\ (\\<forall>X. LESS_THAN(X::'a,j) & LESS_THAN(a(X),a(k)) --> LESS_THAN(X::'a,i)) & \
-\ (\\<forall>X. LESS_THAN(one::'a,i) & LESS_THAN(a(X),a(predecessor(i))) --> LESS_THAN(X::'a,i) | LESS_THAN(n::'a,X)) & \
-\ (\\<forall>X. ~(LESS_THAN(one::'a,X) & LESS_THAN(X::'a,i) & LESS_THAN(a(X),a(predecessor(X))))) & \
-\ (LESS_THAN(j::'a,i)) --> False",
+\ (~mless_THAN(n::'a,j)) & \
+\ (mless_THAN(k::'a,j)) & \
+\ (~mless_THAN(k::'a,i)) & \
+\ (mless_THAN(i::'a,n)) & \
+\ (mless_THAN(a(j),a(k))) & \
+\ (\\<forall>X. mless_THAN(X::'a,j) & mless_THAN(a(X),a(k)) --> mless_THAN(X::'a,i)) & \
+\ (\\<forall>X. mless_THAN(one::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) & \
+\ (\\<forall>X. ~(mless_THAN(one::'a,X) & mless_THAN(X::'a,i) & mless_THAN(a(X),a(predecessor(X))))) & \
+\ (mless_THAN(j::'a,i)) --> False",
meson_tac 1);
(*584 inferences so far. Searching to depth 7. 1.1 secs*)
val PRV005_1 = prove
(EQU001_0_ax ^ "&" ^ SWV001_1_ax ^ "&" ^ SWV001_0_eq ^ " & \
-\ (~LESS_THAN(n::'a,k)) & \
-\ (~LESS_THAN(k::'a,l)) & \
-\ (~LESS_THAN(k::'a,i)) & \
-\ (LESS_THAN(l::'a,n)) & \
-\ (LESS_THAN(one::'a,l)) & \
-\ (LESS_THAN(a(k),a(predecessor(l)))) & \
-\ (\\<forall>X. LESS_THAN(X::'a,successor(n)) & LESS_THAN(a(X),a(k)) --> LESS_THAN(X::'a,l)) & \
-\ (\\<forall>X. LESS_THAN(one::'a,l) & LESS_THAN(a(X),a(predecessor(l))) --> LESS_THAN(X::'a,l) | LESS_THAN(n::'a,X)) & \
-\ (\\<forall>X. ~(LESS_THAN(one::'a,X) & LESS_THAN(X::'a,l) & LESS_THAN(a(X),a(predecessor(X))))) --> False",
+\ (~mless_THAN(n::'a,k)) & \
+\ (~mless_THAN(k::'a,l)) & \
+\ (~mless_THAN(k::'a,i)) & \
+\ (mless_THAN(l::'a,n)) & \
+\ (mless_THAN(one::'a,l)) & \
+\ (mless_THAN(a(k),a(predecessor(l)))) & \
+\ (\\<forall>X. mless_THAN(X::'a,successor(n)) & mless_THAN(a(X),a(k)) --> mless_THAN(X::'a,l)) & \
+\ (\\<forall>X. mless_THAN(one::'a,l) & mless_THAN(a(X),a(predecessor(l))) --> mless_THAN(X::'a,l) | mless_THAN(n::'a,X)) & \
+\ (\\<forall>X. ~(mless_THAN(one::'a,X) & mless_THAN(X::'a,l) & mless_THAN(a(X),a(predecessor(X))))) --> False",
meson_tac 1);
(*2343 inferences so far. Searching to depth 8. 3.5 secs*)
val PRV006_1 = prove
(EQU001_0_ax ^ "&" ^ SWV001_1_ax ^ "&" ^ SWV001_0_eq ^ " & \
-\ (~LESS_THAN(n::'a,m)) & \
-\ (LESS_THAN(i::'a,m)) & \
-\ (LESS_THAN(i::'a,n)) & \
-\ (~LESS_THAN(i::'a,one)) & \
-\ (LESS_THAN(a(i),a(m))) & \
-\ (\\<forall>X. LESS_THAN(X::'a,successor(n)) & LESS_THAN(a(X),a(m)) --> LESS_THAN(X::'a,i)) & \
-\ (\\<forall>X. LESS_THAN(one::'a,i) & LESS_THAN(a(X),a(predecessor(i))) --> LESS_THAN(X::'a,i) | LESS_THAN(n::'a,X)) & \
-\ (\\<forall>X. ~(LESS_THAN(one::'a,X) & LESS_THAN(X::'a,i) & LESS_THAN(a(X),a(predecessor(X))))) --> False",
+\ (~mless_THAN(n::'a,m)) & \
+\ (mless_THAN(i::'a,m)) & \
+\ (mless_THAN(i::'a,n)) & \
+\ (~mless_THAN(i::'a,one)) & \
+\ (mless_THAN(a(i),a(m))) & \
+\ (\\<forall>X. mless_THAN(X::'a,successor(n)) & mless_THAN(a(X),a(m)) --> mless_THAN(X::'a,i)) & \
+\ (\\<forall>X. mless_THAN(one::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) & \
+\ (\\<forall>X. ~(mless_THAN(one::'a,X) & mless_THAN(X::'a,i) & mless_THAN(a(X),a(predecessor(X))))) --> False",
meson_tac 1);
(*86 inferences so far. Searching to depth 14. 0.1 secs*)
val PRV009_1 = prove
- ("(\\<forall>Y X. less_or_equal(X::'a,Y) | less(Y::'a,X)) & \
-\ (less(j::'a,i)) & \
-\ (less_or_equal(m::'a,p)) & \
-\ (less_or_equal(p::'a,q)) & \
-\ (less_or_equal(q::'a,n)) & \
-\ (\\<forall>X Y. less_or_equal(m::'a,X) & less(X::'a,i) & less(j::'a,Y) & less_or_equal(Y::'a,n) --> less_or_equal(a(X),a(Y))) & \
-\ (\\<forall>X Y. less_or_equal(m::'a,X) & less_or_equal(X::'a,Y) & less_or_equal(Y::'a,j) --> less_or_equal(a(X),a(Y))) & \
-\ (\\<forall>X Y. less_or_equal(i::'a,X) & less_or_equal(X::'a,Y) & less_or_equal(Y::'a,n) --> less_or_equal(a(X),a(Y))) & \
-\ (~less_or_equal(a(p),a(q))) --> False",
+ ("(\\<forall>Y X. mless_or_equal(X::'a,Y) | mless(Y::'a,X)) & \
+\ (mless(j::'a,i)) & \
+\ (mless_or_equal(m::'a,p)) & \
+\ (mless_or_equal(p::'a,q)) & \
+\ (mless_or_equal(q::'a,n)) & \
+\ (\\<forall>X Y. mless_or_equal(m::'a,X) & mless(X::'a,i) & mless(j::'a,Y) & mless_or_equal(Y::'a,n) --> mless_or_equal(a(X),a(Y))) & \
+\ (\\<forall>X Y. mless_or_equal(m::'a,X) & mless_or_equal(X::'a,Y) & mless_or_equal(Y::'a,j) --> mless_or_equal(a(X),a(Y))) & \
+\ (\\<forall>X Y. mless_or_equal(i::'a,X) & mless_or_equal(X::'a,Y) & mless_or_equal(Y::'a,n) --> mless_or_equal(a(X),a(Y))) & \
+\ (~mless_or_equal(a(p),a(q))) --> False",
meson_tac 1);
(*222 inferences so far. Searching to depth 8. 0.4 secs*)
--- a/src/HOL/ex/svc_funcs.ML Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/ex/svc_funcs.ML Fri Mar 17 09:34:23 2006 +0100
@@ -112,8 +112,8 @@
b1 orelse b2)
end
else (*might be numeric equality*) (t, is_intnat T)
- | Const("op <", Type ("fun", [T,_])) => (t, is_intnat T)
- | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T)
+ | Const("Orderings.less", Type ("fun", [T,_])) => (t, is_intnat T)
+ | Const("Orderings.less_eq", Type ("fun", [T,_])) => (t, is_intnat T)
| _ => (t, false)
end
in #1 o tag end;
@@ -219,13 +219,13 @@
else fail t
end
(*inequalities: possible types are nat, int, real*)
- | fm pos (t as Const("op <", Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const("Orderings.less", Type ("fun", [T,_])) $ x $ y) =
if not pos orelse T = HOLogic.realT then
Buildin("<", [tm x, tm y])
else if is_intnat T then
Buildin("<=", [suc (tm x), tm y])
else fail t
- | fm pos (t as Const("op <=", Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const("Orderings.less_eq", Type ("fun", [T,_])) $ x $ y) =
if pos orelse T = HOLogic.realT then
Buildin("<=", [tm x, tm y])
else if is_intnat T then