304 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; |
308 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; |
305 val alpha_ts_loc = #preds alpha |
309 val alpha_ts_loc = #preds alpha |
306 val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms) |
310 val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms) |
307 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
311 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
308 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; |
312 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; |
|
313 val fv_ts_loc_nobn = List.take (fv_ts_loc, length perms) |
|
314 val fv_ts_nobn = List.take (fv_ts, length perms) |
309 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
315 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
310 val alpha_ts_nobn = List.take (alpha_ts, length perms) |
316 val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts |
311 val alpha_induct_loc = #induct alpha |
317 val alpha_induct_loc = #induct alpha |
312 val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc]; |
318 val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc]; |
313 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct |
319 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct |
314 val fv_def = ProofContext.export lthy4 lthy3 fv_def_loc; |
320 val fv_def = ProofContext.export lthy4 lthy3 fv_def_loc; |
315 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
321 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
349 map (fn (cname, dts) => |
355 map (fn (cname, dts) => |
350 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
356 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
351 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
357 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
352 val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7; |
358 val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7; |
353 val (consts, const_defs) = split_list consts_defs; |
359 val (consts, const_defs) = split_list consts_defs; |
354 in |
|
355 if !restricted_nominal = 0 then |
|
356 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy8) |
|
357 else |
|
358 let |
|
359 val (bns_rsp_pre, lthy9) = fold_map ( |
360 val (bns_rsp_pre, lthy9) = fold_map ( |
360 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] |
361 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] |
361 (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8; |
362 (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8; |
362 val bns_rsp = flat (map snd bns_rsp_pre); |
363 val bns_rsp = flat (map snd bns_rsp_pre); |
363 val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts |
364 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
364 (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy9; |
365 else fvbv_rsp_tac alpha_induct fv_def 1; |
365 val (const_rsps, lthy11) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
366 val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9 |
366 (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1)) raw_consts lthy10 |
367 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
367 val (perms_rsp, lthy12) = prove_const_rsp Binding.empty perms |
368 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
368 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy11; |
369 fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
369 val qfv_names = map (fn x => "fv_" ^ x) qty_names |
370 else constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1 |
|
371 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
|
372 const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11 |
|
373 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts |
370 val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12; |
374 val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12; |
371 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
375 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
372 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
376 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
373 val thy = Local_Theory.exit_global lthy12b; |
377 val thy = Local_Theory.exit_global lthy12b; |
374 val perm_names = map (fn x => "permute_" ^ x) qty_names |
378 val perm_names = map (fn x => "permute_" ^ x) qty_names |
375 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
379 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
376 val lthy13 = Theory_Target.init NONE thy'; |
380 val lthy13 = Theory_Target.init NONE thy'; |
|
381 in |
|
382 if !restricted_nominal = 0 then |
|
383 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy13) |
|
384 else |
|
385 let |
377 val q_name = space_implode "_" qty_names; |
386 val q_name = space_implode "_" qty_names; |
378 val q_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy13, induct)); |
387 val q_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy13, induct)); |
379 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13; |
388 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13; |
380 val q_perm = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy14, th))) raw_perm_def; |
389 val q_perm = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy14, th))) raw_perm_def; |
381 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14; |
390 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14; |
484 map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs |
493 map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs |
485 |
494 |
486 fun prep_bn env bn_str = |
495 fun prep_bn env bn_str = |
487 case (Syntax.read_term lthy bn_str) of |
496 case (Syntax.read_term lthy bn_str) of |
488 Free (x, _) => (NONE, env_lookup env x) |
497 Free (x, _) => (NONE, env_lookup env x) |
489 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), true), env_lookup env x) |
498 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), false), env_lookup env x) |
490 | _ => error (bn_str ^ " not allowed as binding specification."); |
499 | _ => error (bn_str ^ " not allowed as binding specification."); |
491 |
500 |
492 fun prep_typ env (i, opt_name) = |
501 fun prep_typ env (i, opt_name) = |
493 case opt_name of |
502 case opt_name of |
494 NONE => [] |
503 NONE => [] |