--- a/List.ML Fri Jan 14 12:35:27 1994 +0100
+++ b/List.ML Mon Jan 24 15:59:02 1994 +0100
@@ -281,59 +281,86 @@
by (REPEAT (resolve_tac (List_rec_CONS::prems) 1));
val Abs_map_CONS = result();
-(** null, hd, tl, list_case **)
-
-goalw List.thy [null_def] "null([]) = True";
+(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *)
+val [rew] = goal List.thy
+ "[| !!xs. f(xs) == list_rec(xs,c,h) |] ==> f([]) = c";
+by (rewtac rew);
by (rtac list_rec_Nil 1);
-val null_Nil = result();
+val def_list_rec_Nil = result();
-goalw List.thy [null_def] "null(Cons(x,xs)) = False";
-by (rtac list_rec_Cons 1);
-val null_Cons = result();
-
-
-goalw List.thy [hd_def] "hd(Cons(x,xs)) = x";
+val [rew] = goal List.thy
+ "[| !!xs. f(xs) == list_rec(xs,c,h) |] ==> f(Cons(x,xs)) = h(x,xs,f(xs))";
+by (rewtac rew);
by (rtac list_rec_Cons 1);
-val hd_Cons = result();
-
+val def_list_rec_Cons = result();
-goalw List.thy [tl_def] "tl(Cons(x,xs)) = xs";
-by (rtac list_rec_Cons 1);
-val tl_Cons = result();
+fun list_recs def =
+ [standard (def RS def_list_rec_Nil),
+ standard (def RS def_list_rec_Cons)];
+(*** Unfolding the basic combinators ***)
-goalw List.thy [list_case_def] "list_case([],a,f) = a";
-by (rtac list_rec_Nil 1);
-val list_case_Nil = result();
+val [null_Nil,null_Cons] = list_recs null_def;
+val [_,hd_Cons] = list_recs hd_def;
+val [_,tl_Cons] = list_recs tl_def;
+val [append_Nil,append_Cons] = list_recs append_def;
+val [mem_Nil, mem_Cons] = list_recs mem_def;
+val [map_Nil,map_Cons] = list_recs map_def;
+val [list_case_Nil,list_case_Cons] = list_recs list_case_def;
+val [filter_Nil,filter_Cons] = list_recs filter_def;
+val [list_all_Nil,list_all_Cons] = list_recs list_all_def;
-goalw List.thy [list_case_def] "list_case(Cons(x,xs),a,f) = f(x,xs)";
-by (rtac list_rec_Cons 1);
-val list_case_Cons = result();
+val list_ss = arith_ss addsimps
+ [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq,
+ list_rec_Nil, list_rec_Cons,
+ null_Nil, null_Cons, hd_Cons, tl_Cons,
+ mem_Nil, mem_Cons,
+ list_case_Nil, list_case_Cons,
+ append_Nil, append_Cons,
+ map_Nil, map_Cons,
+ list_all_Nil, list_all_Cons,
+ filter_Nil, filter_Cons];
+
(** @ - append **)
-goalw List.thy [append_def] "[]@xs = xs";
-by (rtac list_rec_Nil 1);
-val append_Nil = result();
-
-goalw List.thy [append_def] "Cons(x,xs)@ys = Cons(x,xs@ys)";
-by (rtac list_rec_Cons 1);
-val append_Cons = result();
-
goal List.thy "(xs@ys)@zs = xs@(ys@zs)";
-by(res_inst_tac [("l","xs")] list_induct 1);
-by(REPEAT(asm_simp_tac (list_ss addsimps [append_Nil,append_Cons]) 1));
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac list_ss));
val append_assoc = result();
-(** The functional "map" **)
+(** mem **)
+
+goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if]))));
+val mem_append = result();
+
+goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if]))));
+val mem_filter = result();
+
+(** list_all **)
-goalw List.thy [map_def] "map(f,Nil) = Nil";
-by (rtac list_rec_Nil 1);
-val map_Nil = result();
+goal List.thy "(Alls x:xs.True) = True";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac list_ss));
+val list_all_True = result();
-goalw List.thy [map_def] "map(f, Cons(x,xs)) = Cons(f(x), map(f,xs))";
-by (rtac list_rec_Cons 1);
-val map_Cons = result();
+goal List.thy "list_all(p,xs@ys) = (list_all(p,xs) & list_all(p,ys))";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac list_ss));
+val list_all_conj = result();
+
+goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if]))));
+by(fast_tac HOL_cs 1);
+val list_all_mem_conv = result();
+
+
+(** The functional "map" **)
val map_simps = [Abs_map_NIL, Abs_map_CONS,
Rep_map_Nil, Rep_map_Cons,
@@ -350,17 +377,6 @@
(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
-(** The functional "list_all" -- creates predicates over lists **)
-
-goalw List.thy [list_all_def] "list_all(P,Nil) = True";
-by (rtac list_rec_Nil 1);
-val list_all_Nil = result();
-
-goalw List.thy [list_all_def]
- "list_all(P, Cons(x,xs)) = (P(x) & list_all(P,xs))";
-by (rtac list_rec_Cons 1);
-val list_all_Cons = result();
-
(** Additional mapping lemmas **)
goal List.thy "map(%x.x, xs) = xs";
@@ -375,11 +391,6 @@
[Rep_map_type,List_Sexp RS subsetD])));
val Abs_Rep_map = result();
-val list_ss = arith_ss addsimps
- [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq,
- list_rec_Nil, list_rec_Cons,
- null_Nil, null_Cons, hd_Cons, tl_Cons,
- list_case_Nil, list_case_Cons,
- append_Nil, append_Cons, append_assoc,
- map_Nil, map_Cons, map_ident,
- list_all_Nil, list_all_Cons];
+val list_ss = list_ss addsimps
+ [mem_append, mem_filter, append_assoc, map_ident,
+ list_all_True, list_all_conj];