src/HOL/List.thy
 changeset 40593 1e57b18d27b1 parent 40365 a1456f2e1c9d child 40608 6c28ab8b8166
equal inserted replaced
40592:f432973ce0f6 40593:1e57b18d27b1
   212
   212
   213 definition
   213 definition
   214   sublist :: "'a list => nat set => 'a list" where
   214   sublist :: "'a list => nat set => 'a list" where
   215   "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
   215   "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
   216
   216
   217 primrec
   217 fun splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   218   splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   218 "splice [] ys = ys" |
   219     "splice [] ys = ys"
   219 "splice xs [] = xs" |
   220   | "splice (x # xs) ys = (if ys = [] then x # xs else x # hd ys # splice xs (tl ys))"
   220 "splice (x#xs) (y#ys) = x # y # splice xs ys"
   221     -- {*Warning: simpset does not contain the second eqn but a derived one. *}

   222
   221
   223 text{*
   222 text{*
   224 \begin{figure}[htbp]
   223 \begin{figure}[htbp]
   225 \fbox{
   224 \fbox{
   226 \begin{tabular}{l}
   225 \begin{tabular}{l}
  3475 qed
  3474 qed
  3476
  3475
  3477
  3476
  3478 subsubsection {* @{const splice} *}
  3477 subsubsection {* @{const splice} *}
  3479
  3478
  3480 lemma splice_Nil2 [simp, code]:
  3479 lemma splice_Nil2 [simp, code]: "splice xs [] = xs"
  3481  "splice xs [] = xs"

  3482 by (cases xs) simp_all
  3480 by (cases xs) simp_all
  3483
  3481
  3484 lemma splice_Cons_Cons [simp, code]:
  3482 declare splice.simps(1,3)[code]
  3485  "splice (x#xs) (y#ys) = x # y # splice xs ys"
  3483 declare splice.simps(2)[simp del]
  3486 by simp

  3487

  3488 declare splice.simps(2) [simp del, code del]

  3489
  3484
  3490 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
  3485 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
  3491 apply(induct xs arbitrary: ys) apply simp
  3486 by (induct xs ys rule: splice.induct) auto
  3492 apply(case_tac ys)

  3493  apply auto

  3494 done

  3495
  3487
  3496
  3488
  3497 subsubsection {* Transpose *}
  3489 subsubsection {* Transpose *}
  3498
  3490
  3499 function transpose where
  3491 function transpose where