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

author | nipkow |

Thu, 26 Nov 2020 19:27:42 +0100 | |

changeset 72734 | e0ceaca7344a |

parent 72731 | 178de0e275a1 (current diff) |

parent 72733 | 7b918b9f0122 (diff) |

child 72737 | 98fe7a10ace3 |

merged

--- a/CONTRIBUTORS Thu Nov 26 18:32:06 2020 +0100 +++ b/CONTRIBUTORS Thu Nov 26 19:27:42 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/Data_Structures/Interval_Tree.thy Thu Nov 26 18:32:06 2020 +0100 +++ b/src/HOL/Data_Structures/Interval_Tree.thy Thu Nov 26 19:27:42 2020 +0100 @@ -265,10 +265,13 @@ fixes has_overlap :: "'t \<Rightarrow> 'a::linorder ivl \<Rightarrow> bool" assumes set_overlap: "invar s \<Longrightarrow> has_overlap s x = Interval_Tree.has_overlap (set s) x" +fun invar :: "('a::{linorder,order_bot}) ivl_tree \<Rightarrow> bool" where +"invar t = (inv_max_hi t \<and> sorted(inorder t))" + interpretation S: Interval_Set where empty = Leaf and insert = insert and delete = delete and has_overlap = search and isin = isin and set = set_tree - and invar = "\<lambda>t. inv_max_hi t \<and> sorted (inorder t)" + and invar = invar proof (standard, goal_cases) case 1 then show ?case by auto

--- a/src/HOL/List.thy Thu Nov 26 18:32:06 2020 +0100 +++ b/src/HOL/List.thy Thu Nov 26 19:27:42 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)