author  nipkow 
Thu, 04 Apr 1996 20:13:46 +0200  
changeset 1653  1a2ffa2fbf7d 
parent 1465  5d7a7e439cec 
child 1728  01beef6262aa 
permissions  rwrr 
1465  1 
(* Title: HOL/indrule.ML 
923  2 
ID: $Id$ 
1465  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
923  4 
Copyright 1994 University of Cambridge 
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 

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

923  15 
end; 
16 

17 

18 
functor Indrule_Fun 

19 
(structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end and 

1465  20 
Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE = 
1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

21 
let 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

22 

ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

23 
val sign = sign_of Inductive.thy; 
923  24 

1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

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

1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

27 
val elem_type = Ind_Syntax.dest_setT (body_type recT); 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

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

1190
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

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

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

34 

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

37 
val big_rec_def::part_rec_defs = Intr_elim.defs; 

38 

39 
(*Used to express induction rules: adds induction hypotheses. 

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

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

47 
let fun mk_sb (rec_tm,pred) = 

48 
(case binder_types (fastype_of pred) of 

49 
[T] => (rec_tm, 

50 
Ind_Syntax.Int_const T $ rec_tm $ 

51 
(Ind_Syntax.Collect_const T $ pred)) 

52 
 _ => error 

53 
"Bug: add_induct_prem called with nonunary predicate") 

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

923  55 
 add_induct_prem ind_alist (prem,iprems) = prem :: iprems; 
56 

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

58 
fun induct_prem ind_alist intr = 

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

60 
val iprems = foldr (add_induct_prem ind_alist) 

1465  61 
(Logic.strip_imp_prems intr,[]) 
1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

62 
val (t,X) = Ind_Syntax.rule_concl intr 
923  63 
val (Some pred) = gen_assoc (op aconv) (ind_alist, X) 
1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

64 
val concl = Ind_Syntax.mk_Trueprop (pred $ t) 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

65 
in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end 
923  66 
handle Bind => error"Recursion term not found in conclusion"; 
67 

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

69 
fun ind_tac [] 0 = all_tac 

70 
 ind_tac(prem::prems) i = 

1465  71 
DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN 
72 
ind_tac prems (i1); 

923  73 

1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

74 
val pred = Free(pred_name, elem_type > Ind_Syntax.boolT); 
923  75 

1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

76 
val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

77 
Inductive.intr_tms; 
923  78 

1190
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

79 
(*Debugging code... 
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

80 
val _ = writeln "ind_prems = "; 
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

81 
val _ = seq (writeln o Sign.string_of_term sign) ind_prems; 
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

82 
*) 
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

83 

923  84 
val quant_induct = 
85 
prove_goalw_cterm part_rec_defs 

1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

86 
(cterm_of sign 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

87 
(Logic.list_implies (ind_prems, 
1465  88 
Ind_Syntax.mk_Trueprop (Ind_Syntax.mk_all_imp 
89 
(big_rec_tm,pred))))) 

923  90 
(fn prems => 
91 
[rtac (impI RS allI) 1, 

1465  92 
DETERM (etac Intr_elim.raw_induct 1), 
1653  93 
asm_full_simp_tac (HOL_ss addsimps [Part_Collect]) 1, 
1465  94 
REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] 
95 
ORELSE' hyp_subst_tac)), 

96 
ind_tac (rev prems) (length prems)]) 

923  97 
handle e => print_sign_exn sign e; 
98 

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

100 

101 
(*Make distinct predicates for each inductive set. 

1190
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

102 
Splits cartesian products in elem_type, IF nested to the right! *) 
923  103 

1190
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

104 
(*Given a recursive set, return the "split" predicate 
923  105 
and a conclusion for the simultaneous induction rule*) 
1190
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

106 
fun mk_predpair rec_tm = 
923  107 
let val rec_name = (#1 o dest_Const o head_of) rec_tm 
1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

108 
val T = Ind_Syntax.factors elem_type > Ind_Syntax.boolT 
923  109 
val pfree = Free(pred_name ^ "_" ^ rec_name, T) 
110 
val frees = mk_frees "za" (binder_types T) 

111 
val qconcl = 

1465  112 
foldr Ind_Syntax.mk_all 
113 
(frees, 

114 
Ind_Syntax.imp $ (Ind_Syntax.mk_mem 

115 
(foldr1 Ind_Syntax.mk_Pair frees, rec_tm)) 

116 
$ (list_comb (pfree,frees))) 

1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

117 
in (Ind_Syntax.ap_split Ind_Syntax.boolT pfree (binder_types T), 
923  118 
qconcl) 
119 
end; 

120 

1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

121 
val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms); 
923  122 

123 
(*Used to form simultaneous induction lemma*) 

124 
fun mk_rec_imp (rec_tm,pred) = 

1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

125 
Ind_Syntax.imp $ (Ind_Syntax.mk_mem (Bound 0, rec_tm)) $ (pred $ Bound 0); 
923  126 

127 
(*To instantiate the main induction rule*) 

128 
val induct_concl = 

1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

129 
Ind_Syntax.mk_Trueprop 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

130 
(Ind_Syntax.mk_all_imp 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

131 
(big_rec_tm, 
1465  132 
Abs("z", elem_type, 
133 
fold_bal (app Ind_Syntax.conj) 

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

1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

135 
and mutual_induct_concl = 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

136 
Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls); 
923  137 

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

139 
prove_goalw_cterm part_rec_defs 

1465  140 
(cterm_of sign (Logic.mk_implies (induct_concl, 
141 
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, refl] 1 

146 
ORELSE dresolve_tac [spec, mp, splitD] 1)]) 

923  147 
handle e => print_sign_exn sign e; 
148 

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

150 

1190
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

151 
(*Simplification largely reduces the mutual induction rule to the 
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

152 
standard rule*) 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1190
diff
changeset

153 
val mut_ss = simpset_of "Fun" 
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1190
diff
changeset

154 
addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq]; 
1190
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

155 

1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

156 
val all_defs = Inductive.con_defs @ part_rec_defs; 
1190
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

157 

923  158 
(*Removes Collects caused by Moperators in the intro rules*) 
1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

159 
val cmonos = [subset_refl RS Int_Collect_mono] RL Inductive.monos RLN 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

160 
(2,[rev_subsetD]); 
923  161 

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

163 
fun mutual_ind_tac [] 0 = all_tac 

164 
 mutual_ind_tac(prem::prems) i = 

165 
DETERM 

166 
(SELECT_GOAL 

1465  167 
( 
168 
(*Simplify the assumptions and goal by unfolding Part and 

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

1190
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

170 
conjunct by contradiction*) 
1465  171 
rewrite_goals_tac all_defs THEN 
172 
simp_tac (mut_ss addsimps [Part_def]) 1 THEN 

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

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

175 
asm_full_simp_tac (mut_ss setmksimps K[]) 1 THEN 

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

177 
REPEAT (rtac impI 1) THEN 

178 
rtac (rewrite_rule all_defs prem) 1 THEN 

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

180 
DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' 

181 
eresolve_tac (conjE::mp::cmonos)))) 

182 
) i) 

