src/ZF/inductive.ML
changeset 516 1957113f0d7d
parent 0 a5a9c433f639
equal deleted inserted replaced
515:abcc438e7c27 516:1957113f0d7d
     1 (*  Title: 	ZF/inductive.ML
     1 (*  Title: 	ZF/inductive.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     4     Copyright   1993  University of Cambridge
     5 
     5 
     6 Inductive Definitions for Zermelo-Fraenkel Set Theory
     6 (Co)Inductive Definitions for Zermelo-Fraenkel Set Theory
     7 
     7 
     8 Uses least fixedpoints with standard products and sums
     8 Inductive definitions use least fixedpoints with standard products and sums
       
     9 Coinductive definitions use greatest fixedpoints with Quine products and sums
     9 
    10 
    10 Sums are used only for mutual recursion;
    11 Sums are used only for mutual recursion;
    11 Products are used only to derive "streamlined" induction rules for relations
    12 Products are used only to derive "streamlined" induction rules for relations
    12 *)
    13 *)
    13 
    14 
    14 
    15 local open Ind_Syntax
       
    16 in
    15 structure Lfp =
    17 structure Lfp =
    16   struct
    18   struct
    17   val oper	= Const("lfp",      [iT,iT-->iT]--->iT)
    19   val oper	= Const("lfp",      [iT,iT-->iT]--->iT)
    18   val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
    20   val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
    19   val bnd_monoI	= bnd_monoI
    21   val bnd_monoI	= bnd_monoI
    46   val inl_iff	= Inl_iff
    48   val inl_iff	= Inl_iff
    47   val inr_iff	= Inr_iff
    49   val inr_iff	= Inr_iff
    48   val distinct	= Inl_Inr_iff
    50   val distinct	= Inl_Inr_iff
    49   val distinct' = Inr_Inl_iff
    51   val distinct' = Inr_Inl_iff
    50   end;
    52   end;
    51 
    53 end;
    52 functor Inductive_Fun (Ind: INDUCTIVE) : sig include INTR_ELIM INDRULE end =
    54 
       
    55 functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
       
    56   : sig include INTR_ELIM INDRULE end =
    53 struct
    57 struct
    54 structure Intr_elim = 
    58 structure Intr_elim = 
    55     Intr_elim_Fun(structure Ind=Ind and Fp=Lfp and 
    59     Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and 
    56 		  Pr=Standard_Prod and Su=Standard_Sum);
    60 		  Pr=Standard_Prod and Su=Standard_Sum);
    57 
    61 
    58 structure Indrule = Indrule_Fun (structure Ind=Ind and 
    62 structure Indrule = Indrule_Fun (structure Inductive=Inductive and 
    59 		                 Pr=Standard_Prod and Intr_elim=Intr_elim);
    63 		                 Pr=Standard_Prod and Intr_elim=Intr_elim);
    60 
    64 
    61 open Intr_elim Indrule
    65 open Intr_elim Indrule
    62 end;
    66 end;
    63 
    67 
       
    68 
       
    69 structure Ind = Add_inductive_def_Fun
       
    70     (structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum);
       
    71 
       
    72 
       
    73 signature INDUCTIVE_STRING =
       
    74   sig
       
    75   val thy_name   : string 		(*name of the new theory*)
       
    76   val rec_doms   : (string*string) list	(*recursion terms and their domains*)
       
    77   val sintrs     : string list		(*desired introduction rules*)
       
    78   end;
       
    79 
       
    80 
       
    81 (*For upwards compatibility: can be called directly from ML*)
       
    82 functor Inductive_Fun
       
    83  (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
       
    84    : sig include INTR_ELIM INDRULE end =
       
    85 Ind_section_Fun
       
    86    (open Inductive Ind_Syntax
       
    87     val sign = sign_of thy;
       
    88     val rec_tms = map (readtm sign iT o #1) rec_doms
       
    89     and domts   = map (readtm sign iT o #2) rec_doms
       
    90     and intr_tms = map (readtm sign propT) sintrs;
       
    91     val thy = thy |> Ind.add_fp_def_i(rec_tms, domts, intr_tms) 
       
    92                   |> add_thyname thy_name);
       
    93 
       
    94 
       
    95 
       
    96 local open Ind_Syntax
       
    97 in
       
    98 structure Gfp =
       
    99   struct
       
   100   val oper	= Const("gfp",      [iT,iT-->iT]--->iT)
       
   101   val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
       
   102   val bnd_monoI	= bnd_monoI
       
   103   val subs	= def_gfp_subset
       
   104   val Tarski	= def_gfp_Tarski
       
   105   val induct	= def_Collect_coinduct
       
   106   end;
       
   107 
       
   108 structure Quine_Prod =
       
   109   struct
       
   110   val sigma	= Const("QSigma", [iT, iT-->iT]--->iT)
       
   111   val pair	= Const("QPair", [iT,iT]--->iT)
       
   112   val split_const	= Const("qsplit", [[iT,iT]--->iT, iT]--->iT)
       
   113   val fsplit_const	= Const("qfsplit", [[iT,iT]--->oT, iT]--->oT)
       
   114   val pair_iff	= QPair_iff
       
   115   val split_eq	= qsplit
       
   116   val fsplitI	= qfsplitI
       
   117   val fsplitD	= qfsplitD
       
   118   val fsplitE	= qfsplitE
       
   119   end;
       
   120 
       
   121 structure Quine_Sum =
       
   122   struct
       
   123   val sum	= Const("op <+>", [iT,iT]--->iT)
       
   124   val inl	= Const("QInl", iT-->iT)
       
   125   val inr	= Const("QInr", iT-->iT)
       
   126   val elim	= Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
       
   127   val case_inl	= qcase_QInl
       
   128   val case_inr	= qcase_QInr
       
   129   val inl_iff	= QInl_iff
       
   130   val inr_iff	= QInr_iff
       
   131   val distinct	= QInl_QInr_iff
       
   132   val distinct' = QInr_QInl_iff
       
   133   end;
       
   134 end;
       
   135 
       
   136 
       
   137 signature COINDRULE =
       
   138   sig
       
   139   val coinduct : thm
       
   140   end;
       
   141 
       
   142 
       
   143 functor CoInd_section_Fun
       
   144  (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
       
   145     : sig include INTR_ELIM COINDRULE end =
       
   146 struct
       
   147 structure Intr_elim = 
       
   148     Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and 
       
   149 		  Pr=Quine_Prod and Su=Quine_Sum);
       
   150 
       
   151 open Intr_elim 
       
   152 val coinduct = raw_induct
       
   153 end;
       
   154 
       
   155 
       
   156 structure CoInd = 
       
   157     Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum);
       
   158 
       
   159 
       
   160 (*For upwards compatibility: can be called directly from ML*)
       
   161 functor CoInductive_Fun
       
   162  (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
       
   163    : sig include INTR_ELIM COINDRULE end =
       
   164 CoInd_section_Fun
       
   165    (open Inductive Ind_Syntax
       
   166     val sign = sign_of thy;
       
   167     val rec_tms = map (readtm sign iT o #1) rec_doms
       
   168     and domts   = map (readtm sign iT o #2) rec_doms
       
   169     and intr_tms = map (readtm sign propT) sintrs;
       
   170     val thy = thy |> CoInd.add_fp_def_i(rec_tms, domts, intr_tms) 
       
   171                   |> add_thyname thy_name);
       
   172 
       
   173 
       
   174 
       
   175 (*For installing the theory section.   co is either "" or "Co"*)
       
   176 fun inductive_decl co =
       
   177   let open ThyParse Ind_Syntax
       
   178       fun mk_intr_name (s,_) =  (*the "op" cancels any infix status*)
       
   179 	  if Syntax.is_identifier s then "op " ^ s  else "_"
       
   180       fun mk_params (((((domains: (string*string) list, ipairs), 
       
   181 			monos), con_defs), type_intrs), type_elims) =
       
   182         let val big_rec_name = space_implode "_" 
       
   183 		             (map (scan_to_id o trim o #1) domains)
       
   184 	    and srec_tms = mk_list (map #1 domains)
       
   185             and sdoms    = mk_list (map #2 domains)
       
   186 	    and sintrs   = mk_big_list (map snd ipairs)
       
   187             val stri_name = big_rec_name ^ "_Intrnl"
       
   188         in
       
   189 	   (";\n\n\
       
   190             \structure " ^ stri_name ^ " =\n\
       
   191             \ let open Ind_Syntax in\n\
       
   192             \  struct\n\
       
   193             \  val rec_tms\t= map (readtm (sign_of thy) iT) "
       
   194 	                     ^ srec_tms ^ "\n\
       
   195             \  and domts\t= map (readtm (sign_of thy) iT) "
       
   196 	                     ^ sdoms ^ "\n\
       
   197             \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
       
   198 	                     ^ sintrs ^ "\n\
       
   199             \  end\n\
       
   200             \ end;\n\n\
       
   201             \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
       
   202 	       stri_name ^ ".rec_tms, " ^
       
   203                stri_name ^ ".domts, " ^
       
   204                stri_name ^ ".intr_tms)"
       
   205            ,
       
   206 	    "structure " ^ big_rec_name ^ " =\n\
       
   207             \  struct\n\
       
   208             \  val _ = writeln \"" ^ co ^ 
       
   209 	               "Inductive definition " ^ big_rec_name ^ "\"\n\
       
   210             \  structure Result = " ^ co ^ "Ind_section_Fun\n\
       
   211             \  (open " ^ stri_name ^ "\n\
       
   212             \   val thy\t\t= thy\n\
       
   213             \   val monos\t\t= " ^ monos ^ "\n\
       
   214             \   val con_defs\t\t= " ^ con_defs ^ "\n\
       
   215             \   val type_intrs\t= " ^ type_intrs ^ "\n\
       
   216             \   val type_elims\t= " ^ type_elims ^ ");\n\n\
       
   217             \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
       
   218             \  open Result\n\
       
   219             \  end\n"
       
   220 	   )
       
   221 	end
       
   222       val domains = "domains" $$-- repeat1 (string --$$ "<=" -- !! string)
       
   223       val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
       
   224       fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
       
   225   in domains -- ipairs -- optstring "monos" -- optstring "con_defs"
       
   226              -- optstring "type_intrs" -- optstring "type_elims"
       
   227      >> mk_params
       
   228   end;