add induction rule for list_all2
authorhuffman
Fri Dec 09 13:42:16 2011 +0100 (2011-12-09)
changeset 4579416e8e4d33c42
parent 45793 331ebffe0593
child 45798 2373d86cf2e8
child 45803 fe44c0b216ef
add induction rule for list_all2
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Fri Dec 09 12:21:03 2011 +0100
     1.2 +++ b/src/HOL/List.thy	Fri Dec 09 13:42:16 2011 +0100
     1.3 @@ -2202,6 +2202,15 @@
     1.4  "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
     1.5  by (cases xs) auto
     1.6  
     1.7 +lemma list_all2_induct
     1.8 +  [consumes 1, case_names Nil Cons, induct set: list_all2]:
     1.9 +  assumes P: "list_all2 P xs ys"
    1.10 +  assumes Nil: "R [] []"
    1.11 +  assumes Cons: "\<And>x xs y ys. \<lbrakk>P x y; R xs ys\<rbrakk> \<Longrightarrow> R (x # xs) (y # ys)"
    1.12 +  shows "R xs ys"
    1.13 +using P
    1.14 +by (induct xs arbitrary: ys) (auto simp add: list_all2_Cons1 Nil Cons)
    1.15 +
    1.16  lemma list_all2_rev [iff]:
    1.17  "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
    1.18  by (simp add: list_all2_def zip_rev cong: conj_cong)