--- 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
*}
--- 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))
--- 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);
--- 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);
--- 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
--- 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 *)
--- 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
--- 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'))
--- 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;
--- 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*)
--- 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
--- 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
--- 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)
--- 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 =
--- 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
--- 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
| _ =>
--- 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*);
--- 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,