1.1 --- a/src/HOL/List.thy Mon Mar 26 19:18:03 2012 +0200
1.2 +++ b/src/HOL/List.thy Mon Mar 26 20:09:52 2012 +0200
1.3 @@ -173,6 +173,12 @@
1.4 hide_const (open) insert
1.5 hide_fact (open) insert_def
1.6
1.7 +primrec find :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option" where
1.8 + "find _ [] = None"
1.9 +| "find P (x#xs) = (if P x then Some x else find P xs)"
1.10 +
1.11 +hide_const (open) find
1.12 +
1.13 primrec
1.14 remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
1.15 "remove1 x [] = []"
1.16 @@ -260,6 +266,8 @@
1.17 @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
1.18 @{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\
1.19 @{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\
1.20 +@{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\
1.21 +@{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\
1.22 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
1.23 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
1.24 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
1.25 @@ -908,8 +916,9 @@
1.26 by (induct rule:list_induct2, simp_all)
1.27
1.28 enriched_type map: map
1.29 - by (simp_all add: fun_eq_iff id_def)
1.30 -
1.31 +by (simp_all add: id_def)
1.32 +
1.33 +declare map.id[simp]
1.34
1.35 subsubsection {* @{text rev} *}
1.36
1.37 @@ -3074,6 +3083,10 @@
1.38 by (induct xs' ys' rule: list_induct2) (auto elim: in_set_zipE)
1.39 qed
1.40
1.41 +lemma set_take_disj_set_drop_if_distinct:
1.42 + "distinct vs \<Longrightarrow> i \<le> j \<Longrightarrow> set (take i vs) \<inter> set (drop j vs) = {}"
1.43 +by (auto simp: in_set_conv_nth distinct_conv_nth)
1.44 +
1.45 (* The next two lemmas help Sledgehammer. *)
1.46
1.47 lemma distinct_singleton: "distinct [x]" by simp
1.48 @@ -3273,7 +3286,40 @@
1.49 by (simp add: List.insert_def)
1.50
1.51
1.52 -subsubsection {* @{text remove1} *}
1.53 +subsubsection {* @{const List.find} *}
1.54 +
1.55 +lemma find_None_iff: "List.find P xs = None \<longleftrightarrow> \<not> (\<exists>x. x \<in> set xs \<and> P x)"
1.56 +proof (induction xs)
1.57 + case Nil thus ?case by simp
1.58 +next
1.59 + case (Cons x xs) thus ?case by (fastforce split: if_splits)
1.60 +qed
1.61 +
1.62 +lemma find_Some_iff:
1.63 + "List.find P xs = Some x \<longleftrightarrow>
1.64 + (\<exists>i<length xs. P (xs!i) \<and> x = xs!i \<and> (\<forall>j<i. \<not> P (xs!j)))"
1.65 +proof (induction xs)
1.66 + case Nil thus ?case by simp
1.67 +next
1.68 + case (Cons x xs) thus ?case
1.69 + by(auto simp: nth_Cons' split: if_splits)
1.70 + (metis One_nat_def diff_Suc_1 less_Suc_eq_0_disj)
1.71 +qed
1.72 +
1.73 +lemma find_cong[fundef_cong]:
1.74 + assumes "xs = ys" and "\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x"
1.75 + shows "List.find P xs = List.find Q ys"
1.76 +proof (cases "List.find P xs")
1.77 + case None thus ?thesis by (metis find_None_iff assms)
1.78 +next
1.79 + case (Some x)
1.80 + hence "List.find Q ys = Some x" using assms
1.81 + by (auto simp add: find_Some_iff)
1.82 + thus ?thesis using Some by auto
1.83 +qed
1.84 +
1.85 +
1.86 +subsubsection {* @{const remove1} *}
1.87
1.88 lemma remove1_append:
1.89 "remove1 x (xs @ ys) =
1.90 @@ -5665,6 +5711,10 @@
1.91 "List.coset [] <= set [] \<longleftrightarrow> False"
1.92 by auto
1.93
1.94 +text{* Optimising a frequent case: *}
1.95 +lemma [code_unfold]: "set xs \<subseteq> set ys \<longleftrightarrow> list_all (\<lambda>x. x \<in> set ys) xs"
1.96 +by (auto simp: list_all_iff)
1.97 +
1.98 lemma setsum_code [code]:
1.99 "setsum f (set xs) = listsum (map f (remdups xs))"
1.100 by (simp add: listsum_distinct_conv_setsum_set)