merged
authornipkow
Fri Feb 28 18:11:11 2014 +0100 (2014-02-28)
changeset 55809d27e7872dd10
parent 55806 519625ec22a0
parent 55808 488c3e8282c8
child 55810 63d63d854fae
child 55812 59fcd209cc0c
merged
     1.1 --- a/src/HOL/Library/DAList_Multiset.thy	Fri Feb 28 17:31:19 2014 +0100
     1.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Fri Feb 28 18:11:11 2014 +0100
     1.3 @@ -66,6 +66,18 @@
     1.4    "sorted_list_of_multiset = sorted_list_of_multiset"
     1.5    ..
     1.6  
     1.7 +lemma [code, code del]:
     1.8 +  "ord_multiset_inst.less_eq_multiset = ord_multiset_inst.less_eq_multiset"
     1.9 +  ..
    1.10 +
    1.11 +lemma [code, code del]:
    1.12 +  "ord_multiset_inst.less_multiset = ord_multiset_inst.less_multiset"
    1.13 +  ..
    1.14 +
    1.15 +lemma [code, code del]:
    1.16 +  "equal_multiset_inst.equal_multiset = equal_multiset_inst.equal_multiset"
    1.17 +  ..
    1.18 +
    1.19  
    1.20  text {* Raw operations on lists *}
    1.21  
    1.22 @@ -215,6 +227,10 @@
    1.23    "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
    1.24  by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
    1.25  
    1.26 +
    1.27 +lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le> m2 \<and> m2 \<le> m1"
    1.28 +by (metis equal_multiset_def eq_iff)
    1.29 +
    1.30  lemma mset_less_eq_Bag [code]:
    1.31    "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
    1.32      (is "?lhs \<longleftrightarrow> ?rhs")
     2.1 --- a/src/HOL/Library/Multiset.thy	Fri Feb 28 17:31:19 2014 +0100
     2.2 +++ b/src/HOL/Library/Multiset.thy	Fri Feb 28 18:11:11 2014 +0100
     2.3 @@ -358,6 +358,12 @@
     2.4  lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
     2.5    by (auto simp add: mset_less_def mset_le_def multiset_eq_iff)
     2.6  
     2.7 +lemma empty_le[simp]: "{#} \<le> A"
     2.8 +  unfolding mset_le_exists_conv by auto
     2.9 +
    2.10 +lemma le_empty[simp]: "(M \<le> {#}) = (M = {#})"
    2.11 +  unfolding mset_le_exists_conv by auto
    2.12 +
    2.13  lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
    2.14    by (auto simp: mset_le_def mset_less_def)
    2.15  
    2.16 @@ -561,6 +567,9 @@
    2.17  lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
    2.18    unfolding set_of_def[symmetric] by simp
    2.19  
    2.20 +lemma set_of_mono: "A \<le> B \<Longrightarrow> set_of A \<subseteq> set_of B"  
    2.21 +  by (metis mset_leD subsetI mem_set_of_iff)
    2.22 +
    2.23  subsubsection {* Size *}
    2.24  
    2.25  instantiation multiset :: (type) size
    2.26 @@ -2083,26 +2092,70 @@
    2.27    "mcard (multiset_of xs) = length xs"
    2.28    by (simp add: mcard_multiset_of)
    2.29  
    2.30 -lemma [code]:
    2.31 -  "A \<le> B \<longleftrightarrow> A #\<inter> B = A" 
    2.32 -  by (auto simp add: inf.order_iff)
    2.33 +fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where 
    2.34 +  "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
    2.35 +| "ms_lesseq_impl (Cons x xs) ys = (case List.extract (op = x) ys of 
    2.36 +     None \<Rightarrow> None
    2.37 +   | Some (ys1,_,ys2) \<Rightarrow> ms_lesseq_impl xs (ys1 @ ys2))"
    2.38 +
    2.39 +lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> multiset_of xs \<le> multiset_of ys) \<and>
    2.40 +  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> multiset_of xs < multiset_of ys) \<and>
    2.41 +  (ms_lesseq_impl xs ys = Some False \<longrightarrow> multiset_of xs = multiset_of ys)"
    2.42 +proof (induct xs arbitrary: ys)
    2.43 +  case (Nil ys)
    2.44 +  show ?case by (auto simp: mset_less_empty_nonempty)
    2.45 +next
    2.46 +  case (Cons x xs ys)
    2.47 +  show ?case
    2.48 +  proof (cases "List.extract (op = x) ys")
    2.49 +    case None
    2.50 +    hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
    2.51 +    {
    2.52 +      assume "multiset_of (x # xs) \<le> multiset_of ys"
    2.53 +      from set_of_mono[OF this] x have False by simp
    2.54 +    } note nle = this
    2.55 +    moreover
    2.56 +    {
    2.57 +      assume "multiset_of (x # xs) < multiset_of ys"
    2.58 +      hence "multiset_of (x # xs) \<le> multiset_of ys" by auto
    2.59 +      from nle[OF this] have False .
    2.60 +    }
    2.61 +    ultimately show ?thesis using None by auto
    2.62 +  next
    2.63 +    case (Some res)
    2.64 +    obtain ys1 y ys2 where res: "res = (ys1,y,ys2)" by (cases res, auto)
    2.65 +    note Some = Some[unfolded res]
    2.66 +    from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp
    2.67 +    hence id: "multiset_of ys = multiset_of (ys1 @ ys2) + {#x#}" 
    2.68 +      by (auto simp: ac_simps)
    2.69 +    show ?thesis unfolding ms_lesseq_impl.simps
    2.70 +      unfolding Some option.simps split
    2.71 +      unfolding id
    2.72 +      using Cons[of "ys1 @ ys2"]
    2.73 +      unfolding mset_le_def mset_less_def by auto
    2.74 +  qed
    2.75 +qed
    2.76 +
    2.77 +lemma [code]: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
    2.78 +  using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
    2.79 +
    2.80 +lemma [code]: "multiset_of xs < multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
    2.81 +  using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
    2.82  
    2.83  instantiation multiset :: (equal) equal
    2.84  begin
    2.85  
    2.86  definition
    2.87 -  [code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
    2.88 +  [code del]: "HOL.equal A (B :: 'a multiset) \<longleftrightarrow> A = B"
    2.89 +lemma [code]: "HOL.equal (multiset_of xs) (multiset_of ys) \<longleftrightarrow> ms_lesseq_impl xs ys = Some False"
    2.90 +  unfolding equal_multiset_def
    2.91 +  using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
    2.92  
    2.93  instance
    2.94 -  by default (simp add: equal_multiset_def eq_iff)
    2.95 -
    2.96 +  by default (simp add: equal_multiset_def)
    2.97  end
    2.98  
    2.99  lemma [code]:
   2.100 -  "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
   2.101 -  by auto
   2.102 -
   2.103 -lemma [code]:
   2.104    "msetsum (multiset_of xs) = listsum xs"
   2.105    by (induct xs) (simp_all add: add.commute)
   2.106  
     3.1 --- a/src/HOL/List.thy	Fri Feb 28 17:31:19 2014 +0100
     3.2 +++ b/src/HOL/List.thy	Fri Feb 28 18:11:11 2014 +0100
     3.3 @@ -182,6 +182,15 @@
     3.4  
     3.5  hide_const (open) find
     3.6  
     3.7 +definition
     3.8 +   "extract" :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> ('a list * 'a * 'a list) option"
     3.9 +where "extract P xs =
    3.10 +  (case dropWhile (Not o P) xs of
    3.11 +     [] \<Rightarrow> None |
    3.12 +     y#ys \<Rightarrow> Some(takeWhile (Not o P) xs, y, ys))"
    3.13 +
    3.14 +hide_const (open) "extract"
    3.15 +
    3.16  primrec those :: "'a option list \<Rightarrow> 'a list option"
    3.17  where
    3.18  "those [] = Some []" |
    3.19 @@ -287,6 +296,8 @@
    3.20  @{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\
    3.21  @{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\
    3.22  @{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\
    3.23 +@{lemma "List.extract (%i::int. i>0) [0,0] = None" by(simp add: extract_def)}\\
    3.24 +@{lemma "List.extract (%i::int. i>0) [0,1,0,2] = Some([0], 1, [0,2])" by(simp add: extract_def)}\\
    3.25  @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
    3.26  @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
    3.27  @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
    3.28 @@ -3648,6 +3659,34 @@
    3.29    by (induct xs) simp_all
    3.30  
    3.31  
    3.32 +subsubsection {* @{const List.extract} *}
    3.33 +
    3.34 +lemma extract_None_iff: "List.extract P xs = None \<longleftrightarrow> \<not> (\<exists> x\<in>set xs. P x)"
    3.35 +by(auto simp: extract_def dropWhile_eq_Cons_conv split: list.splits)
    3.36 +  (metis in_set_conv_decomp)
    3.37 +
    3.38 +lemma extract_SomeE:
    3.39 + "List.extract P xs = Some (ys, y, zs) \<Longrightarrow>
    3.40 +  xs = ys @ y # zs \<and> P y \<and> \<not> (\<exists> y \<in> set ys. P y)" 
    3.41 +by(auto simp: extract_def dropWhile_eq_Cons_conv split: list.splits)
    3.42 +
    3.43 +lemma extract_Some_iff:
    3.44 +  "List.extract P xs = Some (ys, y, zs) \<longleftrightarrow>
    3.45 +   xs = ys @ y # zs \<and> P y \<and> \<not> (\<exists> y \<in> set ys. P y)" 
    3.46 +by(auto simp: extract_def dropWhile_eq_Cons_conv dest: set_takeWhileD split: list.splits)
    3.47 +
    3.48 +lemma extract_Nil_code[code]: "List.extract P [] = None"
    3.49 +by(simp add: extract_def)
    3.50 +
    3.51 +lemma extract_Cons_code[code]:
    3.52 +  "List.extract P (x # xs) = (if P x then Some ([], x, xs) else
    3.53 +   (case List.extract P xs of
    3.54 +      None \<Rightarrow> None |
    3.55 +      Some (ys, y, zs) \<Rightarrow> Some (x#ys, y, zs)))"
    3.56 +by(auto simp add: extract_def split: list.splits)
    3.57 +  (metis comp_def dropWhile_eq_Nil_conv list.distinct(1))
    3.58 +
    3.59 +
    3.60  subsubsection {* @{const remove1} *}
    3.61  
    3.62  lemma remove1_append: