src/ZF/list.ML

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.ML
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Datatype definition of Lists
*)

structure List = Datatype_Fun
 (val thy = Univ.thy;
  val rec_specs = 
      [("list", "univ(A)",
	  [(["Nil"],	"i"), 
	   (["Cons"],	"[i,i]=>i")])];
  val rec_styp = "i=>i";
  val ext = None
  val sintrs = 
      ["Nil : list(A)",
       "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"];
  val monos = [];
  val type_intrs = data_typechecks
  val type_elims = []);

val [NilI, ConsI] = List.intrs;

(*An elimination rule, for type-checking*)
val ConsE = List.mk_cases List.con_defs "Cons(a,l) : list(A)";

(*Proving freeness results*)
val Cons_iff     = List.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'";
val Nil_Cons_iff = List.mk_free "~ Nil=Cons(a,l)";

(*Perform induction on l, then prove the major premise using prems. *)
fun list_ind_tac a prems i = 
    EVERY [res_inst_tac [("x",a)] List.induct i,
	   rename_last_tac a ["1"] (i+2),
	   ares_tac prems i];

(**  Lemmas to justify using "list" in other recursive type definitions **)

goalw List.thy List.defs "!!A B. A<=B ==> list(A) <= list(B)";
by (rtac lfp_mono 1);
by (REPEAT (rtac List.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
val list_mono = result();

(*There is a similar proof by list induction.*)
goalw List.thy ([e-mail]_defs) "list(univ(A)) <= univ(A)";
by (rtac lfp_lowerbound 1);
by (rtac (A_subset_univ RS univ_mono) 2);
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
			    Pair_in_univ]) 1);
val list_univ = result();

val list_subset_univ = standard
    (list_mono RS (list_univ RSN (2,subset_trans)));

(*****
val major::prems = goal List.thy
    "[| l: list(A);    \
\       c: C(0);       \
\       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(<x,y>)  \
\    |] ==> list_case(l,c,h) : C(l)";
by (rtac (major RS list_induct) 1);
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
			    ([list_case_0,list_case_Pair]@prems))));
val list_case_type = result();
****)


(** For recursion **)

goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
by (simp_tac rank_ss 1);
val rank_Cons1 = result();

goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
by (simp_tac rank_ss 1);
val rank_Cons2 = result();