# HG changeset patch
# User boehmes
# Date 1251279628 -7200
# Node ID 5731300da417ce914576d7673a27498c6882a59e
# Parent  5ca6f9a344c010ec7fc5bf7e13e33b8f0473a1fb
added further conversions and conversionals

diff -r 5ca6f9a344c0 -r 5731300da417 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Aug 26 10:48:45 2009 +0200
+++ b/src/HOL/HOL.thy	Wed Aug 26 11:40:28 2009 +0200
@@ -29,6 +29,7 @@
   "~~/src/Tools/induct.ML"
   ("~~/src/Tools/induct_tacs.ML")
   ("Tools/recfun_codegen.ML")
+  "~~/src/Tools/more_conv.ML"
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
diff -r 5ca6f9a344c0 -r 5731300da417 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Aug 26 10:48:45 2009 +0200
+++ b/src/HOL/IsaMakefile	Wed Aug 26 11:40:28 2009 +0200
@@ -108,6 +108,7 @@
   $(SRC)/Tools/random_word.ML \
   $(SRC)/Tools/value.ML \
   $(SRC)/Tools/Code_Generator.thy \
+  $(SRC)/Tools/more_conv.ML \
   HOL.thy \
   Tools/hologic.ML \
   Tools/recfun_codegen.ML \
diff -r 5ca6f9a344c0 -r 5731300da417 src/HOL/Library/normarith.ML
--- a/src/HOL/Library/normarith.ML	Wed Aug 26 10:48:45 2009 +0200
+++ b/src/HOL/Library/normarith.ML	Wed Aug 26 11:40:28 2009 +0200
@@ -15,7 +15,7 @@
 structure NormArith : NORM_ARITH = 
 struct
 
- open Conv Thm Conv2;
+ open Conv Thm;
  val bool_eq = op = : bool *bool -> bool
   fun dest_ratconst t = case term_of t of
    Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
@@ -322,6 +322,7 @@
      val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE 
                                      else SOME(norm_cmul_rule v t))
                             (v ~~ nubs) 
+     fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)
     in inequality_canon_rule ctxt (end_itlist norm_add_rule ths)
     end
    val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @
@@ -332,9 +333,9 @@
   in RealArith.real_linear_prover translator
         (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
             zerodests,
-        map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv
+        map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
                        arg_conv (arg_conv real_poly_conv))) ges',
-        map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv 
+        map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv 
                        arg_conv (arg_conv real_poly_conv))) gts)
   end
 in val real_vector_combo_prover = real_vector_combo_prover
@@ -353,6 +354,7 @@
   val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) []
   val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
   val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
+  fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
   fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
   fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
   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
diff -r 5ca6f9a344c0 -r 5731300da417 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Wed Aug 26 10:48:45 2009 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Wed Aug 26 11:40:28 2009 +0200
@@ -81,82 +81,6 @@
 structure Ctermfunc = FuncFun(type key = cterm val ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t)));
 
 structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
-    (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
-structure Conv2 = 
-struct
- open Conv
-fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
-fun is_comb t = case (term_of t) of _$_ => true | _ => false;
-fun is_abs t = case (term_of t) of Abs _ => true | _ => false;
-
-fun end_itlist f l =
- case l of 
-   []     => error "end_itlist"
- | [x]    => x
- | (h::t) => f h (end_itlist f t);
-
- fun absc cv ct = case term_of ct of 
- Abs (v,_, _) => 
-  let val (x,t) = Thm.dest_abs (SOME v) ct
-  in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t)
-  end
- | _ => all_conv ct;
-
-fun cache_conv conv =
- let 
-  val tab = ref Termtab.empty
-  fun cconv t =  
-    case Termtab.lookup (!tab) (term_of t) of
-     SOME th => th
-   | NONE => let val th = conv t
-             in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end
- in cconv end;
-fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
-  handle CTERM _ => false;
-
-local
- fun thenqc conv1 conv2 tm =
-   case try conv1 tm of
-    SOME th1 => (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2 | NONE => th1)
-  | NONE => conv2 tm
-
- fun thencqc conv1 conv2 tm =
-    let val th1 = conv1 tm 
-    in (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2 | NONE => th1)
-    end
- fun comb_qconv conv tm =
-   let val (l,r) = Thm.dest_comb tm 
-   in (case try conv l of 
-        SOME th1 => (case try conv r of SOME th2 => Thm.combination th1 th2 
-                                      | NONE => Drule.fun_cong_rule th1 r)
-      | NONE => Drule.arg_cong_rule l (conv r))
-   end
- fun repeatqc conv tm = thencqc conv (repeatqc conv) tm 
- fun sub_qconv conv tm =  if is_abs tm then absc conv tm else comb_qconv conv tm 
- fun once_depth_qconv conv tm =
-      (conv else_conv (sub_qconv (once_depth_qconv conv))) tm
- fun depth_qconv conv tm =
-    thenqc (sub_qconv (depth_qconv conv))
-           (repeatqc conv) tm
- fun redepth_qconv conv tm =
-    thenqc (sub_qconv (redepth_qconv conv))
-           (thencqc conv (redepth_qconv conv)) tm
- fun top_depth_qconv conv tm =
-    thenqc (repeatqc conv)
-           (thencqc (sub_qconv (top_depth_qconv conv))
-                    (thencqc conv (top_depth_qconv conv))) tm
- fun top_sweep_qconv conv tm =
-    thenqc (repeatqc conv)
-           (sub_qconv (top_sweep_qconv conv)) tm
-in 
-val (once_depth_conv, depth_conv, rdepth_conv, top_depth_conv, top_sweep_conv) = 
-  (fn c => try_conv (once_depth_qconv c),
-   fn c => try_conv (depth_qconv c),
-   fn c => try_conv (redepth_qconv c),
-   fn c => try_conv (top_depth_qconv c),
-   fn c => try_conv (top_sweep_qconv c));
-end;
-end;
 
 
     (* Some useful derived rules *)
