276 let |
276 let |
277 val thy = ProofContext.theory_of lthy |
277 val thy = ProofContext.theory_of lthy |
278 val thy_name = Context.theory_name thy |
278 val thy_name = Context.theory_name thy |
279 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) = |
279 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) = |
280 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
280 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
281 val bn_funs_decls = []; |
|
282 |
|
283 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
281 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
|
282 val raw_bns_exp = map (apsnd (map (apfst (Morphism.term morphism_2_1)))) raw_bns; |
|
283 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
|
284 |
284 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
285 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
285 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
286 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
286 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
287 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
287 val descr = #descr dtinfo; |
288 val descr = #descr dtinfo; |
288 val sorts = #sorts dtinfo; |
289 val sorts = #sorts dtinfo; |
297 val inducts = #inducts dtinfo; |
298 val inducts = #inducts dtinfo; |
298 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
299 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
299 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
300 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
300 val raw_binds_flat = map (map flat) raw_binds; |
301 val raw_binds_flat = map (map flat) raw_binds; |
301 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; |
302 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; |
302 in |
|
303 if !restricted_nominal = 0 then |
|
304 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
|
305 else |
|
306 let |
|
307 val alpha_ts_loc = #preds alpha |
303 val alpha_ts_loc = #preds alpha |
308 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
304 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
309 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; |
305 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; |
310 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
306 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
311 val alpha_induct_loc = #induct alpha |
307 val alpha_induct_loc = #induct alpha |
319 val alpha_intros = #intrs alpha; |
315 val alpha_intros = #intrs alpha; |
320 val alpha_cases_loc = #elims alpha |
316 val alpha_cases_loc = #elims alpha |
321 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
317 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
322 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 |
318 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 |
323 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
319 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
|
320 in |
|
321 if !restricted_nominal = 0 then |
|
322 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5) |
|
323 else |
|
324 let |
324 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
325 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
325 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
326 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
326 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
327 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
327 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
328 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
328 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
329 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |