src/HOL/Library/Multiset.thy
changeset 46730 e3b99d0231bc
parent 46394 68f973ffd763
child 46756 faf62905cd53
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Feb 28 17:11:18 2012 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Feb 28 20:20:09 2012 +0100
     1.3 @@ -208,11 +208,12 @@
     1.4    by auto
     1.5  
     1.6  lemma union_is_single:
     1.7 -  "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")proof
     1.8 +  "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")
     1.9 +proof
    1.10    assume ?rhs then show ?lhs by auto
    1.11  next
    1.12 -  assume ?lhs thus ?rhs
    1.13 -    by(simp add: multiset_eq_iff split:if_splits) (metis add_is_1)
    1.14 +  assume ?lhs then show ?rhs
    1.15 +    by (simp add: multiset_eq_iff split:if_splits) (metis add_is_1)
    1.16  qed
    1.17  
    1.18  lemma single_is_union:
    1.19 @@ -392,7 +393,7 @@
    1.20    by (simp add: multiset_inter_def multiset_typedef)
    1.21  
    1.22  lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
    1.23 -  by (rule multiset_eqI) (auto simp add: multiset_inter_count)
    1.24 +  by (rule multiset_eqI) auto
    1.25  
    1.26  lemma multiset_union_diff_commute:
    1.27    assumes "B #\<inter> C = {#}"
    1.28 @@ -400,7 +401,7 @@
    1.29  proof (rule multiset_eqI)
    1.30    fix x
    1.31    from assms have "min (count B x) (count C x) = 0"
    1.32 -    by (auto simp add: multiset_inter_count multiset_eq_iff)
    1.33 +    by (auto simp add: multiset_eq_iff)
    1.34    then have "count B x = 0 \<or> count C x = 0"
    1.35      by auto
    1.36    then show "count (A + B - C) x = count (A - C + B) x"
    1.37 @@ -948,15 +949,17 @@
    1.38    note *** = this [of "op <"] this [of "op >"] this [of "op ="]
    1.39    show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
    1.40    proof (cases "f l" ?pivot rule: linorder_cases)
    1.41 -    case less then moreover have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
    1.42 -    ultimately show ?thesis
    1.43 +    case less
    1.44 +    then have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
    1.45 +    with less show ?thesis
    1.46        by (simp add: filter_sort [symmetric] ** ***)
    1.47    next
    1.48      case equal then show ?thesis
    1.49        by (simp add: * less_le)
    1.50    next
    1.51 -    case greater then moreover have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto
    1.52 -    ultimately show ?thesis
    1.53 +    case greater
    1.54 +    then have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto
    1.55 +    with greater show ?thesis
    1.56        by (simp add: filter_sort [symmetric] ** ***)
    1.57    qed
    1.58  qed
    1.59 @@ -1200,7 +1203,7 @@
    1.60      (is "?lhs \<longleftrightarrow> ?rhs")
    1.61  proof
    1.62    assume ?lhs then show ?rhs
    1.63 -    by (auto simp add: mset_le_def count_Bag)
    1.64 +    by (auto simp add: mset_le_def)
    1.65  next
    1.66    assume ?rhs
    1.67    show ?lhs
    1.68 @@ -1209,7 +1212,7 @@
    1.69      from `?rhs` have "count_of (DAList.impl_of xs) x \<le> count A x"
    1.70        by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty)
    1.71      then show "count (Bag xs) x \<le> count A x"
    1.72 -      by (simp add: mset_le_def count_Bag)
    1.73 +      by (simp add: mset_le_def)
    1.74    qed
    1.75  qed
    1.76  
    1.77 @@ -1511,15 +1514,13 @@
    1.78    qed (auto simp add: le_multiset_def irrefl dest: trans)
    1.79  qed
    1.80  
    1.81 -lemma mult_less_irrefl [elim!]:
    1.82 -  "M \<subset># (M::'a::order multiset) ==> R"
    1.83 -  by (simp add: multiset_order.less_irrefl)
    1.84 +lemma mult_less_irrefl [elim!]: "M \<subset># (M::'a::order multiset) ==> R"
    1.85 +  by simp
    1.86  
    1.87  
    1.88  subsubsection {* Monotonicity of multiset union *}
    1.89  
    1.90 -lemma mult1_union:
    1.91 -  "(B, D) \<in> mult1 r ==> (C + B, C + D) \<in> mult1 r"
    1.92 +lemma mult1_union: "(B, D) \<in> mult1 r ==> (C + B, C + D) \<in> mult1 r"
    1.93  apply (unfold mult1_def)
    1.94  apply auto
    1.95  apply (rule_tac x = a in exI)
    1.96 @@ -1625,9 +1626,9 @@
    1.97        from MBb have BsubM: "B < M" by simp
    1.98        show ?case
    1.99        proof cases
   1.100 -        assume "b=c"
   1.101 -        then moreover have "B = C" using MBb MCc by auto
   1.102 -        ultimately show ?thesis using Bu Cv x\<^isub>1 x\<^isub>2 CsubM IH by auto
   1.103 +        assume *: "b = c"
   1.104 +        then have "B = C" using MBb MCc by auto
   1.105 +        with * show ?thesis using Bu Cv x\<^isub>1 x\<^isub>2 CsubM IH by auto
   1.106        next
   1.107          assume diff: "b \<noteq> c"
   1.108          let ?D = "B - {#c#}"
   1.109 @@ -1780,7 +1781,8 @@
   1.110    @{term "{#x+x|x:#M. x<c#}"}.
   1.111  *}
   1.112  
   1.113 -enriched_type image_mset: image_mset proof -
   1.114 +enriched_type image_mset: image_mset
   1.115 +proof -
   1.116    fix f g 
   1.117    show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
   1.118    proof