equal
deleted
inserted
replaced
2306 lemma dropWhile_cong [fundef_cong]: |
2306 lemma dropWhile_cong [fundef_cong]: |
2307 "[| l = k; !!x. x : set l ==> P x = Q x |] |
2307 "[| l = k; !!x. x : set l ==> P x = Q x |] |
2308 ==> dropWhile P l = dropWhile Q k" |
2308 ==> dropWhile P l = dropWhile Q k" |
2309 by (induct k arbitrary: l, simp_all) |
2309 by (induct k arbitrary: l, simp_all) |
2310 |
2310 |
|
2311 lemma takeWhile_idem [simp]: |
|
2312 "takeWhile P (takeWhile P xs) = takeWhile P xs" |
|
2313 by (induct xs) auto |
|
2314 |
|
2315 lemma dropWhile_idem [simp]: |
|
2316 "dropWhile P (dropWhile P xs) = dropWhile P xs" |
|
2317 by (induct xs) auto |
|
2318 |
2311 |
2319 |
2312 subsubsection {* @{const zip} *} |
2320 subsubsection {* @{const zip} *} |
2313 |
2321 |
2314 lemma zip_Nil [simp]: "zip [] ys = []" |
2322 lemma zip_Nil [simp]: "zip [] ys = []" |
2315 by (induct ys) auto |
2323 by (induct ys) auto |
2944 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)" |
2952 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)" |
2945 apply (induct n m arbitrary: i rule: diff_induct) |
2953 apply (induct n m arbitrary: i rule: diff_induct) |
2946 prefer 3 apply (subst map_Suc_upt[symmetric]) |
2954 prefer 3 apply (subst map_Suc_upt[symmetric]) |
2947 apply (auto simp add: less_diff_conv) |
2955 apply (auto simp add: less_diff_conv) |
2948 done |
2956 done |
|
2957 |
|
2958 lemma map_decr_upt: |
|
2959 "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]" |
|
2960 by (induct n) simp_all |
2949 |
2961 |
2950 lemma nth_take_lemma: |
2962 lemma nth_take_lemma: |
2951 "k <= length xs ==> k <= length ys ==> |
2963 "k <= length xs ==> k <= length ys ==> |
2952 (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys" |
2964 (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys" |
2953 apply (atomize, induct k arbitrary: xs ys) |
2965 apply (atomize, induct k arbitrary: xs ys) |
3700 apply clarsimp |
3712 apply clarsimp |
3701 apply (case_tac i) |
3713 apply (case_tac i) |
3702 apply simp |
3714 apply simp |
3703 apply clarsimp |
3715 apply clarsimp |
3704 done |
3716 done |
3705 |
|
3706 |
3717 |
3707 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}" |
3718 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}" |
3708 by (induct n) auto |
3719 by (induct n) auto |
3709 |
3720 |
3710 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}" |
3721 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}" |
3816 then have "m + n > 1" and "concat (replicate (m+n) zs) = xs @ ys" |
3827 then have "m + n > 1" and "concat (replicate (m+n) zs) = xs @ ys" |
3817 using `xs \<noteq> []` and `ys \<noteq> []` |
3828 using `xs \<noteq> []` and `ys \<noteq> []` |
3818 by (auto simp: replicate_add) |
3829 by (auto simp: replicate_add) |
3819 then show ?thesis by blast |
3830 then show ?thesis by blast |
3820 qed |
3831 qed |
|
3832 |
|
3833 lemma Cons_replicate_eq: |
|
3834 "x # xs = replicate n y \<longleftrightarrow> x = y \<and> n > 0 \<and> xs = replicate (n - 1) x" |
|
3835 by (induct n) auto |
|
3836 |
|
3837 lemma replicate_length_same: |
|
3838 "(\<forall>y\<in>set xs. y = x) \<Longrightarrow> replicate (length xs) x = xs" |
|
3839 by (induct xs) simp_all |
|
3840 |
|
3841 lemma foldr_replicate [simp]: |
|
3842 "foldr f (replicate n x) = f x ^^ n" |
|
3843 by (induct n) (simp_all) |
|
3844 |
|
3845 lemma fold_replicate [simp]: |
|
3846 "fold f (replicate n x) = f x ^^ n" |
|
3847 by (subst foldr_fold [symmetric]) simp_all |
3821 |
3848 |
3822 |
3849 |
3823 subsubsection {* @{const enumerate} *} |
3850 subsubsection {* @{const enumerate} *} |
3824 |
3851 |
3825 lemma enumerate_simps [simp, code]: |
3852 lemma enumerate_simps [simp, code]: |