author  lcp 
Thu, 25 Aug 1994 12:09:21 +0200  
changeset 578  efc648d29dd0 
child 734  a3e0fd3c0f2f 
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 

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

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

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

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

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

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

20 
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

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

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

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

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

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

26 

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

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

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

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

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

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

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

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

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

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

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

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

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

39 

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

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

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

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

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

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

45 
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

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

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

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

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

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

51 
val distinct' = Inr_Inl_iff 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

54 

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

55 
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

56 
: sig include INTR_ELIM INDRULE end = 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

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

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

61 

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

62 
structure Indrule = Indrule_Fun (structure Inductive=Inductive and 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

63 
Pr=Standard_Prod and Intr_elim=Intr_elim); 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

64 

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

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

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

67 

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

68 

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

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

70 
(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

71 

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

72 

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

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

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

75 
val thy_name : string (*name of the new theory*) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

76 
val rec_doms : (string*string) list (*recursion terms and their domains*) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

77 
val sintrs : string list (*desired introduction rules*) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

79 

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

80 

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

81 
(*For upwards compatibility: can be called directly from ML*) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

84 
: sig include INTR_ELIM INDRULE end = 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

87 
val sign = sign_of thy; 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

88 
val rec_tms = map (readtm sign iT o #1) rec_doms 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

89 
and domts = map (readtm sign iT o #2) rec_doms 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

90 
and intr_tms = map (readtm sign propT) sintrs; 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

91 
val thy = thy > Ind.add_fp_def_i(rec_tms, domts, intr_tms) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

92 
> add_thyname thy_name); 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

93 

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

94 

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

95 

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

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

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

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

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

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

101 
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

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

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

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

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

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

107 

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

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

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

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

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

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

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

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

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

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

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

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

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

120 

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

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

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

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

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

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

126 
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

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

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

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

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

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

132 
val distinct' = QInr_QInl_iff 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

135 

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

136 

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

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

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

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

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

141 

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

142 

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

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

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

145 
: sig include INTR_ELIM COINDRULE end = 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

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

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

150 

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

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

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

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

154 

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

155 

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

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

157 
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

158 

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

159 

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

160 
(*For upwards compatibility: can be called directly from ML*) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

163 
: sig include INTR_ELIM COINDRULE end = 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

166 
val sign = sign_of thy; 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

167 
val rec_tms = map (readtm sign iT o #1) rec_doms 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

168 
and domts = map (readtm sign iT o #2) rec_doms 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

169 
and intr_tms = map (readtm sign propT) sintrs; 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

170 
val thy = thy > CoInd.add_fp_def_i(rec_tms, domts, intr_tms) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

171 
> add_thyname thy_name); 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

172 

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

173 

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

174 

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

175 
(*For installing the theory section. co is either "" or "Co"*) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

178 
fun mk_intr_name (s,_) = (*the "op" cancels any infix status*) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

179 
if Syntax.is_identifier s then "op " ^ s else "_" 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

180 
fun mk_params (((((domains: (string*string) list, ipairs), 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

181 
monos), con_defs), type_intrs), type_elims) = 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

182 
let val big_rec_name = space_implode "_" 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

183 
(map (scan_to_id o trim o #1) domains) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

184 
and srec_tms = mk_list (map #1 domains) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

185 
and sdoms = mk_list (map #2 domains) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

186 
and sintrs = mk_big_list (map snd ipairs) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

187 
val stri_name = big_rec_name ^ "_Intrnl" 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

190 
\structure " ^ stri_name ^ " =\n\ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

191 
\ let open Ind_Syntax in\n\ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

193 
\ val _ = writeln \"" ^ co ^ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

194 
"Inductive definition " ^ big_rec_name ^ "\"\n\ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

195 
\ val rec_tms\t= map (readtm (sign_of thy) iT) " 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

197 
\ and domts\t= map (readtm (sign_of thy) iT) " 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

199 
\ and intr_tms\t= map (readtm (sign_of thy) propT)\n" 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

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

203 
\val thy = thy > " ^ co ^ "Ind.add_fp_def_i \n (" ^ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

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

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

208 
"structure " ^ big_rec_name ^ " =\n\ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

210 
\ structure Result = " ^ co ^ "Ind_section_Fun\n\ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

211 
\ (open " ^ stri_name ^ "\n\ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

212 
\ val thy\t\t= thy\n\ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

213 
\ val monos\t\t= " ^ monos ^ "\n\ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

214 
\ val con_defs\t\t= " ^ con_defs ^ "\n\ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

215 
\ val type_intrs\t= " ^ type_intrs ^ "\n\ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

216 
\ val type_elims\t= " ^ type_elims ^ ");\n\n\ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

217 
\ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\ 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

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

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

222 
val domains = "domains" $$ repeat1 (string $$ "<="  !! string) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

223 
val ipairs = "intrs" $$ repeat1 (ident  !! string) 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

224 
fun optstring s = optional (s $$ string) "\"[]\"" >> trim 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

225 
in domains  ipairs  optstring "monos"  optstring "con_defs" 
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
diff
changeset

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

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

228 
end; 