author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 1736  fe0b459273f2 
permissions  rwrr 
1461  1 
(* Title: ZF/indrule.ML 
0  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
516  4 
Copyright 1994 University of Cambridge 
0  5 

6 
Induction rule module  for Inductive/Coinductive Definitions 

7 

8 
Proves a strong induction rule and a mutual induction rule 

9 
*) 

10 

11 
signature INDRULE = 

12 
sig 

1461  13 
val induct : thm (*main induction rule*) 
14 
val mutual_induct : thm (*mutual induction rule*) 

0  15 
end; 
16 

17 

516  18 
functor Indrule_Fun 
19 
(structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end 

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

20 
and Pr: PR and Su : SU and 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

21 
Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE = 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

22 
let 
516  23 

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

24 
val sign = sign_of Inductive.thy; 
0  25 

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

26 
val (Const(_,recT),rec_params) = strip_comb (hd Inductive.rec_tms); 
516  27 

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

28 
val big_rec_name = space_implode "_" Intr_elim.rec_names; 
516  29 
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); 
30 

724
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

31 
val _ = writeln " Proving the induction rule..."; 
0  32 

33 
(*** Prove the main induction rule ***) 

34 

1461  35 
val pred_name = "P"; (*name for predicate variables*) 
0  36 

37 
val big_rec_def::part_rec_defs = Intr_elim.defs; 

38 

39 
(*Used to make induction rules; 

40 
ind_alist = [(rec_tm1,pred1),...]  associates predicates with rec ops 

41 
prem is a premise of an intr rule*) 

42 
fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $ 

1461  43 
(Const("op :",_)$t$X), iprems) = 
0  44 
(case gen_assoc (op aconv) (ind_alist, X) of 
1461  45 
Some pred => prem :: Ind_Syntax.mk_tprop (pred $ t) :: iprems 
46 
 None => (*possibly membership in M(rec_tm), for M monotone*) 

47 
let fun mk_sb (rec_tm,pred) = 

48 
(rec_tm, Ind_Syntax.Collect_const$rec_tm$pred) 

49 
in subst_free (map mk_sb ind_alist) prem :: iprems end) 

0  50 
 add_induct_prem ind_alist (prem,iprems) = prem :: iprems; 
51 

52 
(*Make a premise of the induction rule.*) 

53 
fun induct_prem ind_alist intr = 

54 
let val quantfrees = map dest_Free (term_frees intr \\ rec_params) 

55 
val iprems = foldr (add_induct_prem ind_alist) 

1461  56 
(Logic.strip_imp_prems intr,[]) 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

57 
val (t,X) = Ind_Syntax.rule_concl intr 
0  58 
val (Some pred) = gen_assoc (op aconv) (ind_alist, X) 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

59 
val concl = Ind_Syntax.mk_tprop (pred $ t) 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

60 
in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end 
0  61 
handle Bind => error"Recursion term not found in conclusion"; 
62 

633
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

63 
(*Reduces backtracking by delivering the correct premise to each goal. 
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

64 
Intro rules with extra Vars in premises still cause some backtracking *) 
0  65 
fun ind_tac [] 0 = all_tac 
633
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

66 
 ind_tac(prem::prems) i = 
1461  67 
DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN 
68 
ind_tac prems (i1); 

0  69 

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

70 
val pred = Free(pred_name, Ind_Syntax.iT > Ind_Syntax.oT); 
0  71 

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

72 
val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

73 
Inductive.intr_tms; 
0  74 

75 
val quant_induct = 

543
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

76 
prove_goalw_cterm part_rec_defs 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

77 
(cterm_of sign 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

78 
(Logic.list_implies (ind_prems, 
1461  79 
Ind_Syntax.mk_tprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred))))) 
543
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

