# HG changeset patch
# User nipkow
# Date 947516803 -3600
# Node ID c802042066e86ba680d72d8f949ebeedd2bdac36
# Parent  09a7a180cc99bce76c61d39eb1c31fbd48796a08
Forgot to "call" MicroJava in makefile.
Added list_all2 to List.

diff -r 09a7a180cc99 -r c802042066e8 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jan 07 11:06:03 2000 +0100
+++ b/src/HOL/IsaMakefile	Mon Jan 10 16:06:43 2000 +0100
@@ -10,7 +10,7 @@
 images: HOL HOL-Real TLA
 test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Algebra \
   HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-BCV \
-  HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
+  HOL-MicroJava HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
   HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
   HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
 
diff -r 09a7a180cc99 -r c802042066e8 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Jan 07 11:06:03 2000 +0100
+++ b/src/HOL/List.ML	Mon Jan 10 16:06:43 2000 +0100
@@ -993,6 +993,17 @@
 qed_spec_mp "zip_rev";
 
 Goal
+ "!ys. set(zip xs ys) = {(xs!i,ys!i) |i. i < min (length xs) (length ys)}";
+by(induct_tac "xs" 1);
+ by (Simp_tac 1);
+br allI 1;
+by(exhaust_tac "ys" 1);
+ by(Asm_simp_tac 1);
+by(auto_tac (claset(),
+           simpset() addsimps [nth_Cons,gr0_conv_Suc] addsplits [nat.split]));
+qed_spec_mp "set_zip";
+
+Goal
 "!i xs. i < length xs --> i < length ys --> (zip xs ys)!i = (xs!i, ys!i)";
 by (induct_tac "ys" 1);
  by (Simp_tac 1);
@@ -1017,6 +1028,34 @@
 qed "zip_replicate";
 Addsimps [zip_replicate];
 
+(** list_all2 **)
+section "list_all2";
+
+Goalw [list_all2_def] "list_all2 P xs ys ==> length xs = length ys";
+by(Asm_simp_tac 1);
+qed "list_all2_lengthD";
+
+Goalw [list_all2_def] "list_all2 P [] ys = (ys=[])";
+by (Simp_tac 1);
+qed "list_all2_Nil";
+AddIffs [list_all2_Nil];
+
+Goalw [list_all2_def] "list_all2 P xs [] = (xs=[])";
+by (Simp_tac 1);
+qed "list_all2_Nil2";
+AddIffs [list_all2_Nil2];
+
+Goalw [list_all2_def]
+ "list_all2 P (x#xs) (y#ys) = (P x y & list_all2 P xs ys)";
+by (Auto_tac);
+qed "list_all2_Cons";
+AddIffs[list_all2_Cons];
+
+Goalw [list_all2_def]
+  "list_all2 P xs ys = \
+\  (length xs = length ys & (!i<length xs. P (xs!i) (ys!i)))";
+by(force_tac (claset(), simpset() addsimps [set_zip]) 1);
+qed "list_all2_conv_all_nth";
 
 (** foldl **)
 section "foldl";
diff -r 09a7a180cc99 -r c802042066e8 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jan 07 11:06:03 2000 +0100
+++ b/src/HOL/List.thy	Mon Jan 10 16:06:43 2000 +0100
@@ -19,6 +19,7 @@
   hd, last    :: 'a list => 'a
   set         :: 'a list => 'a set
   list_all    :: ('a => bool) => ('a list => bool)
+  list_all2   :: ('a => 'b => bool) => 'a list => 'b list => bool
   map         :: ('a=>'b) => ('a list => 'b list)
   mem         :: ['a, 'a list] => bool                    (infixl 55)
   nth         :: ['a list, nat] => 'a			  (infixl "!" 100)
@@ -164,6 +165,10 @@
 primrec
   replicate_0   "replicate  0      x = []"
   replicate_Suc "replicate (Suc n) x = x # replicate n x"
+defs
+ list_all2_def
+ "list_all2 P xs ys == length xs = length ys & (!(x,y):set(zip xs ys). P x y)"
+
 
 (** Lexicographic orderings on lists **)
 
diff -r 09a7a180cc99 -r c802042066e8 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Fri Jan 07 11:06:03 2000 +0100
+++ b/src/HOL/Nat.ML	Mon Jan 10 16:06:43 2000 +0100
@@ -46,6 +46,10 @@
 (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
 bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
 
+Goal "(0<n) = (EX m. n = Suc m)";
+by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
+qed "gr0_conv_Suc";
+
 Goal "(~(0 < n)) = (n=0)";
 by (rtac iffI 1);
  by (etac swap 1);