--- a/src/ZF/Inductive.ML Mon Jan 29 14:16:13 1996 +0100
+++ b/src/ZF/Inductive.ML Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Inductive.ML
+(* Title: ZF/Inductive.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory
@@ -17,38 +17,38 @@
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
+ 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
+ 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 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]
@@ -60,21 +60,21 @@
let
structure Intr_elim =
Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and
- Pr=Standard_Prod and Su=Standard_Sum);
+ 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)
+ 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 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 intrs = Intr_elim.intrs
+ val elim = Intr_elim.elim
+ val mk_cases = Intr_elim.mk_cases
open Indrule
end
end;
@@ -86,38 +86,38 @@
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
+ 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
+ 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 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]
@@ -136,16 +136,16 @@
let
structure Intr_elim =
Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and
- Pr=Quine_Prod and Su=Quine_Sum);
+ 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 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 intrs = Intr_elim.intrs
+ val elim = Intr_elim.elim
+ val mk_cases = Intr_elim.mk_cases
val coinduct = Intr_elim.raw_induct
end
end;