--- a/NEWS Fri Jul 20 14:28:05 2007 +0200
+++ b/NEWS Fri Jul 20 14:28:25 2007 +0200
@@ -943,9 +943,10 @@
op + ~> HOL.plus_class.plus
op - ~> HOL.minus_class.minus
uminus ~> HOL.minus_class.uminus
+ abs ~> HOL.abs_class.abs
op * ~> HOL.times_class.times
- op < ~> Orderings.ord_class.less
- op <= ~> Orderings.ord_class.less_eq
+ op < ~> HOL.ord_class.less
+ op <= ~> HOL.ord_class.less_eq
Adaptions may be required in the following cases:
@@ -1044,7 +1045,7 @@
r and finally gets the theorem t = r, which is again applied to the
subgoal. An Example is available in HOL/ex/ReflectionEx.thy.
-* Reflection: Automatic refification now handels binding, an example
+* Reflection: Automatic reification now handels binding, an example
is available in HOL/ex/ReflectionEx.thy
--- a/src/HOL/Arith_Tools.thy Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Arith_Tools.thy Fri Jul 20 14:28:25 2007 +0200
@@ -480,14 +480,14 @@
fun proc3 phi ss ct =
(case term_of ct of
- Const(@{const_name "Orderings.less"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
+ Const(@{const_name HOL.less},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name "Orderings.less_eq"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
+ | Const(@{const_name HOL.less_eq},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
@@ -501,14 +501,14 @@
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name "Orderings.less"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
+ | Const(@{const_name HOL.less},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name "Orderings.less_eq"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
+ | Const(@{const_name HOL.less_eq},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
@@ -745,7 +745,7 @@
fun xnormalize_conv ctxt [] ct = reflexive ct
| xnormalize_conv ctxt (vs as (x::_)) ct =
case term_of ct of
- Const(@{const_name "Orderings.less"},_)$_$Const(@{const_name "HOL.zero"},_) =>
+ Const(@{const_name HOL.less},_)$_$Const(@{const_name "HOL.zero"},_) =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -788,7 +788,7 @@
| _ => reflexive ct)
-| Const(@{const_name "Orderings.less_eq"},_)$_$Const(@{const_name "HOL.zero"},_) =>
+| Const(@{const_name HOL.less_eq},_)$_$Const(@{const_name "HOL.zero"},_) =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -877,7 +877,7 @@
val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
in
fun field_isolate_conv phi ctxt vs ct = case term_of ct of
- Const(@{const_name "Orderings.less"},_)$a$b =>
+ Const(@{const_name HOL.less},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
val T = ctyp_of_term ca
val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
@@ -886,7 +886,7 @@
(Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| Const(@{const_name "Orderings.less_eq"},_)$a$b =>
+| Const(@{const_name HOL.less_eq},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
val T = ctyp_of_term ca
val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
@@ -917,11 +917,11 @@
else Ferrante_Rackoff_Data.Nox
| @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
else Ferrante_Rackoff_Data.Nox
- | Const(@{const_name "Orderings.less"},_)$y$z =>
+ | Const(@{const_name HOL.less},_)$y$z =>
if term_of x aconv y then Ferrante_Rackoff_Data.Lt
else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
else Ferrante_Rackoff_Data.Nox
- | Const (@{const_name "Orderings.less_eq"},_)$y$z =>
+ | Const (@{const_name HOL.less_eq},_)$y$z =>
if term_of x aconv y then Ferrante_Rackoff_Data.Le
else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
else Ferrante_Rackoff_Data.Nox
--- a/src/HOL/Complex/ex/linreif.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Complex/ex/linreif.ML Fri Jul 20 14:28:25 2007 +0200
@@ -15,41 +15,37 @@
exception LINR;
(* pseudo reification : term -> intterm *)
-val iT = HOLogic.intT;
val rT = Type ("RealDef.real",[]);
val bT = HOLogic.boolT;
-val realC = Const("RealDef.real",iT --> rT);
-val rzero = Const("0",rT);
+val realC = @{term "RealDef.real :: int => real"};
+val rzero = @{term "0 :: real"};
-fun num_of_term vs t =
- case t of
- Free(xn,xT) => (case AList.lookup (op =) vs t of
- NONE => error "Variable not found in the list!"
- | SOME n => Bound n)
+fun num_of_term vs t = case t
+ of Free(xn,xT) => (case AList.lookup (op =) vs t of
+ NONE => error "Variable not found in the list!"
+ | SOME n => Bound n)
| Const("RealDef.real",_)$ @{term "0::int"} => C 0
| Const("RealDef.real",_)$ @{term "1::int"} => C 1
| @{term "0::real"} => C 0
| @{term "0::real"} => C 1
| Term.Bound i => Bound (nat i)
- | Const(@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
+ | Const (@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
| Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2)
| Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2)
- | Const (@{const_name "HOL.times"},_)$t1$t2 =>
- (case (num_of_term vs t1) of C i =>
- Mul (i,num_of_term vs t2)
- | _ => error "num_of_term: unsupported Multiplication")
+ | Const (@{const_name "HOL.times"},_)$t1$t2 => (case (num_of_term vs t1) of C i =>
+ Mul (i,num_of_term vs t2)
+ | _ => error "num_of_term: unsupported Multiplication")
| Const("RealDef.real",_) $ Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
| Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
| _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t));
-
(* pseudo reification : term -> fm *)
fun fm_of_term vs t =
case t of
Const("True",_) => T
| Const("False",_) => F
- | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
- | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
+ | Const(@{const_name HOL.less},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
+ | Const(@{const_name HOL.less_eq},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
| Const("op =",eqT)$t1$t2 =>
if (domain_type eqT = rT)
then Eqa (Sub (num_of_term vs t1,num_of_term vs t2))
@@ -64,13 +60,10 @@
A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
| _ => error ("fm_of_term : unknown term!" ^ (Display.raw_string_of_term t));
-fun zip [] [] = []
- | zip (x::xs) (y::ys) = (x,y)::(zip xs ys);
-
fun start_vs t =
let val fs = term_frees t
- in zip fs (map nat (0 upto (length fs - 1)))
+ in fs ~~ map nat (0 upto (length fs - 1))
end ;
(* transform num and fm back to terms *)
@@ -84,13 +77,13 @@
fun term_of_num vs t =
case t of
C i => realC $ (HOLogic.mk_number HOLogic.intT i)
- | Bound n => valOf (myassoc2 vs n)
- | Neg t' => Const(@{const_name "HOL.uminus"},rT --> rT)$(term_of_num vs t')
- | Add(t1,t2) => Const(@{const_name "HOL.plus"},[rT,rT] ---> rT)$
+ | Bound n => the (myassoc2 vs n)
+ | Neg t' => Const(@{const_name HOL.uminus},rT --> rT)$(term_of_num vs t')
+ | Add(t1,t2) => Const(@{const_name HOL.plus},[rT,rT] ---> rT)$
(term_of_num vs t1)$(term_of_num vs t2)
- | Sub(t1,t2) => Const(@{const_name "HOL.minus"},[rT,rT] ---> rT)$
+ | Sub(t1,t2) => Const(@{const_name HOL.minus},[rT,rT] ---> rT)$
(term_of_num vs t1)$(term_of_num vs t2)
- | Mul(i,t2) => Const(@{const_name "HOL.times"},[rT,rT] ---> rT)$
+ | Mul(i,t2) => Const(@{const_name HOL.times},[rT,rT] ---> rT)$
(term_of_num vs (C i))$(term_of_num vs t2)
| Cn(n,i,t) => term_of_num vs (Add (Mul(i,Bound n),t));
@@ -98,13 +91,13 @@
case t of
T => HOLogic.true_const
| F => HOLogic.false_const
- | Lta t => Const(@{const_name "Orderings.less"},[rT,rT] ---> bT)$
+ | Lta t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
(term_of_num vs t)$ rzero
- | Lea t => Const(@{const_name "Orderings.less_eq"},[rT,rT] ---> bT)$
+ | Lea t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
(term_of_num vs t)$ rzero
- | Gta t => Const(@{const_name "Orderings.less"},[rT,rT] ---> bT)$
+ | Gta t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
rzero $(term_of_num vs t)
- | Gea t => Const(@{const_name "Orderings.less_eq"},[rT,rT] ---> bT)$
+ | Gea t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
rzero $(term_of_num vs t)
| Eqa t => Const("op =",[rT,rT] ---> bT)$
(term_of_num vs t)$ rzero
--- a/src/HOL/Complex/ex/mireif.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Complex/ex/mireif.ML Fri Jul 20 14:28:25 2007 +0200
@@ -42,8 +42,8 @@
case t of
Const("True",_) => T
| Const("False",_) => F
- | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
- | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
+ | Const(@{const_name HOL.less},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
+ | Const(@{const_name HOL.less_eq},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
| Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Numeral.number_of"},_)$t1))$t2 =>
Dvda (HOLogic.dest_numeral t1, num_of_term vs t2)
| Const("op =",eqT)$t1$t2 =>
--- a/src/HOL/Hoare/hoare.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Hoare/hoare.ML Fri Jul 20 14:28:25 2007 +0200
@@ -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 (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
+fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
(** Makes "Mset <= t" **)
fun Mset_incl t = let val MsetT = fastype_of t
--- a/src/HOL/Hoare/hoareAbort.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Hoare/hoareAbort.ML Fri Jul 20 14:28:25 2007 +0200
@@ -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 (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
+fun inclt ty = Const (@{const_name HOL.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 Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Jul 20 14:28:25 2007 +0200
@@ -166,7 +166,7 @@
import_theory prim_rec;
const_maps
- "<" > Orderings.ord_class.less :: "[nat,nat]=>bool";
+ "<" > HOL.ord_class.less :: "[nat,nat]=>bool";
end_import;
@@ -181,7 +181,7 @@
">" > HOL4Compat.nat_gt
">=" > HOL4Compat.nat_ge
FUNPOW > HOL4Compat.FUNPOW
- "<=" > Orderings.ord_class.less_eq :: "[nat,nat]=>bool"
+ "<=" > HOL.ord_class.less_eq :: "[nat,nat]=>bool"
"+" > HOL.plus_class.plus :: "[nat,nat]=>nat"
"*" > HOL.times_class.times :: "[nat,nat]=>nat"
"-" > HOL.minus_class.minus :: "[nat,nat]=>nat"
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Jul 20 14:28:25 2007 +0200
@@ -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 > Orderings.ord_class.less :: "[real,real] => bool";
+ real_lt > HOL.ord_class.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 > Orderings.ord_class.less_eq :: "[real,real] => bool"
+ real_lte > HOL.ord_class.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 Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp Fri Jul 20 14:28:25 2007 +0200
@@ -23,7 +23,7 @@
"ALT_ZERO" > "HOL4Compat.ALT_ZERO"
">=" > "HOL4Compat.nat_ge"
">" > "HOL4Compat.nat_gt"
- "<=" > "Orderings.ord_class.less_eq" :: "nat => nat => bool"
+ "<=" > "HOL.ord_class.less_eq" :: "nat => nat => bool"
"-" > "HOL.minus_class.minus" :: "nat => nat => nat"
"+" > "HOL.plus_class.plus" :: "nat => nat => nat"
"*" > "HOL.times_class.times" :: "nat => nat => nat"
--- a/src/HOL/Import/HOL/prim_rec.imp Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Import/HOL/prim_rec.imp Fri Jul 20 14:28:25 2007 +0200
@@ -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"
- "<" > "Orderings.ord_class.less" :: "nat => nat => bool"
+ "<" > "HOL.ord_class.less" :: "nat => nat => bool"
thm_maps
"wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
--- a/src/HOL/Import/HOL/real.imp Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Import/HOL/real.imp Fri Jul 20 14:28:25 2007 +0200
@@ -12,7 +12,7 @@
"sum" > "HOL4Real.real.sum"
"real_sub" > "HOL.minus_class.minus" :: "real => real => real"
"real_of_num" > "RealDef.real" :: "nat => real"
- "real_lte" > "Orderings.ord_class.less_eq" :: "real => real => bool"
+ "real_lte" > "HOL.ord_class.less_eq" :: "real => real => bool"
"real_gt" > "HOL4Compat.real_gt"
"real_ge" > "HOL4Compat.real_ge"
"pow" > "Nat.power_class.power" :: "real => nat => real"
--- a/src/HOL/Import/HOL/realax.imp Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Import/HOL/realax.imp Fri Jul 20 14:28:25 2007 +0200
@@ -29,7 +29,7 @@
"treal_0" > "HOL4Real.realax.treal_0"
"real_neg" > "HOL.minus_class.uminus" :: "real => real"
"real_mul" > "HOL.times_class.times" :: "real => real => real"
- "real_lt" > "Orderings.ord_class.less" :: "real => real => bool"
+ "real_lt" > "HOL.ord_class.less" :: "real => real => bool"
"real_add" > "HOL.plus_class.plus" :: "real => real => real"
"real_1" > "HOL.one_class.one" :: "real"
"real_0" > "HOL.zero_class.zero" :: "real"
--- a/src/HOL/Library/sct.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Library/sct.ML Fri Jul 20 14:28:25 2007 +0200
@@ -63,8 +63,8 @@
in Const (nth_const, lT --> HOLogic.natT --> T) $ xs end
-val less_nat_const = Const (@{const_name Orderings.less}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
-val lesseq_nat_const = Const (@{const_name Orderings.less_eq}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+val less_nat_const = Const (@{const_name HOL.less}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+val lesseq_nat_const = Const (@{const_name HOL.less_eq}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
val has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"]
--- a/src/HOL/Orderings.thy Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Orderings.thy Fri Jul 20 14:28:25 2007 +0200
@@ -6,88 +6,12 @@
header {* Syntactic and abstract orders *}
theory Orderings
-imports HOL
+imports Set Fun
uses
(*"~~/src/Provers/quasi.ML"*)
"~~/src/Provers/order.ML"
begin
-subsection {* Order syntax *}
-
-class ord = type +
- fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
- and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50)
-begin
-
-notation
- less_eq ("op \<^loc><=") and
- less_eq ("(_/ \<^loc><= _)" [51, 51] 50) and
- less ("op \<^loc><") and
- less ("(_/ \<^loc>< _)" [51, 51] 50)
-
-notation (xsymbols)
- less_eq ("op \<^loc>\<le>") and
- less_eq ("(_/ \<^loc>\<le> _)" [51, 51] 50)
-
-notation (HTML output)
- less_eq ("op \<^loc>\<le>") and
- less_eq ("(_/ \<^loc>\<le> _)" [51, 51] 50)
-
-abbreviation (input)
- greater (infix "\<^loc>>" 50) where
- "x \<^loc>> y \<equiv> y \<^loc>< x"
-
-abbreviation (input)
- greater_eq (infix "\<^loc>>=" 50) where
- "x \<^loc>>= y \<equiv> y \<^loc><= x"
-
-notation (input)
- greater_eq (infix "\<^loc>\<ge>" 50)
-
-text {*
- syntactic min/max -- these definitions reach
- their usual semantics in class linorder ahead.
-*}
-
-definition
- min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
- "min a b = (if a \<^loc>\<le> b then a else b)"
-
-definition
- max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
- "max a b = (if a \<^loc>\<le> b then b else a)"
-
-end
-
-notation
- less_eq ("op <=") and
- less_eq ("(_/ <= _)" [51, 51] 50) and
- less ("op <") and
- less ("(_/ < _)" [51, 51] 50)
-
-notation (xsymbols)
- less_eq ("op \<le>") and
- less_eq ("(_/ \<le> _)" [51, 51] 50)
-
-notation (HTML output)
- less_eq ("op \<le>") and
- less_eq ("(_/ \<le> _)" [51, 51] 50)
-
-abbreviation (input)
- greater (infix ">" 50) where
- "x > y \<equiv> y < x"
-
-abbreviation (input)
- greater_eq (infix ">=" 50) where
- "x >= y \<equiv> y <= x"
-
-notation (input)
- greater_eq (infix "\<ge>" 50)
-
-lemmas min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
-lemmas max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
-
-
subsection {* Partial orders *}
class order = ord +
@@ -265,7 +189,20 @@
(simp add: less_le, auto intro: antisym order_trans simp add: linear)
-text {* min/max properties *}
+text {* min/max *}
+
+text {* for historic reasons, definitions are done in context ord *}
+
+definition (in ord)
+ min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+ "min a b = (if a \<^loc>\<le> b then a else b)"
+
+definition (in ord)
+ max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+ "max a b = (if a \<^loc>\<le> b then b else a)"
+
+lemmas (in -) min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
+lemmas (in -) max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
lemma min_le_iff_disj:
"min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
@@ -370,11 +307,11 @@
if of_sort t1
then SOME (t1, "=", t2)
else NONE
- | dec (Const (@{const_name Orderings.less_eq}, _) $ t1 $ t2) =
+ | dec (Const (@{const_name HOL.less_eq}, _) $ t1 $ t2) =
if of_sort t1
then SOME (t1, "<=", t2)
else NONE
- | dec (Const (@{const_name Orderings.less}, _) $ t1 $ t2) =
+ | dec (Const (@{const_name HOL.less}, _) $ t1 $ t2) =
if of_sort t1
then SOME (t1, "<", t2)
else NONE
@@ -840,7 +777,81 @@
unfolding le_bool_def less_bool_def by simp_all
-subsection {* Monotonicity, syntactic least value operator and min/max *}
+subsection {* Order on sets *}
+
+instance set :: (type) order
+ by (intro_classes,
+ (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
+
+lemmas basic_trans_rules [trans] =
+ order_trans_rules set_rev_mp set_mp
+
+
+subsection {* Order on functions *}
+
+instance "fun" :: (type, ord) ord
+ le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
+ less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
+
+lemmas [code func del] = le_fun_def less_fun_def
+
+instance "fun" :: (type, order) order
+ by default
+ (auto simp add: le_fun_def less_fun_def expand_fun_eq
+ intro: order_trans order_antisym)
+
+lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
+ unfolding le_fun_def by simp
+
+lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
+ unfolding le_fun_def by simp
+
+lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
+ unfolding le_fun_def by simp
+
+text {*
+ Handy introduction and elimination rules for @{text "\<le>"}
+ on unary and binary predicates
+*}
+
+lemma predicate1I [Pure.intro!, intro!]:
+ assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
+ shows "P \<le> Q"
+ apply (rule le_funI)
+ apply (rule le_boolI)
+ apply (rule PQ)
+ apply assumption
+ done
+
+lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
+ apply (erule le_funE)
+ apply (erule le_boolE)
+ apply assumption+
+ done
+
+lemma predicate2I [Pure.intro!, intro!]:
+ assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
+ shows "P \<le> Q"
+ apply (rule le_funI)+
+ apply (rule le_boolI)
+ apply (rule PQ)
+ apply assumption
+ done
+
+lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
+ apply (erule le_funE)+
+ apply (erule le_boolE)
+ apply assumption+
+ done
+
+lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
+ by (rule predicate1D)
+
+lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
+ by (rule predicate2D)
+
+
+subsection {* Monotonicity, least value operator and min/max *}
locale mono =
fixes f
@@ -849,11 +860,6 @@
lemmas monoI [intro?] = mono.intro
and monoD [dest?] = mono.mono
-constdefs
- Least :: "('a::ord => bool) => 'a" (binder "LEAST " 10)
- "Least P == THE x. P x & (ALL y. P y --> x <= y)"
- -- {* We can no longer use LeastM because the latter requires Hilbert-AC. *}
-
lemma LeastI2_order:
"[| P (x::'a::order);
!!y. P y ==> x <= y;
@@ -864,6 +870,16 @@
apply (blast intro: order_antisym)+
done
+lemma Least_mono:
+ "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
+ ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
+ -- {* Courtesy of Stephan Merz *}
+ apply clarify
+ apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
+ apply (rule LeastI2_order)
+ apply (auto elim: monoD intro!: order_antisym)
+ done
+
lemma Least_equality:
"[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
apply (simp add: Least_def)
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Jul 20 14:28:25 2007 +0200
@@ -74,10 +74,10 @@
| Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
| Const("Not",_) $ (Const ("op =",_)$y$_) =>
if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
-| Const ("Orderings.ord_class.less",_)$y$z =>
+| Const (@{const_name HOL.less}, _) $ y$ z =>
if term_of x aconv y then Lt (Thm.dest_arg ct)
else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
-| Const ("Orderings.ord_class.less_eq",_)$y$z =>
+| Const (@{const_name HOL.less_eq}, _) $ y $ z =>
if term_of x aconv y then Le (Thm.dest_arg ct)
else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
| Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_) =>
@@ -222,10 +222,10 @@
end
| _ => addC$(mulC$one$tm)$zero;
-fun lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less",T)$s$t)) =
- lin vs (Const("Orderings.ord_class.less_eq",T)$t$s)
- | lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less_eq",T)$s$t)) =
- lin vs (Const("Orderings.ord_class.less",T)$t$s)
+fun lin (vs as x::_) (Const("Not", _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) =
+ lin vs (Const(@{const_name HOL.less_eq}, T) $ t $ s)
+ | lin (vs as x::_) (Const("Not",_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) =
+ lin vs (Const(@{const_name HOL.less}, T) $ t $ s)
| lin vs (Const ("Not",T)$t) = Const ("Not",T)$ (lin vs t)
| lin (vs as x::_) (Const(@{const_name Divides.dvd},_)$d$t) =
HOLogic.mk_binrel @{const_name Divides.dvd} (numeral1 abs d, lint vs t)
@@ -298,12 +298,12 @@
fun h (acc,dacc) t =
case (term_of t) of
Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ =>
- if x aconv y
- andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"]
+ if x aconv y andalso member (op =)
+ ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
| Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) =>
- if x aconv y
- andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"]
+ if x aconv y andalso member (op =)
+ [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
| Const(@{const_name Divides.dvd},_)$_$(Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_) =>
if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
@@ -338,10 +338,12 @@
| Const("op |",_)$_$_ => binop_conv unit_conv t
| Const("Not",_)$_ => arg_conv unit_conv t
| Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ =>
- if x=y andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"]
+ if x=y andalso member (op =)
+ ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
| Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) =>
- if x=y andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"]
+ if x=y andalso member (op =)
+ [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
| Const(@{const_name Divides.dvd},_)$d$(r as (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_)) =>
if x=y then
@@ -559,8 +561,8 @@
fun qf_of_term ps vs t = case t
of Const("True",_) => T
| Const("False",_) => F
- | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
- | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
+ | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
+ | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
| Const(@{const_name Divides.dvd},_)$t1$t2 =>
(Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
| @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
--- a/src/HOL/Tools/function_package/lexicographic_order.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML Fri Jul 20 14:28:25 2007 +0200
@@ -130,13 +130,13 @@
fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
let
val goals = mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
- val less_thm = goals "Orderings.ord_class.less" |> prove thy solve_tac
+ val less_thm = goals @{const_name HOL.less} |> prove thy solve_tac
in
if Thm.no_prems less_thm then
Less (Goal.finish less_thm)
else
let
- val lesseq_thm = goals "Orderings.ord_class.less_eq" |> prove thy solve_tac
+ val lesseq_thm = goals @{const_name HOL.less_eq} |> prove thy solve_tac
in
if Thm.no_prems lesseq_thm then
LessEq (Goal.finish lesseq_thm, less_thm)
--- a/src/HOL/Tools/inductive_package.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML Fri Jul 20 14:28:25 2007 +0200
@@ -181,7 +181,7 @@
case concl of
Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
| _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
- | _ $ (Const ("Orderings.ord_class.less_eq", _) $ _ $ _) =>
+ | _ $ (Const ("HOL.ord_class.less_eq", _) $ _ $ _) =>
[dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac [le_funI, le_boolI'])) thm))]
| _ => [thm]
@@ -554,7 +554,7 @@
(make_bool_args HOLogic.mk_not I bs i)) preds));
val ind_concl = HOLogic.mk_Trueprop
- (HOLogic.mk_binrel "Orderings.ord_class.less_eq" (rec_const, ind_pred));
+ (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
--- a/src/HOL/Tools/refute.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Tools/refute.ML Fri Jul 20 14:28:25 2007 +0200
@@ -696,7 +696,7 @@
| Const ("Finite_Set.card", _) => t
| Const ("Finite_Set.Finites", _) => t
| Const ("Finite_Set.finite", _) => t
- | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
+ | Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
| Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
@@ -883,7 +883,7 @@
| Const ("Finite_Set.card", T) => collect_type_axioms (axs, T)
| Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
| Const ("Finite_Set.finite", T) => collect_type_axioms (axs, T)
- | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
+ | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
collect_type_axioms (axs, T)
| Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []),
@@ -2602,13 +2602,13 @@
(* theory -> model -> arguments -> Term.term ->
(interpretation * model * arguments) option *)
- (* only an optimization: 'Orderings.less' could in principle be *)
+ (* only an optimization: 'HOL.less' could in principle be *)
(* interpreted with interpreters available already (using its definition), *)
(* but the code below is more efficient *)
fun Nat_less_interpreter thy model args t =
case t of
- Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
+ Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
let
val (i_nat, _, _) = interpret thy model
--- a/src/HOL/Tools/res_clause.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Tools/res_clause.ML Fri Jul 20 14:28:25 2007 +0200
@@ -89,8 +89,8 @@
(*Provide readable names for the more common symbolic functions*)
val const_trans_table =
Symtab.make [("op =", "equal"),
- (@{const_name Orderings.less_eq}, "lessequals"),
- (@{const_name Orderings.less}, "less"),
+ (@{const_name HOL.less_eq}, "lessequals"),
+ (@{const_name HOL.less}, "less"),
("op &", "and"),
("op |", "or"),
(@{const_name HOL.plus}, "plus"),
--- a/src/HOL/arith_data.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/arith_data.ML Fri Jul 20 14:28:25 2007 +0200
@@ -107,8 +107,8 @@
structure LessCancelSums = CancelSumsFun
(struct
open Sum;
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
end);
@@ -117,8 +117,8 @@
structure LeCancelSums = CancelSumsFun
(struct
open Sum;
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
end);
@@ -370,8 +370,8 @@
val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
in
case rel of
- @{const_name Orderings.less} => SOME (p, i, "<", q, j)
- | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
+ @{const_name HOL.less} => SOME (p, i, "<", q, j)
+ | @{const_name HOL.less_eq} => SOME (p, i, "<=", q, j)
| "op =" => SOME (p, i, "=", q, j)
| _ => NONE
end handle Zero => NONE;
@@ -523,7 +523,7 @@
val rev_terms = rev terms
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
val terms2 = map (subst_term [(split_term, t2)]) rev_terms
- val t1_leq_t2 = Const (@{const_name Orderings.less_eq},
+ val t1_leq_t2 = Const (@{const_name HOL.less_eq},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -538,7 +538,7 @@
val rev_terms = rev terms
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
val terms2 = map (subst_term [(split_term, t2)]) rev_terms
- val t1_leq_t2 = Const (@{const_name Orderings.less_eq},
+ val t1_leq_t2 = Const (@{const_name HOL.less_eq},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -555,9 +555,9 @@
val terms2 = map (subst_term [(split_term, Const (@{const_name HOL.uminus},
split_type --> split_type) $ t1)]) rev_terms
val zero = Const (@{const_name HOL.zero}, split_type)
- val zero_leq_t1 = Const (@{const_name Orderings.less_eq},
+ val zero_leq_t1 = Const (@{const_name HOL.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ t1
- val t1_lt_zero = Const (@{const_name Orderings.less},
+ val t1_lt_zero = Const (@{const_name HOL.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
@@ -578,7 +578,7 @@
(map (incr_boundvars 1) rev_terms)
val t1' = incr_boundvars 1 t1
val t2' = incr_boundvars 1 t2
- val t1_lt_t2 = Const (@{const_name Orderings.less},
+ val t1_lt_t2 = Const (@{const_name HOL.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name HOL.plus},
@@ -602,7 +602,7 @@
val t1' = incr_boundvars 1 t1
val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
(Const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) $ n)
- val t1_lt_zero = Const (@{const_name Orderings.less},
+ val t1_lt_zero = Const (@{const_name HOL.less},
HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
@@ -628,7 +628,7 @@
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val t2_neq_zero = HOLogic.mk_not (Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
- val j_lt_t2 = Const (@{const_name Orderings.less},
+ val j_lt_t2 = Const (@{const_name HOL.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
@@ -660,7 +660,7 @@
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val t2_neq_zero = HOLogic.mk_not (Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
- val j_lt_t2 = Const (@{const_name Orderings.less},
+ val j_lt_t2 = Const (@{const_name HOL.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
@@ -697,18 +697,18 @@
(number_of $
(Const (@{const_name HOL.uminus},
HOLogic.intT --> HOLogic.intT) $ k'))
- val zero_leq_j = Const (@{const_name Orderings.less_eq},
+ val zero_leq_j = Const (@{const_name HOL.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ j
- val j_lt_t2 = Const (@{const_name Orderings.less},
+ val j_lt_t2 = Const (@{const_name HOL.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name HOL.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
- val t2_lt_j = Const (@{const_name Orderings.less},
+ val t2_lt_j = Const (@{const_name HOL.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val j_leq_zero = Const (@{const_name Orderings.less_eq},
+ val j_leq_zero = Const (@{const_name HOL.less_eq},
split_type --> split_type --> HOLogic.boolT) $ j $ zero
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
@@ -749,9 +749,9 @@
(number_of $
(Const (@{const_name HOL.uminus},
HOLogic.intT --> HOLogic.intT) $ k'))
- val zero_leq_j = Const (@{const_name Orderings.less_eq},
+ val zero_leq_j = Const (@{const_name HOL.less_eq},
split_type --> split_type --> HOLogic.boolT) $ zero $ j
- val j_lt_t2 = Const (@{const_name Orderings.less},
+ val j_lt_t2 = Const (@{const_name HOL.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =",
split_type --> split_type --> HOLogic.boolT) $ t1' $
@@ -759,9 +759,9 @@
(Const (@{const_name HOL.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
- val t2_lt_j = Const (@{const_name Orderings.less},
+ val t2_lt_j = Const (@{const_name HOL.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val j_leq_zero = Const (@{const_name Orderings.less_eq},
+ val j_leq_zero = Const (@{const_name HOL.less_eq},
split_type --> split_type --> HOLogic.boolT) $ j $ zero
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
@@ -1011,24 +1011,24 @@
val r = #prop(rep_thm thm);
in
case r of
- Tr $ ((c as Const(@{const_name Orderings.less_eq},T)) $ s $ t) =>
+ Tr $ ((c as Const(@{const_name HOL.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(@{const_name Orderings.less},T) $ s $ t))
+ let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.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(@{const_name Orderings.less},T) $ s $ t)) =>
- let val r' = Tr $ (Const(@{const_name Orderings.less_eq},T) $ s $ t)
+ | Tr $ (Const("Not",_) $ (Const(@{const_name HOL.less},T) $ s $ t)) =>
+ let val r' = Tr $ (Const(@{const_name HOL.less_eq},T) $ s $ t)
in
case Library.find_first (prp r') prems of
NONE =>
- let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name Orderings.less},T) $ t $ s))
+ let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ t $ s))
in case Library.find_first (prp r') prems of
NONE => []
| SOME thm' =>
--- a/src/HOL/ex/coopereif.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/ex/coopereif.ML Fri Jul 20 14:28:25 2007 +0200
@@ -32,8 +32,8 @@
fun qf_of_term ps vs t = case t
of Const("True",_) => T
| Const("False",_) => F
- | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
- | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
+ | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
+ | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
| Const(@{const_name "Divides.dvd"},_)$t1$t2 =>
(Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd")
| @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
--- a/src/HOL/ex/svc_funcs.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/ex/svc_funcs.ML Fri Jul 20 14:28:25 2007 +0200
@@ -112,8 +112,8 @@
b1 orelse b2)
end
else (*might be numeric equality*) (t, is_intnat T)
- | Const(@{const_name Orderings.less}, Type ("fun", [T,_])) => (t, is_intnat T)
- | Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
+ | Const(@{const_name HOL.less}, Type ("fun", [T,_])) => (t, is_intnat T)
+ | Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
| _ => (t, false)
end
in #1 o tag end;
@@ -216,13 +216,13 @@
else fail t
end
(*inequalities: possible types are nat, int, real*)
- | fm pos (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name HOL.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(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name HOL.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
--- a/src/HOL/ex/svc_oracle.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/ex/svc_oracle.ML Fri Jul 20 14:28:25 2007 +0200
@@ -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(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
- | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const(@{const_name HOL.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const(@{const_name HOL.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/int_arith1.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/int_arith1.ML Fri Jul 20 14:28:25 2007 +0200
@@ -110,8 +110,8 @@
mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
(*reorientation simprules using ==, for the following simproc*)
- val meta_zero_reorient = zero_reorient RS eq_reflection
- val meta_one_reorient = one_reorient RS eq_reflection
+ val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
+ val meta_one_reorient = @{thm one_reorient} RS eq_reflection
val meta_number_of_reorient = number_of_reorient RS eq_reflection
(*reorientation simplification procedure: reorients (polymorphic)
@@ -350,9 +350,9 @@
val trans_tac = fn _ => trans_tac
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
- diff_simps @ minus_simps @ add_ac
+ diff_simps @ minus_simps @ @{thms add_ac}
val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
- val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
+ val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -376,8 +376,8 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
val bal_add1 = less_add_iff1 RS trans
val bal_add2 = less_add_iff2 RS trans
);
@@ -385,8 +385,8 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
val bal_add1 = le_add_iff1 RS trans
val bal_add2 = le_add_iff2 RS trans
);
@@ -433,9 +433,9 @@
val trans_tac = fn _ => trans_tac
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
- diff_simps @ minus_simps @ add_ac
+ diff_simps @ minus_simps @ @{thms add_ac}
val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
- val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
+ val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -463,9 +463,9 @@
val trans_tac = fn _ => trans_tac
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
- inverse_1s @ divide_simps @ diff_simps @ minus_simps @ add_ac
+ inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac}
val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
- val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
+ val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -541,7 +541,7 @@
structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
struct
- val assoc_ss = HOL_ss addsimps mult_ac
+ val assoc_ss = HOL_ss addsimps @{thms mult_ac}
val eq_reflection = eq_reflection
end;
--- a/src/HOL/int_factor_simprocs.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/int_factor_simprocs.ML Fri Jul 20 14:28:25 2007 +0200
@@ -33,7 +33,7 @@
val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
- val norm_ss3 = HOL_ss addsimps mult_ac
+ val norm_ss3 = HOL_ss addsimps @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -78,8 +78,8 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
val cancel = @{thm mult_less_cancel_left} RS trans
val neg_exchanges = true
)
@@ -87,8 +87,8 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
val cancel = @{thm mult_le_cancel_left} RS trans
val neg_exchanges = true
)
@@ -216,7 +216,7 @@
(** Final simplification for the CancelFactor simprocs **)
val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq
- [@{thm mult_1_left}, mult_1_right, @{thm zdiv_1}, numeral_1_eq_1];
+ [@{thm mult_1_left}, @{thm mult_1_right}, @{thm zdiv_1}, numeral_1_eq_1];
fun cancel_simplify_meta_eq cancel_th ss th =
simplify_one ss (([th, cancel_th]) MRS trans);
@@ -229,7 +229,7 @@
val dest_coeff = dest_coeff
val find_first = find_first_t []
val trans_tac = fn _ => trans_tac
- val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
+ val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
end;
--- a/src/HOL/nat_simprocs.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/nat_simprocs.ML Fri Jul 20 14:28:25 2007 +0200
@@ -125,15 +125,15 @@
(*Simplify 1*n and n*1 to n*)
-val add_0s = map rename_numerals [add_0, add_0_right];
+val add_0s = map rename_numerals [@{thm add_0}, @{thm add_0_right}];
val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
(*And these help the simproc return False when appropriate, which helps
the arith prover.*)
-val contra_rules = [add_Suc, add_Suc_right, Zero_not_Suc, Suc_not_Zero,
- le_0_eq];
+val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc},
+ @{thm Suc_not_Zero}, @{thm le_0_eq}];
val simplify_meta_eq =
Int_Numeral_Simprocs.simplify_meta_eq
@@ -157,8 +157,8 @@
val trans_tac = fn _ => trans_tac
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
- [@{thm Suc_eq_add_numeral_1_left}] @ add_ac
- val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
+ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
+ val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -181,8 +181,8 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
val bal_add1 = @{thm nat_less_add_iff1} RS trans
val bal_add2 = @{thm nat_less_add_iff2} RS trans
);
@@ -190,8 +190,8 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
val bal_add1 = @{thm nat_le_add_iff1} RS trans
val bal_add2 = @{thm nat_le_add_iff2} RS trans
);
@@ -245,8 +245,8 @@
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv_nohyps
val trans_tac = fn _ => trans_tac
- val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ add_ac
- val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
+ val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
+ val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -271,8 +271,8 @@
val trans_tac = fn _ => trans_tac
val norm_ss1 = num_ss addsimps
- numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ add_ac
- val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
+ numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
+ val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -303,8 +303,8 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
val cancel = @{thm nat_mult_less_cancel1} RS trans
val neg_exchanges = true
)
@@ -312,8 +312,8 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
val cancel = @{thm nat_mult_le_cancel1} RS trans
val neg_exchanges = true
)
@@ -363,7 +363,7 @@
val dest_coeff = dest_coeff
val find_first = find_first_t []
val trans_tac = fn _ => trans_tac
- val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
+ val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
end;
@@ -378,16 +378,16 @@
structure LessCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
);
structure LeCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
+ val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
);