329 |> `(fn thms => (length thms) div 2) |
329 |> `(fn thms => (length thms) div 2) |
330 |> uncurry drop |
330 |> uncurry drop |
331 |
331 |
332 (* definitions of raw permutations *) |
332 (* definitions of raw permutations *) |
333 val _ = warning "Definition of raw permutations"; |
333 val _ = warning "Definition of raw permutations"; |
334 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) = |
334 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = |
335 if get_STEPS lthy0 > 1 |
335 if get_STEPS lthy0 > 1 |
336 then Local_Theory.theory_result |
336 then define_raw_perms raw_full_ty_names raw_tys raw_constrs raw_induct_thm lthy0 |
337 (define_raw_perms raw_full_ty_names raw_tys raw_constrs raw_induct_thm) lthy0 |
|
338 else raise TEST lthy0 |
337 else raise TEST lthy0 |
339 val lthy2a = Named_Target.reinit lthy2 lthy2 |
|
340 |
338 |
341 (* noting the raw permutations as eqvt theorems *) |
339 (* noting the raw permutations as eqvt theorems *) |
342 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a |
340 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a |
343 |
341 |
344 (* definition of raw fv_functions *) |
342 (* definition of raw fv_functions *) |
509 else raise TEST lthy7 |
507 else raise TEST lthy7 |
510 |
508 |
511 (* definition of the quotient permfunctions and pt-class *) |
509 (* definition of the quotient permfunctions and pt-class *) |
512 val lthy9 = |
510 val lthy9 = |
513 if get_STEPS lthy > 18 |
511 if get_STEPS lthy > 18 |
514 then Local_Theory.theory |
512 then define_qperms qtys qty_full_names qperm_descr raw_perm_laws lthy8 |
515 (define_qperms qtys qty_full_names qperm_descr raw_perm_laws) lthy8 |
|
516 else raise TEST lthy8 |
513 else raise TEST lthy8 |
517 |
514 |
518 val lthy9' = |
515 val lthy9a = |
519 if get_STEPS lthy > 19 |
516 if get_STEPS lthy > 19 |
520 then Local_Theory.theory |
517 then define_qsizes qtys qty_full_names qsize_descr lthy9 |
521 (define_qsizes qtys qty_full_names qsize_descr) lthy9 |
|
522 else raise TEST lthy9 |
518 else raise TEST lthy9 |
523 |
|
524 val lthy9a = Named_Target.reinit lthy9' lthy9' |
|
525 |
519 |
526 val qconstrs = map #qconst qconstrs_info |
520 val qconstrs = map #qconst qconstrs_info |
527 val qbns = map #qconst qbns_info |
521 val qbns = map #qconst qbns_info |
528 val qfvs = map #qconst qfvs_info |
522 val qfvs = map #qconst qfvs_info |
529 val qfv_bns = map #qconst qfv_bns_info |
523 val qfv_bns = map #qconst qfv_bns_info |
600 val (qalpha_info, lthy12c) = define_qconsts qtys dd lthy12b; |
594 val (qalpha_info, lthy12c) = define_qconsts qtys dd lthy12b; |
601 val qalpha_bn_trms = map #qconst qalpha_info |
595 val qalpha_bn_trms = map #qconst qalpha_info |
602 val qalphabn_defs = map #def qalpha_info |
596 val qalphabn_defs = map #def qalpha_info |
603 |
597 |
604 val _ = warning "Lifting permutations"; |
598 val _ = warning "Lifting permutations"; |
605 val thy = Local_Theory.exit_global lthy12c; |
|
606 val perm_names = map (fn x => "permute_" ^ x) qty_names |
599 val perm_names = map (fn x => "permute_" ^ x) qty_names |
607 val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs |
600 val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs |
608 (* use Local_Theory.theory_result *) |
601 val lthy13 = define_qperms qtys qty_full_names dd raw_perm_laws lthy12c |
609 val thy' = define_qperms qtys qty_full_names dd raw_perm_laws thy; |
|
610 val lthy13 = Named_Target.init "" thy'; |
|
611 |
602 |
612 val q_name = space_implode "_" qty_names; |
603 val q_name = space_implode "_" qty_names; |
613 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
604 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
614 val _ = warning "Lifting induction"; |
605 val _ = warning "Lifting induction"; |
615 val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs; |
606 val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs; |