1 theory Fv |
1 theory Fv |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" |
3 begin |
3 begin |
4 |
|
5 atom_decl name |
|
6 |
|
7 datatype rlam = |
|
8 rVar "name" |
|
9 | rApp "rlam" "rlam" |
|
10 | rLam "name" "rlam" |
|
11 |
|
12 ML {* |
|
13 open Datatype_Aux (* typ_of_dtyp, DtRec, ... *); |
|
14 fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom}) |
|
15 *} |
|
16 |
|
17 ML {* dest_Type @{typ rlam} *} |
|
18 |
4 |
19 (* Bindings are given as a list which has a length being equal |
5 (* Bindings are given as a list which has a length being equal |
20 to the length of the number of constructors. |
6 to the length of the number of constructors. |
21 |
7 |
22 Each element is a list whose length is equal to the number |
8 Each element is a list whose length is equal to the number |
38 [[], [], [(NONE, 0)]], |
24 [[], [], [(NONE, 0)]], |
39 [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]] |
25 [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]] |
40 *) |
26 *) |
41 |
27 |
42 ML {* |
28 ML {* |
|
29 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
|
30 fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom}); |
|
31 val noatoms = @{term "{} :: atom set"}; |
|
32 fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]; |
|
33 fun mk_union sets = |
|
34 fold (fn a => fn b => |
|
35 if a = noatoms then b else |
|
36 if b = noatoms then a else |
|
37 HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms; |
|
38 fun mk_diff a b = |
|
39 if b = noatoms then a else |
|
40 if b = a then noatoms else |
|
41 HOLogic.mk_binop @{const_name minus} (a, b); |
|
42 *} |
|
43 |
|
44 atom_decl name |
|
45 |
|
46 datatype rlam = |
|
47 rVar "name" |
|
48 | rApp "rlam" "rlam" |
|
49 | rLam "name" "rlam" |
|
50 |
|
51 ML {* |
43 val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam"; |
52 val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam"; |
44 val sorts = []; |
53 val sorts = []; |
45 val noatoms = @{term "{} :: atom set"} |
54 val binds = [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]]; |
46 val binds = [[[]], [[], []], [[], [(NONE, 0)]]]; |
|
47 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
55 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
48 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
56 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
49 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
57 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
50 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
58 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
51 val fv_frees = map Free (fv_names ~~ fv_types); |
59 val fv_frees = map Free (fv_names ~~ fv_types); |
52 fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] |
|
53 fun mk_union sets = |
|
54 fold (fn a => fn b => |
|
55 if a = noatoms then b else |
|
56 if b = noatoms then a else |
|
57 HOLogic.mk_binop @{const_name union} (a, b)) sets noatoms; |
|
58 fun mk_diff a b = |
|
59 if b = noatoms then a else |
|
60 HOLogic.mk_binop @{const_name minus} (a, b); |
|
61 fun fv_eq_constr i (cname, dts) bindcs = |
60 fun fv_eq_constr i (cname, dts) bindcs = |
62 let |
61 let |
63 val Ts = map (typ_of_dtyp descr sorts) dts; |
62 val Ts = map (typ_of_dtyp descr sorts) dts; |
64 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
63 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
65 val args = map Free (names ~~ Ts); |
64 val args = map Free (names ~~ Ts); |
69 fun fv_bind (NONE, i) = mk_single_atom (nth args i) |
68 fun fv_bind (NONE, i) = mk_single_atom (nth args i) |
70 | fv_bind (SOME f, i) = f $ (nth args i); |
69 | fv_bind (SOME f, i) = f $ (nth args i); |
71 fun fv_arg ((dt, x), bindxs) = |
70 fun fv_arg ((dt, x), bindxs) = |
72 let |
71 let |
73 val arg = |
72 val arg = |
74 if is_rec_type dt then nth fv_frees (body_index dt) $ x |
73 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
75 (* TODO: we just assume everything can be 'atomized' *) |
74 (* TODO: we just assume everything can be 'atomized' *) |
76 else HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] |
75 HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] |
77 val sub = mk_union (map fv_bind bindxs) |
76 val sub = mk_union (map fv_bind bindxs) |
78 in |
77 in |
79 mk_diff arg sub |
78 mk_diff arg sub |
80 end; |
79 end; |
81 val _ = tracing (string_of_int (length dts)); |
|
82 val _ = tracing (string_of_int (length bindcs)); |
|
83 in |
80 in |
84 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
81 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
85 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))) |
82 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))) |
86 end; |
83 end; |
87 fun fv_eq (i, (_, _, constrs)) = map2 (fv_eq_constr i) constrs binds; |
84 fun fv_eq (i, (_, _, constrs)) = map2 (fv_eq_constr i) constrs binds; |