(* 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 =structlocalfun 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 ctfun 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 ctinfun 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 ] ctfun eqvt_tac ctxt = CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt)endend; (* structure *)