added lemmas (sublist|prefix|suffix)_list_all
authordesharna
Fri, 05 Mar 2021 15:01:59 +0100
changeset 73629 3fdb94d87e0e
parent 73628 99c1c4f89605
child 73638 3c5a7746ffa4
added lemmas (sublist|prefix|suffix)_list_all
src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Fri Mar 05 14:23:14 2021 +0100
+++ b/src/HOL/Library/Sublist.thy	Fri Mar 05 15:01:59 2021 +0100
@@ -1385,6 +1385,12 @@
     by (simp add: ys zs1 zs2)
 qed
 
+lemma sublist_list_all: "sublist xs ys \<Longrightarrow> list_all P ys \<Longrightarrow> list_all P xs"
+  by (auto simp: sublist_def)
+
+lemmas prefix_list_all = prefix_imp_sublist[THEN sublist_list_all]
+lemmas suffix_list_all = suffix_imp_sublist[THEN sublist_list_all]
+
 subsubsection \<open>\<open>sublists\<close>\<close>
 
 primrec sublists :: "'a list \<Rightarrow> 'a list list" where