src/HOL/List.thy
changeset 51173 3cbb4e95a565
parent 51170 b3cdcba073d5
child 51272 9c8d63b4b6be
     1.1 --- a/src/HOL/List.thy	Sun Feb 17 20:45:49 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Sun Feb 17 21:29:30 2013 +0100
     1.3 @@ -196,6 +196,9 @@
     1.4  abbreviation length :: "'a list \<Rightarrow> nat" where
     1.5  "length \<equiv> size"
     1.6  
     1.7 +definition enumerate :: "nat \<Rightarrow> 'a list \<Rightarrow> (nat \<times> 'a) list" where
     1.8 +enumerate_eq_zip: "enumerate n xs = zip [n..<n + length xs] xs"
     1.9 +
    1.10  primrec rotate1 :: "'a list \<Rightarrow> 'a list" where
    1.11  "rotate1 [] = []" |
    1.12  "rotate1 (x # xs) = xs @ [x]"
    1.13 @@ -245,6 +248,7 @@
    1.14  @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
    1.15  @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
    1.16  @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
    1.17 +@{lemma "enumerate 3 [a,b,c] = [(3,a),(4,b),(5,c)]" by normalization}\\
    1.18  @{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by simp}\\
    1.19  @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
    1.20  @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
    1.21 @@ -2479,6 +2483,20 @@
    1.22    "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
    1.23    by (auto simp add: zip_map_fst_snd)
    1.24  
    1.25 +lemma in_set_zip:
    1.26 +  "p \<in> set (zip xs ys) \<longleftrightarrow> (\<exists>n. xs ! n = fst p \<and> ys ! n = snd p
    1.27 +    \<and> n < length xs \<and> n < length ys)"
    1.28 +  by (cases p) (auto simp add: set_zip)
    1.29 +
    1.30 +lemma pair_list_eqI:
    1.31 +  assumes "map fst xs = map fst ys" and "map snd xs = map snd ys"
    1.32 +  shows "xs = ys"
    1.33 +proof -
    1.34 +  from assms(1) have "length xs = length ys" by (rule map_eq_imp_length_eq)
    1.35 +  from this assms show ?thesis
    1.36 +    by (induct xs ys rule: list_induct2) (simp_all add: prod_eqI)
    1.37 +qed
    1.38 +
    1.39  
    1.40  subsubsection {* @{const list_all2} *}
    1.41  
    1.42 @@ -3880,6 +3898,57 @@
    1.43  qed
    1.44  
    1.45  
    1.46 +subsubsection {* @{const enumerate} *}
    1.47 +
    1.48 +lemma enumerate_simps [simp, code]:
    1.49 +  "enumerate n [] = []"
    1.50 +  "enumerate n (x # xs) = (n, x) # enumerate (Suc n) xs"
    1.51 +  apply (auto simp add: enumerate_eq_zip not_le)
    1.52 +  apply (cases "n < n + length xs")
    1.53 +  apply (auto simp add: upt_conv_Cons)
    1.54 +  done
    1.55 +
    1.56 +lemma length_enumerate [simp]:
    1.57 +  "length (enumerate n xs) = length xs"
    1.58 +  by (simp add: enumerate_eq_zip)
    1.59 +
    1.60 +lemma map_fst_enumerate [simp]:
    1.61 +  "map fst (enumerate n xs) = [n..<n + length xs]"
    1.62 +  by (simp add: enumerate_eq_zip)
    1.63 +
    1.64 +lemma map_snd_enumerate [simp]:
    1.65 +  "map snd (enumerate n xs) = xs"
    1.66 +  by (simp add: enumerate_eq_zip)
    1.67 +  
    1.68 +lemma in_set_enumerate_eq:
    1.69 +  "p \<in> set (enumerate n xs) \<longleftrightarrow> n \<le> fst p \<and> fst p < length xs + n \<and> nth xs (fst p - n) = snd p"
    1.70 +proof -
    1.71 +  { fix m
    1.72 +    assume "n \<le> m"
    1.73 +    moreover assume "m < length xs + n"
    1.74 +    ultimately have "[n..<n + length xs] ! (m - n) = m \<and>
    1.75 +      xs ! (m - n) = xs ! (m - n) \<and> m - n < length xs" by auto
    1.76 +    then have "\<exists>q. [n..<n + length xs] ! q = m \<and>
    1.77 +        xs ! q = xs ! (m - n) \<and> q < length xs" ..
    1.78 +  } then show ?thesis by (cases p) (auto simp add: enumerate_eq_zip in_set_zip)
    1.79 +qed
    1.80 +
    1.81 +lemma nth_enumerate_eq:
    1.82 +  assumes "m < length xs"
    1.83 +  shows "enumerate n xs ! m = (n + m, xs ! m)"
    1.84 +  using assms by (simp add: enumerate_eq_zip)
    1.85 +
    1.86 +lemma enumerate_replicate_eq:
    1.87 +  "enumerate n (replicate m a) = map (\<lambda>q. (q, a)) [n..<n + m]"
    1.88 +  by (rule pair_list_eqI)
    1.89 +    (simp_all add: enumerate_eq_zip comp_def map_replicate_const)
    1.90 +
    1.91 +lemma enumerate_Suc_eq:
    1.92 +  "enumerate (Suc n) xs = map (apfst Suc) (enumerate n xs)"
    1.93 +  by (rule pair_list_eqI)
    1.94 +    (simp_all add: not_le, simp del: map_map [simp del] add: map_Suc_upt map_map [symmetric])
    1.95 +
    1.96 +
    1.97  subsubsection {* @{const rotate1} and @{const rotate} *}
    1.98  
    1.99  lemma rotate0[simp]: "rotate 0 = id"