230 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) = |
230 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) = |
231 define_raw_fvs raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses |
231 define_raw_fvs raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses |
232 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b |
232 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b |
233 |
233 |
234 val _ = trace_msg (K "Defining alpha relations...") |
234 val _ = trace_msg (K "Defining alpha relations...") |
235 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, alpha_result, lthy4) = |
235 val (alpha_result, lthy4) = |
236 define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c |
236 define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c |
237 |
237 |
238 val _ = tracing ("alpha_induct\n" ^ Syntax.string_of_term lthy3c (prop_of alpha_induct)) |
|
239 val _ = tracing ("alpha_intros\n" ^ cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_intros)) |
|
240 |
|
241 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
|
242 |
|
243 val _ = trace_msg (K "Proving distinct theorems...") |
238 val _ = trace_msg (K "Proving distinct theorems...") |
244 val alpha_distincts = |
239 val alpha_distincts = |
245 raw_prove_alpha_distincts lthy4 alpha_result raw_distinct_thms raw_dt_names |
240 raw_prove_alpha_distincts lthy4 alpha_result raw_distinct_thms raw_dt_names |
246 |
241 |
247 val _ = trace_msg (K "Proving eq-iff theorems...") |
242 val _ = trace_msg (K "Proving eq-iff theorems...") |
265 |> map (fn thm => thm RS @{thm sym}) |
260 |> map (fn thm => thm RS @{thm sym}) |
266 |
261 |
267 val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) |
262 val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) |
268 |
263 |
269 val alpha_eqvt = |
264 val alpha_eqvt = |
270 Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 |
265 let |
|
266 val AlphaResult {alpha_trms, alpha_bn_trms, alpha_raw_induct, alpha_intros, ...} = alpha_result |
|
267 in |
|
268 Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_raw_induct alpha_intros lthy5 |
|
269 end |
271 |
270 |
272 val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt |
271 val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt |
273 |
272 |
274 val _ = trace_msg (K "Proving equivalence of alpha...") |
273 val _ = trace_msg (K "Proving equivalence of alpha...") |
275 val alpha_refl_thms = raw_prove_refl lthy5 alpha_result raw_induct_thm |
274 val alpha_refl_thms = raw_prove_refl lthy5 alpha_result raw_induct_thm |
279 |
278 |
280 val (alpha_equivp_thms, alpha_bn_equivp_thms) = |
279 val (alpha_equivp_thms, alpha_bn_equivp_thms) = |
281 raw_prove_equivp lthy5 alpha_result alpha_refl_thms alpha_sym_thms alpha_trans_thms |
280 raw_prove_equivp lthy5 alpha_result alpha_refl_thms alpha_sym_thms alpha_trans_thms |
282 |
281 |
283 val _ = trace_msg (K "Proving alpha implies bn...") |
282 val _ = trace_msg (K "Proving alpha implies bn...") |
284 val alpha_bn_imp_thms = |
283 val alpha_bn_imp_thms = raw_prove_bn_imp lthy5 alpha_result |
285 raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 |
|
286 |
|
287 val _ = tracing ("alpha_bn_imp_thms:\n" ^ cat_lines (map (Syntax.string_of_term lthy5 o prop_of) alpha_bn_imp_thms)) |
|
288 |
284 |
289 val _ = trace_msg (K "Proving respectfulness...") |
285 val _ = trace_msg (K "Proving respectfulness...") |
290 val raw_funs_rsp_aux = |
286 val raw_funs_rsp_aux = |
291 raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
287 raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) |
292 raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy5 |
|
293 |
288 |
294 val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux |
289 val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux |
295 |
290 |
296 val raw_size_rsp = |
291 val raw_size_rsp = |
297 raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct |
292 raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt) |
298 (raw_size_thms @ raw_size_eqvt) lthy5 |
|
299 |> map mk_funs_rsp |
293 |> map mk_funs_rsp |
300 |
294 |
301 val raw_constrs_rsp = |
295 val raw_constrs_rsp = |
302 raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros |
296 raw_constrs_rsp lthy5 alpha_result (flat raw_constrs) (alpha_bn_imp_thms @ raw_funs_rsp_aux) |
303 (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy5 |
|
304 |
297 |
305 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
298 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
306 |
299 |
307 val alpha_bn_rsp = |
300 val alpha_bn_rsp = |
308 raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms |
301 raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms |
309 |
302 |
310 val raw_perm_bn_rsp = |
303 val raw_perm_bn_rsp =raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps |
311 raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct |
|
312 alpha_intros raw_perm_bn_simps lthy5 |
|
313 |
304 |
314 (* noting the quot_respects lemmas *) |
305 (* noting the quot_respects lemmas *) |
315 val (_, lthy6) = |
306 val (_, lthy6) = |
316 Local_Theory.note ((Binding.empty, [rsp_attr]), |
307 Local_Theory.note ((Binding.empty, [rsp_attr]), |
317 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ |
308 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ |
319 |
310 |
320 val _ = trace_msg (K "Defining the quotient types...") |
311 val _ = trace_msg (K "Defining the quotient types...") |
321 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
312 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
322 |
313 |
323 val (qty_infos, lthy7) = |
314 val (qty_infos, lthy7) = |
324 define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 |
315 let |
|
316 val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result |
|
317 in |
|
318 define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 |
|
319 end |
325 |
320 |
326 val qtys = map #qtyp qty_infos |
321 val qtys = map #qtyp qty_infos |
327 val qty_full_names = map (fst o dest_Type) qtys |
322 val qty_full_names = map (fst o dest_Type) qtys |
328 val qty_names = map Long_Name.base_name qty_full_names |
323 val qty_names = map Long_Name.base_name qty_full_names |
329 |
324 |
339 |
334 |
340 val qfv_bns_descr = |
335 val qfv_bns_descr = |
341 map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_fv_bns |
336 map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_fv_bns |
342 |
337 |
343 val qalpha_bns_descr = |
338 val qalpha_bns_descr = |
344 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs alpha_bn_trms |
339 let |
|
340 val AlphaResult {alpha_bn_trms, ...} = alpha_result |
|
341 in |
|
342 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs alpha_bn_trms |
|
343 end |
345 |
344 |
346 val qperm_descr = |
345 val qperm_descr = |
347 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs |
346 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs |
348 |
347 |
349 val qsize_descr = |
348 val qsize_descr = |
482 ||>> Local_Theory.note ((thms_suffix "strong_induct", [case_names_attr]), qstrong_induct_thms) |
481 ||>> Local_Theory.note ((thms_suffix "strong_induct", [case_names_attr]), qstrong_induct_thms) |
483 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
482 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
484 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
483 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
485 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
484 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
486 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
485 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
487 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |
|
488 ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) |
486 ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) |
489 ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) |
487 ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) |
490 ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) |
488 ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) |
491 ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms) |
489 ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms) |
492 in |
490 in |