src/HOL/Library/Multiset.thy
changeset 46921 aa862ff8a8a9
parent 46756 faf62905cd53
child 47143 212f7a975d49
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Mar 14 15:37:51 2012 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Mar 14 15:59:39 2012 +0100
     1.3 @@ -118,8 +118,8 @@
     1.4  lemma count_union [simp]: "count (M + N) a = count M a + count N a"
     1.5    by (simp add: union_def in_multiset multiset_typedef)
     1.6  
     1.7 -instance multiset :: (type) cancel_comm_monoid_add proof
     1.8 -qed (simp_all add: multiset_eq_iff)
     1.9 +instance multiset :: (type) cancel_comm_monoid_add
    1.10 +  by default (simp_all add: multiset_eq_iff)
    1.11  
    1.12  
    1.13  subsubsection {* Difference *}
    1.14 @@ -270,8 +270,8 @@
    1.15  definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
    1.16    mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
    1.17  
    1.18 -instance proof
    1.19 -qed (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)
    1.20 +instance
    1.21 +  by default (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)
    1.22  
    1.23  end
    1.24  
    1.25 @@ -377,10 +377,11 @@
    1.26  definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
    1.27    multiset_inter_def: "inf_multiset A B = A - (A - B)"
    1.28  
    1.29 -instance proof -
    1.30 +instance
    1.31 +proof -
    1.32    have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
    1.33 -  show "OFCLASS('a multiset, semilattice_inf_class)" proof
    1.34 -  qed (auto simp add: multiset_inter_def mset_le_def aux)
    1.35 +  show "OFCLASS('a multiset, semilattice_inf_class)"
    1.36 +    by default (auto simp add: multiset_inter_def mset_le_def aux)
    1.37  qed
    1.38  
    1.39  end
    1.40 @@ -822,7 +823,8 @@
    1.41  lemma multiset_of_eq_length:
    1.42    assumes "multiset_of xs = multiset_of ys"
    1.43    shows "length xs = length ys"
    1.44 -using assms proof (induct xs arbitrary: ys)
    1.45 +using assms
    1.46 +proof (induct xs arbitrary: ys)
    1.47    case Nil then show ?case by simp
    1.48  next
    1.49    case (Cons x xs)
    1.50 @@ -845,7 +847,8 @@
    1.51  next
    1.52    case True
    1.53    moreover have "z \<in># multiset_of ys" using assms True by simp
    1.54 -  show ?thesis using assms proof (induct xs arbitrary: ys)
    1.55 +  show ?thesis using assms
    1.56 +  proof (induct xs arbitrary: ys)
    1.57      case Nil then show ?case by simp
    1.58    next
    1.59      case (Cons x xs)
    1.60 @@ -864,7 +867,8 @@
    1.61    assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
    1.62      and equiv: "multiset_of xs = multiset_of ys"
    1.63    shows "fold f xs = fold f ys"
    1.64 -using f equiv [symmetric] proof (induct xs arbitrary: ys)
    1.65 +using f equiv [symmetric]
    1.66 +proof (induct xs arbitrary: ys)
    1.67    case Nil then show ?case by simp
    1.68  next
    1.69    case (Cons x xs)
    1.70 @@ -898,7 +902,8 @@
    1.71    and "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs"
    1.72    and "sorted (map f ys)"
    1.73    shows "sort_key f xs = ys"
    1.74 -using assms proof (induct xs arbitrary: ys)
    1.75 +using assms
    1.76 +proof (induct xs arbitrary: ys)
    1.77    case Nil then show ?case by simp
    1.78  next
    1.79    case (Cons x xs)
    1.80 @@ -994,10 +999,12 @@
    1.81  proof (cases xs)
    1.82    case Nil then show ?thesis by simp
    1.83  next
    1.84 -  case (Cons _ ys) note hyps = Cons show ?thesis proof (cases ys)
    1.85 +  case (Cons _ ys) note hyps = Cons show ?thesis
    1.86 +  proof (cases ys)
    1.87      case Nil with hyps show ?thesis by simp
    1.88    next
    1.89 -    case (Cons _ zs) note hyps = hyps Cons show ?thesis proof (cases zs)
    1.90 +    case (Cons _ zs) note hyps = hyps Cons show ?thesis
    1.91 +    proof (cases zs)
    1.92        case Nil with hyps show ?thesis by auto
    1.93      next
    1.94        case Cons 
    1.95 @@ -1224,8 +1231,8 @@
    1.96  definition
    1.97    [code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
    1.98  
    1.99 -instance proof
   1.100 -qed (simp add: equal_multiset_def eq_iff)
   1.101 +instance
   1.102 +  by default (simp add: equal_multiset_def eq_iff)
   1.103  
   1.104  end
   1.105  
   1.106 @@ -1512,8 +1519,8 @@
   1.107    qed
   1.108    have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
   1.109      unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
   1.110 -  show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
   1.111 -  qed (auto simp add: le_multiset_def irrefl dest: trans)
   1.112 +  show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
   1.113 +    by default (auto simp add: le_multiset_def irrefl dest: trans)
   1.114  qed
   1.115  
   1.116  lemma mult_less_irrefl [elim!]: "M \<subset># (M::'a::order multiset) ==> R"
   1.117 @@ -1785,14 +1792,12 @@
   1.118  
   1.119  enriched_type image_mset: image_mset
   1.120  proof -
   1.121 -  fix f g 
   1.122 -  show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
   1.123 +  fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
   1.124    proof
   1.125      fix A
   1.126      show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
   1.127        by (induct A) simp_all
   1.128    qed
   1.129 -next
   1.130    show "image_mset id = id"
   1.131    proof
   1.132      fix A