renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
authorwenzelm
Sat Jan 14 20:05:58 2012 +0100 (2012-01-14)
changeset 46218ecf6375e2abb
parent 46217 7b19666f0e3d
child 46219 426ed18eba43
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
src/HOL/Import/shuffler.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/record.ML
src/HOL/ex/SVC_Oracle.thy
src/Pure/logic.ML
src/Pure/primitive_defs.ML
src/Pure/term.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Import/shuffler.ML	Sat Jan 14 19:06:05 2012 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Sat Jan 14 20:05:58 2012 +0100
     1.3 @@ -152,8 +152,8 @@
     1.4  
     1.5  fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t =
     1.6      let
     1.7 -        val lhs = list_all ([xv,yv],t)
     1.8 -        val rhs = list_all ([yv,xv],swap_bound 0 t)
     1.9 +        val lhs = Logic.list_all ([xv,yv],t)
    1.10 +        val rhs = Logic.list_all ([yv,xv],swap_bound 0 t)
    1.11          val rew = Logic.mk_equals (lhs,rhs)
    1.12          val init = Thm.trivial (cterm_of thy rew)
    1.13      in
     2.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Jan 14 19:06:05 2012 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Jan 14 20:05:58 2012 +0100
     2.3 @@ -497,7 +497,7 @@
     2.4                end
     2.5            in (j + 1, j' + length Ts,
     2.6              case dt'' of
     2.7 -                Datatype.DtRec k => list_all (map (pair "x") Us,
     2.8 +                Datatype.DtRec k => Logic.list_all (map (pair "x") Us,
     2.9                    HOLogic.mk_Trueprop (Free (nth rep_set_names k,
    2.10                      T --> HOLogic.boolT) $ free')) :: prems
    2.11                | _ => prems,
    2.12 @@ -1143,7 +1143,7 @@
    2.13              val (Us, U) = strip_type T;
    2.14              val l = length Us;
    2.15            in
    2.16 -            list_all (z :: map (pair "x") Us,
    2.17 +            Logic.list_all (z :: map (pair "x") Us,
    2.18                HOLogic.mk_Trueprop
    2.19                  (make_pred fsT (Datatype_Aux.body_index dt) U $ Bound l $
    2.20                    Datatype_Aux.app_bnds (Free (s, T)) l))
     3.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sat Jan 14 19:06:05 2012 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Jan 14 20:05:58 2012 +0100
     3.3 @@ -240,7 +240,7 @@
     3.4             HOLogic.mk_Trueprop (lift_pred p ts));
     3.5          val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term prem params')
     3.6        in
     3.7 -        (list_all (params', prem), (rev vs, subst_bounds (vs, prem)))
     3.8 +        (Logic.list_all (params', prem), (rev vs, subst_bounds (vs, prem)))
     3.9        end) prems);
    3.10  
    3.11      val ind_vars =
    3.12 @@ -259,7 +259,7 @@
    3.13          lift_pred' (Free (fs_ctxt_name, fsT)) p ts)) concls));
    3.14  
    3.15      val vc_compat = map (fn (params, bvars, prems, (p, ts)) =>
    3.16 -      map (fn q => list_all (params, incr_boundvars ~1 (Logic.list_implies
    3.17 +      map (fn q => Logic.list_all (params, incr_boundvars ~1 (Logic.list_implies
    3.18            (map_filter (fn prem =>
    3.19               if null (preds_of ps prem) then SOME prem
    3.20               else map_term (split_conj (K o I) names) prem prem) prems, q))))
    3.21 @@ -439,9 +439,9 @@
    3.22        map (fn (prem, args, concl, (prems, _)) =>
    3.23          let
    3.24            fun mk_prem (ps, [], _, prems) =
    3.25 -                list_all (ps, Logic.list_implies (prems, concl))
    3.26 +                Logic.list_all (ps, Logic.list_implies (prems, concl))
    3.27              | mk_prem (ps, qs, _, prems) =
    3.28 -                list_all (ps, Logic.mk_implies
    3.29 +                Logic.list_all (ps, Logic.mk_implies
    3.30                    (Logic.list_implies
    3.31                      (mk_distinct qs @
    3.32                       maps (fn (t, T) => map (fn u => HOLogic.mk_Trueprop
     4.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Jan 14 19:06:05 2012 +0100
     4.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Jan 14 20:05:58 2012 +0100
     4.3 @@ -141,7 +141,7 @@
     4.4  
     4.5  fun abs_params params t =
     4.6    let val vs =  map (Var o apfst (rpair 0)) (Term.rename_wrt_term t params)
     4.7 -  in (list_all (params, t), (rev vs, subst_bounds (vs, t))) end;
     4.8 +  in (Logic.list_all (params, t), (rev vs, subst_bounds (vs, t))) end;
     4.9  
    4.10  fun inst_params thy (vs, p) th cts =
    4.11    let val env = Pattern.first_order_match thy (p, prop_of th)
    4.12 @@ -336,7 +336,7 @@
    4.13          val _ $ (f $ (_ $ pi $ l) $ r) = prop_of th2
    4.14          val th2' =
    4.15            Goal.prove ctxt [] []
    4.16 -            (list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop
    4.17 +            (Logic.list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop
    4.18                 (f $ fold_rev (NominalDatatype.mk_perm (rev pTs))
    4.19                    (pis1 @ pi :: pis2) l $ r)))
    4.20              (fn _ => cut_facts_tac [th2] 1 THEN
     5.1 --- a/src/HOL/Statespace/state_fun.ML	Sat Jan 14 19:06:05 2012 +0100
     5.2 +++ b/src/HOL/Statespace/state_fun.ML	Sat Jan 14 20:05:58 2012 +0100
     5.3 @@ -246,7 +246,7 @@
     5.4                  let
     5.5                    val eq1 =
     5.6                      Goal.prove ctxt [] []
     5.7 -                      (list_all (vars, Logic.mk_equals (trm, trm')))
     5.8 +                      (Logic.list_all (vars, Logic.mk_equals (trm, trm')))
     5.9                        (fn _ => rtac meta_ext 1 THEN simp_tac ss1 1);
    5.10                    val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
    5.11                  in SOME (Thm.transitive eq1 eq2) end
    5.12 @@ -308,7 +308,7 @@
    5.13              (let
    5.14                val (eq, eT, nT, swap) = mkeq (dest_sel_eq t) 0;
    5.15                val prop =
    5.16 -                list_all ([("n", nT), ("x", eT)],
    5.17 +                Logic.list_all ([("n", nT), ("x", eT)],
    5.18                    Logic.mk_equals (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
    5.19                val thm = Drule.export_without_context (prove prop);
    5.20                val thm' = if swap then swap_ex_eq OF [thm] else thm
     6.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sat Jan 14 19:06:05 2012 +0100
     6.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Jan 14 20:05:58 2012 +0100
     6.3 @@ -156,7 +156,7 @@
     6.4                  val free_t =
     6.5                    Datatype_Aux.app_bnds (Datatype_Aux.mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
     6.6                in
     6.7 -                (j + 1, list_all (map (pair "x") Ts,
     6.8 +                (j + 1, Logic.list_all (map (pair "x") Ts,
     6.9                    HOLogic.mk_Trueprop
    6.10                      (Free (nth rep_set_names' k, UnivT') $ free_t)) :: prems,
    6.11                  mk_lim free_t Ts :: ts)
     7.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Jan 14 19:06:05 2012 +0100
     7.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Jan 14 20:05:58 2012 +0100
     7.3 @@ -125,7 +125,7 @@
     7.4          fun mk_prem ((dt, s), T) =
     7.5            let val (Us, U) = strip_type T
     7.6            in
     7.7 -            list_all (map (pair "x") Us,
     7.8 +            Logic.list_all (map (pair "x") Us,
     7.9                HOLogic.mk_Trueprop
    7.10                  (make_pred (Datatype_Aux.body_index dt) U $
    7.11                    Datatype_Aux.app_bnds (Free (s, T)) (length Us)))
     8.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Jan 14 19:06:05 2012 +0100
     8.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Jan 14 20:05:58 2012 +0100
     8.3 @@ -74,7 +74,7 @@
     8.4                    val (p, f) = mk_prems (vs @ [r]) ds;
     8.5                  in
     8.6                    (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
     8.7 -                    (list_all (map (pair "x") Us, HOLogic.mk_Trueprop
     8.8 +                    (Logic.list_all (map (pair "x") Us, HOLogic.mk_Trueprop
     8.9                        (make_pred k rT U (Datatype_Aux.app_bnds r i)
    8.10                          (Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f)
    8.11                  end;
     9.1 --- a/src/HOL/Tools/Function/termination.ML	Sat Jan 14 19:06:05 2012 +0100
     9.2 +++ b/src/HOL/Tools/Function/termination.ML	Sat Jan 14 20:05:58 2012 +0100
     9.3 @@ -171,7 +171,7 @@
     9.4    let
     9.5      fun try rel =
     9.6        try_proof (cterm_of thy
     9.7 -        (Term.list_all (vs,
     9.8 +        (Logic.list_all (vs,
     9.9             Logic.mk_implies (HOLogic.mk_Trueprop Gam,
    9.10               HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
    9.11                 $ (m2 $ r) $ (m1 $ l)))))) tac
    10.1 --- a/src/HOL/Tools/inductive.ML	Sat Jan 14 19:06:05 2012 +0100
    10.2 +++ b/src/HOL/Tools/inductive.ML	Sat Jan 14 20:05:58 2012 +0100
    10.3 @@ -423,7 +423,7 @@
    10.4          val frees = map Free (anames ~~ Ts);
    10.5  
    10.6          fun mk_elim_prem ((_, _, us, _), ts, params') =
    10.7 -          list_all (params',
    10.8 +          Logic.list_all (params',
    10.9              Logic.list_implies (map (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   10.10                (frees ~~ us) @ ts, P));
   10.11          val c_intrs = filter (equal c o #1 o #1 o #1) intrs;
    11.1 --- a/src/HOL/Tools/record.ML	Sat Jan 14 19:06:05 2012 +0100
    11.2 +++ b/src/HOL/Tools/record.ML	Sat Jan 14 20:05:58 2012 +0100
    11.3 @@ -1121,7 +1121,7 @@
    11.4                  SOME (trm, trm', vars) =>
    11.5                    SOME
    11.6                      (prove_unfold_defs thy [] []
    11.7 -                      (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
    11.8 +                      (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
    11.9                | NONE => NONE)
   11.10              end
   11.11            else NONE
   11.12 @@ -1249,7 +1249,7 @@
   11.13          if simp then
   11.14            SOME
   11.15              (prove_unfold_defs thy noops' [simproc]
   11.16 -              (list_all (vars, Logic.mk_equals (lhs, rhs))))
   11.17 +              (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
   11.18          else NONE
   11.19        end);
   11.20  
   11.21 @@ -1345,7 +1345,7 @@
   11.22             (let
   11.23               val eq = mkeq (dest_sel_eq t) 0;
   11.24               val prop =
   11.25 -               list_all ([("r", T)],
   11.26 +               Logic.list_all ([("r", T)],
   11.27                   Logic.mk_equals
   11.28                    (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
   11.29              in
    12.1 --- a/src/HOL/ex/SVC_Oracle.thy	Sat Jan 14 19:06:05 2012 +0100
    12.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Sat Jan 14 20:05:58 2012 +0100
    12.3 @@ -101,7 +101,7 @@
    12.4      fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
    12.5        | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
    12.6        | mt t = fm t  (*it might be a formula*)
    12.7 -  in (list_all (params, mt body), !pairs) end;
    12.8 +  in (Logic.list_all (params, mt body), !pairs) end;
    12.9  
   12.10  
   12.11  (*Present the entire subgoal to the oracle, assumptions and all, but possibly
    13.1 --- a/src/Pure/logic.ML	Sat Jan 14 19:06:05 2012 +0100
    13.2 +++ b/src/Pure/logic.ML	Sat Jan 14 20:05:58 2012 +0100
    13.3 @@ -11,6 +11,7 @@
    13.4    val all: term -> term -> term
    13.5    val is_all: term -> bool
    13.6    val dest_all: term -> (string * typ) * term
    13.7 +  val list_all: (string * typ) list * term -> term
    13.8    val mk_equals: term * term -> term
    13.9    val dest_equals: term -> term * term
   13.10    val implies: term
   13.11 @@ -104,6 +105,9 @@
   13.12        in ((x, T), b) end
   13.13    | dest_all t = raise TERM ("dest_all", [t]);
   13.14  
   13.15 +fun list_all ([], t) = t
   13.16 +  | list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t));
   13.17 +
   13.18  
   13.19  (** equality **)
   13.20  
   13.21 @@ -453,8 +457,7 @@
   13.22      let val params = strip_params A;
   13.23          val vars = ListPair.zip (Name.variant_list [] (map #1 params),
   13.24                                   map #2 params)
   13.25 -    in  list_all (vars, remove_params (length vars) n A)
   13.26 -    end;
   13.27 +    in list_all (vars, remove_params (length vars) n A) end;
   13.28  
   13.29  (*Makes parameters in a goal have the names supplied by the list cs.*)
   13.30  fun list_rename_params cs (Const ("==>", _) $ A $ B) =
    14.1 --- a/src/Pure/primitive_defs.ML	Sat Jan 14 19:06:05 2012 +0100
    14.2 +++ b/src/Pure/primitive_defs.ML	Sat Jan 14 20:05:58 2012 +0100
    14.3 @@ -64,7 +64,7 @@
    14.4      else if exists_subterm (fn t => t aconv head) rhs then
    14.5        err "Entity to be defined occurs on rhs"
    14.6      else
    14.7 -      ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
    14.8 +      ((lhs, rhs), fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
    14.9    end;
   14.10  
   14.11  (*!!x. c x == t[x] to c == %x. t[x]*)
    15.1 --- a/src/Pure/term.ML	Sat Jan 14 19:06:05 2012 +0100
    15.2 +++ b/src/Pure/term.ML	Sat Jan 14 20:05:58 2012 +0100
    15.3 @@ -97,7 +97,6 @@
    15.4    val lambda: term -> term -> term
    15.5    val absfree: string * typ -> term -> term
    15.6    val absdummy: typ -> term -> term
    15.7 -  val list_all: (string * typ) list * term -> term
    15.8    val subst_atomic: (term * term) list -> term -> term
    15.9    val typ_subst_atomic: (typ * typ) list -> typ -> typ
   15.10    val subst_atomic_types: (typ * typ) list -> term -> term
   15.11 @@ -760,11 +759,6 @@
   15.12  fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body));
   15.13  fun absdummy T body = Abs (Name.uu_, T, body);
   15.14  
   15.15 -(*Quantification over a list of variables (already bound in body) *)
   15.16 -fun list_all ([], t) = t
   15.17 -  | list_all ((a,T)::vars, t) =
   15.18 -      Const ("all", (T --> propT) --> propT) $ Abs (a, T, list_all (vars, t));
   15.19 -
   15.20  (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
   15.21    A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   15.22  fun subst_atomic [] tm = tm
    16.1 --- a/src/Pure/thm.ML	Sat Jan 14 19:06:05 2012 +0100
    16.2 +++ b/src/Pure/thm.ML	Sat Jan 14 20:05:58 2012 +0100
    16.3 @@ -1404,17 +1404,17 @@
    16.4    let
    16.5      val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
    16.6      val (tpairs, Bs, Bi, C) = dest_state (state, i);
    16.7 -    val params = Term.strip_all_vars Bi
    16.8 -    and rest   = Term.strip_all_body Bi;
    16.9 -    val asms   = Logic.strip_imp_prems rest
   16.10 -    and concl  = Logic.strip_imp_concl rest;
   16.11 +    val params = Term.strip_all_vars Bi;
   16.12 +    val rest = Term.strip_all_body Bi;
   16.13 +    val asms = Logic.strip_imp_prems rest
   16.14 +    val concl = Logic.strip_imp_concl rest;
   16.15      val n = length asms;
   16.16      val m = if k < 0 then n + k else k;
   16.17      val Bi' =
   16.18        if 0 = m orelse m = n then Bi
   16.19        else if 0 < m andalso m < n then
   16.20          let val (ps, qs) = chop m asms
   16.21 -        in list_all (params, Logic.list_implies (qs @ ps, concl)) end
   16.22 +        in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end
   16.23        else raise THM ("rotate_rule", k, [state]);
   16.24    in
   16.25      Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi m) der,