equal
deleted
inserted
replaced
267 *} |
267 *} |
268 |
268 |
269 ML {* |
269 ML {* |
270 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
270 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
271 let |
271 let |
272 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy2) = |
272 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) = |
273 raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
273 raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
274 |
274 |
|
275 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
|
276 val {descr, sorts, ...} = dtinfo; |
|
277 |
|
278 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
|
279 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1; |
275 in |
280 in |
276 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy2) |
281 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy2) |
277 end |
282 end |
278 *} |
283 *} |
279 |
284 |
488 | "b_fnclauses (S fc) = (b_fnclause fc)" |
493 | "b_fnclauses (S fc) = (b_fnclause fc)" |
489 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
494 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
490 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
495 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
491 | "b_fnclause (K x pat exp) = {atom x}" |
496 | "b_fnclause (K x pat exp) = {atom x}" |
492 |
497 |
|
498 |
493 typ exp_raw |
499 typ exp_raw |
494 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars] |
500 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars] |
495 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] |
501 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] |
496 |
502 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars] |
497 |
503 |
498 |
504 |
499 end |
505 |
500 |
506 |
501 |
507 end |
502 |
508 |
|
509 |
|
510 |