src/HOL/Library/Multiset.thy
changeset 11701 3d51fbf81c17
parent 11655 923e4d0d36d5
child 11868 56db9f3a6b3e
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4    "{#} == Abs_multiset (\<lambda>a. 0)"
     1.5  
     1.6    single :: "'a => 'a multiset"    ("{#_#}")
     1.7 -  "{#a#} == Abs_multiset (\<lambda>b. if b = a then 1' else 0)"
     1.8 +  "{#a#} == Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
     1.9  
    1.10    count :: "'a multiset => 'a => nat"
    1.11    "count == Rep_multiset"
    1.12 @@ -54,7 +54,7 @@
    1.13  defs (overloaded)
    1.14    union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
    1.15    diff_def: "M - N == Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
    1.16 -  Zero_def [simp]: "0 == {#}"
    1.17 +  Zero_multiset_def [simp]: "0 == {#}"
    1.18    size_def: "size M == setsum (count M) (set_of M)"
    1.19  
    1.20  
    1.21 @@ -66,7 +66,7 @@
    1.22    apply (simp add: multiset_def)
    1.23    done
    1.24  
    1.25 -lemma only1_in_multiset [simp]: "(\<lambda>b. if b = a then 1' else 0) \<in> multiset"
    1.26 +lemma only1_in_multiset [simp]: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset"
    1.27    apply (simp add: multiset_def)
    1.28    done
    1.29  
    1.30 @@ -139,7 +139,7 @@
    1.31    apply (simp add: count_def Mempty_def)
    1.32    done
    1.33  
    1.34 -theorem count_single [simp]: "count {#b#} a = (if b = a then 1' else 0)"
    1.35 +theorem count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
    1.36    apply (simp add: count_def single_def)
    1.37    done
    1.38  
    1.39 @@ -319,8 +319,8 @@
    1.40  subsection {* Induction over multisets *}
    1.41  
    1.42  lemma setsum_decr:
    1.43 -  "finite F ==> 0 < f a ==>
    1.44 -    setsum (f (a := f a - 1')) F = (if a \<in> F then setsum f F - 1 else setsum f F)"
    1.45 +  "finite F ==> (0::nat) < f a ==>
    1.46 +    setsum (f (a := f a - 1)) F = (if a \<in> F then setsum f F - 1 else setsum f F)"
    1.47    apply (erule finite_induct)
    1.48     apply auto
    1.49    apply (drule_tac a = a in mk_disjoint_insert)
    1.50 @@ -328,7 +328,7 @@
    1.51    done
    1.52  
    1.53  lemma rep_multiset_induct_aux:
    1.54 -  "P (\<lambda>a. 0) ==> (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1')))
    1.55 +  "P (\<lambda>a. (0::nat)) ==> (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1)))
    1.56      ==> \<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
    1.57  proof -
    1.58    case rule_context
    1.59 @@ -347,14 +347,14 @@
    1.60      apply (frule setsum_SucD)
    1.61      apply clarify
    1.62      apply (rename_tac a)
    1.63 -    apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1')) x}")
    1.64 +    apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}")
    1.65       prefer 2
    1.66       apply (rule finite_subset)
    1.67        prefer 2
    1.68        apply assumption
    1.69       apply simp
    1.70       apply blast
    1.71 -    apply (subgoal_tac "f = (f (a := f a - 1'))(a := (f (a := f a - 1')) a + 1')")
    1.72 +    apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)")
    1.73       prefer 2
    1.74       apply (rule ext)
    1.75       apply (simp (no_asm_simp))
    1.76 @@ -362,7 +362,7 @@
    1.77       apply blast
    1.78      apply (erule allE, erule impE, erule_tac [2] mp)
    1.79       apply blast
    1.80 -    apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply)
    1.81 +    apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
    1.82      apply (subgoal_tac "{x. x \<noteq> a --> 0 < f x} = {x. 0 < f x}")
    1.83       prefer 2
    1.84       apply blast
    1.85 @@ -375,7 +375,7 @@
    1.86  
    1.87  theorem rep_multiset_induct:
    1.88    "f \<in> multiset ==> P (\<lambda>a. 0) ==>
    1.89 -    (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1'))) ==> P f"
    1.90 +    (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f"
    1.91    apply (insert rep_multiset_induct_aux)
    1.92    apply blast
    1.93    done
    1.94 @@ -390,7 +390,7 @@
    1.95      apply (rule Rep_multiset_inverse [THEN subst])
    1.96      apply (rule Rep_multiset [THEN rep_multiset_induct])
    1.97       apply (rule prem1)
    1.98 -    apply (subgoal_tac "f (b := f b + 1') = (\<lambda>a. f a + (if a = b then 1' else 0))")
    1.99 +    apply (subgoal_tac "f (b := f b + 1) = (\<lambda>a. f a + (if a = b then 1 else 0))")
   1.100       prefer 2
   1.101       apply (simp add: expand_fun_eq)
   1.102      apply (erule ssubst)