# HG changeset patch # User haftmann # Date 1184934505 -7200 # Node ID 851c74f1bb696129f28a8775066a7605150b0978 # Parent 64b9806e160b81d13cd02cc3383556163fde7d2f moved class ord from Orderings.thy to HOL.thy diff -r 64b9806e160b -r 851c74f1bb69 NEWS --- 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 diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Arith_Tools.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 diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Complex/ex/linreif.ML --- 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 diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Complex/ex/mireif.ML --- 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 => diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Hoare/hoare.ML --- 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 diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Hoare/hoareAbort.ML --- 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 diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- 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" diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Import/Generate-HOL/GenHOL4Real.thy --- 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" diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Import/HOL/arithmetic.imp --- 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" diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Import/HOL/prim_rec.imp --- 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" diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Import/HOL/real.imp --- 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" diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Import/HOL/realax.imp --- 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" diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Library/sct.ML --- 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"] diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Orderings.thy --- 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 \ 'a \ bool" (infix "\" 50) - and less :: "'a \ 'a \ bool" (infix "\" 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>\") and - less_eq ("(_/ \<^loc>\ _)" [51, 51] 50) - -notation (HTML output) - less_eq ("op \<^loc>\") and - less_eq ("(_/ \<^loc>\ _)" [51, 51] 50) - -abbreviation (input) - greater (infix "\<^loc>>" 50) where - "x \<^loc>> y \ y \<^loc>< x" - -abbreviation (input) - greater_eq (infix "\<^loc>>=" 50) where - "x \<^loc>>= y \ y \<^loc><= x" - -notation (input) - greater_eq (infix "\<^loc>\" 50) - -text {* - syntactic min/max -- these definitions reach - their usual semantics in class linorder ahead. -*} - -definition - min :: "'a \ 'a \ 'a" where - "min a b = (if a \<^loc>\ b then a else b)" - -definition - max :: "'a \ 'a \ 'a" where - "max a b = (if a \<^loc>\ 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 \") and - less_eq ("(_/ \ _)" [51, 51] 50) - -notation (HTML output) - less_eq ("op \") and - less_eq ("(_/ \ _)" [51, 51] 50) - -abbreviation (input) - greater (infix ">" 50) where - "x > y \ y < x" - -abbreviation (input) - greater_eq (infix ">=" 50) where - "x >= y \ y <= x" - -notation (input) - greater_eq (infix "\" 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 \ 'a \ 'a" where + "min a b = (if a \<^loc>\ b then a else b)" + +definition (in ord) + max :: "'a \ 'a \ 'a" where + "max a b = (if a \<^loc>\ 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>\ z \ x \<^loc>\ z \ y \<^loc>\ 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 \ g \ \x. f x \ g x" + less_fun_def: "f < g \ f \ g \ f \ 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: "(\x. f x \ g x) \ f \ g" + unfolding le_fun_def by simp + +lemma le_funE: "f \ g \ (f x \ g x \ P) \ P" + unfolding le_fun_def by simp + +lemma le_funD: "f \ g \ f x \ g x" + unfolding le_fun_def by simp + +text {* + Handy introduction and elimination rules for @{text "\"} + on unary and binary predicates +*} + +lemma predicate1I [Pure.intro!, intro!]: + assumes PQ: "\x. P x \ Q x" + shows "P \ Q" + apply (rule le_funI) + apply (rule le_boolI) + apply (rule PQ) + apply assumption + done + +lemma predicate1D [Pure.dest, dest]: "P \ Q \ P x \ Q x" + apply (erule le_funE) + apply (erule le_boolE) + apply assumption+ + done + +lemma predicate2I [Pure.intro!, intro!]: + assumes PQ: "\x y. P x y \ Q x y" + shows "P \ Q" + apply (rule le_funI)+ + apply (rule le_boolI) + apply (rule PQ) + apply assumption + done + +lemma predicate2D [Pure.dest, dest]: "P \ Q \ P x y \ 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) diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Tools/Qelim/cooper.ML --- 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)) diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Tools/function_package/lexicographic_order.ML --- 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) diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Tools/inductive_package.ML --- 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)); diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Tools/refute.ML --- 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 diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Tools/res_clause.ML --- 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"), diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/arith_data.ML --- 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' => diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/ex/coopereif.ML --- 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)) diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/ex/svc_funcs.ML --- 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 diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/ex/svc_oracle.ML --- 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) diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/int_arith1.ML --- 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; diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/int_factor_simprocs.ML --- 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; diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/nat_simprocs.ML --- 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} );