src/HOL/Library/positivstellensatz.ML
changeset 32402 5731300da417
parent 31971 8c1b845ed105
child 32645 1cc5b24f5a01
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Aug 26 10:48:45 2009 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Aug 26 11:40:28 2009 +0200
     1.3 @@ -81,82 +81,6 @@
     1.4  structure Ctermfunc = FuncFun(type key = cterm val ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t)));
     1.5  
     1.6  structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
     1.7 -    (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
     1.8 -structure Conv2 = 
     1.9 -struct
    1.10 - open Conv
    1.11 -fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
    1.12 -fun is_comb t = case (term_of t) of _$_ => true | _ => false;
    1.13 -fun is_abs t = case (term_of t) of Abs _ => true | _ => false;
    1.14 -
    1.15 -fun end_itlist f l =
    1.16 - case l of 
    1.17 -   []     => error "end_itlist"
    1.18 - | [x]    => x
    1.19 - | (h::t) => f h (end_itlist f t);
    1.20 -
    1.21 - fun absc cv ct = case term_of ct of 
    1.22 - Abs (v,_, _) => 
    1.23 -  let val (x,t) = Thm.dest_abs (SOME v) ct
    1.24 -  in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t)
    1.25 -  end
    1.26 - | _ => all_conv ct;
    1.27 -
    1.28 -fun cache_conv conv =
    1.29 - let 
    1.30 -  val tab = ref Termtab.empty
    1.31 -  fun cconv t =  
    1.32 -    case Termtab.lookup (!tab) (term_of t) of
    1.33 -     SOME th => th
    1.34 -   | NONE => let val th = conv t
    1.35 -             in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end
    1.36 - in cconv end;
    1.37 -fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
    1.38 -  handle CTERM _ => false;
    1.39 -
    1.40 -local
    1.41 - fun thenqc conv1 conv2 tm =
    1.42 -   case try conv1 tm of
    1.43 -    SOME th1 => (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2 | NONE => th1)
    1.44 -  | NONE => conv2 tm
    1.45 -
    1.46 - fun thencqc conv1 conv2 tm =
    1.47 -    let val th1 = conv1 tm 
    1.48 -    in (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2 | NONE => th1)
    1.49 -    end
    1.50 - fun comb_qconv conv tm =
    1.51 -   let val (l,r) = Thm.dest_comb tm 
    1.52 -   in (case try conv l of 
    1.53 -        SOME th1 => (case try conv r of SOME th2 => Thm.combination th1 th2 
    1.54 -                                      | NONE => Drule.fun_cong_rule th1 r)
    1.55 -      | NONE => Drule.arg_cong_rule l (conv r))
    1.56 -   end
    1.57 - fun repeatqc conv tm = thencqc conv (repeatqc conv) tm 
    1.58 - fun sub_qconv conv tm =  if is_abs tm then absc conv tm else comb_qconv conv tm 
    1.59 - fun once_depth_qconv conv tm =
    1.60 -      (conv else_conv (sub_qconv (once_depth_qconv conv))) tm
    1.61 - fun depth_qconv conv tm =
    1.62 -    thenqc (sub_qconv (depth_qconv conv))
    1.63 -           (repeatqc conv) tm
    1.64 - fun redepth_qconv conv tm =
    1.65 -    thenqc (sub_qconv (redepth_qconv conv))
    1.66 -           (thencqc conv (redepth_qconv conv)) tm
    1.67 - fun top_depth_qconv conv tm =
    1.68 -    thenqc (repeatqc conv)
    1.69 -           (thencqc (sub_qconv (top_depth_qconv conv))
    1.70 -                    (thencqc conv (top_depth_qconv conv))) tm
    1.71 - fun top_sweep_qconv conv tm =
    1.72 -    thenqc (repeatqc conv)
    1.73 -           (sub_qconv (top_sweep_qconv conv)) tm
    1.74 -in 
    1.75 -val (once_depth_conv, depth_conv, rdepth_conv, top_depth_conv, top_sweep_conv) = 
    1.76 -  (fn c => try_conv (once_depth_qconv c),
    1.77 -   fn c => try_conv (depth_qconv c),
    1.78 -   fn c => try_conv (redepth_qconv c),
    1.79 -   fn c => try_conv (top_depth_qconv c),
    1.80 -   fn c => try_conv (top_sweep_qconv c));
    1.81 -end;
    1.82 -end;
    1.83  
    1.84  
    1.85      (* Some useful derived rules *)
    1.86 @@ -373,15 +297,6 @@
    1.87  fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
    1.88  fun is_comb t = case (term_of t) of _$_ => true | _ => false;
    1.89  
    1.90 -fun cache_conv conv =
    1.91 - let 
    1.92 -  val tab = ref Termtab.empty
    1.93 -  fun cconv t =  
    1.94 -    case Termtab.lookup (!tab) (term_of t) of
    1.95 -     SOME th => th
    1.96 -   | NONE => let val th = conv t
    1.97 -             in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end
    1.98 - in cconv end;
    1.99  fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
   1.100    handle CTERM _ => false;
   1.101  
   1.102 @@ -571,7 +486,7 @@
   1.103     val nnf_norm_conv' = 
   1.104       nnf_conv then_conv 
   1.105       literals_conv [@{term "op &"}, @{term "op |"}] [] 
   1.106 -     (cache_conv 
   1.107 +     (More_Conv.cache_conv 
   1.108         (first_conv [real_lt_conv, real_le_conv, 
   1.109                      real_eq_conv, real_not_lt_conv, 
   1.110                      real_not_le_conv, real_not_eq_conv, all_conv]))