169 val ((f, (_, f_defthm)), lthy') = LocalTheory.def ((fname, mixfix), |
169 val ((f, (_, f_defthm)), lthy') = LocalTheory.def ((fname, mixfix), |
170 ((fname ^ "_def", []), Term.subst_bound (fsum, f_def))) |
170 ((fname ^ "_def", []), Term.subst_bound (fsum, f_def))) |
171 lthy |
171 lthy |
172 in |
172 in |
173 (MutualPart {fvar=(fname, fT), cargTs=cargTs, pthA=pthA, pthR=pthR, f_def=f_def, |
173 (MutualPart {fvar=(fname, fT), cargTs=cargTs, pthA=pthA, pthR=pthR, f_def=f_def, |
174 f=SOME f, f_defthm=SOME f_defthm }, |
174 f=SOME f, f_defthm=SOME f_defthm }, |
175 lthy') |
175 lthy') |
176 end |
176 end |
177 |
177 |
178 val Mutual { defname, fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual |
178 val Mutual { defname, fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual |
179 val (parts', lthy') = fold_map def (parts ~~ fixes) lthy |
179 val (parts', lthy') = fold_map def (parts ~~ fixes) lthy |
180 in |
180 in |
181 (Mutual { defname=defname, fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts', |
181 (Mutual { defname=defname, fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts', |
182 fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum }, |
182 fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum }, |
184 end |
184 end |
185 |
185 |
186 |
186 |
187 fun prepare_fundef_mutual fixes eqss default lthy = |
187 fun prepare_fundef_mutual fixes eqss default lthy = |
188 let |
188 let |
189 val mutual = analyze_eqs lthy (map fst fixes) eqss |
189 val mutual = analyze_eqs lthy (map fst fixes) eqss |
190 val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual |
190 val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual |
191 |
191 |
192 val (prep_result, fsum, lthy') = |
192 val (prep_result, fsum, lthy') = |
193 FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy |
193 FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy |
194 |
194 |
195 val (mutual', lthy'') = define_projections fixes mutual fsum lthy' |
195 val (mutual', lthy'') = define_projections fixes mutual fsum lthy' |
196 in |
196 in |
197 ((mutual', defname, prep_result), lthy'') |
197 ((mutual', defname, prep_result), lthy'') |
198 end |
198 end |
199 |
199 |
200 |
200 |
201 (* Beta-reduce both sides of a meta-equality *) |
201 (* Beta-reduce both sides of a meta-equality *) |
202 fun beta_norm_eq thm = |
202 fun beta_norm_eq thm = |
203 let |
203 let |
204 val (lhs, rhs) = dest_equals (cprop_of thm) |
204 val (lhs, rhs) = dest_equals (cprop_of thm) |
205 val lhs_conv = beta_conversion false lhs |
205 val lhs_conv = beta_conversion false lhs |
206 val rhs_conv = beta_conversion false rhs |
206 val rhs_conv = beta_conversion false rhs |
207 in |
207 in |
208 transitive (symmetric lhs_conv) (transitive thm rhs_conv) |
208 transitive (symmetric lhs_conv) (transitive thm rhs_conv) |
209 end |
209 end |
210 |
210 |
211 fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm |
211 fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm |
212 |
212 |
213 |
213 |
214 fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = |
214 fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = |
215 let |
215 let |
216 val thy = ProofContext.theory_of ctxt |
216 val thy = ProofContext.theory_of ctxt |
217 |
217 |
218 val oqnames = map fst pre_qs |
218 val oqnames = map fst pre_qs |
219 val (qs, ctxt') = Variable.variant_fixes oqnames ctxt |
219 val (qs, ctxt') = Variable.variant_fixes oqnames ctxt |
220 |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
220 |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
221 |
221 |
222 fun inst t = subst_bounds (rev qs, t) |
222 fun inst t = subst_bounds (rev qs, t) |
223 val gs = map inst pre_gs |
223 val gs = map inst pre_gs |
224 val args = map inst pre_args |
224 val args = map inst pre_args |
225 val rhs = inst pre_rhs |
225 val rhs = inst pre_rhs |
226 |
226 |
273 fold (fn x => fn thm => combination thm (reflexive x)) xs thm |
273 fold (fn x => fn thm => combination thm (reflexive x)) xs thm |
274 |> beta_reduce |
274 |> beta_reduce |
275 |> fold_rev forall_intr xs |
275 |> fold_rev forall_intr xs |
276 |> forall_elim_vars 0 |
276 |> forall_elim_vars 0 |
277 end |
277 end |
278 |
278 |
279 |
279 |
280 fun mutual_induct_rules thy induct all_f_defs (Mutual {RST, parts, streeA, ...}) = |
280 fun mutual_induct_rules thy induct all_f_defs (Mutual {RST, parts, streeA, ...}) = |
281 let |
281 let |
282 val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => |
282 val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => |
283 Free (Pname, cargTs ---> HOLogic.boolT)) |
283 Free (Pname, cargTs ---> HOLogic.boolT)) |
284 (mutual_induct_Pnames (length parts)) |
284 (mutual_induct_Pnames (length parts)) |
285 parts |
285 parts |
286 |
286 |
287 fun mk_P (MutualPart {cargTs, ...}) P = |
287 fun mk_P (MutualPart {cargTs, ...}) P = |
288 let |
288 let |
289 val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs |
289 val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs |
290 val atup = foldr1 HOLogic.mk_prod avars |
290 val atup = foldr1 HOLogic.mk_prod avars |
291 in |
291 in |
292 tupled_lambda atup (list_comb (P, avars)) |
292 tupled_lambda atup (list_comb (P, avars)) |
293 end |
293 end |
294 |
294 |
295 val Ps = map2 mk_P parts newPs |
295 val Ps = map2 mk_P parts newPs |
296 val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps |
296 val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps |
297 |
297 |
298 val induct_inst = |
298 val induct_inst = |
299 forall_elim (cterm_of thy case_exp) induct |
299 forall_elim (cterm_of thy case_exp) induct |
300 |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules)) |
300 |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules)) |
301 |> full_simplify (HOL_basic_ss addsimps all_f_defs) |
301 |> full_simplify (HOL_basic_ss addsimps all_f_defs) |
302 |
302 |
303 fun mk_proj rule (MutualPart {cargTs, pthA, ...}) = |
303 fun mk_proj rule (MutualPart {cargTs, pthA, ...}) = |
304 let |
304 let |
305 val afs = map_index (fn (i,T) => Free ("a" ^ string_of_int i, T)) cargTs |
305 val afs = map_index (fn (i,T) => Free ("a" ^ string_of_int i, T)) cargTs |
306 val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs) |
306 val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs) |
307 in |
307 in |
308 rule |
308 rule |
309 |> forall_elim (cterm_of thy inj) |
309 |> forall_elim (cterm_of thy inj) |
310 |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules)) |
310 |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules)) |
311 |> fold_rev (forall_intr o cterm_of thy) (afs @ newPs) |
311 |> fold_rev (forall_intr o cterm_of thy) (afs @ newPs) |
312 end |
312 end |
313 |
313 |
314 in |
314 in |
315 map (mk_proj induct_inst) parts |
315 map (mk_proj induct_inst) parts |
316 end |
316 end |
317 |
317 |
318 |
318 |
319 |
319 |
320 |
320 |
321 |
321 |
322 fun mk_partial_rules_mutual lthy (m as Mutual {RST, parts, streeR, fqgars, ...}) data prep_result = |
322 fun mk_partial_rules_mutual lthy (m as Mutual {RST, parts, streeR, fqgars, ...}) data prep_result = |
323 let |
323 let |
324 val thy = ProofContext.theory_of lthy |
324 val thy = ProofContext.theory_of lthy |
325 |
325 |
326 (* FIXME !? *) |
326 (* FIXME !? *) |
327 val expand = Assumption.export false lthy (LocalTheory.target_of lthy); |
327 val expand = Assumption.export false lthy (LocalTheory.target_of lthy) |
328 val expand_term = Drule.term_rule thy expand; |
328 val expand_term = Drule.term_rule thy expand |
329 |
329 |
330 val result = FundefProof.mk_partial_rules thy data prep_result |
330 val result = FundefProof.mk_partial_rules thy data prep_result |
331 val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result |
331 val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result |
332 |
332 |
333 val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} => |
333 val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} => |
334 mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def))) |
334 mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def))) |
335 parts |
335 parts |
336 |
336 |
337 fun mk_mpsimp fqgar sum_psimp = |
337 fun mk_mpsimp fqgar sum_psimp = |
338 in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp |
338 in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp |
339 |
339 |
340 val mpsimps = map2 mk_mpsimp fqgars psimps |
340 val mpsimps = map2 mk_mpsimp fqgars psimps |
341 |
341 |
342 val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m |
342 val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m |
343 val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro |
343 val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro |
344 in |
344 in |
345 FundefMResult { f=expand_term f, G=expand_term G, R=expand_term R, |
345 FundefMResult { f=expand_term f, G=expand_term G, R=expand_term R, |
346 psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts, |
346 psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts, |
347 cases=expand completeness, termination=expand termination, |
347 cases=expand completeness, termination=expand termination, |
348 domintros=map expand dom_intros } |
348 domintros=map expand dom_intros } |
349 end |
349 end |
350 |
350 |
351 |
351 |
352 |
352 |
353 (* puts an object in the "right bucket" *) |
353 (* puts an object in the "right bucket" *) |
354 fun store_grouped P x [] = [] |
354 fun store_grouped P x [] = [] |
355 | store_grouped P x ((l, xs)::bs) = |
355 | store_grouped P x ((l, xs)::bs) = |
356 if P (x, l) then ((l, x::xs)::bs) else ((l, xs)::store_grouped P x bs) |
356 if P (x, l) then ((l, x::xs)::bs) else ((l, xs)::store_grouped P x bs) |
357 |
357 |
358 fun sort_by_function (Mutual {fqgars, ...}) names xs = |
358 fun sort_by_function (Mutual {fqgars, ...}) names xs = |
359 fold_rev (store_grouped (eq_str o apfst fst)) (* fill *) |
359 fold_rev (store_grouped (eq_str o apfst fst)) (* fill *) |
360 (map name_of_fqgar fqgars ~~ xs) (* the name-thm pairs *) |
360 (map name_of_fqgar fqgars ~~ xs) (* the name-thm pairs *) |
361 (map (rpair []) names) (* in the empty buckets labeled with names *) |
361 (map (rpair []) names) (* in the empty buckets labeled with names *) |
362 |
362 |
363 |> map (snd #> map snd) (* and remove the labels afterwards *) |
363 |> map (snd #> map snd) (* and remove the labels afterwards *) |
364 |
364 |
365 end |
365 end |