300 val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs) |
302 val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs) |
301 in |
303 in |
302 (fv_eq, alpha_eq) |
304 (fv_eq, alpha_eq) |
303 end; |
305 end; |
304 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; |
306 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; |
305 val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr (gather_binds bindsall))) |
307 val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall) |
306 val fv_eqs_all = fv_eqs @ (flat fv_bn_eqs); |
308 val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs)) |
307 val fv_names_all = fv_names @ fv_bn_names; |
309 val rel_bns_nos = map (fn (_, i, _) => i) rel_bns; |
|
310 fun filter_fun (a, b) = b mem rel_bns_nos; |
|
311 val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1)) |
|
312 val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs))) |
|
313 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
|
314 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
|
315 val fv_names_all = fv_names_fst @ fv_bn_names; |
308 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
316 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
309 (* Function_Fun.add_fun Function_Common.default_config ... true *) |
317 (* Function_Fun.add_fun Function_Common.default_config ... true *) |
|
318 val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all) |
310 val (fvs, lthy') = (Primrec.add_primrec |
319 val (fvs, lthy') = (Primrec.add_primrec |
311 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) |
320 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) |
312 val (alphas, lthy'') = (Inductive.add_inductive_i |
321 val (fvs2, lthy'') = |
|
322 if fv_eqs_snd = [] then (([], []), lthy') else |
|
323 (Primrec.add_primrec |
|
324 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy') |
|
325 val (alphas, lthy''') = (Inductive.add_inductive_i |
313 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
326 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
314 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
327 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
315 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
328 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
316 (add_binds alpha_eqs) [] lthy') |
329 (add_binds alpha_eqs) [] lthy'') |
317 in |
330 in |
318 ((fvs, alphas), lthy'') |
331 ((fvs, alphas), lthy'') |
319 end |
332 end |
320 *} |
333 *} |
321 |
334 |