0

1 
(* Title: ZF/coinductive.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Coinductive Definitions for ZermeloFraenkel Set Theory


7 


8 
Uses greatest fixedpoints with Quineinspired 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 
structure Gfp =


15 
struct


16 
val oper = Const("gfp", [iT,iT>iT]>iT)


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


18 
val bnd_monoI = bnd_monoI


19 
val subs = def_gfp_subset


20 
val Tarski = def_gfp_Tarski


21 
val induct = def_Collect_coinduct


22 
end;


23 


24 
structure Quine_Prod =


25 
struct


26 
val sigma = Const("QSigma", [iT, iT>iT]>iT)


27 
val pair = Const("QPair", [iT,iT]>iT)


28 
val split_const = Const("qsplit", [[iT,iT]>iT, iT]>iT)


29 
val fsplit_const = Const("qfsplit", [[iT,iT]>oT, iT]>oT)


30 
val pair_iff = QPair_iff


31 
val split_eq = qsplit


32 
val fsplitI = qfsplitI


33 
val fsplitD = qfsplitD


34 
val fsplitE = qfsplitE


35 
end;


36 


37 
structure Quine_Sum =


38 
struct


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


40 
val inl = Const("QInl", iT>iT)


41 
val inr = Const("QInr", iT>iT)


42 
val elim = Const("qcase", [iT>iT, iT>iT, iT]>iT)


43 
val case_inl = qcase_QInl


44 
val case_inr = qcase_QInr


45 
val inl_iff = QInl_iff


46 
val inr_iff = QInr_iff


47 
val distinct = QInl_QInr_iff


48 
val distinct' = QInr_QInl_iff


49 
end;


50 


51 
signature CO_INDRULE =


52 
sig


53 
val co_induct : thm


54 
end;


55 


56 


57 
functor Co_Inductive_Fun (Ind: INDUCTIVE)


58 
: sig include INTR_ELIM CO_INDRULE end =


59 
struct


60 
structure Intr_elim =


61 
Intr_elim_Fun(structure Ind=Ind and Fp=Gfp and


62 
Pr=Quine_Prod and Su=Quine_Sum);


63 


64 
open Intr_elim


65 
val co_induct = raw_induct


66 
end;


67 
