author  lcp 
Fri, 12 Aug 1994 12:51:34 +0200  
changeset 516  1957113f0d7d 
parent 366  5b6e4340085b 
child 543  e961b2092869 
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 

20 
and Pr: PR 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 

31 
val _ = writeln " Proving the induction rules..."; 

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 

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

63 
fun ind_tac [] 0 = all_tac 

64 
 ind_tac(prem::prems) i = REPEAT (ares_tac [Part_eqI,prem] i) THEN 

65 
ind_tac prems (i1); 

66 

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

68 

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

70 

71 
val quant_induct = 

516  72 
prove_term sign part_rec_defs 
0  73 
(list_implies (ind_prems, mk_tprop (mk_all_imp(big_rec_tm,pred))), 
74 
fn prems => 

75 
[rtac (impI RS allI) 1, 

76 
etac raw_induct 1, 

77 
REPEAT (FIRSTGOAL (eresolve_tac [CollectE,exE,conjE,disjE,ssubst])), 

78 
REPEAT (FIRSTGOAL (eresolve_tac [PartE,CollectE])), 

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

80 

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

82 

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

84 

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

86 
fun mk_pred_typ (t $ A $ Abs(_,_,B)) = 
0  87 
if t = Pr.sigma then iT > mk_pred_typ B 
88 
else iT > oT 

89 
 mk_pred_typ _ = iT > oT 

90 

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

92 
and a conclusion for the simultaneous induction rule*) 

93 
fun mk_predpair (rec_tm,domt) = 

94 
let val rec_name = (#1 o dest_Const o head_of) rec_tm 

95 
val T = mk_pred_typ domt 

96 
val pfree = Free(pred_name ^ "_" ^ rec_name, T) 

97 
val frees = mk_frees "za" (binder_types T) 

98 
val qconcl = 

99 
foldr mk_all (frees, 

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

101 
$ (list_comb (pfree,frees))) 

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

103 
qconcl) 

104 
end; 

105 

106 
val (preds,qconcls) = split_list (map mk_predpair (rec_tms~~domts)); 

107 

108 
(*Used to form simultaneous induction lemma*) 

109 
fun mk_rec_imp (rec_tm,pred) = 

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

111 

112 
(*To instantiate the main induction rule*) 

113 
val induct_concl = 

114 
mk_tprop(mk_all_imp(big_rec_tm, 

115 
Abs("z", iT, 

116 
fold_bal (app conj) 

117 
(map mk_rec_imp (rec_tms~~preds))))) 

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

119 

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

516  121 
prove_term sign part_rec_defs 
0  122 
(mk_implies (induct_concl,mutual_induct_concl), 
123 
fn prems => 

124 
[cut_facts_tac prems 1, 

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

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

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

128 

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

130 

131 
(*Removes Collects caused by Moperators in the intro rules*) 

132 
val cmonos = [subset_refl RS Collect_mono] RL monos RLN (2,[rev_subsetD]); 

133 

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

135 
fun mutual_ind_tac [] 0 = all_tac 

136 
 mutual_ind_tac(prem::prems) i = 

137 
SELECT_GOAL 

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

139 
REPEAT (FIRSTGOAL 

140 
(eresolve_tac ([conjE,mp]@cmonos) ORELSE' 

141 
ares_tac [prem,impI,conjI])) 

142 
(*prove remaining goals by contradiction*) 

143 
THEN rewrite_goals_tac (con_defs@part_rec_defs) 

144 
THEN REPEAT (eresolve_tac (PartE :: sumprod_free_SEs) 1)) 

145 
i THEN mutual_ind_tac prems (i1); 

146 

147 
val mutual_induct_fsplit = 

516  148 
prove_term sign [] 
0  149 
(list_implies (map (induct_prem (rec_tms~~preds)) intr_tms, 
150 
mutual_induct_concl), 

151 
fn prems => 

152 
[rtac (quant_induct RS lemma) 1, 

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

154 

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

156 
val fsplit_tac = 

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

158 
dtac Pr.fsplitD, 

159 
etac Pr.fsplitE, 

160 
bound_hyp_subst_tac])) 

161 
THEN prune_params_tac; 

162 

163 
(*strip quantifier*) 

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

165 

166 
val mutual_induct = rule_by_tactic fsplit_tac mutual_induct_fsplit; 

167 

168 
end; 