1190
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

183 
THEN mutual_ind_tac prems (i1); 
9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

184 

9d1bdce3a38e
Old version of mutual induction never worked. Now ensures that
lcp
parents:
923
diff
changeset

185 
val _ = writeln " Proving the mutual induction rule..."; 
923  186 

187 
val mutual_induct_split = 

188 
prove_goalw_cterm [] 

1465  189 
(cterm_of sign 
190 
(Logic.list_implies (map (induct_prem (Inductive.rec_tms ~~ preds)) 

191 
Inductive.intr_tms, 

192 
mutual_induct_concl))) 

193 
(fn prems => 

194 
[rtac (quant_induct RS lemma) 1, 

195 
mutual_ind_tac (rev prems) (length prems)]) 

923  196 
handle e => print_sign_exn sign e; 
197 

198 
(*Attempts to remove all occurrences of split*) 

199 
val split_tac = 

200 
REPEAT (SOMEGOAL (FIRST' [rtac splitI, 

1465  201 
dtac splitD, 
202 
etac splitE, 

203 
bound_hyp_subst_tac])) 

923  204 
THEN prune_params_tac; 
205 

1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

206 
in 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

207 
struct 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

208 
(*strip quantifier*) 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

209 
val induct = standard (quant_induct RS spec RSN (2,rev_mp)); 
923  210 

1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

211 
val mutual_induct = 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

212 
if length Intr_elim.rec_names > 1 orelse 
1465  213 
length (Ind_Syntax.factors elem_type) > 1 
1424
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

214 
then rule_by_tactic split_tac mutual_induct_split 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

215 
else TrueI; 
ccb3c5ff6707
Now mutual_induct is simply "True" unless it is going to be
paulson
parents:
1264
diff
changeset

216 
end 
923  217 
end; 