4 

     5 ML {*

     6 fun build_alpha_sym_trans_gl alphas (x, y, z) =

     7 let

     8   fun build_alpha alpha =

     9     let

    10       val ty = domain_type (fastype_of alpha);

    11       val var = Free(x, ty);

    12       val var2 = Free(y, ty);

    13       val var3 = Free(z, ty);

    14       val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);

    15       val transp = HOLogic.mk_imp (alpha $ var $ var2,

    16         HOLogic.mk_all (z, ty,

    17           HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))

    18     in

    19       (symp, transp)

    20     end;

    21   val eqs = map build_alpha alphas

    22   val (sym_eqs, trans_eqs) = split_list eqs

    23   fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l

    24 in

    25   (conj sym_eqs, conj trans_eqs)

    26 end

    27 *}

    28 

    29 ML {*

    30 fun build_alpha_refl_gl fv_alphas_lst alphas =

    31 let

    32   val (fvs_alphas, _) = split_list fv_alphas_lst;

    33   val (_, alpha_ts) = split_list fvs_alphas;

    34   val tys = map (domain_type o fastype_of) alpha_ts;

    35   val names = Datatype_Prop.make_tnames tys;

    36   val args = map Free (names ~~ tys);

    37   fun find_alphas ty x =

    38     domain_type (fastype_of x) = ty;

    39   fun refl_eq_arg (ty, arg) =

    40     let

    41       val rel_alphas = filter (find_alphas ty) alphas;

    42     in

    43       map (fn x => x $ arg $ arg) rel_alphas

    44     end;

    45   (* Flattening loses the induction structure *)

    46   val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args))

    47 in

    48   (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs))

    49 end

    50 *}

    51 

    52 ML {*

    53 fun reflp_tac induct eq_iff =

    54   rtac induct THEN_ALL_NEW

    55   simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW

    56   split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}

    57   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps

    58      @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv

    59        add_0_left supp_zero_perm Int_empty_left split_conv prod_rel.simps})

    60 *}

    61 

    62 ML {*

    63 fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =

    64 let

    65   val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas;

    66   val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1);

    67 in

    68   HOLogic.conj_elims refl_conj

    69 end

    70 *}

    71 

    72 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"

    73 apply (erule exE)

    74 apply (rule_tac x="-pi" in exI)

    75 by auto

    76 

    77 ML {*

    78 fun symp_tac induct inj eqvt ctxt =

    79   rtac induct THEN_ALL_NEW

    80   simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac

    81   THEN_ALL_NEW

    82   REPEAT o etac @{thm exi_neg}

    83   THEN_ALL_NEW

    84   split_conj_tac THEN_ALL_NEW

    85   asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW

    86   TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW

    87   (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))

    88 *}

    89 

    90 

    91 lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"

    92 apply (erule exE)+

    93 apply (rule_tac x="pia + pi" in exI)

    94 by auto

    95 

    96 

    97 ML {*

    98 fun eetac rule = 

    99   Subgoal.FOCUS_PARAMS (fn focus =>

   100     let

   101       val concl = #concl focus

   102       val prems = Logic.strip_imp_prems (term_of concl)

   103       val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems

   104       val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs

   105       val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs

   106     in

   107       (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1

   108     end

   109   )

   110 *}

   111 

   112 ML {*

   113 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =

   114   rtac induct THEN_ALL_NEW

   115   (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW

   116   asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW

   117   split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac

   118   THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))

   119   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW

   120   TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW

   121   (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))

   122 *}

   123 

   124 lemma transpI:

   125   "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"

   126   unfolding transp_def

   127   by blast

   128 

   129 ML {*

   130 fun equivp_tac reflps symps transps =

   131   (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *)

   132   simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})

   133   THEN' rtac conjI THEN' rtac allI THEN'

   134   resolve_tac reflps THEN'

   135   rtac conjI THEN' rtac allI THEN' rtac allI THEN'

   136   resolve_tac symps THEN'

   137   rtac @{thm transpI} THEN' resolve_tac transps

   138 *}

   139 

   140 ML {*

   141 fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =

   142 let

   143   val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;

   144   val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z)

   145   fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1;

   146   fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;

   147   val symp_loc = Goal.prove ctxt' [] [] symg symp_tac';

   148   val transp_loc = Goal.prove ctxt' [] [] transg transp_tac';

   149   val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc]

   150   val symps = HOLogic.conj_elims symp

   151   val transps = HOLogic.conj_elims transp

   152   fun equivp alpha =

   153     let

   154       val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})

   155       val goal = @{term Trueprop} $ (equivp $ alpha)

   156       fun tac _ = equivp_tac reflps symps transps 1

   157     in

   158       Goal.prove ctxt [] [] goal tac

   159     end

   160 in

   161   map equivp alphas

   162 end

   163 *}