88 |
88 |
89 (*** Prove the simultaneous induction rule ***) |
89 (*** Prove the simultaneous induction rule ***) |
90 |
90 |
91 (*Make distinct predicates for each inductive set*) |
91 (*Make distinct predicates for each inductive set*) |
92 |
92 |
93 (*Sigmas and Cartesian products may nest ONLY to the right!*) |
93 (*The components of the element type, several if it is a product*) |
94 fun mk_pred_typ (t $ A $ Abs(_,_,B)) = |
94 val elem_type = CP.pseudo_type Inductive.dom_sum; |
95 if t = Pr.sigma then Ind_Syntax.iT --> mk_pred_typ B |
95 val elem_factors = CP.factors elem_type; |
96 else Ind_Syntax.iT --> Ind_Syntax.oT |
96 val elem_frees = mk_frees "za" elem_factors; |
97 | mk_pred_typ _ = Ind_Syntax.iT --> Ind_Syntax.oT |
97 val elem_tuple = CP.mk_tuple Pr.pair elem_type elem_frees; |
98 |
|
99 (*For testing whether the inductive set is a relation*) |
|
100 fun is_sigma (t$_$_) = (t = Pr.sigma) |
|
101 | is_sigma _ = false; |
|
102 |
98 |
103 (*Given a recursive set and its domain, return the "fsplit" predicate |
99 (*Given a recursive set and its domain, return the "fsplit" predicate |
104 and a conclusion for the simultaneous induction rule. |
100 and a conclusion for the simultaneous induction rule. |
105 NOTE. This will not work for mutually recursive predicates. Previously |
101 NOTE. This will not work for mutually recursive predicates. Previously |
106 a summand 'domt' was also an argument, but this required the domain of |
102 a summand 'domt' was also an argument, but this required the domain of |
107 mutual recursion to invariably be a disjoint sum.*) |
103 mutual recursion to invariably be a disjoint sum.*) |
108 fun mk_predpair rec_tm = |
104 fun mk_predpair rec_tm = |
109 let val rec_name = (#1 o dest_Const o head_of) rec_tm |
105 let val rec_name = (#1 o dest_Const o head_of) rec_tm |
110 val T = mk_pred_typ Inductive.dom_sum |
106 val pfree = Free(pred_name ^ "_" ^ rec_name, |
111 val pfree = Free(pred_name ^ "_" ^ rec_name, T) |
107 elem_factors ---> Ind_Syntax.oT) |
112 val frees = mk_frees "za" (binder_types T) |
|
113 val qconcl = |
108 val qconcl = |
114 foldr Ind_Syntax.mk_all (frees, |
109 foldr Ind_Syntax.mk_all |
115 Ind_Syntax.imp $ |
110 (elem_frees, |
116 (Ind_Syntax.mem_const $ foldr1 (app Pr.pair) frees $ |
111 Ind_Syntax.imp $ |
117 rec_tm) |
112 (Ind_Syntax.mem_const $ elem_tuple $ rec_tm) |
118 $ (list_comb (pfree,frees))) |
113 $ (list_comb (pfree, elem_frees))) |
119 in (Ind_Syntax.ap_split Pr.fsplit_const pfree (binder_types T), |
114 in (CP.ap_split elem_type Ind_Syntax.oT pfree, |
120 qconcl) |
115 qconcl) |
121 end; |
116 end; |
122 |
117 |
123 val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms); |
118 val (preds,qconcls) = split_list (map mk_predpair Inductive.rec_tms); |
124 |
119 |
125 (*Used to form simultaneous induction lemma*) |
120 (*Used to form simultaneous induction lemma*) |
127 Ind_Syntax.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $ |
122 Ind_Syntax.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $ |
128 (pred $ Bound 0); |
123 (pred $ Bound 0); |
129 |
124 |
130 (*To instantiate the main induction rule*) |
125 (*To instantiate the main induction rule*) |
131 val induct_concl = |
126 val induct_concl = |
132 Ind_Syntax.mk_tprop(Ind_Syntax.mk_all_imp(big_rec_tm, |
127 Ind_Syntax.mk_tprop |
133 Abs("z", Ind_Syntax.iT, |
128 (Ind_Syntax.mk_all_imp |
134 fold_bal (app Ind_Syntax.conj) |
129 (big_rec_tm, |
135 (map mk_rec_imp (Inductive.rec_tms~~preds))))) |
130 Abs("z", Ind_Syntax.iT, |
|
131 fold_bal (app Ind_Syntax.conj) |
|
132 (map mk_rec_imp (Inductive.rec_tms~~preds))))) |
136 and mutual_induct_concl = |
133 and mutual_induct_concl = |
137 Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls); |
134 Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls); |
|
135 |
|
136 val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp], |
|
137 resolve_tac [allI, impI, conjI, Part_eqI], |
|
138 dresolve_tac [spec, mp, Pr.fsplitD]]; |
138 |
139 |
139 val lemma = (*makes the link between the two induction rules*) |
140 val lemma = (*makes the link between the two induction rules*) |
140 prove_goalw_cterm part_rec_defs |
141 prove_goalw_cterm part_rec_defs |
141 (cterm_of sign (Logic.mk_implies (induct_concl,mutual_induct_concl))) |
142 (cterm_of sign (Logic.mk_implies (induct_concl,mutual_induct_concl))) |
142 (fn prems => |
143 (fn prems => |
143 [cut_facts_tac prems 1, |
144 [cut_facts_tac prems 1, |
144 REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1 |
145 REPEAT (rewrite_goals_tac [Pr.split_eq] THEN |
145 ORELSE resolve_tac [allI, impI, conjI, Part_eqI] 1 |
146 lemma_tac 1)]); |
146 ORELSE dresolve_tac [spec, mp, Pr.fsplitD] 1)]); |
|
147 |
147 |
148 (*Mutual induction follows by freeness of Inl/Inr.*) |
148 (*Mutual induction follows by freeness of Inl/Inr.*) |
149 |
149 |
150 (*Simplification largely reduces the mutual induction rule to the |
150 (*Simplification largely reduces the mutual induction rule to the |
151 standard rule*) |
151 standard rule*) |
195 mutual_induct_concl))) |
195 mutual_induct_concl))) |
196 (fn prems => |
196 (fn prems => |
197 [rtac (quant_induct RS lemma) 1, |
197 [rtac (quant_induct RS lemma) 1, |
198 mutual_ind_tac (rev prems) (length prems)]); |
198 mutual_ind_tac (rev prems) (length prems)]); |
199 |
199 |
200 (*Attempts to remove all occurrences of fsplit*) |
200 |
201 val fsplit_tac = |
201 |
202 REPEAT (SOMEGOAL (FIRST' [rtac Pr.fsplitI, |
202 (** Uncurrying the predicate in the ordinary induction rule **) |
203 dtac Pr.fsplitD, |
203 |
204 etac Pr.fsplitE, (*apparently never used!*) |
204 (*instantiate the variable to a tuple, if it is non-trivial, in order to |
205 bound_hyp_subst_tac])) |
205 allow the predicate to be "opened up". |
206 THEN prune_params_tac |
206 The name "x.1" comes from the "RS spec" !*) |
|
207 val inst = |
|
208 case elem_frees of [_] => I |
|
209 | _ => instantiate ([], [(cterm_of sign (Var(("x",1), Ind_Syntax.iT)), |
|
210 cterm_of sign elem_tuple)]); |
|
211 |
|
212 (*strip quantifier and the implication*) |
|
213 val induct0 = inst (quant_induct RS spec RSN (2,rev_mp)); |
|
214 |
207 |
215 |
208 in |
216 in |
209 struct |
217 struct |
210 (*strip quantifier*) |
218 (*strip quantifier*) |
211 val induct = standard (quant_induct RS spec RSN (2,rev_mp)); |
219 val induct = standard |
212 |
220 (CP.split_rule_var |
213 (*Just "True" unless significantly different from induct, with mutual |
221 (Var((pred_name,2), elem_type --> Ind_Syntax.oT), |
214 recursion or because it involves tuples. This saves storage.*) |
222 induct0)); |
|
223 |
|
224 (*Just "True" unless there's true mutual recursion. This saves storage.*) |
215 val mutual_induct = |
225 val mutual_induct = |
216 if length Intr_elim.rec_names > 1 orelse |
226 if length Intr_elim.rec_names > 1 |
217 is_sigma Inductive.dom_sum |
227 then CP.remove_split mutual_induct_fsplit |
218 then rule_by_tactic fsplit_tac mutual_induct_fsplit |
|
219 else TrueI; |
228 else TrueI; |
220 end |
229 end |
221 end; |
230 end; |