1.1 --- a/src/HOL/HOL.thy	Wed Aug 26 10:48:45 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Aug 26 11:40:28 2009 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    "~~/src/Tools/induct.ML"
     1.5    ("~~/src/Tools/induct_tacs.ML")
     1.6    ("Tools/recfun_codegen.ML")
     1.7 +  "~~/src/Tools/more_conv.ML"
     1.8  begin
     1.9  
    1.10  setup {* Intuitionistic.method_setup @{binding iprover} *}

     2.1 --- a/src/HOL/IsaMakefile	Wed Aug 26 10:48:45 2009 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Wed Aug 26 11:40:28 2009 +0200
     2.3 @@ -108,6 +108,7 @@
     2.4    $(SRC)/Tools/random_word.ML \
     2.5    $(SRC)/Tools/value.ML \
     2.6    $(SRC)/Tools/Code_Generator.thy \
     2.7 +  $(SRC)/Tools/more_conv.ML \
     2.8    HOL.thy \
     2.9    Tools/hologic.ML \
    2.10    Tools/recfun_codegen.ML \

     3.1 --- a/src/HOL/Library/normarith.ML	Wed Aug 26 10:48:45 2009 +0200
     3.2 +++ b/src/HOL/Library/normarith.ML	Wed Aug 26 11:40:28 2009 +0200
     3.3 @@ -15,7 +15,7 @@
     3.4  structure NormArith : NORM_ARITH = 
     3.5  struct
     3.6  
     3.7 - open Conv Thm Conv2;
     3.8 + open Conv Thm;
     3.9   val bool_eq = op = : bool *bool -> bool
    3.10    fun dest_ratconst t = case term_of t of
    3.11     Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    3.12 @@ -322,6 +322,7 @@
    3.13       val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE 
    3.14                                       else SOME(norm_cmul_rule v t))
    3.15                              (v ~~ nubs) 
    3.16 +     fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)
    3.17      in inequality_canon_rule ctxt (end_itlist norm_add_rule ths)
    3.18      end
    3.19     val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @
    3.20 @@ -332,9 +333,9 @@
    3.21    in RealArith.real_linear_prover translator
    3.22          (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
    3.23              zerodests,
    3.24 -        map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv
    3.25 +        map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
    3.26                         arg_conv (arg_conv real_poly_conv))) ges',
    3.27 -        map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv 
    3.28 +        map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv 
    3.29                         arg_conv (arg_conv real_poly_conv))) gts)
    3.30    end
    3.31  in val real_vector_combo_prover = real_vector_combo_prover
    3.32 @@ -353,6 +354,7 @@
    3.33    val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) []
    3.34    val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
    3.35    val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
    3.36 +  fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
    3.37    fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
    3.38    fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
    3.39    val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns

     4.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Aug 26 10:48:45 2009 +0200
     4.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Aug 26 11:40:28 2009 +0200
     4.3 @@ -81,82 +81,6 @@
     4.4  structure Ctermfunc = FuncFun(type key = cterm val ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t)));
     4.5  
     4.6  structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
     4.7 -    (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
     4.8 -structure Conv2 = 
     4.9 -struct
    4.10 - open Conv
    4.11 -fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
    4.12 -fun is_comb t = case (term_of t) of _$_ => true | _ => false;
    4.13 -fun is_abs t = case (term_of t) of Abs _ => true | _ => false;
    4.14 -
    4.15 -fun end_itlist f l =
    4.16 - case l of 
    4.17 -   []     => error "end_itlist"
    4.18 - | [x]    => x
    4.19 - | (h::t) => f h (end_itlist f t);
    4.20 -
    4.21 - fun absc cv ct = case term_of ct of 
    4.22 - Abs (v,_, _) => 
    4.23 -  let val (x,t) = Thm.dest_abs (SOME v) ct
    4.24 -  in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t)
    4.25 -  end
    4.26 - | _ => all_conv ct;
    4.27 -
    4.28 -fun cache_conv conv =
    4.29 - let 
    4.30 -  val tab = ref Termtab.empty
    4.31 -  fun cconv t =  
    4.32 -    case Termtab.lookup (!tab) (term_of t) of
    4.33 -     SOME th => th
    4.34 -   | NONE => let val th = conv t
    4.35 -             in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end
    4.36 - in cconv end;
    4.37 -fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
    4.38 -  handle CTERM _ => false;
    4.39 -
    4.40 -local
    4.41 - fun thenqc conv1 conv2 tm =
    4.42 -   case try conv1 tm of
    4.43 -    SOME th1 => (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2 | NONE => th1)
    4.44 -  | NONE => conv2 tm
    4.45 -
    4.46 - fun thencqc conv1 conv2 tm =
    4.47 -    let val th1 = conv1 tm 
    4.48 -    in (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2 | NONE => th1)
    4.49 -    end
    4.50 - fun comb_qconv conv tm =
    4.51 -   let val (l,r) = Thm.dest_comb tm 
    4.52 -   in (case try conv l of 
    4.53 -        SOME th1 => (case try conv r of SOME th2 => Thm.combination th1 th2 
    4.54 -                                      | NONE => Drule.fun_cong_rule th1 r)
    4.55 -      | NONE => Drule.arg_cong_rule l (conv r))
    4.56 -   end
    4.57 - fun repeatqc conv tm = thencqc conv (repeatqc conv) tm 
    4.58 - fun sub_qconv conv tm =  if is_abs tm then absc conv tm else comb_qconv conv tm 
    4.59 - fun once_depth_qconv conv tm =
    4.60 -      (conv else_conv (sub_qconv (once_depth_qconv conv))) tm
    4.61 - fun depth_qconv conv tm =
    4.62 -    thenqc (sub_qconv (depth_qconv conv))
    4.63 -           (repeatqc conv) tm
    4.64 - fun redepth_qconv conv tm =
    4.65 -    thenqc (sub_qconv (redepth_qconv conv))
    4.66 -           (thencqc conv (redepth_qconv conv)) tm
    4.67 - fun top_depth_qconv conv tm =
    4.68 -    thenqc (repeatqc conv)
    4.69 -           (thencqc (sub_qconv (top_depth_qconv conv))
    4.70 -                    (thencqc conv (top_depth_qconv conv))) tm
    4.71 - fun top_sweep_qconv conv tm =
    4.72 -    thenqc (repeatqc conv)
    4.73 -           (sub_qconv (top_sweep_qconv conv)) tm
    4.74 -in 
    4.75 -val (once_depth_conv, depth_conv, rdepth_conv, top_depth_conv, top_sweep_conv) = 
    4.76 -  (fn c => try_conv (once_depth_qconv c),
    4.77 -   fn c => try_conv (depth_qconv c),
    4.78 -   fn c => try_conv (redepth_qconv c),
    4.79 -   fn c => try_conv (top_depth_qconv c),
    4.80 -   fn c => try_conv (top_sweep_qconv c));
    4.81 -end;
    4.82 -end;
    4.83  
    4.84  
    4.85      (* Some useful derived rules *)
    4.86 @@ -373,15 +297,6 @@
    4.87  fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
    4.88  fun is_comb t = case (term_of t) of _$_ => true | _ => false;
    4.89  
    4.90 -fun cache_conv conv =
    4.91 - let 
    4.92 -  val tab = ref Termtab.empty
    4.93 -  fun cconv t =  
    4.94 -    case Termtab.lookup (!tab) (term_of t) of
    4.95 -     SOME th => th
    4.96 -   | NONE => let val th = conv t
    4.97 -             in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end
    4.98 - in cconv end;
    4.99  fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
   4.100    handle CTERM _ => false;
   4.101  
   4.102 @@ -571,7 +486,7 @@
   4.103     val nnf_norm_conv' = 
   4.104       nnf_conv then_conv 
   4.105       literals_conv [@{term "op &"}, @{term "op |"}] [] 
   4.106 -     (cache_conv 
   4.107 +     (More_Conv.cache_conv 
   4.108         (first_conv [real_lt_conv, real_le_conv, 
   4.109                      real_eq_conv, real_not_lt_conv, 
   4.110                      real_not_le_conv, real_not_eq_conv, all_conv]))

     5.1 --- a/src/HOL/Tools/Function/fundef_core.ML	Wed Aug 26 10:48:45 2009 +0200
     5.2 +++ b/src/HOL/Tools/Function/fundef_core.ML	Wed Aug 26 11:40:28 2009 +0200
     5.3 @@ -577,8 +577,6 @@
     5.4  val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct}
     5.5  
     5.6  
     5.7 -fun binder_conv cv ctxt = Conv.arg_conv (Conv.abs_conv (K cv) ctxt);
     5.8 -
     5.9  fun mk_partial_induct_rule thy globals R complete_thm clauses =
    5.10      let
    5.11        val Globals {domT, x, z, a, P, D, ...} = globals
    5.12 @@ -614,7 +612,7 @@
    5.13      val case_hyp_conv = K (case_hyp RS eq_reflection)
    5.14      local open Conv in
    5.15      val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
    5.16 -    val sih = fconv_rule (binder_conv (arg1_conv (arg_conv (arg_conv case_hyp_conv))) ctxt) aihyp
    5.17 +    val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
    5.18      end
    5.19  
    5.20      fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/more_conv.ML	Wed Aug 26 11:40:28 2009 +0200
     6.3 @@ -0,0 +1,61 @@
     6.4 +(* Title:  Tools/more_conv.ML
     6.5 +   Author: Sascha Boehme
     6.6 +
     6.7 +Further conversions and conversionals.
     6.8 +*)
     6.9 +
    6.10 +signature MORE_CONV =
    6.11 +sig
    6.12 +  val rewrs_conv: thm list -> conv
    6.13 +
    6.14 +  val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
    6.15 +  val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
    6.16 +  val top_conv: (Proof.context -> conv) -> Proof.context -> conv
    6.17 +  val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
    6.18 +
    6.19 +  val binder_conv: (Proof.context -> conv) -> Proof.context -> conv
    6.20 +
    6.21 +  val cache_conv: conv -> conv
    6.22 +end
    6.23 +
    6.24 +
    6.25 +
    6.26 +structure More_Conv : MORE_CONV =
    6.27 +struct
    6.28 +
    6.29 +
    6.30 +fun rewrs_conv eqs = Conv.first_conv (map Conv.rewr_conv eqs)
    6.31 +
    6.32 +
    6.33 +fun sub_conv conv ctxt =
    6.34 +  Conv.comb_conv (conv ctxt) else_conv
    6.35 +  Conv.abs_conv (fn (_, cx) => conv cx) ctxt else_conv
    6.36 +  Conv.all_conv
    6.37 +
    6.38 +fun bottom_conv conv ctxt ct =
    6.39 +  (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct
    6.40 +
    6.41 +fun top_conv conv ctxt ct =
    6.42 +  (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct
    6.43 +
    6.44 +fun top_sweep_conv conv ctxt ct =
    6.45 +  (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct
    6.46 +
    6.47 +
    6.48 +fun binder_conv cv ctxt =
    6.49 +  Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt)
    6.50 +
    6.51 +
    6.52 +fun cache_conv conv =
    6.53 +  let 
    6.54 +    val tab = ref Termtab.empty
    6.55 +    fun add_result t thm =
    6.56 +      let val _ = change tab (Termtab.insert Thm.eq_thm (t, thm))
    6.57 +      in thm end
    6.58 +    fun cconv ct =  
    6.59 +      (case Termtab.lookup (!tab) (Thm.term_of ct) of
    6.60 +        SOME thm => thm
    6.61 +      | NONE => add_result (Thm.term_of ct) (conv ct))
    6.62 +  in cconv end
    6.63 +
    6.64 +end