src/ZF/Induct/Multiset.thy

 (*  Title:      ZF/Induct/Multiset.thy
-    ID:         $Id$
     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
 
 A definitional theory of multisets,
 including a wellfoundedness proof for the multiset order.
 

        else 0"
 
 definition
   mdiff  :: "[i, i] => i" (infixl "-#" 65)  where
   "M -# N ==  normalize(\<lambda>x \<in> mset_of(M).
-			if x \<in> mset_of(N) then M`x #- N`x else M`x)"
+                        if x \<in> mset_of(N) then M`x #- N`x else M`x)"
 
 definition
   (* set of elements of a multiset *)
   msingle :: "i => i"    ("{#_#}")  where
   "{#a#} == {<a, 1>}"

       \<exists>a \<in> A. \<exists>M0 \<in> Mult(A). \<exists>K \<in> Mult(A).
       N=M0 +# {#a#} & M=M0 +# K & (\<forall>b \<in> mset_of(K). <b,a> \<in> r)}"
 
 definition
   multirel :: "[i, i] => i"  where
-  "multirel(A, r) == multirel1(A, r)^+" 		
+  "multirel(A, r) == multirel1(A, r)^+"                 
 
   (* ordinal multiset orderings *)
 
 definition
   omultiset :: "i => o"  where

 apply (auto simp del: int_of_0 simp add: int_of_add [symmetric] int_of_0 [symmetric])
 done
 
 lemma setsum_mcount_Int:
      "Finite(A) ==> setsum(%a. $# mcount(N, a), A Int mset_of(N))
-		  = setsum(%a. $# mcount(N, a), A)"
+                  = setsum(%a. $# mcount(N, a), A)"
 apply (induct rule: Finite_induct)
  apply auto
 apply (subgoal_tac "Finite (B Int mset_of (N))")
 prefer 2 apply (blast intro: subset_Finite)
 apply (auto simp add: mcount_def Int_cons_left)