author  wenzelm 
Wed, 14 Sep 1994 16:05:39 +0200  
changeset 612  1ebe4d36dedc 
parent 591  5a6b0ed377cb 
child 727  711e4eb8c213 
permissions  rwrr 
516  1 
(* Title: ZF/add_ind_def.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1994 University of Cambridge 

5 

6 
Fixedpoint definition module  for Inductive/Coinductive Definitions 

7 

8 
Features: 

9 
* least or greatest fixedpoints 

10 
* userspecified product and sum constructions 

11 
* mutually recursive definitions 

12 
* definitions involving arbitrary monotone operators 

13 
* automatically proves introduction and elimination rules 

14 

15 
The recursive sets must *already* be declared as constants in parent theory! 

16 

17 
Introduction rules have the form 

18 
[ ti:M(Sj), ..., P(x), ... ] ==> t: Sk ] 

19 
where M is some monotone operator (usually the identity) 

20 
P(x) is any (nonconjunctive) side condition on the free variables 

21 
ti, t are any terms 

22 
Sj, Sk are two of the sets being defined in mutual recursion 

23 

24 
Sums are used only for mutual recursion; 

25 
Products are used only to derive "streamlined" induction rules for relations 

26 
*) 

27 

28 
signature FP = (** Description of a fixed point operator **) 

29 
sig 

30 
val oper : term (*fixed point operator*) 

31 
val bnd_mono : term (*monotonicity predicate*) 

32 
val bnd_monoI : thm (*intro rule for bnd_mono*) 

33 
val subs : thm (*subset theorem for fp*) 

34 
val Tarski : thm (*Tarski's fixed point theorem*) 

35 
val induct : thm (*induction/coinduction rule*) 

36 
end; 

37 

38 
signature PR = (** Description of a Cartesian product **) 

39 
sig 

40 
val sigma : term (*Cartesian product operator*) 

41 
val pair : term (*pairing operator*) 

42 
val split_const : term (*splitting operator*) 

43 
val fsplit_const : term (*splitting operator for formulae*) 

44 
val pair_iff : thm (*injectivity of pairing, using <>*) 

45 
val split_eq : thm (*equality rule for split*) 

46 
val fsplitI : thm (*intro rule for fsplit*) 

47 
val fsplitD : thm (*destruct rule for fsplit*) 

48 
val fsplitE : thm (*elim rule for fsplit*) 

49 
end; 

50 

51 
signature SU = (** Description of a disjoint sum **) 

52 
sig 

53 
val sum : term (*disjoint sum operator*) 

54 
val inl : term (*left injection*) 

55 
val inr : term (*right injection*) 

56 
val elim : term (*case operator*) 

57 
val case_inl : thm (*inl equality rule for case*) 

58 
val case_inr : thm (*inr equality rule for case*) 

59 
val inl_iff : thm (*injectivity of inl, using <>*) 

60 
val inr_iff : thm (*injectivity of inr, using <>*) 

61 
val distinct : thm (*distinctness of inl, inr using <>*) 

62 
val distinct' : thm (*distinctness of inr, inl using <>*) 

63 
end; 

64 

65 
signature ADD_INDUCTIVE_DEF = 

66 
sig 

67 
val add_fp_def_i : term list * term list * term list > theory > theory 

68 
val add_fp_def : (string*string) list * string list > theory > theory 

69 
val add_constructs_def : 

70 
string list * ((string*typ*mixfix) * 

71 
string * term list * term list) list list > 

72 
theory > theory 

73 
end; 

74 

75 

76 

77 
(*Declares functions to add fixedpoint/constructor defs to a theory*) 

78 
functor Add_inductive_def_Fun 

79 
(structure Fp: FP and Pr : PR and Su : SU) : ADD_INDUCTIVE_DEF = 

80 
struct 

81 
open Logic Ind_Syntax; 

82 

83 
(*internal version*) 

84 
fun add_fp_def_i (rec_tms, domts, intr_tms) thy = 

85 
let 

86 
val sign = sign_of thy; 

87 

88 
(*recT and rec_params should agree for all mutually recursive components*) 

89 
val (Const(_,recT),rec_params) = strip_comb (hd rec_tms) 

90 
and rec_hds = map head_of rec_tms; 

91 

92 
val rec_names = map (#1 o dest_Const) rec_hds; 

93 

94 
val _ = assert_all Syntax.is_identifier rec_names 

95 
(fn a => "Name of recursive set not an identifier: " ^ a); 

96 

612  97 
val _ = assert_all (is_some o Sign.const_type sign) rec_names 
516  98 
(fn a => "Recursive set not previously declared as constant: " ^ a); 
99 

100 
local (*Checking the introduction rules*) 

101 
val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; 

102 
fun intr_ok set = 

103 
case head_of set of Const(a,recT) => a mem rec_names  _ => false; 

104 
in 

105 
val _ = assert_all intr_ok intr_sets 

106 
(fn t => "Conclusion of rule does not name a recursive set: " ^ 

107 
Sign.string_of_term sign t); 

108 
end; 

109 

110 
val _ = assert_all is_Free rec_params 

111 
(fn t => "Param in recursion term not a free variable: " ^ 

112 
Sign.string_of_term sign t); 

113 

114 
(*** Construct the lfp definition ***) 

115 
val mk_variant = variant (foldr add_term_names (intr_tms,[])); 

116 

117 
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w"; 

118 

119 
fun dest_tprop (Const("Trueprop",_) $ P) = P 

120 
 dest_tprop Q = error ("Illformed premise of introduction rule: " ^ 

121 
Sign.string_of_term sign Q); 

122 

123 
(*Makes a disjunct from an introduction rule*) 

124 
fun lfp_part intr = (*quantify over rule's free vars except parameters*) 

125 
let val prems = map dest_tprop (strip_imp_prems intr) 

126 
val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds 

127 
val exfrees = term_frees intr \\ rec_params 

128 
val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr)) 

129 
in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end; 

130 

131 
val dom_sum = fold_bal (app Su.sum) domts; 

132 

133 
(*The Part(A,h) terms  compose injections to make h*) 

134 
fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*) 

