more lemmas
authorhaftmann
Mon May 24 13:48:57 2010 +0200 (2010-05-24)
changeset 371071535aa1c943a
parent 37106 d56e0b30ce5a
child 37108 00f13d3ad474
more lemmas
src/HOL/Library/Mapping.thy
src/HOL/Library/Multiset.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Library/Mapping.thy	Mon May 24 13:48:56 2010 +0200
     1.2 +++ b/src/HOL/Library/Mapping.thy	Mon May 24 13:48:57 2010 +0200
     1.3 @@ -6,30 +6,6 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -lemma remove1_idem: (*FIXME move to List.thy*)
     1.8 -  assumes "x \<notin> set xs"
     1.9 -  shows "remove1 x xs = xs"
    1.10 -  using assms by (induct xs) simp_all
    1.11 -
    1.12 -lemma remove1_insort [simp]:
    1.13 -  "remove1 x (insort x xs) = xs"
    1.14 -  by (induct xs) simp_all
    1.15 -
    1.16 -lemma sorted_list_of_set_remove:
    1.17 -  assumes "finite A"
    1.18 -  shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
    1.19 -proof (cases "x \<in> A")
    1.20 -  case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
    1.21 -  with False show ?thesis by (simp add: remove1_idem)
    1.22 -next
    1.23 -  case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
    1.24 -  with assms show ?thesis by simp
    1.25 -qed
    1.26 -
    1.27 -lemma sorted_list_of_set_range [simp]:
    1.28 -  "sorted_list_of_set {m..<n} = [m..<n]"
    1.29 -  by (rule sorted_distinct_set_unique) simp_all
    1.30 -
    1.31  subsection {* Type definition and primitive operations *}
    1.32  
    1.33  datatype ('a, 'b) mapping = Mapping "'a \<rightharpoonup> 'b"
     2.1 --- a/src/HOL/Library/Multiset.thy	Mon May 24 13:48:56 2010 +0200
     2.2 +++ b/src/HOL/Library/Multiset.thy	Mon May 24 13:48:57 2010 +0200
     2.3 @@ -708,6 +708,14 @@
     2.4    "multiset_of [] = {#}" |
     2.5    "multiset_of (a # x) = multiset_of x + {# a #}"
     2.6  
     2.7 +lemma in_multiset_in_set:
     2.8 +  "x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs"
     2.9 +  by (induct xs) simp_all
    2.10 +
    2.11 +lemma count_multiset_of:
    2.12 +  "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
    2.13 +  by (induct xs) simp_all
    2.14 +
    2.15  lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
    2.16  by (induct x) auto
    2.17  
    2.18 @@ -783,45 +791,29 @@
    2.19  by (induct xs) (auto simp add: multiset_ext_iff)
    2.20  
    2.21  lemma multiset_of_eq_length:
    2.22 -assumes "multiset_of xs = multiset_of ys"
    2.23 -shows "length xs = length ys"
    2.24 -using assms
    2.25 -proof (induct arbitrary: ys rule: length_induct)
    2.26 -  case (1 xs ys)
    2.27 -  show ?case
    2.28 -  proof (cases xs)
    2.29 -    case Nil with "1.prems" show ?thesis by simp
    2.30 -  next
    2.31 -    case (Cons x xs')
    2.32 -    note xCons = Cons
    2.33 -    show ?thesis
    2.34 -    proof (cases ys)
    2.35 -      case Nil
    2.36 -      with "1.prems" Cons show ?thesis by simp
    2.37 -    next
    2.38 -      case (Cons y ys')
    2.39 -      have x_in_ys: "x = y \<or> x \<in> set ys'"
    2.40 -      proof (cases "x = y")
    2.41 -        case True then show ?thesis ..
    2.42 -      next
    2.43 -        case False
    2.44 -        from "1.prems" [symmetric] xCons Cons have "x :# multiset_of ys' + {#y#}" by simp
    2.45 -        with False show ?thesis by (simp add: mem_set_multiset_eq)
    2.46 -      qed
    2.47 -      from "1.hyps" have IH: "length xs' < length xs \<longrightarrow>
    2.48 -        (\<forall>x. multiset_of xs' = multiset_of x \<longrightarrow> length xs' = length x)" by blast
    2.49 -      from "1.prems" x_in_ys Cons xCons have "multiset_of xs' = multiset_of (remove1 x (y#ys'))"
    2.50 -        apply -
    2.51 -        apply (simp add: multiset_of_remove1, simp only: add_eq_conv_diff)
    2.52 -        apply fastsimp
    2.53 -        done
    2.54 -      with IH xCons have IH': "length xs' = length (remove1 x (y#ys'))" by fastsimp
    2.55 -      from x_in_ys have "x \<noteq> y \<Longrightarrow> length ys' > 0" by auto
    2.56 -      with Cons xCons x_in_ys IH' show ?thesis by (auto simp add: length_remove1)
    2.57 -    qed
    2.58 -  qed
    2.59 +  assumes "multiset_of xs = multiset_of ys"
    2.60 +  shows "length xs = length ys"
    2.61 +using assms proof (induct xs arbitrary: ys)
    2.62 +  case Nil then show ?case by simp
    2.63 +next
    2.64 +  case (Cons x xs)
    2.65 +  then have "x \<in># multiset_of ys" by (simp add: union_single_eq_member)
    2.66 +  then have "x \<in> set ys" by (simp add: in_multiset_in_set)
    2.67 +  from Cons.prems [symmetric] have "multiset_of xs = multiset_of (remove1 x ys)"
    2.68 +    by simp
    2.69 +  with Cons.hyps have "length xs = length (remove1 x ys)" .
    2.70 +  with `x \<in> set ys` show ?case
    2.71 +    by (auto simp add: length_remove1 dest: length_pos_if_in_set)
    2.72  qed
    2.73  
    2.74 +lemma (in linorder) multiset_of_insort [simp]:
    2.75 +  "multiset_of (insort x xs) = {#x#} + multiset_of xs"
    2.76 +  by (induct xs) (simp_all add: ac_simps)
    2.77 +
    2.78 +lemma (in linorder) multiset_of_sort [simp]:
    2.79 +  "multiset_of (sort xs) = multiset_of xs"
    2.80 +  by (induct xs) (simp_all add: ac_simps)
    2.81 +
    2.82  text {*
    2.83    This lemma shows which properties suffice to show that a function
    2.84    @{text "f"} with @{text "f xs = ys"} behaves like sort.
     3.1 --- a/src/HOL/List.thy	Mon May 24 13:48:56 2010 +0200
     3.2 +++ b/src/HOL/List.thy	Mon May 24 13:48:57 2010 +0200
     3.3 @@ -2970,6 +2970,21 @@
     3.4    "List.insert x (remdups xs) = remdups (List.insert x xs)"
     3.5    by (simp add: List.insert_def)
     3.6  
     3.7 +lemma distinct_induct [consumes 1, case_names Nil insert]:
     3.8 +  assumes "distinct xs"
     3.9 +  assumes "P []"
    3.10 +  assumes insert: "\<And>x xs. distinct xs \<Longrightarrow> x \<notin> set xs
    3.11 +    \<Longrightarrow> P xs \<Longrightarrow> P (List.insert x xs)"
    3.12 +  shows "P xs"
    3.13 +using `distinct xs` proof (induct xs)
    3.14 +  case Nil from `P []` show ?case .
    3.15 +next
    3.16 +  case (Cons x xs)
    3.17 +  then have "distinct xs" and "x \<notin> set xs" and "P xs" by simp_all
    3.18 +  with insert have "P (List.insert x xs)" .
    3.19 +  with `x \<notin> set xs` show ?case by simp
    3.20 +qed
    3.21 +
    3.22  
    3.23  subsubsection {* @{text remove1} *}
    3.24  
    3.25 @@ -3023,6 +3038,11 @@
    3.26    "distinct xs \<Longrightarrow> remove1 x (remdups xs) = remdups (remove1 x xs)"
    3.27    by (induct xs) simp_all
    3.28  
    3.29 +lemma remove1_idem:
    3.30 +  assumes "x \<notin> set xs"
    3.31 +  shows "remove1 x xs = xs"
    3.32 +  using assms by (induct xs) simp_all
    3.33 +
    3.34  
    3.35  subsubsection {* @{text removeAll} *}
    3.36  
    3.37 @@ -3801,6 +3821,34 @@
    3.38    shows "sorted (insort_insert x xs)"
    3.39    using assms by (simp add: insort_insert_def sorted_insort)
    3.40  
    3.41 +lemma filter_insort_key_triv:
    3.42 +  "\<not> P x \<Longrightarrow> filter P (insort_key f x xs) = filter P xs"
    3.43 +  by (induct xs) simp_all
    3.44 +
    3.45 +lemma filter_insort_key:
    3.46 +  "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
    3.47 +  using assms by (induct xs)
    3.48 +    (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
    3.49 +
    3.50 +lemma filter_sort_key:
    3.51 +  "filter P (sort_key f xs) = sort_key f (filter P xs)"
    3.52 +  by (induct xs) (simp_all add: filter_insort_key_triv filter_insort_key)
    3.53 +
    3.54 +lemma sorted_same [simp]:
    3.55 +  "sorted [x\<leftarrow>xs. x = f xs]"
    3.56 +proof (induct xs arbitrary: f)
    3.57 +  case Nil then show ?case by simp
    3.58 +next
    3.59 +  case (Cons x xs)
    3.60 +  then have "sorted [y\<leftarrow>xs . y = (\<lambda>xs. x) xs]" .
    3.61 +  moreover from Cons have "sorted [y\<leftarrow>xs . y = (f \<circ> Cons x) xs]" .
    3.62 +  ultimately show ?case by (simp_all add: sorted_Cons)
    3.63 +qed
    3.64 +
    3.65 +lemma remove1_insort [simp]:
    3.66 +  "remove1 x (insort x xs) = xs"
    3.67 +  by (induct xs) simp_all
    3.68 +
    3.69  end
    3.70  
    3.71  lemma sorted_upt[simp]: "sorted[i..<j]"
    3.72 @@ -3999,8 +4047,24 @@
    3.73    show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
    3.74  qed
    3.75  
    3.76 +lemma sorted_list_of_set_remove:
    3.77 +  assumes "finite A"
    3.78 +  shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
    3.79 +proof (cases "x \<in> A")
    3.80 +  case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
    3.81 +  with False show ?thesis by (simp add: remove1_idem)
    3.82 +next
    3.83 +  case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
    3.84 +  with assms show ?thesis by simp
    3.85 +qed
    3.86 +
    3.87  end
    3.88  
    3.89 +lemma sorted_list_of_set_range [simp]:
    3.90 +  "sorted_list_of_set {m..<n} = [m..<n]"
    3.91 +  by (rule sorted_distinct_set_unique) simp_all
    3.92 +
    3.93 +
    3.94  
    3.95  subsubsection {* @{text lists}: the list-forming operator over sets *}
    3.96