(*  Title:      nominal_thmdecls.ML
    Author:     Brian Huffman, Christian Urban
*)

signature NOMINAL_PERMEQ =
sig
  val eqvt_tac: Proof.context -> int -> tactic 

end;

(* TODO:

 - provide a method interface with the usual add and del options

 - print a warning if for a constant no eqvt lemma is stored

 - there seems to be too much simplified in case of multiple 
   permutations, like

      p o q o r o x 

   we usually only want the outermost permutation to "float" in
*)


structure Nominal_Permeq: NOMINAL_PERMEQ =
struct

local

fun eqvt_apply_conv ctxt ct =
  case (term_of ct) of
    (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) =>
      let
        val (perm, t) = Thm.dest_comb ct
        val (_, p) = Thm.dest_comb perm
        val (f, x) = Thm.dest_comb t
        val a = ctyp_of_term x;
        val b = ctyp_of_term t;
        val ty_insts = map SOME [b, a]
        val term_insts = map SOME [p, f, x]
      in
        Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
      end
  | _ => Conv.no_conv ct

fun eqvt_lambda_conv ctxt ct =
  case (term_of ct) of
    (Const (@{const_name "permute"}, _) $ _ $ Abs _) =>
      Conv.rewr_conv @{thm eqvt_lambda} ct
  | _ => Conv.no_conv ct

in

fun eqvt_conv ctxt ct =
  Conv.first_conv
    [ Conv.rewr_conv @{thm eqvt_bound},
      eqvt_apply_conv ctxt
        then_conv Conv.comb_conv (eqvt_conv ctxt),
      eqvt_lambda_conv ctxt
        then_conv Conv.abs_conv (fn (v, ctxt) => eqvt_conv ctxt) ctxt,
      More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvts_raw_thms ctxt),
      Conv.all_conv
    ] ct

fun eqvt_tac ctxt = 
  CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt)

end

end; (* structure *)