329 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
329 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
330 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5 |
330 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5 |
331 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5; |
331 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5; |
332 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
332 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
333 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
333 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
334 in |
334 val alpha_equivp_loc = map (equivp_hack lthy6) (List.take (alpha_ts_loc, length perms)) |
335 if !restricted_nominal = 0 then |
335 (* val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
336 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy6) |
336 inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;*) |
337 else |
|
338 let |
|
339 val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc |
|
340 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
|
341 inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6; |
|
342 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
337 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
343 val qty_binds = map (fn (_, b, _, _) => b) dts; |
338 val qty_binds = map (fn (_, b, _, _) => b) dts; |
344 val qty_names = map Name.of_binding qty_binds; |
339 val qty_names = map Name.of_binding qty_binds; |
345 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
340 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
|
341 in |
|
342 if !restricted_nominal = 0 then |
|
343 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy6) |
|
344 else |
|
345 let |
346 val lthy7 = define_quotient_type |
346 val lthy7 = define_quotient_type |
347 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts)) |
347 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts)) |
348 (ALLGOALS (resolve_tac alpha_equivp)) lthy6; |
348 (ALLGOALS (resolve_tac alpha_equivp)) lthy6; |
349 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
349 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
350 val raw_consts = |
350 val raw_consts = |