expand combinators in Isar proofs constructed by Sledgehammer;
this requires shuffling around a couple of functions previously defined in Refute

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Apr 29 01:11:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Apr 29 01:17:14 2010 +0200
@@ -1260,15 +1260,15 @@
   | t1 $ _ => term_under_def t1
   | _ => t
 
-(* Here we crucially rely on "Refute.specialize_type" performing a preorder
-   traversal of the term, without which the wrong occurrence of a constant could
-   be matched in the face of overloading. *)
+(* Here we crucially rely on "specialize_type" performing a preorder traversal
+   of the term, without which the wrong occurrence of a constant could be
+   matched in the face of overloading. *)
 fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
   if is_built_in_const thy stds fast_descrs x then
     []
   else
     these (Symtab.lookup table s)
-    |> map_filter (try (Refute.specialize_type thy x))
+    |> map_filter (try (specialize_type thy x))
     |> filter (curry (op =) (Const x) o term_under_def)
 
 fun normalized_rhs_of t =
@@ -1381,8 +1381,8 @@
     SOME t' => is_constr_pattern_lhs thy t'
   | NONE => false
 
-(* Similar to "Refute.specialize_type" but returns all matches rather than only
-   the first (preorder) match. *)
+(* Similar to "specialize_type" but returns all matches rather than only the
+   first (preorder) match. *)
 fun multi_specialize_type thy slack (s, T) t =
   let
     fun aux (Const (s', T')) ys =
