equal
deleted
inserted
replaced
125 ML {* |
125 ML {* |
126 fun alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss = |
126 fun alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss = |
127 let |
127 let |
128 fun mk_alphabn_free (bn, ith, _) = |
128 fun mk_alphabn_free (bn, ith, _) = |
129 let |
129 let |
130 val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Free bn))); |
130 val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
131 val ty = nth_dtyp dt_descr sorts ith; |
131 val ty = nth_dtyp dt_descr sorts ith; |
132 val alphabn_type = ty --> ty --> @{typ bool}; |
132 val alphabn_type = ty --> ty --> @{typ bool}; |
133 val alphabn_free = Free(alphabn_name, alphabn_type); |
133 val alphabn_free = Free(alphabn_name, alphabn_type); |
134 in |
134 in |
135 (alphabn_name, alphabn_free) |
135 (alphabn_name, alphabn_free) |
188 map2 alpha_constr constrs bclausess |
188 map2 alpha_constr constrs bclausess |
189 end |
189 end |
190 *} |
190 *} |
191 |
191 |
192 ML {* |
192 ML {* |
193 fun define_raw_alpha (dt_info : Datatype_Aux.info) bn_funs bclausesss fv_frees lthy = |
193 fun define_raw_alpha dt_descr sorts bn_funs bclausesss fv_frees lthy = |
194 let |
194 let |
195 val {descr as dt_descr, sorts, ...} = dt_info; |
|
196 |
|
197 val alpha_names = prefix_dt_names dt_descr sorts "alpha_"; |
195 val alpha_names = prefix_dt_names dt_descr sorts "alpha_"; |
198 val alpha_types = map (fn (i, _) => |
196 val alpha_types = map (fn (i, _) => |
199 nth_dtyp dt_descr sorts i --> nth_dtyp dt_descr sorts i --> @{typ bool}) dt_descr; |
197 nth_dtyp dt_descr sorts i --> nth_dtyp dt_descr sorts i --> @{typ bool}) dt_descr; |
200 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
198 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
201 |
199 |
228 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc; |
226 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc; |
229 val alpha_induct = Morphism.thm morphism alpha_induct_loc; |
227 val alpha_induct = Morphism.thm morphism alpha_induct_loc; |
230 val alpha_intros = Morphism.fact morphism alpha_intros_loc |
228 val alpha_intros = Morphism.fact morphism alpha_intros_loc |
231 val alpha_cases = Morphism.fact morphism alpha_cases_loc |
229 val alpha_cases = Morphism.fact morphism alpha_cases_loc |
232 in |
230 in |
233 (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy') |
231 (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy') |
234 end |
232 end |
235 *} |
233 handle UnequalLengths => error "Main" |
236 |
234 *} |
237 end |
235 |
|
236 end |