src/ZF/listfn.ML
 author lcp Fri, 17 Sep 1993 16:16:38 +0200 changeset 6 8ce8c4d13d4d parent 0 a5a9c433f639 child 14 1c0926788772 permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
```
(*  Title: 	ZF/list-fn.ML
ID:         \$Id\$
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

For list-fn.thy.  Lists in Zermelo-Fraenkel Set Theory
*)

open ListFn;

(** list_rec -- by Vset recursion **)

goal ListFn.thy "list_rec(Nil,c,h) = c";
by (rtac (list_rec_def RS def_Vrec RS trans) 1);
by (simp_tac (ZF_ss addsimps List.case_eqns) 1);
val list_rec_Nil = result();

goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
by (rtac (list_rec_def RS def_Vrec RS trans) 1);
by (simp_tac (ZF_ss addsimps (List.case_eqns @ [Vset_rankI, rank_Cons2])) 1);
val list_rec_Cons = result();

(*Type checking -- proved by induction, as usual*)
val prems = goal ListFn.thy
"[| l: list(A);    \
\       c: C(Nil);       \
\       !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))  \
\    |] ==> list_rec(l,c,h) : C(l)";
by (list_ind_tac "l" prems 1);
by (ALLGOALS (asm_simp_tac
val list_rec_type = result();

(** Versions for use with definitions **)

val [rew] = goal ListFn.thy
"[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
by (rewtac rew);
by (rtac list_rec_Nil 1);
val def_list_rec_Nil = result();

val [rew] = goal ListFn.thy
"[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
by (rewtac rew);
by (rtac list_rec_Cons 1);
val def_list_rec_Cons = result();

fun list_recs def = map standard
([def] RL [def_list_rec_Nil, def_list_rec_Cons]);

(** map **)

val [map_Nil,map_Cons] = list_recs map_def;

val prems = goalw ListFn.thy [map_def]
"[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
by (REPEAT (ares_tac (prems@[list_rec_type, NilI, ConsI]) 1));
val map_type = result();

val [major] = goal ListFn.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})";
by (rtac (major RS map_type) 1);
by (etac RepFunI 1);
val map_type2 = result();

(** length **)

val [length_Nil,length_Cons] = list_recs length_def;

val prems = goalw ListFn.thy [length_def]
"l: list(A) ==> length(l) : nat";
by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, nat_succI]) 1));
val length_type = result();

(** app **)

val [app_Nil,app_Cons] = list_recs app_def;

val prems = goalw ListFn.thy [app_def]
"[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
by (REPEAT (ares_tac (prems @ [list_rec_type, ConsI]) 1));
val app_type = result();

(** rev **)

val [rev_Nil,rev_Cons] = list_recs rev_def;

val prems = goalw ListFn.thy [rev_def]
"xs: list(A) ==> rev(xs) : list(A)";
by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1));
val rev_type = result();

(** flat **)

val [flat_Nil,flat_Cons] = list_recs flat_def;

val prems = goalw ListFn.thy [flat_def]
"ls: list(list(A)) ==> flat(ls) : list(A)";
by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1));
val flat_type = result();

val prems = goalw ListFn.thy [list_add_def]
"xs: list(nat) ==> list_add(xs) : nat";
by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, add_type]) 1));

(** ListFn simplification **)

val list_typechecks =
[NilI, ConsI, list_rec_type,
map_type, map_type2, app_type, length_type, rev_type, flat_type,

val list_ss = arith_ss
map_Nil, map_Cons,
app_Nil, app_Cons,
length_Nil, length_Cons,
rev_Nil, rev_Cons,
flat_Nil, flat_Cons,
setsolver (type_auto_tac list_typechecks);
(*Could also rewrite using the list_typechecks...*)

val prems = goal ListFn.thy
"l: list(A) ==> map(%u.u, l) = l";
by (list_ind_tac "l" prems 1);
by (ALLGOALS (asm_simp_tac list_ss));
val map_ident = result();

val prems = goal ListFn.thy
"l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
by (list_ind_tac "l" prems 1);
by (ALLGOALS (asm_simp_tac list_ss));
val map_compose = result();

val prems = goal ListFn.thy
"xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
by (list_ind_tac "xs" prems 1);
by (ALLGOALS (asm_simp_tac list_ss));
val map_app_distrib = result();

val prems = goal ListFn.thy
"ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
by (list_ind_tac "ls" prems 1);
by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
val map_flat = result();

val prems = goal ListFn.thy
"l: list(A) ==> \
\    list_rec(map(h,l), c, d) = \
\    list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
by (list_ind_tac "l" prems 1);
by (ALLGOALS (asm_simp_tac list_ss));
val list_rec_map = result();

(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)

(* c : list(Collect(B,P)) ==> c : list(B) *)
val list_CollectD = standard (Collect_subset RS list_mono RS subsetD);

val prems = goal ListFn.thy
"l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
by (list_ind_tac "l" prems 1);
by (ALLGOALS (asm_simp_tac list_ss));
val map_list_Collect = result();

val prems = goal ListFn.thy
"xs: list(A) ==> length(map(h,xs)) = length(xs)";
by (list_ind_tac "xs" prems 1);
by (ALLGOALS (asm_simp_tac list_ss));
val length_map = result();

val prems = goal ListFn.thy
"xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
by (list_ind_tac "xs" prems 1);
by (ALLGOALS (asm_simp_tac list_ss));
val length_app = result();

(* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m
Used for rewriting below*)

val prems = goal ListFn.thy
"xs: list(A) ==> length(rev(xs)) = length(xs)";
by (list_ind_tac "xs" prems 1);
val length_rev = result();

val prems = goal ListFn.thy
"ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
by (list_ind_tac "ls" prems 1);
by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app])));
val length_flat = result();

val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs";
by (rtac (major RS List.induct) 1);
by (ALLGOALS (asm_simp_tac list_ss));
val app_right_Nil = result();

val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
by (list_ind_tac "xs" prems 1);
by (ALLGOALS (asm_simp_tac list_ss));
val app_assoc = result();

val prems = goal ListFn.thy
"ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
by (list_ind_tac "ls" prems 1);
by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_assoc])));
val flat_app_distrib = result();

val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
by (list_ind_tac "l" prems 1);
by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
val rev_map_distrib = result();

(*Simplifier needs the premises as assumptions because rewriting will not
instantiate the variable ?A in the rules' typing conditions; note that
rev_type does not instantiate ?A.  Only the premises do.
*)
goal ListFn.thy
"!!xs. [| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
by (etac List.induct 1);
by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_right_Nil,app_assoc])));
val rev_app_distrib = result();

val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l";
by (list_ind_tac "l" prems 1);
by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_app_distrib])));
val rev_rev_ident = result();

val prems = goal ListFn.thy
"ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
by (list_ind_tac "ls" prems 1);
[map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
val rev_flat = result();

val prems = goal ListFn.thy
"[| xs: list(nat);  ys: list(nat) |] ==> \
by (cut_facts_tac prems 1);
by (list_ind_tac "xs" prems 1);
by (ALLGOALS
by (rtac (add_commute RS subst_context) 1);
by (REPEAT (ares_tac [refl, list_add_type] 1));

val prems = goal ListFn.thy
by (list_ind_tac "l" prems 1);
by (ALLGOALS

val prems = goal ListFn.thy
by (list_ind_tac "ls" prems 1);

(** New induction rule **)

val major::prems = goal ListFn.thy
"[| l: list(A);  \
\       P(Nil);        \
\       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x]) \
\    |] ==> P(l)";
by (rtac (major RS rev_rev_ident RS subst) 1);
by (rtac (major RS rev_type RS List.induct) 1);
by (ALLGOALS (asm_simp_tac (list_ss addsimps prems)));
val list_append_induct = result();

```