new material courtesy of Norbert Voelker
authorpaulson
Thu Jul 22 10:33:26 2004 +0200 (2004-07-22)
changeset 150724861bf6af0b4
parent 15071 b65fc0787fbe
child 15073 279c2daaf517
new material courtesy of Norbert Voelker
src/HOL/Library/Multiset.thy
src/HOL/Library/Permutation.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Jul 21 16:35:38 2004 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Jul 22 10:33:26 2004 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/Library/Multiset.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson
     1.7 +    Author:     Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker
     1.8  *)
     1.9  
    1.10  header {* Multisets *}
    1.11 @@ -56,26 +56,21 @@
    1.12  *}
    1.13  
    1.14  lemma const0_in_multiset [simp]: "(\<lambda>a. 0) \<in> multiset"
    1.15 -  apply (simp add: multiset_def)
    1.16 -  done
    1.17 +by (simp add: multiset_def)
    1.18  
    1.19  lemma only1_in_multiset [simp]: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset"
    1.20 -  apply (simp add: multiset_def)
    1.21 -  done
    1.22 +by (simp add: multiset_def)
    1.23  
    1.24  lemma union_preserves_multiset [simp]:
    1.25      "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset"
    1.26 -  apply (unfold multiset_def)
    1.27 -  apply simp
    1.28 -  apply (drule finite_UnI)
    1.29 -   apply assumption
    1.30 +  apply (unfold multiset_def, simp)
    1.31 +  apply (drule finite_UnI, assumption)
    1.32    apply (simp del: finite_Un add: Un_def)
    1.33    done
    1.34  
    1.35  lemma diff_preserves_multiset [simp]:
    1.36      "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset"
    1.37 -  apply (unfold multiset_def)
    1.38 -  apply simp
    1.39 +  apply (unfold multiset_def, simp)
    1.40    apply (rule finite_subset)
    1.41     prefer 2
    1.42     apply assumption
    1.43 @@ -88,16 +83,13 @@
    1.44  subsubsection {* Union *}
    1.45  
    1.46  theorem union_empty [simp]: "M + {#} = M \<and> {#} + M = M"
    1.47 -  apply (simp add: union_def Mempty_def)
    1.48 -  done
    1.49 +by (simp add: union_def Mempty_def)
    1.50  
    1.51  theorem union_commute: "M + N = N + (M::'a multiset)"
    1.52 -  apply (simp add: union_def add_ac)
    1.53 -  done
    1.54 +by (simp add: union_def add_ac)
    1.55  
    1.56  theorem union_assoc: "(M + N) + K = M + (N + (K::'a multiset))"
    1.57 -  apply (simp add: union_def add_ac)
    1.58 -  done
    1.59 +by (simp add: union_def add_ac)
    1.60  
    1.61  theorem union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))"
    1.62    apply (rule union_commute [THEN trans])
    1.63 @@ -119,65 +111,52 @@
    1.64  subsubsection {* Difference *}
    1.65  
    1.66  theorem diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
    1.67 -  apply (simp add: Mempty_def diff_def)
    1.68 -  done
    1.69 +by (simp add: Mempty_def diff_def)
    1.70  
    1.71  theorem diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
    1.72 -  apply (simp add: union_def diff_def)
    1.73 -  done
    1.74 +by (simp add: union_def diff_def)
    1.75  
    1.76  
    1.77  subsubsection {* Count of elements *}
    1.78  
    1.79  theorem count_empty [simp]: "count {#} a = 0"
    1.80 -  apply (simp add: count_def Mempty_def)
    1.81 -  done
    1.82 +by (simp add: count_def Mempty_def)
    1.83  
    1.84  theorem count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
    1.85 -  apply (simp add: count_def single_def)
    1.86 -  done
    1.87 +by (simp add: count_def single_def)
    1.88  
    1.89  theorem count_union [simp]: "count (M + N) a = count M a + count N a"
    1.90 -  apply (simp add: count_def union_def)
    1.91 -  done
    1.92 +by (simp add: count_def union_def)
    1.93  
    1.94  theorem count_diff [simp]: "count (M - N) a = count M a - count N a"
    1.95 -  apply (simp add: count_def diff_def)
    1.96 -  done
    1.97 +by (simp add: count_def diff_def)
    1.98  
    1.99  
   1.100  subsubsection {* Set of elements *}
   1.101  
   1.102  theorem set_of_empty [simp]: "set_of {#} = {}"
   1.103 -  apply (simp add: set_of_def)
   1.104 -  done
   1.105 +by (simp add: set_of_def)
   1.106  
   1.107  theorem set_of_single [simp]: "set_of {#b#} = {b}"
   1.108 -  apply (simp add: set_of_def)
   1.109 -  done
   1.110 +by (simp add: set_of_def)
   1.111  
   1.112  theorem set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N"
   1.113 -  apply (auto simp add: set_of_def)
   1.114 -  done
   1.115 +by (auto simp add: set_of_def)
   1.116  
   1.117  theorem set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
   1.118 -  apply (auto simp add: set_of_def Mempty_def count_def expand_fun_eq)
   1.119 -  done
   1.120 +by (auto simp add: set_of_def Mempty_def count_def expand_fun_eq)
   1.121  
   1.122  theorem mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
   1.123 -  apply (auto simp add: set_of_def)
   1.124 -  done
   1.125 +by (auto simp add: set_of_def)
   1.126  
   1.127  
   1.128  subsubsection {* Size *}
   1.129  
   1.130  theorem size_empty [simp]: "size {#} = 0"
   1.131 -  apply (simp add: size_def)
   1.132 -  done
   1.133 +by (simp add: size_def)
   1.134  
   1.135  theorem size_single [simp]: "size {#b#} = 1"
   1.136 -  apply (simp add: size_def)
   1.137 -  done
   1.138 +by (simp add: size_def)
   1.139  
   1.140  theorem finite_set_of [iff]: "finite (set_of M)"
   1.141    apply (cut_tac x = M in Rep_multiset)
   1.142 @@ -186,8 +165,7 @@
   1.143  
   1.144  theorem setsum_count_Int:
   1.145      "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
   1.146 -  apply (erule finite_induct)
   1.147 -   apply simp
   1.148 +  apply (erule finite_induct, simp)
   1.149    apply (simp add: Int_insert_left set_of_def)
   1.150    done
   1.151  
   1.152 @@ -195,66 +173,54 @@
   1.153    apply (unfold size_def)
   1.154    apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
   1.155     prefer 2
   1.156 -   apply (rule ext)
   1.157 -   apply simp
   1.158 +   apply (rule ext, simp)
   1.159    apply (simp (no_asm_simp) add: setsum_Un setsum_addf setsum_count_Int)
   1.160    apply (subst Int_commute)
   1.161    apply (simp (no_asm_simp) add: setsum_count_Int)
   1.162    done
   1.163  
   1.164  theorem size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
   1.165 -  apply (unfold size_def Mempty_def count_def)
   1.166 -  apply auto
   1.167 +  apply (unfold size_def Mempty_def count_def, auto)
   1.168    apply (simp add: set_of_def count_def expand_fun_eq)
   1.169    done
   1.170  
   1.171  theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M"
   1.172    apply (unfold size_def)
   1.173 -  apply (drule setsum_SucD)
   1.174 -  apply auto
   1.175 +  apply (drule setsum_SucD, auto)
   1.176    done
   1.177  
   1.178  
   1.179  subsubsection {* Equality of multisets *}
   1.180  
   1.181  theorem multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)"
   1.182 -  apply (simp add: count_def expand_fun_eq)
   1.183 -  done
   1.184 +by (simp add: count_def expand_fun_eq)
   1.185  
   1.186  theorem single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
   1.187 -  apply (simp add: single_def Mempty_def expand_fun_eq)
   1.188 -  done
   1.189 +by (simp add: single_def Mempty_def expand_fun_eq)
   1.190  
   1.191  theorem single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)"
   1.192 -  apply (auto simp add: single_def expand_fun_eq)
   1.193 -  done
   1.194 +by (auto simp add: single_def expand_fun_eq)
   1.195  
   1.196  theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})"
   1.197 -  apply (auto simp add: union_def Mempty_def expand_fun_eq)
   1.198 -  done
   1.199 +by (auto simp add: union_def Mempty_def expand_fun_eq)
   1.200  
   1.201  theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})"
   1.202 -  apply (auto simp add: union_def Mempty_def expand_fun_eq)
   1.203 -  done
   1.204 +by (auto simp add: union_def Mempty_def expand_fun_eq)
   1.205  
   1.206  theorem union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))"
   1.207 -  apply (simp add: union_def expand_fun_eq)
   1.208 -  done
   1.209 +by (simp add: union_def expand_fun_eq)
   1.210  
   1.211  theorem union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))"
   1.212 -  apply (simp add: union_def expand_fun_eq)
   1.213 -  done
   1.214 +by (simp add: union_def expand_fun_eq)
   1.215  
   1.216  theorem union_is_single:
   1.217      "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
   1.218 -  apply (unfold Mempty_def single_def union_def)
   1.219 -  apply (simp add: add_is_1 expand_fun_eq)
   1.220 +  apply (simp add: Mempty_def single_def union_def add_is_1 expand_fun_eq)
   1.221    apply blast
   1.222    done
   1.223  
   1.224  theorem single_is_union:
   1.225 -  "({#a#} = M + N) =
   1.226 -    ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
   1.227 +     "({#a#} = M + N) = ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
   1.228    apply (unfold Mempty_def single_def union_def)
   1.229    apply (simp add: add_is_1 one_is_add expand_fun_eq)
   1.230    apply (blast dest: sym)
   1.231 @@ -262,14 +228,10 @@
   1.232  
   1.233  theorem add_eq_conv_diff:
   1.234    "(M + {#a#} = N + {#b#}) =
   1.235 -    (M = N \<and> a = b \<or>
   1.236 -      M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})"
   1.237 +   (M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})"
   1.238    apply (unfold single_def union_def diff_def)
   1.239    apply (simp (no_asm) add: expand_fun_eq)
   1.240 -  apply (rule conjI)
   1.241 -   apply force
   1.242 -  apply safe
   1.243 -  apply simp_all
   1.244 +  apply (rule conjI, force, safe, simp_all)
   1.245    apply (simp add: eq_sym_conv)
   1.246    done
   1.247  
   1.248 @@ -278,15 +240,15 @@
   1.249   "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
   1.250  by (res_inst_tac [("a","F"),("f","\<lambda>A. if finite A then card A else 0")]
   1.251       measure_induct 1);
   1.252 -by (Clarify_tac 1);
   1.253 -by (resolve_tac prems 1);
   1.254 - by (assume_tac 1);
   1.255 -by (Clarify_tac 1);
   1.256 -by (subgoal_tac "finite G" 1);
   1.257 +by (Clarify_tac 1)
   1.258 +by (resolve_tac prems 1)
   1.259 + by (assume_tac 1)
   1.260 +by (Clarify_tac 1)
   1.261 +by (subgoal_tac "finite G" 1)
   1.262   by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
   1.263 -by (etac allE 1);
   1.264 -by (etac impE 1);
   1.265 - by (Blast_tac 2);
   1.266 +by (etac allE 1)
   1.267 +by (etac impE 1)
   1.268 + by (Blast_tac 2)
   1.269  by (asm_simp_tac (simpset() addsimps [psubset_card]) 1);
   1.270  no_qed();
   1.271  val lemma = result();
   1.272 @@ -305,11 +267,9 @@
   1.273  
   1.274  lemma setsum_decr:
   1.275    "finite F ==> (0::nat) < f a ==>
   1.276 -    setsum (f (a := f a - 1)) F = (if a \<in> F then setsum f F - 1 else setsum f F)"
   1.277 -  apply (erule finite_induct)
   1.278 -   apply auto
   1.279 -  apply (drule_tac a = a in mk_disjoint_insert)
   1.280 -  apply auto
   1.281 +    setsum (f (a := f a - 1)) F = (if a\<in>F then setsum f F - 1 else setsum f F)"
   1.282 +  apply (erule finite_induct, auto)
   1.283 +  apply (drule_tac a = a in mk_disjoint_insert, auto)
   1.284    done
   1.285  
   1.286  lemma rep_multiset_induct_aux:
   1.287 @@ -320,17 +280,12 @@
   1.288    note premises = this [unfolded multiset_def]
   1.289    show ?thesis
   1.290      apply (unfold multiset_def)
   1.291 -    apply (induct_tac n)
   1.292 -     apply simp
   1.293 -     apply clarify
   1.294 +    apply (induct_tac n, simp, clarify)
   1.295       apply (subgoal_tac "f = (\<lambda>a.0)")
   1.296        apply simp
   1.297        apply (rule premises)
   1.298 -     apply (rule ext)
   1.299 -     apply force
   1.300 -    apply clarify
   1.301 -    apply (frule setsum_SucD)
   1.302 -    apply clarify
   1.303 +     apply (rule ext, force, clarify)
   1.304 +    apply (frule setsum_SucD, clarify)
   1.305      apply (rename_tac a)
   1.306      apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}")
   1.307       prefer 2
   1.308 @@ -343,10 +298,8 @@
   1.309       prefer 2
   1.310       apply (rule ext)
   1.311       apply (simp (no_asm_simp))
   1.312 -     apply (erule ssubst, rule premises)
   1.313 -     apply blast
   1.314 -    apply (erule allE, erule impE, erule_tac [2] mp)
   1.315 -     apply blast
   1.316 +     apply (erule ssubst, rule premises, blast)
   1.317 +    apply (erule allE, erule impE, erule_tac [2] mp, blast)
   1.318      apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
   1.319      apply (subgoal_tac "{x. x \<noteq> a --> 0 < f x} = {x. 0 < f x}")
   1.320       prefer 2
   1.321 @@ -361,9 +314,7 @@
   1.322  theorem rep_multiset_induct:
   1.323    "f \<in> multiset ==> P (\<lambda>a. 0) ==>
   1.324      (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f"
   1.325 -  apply (insert rep_multiset_induct_aux)
   1.326 -  apply blast
   1.327 -  done
   1.328 +  by (insert rep_multiset_induct_aux, blast)
   1.329  
   1.330  theorem multiset_induct [induct type: multiset]:
   1.331    "P {#} ==> (!!M x. P M ==> P (M + {#x#})) ==> P M"
   1.332 @@ -375,7 +326,7 @@
   1.333      apply (rule Rep_multiset_inverse [THEN subst])
   1.334      apply (rule Rep_multiset [THEN rep_multiset_induct])
   1.335       apply (rule prem1)
   1.336 -    apply (subgoal_tac "f (b := f b + 1) = (\<lambda>a. f a + (if a = b then 1 else 0))")
   1.337 +    apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))")
   1.338       prefer 2
   1.339       apply (simp add: expand_fun_eq)
   1.340      apply (erule ssubst)
   1.341 @@ -388,33 +339,26 @@
   1.342  lemma MCollect_preserves_multiset:
   1.343      "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset"
   1.344    apply (simp add: multiset_def)
   1.345 -  apply (rule finite_subset)
   1.346 -   apply auto
   1.347 +  apply (rule finite_subset, auto)
   1.348    done
   1.349  
   1.350  theorem count_MCollect [simp]:
   1.351      "count {# x:M. P x #} a = (if P a then count M a else 0)"
   1.352 -  apply (unfold count_def MCollect_def)
   1.353 -  apply (simp add: MCollect_preserves_multiset)
   1.354 -  done
   1.355 +  by (simp add: count_def MCollect_def MCollect_preserves_multiset)
   1.356  
   1.357  theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \<inter> {x. P x}"
   1.358 -  apply (auto simp add: set_of_def)
   1.359 -  done
   1.360 +by (auto simp add: set_of_def)
   1.361  
   1.362  theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}"
   1.363 -  apply (subst multiset_eq_conv_count_eq)
   1.364 -  apply auto
   1.365 -  done
   1.366 +by (subst multiset_eq_conv_count_eq, auto)
   1.367  
   1.368  declare Rep_multiset_inject [symmetric, simp del]
   1.369  declare multiset_typedef [simp del]
   1.370  
   1.371  theorem add_eq_conv_ex:
   1.372 -  "(M + {#a#} = N + {#b#}) =
   1.373 -    (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
   1.374 -  apply (auto simp add: add_eq_conv_diff)
   1.375 -  done
   1.376 +      "(M + {#a#} = N + {#b#}) =
   1.377 +       (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
   1.378 +  by (auto simp add: add_eq_conv_diff)
   1.379  
   1.380  
   1.381  subsection {* Multiset orderings *}
   1.382 @@ -557,8 +501,7 @@
   1.383  (*Badly needed: a linear arithmetic procedure for multisets*)
   1.384  
   1.385  lemma diff_union_single_conv: "a :# J ==> I + J - {#a#} = I + (J - {#a#})"
   1.386 -  apply (simp add: multiset_eq_conv_count_eq)
   1.387 -  done
   1.388 +by (simp add: multiset_eq_conv_count_eq)
   1.389  
   1.390  text {* One direction. *}
   1.391  
   1.392 @@ -567,11 +510,8 @@
   1.393      \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
   1.394      (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)"
   1.395    apply (unfold mult_def mult1_def set_of_def)
   1.396 -  apply (erule converse_trancl_induct)
   1.397 -  apply clarify
   1.398 -   apply (rule_tac x = M0 in exI)
   1.399 -   apply simp
   1.400 -  apply clarify
   1.401 +  apply (erule converse_trancl_induct, clarify)
   1.402 +   apply (rule_tac x = M0 in exI, simp, clarify)
   1.403    apply (case_tac "a :# K")
   1.404     apply (rule_tac x = I in exI)
   1.405     apply (simp (no_asm))
   1.406 @@ -588,8 +528,7 @@
   1.407     apply (rule conjI)
   1.408      apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
   1.409     apply (rule conjI)
   1.410 -    apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
   1.411 -    apply simp
   1.412 +    apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
   1.413      apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
   1.414     apply (simp (no_asm_use) add: trans_def)
   1.415     apply blast
   1.416 @@ -599,38 +538,30 @@
   1.417    done
   1.418  
   1.419  lemma elem_imp_eq_diff_union: "a :# M ==> M = M - {#a#} + {#a#}"
   1.420 -  apply (simp add: multiset_eq_conv_count_eq)
   1.421 -  done
   1.422 +by (simp add: multiset_eq_conv_count_eq)
   1.423  
   1.424  lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}"
   1.425    apply (erule size_eq_Suc_imp_elem [THEN exE])
   1.426 -  apply (drule elem_imp_eq_diff_union)
   1.427 -  apply auto
   1.428 +  apply (drule elem_imp_eq_diff_union, auto)
   1.429    done
   1.430  
   1.431  lemma one_step_implies_mult_aux:
   1.432    "trans r ==>
   1.433      \<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r))
   1.434        --> (I + K, I + J) \<in> mult r"
   1.435 -  apply (induct_tac n)
   1.436 -   apply auto
   1.437 -  apply (frule size_eq_Suc_imp_eq_union)
   1.438 -  apply clarify
   1.439 -  apply (rename_tac "J'")
   1.440 -  apply simp
   1.441 -  apply (erule notE)
   1.442 -   apply auto
   1.443 +  apply (induct_tac n, auto)
   1.444 +  apply (frule size_eq_Suc_imp_eq_union, clarify)
   1.445 +  apply (rename_tac "J'", simp)
   1.446 +  apply (erule notE, auto)
   1.447    apply (case_tac "J' = {#}")
   1.448     apply (simp add: mult_def)
   1.449     apply (rule r_into_trancl)
   1.450 -   apply (simp add: mult1_def set_of_def)
   1.451 -   apply blast
   1.452 +   apply (simp add: mult1_def set_of_def, blast)
   1.453    txt {* Now we know @{term "J' \<noteq> {#}"}. *}
   1.454    apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
   1.455    apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
   1.456    apply (erule ssubst)
   1.457 -  apply (simp add: Ball_def)
   1.458 -  apply auto
   1.459 +  apply (simp add: Ball_def, auto)
   1.460    apply (subgoal_tac
   1.461      "((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #},
   1.462        (I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r")
   1.463 @@ -648,8 +579,7 @@
   1.464  theorem one_step_implies_mult:
   1.465    "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r
   1.466      ==> (I + K, I + J) \<in> mult r"
   1.467 -  apply (insert one_step_implies_mult_aux)
   1.468 -  apply blast
   1.469 +  apply (insert one_step_implies_mult_aux, blast)
   1.470    done
   1.471  
   1.472  
   1.473 @@ -677,18 +607,14 @@
   1.474    done
   1.475  
   1.476  theorem mult_less_not_refl: "\<not> M < (M::'a::order multiset)"
   1.477 -  apply (unfold less_multiset_def)
   1.478 -  apply auto
   1.479 -  apply (drule trans_base_order [THEN mult_implies_one_step])
   1.480 -  apply auto
   1.481 +  apply (unfold less_multiset_def, auto)
   1.482 +  apply (drule trans_base_order [THEN mult_implies_one_step], auto)
   1.483    apply (drule finite_set_of [THEN mult_irrefl_aux [rule_format (no_asm)]])
   1.484    apply (simp add: set_of_eq_empty_iff)
   1.485    done
   1.486  
   1.487  lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
   1.488 -  apply (insert mult_less_not_refl)
   1.489 -  apply fast
   1.490 -  done
   1.491 +by (insert mult_less_not_refl, fast)
   1.492  
   1.493  
   1.494  text {* Transitivity. *}
   1.495 @@ -703,20 +629,15 @@
   1.496  theorem mult_less_not_sym: "M < N ==> \<not> N < (M::'a::order multiset)"
   1.497    apply auto
   1.498    apply (rule mult_less_not_refl [THEN notE])
   1.499 -  apply (erule mult_less_trans)
   1.500 -  apply assumption
   1.501 +  apply (erule mult_less_trans, assumption)
   1.502    done
   1.503  
   1.504  theorem mult_less_asym:
   1.505      "M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P"
   1.506 -  apply (insert mult_less_not_sym)
   1.507 -  apply blast
   1.508 -  done
   1.509 +  by (insert mult_less_not_sym, blast)
   1.510  
   1.511  theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)"
   1.512 -  apply (unfold le_multiset_def)
   1.513 -  apply auto
   1.514 -  done
   1.515 +by (unfold le_multiset_def, auto)
   1.516  
   1.517  text {* Anti-symmetry. *}
   1.518  
   1.519 @@ -735,19 +656,15 @@
   1.520    done
   1.521  
   1.522  theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
   1.523 -  apply (unfold le_multiset_def)
   1.524 -  apply auto
   1.525 -  done
   1.526 +by (unfold le_multiset_def, auto)
   1.527  
   1.528  text {* Partial order. *}
   1.529  
   1.530  instance multiset :: (order) order
   1.531    apply intro_classes
   1.532       apply (rule mult_le_refl)
   1.533 -    apply (erule mult_le_trans)
   1.534 -    apply assumption
   1.535 -   apply (erule mult_le_antisym)
   1.536 -   apply assumption
   1.537 +    apply (erule mult_le_trans, assumption)
   1.538 +   apply (erule mult_le_antisym, assumption)
   1.539    apply (rule mult_less_le)
   1.540    done
   1.541  
   1.542 @@ -756,8 +673,7 @@
   1.543  
   1.544  theorem mult1_union:
   1.545      "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
   1.546 -  apply (unfold mult1_def)
   1.547 -  apply auto
   1.548 +  apply (unfold mult1_def, auto)
   1.549    apply (rule_tac x = a in exI)
   1.550    apply (rule_tac x = "C + M0" in exI)
   1.551    apply (simp add: union_assoc)
   1.552 @@ -794,19 +710,123 @@
   1.553     apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
   1.554      prefer 2
   1.555      apply (rule one_step_implies_mult)
   1.556 -      apply (simp only: trans_def)
   1.557 -      apply auto
   1.558 +      apply (simp only: trans_def, auto)
   1.559    done
   1.560  
   1.561  theorem union_upper1: "A <= A + (B::'a::order multiset)"
   1.562 -  apply (subgoal_tac "A + {#} <= A + B")
   1.563 -   prefer 2
   1.564 -   apply (rule union_le_mono)
   1.565 -    apply auto
   1.566 +proof -
   1.567 +  have "A + {#} <= A + B" by (blast intro: union_le_mono) 
   1.568 +  thus ?thesis by simp
   1.569 +qed
   1.570 +
   1.571 +theorem union_upper2: "B <= A + (B::'a::order multiset)"
   1.572 +by (subst union_commute, rule union_upper1)
   1.573 +
   1.574 +
   1.575 +subsection {* Link with lists *} 
   1.576 +
   1.577 +consts 
   1.578 +  multiset_of :: "'a list \<Rightarrow> 'a multiset"
   1.579 +primrec
   1.580 +  "multiset_of [] = {#}"
   1.581 +  "multiset_of (a # x) = multiset_of x + {# a #}"
   1.582 +
   1.583 +lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
   1.584 +  by (induct_tac x, auto) 
   1.585 +
   1.586 +lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
   1.587 +  by (induct_tac x, auto)
   1.588 +
   1.589 +lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
   1.590 + by (induct_tac x, auto) 
   1.591 +
   1.592 +lemma multset_of_append[simp]: 
   1.593 +  "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
   1.594 +  by (rule_tac x=ys in spec, induct_tac xs, auto simp: union_ac) 
   1.595 +
   1.596 +lemma surj_multiset_of: "surj multiset_of"
   1.597 +  apply (unfold surj_def, rule allI) 
   1.598 +  apply (rule_tac M=y in multiset_induct, auto) 
   1.599 +  apply (rule_tac x = "x # xa" in exI, auto) 
   1.600    done
   1.601  
   1.602 -theorem union_upper2: "B <= A + (B::'a::order multiset)"
   1.603 -  apply (subst union_commute, rule union_upper1)
   1.604 +lemma set_count_greater_0: "set x = {a. 0 < count (multiset_of x) a}"
   1.605 +  by (induct_tac x, auto)  
   1.606 +
   1.607 +lemma distinct_count_atmost_1: 
   1.608 +   "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
   1.609 +   apply ( induct_tac x, simp, rule iffI, simp_all)
   1.610 +   apply (rule conjI)  
   1.611 +   apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of) 
   1.612 +   apply (erule_tac x=a in allE, simp, clarify)
   1.613 +   apply (erule_tac x=aa in allE, simp) 
   1.614 +   done
   1.615 +
   1.616 +lemma set_eq_iff_multiset_of_eq_distinct: 
   1.617 +  "\<lbrakk>distinct x; distinct y\<rbrakk> 
   1.618 +   \<Longrightarrow> (set x = set y) = (multiset_of x = multiset_of y)"
   1.619 +  by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1) 
   1.620 +
   1.621 +lemma set_eq_iff_multiset_of_remdups_eq: 
   1.622 +   "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
   1.623 +  apply (rule iffI) 
   1.624 +  apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1]) 
   1.625 +  apply (drule distinct_remdups[THEN distinct_remdups 
   1.626 +                      [THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]]) 
   1.627 +  apply simp
   1.628    done
   1.629  
   1.630 +
   1.631 +subsection {* Pointwise ordering induced by count *}
   1.632 +
   1.633 +consts 
   1.634 +  mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool"
   1.635 +
   1.636 +syntax 
   1.637 +  "_mset_le" :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"   ("_ \<le># _"  [50,51] 50) 
   1.638 +translations 
   1.639 +  "x \<le># y" == "mset_le x y"
   1.640 +
   1.641 +defs 
   1.642 +  mset_le_def:   "xs \<le># ys  == (! a. count xs a \<le> count ys a)"
   1.643 +
   1.644 +lemma mset_le_refl[simp]: "xs \<le># xs"
   1.645 +  by (unfold mset_le_def, auto) 
   1.646 +
   1.647 +lemma mset_le_trans: "\<lbrakk> xs \<le># ys; ys \<le># zs \<rbrakk> \<Longrightarrow> xs \<le># zs"
   1.648 +  by (unfold mset_le_def, fast intro: order_trans) 
   1.649 +
   1.650 +lemma mset_le_antisym: "\<lbrakk> xs\<le># ys; ys \<le># xs\<rbrakk> \<Longrightarrow> xs = ys"
   1.651 +  apply (unfold mset_le_def) 
   1.652 +  apply (rule multiset_eq_conv_count_eq[THEN iffD2]) 
   1.653 +  apply (blast intro: order_antisym)
   1.654 +  done
   1.655 +
   1.656 +lemma mset_le_exists_conv: 
   1.657 +  "(xs \<le># ys) = (? zs. ys = xs + zs)"
   1.658 +  apply (unfold mset_le_def, rule iffI, rule_tac x = "ys - xs" in exI) 
   1.659 +  apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
   1.660 +  done
   1.661 +
   1.662 +lemma mset_le_mono_add_right_cancel[simp]: "(xs + zs \<le># ys + zs) = (xs \<le># ys)"
   1.663 +  by (unfold mset_le_def, auto) 
   1.664 +
   1.665 +lemma mset_le_mono_add_left_cancel[simp]: "(zs + xs \<le># zs + ys) = (xs \<le># ys)"
   1.666 +  by (unfold mset_le_def, auto) 
   1.667 +
   1.668 +lemma mset_le_mono_add: "\<lbrakk> xs \<le># ys; vs \<le># ws \<rbrakk> \<Longrightarrow> xs + vs \<le># ys + ws" 
   1.669 +  apply (unfold mset_le_def, auto) 
   1.670 +  apply (erule_tac x=a in allE)+
   1.671 +  apply auto
   1.672 +  done
   1.673 +
   1.674 +lemma mset_le_add_left[simp]: "xs \<le># xs + ys"
   1.675 +  by (unfold mset_le_def, auto) 
   1.676 +
   1.677 +lemma mset_le_add_right[simp]: "ys \<le># xs + ys"
   1.678 +  by (unfold mset_le_def, auto)
   1.679 +
   1.680 +lemma multiset_of_remdups_le: "multiset_of (remdups x) \<le># multiset_of x"
   1.681 +  by (induct_tac x, auto, rule mset_le_trans, auto)
   1.682 +
   1.683  end
     2.1 --- a/src/HOL/Library/Permutation.thy	Wed Jul 21 16:35:38 2004 +0200
     2.2 +++ b/src/HOL/Library/Permutation.thy	Thu Jul 22 10:33:26 2004 +0200
     2.3 @@ -28,7 +28,8 @@
     2.4  subsection {* Some examples of rule induction on permutations *}
     2.5  
     2.6  lemma xperm_empty_imp_aux: "xs <~~> ys ==> xs = [] --> ys = []"
     2.7 -    -- {* the form of the premise lets the induction bind @{term xs} and @{term ys} *}
     2.8 +    -- {*the form of the premise lets the induction bind @{term xs} 
     2.9 +         and @{term ys} *}
    2.10    apply (erule perm.induct)
    2.11       apply (simp_all (no_asm_simp))
    2.12    done
    2.13 @@ -69,10 +70,7 @@
    2.14    done
    2.15  
    2.16  lemma perm_append_single: "a # xs <~~> xs @ [a]"
    2.17 -  apply (rule perm.trans)
    2.18 -   prefer 2
    2.19 -   apply (rule perm_append_swap, simp)
    2.20 -  done
    2.21 +  by (rule perm.trans [OF _ perm_append_swap], simp)
    2.22  
    2.23  lemma perm_rev: "rev xs <~~> xs"
    2.24    apply (induct xs, simp_all)
    2.25 @@ -120,6 +118,10 @@
    2.26  lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
    2.27  by (induct l, auto)
    2.28  
    2.29 +lemma multiset_of_remove[simp]: 
    2.30 +  "multiset_of (remove a x) = multiset_of x - {#a#}"
    2.31 +  by (induct_tac x, auto simp: multiset_eq_conv_count_eq) 
    2.32 +
    2.33  
    2.34  text {* \medskip Congruence rule *}
    2.35  
    2.36 @@ -127,8 +129,7 @@
    2.37  by (erule perm.induct, auto)
    2.38  
    2.39  lemma remove_hd [simp]: "remove z (z # xs) = xs"
    2.40 -  apply auto
    2.41 -  done
    2.42 +  by auto
    2.43  
    2.44  lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
    2.45  by (drule_tac z = z in perm_remove_perm, auto)
    2.46 @@ -153,31 +154,11 @@
    2.47    apply (blast intro: perm_append_swap)
    2.48    done
    2.49  
    2.50 -(****************** Norbert Voelker 17 June 2004 **************) 
    2.51 -
    2.52 -consts 
    2.53 -  multiset_of :: "'a list \<Rightarrow> 'a multiset"
    2.54 -primrec
    2.55 -  "multiset_of [] = {#}"
    2.56 -  "multiset_of (a # x) = multiset_of x + {# a #}"
    2.57 -
    2.58 -lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
    2.59 -  by (induct_tac x, auto) 
    2.60 -
    2.61 -lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
    2.62 -  by (induct_tac x, auto)
    2.63 -
    2.64 -lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
    2.65 - by (induct_tac x, auto) 
    2.66 -
    2.67 -lemma multiset_of_remove[simp]: 
    2.68 -  "multiset_of (remove a x) = multiset_of x - {#a#}"
    2.69 -  by (induct_tac x, auto simp: multiset_eq_conv_count_eq) 
    2.70 -
    2.71 -lemma multiset_of_eq_perm:  "(multiset_of xs = multiset_of ys) = (xs <~~> ys) "
    2.72 +lemma multiset_of_eq_perm: "(multiset_of xs = multiset_of ys) = (xs <~~> ys) "
    2.73    apply (rule iffI) 
    2.74    apply (erule_tac [2] perm.induct, simp_all add: union_ac) 
    2.75 -  apply (erule rev_mp, rule_tac x=ys in spec, induct_tac xs, auto) 
    2.76 +  apply (erule rev_mp, rule_tac x=ys in spec) 
    2.77 +  apply (induct_tac xs, auto) 
    2.78    apply (erule_tac x = "remove a x" in allE, drule sym, simp) 
    2.79    apply (subgoal_tac "a \<in> set x") 
    2.80    apply (drule_tac z=a in perm.Cons) 
    2.81 @@ -185,15 +166,11 @@
    2.82    apply (drule_tac f=set_of in arg_cong, simp)
    2.83    done
    2.84  
    2.85 -lemma set_count_multiset_of: "set x = {a. 0 < count (multiset_of x) a}"
    2.86 -  by (induct_tac x, auto)  
    2.87 -
    2.88 -lemma distinct_count_multiset_of: 
    2.89 -   "distinct x \<Longrightarrow> count (multiset_of x) a = (if a \<in> set x then 1 else 0)"
    2.90 -  by (erule rev_mp, induct_tac x, auto) 
    2.91 -
    2.92 -lemma distinct_set_eq_iff_multiset_of_eq: 
    2.93 -  "\<lbrakk>distinct x; distinct y\<rbrakk> \<Longrightarrow> (set x = set y) = (multiset_of x = multiset_of y)"
    2.94 -  by (auto simp: multiset_eq_conv_count_eq distinct_count_multiset_of) 
    2.95 +lemma multiset_of_le_perm_append: 
    2.96 +  "(multiset_of xs \<le># multiset_of ys) = (\<exists> zs. xs @ zs <~~> ys)"; 
    2.97 +  apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv) 
    2.98 +  apply (insert surj_multiset_of, drule surjD)
    2.99 +  apply (blast intro: sym)+
   2.100 +  done
   2.101  
   2.102  end
     3.1 --- a/src/HOL/List.thy	Wed Jul 21 16:35:38 2004 +0200
     3.2 +++ b/src/HOL/List.thy	Thu Jul 22 10:33:26 2004 +0200
     3.3 @@ -1338,6 +1338,12 @@
     3.4  lemma distinct_remdups [iff]: "distinct (remdups xs)"
     3.5  by (induct xs) auto
     3.6  
     3.7 +lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
     3.8 +  by (induct_tac x, auto) 
     3.9 +
    3.10 +lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
    3.11 +  by (induct_tac x, auto)
    3.12 +
    3.13  lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
    3.14  by (induct xs) auto
    3.15