# HG changeset patch
# User wenzelm
# Date 1273939146 -7200
# Node ID c52d1c13089806a13a5dc0cfd9160ca2062a845f
# Parent  a3715d7ff337a7c498d65ef1490dcfe3626084cf
incorporated further conversions and conversionals, after some minor tuning;

diff -r a3715d7ff337 -r c52d1c130898 src/HOL/Boogie/Tools/boogie_tactics.ML
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Sat May 15 17:59:06 2010 +0200
@@ -25,8 +25,8 @@
 val label_eqs = [assert_at_def, block_at_def]
 
 fun unfold_labels_tac ctxt =
-  let val unfold = More_Conv.rewrs_conv label_eqs
-  in CONVERSION (More_Conv.top_sweep_conv (K unfold) ctxt) end
+  let val unfold = Conv.rewrs_conv label_eqs
+  in CONVERSION (Conv.top_sweep_conv (K unfold) ctxt) end
 
 fun boogie_tac ctxt rules =
   unfold_labels_tac ctxt
diff -r a3715d7ff337 -r c52d1c130898 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/HOL.thy	Sat May 15 17:59:06 2010 +0200
@@ -29,7 +29,6 @@
   "~~/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 a3715d7ff337 -r c52d1c130898 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/IsaMakefile	Sat May 15 17:59:06 2010 +0200
@@ -128,7 +128,6 @@
   $(SRC)/Tools/induct.ML \
   $(SRC)/Tools/induct_tacs.ML \
   $(SRC)/Tools/intuitionistic.ML \
-  $(SRC)/Tools/more_conv.ML \
   $(SRC)/Tools/nbe.ML \
   $(SRC)/Tools/project_rule.ML \
   $(SRC)/Tools/quickcheck.ML \
diff -r a3715d7ff337 -r c52d1c130898 src/HOL/Library/normarith.ML
--- a/src/HOL/Library/normarith.ML	Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Library/normarith.ML	Sat May 15 17:59:06 2010 +0200
@@ -182,7 +182,6 @@
 fun botc1 conv ct = 
   ((sub_conv (botc1 conv)) then_conv (conv else_conv all_conv)) ct;
 
- fun rewrs_conv eqs ct = first_conv (map rewr_conv eqs) ct;
  val apply_pth1 = rewr_conv @{thm pth_1};
  val apply_pth2 = rewr_conv @{thm pth_2};
  val apply_pth3 = rewr_conv @{thm pth_3};
@@ -333,9 +332,9 @@
   in fst (RealArith.real_linear_prover translator
         (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
             zerodests,
-        map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
+        map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
                        arg_conv (arg_conv real_poly_conv))) ges',
-        map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv 
+        map (fconv_rule (try_conv (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
diff -r a3715d7ff337 -r c52d1c130898 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sat May 15 17:59:06 2010 +0200
@@ -617,7 +617,7 @@
         local open Conv in
           val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
           val sih =
-            fconv_rule (More_Conv.binder_conv
+            fconv_rule (Conv.binder_conv
               (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
         end
 
diff -r a3715d7ff337 -r c52d1c130898 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat May 15 17:59:06 2010 +0200
@@ -490,7 +490,7 @@
       end
   | _ => Conv.all_conv ctrm
 
-fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt
+fun lambda_prs_conv ctxt = Conv.top_conv lambda_prs_simple_conv ctxt
 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
 
 
diff -r a3715d7ff337 -r c52d1c130898 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Sat May 15 17:59:06 2010 +0200
@@ -47,11 +47,11 @@
     "distinct [x, y] == (x ~= y)"
     by simp_all}
   fun distinct_conv _ =
-    if_true_conv is_trivial_distinct (More_Conv.rewrs_conv thms)
+    if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
 in
 fun trivial_distinct ctxt =
   map ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
-    Conv.fconv_rule (More_Conv.top_conv distinct_conv ctxt))
+    Conv.fconv_rule (Conv.top_conv distinct_conv ctxt))
 end
 
 
@@ -67,11 +67,11 @@
     "(case P of True => x | False => y) == (if P then x else y)"
     "(case P of False => y | True => x) == (if P then x else y)"
     by (rule eq_reflection, simp)+}
-  val unfold_conv = if_true_conv is_bool_case (More_Conv.rewrs_conv thms)
+  val unfold_conv = if_true_conv is_bool_case (Conv.rewrs_conv thms)
 in
 fun rewrite_bool_cases ctxt =
   map ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
-    Conv.fconv_rule (More_Conv.top_conv (K unfold_conv) ctxt))
+    Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt))
 end
 
 
@@ -107,7 +107,7 @@
 in
 fun normalize_numerals ctxt =
   map ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ??
-    Conv.fconv_rule (More_Conv.top_sweep_conv pos_conv ctxt))
+    Conv.fconv_rule (Conv.top_sweep_conv pos_conv ctxt))
 end
 
 
@@ -193,7 +193,7 @@
 local
   val eta_conv = eta_expand_conv
 
