1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Nov 22 15:45:42 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Nov 22 15:45:43 2010 +0100
     1.3 @@ -28,12 +28,11 @@
     1.4  structure SMT_Normalize: SMT_NORMALIZE =
     1.5  struct
     1.6  
     1.7 +structure U = SMT_Utils
     1.8 +
     1.9  infix 2 ??
    1.10  fun (test ?? f) x = if test x then f x else x
    1.11  
    1.12 -fun if_conv c cv1 cv2 ct = (if c (Thm.term_of ct) then cv1 else cv2) ct
    1.13 -fun if_true_conv c cv = if_conv c cv Conv.all_conv
    1.14 -
    1.15  
    1.16  
    1.17  (* simplification of trivial distincts (distinct should have at least
    1.18 @@ -53,7 +52,7 @@
    1.19      "SMT.distinct [x, y] = (x ~= y)"
    1.20      by (simp_all add: distinct_def)}
    1.21    fun distinct_conv _ =
    1.22 -    if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
    1.23 +    U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
    1.24  in
    1.25  fun trivial_distinct ctxt =
    1.26    map (apsnd ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
    1.27 @@ -71,7 +70,7 @@
    1.28  
    1.29    val thm = mk_meta_eq @{lemma
    1.30      "(case P of True => x | False => y) = (if P then x else y)" by simp}
    1.31 -  val unfold_conv = if_true_conv is_bool_case (Conv.rewr_conv thm)
    1.32 +  val unfold_conv = U.if_true_conv is_bool_case (Conv.rewr_conv thm)
    1.33  in
    1.34  fun rewrite_bool_cases ctxt =
    1.35    map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
    1.36 @@ -105,7 +104,7 @@
    1.37        "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
    1.38        by simp_all (simp add: pred_def)}
    1.39  
    1.40 -  fun pos_conv ctxt = if_conv (is_strange_number ctxt)
    1.41 +  fun pos_conv ctxt = U.if_conv (is_strange_number ctxt)
    1.42      (Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss))
    1.43      Conv.no_conv
    1.44  in
    1.45 @@ -282,7 +281,7 @@
    1.46          | (_, ts) => forall (is_normed ctxt) ts))
    1.47  in
    1.48  fun norm_binder_conv ctxt =
    1.49 -  if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
    1.50 +  U.if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
    1.51  end
    1.52  
    1.53  fun norm_def ctxt thm =
    1.54 @@ -321,13 +320,6 @@
    1.55  (* lift lambda terms into additional rules *)
    1.56  
    1.57  local
    1.58 -  val meta_eq = @{cpat "op =="}
    1.59 -  val meta_eqT = hd (Thm.dest_ctyp (Thm.ctyp_of_term meta_eq))
    1.60 -  fun inst_meta cT = Thm.instantiate_cterm ([(meta_eqT, cT)], []) meta_eq
    1.61 -  fun mk_meta_eq ct cu = Thm.mk_binop (inst_meta (Thm.ctyp_of_term ct)) ct cu
    1.62 -
    1.63 -  fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
    1.64 -
    1.65    fun used_vars cvs ct =
    1.66      let
    1.67        val lookup = AList.lookup (op aconv) (map (` Thm.term_of) cvs)
    1.68 @@ -350,7 +342,7 @@
    1.69            let
    1.70              val {T, ...} = Thm.rep_cterm ct' and n = Name.uu
    1.71              val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
    1.72 -            val cu = mk_meta_eq (cert ctxt (Free (n', T))) ct'
    1.73 +            val cu = U.mk_cequals (U.certify ctxt (Free (n', T))) ct'
    1.74              val (eq, ctxt'') = yield_singleton Assumption.add_assumes cu ctxt'
    1.75              val defs' = Termtab.update (Thm.term_of ct', eq) defs
    1.76            in (apply_def cvs' eq, (ctxt'', defs')) end)

     2.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Mon Nov 22 15:45:42 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Mon Nov 22 15:45:43 2010 +0100
     2.3 @@ -52,6 +52,9 @@
     2.4  structure SMT_Translate: SMT_TRANSLATE =
     2.5  struct
     2.6  
     2.7 +structure U = SMT_Utils
     2.8 +
     2.9 +
    2.10  (* intermediate term structure *)
    2.11  
    2.12  datatype squant = SForall | SExists
    2.13 @@ -107,13 +110,6 @@
    2.14  
    2.15  (* utility functions *)
    2.16  
    2.17 -val dest_funT =
    2.18 -  let
    2.19 -    fun dest Ts 0 T = (rev Ts, T)
    2.20 -      | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
    2.21 -      | dest _ _ T = raise TYPE ("dest_funT", [T], [])
    2.22 -  in dest [] end
    2.23 -
    2.24  val quantifier = (fn
    2.25      @{const_name All} => SOME SForall
    2.26    | @{const_name Ex} => SOME SExists
    2.27 @@ -348,7 +344,7 @@
    2.28      and new_dtyps dts cx =
    2.29        let
    2.30          fun new_decl i t =
    2.31 -          let val (Ts, T) = dest_funT i (Term.fastype_of t)
    2.32 +          let val (Ts, T) = U.dest_funT i (Term.fastype_of t)
    2.33            in
    2.34              fold_map transT Ts ##>> transT T ##>>
    2.35              new_fun func_prefix t NONE #>> swap
    2.36 @@ -396,7 +392,7 @@
    2.37        | _ => raise TERM ("smt_translate", [t]))
    2.38  
    2.39      and transs t T ts =
    2.40 -      let val (Us, U) = dest_funT (length ts) T
    2.41 +      let val (Us, U) = U.dest_funT (length ts) T
    2.42        in
    2.43          fold_map transT Us ##>> transT U #-> (fn Up =>
    2.44          fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)

     3.1 --- a/src/HOL/Tools/SMT/smt_utils.ML	Mon Nov 22 15:45:42 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/smt_utils.ML	Mon Nov 22 15:45:43 2010 +0100
     3.3 @@ -9,6 +9,10 @@
     3.4    val repeat: ('a -> 'a option) -> 'a -> 'a
     3.5    val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
     3.6  
     3.7 +  (* types *)
     3.8 +  val split_type: typ -> typ * typ
     3.9 +  val dest_funT: int -> typ -> typ list * typ
    3.10 +
    3.11    (* terms *)
    3.12    val dest_conj: term -> term * term
    3.13    val dest_disj: term -> term * term
    3.14 @@ -23,6 +27,7 @@
    3.15  
    3.16    (* certified terms *)
    3.17    val certify: Proof.context -> term -> cterm
    3.18 +  val typ_of: cterm -> typ
    3.19    val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
    3.20    val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
    3.21    val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
    3.22 @@ -50,6 +55,18 @@
    3.23    in rep end
    3.24  
    3.25  
    3.26 +(* types *)
    3.27 +
    3.28 +fun split_type T = (Term.domain_type T, Term.range_type T)
    3.29 +
    3.30 +val dest_funT =
    3.31 +  let
    3.32 +    fun dest Ts 0 T = (rev Ts, T)
    3.33 +      | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
    3.34 +      | dest _ _ T = raise TYPE ("not a function type", [T], [])
    3.35 +  in dest [] end
    3.36 +
    3.37 +
    3.38  (* terms *)
    3.39  
    3.40  fun dest_conj (@{const HOL.conj} $ t $ u) = (t, u)
    3.41 @@ -77,6 +94,8 @@
    3.42  
    3.43  fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
    3.44  
    3.45 +fun typ_of ct = #T (Thm.rep_cterm ct) 
    3.46 +
    3.47  fun dest_cabs ct ctxt =
    3.48    (case Thm.term_of ct of
    3.49      Abs _ =>
    3.50 @@ -93,7 +112,7 @@
    3.51  
    3.52  val dest_all_cbinders = repeat_yield (try o dest_cbinder)
    3.53  
    3.54 -val mk_cprop = Thm.capply @{cterm Trueprop}
    3.55 +val mk_cprop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
    3.56  
    3.57  fun dest_cprop ct =
    3.58    (case Thm.term_of ct of
    3.59 @@ -106,9 +125,9 @@
    3.60  
    3.61  (* conversions *)
    3.62  
    3.63 -fun if_conv f cv1 cv2 ct = if f (Thm.term_of ct) then cv1 ct else cv2 ct
    3.64 +fun if_conv pred cv1 cv2 ct = if pred (Thm.term_of ct) then cv1 ct else cv2 ct
    3.65  
    3.66 -fun if_true_conv f cv = if_conv f cv Conv.all_conv
    3.67 +fun if_true_conv pred cv = if_conv pred cv Conv.all_conv
    3.68  
    3.69  fun binders_conv cv ctxt =
    3.70    Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt

     4.1 --- a/src/HOL/Tools/SMT/z3_model.ML	Mon Nov 22 15:45:42 2010 +0100
     4.2 +++ b/src/HOL/Tools/SMT/z3_model.ML	Mon Nov 22 15:45:43 2010 +0100
     4.3 @@ -13,6 +13,9 @@
     4.4  structure Z3_Model: Z3_MODEL =
     4.5  struct
     4.6  
     4.7 +structure U = SMT_Utils
     4.8 +
     4.9 +
    4.10  (* counterexample expressions *)
    4.11  
    4.12  datatype expr = True | False | Number of int * int option | Value of int |
    4.13 @@ -214,15 +217,13 @@
    4.14  
    4.15  fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U)
    4.16  
    4.17 -fun split_type T = (Term.domain_type T, Term.range_type T)
    4.18 -
    4.19  fun mk_update ([], u) _ = u
    4.20    | mk_update ([t], u) f =
    4.21 -      uncurry mk_fun_upd (split_type (Term.fastype_of f)) $ f $ t $ u
    4.22 +      uncurry mk_fun_upd (U.split_type (Term.fastype_of f)) $ f $ t $ u
    4.23    | mk_update (t :: ts, u) f =
    4.24        let
    4.25 -        val (dT, rT) = split_type (Term.fastype_of f)
    4.26 -        val (dT', rT') = split_type rT
    4.27 +        val (dT, rT) = U.split_type (Term.fastype_of f)
    4.28 +        val (dT', rT') = U.split_type rT
    4.29        in
    4.30          mk_fun_upd dT rT $ f $ t $
    4.31            mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))

     5.1 --- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Mon Nov 22 15:45:42 2010 +0100
     5.2 +++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Mon Nov 22 15:45:43 2010 +0100
     5.3 @@ -13,6 +13,7 @@
     5.4  struct
     5.5  
     5.6  structure U = SMT_Utils
     5.7 +structure T = Z3_Proof_Tools
     5.8  
     5.9  
    5.10  fun apply tac st =
    5.11 @@ -35,26 +36,24 @@
    5.12  
    5.13  fun mk_inv_of ctxt ct =
    5.14    let
    5.15 -    val T = #T (Thm.rep_cterm ct)
    5.16 -    val dT = Term.domain_type T
    5.17 -    val inv = U.certify ctxt (mk_inv_into dT (Term.range_type T))
    5.18 +    val (dT, rT) = U.split_type (U.typ_of ct)
    5.19 +    val inv = U.certify ctxt (mk_inv_into dT rT)
    5.20      val univ = U.certify ctxt (mk_univ dT)
    5.21    in Thm.mk_binop inv univ ct end
    5.22  
    5.23  fun mk_inj_prop ctxt ct =
    5.24    let
    5.25 -    val T = #T (Thm.rep_cterm ct)
    5.26 -    val dT = Term.domain_type T
    5.27 -    val inj = U.certify ctxt (mk_inj_on dT (Term.range_type T))
    5.28 +    val (dT, rT) = U.split_type (U.typ_of ct)
    5.29 +    val inj = U.certify ctxt (mk_inj_on dT rT)
    5.30      val univ = U.certify ctxt (mk_univ dT)
    5.31    in U.mk_cprop (Thm.mk_binop inj ct univ) end
    5.32  
    5.33  
    5.34  val disjE = @{lemma "~P | Q ==> P ==> Q" by fast}
    5.35  
    5.36 -fun prove_inj_prop ctxt hdef lhs =
    5.37 +fun prove_inj_prop ctxt def lhs =
    5.38    let
    5.39 -    val (ct, ctxt') = U.dest_all_cabs (Thm.rhs_of hdef) ctxt
    5.40 +    val (ct, ctxt') = U.dest_all_cabs (Thm.rhs_of def) ctxt
    5.41      val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
    5.42    in
    5.43      Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
    5.44 @@ -64,12 +63,12 @@
    5.45      |> singleton (Variable.export ctxt' ctxt)
    5.46    end
    5.47  
    5.48 -fun prove_rhs ctxt hdef lhs rhs =
    5.49 -  Goal.init rhs
    5.50 -  |> apply (CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv hdef)) ctxt))
    5.51 -  |> apply (REPEAT_ALL_NEW (Tactic.match_tac @{thms allI}))
    5.52 -  |> apply (Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt hdef lhs]))
    5.53 -  |> Goal.norm_result o Goal.finish ctxt
    5.54 +fun prove_rhs ctxt def lhs =
    5.55 +  T.by_tac (
    5.56 +    CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
    5.57 +    THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI})
    5.58 +    THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) #>
    5.59 +  Thm.elim_implies def
    5.60  
    5.61  
    5.62  fun expand thm ct =
    5.63 @@ -80,18 +79,17 @@
    5.64      val thm2 = Thm.instantiate (Thm.match (cpat, cr)) thm
    5.65    in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end
    5.66  
    5.67 -fun prove_lhs ctxt rhs lhs =
    5.68 +fun prove_lhs ctxt rhs =
    5.69    let
    5.70      val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs)))
    5.71    in
    5.72 -    Goal.init lhs
    5.73 -    |> apply (CONVERSION (U.prop_conv (U.binders_conv (K (expand eq)) ctxt)))
    5.74 -    |> apply (Simplifier.simp_tac HOL_ss)
    5.75 -    |> Goal.finish ctxt
    5.76 +    T.by_tac (
    5.77 +      CONVERSION (U.prop_conv (U.binders_conv (K (expand eq)) ctxt))
    5.78 +      THEN' Simplifier.simp_tac HOL_ss)
    5.79    end
    5.80  
    5.81  
    5.82 -fun mk_hdef ctxt rhs =
    5.83 +fun mk_inv_def ctxt rhs =
    5.84    let
    5.85      val (ct, ctxt') = U.dest_all_cbinders (U.dest_cprop rhs) ctxt
    5.86      val (cl, cv) = Thm.dest_binop ct
    5.87 @@ -102,9 +100,8 @@
    5.88  fun prove_inj_eq ctxt ct =
    5.89    let
    5.90      val (lhs, rhs) = pairself U.mk_cprop (Thm.dest_binop (U.dest_cprop ct))
    5.91 -    val hdef = mk_hdef ctxt rhs
    5.92 -    val lhs_thm = Thm.implies_intr rhs (prove_lhs ctxt rhs lhs)
    5.93 -    val rhs_thm = Thm.implies_intr lhs (prove_rhs ctxt hdef lhs rhs)
    5.94 +    val lhs_thm = prove_lhs ctxt rhs lhs
    5.95 +    val rhs_thm = prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs
    5.96    in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end
    5.97  
    5.98  
    5.99 @@ -125,12 +122,10 @@
   5.100  
   5.101  in
   5.102  
   5.103 -fun prove_injectivity ctxt ct =
   5.104 -  ct
   5.105 -  |> Goal.init
   5.106 -  |> apply (CONVERSION (U.prop_conv (norm_conv ctxt)))
   5.107 -  |> apply (CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt)))
   5.108 -  |> Goal.norm_result o Goal.finish ctxt
   5.109 +fun prove_injectivity ctxt =
   5.110 +  T.by_tac (
   5.111 +    CONVERSION (U.prop_conv (norm_conv ctxt))
   5.112 +    THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt)))
   5.113  
   5.114  end
   5.115  

     6.1 --- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Nov 22 15:45:42 2010 +0100
     6.2 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Nov 22 15:45:43 2010 +0100
     6.3 @@ -103,24 +103,20 @@
     6.4     context-independent modulo the current proof context to be able to
     6.5     use fast inference kernel rules during proof reconstruction. *)
     6.6  
     6.7 -fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
     6.8 -
     6.9  val maxidx_of = #maxidx o Thm.rep_cterm
    6.10  
    6.11  fun mk_inst ctxt vars =
    6.12    let
    6.13      val max = fold (Integer.max o fst) vars 0
    6.14      val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
    6.15 -    fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
    6.16 +    fun mk (i, v) = (v, U.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
    6.17    in map mk vars end
    6.18  
    6.19 -val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
    6.20 -
    6.21  fun close ctxt (ct, vars) =
    6.22    let
    6.23      val inst = mk_inst ctxt vars
    6.24      val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
    6.25 -  in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end
    6.26 +  in (U.mk_cprop (Thm.instantiate_cterm ([], inst) ct), names) end
    6.27  
    6.28  
    6.29  fun mk_bound thy (i, T) =
    6.30 @@ -195,7 +191,7 @@
    6.31        |> Symtab.fold (Variable.declare_term o snd) terms
    6.32  
    6.33      fun cert @{const True} = not_false
    6.34 -      | cert t = certify ctxt' t
    6.35 +      | cert t = U.certify ctxt' t
    6.36  
    6.37    in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end
    6.38  
    6.39 @@ -210,7 +206,7 @@
    6.40      SOME _ => cx
    6.41    | NONE => cx |> fresh_name (decl_prefix ^ n)
    6.42        |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
    6.43 -           let val upd = Symtab.update (n, certify ctxt (Free (m, T)))
    6.44 +           let val upd = Symtab.update (n, U.certify ctxt (Free (m, T)))
    6.45             in (typs, upd terms, exprs, steps, vars, ctxt) end))
    6.46  
    6.47  fun mk_typ (typs, _, _, _, _, ctxt) (s as I.Sym (n, _)) = 

     7.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 22 15:45:42 2010 +0100
     7.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 22 15:45:43 2010 +0100
     7.3 @@ -683,33 +683,29 @@
     7.4    val unfold_conv =
     7.5      Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv))
     7.6    val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq
     7.7 +
     7.8 +  fun assume_prems ctxt thm =
     7.9 +    Assumption.add_assumes (Drule.cprems_of thm) ctxt
    7.10 +    |>> (fn thms => fold Thm.elim_implies thms thm)
    7.11  in
    7.12  
    7.13 -fun rewrite' ctxt simpset ths = Thm o with_conv ctxt ths (try_apply ctxt [] [
    7.14 -  named ctxt "conj/disj/distinct" prove_conj_disj_eq,
    7.15 -  T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
    7.16 -    NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
    7.17 -    THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
    7.18 -  T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
    7.19 -    NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
    7.20 -    THEN_ALL_NEW (
    7.21 -      NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
    7.22 -      ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
    7.23 -  T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
    7.24 -    NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
    7.25 -    THEN_ALL_NEW (
    7.26 -      NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
    7.27 -      ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
    7.28 -  named ctxt "injectivity" (M.prove_injectivity ctxt)])
    7.29 -
    7.30 -fun rewrite simpset thms ct ctxt = (* FIXME: join with rewrite' *)
    7.31 -  let
    7.32 -    val thm = rewrite' ctxt simpset thms ct
    7.33 -    val ord = Term_Ord.fast_term_ord o pairself Thm.term_of
    7.34 -    val chyps = fold (Ord_List.union ord o #hyps o Thm.crep_thm o thm_of) thms []
    7.35 -    val new_chyps = Ord_List.subtract ord chyps (#hyps (Thm.crep_thm (thm_of thm)))
    7.36 -    val (_, ctxt') = Assumption.add_assumes new_chyps ctxt
    7.37 -  in (thm, ctxt') end
    7.38 +fun rewrite simpset ths ct ctxt =
    7.39 +  apfst Thm (assume_prems ctxt (with_conv ctxt ths (try_apply ctxt [] [
    7.40 +    named ctxt "conj/disj/distinct" prove_conj_disj_eq,
    7.41 +    T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
    7.42 +      NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
    7.43 +      THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
    7.44 +    T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
    7.45 +      NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
    7.46 +      THEN_ALL_NEW (
    7.47 +        NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
    7.48 +        ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
    7.49 +    T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
    7.50 +      NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
    7.51 +      THEN_ALL_NEW (
    7.52 +        NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
    7.53 +        ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
    7.54 +    named ctxt "injectivity" (M.prove_injectivity ctxt)]) ct))
    7.55  
    7.56  end
    7.57  

     8.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Nov 22 15:45:42 2010 +0100
     8.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Nov 22 15:45:43 2010 +0100
     8.3 @@ -9,7 +9,6 @@
     8.4    (* accessing and modifying terms *)
     8.5    val term_of: cterm -> term
     8.6    val prop_of: thm -> term
     8.7 -  val mk_prop: cterm -> cterm
     8.8    val as_meta_eq: cterm -> cterm
     8.9  
    8.10    (* theorem nets *)
    8.11 @@ -59,9 +58,7 @@
    8.12  fun term_of ct = dest_prop (Thm.term_of ct)
    8.13  fun prop_of thm = dest_prop (Thm.prop_of thm)
    8.14  
    8.15 -val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
    8.16 -
    8.17 -fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (Thm.dest_arg ct))
    8.18 +fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct))
    8.19  
    8.20  
    8.21  
    8.22 @@ -85,7 +82,7 @@
    8.23  (* proof combinators *)
    8.24  
    8.25  fun under_assumption f ct =
    8.26 -  let val ct' = mk_prop ct
    8.27 +  let val ct' = U.mk_cprop ct
    8.28    in Thm.implies_intr ct' (f (Thm.assume ct')) end
    8.29  
    8.30  fun with_conv conv prove ct =
    8.31 @@ -125,9 +122,6 @@
    8.32  
    8.33  local
    8.34  
    8.35 -fun typ_of ct = #T (Thm.rep_cterm ct)
    8.36 -fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
    8.37 -
    8.38  fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
    8.39  
    8.40  fun context_of (ctxt, _, _, _) = ctxt
    8.41 @@ -153,7 +147,8 @@
    8.42      | NONE =>
    8.43          let
    8.44            val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
    8.45 -          val cv = certify ctxt' (Free (n, map typ_of cvs' ---> typ_of ct))
    8.46 +          val cv = U.certify ctxt'
    8.47 +            (Free (n, map U.typ_of cvs' ---> U.typ_of ct))
    8.48            val cu = Drule.list_comb (cv, cvs')
    8.49            val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
    8.50            val beta_norm' = beta_norm orelse not (null cvs')