author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 1737  5a4f382455ce 
permissions  rwrr 
1461  1 
(* Title: ZF/Inductive.ML 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

4 
Copyright 1993 University of Cambridge 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

5 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

6 
(Co)Inductive Definitions for ZermeloFraenkel Set Theory 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

7 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

8 
Inductive definitions use least fixedpoints with standard products and sums 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

9 
Coinductive definitions use greatest fixedpoints with Quine products and sums 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

10 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

11 
Sums are used only for mutual recursion; 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

12 
Products are used only to derive "streamlined" induction rules for relations 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

13 
*) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

14 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

15 
val iT = Ind_Syntax.iT 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

16 
and oT = Ind_Syntax.oT; 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

17 

578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

18 
structure Lfp = 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

19 
struct 
1461  20 
val oper = Const("lfp", [iT,iT>iT]>iT) 
21 
val bnd_mono = Const("bnd_mono", [iT,iT>iT]>oT) 

22 
val bnd_monoI = bnd_monoI 

23 
val subs = def_lfp_subset 

24 
val Tarski = def_lfp_Tarski 

25 
val induct = def_induct 

578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

26 
end; 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

27 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

28 
structure Standard_Prod = 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

29 
struct 
1461  30 
val sigma = Const("Sigma", [iT, iT>iT]>iT) 
31 
val pair = Const("Pair", [iT,iT]>iT) 

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

33 
val fsplit_const = Const("split", [[iT,iT]>oT, iT]>oT) 

34 
val pair_iff = Pair_iff 

35 
val split_eq = split 

36 
val fsplitI = splitI 

37 
val fsplitD = splitD 

38 
val fsplitE = splitE 

578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

39 
end; 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

40 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

41 
structure Standard_Sum = 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

42 
struct 
1461  43 
val sum = Const("op +", [iT,iT]>iT) 
44 
val inl = Const("Inl", iT>iT) 

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

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

47 
val case_inl = case_Inl 

48 
val case_inr = case_Inr 

49 
val inl_iff = Inl_iff 

50 
val inr_iff = Inr_iff 

51 
val distinct = Inl_Inr_iff 

578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

52 
val distinct' = Inr_Inl_iff 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

53 
val free_SEs = Ind_Syntax.mk_free_SEs 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

54 
[distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff] 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

55 
end; 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

56 

578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

57 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

58 
functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

59 
: sig include INTR_ELIM INDRULE end = 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

60 
let 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

61 
structure Intr_elim = 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

62 
Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and 
1461  63 
Pr=Standard_Prod and Su=Standard_Sum); 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

64 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

65 
structure Indrule = 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

66 
Indrule_Fun (structure Inductive=Inductive and 
1461  67 
Pr=Standard_Prod and Su=Standard_Sum and 
68 
Intr_elim=Intr_elim) 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

69 
in 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

70 
struct 
1461  71 
val thy = Intr_elim.thy 
72 
val defs = Intr_elim.defs 

73 
val bnd_mono = Intr_elim.bnd_mono 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

74 
val dom_subset = Intr_elim.dom_subset 
1461  75 
val intrs = Intr_elim.intrs 
76 
val elim = Intr_elim.elim 

77 
val mk_cases = Intr_elim.mk_cases 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

78 
open Indrule 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

79 
end 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

80 
end; 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

81 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

82 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

83 
structure Ind = Add_inductive_def_Fun 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

84 
(structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum); 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

85 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

86 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

87 
structure Gfp = 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

88 
struct 
1461  89 
val oper = Const("gfp", [iT,iT>iT]>iT) 
90 
val bnd_mono = Const("bnd_mono", [iT,iT>iT]>oT) 

91 
val bnd_monoI = bnd_monoI 

92 
val subs = def_gfp_subset 

93 
val Tarski = def_gfp_Tarski 

94 
val induct = def_Collect_coinduct 

578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

95 
end; 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

96 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

97 
structure Quine_Prod = 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

98 
struct 
1461  99 
val sigma = Const("QSigma", [iT, iT>iT]>iT) 
100 
val pair = Const("QPair", [iT,iT]>iT) 

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

102 
val fsplit_const = Const("qsplit", [[iT,iT]>oT, iT]>oT) 

103 
val pair_iff = QPair_iff 

104 
val split_eq = qsplit 

105 
val fsplitI = qsplitI 

106 
val fsplitD = qsplitD 

107 
val fsplitE = qsplitE 

578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

108 
end; 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

109 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

110 
structure Quine_Sum = 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

111 
struct 
1461  112 
val sum = Const("op <+>", [iT,iT]>iT) 
113 
val inl = Const("QInl", iT>iT) 

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

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

116 
val case_inl = qcase_QInl 

117 
val case_inr = qcase_QInr 

118 
val inl_iff = QInl_iff 

119 
val inr_iff = QInr_iff 

120 
val distinct = QInl_QInr_iff 

578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

121 
val distinct' = QInr_QInl_iff 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

122 
val free_SEs = Ind_Syntax.mk_free_SEs 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

123 
[distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff] 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

124 
end; 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

125 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

126 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

127 
signature COINDRULE = 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

128 
sig 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

129 
val coinduct : thm 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

130 
end; 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

131 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

132 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

133 
functor CoInd_section_Fun 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

134 
(Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

135 
: sig include INTR_ELIM COINDRULE end = 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

136 
let 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

137 
structure Intr_elim = 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

138 
Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and 
1461  139 
Pr=Quine_Prod and Su=Quine_Sum); 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

140 
in 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

141 
struct 
1461  142 
val thy = Intr_elim.thy 
143 
val defs = Intr_elim.defs 

144 
val bnd_mono = Intr_elim.bnd_mono 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

145 
val dom_subset = Intr_elim.dom_subset 
1461  146 
val intrs = Intr_elim.intrs 
147 
val elim = Intr_elim.elim 

148 
val mk_cases = Intr_elim.mk_cases 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

149 
val coinduct = Intr_elim.raw_induct 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

150 
end 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

151 
end; 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

152 

efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

153 
structure CoInd = 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

154 
Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum); 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

155 