80 
(fn prems => 
0  81 
[rtac (impI RS allI) 1, 
1461  82 
DETERM (etac Intr_elim.raw_induct 1), 
83 
(*Push Part inside Collect*) 

84 
asm_full_simp_tac (FOL_ss addsimps [Part_Collect]) 1, 

85 
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE, disjE] ORELSE' 

86 
hyp_subst_tac)), 

87 
ind_tac (rev prems) (length prems) ]); 

0  88 

89 
(*** Prove the simultaneous induction rule ***) 

90 

91 
(*Make distinct predicates for each inductive set*) 

92 

93 
(*Sigmas and Cartesian products may nest ONLY to the right!*) 

366
5b6e4340085b
ZF/indrule/mk_pred_typ: corrected pattern to include Abs, allowing it to
lcp
parents:
0
diff
changeset

94 
fun mk_pred_typ (t $ A $ Abs(_,_,B)) = 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

95 
if t = Pr.sigma then Ind_Syntax.iT > mk_pred_typ B 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

96 
else Ind_Syntax.iT > Ind_Syntax.oT 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

97 
 mk_pred_typ _ = Ind_Syntax.iT > Ind_Syntax.oT 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

98 

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

99 
(*For testing whether the inductive set is a relation*) 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

100 
fun is_sigma (t$_$_) = (t = Pr.sigma) 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

101 
 is_sigma _ = false; 
0  102 

103 
(*Given a recursive set and its domain, return the "fsplit" predicate 

724
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

104 
and a conclusion for the simultaneous induction rule. 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

105 
NOTE. This will not work for mutually recursive predicates. Previously 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

106 
a summand 'domt' was also an argument, but this required the domain of 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

107 
mutual recursion to invariably be a disjoint sum.*) 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

108 
fun mk_predpair rec_tm = 
0  109 
let val rec_name = (#1 o dest_Const o head_of) rec_tm 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

110 
val T = mk_pred_typ Inductive.dom_sum 
0  111 
val pfree = Free(pred_name ^ "_" ^ rec_name, T) 
112 
val frees = mk_frees "za" (binder_types T) 

113 
val qconcl = 

1461  114 
foldr Ind_Syntax.mk_all (frees, 
115 
Ind_Syntax.imp $ 

116 
(Ind_Syntax.mem_const $ foldr1 (app Pr.pair) frees $ 

117 
rec_tm) 

118 
$ (list_comb (pfree,frees))) 

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

119 
in (Ind_Syntax.ap_split Pr.fsplit_const pfree (binder_types T), 
0  120 
qconcl) 
121 
end; 

122 

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

123 
val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms); 
0  124 

125 
(*Used to form simultaneous induction lemma*) 

126 
fun mk_rec_imp (rec_tm,pred) = 

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

127 
Ind_Syntax.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $ 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

128 
(pred $ Bound 0); 
0  129 

130 
(*To instantiate the main induction rule*) 

131 
val induct_concl = 

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

132 
Ind_Syntax.mk_tprop(Ind_Syntax.mk_all_imp(big_rec_tm, 
1461  133 
Abs("z", Ind_Syntax.iT, 
134 
fold_bal (app Ind_Syntax.conj) 

135 
(map mk_rec_imp (Inductive.rec_tms~~preds))))) 

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

136 
and mutual_induct_concl = 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

137 
Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls); 
0  138 

139 
val lemma = (*makes the link between the two induction rules*) 

543
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

140 
prove_goalw_cterm part_rec_defs 
1461  141 
(cterm_of sign (Logic.mk_implies (induct_concl,mutual_induct_concl))) 
142 
(fn prems => 

143 
[cut_facts_tac prems 1, 

144 
REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1 

145 
ORELSE resolve_tac [allI, impI, conjI, Part_eqI] 1 

146 
ORELSE dresolve_tac [spec, mp, Pr.fsplitD] 1)]); 

0  147 

148 
(*Mutual induction follows by freeness of Inl/Inr.*) 

149 

724
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

150 
(*Simplification largely reduces the mutual induction rule to the 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

151 
standard rule*) 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

