# HG changeset patch # User berghofe # Date 1265817940 -3600 # Node ID 7722bcb5c37c799bf486466ce5060a7b81f8c8e2 # Parent 4554bb2abfa3871cde6c6bac9278376d2619a3b2# Parent 45dec8e27c4b935967f8809f97cffefbc057bd4d merged diff -r 45dec8e27c4b -r 7722bcb5c37c NEWS --- a/NEWS Wed Feb 10 17:05:18 2010 +0100 +++ b/NEWS Wed Feb 10 17:05:40 2010 +0100 @@ -22,6 +22,8 @@ * Some generic constants have been put to appropriate theories: + less_eq, less: Orderings + abs, sgn: Groups inverse, divide: Rings INCOMPATIBILITY. @@ -80,13 +82,9 @@ INCOMPATIBILITY. -* Index syntax for structures must be imported explicitly from library -theory Structure_Syntax. INCOMPATIBILITY. - * New theory Algebras contains generic algebraic structures and generic algebraic operations. INCOMPATIBILTY: constants zero, one, -plus, minus, uminus, times, abs, sgn, less_eq and -less have been moved from HOL.thy to Algebras.thy. +plus, minus, uminus and times have been moved from HOL.thy to Algebras.thy. * HOLogic.strip_psplit: types are returned in syntactic order, similar to other strip and tuple operations. INCOMPATIBILITY. diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Algebras.thy --- a/src/HOL/Algebras.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Algebras.thy Wed Feb 10 17:05:40 2010 +0100 @@ -55,7 +55,7 @@ end -subsection {* Generic algebraic operations *} +subsection {* Generic syntactic operations *} class zero = fixes zero :: 'a ("0") @@ -63,6 +63,13 @@ class one = fixes one :: 'a ("1") +hide (open) const zero one + +syntax + "_index1" :: index ("\<^sub>1") +translations + (index) "\<^sub>1" => (index) "\<^bsub>\\<^esub>" + lemma Let_0 [simp]: "Let 0 f = f 0" unfolding Let_def .. @@ -89,8 +96,6 @@ in map tr' [@{const_syntax Algebras.one}, @{const_syntax Algebras.zero}] end; *} -- {* show types that are presumably too general *} -hide (open) const zero one - class plus = fixes plus :: "'a \ 'a \ 'a" (infixl "+" 65) @@ -103,51 +108,4 @@ class times = fixes times :: "'a \ 'a \ 'a" (infixl "*" 70) -class abs = - fixes abs :: "'a \ 'a" -begin - -notation (xsymbols) - abs ("\_\") - -notation (HTML output) - abs ("\_\") - -end - -class sgn = - fixes sgn :: "'a \ 'a" - -class ord = - fixes less_eq :: "'a \ 'a \ bool" - and less :: "'a \ 'a \ bool" -begin - -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_eq (infix ">=" 50) where - "x >= y \ y <= x" - -notation (input) - greater_eq (infix "\" 50) - -abbreviation (input) - greater (infix ">" 50) where - "x > y \ y < x" - -end - end \ No newline at end of file diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Feb 10 17:05:40 2010 +0100 @@ -684,7 +684,7 @@ fun xnormalize_conv ctxt [] ct = reflexive ct | xnormalize_conv ctxt (vs as (x::_)) ct = case term_of ct of - Const(@{const_name Algebras.less},_)$_$Const(@{const_name Algebras.zero},_) => + Const(@{const_name Orderings.less},_)$_$Const(@{const_name Algebras.zero},_) => (case whatis x (Thm.dest_arg1 ct) of ("c*x+t",[c,t]) => let @@ -727,7 +727,7 @@ | _ => reflexive ct) -| Const(@{const_name Algebras.less_eq},_)$_$Const(@{const_name Algebras.zero},_) => +| Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Algebras.zero},_) => (case whatis x (Thm.dest_arg1 ct) of ("c*x+t",[c,t]) => let @@ -816,7 +816,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 Algebras.less},_)$a$b => + Const(@{const_name Orderings.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 @@ -825,7 +825,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 Algebras.less_eq},_)$a$b => +| Const(@{const_name Orderings.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 @@ -856,11 +856,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 Algebras.less},_)$y$z => + | Const(@{const_name Orderings.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 Algebras.less_eq},_)$y$z => + | Const (@{const_name Orderings.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 45dec8e27c4b -r 7722bcb5c37c src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 10 17:05:40 2010 +0100 @@ -2958,8 +2958,8 @@ val disjt = @{term "op |"}; val impt = @{term "op -->"}; val ifft = @{term "op = :: bool => _"} -fun llt rT = Const(@{const_name Algebras.less},rrT rT); -fun lle rT = Const(@{const_name Algebras.less},rrT rT); +fun llt rT = Const(@{const_name Orderings.less},rrT rT); +fun lle rT = Const(@{const_name Orderings.less},rrT rT); fun eqt rT = Const("op =",rrT rT); fun rz rT = Const(@{const_name Algebras.zero},rT); @@ -3024,9 +3024,9 @@ | Const("op =",ty)$p$q => if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q) else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q)) - | Const(@{const_name Algebras.less},_)$p$q => + | Const(@{const_name Orderings.less},_)$p$q => @{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q)) - | Const(@{const_name Algebras.less_eq},_)$p$q => + | Const(@{const_name Orderings.less_eq},_)$p$q => @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q)) | Const("Ex",_)$Abs(xn,xT,p) => let val (xn', p') = variant_abs (xn,xT,p) diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Fields.thy --- a/src/HOL/Fields.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Fields.thy Wed Feb 10 17:05:40 2010 +0100 @@ -1035,6 +1035,31 @@ apply (simp add: order_less_imp_le) done + +lemma field_le_epsilon: + fixes x y :: "'a :: {division_by_zero,linordered_field}" + assumes e: "\e. 0 < e \ x \ y + e" + shows "x \ y" +proof (rule ccontr) + obtain two :: 'a where two: "two = 1 + 1" by simp + assume "\ x \ y" + then have yx: "y < x" by simp + then have "y + - y < x + - y" by (rule add_strict_right_mono) + then have "x - y > 0" by (simp add: diff_minus) + then have "(x - y) / two > 0" + by (rule divide_pos_pos) (simp add: two) + then have "x \ y + (x - y) / two" by (rule e) + also have "... = (x - y + two * y) / two" + by (simp add: add_divide_distrib two) + also have "... = (x + y) / two" + by (simp add: two algebra_simps) + also have "... < x" using yx + by (simp add: two pos_divide_less_eq algebra_simps) + finally have "x < x" . + then show False .. +qed + + code_modulename SML Fields Arith diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Groebner_Basis.thy Wed Feb 10 17:05:40 2010 +0100 @@ -556,14 +556,14 @@ fun proc3 phi ss ct = (case term_of ct of - Const(@{const_name Algebras.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.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 Algebras.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => let val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop val _ = map is_number [a,b,c] @@ -577,14 +577,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 Algebras.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.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 Algebras.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => let val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop val _ = map is_number [a,b,c] diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Groups.thy --- a/src/HOL/Groups.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Groups.thy Wed Feb 10 17:05:40 2010 +0100 @@ -5,7 +5,7 @@ header {* Groups, also combined with orderings *} theory Groups -imports Lattices +imports Orderings uses "~~/src/Provers/Arith/abel_cancel.ML" begin @@ -40,6 +40,7 @@ Of course it also works for fields, but it knows nothing about multiplicative inverses or division. This is catered for by @{text field_simps}. *} + subsection {* Semigroups and Monoids *} class semigroup_add = plus + @@ -884,6 +885,32 @@ shows "[|0\a; b b < a + c" by (insert add_le_less_mono [of 0 a b c], simp) +class abs = + fixes abs :: "'a \ 'a" +begin + +notation (xsymbols) + abs ("\_\") + +notation (HTML output) + abs ("\_\") + +end + +class sgn = + fixes sgn :: "'a \ 'a" + +class abs_if = minus + uminus + ord + zero + abs + + assumes abs_if: "\a\ = (if a < 0 then - a else a)" + +class sgn_if = minus + uminus + zero + one + ord + sgn + + assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)" +begin + +lemma sgn0 [simp]: "sgn 0 = 0" + by (simp add:sgn_if) + +end class ordered_ab_group_add_abs = ordered_ab_group_add + abs + assumes abs_ge_zero [simp]: "\a\ \ 0" diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Hoare/hoare_tac.ML Wed Feb 10 17:05:40 2010 +0100 @@ -58,7 +58,7 @@ let val T as Type ("fun",[t,_]) = fastype_of trm in Collect_const t $ trm end; -fun inclt ty = Const (@{const_name Algebras.less_eq}, [ty,ty] ---> boolT); +fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT); fun Mset ctxt prop = diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Wed Feb 10 17:05:40 2010 +0100 @@ -166,7 +166,7 @@ import_theory prim_rec; const_maps - "<" > Algebras.less :: "[nat,nat]=>bool"; + "<" > Orderings.less :: "[nat,nat]=>bool"; end_import; @@ -181,7 +181,7 @@ ">" > HOL4Compat.nat_gt ">=" > HOL4Compat.nat_ge FUNPOW > HOL4Compat.FUNPOW - "<=" > Algebras.less_eq :: "[nat,nat]=>bool" + "<=" > Orderings.less_eq :: "[nat,nat]=>bool" "+" > Algebras.plus :: "[nat,nat]=>nat" "*" > Algebras.times :: "[nat,nat]=>nat" "-" > Algebras.minus :: "[nat,nat]=>nat" diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Import/Generate-HOL/GenHOL4Real.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Wed Feb 10 17:05:40 2010 +0100 @@ -22,7 +22,7 @@ inv > Algebras.inverse :: "real => real" real_add > Algebras.plus :: "[real,real] => real" real_mul > Algebras.times :: "[real,real] => real" - real_lt > Algebras.less :: "[real,real] => bool"; + real_lt > Orderings.less :: "[real,real] => bool"; ignore_thms real_TY_DEF @@ -50,11 +50,11 @@ const_maps real_gt > HOL4Compat.real_gt real_ge > HOL4Compat.real_ge - real_lte > Algebras.less_eq :: "[real,real] => bool" + real_lte > Orderings.less_eq :: "[real,real] => bool" real_sub > Algebras.minus :: "[real,real] => real" "/" > Algebras.divide :: "[real,real] => real" pow > Power.power :: "[real,nat] => real" - abs > Algebras.abs :: "real => real" + abs > Groups.abs :: "real => real" real_of_num > RealDef.real :: "nat => real"; end_import; diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Import/HOL/arithmetic.imp --- a/src/HOL/Import/HOL/arithmetic.imp Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Import/HOL/arithmetic.imp Wed Feb 10 17:05:40 2010 +0100 @@ -23,7 +23,7 @@ "ALT_ZERO" > "HOL4Compat.ALT_ZERO" ">=" > "HOL4Compat.nat_ge" ">" > "HOL4Compat.nat_gt" - "<=" > "Algebras.ord_class.less_eq" :: "nat => nat => bool" + "<=" > "Orderings.less_eq" :: "nat => nat => bool" "-" > "Algebras.minus_class.minus" :: "nat => nat => nat" "+" > "Algebras.plus_class.plus" :: "nat => nat => nat" "*" > "Algebras.times_class.times" :: "nat => nat => nat" diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Import/HOL/prim_rec.imp --- a/src/HOL/Import/HOL/prim_rec.imp Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Import/HOL/prim_rec.imp Wed Feb 10 17:05:40 2010 +0100 @@ -18,7 +18,7 @@ "PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN" "PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC" "PRE" > "HOL4Base.prim_rec.PRE" - "<" > "Algebras.less" :: "nat => nat => bool" + "<" > "Orderings.less" :: "nat => nat => bool" thm_maps "wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef" diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Import/HOL/real.imp --- a/src/HOL/Import/HOL/real.imp Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Import/HOL/real.imp Wed Feb 10 17:05:40 2010 +0100 @@ -12,11 +12,11 @@ "sum" > "HOL4Real.real.sum" "real_sub" > "Algebras.minus" :: "real => real => real" "real_of_num" > "RealDef.real" :: "nat => real" - "real_lte" > "Algebras.less_eq" :: "real => real => bool" + "real_lte" > "Orderings.less_eq" :: "real => real => bool" "real_gt" > "HOL4Compat.real_gt" "real_ge" > "HOL4Compat.real_ge" "pow" > "Power.power_class.power" :: "real => nat => real" - "abs" > "Algebras.abs" :: "real => real" + "abs" > "Groups.abs" :: "real => real" "/" > "Ring.divide" :: "real => real => real" thm_maps diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Import/HOL/realax.imp --- a/src/HOL/Import/HOL/realax.imp Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Import/HOL/realax.imp Wed Feb 10 17:05:40 2010 +0100 @@ -29,7 +29,7 @@ "treal_0" > "HOL4Real.realax.treal_0" "real_neg" > "Algebras.uminus_class.uminus" :: "real => real" "real_mul" > "Algebras.times_class.times" :: "real => real => real" - "real_lt" > "Algebras.ord_class.less" :: "real => real => bool" + "real_lt" > "Orderings.less" :: "real => real => bool" "real_add" > "Algebras.plus_class.plus" :: "real => real => real" "real_1" > "Algebras.one_class.one" :: "real" "real_0" > "Algebras.zero_class.zero" :: "real" diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/IsaMakefile Wed Feb 10 17:05:40 2010 +0100 @@ -397,7 +397,6 @@ Library/Library/document/root.tex Library/Library/document/root.bib \ Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \ Library/Product_ord.thy Library/Char_nat.thy \ - Library/Structure_Syntax.thy \ Library/Sublist_Order.thy Library/List_lexord.thy \ Library/Coinductive_List.thy Library/AssocList.thy \ Library/Formal_Power_Series.thy Library/Binomial.thy \ diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Library/Library.thy Wed Feb 10 17:05:40 2010 +0100 @@ -51,7 +51,6 @@ RBT SML_Quickcheck State_Monad - Structure_Syntax Sum_Of_Squares Transitive_Closure_Table Univ_Poly diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Library/Structure_Syntax.thy --- a/src/HOL/Library/Structure_Syntax.thy Wed Feb 10 17:05:18 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* Author: Florian Haftmann, TU Muenchen *) - -header {* Index syntax for structures *} - -theory Structure_Syntax -imports Pure -begin - -syntax - "_index1" :: index ("\<^sub>1") -translations - (index) "\<^sub>1" => (index) "\<^bsub>\\<^esub>" - -end diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Metis_Examples/Message.thy --- a/src/HOL/Metis_Examples/Message.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Metis_Examples/Message.thy Wed Feb 10 17:05:40 2010 +0100 @@ -252,7 +252,7 @@ declare [[ atp_problem_prefix = "Message__parts_cut" ]] lemma parts_cut: "[|Y\ parts(insert X G); X\ parts H|] ==> Y\ parts(G \ H)" -by (metis Un_subset_iff insert_subset parts_increasing parts_trans) +by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI) @@ -698,13 +698,12 @@ apply (rule subsetI) apply (erule analz.induct) apply (metis UnCI UnE Un_commute analz.Inj) -apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Fst analz_increasing analz_mono insert_absorb insert_subset) -apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Snd analz_increasing analz_mono insert_absorb insert_subset) +apply (metis MPair_synth UnCI UnE Un_commute analz.Fst analz.Inj mem_def) +apply (metis MPair_synth UnCI UnE Un_commute analz.Inj analz.Snd mem_def) apply (blast intro: analz.Decrypt) apply blast done - declare [[ atp_problem_prefix = "Message__analz_synth" ]] lemma analz_synth [simp]: "analz (synth H) = analz H \ synth H" proof (neg_clausify) diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Metis_Examples/TransClosure.thy --- a/src/HOL/Metis_Examples/TransClosure.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Metis_Examples/TransClosure.thy Wed Feb 10 17:05:40 2010 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/MetisTest/TransClosure.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Testing the metis method diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Mutabelle/Mutabelle.thy --- a/src/HOL/Mutabelle/Mutabelle.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Mutabelle/Mutabelle.thy Wed Feb 10 17:05:40 2010 +0100 @@ -16,7 +16,7 @@ (@{const_name dummy_pattern}, "'a::{}"), (@{const_name Algebras.uminus}, "'a"), (@{const_name Nat.size}, "'a"), - (@{const_name Algebras.abs}, "'a")]; + (@{const_name Groups.abs}, "'a")]; val forbidden_thms = ["finite_intvl_succ_class", diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed Feb 10 17:05:40 2010 +0100 @@ -197,7 +197,7 @@ (@{const_name "dummy_pattern"}, "'a::{}") (*, (@{const_name "uminus"}, "'a"), (@{const_name "Nat.size"}, "'a"), - (@{const_name "Algebras.abs"}, "'a") *)] + (@{const_name "Groups.abs"}, "'a") *)] val forbidden_thms = ["finite_intvl_succ_class", diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Orderings.thy Wed Feb 10 17:05:40 2010 +0100 @@ -11,6 +11,41 @@ "~~/src/Provers/quasi.ML" (* FIXME unused? *) begin +subsection {* Syntactic orders *} + +class ord = + fixes less_eq :: "'a \ 'a \ bool" + and less :: "'a \ 'a \ bool" +begin + +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_eq (infix ">=" 50) where + "x >= y \ y <= x" + +notation (input) + greater_eq (infix "\" 50) + +abbreviation (input) + greater (infix ">" 50) where + "x > y \ y < x" + +end + + subsection {* Quasi orders *} class preorder = ord + diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Real.thy --- a/src/HOL/Real.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Real.thy Wed Feb 10 17:05:40 2010 +0100 @@ -2,25 +2,4 @@ imports RComplete RealVector begin -lemma field_le_epsilon: - fixes x y :: "'a:: {number_ring,division_by_zero,linordered_field}" - assumes e: "(!!e. 0 < e ==> x \ y + e)" - shows "x \ y" -proof (rule ccontr) - assume xy: "\ x \ y" - hence "(x-y)/2 > 0" - by simp - hence "x \ y + (x - y) / 2" - by (rule e [of "(x-y)/2"]) - also have "... = (x - y + 2*y)/2" - by (simp add: diff_divide_distrib) - also have "... = (x + y) / 2" - by simp - also have "... < x" using xy - by simp - finally have "x b \ 0 \ c \ c * a \ c * b" @@ -782,15 +782,6 @@ end -class abs_if = minus + uminus + ord + zero + abs + - assumes abs_if: "\a\ = (if a < 0 then - a else a)" - -class sgn_if = minus + uminus + zero + one + ord + sgn + - assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)" - -lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0" -by(simp add:sgn_if) - class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if begin diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Wed Feb 10 17:05:40 2010 +0100 @@ -80,10 +80,10 @@ let val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs) in - case try_proof (goals @{const_name Algebras.less}) solve_tac of + case try_proof (goals @{const_name Orderings.less}) solve_tac of Solved thm => Less thm | Stuck thm => - (case try_proof (goals @{const_name Algebras.less_eq}) solve_tac of + (case try_proof (goals @{const_name Orderings.less_eq}) solve_tac of Solved thm2 => LessEq (thm2, thm) | Stuck thm2 => if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2 diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Tools/Function/termination.ML --- a/src/HOL/Tools/Function/termination.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Tools/Function/termination.ML Wed Feb 10 17:05:40 2010 +0100 @@ -203,10 +203,10 @@ HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"}) $ (m2 $ r) $ (m1 $ l)))))) tac in - case try @{const_name Algebras.less} of + case try @{const_name Orderings.less} of Solved thm => Less thm | Stuck thm => - (case try @{const_name Algebras.less_eq} of + (case try @{const_name Orderings.less_eq} of Solved thm2 => LessEq (thm2, thm) | Stuck thm2 => if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Feb 10 17:05:40 2010 +0100 @@ -223,7 +223,7 @@ @{const_name False}, @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat}, @{const_name Nat.one_nat_inst.one_nat}, - @{const_name Algebras.ord_class.less}, @{const_name Algebras.ord_class.less_eq}, + @{const_name Orderings.less}, @{const_name Orderings.less_eq}, @{const_name Algebras.zero}, @{const_name Algebras.one}, @{const_name Algebras.plus}, @{const_name Nat.ord_nat_inst.less_eq_nat}, diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Tools/Qelim/cooper.ML Wed Feb 10 17:05:40 2010 +0100 @@ -73,10 +73,10 @@ | Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox | Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) => if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox -| Const (@{const_name Algebras.less}, _) $ y$ z => +| Const (@{const_name Orderings.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 (@{const_name Algebras.less_eq}, _) $ y $ z => +| Const (@{const_name Orderings.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 Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_) => @@ -217,10 +217,10 @@ end | _ => addC $ (mulC $ one $ tm) $ zero; -fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Algebras.less}, T) $ s $ t)) = - lin vs (Const (@{const_name Algebras.less_eq}, T) $ t $ s) - | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Algebras.less_eq}, T) $ s $ t)) = - lin vs (Const (@{const_name Algebras.less}, T) $ t $ s) +fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Orderings.less}, T) $ s $ t)) = + lin vs (Const (@{const_name Orderings.less_eq}, T) $ t $ s) + | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Orderings.less_eq}, T) $ s $ t)) = + lin vs (Const (@{const_name Orderings.less}, T) $ t $ s) | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t) | lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) = HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t) @@ -295,11 +295,11 @@ case (term_of t) of Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ => if x aconv y andalso member (op =) - ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s + ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s then (ins (dest_numeral c) acc,dacc) else (acc,dacc) | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) => if x aconv y andalso member (op =) - [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s + [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s then (ins (dest_numeral c) acc, dacc) else (acc,dacc) | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_) => if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc) @@ -337,11 +337,11 @@ | Const (@{const_name Not},_)$_ => arg_conv unit_conv t | Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ => if x=y andalso member (op =) - ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s + ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s then cv (l div dest_numeral c) t else Thm.reflexive t | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) => if x=y andalso member (op =) - [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s + [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s then cv (l div dest_numeral c) t else Thm.reflexive t | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_)) => if x=y then @@ -560,8 +560,8 @@ fun qf_of_term ps vs t = case t of Const("True",_) => T | Const("False",_) => F - | Const(@{const_name Algebras.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2)) - | Const(@{const_name Algebras.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2)) + | 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 Rings.dvd},_)$t1$t2 => (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd") (* FIXME avoid handle _ *) | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2)) diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Tools/inductive.ML Wed Feb 10 17:05:40 2010 +0100 @@ -184,7 +184,7 @@ case concl_of thm of Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq) | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm - | _ $ (Const (@{const_name Algebras.less_eq}, _) $ _ $ _) => + | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) => dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm)) | _ => thm @@ -561,7 +561,7 @@ (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds)); val ind_concl = HOLogic.mk_Trueprop - (HOLogic.mk_binrel @{const_name Algebras.less_eq} (rec_const, ind_pred)); + (HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred)); val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct})); diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Tools/int_arith.ML Wed Feb 10 17:05:40 2010 +0100 @@ -55,7 +55,7 @@ @{const_name Algebras.times}, @{const_name Algebras.uminus}, @{const_name Algebras.minus}, @{const_name Algebras.plus}, @{const_name Algebras.zero}, - @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s + @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s | check (a $ b) = check a andalso check b | check _ = false; diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Tools/lin_arith.ML Wed Feb 10 17:05:40 2010 +0100 @@ -229,8 +229,8 @@ val (q, j) = poly (rhs, Rat.one, ([], Rat.zero)) in case rel of - @{const_name Algebras.less} => SOME (p, i, "<", q, j) - | @{const_name Algebras.less_eq} => SOME (p, i, "<=", q, j) + @{const_name Orderings.less} => SOME (p, i, "<", q, j) + | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j) | "op =" => SOME (p, i, "=", q, j) | _ => NONE end handle Rat.DIVZERO => NONE; @@ -292,7 +292,7 @@ case head_of lhs of Const (a, _) => member (op =) [@{const_name Orderings.max}, @{const_name Orderings.min}, - @{const_name Algebras.abs}, + @{const_name Groups.abs}, @{const_name Algebras.minus}, "Int.nat" (*DYNAMIC BINDING!*), "Divides.div_class.mod" (*DYNAMIC BINDING!*), @@ -372,7 +372,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 Algebras.less_eq}, + val t1_leq_t2 = Const (@{const_name Orderings.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) @@ -387,7 +387,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 Algebras.less_eq}, + val t1_leq_t2 = Const (@{const_name Orderings.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) @@ -397,16 +397,16 @@ SOME [(Ts, subgoal1), (Ts, subgoal2)] end (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *) - | (Const (@{const_name Algebras.abs}, _), [t1]) => + | (Const (@{const_name Groups.abs}, _), [t1]) => let val rev_terms = rev terms val terms1 = map (subst_term [(split_term, t1)]) rev_terms val terms2 = map (subst_term [(split_term, Const (@{const_name Algebras.uminus}, split_type --> split_type) $ t1)]) rev_terms val zero = Const (@{const_name Algebras.zero}, split_type) - val zero_leq_t1 = Const (@{const_name Algebras.less_eq}, + val zero_leq_t1 = Const (@{const_name Orderings.less_eq}, split_type --> split_type --> HOLogic.boolT) $ zero $ t1 - val t1_lt_zero = Const (@{const_name Algebras.less}, + val t1_lt_zero = Const (@{const_name Orderings.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] @@ -427,7 +427,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 Algebras.less}, + val t1_lt_t2 = Const (@{const_name Orderings.less}, split_type --> split_type --> HOLogic.boolT) $ t1 $ t2 val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const (@{const_name Algebras.plus}, @@ -451,7 +451,7 @@ val t1' = incr_boundvars 1 t1 val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $ (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n) - val t1_lt_zero = Const (@{const_name Algebras.less}, + val t1_lt_zero = Const (@{const_name Orderings.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_nat_n) :: terms1 @ [not_false] @@ -477,7 +477,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 Algebras.less}, + val j_lt_t2 = Const (@{const_name Orderings.less}, split_type --> split_type--> HOLogic.boolT) $ j $ t2' val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $ @@ -509,7 +509,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 Algebras.less}, + val j_lt_t2 = Const (@{const_name Orderings.less}, split_type --> split_type--> HOLogic.boolT) $ j $ t2' val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $ @@ -545,17 +545,17 @@ val t2' = incr_boundvars 2 t2 val t2_eq_zero = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero - val zero_lt_t2 = Const (@{const_name Algebras.less}, + val zero_lt_t2 = Const (@{const_name Orderings.less}, split_type --> split_type --> HOLogic.boolT) $ zero $ t2' - val t2_lt_zero = Const (@{const_name Algebras.less}, + val t2_lt_zero = Const (@{const_name Orderings.less}, split_type --> split_type --> HOLogic.boolT) $ t2' $ zero - val zero_leq_j = Const (@{const_name Algebras.less_eq}, + val zero_leq_j = Const (@{const_name Orderings.less_eq}, split_type --> split_type --> HOLogic.boolT) $ zero $ j - val j_leq_zero = Const (@{const_name Algebras.less_eq}, + val j_leq_zero = Const (@{const_name Orderings.less_eq}, split_type --> split_type --> HOLogic.boolT) $ j $ zero - val j_lt_t2 = Const (@{const_name Algebras.less}, + val j_lt_t2 = Const (@{const_name Orderings.less}, split_type --> split_type--> HOLogic.boolT) $ j $ t2' - val t2_lt_j = Const (@{const_name Algebras.less}, + val t2_lt_j = Const (@{const_name Orderings.less}, split_type --> split_type--> HOLogic.boolT) $ t2' $ j val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $ @@ -599,17 +599,17 @@ val t2' = incr_boundvars 2 t2 val t2_eq_zero = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero - val zero_lt_t2 = Const (@{const_name Algebras.less}, + val zero_lt_t2 = Const (@{const_name Orderings.less}, split_type --> split_type --> HOLogic.boolT) $ zero $ t2' - val t2_lt_zero = Const (@{const_name Algebras.less}, + val t2_lt_zero = Const (@{const_name Orderings.less}, split_type --> split_type --> HOLogic.boolT) $ t2' $ zero - val zero_leq_j = Const (@{const_name Algebras.less_eq}, + val zero_leq_j = Const (@{const_name Orderings.less_eq}, split_type --> split_type --> HOLogic.boolT) $ zero $ j - val j_leq_zero = Const (@{const_name Algebras.less_eq}, + val j_leq_zero = Const (@{const_name Orderings.less_eq}, split_type --> split_type --> HOLogic.boolT) $ j $ zero - val j_lt_t2 = Const (@{const_name Algebras.less}, + val j_lt_t2 = Const (@{const_name Orderings.less}, split_type --> split_type--> HOLogic.boolT) $ j $ t2' - val t2_lt_j = Const (@{const_name Algebras.less}, + val t2_lt_j = Const (@{const_name Orderings.less}, split_type --> split_type--> HOLogic.boolT) $ t2' $ j val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $ diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Tools/nat_arith.ML --- a/src/HOL/Tools/nat_arith.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Tools/nat_arith.ML Wed Feb 10 17:05:40 2010 +0100 @@ -69,16 +69,16 @@ structure LessCancelSums = CancelSumsFun (struct open CommonCancelSums; - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}; - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT; + val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}; + val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT; val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"}; end); structure LeCancelSums = CancelSumsFun (struct open CommonCancelSums; - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}; - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT; + 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 uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"}; end); diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Tools/nat_numeral_simprocs.ML --- a/src/HOL/Tools/nat_numeral_simprocs.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Wed Feb 10 17:05:40 2010 +0100 @@ -176,8 +176,8 @@ structure LessCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT + val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} + val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT val bal_add1 = @{thm nat_less_add_iff1} RS trans val bal_add2 = @{thm nat_less_add_iff2} RS trans ); @@ -185,8 +185,8 @@ structure LeCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT + 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 bal_add1 = @{thm nat_le_add_iff1} RS trans val bal_add2 = @{thm nat_le_add_iff2} RS trans ); @@ -308,8 +308,8 @@ structure LessCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT + val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} + val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT val cancel = @{thm nat_mult_less_cancel1} RS trans val neg_exchanges = true ) @@ -317,8 +317,8 @@ structure LeCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT + 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 cancel = @{thm nat_mult_le_cancel1} RS trans val neg_exchanges = true ) @@ -387,16 +387,16 @@ structure LessCancelFactor = ExtractCommonTermFun (open CancelFactorCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT + val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} + val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj} ); structure LeCancelFactor = ExtractCommonTermFun (open CancelFactorCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT + val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj} ); diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Tools/numeral_simprocs.ML Wed Feb 10 17:05:40 2010 +0100 @@ -229,8 +229,8 @@ structure LessCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT + val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} + val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT val bal_add1 = @{thm less_add_iff1} RS trans val bal_add2 = @{thm less_add_iff2} RS trans ); @@ -238,8 +238,8 @@ structure LeCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT + 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 bal_add1 = @{thm le_add_iff1} RS trans val bal_add2 = @{thm le_add_iff2} RS trans ); @@ -409,8 +409,8 @@ structure LessCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT + val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} + val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT val cancel = @{thm mult_less_cancel_left} RS trans val neg_exchanges = true ) @@ -418,8 +418,8 @@ structure LeCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT + 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 cancel = @{thm mult_le_cancel_left} RS trans val neg_exchanges = true ) @@ -485,7 +485,7 @@ fun sign_conv pos_th neg_th ss t = let val T = fastype_of t; val zero = Const(@{const_name Algebras.zero}, T); - val less = Const(@{const_name Algebras.less}, [T,T] ---> HOLogic.boolT); + val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT); val pos = less $ zero $ t and neg = less $ t $ zero fun prove p = Option.map Eq_True_elim (Lin_Arith.simproc ss p) @@ -524,8 +524,8 @@ structure LeCancelFactor = ExtractCommonTermFun (open CancelFactorCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT + 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 simp_conv = sign_conv @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg} ); @@ -534,8 +534,8 @@ structure LessCancelFactor = ExtractCommonTermFun (open CancelFactorCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT + val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} + val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT val simp_conv = sign_conv @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg} ); diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Tools/refute.ML Wed Feb 10 17:05:40 2010 +0100 @@ -708,7 +708,7 @@ (* other optimizations *) | Const (@{const_name Finite_Set.card}, _) => t | Const (@{const_name Finite_Set.finite}, _) => t - | Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []), + | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t | Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t @@ -883,7 +883,7 @@ | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs | Const (@{const_name Finite_Set.finite}, T) => collect_type_axioms T axs - | Const (@{const_name Algebras.less}, T as Type ("fun", [Type ("nat", []), + | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => collect_type_axioms T axs | Const (@{const_name Algebras.plus}, T as Type ("fun", [Type ("nat", []), @@ -2771,7 +2771,7 @@ fun Nat_less_interpreter thy model args t = case t of - Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []), + Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => let val size_of_nat = size_of_type thy model (Type ("nat", [])) diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/Tools/res_clause.ML Wed Feb 10 17:05:40 2010 +0100 @@ -99,7 +99,7 @@ (*Provide readable names for the more common symbolic functions*) val const_trans_table = Symtab.make [(@{const_name "op ="}, "equal"), - (@{const_name Algebras.less_eq}, "lessequals"), + (@{const_name Orderings.less_eq}, "lessequals"), (@{const_name "op &"}, "and"), (@{const_name "op |"}, "or"), (@{const_name "op -->"}, "implies"), diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/ex/SVC_Oracle.thy --- a/src/HOL/ex/SVC_Oracle.thy Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/ex/SVC_Oracle.thy Wed Feb 10 17:05:40 2010 +0100 @@ -95,8 +95,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 Algebras.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) - | fm (t as Const(@{const_name Algebras.less_eq}, 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 = replace t (*entry point, and abstraction of a meta-formula*) fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p) diff -r 45dec8e27c4b -r 7722bcb5c37c src/HOL/ex/svc_funcs.ML --- a/src/HOL/ex/svc_funcs.ML Wed Feb 10 17:05:18 2010 +0100 +++ b/src/HOL/ex/svc_funcs.ML Wed Feb 10 17:05:40 2010 +0100 @@ -107,8 +107,8 @@ b1 orelse b2) end else (*might be numeric equality*) (t, is_intnat T) - | Const(@{const_name Algebras.less}, Type ("fun", [T,_])) => (t, is_intnat T) - | Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) => (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) | _ => (t, false) end in #1 o tag end; @@ -211,13 +211,13 @@ else fail t end (*inequalities: possible types are nat, int, real*) - | fm pos (t as Const(@{const_name Algebras.less}, Type ("fun", [T,_])) $ x $ y) = + | fm pos (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ x $ y) = if not pos orelse T = HOLogic.realT then Buildin("<", [tm x, tm y]) else if is_intnat T then Buildin("<=", [suc (tm x), tm y]) else fail t - | fm pos (t as Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) $ x $ y) = + | fm pos (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ x $ y) = if pos orelse T = HOLogic.realT then Buildin("<=", [tm x, tm y]) else if is_intnat T then