# HG changeset patch # User haftmann # Date 1142584463 -3600 # Node ID f7602e74d9489d6d57dab4d2a3832e1ade2fe0d4 # Parent ac90764bb654819dd2fd84e67c2a984d80b6029d renamed op < <= to Orderings.less(_eq) diff -r ac90764bb654 -r f7602e74d948 NEWS --- 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") diff -r ac90764bb654 -r f7602e74d948 src/HOL/Hoare/hoare.ML --- 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 diff -r ac90764bb654 -r f7602e74d948 src/HOL/Hoare/hoareAbort.ML --- 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 diff -r ac90764bb654 -r f7602e74d948 src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- 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" diff -r ac90764bb654 -r f7602e74d948 src/HOL/Import/Generate-HOL/GenHOL4Real.thy --- 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" diff -r ac90764bb654 -r f7602e74d948 src/HOL/Import/HOL/arithmetic.imp --- 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" diff -r ac90764bb654 -r f7602e74d948 src/HOL/Import/HOL/prim_rec.imp --- 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" diff -r ac90764bb654 -r f7602e74d948 src/HOL/Import/HOL/real.imp --- 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" diff -r ac90764bb654 -r f7602e74d948 src/HOL/Import/HOL/realax.imp --- 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" diff -r ac90764bb654 -r f7602e74d948 src/HOL/Integ/IntDef.thy --- 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" ("(_ int => bool" ("(_ <=/ _)") + "Orderings.less" :: "int => int => bool" ("(_ int => bool" ("(_ <=/ _)") "neg" ("(_ < 0)") code_syntax_tyco int diff -r ac90764bb654 -r f7602e74d948 src/HOL/Integ/cooper_dec.ML --- 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))]; diff -r ac90764bb654 -r f7602e74d948 src/HOL/Integ/cooper_proof.ML --- 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; diff -r ac90764bb654 -r f7602e74d948 src/HOL/Integ/int_arith1.ML --- 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 ); diff -r ac90764bb654 -r f7602e74d948 src/HOL/Integ/int_factor_simprocs.ML --- 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 ) diff -r ac90764bb654 -r f7602e74d948 src/HOL/Integ/nat_simprocs.ML --- 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 ); diff -r ac90764bb654 -r f7602e74d948 src/HOL/Integ/presburger.ML --- 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), diff -r ac90764bb654 -r f7602e74d948 src/HOL/Integ/reflected_cooper.ML --- 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) diff -r ac90764bb654 -r f7602e74d948 src/HOL/Orderings.thy --- 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 \") - "op <=" :: "['a::ord, 'a] => bool" ("(_/ \ _)" [50, 51] 50) + "less_eq" :: "['a::ord, 'a] => bool" ("op \") + "less_eq" :: "['a::ord, 'a] => bool" ("(_/ \ _)" [50, 51] 50) syntax (HTML output) - "op <=" :: "['a::ord, 'a] => bool" ("op \") - "op <=" :: "['a::ord, 'a] => bool" ("(_/ \ _)" [50, 51] 50) + "less_eq" :: "['a::ord, 'a] => bool" ("op \") + "less_eq" :: "['a::ord, 'a] => bool" ("(_/ \ _)" [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 diff -r ac90764bb654 -r f7602e74d948 src/HOL/Real/Float.ML --- 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 diff -r ac90764bb654 -r f7602e74d948 src/HOL/Set.thy --- 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) diff -r ac90764bb654 -r f7602e74d948 src/HOL/Tools/Presburger/cooper_dec.ML --- 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))]; diff -r ac90764bb654 -r f7602e74d948 src/HOL/Tools/Presburger/cooper_proof.ML --- 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; diff -r ac90764bb654 -r f7602e74d948 src/HOL/Tools/Presburger/presburger.ML --- 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), diff -r ac90764bb654 -r f7602e74d948 src/HOL/Tools/Presburger/reflected_cooper.ML --- 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) diff -r ac90764bb654 -r f7602e74d948 src/HOL/Tools/refute.ML --- 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 diff -r ac90764bb654 -r f7602e74d948 src/HOL/Tools/res_clause.ML --- 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"), diff -r ac90764bb654 -r f7602e74d948 src/HOL/antisym_setup.ML --- 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 => diff -r ac90764bb654 -r f7602e74d948 src/HOL/arith_data.ML --- 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' => diff -r ac90764bb654 -r f7602e74d948 src/HOL/ex/SVC_Oracle.ML --- 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) diff -r ac90764bb654 -r f7602e74d948 src/HOL/ex/mesontest2.ML --- 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 = - "(\\X Y. less_equal(X::'a,Y) --> equal(Divide(X::'a,Y),zero)) & \ -\ (\\X Y. equal(Divide(X::'a,Y),zero) --> less_equal(X::'a,Y)) & \ -\ (\\Y X. less_equal(Divide(X::'a,Y),X)) & \ -\ (\\X Y Z. less_equal(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z))) & \ -\ (\\X. less_equal(zero::'a,X)) & \ -\ (\\X Y. less_equal(X::'a,Y) & less_equal(Y::'a,X) --> equal(X::'a,Y)) & \ -\ (\\X. less_equal(X::'a,identity))"; + "(\\X Y. mless_equal(X::'a,Y) --> equal(Divide(X::'a,Y),zero)) & \ +\ (\\X Y. equal(Divide(X::'a,Y),zero) --> mless_equal(X::'a,Y)) & \ +\ (\\Y X. mless_equal(Divide(X::'a,Y),X)) & \ +\ (\\X Y Z. mless_equal(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z))) & \ +\ (\\X. mless_equal(zero::'a,X)) & \ +\ (\\X Y. mless_equal(X::'a,Y) & mless_equal(Y::'a,X) --> equal(X::'a,Y)) & \ +\ (\\X. mless_equal(X::'a,identity))"; val HEN002_0_eq = "(\\A B C. equal(A::'a,B) --> equal(Divide(A::'a,C),Divide(B::'a,C))) & \ \ (\\D F' E. equal(D::'a,E) --> equal(Divide(F'::'a,D),Divide(F'::'a,E))) & \ -\ (\\G H I'. equal(G::'a,H) & less_equal(G::'a,I') --> less_equal(H::'a,I')) & \ -\ (\\J L K'. equal(J::'a,K') & less_equal(L::'a,J) --> less_equal(L::'a,K'))"; +\ (\\G H I'. equal(G::'a,H) & mless_equal(G::'a,I') --> mless_equal(H::'a,I')) & \ +\ (\\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 ^ " & \ -\ (\\X Y. less_equal(X::'a,Y) --> quotient(X::'a,Y,zero)) & \ -\ (\\X Y. quotient(X::'a,Y,zero) --> less_equal(X::'a,Y)) & \ -\ (\\Y Z X. quotient(X::'a,Y,Z) --> less_equal(Z::'a,X)) & \ -\ (\\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)) & \ -\ (\\X. less_equal(zero::'a,X)) & \ -\ (\\X Y. less_equal(X::'a,Y) & less_equal(Y::'a,X) --> equal(X::'a,Y)) & \ -\ (\\X. less_equal(X::'a,identity)) & \ +\ (\\X Y. mless_equal(X::'a,Y) --> quotient(X::'a,Y,zero)) & \ +\ (\\X Y. quotient(X::'a,Y,zero) --> mless_equal(X::'a,Y)) & \ +\ (\\Y Z X. quotient(X::'a,Y,Z) --> mless_equal(Z::'a,X)) & \ +\ (\\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)) & \ +\ (\\X. mless_equal(zero::'a,X)) & \ +\ (\\X Y. mless_equal(X::'a,Y) & mless_equal(Y::'a,X) --> equal(X::'a,Y)) & \ +\ (\\X. mless_equal(X::'a,identity)) & \ \ (\\X Y. quotient(X::'a,Y,Divide(X::'a,Y))) & \ \ (\\X Y Z W. quotient(X::'a,Y,Z) & quotient(X::'a,Y,W) --> equal(Z::'a,W)) & \ \ (\\X Y W Z. equal(X::'a,Y) & quotient(X::'a,W,Z) --> quotient(Y::'a,W,Z)) & \ \ (\\X W Y Z. equal(X::'a,Y) & quotient(W::'a,X,Z) --> quotient(W::'a,Y,Z)) & \ \ (\\X W Z Y. equal(X::'a,Y) & quotient(W::'a,Z,X) --> quotient(W::'a,Z,Y)) & \ -\ (\\X Z Y. equal(X::'a,Y) & less_equal(Z::'a,X) --> less_equal(Z::'a,Y)) & \ -\ (\\X Y Z. equal(X::'a,Y) & less_equal(X::'a,Z) --> less_equal(Y::'a,Z)) & \ +\ (\\X Z Y. equal(X::'a,Y) & mless_equal(Z::'a,X) --> mless_equal(Z::'a,Y)) & \ +\ (\\X Y Z. equal(X::'a,Y) & mless_equal(X::'a,Z) --> mless_equal(Y::'a,Z)) & \ \ (\\X Y W. equal(X::'a,Y) --> equal(Divide(X::'a,W),Divide(Y::'a,W))) & \ \ (\\X W Y. equal(X::'a,Y) --> equal(Divide(W::'a,X),Divide(W::'a,Y))) & \ \ (\\X. quotient(X::'a,identity,zero)) & \ \ (\\X. quotient(zero::'a,X,zero)) & \ \ (\\X. quotient(X::'a,X,zero)) & \ \ (\\X. quotient(X::'a,zero,X)) & \ -\ (\\Y X Z. less_equal(X::'a,Y) & less_equal(Y::'a,Z) --> less_equal(X::'a,Z)) & \ -\ (\\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)) & \ +\ (\\Y X Z. mless_equal(X::'a,Y) & mless_equal(Y::'a,Z) --> mless_equal(X::'a,Z)) & \ +\ (\\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 @@ \ (\\X. equal(Divide(zero::'a,X),zero)) & \ \ (\\X. equal(Divide(X::'a,X),zero)) & \ \ (equal(Divide(a::'a,zero),a)) & \ -\ (\\Y X Z. less_equal(X::'a,Y) & less_equal(Y::'a,Z) --> less_equal(X::'a,Z)) & \ -\ (\\X Z Y. less_equal(Divide(X::'a,Y),Z) --> less_equal(Divide(X::'a,Z),Y)) & \ -\ (\\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", +\ (\\Y X Z. mless_equal(X::'a,Y) & mless_equal(Y::'a,Z) --> mless_equal(X::'a,Z)) & \ +\ (\\X Z Y. mless_equal(Divide(X::'a,Y),Z) --> mless_equal(Divide(X::'a,Z),Y)) & \ +\ (\\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 @@ \ (\\A B. equal(A::'a,B) --> equal(successor(A),successor(B)))"; val NUM001_1_ax = - "(\\A C B. less(A::'a,B) & less(C::'a,A) --> less(C::'a,B)) & \ -\ (\\A B C. equal(add(successor(A),B),C) --> less(B::'a,C)) & \ -\ (\\A B. less(A::'a,B) --> equal(add(successor(predecessor_of_1st_minus_2nd(B::'a,A)),A),B))"; + "(\\A C B. mless(A::'a,B) & mless(C::'a,A) --> mless(C::'a,B)) & \ +\ (\\A B C. equal(add(successor(A),B),C) --> mless(B::'a,C)) & \ +\ (\\A B. mless(A::'a,B) --> equal(add(successor(predecessor_of_1st_minus_2nd(B::'a,A)),A),B))"; val NUM001_2_ax = - "(\\A B. divides(A::'a,B) --> less(A::'a,B) | equal(A::'a,B)) & \ -\ (\\A B. less(A::'a,B) --> divides(A::'a,B)) & \ + "(\\A B. divides(A::'a,B) --> mless(A::'a,B) | equal(A::'a,B)) & \ +\ (\\A B. mless(A::'a,B) --> divides(A::'a,B)) & \ \ (\\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)) & \ \ (\\A. ~equal(successor(A),num0)) --> False", meson_tac 1); @@ -1315,7 +1315,7 @@ (EQU001_0_ax ^ "&" ^ NUM001_0_ax ^ "&" ^ NUM001_1_ax ^ " & \ \ (\\B A. equal(add(A::'a,B),add(B::'a,A))) & \ \ (\\B A C. equal(add(A::'a,B),add(C::'a,B)) --> equal(A::'a,C)) & \ -\ (less(a::'a,a)) & \ +\ (mless(a::'a,a)) & \ \ (\\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 - ("(\\X Y Z. q1(X::'a,Y,Z) & less_or_equal(X::'a,Y) --> q2(X::'a,Y,Z)) & \ -\ (\\X Y Z. q1(X::'a,Y,Z) --> less_or_equal(X::'a,Y) | q3(X::'a,Y,Z)) & \ + ("(\\X Y Z. q1(X::'a,Y,Z) & mless_or_equal(X::'a,Y) --> q2(X::'a,Y,Z)) & \ +\ (\\X Y Z. q1(X::'a,Y,Z) --> mless_or_equal(X::'a,Y) | q3(X::'a,Y,Z)) & \ \ (\\Z X Y. q2(X::'a,Y,Z) --> q4(X::'a,Y,Y)) & \ \ (\\Z Y X. q3(X::'a,Y,Z) --> q4(X::'a,Y,X)) & \ -\ (\\X. less_or_equal(X::'a,X)) & \ -\ (\\X Y. less_or_equal(X::'a,Y) & less_or_equal(Y::'a,X) --> equal(X::'a,Y)) & \ -\ (\\Y X Z. less_or_equal(X::'a,Y) & less_or_equal(Y::'a,Z) --> less_or_equal(X::'a,Z)) & \ -\ (\\Y X. less_or_equal(X::'a,Y) | less_or_equal(Y::'a,X)) & \ -\ (\\X Y. equal(X::'a,Y) --> less_or_equal(X::'a,Y)) & \ -\ (\\X Y Z. equal(X::'a,Y) & less_or_equal(X::'a,Z) --> less_or_equal(Y::'a,Z)) & \ -\ (\\X Z Y. equal(X::'a,Y) & less_or_equal(Z::'a,X) --> less_or_equal(Z::'a,Y)) & \ +\ (\\X. mless_or_equal(X::'a,X)) & \ +\ (\\X Y. mless_or_equal(X::'a,Y) & mless_or_equal(Y::'a,X) --> equal(X::'a,Y)) & \ +\ (\\Y X Z. mless_or_equal(X::'a,Y) & mless_or_equal(Y::'a,Z) --> mless_or_equal(X::'a,Z)) & \ +\ (\\Y X. mless_or_equal(X::'a,Y) | mless_or_equal(Y::'a,X)) & \ +\ (\\X Y. equal(X::'a,Y) --> mless_or_equal(X::'a,Y)) & \ +\ (\\X Y Z. equal(X::'a,Y) & mless_or_equal(X::'a,Z) --> mless_or_equal(Y::'a,Z)) & \ +\ (\\X Z Y. equal(X::'a,Y) & mless_or_equal(Z::'a,X) --> mless_or_equal(Z::'a,Y)) & \ \ (q1(a::'a,b,c)) & \ -\ (\\W. ~(q4(a::'a,b,W) & less_or_equal(a::'a,W) & less_or_equal(b::'a,W) & less_or_equal(W::'a,a))) & \ -\ (\\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", +\ (\\W. ~(q4(a::'a,b,W) & mless_or_equal(a::'a,W) & mless_or_equal(b::'a,W) & mless_or_equal(W::'a,a))) & \ +\ (\\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 @@ \ (\\X. equal(successor(predecessor(X)),X)) & \ \ (\\X Y. equal(predecessor(X),predecessor(Y)) --> equal(X::'a,Y)) & \ \ (\\X Y. equal(successor(X),successor(Y)) --> equal(X::'a,Y)) & \ -\ (\\X. LESS_THAN(predecessor(X),X)) & \ -\ (\\X. LESS_THAN(X::'a,successor(X))) & \ -\ (\\X Y Z. LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,Z) --> LESS_THAN(X::'a,Z)) & \ -\ (\\X Y. LESS_THAN(X::'a,Y) | LESS_THAN(Y::'a,X) | equal(X::'a,Y)) & \ -\ (\\X. ~LESS_THAN(X::'a,X)) & \ -\ (\\Y X. ~(LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,X))) & \ -\ (\\Y X Z. equal(X::'a,Y) & LESS_THAN(X::'a,Z) --> LESS_THAN(Y::'a,Z)) & \ -\ (\\Y Z X. equal(X::'a,Y) & LESS_THAN(Z::'a,X) --> LESS_THAN(Z::'a,Y))"; +\ (\\X. mless_THAN(predecessor(X),X)) & \ +\ (\\X. mless_THAN(X::'a,successor(X))) & \ +\ (\\X Y Z. mless_THAN(X::'a,Y) & mless_THAN(Y::'a,Z) --> mless_THAN(X::'a,Z)) & \ +\ (\\X Y. mless_THAN(X::'a,Y) | mless_THAN(Y::'a,X) | equal(X::'a,Y)) & \ +\ (\\X. ~mless_THAN(X::'a,X)) & \ +\ (\\Y X. ~(mless_THAN(X::'a,Y) & mless_THAN(Y::'a,X))) & \ +\ (\\Y X Z. equal(X::'a,Y) & mless_THAN(X::'a,Z) --> mless_THAN(Y::'a,Z)) & \ +\ (\\Y Z X. equal(X::'a,Y) & mless_THAN(Z::'a,X) --> mless_THAN(Z::'a,Y))"; val SWV001_0_eq = "(\\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))) & \ -\ (\\X. LESS_THAN(X::'a,j) & LESS_THAN(a(X),a(k)) --> LESS_THAN(X::'a,i)) & \ -\ (\\X. LESS_THAN(one::'a,i) & LESS_THAN(a(X),a(predecessor(i))) --> LESS_THAN(X::'a,i) | LESS_THAN(n::'a,X)) & \ -\ (\\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))) & \ +\ (\\X. mless_THAN(X::'a,j) & mless_THAN(a(X),a(k)) --> mless_THAN(X::'a,i)) & \ +\ (\\X. mless_THAN(one::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) & \ +\ (\\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)))) & \ -\ (\\X. LESS_THAN(X::'a,successor(n)) & LESS_THAN(a(X),a(k)) --> LESS_THAN(X::'a,l)) & \ -\ (\\X. LESS_THAN(one::'a,l) & LESS_THAN(a(X),a(predecessor(l))) --> LESS_THAN(X::'a,l) | LESS_THAN(n::'a,X)) & \ -\ (\\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)))) & \ +\ (\\X. mless_THAN(X::'a,successor(n)) & mless_THAN(a(X),a(k)) --> mless_THAN(X::'a,l)) & \ +\ (\\X. mless_THAN(one::'a,l) & mless_THAN(a(X),a(predecessor(l))) --> mless_THAN(X::'a,l) | mless_THAN(n::'a,X)) & \ +\ (\\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))) & \ -\ (\\X. LESS_THAN(X::'a,successor(n)) & LESS_THAN(a(X),a(m)) --> LESS_THAN(X::'a,i)) & \ -\ (\\X. LESS_THAN(one::'a,i) & LESS_THAN(a(X),a(predecessor(i))) --> LESS_THAN(X::'a,i) | LESS_THAN(n::'a,X)) & \ -\ (\\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))) & \ +\ (\\X. mless_THAN(X::'a,successor(n)) & mless_THAN(a(X),a(m)) --> mless_THAN(X::'a,i)) & \ +\ (\\X. mless_THAN(one::'a,i) & mless_THAN(a(X),a(predecessor(i))) --> mless_THAN(X::'a,i) | mless_THAN(n::'a,X)) & \ +\ (\\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 - ("(\\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)) & \ -\ (\\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))) & \ -\ (\\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))) & \ -\ (\\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", + ("(\\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)) & \ +\ (\\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))) & \ +\ (\\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))) & \ +\ (\\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*) diff -r ac90764bb654 -r f7602e74d948 src/HOL/ex/svc_funcs.ML --- 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