59 *) |
59 *) |
60 |
60 |
61 ML {* |
61 ML {* |
62 fun is_atom thy typ = |
62 fun is_atom thy typ = |
63 Sign.of_sort thy (typ, @{sort at}) |
63 Sign.of_sort thy (typ, @{sort at}) |
64 *} |
64 |
|
65 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t |
|
66 | is_atom_set thy _ = false; |
|
67 *} |
|
68 |
65 |
69 |
66 |
70 |
67 (* Like map2, only if the second list is empty passes empty lists insted of error *) |
71 (* Like map2, only if the second list is empty passes empty lists insted of error *) |
68 ML {* |
72 ML {* |
69 fun map2i _ [] [] = [] |
73 fun map2i _ [] [] = [] |
125 val atom_ty = HOLogic.dest_setT ty --> @{typ atom}; |
129 val atom_ty = HOLogic.dest_setT ty --> @{typ atom}; |
126 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
130 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
127 in |
131 in |
128 (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
132 (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
129 end; |
133 end; |
130 (* Copy from Term *) |
|
131 fun is_funtype (Type ("fun", [_, _])) = true |
|
132 | is_funtype _ = false; |
|
133 (* Similar to one in USyntax *) |
134 (* Similar to one in USyntax *) |
134 fun mk_pair (fst, snd) = |
135 fun mk_pair (fst, snd) = |
135 let val ty1 = fastype_of fst |
136 let val ty1 = fastype_of fst |
136 val ty2 = fastype_of snd |
137 val ty2 = fastype_of snd |
137 val c = HOLogic.pair_const ty1 ty2 |
138 val c = HOLogic.pair_const ty1 ty2 |
144 |
145 |
145 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
146 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
146 ML {* |
147 ML {* |
147 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy = |
148 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy = |
148 let |
149 let |
|
150 val thy = ProofContext.theory_of lthy; |
149 val {descr, sorts, ...} = dt_info; |
151 val {descr, sorts, ...} = dt_info; |
150 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
152 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
151 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
153 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
152 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
154 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
153 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
155 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
174 val fv_c = nth fv_frees ith_dtyp; |
176 val fv_c = nth fv_frees ith_dtyp; |
175 val alpha = nth alpha_frees ith_dtyp; |
177 val alpha = nth alpha_frees ith_dtyp; |
176 val arg_nos = 0 upto (length dts - 1) |
178 val arg_nos = 0 upto (length dts - 1) |
177 fun fv_bind args (NONE, i, _) = |
179 fun fv_bind args (NONE, i, _) = |
178 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
180 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
179 (* TODO we assume that all can be 'atomized' *) |
181 if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else |
180 if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else |
182 if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else |
181 mk_single_atom (nth args i) |
183 (* TODO we do not know what to do with non-atomizable things *) |
|
184 @{term "{} :: atom set"} |
182 | fv_bind args (SOME f, i, _) = f $ (nth args i); |
185 | fv_bind args (SOME f, i, _) = f $ (nth args i); |
183 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
186 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
184 fun fv_arg ((dt, x), arg_no) = |
187 fun fv_arg ((dt, x), arg_no) = |
185 let |
188 let |
186 val arg = |
189 val arg = |
187 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
190 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
188 (* TODO: we just assume everything can be 'atomized' *) |
191 if ((is_atom thy) o fastype_of) x then mk_single_atom x else |
189 if (is_funtype o fastype_of) x then mk_atoms x else |
192 if ((is_atom_set thy) o fastype_of) x then mk_atoms x else |
190 HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x]; |
193 (* TODO we do not know what to do with non-atomizable things *) |
|
194 @{term "{} :: atom set"} |
191 (* If i = j then we generate it only once *) |
195 (* If i = j then we generate it only once *) |
192 val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; |
196 val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; |
193 val sub = fv_binds args relevant |
197 val sub = fv_binds args relevant |
194 in |
198 in |
195 mk_diff arg sub |
199 mk_diff arg sub |