author  lcp 
Fri, 06 May 1994 15:49:23 +0200  
changeset 366  5b6e4340085b 
parent 0  a5a9c433f639 
child 516  1957113f0d7d 
permissions  rwrr 
0  1 
(* Title: ZF/indrule.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 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 

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

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

15 
end; 

16 

17 

18 
functor Indrule_Fun (structure Ind: INDUCTIVE and 

19 
Pr: PR and Intr_elim: INTR_ELIM) : INDRULE = 

20 
struct 

21 
open Logic Ind Intr_elim; 

22 

23 
val dummy = writeln "Proving the induction rules..."; 

24 

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

26 

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

28 

29 
val prove = prove_term (sign_of Intr_elim.thy); 

30 

31 
val big_rec_def::part_rec_defs = Intr_elim.defs; 

32 

33 
(*Used to make induction rules; 

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

35 
prem is a premise of an intr rule*) 

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

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

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

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

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

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

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

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

44 

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

46 
fun induct_prem ind_alist intr = 

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

48 
val iprems = foldr (add_induct_prem ind_alist) 

49 
(strip_imp_prems intr,[]) 

50 
val (t,X) = rule_concl intr 

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

52 
val concl = mk_tprop (pred $ t) 

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

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

55 

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

57 
fun ind_tac [] 0 = all_tac 

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

59 
ind_tac prems (i1); 

60 

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

62 

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

64 

65 
val quant_induct = 

66 
prove part_rec_defs 

67 
(list_implies (ind_prems, mk_tprop (mk_all_imp(big_rec_tm,pred))), 

68 
fn prems => 

69 
[rtac (impI RS allI) 1, 

70 
etac raw_induct 1, 

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

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

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

74 

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

76 

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

78 

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

80 
fun mk_pred_typ (t $ A $ Abs(_,_,B)) = 
0  81 
if t = Pr.sigma then iT > mk_pred_typ B 
82 
else iT > oT 

83 
 mk_pred_typ _ = iT > oT 

84 

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

86 
and a conclusion for the simultaneous induction rule*) 

87 
fun mk_predpair (rec_tm,domt) = 

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

89 
val T = mk_pred_typ domt 

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

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

92 
val qconcl = 

93 
foldr mk_all (frees, 

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

95 
$ (list_comb (pfree,frees))) 

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

97 
qconcl) 

98 
end; 

99 

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

101 

102 
(*Used to form simultaneous induction lemma*) 

103 
fun mk_rec_imp (rec_tm,pred) = 

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

105 

106 
(*To instantiate the main induction rule*) 

107 
val induct_concl = 

108 
mk_tprop(mk_all_imp(big_rec_tm, 

109 
Abs("z", iT, 

110 
fold_bal (app conj) 

111 
(map mk_rec_imp (rec_tms~~preds))))) 

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

113 

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

115 
prove part_rec_defs 

116 
(mk_implies (induct_concl,mutual_induct_concl), 

117 
fn prems => 

118 
[cut_facts_tac prems 1, 

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

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

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

122 

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

124 

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

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

127 

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

129 
fun mutual_ind_tac [] 0 = all_tac 

130 
 mutual_ind_tac(prem::prems) i = 

131 
SELECT_GOAL 

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

133 
REPEAT (FIRSTGOAL 

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

135 
ares_tac [prem,impI,conjI])) 

136 
(*prove remaining goals by contradiction*) 

137 
THEN rewrite_goals_tac (con_defs@part_rec_defs) 

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

139 
i THEN mutual_ind_tac prems (i1); 

140 

141 
val mutual_induct_fsplit = 

142 
prove [] 

143 
(list_implies (map (induct_prem (rec_tms~~preds)) intr_tms, 

144 
mutual_induct_concl), 

145 
fn prems => 

146 
[rtac (quant_induct RS lemma) 1, 

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

148 

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

150 
val fsplit_tac = 

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

152 
dtac Pr.fsplitD, 

153 
etac Pr.fsplitE, 

154 
bound_hyp_subst_tac])) 

155 
THEN prune_params_tac; 

156 

157 
(*strip quantifier*) 

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

159 

160 
val mutual_induct = rule_by_tactic fsplit_tac mutual_induct_fsplit; 

161 

162 
end; 