1 theory NewAlpha |
1 theory NewAlpha |
2 imports "NewFv" |
2 imports "NewFv" |
3 begin |
3 begin |
4 |
|
5 (* Given [fv1, fv2, fv3] |
|
6 produces %(x, y, z). fv1 x u fv2 y u fv3 z *) |
|
7 ML {* |
|
8 fun mk_compound_fv fvs = |
|
9 let |
|
10 val nos = (length fvs - 1) downto 0; |
|
11 val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos); |
|
12 val fvs_union = mk_union fvs_applied; |
|
13 val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs); |
|
14 fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t)) |
|
15 in |
|
16 fold fold_fun tys (Abs ("", tyh, fvs_union)) |
|
17 end; |
|
18 *} |
|
19 |
|
20 (* Given [R1, R2, R3] |
|
21 produces %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *) |
|
22 ML {* |
|
23 fun mk_compound_alpha Rs = |
|
24 let |
|
25 val nos = (length Rs - 1) downto 0; |
|
26 val nos2 = (2 * length Rs - 1) downto length Rs; |
|
27 val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no) |
|
28 (Rs ~~ (nos2 ~~ nos)); |
|
29 val Rs_conj = foldr1 HOLogic.mk_conj Rs_applied; |
|
30 val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs); |
|
31 fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t)) |
|
32 val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj)) |
|
33 in |
|
34 fold fold_fun tys (Abs ("", tyh, abs_rhs)) |
|
35 end; |
|
36 *} |
|
37 |
4 |
38 ML {* |
5 ML {* |
39 fun mk_binop2 ctxt s (l, r) = |
6 fun mk_binop2 ctxt s (l, r) = |
40 Syntax.check_term ctxt (Const (s, dummyT) $ l $ r) |
7 Syntax.check_term ctxt (Const (s, dummyT) $ l $ r) |
41 *} |
8 *} |
83 val alphas = map alpha_for_dt body_dts; |
50 val alphas = map alpha_for_dt body_dts; |
84 val alpha = mk_compound_alpha' lthy alphas; |
51 val alpha = mk_compound_alpha' lthy alphas; |
85 val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs |
52 val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs |
86 val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre) |
53 val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre) |
87 val t = Syntax.check_term lthy alpha_gen_ex |
54 val t = Syntax.check_term lthy alpha_gen_ex |
88 in |
55 fun alpha_bn_bind (SOME bn, i) = |
89 case binds of |
56 if member (op =) bodys i then NONE |
90 [(SOME bn, i)] => if member (op =) bodys i then [t] |
57 else SOME ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i) |
91 else [t, ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i)] |
58 | alpha_bn_bind (NONE, _) = NONE |
92 | _ => [t] |
59 in |
|
60 t :: (map_filter alpha_bn_bind binds) |
93 end |
61 end |
94 *} |
62 *} |
95 |
63 |
96 ML {* |
64 ML {* |
97 fun alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn args_in_bn bm = |
65 fun alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn args_in_bn bm = |