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 |
|
31 How the procedure works: |
|
32 For each of the defined datatypes, |
|
33 For each of the constructors, |
|
34 It creates a union of free variables for each argument. |
|
35 |
|
36 For an argument the free variables are the variables minus |
|
37 bound variables. |
|
38 |
|
39 The variables are: |
|
40 For an atom, a singleton set with the atom itself. |
|
41 For an atom set, the atom set itself. |
|
42 For a recursive argument, the appropriate fv function applied to it. |
|
43 (* TODO: This one is not implemented *) |
|
44 For other arguments it should be an appropriate fv function stored |
|
45 in the database. |
|
46 The bound variables are a union of results of all bindings that |
|
47 involve the given argument. For a paricular binding the result is: |
|
48 For a function applied to an argument this function with the argument. |
|
49 For an atom, a singleton set with the atom itself. |
|
50 For an atom set, the atom set itself. |
|
51 For a recursive argument, the appropriate fv function applied to it. |
|
52 (* TODO: This one is not implemented *) |
|
53 For other arguments it should be an appropriate fv function stored |
|
54 in the database. |
26 *) |
55 *) |
27 |
56 |
28 ML {* |
57 ML {* |
29 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
58 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
30 (* TODO: It is the same as one in 'nominal_atoms' *) |
59 (* TODO: It is the same as one in 'nominal_atoms' *) |
38 HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms; |
67 HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms; |
39 fun mk_diff a b = |
68 fun mk_diff a b = |
40 if b = noatoms then a else |
69 if b = noatoms then a else |
41 if b = a then noatoms else |
70 if b = a then noatoms else |
42 HOLogic.mk_binop @{const_name minus} (a, b); |
71 HOLogic.mk_binop @{const_name minus} (a, b); |
|
72 fun mk_atoms t = |
|
73 let |
|
74 val ty = fastype_of t; |
|
75 val atom_ty = HOLogic.dest_setT ty --> @{typ atom}; |
|
76 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
|
77 in |
|
78 (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
|
79 end; |
|
80 (* Copy from Term *) |
|
81 fun is_funtype (Type ("fun", [_, _])) = true |
|
82 | is_funtype _ = false; |
|
83 (* Similar to one in USyntax *) |
|
84 fun mk_pair (fst, snd) = |
|
85 let val ty1 = fastype_of fst |
|
86 val ty2 = fastype_of snd |
|
87 val c = HOLogic.pair_const ty1 ty2 |
|
88 in c $ fst $ snd |
|
89 end; |
|
90 |
43 *} |
91 *} |
44 |
92 |
45 ML {* |
93 ML {* |
46 (* Currently needs just one full_tname to access Datatype *) |
94 (* Currently needs just one full_tname to access Datatype *) |
47 fun define_raw_fv full_tname bindsall lthy = |
95 fun define_fv_alpha full_tname bindsall lthy = |
48 let |
96 let |
49 val thy = ProofContext.theory_of lthy |
97 val thy = ProofContext.theory_of lthy; |
50 val {descr, ...} = Datatype.the_info thy full_tname; |
98 val {descr, ...} = Datatype.the_info thy full_tname; |
51 val sorts = []; (* TODO *) |
99 val sorts = []; (* TODO *) |
52 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
100 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
53 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
101 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
54 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
102 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
55 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
103 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
56 val fv_frees = map Free (fv_names ~~ fv_types); |
104 val fv_frees = map Free (fv_names ~~ fv_types); |
57 fun fv_eq_constr i (cname, dts) bindcs = |
105 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
|
106 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
|
107 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
|
108 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
|
109 fun fv_alpha_constr i (cname, dts) bindcs = |
58 let |
110 let |
59 val Ts = map (typ_of_dtyp descr sorts) dts; |
111 val Ts = map (typ_of_dtyp descr sorts) dts; |
60 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
112 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
61 val args = map Free (names ~~ Ts); |
113 val args = map Free (names ~~ Ts); |
|
114 val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); |
|
115 val args2 = map Free (names2 ~~ Ts); |
62 val c = Const (cname, Ts ---> (nth_dtyp i)); |
116 val c = Const (cname, Ts ---> (nth_dtyp i)); |
63 val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"}); |
117 val fv_c = nth fv_frees i; |
64 fun fv_bind (NONE, i) = |
118 val alpha = nth alpha_frees i; |
|
119 fun fv_bind args (NONE, i) = |
65 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
120 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' *) |
121 (* TODO we assume that all can be 'atomized' *) |
|
122 if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else |
67 mk_single_atom (nth args i) |
123 mk_single_atom (nth args i) |
68 | fv_bind (SOME f, i) = f $ (nth args i); |
124 | fv_bind args (SOME f, i) = f $ (nth args i); |
69 fun fv_arg ((dt, x), bindxs) = |
125 fun fv_arg ((dt, x), bindxs) = |
70 let |
126 let |
71 val arg = |
127 val arg = |
72 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
128 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
73 (* TODO: we just assume everything can be 'atomized' *) |
129 (* TODO: we just assume everything can be 'atomized' *) |
74 HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] |
130 if (is_funtype o fastype_of) x then mk_atoms x else |
75 val sub = mk_union (map fv_bind bindxs) |
131 HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x] |
|
132 val sub = mk_union (map (fv_bind args) bindxs) |
76 in |
133 in |
77 mk_diff arg sub |
134 mk_diff arg sub |
78 end; |
135 end; |
79 val _ = tracing ("d" ^ string_of_int (length dts)); |
136 val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq |
80 val _ = tracing (string_of_int (length args)); |
137 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs)))) |
81 val _ = tracing (string_of_int (length bindcs)); |
138 val alpha_rhs = |
|
139 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
|
140 fun alpha_arg ((dt, bindxs), (arg, arg2)) = |
|
141 if bindxs = [] then ( |
|
142 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
|
143 else (HOLogic.mk_eq (arg, arg2))) |
|
144 else |
|
145 if is_rec_type dt then let |
|
146 (* THE HARD CASE *) |
|
147 val lhs_binds = mk_union (map (fv_bind args) bindxs); |
|
148 val lhs = mk_pair (lhs_binds, arg); |
|
149 val rhs_binds = mk_union (map (fv_bind args2) bindxs); |
|
150 val rhs = mk_pair (rhs_binds, arg2); |
|
151 val alpha = nth alpha_frees (body_index dt); |
|
152 val fv = nth fv_frees (body_index dt); |
|
153 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ (Free ("pi", @{typ perm})) $ rhs; |
|
154 val alpha_gen_t = Syntax.check_term lthy alpha_gen_pre |
|
155 in |
|
156 HOLogic.mk_exists ("pi", @{typ perm}, alpha_gen_t) |
|
157 (* TODO Add some test that is makes sense *) |
|
158 end else @{term "True"} |
|
159 val alpha_lhss = map (HOLogic.mk_Trueprop o alpha_arg) (dts ~~ bindcs ~~ (args ~~ args2)) |
|
160 val alpha_eq = Logic.list_implies (alpha_lhss, alpha_rhs) |
82 in |
161 in |
83 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
162 (fv_eq, alpha_eq) |
84 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))) |
|
85 end; |
163 end; |
86 fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds; |
164 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds; |
87 val fv_eqs = flat (map2 fv_eq descr bindsall) |
165 val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall)) |
|
166 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
|
167 val (fvs, lthy') = (Primrec.add_primrec |
|
168 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy) |
|
169 val (alphas, lthy'') = (Inductive.add_inductive_i |
|
170 {quiet_mode = false, verbose = true, alt_name = Binding.empty, |
|
171 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
|
172 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
|
173 (add_binds alpha_eqs) [] lthy') |
88 in |
174 in |
89 snd (Primrec.add_primrec |
175 ((fvs, alphas), lthy'') |
90 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy) |
|
91 end |
176 end |
92 *} |
177 *} |
93 |
178 |
94 (* test |
179 (* tests |
95 atom_decl name |
180 atom_decl name |
|
181 |
|
182 datatype ty = |
|
183 Var "name set" |
|
184 |
|
185 ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *} |
|
186 |
|
187 local_setup {* define_fv_alpha "Fv.ty" [[[[]]]] *} |
|
188 print_theorems |
|
189 |
96 |
190 |
97 datatype rtrm1 = |
191 datatype rtrm1 = |
98 rVr1 "name" |
192 rVr1 "name" |
99 | rAp1 "rtrm1" "rtrm1" |
193 | rAp1 "rtrm1" "rtrm1" |
100 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
194 | rLm1 "name" "rtrm1" --"name is bound in trm1" |