# HG changeset patch # User wenzelm # Date 1329344370 -3600 # Node ID 89ccf66aa73d7adb0276ba021081cfa24d36996c # Parent b8920f3fd259b2e851a55899a37ca2cd1be064ad renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic; diff -r b8920f3fd259 -r 89ccf66aa73d NEWS --- 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. diff -r b8920f3fd259 -r 89ccf66aa73d doc-src/IsarImplementation/Thy/Logic.thy --- 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 diff -r b8920f3fd259 -r 89ccf66aa73d doc-src/IsarImplementation/Thy/document/Logic.tex --- 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 diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Boogie/Tools/boogie_vcs.ML --- 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) diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Decision_Procs/Dense_Linear_Order.thy --- 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 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 diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Decision_Procs/langford.ML --- 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)); diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/HOL.thy --- 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') diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Library/Efficient_Nat.thy --- 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'' => diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- 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 diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Library/positivstellensatz.ML --- 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)) diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Multivariate_Analysis/normarith.ML --- 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)) diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/Meson/meson_clausify.ML --- 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) diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/Qelim/cooper.ML --- 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)); diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/SMT/smt_normalize.ML --- 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) diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/SMT/smt_real.ML --- 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)}) diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/SMT/smt_solver.ML --- 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 diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/SMT/smt_utils.ML --- 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 diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/SMT/z3_interface.ML --- 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 diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/SMT/z3_proof_literals.ML --- 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}) diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/SMT/z3_proof_methods.ML --- 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 = diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/SMT/z3_proof_parser.ML --- 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) diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- 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 [] diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/SMT/z3_proof_tools.ML --- 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) diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/TFL/dcterm.ML --- 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; diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/groebner.ML --- 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; diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/numeral.ML --- 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; diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/numeral_simprocs.ML --- 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 diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/semiring_normalizer.ML --- 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; diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/transfer.ML --- 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 diff -r b8920f3fd259 -r 89ccf66aa73d src/Pure/conjunction.ML --- 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; diff -r b8920f3fd259 -r 89ccf66aa73d src/Pure/drule.ML --- 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")) diff -r b8920f3fd259 -r 89ccf66aa73d src/Pure/more_thm.ML --- 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 = diff -r b8920f3fd259 -r 89ccf66aa73d src/Pure/thm.ML --- 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) diff -r b8920f3fd259 -r 89ccf66aa73d src/Pure/variable.ML --- 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 = diff -r b8920f3fd259 -r 89ccf66aa73d src/Tools/Code/code_preproc.ML --- 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;