Forgot to "call" MicroJava in makefile.
authornipkow
Mon Jan 10 16:06:43 2000 +0100 (2000-01-10)
changeset 8115c802042066e8
parent 8114 09a7a180cc99
child 8116 759f712f8f06
Forgot to "call" MicroJava in makefile.
Added list_all2 to List.
src/HOL/IsaMakefile
src/HOL/List.ML
src/HOL/List.thy
src/HOL/Nat.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Jan 07 11:06:03 2000 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Jan 10 16:06:43 2000 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  images: HOL HOL-Real TLA
     1.5  test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Algebra \
     1.6    HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-BCV \
     1.7 -  HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
     1.8 +  HOL-MicroJava HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
     1.9    HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
    1.10    HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
    1.11  
     2.1 --- a/src/HOL/List.ML	Fri Jan 07 11:06:03 2000 +0100
     2.2 +++ b/src/HOL/List.ML	Mon Jan 10 16:06:43 2000 +0100
     2.3 @@ -993,6 +993,17 @@
     2.4  qed_spec_mp "zip_rev";
     2.5  
     2.6  Goal
     2.7 + "!ys. set(zip xs ys) = {(xs!i,ys!i) |i. i < min (length xs) (length ys)}";
     2.8 +by(induct_tac "xs" 1);
     2.9 + by (Simp_tac 1);
    2.10 +br allI 1;
    2.11 +by(exhaust_tac "ys" 1);
    2.12 + by(Asm_simp_tac 1);
    2.13 +by(auto_tac (claset(),
    2.14 +           simpset() addsimps [nth_Cons,gr0_conv_Suc] addsplits [nat.split]));
    2.15 +qed_spec_mp "set_zip";
    2.16 +
    2.17 +Goal
    2.18  "!i xs. i < length xs --> i < length ys --> (zip xs ys)!i = (xs!i, ys!i)";
    2.19  by (induct_tac "ys" 1);
    2.20   by (Simp_tac 1);
    2.21 @@ -1017,6 +1028,34 @@
    2.22  qed "zip_replicate";
    2.23  Addsimps [zip_replicate];
    2.24  
    2.25 +(** list_all2 **)
    2.26 +section "list_all2";
    2.27 +
    2.28 +Goalw [list_all2_def] "list_all2 P xs ys ==> length xs = length ys";
    2.29 +by(Asm_simp_tac 1);
    2.30 +qed "list_all2_lengthD";
    2.31 +
    2.32 +Goalw [list_all2_def] "list_all2 P [] ys = (ys=[])";
    2.33 +by (Simp_tac 1);
    2.34 +qed "list_all2_Nil";
    2.35 +AddIffs [list_all2_Nil];
    2.36 +
    2.37 +Goalw [list_all2_def] "list_all2 P xs [] = (xs=[])";
    2.38 +by (Simp_tac 1);
    2.39 +qed "list_all2_Nil2";
    2.40 +AddIffs [list_all2_Nil2];
    2.41 +
    2.42 +Goalw [list_all2_def]
    2.43 + "list_all2 P (x#xs) (y#ys) = (P x y & list_all2 P xs ys)";
    2.44 +by (Auto_tac);
    2.45 +qed "list_all2_Cons";
    2.46 +AddIffs[list_all2_Cons];
    2.47 +
    2.48 +Goalw [list_all2_def]
    2.49 +  "list_all2 P xs ys = \
    2.50 +\  (length xs = length ys & (!i<length xs. P (xs!i) (ys!i)))";
    2.51 +by(force_tac (claset(), simpset() addsimps [set_zip]) 1);
    2.52 +qed "list_all2_conv_all_nth";
    2.53  
    2.54  (** foldl **)
    2.55  section "foldl";
     3.1 --- a/src/HOL/List.thy	Fri Jan 07 11:06:03 2000 +0100
     3.2 +++ b/src/HOL/List.thy	Mon Jan 10 16:06:43 2000 +0100
     3.3 @@ -19,6 +19,7 @@
     3.4    hd, last    :: 'a list => 'a
     3.5    set         :: 'a list => 'a set
     3.6    list_all    :: ('a => bool) => ('a list => bool)
     3.7 +  list_all2   :: ('a => 'b => bool) => 'a list => 'b list => bool
     3.8    map         :: ('a=>'b) => ('a list => 'b list)
     3.9    mem         :: ['a, 'a list] => bool                    (infixl 55)
    3.10    nth         :: ['a list, nat] => 'a			  (infixl "!" 100)
    3.11 @@ -164,6 +165,10 @@
    3.12  primrec
    3.13    replicate_0   "replicate  0      x = []"
    3.14    replicate_Suc "replicate (Suc n) x = x # replicate n x"
    3.15 +defs
    3.16 + list_all2_def
    3.17 + "list_all2 P xs ys == length xs = length ys & (!(x,y):set(zip xs ys). P x y)"
    3.18 +
    3.19  
    3.20  (** Lexicographic orderings on lists **)
    3.21  
     4.1 --- a/src/HOL/Nat.ML	Fri Jan 07 11:06:03 2000 +0100
     4.2 +++ b/src/HOL/Nat.ML	Mon Jan 10 16:06:43 2000 +0100
     4.3 @@ -46,6 +46,10 @@
     4.4  (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
     4.5  bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
     4.6  
     4.7 +Goal "(0<n) = (EX m. n = Suc m)";
     4.8 +by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
     4.9 +qed "gr0_conv_Suc";
    4.10 +
    4.11  Goal "(~(0 < n)) = (n=0)";
    4.12  by (rtac iffI 1);
    4.13   by (etac swap 1);