author | huffman |

Fri Dec 09 13:42:16 2011 +0100 (2011-12-09) | |

changeset 45794 | 16e8e4d33c42 |

parent 45793 | 331ebffe0593 |

child 45798 | 2373d86cf2e8 |

child 45803 | fe44c0b216ef |

add induction rule for list_all2

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)