instantiation replacing primitive instance plus overloaded defs; more conservative type arities
authorhaftmann
Mon Apr 07 15:37:34 2008 +0200 (2008-04-07)
changeset 265677bcebb8c2d33
parent 26566 36a93808642c
child 26568 3a3a83493f00
instantiation replacing primitive instance plus overloaded defs; more conservative type arities
src/HOL/Library/Multiset.thy
     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.4  
     1.5  subsubsection {* Partial-order properties *}
     1.6  
     1.7 -instance multiset :: (type) ord ..
     1.8 +instantiation multiset :: (order) order
     1.9 +begin
    1.10  
    1.11 -defs (overloaded)
    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.19  
    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.25  
    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.36  
    1.37 +end
    1.38 +
    1.39  
    1.40  subsubsection {* Monotonicity of multiset union *}
    1.41