59 | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys |
59 | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys |
60 | map2i f (x :: xs) [] = f x [] :: map2i f xs [] |
60 | map2i f (x :: xs) [] = f x [] :: map2i f xs [] |
61 | map2i _ _ _ = raise UnequalLengths; |
61 | map2i _ _ _ = raise UnequalLengths; |
62 *} |
62 *} |
63 |
63 |
64 (* TODO: should be const_name union *) |
|
65 ML {* |
64 ML {* |
66 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
65 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
67 (* TODO: It is the same as one in 'nominal_atoms' *) |
66 (* TODO: It is the same as one in 'nominal_atoms' *) |
68 fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom}); |
67 fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom}); |
69 val noatoms = @{term "{} :: atom set"}; |
68 val noatoms = @{term "{} :: atom set"}; |
71 fun mk_union sets = |
70 fun mk_union sets = |
72 fold (fn a => fn b => |
71 fold (fn a => fn b => |
73 if a = noatoms then b else |
72 if a = noatoms then b else |
74 if b = noatoms then a else |
73 if b = noatoms then a else |
75 if a = b then a else |
74 if a = b then a else |
76 HOLogic.mk_binop "Set.union" (a, b)) (rev sets) noatoms; |
75 HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms; |
|
76 val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf}) |
77 fun mk_conjl props = |
77 fun mk_conjl props = |
78 fold (fn a => fn b => |
78 fold (fn a => fn b => |
79 if a = @{term True} then b else |
79 if a = @{term True} then b else |
80 if b = @{term True} then a else |
80 if b = @{term True} then a else |
81 HOLogic.mk_conj (a, b)) props @{term True}; |
81 HOLogic.mk_conj (a, b)) props @{term True}; |
176 val lhs = mk_pair (lhs_binds, arg); |
176 val lhs = mk_pair (lhs_binds, arg); |
177 val rhs_binds = fv_binds args2 rbinds; |
177 val rhs_binds = fv_binds args2 rbinds; |
178 val rhs = mk_pair (rhs_binds, arg2); |
178 val rhs = mk_pair (rhs_binds, arg2); |
179 val alpha = nth alpha_frees (body_index dt); |
179 val alpha = nth alpha_frees (body_index dt); |
180 val fv = nth fv_frees (body_index dt); |
180 val fv = nth fv_frees (body_index dt); |
181 (* TODO: check that pis have empty intersection *) |
|
182 val pi = foldr1 add_perm rpis; |
181 val pi = foldr1 add_perm rpis; |
183 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
182 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
|
183 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
|
184 val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
|
185 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) |
184 in |
186 in |
185 Syntax.check_term lthy alpha_gen_pre |
187 if length pi_supps > 1 then |
|
188 HOLogic.mk_conj (alpha_gen, pi_supps_eq) else alpha_gen |
186 (* TODO Add some test that is makes sense *) |
189 (* TODO Add some test that is makes sense *) |
187 end else @{term "True"} |
190 end else @{term "True"} |
188 end |
191 end |
189 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
192 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
190 val alpha_lhss = mk_conjl alphas |
193 val alpha_lhss = mk_conjl alphas |
198 val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr bindsall)) |
201 val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr bindsall)) |
199 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
202 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
200 val (fvs, lthy') = (Primrec.add_primrec |
203 val (fvs, lthy') = (Primrec.add_primrec |
201 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy) |
204 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy) |
202 val (alphas, lthy'') = (Inductive.add_inductive_i |
205 val (alphas, lthy'') = (Inductive.add_inductive_i |
203 {quiet_mode = false, verbose = true, alt_name = Binding.empty, |
206 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
204 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
207 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
205 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
208 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
206 (add_binds alpha_eqs) [] lthy') |
209 (add_binds alpha_eqs) [] lthy') |
207 in |
210 in |
208 ((fvs, alphas), lthy'') |
211 ((fvs, alphas), lthy'') |