renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
--- a/NEWS Wed Feb 15 22:44:31 2012 +0100
+++ b/NEWS Wed Feb 15 23:19:30 2012 +0100
@@ -332,6 +332,9 @@
*** ML ***
+* Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in
+conformance with similar operations in structure Term and Logic.
+
* Antiquotation @{attributes [...]} embeds attribute source
representation into the ML text, which is particularly useful with
declarations like Local_Theory.note.
--- a/doc-src/IsarImplementation/Thy/Logic.thy Wed Feb 15 22:44:31 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Wed Feb 15 23:19:30 2012 +0100
@@ -641,8 +641,8 @@
@{index_ML_type cterm} \\
@{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
@{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
- @{index_ML Thm.capply: "cterm -> cterm -> cterm"} \\
- @{index_ML Thm.cabs: "cterm -> cterm -> cterm"} \\
+ @{index_ML Thm.apply: "cterm -> cterm -> cterm"} \\
+ @{index_ML Thm.lambda: "cterm -> cterm -> cterm"} \\
@{index_ML Thm.all: "cterm -> cterm -> cterm"} \\
@{index_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\
\end{mldecls}
@@ -697,7 +697,7 @@
Full re-certification is relatively slow and should be avoided in
tight reasoning loops.
- \item @{ML Thm.capply}, @{ML Thm.cabs}, @{ML Thm.all}, @{ML
+ \item @{ML Thm.apply}, @{ML Thm.lambda}, @{ML Thm.all}, @{ML
Drule.mk_implies} etc.\ compose certified terms (or propositions)
incrementally. This is equivalent to @{ML Thm.cterm_of} after
unchecked @{ML_op "$"}, @{ML lambda}, @{ML Logic.all}, @{ML
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Feb 15 22:44:31 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Feb 15 23:19:30 2012 +0100
@@ -712,8 +712,8 @@
\indexdef{}{ML type}{cterm}\verb|type cterm| \\
\indexdef{}{ML}{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
\indexdef{}{ML}{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
- \indexdef{}{ML}{Thm.capply}\verb|Thm.capply: cterm -> cterm -> cterm| \\
- \indexdef{}{ML}{Thm.cabs}\verb|Thm.cabs: cterm -> cterm -> cterm| \\
+ \indexdef{}{ML}{Thm.apply}\verb|Thm.apply: cterm -> cterm -> cterm| \\
+ \indexdef{}{ML}{Thm.lambda}\verb|Thm.lambda: cterm -> cterm -> cterm| \\
\indexdef{}{ML}{Thm.all}\verb|Thm.all: cterm -> cterm -> cterm| \\
\indexdef{}{ML}{Drule.mk\_implies}\verb|Drule.mk_implies: cterm * cterm -> cterm| \\
\end{mldecls}
@@ -767,7 +767,7 @@
Full re-certification is relatively slow and should be avoided in
tight reasoning loops.
- \item \verb|Thm.capply|, \verb|Thm.cabs|, \verb|Thm.all|, \verb|Drule.mk_implies| etc.\ compose certified terms (or propositions)
+ \item \verb|Thm.apply|, \verb|Thm.lambda|, \verb|Thm.all|, \verb|Drule.mk_implies| etc.\ compose certified terms (or propositions)
incrementally. This is equivalent to \verb|Thm.cterm_of| after
unchecked \verb|$|, \verb|lambda|, \verb|Logic.all|, \verb|Logic.mk_implies| etc., but there can be a big difference in
performance when large existing entities are composed by a few extra
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Wed Feb 15 23:19:30 2012 +0100
@@ -220,7 +220,7 @@
fun join (Assume (_, pv), pthm) (Assume (t, v), thm) =
let
- val mk_prop = Thm.capply @{cterm Trueprop}
+ val mk_prop = Thm.apply @{cterm Trueprop}
val ct = Thm.cprop_of thm |> Thm.dest_arg |> Thm.dest_arg1 |> mk_prop
val th = Thm.assume ct
val (v', thm') = join (pv, imp_elim th pthm) (v, imp_elim th thm)
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Feb 15 23:19:30 2012 +0100
@@ -660,8 +660,8 @@
fun mk_frac phi cT x =
let val (a, b) = Rat.quotient_of_rat x
in if b = 1 then Numeral.mk_cnumber cT a
- else Thm.capply
- (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
+ else Thm.apply
+ (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
(Numeral.mk_cnumber cT a))
(Numeral.mk_cnumber cT b)
end
@@ -690,9 +690,9 @@
val cz = Thm.dest_arg ct
val neg = cr </ Rat.zero
val cthp = Simplifier.rewrite (simpset_of ctxt)
- (Thm.capply @{cterm "Trueprop"}
- (if neg then Thm.capply (Thm.capply clt c) cz
- else Thm.capply (Thm.capply clt cz) c))
+ (Thm.apply @{cterm "Trueprop"}
+ (if neg then Thm.apply (Thm.apply clt c) cz
+ else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t])
(if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
@@ -713,9 +713,9 @@
val cz = Thm.dest_arg ct
val neg = cr </ Rat.zero
val cthp = Simplifier.rewrite (simpset_of ctxt)
- (Thm.capply @{cterm "Trueprop"}
- (if neg then Thm.capply (Thm.capply clt c) cz
- else Thm.capply (Thm.capply clt cz) c))
+ (Thm.apply @{cterm "Trueprop"}
+ (if neg then Thm.apply (Thm.apply clt c) cz
+ else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
(if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
@@ -734,9 +734,9 @@
val cz = Thm.dest_arg ct
val neg = cr </ Rat.zero
val cthp = Simplifier.rewrite (simpset_of ctxt)
- (Thm.capply @{cterm "Trueprop"}
- (if neg then Thm.capply (Thm.capply clt c) cz
- else Thm.capply (Thm.capply clt cz) c))
+ (Thm.apply @{cterm "Trueprop"}
+ (if neg then Thm.apply (Thm.apply clt c) cz
+ else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
(if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
@@ -758,9 +758,9 @@
val cz = Thm.dest_arg ct
val neg = cr </ Rat.zero
val cthp = Simplifier.rewrite (simpset_of ctxt)
- (Thm.capply @{cterm "Trueprop"}
- (if neg then Thm.capply (Thm.capply clt c) cz
- else Thm.capply (Thm.capply clt cz) c))
+ (Thm.apply @{cterm "Trueprop"}
+ (if neg then Thm.apply (Thm.apply clt c) cz
+ else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
(if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
@@ -777,8 +777,8 @@
val ceq = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
val cthp = Simplifier.rewrite (simpset_of ctxt)
- (Thm.capply @{cterm "Trueprop"}
- (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
+ (Thm.apply @{cterm "Trueprop"}
+ (Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz)))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim
(instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
@@ -799,8 +799,8 @@
val ceq = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
val cthp = Simplifier.rewrite (simpset_of ctxt)
- (Thm.capply @{cterm "Trueprop"}
- (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
+ (Thm.apply @{cterm "Trueprop"}
+ (Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz)))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val rth = Thm.implies_elim
(instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Wed Feb 15 23:19:30 2012 +0100
@@ -125,12 +125,12 @@
Const(@{const_name HOL.conj},_)$_$_ =>
let val (p,q) = Thm.dest_binop fm
in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
- (Thm.cabs x p) (Thm.cabs x q))
+ (Thm.lambda x p) (Thm.lambda x q))
end
| Const(@{const_name HOL.disj},_)$_$_ =>
let val (p,q) = Thm.dest_binop fm
in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
- (Thm.cabs x p) (Thm.cabs x q))
+ (Thm.lambda x p) (Thm.lambda x q))
end
| _ =>
(let val c = wi x fm
--- a/src/HOL/Decision_Procs/langford.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Decision_Procs/langford.ML Wed Feb 15 23:19:30 2012 +0100
@@ -82,7 +82,7 @@
fun fold1 f = foldr1 (uncurry f);
-val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
+val list_conj = fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c') ;
fun mk_conj_tab th =
let fun h acc th =
@@ -128,7 +128,7 @@
let
val e = Thm.dest_fun ct
val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
- val Pp = Thm.capply @{cterm "Trueprop"} p
+ val Pp = Thm.apply @{cterm "Trueprop"} p
val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
in case eqs of
[] =>
@@ -137,14 +137,14 @@
in case ndx of [] => NONE
| _ =>
conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
- (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx))))
+ (Thm.apply @{cterm Trueprop} (list_conj (ndx @dx))))
|> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
|> Conv.fconv_rule (Conv.arg_conv
(Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms ex_simps})))
|> SOME
end
| _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
- (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs))))
+ (Thm.apply @{cterm Trueprop} (list_conj (eqs@neqs))))
|> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
|> Conv.fconv_rule (Conv.arg_conv
(Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms ex_simps})))
@@ -209,7 +209,7 @@
fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
let
fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
- fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
+ fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
val p' = fold_rev gen ts p
in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
--- a/src/HOL/HOL.thy Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/HOL.thy Wed Feb 15 23:19:30 2012 +0100
@@ -1271,7 +1271,7 @@
val cx = cterm_of thy x;
val {T = xT, ...} = rep_cterm cx;
val cf = cterm_of thy f;
- val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
+ val fx_g = Simplifier.rewrite ss (Thm.apply cf cx);
val (_ $ _ $ g) = prop_of fx_g;
val g' = abstract_over (x,g);
in (if (g aconv g')
--- a/src/HOL/Library/Efficient_Nat.thy Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Wed Feb 15 23:19:30 2012 +0100
@@ -124,8 +124,8 @@
| _ $ _ =>
let val (ct1, ct2) = Thm.dest_comb ct
in
- map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
- map (apfst (Thm.capply ct1)) (find_vars ct2)
+ map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @
+ map (apfst (Thm.apply ct1)) (find_vars ct2)
end
| _ => []);
val eqs = maps
@@ -136,8 +136,8 @@
Thm.implies_elim
(Conv.fconv_rule (Thm.beta_conversion true)
(Drule.instantiate'
- [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
- SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
+ [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
+ SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv']
@{thm Suc_if_eq})) (Thm.forall_intr cv' th)
in
case map_filter (fn th'' =>
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Feb 15 23:19:30 2012 +0100
@@ -772,7 +772,7 @@
(* FIXME : This is very bad!!!*)
fun subst_conv eqs t =
let
- val t' = fold (Thm.cabs o Thm.lhs_of) eqs t
+ val t' = fold (Thm.lambda o Thm.lhs_of) eqs t
in Conv.fconv_rule (Thm.beta_conversion true) (fold (C Thm.combination) eqs (Thm.reflexive t'))
end
@@ -819,7 +819,7 @@
fun make_substitution th =
let
val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th))
- val th1 = Drule.arg_cong_rule (Thm.capply @{cterm "op * :: real => _"} (RealArith.cterm_of_rat (Rat.inv c))) (mk_meta_eq th)
+ val th1 = Drule.arg_cong_rule (Thm.apply @{cterm "op * :: real => _"} (RealArith.cterm_of_rat (Rat.inv c))) (mk_meta_eq th)
val th2 = fconv_rule (binop_conv real_poly_mul_conv) th1
in fconv_rule (arg_conv real_poly_conv) (isolate_variable v th2)
end
--- a/src/HOL/Library/positivstellensatz.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Library/positivstellensatz.ML Wed Feb 15 23:19:30 2012 +0100
@@ -285,7 +285,7 @@
let val (a, b) = Rat.quotient_of_rat x
in
if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
- else Thm.capply (Thm.capply @{cterm "op / :: real => _"}
+ else Thm.apply (Thm.apply @{cterm "op / :: real => _"}
(Numeral.mk_cnumber @{ctyp "real"} a))
(Numeral.mk_cnumber @{ctyp "real"} b)
end;
@@ -319,7 +319,7 @@
(* Map back polynomials to HOL. *)
-fun cterm_of_varpow x k = if k = 1 then x else Thm.capply (Thm.capply @{cterm "op ^ :: real => _"} x)
+fun cterm_of_varpow x k = if k = 1 then x else Thm.apply (Thm.apply @{cterm "op ^ :: real => _"} x)
(Numeral.mk_cnumber @{ctyp nat} k)
fun cterm_of_monomial m =
@@ -328,12 +328,12 @@
let
val m' = FuncUtil.dest_monomial m
val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' []
- in foldr1 (fn (s, t) => Thm.capply (Thm.capply @{cterm "op * :: real => _"} s) t) vps
+ in foldr1 (fn (s, t) => Thm.apply (Thm.apply @{cterm "op * :: real => _"} s) t) vps
end
fun cterm_of_cmonomial (m,c) = if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
else if c = Rat.one then cterm_of_monomial m
- else Thm.capply (Thm.capply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
+ else Thm.apply (Thm.apply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
fun cterm_of_poly p =
if FuncUtil.Monomialfunc.is_empty p then @{cterm "0::real"}
@@ -341,7 +341,7 @@
let
val cms = map cterm_of_cmonomial
(sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p))
- in foldr1 (fn (t1, t2) => Thm.capply(Thm.capply @{cterm "op + :: real => _"} t1) t2) cms
+ in foldr1 (fn (t1, t2) => Thm.apply(Thm.apply @{cterm "op + :: real => _"} t1) t2) cms
end;
(* A general real arithmetic prover *)
@@ -397,14 +397,14 @@
Axiom_eq n => nth eqs n
| Axiom_le n => nth les n
| Axiom_lt n => nth lts n
- | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.capply @{cterm Trueprop}
- (Thm.capply (Thm.capply @{cterm "op =::real => _"} (mk_numeric x))
+ | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply @{cterm Trueprop}
+ (Thm.apply (Thm.apply @{cterm "op =::real => _"} (mk_numeric x))
@{cterm "0::real"})))
- | Rational_le x => eqT_elim(numeric_ge_conv(Thm.capply @{cterm Trueprop}
- (Thm.capply (Thm.capply @{cterm "op <=::real => _"}
+ | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply @{cterm Trueprop}
+ (Thm.apply (Thm.apply @{cterm "op <=::real => _"}
@{cterm "0::real"}) (mk_numeric x))))
- | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.capply @{cterm Trueprop}
- (Thm.capply (Thm.capply @{cterm "op <::real => _"} @{cterm "0::real"})
+ | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply @{cterm Trueprop}
+ (Thm.apply (Thm.apply @{cterm "op <::real => _"} @{cterm "0::real"})
(mk_numeric x))))
| Square pt => square_rule (cterm_of_poly pt)
| Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
@@ -432,8 +432,8 @@
val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
in Thm.implies_elim (Thm.implies_elim
(Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
- (Thm.implies_intr (Thm.capply @{cterm Trueprop} p) th1))
- (Thm.implies_intr (Thm.capply @{cterm Trueprop} q) th2)
+ (Thm.implies_intr (Thm.apply @{cterm Trueprop} p) th1))
+ (Thm.implies_intr (Thm.apply @{cterm Trueprop} q) th2)
end
fun overall cert_choice dun ths = case ths of
[] =>
@@ -452,8 +452,8 @@
overall cert_choice dun (th1::th2::oths) end
else if is_disj ct then
let
- val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
- val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
+ val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
+ val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
in (disj_cases th th1 th2, Branch (cert1, cert2)) end
else overall cert_choice (th::dun) oths
end
@@ -469,8 +469,8 @@
val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
val th' = Drule.binop_cong_rule @{cterm HOL.disj}
- (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
- (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
+ (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
+ (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
in Thm.transitive th th'
end
fun equal_implies_1_rule PQ =
@@ -496,7 +496,7 @@
val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
- fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
+ fun mk_ex v t = Thm.apply (ext (ctyp_of_term v)) (Thm.lambda v t)
fun choose v th th' = case concl_of th of
@{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
@@ -506,13 +506,13 @@
val th0 = fconv_rule (Thm.beta_conversion true)
(instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
val pv = (Thm.rhs_of o Thm.beta_conversion true)
- (Thm.capply @{cterm Trueprop} (Thm.capply p v))
+ (Thm.apply @{cterm Trueprop} (Thm.apply p v))
val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
in Thm.implies_elim (Thm.implies_elim th0 th) th1 end
| _ => raise THM ("choose",0,[th, th'])
fun simple_choose v th =
- choose v (Thm.assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
+ choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
val strip_forall =
let fun h (acc, t) =
@@ -534,7 +534,7 @@
fun absremover ct = (literals_conv [@{term HOL.conj}, @{term HOL.disj}] []
(try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv
try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
- val nct = Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} ct)
+ val nct = Thm.apply @{cterm Trueprop} (Thm.apply @{cterm "Not"} ct)
val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct
val tm0 = Thm.dest_arg (Thm.rhs_of th0)
val (th, certificates) = if tm0 aconvc @{cterm False} then (equal_implies_1_rule th0, Trivial) else
@@ -543,7 +543,7 @@
val (avs,ibod) = strip_forall bod
val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
- val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.capply @{cterm Trueprop} bod))) th2)
+ val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
end
in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
@@ -699,7 +699,7 @@
fun eliminate_construct p c tm =
let
val t = find_cterm p tm
- val th0 = (Thm.symmetric o Thm.beta_conversion false) (Thm.capply (Thm.cabs t tm) t)
+ val th0 = (Thm.symmetric o Thm.beta_conversion false) (Thm.apply (Thm.lambda t tm) t)
val (p,ax) = (Thm.dest_comb o Thm.rhs_of) th0
in fconv_rule(arg_conv(binop_conv (arg_conv (Thm.beta_conversion false))))
(Thm.transitive th0 (c p ax))
--- a/src/HOL/Multivariate_Analysis/normarith.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Wed Feb 15 23:19:30 2012 +0100
@@ -149,7 +149,7 @@
let val (a, b) = Rat.quotient_of_rat x
in
if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
- else Thm.capply (Thm.capply @{cterm "op / :: real => _"}
+ else Thm.apply (Thm.apply @{cterm "op / :: real => _"}
(Numeral.mk_cnumber @{ctyp "real"} a))
(Numeral.mk_cnumber @{ctyp "real"} b)
end;
@@ -335,8 +335,8 @@
val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
- fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
- fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
+ fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
+ fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (cterm_of (Proof_Context.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns
val replace_conv = try_conv (rewrs_conv asl)
val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
--- a/src/HOL/Tools/Meson/meson_clausify.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Wed Feb 15 23:19:30 2012 +0100
@@ -155,7 +155,7 @@
val (v, _) = dest_Free (term_of cv)
val u_th = introduce_combinators_in_cterm cta
val cu = Thm.rhs_of u_th
- val comb_eq = abstract (Thm.cabs cv cu)
+ val comb_eq = abstract (Thm.lambda cv cu)
in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
| _ $ _ =>
let val (ct1, ct2) = Thm.dest_comb ct in
@@ -205,10 +205,10 @@
| _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"",
[hilbert])
val cex = cterm_of thy (HOLogic.exists_const T)
- val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
+ val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
val conc =
Drule.list_comb (rhs, frees)
- |> Drule.beta_conv cabs |> Thm.capply cTrueprop
+ |> Drule.beta_conv cabs |> Thm.apply cTrueprop
fun tacf [prem] =
rewrite_goals_tac skolem_def_raw
THEN rtac ((prem |> rewrite_rule skolem_def_raw)
--- a/src/HOL/Tools/Qelim/cooper.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Feb 15 23:19:30 2012 +0100
@@ -144,7 +144,7 @@
let val (x,eq) =
(Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg)
(Thm.dest_arg t)
-in (Thm.cabs x o Thm.dest_arg o Thm.dest_arg) eq end;
+in (Thm.lambda x o Thm.dest_arg o Thm.dest_arg) eq end;
val get_pmi = get_pmi_term o cprop_of;
@@ -179,15 +179,15 @@
fun numeral2 f m n = HOLogic.mk_number iT (f (dest_number m) (dest_number n));
val [minus1,plus1] =
- map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd];
+ map (fn c => fn t => Thm.apply (Thm.apply c t) cone) [cminus,cadd];
fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle,
asetgt, asetge,asetdvd,asetndvd,asetP,
infDdvd, infDndvd, asetconj,
asetdisj, infDconj, infDdisj] cp =
case (whatis x cp) of
- And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
-| Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
+ And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.lambda x p) (Thm.lambda x q))
+| Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.lambda x p) (Thm.lambda x q))
| Eq t => ([], K (inst' [t] pieq, FWD (inst' [t] aseteq) [inS (plus1 t)], infDFalse))
| NEq t => ([], K (inst' [t] pineq, FWD (inst' [t] asetneq) [inS t], infDTrue))
| Lt t => ([], K (inst' [t] pilt, FWD (inst' [t] asetlt) [inS t], infDFalse))
@@ -206,8 +206,8 @@
infDdvd, infDndvd, bsetconj,
bsetdisj, infDconj, infDdisj] cp =
case (whatis x cp) of
- And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
-| Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
+ And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.lambda x p) (Thm.lambda x q))
+| Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.lambda x p) (Thm.lambda x q))
| Eq t => ([], K (inst' [t] mieq, FWD (inst' [t] bseteq) [inS (minus1 t)], infDFalse))
| NEq t => ([], K (inst' [t] mineq, FWD (inst' [t] bsetneq) [inS t], infDTrue))
| Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue))
@@ -368,8 +368,8 @@
let
val th =
Simplifier.rewrite lin_ss
- (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
- (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
+ (Thm.apply @{cterm Trueprop} (Thm.apply @{cterm "Not"}
+ (Thm.apply (Thm.apply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
@{cterm "0::int"})))
in Thm.equal_elim (Thm.symmetric th) TrueI end;
val notz =
@@ -411,9 +411,9 @@
| _ => Thm.reflexive t
val uth = unit_conv p
val clt = Numeral.mk_cnumber @{ctyp "int"} l
- val ltx = Thm.capply (Thm.capply cmulC clt) cx
+ val ltx = Thm.apply (Thm.apply cmulC clt) cx
val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
- val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
+ val th' = inst' [Thm.lambda ltx (Thm.rhs_of uth), clt] unity_coeff_ex
val thf = Thm.transitive th
(Thm.transitive (Thm.symmetric (Thm.beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
@@ -423,7 +423,7 @@
val emptyIS = @{cterm "{}::int set"};
val insert_tm = @{cterm "insert :: int => _"};
-fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS;
+fun mkISet cts = fold_rev (Thm.apply insert_tm #> Thm.apply) cts emptyIS;
val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1;
val [A_tm,B_tm] = map (fn th => cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
|> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
@@ -459,8 +459,8 @@
let
val th =
Simplifier.rewrite lin_ss
- (Thm.capply @{cterm Trueprop}
- (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
+ (Thm.apply @{cterm Trueprop}
+ (Thm.apply (Thm.apply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
in Thm.equal_elim (Thm.symmetric th) TrueI end;
val dvd =
let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
@@ -471,8 +471,8 @@
end
val dp =
let val th = Simplifier.rewrite lin_ss
- (Thm.capply @{cterm Trueprop}
- (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
+ (Thm.apply @{cterm Trueprop}
+ (Thm.apply (Thm.apply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
in Thm.equal_elim (Thm.symmetric th) TrueI end;
(* A and B set *)
local
@@ -714,9 +714,9 @@
val (ps, c) = split_last (strip_objimp p)
val qs = filter P ps
val q = if P c then c else @{cterm "False"}
- val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs
- (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm HOL.implies} p) q) qs q)
- val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
+ val ng = fold_rev (fn (a,v) => fn t => Thm.apply a (Thm.lambda v t)) qvs
+ (fold_rev (fn p => fn q => Thm.apply (Thm.apply @{cterm HOL.implies} p) q) qs q)
+ val g = Thm.apply (Thm.apply @{cterm "op ==>"} (Thm.apply @{cterm "Trueprop"} ng)) p'
val ntac = (case qs of [] => q aconvc @{cterm "False"}
| _ => false)
in
@@ -777,7 +777,7 @@
fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
let
fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
- fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
+ fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
val p' = fold_rev gen ts p
in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
--- a/src/HOL/Tools/SMT/smt_normalize.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Feb 15 23:19:30 2012 +0100
@@ -196,7 +196,7 @@
val pat =
SMT_Utils.mk_const_pat @{theory} @{const_name SMT.pat} SMT_Utils.destT1
- fun mk_pat ct = Thm.capply (SMT_Utils.instT' ct pat) ct
+ fun mk_pat ct = Thm.apply (SMT_Utils.instT' ct pat) ct
fun mk_clist T = pairself (Thm.cterm_of @{theory})
(HOLogic.cons_const T, HOLogic.nil_const T)
--- a/src/HOL/Tools/SMT/smt_real.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML Wed Feb 15 23:19:30 2012 +0100
@@ -67,7 +67,7 @@
if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
else NONE
- val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (real)})
+ val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)})
val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
--- a/src/HOL/Tools/SMT/smt_solver.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Feb 15 23:19:30 2012 +0100
@@ -283,7 +283,7 @@
val {facts, goal, ...} = Proof.goal st
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
- fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
+ fun negate ct = Thm.dest_comb ct ||> Thm.apply cnot |-> Thm.apply
val cprop =
(case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl)) of
SOME ct => ct
--- a/src/HOL/Tools/SMT/smt_utils.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_utils.ML Wed Feb 15 23:19:30 2012 +0100
@@ -182,7 +182,7 @@
val dest_all_cbinders = repeat_yield (try o dest_cbinder)
-val mk_cprop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
+val mk_cprop = Thm.apply (Thm.cterm_of @{theory} @{const Trueprop})
fun dest_cprop ct =
(case Thm.term_of ct of
--- a/src/HOL/Tools/SMT/z3_interface.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML Wed Feb 15 23:19:30 2012 +0100
@@ -138,7 +138,7 @@
val mk_true = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
val mk_false = Thm.cterm_of @{theory} @{const False}
-val mk_not = Thm.capply (Thm.cterm_of @{theory} @{const Not})
+val mk_not = Thm.apply (Thm.cterm_of @{theory} @{const Not})
val mk_implies = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.implies})
val mk_iff = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.eq (bool)})
val conj = Thm.cterm_of @{theory} @{const HOL.conj}
@@ -154,7 +154,7 @@
SMT_Utils.mk_const_pat @{theory} @{const_name If}
(SMT_Utils.destT1 o SMT_Utils.destT2)
fun mk_if cc ct cu =
- Thm.mk_binop (Thm.capply (SMT_Utils.instT' ct if_term) cc) ct cu
+ Thm.mk_binop (Thm.apply (SMT_Utils.instT' ct if_term) cc) ct cu
val nil_term =
SMT_Utils.mk_const_pat @{theory} @{const_name Nil} SMT_Utils.destT1
@@ -168,22 +168,22 @@
(SMT_Utils.destT1 o SMT_Utils.destT1)
fun mk_distinct [] = mk_true
| mk_distinct (cts as (ct :: _)) =
- Thm.capply (SMT_Utils.instT' ct distinct)
+ Thm.apply (SMT_Utils.instT' ct distinct)
(mk_list (Thm.ctyp_of_term ct) cts)
val access =
SMT_Utils.mk_const_pat @{theory} @{const_name fun_app} SMT_Utils.destT1
-fun mk_access array = Thm.capply (SMT_Utils.instT' array access) array
+fun mk_access array = Thm.apply (SMT_Utils.instT' array access) array
val update = SMT_Utils.mk_const_pat @{theory} @{const_name fun_upd}
(Thm.dest_ctyp o SMT_Utils.destT1)
fun mk_update array index value =
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
in
- Thm.capply (Thm.mk_binop (SMT_Utils.instTs cTs update) array index) value
+ Thm.apply (Thm.mk_binop (SMT_Utils.instTs cTs update) array index) value
end
-val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (int)})
+val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (int)})
val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (int)})
val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (int)})
val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (int)})
@@ -207,7 +207,7 @@
| (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) (* FIXME: remove *)
| (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu)
| (Sym ("distinct", _), _) => SOME (mk_distinct cts)
- | (Sym ("select", _), [ca, ck]) => SOME (Thm.capply (mk_access ca) ck)
+ | (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck)
| (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
| _ =>
(case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Wed Feb 15 23:19:30 2012 +0100
@@ -82,7 +82,7 @@
| NONE => false)
in exists end
-val negate = Thm.capply (Thm.cterm_of @{theory} @{const Not})
+val negate = Thm.apply (Thm.cterm_of @{theory} @{const Not})
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML Wed Feb 15 23:19:30 2012 +0100
@@ -109,7 +109,7 @@
SMT_Utils.dest_all_cbinders (SMT_Utils.dest_cprop rhs) ctxt
val (cl, cv) = Thm.dest_binop ct
val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last
- val cu = fold_rev Thm.cabs cargs (mk_inv_of ctxt' (Thm.cabs cv cf))
+ val cu = fold_rev Thm.lambda cargs (mk_inv_of ctxt' (Thm.lambda cv cf))
in Thm.assume (SMT_Utils.mk_cequals cg cu) end
fun prove_inj_eq ctxt ct =
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Wed Feb 15 23:19:30 2012 +0100
@@ -134,7 +134,7 @@
| _ => SMT_Utils.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T)))
fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
val vars' = map_filter dec vars
- in (Thm.capply (SMT_Utils.instT' cv q) (Thm.cabs cv ct), vars') end
+ in (Thm.apply (SMT_Utils.instT' cv q) (Thm.lambda cv ct), vars') end
fun quant name =
SMT_Utils.mk_const_pat @{theory} name (SMT_Utils.destT1 o SMT_Utils.destT1)
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Feb 15 23:19:30 2012 +0100
@@ -618,7 +618,7 @@
SMT_Utils.mk_const_pat @{theory} @{const_name all}
(SMT_Utils.destT1 o SMT_Utils.destT1)
fun mk_forall cv ct =
- Thm.capply (SMT_Utils.instT' cv forall) (Thm.cabs cv ct)
+ Thm.apply (SMT_Utils.instT' cv forall) (Thm.lambda cv ct)
fun get_vars f mk pred ctxt t =
Term.fold_aterms f t []
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Feb 15 23:19:30 2012 +0100
@@ -116,7 +116,7 @@
let
val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
val (cf, cvs) = Drule.strip_comb lhs
- val eq = SMT_Utils.mk_cequals cf (fold_rev Thm.cabs cvs rhs)
+ val eq = SMT_Utils.mk_cequals cf (fold_rev Thm.lambda cvs rhs)
fun apply cv th =
Thm.combination th (Thm.reflexive cv)
|> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
@@ -159,14 +159,14 @@
val cv = SMT_Utils.certify ctxt'
(Free (n, map SMT_Utils.typ_of cvs' ---> SMT_Utils.typ_of ct))
val cu = Drule.list_comb (cv, cvs')
- val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
+ val e = (t, (cv, fold_rev Thm.lambda cvs' ct))
val beta_norm' = beta_norm orelse not (null cvs')
in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
end
fun abs_comb f g dcvs ct =
let val (cf, cu) = Thm.dest_comb ct
- in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.capply end
+ in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.apply end
fun abs_arg f = abs_comb (K pair) f
@@ -184,7 +184,7 @@
fun abs_abs f (depth, cvs) ct =
let val (cv, cu) = Thm.dest_abs NONE ct
- in f (depth, cv :: cvs) cu #>> Thm.cabs cv end
+ in f (depth, cv :: cvs) cu #>> Thm.lambda cv end
val is_atomic =
(fn Free _ => true | Var _ => true | Bound _ => true | _ => false)
--- a/src/HOL/Tools/TFL/dcterm.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/TFL/dcterm.ML Wed Feb 15 23:19:30 2012 +0100
@@ -56,10 +56,10 @@
fun dest_abs a t = Thm.dest_abs a t
handle CTERM (msg, _) => raise ERR "dest_abs" msg;
-fun capply t u = Thm.capply t u
+fun capply t u = Thm.apply t u
handle CTERM (msg, _) => raise ERR "capply" msg;
-fun cabs a t = Thm.cabs a t
+fun cabs a t = Thm.lambda a t
handle CTERM (msg, _) => raise ERR "cabs" msg;
--- a/src/HOL/Tools/groebner.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/groebner.ML Wed Feb 15 23:19:30 2012 +0100
@@ -395,7 +395,7 @@
| _ => rfn tm ;
val notnotD = @{thm notnotD};
-fun mk_binop ct x y = Thm.capply (Thm.capply ct x) y
+fun mk_binop ct x y = Thm.apply (Thm.apply ct x) y
fun is_neg t =
case term_of t of
@@ -451,10 +451,10 @@
val cTrp = @{cterm "Trueprop"};
val cConj = @{cterm HOL.conj};
val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
-val assume_Trueprop = Thm.capply cTrp #> Thm.assume;
+val assume_Trueprop = Thm.apply cTrp #> Thm.assume;
val list_mk_conj = list_mk_binop cConj;
val conjs = list_dest_binop cConj;
-val mk_neg = Thm.capply cNot;
+val mk_neg = Thm.apply cNot;
fun striplist dest =
let
@@ -462,7 +462,7 @@
SOME (a,b) => h (h acc b) a
| NONE => x::acc
in h [] end;
-fun list_mk_binop b = foldr1 (fn (s,t) => Thm.capply (Thm.capply b s) t);
+fun list_mk_binop b = foldr1 (fn (s,t) => Thm.apply (Thm.apply b s) t);
val eq_commute = mk_meta_eq @{thm eq_commute};
@@ -479,7 +479,7 @@
fun fold1 f = foldr1 (uncurry f);
-val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
+val list_conj = fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c') ;
fun mk_conj_tab th =
let fun h acc th =
@@ -500,8 +500,8 @@
fun conj_ac_rule eq =
let
val (l,r) = Thm.dest_equals eq
- val ctabl = mk_conj_tab (Thm.assume (Thm.capply @{cterm Trueprop} l))
- val ctabr = mk_conj_tab (Thm.assume (Thm.capply @{cterm Trueprop} r))
+ val ctabl = mk_conj_tab (Thm.assume (Thm.apply @{cterm Trueprop} l))
+ val ctabr = mk_conj_tab (Thm.assume (Thm.apply @{cterm Trueprop} r))
fun tabl c = the (Termtab.lookup ctabl (term_of c))
fun tabr c = the (Termtab.lookup ctabr (term_of c))
val thl = prove_conj tabl (conjuncts r) |> implies_intr_hyps
@@ -514,7 +514,7 @@
(* Conversion for the equivalence of existential statements where
EX quantifiers are rearranged differently *)
fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
- fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
+ fun mk_ex v t = Thm.apply (ext (ctyp_of_term v)) (Thm.lambda v t)
fun choose v th th' = case concl_of th of
@{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
@@ -524,19 +524,19 @@
val th0 = Conv.fconv_rule (Thm.beta_conversion true)
(instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
val pv = (Thm.rhs_of o Thm.beta_conversion true)
- (Thm.capply @{cterm Trueprop} (Thm.capply p v))
+ (Thm.apply @{cterm Trueprop} (Thm.apply p v))
val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
in Thm.implies_elim (Thm.implies_elim th0 th) th1 end
| _ => error "" (* FIXME ? *)
fun simple_choose v th =
- choose v (Thm.assume ((Thm.capply @{cterm Trueprop} o mk_ex v)
+ choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v)
((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
fun mkexi v th =
let
- val p = Thm.cabs v (Thm.dest_arg (Thm.cprop_of th))
+ val p = Thm.lambda v (Thm.dest_arg (Thm.cprop_of th))
in Thm.implies_elim
(Conv.fconv_rule (Thm.beta_conversion true)
(instantiate' [SOME (ctyp_of_term v)] [SOME p, SOME v] @{thm exI}))
@@ -547,7 +547,7 @@
val (p0,q0) = Thm.dest_binop t
val (vs',P) = strip_exists p0
val (vs,_) = strip_exists q0
- val th = Thm.assume (Thm.capply @{cterm Trueprop} P)
+ val th = Thm.assume (Thm.apply @{cterm Trueprop} P)
val th1 = implies_intr_hyps (fold simple_choose vs' (fold mkexi vs th))
val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th))
val p = (Thm.dest_arg o Thm.dest_arg1 o cprop_of) th1
@@ -561,8 +561,8 @@
Free(s,_) => s
| Var ((s,_),_) => s
| _ => "x"
- fun mk_eq s t = Thm.capply (Thm.capply @{cterm "op == :: bool => _"} s) t
- fun mkeq s t = Thm.capply @{cterm Trueprop} (Thm.capply (Thm.capply @{cterm "op = :: bool => _"} s) t)
+ fun mk_eq s t = Thm.apply (Thm.apply @{cterm "op == :: bool => _"} s) t
+ fun mkeq s t = Thm.apply @{cterm Trueprop} (Thm.apply (Thm.apply @{cterm "op = :: bool => _"} s) t)
fun mk_exists v th = Drule.arg_cong_rule (ext (ctyp_of_term v))
(Thm.abstract_rule (getname v) v th)
val simp_ex_conv =
@@ -573,7 +573,7 @@
val vsubst = let
fun vsubst (t,v) tm =
- (Thm.rhs_of o Thm.beta_conversion false) (Thm.capply (Thm.cabs v tm) t)
+ (Thm.rhs_of o Thm.beta_conversion false) (Thm.apply (Thm.lambda v tm) t)
in fold vsubst end;
@@ -607,7 +607,7 @@
else raise CTERM ("ring_dest_neg", [t])
end
- val ring_mk_neg = fn tm => Thm.capply (ring_neg_tm) (tm);
+ val ring_mk_neg = fn tm => Thm.apply (ring_neg_tm) (tm);
fun field_dest_inv t =
let val (l,r) = Thm.dest_comb t in
if Term.could_unify(term_of l, term_of field_inv_tm) then r
@@ -727,7 +727,7 @@
((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1
val conc = th2 |> concl |> Thm.dest_arg
val (l,r) = conc |> dest_eq
- in Thm.implies_intr (Thm.capply cTrp tm)
+ in Thm.implies_intr (Thm.apply cTrp tm)
(Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th2))
(Thm.reflexive l |> mk_object_eq))
end
@@ -758,7 +758,7 @@
fun thm_fn pols =
if null pols then Thm.reflexive(mk_const rat_0) else
end_itlist mk_add
- (map (fn (i,p) => Drule.arg_cong_rule (Thm.capply ring_mul_tm p)
+ (map (fn (i,p) => Drule.arg_cong_rule (Thm.apply ring_mul_tm p)
(nth eths i |> mk_meta_eq)) pols)
val th1 = thm_fn herts_pos
val th2 = thm_fn herts_neg
@@ -767,7 +767,7 @@
Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv)
(neq_rule l th3)
val (l,r) = dest_eq(Thm.dest_arg(concl th4))
- in Thm.implies_intr (Thm.capply cTrp tm)
+ in Thm.implies_intr (Thm.apply cTrp tm)
(Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th4))
(Thm.reflexive l |> mk_object_eq))
end
@@ -776,9 +776,9 @@
fun ring tm =
let
fun mk_forall x p =
- Thm.capply
+ Thm.apply
(Drule.cterm_rule (instantiate' [SOME (ctyp_of_term x)] [])
- @{cpat "All:: (?'a => bool) => _"}) (Thm.cabs x p)
+ @{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
val avs = Thm.add_cterm_frees tm []
val P' = fold mk_forall avs tm
val th1 = initial_conv(mk_neg P')
@@ -892,7 +892,7 @@
(striplist ring_dest_add tm)
val cofactors = map (fn v => find_multipliers v vmons) vars
val cnc = if null cmons then zero_tm
- else Thm.capply ring_neg_tm
+ else Thm.apply ring_neg_tm
(list_mk_binop ring_add_tm cmons)
in (cofactors,cnc)
end;
--- a/src/HOL/Tools/numeral.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/numeral.ML Wed Feb 15 23:19:30 2012 +0100
@@ -24,7 +24,7 @@
| mk_cnumeral ~1 = @{cterm "Int.Min"}
| mk_cnumeral i =
let val (q, r) = Integer.div_mod i 2 in
- Thm.capply (mk_cbit r) (mk_cnumeral q)
+ Thm.apply (mk_cbit r) (mk_cnumeral q)
end;
@@ -47,7 +47,7 @@
fun mk_cnumber T 0 = instT T zeroT zero
| mk_cnumber T 1 = instT T oneT one
- | mk_cnumber T i = Thm.capply (instT T numberT number_of) (mk_cnumeral i);
+ | mk_cnumber T i = Thm.apply (instT T numberT number_of) (mk_cnumeral i);
end;
--- a/src/HOL/Tools/numeral_simprocs.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Wed Feb 15 23:19:30 2012 +0100
@@ -566,8 +566,8 @@
val z = Thm.instantiate_cterm ([(zT,T)],[]) zr
val eq = Thm.instantiate_cterm ([(eqT,T)],[]) geq
val th = Simplifier.rewrite (ss addsimps @{thms simp_thms})
- (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
- (Thm.capply (Thm.capply eq t) z)))
+ (Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"}
+ (Thm.apply (Thm.apply eq t) z)))
in Thm.equal_elim (Thm.symmetric th) TrueI
end
--- a/src/HOL/Tools/semiring_normalizer.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML Wed Feb 15 23:19:30 2012 +0100
@@ -199,8 +199,8 @@
fun mk_const phi cT x =
let val (a, b) = Rat.quotient_of_rat x
in if b = 1 then Numeral.mk_cnumber cT a
- else Thm.capply
- (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
+ else Thm.apply
+ (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
(Numeral.mk_cnumber cT a))
(Numeral.mk_cnumber cT b)
end
@@ -725,7 +725,7 @@
(* Power of polynomial (optimized for the monomial and trivial cases). *)
fun num_conv n =
- nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
+ nat_add_conv (Thm.apply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
|> Thm.symmetric;
--- a/src/HOL/Tools/transfer.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/transfer.ML Wed Feb 15 23:19:30 2012 +0100
@@ -109,7 +109,7 @@
val ([a, D], ctxt2) = ctxt1
|> Variable.import true (map Drule.mk_term [raw_a, raw_D])
|>> map Drule.dest_term o snd;
- val transform = Thm.capply @{cterm "Trueprop"} o Thm.capply D;
+ val transform = Thm.apply @{cterm "Trueprop"} o Thm.apply D;
val T = Thm.typ_of (Thm.ctyp_of_term a);
val (aT, bT) = (Term.range_type T, Term.domain_type T);
@@ -124,7 +124,7 @@
val c_vars = map (certify o Var) vars;
val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3;
val c_vars' = map (certify o (fn v => Free (v, bT))) vs';
- val c_exprs' = map (Thm.capply a) c_vars';
+ val c_exprs' = map (Thm.apply a) c_vars';
(* transfer *)
val (hyps, ctxt5) = ctxt4
--- a/src/Pure/conjunction.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/Pure/conjunction.ML Wed Feb 15 23:19:30 2012 +0100
@@ -35,7 +35,7 @@
val true_prop = certify Logic.true_prop;
val conjunction = certify Logic.conjunction;
-fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
+fun mk_conjunction (A, B) = Thm.apply (Thm.apply conjunction A) B;
fun mk_conjunction_balanced [] = true_prop
| mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
--- a/src/Pure/drule.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/Pure/drule.ML Wed Feb 15 23:19:30 2012 +0100
@@ -143,7 +143,7 @@
fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
val implies = certify Logic.implies;
-fun mk_implies (A, B) = Thm.capply (Thm.capply implies A) B;
+fun mk_implies (A, B) = Thm.apply (Thm.apply implies A) B;
(*cterm version of list_implies: [A1,...,An], B goes to [|A1;==>;An|]==>B *)
fun list_implies([], B) = B
@@ -151,7 +151,7 @@
(*cterm version of list_comb: maps (f, [t1,...,tn]) to f(t1,...,tn) *)
fun list_comb (f, []) = f
- | list_comb (f, t::ts) = list_comb (Thm.capply f t, ts);
+ | list_comb (f, t::ts) = list_comb (Thm.apply f t, ts);
(*cterm version of strip_comb: maps f(t1,...,tn) to (f, [t1,...,tn]) *)
fun strip_comb ct =
@@ -173,7 +173,7 @@
(*Beta-conversion for cterms, where x is an abstraction. Simply returns the rhs
of the meta-equality returned by the beta_conversion rule.*)
fun beta_conv x y =
- Thm.dest_arg (cprop_of (Thm.beta_conversion false (Thm.capply x y)));
+ Thm.dest_arg (cprop_of (Thm.beta_conversion false (Thm.apply x y)));
@@ -673,7 +673,7 @@
(* protect *)
-val protect = Thm.capply (certify Logic.protectC);
+val protect = Thm.apply (certify Logic.protectC);
val protectI =
store_standard_thm (Binding.conceal (Binding.name "protectI"))
--- a/src/Pure/more_thm.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/Pure/more_thm.ML Wed Feb 15 23:19:30 2012 +0100
@@ -120,11 +120,11 @@
let
val cert = Thm.cterm_of (Thm.theory_of_cterm t);
val T = #T (Thm.rep_cterm t);
- in Thm.capply (cert (Const ("all", (T --> propT) --> propT))) (Thm.cabs_name (x, t) A) end;
+ in Thm.apply (cert (Const ("all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
fun all t A = all_name ("", t) A;
-fun mk_binop c a b = Thm.capply (Thm.capply c a) b;
+fun mk_binop c a b = Thm.apply (Thm.apply c a) b;
fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct);
fun dest_implies ct =
--- a/src/Pure/thm.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/Pure/thm.ML Wed Feb 15 23:19:30 2012 +0100
@@ -75,9 +75,9 @@
val dest_fun2: cterm -> cterm
val dest_arg1: cterm -> cterm
val dest_abs: string option -> cterm -> cterm * cterm
- val capply: cterm -> cterm -> cterm
- val cabs_name: string * cterm -> cterm -> cterm
- val cabs: cterm -> cterm -> cterm
+ val apply: cterm -> cterm -> cterm
+ val lambda_name: string * cterm -> cterm -> cterm
+ val lambda: cterm -> cterm -> cterm
val adjust_maxidx_cterm: int -> cterm -> cterm
val incr_indexes_cterm: int -> cterm -> cterm
val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
@@ -259,7 +259,7 @@
(* constructors *)
-fun capply
+fun apply
(cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...})
(cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) =
if T = dty then
@@ -268,10 +268,10 @@
T = rty,
maxidx = Int.max (maxidx1, maxidx2),
sorts = Sorts.union sorts1 sorts2}
- else raise CTERM ("capply: types don't agree", [cf, cx])
- | capply cf cx = raise CTERM ("capply: first arg is not a function", [cf, cx]);
+ else raise CTERM ("apply: types don't agree", [cf, cx])
+ | apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]);
-fun cabs_name
+fun lambda_name
(x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
(ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) =
let val t = Term.lambda_name (x, t1) t2 in
@@ -281,7 +281,7 @@
sorts = Sorts.union sorts1 sorts2}
end;
-fun cabs t u = cabs_name ("", t) u;
+fun lambda t u = lambda_name ("", t) u;
(* indexes *)
@@ -1548,7 +1548,7 @@
if member (op =) ys y
then del_clashing true (x :: xs) (x :: ys) ps qs
else del_clashing clash xs (y :: ys) ps (p :: qs);
- val al'' = del_clashing false unchanged unchanged al' [];
+ val al'' = del_clashing false unchanged unchanged al' [];
fun rename (t as Var ((x, i), T)) =
(case AList.lookup (op =) al'' x of
SOME y => Var ((y, i), T)
--- a/src/Pure/variable.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/Pure/variable.ML Wed Feb 15 23:19:30 2012 +0100
@@ -539,7 +539,7 @@
in (((xs ~~ ps), t'), ctxt') end;
fun forall_elim_prop t prop =
- Thm.beta_conversion false (Thm.capply (Thm.dest_arg prop) t)
+ Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t)
|> Thm.cprop_of |> Thm.dest_arg;
fun focus_cterm goal ctxt =
--- a/src/Tools/Code/code_preproc.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/Tools/Code/code_preproc.ML Wed Feb 15 23:19:30 2012 +0100
@@ -117,7 +117,7 @@
|> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
in
ct
- |> fold_rev Thm.cabs all_vars
+ |> fold_rev Thm.lambda all_vars
|> conv
|> fold apply_beta all_vars
end;