author  lcp 
Mon, 01 Aug 1994 17:34:57 +0200  
changeset 503  15375d7b379c 
parent 486  6b58082796f6 
child 515  abcc438e7c27 
permissions  rwrr 
56  1 
(* Title: ZF/ex/data.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
Sample datatype definition. 

7 
It has four contructors, of arities 03, and two parameters A and B. 

8 
*) 

9 

10 
structure Data = Datatype_Fun 

279  11 
(val thy = Univ.thy 
503  12 
val thy_name = "Data" 
279  13 
val rec_specs = [("data", "univ(A Un B)", 
486  14 
[(["Con0"], "i", NoSyn), 
15 
(["Con1"], "i=>i", NoSyn), 

16 
(["Con2"], "[i,i]=>i", NoSyn), 

17 
(["Con3"], "[i,i,i]=>i", NoSyn)])] 

279  18 
val rec_styp = "[i,i]=>i" 
19 
val sintrs = 

20 
["Con0 : data(A,B)", 

21 
"[ a: A ] ==> Con1(a) : data(A,B)", 

22 
"[ a: A; b: B ] ==> Con2(a,b) : data(A,B)", 

23 
"[ a: A; b: B; d: data(A,B) ] ==> Con3(a,b,d) : data(A,B)"] 

24 
val monos = [] 

71
729fe026c5f3
sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents:
56
diff
changeset

25 
val type_intrs = datatype_intrs 
729fe026c5f3
sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents:
56
diff
changeset

26 
val type_elims = datatype_elims); 
56  27 

28 

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

30 

31 
goalw Data.thy Data.defs "!!A B. [ A<=C; B<=D ] ==> data(A,B) <= data(C,D)"; 

32 
by (rtac lfp_mono 1); 

33 
by (REPEAT (rtac Data.bnd_mono 1)); 

34 
by (REPEAT (ares_tac (univ_mono::Un_mono::basic_monos) 1)); 

35 
val data_mono = result(); 

36 

37 
goalw Data.thy (Data.defs@Data.con_defs) "data(univ(A),univ(A)) <= univ(A)"; 

38 
by (rtac lfp_lowerbound 1); 

39 
by (rtac ([A_subset_univ, Un_upper1] MRS subset_trans RS univ_mono) 2); 

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

41 
Pair_in_univ]) 1); 

42 
val data_univ = result(); 

43 

44 
val data_subset_univ = standard ([data_mono, data_univ] MRS subset_trans); 

45 

46 