src/HOL/Tools/Qelim/cooper.ML
changeset 36945 9bec62c10714
parent 36833 9628f969d843
child 37117 59cee8807c29
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -331,7 +331,7 @@
     1.4  | t => if is_intrel t
     1.5        then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
     1.6         RS eq_reflection
     1.7 -      else reflexive ct;
     1.8 +      else Thm.reflexive ct;
     1.9  
    1.10  val dvdc = @{cterm "op dvd :: int => _"};
    1.11  
    1.12 @@ -369,7 +369,7 @@
    1.13        (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
    1.14             (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
    1.15             @{cterm "0::int"})))
    1.16 -   in equal_elim (Thm.symmetric th) TrueI end;
    1.17 +   in Thm.equal_elim (Thm.symmetric th) TrueI end;
    1.18    val notz =
    1.19      let val tab = fold Inttab.update
    1.20            (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
    1.21 @@ -412,11 +412,11 @@
    1.22    val ltx = Thm.capply (Thm.capply cmulC clt) cx
    1.23    val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
    1.24    val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
    1.25 -  val thf = transitive th
    1.26 -      (transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
    1.27 +  val thf = Thm.transitive th
    1.28 +      (Thm.transitive (Thm.symmetric (Thm.beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
    1.29    val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
    1.30 -                  ||> beta_conversion true |>> Thm.symmetric
    1.31 - in transitive (transitive lth thf) rth end;
    1.32 +                  ||> Thm.beta_conversion true |>> Thm.symmetric
    1.33 + in Thm.transitive (Thm.transitive lth thf) rth end;
    1.34  
    1.35  
    1.36  val emptyIS = @{cterm "{}::int set"};
    1.37 @@ -459,7 +459,7 @@
    1.38       Simplifier.rewrite lin_ss
    1.39        (Thm.capply @{cterm Trueprop}
    1.40             (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
    1.41 -   in equal_elim (Thm.symmetric th) TrueI end;
    1.42 +   in Thm.equal_elim (Thm.symmetric th) TrueI end;
    1.43   val dvd =
    1.44     let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
    1.45       fn ct => the (Inttab.lookup tab (term_of ct |> dest_number))
    1.46 @@ -471,7 +471,7 @@
    1.47     let val th = Simplifier.rewrite lin_ss
    1.48        (Thm.capply @{cterm Trueprop}
    1.49             (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
    1.50 -   in equal_elim (Thm.symmetric th) TrueI end;
    1.51 +   in Thm.equal_elim (Thm.symmetric th) TrueI end;
    1.52      (* A and B set *)
    1.53     local
    1.54       val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
    1.55 @@ -483,7 +483,7 @@
    1.56        | Const(@{const_name insert}, _) $ y $ _ =>
    1.57           let val (cy,S') = Thm.dest_binop S
    1.58           in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
    1.59 -         else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
    1.60 +         else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
    1.61                             (provein x S')
    1.62           end
    1.63     end
    1.64 @@ -494,14 +494,14 @@
    1.65     if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
    1.66     then
    1.67      (bl,b0,decomp_minf,
    1.68 -     fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
    1.69 +     fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
    1.70                       [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
    1.71                     (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
    1.72                          [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
    1.73                           bsetdisj,infDconj, infDdisj]),
    1.74                         cpmi)
    1.75       else (al,a0,decomp_pinf,fn A =>
    1.76 -          (map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
    1.77 +          (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
    1.78                     [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
    1.79                     (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
    1.80                     [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
    1.81 @@ -776,7 +776,7 @@
    1.82     fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
    1.83     val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
    1.84     val p' = fold_rev gen ts p
    1.85 - in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
    1.86 + in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
    1.87  
    1.88  local
    1.89  val ss1 = comp_ss
    1.90 @@ -792,7 +792,7 @@
    1.91              @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
    1.92    addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
    1.93  val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
    1.94 -  @ map (symmetric o mk_meta_eq) 
    1.95 +  @ map (Thm.symmetric o mk_meta_eq) 
    1.96      [@{thm "dvd_eq_mod_eq_0"},
    1.97       @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
    1.98       @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
    1.99 @@ -823,7 +823,7 @@
   1.100         then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
   1.101         else Conv.arg_conv (conv ctxt) p
   1.102      val p' = Thm.rhs_of cpth
   1.103 -    val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
   1.104 +    val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
   1.105     in rtac th i end
   1.106     handle COOPER _ => no_tac);
   1.107