src/HOL/List.thy
changeset 40593 1e57b18d27b1
parent 40365 a1456f2e1c9d
child 40608 6c28ab8b8166
equal deleted 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