51 For a recursive argument, the appropriate fv function applied to it. |
51 For a recursive argument, the appropriate fv function applied to it. |
52 (* TODO: This one is not implemented *) |
52 (* TODO: This one is not implemented *) |
53 For other arguments it should be an appropriate fv function stored |
53 For other arguments it should be an appropriate fv function stored |
54 in the database. |
54 in the database. |
55 *) |
55 *) |
|
56 |
|
57 ML {* |
|
58 fun map2i _ [] [] = [] |
|
59 | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys |
|
60 | map2i f (x :: xs) [] = f x [] :: map2i f xs [] |
|
61 | map2i _ _ _ = raise UnequalLengths; |
|
62 *} |
56 |
63 |
57 (* TODO: should be const_name union *) |
64 (* TODO: should be const_name union *) |
58 ML {* |
65 ML {* |
59 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
66 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
60 (* TODO: It is the same as one in 'nominal_atoms' *) |
67 (* TODO: It is the same as one in 'nominal_atoms' *) |
183 fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss |
190 fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss |
184 val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs) |
191 val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs) |
185 in |
192 in |
186 (fv_eq, alpha_eq) |
193 (fv_eq, alpha_eq) |
187 end; |
194 end; |
188 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds; |
195 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; |
189 val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall)) |
196 val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr bindsall)) |
190 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
197 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
191 val (fvs, lthy') = (Primrec.add_primrec |
198 val (fvs, lthy') = (Primrec.add_primrec |
192 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy) |
199 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy) |
193 val (alphas, lthy'') = (Inductive.add_inductive_i |
200 val (alphas, lthy'') = (Inductive.add_inductive_i |
194 {quiet_mode = false, verbose = true, alt_name = Binding.empty, |
201 {quiet_mode = false, verbose = true, alt_name = Binding.empty, |