320 val raw_induct_thms = #inducts dtinfo; |
320 val raw_induct_thms = #inducts dtinfo; |
321 val exhaust_thms = map #exhaust dtinfos; |
321 val exhaust_thms = map #exhaust dtinfos; |
322 val raw_size_trms = map (fn ty => Const (@{const_name size}, ty --> @{typ nat})) all_raw_tys |
322 val raw_size_trms = map (fn ty => Const (@{const_name size}, ty --> @{typ nat})) all_raw_tys |
323 val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) |
323 val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) |
324 |> `(fn thms => (length thms) div 2) |
324 |> `(fn thms => (length thms) div 2) |
325 |> (uncurry drop) |
325 |> uncurry drop |
326 |
326 |
327 |
327 |
328 (* definitions of raw permutations *) |
328 (* definitions of raw permutations *) |
329 val _ = warning "Definition of raw permutations"; |
329 val _ = warning "Definition of raw permutations"; |
330 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) = |
330 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) = |
440 |
440 |
441 (* auxiliary lemmas for respectfulness proofs *) |
441 (* auxiliary lemmas for respectfulness proofs *) |
442 val raw_funs_rsp = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
442 val raw_funs_rsp = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
443 raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6 |
443 raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6 |
444 |
444 |
|
445 val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct |
|
446 (raw_size_thms @ raw_size_eqvt) lthy6 |
|
447 |
445 |
448 |
446 (* defining the quotient type *) |
449 (* defining the quotient type *) |
447 val _ = warning "Declaring the quotient types" |
450 val _ = warning "Declaring the quotient types" |
448 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
451 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
449 val qty_binds = map (fn (_, bind, _, _) => bind) dts |
452 val qty_binds = map (fn (_, bind, _, _) => bind) dts |
502 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
505 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
503 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
506 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
504 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
507 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
505 ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp) |
508 ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp) |
506 ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt) |
509 ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt) |
|
510 ||>> Local_Theory.note ((@{binding "size_simps"}, []), raw_size_thms) |
|
511 ||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp) |
507 ||>> Local_Theory.note ((@{binding "alpha_sym_thms"}, []), alpha_sym_thms) |
512 ||>> Local_Theory.note ((@{binding "alpha_sym_thms"}, []), alpha_sym_thms) |
508 ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms) |
513 ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms) |
509 |
514 |
510 val _ = |
515 val _ = |
511 if get_STEPS lthy > 17 |
516 if get_STEPS lthy > 17 |