added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
authorwenzelm
Thu Mar 24 16:56:19 2011 +0100 (2011-03-24)
changeset 42083e1209fc7ecdc
parent 42082 47f8bfe0f597
child 42084 532b3a76103f
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/HOLCF/Tools/cont_proc.ML
src/HOL/Product_Type.thy
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_set.ML
src/Pure/Isar/specification.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/consts.ML
src/Pure/envir.ML
src/Pure/pattern.ML
src/Pure/term.ML
src/Tools/atomize_elim.ML
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Thu Mar 24 16:47:24 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Thu Mar 24 16:56:19 2011 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4      val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     1.5      val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
     1.6      fun mk_all ((s, T), (P,n)) =
     1.7 -      if member (op =) (loose_bnos P) 0 then
     1.8 +      if Term.is_dependent P then
     1.9          (HOLogic.all_const T $ Abs (s, T, P), n)
    1.10        else (incr_boundvars ~1 P, n-1)
    1.11      fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
     2.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Mar 24 16:47:24 2011 +0100
     2.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Mar 24 16:56:19 2011 +0100
     2.3 @@ -51,7 +51,7 @@
     2.4      val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     2.5      val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
     2.6      fun mk_all ((s, T), (P,n)) =
     2.7 -      if member (op =) (loose_bnos P) 0 then
     2.8 +      if Term.is_dependent P then
     2.9          (HOLogic.all_const T $ Abs (s, T, P), n)
    2.10        else (incr_boundvars ~1 P, n-1)
    2.11      fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
     3.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Thu Mar 24 16:47:24 2011 +0100
     3.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Thu Mar 24 16:56:19 2011 +0100
     3.3 @@ -66,7 +66,7 @@
     3.4      val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     3.5      val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
     3.6      fun mk_all ((s, T), (P,n)) =
     3.7 -      if member (op =) (loose_bnos P) 0 then
     3.8 +      if Term.is_dependent P then
     3.9          (HOLogic.all_const T $ Abs (s, T, P), n)
    3.10        else (incr_boundvars ~1 P, n-1)
    3.11      fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
     4.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML	Thu Mar 24 16:47:24 2011 +0100
     4.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Thu Mar 24 16:56:19 2011 +0100
     4.3 @@ -23,9 +23,6 @@
     4.4  val cont_L = @{thm cont2cont_LAM}
     4.5  val cont_R = @{thm cont_Rep_cfun2}
     4.6  
     4.7 -(* checks whether a term contains no dangling bound variables *)
     4.8 -fun is_closed_term t = not (Term.loose_bvar (t, 0))
     4.9 -
    4.10  (* checks whether a term is written entirely in the LCF sublanguage *)
    4.11  fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) =
    4.12        is_lcf_term t andalso is_lcf_term u
    4.13 @@ -34,7 +31,7 @@
    4.14    | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) =
    4.15        is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
    4.16    | is_lcf_term (Bound _) = true
    4.17 -  | is_lcf_term t = is_closed_term t
    4.18 +  | is_lcf_term t = not (Term.is_open t)
    4.19  
    4.20  (*
    4.21    efficiently generates a cont thm for every LAM abstraction in a term,
     5.1 --- a/src/HOL/Product_Type.thy	Thu Mar 24 16:47:24 2011 +0100
     5.2 +++ b/src/HOL/Product_Type.thy	Thu Mar 24 16:56:19 2011 +0100
     5.3 @@ -272,7 +272,7 @@
     5.4    fun contract Q f ts =
     5.5      case ts of
     5.6        [A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)]
     5.7 -      => if loose_bvar1 (t,0) then f ts else Syntax.const Q $ A $ s
     5.8 +      => if Term.is_dependent t then f ts else Syntax.const Q $ A $ s
     5.9      | _ => f ts;
    5.10    fun contract2 (Q,f) = (Q, contract Q f);
    5.11    val pairs =
     6.1 --- a/src/HOL/Statespace/state_fun.ML	Thu Mar 24 16:47:24 2011 +0100
     6.2 +++ b/src/HOL/Statespace/state_fun.ML	Thu Mar 24 16:56:19 2011 +0100
     6.3 @@ -275,10 +275,10 @@
     6.4           fun mkeq (swap,Teq,lT,lo,d,n,x,s) i =
     6.5                 let val (_::nT::_) = binder_types lT;
     6.6                           (*  ('v => 'a) => 'n => ('n => 'v) => 'a *)
     6.7 -                   val x' = if not (loose_bvar1 (x,0))
     6.8 +                   val x' = if not (Term.is_dependent x)
     6.9                              then Bound 1
    6.10                              else raise TERM ("",[x]);
    6.11 -                   val n' = if not (loose_bvar1 (n,0))
    6.12 +                   val n' = if not (Term.is_dependent n)
    6.13                              then Bound 2
    6.14                              else raise TERM ("",[n]);
    6.15                     val sel' = lo $ d $ n' $ s;
     7.1 --- a/src/HOL/Tools/Function/partial_function.ML	Thu Mar 24 16:47:24 2011 +0100
     7.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Thu Mar 24 16:56:19 2011 +0100
     7.3 @@ -87,7 +87,7 @@
     7.4           NONE => no_tac
     7.5         | SOME (arg, conv) =>
     7.6             let open Conv in
     7.7 -              if not (null (loose_bnos arg)) then no_tac
     7.8 +              if Term.is_open arg then no_tac
     7.9                else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
    7.10                  THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
    7.11                  THEN_ALL_NEW etac @{thm thin_rl}
     8.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Mar 24 16:47:24 2011 +0100
     8.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Mar 24 16:56:19 2011 +0100
     8.3 @@ -119,8 +119,8 @@
     8.4          | Var _ => makeK()  (*though Var isn't expected*)
     8.5          | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
     8.6          | rator$rand =>
     8.7 -            if loose_bvar1 (rator,0) then (*C or S*)
     8.8 -               if loose_bvar1 (rand,0) then (*S*)
     8.9 +            if Term.is_dependent rator then (*C or S*)
    8.10 +               if Term.is_dependent rand then (*S*)
    8.11                   let val crator = cterm_of thy (Abs(x,xT,rator))
    8.12                       val crand = cterm_of thy (Abs(x,xT,rand))
    8.13                       val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
    8.14 @@ -135,7 +135,7 @@
    8.15                   in
    8.16                     Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
    8.17                   end
    8.18 -            else if loose_bvar1 (rand,0) then (*B or eta*)
    8.19 +            else if Term.is_dependent rand then (*B or eta*)
    8.20                 if rand = Bound 0 then Thm.eta_conversion ct
    8.21                 else (*B*)
    8.22                   let val crand = cterm_of thy (Abs(x,xT,rand))
     9.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Mar 24 16:47:24 2011 +0100
     9.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Mar 24 16:56:19 2011 +0100
     9.3 @@ -738,10 +738,10 @@
     9.4                    val ts2' = map
     9.5                      (fn Bound i => Term.dummy_pattern (nth Ts (length Ts - i - 1)) | t => t) ts2;
     9.6                    val (ots, its) = List.partition is_Bound ts2;
     9.7 -                  val no_loose = forall (fn t => not (loose_bvar (t, 0)))
     9.8 +                  val closed = forall (not o Term.is_open)
     9.9                  in
    9.10                    if null (duplicates op = ots) andalso
    9.11 -                    no_loose ts1 andalso no_loose its
    9.12 +                    closed ts1 andalso closed its
    9.13                    then
    9.14                      let val (call_p, gr') = mk_ind_call thy defs dep module true
    9.15                        s T (ts1 @ ts2') names thyname k intrs gr 
    10.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Mar 24 16:47:24 2011 +0100
    10.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Mar 24 16:56:19 2011 +0100
    10.3 @@ -40,7 +40,7 @@
    10.4               (case try (HOLogic.strip_ptuple ps) q of
    10.5                  NONE => NONE
    10.6                | SOME ts =>
    10.7 -                  if not (loose_bvar (S', 0)) andalso
    10.8 +                  if not (Term.is_open S') andalso
    10.9                      ts = map Bound (length ps downto 0)
   10.10                    then
   10.11                      let val simp = full_simp_tac (Simplifier.inherit_context ss
   10.12 @@ -128,7 +128,7 @@
   10.13      fun eta b (Abs (a, T, body)) =
   10.14            (case eta b body of
   10.15               body' as (f $ Bound 0) =>
   10.16 -               if loose_bvar1 (f, 0) orelse not b then Abs (a, T, body')
   10.17 +               if Term.is_dependent f orelse not b then Abs (a, T, body')
   10.18                 else incr_boundvars ~1 f
   10.19             | body' => Abs (a, T, body'))
   10.20        | eta b (t $ u) = eta b t $ eta (p (head_of t)) u
    11.1 --- a/src/Pure/Isar/specification.ML	Thu Mar 24 16:47:24 2011 +0100
    11.2 +++ b/src/Pure/Isar/specification.ML	Thu Mar 24 16:56:19 2011 +0100
    11.3 @@ -107,7 +107,7 @@
    11.4        | abs_body _ _ a = a;
    11.5      fun close (y, U) B =
    11.6        let val B' = abs_body 0 y (Term.incr_boundvars 1 B)
    11.7 -      in if Term.loose_bvar1 (B', 0) then Term.all dummyT $ Abs (y, U, B') else B end;
    11.8 +      in if Term.is_dependent B' then Term.all dummyT $ Abs (y, U, B') else B end;
    11.9      fun close_form A =
   11.10        let
   11.11          val occ_frees = rev (fold_aterms add_free A []);
    12.1 --- a/src/Pure/Syntax/syn_trans.ML	Thu Mar 24 16:47:24 2011 +0100
    12.2 +++ b/src/Pure/Syntax/syn_trans.ML	Thu Mar 24 16:56:19 2011 +0100
    12.3 @@ -274,7 +274,7 @@
    12.4      val body = body_of tm;
    12.5      val rev_new_vars = Term.rename_wrt_term body vars;
    12.6      fun subst (x, T) b =
    12.7 -      if can Name.dest_internal x andalso not (Term.loose_bvar1 (b, 0))
    12.8 +      if can Name.dest_internal x andalso not (Term.is_dependent b)
    12.9        then (Const ("_idtdummy", T), incr_boundvars ~1 b)
   12.10        else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b));
   12.11      val (rev_vars', body') = fold_map subst rev_new_vars body;
   12.12 @@ -297,8 +297,8 @@
   12.13              t' as f $ u =>
   12.14                (case eta_abs u of
   12.15                  Bound 0 =>
   12.16 -                  if Term.loose_bvar1 (f, 0) orelse is_aprop f then Abs (a, T, t')
   12.17 -                  else  incr_boundvars ~1 f
   12.18 +                  if Term.is_dependent f orelse is_aprop f then Abs (a, T, t')
   12.19 +                  else incr_boundvars ~1 f
   12.20                | _ => Abs (a, T, t'))
   12.21            | t' => Abs (a, T, t'))
   12.22        | eta_abs t = t;
   12.23 @@ -432,10 +432,10 @@
   12.24  val variant_abs' = var_abs mark_boundT;
   12.25  
   12.26  fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
   12.27 -      if Term.loose_bvar1 (B, 0) then
   12.28 +      if Term.is_dependent B then
   12.29          let val (x', B') = variant_abs' (x, dummyT, B);
   12.30          in Term.list_comb (Lexicon.const q $ mark_boundT (x', T) $ A $ B', ts) end
   12.31 -      else Term.list_comb (Lexicon.const r $ A $ B, ts)
   12.32 +      else Term.list_comb (Lexicon.const r $ A $ B, ts)  (* FIXME decr!? *)
   12.33    | dependent_tr' _ _ = raise Match;
   12.34  
   12.35  
    13.1 --- a/src/Pure/consts.ML	Thu Mar 24 16:47:24 2011 +0100
    13.2 +++ b/src/Pure/consts.ML	Thu Mar 24 16:56:19 2011 +0100
    13.3 @@ -255,7 +255,7 @@
    13.4  local
    13.5  
    13.6  fun strip_abss (t as Abs (x, T, b)) =
    13.7 -      if Term.loose_bvar1 (b, 0) then strip_abss b |>> cons (x, T)
    13.8 +      if Term.is_dependent b then strip_abss b |>> cons (x, T)  (* FIXME decr!? *)
    13.9        else ([], t)
   13.10    | strip_abss t = ([], t);
   13.11  
    14.1 --- a/src/Pure/envir.ML	Thu Mar 24 16:47:24 2011 +0100
    14.2 +++ b/src/Pure/envir.ML	Thu Mar 24 16:56:19 2011 +0100
    14.3 @@ -255,12 +255,12 @@
    14.4  fun eta (Abs (a, T, body)) =
    14.5      ((case eta body of
    14.6          body' as (f $ Bound 0) =>
    14.7 -          if loose_bvar1 (f, 0) then Abs (a, T, body')
    14.8 +          if Term.is_dependent f then Abs (a, T, body')
    14.9            else decrh 0 f
   14.10       | body' => Abs (a, T, body')) handle Same.SAME =>
   14.11          (case body of
   14.12            f $ Bound 0 =>
   14.13 -            if loose_bvar1 (f, 0) then raise Same.SAME
   14.14 +            if Term.is_dependent f then raise Same.SAME
   14.15              else decrh 0 f
   14.16          | _ => raise Same.SAME))
   14.17    | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u)
    15.1 --- a/src/Pure/pattern.ML	Thu Mar 24 16:47:24 2011 +0100
    15.2 +++ b/src/Pure/pattern.ML	Thu Mar 24 16:56:19 2011 +0100
    15.3 @@ -316,7 +316,7 @@
    15.4    let
    15.5      fun mtch k (instsp as (tyinsts,insts)) = fn
    15.6          (Var(ixn,T), t)  =>
    15.7 -          if k > 0 andalso loose_bvar(t,0) then raise MATCH
    15.8 +          if k > 0 andalso Term.is_open t then raise MATCH
    15.9            else (case Envir.lookup' (insts, (ixn, T)) of
   15.10                    NONE => (typ_match thy (T, fastype_of t) tyinsts,
   15.11                             Vartab.update_new (ixn, (T, t)) insts)
    16.1 --- a/src/Pure/term.ML	Thu Mar 24 16:47:24 2011 +0100
    16.2 +++ b/src/Pure/term.ML	Thu Mar 24 16:56:19 2011 +0100
    16.3 @@ -154,6 +154,8 @@
    16.4    val match_bvars: (term * term) * (string * string) list -> (string * string) list
    16.5    val map_abs_vars: (string -> string) -> term -> term
    16.6    val rename_abs: term -> term -> term -> term option
    16.7 +  val is_open: term -> bool
    16.8 +  val is_dependent: term -> bool
    16.9    val lambda_name: string * term -> term -> term
   16.10    val close_schematic_term: term -> term
   16.11    val maxidx_typ: typ -> int -> int
   16.12 @@ -650,6 +652,9 @@
   16.13    | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   16.14    | loose_bvar1 _ = false;
   16.15  
   16.16 +fun is_open t = loose_bvar (t, 0);
   16.17 +fun is_dependent t = loose_bvar1 (t, 0);
   16.18 +
   16.19  (*Substitute arguments for loose bound variables.
   16.20    Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   16.21    Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
    17.1 --- a/src/Tools/atomize_elim.ML	Thu Mar 24 16:47:24 2011 +0100
    17.2 +++ b/src/Tools/atomize_elim.ML	Thu Mar 24 16:56:19 2011 +0100
    17.3 @@ -80,7 +80,7 @@
    17.4        fun movea_conv ctxt ct =
    17.5            let
    17.6              val _ $ Abs (_, _, b) = term_of ct
    17.7 -            val idxs = fold_index (fn (i, t) => not (loose_bvar1 (t, 0)) ? cons i)
    17.8 +            val idxs = fold_index (fn (i, t) => not (Term.is_dependent t) ? cons i)
    17.9                         (Logic.strip_imp_prems b) []
   17.10                         |> rev
   17.11