# HG changeset patch
# User wenzelm
# Date 1300982179 -3600
# Node ID e1209fc7ecdcf926d0ce156e2d434e594a82f4c8
# Parent  47f8bfe0f5973beec17b6d124bce16c10062c884
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;

diff -r 47f8bfe0f597 -r e1209fc7ecdc src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Thu Mar 24 16:56:19 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;
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Mar 24 16:56:19 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;
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Thu Mar 24 16:56:19 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;
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/HOL/HOLCF/Tools/cont_proc.ML
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Thu Mar 24 16:56:19 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,
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/HOL/Product_Type.thy	Thu Mar 24 16:56:19 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 =
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Thu Mar 24 16:56:19 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;
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Thu Mar 24 16:56:19 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}
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Mar 24 16:56:19 2011 +0100
@@ -119,8 +119,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}
@@ -135,7 +135,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))
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Mar 24 16:56:19 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 
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Thu Mar 24 16:56:19 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
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Mar 24 16:56:19 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 []);
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Thu Mar 24 16:56:19 2011 +0100
@@ -274,7 +274,7 @@
     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;
@@ -297,8 +297,8 @@
             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
+                  if Term.is_dependent f 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;
@@ -432,10 +432,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 $ B, ts)  (* FIXME decr!? *)
   | dependent_tr' _ _ = raise Match;
 
 
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/Pure/consts.ML
--- a/src/Pure/consts.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/Pure/consts.ML	Thu Mar 24 16:56:19 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);
 
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/Pure/envir.ML
--- a/src/Pure/envir.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/Pure/envir.ML	Thu Mar 24 16:56:19 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)
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/Pure/pattern.ML	Thu Mar 24 16:56:19 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)
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/Pure/term.ML	Thu Mar 24 16:56:19 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
diff -r 47f8bfe0f597 -r e1209fc7ecdc src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/Tools/atomize_elim.ML	Thu Mar 24 16:56:19 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