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.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})
```