263 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
263 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
264 if get_STEPS lthy > 0 |
264 if get_STEPS lthy > 0 |
265 then define_raw_dts dts bn_funs bn_eqs bclauses lthy |
265 then define_raw_dts dts bn_funs bn_eqs bclauses lthy |
266 else raise TEST lthy |
266 else raise TEST lthy |
267 |
267 |
268 val _ = tracing ("raw_bn_funs\n" ^ cat_lines (map (@{make_string} o #1) raw_bn_funs)) |
|
269 |
|
270 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
268 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
271 val {descr, sorts, ...} = dtinfo |
269 val {descr, sorts, ...} = dtinfo |
272 |
270 |
273 val raw_tys = all_dtyps descr sorts |
271 val raw_tys = all_dtyps descr sorts |
274 val raw_full_ty_names = map (fst o dest_Type) raw_tys |
272 val raw_full_ty_names = map (fst o dest_Type) raw_tys |
307 if get_STEPS lthy3 > 1 |
305 if get_STEPS lthy3 > 1 |
308 then define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
306 then define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
309 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
307 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
310 else raise TEST lthy3 |
308 else raise TEST lthy3 |
311 |
309 |
312 (* |
|
313 val _ = tracing ("RAW_BNS\n" ^ cat_lines (map (Syntax.string_of_term lthy3) raw_bns)) |
|
314 val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map (Syntax.string_of_term lthy3 o #1) raw_bn_info)) |
|
315 val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map @{make_string} raw_bn_info)) |
|
316 *) |
|
317 |
|
318 (* defining the permute_bn functions *) |
310 (* defining the permute_bn functions *) |
319 val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = |
311 val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = |
320 if get_STEPS lthy3a > 2 |
312 if get_STEPS lthy3a > 2 |
321 then define_raw_bn_perms raw_tys raw_bn_info raw_cns_info |
313 then define_raw_bn_perms raw_tys raw_bn_info raw_cns_info |
322 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a |
314 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a |
491 map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns |
483 map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns |
492 |
484 |
493 val qalpha_bns_descr = |
485 val qalpha_bns_descr = |
494 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms |
486 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms |
495 |
487 |
496 (* |
|
497 val _ = tracing ("raw_bn_info\n" ^ cat_lines (map (Syntax.string_of_term lthy7 o #1) raw_bn_info)) |
|
498 val _ = tracing ("bn_funs\n" ^ cat_lines (map (@{make_string} o #1) bn_funs)) |
|
499 val _ = tracing ("raw_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_bns)) |
|
500 val _ = tracing ("raw_fv_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_fv_bns)) |
|
501 val _ = tracing ("alpha_bn_trms\n" ^ cat_lines (map (Syntax.string_of_term lthy7) alpha_bn_trms)) |
|
502 *) |
|
503 |
|
504 val qperm_descr = |
488 val qperm_descr = |
505 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs |
489 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs |
506 |
490 |
507 val qsize_descr = |
491 val qsize_descr = |
508 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
492 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
557 ||>> lift_thms qtys [] raw_bn_defs |
541 ||>> lift_thms qtys [] raw_bn_defs |
558 ||>> lift_thms qtys [] raw_perm_simps |
542 ||>> lift_thms qtys [] raw_perm_simps |
559 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
543 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
560 else raise TEST lthy9a |
544 else raise TEST lthy9a |
561 |
545 |
562 val (((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), lthyB) = |
546 val ((((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), qalpha_refl_thms), lthyB) = |
563 if get_STEPS lthy > 28 |
547 if get_STEPS lthy > 28 |
564 then |
548 then |
565 lthyA |
549 lthyA |
566 |> lift_thms qtys [] raw_size_eqvt |
550 |> lift_thms qtys [] raw_size_eqvt |
567 ||>> lift_thms qtys [] [raw_induct_thm] |
551 ||>> lift_thms qtys [] [raw_induct_thm] |
568 ||>> lift_thms qtys [] raw_exhaust_thms |
552 ||>> lift_thms qtys [] raw_exhaust_thms |
569 ||>> lift_thms qtys [] raw_size_thms |
553 ||>> lift_thms qtys [] raw_size_thms |
570 ||>> lift_thms qtys [] raw_perm_bn_simps |
554 ||>> lift_thms qtys [] raw_perm_bn_simps |
|
555 ||>> lift_thms qtys [] alpha_refl_thms |
571 else raise TEST lthyA |
556 else raise TEST lthyA |
572 |
557 |
573 val qinducts = Project_Rule.projections lthyA qinduct |
558 val qinducts = Project_Rule.projections lthyA qinduct |
574 |
559 |
575 (* supports lemmas *) |
560 (* supports lemmas *) |
624 if get_STEPS lthy > 33 |
609 if get_STEPS lthy > 33 |
625 then prove_bns_finite qtys qbns qinduct qbn_defs lthyC |
610 then prove_bns_finite qtys qbns qinduct qbn_defs lthyC |
626 else [] |
611 else [] |
627 |
612 |
628 (* proving that perm_bns preserve alpha *) |
613 (* proving that perm_bns preserve alpha *) |
629 val qperm_bn_alpha_thms = @{thms TrueI} |
614 val qperm_bn_alpha_thms = |
630 (* if get_STEPS lthy > 33 |
615 if get_STEPS lthy > 33 |
631 then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' lthyC |
616 then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' |
632 else []*) |
617 qalpha_refl_thms lthyC |
633 |
618 else [] |
634 |
619 |
635 (* noting the theorems *) |
620 (* noting the theorems *) |
636 |
621 |
637 (* generating the prefix for the theorem names *) |
622 (* generating the prefix for the theorem names *) |
638 val thms_name = |
623 val thms_name = |