equal
deleted
inserted
replaced
275 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
275 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
276 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
276 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
277 val thy = Local_Theory.exit_global lthy2; |
277 val thy = Local_Theory.exit_global lthy2; |
278 val lthy3 = Theory_Target.init NONE thy; |
278 val lthy3 = Theory_Target.init NONE thy; |
279 |
279 |
280 val (_, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
280 val ((fv, fvbn), info, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
281 in |
281 in |
282 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4) |
282 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4) |
283 end |
283 end |
284 *} |
284 *} |
285 |
285 |
458 | Let p::pt t::lam bind_set "bn p" in t |
458 | Let p::pt t::lam bind_set "bn p" in t |
459 and pt = |
459 and pt = |
460 P1 name |
460 P1 name |
461 | P2 pt pt |
461 | P2 pt pt |
462 binder |
462 binder |
463 bn::"pt \<Rightarrow> atom set" |
463 bn::"pt \<Rightarrow> atom set" |
464 where |
464 where |
465 "bn (P1 x) = {atom x}" |
465 "bn (P1 x) = {atom x}" |
466 | "bn (P2 p1 p2) = bn p1 \<union> bn p2" |
466 | "bn (P2 p1 p2) = bn p1 \<union> bn p2" |
467 |
467 |
|
468 thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps |
468 |
469 |
469 nominal_datatype exp = |
470 nominal_datatype exp = |
470 EVar name |
471 EVar name |
471 | EUnit |
472 | EUnit |
472 | EPair q1::exp q2::exp bind_set q1 q2 in q1 q2 |
473 | EPair q1::exp q2::exp bind_set q1 q2 in q1 q2 |