author  lcp 
Fri, 22 Oct 1993 11:34:41 +0100  
changeset 70  8a29f8b4aca1 
parent 55  331d93292ee0 
permissions  rwrr 
0  1 
(* Title: ZF/intrelim.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
Introduction/elimination rule 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 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

22 
Sj, Sk are two of the sets being defined in mutual recursion 
0  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 INDUCTIVE = (** Description of a (co)inductive defn **) 

66 
sig 

67 
val thy : theory (*parent theory*) 

68 
val rec_doms : (string*string) list (*recursion ops and their domains*) 

69 
val sintrs : string list (*desired introduction rules*) 

70 
val monos : thm list (*monotonicity of each M operator*) 

71 
val con_defs : thm list (*definitions of the constructors*) 

72 
val type_intrs : thm list (*typechecking intro rules*) 

73 
val type_elims : thm list (*typechecking elim rules*) 

74 
end; 

75 

76 
signature INTR_ELIM = 

77 
sig 

78 
val thy : theory (*new theory*) 

79 
val defs : thm list (*definitions made in thy*) 

80 
val bnd_mono : thm (*monotonicity for the lfp definition*) 

81 
val unfold : thm (*fixedpoint equation*) 

82 
val dom_subset : thm (*inclusion of recursive set in dom*) 

83 
val intrs : thm list (*introduction rules*) 

84 
val elim : thm (*case analysis theorem*) 

85 
val raw_induct : thm (*raw induction rule from Fp.induct*) 

86 
val mk_cases : thm list > string > thm (*generates case theorems*) 

87 
(*internal items...*) 

88 
val big_rec_tm : term (*the lhs of the fixedpoint defn*) 

89 
val rec_tms : term list (*the mutually recursive sets*) 

90 
val domts : term list (*domains of the recursive sets*) 

91 
val intr_tms : term list (*terms for the introduction rules*) 

92 
val rec_params : term list (*parameters of the recursion*) 

93 
val sumprod_free_SEs : thm list (*destruct rules for Su and Pr*) 

94 
end; 

95 

96 

97 
functor Intr_elim_Fun (structure Ind: INDUCTIVE and 

98 
Fp: FP and Pr : PR and Su : SU) : INTR_ELIM = 

99 
struct 

100 
open Logic Ind; 

101 

102 
(*** Extract basic information from arguments ***) 

103 

104 
val sign = sign_of Ind.thy; 

105 

106 
fun rd T a = 

107 
Sign.read_cterm sign (a,T) 

108 
handle ERROR => error ("The error above occurred for " ^ a); 

109 

110 
val rec_names = map #1 rec_doms 

111 
and domts = map (Sign.term_of o rd iT o #2) rec_doms; 

112 

113 
val dummy = assert_all Syntax.is_identifier rec_names 

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

115 

116 
val dummy = assert_all (is_some o lookup_const sign) rec_names 

117 
(fn a => "Name of recursive set not declared as constant: " ^ a); 

118 

119 
val intr_tms = map (Sign.term_of o rd propT) sintrs; 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

120 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

121 
local (*Checking the introduction rules*) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

122 
val intr_sets = map (#2 o rule_concl) intr_tms; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

123 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

124 
fun intr_ok set = 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

125 
case head_of set of Const(a,recT) => a mem rec_names  _ => false; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

126 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

127 
val dummy = assert_all intr_ok intr_sets 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

128 
(fn t => "Conclusion of rule does not name a recursive set: " ^ 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

129 
Sign.string_of_term sign t); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

130 
in 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

131 
val (Const(_,recT),rec_params) = strip_comb (hd intr_sets) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

132 
end; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

133 

0  134 
val rec_hds = map (fn a=> Const(a,recT)) rec_names; 
135 
val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds; 

136 

137 
val dummy = assert_all is_Free rec_params 

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

139 
Sign.string_of_term sign t); 

140 

141 
(*** Construct the lfp definition ***) 

142 

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

144 

145 
val z' = mk_variant"z" 

146 
and X' = mk_variant"X" 

147 
and w' = mk_variant"w"; 

148 

149 
(*simple errorchecking in the premises*) 

150 
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) = 

151 
error"Premises may not be conjuctive" 

152 
 chk_prem rec_hd (Const("op :",_) $ t $ X) = 

153 
deny (rec_hd occs t) "Recursion term on left of member symbol" 

154 
 chk_prem rec_hd t = 

155 
deny (rec_hd occs t) "Recursion term in side formula"; 

156 

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

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

159 
let val prems = map dest_tprop (strip_imp_prems intr) 

160 
val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds 

161 
val exfrees = term_frees intr \\ rec_params 

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

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

164 

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

166 

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

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

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

170 

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

172 
val parts = 

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

174 
(length rec_doms)); 

