equal
deleted
inserted
replaced
2200 |
2200 |
2201 lemma list_all2_Cons2: |
2201 lemma list_all2_Cons2: |
2202 "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)" |
2202 "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)" |
2203 by (cases xs) auto |
2203 by (cases xs) auto |
2204 |
2204 |
|
2205 lemma list_all2_induct |
|
2206 [consumes 1, case_names Nil Cons, induct set: list_all2]: |
|
2207 assumes P: "list_all2 P xs ys" |
|
2208 assumes Nil: "R [] []" |
|
2209 assumes Cons: "\<And>x xs y ys. \<lbrakk>P x y; R xs ys\<rbrakk> \<Longrightarrow> R (x # xs) (y # ys)" |
|
2210 shows "R xs ys" |
|
2211 using P |
|
2212 by (induct xs arbitrary: ys) (auto simp add: list_all2_Cons1 Nil Cons) |
|
2213 |
2205 lemma list_all2_rev [iff]: |
2214 lemma list_all2_rev [iff]: |
2206 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys" |
2215 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys" |
2207 by (simp add: list_all2_def zip_rev cong: conj_cong) |
2216 by (simp add: list_all2_def zip_rev cong: conj_cong) |
2208 |
2217 |
2209 lemma list_all2_rev1: |
2218 lemma list_all2_rev1: |