247 in |
247 in |
248 (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) |
248 (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) |
249 end |
249 end |
250 *} |
250 *} |
251 |
251 |
252 |
|
253 ML {* |
252 ML {* |
254 (* for testing porposes - to exit the procedure early *) |
253 (* for testing porposes - to exit the procedure early *) |
255 exception TEST of Proof.context |
254 exception TEST of Proof.context |
256 |
255 |
257 val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 100); |
256 val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 100); |
258 |
257 |
259 fun get_STEPS ctxt = Config.get ctxt STEPS |
258 fun get_STEPS ctxt = Config.get ctxt STEPS |
260 *} |
259 *} |
|
260 |
261 |
261 |
262 setup STEPS_setup |
262 setup STEPS_setup |
263 |
263 |
264 ML {* |
264 ML {* |
265 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = |
265 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = |
331 val _ = warning "Distinct theorems"; |
331 val _ = warning "Distinct theorems"; |
332 val alpha_distincts = |
332 val alpha_distincts = |
333 mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys |
333 mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys |
334 |
334 |
335 (* definition of alpha_eq_iff lemmas *) |
335 (* definition of alpha_eq_iff lemmas *) |
336 (* they have a funny shape for the simplifier ---- CHECK WHETHER NEEDED*) |
|
337 val _ = warning "Eq-iff theorems"; |
336 val _ = warning "Eq-iff theorems"; |
338 val (alpha_eq_iff_simps, alpha_eq_iff) = |
337 val alpha_eq_iff = |
339 if get_STEPS lthy > 5 |
338 if get_STEPS lthy > 5 |
340 then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases |
339 then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases |
341 else raise TEST lthy4 |
340 else raise TEST lthy4 |
342 |
341 |
343 (* proving equivariance lemmas for bns, fvs, size and alpha *) |
342 (* proving equivariance lemmas for bns, fvs, size and alpha *) |
540 else raise TEST lthyA |
539 else raise TEST lthyA |
541 |
540 |
542 val qinducts = Project_Rule.projections lthyA qinduct |
541 val qinducts = Project_Rule.projections lthyA qinduct |
543 |
542 |
544 (* supports lemmas *) |
543 (* supports lemmas *) |
|
544 val _ = warning "Proving Supports Lemmas and fs-Instances" |
545 val qsupports_thms = |
545 val qsupports_thms = |
546 if get_STEPS lthy > 28 |
546 if get_STEPS lthy > 28 |
547 then prove_supports lthyB qperm_simps qtrms |
547 then prove_supports lthyB qperm_simps qtrms |
548 else raise TEST lthyB |
548 else raise TEST lthyB |
549 |
549 |
557 val lthyC = |
557 val lthyC = |
558 if get_STEPS lthy > 30 |
558 if get_STEPS lthy > 30 |
559 then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB |
559 then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB |
560 else raise TEST lthyB |
560 else raise TEST lthyB |
561 |
561 |
|
562 (* fv - supp equality *) |
|
563 val _ = warning "Proving Equality between fv and supp" |
|
564 val qfv_supp_thms = |
|
565 if get_STEPS lthy > 31 |
|
566 then prove_fv_supp qtys qfvs qfv_bns qalpha_bns qbn_defs qfv_defs qeq_iffs |
|
567 qperm_simps qfv_qbn_eqvts qinducts (flat raw_bclauses) lthyC |
|
568 else [] |
|
569 |
|
570 |
562 (* noting the theorems *) |
571 (* noting the theorems *) |
563 |
572 |
564 (* generating the prefix for the theorem names *) |
573 (* generating the prefix for the theorem names *) |
565 val thms_name = |
574 val thms_name = |
566 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
575 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
573 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
582 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
574 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
583 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
575 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
584 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
576 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
585 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
577 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
586 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
578 ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) |
587 ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) |
579 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
588 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
580 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
589 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
581 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
590 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
|
591 ||>> Local_Theory.note ((thms_suffix "supp", []), qfv_supp_thms) |
582 in |
592 in |
583 (0, lthy9') |
593 (0, lthy9') |
584 end handle TEST ctxt => (0, ctxt) |
594 end handle TEST ctxt => (0, ctxt) |
585 *} |
595 *} |
|
596 |
586 |
597 |
587 section {* Preparing and parsing of the specification *} |
598 section {* Preparing and parsing of the specification *} |
588 |
599 |
589 ML {* |
600 ML {* |
590 (* generates the parsed datatypes and |
601 (* generates the parsed datatypes and |