175 

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

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

178 

179 
val lfp_abs = absfree(X', iT, 

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

181 

182 
val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs 

183 

184 
val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 

185 
"Illegal occurrence of recursion operator") 

186 
rec_hds; 

187 

188 
(*** Make the new theory ***) 

189 

190 
(*A key definition: 

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

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

193 
val big_rec_name = space_implode "_" rec_names; 

194 

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

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

197 

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

199 
val axpairs = map (mk_defpair sign) 

200 
((big_rec_tm, lfp_rhs) :: 

201 
(case parts of 

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

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

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

205 

206 
val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive") 

207 
([], [], [], [], [], None) axpairs; 

208 

209 
val defs = map (get_axiom thy o #1) axpairs; 

210 

211 
val big_rec_def::part_rec_defs = defs; 

212 

213 
val prove = prove_term (sign_of thy); 

214 

215 
(********) 

216 
val dummy = writeln "Proving monotonocity..."; 

217 

218 
val bnd_mono = 

219 
prove [] (mk_tprop (Fp.bnd_mono $ dom_sum $ lfp_abs), 

220 
fn _ => 

221 
[rtac (Collect_subset RS bnd_monoI) 1, 

222 
REPEAT (ares_tac (basic_monos @ monos) 1)]); 

223 

224 
val dom_subset = standard (big_rec_def RS Fp.subs); 

225 

226 
val unfold = standard (bnd_mono RS (big_rec_def RS Fp.Tarski)); 

227 

228 
(********) 

229 
val dummy = writeln "Proving the introduction rules..."; 

230 

231 
(*Mutual recursion: Needs subset rules for the individual sets???*) 

232 
val rec_typechecks = [dom_subset] RL (asm_rl::monos) RL [subsetD]; 

233 

234 
(*Typechecking is hardest aspect of proof; 

235 
disjIn selects the correct disjunct after unfolding*) 

236 
fun intro_tacsf disjIn prems = 

237 
[(*insert prems and underlying sets*) 

55  238 
cut_facts_tac prems 1, 
0  239 
rtac (unfold RS ssubst) 1, 
240 
REPEAT (resolve_tac [Part_eqI,CollectI] 1), 

241 
(*Now 23 subgoals: typechecking, the disjunction, perhaps equality.*) 

242 
rtac disjIn 2, 

243 
REPEAT (ares_tac [refl,exI,conjI] 2), 

244 
rewrite_goals_tac con_defs, 

245 
(*Now can solve the trivial equation*) 

246 
REPEAT (rtac refl 2), 

55  247 
REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::PartE::type_elims) 
248 
ORELSE' hyp_subst_tac 

0  249 
ORELSE' dresolve_tac rec_typechecks)), 
55  250 
DEPTH_SOLVE (swap_res_tac type_intrs 1)]; 
0  251 

252 
(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*) 

253 
val mk_disj_rls = 

254 
let fun f rl = rl RS disjI1 

255 
and g rl = rl RS disjI2 

256 
in accesses_bal(f, g, asm_rl) end; 

257 

258 
val intrs = map (prove part_rec_defs) 

259 
(intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms))); 

260 

261 
(********) 

262 
val dummy = writeln "Proving the elimination rule..."; 

263 

55  264 
(*Includes rules for succ and Pair since they are common constructions*) 
265 
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 

70
8a29f8b4aca1
ZF/indsyntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents:
55
diff
changeset

266 
Pair_neq_0, sym RS Pair_neq_0, make_elim succ_inject, 
8a29f8b4aca1
ZF/indsyntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents:
55
diff
changeset

267 
refl_thin, conjE, exE, disjE]; 
0  268 

269 
val sumprod_free_SEs = 

270 
map (gen_make_elim [conjE,FalseE]) 

271 
([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 

272 
RL [iffD1]); 

273 

274 
(*Breaks down logical connectives in the monotonic function*) 

275 
val basic_elim_tac = 

276 
REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs) 

277 
ORELSE' bound_hyp_subst_tac)) 

278 
THEN prune_params_tac; 

279 

280 
val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD); 

281 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

282 
(*Applies freeness of the given constructors, which *must* be unfolded by 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

283 
the given defs. Cannot simply use the local con_defs because con_defs=[] 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

284 
for inference systems. *) 
0  285 
fun con_elim_tac defs = 
70
8a29f8b4aca1
ZF/indsyntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents:
55
diff
changeset

286 
rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs; 
0  287 

288 
(*String s should have the form t:Si where Si is an inductive set*) 

289 
fun mk_cases defs s = 

290 
rule_by_tactic (con_elim_tac defs) 

291 
(assume_read thy s RS elim); 

292 

293 
val defs = big_rec_def::part_rec_defs; 

294 

295 
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct); 

296 

297 
end; 