@@ -373,15 +297,6 @@
 fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
 fun is_comb t = case (term_of t) of _$_ => true | _ => false;
 
-fun cache_conv conv =
- let 
-  val tab = ref Termtab.empty
-  fun cconv t =  
-    case Termtab.lookup (!tab) (term_of t) of
-     SOME th => th
-   | NONE => let val th = conv t
-             in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end
- in cconv end;
 fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
   handle CTERM _ => false;
 
@@ -571,7 +486,7 @@
    val nnf_norm_conv' = 
      nnf_conv then_conv 
      literals_conv [@{term "op &"}, @{term "op |"}] [] 
-     (cache_conv 
+     (More_Conv.cache_conv 
        (first_conv [real_lt_conv, real_le_conv, 
                     real_eq_conv, real_not_lt_conv, 
                     real_not_le_conv, real_not_eq_conv, all_conv]))
diff -r 5ca6f9a344c0 -r 5731300da417 src/HOL/Tools/Function/fundef_core.ML
--- a/src/HOL/Tools/Function/fundef_core.ML	Wed Aug 26 10:48:45 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_core.ML	Wed Aug 26 11:40:28 2009 +0200
@@ -577,8 +577,6 @@
 val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct}
 
 
-fun binder_conv cv ctxt = Conv.arg_conv (Conv.abs_conv (K cv) ctxt);
-
 fun mk_partial_induct_rule thy globals R complete_thm clauses =
     let
       val Globals {domT, x, z, a, P, D, ...} = globals
@@ -614,7 +612,7 @@
     val case_hyp_conv = K (case_hyp RS eq_reflection)
     local open Conv in
     val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
-    val sih = fconv_rule (binder_conv (arg1_conv (arg_conv (arg_conv case_hyp_conv))) ctxt) aihyp
+    val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
     end
 
     fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
diff -r 5ca6f9a344c0 -r 5731300da417 src/Tools/more_conv.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/more_conv.ML	Wed Aug 26 11:40:28 2009 +0200
@@ -0,0 +1,61 @@
+(* Title:  Tools/more_conv.ML
+   Author: Sascha Boehme
+
+Further conversions and conversionals.
+*)
+
+signature MORE_CONV =
+sig
+  val rewrs_conv: thm list -> conv
+
+  val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
+  val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
+  val top_conv: (Proof.context -> conv) -> Proof.context -> conv
+  val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
+
+  val binder_conv: (Proof.context -> conv) -> Proof.context -> conv
+
+  val cache_conv: conv -> conv
+end
+
+
+
+structure More_Conv : MORE_CONV =
+struct
+
+
+fun rewrs_conv eqs = Conv.first_conv (map Conv.rewr_conv eqs)
+
+
+fun sub_conv conv ctxt =
+  Conv.comb_conv (conv ctxt) else_conv
+  Conv.abs_conv (fn (_, cx) => conv cx) ctxt else_conv
+  Conv.all_conv
+
+fun bottom_conv conv ctxt ct =
+  (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct
+
+fun top_conv conv ctxt ct =
+  (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct
+
+fun top_sweep_conv conv ctxt ct =
+  (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct
+
+
+fun binder_conv cv ctxt =
+  Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt)
+
+
+fun cache_conv conv =
+  let 
+    val tab = ref Termtab.empty
+    fun add_result t thm =
+      let val _ = change tab (Termtab.insert Thm.eq_thm (t, thm))
+      in thm end
+    fun cconv ct =  
+      (case Termtab.lookup (!tab) (Thm.term_of ct) of
+        SOME thm => thm
+      | NONE => add_result (Thm.term_of ct) (conv ct))
+  in cconv end
+
+end