--- a/src/HOL/Decision_Procs/cooper_tac.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat Mar 26 15:55:22 2011 +0100
@@ -46,7 +46,7 @@
val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
fun mk_all ((s, T), (P,n)) =
- if member (op =) (loose_bnos P) 0 then
+ if Term.is_dependent P then
(HOLogic.all_const T $ Abs (s, T, P), n)
else (incr_boundvars ~1 P, n-1)
fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sat Mar 26 15:55:22 2011 +0100
@@ -51,7 +51,7 @@
val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
fun mk_all ((s, T), (P,n)) =
- if member (op =) (loose_bnos P) 0 then
+ if Term.is_dependent P then
(HOLogic.all_const T $ Abs (s, T, P), n)
else (incr_boundvars ~1 P, n-1)
fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
--- a/src/HOL/Decision_Procs/mir_tac.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sat Mar 26 15:55:22 2011 +0100
@@ -66,7 +66,7 @@
val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
fun mk_all ((s, T), (P,n)) =
- if member (op =) (loose_bnos P) 0 then
+ if Term.is_dependent P then
(HOLogic.all_const T $ Abs (s, T, P), n)
else (incr_boundvars ~1 P, n-1)
fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
--- a/src/HOL/HOLCF/Tools/cont_proc.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML Sat Mar 26 15:55:22 2011 +0100
@@ -23,9 +23,6 @@
val cont_L = @{thm cont2cont_LAM}
val cont_R = @{thm cont_Rep_cfun2}
-(* checks whether a term contains no dangling bound variables *)
-fun is_closed_term t = not (Term.loose_bvar (t, 0))
-
(* checks whether a term is written entirely in the LCF sublanguage *)
fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) =
is_lcf_term t andalso is_lcf_term u
@@ -34,7 +31,7 @@
| is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) =
is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
| is_lcf_term (Bound _) = true
- | is_lcf_term t = is_closed_term t
+ | is_lcf_term t = not (Term.is_open t)
(*
efficiently generates a cont thm for every LAM abstraction in a term,
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat Mar 26 15:55:22 2011 +0100
@@ -93,20 +93,14 @@
annquote_tr' (Syntax.const name) (r :: t :: ts)
| annbexp_tr' _ _ = raise Match;
- fun K_tr' (Abs (_, _, t)) =
- if null (loose_bnos t) then t else raise Match
- | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
- if null (loose_bnos t) then t else raise Match
- | K_tr' _ = raise Match;
-
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
- (Abs (x, dummyT, K_tr' k) :: ts)
+ (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
| assign_tr' _ = raise Match;
fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax.update_name_tr' f)
- (Abs (x, dummyT, K_tr' k) :: ts)
+ (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
| annassign_tr' _ = raise Match;
fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat Mar 26 15:55:22 2011 +0100
@@ -67,15 +67,9 @@
quote_tr' (Syntax.const name) (t :: ts)
| bexp_tr' _ _ = raise Match;
- fun K_tr' (Abs (_, _, t)) =
- if null (loose_bnos t) then t else raise Match
- | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
- if null (loose_bnos t) then t else raise Match
- | K_tr' _ = raise Match;
-
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
- (Abs (x, dummyT, K_tr' k) :: ts)
+ (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
| assign_tr' _ = raise Match;
in
[(@{const_syntax Collect}, assert_tr'),
--- a/src/HOL/Isar_Examples/Hoare.thy Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Sat Mar 26 15:55:22 2011 +0100
@@ -237,15 +237,9 @@
quote_tr' (Syntax.const name) (t :: ts)
| bexp_tr' _ _ = raise Match;
- fun K_tr' (Abs (_, _, t)) =
- if null (loose_bnos t) then t else raise Match
- | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
- if null (loose_bnos t) then t else raise Match
- | K_tr' _ = raise Match;
-
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
- (Abs (x, dummyT, K_tr' k) :: ts)
+ (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
| assign_tr' _ = raise Match;
in
[(@{const_syntax Collect}, assert_tr'),
--- a/src/HOL/Product_Type.thy Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Product_Type.thy Sat Mar 26 15:55:22 2011 +0100
@@ -272,7 +272,7 @@
fun contract Q f ts =
case ts of
[A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)]
- => if loose_bvar1 (t,0) then f ts else Syntax.const Q $ A $ s
+ => if Term.is_dependent t then f ts else Syntax.const Q $ A $ s
| _ => f ts;
fun contract2 (Q,f) = (Q, contract Q f);
val pairs =
--- a/src/HOL/Statespace/state_fun.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Statespace/state_fun.ML Sat Mar 26 15:55:22 2011 +0100
@@ -275,10 +275,10 @@
fun mkeq (swap,Teq,lT,lo,d,n,x,s) i =
let val (_::nT::_) = binder_types lT;
(* ('v => 'a) => 'n => ('n => 'v) => 'a *)
- val x' = if not (loose_bvar1 (x,0))
+ val x' = if not (Term.is_dependent x)
then Bound 1
else raise TERM ("",[x]);
- val n' = if not (loose_bvar1 (n,0))
+ val n' = if not (Term.is_dependent n)
then Bound 2
else raise TERM ("",[n]);
val sel' = lo $ d $ n' $ s;
--- a/src/HOL/Tools/Function/function_common.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Sat Mar 26 15:55:22 2011 +0100
@@ -243,8 +243,8 @@
val _ = length args > 0 orelse input_error "Function has no arguments:"
fun add_bvs t is = add_loose_bnos (t, 0, is)
- val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
- |> map (fst o nth (rev qs))
+ val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
+ |> map (fst o nth (rev qs))
val _ = null rvs orelse input_error
("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^
--- a/src/HOL/Tools/Function/partial_function.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Sat Mar 26 15:55:22 2011 +0100
@@ -87,7 +87,7 @@
NONE => no_tac
| SOME (arg, conv) =>
let open Conv in
- if not (null (loose_bnos arg)) then no_tac
+ if Term.is_open arg then no_tac
else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
THEN_ALL_NEW etac @{thm thin_rl}
--- a/src/HOL/Tools/Meson/meson_clausify.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Sat Mar 26 15:55:22 2011 +0100
@@ -125,8 +125,8 @@
| Var _ => makeK() (*though Var isn't expected*)
| Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
| rator$rand =>
- if loose_bvar1 (rator,0) then (*C or S*)
- if loose_bvar1 (rand,0) then (*S*)
+ if Term.is_dependent rator then (*C or S*)
+ if Term.is_dependent rand then (*S*)
let val crator = cterm_of thy (Abs(x,xT,rator))
val crand = cterm_of thy (Abs(x,xT,rand))
val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
@@ -141,7 +141,7 @@
in
Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
end
- else if loose_bvar1 (rand,0) then (*B or eta*)
+ else if Term.is_dependent rand then (*B or eta*)
if rand = Bound 0 then Thm.eta_conversion ct
else (*B*)
let val crand = cterm_of thy (Abs(x,xT,rand))
--- a/src/HOL/Tools/inductive_codegen.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Sat Mar 26 15:55:22 2011 +0100
@@ -738,10 +738,10 @@
val ts2' = map
(fn Bound i => Term.dummy_pattern (nth Ts (length Ts - i - 1)) | t => t) ts2;
val (ots, its) = List.partition is_Bound ts2;
- val no_loose = forall (fn t => not (loose_bvar (t, 0)))
+ val closed = forall (not o Term.is_open)
in
if null (duplicates op = ots) andalso
- no_loose ts1 andalso no_loose its
+ closed ts1 andalso closed its
then
let val (call_p, gr') = mk_ind_call thy defs dep module true
s T (ts1 @ ts2') names thyname k intrs gr
--- a/src/HOL/Tools/inductive_set.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Tools/inductive_set.ML Sat Mar 26 15:55:22 2011 +0100
@@ -40,7 +40,7 @@
(case try (HOLogic.strip_ptuple ps) q of
NONE => NONE
| SOME ts =>
- if not (loose_bvar (S', 0)) andalso
+ if not (Term.is_open S') andalso
ts = map Bound (length ps downto 0)
then
let val simp = full_simp_tac (Simplifier.inherit_context ss
@@ -128,7 +128,7 @@
fun eta b (Abs (a, T, body)) =
(case eta b body of
body' as (f $ Bound 0) =>
- if loose_bvar1 (f, 0) orelse not b then Abs (a, T, body')
+ if Term.is_dependent f orelse not b then Abs (a, T, body')
else incr_boundvars ~1 f
| body' => Abs (a, T, body'))
| eta b (t $ u) = eta b t $ eta (p (head_of t)) u
--- a/src/HOL/Tools/record.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/HOL/Tools/record.ML Sat Mar 26 15:55:22 2011 +0100
@@ -961,21 +961,11 @@
fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
(case dest_update ctxt c of
SOME name =>
- let
- val opt_t =
- (case k of
- Abs (_, _, Abs (_, _, t) $ Bound 0) =>
- if null (loose_bnos t) then SOME t else NONE
- | Abs (_, _, t) =>
- if null (loose_bnos t) then SOME t else NONE
- | _ => NONE);
- in
- (case opt_t of
- SOME t =>
- apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
- (field_updates_tr' ctxt u)
- | NONE => ([], tm))
- end
+ (case try Syntax.const_abs_tr' k of
+ SOME t =>
+ apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
+ (field_updates_tr' ctxt u)
+ | NONE => ([], tm))
| NONE => ([], tm))
| field_updates_tr' _ tm = ([], tm);
--- a/src/Provers/hypsubst.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Provers/hypsubst.ML Sat Mar 26 15:55:22 2011 +0100
@@ -58,8 +58,6 @@
exception EQ_VAR;
-fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
-
(*Simplifier turns Bound variables to special Free variables:
change it back (any Bound variable will do)*)
fun contract t =
@@ -84,22 +82,24 @@
if novars andalso (has_tvars t orelse has_tvars u)
then raise Match (*variables in the type!*)
else
- case (contract t, contract u) of
- (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u
- then raise Match
- else true (*eliminates t*)
- | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
- then raise Match
- else false (*eliminates u*)
- | (t' as Free _, _) => if bnd orelse Logic.occs(t',u) orelse
- novars andalso has_vars u
- then raise Match
- else true (*eliminates t*)
- | (_, u' as Free _) => if bnd orelse Logic.occs(u',t) orelse
- novars andalso has_vars t
- then raise Match
- else false (*eliminates u*)
- | _ => raise Match;
+ (case (contract t, contract u) of
+ (Bound i, _) =>
+ if loose_bvar1 (u, i) orelse novars andalso has_vars u
+ then raise Match
+ else true (*eliminates t*)
+ | (_, Bound i) =>
+ if loose_bvar1 (t, i) orelse novars andalso has_vars t
+ then raise Match
+ else false (*eliminates u*)
+ | (t' as Free _, _) =>
+ if bnd orelse Logic.occs (t', u) orelse novars andalso has_vars u
+ then raise Match
+ else true (*eliminates t*)
+ | (_, u' as Free _) =>
+ if bnd orelse Logic.occs (u', t) orelse novars andalso has_vars t
+ then raise Match
+ else false (*eliminates u*)
+ | _ => raise Match);
(*Locates a substitutable variable on the left (resp. right) of an equality
assumption. Returns the number of intervening assumptions. *)
--- a/src/Pure/Isar/specification.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Pure/Isar/specification.ML Sat Mar 26 15:55:22 2011 +0100
@@ -107,7 +107,7 @@
| abs_body _ _ a = a;
fun close (y, U) B =
let val B' = abs_body 0 y (Term.incr_boundvars 1 B)
- in if Term.loose_bvar1 (B', 0) then Term.all dummyT $ Abs (y, U, B') else B end;
+ in if Term.is_dependent B' then Term.all dummyT $ Abs (y, U, B') else B end;
fun close_form A =
let
val occ_frees = rev (fold_aterms add_free A []);
--- a/src/Pure/Syntax/syn_trans.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML Sat Mar 26 15:55:22 2011 +0100
@@ -10,10 +10,11 @@
val eta_contract_raw: Config.raw
val eta_contract: bool Config.T
val atomic_abs_tr': string * typ * term -> term * term
+ val const_abs_tr': term -> term
+ val mk_binder_tr: string * string -> string * (term list -> term)
+ val mk_binder_tr': string * string -> string * (term list -> term)
val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
- val mk_binder_tr: string * string -> string * (term list -> term)
- val mk_binder_tr': string * string -> string * (term list -> term)
val dependent_tr': string * string -> term list -> term
val antiquote_tr: string -> term -> term
val quote_tr: string -> term -> term
@@ -198,7 +199,8 @@
if Type_Ext.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
else
list_comb (c $ update_name_tr [t] $
- (Lexicon.fun_type $ (Lexicon.fun_type $ ty $ ty) $ Lexicon.dummy_type), ts)
+ (Lexicon.fun_type $
+ (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts)
| update_name_tr ts = raise TERM ("update_name_tr", ts);
@@ -259,6 +261,28 @@
| applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];
+(* partial eta-contraction before printing *)
+
+fun eta_abs (Abs (a, T, t)) =
+ (case eta_abs t of
+ t' as Const ("_aprop", _) $ _ => Abs (a, T, t')
+ | t' as f $ u =>
+ (case eta_abs u of
+ Bound 0 =>
+ if Term.is_dependent f then Abs (a, T, t')
+ else incr_boundvars ~1 f
+ | _ => Abs (a, T, t'))
+ | t' => Abs (a, T, t'))
+ | eta_abs t = t;
+
+val eta_contract_default = Unsynchronized.ref true;
+val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
+val eta_contract = Config.bool eta_contract_raw;
+
+fun eta_contr ctxt tm =
+ if Config.get ctxt eta_contract then eta_abs tm else tm;
+
+
(* abstraction *)
fun mark_boundT (x, T) = Const ("_bound", T --> T) $ Free (x, T);
@@ -273,39 +297,13 @@
val body = body_of tm;
val rev_new_vars = Term.rename_wrt_term body vars;
fun subst (x, T) b =
- if can Name.dest_internal x andalso not (Term.loose_bvar1 (b, 0))
+ if can Name.dest_internal x andalso not (Term.is_dependent b)
then (Const ("_idtdummy", T), incr_boundvars ~1 b)
else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b));
val (rev_vars', body') = fold_map subst rev_new_vars body;
in (rev rev_vars', body') end;
-(*do (partial) eta-contraction before printing*)
-
-val eta_contract_default = Unsynchronized.ref true;
-val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
-val eta_contract = Config.bool eta_contract_raw;
-
-fun eta_contr ctxt tm =
- let
- fun is_aprop (Const ("_aprop", _)) = true
- | is_aprop _ = false;
-
- fun eta_abs (Abs (a, T, t)) =
- (case eta_abs t of
- t' as f $ u =>
- (case eta_abs u of
- Bound 0 =>
- if Term.loose_bvar1 (f, 0) orelse is_aprop f then Abs (a, T, t')
- else incr_boundvars ~1 f
- | _ => Abs (a, T, t'))
- | t' => Abs (a, T, t'))
- | eta_abs t = t;
- in
- if Config.get ctxt eta_contract then eta_abs tm else tm
- end;
-
-
fun abs_tr' ctxt tm =
uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
(strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
@@ -314,21 +312,20 @@
let val [xT] = Term.rename_wrt_term t [(x, T)]
in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
-fun abs_ast_tr' (*"_abs"*) asts =
+fun abs_ast_tr' asts =
(case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
([], _) => raise Ast.AST ("abs_ast_tr'", asts)
| (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
-fun preserve_binder_abs_tr' name syn = (name, fn (Abs abs :: ts) =>
- let val (x, t) = atomic_abs_tr' abs
- in list_comb (Lexicon.const syn $ x $ t, ts) end);
-
-fun preserve_binder_abs2_tr' name syn = (name, fn (A :: Abs abs :: ts) =>
- let val (x, t) = atomic_abs_tr' abs
- in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
+fun const_abs_tr' t =
+ (case eta_abs t of
+ Abs (_, _, t') =>
+ if Term.is_dependent t' then raise Match
+ else incr_boundvars ~1 t'
+ | _ => raise Match);
-(* binder *)
+(* binders *)
fun mk_binder_tr' (name, syn) =
let
@@ -345,6 +342,14 @@
| binder_tr' [] = raise Match;
in (name, binder_tr') end;
+fun preserve_binder_abs_tr' name syn = (name, fn Abs abs :: ts =>
+ let val (x, t) = atomic_abs_tr' abs
+ in list_comb (Lexicon.const syn $ x $ t, ts) end);
+
+fun preserve_binder_abs2_tr' name syn = (name, fn A :: Abs abs :: ts =>
+ let val (x, t) = atomic_abs_tr' abs
+ in list_comb (Lexicon.const syn $ x $ A $ t, ts) end);
+
(* idtyp constraints *)
@@ -431,10 +436,10 @@
val variant_abs' = var_abs mark_boundT;
fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
- if Term.loose_bvar1 (B, 0) then
+ if Term.is_dependent B then
let val (x', B') = variant_abs' (x, dummyT, B);
in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end
- else Term.list_comb (Lexicon.const r $ A $ B, ts)
+ else Term.list_comb (Lexicon.const r $ A $ incr_boundvars ~1 B, ts)
| dependent_tr' _ _ = raise Match;
@@ -443,8 +448,8 @@
fun antiquote_tr' name =
let
fun tr' i (t $ u) =
- if u aconv Bound i then Lexicon.const name $ tr' i t
- else tr' i t $ tr' i u
+ if u aconv Bound i then Lexicon.const name $ tr' i t
+ else tr' i t $ tr' i u
| tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
| tr' i a = if a aconv Bound i then raise Match else a;
in tr' 0 end;
@@ -461,16 +466,25 @@
(* corresponding updates *)
+local
+
+fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T
+ | upd_type _ = dummyT;
+
fun upd_tr' (x_upd, T) =
(case try (unsuffix "_update") x_upd of
- SOME x => (x, if T = dummyT then T else Term.domain_type T)
+ SOME x => (x, upd_type T)
| NONE => raise Match);
+in
+
fun update_name_tr' (Free x) = Free (upd_tr' x)
| update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x)
| update_name_tr' (Const x) = Const (upd_tr' x)
| update_name_tr' _ = raise Match;
+end;
+
(* indexed syntax *)
--- a/src/Pure/consts.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Pure/consts.ML Sat Mar 26 15:55:22 2011 +0100
@@ -255,7 +255,7 @@
local
fun strip_abss (t as Abs (x, T, b)) =
- if Term.loose_bvar1 (b, 0) then strip_abss b |>> cons (x, T)
+ if Term.is_dependent b then strip_abss b |>> cons (x, T) (* FIXME decr!? *)
else ([], t)
| strip_abss t = ([], t);
--- a/src/Pure/envir.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Pure/envir.ML Sat Mar 26 15:55:22 2011 +0100
@@ -255,12 +255,12 @@
fun eta (Abs (a, T, body)) =
((case eta body of
body' as (f $ Bound 0) =>
- if loose_bvar1 (f, 0) then Abs (a, T, body')
+ if Term.is_dependent f then Abs (a, T, body')
else decrh 0 f
| body' => Abs (a, T, body')) handle Same.SAME =>
(case body of
f $ Bound 0 =>
- if loose_bvar1 (f, 0) then raise Same.SAME
+ if Term.is_dependent f then raise Same.SAME
else decrh 0 f
| _ => raise Same.SAME))
| eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u)
--- a/src/Pure/pattern.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Pure/pattern.ML Sat Mar 26 15:55:22 2011 +0100
@@ -316,7 +316,7 @@
let
fun mtch k (instsp as (tyinsts,insts)) = fn
(Var(ixn,T), t) =>
- if k > 0 andalso loose_bvar(t,0) then raise MATCH
+ if k > 0 andalso Term.is_open t then raise MATCH
else (case Envir.lookup' (insts, (ixn, T)) of
NONE => (typ_match thy (T, fastype_of t) tyinsts,
Vartab.update_new (ixn, (T, t)) insts)
--- a/src/Pure/term.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Pure/term.ML Sat Mar 26 15:55:22 2011 +0100
@@ -154,6 +154,8 @@
val match_bvars: (term * term) * (string * string) list -> (string * string) list
val map_abs_vars: (string -> string) -> term -> term
val rename_abs: term -> term -> term -> term option
+ val is_open: term -> bool
+ val is_dependent: term -> bool
val lambda_name: string * term -> term -> term
val close_schematic_term: term -> term
val maxidx_typ: typ -> int -> int
@@ -650,6 +652,9 @@
| loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
| loose_bvar1 _ = false;
+fun is_open t = loose_bvar (t, 0);
+fun is_dependent t = loose_bvar1 (t, 0);
+
(*Substitute arguments for loose bound variables.
Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
--- a/src/Tools/atomize_elim.ML Sat Mar 26 00:23:20 2011 +0100
+++ b/src/Tools/atomize_elim.ML Sat Mar 26 15:55:22 2011 +0100
@@ -80,7 +80,7 @@
fun movea_conv ctxt ct =
let
val _ $ Abs (_, _, b) = term_of ct
- val idxs = fold_index (fn (i, t) => not (loose_bvar1 (t, 0)) ? cons i)
+ val idxs = fold_index (fn (i, t) => not (Term.is_dependent t) ? cons i)
(Logic.strip_imp_prems b) []
|> rev