author  lcp 
Mon, 21 Nov 1994 14:06:59 +0100  
changeset 724  36c0ac2f4935 
parent 633  9e4d4f3eb812 
child 751  f0aacbcedb77 
permissions  rwrr 
0  1 
(* Title: ZF/indrule.ML 
2 
ID: $Id$ 

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 

13 
val induct : thm (*main induction rule*) 

14 
val mutual_induct : thm (*mutual induction rule*) 

15 
end; 

16 

17 

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

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

20 
and Pr: PR and Su : SU and Intr_elim: INTR_ELIM) : INDRULE = 
0  21 
struct 
516  22 
open Logic Ind_Syntax Inductive Intr_elim; 
23 

24 
val sign = sign_of thy; 

0  25 

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

28 
val big_rec_name = space_implode "_" rec_names; 

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 

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

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",_) $ 

43 
(Const("op :",_)$t$X), iprems) = 

44 
(case gen_assoc (op aconv) (ind_alist, X) of 

45 
Some pred => prem :: mk_tprop (pred $ t) :: iprems 

46 
 None => (*possibly membership in M(rec_tm), for M monotone*) 

47 
let fun mk_sb (rec_tm,pred) = (rec_tm, Collect_const$rec_tm$pred) 

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

49 
 add_induct_prem ind_alist (prem,iprems) = prem :: iprems; 

50 

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

52 
fun induct_prem ind_alist intr = 

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

54 
val iprems = foldr (add_induct_prem ind_alist) 

55 
(strip_imp_prems intr,[]) 

56 
val (t,X) = rule_concl intr 

57 
val (Some pred) = gen_assoc (op aconv) (ind_alist, X) 

58 
val concl = mk_tprop (pred $ t) 

59 
in list_all_free (quantfrees, list_implies (iprems,concl)) end 

60 
handle Bind => error"Recursion term not found in conclusion"; 

61 

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

62 
(*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

63 
Intro rules with extra Vars in premises still cause some backtracking *) 
0  64 
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

65 
 ind_tac(prem::prems) i = 
724
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

66 
DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN 
633
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

67 
ind_tac prems (i1); 
0  68 

69 
val pred = Free(pred_name, iT>oT); 

70 

71 
val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms; 

72 

73 
val quant_induct = 

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

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

75 
(cterm_of sign (list_implies (ind_prems, 
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

76 
mk_tprop (mk_all_imp(big_rec_tm,pred))))) 
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

77 
(fn prems => 
0  78 
[rtac (impI RS allI) 1, 
724
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

79 
DETERM (etac raw_induct 1), 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

80 
(*Push Part inside Collect*) 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

81 
asm_full_simp_tac (FOL_ss addsimps [Part_Collect]) 1, 
590
800603278425
{HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by
lcp
parents:
543
diff
changeset

82 
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE, disjE] ORELSE' 
800603278425
{HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by
lcp
parents:
543
diff
changeset

83 
hyp_subst_tac)), 
0  84 
ind_tac (rev prems) (length prems) ]); 
85 

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

87 

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

89 

90 
(*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

91 
fun mk_pred_typ (t $ A $ Abs(_,_,B)) = 
0  92 
if t = Pr.sigma then iT > mk_pred_typ B 
93 
else iT > oT 

94 
 mk_pred_typ _ = iT > oT 

95 

96 
(*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

97 
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

98 
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

99 
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

100 
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

101 
fun mk_predpair rec_tm = 
0  102 
let val rec_name = (#1 o dest_Const o head_of) rec_tm 
724
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

103 
val T = mk_pred_typ dom_sum 
0  104 
val pfree = Free(pred_name ^ "_" ^ rec_name, T) 
105 
val frees = mk_frees "za" (binder_types T) 

106 
val qconcl = 

107 
foldr mk_all (frees, 

108 
imp $ (mem_const $ foldr1 (app Pr.pair) frees $ rec_tm) 

109 
$ (list_comb (pfree,frees))) 

110 
in (ap_split Pr.fsplit_const pfree (binder_types T), 

111 
qconcl) 

112 
end; 

113 

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

114 
val (preds,qconcls) = split_list (map mk_predpair rec_tms); 
0  115 

116 
(*Used to form simultaneous induction lemma*) 

117 
fun mk_rec_imp (rec_tm,pred) = 

118 
imp $ (mem_const $ Bound 0 $ rec_tm) $ (pred $ Bound 0); 

119 

120 
(*To instantiate the main induction rule*) 

121 
val induct_concl = 

122 
mk_tprop(mk_all_imp(big_rec_tm, 

123 
Abs("z", iT, 

124 
fold_bal (app conj) 

125 
(map mk_rec_imp (rec_tms~~preds))))) 

126 
and mutual_induct_concl = mk_tprop(fold_bal (app conj) qconcls); 

127 

128 
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

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

130 
(cterm_of sign (mk_implies (induct_concl,mutual_induct_concl))) 
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

131 
(fn prems => 
724
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

132 
[cut_facts_tac prems 1, 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

133 
REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

134 
ORELSE resolve_tac [allI, impI, conjI, Part_eqI] 1 
0  135 
ORELSE dresolve_tac [spec, mp, Pr.fsplitD] 1)]); 
136 

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

138 

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

139 
(*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

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

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

142 
FOL_ss addcongs [Collect_cong] 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

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

144 

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

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

146 

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

147 
(*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

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

149 
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

150 
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

151 
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

152 
*) 
0  153 
val cmonos = [subset_refl RS Collect_mono] RL monos RLN (2,[rev_subsetD]); 
154 

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

156 
fun mutual_ind_tac [] 0 = all_tac 

157 
 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

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

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

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

161 
(*Simplify the assumptions and goal by unfolding Part and 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

162 
using freeness of the Sum constructors*) 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

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

164 
simp_tac (mut_ss addsimps [Part_iff]) 1 THEN 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

165 
IF_UNSOLVED (*simp_tac may have finished it off!*) 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

166 
(asm_full_simp_tac mut_ss 1 THEN 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

167 
(*unpackage and use "prem" in the corresponding place*) 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

168 
REPEAT (rtac impI 1) THEN 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

169 
rtac (rewrite_rule all_defs prem) 1 THEN 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

170 
(*prem must not be REPEATed below: could loop!*) 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

171 
DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

172 
eresolve_tac ([conjE]@cmonos)))) 
36c0ac2f4935
ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of
lcp
parents:
633
diff
changeset

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

174 
THEN mutual_ind_tac prems (i1); 
0  175 

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

176 
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

177 

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

179 
prove_goalw_cterm [] 
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

180 
(cterm_of sign 
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

181 
(list_implies (map (induct_prem (rec_tms~~preds)) intr_tms, 
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

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

183 
(fn prems => 
0  184 
[rtac (quant_induct RS lemma) 1, 
185 
mutual_ind_tac (rev prems) (length prems)]); 

186 

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

188 
val fsplit_tac = 

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

190 
dtac Pr.fsplitD, 

191 
etac Pr.fsplitE, 

192 
bound_hyp_subst_tac])) 

193 
THEN prune_params_tac; 

194 

195 
(*strip quantifier*) 

196 
val induct = standard (quant_induct RS spec RSN (2,rev_mp)); 

197 

198 
val mutual_induct = rule_by_tactic fsplit_tac mutual_induct_fsplit; 

199 

200 
end; 