# HG changeset patch # User haftmann # Date 1266587221 -3600 # Node ID 8dfd816713c662fd3ecbe7ffa053f8398d8d5c70 # Parent 07a56610c00bd49e2d1d54a8fb552f9175db829a moved remaning class operations from Algebras.thy to Groups.thy diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Algebra/abstract/Ring2.thy --- a/src/HOL/Algebra/abstract/Ring2.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Algebra/abstract/Ring2.thy Fri Feb 19 14:47:01 2010 +0100 @@ -205,8 +205,8 @@ ML {* fun ring_ord (Const (a, _)) = find_index (fn a' => a = a') - [@{const_name Algebras.zero}, @{const_name Algebras.plus}, @{const_name Algebras.uminus}, - @{const_name Algebras.minus}, @{const_name Algebras.one}, @{const_name Algebras.times}] + [@{const_name Groups.zero}, @{const_name Groups.plus}, @{const_name Groups.uminus}, + @{const_name Groups.minus}, @{const_name Groups.one}, @{const_name Groups.times}] | ring_ord _ = ~1; fun termless_ring (a, b) = (TermOrd.term_lpo ring_ord (a, b) = LESS); diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Algebras.thy --- a/src/HOL/Algebras.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Algebras.thy Fri Feb 19 14:47:01 2010 +0100 @@ -8,8 +8,6 @@ imports HOL begin -subsection {* Generic algebraic structures *} - text {* These locales provide basic structures for interpretation into bigger structures; extensions require careful thinking, otherwise @@ -54,58 +52,4 @@ end - -subsection {* Generic syntactic operations *} - -class zero = - fixes zero :: 'a ("0") - -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 .. - -lemma Let_1 [simp]: "Let 1 f = f 1" - unfolding Let_def .. - -setup {* - Reorient_Proc.add - (fn Const(@{const_name Algebras.zero}, _) => true - | Const(@{const_name Algebras.one}, _) => true - | _ => false) -*} - -simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc -simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc - -typed_print_translation {* -let - fun tr' c = (c, fn show_sorts => fn T => fn ts => - if (not o null) ts orelse T = dummyT - orelse not (! show_types) andalso can Term.dest_Type T - then raise Match - else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); -in map tr' [@{const_syntax Algebras.one}, @{const_syntax Algebras.zero}] end; -*} -- {* show types that are presumably too general *} - -class plus = - fixes plus :: "'a \ 'a \ 'a" (infixl "+" 65) - -class minus = - fixes minus :: "'a \ 'a \ 'a" (infixl "-" 65) - -class uminus = - fixes uminus :: "'a \ 'a" ("- _" [81] 80) - -class times = - fixes times :: "'a \ 'a \ 'a" (infixl "*" 70) - end \ No newline at end of file diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri Feb 19 14:47:01 2010 +0100 @@ -670,13 +670,13 @@ end fun whatis x ct = case term_of ct of - Const(@{const_name Algebras.plus}, _)$(Const(@{const_name Algebras.times},_)$_$y)$_ => + Const(@{const_name Groups.plus}, _)$(Const(@{const_name Groups.times},_)$_$y)$_ => if y aconv term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct]) else ("Nox",[]) -| Const(@{const_name Algebras.plus}, _)$y$_ => +| Const(@{const_name Groups.plus}, _)$y$_ => if y aconv term_of x then ("x+t",[Thm.dest_arg ct]) else ("Nox",[]) -| Const(@{const_name Algebras.times}, _)$_$y => +| Const(@{const_name Groups.times}, _)$_$y => if y aconv term_of x then ("c*x",[Thm.dest_arg1 ct]) else ("Nox",[]) | t => if t aconv term_of x then ("x",[]) else ("Nox",[]); @@ -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 Orderings.less},_)$_$Const(@{const_name Algebras.zero},_) => + Const(@{const_name Orderings.less},_)$_$Const(@{const_name Groups.zero},_) => (case whatis x (Thm.dest_arg1 ct) of ("c*x+t",[c,t]) => let @@ -727,7 +727,7 @@ | _ => reflexive ct) -| Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Algebras.zero},_) => +| Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Groups.zero},_) => (case whatis x (Thm.dest_arg1 ct) of ("c*x+t",[c,t]) => let @@ -771,7 +771,7 @@ in rth end | _ => reflexive ct) -| Const("op =",_)$_$Const(@{const_name Algebras.zero},_) => +| Const("op =",_)$_$Const(@{const_name Groups.zero},_) => (case whatis x (Thm.dest_arg1 ct) of ("c*x+t",[c,t]) => let diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Feb 19 14:47:01 2010 +0100 @@ -2947,10 +2947,10 @@ fun rrelT rT = [rT,rT] ---> rT; fun rrT rT = [rT, rT] ---> bT; fun divt rT = Const(@{const_name Rings.divide},rrelT rT); -fun timest rT = Const(@{const_name Algebras.times},rrelT rT); -fun plust rT = Const(@{const_name Algebras.plus},rrelT rT); -fun minust rT = Const(@{const_name Algebras.minus},rrelT rT); -fun uminust rT = Const(@{const_name Algebras.uminus}, rT --> rT); +fun timest rT = Const(@{const_name Groups.times},rrelT rT); +fun plust rT = Const(@{const_name Groups.plus},rrelT rT); +fun minust rT = Const(@{const_name Groups.minus},rrelT rT); +fun uminust rT = Const(@{const_name Groups.uminus}, rT --> rT); fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT); val brT = [bT, bT] ---> bT; val nott = @{term "Not"}; @@ -2961,7 +2961,7 @@ 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); +fun rz rT = Const(@{const_name Groups.zero},rT); fun dest_nat t = case t of Const ("Suc",_)$t' => 1 + dest_nat t' @@ -2969,10 +2969,10 @@ fun num_of_term m t = case t of - Const(@{const_name Algebras.uminus},_)$t => @{code poly.Neg} (num_of_term m t) - | Const(@{const_name Algebras.plus},_)$a$b => @{code poly.Add} (num_of_term m a, num_of_term m b) - | Const(@{const_name Algebras.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b) - | Const(@{const_name Algebras.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b) + Const(@{const_name Groups.uminus},_)$t => @{code poly.Neg} (num_of_term m t) + | Const(@{const_name Groups.plus},_)$a$b => @{code poly.Add} (num_of_term m a, num_of_term m b) + | Const(@{const_name Groups.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b) + | Const(@{const_name Groups.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b) | Const(@{const_name Power.power},_)$a$n => @{code poly.Pw} (num_of_term m a, dest_nat n) | Const(@{const_name Rings.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd) | _ => (@{code poly.C} (HOLogic.dest_number t |> snd,1) @@ -2980,10 +2980,10 @@ fun tm_of_term m m' t = case t of - Const(@{const_name Algebras.uminus},_)$t => @{code Neg} (tm_of_term m m' t) - | Const(@{const_name Algebras.plus},_)$a$b => @{code Add} (tm_of_term m m' a, tm_of_term m m' b) - | Const(@{const_name Algebras.minus},_)$a$b => @{code Sub} (tm_of_term m m' a, tm_of_term m m' b) - | Const(@{const_name Algebras.times},_)$a$b => @{code Mul} (num_of_term m' a, tm_of_term m m' b) + Const(@{const_name Groups.uminus},_)$t => @{code Neg} (tm_of_term m m' t) + | Const(@{const_name Groups.plus},_)$a$b => @{code Add} (tm_of_term m m' a, tm_of_term m m' b) + | Const(@{const_name Groups.minus},_)$a$b => @{code Sub} (tm_of_term m m' a, tm_of_term m m' b) + | Const(@{const_name Groups.times},_)$a$b => @{code Mul} (num_of_term m' a, tm_of_term m m' b) | _ => (@{code CP} (num_of_term m' t) handle TERM _ => @{code Bound} (AList.lookup (op aconv) m t |> the) | Option => @{code Bound} (AList.lookup (op aconv) m t |> the)); diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Decision_Procs/commutative_ring_tac.ML --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Fri Feb 19 14:47:01 2010 +0100 @@ -13,8 +13,8 @@ struct (* Zero and One of the commutative ring *) -fun cring_zero T = Const (@{const_name Algebras.zero}, T); -fun cring_one T = Const (@{const_name Algebras.one}, T); +fun cring_zero T = Const (@{const_name Groups.zero}, T); +fun cring_one T = Const (@{const_name Groups.one}, T); (* reification functions *) (* add two polynom expressions *) @@ -49,13 +49,13 @@ | reif_pol T vs t = pol_Pc T $ t; (* reification of polynom expressions *) -fun reif_polex T vs (Const (@{const_name Algebras.plus}, _) $ a $ b) = +fun reif_polex T vs (Const (@{const_name Groups.plus}, _) $ a $ b) = polex_add T $ reif_polex T vs a $ reif_polex T vs b - | reif_polex T vs (Const (@{const_name Algebras.minus}, _) $ a $ b) = + | reif_polex T vs (Const (@{const_name Groups.minus}, _) $ a $ b) = polex_sub T $ reif_polex T vs a $ reif_polex T vs b - | reif_polex T vs (Const (@{const_name Algebras.times}, _) $ a $ b) = + | reif_polex T vs (Const (@{const_name Groups.times}, _) $ a $ b) = polex_mul T $ reif_polex T vs a $ reif_polex T vs b - | reif_polex T vs (Const (@{const_name Algebras.uminus}, _) $ a) = + | reif_polex T vs (Const (@{const_name Groups.uminus}, _) $ a) = polex_neg T $ reif_polex T vs a | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) = polex_pow T $ reif_polex T vs a $ n diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Finite_Set.thy Fri Feb 19 14:47:01 2010 +0100 @@ -1055,7 +1055,7 @@ subsection {* Generalized summation over a set *} -interpretation comm_monoid_add: comm_monoid_mult "0::'a::comm_monoid_add" "op +" +interpretation comm_monoid_add: comm_monoid_mult "op +" "0::'a::comm_monoid_add" proof qed (auto intro: add_assoc add_commute) definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add" diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Groups.thy --- a/src/HOL/Groups.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Groups.thy Fri Feb 19 14:47:01 2010 +0100 @@ -6,9 +6,64 @@ theory Groups imports Orderings -uses "~~/src/Provers/Arith/abel_cancel.ML" +uses ("~~/src/Provers/Arith/abel_cancel.ML") begin +subsection {* Generic operations *} + +class zero = + fixes zero :: 'a ("0") + +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 .. + +lemma Let_1 [simp]: "Let 1 f = f 1" + unfolding Let_def .. + +setup {* + Reorient_Proc.add + (fn Const(@{const_name Groups.zero}, _) => true + | Const(@{const_name Groups.one}, _) => true + | _ => false) +*} + +simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc +simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc + +typed_print_translation {* +let + fun tr' c = (c, fn show_sorts => fn T => fn ts => + if (not o null) ts orelse T = dummyT + orelse not (! show_types) andalso can Term.dest_Type T + then raise Match + else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); +in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end; +*} -- {* show types that are presumably too general *} + +class plus = + fixes plus :: "'a \ 'a \ 'a" (infixl "+" 65) + +class minus = + fixes minus :: "'a \ 'a \ 'a" (infixl "-" 65) + +class uminus = + fixes uminus :: "'a \ 'a" ("- _" [81] 80) + +class times = + fixes times :: "'a \ 'a \ 'a" (infixl "*" 70) + +use "~~/src/Provers/Arith/abel_cancel.ML" + text {* The theory of partially ordered groups is taken from the books: \begin{itemize} @@ -1129,8 +1184,8 @@ (* term order for abelian groups *) fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') - [@{const_name Algebras.zero}, @{const_name Algebras.plus}, - @{const_name Algebras.uminus}, @{const_name Algebras.minus}] + [@{const_name Groups.zero}, @{const_name Groups.plus}, + @{const_name Groups.uminus}, @{const_name Groups.minus}] | agrp_ord _ = ~1; fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS); @@ -1139,9 +1194,9 @@ val ac1 = mk_meta_eq @{thm add_assoc}; val ac2 = mk_meta_eq @{thm add_commute}; val ac3 = mk_meta_eq @{thm add_left_commute}; - fun solve_add_ac thy _ (_ $ (Const (@{const_name Algebras.plus},_) $ _ $ _) $ _) = + fun solve_add_ac thy _ (_ $ (Const (@{const_name Groups.plus},_) $ _ $ _) $ _) = SOME ac1 - | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Algebras.plus},_) $ y $ z)) = + | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Groups.plus},_) $ y $ z)) = if termless_agrp (y, x) then SOME ac3 else NONE | solve_add_ac thy _ (_ $ x $ y) = if termless_agrp (y, x) then SOME ac2 else NONE diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Feb 19 14:47:01 2010 +0100 @@ -182,9 +182,9 @@ ">=" > HOL4Compat.nat_ge FUNPOW > HOL4Compat.FUNPOW "<=" > Orderings.less_eq :: "[nat,nat]=>bool" - "+" > Algebras.plus :: "[nat,nat]=>nat" - "*" > Algebras.times :: "[nat,nat]=>nat" - "-" > Algebras.minus :: "[nat,nat]=>nat" + "+" > Groups.plus :: "[nat,nat]=>nat" + "*" > Groups.times :: "[nat,nat]=>nat" + "-" > Groups.minus :: "[nat,nat]=>nat" MIN > Orderings.min :: "[nat,nat]=>nat" MAX > Orderings.max :: "[nat,nat]=>nat" DIV > Divides.div :: "[nat,nat]=>nat" diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Import/Generate-HOL/GenHOL4Real.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Fri Feb 19 14:47:01 2010 +0100 @@ -16,12 +16,12 @@ real > RealDef.real; const_maps - real_0 > Algebras.zero :: real - real_1 > Algebras.one :: real - real_neg > Algebras.uminus :: "real => real" - inv > Algebras.inverse :: "real => real" - real_add > Algebras.plus :: "[real,real] => real" - real_mul > Algebras.times :: "[real,real] => real" + real_0 > Groups.zero :: real + real_1 > Groups.one :: real + real_neg > Groups.uminus :: "real => real" + inv > Groups.inverse :: "real => real" + real_add > Groups.plus :: "[real,real] => real" + real_mul > Groups.times :: "[real,real] => real" real_lt > Orderings.less :: "[real,real] => bool"; ignore_thms @@ -51,8 +51,8 @@ real_gt > HOL4Compat.real_gt real_ge > HOL4Compat.real_ge real_lte > Orderings.less_eq :: "[real,real] => bool" - real_sub > Algebras.minus :: "[real,real] => real" - "/" > Algebras.divide :: "[real,real] => real" + real_sub > Groups.minus :: "[real,real] => real" + "/" > Rings.divide :: "[real,real] => real" pow > Power.power :: "[real,nat] => real" abs > Groups.abs :: "real => real" real_of_num > RealDef.real :: "nat => real"; diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Feb 19 14:47:01 2010 +0100 @@ -76,9 +76,9 @@ SUC > Suc PRE > HOLLightCompat.Pred NUMERAL > HOL4Compat.NUMERAL - "+" > Algebras.plus :: "nat \ nat \ nat" - "*" > Algebras.times :: "nat \ nat \ nat" - "-" > Algebras.minus :: "nat \ nat \ nat" + "+" > Groups.plus :: "nat \ nat \ nat" + "*" > Groups.times :: "nat \ nat \ nat" + "-" > Groups.minus :: "nat \ nat \ nat" BIT0 > HOLLightCompat.NUMERAL_BIT0 BIT1 > HOL4Compat.NUMERAL_BIT1 INL > Sum_Type.Inl diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Import/HOL/arithmetic.imp --- a/src/HOL/Import/HOL/arithmetic.imp Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Import/HOL/arithmetic.imp Fri Feb 19 14:47:01 2010 +0100 @@ -24,9 +24,9 @@ ">=" > "HOL4Compat.nat_ge" ">" > "HOL4Compat.nat_gt" "<=" > "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" + "-" > "Groups.minus" :: "nat => nat => nat" + "+" > "Groups.plus" :: "nat => nat => nat" + "*" > "Groups.times" :: "nat => nat => nat" thm_maps "num_case_def" > "HOL4Compat.num_case_def" diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Import/HOL/real.imp --- a/src/HOL/Import/HOL/real.imp Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Import/HOL/real.imp Fri Feb 19 14:47:01 2010 +0100 @@ -10,7 +10,7 @@ const_maps "sup" > "HOL4Real.real.sup" "sum" > "HOL4Real.real.sum" - "real_sub" > "Algebras.minus" :: "real => real => real" + "real_sub" > "Groups.minus" :: "real => real => real" "real_of_num" > "RealDef.real" :: "nat => real" "real_lte" > "Orderings.less_eq" :: "real => real => bool" "real_gt" > "HOL4Compat.real_gt" diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Import/HOL/realax.imp --- a/src/HOL/Import/HOL/realax.imp Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Import/HOL/realax.imp Fri Feb 19 14:47:01 2010 +0100 @@ -27,12 +27,12 @@ "treal_add" > "HOL4Real.realax.treal_add" "treal_1" > "HOL4Real.realax.treal_1" "treal_0" > "HOL4Real.realax.treal_0" - "real_neg" > "Algebras.uminus_class.uminus" :: "real => real" - "real_mul" > "Algebras.times_class.times" :: "real => real => real" + "real_neg" > "Groups.uminus" :: "real => real" + "real_mul" > "Groups.times" :: "real => real => real" "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" + "real_add" > "Groups.plus" :: "real => real => real" + "real_1" > "Groups.one" :: "real" + "real_0" > "Groups.zero" :: "real" "inv" > "Ring.inverse" :: "real => real" "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal" diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Import/HOLLight/hollight.imp --- a/src/HOL/Import/HOLLight/hollight.imp Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Import/HOLLight/hollight.imp Fri Feb 19 14:47:01 2010 +0100 @@ -238,10 +238,10 @@ "<=" > "HOLLight.hollight.<=" "<" > "HOLLight.hollight.<" "/\\" > "op &" - "-" > "Algebras.minus_class.minus" :: "nat => nat => nat" + "-" > "Groups.minus" :: "nat => nat => nat" "," > "Pair" - "+" > "Algebras.plus_class.plus" :: "nat => nat => nat" - "*" > "Algebras.times_class.times" :: "nat => nat => nat" + "+" > "Groups.plus" :: "nat => nat => nat" + "*" > "Groups.times" :: "nat => nat => nat" "$" > "HOLLight.hollight.$" "!" > "All" diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Library/SetsAndFunctions.thy --- a/src/HOL/Library/SetsAndFunctions.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Library/SetsAndFunctions.thy Fri Feb 19 14:47:01 2010 +0100 @@ -119,14 +119,14 @@ apply (force simp add: mult_assoc) done -interpretation set_comm_monoid_add: comm_monoid_add "{0}" "op \ :: ('a::comm_monoid_add) set => 'a set => 'a set" +interpretation set_comm_monoid_add: comm_monoid_add "op \ :: ('a::comm_monoid_add) set => 'a set => 'a set" "{0}" apply default apply (unfold set_plus_def) apply (force simp add: add_ac) apply force done -interpretation set_comm_monoid_mult: comm_monoid_mult "{1}" "op \ :: ('a::comm_monoid_mult) set => 'a set => 'a set" +interpretation set_comm_monoid_mult: comm_monoid_mult "op \ :: ('a::comm_monoid_mult) set => 'a set => 'a set" "{1}" apply default apply (unfold set_times_def) apply (force simp add: mult_ac) diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/List.thy --- a/src/HOL/List.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/List.thy Fri Feb 19 14:47:01 2010 +0100 @@ -2352,7 +2352,7 @@ proof (induct xss arbitrary: xs) case Nil show ?case by simp next - interpret monoid_add "[]" "op @" proof qed simp_all + interpret monoid_add "op @" "[]" proof qed simp_all case Cons then show ?case by (simp add: foldl_absorb0) qed diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Mutabelle/Mutabelle.thy --- a/src/HOL/Mutabelle/Mutabelle.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Mutabelle/Mutabelle.thy Fri Feb 19 14:47:01 2010 +0100 @@ -14,7 +14,7 @@ (@{const_name HOL.undefined}, "'a"), (@{const_name HOL.default}, "'a"), (@{const_name dummy_pattern}, "'a::{}"), - (@{const_name Algebras.uminus}, "'a"), + (@{const_name Groups.uminus}, "'a"), (@{const_name Nat.size}, "'a"), (@{const_name Groups.abs}, "'a")]; diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/NSA/NSA.thy --- a/src/HOL/NSA/NSA.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/NSA/NSA.thy Fri Feb 19 14:47:01 2010 +0100 @@ -671,12 +671,12 @@ 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) fun reorient_proc sg _ (_ $ t $ u) = case u of - Const(@{const_name Algebras.zero}, _) => NONE - | Const(@{const_name Algebras.one}, _) => NONE + Const(@{const_name Groups.zero}, _) => NONE + | Const(@{const_name Groups.one}, _) => NONE | Const(@{const_name Int.number_of}, _) $ _ => NONE | _ => SOME (case t of - Const(@{const_name Algebras.zero}, _) => meta_zero_approx_reorient - | Const(@{const_name Algebras.one}, _) => meta_one_approx_reorient + Const(@{const_name Groups.zero}, _) => meta_zero_approx_reorient + | Const(@{const_name Groups.one}, _) => meta_one_approx_reorient | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_approx_reorient); diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/Function/size.ML Fri Feb 19 14:47:01 2010 +0100 @@ -25,7 +25,7 @@ val lookup_size = SizeData.get #> Symtab.lookup; -fun plus (t1, t2) = Const (@{const_name Algebras.plus}, +fun plus (t1, t2) = Const (@{const_name Groups.plus}, HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; fun size_of_type f g h (T as Type (s, Ts)) = diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Feb 19 14:47:01 2010 +0100 @@ -2436,8 +2436,8 @@ val [polarity, depth] = additional_arguments val polarity' = (case prem of Prem _ => I | Negprem _ => HOLogic.mk_not | _ => I) polarity val depth' = - Const ("Algebras.minus", @{typ "code_numeral => code_numeral => code_numeral"}) - $ depth $ Const ("Algebras.one", @{typ "Code_Numeral.code_numeral"}) + Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"}) + $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"}) in [polarity', depth'] end } diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Feb 19 14:47:01 2010 +0100 @@ -224,8 +224,8 @@ @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat}, @{const_name Nat.one_nat_inst.one_nat}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}, - @{const_name Algebras.zero}, - @{const_name Algebras.one}, @{const_name Algebras.plus}, + @{const_name Groups.zero}, + @{const_name Groups.one}, @{const_name Groups.plus}, @{const_name Nat.ord_nat_inst.less_eq_nat}, @{const_name Nat.ord_nat_inst.less_nat}, @{const_name number_nat_inst.number_of_nat}, diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/Qelim/cooper.ML Fri Feb 19 14:47:01 2010 +0100 @@ -79,9 +79,9 @@ | 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$_) => +| Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_) => if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox -| Const (@{const_name Not},_) $ (Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_)) => +| Const (@{const_name Not},_) $ (Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_)) => if term_of x aconv y then NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox | _ => Nox) @@ -175,18 +175,18 @@ (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]); fun linear_cmul 0 tm = zero | linear_cmul n tm = case tm of - Const (@{const_name Algebras.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b - | Const (@{const_name Algebras.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x - | Const (@{const_name Algebras.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b - | (m as Const (@{const_name Algebras.uminus}, _)) $ a => m $ linear_cmul n a + Const (@{const_name Groups.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b + | Const (@{const_name Groups.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x + | Const (@{const_name Groups.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b + | (m as Const (@{const_name Groups.uminus}, _)) $ a => m $ linear_cmul n a | _ => numeral1 (fn m => n * m) tm; fun earlier [] x y = false | earlier (h::t) x y = if h aconv y then false else if h aconv x then true else earlier t x y; fun linear_add vars tm1 tm2 = case (tm1, tm2) of - (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1, - Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) => + (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, + Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) => if x1 = x2 then let val c = numeral2 Integer.add c1 c2 in if c = zero then linear_add vars r1 r2 @@ -194,9 +194,9 @@ end else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 - | (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1, _) => + | (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, _) => addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 - | (_, Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) => + | (_, Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) => addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 | (_, _) => numeral2 Integer.add tm1 tm2; @@ -205,10 +205,10 @@ fun lint vars tm = if is_numeral tm then tm else case tm of - Const (@{const_name Algebras.uminus}, _) $ t => linear_neg (lint vars t) -| Const (@{const_name Algebras.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t) -| Const (@{const_name Algebras.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t) -| Const (@{const_name Algebras.times}, _) $ s $ t => + Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t) +| Const (@{const_name Groups.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t) +| Const (@{const_name Groups.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t) +| Const (@{const_name Groups.times}, _) $ s $ t => let val s' = lint vars s val t' = lint vars t in if is_numeral s' then (linear_cmul (dest_numeral s') t') @@ -270,7 +270,7 @@ val d'' = Thm.rhs_of dth |> Thm.dest_arg1 in case tt' of - Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$_)$_ => + Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ => let val x = dest_numeral c in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs))) (Thm.transitive dth (inst' [d'',t'] dvd_uminus')) @@ -293,15 +293,15 @@ val ins = insert (op = : int * int -> bool) fun h (acc,dacc) t = case (term_of t) of - Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ => + Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ => if x aconv y andalso member (op =) ["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) => + | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) => if x aconv y andalso member (op =) [@{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)$_) => + | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) => if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc) | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) @@ -335,15 +335,15 @@ Const("op &",_)$_$_ => binop_conv unit_conv t | Const("op |",_)$_$_ => binop_conv unit_conv t | Const (@{const_name Not},_)$_ => arg_conv unit_conv t - | Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ => + | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ => if x=y andalso member (op =) ["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) => + | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) => if x=y andalso member (op =) [@{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)$_)) => + | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_)) => if x=y then let val k = l div dest_numeral c @@ -546,10 +546,10 @@ | @{term "0::int"} => C 0 | @{term "1::int"} => C 1 | Term.Bound i => Bound i - | Const(@{const_name Algebras.uminus},_)$t' => Neg (i_of_term vs t') - | Const(@{const_name Algebras.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2) - | Const(@{const_name Algebras.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2) - | Const(@{const_name Algebras.times},_)$t1$t2 => + | Const(@{const_name Groups.uminus},_)$t' => Neg (i_of_term vs t') + | Const(@{const_name Groups.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2) + | Const(@{const_name Groups.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2) + | Const(@{const_name Groups.times},_)$t1$t2 => (Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle TERM _ => (Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1) diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Tools/Qelim/presburger.ML --- a/src/HOL/Tools/Qelim/presburger.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/Qelim/presburger.ML Fri Feb 19 14:47:01 2010 +0100 @@ -52,15 +52,15 @@ local fun isnum t = case t of - Const(@{const_name Algebras.zero},_) => true - | Const(@{const_name Algebras.one},_) => true + Const(@{const_name Groups.zero},_) => true + | Const(@{const_name Groups.one},_) => true | @{term "Suc"}$s => isnum s | @{term "nat"}$s => isnum s | @{term "int"}$s => isnum s - | Const(@{const_name Algebras.uminus},_)$s => isnum s - | Const(@{const_name Algebras.plus},_)$l$r => isnum l andalso isnum r - | Const(@{const_name Algebras.times},_)$l$r => isnum l andalso isnum r - | Const(@{const_name Algebras.minus},_)$l$r => isnum l andalso isnum r + | Const(@{const_name Groups.uminus},_)$s => isnum s + | Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r + | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r + | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Tools/arith_data.ML --- a/src/HOL/Tools/arith_data.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/arith_data.ML Fri Feb 19 14:47:01 2010 +0100 @@ -75,11 +75,11 @@ fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n; -val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus}; +val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; fun mk_minus t = let val T = Term.fastype_of t - in Const (@{const_name Algebras.uminus}, T --> T) $ t end; + in Const (@{const_name Groups.uminus}, T --> T) $ t end; (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) fun mk_sum T [] = mk_number T 0 @@ -91,9 +91,9 @@ | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); (*decompose additions AND subtractions as a sum*) -fun dest_summing (pos, Const (@{const_name Algebras.plus}, _) $ t $ u, ts) = +fun dest_summing (pos, Const (@{const_name Groups.plus}, _) $ t $ u, ts) = dest_summing (pos, t, dest_summing (pos, u, ts)) - | dest_summing (pos, Const (@{const_name Algebras.minus}, _) $ t $ u, ts) = + | dest_summing (pos, Const (@{const_name Groups.minus}, _) $ t $ u, ts) = dest_summing (pos, t, dest_summing (not pos, u, ts)) | dest_summing (pos, t, ts) = if pos then t::ts else mk_minus t :: ts; diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/hologic.ML Fri Feb 19 14:47:01 2010 +0100 @@ -440,9 +440,9 @@ val natT = Type ("nat", []); -val zero = Const ("Algebras.zero_class.zero", natT); +val zero = Const ("Groups.zero_class.zero", natT); -fun is_zero (Const ("Algebras.zero_class.zero", _)) = true +fun is_zero (Const ("Groups.zero_class.zero", _)) = true | is_zero _ = false; fun mk_Suc t = Const ("Suc", natT --> natT) $ t; @@ -458,7 +458,7 @@ | mk n = mk_Suc (mk (n - 1)); in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end; -fun dest_nat (Const ("Algebras.zero_class.zero", _)) = 0 +fun dest_nat (Const ("Groups.zero_class.zero", _)) = 0 | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1 | dest_nat t = raise TERM ("dest_nat", [t]); @@ -508,12 +508,12 @@ | add_numerals (Abs (_, _, t)) = add_numerals t | add_numerals _ = I; -fun mk_number T 0 = Const ("Algebras.zero_class.zero", T) - | mk_number T 1 = Const ("Algebras.one_class.one", T) +fun mk_number T 0 = Const ("Groups.zero_class.zero", T) + | mk_number T 1 = Const ("Groups.one_class.one", T) | mk_number T i = number_of_const T $ mk_numeral i; -fun dest_number (Const ("Algebras.zero_class.zero", T)) = (T, 0) - | dest_number (Const ("Algebras.one_class.one", T)) = (T, 1) +fun dest_number (Const ("Groups.zero_class.zero", T)) = (T, 0) + | dest_number (Const ("Groups.one_class.one", T)) = (T, 1) | dest_number (Const ("Int.number_class.number_of", Type ("fun", [_, T])) $ t) = (T, dest_numeral t) | dest_number t = raise TERM ("dest_number", [t]); diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/int_arith.ML Fri Feb 19 14:47:01 2010 +0100 @@ -49,12 +49,12 @@ make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc", proc = proc1, identifier = []}; -fun check (Const (@{const_name Algebras.one}, @{typ int})) = false - | check (Const (@{const_name Algebras.one}, _)) = true +fun check (Const (@{const_name Groups.one}, @{typ int})) = false + | check (Const (@{const_name Groups.one}, _)) = true | check (Const (s, _)) = member (op =) [@{const_name "op ="}, - @{const_name Algebras.times}, @{const_name Algebras.uminus}, - @{const_name Algebras.minus}, @{const_name Algebras.plus}, - @{const_name Algebras.zero}, + @{const_name Groups.times}, @{const_name Groups.uminus}, + @{const_name Groups.minus}, @{const_name Groups.plus}, + @{const_name Groups.zero}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s | check (a $ b) = check a andalso check b | check _ = false; diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/lin_arith.ML Fri Feb 19 14:47:01 2010 +0100 @@ -138,8 +138,8 @@ *) fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat = let - fun demult ((mC as Const (@{const_name Algebras.times}, _)) $ s $ t, m) = - (case s of Const (@{const_name Algebras.times}, _) $ s1 $ s2 => + fun demult ((mC as Const (@{const_name Groups.times}, _)) $ s $ t, m) = + (case s of Const (@{const_name Groups.times}, _) $ s1 $ s2 => (* bracketing to the right: '(s1 * s2) * t' becomes 's1 * (s2 * t)' *) demult (mC $ s1 $ (mC $ s2 $ t), m) | _ => @@ -170,9 +170,9 @@ (SOME _, _) => (SOME (mC $ s $ t), m) | (NONE, m') => apsnd (Rat.mult (Rat.inv m')) (demult (s, m))) (* terms that evaluate to numeric constants *) - | demult (Const (@{const_name Algebras.uminus}, _) $ t, m) = demult (t, Rat.neg m) - | demult (Const (@{const_name Algebras.zero}, _), m) = (NONE, Rat.zero) - | demult (Const (@{const_name Algebras.one}, _), m) = (NONE, m) + | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m) + | demult (Const (@{const_name Groups.zero}, _), m) = (NONE, Rat.zero) + | demult (Const (@{const_name Groups.one}, _), m) = (NONE, m) (*Warning: in rare cases number_of encloses a non-numeral, in which case dest_numeral raises TERM; hence all the handles below. Same for Suc-terms that turn out not to be numerals - @@ -196,19 +196,19 @@ (* Turns a term 'all' and associated multiplicity 'm' into a list 'p' of summands and associated multiplicities, plus a constant 'i' (with implicit multiplicity 1) *) - fun poly (Const (@{const_name Algebras.plus}, _) $ s $ t, + fun poly (Const (@{const_name Groups.plus}, _) $ s $ t, m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi)) - | poly (all as Const (@{const_name Algebras.minus}, T) $ s $ t, m, pi) = + | poly (all as Const (@{const_name Groups.minus}, T) $ s $ t, m, pi) = if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi)) - | poly (all as Const (@{const_name Algebras.uminus}, T) $ t, m, pi) = + | poly (all as Const (@{const_name Groups.uminus}, T) $ t, m, pi) = if nT T then add_atom all m pi else poly (t, Rat.neg m, pi) - | poly (Const (@{const_name Algebras.zero}, _), _, pi) = + | poly (Const (@{const_name Groups.zero}, _), _, pi) = pi - | poly (Const (@{const_name Algebras.one}, _), m, (p, i)) = + | poly (Const (@{const_name Groups.one}, _), m, (p, i)) = (p, Rat.add i m) | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) = poly (t, m, (p, Rat.add i m)) - | poly (all as Const (@{const_name Algebras.times}, _) $ _ $ _, m, pi as (p, i)) = + | poly (all as Const (@{const_name Groups.times}, _) $ _ $ _, m, pi as (p, i)) = (case demult inj_consts (all, m) of (NONE, m') => (p, Rat.add i m') | (SOME u, m') => add_atom u m' pi) @@ -293,7 +293,7 @@ Const (a, _) => member (op =) [@{const_name Orderings.max}, @{const_name Orderings.min}, @{const_name Groups.abs}, - @{const_name Algebras.minus}, + @{const_name Groups.minus}, "Int.nat" (*DYNAMIC BINDING!*), "Divides.div_class.mod" (*DYNAMIC BINDING!*), "Divides.div_class.div" (*DYNAMIC BINDING!*)] a @@ -401,9 +401,9 @@ 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}, + val terms2 = map (subst_term [(split_term, Const (@{const_name Groups.uminus}, split_type --> split_type) $ t1)]) rev_terms - val zero = Const (@{const_name Algebras.zero}, split_type) + val zero = Const (@{const_name Groups.zero}, split_type) 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 Orderings.less}, @@ -415,12 +415,12 @@ SOME [(Ts, subgoal1), (Ts, subgoal2)] end (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *) - | (Const (@{const_name Algebras.minus}, _), [t1, t2]) => + | (Const (@{const_name Groups.minus}, _), [t1, t2]) => let (* "d" in the above theorem becomes a new bound variable after NNF *) (* transformation, therefore some adjustment of indices is necessary *) val rev_terms = rev terms - val zero = Const (@{const_name Algebras.zero}, split_type) + val zero = Const (@{const_name Groups.zero}, split_type) val d = Bound 0 val terms1 = map (subst_term [(split_term, zero)]) rev_terms val terms2 = map (subst_term [(incr_boundvars 1 split_term, d)]) @@ -430,7 +430,7 @@ 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}, + (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $ t2' $ d) val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) val subgoal1 = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false] @@ -442,8 +442,8 @@ | (Const ("Int.nat", _), [t1]) => let val rev_terms = rev terms - val zero_int = Const (@{const_name Algebras.zero}, HOLogic.intT) - val zero_nat = Const (@{const_name Algebras.zero}, HOLogic.natT) + val zero_int = Const (@{const_name Groups.zero}, HOLogic.intT) + val zero_nat = Const (@{const_name Groups.zero}, HOLogic.natT) val n = Bound 0 val terms1 = map (subst_term [(incr_boundvars 1 split_term, n)]) (map (incr_boundvars 1) rev_terms) @@ -465,7 +465,7 @@ | (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) => let val rev_terms = rev terms - val zero = Const (@{const_name Algebras.zero}, split_type) + val zero = Const (@{const_name Groups.zero}, split_type) val i = Bound 1 val j = Bound 0 val terms1 = map (subst_term [(split_term, t1)]) rev_terms @@ -480,8 +480,8 @@ 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) $ - (Const (@{const_name Algebras.times}, + (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $ + (Const (@{const_name Groups.times}, split_type --> split_type --> split_type) $ t2' $ i) $ j) val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] @@ -497,7 +497,7 @@ | (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) => let val rev_terms = rev terms - val zero = Const (@{const_name Algebras.zero}, split_type) + val zero = Const (@{const_name Groups.zero}, split_type) val i = Bound 1 val j = Bound 0 val terms1 = map (subst_term [(split_term, zero)]) rev_terms @@ -512,8 +512,8 @@ 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) $ - (Const (@{const_name Algebras.times}, + (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $ + (Const (@{const_name Groups.times}, split_type --> split_type --> split_type) $ t2' $ i) $ j) val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] @@ -535,7 +535,7 @@ Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) => let val rev_terms = rev terms - val zero = Const (@{const_name Algebras.zero}, split_type) + val zero = Const (@{const_name Groups.zero}, split_type) val i = Bound 1 val j = Bound 0 val terms1 = map (subst_term [(split_term, t1)]) rev_terms @@ -558,8 +558,8 @@ 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) $ - (Const (@{const_name Algebras.times}, + (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $ + (Const (@{const_name Groups.times}, split_type --> split_type --> split_type) $ t2' $ i) $ j) val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] @@ -589,7 +589,7 @@ Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) => let val rev_terms = rev terms - val zero = Const (@{const_name Algebras.zero}, split_type) + val zero = Const (@{const_name Groups.zero}, split_type) val i = Bound 1 val j = Bound 0 val terms1 = map (subst_term [(split_term, zero)]) rev_terms @@ -612,8 +612,8 @@ 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) $ - (Const (@{const_name Algebras.times}, + (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $ + (Const (@{const_name Groups.times}, split_type --> split_type --> split_type) $ t2' $ i) $ j) val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const) val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false] diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Tools/nat_arith.ML --- a/src/HOL/Tools/nat_arith.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/nat_arith.ML Fri Feb 19 14:47:01 2010 +0100 @@ -19,8 +19,8 @@ (** abstract syntax of structure nat: 0, Suc, + **) -val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus}; -val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT; +val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; +val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; fun mk_sum [] = HOLogic.zero | mk_sum [t] = t @@ -85,8 +85,8 @@ structure DiffCancelSums = CancelSumsFun (struct open CommonCancelSums; - val mk_bal = HOLogic.mk_binop @{const_name Algebras.minus}; - val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT; + val mk_bal = HOLogic.mk_binop @{const_name Groups.minus}; + val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT; val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"}; end); diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Tools/nat_numeral_simprocs.ML --- a/src/HOL/Tools/nat_numeral_simprocs.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Fri Feb 19 14:47:01 2010 +0100 @@ -32,7 +32,7 @@ | find_first_numeral past [] = raise TERM("find_first_numeral", []); val zero = mk_number 0; -val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus}; +val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) fun mk_sum [] = zero @@ -43,7 +43,7 @@ fun long_mk_sum [] = HOLogic.zero | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); -val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT; +val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; (** Other simproc items **) @@ -61,14 +61,14 @@ (*** CancelNumerals simprocs ***) val one = mk_number 1; -val mk_times = HOLogic.mk_binop @{const_name Algebras.times}; +val mk_times = HOLogic.mk_binop @{const_name Groups.times}; fun mk_prod [] = one | mk_prod [t] = t | mk_prod (t :: ts) = if t = one then mk_prod ts else mk_times (t, mk_prod ts); -val dest_times = HOLogic.dest_bin @{const_name Algebras.times} HOLogic.natT; +val dest_times = HOLogic.dest_bin @{const_name Groups.times} HOLogic.natT; fun dest_prod t = let val (t,u) = dest_times t @@ -194,8 +194,8 @@ structure DiffCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name Algebras.minus} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT + val mk_bal = HOLogic.mk_binop @{const_name Groups.minus} + val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT val bal_add1 = @{thm nat_diff_add_eq1} RS trans val bal_add2 = @{thm nat_diff_add_eq2} RS trans ); diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/numeral_simprocs.ML Fri Feb 19 14:47:01 2010 +0100 @@ -34,12 +34,12 @@ val long_mk_sum = Arith_Data.long_mk_sum; val dest_sum = Arith_Data.dest_sum; -val mk_diff = HOLogic.mk_binop @{const_name Algebras.minus}; -val dest_diff = HOLogic.dest_bin @{const_name Algebras.minus} Term.dummyT; +val mk_diff = HOLogic.mk_binop @{const_name Groups.minus}; +val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} Term.dummyT; -val mk_times = HOLogic.mk_binop @{const_name Algebras.times}; +val mk_times = HOLogic.mk_binop @{const_name Groups.times}; -fun one_of T = Const(@{const_name Algebras.one}, T); +fun one_of T = Const(@{const_name Groups.one}, T); (* build product with trailing 1 rather than Numeral 1 in order to avoid the unnecessary restriction to type class number_ring @@ -56,7 +56,7 @@ fun long_mk_prod T [] = one_of T | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts); -val dest_times = HOLogic.dest_bin @{const_name Algebras.times} Term.dummyT; +val dest_times = HOLogic.dest_bin @{const_name Groups.times} Term.dummyT; fun dest_prod t = let val (t,u) = dest_times t @@ -72,7 +72,7 @@ fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t); (*Express t as a product of (possibly) a numeral with other sorted terms*) -fun dest_coeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_coeff (~sign) t +fun dest_coeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_coeff (~sign) t | dest_coeff sign t = let val ts = sort TermOrd.term_ord (dest_prod t) val (n, ts') = find_first_numeral [] ts @@ -104,7 +104,7 @@ in mk_times (mk_divide (mk_number T p, mk_number T q), t) end; (*Express t as a product of a fraction with other sorted terms*) -fun dest_fcoeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_fcoeff (~sign) t +fun dest_fcoeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_fcoeff (~sign) t | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) = let val (p, t') = dest_coeff sign t val (q, u') = dest_coeff 1 u @@ -484,7 +484,7 @@ in fun sign_conv pos_th neg_th ss t = let val T = fastype_of t; - val zero = Const(@{const_name Algebras.zero}, T); + val zero = Const(@{const_name Groups.zero}, T); val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT); val pos = less $ zero $ t and neg = less $ t $ zero fun prove p = diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/refute.ML Fri Feb 19 14:47:01 2010 +0100 @@ -710,11 +710,11 @@ | Const (@{const_name Finite_Set.finite}, _) => t | 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", []), + | Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t - | Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []), + | Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t - | Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []), + | Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t | Const (@{const_name List.append}, _) => t | Const (@{const_name lfp}, _) => t @@ -886,13 +886,13 @@ | 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", []), + | Const (@{const_name Groups.plus}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms T axs - | Const (@{const_name Algebras.minus}, T as Type ("fun", [Type ("nat", []), + | Const (@{const_name Groups.minus}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms T axs - | Const (@{const_name Algebras.times}, T as Type ("fun", [Type ("nat", []), + | Const (@{const_name Groups.times}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms T axs | Const (@{const_name List.append}, T) => collect_type_axioms T axs @@ -2794,7 +2794,7 @@ fun Nat_plus_interpreter thy model args t = case t of - Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []), + Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => let val size_of_nat = size_of_type thy model (Type ("nat", [])) @@ -2825,7 +2825,7 @@ fun Nat_minus_interpreter thy model args t = case t of - Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []), + Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => let val size_of_nat = size_of_type thy model (Type ("nat", [])) @@ -2853,7 +2853,7 @@ fun Nat_times_interpreter thy model args t = case t of - Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []), + Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => let val size_of_nat = size_of_type thy model (Type ("nat", [])) diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/ex/Arith_Examples.thy --- a/src/HOL/ex/Arith_Examples.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/ex/Arith_Examples.thy Fri Feb 19 14:47:01 2010 +0100 @@ -33,7 +33,7 @@ *) subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs}, - @{term Algebras.minus}, @{term nat}, @{term Divides.mod}, + @{term minus}, @{term nat}, @{term Divides.mod}, @{term Divides.div} *} lemma "(i::nat) <= max i j" diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/ex/Binary.thy --- a/src/HOL/ex/Binary.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/ex/Binary.thy Fri Feb 19 14:47:01 2010 +0100 @@ -24,8 +24,8 @@ | dest_bit (Const (@{const_name True}, _)) = 1 | dest_bit t = raise TERM ("dest_bit", [t]); - fun dest_binary (Const (@{const_name Algebras.zero}, Type (@{type_name nat}, _))) = 0 - | dest_binary (Const (@{const_name Algebras.one}, Type (@{type_name nat}, _))) = 1 + fun dest_binary (Const (@{const_name Groups.zero}, Type (@{type_name nat}, _))) = 0 + | dest_binary (Const (@{const_name Groups.one}, Type (@{type_name nat}, _))) = 1 | dest_binary (Const (@{const_name bit}, _) $ bs $ b) = 2 * dest_binary bs + dest_bit b | dest_binary t = raise TERM ("dest_binary", [t]); diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/ex/SVC_Oracle.thy --- a/src/HOL/ex/SVC_Oracle.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/ex/SVC_Oracle.thy Fri Feb 19 14:47:01 2010 +0100 @@ -63,21 +63,21 @@ (*abstraction of a numeric literal*) fun lit t = if can HOLogic.dest_number t then t else replace t; (*abstraction of a real/rational expression*) - fun rat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y) + fun rat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y) + | rat ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y) | rat ((c as Const(@{const_name Rings.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (rat x) + | rat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (rat x) $ (rat y) + | rat ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (rat x) | rat t = lit t (*abstraction of an integer expression: no div, mod*) - fun int ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (int x) $ (int y) - | int ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (int x) $ (int y) - | int ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (int x) $ (int y) - | int ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (int x) + fun int ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (int x) $ (int y) + | int ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (int x) $ (int y) + | int ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (int x) $ (int y) + | int ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (int x) | int t = lit t (*abstraction of a natural number expression: no minus*) - fun nat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y) - | nat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (nat x) $ (nat y) + fun nat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y) + | nat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (nat x) $ (nat y) | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x) | nat t = lit t (*abstraction of a relation: =, <, <=*) diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/ex/Summation.thy --- a/src/HOL/ex/Summation.thy Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/ex/Summation.thy Fri Feb 19 14:47:01 2010 +0100 @@ -28,7 +28,7 @@ lemma \_same_shift: assumes "\ f = \ g" - shows "\l. (op +) l \ f = g" + shows "\l. plus l \ f = g" proof - fix k from assms have "\k. \ f k = \ g k" by simp @@ -44,9 +44,9 @@ show "f k - g k = f 0 - g 0" by (induct k rule: int_induct) (simp_all add: k_incr k_decr) qed - then have "\k. ((op +) (g 0 - f 0) \ f) k = g k" + then have "\k. (plus (g 0 - f 0) \ f) k = g k" by (simp add: algebra_simps) - then have "(op +) (g 0 - f 0) \ f = g" .. + then have "plus (g 0 - f 0) \ f = g" .. then show ?thesis .. qed @@ -99,7 +99,7 @@ "\ (\ f) j l = f l - f j" proof - from \_\ have "\ (\ (\ f) j) = \ f" . - then obtain k where "(op +) k \ \ (\ f) j = f" by (blast dest: \_same_shift) + then obtain k where "plus k \ \ (\ f) j = f" by (blast dest: \_same_shift) then have "\q. f q = k + \ (\ f) j q" by (simp add: expand_fun_eq) then show ?thesis by simp qed diff -r 07a56610c00b -r 8dfd816713c6 src/HOL/ex/svc_funcs.ML --- a/src/HOL/ex/svc_funcs.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/ex/svc_funcs.ML Fri Feb 19 14:47:01 2010 +0100 @@ -146,16 +146,16 @@ (*translation of a literal*) val lit = snd o HOLogic.dest_number; (*translation of a literal expression [no variables]*) - fun litExp (Const(@{const_name Algebras.plus}, T) $ x $ y) = + fun litExp (Const(@{const_name Groups.plus}, T) $ x $ y) = if is_numeric_op T then (litExp x) + (litExp y) else fail t - | litExp (Const(@{const_name Algebras.minus}, T) $ x $ y) = + | litExp (Const(@{const_name Groups.minus}, T) $ x $ y) = if is_numeric_op T then (litExp x) - (litExp y) else fail t - | litExp (Const(@{const_name Algebras.times}, T) $ x $ y) = + | litExp (Const(@{const_name Groups.times}, T) $ x $ y) = if is_numeric_op T then (litExp x) * (litExp y) else fail t - | litExp (Const(@{const_name Algebras.uminus}, T) $ x) = + | litExp (Const(@{const_name Groups.uminus}, T) $ x) = if is_numeric_op T then ~(litExp x) else fail t | litExp t = lit t @@ -163,21 +163,21 @@ (*translation of a real/rational expression*) fun suc t = Interp("+", [Int 1, t]) fun tm (Const(@{const_name Suc}, T) $ x) = suc (tm x) - | tm (Const(@{const_name Algebras.plus}, T) $ x $ y) = + | tm (Const(@{const_name Groups.plus}, T) $ x $ y) = if is_numeric_op T then Interp("+", [tm x, tm y]) else fail t - | tm (Const(@{const_name Algebras.minus}, T) $ x $ y) = + | tm (Const(@{const_name Groups.minus}, T) $ x $ y) = if is_numeric_op T then Interp("+", [tm x, Interp("*", [Int ~1, tm y])]) else fail t - | tm (Const(@{const_name Algebras.times}, T) $ x $ y) = + | tm (Const(@{const_name Groups.times}, T) $ x $ y) = if is_numeric_op T then Interp("*", [tm x, tm y]) else fail t | tm (Const(@{const_name Rings.inverse}, T) $ x) = if domain_type T = HOLogic.realT then Rat(1, litExp x) else fail t - | tm (Const(@{const_name Algebras.uminus}, T) $ x) = + | tm (Const(@{const_name Groups.uminus}, T) $ x) = if is_numeric_op T then Interp("*", [Int ~1, tm x]) else fail t | tm t = Int (lit t) diff -r 07a56610c00b -r 8dfd816713c6 src/Provers/Arith/abel_cancel.ML --- a/src/Provers/Arith/abel_cancel.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/Provers/Arith/abel_cancel.ML Fri Feb 19 14:47:01 2010 +0100 @@ -28,29 +28,29 @@ (* FIXME dependent on abstract syntax *) -fun zero t = Const (@{const_name Algebras.zero}, t); -fun minus t = Const (@{const_name Algebras.uminus}, t --> t); +fun zero t = Const (@{const_name Groups.zero}, t); +fun minus t = Const (@{const_name Groups.uminus}, t --> t); -fun add_terms pos (Const (@{const_name Algebras.plus}, _) $ x $ y, ts) = +fun add_terms pos (Const (@{const_name Groups.plus}, _) $ x $ y, ts) = add_terms pos (x, add_terms pos (y, ts)) - | add_terms pos (Const (@{const_name Algebras.minus}, _) $ x $ y, ts) = + | add_terms pos (Const (@{const_name Groups.minus}, _) $ x $ y, ts) = add_terms pos (x, add_terms (not pos) (y, ts)) - | add_terms pos (Const (@{const_name Algebras.uminus}, _) $ x, ts) = + | add_terms pos (Const (@{const_name Groups.uminus}, _) $ x, ts) = add_terms (not pos) (x, ts) | add_terms pos (x, ts) = (pos,x) :: ts; fun terms fml = add_terms true (fml, []); -fun zero1 pt (u as (c as Const(@{const_name Algebras.plus},_)) $ x $ y) = +fun zero1 pt (u as (c as Const(@{const_name Groups.plus},_)) $ x $ y) = (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE | SOME z => SOME(c $ x $ z)) | SOME z => SOME(c $ z $ y)) - | zero1 (pos,t) (u as (c as Const(@{const_name Algebras.minus},_)) $ x $ y) = + | zero1 (pos,t) (u as (c as Const(@{const_name Groups.minus},_)) $ x $ y) = (case zero1 (pos,t) x of NONE => (case zero1 (not pos,t) y of NONE => NONE | SOME z => SOME(c $ x $ z)) | SOME z => SOME(c $ z $ y)) - | zero1 (pos,t) (u as (c as Const(@{const_name Algebras.uminus},_)) $ x) = + | zero1 (pos,t) (u as (c as Const(@{const_name Groups.uminus},_)) $ x) = (case zero1 (not pos,t) x of NONE => NONE | SOME z => SOME(c $ z)) | zero1 (pos,t) u = @@ -71,7 +71,7 @@ fun cancel t = let val c $ lhs $ rhs = t - val opp = case c of Const(@{const_name Algebras.plus},_) => true | _ => false; + val opp = case c of Const(@{const_name Groups.plus},_) => true | _ => false; val (pos,l) = find_common opp (terms lhs) (terms rhs) val posr = if opp then not pos else pos val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs)) diff -r 07a56610c00b -r 8dfd816713c6 src/Provers/Arith/cancel_div_mod.ML --- a/src/Provers/Arith/cancel_div_mod.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/Provers/Arith/cancel_div_mod.ML Fri Feb 19 14:47:01 2010 +0100 @@ -34,12 +34,12 @@ functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD = struct -fun coll_div_mod (Const(@{const_name Algebras.plus},_) $ s $ t) dms = +fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms = coll_div_mod t (coll_div_mod s dms) - | coll_div_mod (Const(@{const_name Algebras.times},_) $ m $ (Const(d,_) $ s $ n)) + | coll_div_mod (Const(@{const_name Groups.times},_) $ m $ (Const(d,_) $ s $ n)) (dms as (divs,mods)) = if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms - | coll_div_mod (Const(@{const_name Algebras.times},_) $ (Const(d,_) $ s $ n) $ m) + | coll_div_mod (Const(@{const_name Groups.times},_) $ (Const(d,_) $ s $ n) $ m) (dms as (divs,mods)) = if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) = @@ -55,8 +55,8 @@ ==> thesis by transitivity *) -val mk_plus = Data.mk_binop @{const_name Algebras.plus}; -val mk_times = Data.mk_binop @{const_name Algebras.times}; +val mk_plus = Data.mk_binop @{const_name Groups.plus}; +val mk_times = Data.mk_binop @{const_name Groups.times}; fun rearrange t pq = let val ts = Data.dest_sum t;