7 "Abs" |
7 "Abs" |
8 uses ("nominal_dt_rawperm.ML") |
8 uses ("nominal_dt_rawperm.ML") |
9 ("nominal_dt_rawfuns.ML") |
9 ("nominal_dt_rawfuns.ML") |
10 ("nominal_dt_alpha.ML") |
10 ("nominal_dt_alpha.ML") |
11 ("nominal_dt_quot.ML") |
11 ("nominal_dt_quot.ML") |
|
12 ("nominal_dt_supp.ML") |
12 begin |
13 begin |
13 |
14 |
14 use "nominal_dt_rawperm.ML" |
15 use "nominal_dt_rawperm.ML" |
15 ML {* open Nominal_Dt_RawPerm *} |
16 ML {* open Nominal_Dt_RawPerm *} |
16 |
17 |
21 ML {* open Nominal_Dt_Alpha *} |
22 ML {* open Nominal_Dt_Alpha *} |
22 |
23 |
23 use "nominal_dt_quot.ML" |
24 use "nominal_dt_quot.ML" |
24 ML {* open Nominal_Dt_Quot *} |
25 ML {* open Nominal_Dt_Quot *} |
25 |
26 |
|
27 use "nominal_dt_supp.ML" |
|
28 ML {* open Nominal_Dt_Supp *} |
26 |
29 |
27 section{* Interface for nominal_datatype *} |
30 section{* Interface for nominal_datatype *} |
28 |
31 |
29 ML {* |
32 ML {* |
30 (* attributes *) |
33 (* attributes *) |
31 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
34 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
32 val rsp_attrib = Attrib.internal (K Quotient_Info.rsp_rules_add) |
35 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
|
36 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
33 |
37 |
34 *} |
38 *} |
35 |
39 |
36 ML {* print_depth 50 *} |
40 ML {* print_depth 50 *} |
37 |
41 |
298 if get_STEPS lthy0 > 1 |
302 if get_STEPS lthy0 > 1 |
299 then define_raw_perms raw_full_ty_names raw_tys tvs raw_constrs raw_induct_thm lthy0 |
303 then define_raw_perms raw_full_ty_names raw_tys tvs raw_constrs raw_induct_thm lthy0 |
300 else raise TEST lthy0 |
304 else raise TEST lthy0 |
301 |
305 |
302 (* noting the raw permutations as eqvt theorems *) |
306 (* noting the raw permutations as eqvt theorems *) |
303 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a |
307 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a |
304 |
308 |
305 (* definition of raw fv_functions *) |
309 (* definition of raw fv_functions *) |
306 val _ = warning "Definition of raw fv-functions"; |
310 val _ = warning "Definition of raw fv-functions"; |
307 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) = |
311 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) = |
308 if get_STEPS lthy3 > 2 |
312 if get_STEPS lthy3 > 2 |
343 if get_STEPS lthy > 6 |
347 if get_STEPS lthy > 6 |
344 then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_defs @ raw_perm_simps) lthy4 |
348 then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_defs @ raw_perm_simps) lthy4 |
345 else raise TEST lthy4 |
349 else raise TEST lthy4 |
346 |
350 |
347 (* noting the raw_bn_eqvt lemmas in a temprorary theory *) |
351 (* noting the raw_bn_eqvt lemmas in a temprorary theory *) |
348 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_bn_eqvt) lthy4) |
352 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) lthy4) |
349 |
353 |
350 val raw_fv_eqvt = |
354 val raw_fv_eqvt = |
351 if get_STEPS lthy > 7 |
355 if get_STEPS lthy > 7 |
352 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) |
356 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) |
353 (Local_Theory.restore lthy_tmp) |
357 (Local_Theory.restore lthy_tmp) |
359 (Local_Theory.restore lthy_tmp) |
363 (Local_Theory.restore lthy_tmp) |
360 |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) |
364 |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) |
361 |> map (fn thm => thm RS @{thm sym}) |
365 |> map (fn thm => thm RS @{thm sym}) |
362 else raise TEST lthy4 |
366 else raise TEST lthy4 |
363 |
367 |
364 val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_fv_eqvt) lthy_tmp) |
368 val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) |
365 |
369 |
366 val (alpha_eqvt, lthy6) = |
370 val (alpha_eqvt, lthy6) = |
367 if get_STEPS lthy > 9 |
371 if get_STEPS lthy > 9 |
368 then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 |
372 then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 |
369 else raise TEST lthy4 |
373 else raise TEST lthy4 |
438 else raise TEST lthy6 |
442 else raise TEST lthy6 |
439 |
443 |
440 (* noting the quot_respects lemmas *) |
444 (* noting the quot_respects lemmas *) |
441 val (_, lthy6a) = |
445 val (_, lthy6a) = |
442 if get_STEPS lthy > 21 |
446 if get_STEPS lthy > 21 |
443 then Local_Theory.note ((Binding.empty, [rsp_attrib]), |
447 then Local_Theory.note ((Binding.empty, [rsp_attr]), |
444 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6 |
448 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6 |
445 else raise TEST lthy6 |
449 else raise TEST lthy6 |
446 |
450 |
447 (* defining the quotient type *) |
451 (* defining the quotient type *) |
448 val _ = warning "Declaring the quotient types" |
452 val _ = warning "Declaring the quotient types" |
501 val lthy9a = |
505 val lthy9a = |
502 if get_STEPS lthy > 25 |
506 if get_STEPS lthy > 25 |
503 then define_qsizes qtys qty_full_names tvs qsize_descr lthy9 |
507 then define_qsizes qtys qty_full_names tvs qsize_descr lthy9 |
504 else raise TEST lthy9 |
508 else raise TEST lthy9 |
505 |
509 |
506 val qconstrs = map #qconst qconstrs_info |
510 val qtrms = map #qconst qconstrs_info |
507 val qbns = map #qconst qbns_info |
511 val qbns = map #qconst qbns_info |
508 val qfvs = map #qconst qfvs_info |
512 val qfvs = map #qconst qfvs_info |
509 val qfv_bns = map #qconst qfv_bns_info |
513 val qfv_bns = map #qconst qfv_bns_info |
510 val qalpha_bns = map #qconst qalpha_bns_info |
514 val qalpha_bns = map #qconst qalpha_bns_info |
511 |
515 |
534 |> lift_thms qtys [] raw_size_eqvt |
538 |> lift_thms qtys [] raw_size_eqvt |
535 ||>> lift_thms qtys [] [raw_induct_thm] |
539 ||>> lift_thms qtys [] [raw_induct_thm] |
536 ||>> lift_thms qtys [] raw_exhaust_thms |
540 ||>> lift_thms qtys [] raw_exhaust_thms |
537 else raise TEST lthyA |
541 else raise TEST lthyA |
538 |
542 |
|
543 (* Supports lemmas *) |
|
544 |
|
545 val qsupports_thms = |
|
546 if get_STEPS lthy > 28 |
|
547 then prove_supports lthyB qperm_simps qtrms |
|
548 else raise TEST lthyB |
|
549 |
|
550 |
539 (* noting the theorems *) |
551 (* noting the theorems *) |
540 |
552 |
541 (* generating the prefix for the theorem names *) |
553 (* generating the prefix for the theorem names *) |
542 val thms_name = |
554 val thms_name = |
543 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
555 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
546 val (_, lthy9') = lthyB |
558 val (_, lthy9') = lthyB |
547 |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) |
559 |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) |
548 ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs) |
560 ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs) |
549 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
561 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
550 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
562 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
551 ||>> Local_Theory.note ((thms_suffix "perm_simps", []), qperm_simps) |
563 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
552 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
564 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
553 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
565 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
554 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
566 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
555 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
567 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
|
568 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
556 |
569 |
557 in |
570 in |
558 (0, lthy9') |
571 (0, lthy9') |
559 end handle TEST ctxt => (0, ctxt) |
572 end handle TEST ctxt => (0, ctxt) |
560 *} |
573 *} |