0

1 
(* Title: ZF/inductive.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Inductive Definitions for ZermeloFraenkel Set Theory


7 


8 
Uses least fixedpoints with standard products and sums


9 


10 
Sums are used only for mutual recursion;


11 
Products are used only to derive "streamlined" induction rules for relations


12 
*)


13 


14 


15 
structure Lfp =


16 
struct


17 
val oper = Const("lfp", [iT,iT>iT]>iT)


18 
val bnd_mono = Const("bnd_mono", [iT,iT>iT]>oT)


19 
val bnd_monoI = bnd_monoI


20 
val subs = def_lfp_subset


21 
val Tarski = def_lfp_Tarski


22 
val induct = def_induct


23 
end;


24 


25 
structure Standard_Prod =


26 
struct


27 
val sigma = Const("Sigma", [iT, iT>iT]>iT)


28 
val pair = Const("Pair", [iT,iT]>iT)


29 
val split_const = Const("split", [[iT,iT]>iT, iT]>iT)


30 
val fsplit_const = Const("fsplit", [[iT,iT]>oT, iT]>oT)


31 
val pair_iff = Pair_iff


32 
val split_eq = split


33 
val fsplitI = fsplitI


34 
val fsplitD = fsplitD


35 
val fsplitE = fsplitE


36 
end;


37 


38 
structure Standard_Sum =


39 
struct


40 
val sum = Const("op +", [iT,iT]>iT)


41 
val inl = Const("Inl", iT>iT)


42 
val inr = Const("Inr", iT>iT)


43 
val elim = Const("case", [iT>iT, iT>iT, iT]>iT)


44 
val case_inl = case_Inl


45 
val case_inr = case_Inr


46 
val inl_iff = Inl_iff


47 
val inr_iff = Inr_iff


48 
val distinct = Inl_Inr_iff


49 
val distinct' = Inr_Inl_iff


50 
end;


51 


52 
functor Inductive_Fun (Ind: INDUCTIVE) : sig include INTR_ELIM INDRULE end =


53 
struct


54 
structure Intr_elim =


55 
Intr_elim_Fun(structure Ind=Ind and Fp=Lfp and


56 
Pr=Standard_Prod and Su=Standard_Sum);


57 


58 
structure Indrule = Indrule_Fun (structure Ind=Ind and


59 
Pr=Standard_Prod and Intr_elim=Intr_elim);


60 


61 
open Intr_elim Indrule


62 
end;


63 
