List.ML

--- 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];