share and use more utility functions;
slightly reduced complexity for Z3 proof rule 'rewrite'

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Nov 22 15:45:42 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Nov 22 15:45:43 2010 +0100
@@ -28,12 +28,11 @@
 structure SMT_Normalize: SMT_NORMALIZE =
 struct
 
+structure U = SMT_Utils
+
 infix 2 ??
 fun (test ?? f) x = if test x then f x else x
 
-fun if_conv c cv1 cv2 ct = (if c (Thm.term_of ct) then cv1 else cv2) ct
-fun if_true_conv c cv = if_conv c cv Conv.all_conv
-
 
 
 (* simplification of trivial distincts (distinct should have at least
@@ -53,7 +52,7 @@
     "SMT.distinct [x, y] = (x ~= y)"
     by (simp_all add: distinct_def)}
   fun distinct_conv _ =
-    if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
+    U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
 in
 fun trivial_distinct ctxt =
   map (apsnd ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
@@ -71,7 +70,7 @@
 
   val thm = mk_meta_eq @{lemma
     "(case P of True => x | False => y) = (if P then x else y)" by simp}
-  val unfold_conv = if_true_conv is_bool_case (Conv.rewr_conv thm)
+  val unfold_conv = U.if_true_conv is_bool_case (Conv.rewr_conv thm)
 in
 fun rewrite_bool_cases ctxt =
   map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
@@ -105,7 +104,7 @@
       "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
       by simp_all (simp add: pred_def)}
 
-  fun pos_conv ctxt = if_conv (is_strange_number ctxt)
+  fun pos_conv ctxt = U.if_conv (is_strange_number ctxt)
     (Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss))
     Conv.no_conv
 in
@@ -282,7 +281,7 @@
         | (_, ts) => forall (is_normed ctxt) ts))
 in
 fun norm_binder_conv ctxt =
-  if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
+  U.if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
 end
 
 fun norm_def ctxt thm =
@@ -321,13 +320,6 @@
 (* lift lambda terms into additional rules *)
 
 local
