tuned signature;
authorwenzelm
Fri May 24 17:00:46 2013 +0200 (2013-05-24)
changeset 52131366fa32ee2a3
parent 52130 86f7d8bc2a5f
child 52132 fa9e563f6bcf
tuned signature;
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/List.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/lin_arith.ML
src/HOL/ex/SVC_Oracle.thy
src/Provers/Arith/fast_lin_arith.ML
src/Provers/hypsubst.ML
src/Provers/splitter.ML
src/Pure/drule.ML
src/Pure/envir.ML
src/Pure/pattern.ML
src/Pure/tactical.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri May 24 16:42:57 2013 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri May 24 17:00:46 2013 +0200
     1.3 @@ -3411,7 +3411,7 @@
     1.4          (term_of_float_float_option_list o float_float_option_list_of_term) t
     1.5      | _ => bad t;
     1.6  
     1.7 -  val normalize = eval o Envir.beta_norm o Pattern.eta_long [];
     1.8 +  val normalize = eval o Envir.beta_norm o Envir.eta_long [];
     1.9  
    1.10  in Thm.cterm_of thy (Logic.mk_equals (t, normalize t)) end
    1.11  *}
     2.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri May 24 16:42:57 2013 +0200
     2.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri May 24 17:00:46 2013 +0200
     2.3 @@ -110,7 +110,7 @@
     2.4      (* The result of the quantifier elimination *)
     2.5      val (th, tac) = case (prop_of pre_thm) of
     2.6          Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     2.7 -    let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
     2.8 +    let val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
     2.9      in
    2.10            ((pth RS iffD2) RS pre_thm,
    2.11              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
     3.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri May 24 16:42:57 2013 +0200
     3.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Fri May 24 17:00:46 2013 +0200
     3.3 @@ -85,7 +85,7 @@
     3.4      (* The result of the quantifier elimination *)
     3.5      val (th, tac) = case prop_of pre_thm of
     3.6          Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     3.7 -    let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
     3.8 +    let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
     3.9      in 
    3.10            (trace_msg ("calling procedure with term:\n" ^
    3.11               Syntax.string_of_term ctxt t1);
     4.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Fri May 24 16:42:57 2013 +0200
     4.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri May 24 17:00:46 2013 +0200
     4.3 @@ -133,8 +133,8 @@
     4.4      let val pth =
     4.5            (* If quick_and_dirty then run without proof generation as oracle*)
     4.6               if Config.get ctxt quick_and_dirty
     4.7 -             then mirfr_oracle (false, cterm_of thy (Pattern.eta_long [] t1))
     4.8 -             else mirfr_oracle (true, cterm_of thy (Pattern.eta_long [] t1))
     4.9 +             then mirfr_oracle (false, cterm_of thy (Envir.eta_long [] t1))
    4.10 +             else mirfr_oracle (true, cterm_of thy (Envir.eta_long [] t1))
    4.11      in 
    4.12            (trace_msg ("calling procedure with term:\n" ^
    4.13               Syntax.string_of_term ctxt t1);
     5.1 --- a/src/HOL/List.thy	Fri May 24 16:42:57 2013 +0200
     5.2 +++ b/src/HOL/List.thy	Fri May 24 17:00:46 2013 +0200
     5.3 @@ -641,7 +641,7 @@
     5.4        (case dest_case t of
     5.5          SOME (x, T, i, cont) =>
     5.6            let
     5.7 -            val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
     5.8 +            val (vs, body) = strip_abs (Envir.eta_long (map snd bound_vs) cont)
     5.9              val x' = incr_boundvars (length vs) x
    5.10              val eqs' = map (incr_boundvars (length vs)) eqs
    5.11              val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri May 24 16:42:57 2013 +0200
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri May 24 17:00:46 2013 +0200
     6.3 @@ -196,7 +196,7 @@
     6.4        | NONE =>
     6.5            let
     6.6              val (f, args) = strip_comb t
     6.7 -            val args = map (Pattern.eta_long []) args
     6.8 +            val args = map (Envir.eta_long []) args
     6.9              val _ = @{assert} (fastype_of t = body_type (fastype_of t))
    6.10              val f' = lookup_pred f
    6.11              val Ts = case f' of
    6.12 @@ -232,7 +232,7 @@
    6.13                    in (resvar, (resname :: names', prem :: prems')) end))
    6.14            end
    6.15    in
    6.16 -    map (apfst Envir.eta_contract) (flatten' (Pattern.eta_long [] t) (names, prems))
    6.17 +    map (apfst Envir.eta_contract) (flatten' (Envir.eta_long [] t) (names, prems))
    6.18    end;
    6.19  
    6.20  (* FIXME: create new predicate name -- does not avoid nameclashing *)
     7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri May 24 16:42:57 2013 +0200
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri May 24 17:00:46 2013 +0200
     7.3 @@ -76,7 +76,7 @@
     7.4  fun flatten constname atom (defs, thy) =
     7.5    if is_compound atom then
     7.6      let
     7.7 -      val atom = Envir.beta_norm (Pattern.eta_long [] atom)
     7.8 +      val atom = Envir.beta_norm (Envir.eta_long [] atom)
     7.9        val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
    7.10          ((Long_Name.base_name constname) ^ "_aux")
    7.11        val full_constname = Sign.full_bname thy constname
     8.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri May 24 16:42:57 2013 +0200
     8.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri May 24 17:00:46 2013 +0200
     8.3 @@ -851,7 +851,7 @@
     8.4     let
     8.5      val cpth = 
     8.6         if Config.get ctxt quick_and_dirty
     8.7 -       then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
     8.8 +       then oracle (ctxt, Envir.beta_norm (Envir.eta_long [] (term_of (Thm.dest_arg p))))
     8.9         else Conv.arg_conv (conv ctxt) p
    8.10      val p' = Thm.rhs_of cpth
    8.11      val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
     9.1 --- a/src/HOL/Tools/lin_arith.ML	Fri May 24 16:42:57 2013 +0200
     9.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri May 24 17:00:46 2013 +0200
     9.3 @@ -125,9 +125,9 @@
     9.4  
     9.5  fun add_atom (t : term) (m : Rat.rat) (p : (term * Rat.rat) list, i : Rat.rat) :
     9.6               (term * Rat.rat) list * Rat.rat =
     9.7 -  case AList.lookup Pattern.aeconv p t of
     9.8 +  case AList.lookup Envir.aeconv p t of
     9.9        NONE   => ((t, m) :: p, i)
    9.10 -    | SOME n => (AList.update Pattern.aeconv (t, Rat.add n m) p, i);
    9.11 +    | SOME n => (AList.update Envir.aeconv (t, Rat.add n m) p, i);
    9.12  
    9.13  (* decompose nested multiplications, bracketing them to the right and combining
    9.14     all their coefficients
    9.15 @@ -320,7 +320,7 @@
    9.16  
    9.17  fun subst_term ([] : (term * term) list) (t : term) = t
    9.18    | subst_term pairs                     t          =
    9.19 -      (case AList.lookup Pattern.aeconv pairs t of
    9.20 +      (case AList.lookup Envir.aeconv pairs t of
    9.21          SOME new =>
    9.22            new
    9.23        | NONE     =>
    9.24 @@ -672,7 +672,7 @@
    9.25  fun negated_term_occurs_positively (terms : term list) : bool =
    9.26    List.exists
    9.27      (fn (Trueprop $ (Const (@{const_name Not}, _) $ t)) =>
    9.28 -      member Pattern.aeconv terms (Trueprop $ t)
    9.29 +      member Envir.aeconv terms (Trueprop $ t)
    9.30        | _ => false)
    9.31      terms;
    9.32  
    10.1 --- a/src/HOL/ex/SVC_Oracle.thy	Fri May 24 16:42:57 2013 +0200
    10.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Fri May 24 17:00:46 2013 +0200
    10.3 @@ -57,7 +57,7 @@
    10.4          case t of
    10.5              Free _  => t  (*but not existing Vars, lest the names clash*)
    10.6            | Bound _ => t
    10.7 -          | _ => (case AList.lookup Pattern.aeconv (!pairs) t of
    10.8 +          | _ => (case AList.lookup Envir.aeconv (!pairs) t of
    10.9                        SOME v => v
   10.10                      | NONE   => insert t)
   10.11      (*abstraction of a numeric literal*)
    11.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri May 24 16:42:57 2013 +0200
    11.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Fri May 24 17:00:46 2013 +0200
    11.3 @@ -458,8 +458,8 @@
    11.4  fun trace_msg ctxt msg =
    11.5    if Config.get ctxt LA_Data.trace then tracing msg else ();
    11.6  
    11.7 -val union_term = union Pattern.aeconv;
    11.8 -val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'));
    11.9 +val union_term = union Envir.aeconv;
   11.10 +val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Envir.aeconv (t, t'));
   11.11  
   11.12  fun add_atoms (lhs, _, _, rhs, _, _) =
   11.13    union_term (map fst lhs) o union_term (map fst rhs);
   11.14 @@ -572,7 +572,7 @@
   11.15  end;
   11.16  
   11.17  fun coeff poly atom =
   11.18 -  AList.lookup Pattern.aeconv poly atom |> the_default 0;
   11.19 +  AList.lookup Envir.aeconv poly atom |> the_default 0;
   11.20  
   11.21  fun integ(rlhs,r,rel,rrhs,s,d) =
   11.22  let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
    12.1 --- a/src/Provers/hypsubst.ML	Fri May 24 16:42:57 2013 +0200
    12.2 +++ b/src/Provers/hypsubst.ML	Fri May 24 17:00:46 2013 +0200
    12.3 @@ -224,7 +224,7 @@
    12.4                |> Logic.strip_assums_concl
    12.5                |> Data.dest_Trueprop |> Data.dest_imp;
    12.6              val (r', tac) =
    12.7 -              if Pattern.aeconv (hyp, hyp')
    12.8 +              if Envir.aeconv (hyp, hyp')
    12.9                then (r, imp_intr_tac i THEN rotate_tac ~1 i)
   12.10                else (*leave affected hyps at end*) (r + 1, imp_intr_tac i);
   12.11            in
    13.1 --- a/src/Provers/splitter.ML	Fri May 24 16:42:57 2013 +0200
    13.2 +++ b/src/Provers/splitter.ML	Fri May 24 17:00:46 2013 +0200
    13.3 @@ -139,7 +139,7 @@
    13.4  
    13.5  fun mk_cntxt_splitthm t tt T =
    13.6    let fun repl lev t =
    13.7 -    if Pattern.aeconv(incr_boundvars lev tt, t) then Bound lev
    13.8 +    if Envir.aeconv(incr_boundvars lev tt, t) then Bound lev
    13.9      else case t of
   13.10          (Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t)
   13.11        | (Bound i) => Bound (if i>=lev then i+1 else i)
    14.1 --- a/src/Pure/drule.ML	Fri May 24 16:42:57 2013 +0200
    14.2 +++ b/src/Pure/drule.ML	Fri May 24 17:00:46 2013 +0200
    14.3 @@ -470,7 +470,7 @@
    14.4  fun eta_long_conversion ct =
    14.5    Thm.transitive
    14.6      (beta_eta_conversion ct)
    14.7 -    (Thm.symmetric (beta_eta_conversion (cterm_fun (Pattern.eta_long []) ct)));
    14.8 +    (Thm.symmetric (beta_eta_conversion (cterm_fun (Envir.eta_long []) ct)));
    14.9  
   14.10  (*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*)
   14.11  fun eta_contraction_rule th =
    15.1 --- a/src/Pure/envir.ML	Fri May 24 16:42:57 2013 +0200
    15.2 +++ b/src/Pure/envir.ML	Fri May 24 17:00:46 2013 +0200
    15.3 @@ -31,8 +31,10 @@
    15.4    val norm_term: env -> term -> term
    15.5    val beta_norm: term -> term
    15.6    val head_norm: env -> term -> term
    15.7 +  val eta_long: typ list -> term -> term
    15.8    val eta_contract: term -> term
    15.9    val beta_eta_contract: term -> term
   15.10 +  val aeconv: term * term -> bool
   15.11    val body_type: env -> int -> typ -> typ
   15.12    val binder_types: env -> int -> typ -> typ list
   15.13    val strip_type: env -> int -> typ -> typ list * typ
   15.14 @@ -224,7 +226,7 @@
   15.15  end;
   15.16  
   15.17  
   15.18 -(*Put a term into head normal form for unification.*)
   15.19 +(* head normal form for unification *)
   15.20  
   15.21  fun head_norm env =
   15.22    let
   15.23 @@ -242,7 +244,24 @@
   15.24    in Same.commit norm end;
   15.25  
   15.26  
   15.27 -(*Eta-contract a term (fully)*)
   15.28 +(* eta-long beta-normal form *)
   15.29 +
   15.30 +fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
   15.31 +  | eta_long Ts t =
   15.32 +      (case strip_comb t of
   15.33 +        (Abs _, _) => eta_long Ts (beta_norm t)
   15.34 +      | (u, ts) =>
   15.35 +          let
   15.36 +            val Us = binder_types (fastype_of1 (Ts, t));
   15.37 +            val i = length Us;
   15.38 +          in
   15.39 +            fold_rev (Term.abs o pair "x") Us
   15.40 +              (list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
   15.41 +                (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
   15.42 +          end);
   15.43 +
   15.44 +
   15.45 +(* full eta contraction *)
   15.46  
   15.47  local
   15.48  
   15.49 @@ -271,9 +290,11 @@
   15.50  fun eta_contract t =
   15.51    if Term.has_abs t then Same.commit eta t else t;
   15.52  
   15.53 +end;
   15.54 +
   15.55  val beta_eta_contract = eta_contract o beta_norm;
   15.56  
   15.57 -end;
   15.58 +fun aeconv (t, u) = t aconv u orelse eta_contract t aconv eta_contract u;
   15.59  
   15.60  
   15.61  fun body_type _ 0 T = T
    16.1 --- a/src/Pure/pattern.ML	Fri May 24 16:42:57 2013 +0200
    16.2 +++ b/src/Pure/pattern.ML	Fri May 24 17:00:46 2013 +0200
    16.3 @@ -10,13 +10,9 @@
    16.4  TODO: optimize red by special-casing it
    16.5  *)
    16.6  
    16.7 -infix aeconv;
    16.8 -
    16.9  signature PATTERN =
   16.10  sig
   16.11    val trace_unify_fail: bool Unsynchronized.ref
   16.12 -  val aeconv: term * term -> bool
   16.13 -  val eta_long: typ list -> term -> term
   16.14    val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   16.15    val first_order_match: theory -> term * term
   16.16      -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   16.17 @@ -280,27 +276,6 @@
   16.18  fun unify thy = unif thy [];
   16.19  
   16.20  
   16.21 -(* put a term into eta long beta normal form *)
   16.22 -fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
   16.23 -  | eta_long Ts t =
   16.24 -      (case strip_comb t of
   16.25 -        (Abs _, _) => eta_long Ts (Envir.beta_norm t)
   16.26 -      | (u, ts) =>
   16.27 -          let
   16.28 -            val Us = binder_types (fastype_of1 (Ts, t));
   16.29 -            val i = length Us;
   16.30 -          in
   16.31 -            fold_rev (Term.abs o pair "x") Us
   16.32 -              (list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
   16.33 -                (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
   16.34 -          end);
   16.35 -
   16.36 -
   16.37 -(*Tests whether 2 terms are alpha/eta-convertible and have same type.
   16.38 -  Note that Consts and Vars may have more than one type.*)
   16.39 -fun t aeconv u = t aconv u orelse
   16.40 -  Envir.eta_contract t aconv Envir.eta_contract u;
   16.41 -
   16.42  
   16.43  (*** Matching ***)
   16.44  
   16.45 @@ -323,7 +298,7 @@
   16.46            else (case Envir.lookup1 insts (ixn, T) of
   16.47                    NONE => (typ_match thy (T, fastype_of t) tyinsts,
   16.48                             Vartab.update_new (ixn, (T, t)) insts)
   16.49 -                | SOME u => if t aeconv u then instsp else raise MATCH)
   16.50 +                | SOME u => if Envir.aeconv (t, u) then instsp else raise MATCH)
   16.51        | (Free (a,T), Free (b,U)) =>
   16.52            if a=b then (typ_match thy (T,U) tyinsts, insts) else raise MATCH
   16.53        | (Const (a,T), Const (b,U))  =>
   16.54 @@ -377,7 +352,7 @@
   16.55             let val is = ints_of pargs
   16.56             in case Envir.lookup1 itms (ixn, T) of
   16.57                  NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj))
   16.58 -              | SOME u => if obj aeconv (red u is []) then env
   16.59 +              | SOME u => if Envir.aeconv (obj, red u is []) then env
   16.60                            else raise MATCH
   16.61             end
   16.62         | _ =>
    17.1 --- a/src/Pure/tactical.ML	Fri May 24 16:42:57 2013 +0200
    17.2 +++ b/src/Pure/tactical.ML	Fri May 24 17:00:46 2013 +0200
    17.3 @@ -340,7 +340,7 @@
    17.4          fun diff st' =
    17.5              Thm.nprems_of st' - d <= 0   (*the subgoal no longer exists*)
    17.6              orelse
    17.7 -             not (Pattern.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
    17.8 +             not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
    17.9      in  Seq.filter diff (tac i st)  end
   17.10      handle General.Subscript => Seq.empty  (*no subgoal i*);
   17.11  
    18.1 --- a/src/Pure/thm.ML	Fri May 24 16:42:57 2013 +0200
    18.2 +++ b/src/Pure/thm.ML	Fri May 24 17:00:46 2013 +0200
    18.3 @@ -888,7 +888,7 @@
    18.4      shyps = sorts,
    18.5      hyps = [],
    18.6      tpairs = [],
    18.7 -    prop = Logic.mk_equals (t, Pattern.eta_long [] t)});
    18.8 +    prop = Logic.mk_equals (t, Envir.eta_long [] t)});
    18.9  
   18.10  (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   18.11    The bound variable will be named "a" (since x will be something like x320)
   18.12 @@ -1384,7 +1384,7 @@
   18.13      val (tpairs, Bs, Bi, C) = dest_state (state, i);
   18.14      val (_, asms, concl) = Logic.assum_problems (~1, Bi);
   18.15    in
   18.16 -    (case find_index (fn asm => Pattern.aeconv (asm, concl)) asms of
   18.17 +    (case find_index (fn asm => Envir.aeconv (asm, concl)) asms of
   18.18        ~1 => raise THM ("eq_assumption", 0, [state])
   18.19      | n =>
   18.20          Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der,