@@ -1390,8 +1390,8 @@
           ys |> (if AList.defined (op =) ys T' then
                    I
                  else
-                   cons (T', Refute.monomorphic_term
-                                 (Sign.typ_match thy (T', T) Vartab.empty) t)
+                   cons (T', monomorphic_term (Sign.typ_match thy (T', T)
+                                                              Vartab.empty) t)
                    handle Type.TYPE_MATCH => I
                         | Refute.REFUTE _ =>
                           if slack then
@@ -1682,7 +1682,7 @@
   let val abs_T = domain_type T in
     typedef_info thy (fst (dest_Type abs_T)) |> the
     |> pairf #Abs_inverse #Rep_inverse
-    |> pairself (Refute.specialize_type thy x o prop_of o the)
+    |> pairself (specialize_type thy x o prop_of o the)
     ||> single |> op ::
   end
 fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
@@ -1697,7 +1697,7 @@
         val set_t = Const (set_name, rep_T --> bool_T)
         val set_t' =
           prop_of_Rep |> HOLogic.dest_Trueprop
-                      |> Refute.specialize_type thy (dest_Const rep_t)
+                      |> specialize_type thy (dest_Const rep_t)
                       |> HOLogic.dest_mem |> snd
       in
         [HOLogic.all_const abs_T

--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Apr 29 01:11:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Apr 29 01:17:14 2010 +0200
@@ -914,8 +914,8 @@
                  val class = Logic.class_of_const s
                  val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
                                                    class)
-                 val ax1 = try (Refute.specialize_type thy x) of_class
-                 val ax2 = Option.map (Refute.specialize_type thy x o snd)
+                 val ax1 = try (specialize_type thy x) of_class
+                 val ax2 = Option.map (specialize_type thy x o snd)
                                       (Refute.get_classdef thy class)
                in
                  fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
@@ -997,7 +997,7 @@
           map (fn t => case Term.add_tvars t [] of
                          [] => t
                        | [(x, S)] =>
-                         Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
+                         monomorphic_term (Vartab.make [(x, (S, T))]) t
                        | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
                                           \add_axioms_for_sort", [t]))
               class_axioms

--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Apr 29 01:11:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Apr 29 01:17:14 2010 +0200
@@ -57,6 +57,8 @@
   val bool_T : typ
   val nat_T : typ
   val int_T : typ
+  val monomorphic_term : Type.tyenv -> term -> term
+  val specialize_type : theory -> (string * typ) -> term -> term
   val nat_subscript : int -> string
   val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
   val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
@@ -227,6 +229,9 @@
 val nat_T = @{typ nat}
 val int_T = @{typ int}
 
+val monomorphic_term = Sledgehammer_Util.monomorphic_term
+val specialize_type = Sledgehammer_Util.specialize_type
+
 val subscript = implode o map (prefix "\<^isub>") o explode
 fun nat_subscript n =
   (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 01:11:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 01:17:14 2010 +0200
@@ -392,6 +392,21 @@
   fold forall_of (Term.add_consts t []
                  |> filter (is_skolem_const_name o fst) |> map Const) t
 
+val combinator_table =
+  [(@{const_name COMBI}, @{thm COMBI_def_raw}),
+   (@{const_name COMBK}, @{thm COMBK_def_raw}),
+   (@{const_name COMBB}, @{thm COMBB_def_raw}),
+   (@{const_name COMBC}, @{thm COMBC_def_raw}),
+   (@{const_name COMBS}, @{thm COMBS_def_raw})]
+
+fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
+  | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
+  | uncombine_term (t as Const (x as (s, _))) =
+    (case AList.lookup (op =) combinator_table s of
+       SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
+     | NONE => t)
+  | uncombine_term t = t
+
 (* Interpret a list of syntax trees as a clause, given by "real" literals and
    sort constraints. "vt" holds the initial sort constraints, from the
    conjecture clauses. *)
@@ -435,15 +450,16 @@
       val t2 = clause_of_nodes ctxt vt us
       val (t1, t2) =
         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
-        |> unvarify_args |> check_clause ctxt |> HOLogic.dest_eq
+        |> unvarify_args |> uncombine_term |> check_clause ctxt
+        |> HOLogic.dest_eq
     in
       (Definition (num, t1, t2),
        fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
     end
   | decode_line vt (Inference (num, us, deps)) ctxt =
     let
-      val t = us |> clause_of_nodes ctxt vt |> unskolemize_term
-                 |> check_clause ctxt
+      val t = us |> clause_of_nodes ctxt vt
+                 |> unskolemize_term |> uncombine_term |> check_clause ctxt
     in
       (Inference (num, t, deps),
        fold Variable.declare_term (OldTerm.term_frees t) ctxt)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Apr 29 01:11:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Apr 29 01:17:14 2010 +0200
@@ -18,6 +18,8 @@
   val nat_subscript : int -> string
   val unyxml : string -> string
   val maybe_quote : string -> string
+  val monomorphic_term : Type.tyenv -> term -> term
+  val specialize_type : theory -> (string * typ) -> term -> term
 end;
  
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -103,4 +105,30 @@
            OuterKeyword.is_keyword s) ? quote
   end
 
+fun monomorphic_term subst t =
+  map_types (map_type_tvar (fn v =>
+      case Type.lookup subst v of
+        SOME typ => typ
+      | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
+                            \variable", [t]))) t
+
+fun specialize_type thy (s, T) t =
+  let
+    fun subst_for (Const (s', T')) =
+      if s = s' then
+        SOME (Sign.typ_match thy (T', T) Vartab.empty)
+        handle Type.TYPE_MATCH => NONE
+      else
+        NONE
+    | subst_for (t1 $ t2) =
+      (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2)
+    | subst_for (Abs (_, _, t')) = subst_for t'
+    | subst_for _ = NONE
+  in
+    case subst_for t of
+      SOME subst => monomorphic_term subst t
+    | NONE => raise Type.TYPE_MATCH
+  end
+
+
 end;

--- a/src/HOL/Tools/refute.ML	Thu Apr 29 01:11:06 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Thu Apr 29 01:17:14 2010 +0200
@@ -70,8 +70,6 @@
   val is_IDT_constructor : theory -> string * typ -> bool
   val is_IDT_recursor : theory -> string * typ -> bool
   val is_const_of_class: theory -> string * typ -> bool
-  val monomorphic_term : Type.tyenv -> term -> term
-  val specialize_type : theory -> (string * typ) -> term -> term
   val string_of_typ : typ -> string
   val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
 end;  (* signature REFUTE *)
@@ -449,57 +447,8 @@
       Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
   end;
 
-(* ------------------------------------------------------------------------- *)
-(* monomorphic_term: applies a type substitution 'typeSubs' for all type     *)
-(*                   variables in a term 't'                                 *)
-(* ------------------------------------------------------------------------- *)
-
-  (* Type.tyenv -> Term.term -> Term.term *)
-
-  fun monomorphic_term typeSubs t =
-    map_types (map_type_tvar
-      (fn v =>
-        case Type.lookup typeSubs v of
-          NONE =>
-          (* schematic type variable not instantiated *)
-          raise REFUTE ("monomorphic_term",
-            "no substitution for type variable " ^ fst (fst v) ^
-            " in term " ^ Syntax.string_of_term_global Pure.thy t)
-        | SOME typ =>
-          typ)) t;
-
-(* ------------------------------------------------------------------------- *)
-(* specialize_type: given a constant 's' of type 'T', which is a subterm of  *)
-(*                  't', where 't' has a (possibly) more general type, the   *)
-(*                  schematic type variables in 't' are instantiated to      *)
-(*                  match the type 'T' (may raise Type.TYPE_MATCH)           *)
-(* ------------------------------------------------------------------------- *)
-
-  (* theory -> (string * Term.typ) -> Term.term -> Term.term *)
-
-  fun specialize_type thy (s, T) t =
-  let
-    fun find_typeSubs (Const (s', T')) =
-      if s=s' then
-        SOME (Sign.typ_match thy (T', T) Vartab.empty)
-          handle Type.TYPE_MATCH => NONE
-      else
-        NONE
-      | find_typeSubs (Free _)           = NONE
-      | find_typeSubs (Var _)            = NONE
-      | find_typeSubs (Bound _)          = NONE
-      | find_typeSubs (Abs (_, _, body)) = find_typeSubs body
-      | find_typeSubs (t1 $ t2)          =
-      (case find_typeSubs t1 of SOME x => SOME x
-                              | NONE   => find_typeSubs t2)
-  in
-    case find_typeSubs t of
-      SOME typeSubs =>
-      monomorphic_term typeSubs t
-    | NONE =>
-      (* no match found - perhaps due to sort constraints *)
-      raise Type.TYPE_MATCH
-  end;
+val monomorphic_term = Sledgehammer_Util.monomorphic_term
+val specialize_type = Sledgehammer_Util.specialize_type
 
 (* ------------------------------------------------------------------------- *)
 (* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that   *)