317 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; |
317 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; |
318 val alpha_ts_loc = #preds alpha |
318 val alpha_ts_loc = #preds alpha |
319 val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms) |
319 val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms) |
320 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
320 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
321 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; |
321 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; |
322 val fv_ts_loc_nobn = List.take (fv_ts_loc, length perms) |
322 val (fv_ts_loc_nobn, fv_ts_loc_bn) = chop (length perms) fv_ts_loc; |
323 val fv_ts_nobn = List.take (fv_ts, length perms) |
323 val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts; |
324 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
324 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
325 val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts |
325 val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts |
326 val alpha_induct_loc = #induct alpha |
326 val alpha_induct_loc = #induct alpha |
327 val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc]; |
327 val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc]; |
328 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct |
328 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct |
344 val _ = map tracing (map PolyML.makestring alpha_eqvt) |
344 val _ = map tracing (map PolyML.makestring alpha_eqvt) |
345 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
345 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
346 val fv_eqvt_tac = |
346 val fv_eqvt_tac = |
347 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
347 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
348 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5 |
348 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5 |
349 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5; |
349 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5; |
|
350 val (fv_bn_eqvts, lthy6a) = fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) (fv_ts_loc_bn ~~ (map snd bns)) lthy6; |
|
351 val lthy6 = lthy6a; |
350 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
352 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
351 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
353 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
352 val alpha_equivp_loc = |
354 val alpha_equivp_loc = |
353 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn |
355 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn |
354 else build_equivps alpha_ts_loc induct alpha_induct_loc |
356 else build_equivps alpha_ts_loc induct alpha_induct_loc |