191 in |
191 in |
192 ((bn, fvbn), (fvbn_name, eqs)) |
192 ((bn, fvbn), (fvbn_name, eqs)) |
193 end |
193 end |
194 *} |
194 *} |
195 |
195 |
|
196 ML {* |
|
197 fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) = |
|
198 let |
|
199 val {descr, sorts, ...} = dt_info; |
|
200 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
|
201 val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
|
202 val alpha_bn_type = @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} |
|
203 val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type); |
|
204 (*... *) |
|
205 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
|
206 val eqs = [] (*map2i alpha_bn_constr constrs args_in_bns*) |
|
207 in |
|
208 ((bn, alpha_bn_name), (alpha_bn_free, eqs)) |
|
209 end |
|
210 *} |
|
211 |
196 ML {* fn x => split_list(flat x) *} |
212 ML {* fn x => split_list(flat x) *} |
197 ML {* fn x => apsnd flat (split_list (map split_list x)) *} |
213 ML {* fn x => apsnd flat (split_list (map split_list x)) *} |
198 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
214 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
199 ML {* |
215 ML {* |
200 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy = |
216 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy = |
207 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
223 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
208 val fv_frees = map Free (fv_names ~~ fv_types); |
224 val fv_frees = map Free (fv_names ~~ fv_types); |
209 val nr_bns = non_rec_binds bindsall; |
225 val nr_bns = non_rec_binds bindsall; |
210 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
226 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
211 val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); |
227 val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); |
212 val fv_bns = map snd bn_fv_bns; |
|
213 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
228 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
214 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
229 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
215 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
230 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
216 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
231 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
217 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
232 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
218 val alpha_bnnames = map (fn (bn, _, _) => "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)))) bns; |
233 (* We assume that a bn is either recursive or not *) |
219 val alpha_bntypes = map (fn (_, i, _) => @{typ perm} --> nth_dtyp i --> nth_dtyp i --> @{typ bool}) bns; |
234 val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns; |
220 val alpha_bnfrees = map Free (alpha_bnnames ~~ alpha_bntypes); |
235 |
|
236 val alpha_bnfrees = map (fst o snd) (map (alpha_bn thy dt_info alpha_frees) (bns ~~ bns_rec)) |
|
237 |
221 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
238 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
222 let |
239 let |
223 val Ts = map (typ_of_dtyp descr sorts) dts; |
240 val Ts = map (typ_of_dtyp descr sorts) dts; |
224 val bindslen = length bindcs |
241 val bindslen = length bindcs |
225 val pi_strs_same = replicate bindslen "pi" |
242 val pi_strs_same = replicate bindslen "pi" |
300 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *) |
317 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *) |
301 in |
318 in |
302 (* if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) |
319 (* if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) |
303 alpha_gen |
320 alpha_gen |
304 end |
321 end |
|
322 | _ => error "Fv.alpha: not supported binding structure" |
305 end |
323 end |
306 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
324 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
307 val alpha_lhss = mk_conjl alphas |
325 val alpha_lhss = mk_conjl alphas |
308 val alpha_lhss_ex = |
326 val alpha_lhss_ex = |
309 fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss |
327 fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss |
313 end; |
331 end; |
314 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; |
332 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; |
315 val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall) |
333 val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall) |
316 val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs)) |
334 val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs)) |
317 val rel_bns_nos = map (fn (_, i, _) => i) rel_bns; |
335 val rel_bns_nos = map (fn (_, i, _) => i) rel_bns; |
318 fun filter_fun (a, b) = b mem rel_bns_nos; |
336 fun filter_fun (_, b) = b mem rel_bns_nos; |
319 val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1)) |
337 val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1)) |
320 val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs))) |
338 val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs))) |
321 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
339 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
322 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
340 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
323 val fv_names_all = fv_names_fst @ fv_bn_names; |
341 val fv_names_all = fv_names_fst @ fv_bn_names; |
333 val (alphas, lthy''') = (Inductive.add_inductive_i |
351 val (alphas, lthy''') = (Inductive.add_inductive_i |
334 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
352 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
335 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
353 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
336 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
354 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
337 (add_binds alpha_eqs) [] lthy'') |
355 (add_binds alpha_eqs) [] lthy'') |
338 in |
356 val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2) |
339 ((fvs, alphas), lthy''') |
357 in |
|
358 ((all_fvs, alphas), lthy''') |
340 end |
359 end |
341 *} |
360 *} |
342 |
361 |
343 (* |
362 (* |
344 atom_decl name |
363 atom_decl name |