src/ZF/datatype.ML
author lcp
Fri, 15 Oct 1993 10:21:01 +0100
changeset 55 331d93292ee0
parent 0 a5a9c433f639
child 70 8a29f8b4aca1
permissions -rw-r--r--
ZF/ind-syntax/refl_thin: new ZF/intr-elim: added Pair_neq_0, succ_neq_0, refl_thin to simplify case rules ZF/sum/Inl_iff, etc.: tidied and proved using simp_tac ZF/qpair/QInl_iff, etc.: tidied and proved using simp_tac ZF/datatype,intr_elim: replaced the undirectional use of sum_univ RS subsetD by dresolve_tac InlD,InrD and etac PartE
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/datatype.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
(Co-) Datatype Definitions for Zermelo-Fraenkel Set Theory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
(*Datatype definitions use least fixedpoints, standard products and sums*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
functor Datatype_Fun (Const: CONSTRUCTOR) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
         : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
structure Constructor = Constructor_Fun (structure Const=Const and 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  		                      Pr=Standard_Prod and Su=Standard_Sum);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
open Const Constructor;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
structure Inductive = Inductive_Fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
        (val thy = con_thy;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
	 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
	 val sintrs = sintrs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
	 val monos = monos;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
	 val con_defs = con_defs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
	 val type_intrs = type_intrs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
	 val type_elims = type_elims);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
open Inductive
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
(*Co-datatype definitions use greatest fixedpoints, Quine products and sums*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
functor Co_Datatype_Fun (Const: CONSTRUCTOR) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
         : sig include CONSTRUCTOR_RESULT INTR_ELIM CO_INDRULE end =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
structure Constructor = Constructor_Fun (structure Const=Const and 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  		                      Pr=Quine_Prod and Su=Quine_Sum);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
open Const Constructor;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
structure Co_Inductive = Co_Inductive_Fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
        (val thy = con_thy;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
	 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
	 val sintrs = sintrs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
	 val monos = monos;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
	 val con_defs = con_defs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
	 val type_intrs = type_intrs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
	 val type_elims = type_elims);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
open Co_Inductive
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
(*For most datatypes involving univ*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
val data_typechecks = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
    [SigmaI, InlI, InrI,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
     Pair_in_univ, Inl_in_univ, Inr_in_univ, 
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 0
diff changeset
    58
     zero_in_univ, A_into_univ, nat_into_univ, UnCI];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 0
diff changeset
    60
(*Needed for mutual recursion*)
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 0
diff changeset
    61
val data_elims = [make_elim InlD, make_elim InrD];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
(*For most co-datatypes involving quniv*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
val co_data_typechecks = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
    [QSigmaI, QInlI, QInrI,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
     QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 0
diff changeset
    67
     zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 0
diff changeset
    69
val co_data_elims = [make_elim QInlD, make_elim QInrD];
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 0
diff changeset
    70