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

author | nipkow |

Thu, 26 Nov 2020 14:53:38 +0100 | |

changeset 72732 | bfd1022cd947 |

parent 72713 | fabd29c73098 |

child 72733 | 7b918b9f0122 |

removed assumptions in lemma (Stepan Holub)

CONTRIBUTORS | file | annotate | diff | comparison | revisions | |

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

--- a/CONTRIBUTORS Wed Nov 25 21:13:45 2020 +0100 +++ b/CONTRIBUTORS Thu Nov 26 14:53:38 2020 +0100 @@ -5,6 +5,8 @@ Contributions to this Isabelle version -------------------------------------- +* November 2020: Stepan Holub + Removed preconditions from lemma comm_append_are_replicate * November 2020: Florian Haftmann Bundle mixins for locale and class expressions.

--- a/src/HOL/List.thy Wed Nov 25 21:13:45 2020 +0100 +++ b/src/HOL/List.thy Thu Nov 26 14:53:38 2020 +0100 @@ -4543,47 +4543,44 @@ by (induct xs) auto lemma comm_append_are_replicate: - "\<lbrakk> xs \<noteq> []; ys \<noteq> []; xs @ ys = ys @ xs \<rbrakk> - \<Longrightarrow> \<exists>m n zs. concat (replicate m zs) = xs \<and> concat (replicate n zs) = ys" -proof (induction "length (xs @ ys)" arbitrary: xs ys rule: less_induct) + "xs @ ys = ys @ xs \<Longrightarrow> \<exists>m n zs. concat (replicate m zs) = xs \<and> concat (replicate n zs) = ys" +proof (induction "length (xs @ ys) + length xs" arbitrary: xs ys rule: less_induct) case less - - define xs' ys' where "xs' = (if (length xs \<le> length ys) then xs else ys)" - and "ys' = (if (length xs \<le> length ys) then ys else xs)" - then have - prems': "length xs' \<le> length ys'" - "xs' @ ys' = ys' @ xs'" - and "xs' \<noteq> []" - and len: "length (xs @ ys) = length (xs' @ ys')" - using less by (auto intro: less.hyps) - - from prems' - obtain ws where "ys' = xs' @ ws" - by (auto simp: append_eq_append_conv2) - - have "\<exists>m n zs. concat (replicate m zs) = xs' \<and> concat (replicate n zs) = ys'" - proof (cases "ws = []") - case True - then have "concat (replicate 1 xs') = xs'" - and "concat (replicate 1 xs') = ys'" - using \<open>ys' = xs' @ ws\<close> by auto - then show ?thesis by blast + consider (1) "length ys < length xs" | (2) "xs = []" | (3) "length xs \<le> length ys \<and> xs \<noteq> []" + by linarith + then show ?case + proof (cases) + case 1 + then show ?thesis + using less.hyps[OF _ less.prems[symmetric]] nat_add_left_cancel_less by auto + next + case 2 + then have "concat (replicate 0 ys) = xs \<and> concat (replicate 1 ys) = ys" + by simp + then show ?thesis + by blast next - case False - from \<open>ys' = xs' @ ws\<close> and \<open>xs' @ ys' = ys' @ xs'\<close> - have "xs' @ ws = ws @ xs'" by simp - then have "\<exists>m n zs. concat (replicate m zs) = xs' \<and> concat (replicate n zs) = ws" - using False and \<open>xs' \<noteq> []\<close> and \<open>ys' = xs' @ ws\<close> and len - by (intro less.hyps) auto - then obtain m n zs where *: "concat (replicate m zs) = xs'" - and "concat (replicate n zs) = ws" by blast - then have "concat (replicate (m + n) zs) = ys'" - using \<open>ys' = xs' @ ws\<close> + case 3 + then have "length xs \<le> length ys" and "xs \<noteq> []" + by blast+ + from \<open>length xs \<le> length ys\<close> and \<open>xs @ ys = ys @ xs\<close> + obtain ws where "ys = xs @ ws" + by (auto simp: append_eq_append_conv2) + from this and \<open>xs \<noteq> []\<close> + have "length ws < length ys" + by simp + from \<open>xs @ ys = ys @ xs\<close>[unfolded \<open>ys = xs @ ws\<close>] + have "xs @ ws = ws @ xs" + by simp + from less.hyps[OF _ this] \<open>length ws < length ys\<close> + obtain m n' zs where "concat (replicate m zs) = xs" and "concat (replicate n' zs) = ws" + by auto + then have "concat (replicate (m+n') zs) = ys" + using \<open>ys = xs @ ws\<close> by (simp add: replicate_add) - with * show ?thesis by blast + then show ?thesis + using \<open>concat (replicate m zs) = xs\<close> by blast qed - then show ?case - using xs'_def ys'_def by meson qed lemma comm_append_is_replicate: @@ -4594,7 +4591,7 @@ proof - obtain m n zs where "concat (replicate m zs) = xs" and "concat (replicate n zs) = ys" - using comm_append_are_replicate[of xs ys, OF assms] by blast + using comm_append_are_replicate[OF assms(3)] by blast then have "m + n > 1" and "concat (replicate (m+n) zs) = xs @ ys" using \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close> by (auto simp: replicate_add)