387   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =

   387   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =

   388     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;

   388     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;

   389   val raw_binds_flat = map (map flat) raw_binds;

   389   val raw_binds_flat = map (map flat) raw_binds;

   390   val ((((fv_ts, ordered_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) =

   390   val ((((fv_ts, ordered_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) =

   391     define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3;

   391     define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3;

   393   val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts

   392   val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts

   394   val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct;

   393   val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct;

   395   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);

   394   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);

   396   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;

   395   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;

   397   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;

   396   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;

   401   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)

   400   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)

   402     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))

   401     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))

   403   val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4

   402   val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4

   404   val _ = tracing "Proving equivariance";

   403   val _ = tracing "Proving equivariance";

   405   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4

   404   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4

   407   fun alpha_eqvt_tac' _ =

   406   fun alpha_eqvt_tac' _ =

   408     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy

   407     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy

   409     else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1

   408     else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1

   410   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;

   409   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;

   411   val _ = tracing "Proving equivalence";

   410   val _ = tracing "Proving equivalence";

   437   fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy

   436   fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy

   438     else fvbv_rsp_tac alpha_induct fv_def lthy8 1;

   437     else fvbv_rsp_tac alpha_induct fv_def lthy8 1;

   439   val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;

   438   val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;

   440   val (fv_rsp_pre, lthy10) = fold_map

   439   val (fv_rsp_pre, lthy10) = fold_map

   441     (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]

   440     (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]

   443   val fv_rsp = flat (map snd fv_rsp_pre);

   442   val fv_rsp = flat (map snd fv_rsp_pre);

   444   val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms

   443   val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms

   445     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;

   444     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;

   446   val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11;

   445   val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11;

   447   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]

   446   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]