src/ZF/Inductive.ML

Improving space efficiency of inductive/datatype definitions.
Reduce usage of "open" and change struct open X; D end to
let open X in struct D end end whenever possible -- removes X from the final
structure. Especially needed for functors Intr_elim and Indrule.

intr_elim.ML and constructor.ML now use a common Su.free_SEs instead of
generating a new one. Inductive defs no longer export sumprod_free_SEs

ZF/intr_elim: Removed unfold:thm from signature INTR_ELIM.
It is never used outside, is easily recovered using
bnd_mono and def_lfp_Tarski, and takes up considerable store.

Moved raw_induct and rec_names to separate signature INTR_ELIM_AUX, for items
no longer exported.

mutual_induct is simply "True" unless it is going to be
significantly different from induct -- either because there is mutual
recursion or because it involves tuples.

(*  Title: 	ZF/Inductive.ML
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory

Inductive definitions use least fixedpoints with standard products and sums
Coinductive definitions use greatest fixedpoints with Quine products and sums

Sums are used only for mutual recursion;
Products are used only to derive "streamlined" induction rules for relations
*)

val iT = Ind_Syntax.iT
and oT = Ind_Syntax.oT;

structure Lfp =
  struct
  val oper	= Const("lfp",      [iT,iT-->iT]--->iT)
  val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
  val bnd_monoI	= bnd_monoI
  val subs	= def_lfp_subset
  val Tarski	= def_lfp_Tarski
  val induct	= def_induct
  end;

structure Standard_Prod =
  struct
  val sigma	= Const("Sigma", [iT, iT-->iT]--->iT)
  val pair	= Const("Pair", [iT,iT]--->iT)
  val split_const	= Const("split", [[iT,iT]--->iT, iT]--->iT)
  val fsplit_const	= Const("split", [[iT,iT]--->oT, iT]--->oT)
  val pair_iff	= Pair_iff
  val split_eq	= split
  val fsplitI	= splitI
  val fsplitD	= splitD
  val fsplitE	= splitE
  end;

structure Standard_Sum =
  struct
  val sum	= Const("op +", [iT,iT]--->iT)
  val inl	= Const("Inl", iT-->iT)
  val inr	= Const("Inr", iT-->iT)
  val elim	= Const("case", [iT-->iT, iT-->iT, iT]--->iT)
  val case_inl	= case_Inl
  val case_inr	= case_Inr
  val inl_iff	= Inl_iff
  val inr_iff	= Inr_iff
  val distinct	= Inl_Inr_iff
  val distinct' = Inr_Inl_iff
  val free_SEs  = Ind_Syntax.mk_free_SEs 
            [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
  end;


functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
  : sig include INTR_ELIM INDRULE end =
let
  structure Intr_elim = 
      Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and 
		    Pr=Standard_Prod and Su=Standard_Sum);

  structure Indrule = 
      Indrule_Fun (structure Inductive=Inductive and 
		   Pr=Standard_Prod and Su=Standard_Sum and 
		       Intr_elim=Intr_elim)
in 
   struct 
   val thy	= Intr_elim.thy
   val defs	= Intr_elim.defs
   val bnd_mono	= Intr_elim.bnd_mono
   val dom_subset = Intr_elim.dom_subset
   val intrs	= Intr_elim.intrs
   val elim	= Intr_elim.elim
   val mk_cases	= Intr_elim.mk_cases
   open Indrule 
   end
end;


structure Ind = Add_inductive_def_Fun
    (structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum);


structure Gfp =
  struct
  val oper	= Const("gfp",      [iT,iT-->iT]--->iT)
  val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
  val bnd_monoI	= bnd_monoI
  val subs	= def_gfp_subset
  val Tarski	= def_gfp_Tarski
  val induct	= def_Collect_coinduct
  end;

structure Quine_Prod =
  struct
  val sigma	= Const("QSigma", [iT, iT-->iT]--->iT)
  val pair	= Const("QPair", [iT,iT]--->iT)
  val split_const	= Const("qsplit", [[iT,iT]--->iT, iT]--->iT)
  val fsplit_const	= Const("qsplit", [[iT,iT]--->oT, iT]--->oT)
  val pair_iff	= QPair_iff
  val split_eq	= qsplit
  val fsplitI	= qsplitI
  val fsplitD	= qsplitD
  val fsplitE	= qsplitE
  end;

structure Quine_Sum =
  struct
  val sum	= Const("op <+>", [iT,iT]--->iT)
  val inl	= Const("QInl", iT-->iT)
  val inr	= Const("QInr", iT-->iT)
  val elim	= Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
  val case_inl	= qcase_QInl
  val case_inr	= qcase_QInr
  val inl_iff	= QInl_iff
  val inr_iff	= QInr_iff
  val distinct	= QInl_QInr_iff
  val distinct' = QInr_QInl_iff
  val free_SEs  = Ind_Syntax.mk_free_SEs 
            [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
  end;


signature COINDRULE =
  sig
  val coinduct : thm
  end;


functor CoInd_section_Fun
 (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
    : sig include INTR_ELIM COINDRULE end =
let
  structure Intr_elim = 
      Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and 
		    Pr=Quine_Prod and Su=Quine_Sum);
in
   struct
   val thy	= Intr_elim.thy
   val defs	= Intr_elim.defs
   val bnd_mono	= Intr_elim.bnd_mono
   val dom_subset = Intr_elim.dom_subset
   val intrs	= Intr_elim.intrs
   val elim	= Intr_elim.elim
   val mk_cases	= Intr_elim.mk_cases
   val coinduct = Intr_elim.raw_induct
   end
end;

structure CoInd = 
    Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum);