129 val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts |
129 val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts |
130 val dt_full_names = map (Long_Name.qualify thy_name) dt_names |
130 val dt_full_names = map (Long_Name.qualify thy_name) dt_names |
131 val dt_full_names' = add_raws dt_full_names |
131 val dt_full_names' = add_raws dt_full_names |
132 val dts_env = dt_full_names ~~ dt_full_names' |
132 val dts_env = dt_full_names ~~ dt_full_names' |
133 |
133 |
134 val cnstrs = get_cnstr_strs dts |
134 val cnstr_names = get_cnstr_strs dts |
135 val cnstrs_ty = get_typed_cnstrs dts |
135 val cnstr_tys = get_typed_cnstrs dts |
136 val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs |
136 val cnstr_full_names = map (Long_Name.qualify thy_name) cnstr_names |
137 val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name |
137 val cnstr_full_names' = map (fn (x, y) => Long_Name.qualify thy_name |
138 (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty |
138 (Long_Name.qualify (add_raw x) (add_raw y))) cnstr_tys |
139 val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names' |
139 val cnstrs_env = cnstr_full_names ~~ cnstr_full_names' |
140 |
140 |
141 val bn_fun_strs = get_bn_fun_strs bn_funs |
141 val bn_fun_strs = get_bn_fun_strs bn_funs |
142 val bn_fun_strs' = add_raws bn_fun_strs |
142 val bn_fun_strs' = add_raws bn_fun_strs |
143 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' |
143 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' |
144 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) |
144 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) |
172 ML {* |
172 ML {* |
173 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = |
173 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = |
174 let |
174 let |
175 (* definition of the raw datatypes *) |
175 (* definition of the raw datatypes *) |
176 val _ = warning "Definition of raw datatypes"; |
176 val _ = warning "Definition of raw datatypes"; |
177 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
177 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy0) = |
178 if get_STEPS lthy > 0 |
178 if get_STEPS lthy > 0 |
179 then define_raw_dts dts bn_funs bn_eqs bclauses lthy |
179 then define_raw_dts dts bn_funs bn_eqs bclauses lthy |
180 else raise TEST lthy |
180 else raise TEST lthy |
181 |
181 |
182 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
182 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
538 |
538 |
539 (* proving the strong exhausts and induct lemmas *) |
539 (* proving the strong exhausts and induct lemmas *) |
540 val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs' |
540 val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs' |
541 qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms |
541 qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms |
542 |
542 |
543 val qstrong_induct_thms = prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses |
543 val qstrong_induct_thms = prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses |
544 |
544 |
545 |
545 |
546 (* noting the theorems *) |
546 (* noting the theorems *) |
547 |
547 |
548 (* generating the prefix for the theorem names *) |
548 (* generating the prefix for the theorem names *) |
549 val thms_name = |
549 val thms_name = |
550 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
550 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
551 fun thms_suffix s = Binding.qualified true s thms_name |
551 fun thms_suffix s = Binding.qualified true s thms_name |
|
552 val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names)) |
552 |
553 |
553 val (_, lthy9') = lthyC |
554 val (_, lthy9') = lthyC |
554 |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) |
555 |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) |
555 ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs') |
556 ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs') |
556 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
557 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
557 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
558 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
558 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
559 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
559 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
560 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
560 ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps) |
561 ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps) |
561 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
562 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
562 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
563 ||>> Local_Theory.note ((thms_suffix "induct", [case_names_attr]), [qinduct]) |
563 ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) |
564 ||>> Local_Theory.note ((thms_suffix "inducts", [case_names_attr]), qinducts) |
564 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
565 ||>> Local_Theory.note ((thms_suffix "exhaust", [case_names_attr]), qexhausts) |
565 ||>> Local_Theory.note ((thms_suffix "strong_exhaust", []), qstrong_exhaust_thms) |
566 ||>> Local_Theory.note ((thms_suffix "strong_exhaust", [case_names_attr]), qstrong_exhaust_thms) |
566 ||>> Local_Theory.note ((thms_suffix "strong_induct", []), qstrong_induct_thms) |
567 ||>> Local_Theory.note ((thms_suffix "strong_induct", [case_names_attr]), qstrong_induct_thms) |
567 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
568 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
568 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
569 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
569 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
570 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
570 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
571 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
571 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |
572 ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros) |