152 
val mut_ss = 
751
f0aacbcedb77
ZF/indrule/mutual_ind_tac: ensured that asm_full_simp_tac ignores any
lcp
parents:
724
diff
changeset

153 
FOL_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff]; 
724
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

154 

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

155 
val all_defs = Inductive.con_defs @ part_rec_defs; 
724
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

156 

36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

157 
(*Removes Collects caused by Moperators in the intro rules. It is very 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

158 
hard to simplify 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

159 
list({v: tf. (v : t > P_t(v)) & (v : f > P_f(v))}) 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

160 
where t==Part(tf,Inl) and f==Part(tf,Inr) to list({v: tf. P_t(v)}). 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

161 
Instead the following rules extract the relevant conjunct. 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

162 
*) 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

163 
val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos RLN (2,[rev_subsetD]); 
0  164 

165 
(*Avoids backtracking by delivering the correct premise to each goal*) 

166 
fun mutual_ind_tac [] 0 = all_tac 

167 
 mutual_ind_tac(prem::prems) i = 

633
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

168 
DETERM 
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

169 
(SELECT_GOAL 
1461  170 
( 
171 
(*Simplify the assumptions and goal by unfolding Part and 

172 
using freeness of the Sum constructors; proves all but one 

751
f0aacbcedb77
ZF/indrule/mutual_ind_tac: ensured that asm_full_simp_tac ignores any
lcp
parents:
724
diff
changeset

173 
conjunct by contradiction*) 
1461  174 
rewrite_goals_tac all_defs THEN 
175 
simp_tac (mut_ss addsimps [Part_iff]) 1 THEN 

176 
IF_UNSOLVED (*simp_tac may have finished it off!*) 

177 
((*simplify assumptions, but don't accept new rewrite rules!*) 

178 
asm_full_simp_tac (mut_ss setmksimps (fn _=>[])) 1 THEN 

179 
(*unpackage and use "prem" in the corresponding place*) 

180 
REPEAT (rtac impI 1) THEN 

181 
rtac (rewrite_rule all_defs prem) 1 THEN 

182 
(*prem must not be REPEATed below: could loop!*) 

183 
DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' 

184 
eresolve_tac (conjE::mp::cmonos)))) 

185 
) i) 

633
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

186 
THEN mutual_ind_tac prems (i1); 
0  187 

724
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

188 
val _ = writeln " Proving the mutual induction rule..."; 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

189 

0  190 
val mutual_induct_fsplit = 
543
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

191 
prove_goalw_cterm [] 
1461  192 
(cterm_of sign 
193 
(Logic.list_implies 

194 
(map (induct_prem (Inductive.rec_tms~~preds)) Inductive.intr_tms, 

195 
mutual_induct_concl))) 

196 
(fn prems => 

197 
[rtac (quant_induct RS lemma) 1, 

198 
mutual_ind_tac (rev prems) (length prems)]); 

0  199 

200 
(*Attempts to remove all occurrences of fsplit*) 

201 
val fsplit_tac = 

202 
REPEAT (SOMEGOAL (FIRST' [rtac Pr.fsplitI, 

1461  203 
dtac Pr.fsplitD, 
204 
etac Pr.fsplitE, (*apparently never used!*) 

205 
bound_hyp_subst_tac])) 

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

206 
THEN prune_params_tac 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

207 

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

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

209 
struct 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

210 
(*strip quantifier*) 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

211 
val induct = standard (quant_induct RS spec RSN (2,rev_mp)); 
0  212 

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

213 
(*Just "True" unless significantly different from induct, with mutual 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

214 
recursion or because it involves tuples. This saves storage.*) 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

215 
val mutual_induct = 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

216 
if length Intr_elim.rec_names > 1 orelse 
1461  217 
is_sigma Inductive.dom_sum 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

218 
then rule_by_tactic fsplit_tac mutual_induct_fsplit 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

219 
else TrueI; 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1104
diff
changeset

220 
end 
0  221 
end; 