--- a/src/HOL/Import/shuffler.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Import/shuffler.ML Sat Jan 14 20:05:58 2012 +0100
@@ -152,8 +152,8 @@
fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t =
let
- val lhs = list_all ([xv,yv],t)
- val rhs = list_all ([yv,xv],swap_bound 0 t)
+ val lhs = Logic.list_all ([xv,yv],t)
+ val rhs = Logic.list_all ([yv,xv],swap_bound 0 t)
val rew = Logic.mk_equals (lhs,rhs)
val init = Thm.trivial (cterm_of thy rew)
in
--- a/src/HOL/Nominal/nominal_datatype.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sat Jan 14 20:05:58 2012 +0100
@@ -497,7 +497,7 @@
end
in (j + 1, j' + length Ts,
case dt'' of
- Datatype.DtRec k => list_all (map (pair "x") Us,
+ Datatype.DtRec k => Logic.list_all (map (pair "x") Us,
HOLogic.mk_Trueprop (Free (nth rep_set_names k,
T --> HOLogic.boolT) $ free')) :: prems
| _ => prems,
@@ -1143,7 +1143,7 @@
val (Us, U) = strip_type T;
val l = length Us;
in
- list_all (z :: map (pair "x") Us,
+ Logic.list_all (z :: map (pair "x") Us,
HOLogic.mk_Trueprop
(make_pred fsT (Datatype_Aux.body_index dt) U $ Bound l $
Datatype_Aux.app_bnds (Free (s, T)) l))
--- a/src/HOL/Nominal/nominal_inductive.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Sat Jan 14 20:05:58 2012 +0100
@@ -240,7 +240,7 @@
HOLogic.mk_Trueprop (lift_pred p ts));
val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term prem params')
in
- (list_all (params', prem), (rev vs, subst_bounds (vs, prem)))
+ (Logic.list_all (params', prem), (rev vs, subst_bounds (vs, prem)))
end) prems);
val ind_vars =
@@ -259,7 +259,7 @@
lift_pred' (Free (fs_ctxt_name, fsT)) p ts)) concls));
val vc_compat = map (fn (params, bvars, prems, (p, ts)) =>
- map (fn q => list_all (params, incr_boundvars ~1 (Logic.list_implies
+ map (fn q => Logic.list_all (params, incr_boundvars ~1 (Logic.list_implies
(map_filter (fn prem =>
if null (preds_of ps prem) then SOME prem
else map_term (split_conj (K o I) names) prem prem) prems, q))))
@@ -439,9 +439,9 @@
map (fn (prem, args, concl, (prems, _)) =>
let
fun mk_prem (ps, [], _, prems) =
- list_all (ps, Logic.list_implies (prems, concl))
+ Logic.list_all (ps, Logic.list_implies (prems, concl))
| mk_prem (ps, qs, _, prems) =
- list_all (ps, Logic.mk_implies
+ Logic.list_all (ps, Logic.mk_implies
(Logic.list_implies
(mk_distinct qs @
maps (fn (t, T) => map (fn u => HOLogic.mk_Trueprop
--- a/src/HOL/Nominal/nominal_inductive2.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Jan 14 20:05:58 2012 +0100
@@ -141,7 +141,7 @@
fun abs_params params t =
let val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term t params)
- in (list_all (params, t), (rev vs, subst_bounds (vs, t))) end;
+ in (Logic.list_all (params, t), (rev vs, subst_bounds (vs, t))) end;
fun inst_params thy (vs, p) th cts =
let val env = Pattern.first_order_match thy (p, prop_of th)
@@ -336,7 +336,7 @@
val _ $ (f $ (_ $ pi $ l) $ r) = prop_of th2
val th2' =
Goal.prove ctxt [] []
- (list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop
+ (Logic.list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop
(f $ fold_rev (NominalDatatype.mk_perm (rev pTs))
(pis1 @ pi :: pis2) l $ r)))
(fn _ => cut_facts_tac [th2] 1 THEN
--- a/src/HOL/Statespace/state_fun.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Statespace/state_fun.ML Sat Jan 14 20:05:58 2012 +0100
@@ -246,7 +246,7 @@
let
val eq1 =
Goal.prove ctxt [] []
- (list_all (vars, Logic.mk_equals (trm, trm')))
+ (Logic.list_all (vars, Logic.mk_equals (trm, trm')))
(fn _ => rtac meta_ext 1 THEN simp_tac ss1 1);
val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
in SOME (Thm.transitive eq1 eq2) end
@@ -308,7 +308,7 @@
(let
val (eq, eT, nT, swap) = mkeq (dest_sel_eq t) 0;
val prop =
- list_all ([("n", nT), ("x", eT)],
+ Logic.list_all ([("n", nT), ("x", eT)],
Logic.mk_equals (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
val thm = Drule.export_without_context (prove prop);
val thm' = if swap then swap_ex_eq OF [thm] else thm
--- a/src/HOL/Tools/Datatype/datatype.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Sat Jan 14 20:05:58 2012 +0100
@@ -156,7 +156,7 @@
val free_t =
Datatype_Aux.app_bnds (Datatype_Aux.mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
in
- (j + 1, list_all (map (pair "x") Ts,
+ (j + 1, Logic.list_all (map (pair "x") Ts,
HOLogic.mk_Trueprop
(Free (nth rep_set_names' k, UnivT') $ free_t)) :: prems,
mk_lim free_t Ts :: ts)
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Sat Jan 14 20:05:58 2012 +0100
@@ -125,7 +125,7 @@
fun mk_prem ((dt, s), T) =
let val (Us, U) = strip_type T
in
- list_all (map (pair "x") Us,
+ Logic.list_all (map (pair "x") Us,
HOLogic.mk_Trueprop
(make_pred (Datatype_Aux.body_index dt) U $
Datatype_Aux.app_bnds (Free (s, T)) (length Us)))
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Jan 14 20:05:58 2012 +0100
@@ -74,7 +74,7 @@
val (p, f) = mk_prems (vs @ [r]) ds;
in
(mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
- (list_all (map (pair "x") Us, HOLogic.mk_Trueprop
+ (Logic.list_all (map (pair "x") Us, HOLogic.mk_Trueprop
(make_pred k rT U (Datatype_Aux.app_bnds r i)
(Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f)
end;
--- a/src/HOL/Tools/Function/termination.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Tools/Function/termination.ML Sat Jan 14 20:05:58 2012 +0100
@@ -171,7 +171,7 @@
let
fun try rel =
try_proof (cterm_of thy
- (Term.list_all (vs,
+ (Logic.list_all (vs,
Logic.mk_implies (HOLogic.mk_Trueprop Gam,
HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
$ (m2 $ r) $ (m1 $ l)))))) tac
--- a/src/HOL/Tools/inductive.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Tools/inductive.ML Sat Jan 14 20:05:58 2012 +0100
@@ -423,7 +423,7 @@
val frees = map Free (anames ~~ Ts);
fun mk_elim_prem ((_, _, us, _), ts, params') =
- list_all (params',
+ Logic.list_all (params',
Logic.list_implies (map (HOLogic.mk_Trueprop o HOLogic.mk_eq)
(frees ~~ us) @ ts, P));
val c_intrs = filter (equal c o #1 o #1 o #1) intrs;
--- a/src/HOL/Tools/record.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/Tools/record.ML Sat Jan 14 20:05:58 2012 +0100
@@ -1121,7 +1121,7 @@
SOME (trm, trm', vars) =>
SOME
(prove_unfold_defs thy [] []
- (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
+ (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
| NONE => NONE)
end
else NONE
@@ -1249,7 +1249,7 @@
if simp then
SOME
(prove_unfold_defs thy noops' [simproc]
- (list_all (vars, Logic.mk_equals (lhs, rhs))))
+ (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
else NONE
end);
@@ -1345,7 +1345,7 @@
(let
val eq = mkeq (dest_sel_eq t) 0;
val prop =
- list_all ([("r", T)],
+ Logic.list_all ([("r", T)],
Logic.mk_equals
(Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
in
--- a/src/HOL/ex/SVC_Oracle.thy Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Sat Jan 14 20:05:58 2012 +0100
@@ -101,7 +101,7 @@
fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
| mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q)
| mt t = fm t (*it might be a formula*)
- in (list_all (params, mt body), !pairs) end;
+ in (Logic.list_all (params, mt body), !pairs) end;
(*Present the entire subgoal to the oracle, assumptions and all, but possibly
--- a/src/Pure/logic.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/Pure/logic.ML Sat Jan 14 20:05:58 2012 +0100
@@ -11,6 +11,7 @@
val all: term -> term -> term
val is_all: term -> bool
val dest_all: term -> (string * typ) * term
+ val list_all: (string * typ) list * term -> term
val mk_equals: term * term -> term
val dest_equals: term -> term * term
val implies: term
@@ -104,6 +105,9 @@
in ((x, T), b) end
| dest_all t = raise TERM ("dest_all", [t]);
+fun list_all ([], t) = t
+ | list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t));
+
(** equality **)
@@ -453,8 +457,7 @@
let val params = strip_params A;
val vars = ListPair.zip (Name.variant_list [] (map #1 params),
map #2 params)
- in list_all (vars, remove_params (length vars) n A)
- end;
+ in list_all (vars, remove_params (length vars) n A) end;
(*Makes parameters in a goal have the names supplied by the list cs.*)
fun list_rename_params cs (Const ("==>", _) $ A $ B) =
--- a/src/Pure/primitive_defs.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/Pure/primitive_defs.ML Sat Jan 14 20:05:58 2012 +0100
@@ -64,7 +64,7 @@
else if exists_subterm (fn t => t aconv head) rhs then
err "Entity to be defined occurs on rhs"
else
- ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
+ ((lhs, rhs), fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
end;
(*!!x. c x == t[x] to c == %x. t[x]*)
--- a/src/Pure/term.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/Pure/term.ML Sat Jan 14 20:05:58 2012 +0100
@@ -97,7 +97,6 @@
val lambda: term -> term -> term
val absfree: string * typ -> term -> term
val absdummy: typ -> term -> term
- val list_all: (string * typ) list * term -> term
val subst_atomic: (term * term) list -> term -> term
val typ_subst_atomic: (typ * typ) list -> typ -> typ
val subst_atomic_types: (typ * typ) list -> term -> term
@@ -760,11 +759,6 @@
fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body));
fun absdummy T body = Abs (Name.uu_, T, body);
-(*Quantification over a list of variables (already bound in body) *)
-fun list_all ([], t) = t
- | list_all ((a,T)::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. *)
fun subst_atomic [] tm = tm
--- a/src/Pure/thm.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/Pure/thm.ML Sat Jan 14 20:05:58 2012 +0100
@@ -1404,17 +1404,17 @@
let
val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
val (tpairs, Bs, Bi, C) = dest_state (state, i);
- val params = Term.strip_all_vars Bi
- and rest = Term.strip_all_body Bi;
- val asms = Logic.strip_imp_prems rest
- and concl = Logic.strip_imp_concl rest;
+ val params = Term.strip_all_vars Bi;
+ val rest = Term.strip_all_body Bi;
+ val asms = Logic.strip_imp_prems rest
+ val concl = Logic.strip_imp_concl rest;
val n = length asms;
val m = if k < 0 then n + k else k;
val Bi' =
if 0 = m orelse m = n then Bi
else if 0 < m andalso m < n then
let val (ps, qs) = chop m asms
- in list_all (params, Logic.list_implies (qs @ ps, concl)) end
+ in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end
else raise THM ("rotate_rule", k, [state]);
in
Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi m) der,