author  lcp 
Fri, 22 Oct 1993 11:34:41 +0100  
changeset 70  8a29f8b4aca1 
parent 55  331d93292ee0 
child 120  09287f26bfb8 
permissions  rwrr 
0  1 
(* Title: ZF/datatype.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
(Co) Datatype Definitions for ZermeloFraenkel Set Theory 

7 

8 
*) 

9 

10 

11 
(*Datatype definitions use least fixedpoints, standard products and sums*) 

12 
functor Datatype_Fun (Const: CONSTRUCTOR) 

13 
: sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end = 

14 
struct 

15 
structure Constructor = Constructor_Fun (structure Const=Const and 

16 
Pr=Standard_Prod and Su=Standard_Sum); 

17 
open Const Constructor; 

18 

19 
structure Inductive = Inductive_Fun 

20 
(val thy = con_thy; 

21 
val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs); 

22 
val sintrs = sintrs; 

23 
val monos = monos; 

24 
val con_defs = con_defs; 

25 
val type_intrs = type_intrs; 

26 
val type_elims = type_elims); 

27 

28 
open Inductive 

29 
end; 

30 

31 

32 
(*Codatatype definitions use greatest fixedpoints, Quine products and sums*) 

33 
functor Co_Datatype_Fun (Const: CONSTRUCTOR) 

34 
: sig include CONSTRUCTOR_RESULT INTR_ELIM CO_INDRULE end = 

35 
struct 

36 
structure Constructor = Constructor_Fun (structure Const=Const and 

37 
Pr=Quine_Prod and Su=Quine_Sum); 

38 
open Const Constructor; 

39 

40 
structure Co_Inductive = Co_Inductive_Fun 

41 
(val thy = con_thy; 

42 
val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs); 

43 
val sintrs = sintrs; 

44 
val monos = monos; 

45 
val con_defs = con_defs; 

46 
val type_intrs = type_intrs; 

47 
val type_elims = type_elims); 

48 

49 
open Co_Inductive 

50 
end; 

51 

52 

53 

54 
(*For most datatypes involving univ*) 

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

55 
val datatype_intrs = 
0  56 
[SigmaI, InlI, InrI, 
57 
Pair_in_univ, Inl_in_univ, Inr_in_univ, 

55  58 
zero_in_univ, A_into_univ, nat_into_univ, UnCI]; 
0  59 

55  60 
(*Needed for mutual recursion*) 
70
8a29f8b4aca1
ZF/indsyntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents:
55
diff
changeset

61 
val datatype_elims = [make_elim InlD, make_elim InrD]; 
0  62 

63 
(*For most codatatypes involving quniv*) 

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

64 
val co_datatype_intrs = 
0  65 
[QSigmaI, QInlI, QInrI, 
66 
QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 

55  67 
zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI]; 
0  68 

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

69 
val co_datatype_elims = [make_elim QInlD, make_elim QInrD]; 
55  70 