author  lcp 
Wed, 12 Oct 1994 12:09:54 +0100  
changeset 633  9e4d4f3eb812 
parent 590  800603278425 
child 724  36c0ac2f4935 
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 

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 = 
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

66 
DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN 
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, 
79 
etac raw_induct 1, 

590
800603278425
{HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by
lcp
parents:
543
diff
changeset

80 
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

81 
hyp_subst_tac)), 
0  82 
REPEAT (FIRSTGOAL (eresolve_tac [PartE,CollectE])), 
83 
ind_tac (rev prems) (length prems) ]); 

84 

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

86 

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

88 

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

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

93 
 mk_pred_typ _ = iT > oT 

94 

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

96 
and a conclusion for the simultaneous induction rule*) 

97 
fun mk_predpair (rec_tm,domt) = 

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

99 
val T = mk_pred_typ domt 

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

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

102 
val qconcl = 

103 
foldr mk_all (frees, 

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

105 
$ (list_comb (pfree,frees))) 

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

107 
qconcl) 

108 
end; 

109 

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

111 

112 
(*Used to form simultaneous induction lemma*) 

113 
fun mk_rec_imp (rec_tm,pred) = 

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

115 

116 
(*To instantiate the main induction rule*) 

117 
val induct_concl = 

118 
mk_tprop(mk_all_imp(big_rec_tm, 

119 
Abs("z", iT, 

120 
fold_bal (app conj) 

121 
(map mk_rec_imp (rec_tms~~preds))))) 

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

123 

124 
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

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

126 
(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

127 
(fn prems => 
0  128 
[cut_facts_tac prems 1, 
129 
REPEAT (eresolve_tac [asm_rl,conjE,PartE,mp] 1 

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

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

132 

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

134 

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

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

137 

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

139 
fun mutual_ind_tac [] 0 = all_tac 

140 
 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

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

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

143 
((*unpackage and use "prem" in the corresponding place*) 
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

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

145 
(etac conjE ORELSE' eq_mp_tac ORELSE' 
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

146 
ares_tac [impI, conjI])) 
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

147 
(*prem is not allowed in the REPEAT, lest it loop!*) 
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

148 
THEN TRYALL (rtac prem) 
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

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

150 
(FIRSTGOAL (ares_tac [impI] ORELSE' 
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

151 
eresolve_tac (mp::cmonos))) 
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

152 
(*prove remaining goals by contradiction*) 
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

153 
THEN rewrite_goals_tac (con_defs@part_rec_defs) 
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

154 
THEN DEPTH_SOLVE (eresolve_tac (PartE :: sumprod_free_SEs) 1)) 
9e4d4f3eb812
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
lcp
parents:
590
diff
changeset

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

156 
THEN mutual_ind_tac prems (i1); 
0  157 

158 
val mutual_induct_fsplit = 

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

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

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

161 
(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

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

163 
(fn prems => 
0  164 
[rtac (quant_induct RS lemma) 1, 
165 
mutual_ind_tac (rev prems) (length prems)]); 

166 

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

168 
val fsplit_tac = 

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

170 
dtac Pr.fsplitD, 

171 
etac Pr.fsplitE, 

172 
bound_hyp_subst_tac])) 

173 
THEN prune_params_tac; 

174 

175 
(*strip quantifier*) 

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

177 

178 
val mutual_induct = rule_by_tactic fsplit_tac mutual_induct_fsplit; 

179 

180 
end; 