src/HOL/Library/Sublist.thy
changeset 73381 3fdb94d87e0e
parent 73380 99c1c4f89605
child 73397 d47c8a89c6a5
equal deleted inserted replaced
73380:99c1c4f89605 73381:3fdb94d87e0e
  1383     by (auto simp: prefix_def)
  1383     by (auto simp: prefix_def)
  1384   show ?thesis
  1384   show ?thesis
  1385     by (simp add: ys zs1 zs2)
  1385     by (simp add: ys zs1 zs2)
  1386 qed
  1386 qed
  1387 
  1387 
       
  1388 lemma sublist_list_all: "sublist xs ys \<Longrightarrow> list_all P ys \<Longrightarrow> list_all P xs"
       
  1389   by (auto simp: sublist_def)
       
  1390 
       
  1391 lemmas prefix_list_all = prefix_imp_sublist[THEN sublist_list_all]
       
  1392 lemmas suffix_list_all = suffix_imp_sublist[THEN sublist_list_all]
       
  1393 
  1388 subsubsection \<open>\<open>sublists\<close>\<close>
  1394 subsubsection \<open>\<open>sublists\<close>\<close>
  1389 
  1395 
  1390 primrec sublists :: "'a list \<Rightarrow> 'a list list" where
  1396 primrec sublists :: "'a list \<Rightarrow> 'a list list" where
  1391   "sublists [] = [[]]"
  1397   "sublists [] = [[]]"
  1392 | "sublists (x # xs) = sublists xs @ map ((#) x) (prefixes xs)"
  1398 | "sublists (x # xs) = sublists xs @ map ((#) x) (prefixes xs)"