author | noschinl |

Mon May 09 16:11:20 2011 +0200 (2011-05-09) | |

changeset 42714 | fcba668b0839 |

parent 42713 | 276c8cbeb5d2 |

child 42715 | fe8ee8099b47 |

add a lemma about commutative append to List.thy

1.1 --- a/src/HOL/List.thy Mon May 09 12:26:25 2011 +0200 1.2 +++ b/src/HOL/List.thy Mon May 09 16:11:20 2011 +0200 1.3 @@ -3326,6 +3326,71 @@ 1.4 "replicate (length (filter (\<lambda>y. x = y) xs)) x = filter (\<lambda>y. x = y) xs" 1.5 by (induct xs) auto 1.6 1.7 +lemma comm_append_are_replicate: 1.8 + fixes xs ys :: "'a list" 1.9 + assumes "xs \<noteq> []" "ys \<noteq> []" 1.10 + assumes "xs @ ys = ys @ xs" 1.11 + shows "\<exists>m n zs. concat (replicate m zs) = xs \<and> concat (replicate n zs) = ys" 1.12 + using assms 1.13 +proof (induct "length (xs @ ys)" arbitrary: xs ys rule: less_induct) 1.14 + case less 1.15 + 1.16 + def xs' \<equiv> "if (length xs \<le> length ys) then xs else ys" 1.17 + and ys' \<equiv> "if (length xs \<le> length ys) then ys else xs" 1.18 + then have 1.19 + prems': "length xs' \<le> length ys'" 1.20 + "xs' @ ys' = ys' @ xs'" 1.21 + and "xs' \<noteq> []" 1.22 + and len: "length (xs @ ys) = length (xs' @ ys')" 1.23 + using less by (auto intro: less.hyps) 1.24 + 1.25 + from prems' 1.26 + obtain ws where "ys' = xs' @ ws" 1.27 + by (auto simp: append_eq_append_conv2) 1.28 + 1.29 + have "\<exists>m n zs. concat (replicate m zs) = xs' \<and> concat (replicate n zs) = ys'" 1.30 + proof (cases "ws = []") 1.31 + case True 1.32 + then have "concat (replicate 1 xs') = xs'" 1.33 + and "concat (replicate 1 xs') = ys'" 1.34 + using `ys' = xs' @ ws` by auto 1.35 + then show ?thesis by blast 1.36 + next 1.37 + case False 1.38 + from `ys' = xs' @ ws` and `xs' @ ys' = ys' @ xs'` 1.39 + have "xs' @ ws = ws @ xs'" by simp 1.40 + then have "\<exists>m n zs. concat (replicate m zs) = xs' \<and> concat (replicate n zs) = ws" 1.41 + using False and `xs' \<noteq> []` and `ys' = xs' @ ws` and len 1.42 + by (intro less.hyps) auto 1.43 + then obtain m n zs where "concat (replicate m zs) = xs'" 1.44 + and "concat (replicate n zs) = ws" by blast 1.45 + moreover 1.46 + then have "concat (replicate (m + n) zs) = ys'" 1.47 + using `ys' = xs' @ ws` 1.48 + by (simp add: replicate_add) 1.49 + ultimately 1.50 + show ?thesis by blast 1.51 + qed 1.52 + then show ?case 1.53 + using xs'_def ys'_def by metis 1.54 +qed 1.55 + 1.56 +lemma comm_append_is_replicate: 1.57 + fixes xs ys :: "'a list" 1.58 + assumes "xs \<noteq> []" "ys \<noteq> []" 1.59 + assumes "xs @ ys = ys @ xs" 1.60 + shows "\<exists>n zs. n > 1 \<and> concat (replicate n zs) = xs @ ys" 1.61 + 1.62 +proof - 1.63 + obtain m n zs where "concat (replicate m zs) = xs" 1.64 + and "concat (replicate n zs) = ys" 1.65 + using assms by (metis comm_append_are_replicate) 1.66 + then have "m + n > 1" and "concat (replicate (m+n) zs) = xs @ ys" 1.67 + using `xs \<noteq> []` and `ys \<noteq> []` 1.68 + by (auto simp: replicate_add) 1.69 + then show ?thesis by blast 1.70 +qed 1.71 + 1.72 1.73 subsubsection{*@{text rotate1} and @{text rotate}*} 1.74