src/HOL/Library/positivstellensatz.ML
changeset 59582 0fbed69ff081
parent 59058 a78612c67ec0
child 59586 ddf6deaadfe8
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4  structure Symfunc = FuncFun(type key = string val ord = fast_string_ord);
     1.5  structure Termfunc = FuncFun(type key = term val ord = Term_Ord.fast_term_ord);
     1.6  
     1.7 -val cterm_ord = Term_Ord.fast_term_ord o apply2 term_of
     1.8 +val cterm_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of
     1.9  
    1.10  structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
    1.11  
    1.12 @@ -170,11 +170,11 @@
    1.13  
    1.14      (* Some useful derived rules *)
    1.15  fun deduct_antisym_rule tha thb =
    1.16 -    Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha)
    1.17 -     (Thm.implies_intr (cprop_of tha) thb);
    1.18 +    Thm.equal_intr (Thm.implies_intr (Thm.cprop_of thb) tha)
    1.19 +     (Thm.implies_intr (Thm.cprop_of tha) thb);
    1.20  
    1.21  fun prove_hyp tha thb =
    1.22 -  if exists (curry op aconv (concl_of tha)) (Thm.hyps_of thb)  (* FIXME !? *)
    1.23 +  if exists (curry op aconv (Thm.concl_of tha)) (Thm.hyps_of thb)  (* FIXME !? *)
    1.24    then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb;
    1.25  
    1.26  val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and
    1.27 @@ -279,10 +279,10 @@
    1.28  fun literals_conv bops uops cv =
    1.29    let
    1.30      fun h t =
    1.31 -      case (term_of t) of
    1.32 +      (case Thm.term_of t of
    1.33          b$_$_ => if member (op aconv) bops b then binop_conv h t else cv t
    1.34        | u$_ => if member (op aconv) uops u then arg_conv h t else cv t
    1.35 -      | _ => cv t
    1.36 +      | _ => cv t)
    1.37    in h end;
    1.38  
    1.39  fun cterm_of_rat x =
    1.40 @@ -296,9 +296,9 @@
    1.41    end;
    1.42  
    1.43  fun dest_ratconst t =
    1.44 -  case term_of t of
    1.45 +  case Thm.term_of t of
    1.46      Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.47 -  | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
    1.48 +  | _ => Rat.rat_of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
    1.49  fun is_ratconst t = can dest_ratconst t
    1.50  
    1.51  (*
    1.52 @@ -311,14 +311,14 @@
    1.53  
    1.54  fun find_cterm p t =
    1.55    if p t then t else
    1.56 -  case term_of t of
    1.57 +  case Thm.term_of t of
    1.58      _$_ => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t))
    1.59    | Abs (_,_,_) => find_cterm p (Thm.dest_abs NONE t |> snd)
    1.60    | _ => raise CTERM ("find_cterm",[t]);
    1.61  
    1.62      (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
    1.63  fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
    1.64 -fun is_comb t = case (term_of t) of _$_ => true | _ => false;
    1.65 +fun is_comb t = (case Thm.term_of t of _ $ _ => true | _ => false);
    1.66  
    1.67  fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
    1.68    handle CTERM _ => false;
    1.69 @@ -428,7 +428,7 @@
    1.70          nnf_conv ctxt then_conv skolemize_conv then_conv prenex_conv then_conv
    1.71          weak_dnf_conv
    1.72  
    1.73 -    val concl = Thm.dest_arg o cprop_of
    1.74 +    val concl = Thm.dest_arg o Thm.cprop_of
    1.75      fun is_binop opr ct = (Thm.dest_fun2 ct aconvc opr handle CTERM _ => false)
    1.76      val is_req = is_binop @{cterm "op =:: real => _"}
    1.77      val is_ge = is_binop @{cterm "op <=:: real => _"}
    1.78 @@ -501,36 +501,36 @@
    1.79      val strip_exists =
    1.80        let
    1.81          fun h (acc, t) =
    1.82 -          case (term_of t) of
    1.83 +          case Thm.term_of t of
    1.84              Const(@{const_name Ex},_)$Abs(_,_,_) =>
    1.85                h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    1.86            | _ => (acc,t)
    1.87        in fn t => h ([],t)
    1.88        end
    1.89      fun name_of x =
    1.90 -      case term_of x of
    1.91 +      case Thm.term_of x of
    1.92          Free(s,_) => s
    1.93        | Var ((s,_),_) => s
    1.94        | _ => "x"
    1.95  
    1.96      fun mk_forall x th =
    1.97        Drule.arg_cong_rule
    1.98 -        (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" })
    1.99 +        (instantiate_cterm' [SOME (Thm.ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" })
   1.100          (Thm.abstract_rule (name_of x) x th)
   1.101  
   1.102      val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
   1.103  
   1.104      fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   1.105 -    fun mk_ex v t = Thm.apply (ext (ctyp_of_term v)) (Thm.lambda v t)
   1.106 +    fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_term v)) (Thm.lambda v t)
   1.107  
   1.108      fun choose v th th' =
   1.109 -      case concl_of th of
   1.110 +      case Thm.concl_of th of
   1.111          @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
   1.112          let
   1.113 -          val p = (funpow 2 Thm.dest_arg o cprop_of) th
   1.114 -          val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
   1.115 +          val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
   1.116 +          val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_term) p
   1.117            val th0 = fconv_rule (Thm.beta_conversion true)
   1.118 -            (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
   1.119 +            (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
   1.120            val pv = (Thm.rhs_of o Thm.beta_conversion true)
   1.121              (Thm.apply @{cterm Trueprop} (Thm.apply p v))
   1.122            val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
   1.123 @@ -545,7 +545,7 @@
   1.124      val strip_forall =
   1.125        let
   1.126          fun h (acc, t) =
   1.127 -          case (term_of t) of
   1.128 +          case Thm.term_of t of
   1.129              Const(@{const_name All},_)$Abs(_,_,_) =>
   1.130                h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   1.131            | _ => (acc,t)
   1.132 @@ -693,15 +693,15 @@
   1.133        end
   1.134  
   1.135    fun is_alien ct =
   1.136 -      case term_of ct of
   1.137 -        Const(@{const_name "real"}, _)$ n =>
   1.138 -        if can HOLogic.dest_number n then false else true
   1.139 -      | _ => false
   1.140 +    case Thm.term_of ct of
   1.141 +      Const(@{const_name "real"}, _)$ n =>
   1.142 +      if can HOLogic.dest_number n then false else true
   1.143 +    | _ => false
   1.144  in
   1.145  fun real_linear_prover translator (eq,le,lt) =
   1.146    let
   1.147 -    val lhs = lin_of_hol o Thm.dest_arg1 o Thm.dest_arg o cprop_of
   1.148 -    val rhs = lin_of_hol o Thm.dest_arg o Thm.dest_arg o cprop_of
   1.149 +    val lhs = lin_of_hol o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of
   1.150 +    val rhs = lin_of_hol o Thm.dest_arg o Thm.dest_arg o Thm.cprop_of
   1.151      val eq_pols = map lhs eq
   1.152      val le_pols = map rhs le
   1.153      val lt_pols = map rhs lt
   1.154 @@ -770,7 +770,7 @@
   1.155  
   1.156  fun gen_prover_real_arith ctxt prover =
   1.157    let
   1.158 -    fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
   1.159 +    fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
   1.160      val {add, mul, neg, pow = _, sub = _, main} =
   1.161          Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
   1.162          (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))