src/HOL/List.thy
changeset 36154 11c6106d7787
parent 35828 46cfc4b8112e
child 36176 3fe7e97ccca8
     1.1 --- a/src/HOL/List.thy	Thu Apr 15 12:27:14 2010 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Apr 15 16:55:12 2010 +0200
     1.3 @@ -513,6 +513,17 @@
     1.4      (cases zs, simp_all)
     1.5  qed
     1.6  
     1.7 +lemma list_induct4 [consumes 3, case_names Nil Cons]:
     1.8 +  "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow>
     1.9 +   P [] [] [] [] \<Longrightarrow> (\<And>x xs y ys z zs w ws. length xs = length ys \<Longrightarrow>
    1.10 +   length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow> P xs ys zs ws \<Longrightarrow>
    1.11 +   P (x#xs) (y#ys) (z#zs) (w#ws)) \<Longrightarrow> P xs ys zs ws"
    1.12 +proof (induct xs arbitrary: ys zs ws)
    1.13 +  case Nil then show ?case by simp
    1.14 +next
    1.15 +  case (Cons x xs ys zs ws) then show ?case by ((cases ys, simp_all), (cases zs,simp_all)) (cases ws, simp_all)
    1.16 +qed
    1.17 +
    1.18  lemma list_induct2': 
    1.19    "\<lbrakk> P [] [];
    1.20    \<And>x xs. P (x#xs) [];