141 |
142 |
142 *} |
143 *} |
143 |
144 |
144 ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *} |
145 ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *} |
145 |
146 |
|
147 ML {* |
|
148 fun non_rec_binds l = |
|
149 let |
|
150 fun is_non_rec (SOME (f, false), _, _) = SOME f |
|
151 | is_non_rec _ = NONE |
|
152 in |
|
153 distinct (op =) (map_filter is_non_rec (flat (flat l))) |
|
154 end |
|
155 *} |
|
156 |
|
157 (* We assume no bindings in the type on which bn is defined *) |
|
158 ML {* |
|
159 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bn) = |
|
160 let |
|
161 val {descr, sorts, ...} = dt_info; |
|
162 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
|
163 val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
|
164 val fvbn = Free (fvbn_name, fastype_of (nth fv_frees ith_dtyp)); |
|
165 fun fv_bn_constr (cname, dts) = |
|
166 let |
|
167 val Ts = map (typ_of_dtyp descr sorts) dts; |
|
168 val names = Datatype_Prop.make_tnames Ts; |
|
169 val args = map Free (names ~~ Ts); |
|
170 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
|
171 fun fv_arg ((dt, x), arg_no) = |
|
172 let |
|
173 val ty = fastype_of x |
|
174 in |
|
175 if arg_no mem args_in_bn then |
|
176 (if is_rec_type dt then |
|
177 (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: not good") |
|
178 else @{term "{} :: atom set"}) else |
|
179 if is_atom thy ty then mk_single_atom x else |
|
180 if is_atom_set thy ty then mk_atoms x else |
|
181 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
|
182 @{term "{} :: atom set"} |
|
183 end; |
|
184 val arg_nos = 0 upto (length dts - 1) |
|
185 in |
|
186 HOLogic.mk_Trueprop (HOLogic.mk_eq |
|
187 (fvbn $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |
|
188 end; |
|
189 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
|
190 val eqs = map fv_bn_constr constrs |
|
191 in |
|
192 ((bn, fvbn), (fvbn_name, eqs)) |
|
193 end |
|
194 *} |
|
195 |
146 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
196 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
147 ML {* |
197 ML {* |
148 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy = |
198 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy = |
149 let |
199 let |
150 val thy = ProofContext.theory_of lthy; |
200 val thy = ProofContext.theory_of lthy; |
151 val {descr, sorts, ...} = dt_info; |
201 val {descr, sorts, ...} = dt_info; |
152 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
202 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
153 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
203 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
154 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
204 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
155 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
205 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
156 val fv_frees = map Free (fv_names ~~ fv_types); |
206 val fv_frees = map Free (fv_names ~~ fv_types); |
|
207 val nr_bns = non_rec_binds bindsall; |
|
208 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
|
209 val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); |
|
210 val fv_bns = map snd bn_fv_bns; |
|
211 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
157 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
212 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
158 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
213 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
159 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
214 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
160 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
215 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
161 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
216 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
180 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
235 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
181 if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else |
236 if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else |
182 if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else |
237 if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else |
183 (* TODO we do not know what to do with non-atomizable things *) |
238 (* TODO we do not know what to do with non-atomizable things *) |
184 @{term "{} :: atom set"} |
239 @{term "{} :: atom set"} |
185 | fv_bind args (SOME f, i, _) = f $ (nth args i); |
240 | fv_bind args (SOME (f, _), i, _) = f $ (nth args i); |
186 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
241 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
|
242 fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE |
|
243 | find_nonrec_binder _ _ = NONE |
187 fun fv_arg ((dt, x), arg_no) = |
244 fun fv_arg ((dt, x), arg_no) = |
188 let |
245 case get_first (find_nonrec_binder arg_no) bindcs of |
189 val arg = |
246 SOME f => |
190 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
247 (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of |
191 if ((is_atom thy) o fastype_of) x then mk_single_atom x else |
248 SOME fv_bn => fv_bn $ x |
192 if ((is_atom_set thy) o fastype_of) x then mk_atoms x else |
249 | NONE => error "bn specified in a non-rec binding but not in bn list") |
193 (* TODO we do not know what to do with non-atomizable things *) |
250 | NONE => |
194 @{term "{} :: atom set"} |
251 let |
195 (* If i = j then we generate it only once *) |
252 val arg = |
196 val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; |
253 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
197 val sub = fv_binds args relevant |
254 if ((is_atom thy) o fastype_of) x then mk_single_atom x else |
198 in |
255 if ((is_atom_set thy) o fastype_of) x then mk_atoms x else |
199 mk_diff arg sub |
256 (* TODO we do not know what to do with non-atomizable things *) |
200 end; |
257 @{term "{} :: atom set"} |
|
258 (* If i = j then we generate it only once *) |
|
259 val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; |
|
260 val sub = fv_binds args relevant |
|
261 in |
|
262 mk_diff arg sub |
|
263 end; |
201 val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq |
264 val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq |
202 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |
265 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |
203 val alpha_rhs = |
266 val alpha_rhs = |
204 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
267 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
205 fun alpha_arg ((dt, arg_no), (arg, arg2)) = |
268 fun alpha_arg ((dt, arg_no), (arg, arg2)) = |
238 in |
301 in |
239 (fv_eq, alpha_eq) |
302 (fv_eq, alpha_eq) |
240 end; |
303 end; |
241 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; |
304 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; |
242 val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr (gather_binds bindsall))) |
305 val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr (gather_binds bindsall))) |
|
306 val fv_eqs_all = fv_eqs @ (flat fv_bn_eqs); |
|
307 val fv_names_all = fv_names @ fv_bn_names; |
243 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
308 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
|
309 (* Function_Fun.add_fun Function_Common.default_config ... true *) |
244 val (fvs, lthy') = (Primrec.add_primrec |
310 val (fvs, lthy') = (Primrec.add_primrec |
245 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy) |
311 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) |
246 val (alphas, lthy'') = (Inductive.add_inductive_i |
312 val (alphas, lthy'') = (Inductive.add_inductive_i |
247 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
313 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
248 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
314 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
249 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
315 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
250 (add_binds alpha_eqs) [] lthy') |
316 (add_binds alpha_eqs) [] lthy') |
251 in |
317 in |
252 ((fvs, alphas), lthy'') |
318 ((fvs, alphas), lthy'') |
253 end |
319 end |
254 *} |
320 *} |
255 |
321 |
256 (* tests |
322 (* |
257 atom_decl name |
323 atom_decl name |
258 |
324 |
259 datatype ty = |
325 datatype lam = |
260 Var "name set" |
326 VAR "name" |
261 |
327 | APP "lam" "lam" |
262 ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *} |
328 | LET "bp" "lam" |
263 |
329 and bp = |
264 local_setup {* define_fv_alpha "Fv.ty" [[[[]]]] *} |
330 BP "name" "lam" |
|
331 |
|
332 primrec |
|
333 bi::"bp \<Rightarrow> atom set" |
|
334 where |
|
335 "bi (BP x t) = {atom x}" |
|
336 |
|
337 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *} |
|
338 |
|
339 |
|
340 local_setup {* |
|
341 snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam") |
|
342 [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [0])] *} |
265 print_theorems |
343 print_theorems |
266 |
344 *) |
267 |
345 |
|
346 (* |
268 datatype rtrm1 = |
347 datatype rtrm1 = |
269 rVr1 "name" |
348 rVr1 "name" |
270 | rAp1 "rtrm1" "rtrm1" |
349 | rAp1 "rtrm1" "rtrm1" |
271 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
350 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
272 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
351 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |