src/HOL/Library/positivstellensatz.ML
changeset 36945 9bec62c10714
parent 36753 5cf4e9128f22
child 37117 59cee8807c29
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -182,12 +182,12 @@
     1.4  
     1.5      (* Some useful derived rules *)
     1.6  fun deduct_antisym_rule tha thb = 
     1.7 -    equal_intr (implies_intr (cprop_of thb) tha) 
     1.8 -     (implies_intr (cprop_of tha) thb);
     1.9 +    Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha) 
    1.10 +     (Thm.implies_intr (cprop_of tha) thb);
    1.11  
    1.12  fun prove_hyp tha thb = 
    1.13    if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) 
    1.14 -  then equal_elim (symmetric (deduct_antisym_rule tha thb)) tha else thb;
    1.15 +  then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb;
    1.16  
    1.17  val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and
    1.18       "((x = y) == (x - y = 0))" and "((~(x < y)) == (x - y >= 0))" and
    1.19 @@ -375,7 +375,7 @@
    1.20   val skolemize_conv = Simplifier.rewrite (Simplifier.context ctxt skolemize_ss)
    1.21   val weak_dnf_ss = HOL_basic_ss addsimps weak_dnf_simps
    1.22   val weak_dnf_conv = Simplifier.rewrite (Simplifier.context ctxt weak_dnf_ss)
    1.23 - fun eqT_elim th = equal_elim (symmetric th) @{thm TrueI}
    1.24 + fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
    1.25   fun oprconv cv ct = 
    1.26    let val g = Thm.dest_fun2 ct
    1.27    in if g aconvc @{cterm "op <= :: real => _"} 
    1.28 @@ -387,7 +387,7 @@
    1.29    let
    1.30     val th' = (Thm.instantiate (Thm.match (Thm.lhs_of th, ct)) th 
    1.31        handle MATCH => raise CTERM ("real_ineq_conv", [ct]))
    1.32 -  in transitive th' (oprconv poly_conv (Thm.rhs_of th'))
    1.33 +  in Thm.transitive th' (oprconv poly_conv (Thm.rhs_of th'))
    1.34    end 
    1.35    val [real_lt_conv, real_le_conv, real_eq_conv,
    1.36         real_not_lt_conv, real_not_le_conv, _] =
    1.37 @@ -446,10 +446,10 @@
    1.38     let val (p,q) = Thm.dest_binop (concl th)
    1.39         val c = concl th1
    1.40         val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
    1.41 -   in implies_elim (implies_elim
    1.42 -          (implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
    1.43 -          (implies_intr (Thm.capply @{cterm Trueprop} p) th1))
    1.44 -        (implies_intr (Thm.capply @{cterm Trueprop} q) th2)
    1.45 +   in Thm.implies_elim (Thm.implies_elim
    1.46 +          (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
    1.47 +          (Thm.implies_intr (Thm.capply @{cterm Trueprop} p) th1))
    1.48 +        (Thm.implies_intr (Thm.capply @{cterm Trueprop} q) th2)
    1.49     end
    1.50   fun overall cert_choice dun ths = case ths of
    1.51    [] =>
    1.52 @@ -468,8 +468,8 @@
    1.53        overall cert_choice dun (th1::th2::oths) end
    1.54      else if is_disj ct then
    1.55        let 
    1.56 -       val (th1, cert1) = overall (Left::cert_choice) dun (assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
    1.57 -       val (th2, cert2) = overall (Right::cert_choice) dun (assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
    1.58 +       val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
    1.59 +       val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
    1.60        in (disj_cases th th1 th2, Branch (cert1, cert2)) end
    1.61     else overall cert_choice (th::dun) oths
    1.62    end
    1.63 @@ -487,12 +487,12 @@
    1.64      val th' = Drule.binop_cong_rule @{cterm "op |"} 
    1.65       (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
    1.66       (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
    1.67 -    in transitive th th' 
    1.68 +    in Thm.transitive th th' 
    1.69    end
    1.70   fun equal_implies_1_rule PQ = 
    1.71    let 
    1.72     val P = Thm.lhs_of PQ
    1.73 -  in implies_intr P (equal_elim PQ (assume P))
    1.74 +  in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P))
    1.75    end
    1.76   (* FIXME!!! Copied from groebner.ml *)
    1.77   val strip_exists =
    1.78 @@ -507,7 +507,7 @@
    1.79   | Var ((s,_),_) => s
    1.80   | _ => "x"
    1.81  
    1.82 -  fun mk_forall x th = Drule.arg_cong_rule (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" }) (abstract_rule (name_of x) x th)
    1.83 +  fun mk_forall x th = Drule.arg_cong_rule (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" }) (Thm.abstract_rule (name_of x) x th)
    1.84  
    1.85    val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
    1.86  
    1.87 @@ -523,12 +523,12 @@
    1.88           (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
    1.89       val pv = (Thm.rhs_of o Thm.beta_conversion true) 
    1.90             (Thm.capply @{cterm Trueprop} (Thm.capply p v))
    1.91 -     val th1 = forall_intr v (implies_intr pv th')
    1.92 -    in implies_elim (implies_elim th0 th) th1  end
    1.93 +     val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
    1.94 +    in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
    1.95   | _ => raise THM ("choose",0,[th, th'])
    1.96  
    1.97    fun simple_choose v th = 
    1.98 -     choose v (assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
    1.99 +     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
   1.100  
   1.101   val strip_forall =
   1.102    let fun h (acc, t) =
   1.103 @@ -558,11 +558,11 @@
   1.104      val (evs,bod) = strip_exists tm0
   1.105      val (avs,ibod) = strip_forall bod
   1.106      val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
   1.107 -    val (th2, certs) = overall [] [] [specl avs (assume (Thm.rhs_of th1))]
   1.108 -    val th3 = fold simple_choose evs (prove_hyp (equal_elim th1 (assume (Thm.capply @{cterm Trueprop} bod))) th2)
   1.109 -   in (Drule.implies_intr_hyps (prove_hyp (equal_elim th0 (assume nct)) th3), certs)
   1.110 +    val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
   1.111 +    val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.capply @{cterm Trueprop} bod))) th2)
   1.112 +   in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
   1.113     end
   1.114 -  in (implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
   1.115 +  in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
   1.116   end
   1.117  in f
   1.118  end;
   1.119 @@ -715,10 +715,10 @@
   1.120     fun eliminate_construct p c tm =
   1.121      let 
   1.122       val t = find_cterm p tm
   1.123 -     val th0 = (symmetric o beta_conversion false) (Thm.capply (Thm.cabs t tm) t)
   1.124 +     val th0 = (Thm.symmetric o Thm.beta_conversion false) (Thm.capply (Thm.cabs t tm) t)
   1.125       val (p,ax) = (Thm.dest_comb o Thm.rhs_of) th0
   1.126 -    in fconv_rule(arg_conv(binop_conv (arg_conv (beta_conversion false))))
   1.127 -               (transitive th0 (c p ax))
   1.128 +    in fconv_rule(arg_conv(binop_conv (arg_conv (Thm.beta_conversion false))))
   1.129 +               (Thm.transitive th0 (c p ax))
   1.130     end
   1.131  
   1.132     val elim_abs = eliminate_construct is_abs