equal
deleted
inserted
replaced
272 in |
272 in |
273 fold fold_fun tys (Abs ("", tyh, abs_rhs)) |
273 fold fold_fun tys (Abs ("", tyh, abs_rhs)) |
274 end; |
274 end; |
275 *} |
275 *} |
276 |
276 |
277 ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *} |
|
278 |
277 |
279 ML {* |
278 ML {* |
280 fun non_rec_binds l = |
279 fun non_rec_binds l = |
281 let |
280 let |
282 fun is_non_rec (SOME (f, false), _, _, _) = SOME f |
281 fun is_non_rec (SOME (f, false), _, _, _) = SOME f |
594 val rhs = mk_pair (rhs_binds, rhs_arg); |
593 val rhs = mk_pair (rhs_binds, rhs_arg); |
595 val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos); |
594 val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos); |
596 val fv = mk_compound_fv fvs; |
595 val fv = mk_compound_fv fvs; |
597 val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos); |
596 val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos); |
598 val alpha = mk_compound_alpha alphas; |
597 val alpha = mk_compound_alpha alphas; |
599 val pi = foldr1 add_perm (distinct (op =) rpis); |
598 val pi = foldr1 (uncurry mk_plus) (distinct (op =) rpis); |
600 val alpha_gen_pre = Const (atyp_const atyp, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
599 val alpha_gen_pre = Const (atyp_const atyp, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
601 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
600 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
602 in |
601 in |
603 alpha_gen |
602 alpha_gen |
604 end |
603 end |
616 val lhs = mk_pair (lhs_binds, arg); |
615 val lhs = mk_pair (lhs_binds, arg); |
617 val rhs_binds = fv_binds args2 rbinds; |
616 val rhs_binds = fv_binds args2 rbinds; |
618 val rhs = mk_pair (rhs_binds, arg2); |
617 val rhs = mk_pair (rhs_binds, arg2); |
619 val alpha = nth alpha_frees (body_index dt); |
618 val alpha = nth alpha_frees (body_index dt); |
620 val fv = nth fv_frees (body_index dt); |
619 val fv = nth fv_frees (body_index dt); |
621 val pi = foldr1 add_perm (distinct (op =) rpis); |
620 val pi = foldr1 (uncurry mk_plus) (distinct (op =) rpis); |
622 val alpha_const = alpha_const_for_binds rbinds; |
621 val alpha_const = alpha_const_for_binds rbinds; |
623 val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
622 val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
624 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
623 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
625 in |
624 in |
626 alpha_gen |
625 alpha_gen |