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
```