--- a/CONTRIBUTORS Thu Nov 26 18:09:15 2020 +0000
+++ b/CONTRIBUTORS Thu Nov 26 20:49:40 2020 +0000
@@ -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:09:15 2020 +0000
+++ b/src/HOL/Data_Structures/Interval_Tree.thy Thu Nov 26 20:49:40 2020 +0000
@@ -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:09:15 2020 +0000
+++ b/src/HOL/List.thy Thu Nov 26 20:49:40 2020 +0000
@@ -4542,27 +4542,25 @@
"replicate (length (filter (\<lambda>y. x = y) xs)) x = filter (\<lambda>y. x = y) xs"
by (induct xs) auto
-text \<open>This stronger version is thanks to Stepan Holub\<close>
lemma comm_append_are_replicate:
- "xs @ ys = ys @ xs
- \<Longrightarrow> \<exists>m n zs. concat (replicate m zs) = xs \<and> concat (replicate n zs) = ys"
+ "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
- consider "length ys < length xs" | "xs = []" | "length xs \<le> length ys \<and> xs \<noteq> []"
+ consider (1) "length ys < length xs" | (2) "xs = []" | (3) "length xs \<le> length ys \<and> xs \<noteq> []"
by linarith
then show ?case
proof (cases)
- assume "length ys < length xs"
+ case 1
then show ?thesis
using less.hyps[OF _ less.prems[symmetric]] nat_add_left_cancel_less by auto
next
- assume "xs = []"
+ case 2
then have "concat (replicate 0 ys) = xs \<and> concat (replicate 1 ys) = ys"
by simp
- then show ?case
+ then show ?thesis
by blast
next
- assume "length xs \<le> length ys \<and> xs \<noteq> []"
+ 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>
@@ -4580,7 +4578,7 @@
then have "concat (replicate (m+n') zs) = ys"
using \<open>ys = xs @ ws\<close>
by (simp add: replicate_add)
- then show ?case
+ then show ?thesis
using \<open>concat (replicate m zs) = xs\<close> by blast
qed
qed
@@ -4593,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] 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)