src/HOL/List.thy
changeset 69140 f2d233f6356c
parent 69137 d4baf535f845
child 69206 a5c0d61ce5db
equal deleted inserted replaced
69139:4f3d93f0ba94 69140:f2d233f6356c
  4532 by (induct xs ys rule: splice.induct) auto
  4532 by (induct xs ys rule: splice.induct) auto
  4533 
  4533 
  4534 lemma split_Nil_iff[simp]: "splice xs ys = [] \<longleftrightarrow> xs = [] \<and> ys = []"
  4534 lemma split_Nil_iff[simp]: "splice xs ys = [] \<longleftrightarrow> xs = [] \<and> ys = []"
  4535 by (induct xs ys rule: splice.induct) auto
  4535 by (induct xs ys rule: splice.induct) auto
  4536 
  4536 
       
  4537 lemma splice_replicate[simp]: "splice (replicate m x) (replicate n x) = replicate (m+n) x"
       
  4538 apply(induction "replicate m x" "replicate n x" arbitrary: m n rule: splice.induct)
       
  4539 apply (auto simp add: Cons_replicate_eq dest: gr0_implies_Suc)
       
  4540 done
  4537 
  4541 
  4538 subsubsection \<open>@{const shuffles}\<close>
  4542 subsubsection \<open>@{const shuffles}\<close>
  4539 
  4543 
  4540 lemma shuffles_commutes: "shuffles xs ys = shuffles ys xs"
  4544 lemma shuffles_commutes: "shuffles xs ys = shuffles ys xs"
  4541 by (induction xs ys rule: shuffles.induct) (simp_all add: Un_commute)
  4545 by (induction xs ys rule: shuffles.induct) (simp_all add: Un_commute)