src/HOL/List.thy
changeset 42714 fcba668b0839
parent 42713 276c8cbeb5d2
child 42809 5b45125b15ba
     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