# HG changeset patch # User wenzelm # Date 1326567958 -3600 # Node ID ecf6375e2abb3d0301b6c2a0ca72c158d3ff963f # Parent 7b19666f0e3d253cec2207df6027be777f77a2ad renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all; diff -r 7b19666f0e3d -r ecf6375e2abb src/HOL/Import/shuffler.ML --- 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 diff -r 7b19666f0e3d -r ecf6375e2abb src/HOL/Nominal/nominal_datatype.ML --- 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)) diff -r 7b19666f0e3d -r ecf6375e2abb src/HOL/Nominal/nominal_inductive.ML --- 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 diff -r 7b19666f0e3d -r ecf6375e2abb src/HOL/Nominal/nominal_inductive2.ML --- 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 diff -r 7b19666f0e3d -r ecf6375e2abb src/HOL/Statespace/state_fun.ML --- 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 diff -r 7b19666f0e3d -r ecf6375e2abb src/HOL/Tools/Datatype/datatype.ML --- 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) diff -r 7b19666f0e3d -r ecf6375e2abb src/HOL/Tools/Datatype/datatype_prop.ML --- 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))) diff -r 7b19666f0e3d -r ecf6375e2abb src/HOL/Tools/Datatype/datatype_realizer.ML --- 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; diff -r 7b19666f0e3d -r ecf6375e2abb src/HOL/Tools/Function/termination.ML --- 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 diff -r 7b19666f0e3d -r ecf6375e2abb src/HOL/Tools/inductive.ML --- 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; diff -r 7b19666f0e3d -r ecf6375e2abb src/HOL/Tools/record.ML --- 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 diff -r 7b19666f0e3d -r ecf6375e2abb src/HOL/ex/SVC_Oracle.thy --- 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 diff -r 7b19666f0e3d -r ecf6375e2abb src/Pure/logic.ML --- 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) = diff -r 7b19666f0e3d -r ecf6375e2abb src/Pure/primitive_defs.ML --- 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]*) diff -r 7b19666f0e3d -r ecf6375e2abb src/Pure/term.ML --- 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 diff -r 7b19666f0e3d -r ecf6375e2abb src/Pure/thm.ML --- 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,