--- a/Nominal-General/nominal_permeq.ML	Sun Nov 14 12:09:14 2010 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,174 +0,0 @@
-(*  Title:      nominal_permeq.ML
-    Author:     Christian Urban
-    Author:     Brian Huffman
-*)
-
-signature NOMINAL_PERMEQ =
-sig
-  val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic
-  val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic
-  
-  val perm_simp_meth: thm list * string list -> Proof.context -> Method.method
-  val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method
-  val args_parser: (thm list * string list) context_parser
-
-  val trace_eqvt: bool Config.T
-  val setup: theory -> theory
-end;
-
-(* 
-
-- eqvt_tac and eqvt_strict_tac take a list of theorems
-  which are first tried to simplify permutations
-
-  the string list contains constants that should not be
-  analysed (for example there is no raw eqvt-lemma for
-  the constant The); therefore it should not be analysed 
-
-- setting [[trace_eqvt = true]] switches on tracing 
-  information  
-
-*)
-
-structure Nominal_Permeq: NOMINAL_PERMEQ =
-struct
-
-open Nominal_ThmDecls;
-
-(* tracing infrastructure *)
-val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false);
-
-fun trace_enabled ctxt = Config.get ctxt trace_eqvt
-
-fun trace_msg ctxt result = 
-  let
-    val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result))
-    val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result))
-  in
-    warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str]))
-  end
-
-fun trace_conv ctxt conv ctrm =
-  let
-    val result = conv ctrm
-  in
-    if Thm.is_reflexive result 
-    then result
-    else (trace_msg ctxt result; result)
-  end
-
-(* this conversion always fails, but prints 
-   out the analysed term  *)
-fun trace_info_conv ctxt ctrm = 
-  let
-    val trm = term_of ctrm
-    val _ = case (head_of trm) of 
-        @{const "Trueprop"} => ()
-      | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm)
-  in
-    Conv.no_conv ctrm
-  end
-
-(* conversion for applications *)
-fun eqvt_apply_conv ctrm =
-  case (term_of ctrm) of
-    Const (@{const_name "permute"}, _) $ _ $ (_ $ _) =>
-      let
-        val (perm, t) = Thm.dest_comb ctrm
-        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 ctrm
-
-(* conversion for lambdas *)
-fun eqvt_lambda_conv ctrm =
-  case (term_of ctrm) of
-    Const (@{const_name "permute"}, _) $ _ $ (Abs _) =>
-      Conv.rewr_conv @{thm eqvt_lambda} ctrm
-  | _ => Conv.no_conv ctrm
-
-
-(* conversion that raises an error or prints a warning message, 
-   if a permutation on a constant or application cannot be analysed *)
-
-fun is_excluded excluded (Const (a, _)) = member (op=) excluded a 
-  | is_excluded _ _ = false 
-
-fun progress_info_conv ctxt strict_flag excluded ctrm =
-  let
-    fun msg trm =
-      if is_excluded excluded trm then () else 
-        (if strict_flag then error else warning) 
-          ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
-
-    val _ = case (term_of ctrm) of
-        Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
-      | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm
-      | _ => () 
-  in
-    Conv.all_conv ctrm 
-  end
-
-(* main conversion *) 
-fun eqvt_conv ctxt strict_flag user_thms excluded ctrm =
-  let
-    val first_conv_wrapper = 
-      if trace_enabled ctxt 
-      then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt))
-      else Conv.first_conv
-
-    val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt
-    val post_thms = map safe_mk_equiv @{thms permute_pure}
-  in
-    first_conv_wrapper
-      [ Conv.rewrs_conv pre_thms,
-        eqvt_apply_conv,
-        eqvt_lambda_conv,
-        Conv.rewrs_conv post_thms,
-        progress_info_conv ctxt strict_flag excluded
-      ] ctrm
-  end
-
-(* the eqvt-tactics first eta-normalise goals in 
-   order to avoid problems with inductions in the
-   equivaraince command. *)
-
-(* raises an error if some permutations cannot be eliminated *)
-fun eqvt_strict_tac ctxt user_thms excluded = 
-  CONVERSION (Conv.top_conv 
-    (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt)
-
-(* prints a warning message if some permutations cannot be eliminated *)
-fun eqvt_tac ctxt user_thms excluded = 
-  CONVERSION (Conv.top_conv 
-    (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt)
-
-(* setup of the configuration value *)
-val setup =
-  trace_eqvt_setup
-
-
-(** methods **)
-fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ "exclude") -- Args.colon)) scan
-
-val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- 
-   Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) [];
-
-val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- 
-  (Scan.repeat (Args.const true))) []
-
-val args_parser =  add_thms_parser -- exclude_consts_parser 
-
-fun perm_simp_meth (thms, consts) ctxt = 
-  SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts))
-
-fun perm_strict_simp_meth (thms, consts) ctxt = 
-  SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts))
-
-end; (* structure *)