135 
 mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h); 

136 

137 
(*Access to balanced disjoint sums via injections*) 

138 
val parts = 

139 
map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) 

140 
(length rec_tms)); 

141 

142 
(*replace each set by the corresponding Part(A,h)*) 

143 
val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms; 

144 

145 
val lfp_abs = absfree(X', iT, 

146 
mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs)); 

147 

148 
val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs 

149 

150 
val _ = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 

151 
"Illegal occurrence of recursion operator") 

152 
rec_hds; 

153 

154 
(*** Make the new theory ***) 

155 

156 
(*A key definition: 

157 
If no mutual recursion then it equals the one recursive set. 

158 
If mutual recursion then it differs from all the recursive sets. *) 

159 
val big_rec_name = space_implode "_" rec_names; 

160 

161 
(*Big_rec... is the union of the mutually recursive sets*) 

162 
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); 

163 

164 
(*The individual sets must already be declared*) 

165 
val axpairs = map mk_defpair 

166 
((big_rec_tm, lfp_rhs) :: 

167 
(case parts of 

168 
[_] => [] (*no mutual recursion*) 

169 
 _ => rec_tms ~~ (*define the sets as Parts*) 

170 
map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts)); 

171 

591
5a6b0ed377cb
ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal
lcp
parents:
567
diff
changeset

172 
val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs 
5a6b0ed377cb
ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal
lcp
parents:
567
diff
changeset

173 

567  174 
in thy > add_defs_i axpairs end 
516  175 

176 

177 
(*external, stringbased version; needed?*) 

178 
fun add_fp_def (rec_doms, sintrs) thy = 

179 
let val sign = sign_of thy; 

180 
val rec_tms = map (readtm sign iT o fst) rec_doms 

181 
and domts = map (readtm sign iT o snd) rec_doms 

182 
val intr_tms = map (readtm sign propT) sintrs 

183 
in add_fp_def_i (rec_tms, domts, intr_tms) thy end 

184 

185 

186 
(*Expects the recursive sets to have been defined already. 

187 
con_ty_lists specifies the constructors in the form (name,prems,mixfix) *) 

188 
fun add_constructs_def (rec_names, con_ty_lists) thy = 

189 
let 

190 
val _ = writeln" Defining the constructor functions..."; 

191 
val case_name = "f"; (*name for case variables*) 

192 

193 
(** Define the constructors **) 

194 

195 
(*The empty tuple is 0*) 

196 
fun mk_tuple [] = Const("0",iT) 

197 
 mk_tuple args = foldr1 (app Pr.pair) args; 

198 

199 
fun mk_inject n k u = access_bal(ap Su.inl, ap Su.inr, u) n k; 

200 

201 
val npart = length rec_names; (*total # of mutually recursive parts*) 

202 

203 
(*Make constructor definition; kpart is # of this mutually recursive part*) 

204 
fun mk_con_defs (kpart, con_ty_list) = 

205 
let val ncon = length con_ty_list (*number of constructors*) 

206 
fun mk_def (((id,T,syn), name, args, prems), kcon) = 

207 
(*kcon is index of constructor*) 

208 
mk_defpair (list_comb (Const(name,T), args), 

209 
mk_inject npart kpart 

210 
(mk_inject ncon kcon (mk_tuple args))) 

211 
in map mk_def (con_ty_list ~~ (1 upto ncon)) end; 

212 

213 
(** Define the case operator **) 

214 

215 
(*Combine split terms using case; yields the case operator for one part*) 

216 
fun call_case case_list = 

217 
let fun call_f (free,args) = 

218 
ap_split Pr.split_const free (map (#2 o dest_Free) args) 

219 
in fold_bal (app Su.elim) (map call_f case_list) end; 

220 

221 
(** Generating function variables for the case definition 

222 
Nonidentifiers (e.g. infixes) get a name of the form f_op_nnn. **) 

223 

224 
(*Treatment of a single constructor*) 

225 
fun add_case (((id,T,syn), name, args, prems), (opno,cases)) = 

226 
if Syntax.is_identifier id 

227 
then (opno, 

228 
(Free(case_name ^ "_" ^ id, T), args) :: cases) 

229 
else (opno+1, 

230 
(Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: 

231 
cases) 

232 

233 
(*Treatment of a list of constructors, for one part*) 

234 
fun add_case_list (con_ty_list, (opno,case_lists)) = 

235 
let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[])) 

236 
in (opno', case_list :: case_lists) end; 

237 

238 
(*Treatment of all parts*) 

239 
val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[])); 

240 

241 
val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) > (iT>iT); 

242 

243 
val big_rec_name = space_implode "_" rec_names; 

244 

245 
val big_case_name = big_rec_name ^ "_case"; 

246 

247 
(*The list of all the function variables*) 

248 
val big_case_args = flat (map (map #1) case_lists); 

249 

250 
val big_case_tm = 

251 
list_comb (Const(big_case_name, big_case_typ), big_case_args); 

252 

253 
val big_case_def = mk_defpair 

254 
(big_case_tm, fold_bal (app Su.elim) (map call_case case_lists)); 

255 

256 
(** Build the new theory **) 

257 

258 
val const_decs = 

259 
(big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists); 

260 

261 
val axpairs = 

262 
big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists)) 

263 

567  264 
in thy > add_consts_i const_decs > add_defs_i axpairs end; 
516  265 
end; 