--- 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];
--- a/List.thy Fri Jan 14 12:35:27 1994 +0100
+++ b/List.thy Mon Jan 24 15:59:02 1994 +0100
@@ -37,22 +37,29 @@
null :: "'a list => bool"
hd :: "'a list => 'a"
tl :: "'a list => 'a list"
+ mem :: "['a, 'a list] => bool" (infixl 55)
list_all :: "('a => bool) => ('a list => bool)"
map :: "('a=>'b) => ('a list => 'b list)"
"@" :: "['a list, 'a list] => 'a list" (infixr 65)
list_case :: "['a list, 'b, ['a, 'a list]=>'b] => 'b"
+ filter :: "['a => bool, 'a list] => 'a list"
(* List Enumeration *)
"[]" :: "'a list" ("[]")
"@List" :: "args => 'a list" ("[(_)]")
+ (* Special syntax for list_all and filter *)
+ "@Alls" :: "[id, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10)
+ "@filter" :: "[id, 'a list, bool] => 'a list" ("(1[_:_ ./ _])")
translations
"[x, xs]" == "Cons(x, [xs])"
"[x]" == "Cons(x, [])"
"[]" == "Nil"
+ "[x:xs . P]" == "filter(%x.P,xs)"
+ "Alls x:xs.P" == "list_all(%x.P,xs)"
rules
@@ -97,9 +104,13 @@
null_def "null(xs) == list_rec(xs, True, %x xs r.False)"
hd_def "hd(xs) == list_rec(xs, @x.True, %x xs r.x)"
tl_def "tl(xs) == list_rec(xs, @xs.True, %x xs r.xs)"
+ mem_def "x mem xs == \
+\ list_rec(xs, False, %y ys r. if(y=x, True, r))"
list_all_def "list_all(P, xs) == list_rec(xs, True, %x l r. P(x) & r)"
- map_def "map(f, xs) == list_rec(xs, Nil, %x l r. Cons(f(x), r))"
+ map_def "map(f, xs) == list_rec(xs, [], %x l r. Cons(f(x),r))"
append_def "xs@ys == list_rec(xs, ys, %x l r. Cons(x,r))"
+ filter_def "filter(P,xs) == \
+\ list_rec(xs, [], %x xs r. if(P(x), Cons(x,r), r))"
list_case_def "list_case(xs, a, f) == list_rec(xs, a, %x xs r.f(x, xs))"
end
--- a/Makefile Fri Jan 14 12:35:27 1994 +0100
+++ b/Makefile Mon Jan 24 15:59:02 1994 +0100
@@ -29,6 +29,7 @@
EX_FILES = ex/ROOT.ML ex/cla.ML ex/finite.ML ex/finite.thy\
ex/lexprod.ML ex/lexprod.thy ex/meson.ML ex/mesontest.ML\
ex/mt.ML ex/mt.thy ex/pl.ML ex/pl.thy ex/puzzle.ML ex/puzzle.thy\
+ ex/qsort.thy ex/qsort.ML\
ex/rec.ML ex/rec.thy ex/rel.ML ex/set.ML ex/simult.ML ex/simult.thy\
ex/term.ML ex/term.thy
--- a/simpdata.ML Fri Jan 14 12:35:27 1994 +0100
+++ b/simpdata.ML Mon Jan 24 15:59:02 1994 +0100
@@ -67,6 +67,7 @@
in
+val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";
val if_True = prove_goal HOL.thy "if(True,x,y) = x"
(fn _=>[stac if_def 1, fast_tac (HOL_cs addIs [select_equality]) 1]);
@@ -94,7 +95,7 @@
setmksimps mk_rews
setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac)
setsubgoaler asm_simp_tac
- addsimps ([if_True, if_False, o_apply] @ simp_thms)
+ addsimps ([if_True, if_False, o_apply, conj_assoc] @ simp_thms)
addcongs [imp_cong];
fun split_tac splits =