renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
authorwenzelm
Sat Jan 14 19:06:05 2012 +0100 (2012-01-14)
changeset 462177b19666f0e3d
parent 46216 7fcdb5562461
child 46218 ecf6375e2abb
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/refute.ML
src/Pure/Isar/specification.ML
src/Pure/Proof/reconstruct.ML
src/Pure/logic.ML
src/Pure/term.ML
src/Pure/thm.ML
src/Tools/IsaPlanner/isand.ML
     1.1 --- a/src/HOL/Tools/Function/function_core.ML	Sat Jan 14 18:18:06 2012 +0100
     1.2 +++ b/src/HOL/Tools/Function/function_core.ML	Sat Jan 14 19:06:05 2012 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4            (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
     1.5              HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
     1.6          |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
     1.7 -        |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
     1.8 +        |> fold_rev (fn (n,T) => fn b => Logic.all_const T $ Abs(n,T,b)) (qs @ qs')
     1.9          |> curry abstract_over fvar
    1.10          |> curry subst_bound f
    1.11        end
    1.12 @@ -389,7 +389,7 @@
    1.13      val thy = Proof_Context.theory_of ctxt
    1.14  
    1.15      (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
    1.16 -    val ihyp = Term.all domT $ Abs ("z", domT,
    1.17 +    val ihyp = Logic.all_const domT $ Abs ("z", domT,
    1.18        Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
    1.19          HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
    1.20            Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
    1.21 @@ -600,7 +600,7 @@
    1.22        |> cterm_of thy
    1.23  
    1.24      (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
    1.25 -    val ihyp = Term.all domT $ Abs ("z", domT,
    1.26 +    val ihyp = Logic.all_const domT $ Abs ("z", domT,
    1.27        Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
    1.28          HOLogic.mk_Trueprop (P $ Bound 0)))
    1.29        |> cterm_of thy
    1.30 @@ -780,7 +780,7 @@
    1.31        |> cterm_of thy (* "wf R'" *)
    1.32  
    1.33      (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
    1.34 -    val ihyp = Term.all domT $ Abs ("z", domT,
    1.35 +    val ihyp = Logic.all_const domT $ Abs ("z", domT,
    1.36        Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
    1.37          HOLogic.mk_Trueprop (acc_R $ Bound 0)))
    1.38        |> cterm_of thy
     2.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sat Jan 14 18:18:06 2012 +0100
     2.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sat Jan 14 19:06:05 2012 +0100
     2.3 @@ -217,7 +217,7 @@
     2.4      val P_comp = mk_ind_goal thy branches
     2.5  
     2.6      (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
     2.7 -    val ihyp = Term.all T $ Abs ("z", T,
     2.8 +    val ihyp = Logic.all_const T $ Abs ("z", T,
     2.9        Logic.mk_implies
    2.10          (HOLogic.mk_Trueprop (
    2.11            Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 14 18:18:06 2012 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 14 19:06:05 2012 +0100
     3.3 @@ -894,7 +894,7 @@
     3.4    let
     3.5      fun close_up zs zs' =
     3.6        fold (fn (z as ((s, _), T)) => fn t' =>
     3.7 -               Term.all T $ Abs (s, T, abstract_over (Var z, t')))
     3.8 +               Logic.all_const T $ Abs (s, T, abstract_over (Var z, t')))
     3.9             (take (length zs' - length zs) zs')
    3.10      fun aux zs (@{const "==>"} $ t1 $ t2) =
    3.11          let val zs' = Term.add_vars t1 zs in
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Jan 14 18:18:06 2012 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Jan 14 19:06:05 2012 +0100
     4.3 @@ -163,7 +163,7 @@
     4.4    |> fold (fn ((s, i), T) => fn (t', taken) =>
     4.5                let val s' = singleton (Name.variant_list taken) s in
     4.6                  ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
     4.7 -                  else Term.all) T
     4.8 +                  else Logic.all_const) T
     4.9                   $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
    4.10                   s' :: taken)
    4.11                end)
     5.1 --- a/src/HOL/Tools/refute.ML	Sat Jan 14 18:18:06 2012 +0100
     5.2 +++ b/src/HOL/Tools/refute.ML	Sat Jan 14 19:06:05 2012 +0100
     5.3 @@ -416,7 +416,7 @@
     5.4      val vars = sort_wrt (fst o fst) (Term.add_vars t [])
     5.5    in
     5.6      fold (fn ((x, i), T) => fn t' =>
     5.7 -      Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
     5.8 +      Logic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
     5.9    end;
    5.10  
    5.11  val monomorphic_term = ATP_Util.monomorphic_term
     6.1 --- a/src/Pure/Isar/specification.ML	Sat Jan 14 18:18:06 2012 +0100
     6.2 +++ b/src/Pure/Isar/specification.ML	Sat Jan 14 19:06:05 2012 +0100
     6.3 @@ -102,7 +102,7 @@
     6.4        | abs_body _ _ a = a;
     6.5      fun close (y, U) B =
     6.6        let val B' = abs_body 0 y (Term.incr_boundvars 1 B)
     6.7 -      in if Term.is_dependent B' then Term.all dummyT $ Abs (y, U, B') else B end;
     6.8 +      in if Term.is_dependent B' then Logic.all_const dummyT $ Abs (y, U, B') else B end;
     6.9      fun close_form A =
    6.10        let
    6.11          val occ_frees = rev (Variable.add_free_names ctxt A []);
     7.1 --- a/src/Pure/Proof/reconstruct.ML	Sat Jan 14 18:18:06 2012 +0100
     7.2 +++ b/src/Pure/Proof/reconstruct.ML	Sat Jan 14 19:06:05 2012 +0100
     7.3 @@ -305,7 +305,7 @@
     7.4  
     7.5  fun prop_of0 Hs (PBound i) = nth Hs i
     7.6    | prop_of0 Hs (Abst (s, SOME T, prf)) =
     7.7 -      Term.all T $ (Abs (s, T, prop_of0 Hs prf))
     7.8 +      Logic.all_const T $ (Abs (s, T, prop_of0 Hs prf))
     7.9    | prop_of0 Hs (AbsP (s, SOME t, prf)) =
    7.10        Logic.mk_implies (t, prop_of0 (t :: Hs) prf)
    7.11    | prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of
     8.1 --- a/src/Pure/logic.ML	Sat Jan 14 18:18:06 2012 +0100
     8.2 +++ b/src/Pure/logic.ML	Sat Jan 14 19:06:05 2012 +0100
     8.3 @@ -7,6 +7,7 @@
     8.4  
     8.5  signature LOGIC =
     8.6  sig
     8.7 +  val all_const: typ -> term
     8.8    val all: term -> term -> term
     8.9    val is_all: term -> bool
    8.10    val dest_all: term -> (string * typ) * term
    8.11 @@ -91,7 +92,9 @@
    8.12  
    8.13  (** all **)
    8.14  
    8.15 -fun all v t = Const ("all", (Term.fastype_of v --> propT) --> propT) $ lambda v t;
    8.16 +fun all_const T = Const ("all", (T --> propT) --> propT);
    8.17 +
    8.18 +fun all v t = all_const (Term.fastype_of v) $ lambda v t;
    8.19  
    8.20  fun is_all (Const ("all", _) $ Abs _) = true
    8.21    | is_all _ = false;
    8.22 @@ -161,7 +164,7 @@
    8.23  
    8.24  (** conjunction **)
    8.25  
    8.26 -val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
    8.27 +val true_prop = all_const propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
    8.28  val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
    8.29  
    8.30  
     9.1 --- a/src/Pure/term.ML	Sat Jan 14 18:18:06 2012 +0100
     9.2 +++ b/src/Pure/term.ML	Sat Jan 14 19:06:05 2012 +0100
     9.3 @@ -121,7 +121,6 @@
     9.4    val aT: sort -> typ
     9.5    val itselfT: typ -> typ
     9.6    val a_itselfT: typ
     9.7 -  val all: typ -> term
     9.8    val argument_type_of: term -> int -> typ
     9.9    val add_tvar_namesT: typ -> indexname list -> indexname list
    9.10    val add_tvar_names: term -> indexname list -> indexname list
    9.11 @@ -579,9 +578,7 @@
    9.12  fun itselfT ty = Type ("itself", [ty]);
    9.13  val a_itselfT = itselfT (TFree (Name.aT, []));
    9.14  
    9.15 -val propT : typ = Type("prop",[]);
    9.16 -
    9.17 -fun all T = Const("all", (T-->propT)-->propT);
    9.18 +val propT : typ = Type ("prop",[]);
    9.19  
    9.20  (* maps  !!x1...xn. t   to   t  *)
    9.21  fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
    9.22 @@ -766,7 +763,7 @@
    9.23  (*Quantification over a list of variables (already bound in body) *)
    9.24  fun list_all ([], t) = t
    9.25    | list_all ((a,T)::vars, t) =
    9.26 -        all T $ Abs (a, T, list_all (vars, t));
    9.27 +      Const ("all", (T --> propT) --> propT) $ Abs (a, T, list_all (vars, t));
    9.28  
    9.29  (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
    9.30    A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
    10.1 --- a/src/Pure/thm.ML	Sat Jan 14 18:18:06 2012 +0100
    10.2 +++ b/src/Pure/thm.ML	Sat Jan 14 19:06:05 2012 +0100
    10.3 @@ -753,7 +753,7 @@
    10.4          shyps = Sorts.union sorts shyps,
    10.5          hyps = hyps,
    10.6          tpairs = tpairs,
    10.7 -        prop = Term.all T $ Abs (a, T, abstract_over (x, prop))});
    10.8 +        prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))});
    10.9      fun check_occs a x ts =
   10.10        if exists (fn t => Logic.occs (x, t)) ts then
   10.11          raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th])
   10.12 @@ -1588,7 +1588,7 @@
   10.13          val T' = Envir.subst_type (Envir.type_env env) T
   10.14          (*Must instantiate types of parameters because they are flattened;
   10.15            this could be a NEW parameter*)
   10.16 -      in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
   10.17 +      in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end
   10.18    | norm_term_skip env n (Const ("==>", _) $ A $ B) =
   10.19        Logic.mk_implies (A, norm_term_skip env (n - 1) B)
   10.20    | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??";
    11.1 --- a/src/Tools/IsaPlanner/isand.ML	Sat Jan 14 18:18:06 2012 +0100
    11.2 +++ b/src/Tools/IsaPlanner/isand.ML	Sat Jan 14 19:06:05 2012 +0100
    11.3 @@ -130,7 +130,7 @@
    11.4        val premts = Thm.prems_of th;
    11.5      
    11.6        fun allify_prem_var (vt as (n,ty),t)  = 
    11.7 -          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
    11.8 +          (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
    11.9  
   11.10        fun allify_prem Ts p = List.foldr allify_prem_var p Ts
   11.11  
   11.12 @@ -171,7 +171,7 @@
   11.13  fun assume_allified sgn (tyvs,vs) t = 
   11.14      let
   11.15        fun allify_var (vt as (n,ty),t)  = 
   11.16 -          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
   11.17 +          (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
   11.18        fun allify Ts p = List.foldr allify_var p Ts
   11.19  
   11.20        val ctermify = Thm.cterm_of sgn;
   11.21 @@ -303,7 +303,7 @@
   11.22  fun allify_term (v, t) = 
   11.23      let val vt = #t (Thm.rep_cterm v)
   11.24        val (n,ty) = Term.dest_Free vt
   11.25 -    in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
   11.26 +    in (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
   11.27  
   11.28  fun allify_for_sg_term ctermify vs t =
   11.29      let val t_alls = List.foldr allify_term t vs;