(*  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 *)