src/HOL/List.thy
changeset 69137 d4baf535f845
parent 69125 60b6c759134f
child 69140 f2d233f6356c
equal deleted inserted replaced
69135:be20f5f6feb9 69137:d4baf535f845
  4527 
  4527 
  4528 lemma splice_Nil2 [simp]: "splice xs [] = xs"
  4528 lemma splice_Nil2 [simp]: "splice xs [] = xs"
  4529 by (cases xs) simp_all
  4529 by (cases xs) simp_all
  4530 
  4530 
  4531 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
  4531 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
  4532   by (induct xs ys rule: splice.induct) auto
  4532 by (induct xs ys rule: splice.induct) auto
       
  4533 
       
  4534 lemma split_Nil_iff[simp]: "splice xs ys = [] \<longleftrightarrow> xs = [] \<and> ys = []"
       
  4535 by (induct xs ys rule: splice.induct) auto
  4533 
  4536 
  4534 
  4537 
  4535 subsubsection \<open>@{const shuffles}\<close>
  4538 subsubsection \<open>@{const shuffles}\<close>
  4536 
  4539 
  4537 lemma shuffles_commutes: "shuffles xs ys = shuffles ys xs"
  4540 lemma shuffles_commutes: "shuffles xs ys = shuffles ys xs"