# HG changeset patch
# User wenzelm
# Date 1369407646 -7200
# Node ID 366fa32ee2a361184e47fb1de4918e48e315bda3
# Parent  86f7d8bc2a5f19ec71ac6ca3b2e12a4cd7178013
tuned signature;

diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri May 24 16:42:57 2013 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Fri May 24 17:00:46 2013 +0200
@@ -3411,7 +3411,7 @@
         (term_of_float_float_option_list o float_float_option_list_of_term) t
     | _ => bad t;
 
-  val normalize = eval o Envir.beta_norm o Pattern.eta_long [];
+  val normalize = eval o Envir.beta_norm o Envir.eta_long [];
 
 in Thm.cterm_of thy (Logic.mk_equals (t, normalize t)) end
 *}
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri May 24 17:00:46 2013 +0200
@@ -110,7 +110,7 @@
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
         Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
-    let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
+    let val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
     in
           ((pth RS iffD2) RS pre_thm,
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Fri May 24 17:00:46 2013 +0200
@@ -85,7 +85,7 @@
     (* The result of the quantifier elimination *)
     val (th, tac) = case prop_of pre_thm of
         Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
-    let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
+    let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
     in 
           (trace_msg ("calling procedure with term:\n" ^
              Syntax.string_of_term ctxt t1);
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri May 24 17:00:46 2013 +0200
@@ -133,8 +133,8 @@
     let val pth =
           (* If quick_and_dirty then run without proof generation as oracle*)
              if Config.get ctxt quick_and_dirty
-             then mirfr_oracle (false, cterm_of thy (Pattern.eta_long [] t1))
-             else mirfr_oracle (true, cterm_of thy (Pattern.eta_long [] t1))
+             then mirfr_oracle (false, cterm_of thy (Envir.eta_long [] t1))
+             else mirfr_oracle (true, cterm_of thy (Envir.eta_long [] t1))
     in 
           (trace_msg ("calling procedure with term:\n" ^
              Syntax.string_of_term ctxt t1);
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 24 16:42:57 2013 +0200
+++ b/src/HOL/List.thy	Fri May 24 17:00:46 2013 +0200
@@ -641,7 +641,7 @@
       (case dest_case t of
         SOME (x, T, i, cont) =>
           let
-            val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
+            val (vs, body) = strip_abs (Envir.eta_long (map snd bound_vs) cont)
             val x' = incr_boundvars (length vs) x
             val eqs' = map (incr_boundvars (length vs)) eqs
             val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri May 24 17:00:46 2013 +0200
@@ -196,7 +196,7 @@
       | NONE =>
           let
             val (f, args) = strip_comb t
-            val args = map (Pattern.eta_long []) args
+            val args = map (Envir.eta_long []) args
             val _ = @{assert} (fastype_of t = body_type (fastype_of t))
             val f' = lookup_pred f
             val Ts = case f' of
@@ -232,7 +232,7 @@
                   in (resvar, (resname :: names', prem :: prems')) end))
           end
   in
-    map (apfst Envir.eta_contract) (flatten' (Pattern.eta_long [] t) (names, prems))
+    map (apfst Envir.eta_contract) (flatten' (Envir.eta_long [] t) (names, prems))
   end;
 
 (* FIXME: create new predicate name -- does not avoid nameclashing *)
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri May 24 17:00:46 2013 +0200
@@ -76,7 +76,7 @@
 fun flatten constname atom (defs, thy) =
   if is_compound atom then
     let
-      val atom = Envir.beta_norm (Pattern.eta_long [] atom)
+      val atom = Envir.beta_norm (Envir.eta_long [] atom)
       val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
         ((Long_Name.base_name constname) ^ "_aux")
       val full_constname = Sign.full_bname thy constname
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri May 24 17:00:46 2013 +0200
@@ -851,7 +851,7 @@
    let
     val cpth = 
        if Config.get ctxt quick_and_dirty
-       then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
+       then oracle (ctxt, Envir.beta_norm (Envir.eta_long [] (term_of (Thm.dest_arg p))))
        else Conv.arg_conv (conv ctxt) p
     val p' = Thm.rhs_of cpth
     val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Fri May 24 17:00:46 2013 +0200
@@ -125,9 +125,9 @@
 
 fun add_atom (t : term) (m : Rat.rat) (p : (term * Rat.rat) list, i : Rat.rat) :
              (term * Rat.rat) list * Rat.rat =
-  case AList.lookup Pattern.aeconv p t of
+  case AList.lookup Envir.aeconv p t of
       NONE   => ((t, m) :: p, i)
-    | SOME n => (AList.update Pattern.aeconv (t, Rat.add n m) p, i);
+    | SOME n => (AList.update Envir.aeconv (t, Rat.add n m) p, i);
 
 (* decompose nested multiplications, bracketing them to the right and combining
    all their coefficients
@@ -320,7 +320,7 @@
 
 fun subst_term ([] : (term * term) list) (t : term) = t
   | subst_term pairs                     t          =
-      (case AList.lookup Pattern.aeconv pairs t of
+      (case AList.lookup Envir.aeconv pairs t of
         SOME new =>
           new
       | NONE     =>
@@ -672,7 +672,7 @@
 fun negated_term_occurs_positively (terms : term list) : bool =
   List.exists
     (fn (Trueprop $ (Const (@{const_name Not}, _) $ t)) =>
-      member Pattern.aeconv terms (Trueprop $ t)
+      member Envir.aeconv terms (Trueprop $ t)
       | _ => false)
     terms;
 
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Fri May 24 16:42:57 2013 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Fri May 24 17:00:46 2013 +0200
@@ -57,7 +57,7 @@
         case t of
             Free _  => t  (*but not existing Vars, lest the names clash*)
           | Bound _ => t
-          | _ => (case AList.lookup Pattern.aeconv (!pairs) t of
+          | _ => (case AList.lookup Envir.aeconv (!pairs) t of
                       SOME v => v
                     | NONE   => insert t)
     (*abstraction of a numeric literal*)
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Fri May 24 17:00:46 2013 +0200
@@ -458,8 +458,8 @@
 fun trace_msg ctxt msg =
   if Config.get ctxt LA_Data.trace then tracing msg else ();
 
-val union_term = union Pattern.aeconv;
-val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'));
+val union_term = union Envir.aeconv;
+val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Envir.aeconv (t, t'));
 
 fun add_atoms (lhs, _, _, rhs, _, _) =
   union_term (map fst lhs) o union_term (map fst rhs);
@@ -572,7 +572,7 @@
 end;
 
 fun coeff poly atom =
-  AList.lookup Pattern.aeconv poly atom |> the_default 0;
+  AList.lookup Envir.aeconv poly atom |> the_default 0;
 
 fun integ(rlhs,r,rel,rrhs,s,d) =
 let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/Provers/hypsubst.ML	Fri May 24 17:00:46 2013 +0200
@@ -224,7 +224,7 @@
               |> Logic.strip_assums_concl
               |> Data.dest_Trueprop |> Data.dest_imp;
             val (r', tac) =
-              if Pattern.aeconv (hyp, hyp')
+              if Envir.aeconv (hyp, hyp')
               then (r, imp_intr_tac i THEN rotate_tac ~1 i)
               else (*leave affected hyps at end*) (r + 1, imp_intr_tac i);
           in
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/Provers/splitter.ML	Fri May 24 17:00:46 2013 +0200
@@ -139,7 +139,7 @@
 
 fun mk_cntxt_splitthm t tt T =
   let fun repl lev t =
-    if Pattern.aeconv(incr_boundvars lev tt, t) then Bound lev
+    if Envir.aeconv(incr_boundvars lev tt, t) then Bound lev
     else case t of
         (Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t)
       | (Bound i) => Bound (if i>=lev then i+1 else i)
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/Pure/drule.ML	Fri May 24 17:00:46 2013 +0200
@@ -470,7 +470,7 @@
 fun eta_long_conversion ct =
   Thm.transitive
     (beta_eta_conversion ct)
-    (Thm.symmetric (beta_eta_conversion (cterm_fun (Pattern.eta_long []) ct)));
+    (Thm.symmetric (beta_eta_conversion (cterm_fun (Envir.eta_long []) ct)));
 
 (*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*)
 fun eta_contraction_rule th =
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/Pure/envir.ML	Fri May 24 17:00:46 2013 +0200
@@ -31,8 +31,10 @@
   val norm_term: env -> term -> term
   val beta_norm: term -> term
   val head_norm: env -> term -> term
+  val eta_long: typ list -> term -> term
   val eta_contract: term -> term
   val beta_eta_contract: term -> term
+  val aeconv: term * term -> bool
   val body_type: env -> int -> typ -> typ
   val binder_types: env -> int -> typ -> typ list
   val strip_type: env -> int -> typ -> typ list * typ
@@ -224,7 +226,7 @@
 end;
 
 
-(*Put a term into head normal form for unification.*)
+(* head normal form for unification *)
 
 fun head_norm env =
   let
@@ -242,7 +244,24 @@
   in Same.commit norm end;
 
 
-(*Eta-contract a term (fully)*)
+(* eta-long beta-normal form *)
+
+fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
+  | eta_long Ts t =
+      (case strip_comb t of
+        (Abs _, _) => eta_long Ts (beta_norm t)
+      | (u, ts) =>
+          let
+            val Us = binder_types (fastype_of1 (Ts, t));
+            val i = length Us;
+          in
+            fold_rev (Term.abs o pair "x") Us
+              (list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
+                (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
+          end);
+
+
+(* full eta contraction *)
 
 local
 
@@ -271,9 +290,11 @@
 fun eta_contract t =
   if Term.has_abs t then Same.commit eta t else t;
 
+end;
+
 val beta_eta_contract = eta_contract o beta_norm;
 
-end;
+fun aeconv (t, u) = t aconv u orelse eta_contract t aconv eta_contract u;
 
 
 fun body_type _ 0 T = T
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/Pure/pattern.ML	Fri May 24 17:00:46 2013 +0200
@@ -10,13 +10,9 @@
 TODO: optimize red by special-casing it
 *)
 
-infix aeconv;
-
 signature PATTERN =
 sig
   val trace_unify_fail: bool Unsynchronized.ref
-  val aeconv: term * term -> bool
-  val eta_long: typ list -> term -> term
   val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   val first_order_match: theory -> term * term
     -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
@@ -280,27 +276,6 @@
 fun unify thy = unif thy [];
 
 
-(* put a term into eta long beta normal form *)
-fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
-  | eta_long Ts t =
-      (case strip_comb t of
-        (Abs _, _) => eta_long Ts (Envir.beta_norm t)
-      | (u, ts) =>
-          let
-            val Us = binder_types (fastype_of1 (Ts, t));
-            val i = length Us;
-          in
-            fold_rev (Term.abs o pair "x") Us
-              (list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
-                (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
-          end);
-
-
-(*Tests whether 2 terms are alpha/eta-convertible and have same type.
-  Note that Consts and Vars may have more than one type.*)
-fun t aeconv u = t aconv u orelse
-  Envir.eta_contract t aconv Envir.eta_contract u;
-
 
 (*** Matching ***)
 
@@ -323,7 +298,7 @@
           else (case Envir.lookup1 insts (ixn, T) of
                   NONE => (typ_match thy (T, fastype_of t) tyinsts,
                            Vartab.update_new (ixn, (T, t)) insts)
-                | SOME u => if t aeconv u then instsp else raise MATCH)
+                | SOME u => if Envir.aeconv (t, u) then instsp else raise MATCH)
       | (Free (a,T), Free (b,U)) =>
           if a=b then (typ_match thy (T,U) tyinsts, insts) else raise MATCH
       | (Const (a,T), Const (b,U))  =>
@@ -377,7 +352,7 @@
            let val is = ints_of pargs
            in case Envir.lookup1 itms (ixn, T) of
                 NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj))
-              | SOME u => if obj aeconv (red u is []) then env
+              | SOME u => if Envir.aeconv (obj, red u is []) then env
                           else raise MATCH
            end
        | _ =>
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/Pure/tactical.ML	Fri May 24 17:00:46 2013 +0200
@@ -340,7 +340,7 @@
         fun diff st' =
             Thm.nprems_of st' - d <= 0   (*the subgoal no longer exists*)
             orelse
-             not (Pattern.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
+             not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
     in  Seq.filter diff (tac i st)  end
     handle General.Subscript => Seq.empty  (*no subgoal i*);
 
diff -r 86f7d8bc2a5f -r 366fa32ee2a3 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri May 24 16:42:57 2013 +0200
+++ b/src/Pure/thm.ML	Fri May 24 17:00:46 2013 +0200
@@ -888,7 +888,7 @@
     shyps = sorts,
     hyps = [],
     tpairs = [],
-    prop = Logic.mk_equals (t, Pattern.eta_long [] t)});
+    prop = Logic.mk_equals (t, Envir.eta_long [] t)});
 
 (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   The bound variable will be named "a" (since x will be something like x320)
@@ -1384,7 +1384,7 @@
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     val (_, asms, concl) = Logic.assum_problems (~1, Bi);
   in
-    (case find_index (fn asm => Pattern.aeconv (asm, concl)) asms of
+    (case find_index (fn asm => Envir.aeconv (asm, concl)) asms of
       ~1 => raise THM ("eq_assumption", 0, [state])
     | n =>
         Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der,