support Vampire definitions of constants as "let" constructs in Isar proofs
authorblanchet
Wed Apr 28 12:46:50 2010 +0200 (2010-04-28)
changeset 36486c2d7e2dff59e
parent 36485 56ce8fc56be3
child 36487 50fd056cc3ce
support Vampire definitions of constants as "let" constructs in Isar proofs
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 18:58:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 28 12:46:50 2010 +0200
     1.3 @@ -33,6 +33,10 @@
     1.4  structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
     1.5  struct
     1.6  
     1.7 +datatype ('a, 'b, 'c, 'd, 'e) raw_step =
     1.8 +  Definition of 'a * 'b * 'c |
     1.9 +  Inference of 'a * 'd * 'e list
    1.10 +
    1.11  open Sledgehammer_Util
    1.12  open Sledgehammer_FOL_Clause
    1.13  open Sledgehammer_Fact_Preprocessor
    1.14 @@ -53,11 +57,11 @@
    1.15  (**** PARSING OF TSTP FORMAT ****)
    1.16  
    1.17  (* Syntax trees, either term list or formulae *)
    1.18 -datatype stree = SInt of int | SBranch of string * stree list;
    1.19 +datatype node = IntLeaf of int | StrNode of string * node list
    1.20  
    1.21 -fun atom x = SBranch (x, [])
    1.22 +fun atom x = StrNode (x, [])
    1.23  
    1.24 -fun scons (x, y) = SBranch ("cons", [x, y])
    1.25 +fun scons (x, y) = StrNode ("cons", [x, y])
    1.26  val slist_of = List.foldl scons (atom "nil")
    1.27  
    1.28  (*Strings enclosed in single quotes, e.g. filenames*)
    1.29 @@ -75,54 +79,63 @@
    1.30  (* The "x" argument is not strictly necessary, but without it Poly/ML loops
    1.31     forever at compile time. *)
    1.32  fun parse_term pool x =
    1.33 -  (parse_quoted >> atom
    1.34 -   || parse_integer >> SInt
    1.35 +     (parse_quoted >> atom
    1.36 +   || parse_integer >> IntLeaf
    1.37     || $$ "$" |-- Symbol.scan_id >> (atom o repair_bool_literal)
    1.38     || (Symbol.scan_id >> repair_name pool)
    1.39 -      -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> SBranch
    1.40 +      -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
    1.41     || $$ "(" |-- parse_term pool --| $$ ")"
    1.42     || $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
    1.43  and parse_terms pool x =
    1.44    (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
    1.45  
    1.46 -fun negate_stree t = SBranch ("c_Not", [t])
    1.47 -fun equate_strees t1 t2 = SBranch ("c_equal", [t1, t2]);
    1.48 +fun negate_node u = StrNode ("c_Not", [u])
    1.49 +fun equate_nodes u1 u2 = StrNode ("c_equal", [u1, u2])
    1.50  
    1.51  (* Apply equal or not-equal to a term. *)
    1.52 -fun repair_predicate_term (t, NONE) = t
    1.53 -  | repair_predicate_term (t1, SOME (NONE, t2)) = equate_strees t1 t2
    1.54 -  | repair_predicate_term (t1, SOME (SOME _, t2)) =
    1.55 -    negate_stree (equate_strees t1 t2)
    1.56 +fun repair_predicate_term (u, NONE) = u
    1.57 +  | repair_predicate_term (u1, SOME (NONE, u2)) = equate_nodes u1 u2
    1.58 +  | repair_predicate_term (u1, SOME (SOME _, u2)) =
    1.59 +    negate_node (equate_nodes u1 u2)
    1.60  fun parse_predicate_term pool =
    1.61    parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
    1.62                                    -- parse_term pool)
    1.63    >> repair_predicate_term
    1.64 -(*Literals can involve negation, = and !=.*)
    1.65 +(* Literals can involve "~", "=", and "!=". *)
    1.66  fun parse_literal pool x =
    1.67 -  ($$ "~" |-- parse_literal pool >> negate_stree || parse_predicate_term pool) x
    1.68 +  ($$ "~" |-- parse_literal pool >> negate_node || parse_predicate_term pool) x
    1.69  
    1.70  fun parse_literals pool =
    1.71    parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
    1.72  
    1.73 -(* Clause: a list of literals separated by the disjunction sign. *)
    1.74 +(* Clause: a list of literals separated by disjunction operators ("|"). *)
    1.75  fun parse_clause pool =
    1.76    $$ "(" |-- parse_literals pool --| $$ ")" || Scan.single (parse_literal pool)
    1.77  
    1.78 -fun ints_of_stree (SInt n) = cons n
    1.79 -  | ints_of_stree (SBranch (_, ts)) = fold ints_of_stree ts
    1.80 +fun ints_of_node (IntLeaf n) = cons n
    1.81 +  | ints_of_node (StrNode (_, us)) = fold ints_of_node us
    1.82  val parse_tstp_annotations =
    1.83    Scan.optional ($$ "," |-- parse_term NONE
    1.84                     --| Scan.option ($$ "," |-- parse_terms NONE)
    1.85 -                 >> (fn source => ints_of_stree source [])) []
    1.86 +                 >> (fn source => ints_of_node source [])) []
    1.87 +
    1.88 +fun parse_definition pool =
    1.89 +  $$ "(" |-- parse_literal NONE --| Scan.this_string "<=>"
    1.90 +  -- parse_clause pool --| $$ ")"
    1.91  
    1.92 -(* cnf(<name>, <formula_role>, <cnf_formula> <annotations>).
    1.93 -   The <name> could be an identifier, but we assume integers. *)
    1.94 -fun retuple_tstp_line ((name, ts), deps) = (name, ts, deps)
    1.95 +(* Syntax: cnf(<num>, <formula_role>, <cnf_formula> <annotations>).
    1.96 +   The <num> could be an identifier, but we assume integers. *)
    1.97 +fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us)
    1.98 +fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps)
    1.99  fun parse_tstp_line pool =
   1.100 -  (Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
   1.101 -   --| Symbol.scan_id --| $$ "," -- parse_clause pool -- parse_tstp_annotations
   1.102 -   --| $$ ")" --| $$ "."
   1.103 -  >> retuple_tstp_line
   1.104 +     ((Scan.this_string "fof" -- $$ "(") |-- parse_integer --| $$ ","
   1.105 +       --| Scan.this_string "definition" --| $$ "," -- parse_definition pool
   1.106 +       --| parse_tstp_annotations --| $$ ")" --| $$ "."
   1.107 +      >> finish_tstp_definition_line)
   1.108 +  || ((Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
   1.109 +       --| Symbol.scan_id --| $$ "," -- parse_clause pool
   1.110 +       -- parse_tstp_annotations --| $$ ")" --| $$ "."
   1.111 +      >> finish_tstp_inference_line)
   1.112  
   1.113  (**** PARSING OF SPASS OUTPUT ****)
   1.114  
   1.115 @@ -143,22 +156,22 @@
   1.116    Scan.repeat (parse_starred_predicate_term pool) --| $$ "-" --| $$ ">"
   1.117    -- Scan.repeat (parse_starred_predicate_term pool)
   1.118    >> (fn ([], []) => [atom "c_False"]
   1.119 -       | (clauses1, clauses2) => map negate_stree clauses1 @ clauses2)
   1.120 +       | (clauses1, clauses2) => map negate_node clauses1 @ clauses2)
   1.121  
   1.122 -(* Syntax: <name>[0:<inference><annotations>] ||
   1.123 +(* Syntax: <num>[0:<inference><annotations>] ||
   1.124             <cnf_formulas> -> <cnf_formulas>. *)
   1.125 -fun retuple_spass_line ((name, deps), ts) = (name, ts, deps)
   1.126 +fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
   1.127  fun parse_spass_line pool =
   1.128    parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
   1.129    -- parse_spass_annotations --| $$ "]" --| $$ "|" --| $$ "|"
   1.130    -- parse_horn_clause pool --| $$ "."
   1.131 -  >> retuple_spass_line
   1.132 +  >> finish_spass_line
   1.133  
   1.134  fun parse_line pool = fst o (parse_tstp_line pool || parse_spass_line pool)
   1.135  
   1.136  (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   1.137  
   1.138 -exception STREE of stree;
   1.139 +exception NODE of node
   1.140  
   1.141  (*If string s has the prefix s1, return the result of deleting it.*)
   1.142  fun strip_prefix s1 s =
   1.143 @@ -181,24 +194,21 @@
   1.144  
   1.145  (*Type variables are given the basic sort, HOL.type. Some will later be constrained
   1.146    by information from type literals, or by type inference.*)
   1.147 -fun type_of_stree t =
   1.148 -  case t of
   1.149 -      SInt _ => raise STREE t
   1.150 -    | SBranch (a,ts) =>
   1.151 -        let val Ts = map type_of_stree ts
   1.152 -        in
   1.153 -          case strip_prefix tconst_prefix a of
   1.154 -              SOME b => Type(invert_type_const b, Ts)
   1.155 -            | NONE =>
   1.156 -                if not (null ts) then raise STREE t  (*only tconsts have type arguments*)
   1.157 -                else
   1.158 -                case strip_prefix tfree_prefix a of
   1.159 -                    SOME b => TFree("'" ^ b, HOLogic.typeS)
   1.160 -                  | NONE =>
   1.161 -                case strip_prefix tvar_prefix a of
   1.162 -                    SOME b => make_tvar b
   1.163 -                  | NONE => make_tparam a  (* Variable from the ATP, say "X1" *)
   1.164 -        end;
   1.165 +fun type_of_node (u as IntLeaf _) = raise NODE u
   1.166 +  | type_of_node (u as StrNode (a, us)) =
   1.167 +    let val Ts = map type_of_node us in
   1.168 +      case strip_prefix tconst_prefix a of
   1.169 +        SOME b => Type (invert_type_const b, Ts)
   1.170 +      | NONE =>
   1.171 +        if not (null us) then
   1.172 +          raise NODE u  (*only tconsts have type arguments*)
   1.173 +        else case strip_prefix tfree_prefix a of
   1.174 +          SOME b => TFree ("'" ^ b, HOLogic.typeS)
   1.175 +        | NONE =>
   1.176 +          case strip_prefix tvar_prefix a of
   1.177 +            SOME b => make_tvar b
   1.178 +          | NONE => make_tparam a  (* Variable from the ATP, say "X1" *)
   1.179 +    end
   1.180  
   1.181  (*Invert the table of translations between Isabelle and ATPs*)
   1.182  val const_trans_table_inv =
   1.183 @@ -213,46 +223,68 @@
   1.184  (*Generates a constant, given its type arguments*)
   1.185  fun const_of thy (a,Ts) = Const(a, Sign.const_instance thy (a,Ts));
   1.186  
   1.187 +fun fix_atp_variable_name s =
   1.188 +  let
   1.189 +    fun subscript_name s n = s ^ nat_subscript n
   1.190 +    val s = String.map Char.toLower s
   1.191 +  in
   1.192 +    case space_explode "_" s of
   1.193 +      [_] => (case take_suffix Char.isDigit (String.explode s) of
   1.194 +                (cs1 as _ :: _, cs2 as _ :: _) =>
   1.195 +                subscript_name (String.implode cs1)
   1.196 +                               (the (Int.fromString (String.implode cs2)))
   1.197 +              | (_, _) => s)
   1.198 +    | [s1, s2] => (case Int.fromString s2 of
   1.199 +                     SOME n => subscript_name s1 n
   1.200 +                   | NONE => s)
   1.201 +    | _ => s
   1.202 +  end
   1.203 +
   1.204  (*First-order translation. No types are known for variables. HOLogic.typeT should allow
   1.205    them to be inferred.*)
   1.206 -fun term_of_stree args thy t =
   1.207 -  case t of
   1.208 -      SInt _ => raise STREE t
   1.209 -    | SBranch ("hBOOL", [t]) => term_of_stree [] thy t  (*ignore hBOOL*)
   1.210 -    | SBranch ("hAPP", [t, u]) => term_of_stree (u::args) thy t
   1.211 -    | SBranch (a, ts) =>
   1.212 -        case strip_prefix const_prefix a of
   1.213 -            SOME "equal" =>
   1.214 -              list_comb(Const (@{const_name "op ="}, HOLogic.typeT), List.map (term_of_stree [] thy) ts)
   1.215 -          | SOME b =>
   1.216 -              let val c = invert_const b
   1.217 -                  val nterms = length ts - num_typargs thy c
   1.218 -                  val us = List.map (term_of_stree [] thy) (List.take(ts,nterms) @ args)
   1.219 -                  (*Extra args from hAPP come AFTER any arguments given directly to the
   1.220 -                    constant.*)
   1.221 -                  val Ts = List.map type_of_stree (List.drop(ts,nterms))
   1.222 -              in  list_comb(const_of thy (c, Ts), us)  end
   1.223 -          | NONE => (*a variable, not a constant*)
   1.224 -              let val T = HOLogic.typeT
   1.225 -                  val opr = (*a Free variable is typically a Skolem function*)
   1.226 -                    case strip_prefix fixed_var_prefix a of
   1.227 -                        SOME b => Free(b,T)
   1.228 -                      | NONE =>
   1.229 -                    case strip_prefix schematic_var_prefix a of
   1.230 -                        SOME b => make_var (b,T)
   1.231 -                      | NONE => make_var (a,T)  (* Variable from the ATP, say "X1" *)
   1.232 -              in  list_comb (opr, List.map (term_of_stree [] thy) (ts@args))  end;
   1.233 +fun term_of_node args thy u =
   1.234 +  case u of
   1.235 +    IntLeaf _ => raise NODE u
   1.236 +  | StrNode ("hBOOL", [u]) => term_of_node [] thy u  (* ignore hBOOL *)
   1.237 +  | StrNode ("hAPP", [u1, u2]) => term_of_node (u2 :: args) thy u1
   1.238 +  | StrNode (a, us) =>
   1.239 +    case strip_prefix const_prefix a of
   1.240 +      SOME "equal" =>
   1.241 +      list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
   1.242 +                 map (term_of_node [] thy) us)
   1.243 +    | SOME b =>
   1.244 +      let
   1.245 +        val c = invert_const b
   1.246 +        val nterms = length us - num_typargs thy c
   1.247 +        val ts = map (term_of_node [] thy) (take nterms us @ args)
   1.248 +        (*Extra args from hAPP come AFTER any arguments given directly to the
   1.249 +          constant.*)
   1.250 +        val Ts = map type_of_node (drop nterms us)
   1.251 +      in list_comb(const_of thy (c, Ts), ts) end
   1.252 +    | NONE => (*a variable, not a constant*)
   1.253 +      let
   1.254 +        val opr =
   1.255 +          (* a Free variable is typically a Skolem function *)
   1.256 +          case strip_prefix fixed_var_prefix a of
   1.257 +            SOME b => Free (b, HOLogic.typeT)
   1.258 +          | NONE =>
   1.259 +            case strip_prefix schematic_var_prefix a of
   1.260 +              SOME b => make_var (b, HOLogic.typeT)
   1.261 +            | NONE =>
   1.262 +              (* Variable from the ATP, say "X1" *)
   1.263 +              make_var (fix_atp_variable_name a, HOLogic.typeT)
   1.264 +      in list_comb (opr, map (term_of_node [] thy) (us @ args)) end
   1.265  
   1.266  (* Type class literal applied to a type. Returns triple of polarity, class,
   1.267     type. *)
   1.268 -fun constraint_of_stree pol (SBranch ("c_Not", [t])) =
   1.269 -    constraint_of_stree (not pol) t
   1.270 -  | constraint_of_stree pol t = case t of
   1.271 -        SInt _ => raise STREE t
   1.272 -      | SBranch (a, ts) =>
   1.273 -            (case (strip_prefix class_prefix a, map type_of_stree ts) of
   1.274 -                 (SOME b, [T]) => (pol, b, T)
   1.275 -               | _ => raise STREE t);
   1.276 +fun constraint_of_node pos (StrNode ("c_Not", [u])) =
   1.277 +    constraint_of_node (not pos) u
   1.278 +  | constraint_of_node pos u = case u of
   1.279 +        IntLeaf _ => raise NODE u
   1.280 +      | StrNode (a, us) =>
   1.281 +            (case (strip_prefix class_prefix a, map type_of_node us) of
   1.282 +                 (SOME b, [T]) => (pos, b, T)
   1.283 +               | _ => raise NODE u)
   1.284  
   1.285  (** Accumulate type constraints in a clause: negative type literals **)
   1.286  
   1.287 @@ -276,7 +308,8 @@
   1.288      @{const "op |"} $ negate_term thy t1 $ negate_term thy t2
   1.289    | negate_term thy (@{const "op |"} $ t1 $ t2) =
   1.290      @{const "op &"} $ negate_term thy t1 $ negate_term thy t2
   1.291 -  | negate_term thy (@{const Not} $ t) = t
   1.292 +  | negate_term _ (@{const Not} $ t) = t
   1.293 +  | negate_term _ t = @{const Not} $ t
   1.294  fun negate_formula thy (@{const Trueprop} $ t) =
   1.295      @{const Trueprop} $ negate_term thy t
   1.296    | negate_formula thy t =
   1.297 @@ -301,11 +334,10 @@
   1.298           |> clause_for_literals thy
   1.299  
   1.300  (*Accumulate sort constraints in vt, with "real" literals in lits.*)
   1.301 -fun lits_of_strees thy (vt, lits) [] = (vt, finish_clause thy lits)
   1.302 -  | lits_of_strees thy (vt, lits) (t :: ts) =
   1.303 -    lits_of_strees thy (add_constraint (constraint_of_stree true t, vt), lits)
   1.304 -                   ts
   1.305 -    handle STREE _ => lits_of_strees thy (vt, term_of_stree [] thy t :: lits) ts
   1.306 +fun lits_of_nodes thy (vt, lits) [] = (vt, finish_clause thy lits)
   1.307 +  | lits_of_nodes thy (vt, lits) (u :: us) =
   1.308 +    lits_of_nodes thy (add_constraint (constraint_of_node true u, vt), lits) us
   1.309 +    handle NODE _ => lits_of_nodes thy (vt, term_of_node [] thy u :: lits) us
   1.310  
   1.311  (*Update TVars/TFrees with detected sort constraints.*)
   1.312  fun repair_sorts vt =
   1.313 @@ -317,103 +349,133 @@
   1.314          | tmsubst (Var (xi, T)) = Var (xi, tysubst T)
   1.315          | tmsubst (t as Bound _) = t
   1.316          | tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t)
   1.317 -        | tmsubst (t $ u) = tmsubst t $ tmsubst u;
   1.318 +        | tmsubst (t1 $ t2) = tmsubst t1 $ tmsubst t2
   1.319    in not (Vartab.is_empty vt) ? tmsubst end;
   1.320  
   1.321 -(*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
   1.322 -  vt0 holds the initial sort constraints, from the conjecture clauses.*)
   1.323 -fun clause_of_strees ctxt vt ts =
   1.324 -  let val (vt, dt) = lits_of_strees (ProofContext.theory_of ctxt) (vt, []) ts in
   1.325 -    dt |> repair_sorts vt |> TypeInfer.constrain HOLogic.boolT
   1.326 -       |> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic
   1.327 -                                                   ctxt)
   1.328 -  end
   1.329 -
   1.330 -fun decode_line vt0 (name, ts, deps) ctxt =
   1.331 -  let val cl = clause_of_strees ctxt vt0 ts in
   1.332 -    ((name, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt)
   1.333 +(* Interpret a list of syntax trees as a clause, given by "real" literals and
   1.334 +   sort constraints. "vt" holds the initial sort constraints, from the
   1.335 +   conjecture clauses. *)
   1.336 +fun clause_of_nodes ctxt vt us =
   1.337 +  let val (vt, dt) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in
   1.338 +    dt |> repair_sorts vt
   1.339    end
   1.340 -
   1.341 -(** Global sort constraints on TFrees (from tfree_tcs) are positive unit clauses. **)
   1.342 +fun check_clause ctxt =
   1.343 +  TypeInfer.constrain HOLogic.boolT
   1.344 +  #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
   1.345 +fun checked_clause_of_nodes ctxt = check_clause ctxt oo clause_of_nodes ctxt
   1.346  
   1.347 -fun add_tfree_constraint ((true, cl, TFree(a,_)), vt) =
   1.348 -    add_var ((a, ~1) , cl) vt
   1.349 -  | add_tfree_constraint (_, vt) = vt;
   1.350 +(** Global sort constraints on TFrees (from tfree_tcs) are positive unit
   1.351 +    clauses. **)
   1.352  
   1.353 +fun add_tfree_constraint (true, cl, TFree (a, _)) = add_var ((a, ~1), cl)
   1.354 +  | add_tfree_constraint _ = I
   1.355  fun tfree_constraints_of_clauses vt [] = vt
   1.356 -  | tfree_constraints_of_clauses vt ([lit]::tss) =
   1.357 -      (tfree_constraints_of_clauses (add_tfree_constraint (constraint_of_stree true lit, vt)) tss
   1.358 -       handle STREE _ => (*not a positive type constraint: ignore*)
   1.359 -       tfree_constraints_of_clauses vt tss)
   1.360 -  | tfree_constraints_of_clauses vt (_::tss) = tfree_constraints_of_clauses vt tss;
   1.361 +  | tfree_constraints_of_clauses vt ([lit] :: uss) =
   1.362 +    (tfree_constraints_of_clauses (add_tfree_constraint
   1.363 +                                          (constraint_of_node true lit) vt) uss
   1.364 +     handle NODE _ => (* Not a positive type constraint? Ignore the literal. *)
   1.365 +     tfree_constraints_of_clauses vt uss)
   1.366 +  | tfree_constraints_of_clauses vt (_ :: uss) =
   1.367 +    tfree_constraints_of_clauses vt uss
   1.368  
   1.369  
   1.370  (**** Translation of TSTP files to Isar Proofs ****)
   1.371  
   1.372 -fun decode_lines ctxt tuples =
   1.373 -  let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #2 tuples) in
   1.374 -    #1 (fold_map (decode_line vt0) tuples ctxt)
   1.375 -  end
   1.376 +fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   1.377 +  | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   1.378  
   1.379 -fun unequal t (_, t', _) = not (t aconv t');
   1.380 +fun clauses_in_lines (Definition (_, u, us)) = u :: us
   1.381 +  | clauses_in_lines (Inference (_, us, _)) = us
   1.382  
   1.383 -(*No "real" literals means only type information*)
   1.384 -fun eq_types t = t aconv HOLogic.true_const;
   1.385 +fun decode_line vt (Definition (num, u, us)) ctxt =
   1.386 +    let
   1.387 +      val cl1 = clause_of_nodes ctxt vt [u]
   1.388 +      val vars = snd (strip_comb cl1)
   1.389 +      val frees = map unvarify_term vars
   1.390 +      val unvarify_args = subst_atomic (vars ~~ frees)
   1.391 +      val cl2 = clause_of_nodes ctxt vt us
   1.392 +      val (cl1, cl2) =
   1.393 +        HOLogic.eq_const HOLogic.typeT $ cl1 $ cl2
   1.394 +        |> unvarify_args |> check_clause ctxt |> HOLogic.dest_eq
   1.395 +    in
   1.396 +      (Definition (num, cl1, cl2),
   1.397 +       fold Variable.declare_term (maps OldTerm.term_frees [cl1, cl2]) ctxt)
   1.398 +    end
   1.399 +  | decode_line vt (Inference (num, us, deps)) ctxt =
   1.400 +    let val cl = us |> clause_of_nodes ctxt vt |> check_clause ctxt in
   1.401 +      (Inference (num, cl, deps),
   1.402 +       fold Variable.declare_term (OldTerm.term_frees cl) ctxt)
   1.403 +    end
   1.404 +fun decode_lines ctxt lines =
   1.405 +  let
   1.406 +    val vt = tfree_constraints_of_clauses Vartab.empty
   1.407 +                                          (map clauses_in_lines lines)
   1.408 +  in #1 (fold_map (decode_line vt) lines ctxt) end
   1.409  
   1.410 -fun replace_dep (old, new) dep = if dep = old then new else [dep]
   1.411 -fun replace_deps p (num, t, deps) =
   1.412 -  (num, t, fold (union (op =) o replace_dep p) deps [])
   1.413 +fun aint_inference _ (Definition _) = true
   1.414 +  | aint_inference t (Inference (_, t', _)) = not (t aconv t')
   1.415 +
   1.416 +(* No "real" literals means only type information (tfree_tcs, clsrel, or
   1.417 +   clsarity). *)
   1.418 +val is_only_type_information = curry (op aconv) HOLogic.true_const
   1.419 +
   1.420 +fun replace_one_dep (old, new) dep = if dep = old then new else [dep]
   1.421 +fun replace_deps_in_line _ (line as Definition _) = line
   1.422 +  | replace_deps_in_line p (Inference (num, t, deps)) =
   1.423 +    Inference (num, t, fold (union (op =) o replace_one_dep p) deps [])
   1.424  
   1.425  (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
   1.426    only in type information.*)
   1.427 -fun add_line thm_names (num, t, []) lines =
   1.428 -      (* No dependencies: axiom or conjecture clause? *)
   1.429 -      if is_axiom_clause_number thm_names num then
   1.430 -        (* Axioms are not proof lines *)
   1.431 -        if eq_types t then
   1.432 -          (* Must be clsrel/clsarity: type information, so delete refs to it *)
   1.433 -          map (replace_deps (num, [])) lines
   1.434 -        else
   1.435 -          (case take_prefix (unequal t) lines of
   1.436 -             (_,[]) => lines                  (*no repetition of proof line*)
   1.437 -           | (pre, (num', _, _) :: post) =>   (*repetition: replace later line by earlier one*)
   1.438 -               pre @ map (replace_deps (num', [num])) post)
   1.439 -      else
   1.440 -        (num, t, []) :: lines
   1.441 -  | add_line _ (num, t, deps) lines =
   1.442 -      if eq_types t then (num, t, deps) :: lines
   1.443 -      (*Type information will be deleted later; skip repetition test.*)
   1.444 -      else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
   1.445 -      case take_prefix (unequal t) lines of
   1.446 -         (_,[]) => (num, t, deps) :: lines  (*no repetition of proof line*)
   1.447 -       | (pre, (num', t', _) :: post) =>
   1.448 -           (num, t', deps) ::               (*repetition: replace later line by earlier one*)
   1.449 -           (pre @ map (replace_deps (num', [num])) post);
   1.450 +fun add_line _ (line as Definition _) lines = line :: lines
   1.451 +  | add_line thm_names (Inference (num, t, [])) lines =
   1.452 +    (* No dependencies: axiom or conjecture clause *)
   1.453 +    if is_axiom_clause_number thm_names num then
   1.454 +      (* Axioms are not proof lines. *)
   1.455 +      if is_only_type_information t then
   1.456 +        map (replace_deps_in_line (num, [])) lines
   1.457 +      (* Is there a repetition? If so, replace later line by earlier one. *)
   1.458 +      else case take_prefix (aint_inference t) lines of
   1.459 +        (_, []) => lines (*no repetition of proof line*)
   1.460 +      | (pre, Inference (num', _, _) :: post) =>
   1.461 +        pre @ map (replace_deps_in_line (num', [num])) post
   1.462 +    else
   1.463 +      Inference (num, t, []) :: lines
   1.464 +  | add_line _ (Inference (num, t, deps)) lines =
   1.465 +    (* Type information will be deleted later; skip repetition test. *)
   1.466 +    if is_only_type_information t then
   1.467 +      Inference (num, t, deps) :: lines
   1.468 +    (* Is there a repetition? If so, replace later line by earlier one. *)
   1.469 +    else case take_prefix (aint_inference t) lines of
   1.470 +      (* FIXME: Doesn't this code risk conflating proofs involving different
   1.471 +         types?? *)
   1.472 +       (_, []) => Inference (num, t, deps) :: lines
   1.473 +     | (pre, Inference (num', t', _) :: post) =>
   1.474 +       Inference (num, t', deps) ::
   1.475 +       pre @ map (replace_deps_in_line (num', [num])) post
   1.476  
   1.477 -(*Recursively delete empty lines (type information) from the proof.*)
   1.478 -fun add_nonnull_line (num, t, []) lines = (*no dependencies, so a conjecture clause*)
   1.479 -    if eq_types t then
   1.480 -      (*must be type information, tfree_tcs, clsrel, clsarity: delete refs to it*)
   1.481 -      delete_dep num lines
   1.482 -    else
   1.483 -      (num, t, []) :: lines
   1.484 -  | add_nonnull_line (num, t, deps) lines = (num, t, deps) :: lines
   1.485 +(* Recursively delete empty lines (type information) from the proof. *)
   1.486 +fun add_nontrivial_line (Inference (num, t, [])) lines =
   1.487 +    if is_only_type_information t then delete_dep num lines
   1.488 +    else Inference (num, t, []) :: lines
   1.489 +  | add_nontrivial_line line lines = line :: lines
   1.490  and delete_dep num lines =
   1.491 -  fold_rev add_nonnull_line (map (replace_deps (num, [])) lines) []
   1.492 +  fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
   1.493 +
   1.494 +fun is_bad_free (Free (a, _)) = String.isPrefix skolem_prefix a
   1.495 +  | is_bad_free _ = false
   1.496  
   1.497 -fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a
   1.498 -  | bad_free _ = false;
   1.499 -
   1.500 -fun add_desired_line ctxt _ (num, t, []) (j, lines) =
   1.501 -    (j, (num, t, []) :: lines)  (* conjecture clauses must be kept *)
   1.502 -  | add_desired_line ctxt shrink_factor (num, t, deps) (j, lines) =
   1.503 +fun add_desired_line _ _ (line as Definition _) (j, lines) = (j, line :: lines)
   1.504 +  | add_desired_line ctxt _ (Inference (num, t, [])) (j, lines) =
   1.505 +    (j, Inference (num, t, []) :: lines)  (* conjecture clauses must be kept *)
   1.506 +  | add_desired_line ctxt shrink_factor (Inference (num, t, deps)) (j, lines) =
   1.507      (j + 1,
   1.508 -     if eq_types t orelse not (null (Term.add_tvars t [])) orelse
   1.509 -        exists_subterm bad_free t orelse
   1.510 +     if is_only_type_information t orelse
   1.511 +        not (null (Term.add_tvars t [])) orelse
   1.512 +        exists_subterm is_bad_free t orelse
   1.513          (length deps < 2 orelse j mod shrink_factor <> 0) then
   1.514 -       map (replace_deps (num, deps)) lines  (* delete line *)
   1.515 +       map (replace_deps_in_line (num, deps)) lines  (* delete line *)
   1.516       else
   1.517 -       (num, t, deps) :: lines)
   1.518 +       Inference (num, t, deps) :: lines)
   1.519  
   1.520  (** EXTRACTING LEMMAS **)
   1.521  
   1.522 @@ -465,20 +527,22 @@
   1.523      val n = Logic.count_prems (prop_of goal)
   1.524    in (metis_line i n lemmas ^ minimize_line minimize_command lemmas, lemmas) end
   1.525  
   1.526 -val is_valid_line = String.isPrefix "cnf(" orf String.isSubstring "||"
   1.527 +val is_valid_line =
   1.528 +  String.isPrefix "fof(" orf String.isPrefix "cnf(" orf String.isSubstring "||"
   1.529  
   1.530 -(** NEW PROOF RECONSTRUCTION CODE **)
   1.531 +(** Isar proof construction and manipulation **)
   1.532 +
   1.533 +fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
   1.534 +  (union (op =) ls1 ls2, union (op =) ss1 ss2)
   1.535  
   1.536  type label = string * int
   1.537  type facts = label list * string list
   1.538  
   1.539 -fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
   1.540 -  (union (op =) ls1 ls2, union (op =) ss1 ss2)
   1.541 -
   1.542  datatype qualifier = Show | Then | Moreover | Ultimately
   1.543  
   1.544  datatype step =
   1.545    Fix of (string * typ) list |
   1.546 +  Let of term * term |
   1.547    Assume of label * term |
   1.548    Have of qualifier list * label * term * byline
   1.549  and byline =
   1.550 @@ -495,11 +559,12 @@
   1.551    else
   1.552      apfst (insert (op =) (raw_prefix, num))
   1.553  
   1.554 -fun generalize_all_vars t = fold_rev Logic.all (map Var (Term.add_vars t [])) t
   1.555 -fun step_for_tuple _ _ (label, t, []) = Assume ((raw_prefix, label), t)
   1.556 -  | step_for_tuple thm_names j (label, t, deps) =
   1.557 -    Have (if j = 1 then [Show] else [], (raw_prefix, label),
   1.558 -          generalize_all_vars (HOLogic.mk_Trueprop t),
   1.559 +fun quantify_over_all_vars t = fold_rev Logic.all (map Var ((*Term.add_vars t###*) [])) t
   1.560 +fun step_for_line _ _ (Definition (num, t1, t2)) = Let (t1, t2)
   1.561 +  | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
   1.562 +  | step_for_line thm_names j (Inference (num, t, deps)) =
   1.563 +    Have (if j = 1 then [Show] else [], (raw_prefix, num),
   1.564 +          quantify_over_all_vars (HOLogic.mk_Trueprop t),
   1.565            Facts (fold (add_fact_from_dep thm_names) deps ([], [])))
   1.566  
   1.567  fun strip_spaces_in_list [] = ""
   1.568 @@ -521,18 +586,18 @@
   1.569  
   1.570  fun proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names frees =
   1.571    let
   1.572 -    val tuples =
   1.573 -      atp_proof |> split_lines |> map strip_spaces
   1.574 -                |> filter is_valid_line
   1.575 -                |> map (parse_line pool o explode)
   1.576 -                |> decode_lines ctxt
   1.577 -    val tuples = fold_rev (add_line thm_names) tuples []
   1.578 -    val tuples = fold_rev add_nonnull_line tuples []
   1.579 -    val tuples = fold_rev (add_desired_line ctxt shrink_factor) tuples (0, [])
   1.580 -                 |> snd
   1.581 +    val lines =
   1.582 +      atp_proof
   1.583 +      |> split_lines |> map strip_spaces |> filter is_valid_line
   1.584 +      |> map (parse_line pool o explode)
   1.585 +      |> decode_lines ctxt
   1.586 +      |> rpair [] |-> fold_rev (add_line thm_names)
   1.587 +      |> rpair [] |-> fold_rev add_nontrivial_line
   1.588 +      |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor)
   1.589 +      |> snd
   1.590    in
   1.591      (if null frees then [] else [Fix frees]) @
   1.592 -    map2 (step_for_tuple thm_names) (length tuples downto 1) tuples
   1.593 +    map2 (step_for_line thm_names) (length lines downto 1) lines
   1.594    end
   1.595  
   1.596  val indent_size = 2
   1.597 @@ -555,6 +620,7 @@
   1.598  and using_of proof = fold (union (op =) o using_of_step) proof []
   1.599  
   1.600  fun new_labels_of_step (Fix _) = []
   1.601 +  | new_labels_of_step (Let _) = []
   1.602    | new_labels_of_step (Assume (l, _)) = [l]
   1.603    | new_labels_of_step (Have (_, l, _, _)) = [l]
   1.604  val new_labels_of = maps new_labels_of_step
   1.605 @@ -594,6 +660,8 @@
   1.606      fun first_pass ([], contra) = ([], contra)
   1.607        | first_pass ((ps as Fix _) :: proof, contra) =
   1.608          first_pass (proof, contra) |>> cons ps
   1.609 +      | first_pass ((ps as Let _) :: proof, contra) =
   1.610 +        first_pass (proof, contra) |>> cons ps
   1.611        | first_pass ((ps as Assume (l, t)) :: proof, contra) =
   1.612          if member (op =) concl_ls l then
   1.613            first_pass (proof, contra ||> cons ps)
   1.614 @@ -671,17 +739,15 @@
   1.615               end
   1.616             | _ => raise Fail "malformed proof")
   1.617         | second_pass _ _ = raise Fail "malformed proof"
   1.618 -    val (proof_bottom, _) =
   1.619 -      second_pass [Show] (contra_proof, [], ([], ([], [])))
   1.620 +    val proof_bottom =
   1.621 +      second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
   1.622    in proof_top @ proof_bottom end
   1.623  
   1.624  val kill_duplicate_assumptions_in_proof =
   1.625    let
   1.626      fun relabel_facts subst =
   1.627        apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
   1.628 -    fun do_step (ps as Fix _) (proof, subst, assums) =
   1.629 -        (ps :: proof, subst, assums)
   1.630 -      | do_step (ps as Assume (l, t)) (proof, subst, assums) =
   1.631 +    fun do_step (ps as Assume (l, t)) (proof, subst, assums) =
   1.632          (case AList.lookup (op aconv) assums t of
   1.633             SOME l' => (proof, (l', l) :: subst, assums)
   1.634           | NONE => (ps :: proof, subst, (t, l) :: assums))
   1.635 @@ -692,13 +758,13 @@
   1.636                 | CaseSplit (proofs, facts) =>
   1.637                   CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
   1.638           proof, subst, assums)
   1.639 +      | do_step ps (proof, subst, assums) = (ps :: proof, subst, assums)
   1.640      and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   1.641    in do_proof end
   1.642  
   1.643  val then_chain_proof =
   1.644    let
   1.645      fun aux _ [] = []
   1.646 -      | aux _ ((ps as Fix _) :: proof) = ps :: aux no_label proof
   1.647        | aux _ ((ps as Assume (l, _)) :: proof) = ps :: aux l proof
   1.648        | aux l' (Have (qs, l, t, by) :: proof) =
   1.649          (case by of
   1.650 @@ -711,20 +777,21 @@
   1.651           | CaseSplit (proofs, facts) =>
   1.652             Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
   1.653          aux l proof
   1.654 +      | aux _ (ps :: proof) = ps :: aux no_label proof
   1.655    in aux no_label end
   1.656  
   1.657  fun kill_useless_labels_in_proof proof =
   1.658    let
   1.659      val used_ls = using_of proof
   1.660      fun do_label l = if member (op =) used_ls l then l else no_label
   1.661 -    fun kill (Fix xs) = Fix xs
   1.662 -      | kill (Assume (l, t)) = Assume (do_label l, t)
   1.663 +    fun kill (Assume (l, t)) = Assume (do_label l, t)
   1.664        | kill (Have (qs, l, t, by)) =
   1.665          Have (qs, do_label l, t,
   1.666                case by of
   1.667                  CaseSplit (proofs, facts) =>
   1.668                  CaseSplit (map (map kill) proofs, facts)
   1.669                | _ => by)
   1.670 +      | kill ps = ps
   1.671    in map kill proof end
   1.672  
   1.673  fun prefix_for_depth n = replicate_string (n + 1)
   1.674 @@ -732,8 +799,6 @@
   1.675  val relabel_proof =
   1.676    let
   1.677      fun aux _ _ _ [] = []
   1.678 -      | aux subst depth nextp ((ps as Fix _) :: proof) =
   1.679 -        ps :: aux subst depth nextp proof
   1.680        | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
   1.681          if l = no_label then
   1.682            Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
   1.683 @@ -751,7 +816,7 @@
   1.684                let
   1.685                  val l' = (prefix_for_depth depth fact_prefix, next_fact)
   1.686                in (l', (l, l') :: subst, next_fact + 1) end
   1.687 -          val relabel_facts = apfst (map (the o AList.lookup (op =) subst))
   1.688 +          val relabel_facts = apfst (map_filter (AList.lookup (op =) subst))
   1.689            val by =
   1.690              case by of
   1.691                Facts facts => Facts (relabel_facts facts)
   1.692 @@ -762,6 +827,7 @@
   1.693            Have (qs, l', t, by) ::
   1.694            aux subst depth (next_assum, next_fact) proof
   1.695          end
   1.696 +      | aux subst depth nextp (ps :: proof) = ps :: aux subst depth nextp proof
   1.697    in aux [] 0 (1, 1) end
   1.698  
   1.699  fun string_for_proof ctxt sorts i n =
   1.700 @@ -785,12 +851,13 @@
   1.701      val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
   1.702      fun do_using [] = ""
   1.703        | do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " "
   1.704 -    fun do_by_facts [] [] = "by blast"
   1.705 -      | do_by_facts _ [] = "by metis"
   1.706 -      | do_by_facts _ ss = "by (metis " ^ space_implode " " ss ^ ")"
   1.707 -    fun do_facts (ls, ss) = do_using ls ^ do_by_facts ls ss
   1.708 +    fun do_by_facts [] = "by metis"
   1.709 +      | do_by_facts ss = "by (metis " ^ space_implode " " ss ^ ")"
   1.710 +    fun do_facts (ls, ss) = do_using ls ^ do_by_facts ss
   1.711      and do_step ind (Fix xs) =
   1.712          do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   1.713 +      | do_step ind (Let (t1, t2)) =
   1.714 +        do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
   1.715        | do_step ind (Assume (l, t)) =
   1.716          do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
   1.717        | do_step ind (Have (qs, l, t, Facts facts)) =
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Apr 27 18:58:05 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 28 12:46:50 2010 +0200
     2.3 @@ -14,6 +14,7 @@
     2.4    val timestamp : unit -> string
     2.5    val parse_bool_option : bool -> string -> string -> bool option
     2.6    val parse_time_option : string -> string -> Time.time option
     2.7 +  val nat_subscript : int -> string
     2.8    val unyxml : string -> string
     2.9    val maybe_quote : string -> string
    2.10  end;
    2.11 @@ -74,6 +75,9 @@
    2.12          SOME (Time.fromMilliseconds msecs)
    2.13      end
    2.14  
    2.15 +val subscript = implode o map (prefix "\<^isub>") o explode
    2.16 +val nat_subscript = subscript o string_of_int
    2.17 +
    2.18  fun plain_string_from_xml_tree t =
    2.19    Buffer.empty |> XML.add_content t |> Buffer.content
    2.20  val unyxml = plain_string_from_xml_tree o YXML.parse