# HG changeset patch
# User boehmes
# Date 1273701241 -7200
# Node ID 6d1ecdb81ff0945fc459e01b206e76b80c13344d
# Parent  c030819254d30e7371f5be2f09f39c371fe845cf
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite

diff -r c030819254d3 -r 6d1ecdb81ff0 src/HOL/SMT/Tools/smt_translate.ML
--- a/src/HOL/SMT/Tools/smt_translate.ML	Wed May 12 23:54:00 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_translate.ML	Wed May 12 23:54:01 2010 +0200
@@ -144,36 +144,24 @@
 val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
 
 
-val is_let = (fn Const (@{const_name Let}, _) $ _ $ Abs _ => true | _ => false)
-
-val is_true_eq = (fn
-    @{term "op = :: bool => _"} $ _ $ @{term True} => true
-  | _ => false)
-
-val true_eq_rewr = @{lemma "P = True == P" by simp}
-
-val is_trivial_if = (fn
-    Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true
+val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
+    Const (@{const_name Let}, _) => true
+  | @{term "op = :: bool => _"} $ _ $ @{term True} => true
+  | Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true
   | _ => false)
 
-val trivial_if_rewr = @{lemma "(if P then True else False) == P"
-  by (atomize(full)) simp}
+val rewrite_rules = [
+  Let_def,
+  @{lemma "P = True == P" by (rule eq_reflection) simp},
+  @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
 
-fun rewrite _ ct =
-  if is_trivial_if (Thm.term_of ct) then Conv.rewr_conv trivial_if_rewr ct
-  else if is_true_eq (Thm.term_of ct) then Conv.rewr_conv true_eq_rewr ct
-  else if is_let (Thm.term_of ct) then Conv.rewr_conv @{thm Let_def} ct
-  else Conv.all_conv ct
-
-val needs_rewrite =
-  Term.exists_subterm (is_trivial_if orf is_true_eq orf is_let)
+fun rewrite ctxt = Simplifier.full_rewrite
+  (Simplifier.context ctxt empty_ss addsimps rewrite_rules)
 
 fun normalize ctxt thm =
-  if needs_rewrite (Thm.prop_of thm)
-  then Conv.fconv_rule (More_Conv.top_conv rewrite ctxt) thm
-  else thm
+  if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm
 
-val unfold_rules = [term_eq_rewr, Let_def, trivial_if_rewr, true_eq_rewr]
+val unfold_rules = term_eq_rewr :: rewrite_rules
 
 
 val revert_types =
diff -r c030819254d3 -r 6d1ecdb81ff0 src/HOL/SMT/Tools/z3_proof_reconstruction.ML
--- a/src/HOL/SMT/Tools/z3_proof_reconstruction.ML	Wed May 12 23:54:00 2010 +0200
+++ b/src/HOL/SMT/Tools/z3_proof_reconstruction.ML	Wed May 12 23:54:01 2010 +0200
@@ -136,10 +136,10 @@
 
   val prep_rules = [@{thm Let_def}, remove_trigger, L.rewrite_true]
 
-  fun rewrite_conv ctxt eqs =
-    More_Conv.top_conv (K (Conv.try_conv (More_Conv.rewrs_conv eqs))) ctxt
+  fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
+    (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
 
-  fun rewrite_rules eqs = map (Simplifier.rewrite_rule eqs)
+  fun rewrites ctxt eqs = map (Conv.fconv_rule (rewrite_conv ctxt eqs))
 
   fun trace ctxt thm =
     if Config.get ctxt trace_assms
@@ -152,10 +152,10 @@
     | _ => z3_exn ("not asserted: " ^
         quote (Syntax.string_of_term ctxt (Thm.term_of ct))))
 in
-fun prepare_assms unfolds assms =
+fun prepare_assms ctxt unfolds assms =
   let
-    val unfolds' = rewrite_rules [L.rewrite_true] unfolds
-    val assms' = rewrite_rules (union Thm.eq_thm unfolds' prep_rules) assms
+    val unfolds' = rewrites ctxt [L.rewrite_true] unfolds
+    val assms' = rewrites ctxt (union Thm.eq_thm unfolds' prep_rules) assms
   in (unfolds', T.thm_net_of assms') end
 
 fun asserted _ NONE ct = Thm (Thm.assume ct)
@@ -736,7 +736,7 @@
 
 fun prove ctxt unfolds assms vars =
   let
-    val assms' = Option.map (prepare_assms unfolds) assms
+    val assms' = Option.map (prepare_assms ctxt unfolds) assms
     val simpset = T.make_simpset ctxt (Z3_Simps.get ctxt)
 
     fun step r ps ct (cxp as (cx, ptab)) =