author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Thu, 18 Feb 2010 13:36:38 +0100 | |
changeset 1191 | 15362b433d64 |
parent 1185 | 7566b899ca6a |
child 1192 | 6fd072d3acd2 |
permissions | -rw-r--r-- |
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Fv |
1178 | 2 |
imports "Nominal2_Atoms" |
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
1169
b9d02e0800e9
Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1168
diff
changeset
|
5 |
(* Bindings are given as a list which has a length being equal |
1172
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
6 |
to the length of the number of constructors. |
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
7 |
|
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
8 |
Each element is a list whose length is equal to the number |
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
9 |
of arguents. |
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
10 |
|
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
11 |
Every element specifies bindings of this argument given as |
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
12 |
a tuple: function, bound argument. |
1169
b9d02e0800e9
Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1168
diff
changeset
|
13 |
|
b9d02e0800e9
Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1168
diff
changeset
|
14 |
Eg: |
b9d02e0800e9
Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1168
diff
changeset
|
15 |
nominal_datatype |
b9d02e0800e9
Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1168
diff
changeset
|
16 |
|
b9d02e0800e9
Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1168
diff
changeset
|
17 |
C1 |
b9d02e0800e9
Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1168
diff
changeset
|
18 |
| C2 x y z bind x in z |
1172
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
19 |
| C3 x y z bind f x in z bind g y in z |
1169
b9d02e0800e9
Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1168
diff
changeset
|
20 |
|
b9d02e0800e9
Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1168
diff
changeset
|
21 |
yields: |
1172
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
22 |
[ |
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
23 |
[], |
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
24 |
[[], [], [(NONE, 0)]], |
1173
9cb99a28b40e
Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1172
diff
changeset
|
25 |
[[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]] |
1185
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
26 |
|
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
27 |
A SOME binding has to have a function returning an atom set, |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
28 |
and a NONE binding has to be on an argument that is an atom |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
29 |
or an atom set. |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
30 |
|
1191
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
31 |
How the procedure works: |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
32 |
For each of the defined datatypes, |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
33 |
For each of the constructors, |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
34 |
It creates a union of free variables for each argument. |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
35 |
|
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
36 |
For an argument the free variables are the variables minus |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
37 |
bound variables. |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
38 |
|
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
39 |
The variables are: |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
40 |
For an atom, a singleton set with the atom itself. |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
41 |
For an atom set, the atom set itself. |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
42 |
For a recursive argument, the appropriate fv function applied to it. |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
43 |
(* TODO: This one is not implemented *) |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
44 |
For other arguments it should be an appropriate fv function stored |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
45 |
in the database. |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
46 |
The bound variables are a union of results of all bindings that |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
47 |
involve the given argument. For a paricular binding the result is: |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
48 |
For a function applied to an argument this function with the argument. |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
49 |
For an atom, a singleton set with the atom itself. |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
50 |
For an atom set, the atom set itself. |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
51 |
For a recursive argument, the appropriate fv function applied to it. |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
52 |
(* TODO: This one is not implemented *) |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
53 |
For other arguments it should be an appropriate fv function stored |
15362b433d64
Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1185
diff
changeset
|
54 |
in the database. |
1169
b9d02e0800e9
Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1168
diff
changeset
|
55 |
*) |
b9d02e0800e9
Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1168
diff
changeset
|
56 |
|
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
57 |
ML {* |
1175 | 58 |
open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
1178 | 59 |
(* TODO: It is the same as one in 'nominal_atoms' *) |
1175 | 60 |
fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom}); |
61 |
val noatoms = @{term "{} :: atom set"}; |
|
62 |
fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]; |
|
63 |
fun mk_union sets = |
|
64 |
fold (fn a => fn b => |
|
65 |
if a = noatoms then b else |
|
66 |
if b = noatoms then a else |
|
67 |
HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms; |
|
68 |
fun mk_diff a b = |
|
69 |
if b = noatoms then a else |
|
70 |
if b = a then noatoms else |
|
71 |
HOLogic.mk_binop @{const_name minus} (a, b); |
|
1185
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
72 |
fun mk_atoms t = |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
73 |
let |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
74 |
val ty = fastype_of t; |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
75 |
val atom_ty = HOLogic.dest_setT ty --> @{typ atom}; |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
76 |
val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
77 |
in |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
78 |
(Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
79 |
end; |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
80 |
(* Copy from Term *) |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
81 |
fun is_funtype (Type ("fun", [_, _])) = true |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
82 |
| is_funtype _ = false; |
1175 | 83 |
*} |
84 |
||
85 |
ML {* |
|
1178 | 86 |
(* Currently needs just one full_tname to access Datatype *) |
87 |
fun define_raw_fv full_tname bindsall lthy = |
|
88 |
let |
|
1185
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
89 |
val thy = ProofContext.theory_of lthy; |
1178 | 90 |
val {descr, ...} = Datatype.the_info thy full_tname; |
91 |
val sorts = []; (* TODO *) |
|
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
92 |
fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
93 |
val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
94 |
"fv_" ^ name_of_typ (nth_dtyp i)) descr); |
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
95 |
val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
96 |
val fv_frees = map Free (fv_names ~~ fv_types); |
1173
9cb99a28b40e
Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1172
diff
changeset
|
97 |
fun fv_eq_constr i (cname, dts) bindcs = |
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
98 |
let |
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
99 |
val Ts = map (typ_of_dtyp descr sorts) dts; |
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
100 |
val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
101 |
val args = map Free (names ~~ Ts); |
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
102 |
val c = Const (cname, Ts ---> (nth_dtyp i)); |
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
103 |
val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"}); |
1177
6f01720fe520
Add bindings of recursive types by free_variables.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1176
diff
changeset
|
104 |
fun fv_bind (NONE, i) = |
6f01720fe520
Add bindings of recursive types by free_variables.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1176
diff
changeset
|
105 |
if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
6f01720fe520
Add bindings of recursive types by free_variables.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1176
diff
changeset
|
106 |
(* TODO we assume that all can be 'atomized' *) |
1185
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
107 |
if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else |
1177
6f01720fe520
Add bindings of recursive types by free_variables.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1176
diff
changeset
|
108 |
mk_single_atom (nth args i) |
1174 | 109 |
| fv_bind (SOME f, i) = f $ (nth args i); |
1173
9cb99a28b40e
Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1172
diff
changeset
|
110 |
fun fv_arg ((dt, x), bindxs) = |
1172
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
111 |
let |
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
112 |
val arg = |
1175 | 113 |
if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
1174 | 114 |
(* TODO: we just assume everything can be 'atomized' *) |
1185
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
115 |
if (is_funtype o fastype_of) x then mk_atoms x else |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
116 |
HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x] |
1173
9cb99a28b40e
Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1172
diff
changeset
|
117 |
val sub = mk_union (map fv_bind bindxs) |
1172
9a609fefcf24
Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1169
diff
changeset
|
118 |
in |
1173
9cb99a28b40e
Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1172
diff
changeset
|
119 |
mk_diff arg sub |
9cb99a28b40e
Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1172
diff
changeset
|
120 |
end; |
1176
29c4a0cf9237
Bindings adapted to multiple defined datatypes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1175
diff
changeset
|
121 |
val _ = tracing ("d" ^ string_of_int (length dts)); |
29c4a0cf9237
Bindings adapted to multiple defined datatypes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1175
diff
changeset
|
122 |
val _ = tracing (string_of_int (length args)); |
29c4a0cf9237
Bindings adapted to multiple defined datatypes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1175
diff
changeset
|
123 |
val _ = tracing (string_of_int (length bindcs)); |
1173
9cb99a28b40e
Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1172
diff
changeset
|
124 |
in |
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
125 |
(Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
1173
9cb99a28b40e
Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1172
diff
changeset
|
126 |
(fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))) |
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
127 |
end; |
1176
29c4a0cf9237
Bindings adapted to multiple defined datatypes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1175
diff
changeset
|
128 |
fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds; |
29c4a0cf9237
Bindings adapted to multiple defined datatypes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1175
diff
changeset
|
129 |
val fv_eqs = flat (map2 fv_eq descr bindsall) |
1178 | 130 |
in |
131 |
snd (Primrec.add_primrec |
|
132 |
(map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy) |
|
133 |
end |
|
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
134 |
*} |
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
135 |
|
1185
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
136 |
(* tests: |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
137 |
|
1178 | 138 |
atom_decl name |
139 |
||
1185
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
140 |
datatype ty = |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
141 |
Var "name set" |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
142 |
|
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
143 |
ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *} |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
144 |
|
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
145 |
local_setup {* define_raw_fv "Fv.ty" [[[[]]]] *} |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
146 |
print_theorems |
7566b899ca6a
Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1180
diff
changeset
|
147 |
|
1178 | 148 |
datatype rtrm1 = |
149 |
rVr1 "name" |
|
150 |
| rAp1 "rtrm1" "rtrm1" |
|
151 |
| rLm1 "name" "rtrm1" --"name is bound in trm1" |
|
152 |
| rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
|
153 |
and bp = |
|
154 |
BUnit |
|
155 |
| BVr "name" |
|
156 |
| BPr "bp" "bp" |
|
157 |
||
158 |
(* to be given by the user *) |
|
159 |
||
160 |
primrec |
|
161 |
bv1 |
|
162 |
where |
|
163 |
"bv1 (BUnit) = {}" |
|
164 |
| "bv1 (BVr x) = {atom x}" |
|
165 |
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
|
166 |
||
167 |
local_setup {* define_raw_fv "Fv.rtrm1" |
|
168 |
[[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], |
|
169 |
[[], [[]], [[], []]]] *} |
|
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
170 |
print_theorems |
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
171 |
|
1180 | 172 |
*) |
173 |
||
1168
5c1e16806901
Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
174 |
end |