author haftmann Mon Apr 07 15:37:34 2008 +0200 (2008-04-07) changeset 26567 7bcebb8c2d33 parent 26566 36a93808642c child 26568 3a3a83493f00
instantiation replacing primitive instance plus overloaded defs; more conservative type arities
1.1 --- a/src/HOL/Library/Multiset.thy	Mon Apr 07 15:37:33 2008 +0200
1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Apr 07 15:37:34 2008 +0200
1.3 @@ -712,11 +712,14 @@
1.5  subsubsection {* Partial-order properties *}
1.7 -instance multiset :: (type) ord ..
1.8 +instantiation multiset :: (order) order
1.9 +begin
1.12 -  less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"
1.13 -  le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)"
1.14 +definition
1.15 +  less_multiset_def: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
1.16 +
1.17 +definition
1.18 +  le_multiset_def: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
1.20  lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
1.21  unfolding trans_def by (blast intro: order_less_trans)
1.22 @@ -775,9 +778,7 @@
1.23  theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
1.24  unfolding le_multiset_def by auto
1.26 -text {* Partial order. *}
1.27 -
1.28 -instance multiset :: (order) order
1.29 +instance
1.30  apply intro_classes
1.31     apply (rule mult_less_le)
1.32    apply (rule mult_le_refl)
1.33 @@ -785,6 +786,8 @@
1.34  apply (erule mult_le_antisym, assumption)
1.35  done
1.37 +end
1.38 +
1.40  subsubsection {* Monotonicity of multiset union *}