equal
deleted
inserted
replaced
165 |
165 |
166 |
166 |
167 ML {* |
167 ML {* |
168 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = |
168 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = |
169 let |
169 let |
170 (* definition of the raw datatypes *) |
|
171 val _ = trace_msg (K "Defining raw datatypes...") |
170 val _ = trace_msg (K "Defining raw datatypes...") |
172 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy0) = |
171 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy0) = |
173 define_raw_dts dts bn_funs bn_eqs bclauses lthy |
172 define_raw_dts dts bn_funs bn_eqs bclauses lthy |
174 |
173 |
175 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
174 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
200 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = |
199 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = |
201 define_raw_perms raw_full_ty_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0 |
200 define_raw_perms raw_full_ty_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0 |
202 |
201 |
203 (* noting the raw permutations as eqvt theorems *) |
202 (* noting the raw permutations as eqvt theorems *) |
204 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a |
203 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a |
205 |
|
206 |
204 |
207 val _ = trace_msg (K "Defining raw fv- and bn-functions...") |
205 val _ = trace_msg (K "Defining raw fv- and bn-functions...") |
208 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) = |
206 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) = |
209 define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
207 define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
210 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
208 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
360 val qfvs = map #qconst qfvs_info |
358 val qfvs = map #qconst qfvs_info |
361 val qfv_bns = map #qconst qfv_bns_info |
359 val qfv_bns = map #qconst qfv_bns_info |
362 val qalpha_bns = map #qconst qalpha_bns_info |
360 val qalpha_bns = map #qconst qalpha_bns_info |
363 val qperm_bns = map #qconst qperm_bns_info |
361 val qperm_bns = map #qconst qperm_bns_info |
364 |
362 |
365 val _ = trace_msg (K "Lifting of theorems...") |
363 val _ = trace_msg (K "Lifting of theorems...") |
366 |
|
367 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def |
364 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def |
368 prod.cases} |
365 prod.cases} |
369 |
366 |
370 val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = |
367 val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = |
371 lthy9a |
368 lthy9a |
401 val qfv_supp_thms = |
398 val qfv_supp_thms = |
402 prove_fv_supp qtys (flat qtrms) qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs |
399 prove_fv_supp qtys (flat qtrms) qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs |
403 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
400 qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |
404 |
401 |
405 (* postprocessing of eq and fv theorems *) |
402 (* postprocessing of eq and fv theorems *) |
406 |
|
407 val qeq_iffs' = qeq_iffs |
403 val qeq_iffs' = qeq_iffs |
408 |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms)) |
404 |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms)) |
409 |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
405 |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
410 |
406 |
411 val qsupp_constrs = qfv_defs |
407 val qsupp_constrs = qfv_defs |