src/HOL/Library/positivstellensatz.ML
changeset 60642 48dd1cefb4ae
parent 59586 ddf6deaadfe8
child 60801 7664e0916eec
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri Jul 03 16:19:45 2015 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Sun Jul 05 15:02:30 2015 +0200
     1.3 @@ -483,7 +483,7 @@
     1.4      fun real_not_eq_conv ct =
     1.5        let
     1.6          val (l,r) = dest_eq (Thm.dest_arg ct)
     1.7 -        val th = Thm.instantiate ([],[(@{cpat "?x::real"},l),(@{cpat "?y::real"},r)]) neq_th
     1.8 +        val th = Thm.instantiate ([],[((("x", 0), @{typ real}),l),((("y", 0), @{typ real}),r)]) neq_th
     1.9          val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
    1.10          val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
    1.11          val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
    1.12 @@ -729,9 +729,9 @@
    1.13        val pth_max = instantiate' [SOME @{ctyp real}] [] max_split
    1.14        val pth_min = instantiate' [SOME @{ctyp real}] [] min_split
    1.15        val abs_tm = @{cterm "abs :: real => _"}
    1.16 -      val p_tm = @{cpat "?P :: real => bool"}
    1.17 -      val x_tm = @{cpat "?x :: real"}
    1.18 -      val y_tm = @{cpat "?y::real"}
    1.19 +      val p_v = (("P", 0), @{typ "real \<Rightarrow> bool"})
    1.20 +      val x_v = (("x", 0), @{typ real})
    1.21 +      val y_v = (("y", 0), @{typ real})
    1.22        val is_max = is_binop @{cterm "max :: real => _"}
    1.23        val is_min = is_binop @{cterm "min :: real => _"}
    1.24        fun is_abs t = is_comb t andalso Thm.dest_fun t aconvc abs_tm
    1.25 @@ -746,16 +746,16 @@
    1.26  
    1.27        val elim_abs = eliminate_construct is_abs
    1.28          (fn p => fn ax =>
    1.29 -          Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax)]) pth_abs)
    1.30 +          Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax)]) pth_abs)
    1.31        val elim_max = eliminate_construct is_max
    1.32          (fn p => fn ax =>
    1.33            let val (ax,y) = Thm.dest_comb ax
    1.34 -          in Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)])
    1.35 +          in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)])
    1.36                               pth_max end)
    1.37        val elim_min = eliminate_construct is_min
    1.38          (fn p => fn ax =>
    1.39            let val (ax,y) = Thm.dest_comb ax
    1.40 -          in Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)])
    1.41 +          in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)])
    1.42                               pth_min end)
    1.43      in first_conv [elim_abs, elim_max, elim_min, all_conv]
    1.44      end;