-  fun keep_conv ctxt = More_Conv.binder_conv norm_conv ctxt
+  fun keep_conv ctxt = Conv.binder_conv (norm_conv o snd) ctxt
   and eta_binder_conv ctxt = Conv.arg_conv (eta_conv norm_conv ctxt)
   and keep_let_conv ctxt = Conv.combination_conv
     (Conv.arg_conv (norm_conv ctxt)) (Conv.abs_conv (norm_conv o snd) ctxt)
@@ -267,7 +267,7 @@
       Conv.binop_conv (atomize_conv ctxt) then_conv
       Conv.rewr_conv @{thm atomize_eq}
   | Const (@{const_name all}, _) $ Abs _ =>
-      More_Conv.binder_conv atomize_conv ctxt then_conv
+      Conv.binder_conv (atomize_conv o snd) ctxt then_conv
       Conv.rewr_conv @{thm atomize_all}
   | _ => Conv.all_conv) ct
 
diff -r a3715d7ff337 -r c52d1c130898 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Sat May 15 17:59:06 2010 +0200
@@ -81,7 +81,7 @@
 
 fun unfold_abs_min_max_defs ctxt thm =
   if exists_abs_min_max (Thm.prop_of thm)
-  then Conv.fconv_rule (More_Conv.top_conv unfold_def_conv ctxt) thm
+  then Conv.fconv_rule (Conv.top_conv unfold_def_conv ctxt) thm
   else thm
 
 
diff -r a3715d7ff337 -r c52d1c130898 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat May 15 17:59:06 2010 +0200
@@ -540,7 +540,7 @@
 
   fun elim_unused_conv ctxt =
     Conv.params_conv ~1 (K (Conv.arg_conv (Conv.arg1_conv
-      (More_Conv.rewrs_conv [elim_all, elim_ex])))) ctxt
+      (Conv.rewrs_conv [elim_all, elim_ex])))) ctxt
 
   fun elim_unused_tac ctxt =
     REPEAT_ALL_NEW (
diff -r a3715d7ff337 -r c52d1c130898 src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Sat May 15 17:59:06 2010 +0200
@@ -96,7 +96,7 @@
 
 fun unfold_eqs _ [] = Conv.all_conv
   | unfold_eqs ctxt eqs =
-      More_Conv.top_sweep_conv (K (More_Conv.rewrs_conv eqs)) ctxt
+      Conv.top_sweep_conv (K (Conv.rewrs_conv eqs)) ctxt
 
 fun match_instantiate f ct thm =
   Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
@@ -256,7 +256,7 @@
   val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
 
   fun set_conv ct =
-    (More_Conv.rewrs_conv [set1, set2, set3, set4] else_conv
+    (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
     (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
 
   val dist1 = @{lemma "distinct [] == ~False" by simp}
@@ -267,7 +267,7 @@
   fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
 in
 fun unfold_distinct_conv ct =
-  (More_Conv.rewrs_conv [dist1, dist2] else_conv
+  (Conv.rewrs_conv [dist1, dist2] else_conv
   (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
 end
 
diff -r a3715d7ff337 -r c52d1c130898 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Sat May 15 15:31:33 2010 +0200
+++ b/src/Pure/conv.ML	Sat May 15 17:59:06 2010 +0200
@@ -1,5 +1,6 @@
 (*  Title:      Pure/conv.ML
     Author:     Amine Chaieb, TU Muenchen
+    Author:     Sascha Boehme, TU Muenchen
     Author:     Makarius
 
 Conversions: primitive equality reasoning.
@@ -32,10 +33,16 @@
   val arg1_conv: conv -> conv
   val fun2_conv: conv -> conv
   val binop_conv: conv -> conv
+  val binder_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
   val forall_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
   val implies_conv: conv -> conv -> conv
   val implies_concl_conv: conv -> conv
   val rewr_conv: thm -> conv
+  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 params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
   val prems_conv: int -> conv -> conv
   val concl_conv: int -> conv -> conv
@@ -105,6 +112,29 @@
 
 fun binop_conv cv = combination_conv (arg_conv cv) cv;
 
+fun binder_conv cv ctxt = arg_conv (abs_conv cv ctxt);
+
+
+(* subterm structure *)
+
+(*cf. SUB_CONV in HOL*)
+fun sub_conv conv ctxt =
+  comb_conv (conv ctxt) else_conv
+  abs_conv (conv o snd) ctxt else_conv
+  all_conv;
+
+(*cf. BOTTOM_CONV in HOL*)
+fun bottom_conv conv ctxt ct =
+  (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct;
+
+(*cf. TOP_CONV in HOL*)
+fun top_conv conv ctxt ct =
+  (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct;
+
+(*cf. TOP_SWEEP_CONV in HOL*)
+fun top_sweep_conv conv ctxt ct =
+  (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct;
+
 
 (* primitive logic *)
 
@@ -136,6 +166,8 @@
       handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
   end;
 
+fun rewrs_conv rules = first_conv (map rewr_conv rules);
+
 
 (* conversions on HHF rules *)
 
diff -r a3715d7ff337 -r c52d1c130898 src/Tools/more_conv.ML
--- a/src/Tools/more_conv.ML	Sat May 15 15:31:33 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*  Title:       Tools/more_conv.ML
-    Author:      Sascha Boehme, TU Muenchen
-
-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
-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)
-
-end