21 yields: |
21 yields: |
22 [ |
22 [ |
23 [], |
23 [], |
24 [[], [], [(NONE, 0)]], |
24 [[], [], [(NONE, 0)]], |
25 [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]] |
25 [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]] |
|
26 |
|
27 A SOME binding has to have a function returning an atom set, |
|
28 and a NONE binding has to be on an argument that is an atom |
|
29 or an atom set. |
|
30 |
26 *) |
31 *) |
27 |
32 |
28 ML {* |
33 ML {* |
29 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
34 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
30 (* TODO: It is the same as one in 'nominal_atoms' *) |
35 (* TODO: It is the same as one in 'nominal_atoms' *) |
38 HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms; |
43 HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms; |
39 fun mk_diff a b = |
44 fun mk_diff a b = |
40 if b = noatoms then a else |
45 if b = noatoms then a else |
41 if b = a then noatoms else |
46 if b = a then noatoms else |
42 HOLogic.mk_binop @{const_name minus} (a, b); |
47 HOLogic.mk_binop @{const_name minus} (a, b); |
|
48 fun mk_atoms t = |
|
49 let |
|
50 val ty = fastype_of t; |
|
51 val atom_ty = HOLogic.dest_setT ty --> @{typ atom}; |
|
52 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
|
53 in |
|
54 (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
|
55 end; |
|
56 (* Copy from Term *) |
|
57 fun is_funtype (Type ("fun", [_, _])) = true |
|
58 | is_funtype _ = false; |
43 *} |
59 *} |
44 |
60 |
45 ML {* |
61 ML {* |
46 (* Currently needs just one full_tname to access Datatype *) |
62 (* Currently needs just one full_tname to access Datatype *) |
47 fun define_raw_fv full_tname bindsall lthy = |
63 fun define_raw_fv full_tname bindsall lthy = |
48 let |
64 let |
49 val thy = ProofContext.theory_of lthy |
65 val thy = ProofContext.theory_of lthy; |
50 val {descr, ...} = Datatype.the_info thy full_tname; |
66 val {descr, ...} = Datatype.the_info thy full_tname; |
51 val sorts = []; (* TODO *) |
67 val sorts = []; (* TODO *) |
52 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
68 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
53 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
69 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
54 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
70 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
62 val c = Const (cname, Ts ---> (nth_dtyp i)); |
78 val c = Const (cname, Ts ---> (nth_dtyp i)); |
63 val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"}); |
79 val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"}); |
64 fun fv_bind (NONE, i) = |
80 fun fv_bind (NONE, i) = |
65 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
81 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
66 (* TODO we assume that all can be 'atomized' *) |
82 (* TODO we assume that all can be 'atomized' *) |
|
83 if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else |
67 mk_single_atom (nth args i) |
84 mk_single_atom (nth args i) |
68 | fv_bind (SOME f, i) = f $ (nth args i); |
85 | fv_bind (SOME f, i) = f $ (nth args i); |
69 fun fv_arg ((dt, x), bindxs) = |
86 fun fv_arg ((dt, x), bindxs) = |
70 let |
87 let |
71 val arg = |
88 val arg = |
72 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
89 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
73 (* TODO: we just assume everything can be 'atomized' *) |
90 (* TODO: we just assume everything can be 'atomized' *) |
74 HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] |
91 if (is_funtype o fastype_of) x then mk_atoms x else |
|
92 HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x] |
75 val sub = mk_union (map fv_bind bindxs) |
93 val sub = mk_union (map fv_bind bindxs) |
76 in |
94 in |
77 mk_diff arg sub |
95 mk_diff arg sub |
78 end; |
96 end; |
79 val _ = tracing ("d" ^ string_of_int (length dts)); |
97 val _ = tracing ("d" ^ string_of_int (length dts)); |
89 snd (Primrec.add_primrec |
107 snd (Primrec.add_primrec |
90 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy) |
108 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy) |
91 end |
109 end |
92 *} |
110 *} |
93 |
111 |
94 (* test |
112 (* tests: |
|
113 |
95 atom_decl name |
114 atom_decl name |
|
115 |
|
116 datatype ty = |
|
117 Var "name set" |
|
118 |
|
119 ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *} |
|
120 |
|
121 local_setup {* define_raw_fv "Fv.ty" [[[[]]]] *} |
|
122 print_theorems |
96 |
123 |
97 datatype rtrm1 = |
124 datatype rtrm1 = |
98 rVr1 "name" |
125 rVr1 "name" |
99 | rAp1 "rtrm1" "rtrm1" |
126 | rAp1 "rtrm1" "rtrm1" |
100 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
127 | rLm1 "name" "rtrm1" --"name is bound in trm1" |