1 theory NewAlpha |
1 theory NewAlpha |
2 imports "NewFv" |
2 imports "Abs" "Perm" "Nominal2_FSet" |
|
3 uses ("nominal_dt_rawperm.ML") |
|
4 ("nominal_dt_rawfuns.ML") |
3 begin |
5 begin |
|
6 |
|
7 use "nominal_dt_rawperm.ML" |
|
8 use "nominal_dt_rawfuns.ML" |
|
9 |
|
10 ML {* |
|
11 open Nominal_Dt_RawPerm |
|
12 open Nominal_Dt_RawFuns |
|
13 *} |
|
14 |
4 |
15 |
5 ML {* |
16 ML {* |
6 fun mk_binop2 ctxt s (l, r) = |
17 fun mk_binop2 ctxt s (l, r) = |
7 Syntax.check_term ctxt (Const (s, dummyT) $ l $ r) |
18 Syntax.check_term ctxt (Const (s, dummyT) $ l $ r) |
8 *} |
19 *} |
14 |
25 |
15 ML {* |
26 ML {* |
16 fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees |
27 fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees |
17 bn_alphabn alpha_const binds bodys = |
28 bn_alphabn alpha_const binds bodys = |
18 let |
29 let |
19 val thy = ProofContext.theory_of lthy; |
30 fun bind_set args (NONE, no) = setify lthy (nth args no) |
20 fun bind_set args (NONE, no) = setify thy (nth args no) |
|
21 | bind_set args (SOME f, no) = f $ (nth args no) |
31 | bind_set args (SOME f, no) = f $ (nth args no) |
22 fun bind_lst args (NONE, no) = listify thy (nth args no) |
32 fun bind_lst args (NONE, no) = listify lthy (nth args no) |
23 | bind_lst args (SOME f, no) = f $ (nth args no) |
33 | bind_lst args (SOME f, no) = f $ (nth args no) |
24 fun append (t1, t2) = |
34 fun append (t1, t2) = |
25 Const(@{const_name append}, @{typ "atom list \<Rightarrow> atom list \<Rightarrow> atom list"}) $ t1 $ t2; |
35 Const(@{const_name append}, @{typ "atom list \<Rightarrow> atom list \<Rightarrow> atom list"}) $ t1 $ t2; |
26 fun binds_fn args nos = |
36 fun binds_fn args nos = |
27 if alpha_const = @{const_name alpha_lst} |
37 if alpha_const = @{const_name alpha_lst} |
28 then foldr1 append (map (bind_lst args) nos) |
38 then foldr1 append (map (bind_lst args) nos) |
29 else mk_union (map (bind_set args) nos); |
39 else fold_union (map (bind_set args) nos); |
30 val lhs_binds = binds_fn args binds; |
40 val lhs_binds = binds_fn args binds; |
31 val rhs_binds = binds_fn args2 binds; |
41 val rhs_binds = binds_fn args2 binds; |
32 val lhs_bodys = foldr1 HOLogic.mk_prod (map (nth args) bodys); |
42 val lhs_bodys = foldr1 HOLogic.mk_prod (map (nth args) bodys); |
33 val rhs_bodys = foldr1 HOLogic.mk_prod (map (nth args2) bodys); |
43 val rhs_bodys = foldr1 HOLogic.mk_prod (map (nth args2) bodys); |
34 val lhs = HOLogic.mk_prod (lhs_binds, lhs_bodys); |
44 val lhs = HOLogic.mk_prod (lhs_binds, lhs_bodys); |
75 then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2] |
85 then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2] |
76 else [HOLogic.mk_eq (arg, arg2)] |
86 else [HOLogic.mk_eq (arg, arg2)] |
77 | SOME (SOME (f : term)) => [(the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2] |
87 | SOME (SOME (f : term)) => [(the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2] |
78 | SOME NONE => [] |
88 | SOME NONE => [] |
79 end |
89 end |
80 | BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees |
90 | BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees |
81 fv_frees bn_alphabn @{const_name alpha_lst} x y |
91 fv_frees bn_alphabn @{const_name alpha_lst} x y |
82 | BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees |
92 | BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees |
83 fv_frees bn_alphabn @{const_name alpha_gen} x y |
93 fv_frees bn_alphabn @{const_name alpha_gen} x y |
84 | BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees |
94 | BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees |
85 fv_frees bn_alphabn @{const_name alpha_res} x y |
95 fv_frees bn_alphabn @{const_name alpha_res} x y |
86 *} |
96 *} |
87 |
97 |
88 |
98 |
89 ML {* |
99 ML {* |
135 *} |
145 *} |
136 |
146 |
137 ML {* |
147 ML {* |
138 fun alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn bm = |
148 fun alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn bm = |
139 case bm of |
149 case bm of |
140 BEmy i => |
150 BC (_, [], [i]) => |
141 let |
151 let |
142 val arg = nth args i; |
152 val arg = nth args i; |
143 val arg2 = nth args2 i; |
153 val arg2 = nth args2 i; |
144 val dt = nth dts i; |
154 val dt = nth dts i; |
145 in |
155 in |
146 if Datatype_Aux.is_rec_type dt |
156 if Datatype_Aux.is_rec_type dt |
147 then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2] |
157 then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2] |
148 else [HOLogic.mk_eq (arg, arg2)] |
158 else [HOLogic.mk_eq (arg, arg2)] |
149 end |
159 end |
150 | BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees |
160 | BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees |
151 fv_frees bn_alphabn @{const_name alpha_lst} x y |
161 fv_frees bn_alphabn @{const_name alpha_lst} x y |
152 | BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees |
162 | BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees |
153 fv_frees bn_alphabn @{const_name alpha_gen} x y |
163 fv_frees bn_alphabn @{const_name alpha_gen} x y |
154 | BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees |
164 | BC (Res, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees |
155 fv_frees bn_alphabn @{const_name alpha_res} x y |
165 fv_frees bn_alphabn @{const_name alpha_res} x y |
156 *} |
166 *} |
157 |
167 |
158 ML {* |
168 ML {* |
159 fun alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess (alpha_free, ith_dtyp) = |
169 fun alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess (alpha_free, ith_dtyp) = |