0

1 
(* Title: ZF/list.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Datatype definition of Lists


7 
*)


8 


9 
structure List = Datatype_Fun


10 
(val thy = Univ.thy;


11 
val rec_specs =


12 
[("list", "univ(A)",


13 
[(["Nil"], "i"),


14 
(["Cons"], "[i,i]=>i")])];


15 
val rec_styp = "i=>i";


16 
val ext = None


17 
val sintrs =


18 
["Nil : list(A)",


19 
"[ a: A; l: list(A) ] ==> Cons(a,l) : list(A)"];


20 
val monos = [];


21 
val type_intrs = data_typechecks


22 
val type_elims = []);


23 


24 
val [NilI, ConsI] = List.intrs;


25 


26 
(*An elimination rule, for typechecking*)


27 
val ConsE = List.mk_cases List.con_defs "Cons(a,l) : list(A)";


28 


29 
(*Proving freeness results*)


30 
val Cons_iff = List.mk_free "Cons(a,l)=Cons(a',l') <> a=a' & l=l'";


31 
val Nil_Cons_iff = List.mk_free "~ Nil=Cons(a,l)";


32 


33 
(*Perform induction on l, then prove the major premise using prems. *)


34 
fun list_ind_tac a prems i =


35 
EVERY [res_inst_tac [("x",a)] List.induct i,


36 
rename_last_tac a ["1"] (i+2),


37 
ares_tac prems i];


38 


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


40 


41 
goalw List.thy List.defs "!!A B. A<=B ==> list(A) <= list(B)";


42 
by (rtac lfp_mono 1);


43 
by (REPEAT (rtac List.bnd_mono 1));


44 
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));


45 
val list_mono = result();


46 


47 
(*There is a similar proof by list induction.*)


48 
goalw List.thy (List.defs@List.con_defs) "list(univ(A)) <= univ(A)";


49 
by (rtac lfp_lowerbound 1);


50 
by (rtac (A_subset_univ RS univ_mono) 2);


51 
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,


52 
Pair_in_univ]) 1);


53 
val list_univ = result();


54 


55 
val list_subset_univ = standard


56 
(list_mono RS (list_univ RSN (2,subset_trans)));


57 


58 
(*****


59 
val major::prems = goal List.thy


60 
"[ l: list(A); \


61 
\ c: C(0); \


62 
\ !!x y. [ x: A; y: list(A) ] ==> h(x,y): C(<x,y>) \


63 
\ ] ==> list_case(l,c,h) : C(l)";


64 
by (rtac (major RS list_induct) 1);


65 
by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews


66 
([list_case_0,list_case_Pair]@prems))));


67 
val list_case_type = result();


68 
****)


69 


70 


71 
(** For recursion **)


72 


73 
goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";


74 
by (SIMP_TAC rank_ss 1);


75 
val rank_Cons1 = result();


76 


77 
goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";


78 
by (SIMP_TAC rank_ss 1);


79 
val rank_Cons2 = result();


80 
