src/HOL/List.thy
changeset 14247 cb32eb89bddd
parent 14208 144f45277d5a
child 14300 bf8b8c9425c3
     1.1 --- a/src/HOL/List.thy	Fri Oct 24 01:44:12 2003 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Oct 29 01:17:06 2003 +0100
     1.3 @@ -291,6 +291,17 @@
     1.4  apply (induct xs, auto)
     1.5  done
     1.6  
     1.7 +lemma list_induct2[consumes 1]: "\<And>ys.
     1.8 + \<lbrakk> length xs = length ys;
     1.9 +   P [] [];
    1.10 +   \<And>x xs y ys. \<lbrakk> length xs = length ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
    1.11 + \<Longrightarrow> P xs ys"
    1.12 +apply(induct xs)
    1.13 + apply simp
    1.14 +apply(case_tac ys)
    1.15 + apply simp
    1.16 +apply(simp)
    1.17 +done
    1.18  
    1.19  subsection {* @{text "@"} -- append *}
    1.20  
    1.21 @@ -968,10 +979,8 @@
    1.22  by (simp add: zip_append1)
    1.23  
    1.24  lemma zip_rev:
    1.25 -"!!xs. length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
    1.26 -apply (induct ys, simp)
    1.27 -apply (case_tac xs, simp_all)
    1.28 -done
    1.29 +"length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
    1.30 +by (induct rule:list_induct2, simp_all)
    1.31  
    1.32  lemma nth_zip [simp]:
    1.33  "!!i xs. [| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
    1.34 @@ -1051,11 +1060,9 @@
    1.35  done
    1.36  
    1.37  lemma list_all2_append:
    1.38 -  "\<And>b. length a = length b \<Longrightarrow>
    1.39 -  list_all2 P (a@c) (b@d) = (list_all2 P a b \<and> list_all2 P c d)"
    1.40 -  apply (induct a, simp)
    1.41 -  apply (case_tac b, auto)
    1.42 -  done
    1.43 +  "length xs = length ys \<Longrightarrow>
    1.44 +  list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"
    1.45 +by (induct rule:list_induct2, simp_all)
    1.46  
    1.47  lemma list_all2_appendI [intro?, trans]:
    1.48    "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"