author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 279  7738aed3f84d 
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 

279  10 
(val thy = Univ.thy 
11 
val rec_specs = [("list", "univ(A)", 

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

13 
(["Cons"], "[i,i]=>i")])] 

14 
val rec_styp = "i=>i" 

15 
val ext = None 

16 
val sintrs = ["Nil : list(A)", 

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

18 
val monos = [] 

70
8a29f8b4aca1
ZF/indsyntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents:
55
diff
changeset

19 
val type_intrs = datatype_intrs 
84  20 
val type_elims = datatype_elims); 
0  21 

124  22 
store_theory "List" List.thy; 
23 

0  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  55 
val list_subset_univ = standard ([list_mono, list_univ] MRS subset_trans); 
0  56 

57 
val major::prems = goal List.thy 

58 
"[ l: list(A); \ 

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

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

60 
\ !!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

61 
\ ] ==> 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

62 
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

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

66 

67 
(** For recursion **) 

68 

30  69 
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

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

30  73 
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

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