src/HOL/Library/positivstellensatz.ML
changeset 60801 7664e0916eec
parent 60642 48dd1cefb4ae
child 60949 ccbf9379e355
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Jul 27 16:35:12 2015 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Mon Jul 27 17:44:55 2015 +0200
     1.3 @@ -317,7 +317,7 @@
     1.4    | _ => raise CTERM ("find_cterm",[t]);
     1.5  
     1.6      (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
     1.7 -fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
     1.8 +fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
     1.9  fun is_comb t = (case Thm.term_of t of _ $ _ => true | _ => false);
    1.10  
    1.11  fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
    1.12 @@ -396,9 +396,9 @@
    1.13      fun add_rule th th' = fconv_rule (arg_conv (oprconv poly_add_conv))
    1.14           (match_mp_rule pth_add [th, th'])
    1.15      fun emul_rule ct th = fconv_rule (arg_conv (oprconv poly_mul_conv))
    1.16 -       (instantiate' [] [SOME ct] (th RS pth_emul))
    1.17 +       (Thm.instantiate' [] [SOME ct] (th RS pth_emul))
    1.18      fun square_rule t = fconv_rule (arg_conv (oprconv poly_conv))
    1.19 -       (instantiate' [] [SOME t] pth_square)
    1.20 +       (Thm.instantiate' [] [SOME t] pth_square)
    1.21  
    1.22      fun hol_of_positivstellensatz(eqs,les,lts) proof =
    1.23        let
    1.24 @@ -444,7 +444,7 @@
    1.25            if c aconvc (concl th2) then ()
    1.26            else error "disj_cases : conclusions not alpha convertible"
    1.27        in Thm.implies_elim (Thm.implies_elim
    1.28 -          (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
    1.29 +          (Thm.implies_elim (Thm.instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
    1.30            (Thm.implies_intr (Thm.apply @{cterm Trueprop} p) th1))
    1.31          (Thm.implies_intr (Thm.apply @{cterm Trueprop} q) th2)
    1.32        end
    1.33 @@ -518,9 +518,9 @@
    1.34          (instantiate_cterm' [SOME (Thm.ctyp_of_cterm x)] [] @{cpat "All :: (?'a => bool) => _" })
    1.35          (Thm.abstract_rule (name_of x) x th)
    1.36  
    1.37 -    val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
    1.38 +    val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
    1.39  
    1.40 -    fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
    1.41 +    fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex}
    1.42      fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
    1.43  
    1.44      fun choose v th th' =
    1.45 @@ -530,7 +530,7 @@
    1.46            val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
    1.47            val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
    1.48            val th0 = fconv_rule (Thm.beta_conversion true)
    1.49 -            (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
    1.50 +            (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
    1.51            val pv = (Thm.rhs_of o Thm.beta_conversion true)
    1.52              (Thm.apply @{cterm Trueprop} (Thm.apply p v))
    1.53            val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
    1.54 @@ -579,7 +579,7 @@
    1.55                  (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
    1.56            in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
    1.57            end
    1.58 -      in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
    1.59 +      in (Thm.implies_elim (Thm.instantiate' [] [SOME ct] pth_final) th, certificates)
    1.60        end
    1.61    in f
    1.62    end;
    1.63 @@ -710,7 +710,7 @@
    1.64                  (eq_pols @ le_pols @ lt_pols) [])
    1.65      val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
    1.66      val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
    1.67 -    val le' = le @ map (fn a => instantiate' [] [SOME (Thm.dest_arg a)] @{thm real_of_nat_ge_zero}) aliens
    1.68 +    val le' = le @ map (fn a => Thm.instantiate' [] [SOME (Thm.dest_arg a)] @{thm real_of_nat_ge_zero}) aliens
    1.69    in ((translator (eq,le',lt) proof), Trivial)
    1.70    end
    1.71  end;
    1.72 @@ -725,9 +725,9 @@
    1.73  
    1.74    val absmaxmin_elim_conv2 =
    1.75      let
    1.76 -      val pth_abs = instantiate' [SOME @{ctyp real}] [] abs_split'
    1.77 -      val pth_max = instantiate' [SOME @{ctyp real}] [] max_split
    1.78 -      val pth_min = instantiate' [SOME @{ctyp real}] [] min_split
    1.79 +      val pth_abs = Thm.instantiate' [SOME @{ctyp real}] [] abs_split'
    1.80 +      val pth_max = Thm.instantiate' [SOME @{ctyp real}] [] max_split
    1.81 +      val pth_min = Thm.instantiate' [SOME @{ctyp real}] [] min_split
    1.82        val abs_tm = @{cterm "abs :: real => _"}
    1.83        val p_v = (("P", 0), @{typ "real \<Rightarrow> bool"})
    1.84        val x_v = (("x", 0), @{typ real})