--- a/src/HOL/Tools/Function/function_core.ML Sat Jan 14 18:18:06 2012 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Sat Jan 14 19:06:05 2012 +0100
@@ -115,7 +115,7 @@
(HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
|> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
- |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
+ |> fold_rev (fn (n,T) => fn b => Logic.all_const T $ Abs(n,T,b)) (qs @ qs')
|> curry abstract_over fvar
|> curry subst_bound f
end
@@ -389,7 +389,7 @@
val thy = Proof_Context.theory_of ctxt
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
- val ihyp = Term.all domT $ Abs ("z", domT,
+ val ihyp = Logic.all_const domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
@@ -600,7 +600,7 @@
|> cterm_of thy
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
- val ihyp = Term.all domT $ Abs ("z", domT,
+ val ihyp = Logic.all_const domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
HOLogic.mk_Trueprop (P $ Bound 0)))
|> cterm_of thy
@@ -780,7 +780,7 @@
|> cterm_of thy (* "wf R'" *)
(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
- val ihyp = Term.all domT $ Abs ("z", domT,
+ val ihyp = Logic.all_const domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
HOLogic.mk_Trueprop (acc_R $ Bound 0)))
|> cterm_of thy
--- a/src/HOL/Tools/Function/induction_schema.ML Sat Jan 14 18:18:06 2012 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Sat Jan 14 19:06:05 2012 +0100
@@ -217,7 +217,7 @@
val P_comp = mk_ind_goal thy branches
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
- val ihyp = Term.all T $ Abs ("z", T,
+ val ihyp = Logic.all_const T $ Abs ("z", T,
Logic.mk_implies
(HOLogic.mk_Trueprop (
Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Jan 14 18:18:06 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Jan 14 19:06:05 2012 +0100
@@ -894,7 +894,7 @@
let
fun close_up zs zs' =
fold (fn (z as ((s, _), T)) => fn t' =>
- Term.all T $ Abs (s, T, abstract_over (Var z, t')))
+ Logic.all_const T $ Abs (s, T, abstract_over (Var z, t')))
(take (length zs' - length zs) zs')
fun aux zs (@{const "==>"} $ t1 $ t2) =
let val zs' = Term.add_vars t1 zs in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Jan 14 18:18:06 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Jan 14 19:06:05 2012 +0100
@@ -163,7 +163,7 @@
|> fold (fn ((s, i), T) => fn (t', taken) =>
let val s' = singleton (Name.variant_list taken) s in
((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
- else Term.all) T
+ else Logic.all_const) T
$ Abs (s', T, abstract_over (Var ((s, i), T), t')),
s' :: taken)
end)
--- a/src/HOL/Tools/refute.ML Sat Jan 14 18:18:06 2012 +0100
+++ b/src/HOL/Tools/refute.ML Sat Jan 14 19:06:05 2012 +0100
@@ -416,7 +416,7 @@
val vars = sort_wrt (fst o fst) (Term.add_vars t [])
in
fold (fn ((x, i), T) => fn t' =>
- Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
+ Logic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
end;
val monomorphic_term = ATP_Util.monomorphic_term
--- a/src/Pure/Isar/specification.ML Sat Jan 14 18:18:06 2012 +0100
+++ b/src/Pure/Isar/specification.ML Sat Jan 14 19:06:05 2012 +0100
@@ -102,7 +102,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.is_dependent B' then Term.all dummyT $ Abs (y, U, B') else B end;
+ in if Term.is_dependent B' then Logic.all_const dummyT $ Abs (y, U, B') else B end;
fun close_form A =
let
val occ_frees = rev (Variable.add_free_names ctxt A []);
--- a/src/Pure/Proof/reconstruct.ML Sat Jan 14 18:18:06 2012 +0100
+++ b/src/Pure/Proof/reconstruct.ML Sat Jan 14 19:06:05 2012 +0100
@@ -305,7 +305,7 @@
fun prop_of0 Hs (PBound i) = nth Hs i
| prop_of0 Hs (Abst (s, SOME T, prf)) =
- Term.all T $ (Abs (s, T, prop_of0 Hs prf))
+ Logic.all_const T $ (Abs (s, T, prop_of0 Hs prf))
| prop_of0 Hs (AbsP (s, SOME t, prf)) =
Logic.mk_implies (t, prop_of0 (t :: Hs) prf)
| prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of
--- a/src/Pure/logic.ML Sat Jan 14 18:18:06 2012 +0100
+++ b/src/Pure/logic.ML Sat Jan 14 19:06:05 2012 +0100
@@ -7,6 +7,7 @@
signature LOGIC =
sig
+ val all_const: typ -> term
val all: term -> term -> term
val is_all: term -> bool
val dest_all: term -> (string * typ) * term
@@ -91,7 +92,9 @@
(** all **)
-fun all v t = Const ("all", (Term.fastype_of v --> propT) --> propT) $ lambda v t;
+fun all_const T = Const ("all", (T --> propT) --> propT);
+
+fun all v t = all_const (Term.fastype_of v) $ lambda v t;
fun is_all (Const ("all", _) $ Abs _) = true
| is_all _ = false;
@@ -161,7 +164,7 @@
(** conjunction **)
-val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
+val true_prop = all_const propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
--- a/src/Pure/term.ML Sat Jan 14 18:18:06 2012 +0100
+++ b/src/Pure/term.ML Sat Jan 14 19:06:05 2012 +0100
@@ -121,7 +121,6 @@
val aT: sort -> typ
val itselfT: typ -> typ
val a_itselfT: typ
- val all: typ -> term
val argument_type_of: term -> int -> typ
val add_tvar_namesT: typ -> indexname list -> indexname list
val add_tvar_names: term -> indexname list -> indexname list
@@ -579,9 +578,7 @@
fun itselfT ty = Type ("itself", [ty]);
val a_itselfT = itselfT (TFree (Name.aT, []));
-val propT : typ = Type("prop",[]);
-
-fun all T = Const("all", (T-->propT)-->propT);
+val propT : typ = Type ("prop",[]);
(* maps !!x1...xn. t to t *)
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t
@@ -766,7 +763,7 @@
(*Quantification over a list of variables (already bound in body) *)
fun list_all ([], t) = t
| list_all ((a,T)::vars, t) =
- all T $ Abs (a, T, list_all (vars, t));
+ Const ("all", (T --> propT) --> propT) $ Abs (a, T, list_all (vars, t));
(*Replace the ATOMIC term ti by ui; inst = [(t1,u1), ..., (tn,un)].
A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *)
--- a/src/Pure/thm.ML Sat Jan 14 18:18:06 2012 +0100
+++ b/src/Pure/thm.ML Sat Jan 14 19:06:05 2012 +0100
@@ -753,7 +753,7 @@
shyps = Sorts.union sorts shyps,
hyps = hyps,
tpairs = tpairs,
- prop = Term.all T $ Abs (a, T, abstract_over (x, prop))});
+ prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))});
fun check_occs a x ts =
if exists (fn t => Logic.occs (x, t)) ts then
raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th])
@@ -1588,7 +1588,7 @@
val T' = Envir.subst_type (Envir.type_env env) T
(*Must instantiate types of parameters because they are flattened;
this could be a NEW parameter*)
- in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
+ in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end
| norm_term_skip env n (Const ("==>", _) $ A $ B) =
Logic.mk_implies (A, norm_term_skip env (n - 1) B)
| norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??";
--- a/src/Tools/IsaPlanner/isand.ML Sat Jan 14 18:18:06 2012 +0100
+++ b/src/Tools/IsaPlanner/isand.ML Sat Jan 14 19:06:05 2012 +0100
@@ -130,7 +130,7 @@
val premts = Thm.prems_of th;
fun allify_prem_var (vt as (n,ty),t) =
- (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
+ (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
fun allify_prem Ts p = List.foldr allify_prem_var p Ts
@@ -171,7 +171,7 @@
fun assume_allified sgn (tyvs,vs) t =
let
fun allify_var (vt as (n,ty),t) =
- (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
+ (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
fun allify Ts p = List.foldr allify_var p Ts
val ctermify = Thm.cterm_of sgn;
@@ -303,7 +303,7 @@
fun allify_term (v, t) =
let val vt = #t (Thm.rep_cterm v)
val (n,ty) = Term.dest_Free vt
- in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
+ in (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
fun allify_for_sg_term ctermify vs t =
let val t_alls = List.foldr allify_term t vs;