-  val meta_eq = @{cpat "op =="}
-  val meta_eqT = hd (Thm.dest_ctyp (Thm.ctyp_of_term meta_eq))
-  fun inst_meta cT = Thm.instantiate_cterm ([(meta_eqT, cT)], []) meta_eq
-  fun mk_meta_eq ct cu = Thm.mk_binop (inst_meta (Thm.ctyp_of_term ct)) ct cu
-
-  fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
-
   fun used_vars cvs ct =
     let
       val lookup = AList.lookup (op aconv) (map (` Thm.term_of) cvs)
@@ -350,7 +342,7 @@
           let
             val {T, ...} = Thm.rep_cterm ct' and n = Name.uu
             val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
-            val cu = mk_meta_eq (cert ctxt (Free (n', T))) ct'
+            val cu = U.mk_cequals (U.certify ctxt (Free (n', T))) ct'
             val (eq, ctxt'') = yield_singleton Assumption.add_assumes cu ctxt'
             val defs' = Termtab.update (Thm.term_of ct', eq) defs
           in (apply_def cvs' eq, (ctxt'', defs')) end)

--- a/src/HOL/Tools/SMT/smt_translate.ML	Mon Nov 22 15:45:42 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Mon Nov 22 15:45:43 2010 +0100
@@ -52,6 +52,9 @@
 structure SMT_Translate: SMT_TRANSLATE =
 struct
 
+structure U = SMT_Utils
+
+
 (* intermediate term structure *)
 
 datatype squant = SForall | SExists
@@ -107,13 +110,6 @@
 
 (* utility functions *)
 
-val dest_funT =
-  let
-    fun dest Ts 0 T = (rev Ts, T)
-      | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
-      | dest _ _ T = raise TYPE ("dest_funT", [T], [])
-  in dest [] end
-
 val quantifier = (fn
     @{const_name All} => SOME SForall
   | @{const_name Ex} => SOME SExists
@@ -348,7 +344,7 @@
     and new_dtyps dts cx =
       let
         fun new_decl i t =
-          let val (Ts, T) = dest_funT i (Term.fastype_of t)
+          let val (Ts, T) = U.dest_funT i (Term.fastype_of t)
           in
             fold_map transT Ts ##>> transT T ##>>
             new_fun func_prefix t NONE #>> swap
@@ -396,7 +392,7 @@
       | _ => raise TERM ("smt_translate", [t]))
 
     and transs t T ts =
-      let val (Us, U) = dest_funT (length ts) T
+      let val (Us, U) = U.dest_funT (length ts) T
       in
         fold_map transT Us ##>> transT U #-> (fn Up =>
         fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)

--- a/src/HOL/Tools/SMT/smt_utils.ML	Mon Nov 22 15:45:42 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_utils.ML	Mon Nov 22 15:45:43 2010 +0100
@@ -9,6 +9,10 @@
   val repeat: ('a -> 'a option) -> 'a -> 'a
   val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
 
+  (* types *)
+  val split_type: typ -> typ * typ
+  val dest_funT: int -> typ -> typ list * typ
+
   (* terms *)
   val dest_conj: term -> term * term
   val dest_disj: term -> term * term
@@ -23,6 +27,7 @@
 
   (* certified terms *)
   val certify: Proof.context -> term -> cterm
+  val typ_of: cterm -> typ
   val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
   val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
   val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
@@ -50,6 +55,18 @@
   in rep end
 
 
+(* types *)
+
+fun split_type T = (Term.domain_type T, Term.range_type T)
+
+val dest_funT =
+  let
+    fun dest Ts 0 T = (rev Ts, T)
+      | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
+      | dest _ _ T = raise TYPE ("not a function type", [T], [])
+  in dest [] end
+
+
 (* terms *)
 
 fun dest_conj (@{const HOL.conj} $ t $ u) = (t, u)
@@ -77,6 +94,8 @@
 
 fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
 
+fun typ_of ct = #T (Thm.rep_cterm ct) 
+
 fun dest_cabs ct ctxt =
   (case Thm.term_of ct of
     Abs _ =>
@@ -93,7 +112,7 @@
 
 val dest_all_cbinders = repeat_yield (try o dest_cbinder)
 
-val mk_cprop = Thm.capply @{cterm Trueprop}
+val mk_cprop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
 
 fun dest_cprop ct =
   (case Thm.term_of ct of
@@ -106,9 +125,9 @@
 
 (* conversions *)
 
-fun if_conv f cv1 cv2 ct = if f (Thm.term_of ct) then cv1 ct else cv2 ct
+fun if_conv pred cv1 cv2 ct = if pred (Thm.term_of ct) then cv1 ct else cv2 ct
 
-fun if_true_conv f cv = if_conv f cv Conv.all_conv
+fun if_true_conv pred cv = if_conv pred cv Conv.all_conv
 
 fun binders_conv cv ctxt =
   Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt

--- a/src/HOL/Tools/SMT/z3_model.ML	Mon Nov 22 15:45:42 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_model.ML	Mon Nov 22 15:45:43 2010 +0100
@@ -13,6 +13,9 @@
 structure Z3_Model: Z3_MODEL =
 struct
 
+structure U = SMT_Utils
+
+
 (* counterexample expressions *)
 
 datatype expr = True | False | Number of int * int option | Value of int |
@@ -214,15 +217,13 @@
 
 fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U)
 
-fun split_type T = (Term.domain_type T, Term.range_type T)
-
 fun mk_update ([], u) _ = u
   | mk_update ([t], u) f =
-      uncurry mk_fun_upd (split_type (Term.fastype_of f)) $ f $ t $ u
+      uncurry mk_fun_upd (U.split_type (Term.fastype_of f)) $ f $ t $ u
   | mk_update (t :: ts, u) f =
       let
-        val (dT, rT) = split_type (Term.fastype_of f)
-        val (dT', rT') = split_type rT
+        val (dT, rT) = U.split_type (Term.fastype_of f)
+        val (dT', rT') = U.split_type rT
       in
         mk_fun_upd dT rT $ f $ t $
           mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))

--- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Mon Nov 22 15:45:42 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Mon Nov 22 15:45:43 2010 +0100
@@ -13,6 +13,7 @@
 struct
 
 structure U = SMT_Utils
+structure T = Z3_Proof_Tools
 
 
 fun apply tac st =
@@ -35,26 +36,24 @@
 
 fun mk_inv_of ctxt ct =
   let
-    val T = #T (Thm.rep_cterm ct)
-    val dT = Term.domain_type T
-    val inv = U.certify ctxt (mk_inv_into dT (Term.range_type T))
+    val (dT, rT) = U.split_type (U.typ_of ct)
+    val inv = U.certify ctxt (mk_inv_into dT rT)
     val univ = U.certify ctxt (mk_univ dT)
   in Thm.mk_binop inv univ ct end
 
 fun mk_inj_prop ctxt ct =
   let
-    val T = #T (Thm.rep_cterm ct)
-    val dT = Term.domain_type T
-    val inj = U.certify ctxt (mk_inj_on dT (Term.range_type T))
+    val (dT, rT) = U.split_type (U.typ_of ct)
+    val inj = U.certify ctxt (mk_inj_on dT rT)
     val univ = U.certify ctxt (mk_univ dT)
   in U.mk_cprop (Thm.mk_binop inj ct univ) end
 
 
 val disjE = @{lemma "~P | Q ==> P ==> Q" by fast}
 
-fun prove_inj_prop ctxt hdef lhs =
+fun prove_inj_prop ctxt def lhs =
   let
-    val (ct, ctxt') = U.dest_all_cabs (Thm.rhs_of hdef) ctxt
+    val (ct, ctxt') = U.dest_all_cabs (Thm.rhs_of def) ctxt
     val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
   in
     Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
@@ -64,12 +63,12 @@
     |> singleton (Variable.export ctxt' ctxt)
   end
 
-fun prove_rhs ctxt hdef lhs rhs =
-  Goal.init rhs
-  |> apply (CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv hdef)) ctxt))
-  |> apply (REPEAT_ALL_NEW (Tactic.match_tac @{thms allI}))
-  |> apply (Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt hdef lhs]))
-  |> Goal.norm_result o Goal.finish ctxt
+fun prove_rhs ctxt def lhs =
+  T.by_tac (
+    CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
+    THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI})
+    THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) #>
+  Thm.elim_implies def
 
 
 fun expand thm ct =
@@ -80,18 +79,17 @@
     val thm2 = Thm.instantiate (Thm.match (cpat, cr)) thm
   in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end
 
-fun prove_lhs ctxt rhs lhs =
+fun prove_lhs ctxt rhs =
   let
     val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs)))
   in
-    Goal.init lhs
-    |> apply (CONVERSION (U.prop_conv (U.binders_conv (K (expand eq)) ctxt)))
-    |> apply (Simplifier.simp_tac HOL_ss)
-    |> Goal.finish ctxt
+    T.by_tac (
+      CONVERSION (U.prop_conv (U.binders_conv (K (expand eq)) ctxt))
+      THEN' Simplifier.simp_tac HOL_ss)
   end
 
 
-fun mk_hdef ctxt rhs =
+fun mk_inv_def ctxt rhs =
   let
     val (ct, ctxt') = U.dest_all_cbinders (U.dest_cprop rhs) ctxt
     val (cl, cv) = Thm.dest_binop ct
@@ -102,9 +100,8 @@
 fun prove_inj_eq ctxt ct =
   let
     val (lhs, rhs) = pairself U.mk_cprop (Thm.dest_binop (U.dest_cprop ct))
-    val hdef = mk_hdef ctxt rhs
-    val lhs_thm = Thm.implies_intr rhs (prove_lhs ctxt rhs lhs)
-    val rhs_thm = Thm.implies_intr lhs (prove_rhs ctxt hdef lhs rhs)
+    val lhs_thm = prove_lhs ctxt rhs lhs
+    val rhs_thm = prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs
   in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end
 
 
@@ -125,12 +122,10 @@
 
 in
 
-fun prove_injectivity ctxt ct =
-  ct
-  |> Goal.init
-  |> apply (CONVERSION (U.prop_conv (norm_conv ctxt)))
-  |> apply (CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt)))
-  |> Goal.norm_result o Goal.finish ctxt
+fun prove_injectivity ctxt =
+  T.by_tac (
+    CONVERSION (U.prop_conv (norm_conv ctxt))
+    THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt)))
 
 end
 

--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Nov 22 15:45:42 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Nov 22 15:45:43 2010 +0100
@@ -103,24 +103,20 @@
    context-independent modulo the current proof context to be able to
    use fast inference kernel rules during proof reconstruction. *)
 
-fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
-
 val maxidx_of = #maxidx o Thm.rep_cterm
 
 fun mk_inst ctxt vars =
   let
     val max = fold (Integer.max o fst) vars 0
     val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
-    fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
+    fun mk (i, v) = (v, U.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
   in map mk vars end
 
-val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
-
 fun close ctxt (ct, vars) =
   let
     val inst = mk_inst ctxt vars
     val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
-  in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end
+  in (U.mk_cprop (Thm.instantiate_cterm ([], inst) ct), names) end
 
 
 fun mk_bound thy (i, T) =
@@ -195,7 +191,7 @@
       |> Symtab.fold (Variable.declare_term o snd) terms
 
     fun cert @{const True} = not_false
-      | cert t = certify ctxt' t
+      | cert t = U.certify ctxt' t
 
   in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end
 
@@ -210,7 +206,7 @@
     SOME _ => cx
   | NONE => cx |> fresh_name (decl_prefix ^ n)
       |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
-           let val upd = Symtab.update (n, certify ctxt (Free (m, T)))
+           let val upd = Symtab.update (n, U.certify ctxt (Free (m, T)))
            in (typs, upd terms, exprs, steps, vars, ctxt) end))
 
 fun mk_typ (typs, _, _, _, _, ctxt) (s as I.Sym (n, _)) = 

--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 22 15:45:42 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 22 15:45:43 2010 +0100
@@ -683,33 +683,29 @@
   val unfold_conv =
     Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv))
   val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq
+
+  fun assume_prems ctxt thm =
+    Assumption.add_assumes (Drule.cprems_of thm) ctxt
+    |>> (fn thms => fold Thm.elim_implies thms thm)
 in
 
-fun rewrite' ctxt simpset ths = Thm o with_conv ctxt ths (try_apply ctxt [] [
-  named ctxt "conj/disj/distinct" prove_conj_disj_eq,
-  T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
-    NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
-    THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
-  T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
-    NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
-    THEN_ALL_NEW (
-      NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
-      ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
-  T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
-    NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
-    THEN_ALL_NEW (
-      NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
-      ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
-  named ctxt "injectivity" (M.prove_injectivity ctxt)])
-
-fun rewrite simpset thms ct ctxt = (* FIXME: join with rewrite' *)
-  let
-    val thm = rewrite' ctxt simpset thms ct
-    val ord = Term_Ord.fast_term_ord o pairself Thm.term_of
-    val chyps = fold (Ord_List.union ord o #hyps o Thm.crep_thm o thm_of) thms []
-    val new_chyps = Ord_List.subtract ord chyps (#hyps (Thm.crep_thm (thm_of thm)))
-    val (_, ctxt') = Assumption.add_assumes new_chyps ctxt
-  in (thm, ctxt') end
+fun rewrite simpset ths ct ctxt =
+  apfst Thm (assume_prems ctxt (with_conv ctxt ths (try_apply ctxt [] [
+    named ctxt "conj/disj/distinct" prove_conj_disj_eq,
+    T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
+      NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
+      THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
+    T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
+      NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
+      THEN_ALL_NEW (
+        NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
+        ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
+    T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
+      NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
+      THEN_ALL_NEW (
+        NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
+        ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
+    named ctxt "injectivity" (M.prove_injectivity ctxt)]) ct))
 
 end
 

--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Nov 22 15:45:42 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Nov 22 15:45:43 2010 +0100
@@ -9,7 +9,6 @@
   (* accessing and modifying terms *)
   val term_of: cterm -> term
   val prop_of: thm -> term
-  val mk_prop: cterm -> cterm
   val as_meta_eq: cterm -> cterm
 
   (* theorem nets *)
@@ -59,9 +58,7 @@
 fun term_of ct = dest_prop (Thm.term_of ct)
 fun prop_of thm = dest_prop (Thm.prop_of thm)
 
-val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
-
-fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (Thm.dest_arg ct))
+fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct))
 
 
 
@@ -85,7 +82,7 @@
 (* proof combinators *)
 
 fun under_assumption f ct =
-  let val ct' = mk_prop ct
+  let val ct' = U.mk_cprop ct
   in Thm.implies_intr ct' (f (Thm.assume ct')) end
 
 fun with_conv conv prove ct =
@@ -125,9 +122,6 @@
 
 local
 
-fun typ_of ct = #T (Thm.rep_cterm ct)
-fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
-
 fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
 
 fun context_of (ctxt, _, _, _) = ctxt
@@ -153,7 +147,8 @@
     | NONE =>
         let
           val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
-          val cv = certify ctxt' (Free (n, map typ_of cvs' ---> typ_of ct))
+          val cv = U.certify ctxt'
+            (Free (n, map U.typ_of cvs' ---> U.typ_of ct))
           val cu = Drule.list_comb (cv, cvs')
           val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
           val beta_norm' = beta_norm orelse not (null cvs')