equal
deleted
inserted
replaced
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 