src/HOL/Library/Multiset.thy
changeset 10277 081c8641aa11
parent 10249 e4d13d8a9011
child 10313 51e830bb7abe
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Oct 19 21:22:05 2000 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Oct 19 21:22:44 2000 +0200
     1.3 @@ -16,12 +16,12 @@
     1.4  
     1.5  typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}"
     1.6  proof
     1.7 -  show "(\<lambda>x. 0::nat) \<in> {f. finite {x. 0 < f x}}"
     1.8 -    by simp
     1.9 +  show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp
    1.10  qed
    1.11  
    1.12  lemmas multiset_typedef [simp] =
    1.13 -  Abs_multiset_inverse Rep_multiset_inverse Rep_multiset
    1.14 +    Abs_multiset_inverse Rep_multiset_inverse Rep_multiset
    1.15 +  and [simp] = Rep_multiset_inject [symmetric]
    1.16  
    1.17  constdefs
    1.18    Mempty :: "'a multiset"    ("{#}")
    1.19 @@ -89,33 +89,6 @@
    1.20    apply auto
    1.21    done
    1.22  
    1.23 -text {*
    1.24 - \medskip Injectivity of @{term Rep_multiset}.
    1.25 -*}  (* FIXME typedef package (!?) *)
    1.26 -
    1.27 -lemma multiset_eq_conv_Rep_eq [simp]:
    1.28 -    "(M = N) = (Rep_multiset M = Rep_multiset N)"
    1.29 -  apply (rule iffI)
    1.30 -   apply simp
    1.31 -  apply (drule_tac f = Abs_multiset in arg_cong)
    1.32 -  apply simp
    1.33 -  done
    1.34 -
    1.35 -(* FIXME
    1.36 -Goal
    1.37 - "[| f : multiset; g : multiset |] ==> \
    1.38 -\ (Abs_multiset f = Abs_multiset g) = (!x. f x = g x)";
    1.39 -by (rtac iffI 1);
    1.40 - by (dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
    1.41 - by (Asm_full_simp_tac 1);
    1.42 -by (subgoal_tac "f = g" 1);
    1.43 - by (Asm_simp_tac 1);
    1.44 -by (rtac ext 1);
    1.45 -by (Blast_tac 1);
    1.46 -qed "Abs_multiset_eq";
    1.47 -Addsimps [Abs_multiset_eq];
    1.48 -*)
    1.49 -
    1.50  
    1.51  subsection {* Algebraic properties of multisets *}
    1.52  
    1.53 @@ -141,6 +114,13 @@
    1.54  
    1.55  theorems union_ac = union_assoc union_commute union_lcomm
    1.56  
    1.57 +instance multiset :: ("term") plus_ac0
    1.58 +  apply intro_classes
    1.59 +    apply (rule union_commute)
    1.60 +   apply (rule union_assoc)
    1.61 +  apply simp
    1.62 +  done
    1.63 +
    1.64  
    1.65  subsubsection {* Difference *}
    1.66  
    1.67 @@ -442,7 +422,7 @@
    1.68    apply auto
    1.69    done
    1.70  
    1.71 -declare multiset_eq_conv_Rep_eq [simp del]
    1.72 +declare Rep_multiset_inject [symmetric, simp del]
    1.73  declare multiset_typedef [simp del]
    1.74  
    1.75  theorem add_eq_conv_ex:
    1.76 @@ -466,8 +446,7 @@
    1.77    "mult r == (mult1 r)^+"
    1.78  
    1.79  lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
    1.80 -  apply (simp add: mult1_def)
    1.81 -  done
    1.82 +  by (simp add: mult1_def)
    1.83  
    1.84  lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==>
    1.85      (\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or>
    1.86 @@ -629,7 +608,7 @@
    1.87      apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
    1.88     apply (simp (no_asm_use) add: trans_def)
    1.89     apply blast
    1.90 -  apply (subgoal_tac "a :# (M0 +{#a#})")
    1.91 +  apply (subgoal_tac "a :# (M0 + {#a#})")
    1.92     apply simp
    1.93    apply (simp (no_asm))
    1.94    done
    1.95 @@ -775,6 +754,18 @@
    1.96    apply auto
    1.97    done
    1.98  
    1.99 +text {* Partial order. *}
   1.100 +
   1.101 +instance multiset :: (order) order
   1.102 +  apply intro_classes
   1.103 +     apply (rule mult_le_refl)
   1.104 +    apply (erule mult_le_trans)
   1.105 +    apply assumption
   1.106 +   apply (erule mult_le_antisym)
   1.107 +   apply assumption
   1.108 +  apply (rule mult_less_le)
   1.109 +  done
   1.110 +
   1.111  
   1.112  subsubsection {* Monotonicity of multiset union *}
   1.113  
   1.114 @@ -834,21 +825,4 @@
   1.115    apply (subst union_commute, rule union_upper1)
   1.116    done
   1.117  
   1.118 -instance multiset :: (order) order
   1.119 -  apply intro_classes
   1.120 -     apply (rule mult_le_refl)
   1.121 -    apply (erule mult_le_trans)
   1.122 -    apply assumption
   1.123 -   apply (erule mult_le_antisym)
   1.124 -   apply assumption
   1.125 -  apply (rule mult_less_le)
   1.126 -  done
   1.127 -
   1.128 -instance multiset :: ("term") plus_ac0
   1.129 -  apply intro_classes
   1.130 -    apply (rule union_commute)
   1.131 -   apply (rule union_assoc)
   1.132 -  apply simp
   1.133 -  done
   1.134 -
   1.135  end