src/HOL/Library/Multiset.thy
changeset 10313 51e830bb7abe
parent 10277 081c8641aa11
child 10392 f27afee8475d
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Oct 23 22:12:04 2000 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Oct 23 22:17:55 2000 +0200
     1.3 @@ -47,9 +47,9 @@
     1.4    set_of :: "'a multiset => 'a set"
     1.5    "set_of M == {x. x :# M}"
     1.6  
     1.7 -instance multiset :: ("term") plus by intro_classes
     1.8 -instance multiset :: ("term") minus by intro_classes
     1.9 -instance multiset :: ("term") zero by intro_classes
    1.10 +instance multiset :: ("term") plus ..
    1.11 +instance multiset :: ("term") minus ..
    1.12 +instance multiset :: ("term") zero ..
    1.13  
    1.14  defs (overloaded)
    1.15    union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
    1.16 @@ -327,7 +327,7 @@
    1.17    apply auto
    1.18    done
    1.19  
    1.20 -lemma Rep_multiset_induct_aux:
    1.21 +lemma rep_multiset_induct_aux:
    1.22    "P (\<lambda>a. 0) ==> (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1)))
    1.23      ==> \<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
    1.24  proof -
    1.25 @@ -373,10 +373,10 @@
    1.26      done
    1.27  qed
    1.28  
    1.29 -theorem Rep_multiset_induct:
    1.30 +theorem rep_multiset_induct:
    1.31    "f \<in> multiset ==> P (\<lambda>a. 0) ==>
    1.32      (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f"
    1.33 -  apply (insert Rep_multiset_induct_aux)
    1.34 +  apply (insert rep_multiset_induct_aux)
    1.35    apply blast
    1.36    done
    1.37  
    1.38 @@ -388,7 +388,7 @@
    1.39    assume prem2 [unfolded defns]: "!!M x. P M ==> P (M + {#x#})"
    1.40    show ?thesis
    1.41      apply (rule Rep_multiset_inverse [THEN subst])
    1.42 -    apply (rule Rep_multiset [THEN Rep_multiset_induct])
    1.43 +    apply (rule Rep_multiset [THEN rep_multiset_induct])
    1.44       apply (rule prem1)
    1.45      apply (subgoal_tac "f (b := f b + 1) = (\<lambda>a. f a + (if a = b then 1 else 0))")
    1.46       prefer 2
    1.47 @@ -670,7 +670,7 @@
    1.48  
    1.49  subsubsection {* Partial-order properties *}
    1.50  
    1.51 -instance multiset :: ("term") ord by intro_classes
    1.52 +instance multiset :: ("term") ord ..
    1.53  
    1.54  defs (overloaded)
    1.55    less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"