--- a/src/HOL/Nominal/nominal_datatype.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sat Jan 14 21:16:15 2012 +0100
@@ -231,12 +231,13 @@
let val T = type_of x
in if Datatype_Aux.is_rec_type dt then
let val Us = binder_types T
- in list_abs (map (pair "x") Us,
- Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $
- list_comb (x, map (fn (i, U) =>
- Const ("Nominal.perm", permT --> U --> U) $
- (Const ("List.rev", permT --> permT) $ pi) $
- Bound i) ((length Us - 1 downto 0) ~~ Us)))
+ in
+ fold_rev (Term.abs o pair "x") Us
+ (Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $
+ list_comb (x, map (fn (i, U) =>
+ Const ("Nominal.perm", permT --> U --> U) $
+ (Const ("List.rev", permT --> permT) $ pi) $
+ Bound i) ((length Us - 1 downto 0) ~~ Us)))
end
else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
end;
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sat Jan 14 21:16:15 2012 +0100
@@ -23,7 +23,7 @@
val Ts = map snd ps;
val tinst' = map (fn (t, u) =>
(head_of (Logic.incr_indexes (Ts, j) t),
- list_abs (ps, u))) tinst;
+ fold_rev Term.abs ps u)) tinst;
val th' = instf
(map (pairself (ctyp_of thy)) tyinst')
(map (pairself (cterm_of thy)) tinst')
@@ -155,9 +155,10 @@
let val vars' = Misc_Legacy.term_vars (prop_of st);
val thy = theory_of_thm st;
in case subtract (op =) vars vars' of
- [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
+ [x] =>
+ Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st)
| _ => error "fresh_fun_simp: Too many variables, please report."
- end
+ end
in
((fn st =>
let
--- a/src/HOL/Nominal/nominal_permeq.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Sat Jan 14 21:16:15 2012 +0100
@@ -301,8 +301,8 @@
val s = fold_rev (fn v => fn s =>
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
vs HOLogic.unit;
- val s' = list_abs (ps,
- Const ("Nominal.supp", fastype_of1 (Ts, s) -->
+ val s' = fold_rev Term.abs ps
+ (Const ("Nominal.supp", fastype_of1 (Ts, s) -->
Term.range_type T) $ s);
val supports_rule' = Thm.lift_rule goal supports_rule;
val _ $ (_ $ S $ _) =
@@ -345,8 +345,9 @@
val s = fold_rev (fn v => fn s =>
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
vs HOLogic.unit;
- val s' = list_abs (ps,
- Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s);
+ val s' =
+ fold_rev Term.abs ps
+ (Const ("Nominal.supp", fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
val _ $ (_ $ S $ _) =
Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
--- a/src/HOL/Tools/Datatype/datatype.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Sat Jan 14 21:16:15 2012 +0100
@@ -381,8 +381,8 @@
(Logic.mk_implies
(HOLogic.mk_Trueprop (HOLogic.list_all
(map (pair "x") Ts, S $ Datatype_Aux.app_bnds f i)),
- HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
- r $ (a $ Datatype_Aux.app_bnds f i)), f))))
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (fold_rev (Term.abs o pair "x") Ts
+ (r $ (a $ Datatype_Aux.app_bnds f i)), f))))
(fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
REPEAT (etac allE 1), rtac thm 1, atac 1])
end
--- a/src/HOL/Tools/Datatype/datatype_case.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Sat Jan 14 21:16:15 2012 +0100
@@ -345,7 +345,7 @@
val (xs, ys) =
if j < i then (zs @ map (pair "x") (drop j Us), [])
else chop i zs;
- val u = list_abs (ys, strip_abs_body t);
+ val u = fold_rev Term.abs ys (strip_abs_body t);
val xs' = map Free
((fold_map Name.variant (map fst xs)
(Term.declare_term_names u used) |> fst) ~~
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Sat Jan 14 21:16:15 2012 +0100
@@ -235,8 +235,8 @@
fun mk_reccomb ((dt, T), t) =
let val (Us, U) = strip_type T in
- list_abs (map (pair "x") Us,
- nth reccombs (Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))
+ fold_rev (Term.abs o pair "x") Us
+ (nth reccombs (Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))
end;
val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees');
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Jan 14 21:16:15 2012 +0100
@@ -216,8 +216,8 @@
(map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
val r' =
Logic.varify_global (Abs ("y", T,
- list_abs (map dest_Free rs, list_comb (r,
- map Bound ((length rs - 1 downto 0) @ [length rs])))));
+ (fold_rev (Term.abs o dest_Free) rs
+ (list_comb (r, map Bound ((length rs - 1 downto 0) @ [length rs]))))));
in
Extraction.add_realizers_i
[(exh_name, (["P"], r', prf)),
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Jan 14 21:16:15 2012 +0100
@@ -2119,9 +2119,8 @@
fun ap_curry [_] _ t = t
| ap_curry arg_Ts tuple_T t =
let val n = length arg_Ts in
- list_abs (map (pair "c") arg_Ts,
- incr_boundvars n t
- $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
+ fold_rev (Term.abs o pair "c") arg_Ts
+ (incr_boundvars n t $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
end
fun num_occs_of_bound_in_term j (t1 $ t2) =
@@ -2182,9 +2181,9 @@
val step_body = recs |> map (repair_rec j)
|> List.foldl s_disj @{const False}
in
- (list_abs (tl xs, incr_bv (~1, j, base_body))
+ (fold_rev Term.abs (tl xs) (incr_bv (~1, j, base_body))
|> ap_n_split (length arg_Ts) tuple_T bool_T,
- Abs ("y", tuple_T, list_abs (tl xs, step_body)
+ Abs ("y", tuple_T, fold_rev Term.abs (tl xs) step_body
|> ap_n_split (length arg_Ts) tuple_T bool_T))
end
| aux t =
@@ -2235,7 +2234,7 @@
image_const $ (rtrancl_const $ step_set) $ base_set
|> predicatify tuple_T
in
- list_abs (outer, image_set |> ap_curry tuple_arg_Ts tuple_T)
+ fold_rev Term.abs outer (image_set |> ap_curry tuple_arg_Ts tuple_T)
|> unfold_defs_in_term hol_ctxt
end
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Sat Jan 14 21:16:15 2012 +0100
@@ -436,7 +436,7 @@
val bs = map (pair "x") inpTs
val bounds = map Bound (rev (0 upto (length bs) - 1))
val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)
- in list_abs (bs, mk_single compfuns (list_comb (f, bounds))) end
+ in fold_rev Term.abs bs (mk_single compfuns (list_comb (f, bounds))) end
fun register_alternative_function pred_name mode fun_name =
Alt_Compilations_Data.map (Symtab.insert_list (eq_pair eq_mode (K false))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Jan 14 21:16:15 2012 +0100
@@ -703,12 +703,12 @@
let
val bs = map (pair "x") (binder_types (fastype_of t))
val bounds = map Bound (rev (0 upto (length bs) - 1))
- in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end)
+ in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end)
| (t, Context m) =>
let
val bs = map (pair "x") (binder_types (fastype_of t))
val bounds = map Bound (rev (0 upto (length bs) - 1))
- in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end
+ in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end
| (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
(case (expr_of (t1, d1), expr_of (t2, d2)) of
(NONE, NONE) => NONE
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sat Jan 14 21:16:15 2012 +0100
@@ -235,10 +235,10 @@
Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e
val Ts = binder_types (fastype_of t)
in
- list_abs (map (pair "x") Ts @ [("b", @{typ bool})],
- mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)),
- HOLogic.mk_eq (@{term True}, Bound 0),
- HOLogic.mk_eq (@{term False}, Bound 0)))
+ fold_rev Term.abs (map (pair "x") Ts @ [("b", @{typ bool})])
+ (mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)),
+ HOLogic.mk_eq (@{term True}, Bound 0),
+ HOLogic.mk_eq (@{term False}, Bound 0)))
end
val argvs' = map2 lift_arg Ts argvs
val resname = singleton (Name.variant_list names') "res"
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Jan 14 21:16:15 2012 +0100
@@ -462,7 +462,7 @@
let
val frees = Term.add_frees t []
val t' = fold_rev absfree frees t
- fun wrap f t = list_abs (f (strip_abs t))
+ fun wrap f t = uncurry (fold_rev Term.abs) (f (strip_abs t))
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
fun ensure_testable t =
Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
--- a/src/HOL/Tools/inductive.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/inductive.ML Sat Jan 14 21:16:15 2012 +0100
@@ -652,9 +652,10 @@
val k = length Ts;
val bs = map Bound (k - 1 downto 0);
val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
- val Q = list_abs (mk_names "x" k ~~ Ts,
- HOLogic.mk_binop inductive_conj_name
- (list_comb (incr_boundvars k s, bs), P));
+ val Q =
+ fold_rev Term.abs (mk_names "x" k ~~ Ts)
+ (HOLogic.mk_binop inductive_conj_name
+ (list_comb (incr_boundvars k s, bs), P));
in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
| NONE =>
(case s of
@@ -760,9 +761,10 @@
val l = length Us;
val zs = map Bound (l - 1 downto 0);
in
- list_abs (map (pair "z") Us, list_comb (p,
- make_bool_args' bs i @ make_args argTs
- ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
+ fold_rev (Term.abs o pair "z") Us
+ (list_comb (p,
+ make_bool_args' bs i @ make_args argTs
+ ((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
end
| NONE =>
(case t of
--- a/src/HOL/Tools/inductive_realizer.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Sat Jan 14 21:16:15 2012 +0100
@@ -88,8 +88,9 @@
val u = list_comb (t, map Bound (i - 1 downto 0))
in
if member (op =) vs a then
- list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
- else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
+ fold_rev Term.abs (("r", U) :: xs) (mk_rlz U $ Bound i $ u)
+ else
+ fold_rev Term.abs xs (mk_rlz Extraction.nullT $ Extraction.nullt $ u)
end
| gen_rvar _ t = t;
@@ -164,24 +165,25 @@
let
val prem' :: prems' = prems;
val U = Extraction.etype_of thy vs [] prem';
- in if U = Extraction.nullT
+ in
+ if U = Extraction.nullT
then fun_of (Free (x, T) :: ts)
(Free (r, binder_types T ---> HOLogic.unitT) :: rts)
(Free (x, T) :: args) (x :: r :: used) prems'
else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts)
(Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
end
- else (case strip_type T of
+ else
+ (case strip_type T of
(Ts, Type (@{type_name Product_Type.prod}, [T1, T2])) =>
let
val fx = Free (x, Ts ---> T1);
val fr = Free (r, Ts ---> T2);
val bs = map Bound (length Ts - 1 downto 0);
- val t = list_abs (map (pair "z") Ts,
- HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)))
- in fun_of (fx :: ts) (fr :: rts) (t::args)
- (x :: r :: used) prems
- end
+ val t =
+ fold_rev (Term.abs o pair "z") Ts
+ (HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)));
+ in fun_of (fx :: ts) (fr :: rts) (t::args) (x :: r :: used) prems end
| (Ts, U) => fun_of (Free (x, T) :: ts)
(Free (r, binder_types T ---> HOLogic.unitT) :: rts)
(Free (x, T) :: args) (x :: r :: used) prems)
@@ -439,13 +441,16 @@
val T' = Extraction.etype_of thy (vs @ Ps) [] p;
val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T';
val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim);
- val r = if null Ps then Extraction.nullt
- else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
- (if dummy then
- [Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))]
- else []) @
- map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
- [Bound (length prems)]));
+ val r =
+ if null Ps then Extraction.nullt
+ else
+ fold_rev (Term.abs o pair "x") Ts
+ (list_comb (Const (case_name, T),
+ (if dummy then
+ [Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))]
+ else []) @
+ map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
+ [Bound (length prems)]));
val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
val rews = map mk_meta_eq case_thms;
--- a/src/HOL/Tools/inductive_set.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/inductive_set.ML Sat Jan 14 21:16:15 2012 +0100
@@ -101,7 +101,7 @@
NONE => NONE
| SOME (bop, (m, p, S, S')) =>
SOME (close (Goal.prove (Simplifier.the_context ss) [] [])
- (Logic.mk_equals (t, list_abs (xs, m $ p $ (bop $ S $ S'))))
+ (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S'))))
(K (EVERY
[rtac eq_reflection 1, REPEAT (rtac ext 1), rtac iffI 1,
EVERY [etac conjE 1, rtac IntI 1, simp, simp,
@@ -370,9 +370,9 @@
val x' = map_type (K (HOLogic.mk_setT T)) x
in
(cterm_of thy x,
- cterm_of thy (list_abs (map (pair "x") Ts, HOLogic.mk_mem
- (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
- end) fs
+ cterm_of thy (fold_rev (Term.abs o pair "x") Ts
+ (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
+ end) fs;
in
thm |>
Thm.instantiate ([], insts) |>
@@ -434,9 +434,9 @@
(x, (x',
(HOLogic.Collect_const T $
HOLogic.mk_psplits fs T HOLogic.boolT x',
- list_abs (map (pair "x") Ts, HOLogic.mk_mem
- (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)),
- x)))))
+ fold_rev (Term.abs o pair "x") Ts
+ (HOLogic.mk_mem
+ (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)), x)))))
end
| NONE => (x, (x, (x, x))))) params;
val (params1, (params2, params3)) =
@@ -503,8 +503,8 @@
Goal.prove lthy (map (fst o dest_Free) params) []
(HOLogic.mk_Trueprop (HOLogic.mk_eq
(list_comb (p, params3),
- list_abs (map (pair "x") Ts, HOLogic.mk_mem
- (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
+ fold_rev (Term.abs o pair "x") Ts
+ (HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
list_comb (c, params))))))
(K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
[def, mem_Collect_eq, @{thm split_conv}]) 1))
--- a/src/HOL/Tools/record.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/record.ML Sat Jan 14 21:16:15 2012 +0100
@@ -1484,8 +1484,8 @@
NONE => error "try_param_tac: no such variable"
| SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
| (_, T) :: _ =>
- [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
- (x, list_abs (params, Bound 0))])) rule';
+ [(P, fold_rev Term.abs params (if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
+ (x, fold_rev Term.abs params (Bound 0))])) rule';
in compose_tac (false, rule'', nprems_of rule) i end);
--- a/src/Provers/hypsubst.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Provers/hypsubst.ML Sat Jan 14 21:16:15 2012 +0100
@@ -156,18 +156,20 @@
val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
(Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
val (Ts, V) = split_last (Term.binder_types T);
- val u = list_abs (ps @ [("x", U)], case (if b then t else t') of
- Bound j => subst_bounds (map Bound
- ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
- | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
+ val u =
+ fold_rev Term.abs (ps @ [("x", U)])
+ (case (if b then t else t') of
+ Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
+ | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
val thy = Thm.theory_of_thm rl';
val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
- in compose_tac (true, Drule.instantiate_normalize (instT,
- map (pairself (cterm_of thy))
- [(Var (ixn, Ts ---> U --> body_type T), u),
- (Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),
- (Var (fst (dest_Var (head_of v2)), Ts ---> U), list_abs (ps, t'))]) rl',
- nprems_of rl) i
+ in
+ compose_tac (true, Drule.instantiate_normalize (instT,
+ map (pairself (cterm_of thy))
+ [(Var (ixn, Ts ---> U --> body_type T), u),
+ (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
+ (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
+ nprems_of rl) i
end
| NONE => no_tac);
--- a/src/Pure/Isar/auto_bind.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/Isar/auto_bind.ML Sat Jan 14 21:16:15 2012 +0100
@@ -26,7 +26,7 @@
fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl;
fun statement_binds thy name prop =
- [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
+ [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment thy prop)))];
(* goal *)
@@ -39,7 +39,7 @@
fun get_arg thy prop =
(case strip_judgment thy prop of
- _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
+ _ $ t => SOME (fold_rev Term.abs (Logic.strip_params prop) t)
| _ => NONE);
fun facts _ [] = []
--- a/src/Pure/Isar/obtain.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/Isar/obtain.ML Sat Jan 14 21:16:15 2012 +0100
@@ -286,7 +286,7 @@
val ts = map Free ps;
val asms =
Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
- |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));
+ |> map (fn asm => (Term.betapplys (fold_rev Term.abs ps asm, ts), []));
val _ = not (null asms) orelse error "Trivial result -- nothing guessed";
in
state'
--- a/src/Pure/Isar/rule_cases.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/Isar/rule_cases.ML Sat Jan 14 21:16:15 2012 +0100
@@ -76,7 +76,6 @@
local
-fun abs xs t = Term.list_abs (xs, t);
fun app us t = Term.betapplys (t, us);
fun dest_binops cs tm =
@@ -115,10 +114,12 @@
fun extract prop =
let
val (fixes1, fixes2) = extract_fixes case_outline prop;
- val abs_fixes = abs (fixes1 @ fixes2);
+ val abs_fixes = fold_rev Term.abs (fixes1 @ fixes2);
fun abs_fixes1 t =
if not nested then abs_fixes t
- else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
+ else
+ fold_rev Term.abs fixes1
+ (app (map (Term.dummy_pattern o #2) fixes2) (fold_rev Term.abs fixes2 t));
val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) hnames case_outline prop
|> pairself (map (apsnd (maps Logic.dest_conjunctions)));
--- a/src/Pure/Proof/extraction.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/Proof/extraction.ML Sat Jan 14 21:16:15 2012 +0100
@@ -283,11 +283,14 @@
val {typeof_eqns, ...} = ExtractionData.get thy;
fun err () = error ("Unable to determine type of extracted program for\n" ^
Syntax.string_of_term_global thy t)
- in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
- [typeof_proc [] vs]) (list_abs (map (pair "x") (rev Ts),
- Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
+ in
+ (case
+ strip_abs_body
+ (freeze_thaw (condrew thy (#net typeof_eqns) [typeof_proc [] vs])
+ (fold (Term.abs o pair "x") Ts
+ (Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ())
- | _ => err ()
+ | _ => err ())
end;
(** realizers for axioms / theorems, together with correctness proofs **)
@@ -513,9 +516,10 @@
fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
- fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
- (condrew thy' rrews (procs @ [typroc vs, rlz_proc])) (list_abs
- (map (pair "x") (rev Ts), t)));
+ fun app_rlz_rews Ts vs t =
+ strip_abs (length Ts)
+ (freeze_thaw (condrew thy' rrews (procs @ [typroc vs, rlz_proc]))
+ (fold (Term.abs o pair "x") Ts t));
fun realizes_null vs prop = app_rlz_rews [] vs
(Const ("realizes", nullT --> propT --> propT) $ nullt $ prop);
@@ -564,7 +568,7 @@
val u' = (case AList.lookup (op =) types (tname_of T) of
SOME ((_, SOME f)) => f r eT u T
| _ => Const ("realizes", eT --> T --> T) $ r $ u)
- in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end
+ in app_rlz_rews Ts vs (fold_rev (Term.abs o pair "x") Us' u') end
in (defs', corr_prf % SOME u) end
| corr d defs vs ts Ts hs cs (prf1 %% prf2) (prf1' %% prf2') t =
--- a/src/Pure/Proof/proof_rewrite_rules.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Sat Jan 14 21:16:15 2012 +0100
@@ -284,8 +284,8 @@
| hidden_variable (Free f) = not (member (op =) tf f)
| hidden_variable _ = false;
- fun mk_default' T = list_abs
- (apfst (map (pair "x")) (apsnd mk_default (strip_type T)));
+ fun mk_default' T =
+ fold_rev (Term.abs o pair "x") (binder_types T) (mk_default (body_type T));
fun elim_varst (t $ u) = elim_varst t $ elim_varst u
| elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
--- a/src/Pure/pattern.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/pattern.ML Sat Jan 14 21:16:15 2012 +0100
@@ -281,16 +281,18 @@
(* put a term into eta long beta normal form *)
fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
- | eta_long Ts t = (case strip_comb t of
- (Abs _, _) => eta_long Ts (Envir.beta_norm t)
- | (u, ts) =>
- let
- val Us = binder_types (fastype_of1 (Ts, t));
- val i = length Us
- in list_abs (map (pair "x") Us,
- list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
- (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
- end);
+ | eta_long Ts t =
+ (case strip_comb t of
+ (Abs _, _) => eta_long Ts (Envir.beta_norm t)
+ | (u, ts) =>
+ let
+ val Us = binder_types (fastype_of1 (Ts, t));
+ val i = length Us;
+ in
+ fold_rev (Term.abs o pair "x") Us
+ (list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
+ (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
+ end);
(*Tests whether 2 terms are alpha/eta-convertible and have same type.
--- a/src/Pure/term.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/term.ML Sat Jan 14 21:16:15 2012 +0100
@@ -56,7 +56,6 @@
val type_of: term -> typ
val fastype_of1: typ list * term -> typ
val fastype_of: term -> typ
- val list_abs: (string * typ) list * term -> term
val strip_abs: term -> (string * typ) list * term
val strip_abs_body: term -> term
val strip_abs_vars: term -> (string * typ) list
@@ -121,6 +120,7 @@
val itselfT: typ -> typ
val a_itselfT: typ
val argument_type_of: term -> int -> typ
+ val abs: string * typ -> term -> term
val add_tvar_namesT: typ -> indexname list -> indexname list
val add_tvar_names: term -> indexname list -> indexname list
val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
@@ -353,7 +353,7 @@
in arg k [] tm end;
-val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));
+fun abs (x, T) t = Abs (x, T, t);
fun strip_abs (Abs (a, T, t)) =
let val (a', t') = strip_abs t
--- a/src/Pure/unify.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/unify.ML Sat Jan 14 21:16:15 2012 +0100
@@ -339,7 +339,7 @@
in (env', map (fn var => Logic.combound (var, 0, length binder)) vars) end;
-(*Abstraction over a list of types, like list_abs*)
+(*Abstraction over a list of types*)
fun types_abs ([], u) = u
| types_abs (T :: Ts, u) = Abs ("", T, types_abs (Ts, u));
--- a/src/Tools/cong_tac.ML Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Tools/cong_tac.ML Sat Jan 14 21:16:15 2012 +0100
@@ -25,7 +25,7 @@
Logic.strip_assums_concl (Thm.prop_of cong');
val ps = Logic.strip_params (Thm.concl_of cong');
val insts = [(f', f), (g', g), (x', x), (y', y)]
- |> map (fn (t, u) => (cert (Term.head_of t), cert (Term.list_abs (ps, u))));
+ |> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
in
fn st => compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
handle THM _ => no_tac st