src/ZF/Datatype.ML
author lcp
Thu, 24 Nov 1994 10:23:41 +0100
changeset 737 436019ca97d7
parent 733 5207fca25b6b
child 802 2f2fbf0a7e4f
permissions -rw-r--r--
cons_fun_eq: modified strange uses of classical reasoner
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
     1
(*  Title:      ZF/Datatype.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
120
09287f26bfb8 changed all co- and co_ to co
lcp
parents: 70
diff changeset
     6
(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory
0
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
(*For most datatypes involving univ*)
70
8a29f8b4aca1 ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents: 55
diff changeset
    11
val datatype_intrs = 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
    [SigmaI, InlI, InrI,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
     Pair_in_univ, Inl_in_univ, Inr_in_univ, 
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 0
diff changeset
    14
     zero_in_univ, A_into_univ, nat_into_univ, UnCI];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 0
diff changeset
    16
(*Needed for mutual recursion*)
70
8a29f8b4aca1 ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents: 55
diff changeset
    17
val datatype_elims = [make_elim InlD, make_elim InrD];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
120
09287f26bfb8 changed all co- and co_ to co
lcp
parents: 70
diff changeset
    19
(*For most codatatypes involving quniv*)
09287f26bfb8 changed all co- and co_ to co
lcp
parents: 70
diff changeset
    20
val codatatype_intrs = 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
    [QSigmaI, QInlI, QInrI,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
     QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 0
diff changeset
    23
     zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
120
09287f26bfb8 changed all co- and co_ to co
lcp
parents: 70
diff changeset
    25
val codatatype_elims = [make_elim QInlD, make_elim QInrD];
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 0
diff changeset
    26
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    27
signature INDUCTIVE_THMS =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    28
  sig
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    29
  val monos      : thm list		(*monotonicity of each M operator*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    30
  val type_intrs : thm list		(*type-checking intro rules*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    31
  val type_elims : thm list		(*type-checking elim rules*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    32
  end;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    33
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    34
functor Data_section_Fun
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    35
 (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    36
    : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    37
struct
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    38
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    39
structure Con = Constructor_Fun 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    40
 	(structure Const = Arg and Pr=Standard_Prod and Su=Standard_Sum);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    41
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    42
structure Inductive = Ind_section_Fun
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    43
   (open Arg; 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    44
    val con_defs = Con.con_defs
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    45
    val type_intrs = Arg.type_intrs @ datatype_intrs
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    46
    val type_elims = Arg.type_elims @ datatype_elims);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    47
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    48
open Inductive Con
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    49
end;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    50
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    51
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    52
functor CoData_section_Fun
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    53
 (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    54
    : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    55
struct
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    56
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    57
structure Con = Constructor_Fun 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    58
 	(structure Const = Arg and Pr=Quine_Prod and Su=Quine_Sum);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    59
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    60
structure CoInductive = CoInd_section_Fun
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    61
   (open Arg; 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    62
    val con_defs = Con.con_defs
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    63
    val type_intrs = Arg.type_intrs @ codatatype_intrs
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    64
    val type_elims = Arg.type_elims @ codatatype_elims);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    65
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    66
open CoInductive Con
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    67
end;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    68
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    69
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    70
(*For installing the theory section.   co is either "" or "Co"*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    71
fun datatype_decl co =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    72
  let open ThyParse Ind_Syntax
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    73
      (*generate strings*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    74
      fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    75
      val mk_data = mk_list o map mk_const o snd
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    76
      val mk_scons = mk_big_list o map mk_data
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    77
      fun mk_intr_name s =  (*the "op" cancels any infix status*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    78
	  if Syntax.is_identifier s then "op " ^ s ^ "_I" else "_"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    79
      fun mk_params ((((dom, rec_pairs), monos), type_intrs), type_elims) =
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    80
        let val rec_names = map (scan_to_id o trim o fst) rec_pairs
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    81
	    val big_rec_name = space_implode "_" rec_names
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    82
	    and srec_tms = mk_list (map fst rec_pairs)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    83
            and scons    = mk_scons rec_pairs
733
5207fca25b6b ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually
lcp
parents: 516
diff changeset
    84
            and sdom_sum = 
5207fca25b6b ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually
lcp
parents: 516
diff changeset
    85
		if dom = ""  then co ^ "data_domain rec_tms" (*default*)
5207fca25b6b ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually
lcp
parents: 516
diff changeset
    86
		else "readtm (sign_of thy) iT " ^ dom
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    87
            val stri_name = big_rec_name ^ "_Intrnl"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    88
            val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    89
        in
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    90
	   (";\n\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    91
            \structure " ^ stri_name ^ " =\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    92
            \ let open Ind_Syntax in\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    93
            \  struct\n\
733
5207fca25b6b ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually
lcp
parents: 516
diff changeset
    94
            \  val _ = writeln \"" ^ co ^ 
5207fca25b6b ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually
lcp
parents: 516
diff changeset
    95
	               "Datatype definition " ^ big_rec_name ^ "\"\n\
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    96
            \  val rec_tms\t= map (readtm (sign_of thy) iT) " ^ srec_tms ^ "\n\
733
5207fca25b6b ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually
lcp
parents: 516
diff changeset
    97
            \  val dom_sum\t= " ^ sdom_sum ^ "\n\
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    98
            \  and con_ty_lists\t= read_constructs (sign_of thy)\n" 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    99
	           ^ scons ^ "\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   100
            \  val intr_tms\t= mk_all_intr_tms (rec_tms, con_ty_lists)\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   101
            \  end\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   102
            \ end;\n\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   103
            \val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^ 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   104
	         mk_list (map quote rec_names) ^ ", " ^ 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   105
                 stri_name ^ ".con_ty_lists) \n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   106
            \              |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   107
	       stri_name ^ ".rec_tms, " ^
733
5207fca25b6b ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually
lcp
parents: 516
diff changeset
   108
               stri_name ^ ".dom_sum, " ^
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   109
               stri_name ^ ".intr_tms)"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   110
           ,
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   111
	    "structure " ^ big_rec_name ^ " =\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   112
            \  struct\n\
733
5207fca25b6b ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually
lcp
parents: 516
diff changeset
   113
            \  val _ = writeln \"Proofs for " ^ co ^ 
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   114
	               "Datatype definition " ^ big_rec_name ^ "\"\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   115
            \  structure Result = " ^ co ^ "Data_section_Fun\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   116
            \  (open " ^ stri_name ^ "\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   117
            \   val thy\t\t= thy\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   118
            \   val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   119
            \   val monos\t\t= " ^ monos ^ "\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   120
            \   val type_intrs\t= " ^ type_intrs ^ "\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   121
            \   val type_elims\t= " ^ type_elims ^ ");\n\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   122
            \  val " ^ mk_list (map mk_intr_name con_names) ^ " = Result.intrs;\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   123
            \  open Result\n\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   124
            \  end\n"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   125
	   )
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   126
	end
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   127
      fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   128
      val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   129
      val construct = name -- string_list -- opt_mixfix;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   130
  in optional ("<=" $$-- string) "" --
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   131
     enum1 "and" (string --$$ "=" -- enum1 "|" construct) --
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   132
     optstring "monos" -- optstring "type_intrs" -- optstring "type_elims"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   133
     >> mk_params
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
   134
end;