--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_permeq.ML	Thu Feb 25 07:48:33 2010 +0100
@@ -0,0 +1,71 @@
+(*  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 *)
\ No newline at end of file