259 |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) |
259 |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) |
260 |> map (fn thm => thm RS @{thm sym}) |
260 |> map (fn thm => thm RS @{thm sym}) |
261 |
261 |
262 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) |
263 |
263 |
264 val (alpha_eqvt, lthy6) = |
264 val alpha_eqvt = |
265 Nominal_Eqvt.raw_equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 |
265 Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 |
|
266 |
|
267 val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt |
266 |
268 |
267 val _ = trace_msg (K "Proving equivalence of alpha...") |
269 val _ = trace_msg (K "Proving equivalence of alpha...") |
268 val alpha_refl_thms = |
270 val alpha_refl_thms = |
269 raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy6 |
271 raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy5 |
270 |
272 |
271 val alpha_sym_thms = |
273 val alpha_sym_thms = |
272 raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy6 |
274 raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct alpha_eqvt_norm lthy5 |
273 |
275 |
274 val alpha_trans_thms = |
276 val alpha_trans_thms = |
275 raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms) |
277 raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms) |
276 alpha_intros alpha_induct alpha_cases lthy6 |
278 alpha_intros alpha_induct alpha_cases alpha_eqvt_norm lthy5 |
277 |
279 |
278 val (alpha_equivp_thms, alpha_bn_equivp_thms) = |
280 val (alpha_equivp_thms, alpha_bn_equivp_thms) = |
279 raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms |
281 raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms |
280 alpha_trans_thms lthy6 |
282 alpha_trans_thms lthy5 |
281 |
283 |
282 val _ = trace_msg (K "Proving alpha implies bn...") |
284 val _ = trace_msg (K "Proving alpha implies bn...") |
283 val alpha_bn_imp_thms = |
285 val alpha_bn_imp_thms = |
284 raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 |
286 raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 |
285 |
287 |
286 val _ = trace_msg (K "Proving respectfulness...") |
288 val _ = trace_msg (K "Proving respectfulness...") |
287 val raw_funs_rsp_aux = |
289 val raw_funs_rsp_aux = |
288 raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
290 raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
289 raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6 |
291 raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy5 |
290 |
292 |
291 val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux |
293 val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux |
292 |
294 |
293 val raw_size_rsp = |
295 val raw_size_rsp = |
294 raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct |
296 raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct |
295 (raw_size_thms @ raw_size_eqvt) lthy6 |
297 (raw_size_thms @ raw_size_eqvt) lthy5 |
296 |> map mk_funs_rsp |
298 |> map mk_funs_rsp |
297 |
299 |
298 val raw_constrs_rsp = |
300 val raw_constrs_rsp = |
299 raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros |
301 raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros |
300 (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 |
302 (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy5 |
301 |
303 |
302 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
304 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
303 |
305 |
304 val alpha_bn_rsp = |
306 val alpha_bn_rsp = |
305 raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms |
307 raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms |
306 |
308 |
307 val raw_perm_bn_rsp = |
309 val raw_perm_bn_rsp = |
308 raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct |
310 raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct |
309 alpha_intros raw_perm_bn_simps lthy6 |
311 alpha_intros raw_perm_bn_simps lthy5 |
310 |
312 |
311 (* noting the quot_respects lemmas *) |
313 (* noting the quot_respects lemmas *) |
312 val (_, lthy6a) = |
314 val (_, lthy6) = |
313 Local_Theory.note ((Binding.empty, [rsp_attr]), |
315 Local_Theory.note ((Binding.empty, [rsp_attr]), |
314 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ |
316 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ |
315 alpha_bn_rsp @ raw_perm_bn_rsp) lthy6 |
317 alpha_bn_rsp @ raw_perm_bn_rsp) lthy5 |
316 |
318 |
317 val _ = trace_msg (K "Defining the quotient types...") |
319 val _ = trace_msg (K "Defining the quotient types...") |
318 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
320 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
319 |
321 |
320 val (qty_infos, lthy7) = |
322 val (qty_infos, lthy7) = |
321 define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a |
323 define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 |
322 |
324 |
323 val qtys = map #qtyp qty_infos |
325 val qtys = map #qtyp qty_infos |
324 val qty_full_names = map (fst o dest_Type) qtys |
326 val qty_full_names = map (fst o dest_Type) qtys |
325 val qty_names = map Long_Name.base_name qty_full_names |
327 val qty_names = map Long_Name.base_name qty_full_names |
326 |
328 |