# HG changeset patch
# User wenzelm
# Date 971983364 -7200
# Node ID 081c8641aa110ab9435331e03d1671ed84bfba22
# Parent  75e2c6cb4153ac413028c5a7a932c665469a91ee
improved typedef;
tuned;

diff -r 75e2c6cb4153 -r 081c8641aa11 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Oct 19 21:22:05 2000 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Oct 19 21:22:44 2000 +0200
@@ -16,12 +16,12 @@
 
 typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}"
 proof
-  show "(\<lambda>x. 0::nat) \<in> {f. finite {x. 0 < f x}}"
-    by simp
+  show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp
 qed
 
 lemmas multiset_typedef [simp] =
-  Abs_multiset_inverse Rep_multiset_inverse Rep_multiset
+    Abs_multiset_inverse Rep_multiset_inverse Rep_multiset
+  and [simp] = Rep_multiset_inject [symmetric]
 
 constdefs
   Mempty :: "'a multiset"    ("{#}")
@@ -89,33 +89,6 @@
   apply auto
   done
 
-text {*
- \medskip Injectivity of @{term Rep_multiset}.
-*}  (* FIXME typedef package (!?) *)
-
-lemma multiset_eq_conv_Rep_eq [simp]:
-    "(M = N) = (Rep_multiset M = Rep_multiset N)"
-  apply (rule iffI)
-   apply simp
-  apply (drule_tac f = Abs_multiset in arg_cong)
-  apply simp
-  done
-
-(* FIXME
-Goal
- "[| f : multiset; g : multiset |] ==> \
-\ (Abs_multiset f = Abs_multiset g) = (!x. f x = g x)";
-by (rtac iffI 1);
- by (dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
- by (Asm_full_simp_tac 1);
-by (subgoal_tac "f = g" 1);
- by (Asm_simp_tac 1);
-by (rtac ext 1);
-by (Blast_tac 1);
-qed "Abs_multiset_eq";
-Addsimps [Abs_multiset_eq];
-*)
-
 
 subsection {* Algebraic properties of multisets *}
 
@@ -141,6 +114,13 @@
 
 theorems union_ac = union_assoc union_commute union_lcomm
 
+instance multiset :: ("term") plus_ac0
+  apply intro_classes
+    apply (rule union_commute)
+   apply (rule union_assoc)
+  apply simp
+  done
+
 
 subsubsection {* Difference *}
 
@@ -442,7 +422,7 @@
   apply auto
   done
 
-declare multiset_eq_conv_Rep_eq [simp del]
+declare Rep_multiset_inject [symmetric, simp del]
 declare multiset_typedef [simp del]
 
 theorem add_eq_conv_ex:
@@ -466,8 +446,7 @@
   "mult r == (mult1 r)^+"
 
 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
-  apply (simp add: mult1_def)
-  done
+  by (simp add: mult1_def)
 
 lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==>
     (\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or>
@@ -629,7 +608,7 @@
     apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
    apply (simp (no_asm_use) add: trans_def)
    apply blast
-  apply (subgoal_tac "a :# (M0 +{#a#})")
+  apply (subgoal_tac "a :# (M0 + {#a#})")
    apply simp
   apply (simp (no_asm))
   done
@@ -775,6 +754,18 @@
   apply auto
   done
 
+text {* Partial order. *}
+
+instance multiset :: (order) order
+  apply intro_classes
+     apply (rule mult_le_refl)
+    apply (erule mult_le_trans)
+    apply assumption
+   apply (erule mult_le_antisym)
+   apply assumption
+  apply (rule mult_less_le)
+  done
+
 
 subsubsection {* Monotonicity of multiset union *}
 
@@ -834,21 +825,4 @@
   apply (subst union_commute, rule union_upper1)
   done
 
-instance multiset :: (order) order
-  apply intro_classes
-     apply (rule mult_le_refl)
-    apply (erule mult_le_trans)
-    apply assumption
-   apply (erule mult_le_antisym)
-   apply assumption
-  apply (rule mult_less_le)
-  done
-
-instance multiset :: ("term") plus_ac0
-  apply intro_classes
-    apply (rule union_commute)
-   apply (rule union_assoc)
-  apply simp
-  done
-
 end