1.1 --- a/src/HOL/List.thy	Sat Mar 24 20:24:16 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Mon Mar 26 18:54:41 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)