author  lcp 
Wed, 06 Oct 1993 09:58:53 +0100  
changeset 30  d49df4181f0d 
parent 14  1c0926788772 
child 55  331d93292ee0 
permissions  rwrr 
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 
val major::prems = goal List.thy 

59 
"[ l: list(A); \ 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

60 
\ c: C(Nil); \ 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

61 
\ !!x y. [ x: A; y: list(A) ] ==> h(x,y): C(Cons(x,y)) \ 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

62 
\ ] ==> list_case(c,h,l) : C(l)"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

63 
by (rtac (major RS List.induct) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

64 
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (List.case_eqns @ prems)))); 
0  65 
val list_case_type = result(); 
66 

67 

68 
(** For recursion **) 

69 

30  70 
goalw List.thy List.con_defs "rank(a) < rank(Cons(a,l))"; 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

71 
by (simp_tac rank_ss 1); 
0  72 
val rank_Cons1 = result(); 
73 

30  74 
goalw List.thy List.con_defs "rank(l) < rank(Cons(a,l))"; 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

75 
by (simp_tac rank_ss 1); 
0  76 
val rank_Cons2 = result(); 
77 