src/HOL/List.ML
changeset 5518 654ead0ba4f7
parent 5448 40a09282ba14
child 5537 c2bd39a2c0ee
     1.1 --- a/src/HOL/List.ML	Mon Sep 21 22:58:43 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Mon Sep 21 23:03:11 1998 +0200
     1.3 @@ -469,21 +469,31 @@
     1.4  bind_thm("in_listsI",in_lists_conv_set RS iffD2);
     1.5  AddSIs [in_listsI];
     1.6  
     1.7 +(** mem **)
     1.8 + 
     1.9 +section "mem";
    1.10 +
    1.11 +Goal "(x mem xs) = (x: set xs)";
    1.12 +by (induct_tac "xs" 1);
    1.13 +by Auto_tac;
    1.14 +qed "set_mem_eq";
    1.15 +
    1.16 +
    1.17  (** list_all **)
    1.18  
    1.19  section "list_all";
    1.20  
    1.21 +Goal "list_all P xs = (!x:set xs. P x)";
    1.22 +by (induct_tac "xs" 1);
    1.23 +by Auto_tac;
    1.24 +qed "list_all_conv";
    1.25 +
    1.26  Goal "list_all P (xs@ys) = (list_all P xs & list_all P ys)";
    1.27  by (induct_tac "xs" 1);
    1.28  by Auto_tac;
    1.29  qed "list_all_append";
    1.30  Addsimps [list_all_append];
    1.31  
    1.32 -Goal "list_all P xs = (!x. x mem xs --> P x)";
    1.33 -by (induct_tac "xs" 1);
    1.34 -by Auto_tac;
    1.35 -qed "list_all_conv";
    1.36 -
    1.37  
    1.38  (** filter **)
    1.39  
    1.40 @@ -583,7 +593,7 @@
    1.41  qed_spec_mp "nth_map";
    1.42  Addsimps [nth_map];
    1.43  
    1.44 -Goal "!n. n < length xs --> list_all P xs --> P(xs!n)";
    1.45 +Goal "!n. n < length xs --> Ball (set xs) P --> P(xs!n)";
    1.46  by (induct_tac "xs" 1);
    1.47  (* case [] *)
    1.48  by (Simp_tac 1);
    1.49 @@ -591,9 +601,9 @@
    1.50  by (rtac allI 1);
    1.51  by (induct_tac "n" 1);
    1.52  by Auto_tac;
    1.53 -qed_spec_mp "list_all_nth";
    1.54 +qed_spec_mp "list_ball_nth";
    1.55  
    1.56 -Goal "!n. n < length xs --> xs!n mem xs";
    1.57 +Goal "!n. n < length xs --> xs!n : set xs";
    1.58  by (induct_tac "xs" 1);
    1.59  (* case [] *)
    1.60  by (Simp_tac 1);
    1.61 @@ -607,6 +617,7 @@
    1.62  qed_spec_mp "nth_mem";
    1.63  Addsimps [nth_mem];
    1.64  
    1.65 +
    1.66  (** list update **)
    1.67  
    1.68  section "list update";