author  paulson 
Fri, 22 Dec 1995 11:09:28 +0100  
changeset 1418  f5f97ee67cbb 
parent 1093  c2b3b7b7a69f 
child 1461  6bcb44e4d6e5 
permissions  rwrr 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
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 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

20 
val oper = Const("lfp", [iT,iT>iT]>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

21 
val bnd_mono = Const("bnd_mono", [iT,iT>iT]>oT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

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

25 
val induct = def_induct 
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 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

30 
val sigma = Const("Sigma", [iT, iT>iT]>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

31 
val pair = Const("Pair", [iT,iT]>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

32 
val split_const = Const("split", [[iT,iT]>iT, iT]>iT) 
1093
c2b3b7b7a69f
Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents:
802
diff
changeset

33 
val fsplit_const = Const("split", [[iT,iT]>oT, iT]>oT) 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

35 
val split_eq = split 
1093
c2b3b7b7a69f
Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents:
802
diff
changeset

36 
val fsplitI = splitI 
c2b3b7b7a69f
Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents:
802
diff
changeset

37 
val fsplitD = splitD 
c2b3b7b7a69f
Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents:
802
diff
changeset

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 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

43 
val sum = Const("op +", [iT,iT]>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

44 
val inl = Const("Inl", iT>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

45 
val inr = Const("Inr", iT>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

46 
val elim = Const("case", [iT>iT, iT>iT, iT]>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

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

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

51 
val distinct = Inl_Inr_iff 
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 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

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 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

67 
Pr=Standard_Prod and Su=Standard_Sum and 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

68 
Intr_elim=Intr_elim) 
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 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

71 
val thy = Intr_elim.thy 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

72 
val defs = Intr_elim.defs 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

73 
val bnd_mono = Intr_elim.bnd_mono 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

74 
val dom_subset = Intr_elim.dom_subset 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

75 
val intrs = Intr_elim.intrs 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

76 
val elim = Intr_elim.elim 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

77 
val mk_cases = Intr_elim.mk_cases 
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 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

89 
val oper = Const("gfp", [iT,iT>iT]>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

90 
val bnd_mono = Const("bnd_mono", [iT,iT>iT]>oT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

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

94 
val induct = def_Collect_coinduct 
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 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

99 
val sigma = Const("QSigma", [iT, iT>iT]>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

100 
val pair = Const("QPair", [iT,iT]>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

101 
val split_const = Const("qsplit", [[iT,iT]>iT, iT]>iT) 
1093
c2b3b7b7a69f
Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents:
802
diff
changeset

102 
val fsplit_const = Const("qsplit", [[iT,iT]>oT, iT]>oT) 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

104 
val split_eq = qsplit 
1093
c2b3b7b7a69f
Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents:
802
diff
changeset

105 
val fsplitI = qsplitI 
c2b3b7b7a69f
Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents:
802
diff
changeset

106 
val fsplitD = qsplitD 
c2b3b7b7a69f
Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents:
802
diff
changeset

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 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

112 
val sum = Const("op <+>", [iT,iT]>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

113 
val inl = Const("QInl", iT>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

114 
val inr = Const("QInr", iT>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

115 
val elim = Const("qcase", [iT>iT, iT>iT, iT]>iT) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

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

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

120 
val distinct = QInl_QInr_iff 
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 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

139 
Pr=Quine_Prod and Su=Quine_Sum); 
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 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

142 
val thy = Intr_elim.thy 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

143 
val defs = Intr_elim.defs 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

144 
val bnd_mono = Intr_elim.bnd_mono 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

145 
val dom_subset = Intr_elim.dom_subset 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

146 
val intrs = Intr_elim.intrs 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

147 
val elim = Intr_elim.elim 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1093
diff
changeset

148 
val mk_cases = Intr_elim.mk_cases 
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 