# HG changeset patch # User haftmann # Date 1266826669 -3600 # Node ID 3745987488b2660001edbe76a3e9f394fd64186c # Parent 9927471cca354b234d77802c657c8d064d16d9fa# Parent 1cb90bbbf45e2f4175e88c5efd7aa2a9e789104d merged diff -r 9927471cca35 -r 3745987488b2 NEWS --- a/NEWS Sun Feb 21 23:05:37 2010 +0100 +++ b/NEWS Mon Feb 22 09:17:49 2010 +0100 @@ -52,6 +52,12 @@ *** HOL *** +* Multisets: changed orderings: + * pointwise ordering is instance of class order with standard syntax <= and <; + * multiset ordering has syntax <=# and <#; partial order properties are provided + by means of interpretation with prefix multiset_order. +INCOMPATIBILITY. + * New set of rules "ac_simps" provides combined assoc / commute rewrites for all interpretations of the appropriate generic locales. @@ -63,7 +69,7 @@ * Some generic constants have been put to appropriate theories: less_eq, less: Orderings - abs, sgn: Groups + zero, one, plus, minus, uminus, times, abs, sgn: Groups inverse, divide: Rings INCOMPATIBILITY. @@ -123,8 +129,7 @@ INCOMPATIBILITY. * New theory Algebras contains generic algebraic structures and -generic algebraic operations. INCOMPATIBILTY: constants zero, one, -plus, minus, uminus and times have been moved from HOL.thy to Algebras.thy. +generic algebraic operations. * HOLogic.strip_psplit: types are returned in syntactic order, similar to other strip and tuple operations. INCOMPATIBILITY. @@ -133,10 +138,11 @@ replaced by new-style primrec, especially in theory List. The corresponding constants now have authentic syntax. INCOMPATIBILITY. -* Reorganized theory Multiset: less duplication, less historical -organization of sections, conversion from associations lists to -multisets, rudimentary code generation. Use insert_DiffM2 [symmetric] -instead of elem_imp_eq_diff_union, if needed. INCOMPATIBILITY. +* Reorganized theory Multiset: swapped notation of pointwise and multiset +order; less duplication, less historical organization of sections, +conversion from associations lists to multisets, rudimentary code generation. +Use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed. +INCOMPATIBILITY. * Reorganized theory Sum_Type; Inl and Inr now have authentic syntax. INCOMPATIBILITY. diff -r 9927471cca35 -r 3745987488b2 src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Algebra/Divisibility.thy Mon Feb 22 09:17:49 2010 +0100 @@ -2250,7 +2250,7 @@ assumes ab: "a divides b" and afs: "wfactors G as a" and bfs: "wfactors G bs b" and carr: "a \ carrier G" "b \ carrier G" "set as \ carrier G" "set bs \ carrier G" - shows "fmset G as \# fmset G bs" + shows "fmset G as \ fmset G bs" using ab proof (elim dividesE) fix c @@ -2270,7 +2270,7 @@ qed lemma (in comm_monoid_cancel) fmsubset_divides: - assumes msubset: "fmset G as \# fmset G bs" + assumes msubset: "fmset G as \ fmset G bs" and afs: "wfactors G as a" and bfs: "wfactors G bs b" and acarr: "a \ carrier G" and bcarr: "b \ carrier G" and ascarr: "set as \ carrier G" and bscarr: "set bs \ carrier G" @@ -2323,7 +2323,7 @@ assumes "wfactors G as a" and "wfactors G bs b" and "a \ carrier G" and "b \ carrier G" and "set as \ carrier G" and "set bs \ carrier G" - shows "a divides b = (fmset G as \# fmset G bs)" + shows "a divides b = (fmset G as \ fmset G bs)" using assms by (blast intro: divides_fmsubset fmsubset_divides) @@ -2331,7 +2331,7 @@ text {* Proper factors on multisets *} lemma (in factorial_monoid) fmset_properfactor: - assumes asubb: "fmset G as \# fmset G bs" + assumes asubb: "fmset G as \ fmset G bs" and anb: "fmset G as \ fmset G bs" and "wfactors G as a" and "wfactors G bs b" and "a \ carrier G" and "b \ carrier G" @@ -2341,10 +2341,10 @@ apply (rule fmsubset_divides[of as bs], fact+) proof assume "b divides a" - hence "fmset G bs \# fmset G as" + hence "fmset G bs \ fmset G as" by (rule divides_fmsubset) fact+ with asubb - have "fmset G as = fmset G bs" by (simp add: mset_le_antisym) + have "fmset G as = fmset G bs" by (rule order_antisym) with anb show "False" .. qed @@ -2354,7 +2354,7 @@ and "wfactors G as a" and "wfactors G bs b" and "a \ carrier G" and "b \ carrier G" and "set as \ carrier G" and "set bs \ carrier G" - shows "fmset G as \# fmset G bs \ fmset G as \ fmset G bs" + shows "fmset G as \ fmset G bs \ fmset G as \ fmset G bs" using pf apply (elim properfactorE) apply rule @@ -2738,12 +2738,12 @@ have "c gcdof a b" proof (simp add: isgcd_def, safe) from csmset - have "fmset G cs \# fmset G as" + have "fmset G cs \ fmset G as" by (simp add: multiset_inter_def mset_le_def) thus "c divides a" by (rule fmsubset_divides) fact+ next from csmset - have "fmset G cs \# fmset G bs" + have "fmset G cs \ fmset G bs" by (simp add: multiset_inter_def mset_le_def, force) thus "c divides b" by (rule fmsubset_divides) fact+ next @@ -2756,13 +2756,13 @@ by auto assume "y divides a" - hence ya: "fmset G ys \# fmset G as" by (rule divides_fmsubset) fact+ + hence ya: "fmset G ys \ fmset G as" by (rule divides_fmsubset) fact+ assume "y divides b" - hence yb: "fmset G ys \# fmset G bs" by (rule divides_fmsubset) fact+ + hence yb: "fmset G ys \ fmset G bs" by (rule divides_fmsubset) fact+ from ya yb csmset - have "fmset G ys \# fmset G cs" by (simp add: mset_le_def multiset_inter_count) + have "fmset G ys \ fmset G cs" by (simp add: mset_le_def multiset_inter_count) thus "y divides c" by (rule fmsubset_divides) fact+ qed @@ -2837,10 +2837,10 @@ have "c lcmof a b" proof (simp add: islcm_def, safe) - from csmset have "fmset G as \# fmset G cs" by (simp add: mset_le_def, force) + from csmset have "fmset G as \ fmset G cs" by (simp add: mset_le_def, force) thus "a divides c" by (rule fmsubset_divides) fact+ next - from csmset have "fmset G bs \# fmset G cs" by (simp add: mset_le_def) + from csmset have "fmset G bs \ fmset G cs" by (simp add: mset_le_def) thus "b divides c" by (rule fmsubset_divides) fact+ next fix y @@ -2852,13 +2852,13 @@ by auto assume "a divides y" - hence ya: "fmset G as \# fmset G ys" by (rule divides_fmsubset) fact+ + hence ya: "fmset G as \ fmset G ys" by (rule divides_fmsubset) fact+ assume "b divides y" - hence yb: "fmset G bs \# fmset G ys" by (rule divides_fmsubset) fact+ + hence yb: "fmset G bs \ fmset G ys" by (rule divides_fmsubset) fact+ from ya yb csmset - have "fmset G cs \# fmset G ys" + have "fmset G cs \ fmset G ys" apply (simp add: mset_le_def, clarify) apply (case_tac "count (fmset G as) a < count (fmset G bs) a") apply simp diff -r 9927471cca35 -r 3745987488b2 src/HOL/Algebra/abstract/Ring2.thy --- a/src/HOL/Algebra/abstract/Ring2.thy Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Algebra/abstract/Ring2.thy Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Algebras.thy --- a/src/HOL/Algebras.thy Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Algebras.thy Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Decision_Procs/commutative_ring_tac.ML --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Finite_Set.thy Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Groups.thy --- a/src/HOL/Groups.thy Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Groups.thy Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Import/Generate-HOL/GenHOL4Real.thy --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Import/HOL/arithmetic.imp --- a/src/HOL/Import/HOL/arithmetic.imp Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Import/HOL/arithmetic.imp Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Import/HOL/real.imp --- a/src/HOL/Import/HOL/real.imp Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Import/HOL/real.imp Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Import/HOL/realax.imp --- a/src/HOL/Import/HOL/realax.imp Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Import/HOL/realax.imp Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Import/HOLLight/hollight.imp --- a/src/HOL/Import/HOLLight/hollight.imp Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Import/HOLLight/hollight.imp Mon Feb 22 09:17:49 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 9927471cca35 -r 3745987488b2 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Sun Feb 21 23:05:37 2010 +0100 +++ b/src/HOL/Library/Multiset.thy Mon Feb 22 09:17:49 2010 +0100 @@ -176,64 +176,6 @@ by (simp add: multiset_eq_conv_count_eq) -subsubsection {* Intersection *} - -definition multiset_inter :: "'a multiset \ 'a multiset \ 'a multiset" (infixl "#\" 70) where - "multiset_inter A B = A - (A - B)" - -lemma multiset_inter_count: - "count (A #\ B) x = min (count A x) (count B x)" - by (simp add: multiset_inter_def multiset_typedef) - -lemma multiset_inter_commute: "A #\ B = B #\ A" - by (rule multi_count_ext) (simp add: multiset_inter_count) - -lemma multiset_inter_assoc: "A #\ (B #\ C) = A #\ B #\ C" - by (rule multi_count_ext) (simp add: multiset_inter_count) - -lemma multiset_inter_left_commute: "A #\ (B #\ C) = B #\ (A #\ C)" - by (rule multi_count_ext) (simp add: multiset_inter_count) - -lemmas multiset_inter_ac = - multiset_inter_commute - multiset_inter_assoc - multiset_inter_left_commute - -lemma multiset_inter_single: "a \ b \ {#a#} #\ {#b#} = {#}" - by (rule multi_count_ext) (auto simp add: multiset_inter_count) - -lemma multiset_union_diff_commute: - assumes "B #\ C = {#}" - shows "A + B - C = A - C + B" -proof (rule multi_count_ext) - fix x - from assms have "min (count B x) (count C x) = 0" - by (auto simp add: multiset_inter_count multiset_eq_conv_count_eq) - then have "count B x = 0 \ count C x = 0" - by auto - then show "count (A + B - C) x = count (A - C + B) x" - by auto -qed - - -subsubsection {* Comprehension (filter) *} - -lemma count_MCollect [simp]: - "count {# x:#M. P x #} a = (if P a then count M a else 0)" - by (simp add: MCollect_def in_multiset multiset_typedef) - -lemma MCollect_empty [simp]: "MCollect {#} P = {#}" - by (rule multi_count_ext) simp - -lemma MCollect_single [simp]: - "MCollect {#x#} P = (if P x then {#x#} else {#})" - by (rule multi_count_ext) simp - -lemma MCollect_union [simp]: - "MCollect (M + N) f = MCollect M f + MCollect N f" - by (rule multi_count_ext) simp - - subsubsection {* Equality of multisets *} lemma single_not_empty [simp]: "{#a#} \ {#} \ {#} \ {#a#}" @@ -335,64 +277,61 @@ subsubsection {* Pointwise ordering induced by count *} -definition mset_le :: "'a multiset \ 'a multiset \ bool" (infix "\#" 50) where - "A \# B \ (\a. count A a \ count B a)" +instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le +begin + +definition less_eq_multiset :: "'a multiset \ 'a multiset \ bool" where + mset_le_def: "A \ B \ (\a. count A a \ count B a)" -definition mset_less :: "'a multiset \ 'a multiset \ bool" (infix "<#" 50) where - "A <# B \ A \# B \ A \ B" +definition less_multiset :: "'a multiset \ 'a multiset \ bool" where + mset_less_def: "(A::'a multiset) < B \ A \ B \ A \ B" -notation mset_le (infix "\#" 50) -notation mset_less (infix "\#" 50) +instance proof +qed (auto simp add: mset_le_def mset_less_def multiset_eq_conv_count_eq intro: order_trans antisym) + +end lemma mset_less_eqI: - "(\x. count A x \ count B x) \ A \# B" + "(\x. count A x \ count B x) \ A \ B" by (simp add: mset_le_def) -lemma mset_le_refl[simp]: "A \# A" -unfolding mset_le_def by auto - -lemma mset_le_trans: "A \# B \ B \# C \ A \# C" -unfolding mset_le_def by (fast intro: order_trans) - -lemma mset_le_antisym: "A \# B \ B \# A \ A = B" -apply (unfold mset_le_def) -apply (rule multiset_eq_conv_count_eq [THEN iffD2]) -apply (blast intro: order_antisym) -done - -lemma mset_le_exists_conv: "(A \# B) = (\C. B = A + C)" +lemma mset_le_exists_conv: + "(A::'a multiset) \ B \ (\C. B = A + C)" apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI) apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2]) done -lemma mset_le_mono_add_right_cancel[simp]: "(A + C \# B + C) = (A \# B)" -unfolding mset_le_def by auto +lemma mset_le_mono_add_right_cancel [simp]: + "(A::'a multiset) + C \ B + C \ A \ B" + by (fact add_le_cancel_right) -lemma mset_le_mono_add_left_cancel[simp]: "(C + A \# C + B) = (A \# B)" -unfolding mset_le_def by auto +lemma mset_le_mono_add_left_cancel [simp]: + "C + (A::'a multiset) \ C + B \ A \ B" + by (fact add_le_cancel_left) + +lemma mset_le_mono_add: + "(A::'a multiset) \ B \ C \ D \ A + C \ B + D" + by (fact add_mono) -lemma mset_le_mono_add: "\ A \# B; C \# D \ \ A + C \# B + D" -apply (unfold mset_le_def) -apply auto -apply (erule_tac x = a in allE)+ -apply auto -done +lemma mset_le_add_left [simp]: + "(A::'a multiset) \ A + B" + unfolding mset_le_def by auto + +lemma mset_le_add_right [simp]: + "B \ (A::'a multiset) + B" + unfolding mset_le_def by auto -lemma mset_le_add_left[simp]: "A \# A + B" -unfolding mset_le_def by auto - -lemma mset_le_add_right[simp]: "B \# A + B" -unfolding mset_le_def by auto +lemma mset_le_single: + "a :# B \ {#a#} \ B" + by (simp add: mset_le_def) -lemma mset_le_single: "a :# B \ {#a#} \# B" -by (simp add: mset_le_def) - -lemma multiset_diff_union_assoc: "C \# B \ A + B - C = A + (B - C)" -by (simp add: multiset_eq_conv_count_eq mset_le_def) +lemma multiset_diff_union_assoc: + "C \ B \ (A::'a multiset) + B - C = A + (B - C)" + by (simp add: multiset_eq_conv_count_eq mset_le_def) lemma mset_le_multiset_union_diff_commute: -assumes "B \# A" -shows "A - B + C = A + C - B" + assumes "B \ A" + shows "(A::'a multiset) - B + C = A + C - B" proof - from mset_le_exists_conv [of "B" "A"] assms have "\D. A = B + D" .. from this obtain D where "A = B + D" .. @@ -410,31 +349,19 @@ done qed -interpretation mset_order: order "op \#" "op <#" -proof qed (auto intro: order.intro mset_le_refl mset_le_antisym - mset_le_trans simp: mset_less_def) - -interpretation mset_order_cancel_semigroup: - ordered_cancel_ab_semigroup_add "op +" "op \#" "op <#" -proof qed (erule mset_le_mono_add [OF mset_le_refl]) - -interpretation mset_order_semigroup_cancel: - ordered_ab_semigroup_add_imp_le "op +" "op \#" "op <#" -proof qed simp - -lemma mset_lessD: "A \# B \ x \# A \ x \# B" +lemma mset_lessD: "A < B \ x \# A \ x \# B" apply (clarsimp simp: mset_le_def mset_less_def) apply (erule_tac x=x in allE) apply auto done -lemma mset_leD: "A \# B \ x \# A \ x \# B" +lemma mset_leD: "A \ B \ x \# A \ x \# B" apply (clarsimp simp: mset_le_def mset_less_def) apply (erule_tac x = x in allE) apply auto done -lemma mset_less_insertD: "(A + {#x#} \# B) \ (x \# B \ A \# B)" +lemma mset_less_insertD: "(A + {#x#} < B) \ (x \# B \ A < B)" apply (rule conjI) apply (simp add: mset_lessD) apply (clarsimp simp: mset_le_def mset_less_def) @@ -443,30 +370,90 @@ apply (auto split: split_if_asm) done -lemma mset_le_insertD: "(A + {#x#} \# B) \ (x \# B \ A \# B)" +lemma mset_le_insertD: "(A + {#x#} \ B) \ (x \# B \ A \ B)" apply (rule conjI) apply (simp add: mset_leD) apply (force simp: mset_le_def mset_less_def split: split_if_asm) done -lemma mset_less_of_empty[simp]: "A \# {#} \ False" +lemma mset_less_of_empty[simp]: "A < {#} \ False" by (auto simp add: mset_less_def mset_le_def multiset_eq_conv_count_eq) -lemma multi_psub_of_add_self[simp]: "A \# A + {#x#}" -by (auto simp: mset_le_def mset_less_def) +lemma multi_psub_of_add_self[simp]: "A < A + {#x#}" + by (auto simp: mset_le_def mset_less_def) -lemma multi_psub_self[simp]: "A \# A = False" -by (auto simp: mset_le_def mset_less_def) +lemma multi_psub_self[simp]: "(A::'a multiset) < A = False" + by simp lemma mset_less_add_bothsides: - "T + {#x#} \# S + {#x#} \ T \# S" -by (auto simp: mset_le_def mset_less_def) + "T + {#x#} < S + {#x#} \ T < S" + by (fact add_less_imp_less_right) + +lemma mset_less_empty_nonempty: + "{#} < S \ S \ {#}" + by (auto simp: mset_le_def mset_less_def) + +lemma mset_less_diff_self: + "c \# B \ B - {#c#} < B" + by (auto simp: mset_le_def mset_less_def multiset_eq_conv_count_eq) + + +subsubsection {* Intersection *} + +instantiation multiset :: (type) semilattice_inf +begin + +definition inf_multiset :: "'a multiset \ 'a multiset \ 'a multiset" where + multiset_inter_def: "inf_multiset A B = A - (A - B)" + +instance proof - + have aux: "\m n q :: nat. m \ n \ m \ q \ m \ n - (n - q)" by arith + show "OFCLASS('a multiset, semilattice_inf_class)" proof + qed (auto simp add: multiset_inter_def mset_le_def aux) +qed + +end + +abbreviation multiset_inter :: "'a multiset \ 'a multiset \ 'a multiset" (infixl "#\" 70) where + "multiset_inter \ inf" -lemma mset_less_empty_nonempty: "({#} \# S) = (S \ {#})" -by (auto simp: mset_le_def mset_less_def) +lemma multiset_inter_count: + "count (A #\ B) x = min (count A x) (count B x)" + by (simp add: multiset_inter_def multiset_typedef) + +lemma multiset_inter_single: "a \ b \ {#a#} #\ {#b#} = {#}" + by (rule multi_count_ext) (auto simp add: multiset_inter_count) -lemma mset_less_diff_self: "c \# B \ B - {#c#} \# B" - by (auto simp: mset_le_def mset_less_def multiset_eq_conv_count_eq) +lemma multiset_union_diff_commute: + assumes "B #\ C = {#}" + shows "A + B - C = A - C + B" +proof (rule multi_count_ext) + fix x + from assms have "min (count B x) (count C x) = 0" + by (auto simp add: multiset_inter_count multiset_eq_conv_count_eq) + then have "count B x = 0 \ count C x = 0" + by auto + then show "count (A + B - C) x = count (A - C + B) x" + by auto +qed + + +subsubsection {* Comprehension (filter) *} + +lemma count_MCollect [simp]: + "count {# x:#M. P x #} a = (if P a then count M a else 0)" + by (simp add: MCollect_def in_multiset multiset_typedef) + +lemma MCollect_empty [simp]: "MCollect {#} P = {#}" + by (rule multi_count_ext) simp + +lemma MCollect_single [simp]: + "MCollect {#x#} P = (if P x then {#x#} else {#})" + by (rule multi_count_ext) simp + +lemma MCollect_union [simp]: + "MCollect (M + N) f = MCollect M f + MCollect N f" + by (rule multi_count_ext) simp subsubsection {* Set of elements *} @@ -657,7 +644,7 @@ apply auto done -lemma mset_less_size: "A \# B \ size A < size B" +lemma mset_less_size: "(A::'a multiset) < B \ size A < size B" proof (induct A arbitrary: B) case (empty M) then have "M \ {#}" by (simp add: mset_less_empty_nonempty) @@ -666,12 +653,12 @@ then show ?case by simp next case (add S x T) - have IH: "\B. S \# B \ size S < size B" by fact - have SxsubT: "S + {#x#} \# T" by fact - then have "x \# T" and "S \# T" by (auto dest: mset_less_insertD) + have IH: "\B. S < B \ size S < size B" by fact + have SxsubT: "S + {#x#} < T" by fact + then have "x \# T" and "S < T" by (auto dest: mset_less_insertD) then obtain T' where T: "T = T' + {#x#}" by (blast dest: multi_member_split) - then have "S \# T'" using SxsubT + then have "S < T'" using SxsubT by (blast intro: mset_less_add_bothsides) then have "size S < size T'" using IH by simp then show ?case using T by simp @@ -686,7 +673,7 @@ definition mset_less_rel :: "('a multiset * 'a multiset) set" where - "mset_less_rel = {(A,B). A \# B}" + "mset_less_rel = {(A,B). A < B}" lemma multiset_add_sub_el_shuffle: assumes "c \# B" and "b \ c" @@ -709,29 +696,29 @@ text {* The induction rules: *} lemma full_multiset_induct [case_names less]: -assumes ih: "\B. \A. A \# B \ P A \ P B" +assumes ih: "\B. \(A::'a multiset). A < B \ P A \ P B" shows "P B" apply (rule wf_mset_less_rel [THEN wf_induct]) apply (rule ih, auto simp: mset_less_rel_def) done lemma multi_subset_induct [consumes 2, case_names empty add]: -assumes "F \# A" +assumes "F \ A" and empty: "P {#}" and insert: "\a F. a \# A \ P F \ P (F + {#a#})" shows "P F" proof - - from `F \# A` + from `F \ A` show ?thesis proof (induct F) show "P {#}" by fact next fix x F - assume P: "F \# A \ P F" and i: "F + {#x#} \# A" + assume P: "F \ A \ P F" and i: "F + {#x#} \ A" show "P (F + {#x#})" proof (rule insert) from i show "x \# A" by (auto dest: mset_le_insertD) - from i have "F \# A" by (auto dest: mset_le_insertD) + from i have "F \ A" by (auto dest: mset_le_insertD) with P show "P F" . qed qed @@ -875,12 +862,8 @@ by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1) qed -lemma multiset_of_remdups_le: "multiset_of (remdups xs) \# multiset_of xs" -apply (induct xs) - apply auto -apply (rule mset_le_trans) - apply auto -done +lemma multiset_of_remdups_le: "multiset_of (remdups xs) \ multiset_of xs" + by (induct xs) (auto intro: order_trans) lemma multiset_of_update: "i < length ls \ multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}" @@ -969,7 +952,7 @@ by (simp add: multiset_eq_conv_count_eq count_of_filter) lemma mset_less_eq_Bag [code]: - "Bag xs \# A \ (\(x, n) \ set xs. count_of xs x \ count A x)" + "Bag xs \ A \ (\(x, n) \ set xs. count_of xs x \ count A x)" (is "?lhs \ ?rhs") proof assume ?lhs then show ?rhs @@ -990,10 +973,10 @@ begin definition - "HOL.eq A B \ A \# B \ B \# A" + "HOL.eq A B \ (A::'a multiset) \ B \ B \ A" instance proof -qed (simp add: eq_multiset_def mset_order.eq_iff) +qed (simp add: eq_multiset_def eq_iff) end @@ -1223,76 +1206,46 @@ subsubsection {* Partial-order properties *} -instantiation multiset :: (order) order -begin - -definition less_multiset_def: - "M' < M \ (M', M) \ mult {(x', x). x' < x}" - -definition le_multiset_def: - "M' <= M \ M' = M \ M' < (M::'a multiset)" - -lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}" -unfolding trans_def by (blast intro: order_less_trans) - -text {* - \medskip Irreflexivity. -*} +definition less_multiset :: "'a\order multiset \ 'a multiset \ bool" (infix "<#" 50) where + "M' <# M \ (M', M) \ mult {(x', x). x' < x}" -lemma mult_irrefl_aux: - "finite A ==> (\x \ A. \y \ A. x < (y::'a::order)) \ A = {}" -by (induct rule: finite_induct) (auto intro: order_less_trans) +definition le_multiset :: "'a\order multiset \ 'a multiset \ bool" (infix "<=#" 50) where + "M' <=# M \ M' <# M \ M' = M" -lemma mult_less_not_refl: "\ M < (M::'a::order multiset)" -apply (unfold less_multiset_def, auto) -apply (drule trans_base_order [THEN mult_implies_one_step], auto) -apply (drule finite_set_of [THEN mult_irrefl_aux [rule_format (no_asm)]]) -apply (simp add: set_of_eq_empty_iff) -done - -lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R" -using insert mult_less_not_refl by fast - - -text {* Transitivity. *} +notation (xsymbol) less_multiset (infix "\#" 50) +notation (xsymbol) le_multiset (infix "\#" 50) -theorem mult_less_trans: "K < M ==> M < N ==> K < (N::'a::order multiset)" -unfolding less_multiset_def mult_def by (blast intro: trancl_trans) - -text {* Asymmetry. *} - -theorem mult_less_not_sym: "M < N ==> \ N < (M::'a::order multiset)" -apply auto -apply (rule mult_less_not_refl [THEN notE]) -apply (erule mult_less_trans, assumption) -done - -theorem mult_less_asym: - "M < N ==> (\ P ==> N < (M::'a::order multiset)) ==> P" -using mult_less_not_sym by blast - -theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)" -unfolding le_multiset_def by auto +interpretation multiset_order: order le_multiset less_multiset +proof - + have irrefl: "\M :: 'a multiset. \ M \# M" + proof + fix M :: "'a multiset" + assume "M \# M" + then have MM: "(M, M) \ mult {(x, y). x < y}" by (simp add: less_multiset_def) + have "trans {(x'::'a, x). x' < x}" + by (rule transI) simp + moreover note MM + ultimately have "\I J K. M = I + J \ M = I + K + \ J \ {#} \ (\k\set_of K. \j\set_of J. (k, j) \ {(x, y). x < y})" + by (rule mult_implies_one_step) + then obtain I J K where "M = I + J" and "M = I + K" + and "J \ {#}" and "(\k\set_of K. \j\set_of J. (k, j) \ {(x, y). x < y})" by blast + then have aux1: "K \ {#}" and aux2: "\k\set_of K. \j\set_of K. k < j" by auto + have "finite (set_of K)" by simp + moreover note aux2 + ultimately have "set_of K = {}" + by (induct rule: finite_induct) (auto intro: order_less_trans) + with aux1 show False by simp + qed + have trans: "\K M N :: 'a multiset. K \# M \ M \# N \ K \# N" + unfolding less_multiset_def mult_def by (blast intro: trancl_trans) + show "order (le_multiset :: 'a multiset \ _) less_multiset" proof + qed (auto simp add: le_multiset_def irrefl dest: trans) +qed -text {* Anti-symmetry. *} - -theorem mult_le_antisym: - "M <= N ==> N <= M ==> M = (N::'a::order multiset)" -unfolding le_multiset_def by (blast dest: mult_less_not_sym) - -text {* Transitivity. *} - -theorem mult_le_trans: - "K <= M ==> M <= N ==> K <= (N::'a::order multiset)" -unfolding le_multiset_def by (blast intro: mult_less_trans) - -theorem mult_less_le: "(M < N) = (M <= N \ M \ (N::'a::order multiset))" -unfolding le_multiset_def by auto - -instance proof -qed (auto simp add: mult_less_le dest: mult_le_antisym elim: mult_le_trans) - -end +lemma mult_less_irrefl [elim!]: + "M \# (M::'a::order multiset) ==> R" + by (simp add: multiset_order.less_irrefl) subsubsection {* Monotonicity of multiset union *} @@ -1306,52 +1259,26 @@ apply (simp add: add_assoc) done -lemma union_less_mono2: "B < D ==> C + B < C + (D::'a::order multiset)" +lemma union_less_mono2: "B \# D ==> C + B \# C + (D::'a::order multiset)" apply (unfold less_multiset_def mult_def) apply (erule trancl_induct) apply (blast intro: mult1_union transI order_less_trans r_into_trancl) apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans) done -lemma union_less_mono1: "B < D ==> B + C < D + (C::'a::order multiset)" +lemma union_less_mono1: "B \# D ==> B + C \# D + (C::'a::order multiset)" apply (subst add_commute [of B C]) apply (subst add_commute [of D C]) apply (erule union_less_mono2) done lemma union_less_mono: - "A < C ==> B < D ==> A + B < C + (D::'a::order multiset)" -by (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans) - -lemma union_le_mono: - "A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)" -unfolding le_multiset_def -by (blast intro: union_less_mono union_less_mono1 union_less_mono2) + "A \# C ==> B \# D ==> A + B \# C + (D::'a::order multiset)" + by (blast intro!: union_less_mono1 union_less_mono2 multiset_order.less_trans) -lemma empty_leI [iff]: "{#} <= (M::'a::order multiset)" -apply (unfold le_multiset_def less_multiset_def) -apply (case_tac "M = {#}") - prefer 2 - apply (subgoal_tac "({#} + {#}, {#} + M) \ mult (Collect (split op <))") - prefer 2 - apply (rule one_step_implies_mult) - apply (simp only: trans_def) - apply auto -done - -lemma union_upper1: "A <= A + (B::'a::order multiset)" -proof - - have "A + {#} <= A + B" by (blast intro: union_le_mono) - then show ?thesis by simp -qed - -lemma union_upper2: "B <= A + (B::'a::order multiset)" -by (subst add_commute) (rule union_upper1) - -instance multiset :: (order) ordered_ab_semigroup_add -apply intro_classes -apply (erule union_le_mono[OF mult_le_refl]) -done +interpretation multiset_order: ordered_ab_semigroup_add plus le_multiset less_multiset +proof +qed (auto simp add: le_multiset_def intro: union_less_mono2) subsection {* The fold combinator *} @@ -1406,7 +1333,7 @@ "fold_msetG f z A x \