1.1 --- a/src/HOL/Tools/Qelim/cooper.ML Wed Feb 15 22:44:31 2012 +0100
1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML Wed Feb 15 23:19:30 2012 +0100
1.3 @@ -144,7 +144,7 @@
1.4 let val (x,eq) =
1.5 (Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg)
1.6 (Thm.dest_arg t)
1.7 -in (Thm.cabs x o Thm.dest_arg o Thm.dest_arg) eq end;
1.8 +in (Thm.lambda x o Thm.dest_arg o Thm.dest_arg) eq end;
1.9
1.10 val get_pmi = get_pmi_term o cprop_of;
1.11
1.12 @@ -179,15 +179,15 @@
1.13 fun numeral2 f m n = HOLogic.mk_number iT (f (dest_number m) (dest_number n));
1.14
1.15 val [minus1,plus1] =
1.16 - map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd];
1.17 + map (fn c => fn t => Thm.apply (Thm.apply c t) cone) [cminus,cadd];
1.18
1.19 fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle,
1.20 asetgt, asetge,asetdvd,asetndvd,asetP,
1.21 infDdvd, infDndvd, asetconj,
1.22 asetdisj, infDconj, infDdisj] cp =
1.23 case (whatis x cp) of
1.24 - And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
1.25 -| Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
1.26 + And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.lambda x p) (Thm.lambda x q))
1.27 +| Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.lambda x p) (Thm.lambda x q))
1.28 | Eq t => ([], K (inst' [t] pieq, FWD (inst' [t] aseteq) [inS (plus1 t)], infDFalse))
1.29 | NEq t => ([], K (inst' [t] pineq, FWD (inst' [t] asetneq) [inS t], infDTrue))
1.30 | Lt t => ([], K (inst' [t] pilt, FWD (inst' [t] asetlt) [inS t], infDFalse))
1.31 @@ -206,8 +206,8 @@
1.32 infDdvd, infDndvd, bsetconj,
1.33 bsetdisj, infDconj, infDdisj] cp =
1.34 case (whatis x cp) of
1.35 - And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
1.36 -| Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
1.37 + And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.lambda x p) (Thm.lambda x q))
1.38 +| Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.lambda x p) (Thm.lambda x q))
1.39 | Eq t => ([], K (inst' [t] mieq, FWD (inst' [t] bseteq) [inS (minus1 t)], infDFalse))
1.40 | NEq t => ([], K (inst' [t] mineq, FWD (inst' [t] bsetneq) [inS t], infDTrue))
1.41 | Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue))
1.42 @@ -368,8 +368,8 @@
1.43 let
1.44 val th =
1.45 Simplifier.rewrite lin_ss
1.46 - (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
1.47 - (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
1.48 + (Thm.apply @{cterm Trueprop} (Thm.apply @{cterm "Not"}
1.49 + (Thm.apply (Thm.apply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
1.50 @{cterm "0::int"})))
1.51 in Thm.equal_elim (Thm.symmetric th) TrueI end;
1.52 val notz =
1.53 @@ -411,9 +411,9 @@
1.54 | _ => Thm.reflexive t
1.55 val uth = unit_conv p
1.56 val clt = Numeral.mk_cnumber @{ctyp "int"} l
1.57 - val ltx = Thm.capply (Thm.capply cmulC clt) cx
1.58 + val ltx = Thm.apply (Thm.apply cmulC clt) cx
1.59 val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
1.60 - val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
1.61 + val th' = inst' [Thm.lambda ltx (Thm.rhs_of uth), clt] unity_coeff_ex
1.62 val thf = Thm.transitive th
1.63 (Thm.transitive (Thm.symmetric (Thm.beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
1.64 val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
1.65 @@ -423,7 +423,7 @@
1.66
1.67 val emptyIS = @{cterm "{}::int set"};
1.68 val insert_tm = @{cterm "insert :: int => _"};
1.69 -fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS;
1.70 +fun mkISet cts = fold_rev (Thm.apply insert_tm #> Thm.apply) cts emptyIS;
1.71 val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1;
1.72 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
1.73 |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
1.74 @@ -459,8 +459,8 @@
1.75 let
1.76 val th =
1.77 Simplifier.rewrite lin_ss
1.78 - (Thm.capply @{cterm Trueprop}
1.79 - (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
1.80 + (Thm.apply @{cterm Trueprop}
1.81 + (Thm.apply (Thm.apply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
1.82 in Thm.equal_elim (Thm.symmetric th) TrueI end;
1.83 val dvd =
1.84 let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
1.85 @@ -471,8 +471,8 @@
1.86 end
1.87 val dp =
1.88 let val th = Simplifier.rewrite lin_ss
1.89 - (Thm.capply @{cterm Trueprop}
1.90 - (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
1.91 + (Thm.apply @{cterm Trueprop}
1.92 + (Thm.apply (Thm.apply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
1.93 in Thm.equal_elim (Thm.symmetric th) TrueI end;
1.94 (* A and B set *)
1.95 local
1.96 @@ -714,9 +714,9 @@
1.97 val (ps, c) = split_last (strip_objimp p)
1.98 val qs = filter P ps
1.99 val q = if P c then c else @{cterm "False"}
1.100 - val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs
1.101 - (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm HOL.implies} p) q) qs q)
1.102 - val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
1.103 + val ng = fold_rev (fn (a,v) => fn t => Thm.apply a (Thm.lambda v t)) qvs
1.104 + (fold_rev (fn p => fn q => Thm.apply (Thm.apply @{cterm HOL.implies} p) q) qs q)
1.105 + val g = Thm.apply (Thm.apply @{cterm "op ==>"} (Thm.apply @{cterm "Trueprop"} ng)) p'
1.106 val ntac = (case qs of [] => q aconvc @{cterm "False"}
1.107 | _ => false)
1.108 in
1.109 @@ -777,7 +777,7 @@
1.110 fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
1.111 let
1.112 fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
1.113 - fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
1.114 + fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
1.115 val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
1.116 val p' = fold_rev gen ts p
1.117 in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));