src/HOL/Library/Multiset.thy
changeset 55808 488c3e8282c8
parent 55565 f663fc1e653b
child 55811 aa1acc25126b
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri Feb 28 18:09:37 2014 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Feb 28 18:11:02 2014 +0100
     1.3 @@ -358,6 +358,12 @@
     1.4  lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
     1.5    by (auto simp add: mset_less_def mset_le_def multiset_eq_iff)
     1.6  
     1.7 +lemma empty_le[simp]: "{#} \<le> A"
     1.8 +  unfolding mset_le_exists_conv by auto
     1.9 +
    1.10 +lemma le_empty[simp]: "(M \<le> {#}) = (M = {#})"
    1.11 +  unfolding mset_le_exists_conv by auto
    1.12 +
    1.13  lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
    1.14    by (auto simp: mset_le_def mset_less_def)
    1.15  
    1.16 @@ -561,6 +567,9 @@
    1.17  lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
    1.18    unfolding set_of_def[symmetric] by simp
    1.19  
    1.20 +lemma set_of_mono: "A \<le> B \<Longrightarrow> set_of A \<subseteq> set_of B"  
    1.21 +  by (metis mset_leD subsetI mem_set_of_iff)
    1.22 +
    1.23  subsubsection {* Size *}
    1.24  
    1.25  instantiation multiset :: (type) size
    1.26 @@ -2083,26 +2092,70 @@
    1.27    "mcard (multiset_of xs) = length xs"
    1.28    by (simp add: mcard_multiset_of)
    1.29  
    1.30 -lemma [code]:
    1.31 -  "A \<le> B \<longleftrightarrow> A #\<inter> B = A" 
    1.32 -  by (auto simp add: inf.order_iff)
    1.33 +fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where 
    1.34 +  "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
    1.35 +| "ms_lesseq_impl (Cons x xs) ys = (case List.extract (op = x) ys of 
    1.36 +     None \<Rightarrow> None
    1.37 +   | Some (ys1,_,ys2) \<Rightarrow> ms_lesseq_impl xs (ys1 @ ys2))"
    1.38 +
    1.39 +lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> multiset_of xs \<le> multiset_of ys) \<and>
    1.40 +  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> multiset_of xs < multiset_of ys) \<and>
    1.41 +  (ms_lesseq_impl xs ys = Some False \<longrightarrow> multiset_of xs = multiset_of ys)"
    1.42 +proof (induct xs arbitrary: ys)
    1.43 +  case (Nil ys)
    1.44 +  show ?case by (auto simp: mset_less_empty_nonempty)
    1.45 +next
    1.46 +  case (Cons x xs ys)
    1.47 +  show ?case
    1.48 +  proof (cases "List.extract (op = x) ys")
    1.49 +    case None
    1.50 +    hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
    1.51 +    {
    1.52 +      assume "multiset_of (x # xs) \<le> multiset_of ys"
    1.53 +      from set_of_mono[OF this] x have False by simp
    1.54 +    } note nle = this
    1.55 +    moreover
    1.56 +    {
    1.57 +      assume "multiset_of (x # xs) < multiset_of ys"
    1.58 +      hence "multiset_of (x # xs) \<le> multiset_of ys" by auto
    1.59 +      from nle[OF this] have False .
    1.60 +    }
    1.61 +    ultimately show ?thesis using None by auto
    1.62 +  next
    1.63 +    case (Some res)
    1.64 +    obtain ys1 y ys2 where res: "res = (ys1,y,ys2)" by (cases res, auto)
    1.65 +    note Some = Some[unfolded res]
    1.66 +    from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp
    1.67 +    hence id: "multiset_of ys = multiset_of (ys1 @ ys2) + {#x#}" 
    1.68 +      by (auto simp: ac_simps)
    1.69 +    show ?thesis unfolding ms_lesseq_impl.simps
    1.70 +      unfolding Some option.simps split
    1.71 +      unfolding id
    1.72 +      using Cons[of "ys1 @ ys2"]
    1.73 +      unfolding mset_le_def mset_less_def by auto
    1.74 +  qed
    1.75 +qed
    1.76 +
    1.77 +lemma [code]: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
    1.78 +  using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
    1.79 +
    1.80 +lemma [code]: "multiset_of xs < multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
    1.81 +  using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
    1.82  
    1.83  instantiation multiset :: (equal) equal
    1.84  begin
    1.85  
    1.86  definition
    1.87 -  [code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
    1.88 +  [code del]: "HOL.equal A (B :: 'a multiset) \<longleftrightarrow> A = B"
    1.89 +lemma [code]: "HOL.equal (multiset_of xs) (multiset_of ys) \<longleftrightarrow> ms_lesseq_impl xs ys = Some False"
    1.90 +  unfolding equal_multiset_def
    1.91 +  using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
    1.92  
    1.93  instance
    1.94 -  by default (simp add: equal_multiset_def eq_iff)
    1.95 -
    1.96 +  by default (simp add: equal_multiset_def)
    1.97  end
    1.98  
    1.99  lemma [code]:
   1.100 -  "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
   1.101 -  by auto
   1.102 -
   1.103 -lemma [code]:
   1.104    "msetsum (multiset_of xs) = listsum xs"
   1.105    by (induct xs) (simp_all add: add.commute)
   1.106