summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 17 Nov 2010 21:35:23 +0100 | |

changeset 40593 | 1e57b18d27b1 |

parent 40592 | f432973ce0f6 |

child 40595 | 448520778e38 |

code eqn for slice was missing; redefined splice with fun

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.thy Wed Nov 17 08:47:58 2010 -0800 +++ b/src/HOL/List.thy Wed Nov 17 21:35:23 2010 +0100 @@ -214,11 +214,10 @@ sublist :: "'a list => nat set => 'a list" where "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))" -primrec - splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where - "splice [] ys = ys" - | "splice (x # xs) ys = (if ys = [] then x # xs else x # hd ys # splice xs (tl ys))" - -- {*Warning: simpset does not contain the second eqn but a derived one. *} +fun splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where +"splice [] ys = ys" | +"splice xs [] = xs" | +"splice (x#xs) (y#ys) = x # y # splice xs ys" text{* \begin{figure}[htbp] @@ -3477,21 +3476,14 @@ subsubsection {* @{const splice} *} -lemma splice_Nil2 [simp, code]: - "splice xs [] = xs" +lemma splice_Nil2 [simp, code]: "splice xs [] = xs" by (cases xs) simp_all -lemma splice_Cons_Cons [simp, code]: - "splice (x#xs) (y#ys) = x # y # splice xs ys" -by simp - -declare splice.simps(2) [simp del, code del] +declare splice.simps(1,3)[code] +declare splice.simps(2)[simp del] lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys" -apply(induct xs arbitrary: ys) apply simp -apply(case_tac ys) - apply auto -done +by (induct xs ys rule: splice.induct) auto subsubsection {* Transpose *}