144 *} |
144 *} |
145 |
145 |
146 ML {* |
146 ML {* |
147 fun rawify_binds dts_env cnstrs_env bn_fun_env binds = |
147 fun rawify_binds dts_env cnstrs_env bn_fun_env binds = |
148 map (map (map (map (fn (opt_trm, i, j) => |
148 map (map (map (map (fn (opt_trm, i, j) => |
149 (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env) opt_trm, i, j))))) binds |
149 (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j))))) binds |
150 *} |
150 *} |
151 |
151 |
152 ML {* |
152 ML {* |
153 fun add_primrec_wrapper funs eqs lthy = |
153 fun add_primrec_wrapper funs eqs lthy = |
154 if null funs then (([], []), lthy) |
154 if null funs then (([], []), lthy) |
230 let |
230 let |
231 val thy = ProofContext.theory_of lthy |
231 val thy = ProofContext.theory_of lthy |
232 val thy_name = Context.theory_name thy |
232 val thy_name = Context.theory_name thy |
233 val (((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), lthy2) = |
233 val (((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), lthy2) = |
234 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
234 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
|
235 val bn_funs_decls = []; |
|
236 |
235 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
237 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
236 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
238 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
237 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
239 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
238 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
240 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
239 val descr = #descr dtinfo; |
241 val descr = #descr dtinfo; |
248 val induct = #induct dtinfo; |
250 val induct = #induct dtinfo; |
249 val inducts = #inducts dtinfo; |
251 val inducts = #inducts dtinfo; |
250 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
252 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
251 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
253 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
252 val raw_binds_flat = map (map flat) raw_binds; |
254 val raw_binds_flat = map (map flat) raw_binds; |
253 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat lthy3; |
255 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; |
|
256 in |
|
257 if !restricted_nominal = 0 then |
|
258 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
|
259 else |
|
260 let |
254 val alpha_ts_loc = #preds alpha |
261 val alpha_ts_loc = #preds alpha |
255 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
262 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
256 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; |
263 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; |
257 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
264 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
258 val alpha_induct_loc = #induct alpha |
265 val alpha_induct_loc = #induct alpha |
266 val alpha_intros = #intrs alpha; |
273 val alpha_intros = #intrs alpha; |
267 val alpha_cases_loc = #elims alpha |
274 val alpha_cases_loc = #elims alpha |
268 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
275 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
269 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 |
276 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 |
270 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
277 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
271 in |
|
272 if !restricted_nominal = 0 then |
|
273 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
|
274 else |
|
275 let |
|
276 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
278 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
277 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
279 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
278 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
280 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
279 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
281 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
280 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
282 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
434 map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs |
436 map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs |
435 |
437 |
436 fun prep_bn env bn_str = |
438 fun prep_bn env bn_str = |
437 case (Syntax.read_term lthy bn_str) of |
439 case (Syntax.read_term lthy bn_str) of |
438 Free (x, _) => (NONE, env_lookup env x) |
440 Free (x, _) => (NONE, env_lookup env x) |
439 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), env_lookup env x) |
441 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), true), env_lookup env x) |
440 | _ => error (bn_str ^ " not allowed as binding specification."); |
442 | _ => error (bn_str ^ " not allowed as binding specification."); |
441 |
443 |
442 fun prep_typ env (i, opt_name) = |
444 fun prep_typ env (i, opt_name) = |
443 case opt_name of |
445 case opt_name of |
444 NONE => [] |
446 NONE => [] |