list_all2_rev
authorkleing
Sun Dec 16 00:17:18 2001 +0100 (2001-12-16)
changeset 125153fb416265ba9
parent 12514 4bdbc5a977f6
child 12516 d09d0f160888
list_all2_rev
src/HOL/List.ML
     1.1 --- a/src/HOL/List.ML	Fri Dec 14 22:32:52 2001 +0100
     1.2 +++ b/src/HOL/List.ML	Sun Dec 16 00:17:18 2001 +0100
     1.3 @@ -1092,6 +1092,12 @@
     1.4  qed "list_all2_Cons2";
     1.5  
     1.6  Goalw [list_all2_def]
     1.7 + "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys";
     1.8 +by (asm_full_simp_tac (simpset() addsimps [zip_rev] addcongs [conj_cong]) 1);
     1.9 +qed "list_all2_rev";
    1.10 +AddIffs[list_all2_rev];
    1.11 +
    1.12 +Goalw [list_all2_def]
    1.13   "list_all2 P (xs@ys) zs = \
    1.14  \ (EX us vs. zs = us@vs & length us = length xs & length vs = length ys & \
    1.15  \            list_all2 P xs us & list_all2 P ys vs)";