introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
authorblanchet
Mon Apr 26 21:20:43 2010 +0200 (2010-04-26 ago)
changeset 364021b20805974c7
parent 36401 31252c4d4923
child 36403 9a4baad039c4
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
the code is still somewhat experimental but any exceptions it throws are catched, and Sledgehammer will still yield a one-line metis proof in case of proof reconstruction failure
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Apr 26 21:18:20 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Apr 26 21:20:43 2010 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  (* minimalization of thms *)
     1.5  
     1.6  fun minimize_theorems (params as {debug, atps, minimize_timeout, isar_proof,
     1.7 -                                  modulus, sorts, ...})
     1.8 +                                  shrink_factor, sorts, ...})
     1.9                        i state name_thms_pairs =
    1.10    let
    1.11      val thy = Proof.theory_of state
    1.12 @@ -92,8 +92,8 @@
    1.13    in
    1.14      (* try prove first to check result and get used theorems *)
    1.15      (case test_thms_fun NONE name_thms_pairs of
    1.16 -      result as {outcome = NONE, pool, internal_thm_names, filtered_clauses,
    1.17 -                 ...} =>
    1.18 +      result as {outcome = NONE, pool, internal_thm_names, conjecture_shape,
    1.19 +                 filtered_clauses, ...} =>
    1.20          let
    1.21            val used = internal_thm_names |> Vector.foldr (op ::) []
    1.22                                          |> sort_distinct string_ord
    1.23 @@ -110,7 +110,9 @@
    1.24              ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
    1.25          in
    1.26            (SOME min_thms,
    1.27 -           proof_text isar_proof pool debug modulus sorts ctxt
    1.28 +           proof_text isar_proof
    1.29 +                      (pool, debug, shrink_factor, sorts, ctxt,
    1.30 +                       conjecture_shape)
    1.31                        (K "", proof, internal_thm_names, goal, i) |> fst)
    1.32          end
    1.33      | {outcome = SOME TimedOut, ...} =>
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 26 21:18:20 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 26 21:20:43 2010 +0200
     2.3 @@ -38,10 +38,10 @@
     2.4         hol_clause list
     2.5    val write_tptp_file : bool -> bool -> bool -> Path.T ->
     2.6      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
     2.7 -    classrel_clause list * arity_clause list -> name_pool option
     2.8 +    classrel_clause list * arity_clause list -> name_pool option * int
     2.9    val write_dfg_file : bool -> bool -> Path.T ->
    2.10      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    2.11 -    classrel_clause list * arity_clause list -> name_pool option
    2.12 +    classrel_clause list * arity_clause list -> name_pool option * int
    2.13  end
    2.14  
    2.15  structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
    2.16 @@ -56,7 +56,7 @@
    2.17  
    2.18     If "explicit_apply" is false, each function will be directly applied to as
    2.19     many arguments as possible, avoiding use of the "apply" operator. Use of
    2.20 -   hBOOL is also minimized.
    2.21 +   "hBOOL" is also minimized.
    2.22  *)
    2.23  
    2.24  fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
    2.25 @@ -518,17 +518,19 @@
    2.26      val arity_clss = map tptp_arity_clause arity_clauses
    2.27      val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
    2.28                                         helper_clauses pool
    2.29 +    val conjecture_offset =
    2.30 +      length ax_clss + length classrel_clss + length arity_clss
    2.31 +      + length helper_clss
    2.32      val _ =
    2.33        File.write_list file
    2.34            (header () ::
    2.35             section "Relevant fact" ax_clss @
    2.36 +           section "Class relationship" classrel_clss @
    2.37 +           section "Arity declaration" arity_clss @
    2.38             section "Helper fact" helper_clss @
    2.39 -           section "Type variable" tfree_clss @
    2.40             section "Conjecture" conjecture_clss @
    2.41 -           section "Class relationship" classrel_clss @
    2.42 -           section "Arity declaration" arity_clss)
    2.43 -  in pool end
    2.44 -
    2.45 +           section "Type variable" tfree_clss)
    2.46 +  in (pool, conjecture_offset) end
    2.47  
    2.48  (* DFG format *)
    2.49  
    2.50 @@ -551,6 +553,9 @@
    2.51        pool_map (apfst fst oo dfg_clause params) helper_clauses pool
    2.52      val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
    2.53      and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
    2.54 +    val conjecture_offset =
    2.55 +      length axclauses + length classrel_clauses + length arity_clauses
    2.56 +      + length helper_clauses
    2.57      val _ =
    2.58        File.write_list file
    2.59            (header () ::
    2.60 @@ -564,10 +569,10 @@
    2.61             map dfg_arity_clause arity_clauses @
    2.62             helper_clauses_strs @
    2.63             ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
    2.64 +           conjecture_clss @
    2.65             tfree_clss @
    2.66 -           conjecture_clss @
    2.67             ["end_of_list.\n\n",
    2.68              "end_problem.\n"])
    2.69 -  in pool end
    2.70 +  in (pool, conjecture_offset) end
    2.71  
    2.72  end;
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Apr 26 21:18:20 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Apr 26 21:20:43 2010 +0200
     3.3 @@ -21,11 +21,11 @@
     3.4      minimize_command * string * string vector * thm * int
     3.5      -> string * string list
     3.6    val isar_proof_text:
     3.7 -    name_pool option -> bool -> int -> bool -> Proof.context
     3.8 +    name_pool option * bool * int * bool * Proof.context * int list list
     3.9      -> minimize_command * string * string vector * thm * int
    3.10      -> string * string list
    3.11    val proof_text:
    3.12 -    bool -> name_pool option -> bool -> int -> bool -> Proof.context
    3.13 +    bool -> name_pool option * bool * int * bool * Proof.context * int list list
    3.14      -> minimize_command * string * string vector * thm * int
    3.15      -> string * string list
    3.16  end;
    3.17 @@ -41,8 +41,7 @@
    3.18  fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
    3.19  fun is_head_digit s = Char.isDigit (String.sub (s, 0))
    3.20  
    3.21 -fun is_axiom_clause_number thm_names line_num =
    3.22 -  line_num <= Vector.length thm_names
    3.23 +fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
    3.24  
    3.25  fun ugly_name NONE s = s
    3.26    | ugly_name (SOME the_pool) s =
    3.27 @@ -50,12 +49,6 @@
    3.28        SOME s' => s'
    3.29      | NONE => s
    3.30  
    3.31 -val trace_path = Path.basic "sledgehammer_proof_trace"
    3.32 -fun trace_proof_msg f =
    3.33 -  if !trace then File.append (File.tmp_path trace_path) (f ()) else ();
    3.34 -
    3.35 -val string_of_thm = PrintMode.setmp [] o Display.string_of_thm
    3.36 -
    3.37  (**** PARSING OF TSTP FORMAT ****)
    3.38  
    3.39  (* Syntax trees, either term list or formulae *)
    3.40 @@ -110,7 +103,7 @@
    3.41  fun parse_literals pool =
    3.42    parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
    3.43  
    3.44 -(*Clause: a list of literals separated by the disjunction sign*)
    3.45 +(* Clause: a list of literals separated by the disjunction sign. *)
    3.46  fun parse_clause pool =
    3.47    $$ "(" |-- parse_literals pool --| $$ ")" || Scan.single (parse_literal pool)
    3.48  
    3.49 @@ -153,15 +146,14 @@
    3.50  
    3.51  (* Syntax: <name>[0:<inference><annotations>] ||
    3.52             <cnf_formulas> -> <cnf_formulas>. *)
    3.53 -fun retuple_spass_proof_line ((name, deps), ts) = (name, ts, deps)
    3.54 -fun parse_spass_proof_line pool =
    3.55 +fun retuple_spass_line ((name, deps), ts) = (name, ts, deps)
    3.56 +fun parse_spass_line pool =
    3.57    parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
    3.58    -- parse_spass_annotations --| $$ "]" --| $$ "|" --| $$ "|"
    3.59    -- parse_horn_clause pool --| $$ "."
    3.60 -  >> retuple_spass_proof_line
    3.61 +  >> retuple_spass_line
    3.62  
    3.63 -fun parse_proof_line pool = 
    3.64 -  fst o (parse_tstp_line pool || parse_spass_proof_line pool)
    3.65 +fun parse_line pool = fst o (parse_tstp_line pool || parse_spass_line pool)
    3.66  
    3.67  (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
    3.68  
    3.69 @@ -209,13 +201,10 @@
    3.70  
    3.71  (*Invert the table of translations between Isabelle and ATPs*)
    3.72  val const_trans_table_inv =
    3.73 -      Symtab.update ("fequal", "op =")
    3.74 -        (Symtab.make (map swap (Symtab.dest const_trans_table)));
    3.75 +  Symtab.update ("fequal", @{const_name "op ="})
    3.76 +                (Symtab.make (map swap (Symtab.dest const_trans_table)))
    3.77  
    3.78 -fun invert_const c =
    3.79 -    case Symtab.lookup const_trans_table_inv c of
    3.80 -        SOME c' => c'
    3.81 -      | NONE => c;
    3.82 +fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c
    3.83  
    3.84  (*The number of type arguments of a constant, zero if it's monomorphic*)
    3.85  fun num_typargs thy s = length (Sign.const_typargs thy (s, Sign.the_const_type thy s));
    3.86 @@ -272,21 +261,52 @@
    3.87    | add_constraint ((false, cl, TVar(ix,_)), vt) = addix (ix,cl) vt
    3.88    | add_constraint (_, vt) = vt;
    3.89  
    3.90 -(* Final treatment of the list of "real" literals from a clause. *)
    3.91 -fun finish [] =
    3.92 -    (* No "real" literals means only type information. *)
    3.93 -    HOLogic.true_const
    3.94 -  | finish lits =
    3.95 -    case filter_out (curry (op =) HOLogic.false_const) lits of
    3.96 -      [] => HOLogic.false_const
    3.97 -    | xs => foldr1 HOLogic.mk_disj (rev xs);
    3.98 +fun is_positive_literal (@{const Trueprop} $ t) = is_positive_literal t
    3.99 +  | is_positive_literal (@{const Not} $ _) = false
   3.100 +  | is_positive_literal t = true
   3.101 +
   3.102 +fun negate_term thy (@{const Trueprop} $ t) =
   3.103 +    @{const Trueprop} $ negate_term thy t
   3.104 +  | negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) =
   3.105 +    Const (@{const_name Ex}, T) $ Abs (s, T', negate_term thy t')
   3.106 +  | negate_term thy (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
   3.107 +    Const (@{const_name All}, T) $ Abs (s, T', negate_term thy t')
   3.108 +  | negate_term thy (@{const "op -->"} $ t1 $ t2) =
   3.109 +    @{const "op &"} $ t1 $ negate_term thy t2
   3.110 +  | negate_term thy (@{const "op &"} $ t1 $ t2) =
   3.111 +    @{const "op |"} $ negate_term thy t1 $ negate_term thy t2
   3.112 +  | negate_term thy (@{const "op |"} $ t1 $ t2) =
   3.113 +    @{const "op &"} $ negate_term thy t1 $ negate_term thy t2
   3.114 +  | negate_term thy (@{const Not} $ t) = t
   3.115 +  | negate_term thy t =
   3.116 +    if fastype_of t = @{typ prop} then
   3.117 +      HOLogic.mk_Trueprop (negate_term thy (Object_Logic.atomize_term thy t))
   3.118 +    else
   3.119 +      @{const Not} $ t
   3.120 +
   3.121 +fun clause_for_literals _ [] = HOLogic.false_const
   3.122 +  | clause_for_literals _ [lit] = lit
   3.123 +  | clause_for_literals thy lits =
   3.124 +    case List.partition is_positive_literal lits of
   3.125 +      (pos_lits as _ :: _, neg_lits as _ :: _) =>
   3.126 +      @{const "op -->"}
   3.127 +          $ foldr1 HOLogic.mk_conj (map (negate_term thy) neg_lits)
   3.128 +          $ foldr1 HOLogic.mk_disj pos_lits
   3.129 +    | _ => foldr1 HOLogic.mk_disj lits
   3.130 +
   3.131 +(* Final treatment of the list of "real" literals from a clause.
   3.132 +   No "real" literals means only type information. *)
   3.133 +fun finish_clause _ [] = HOLogic.true_const
   3.134 +  | finish_clause thy lits =
   3.135 +    lits |> filter_out (curry (op =) HOLogic.false_const) |> rev
   3.136 +         |> clause_for_literals thy
   3.137  
   3.138  (*Accumulate sort constraints in vt, with "real" literals in lits.*)
   3.139 -fun lits_of_strees _ (vt, lits) [] = (vt, finish lits)
   3.140 -  | lits_of_strees ctxt (vt, lits) (t::ts) =
   3.141 -      lits_of_strees ctxt (add_constraint (constraint_of_stree true t, vt), lits) ts
   3.142 -      handle STREE _ =>
   3.143 -      lits_of_strees ctxt (vt, term_of_stree [] (ProofContext.theory_of ctxt) t :: lits) ts;
   3.144 +fun lits_of_strees thy (vt, lits) [] = (vt, finish_clause thy lits)
   3.145 +  | lits_of_strees thy (vt, lits) (t :: ts) =
   3.146 +    lits_of_strees thy (add_constraint (constraint_of_stree true t, vt), lits)
   3.147 +                   ts
   3.148 +    handle STREE _ => lits_of_strees thy (vt, term_of_stree [] thy t :: lits) ts
   3.149  
   3.150  (*Update TVars/TFrees with detected sort constraints.*)
   3.151  fun repair_sorts vt =
   3.152 @@ -304,14 +324,14 @@
   3.153  (*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
   3.154    vt0 holds the initial sort constraints, from the conjecture clauses.*)
   3.155  fun clause_of_strees ctxt vt ts =
   3.156 -  let val (vt, dt) = lits_of_strees ctxt (vt, []) ts in
   3.157 +  let val (vt, dt) = lits_of_strees (ProofContext.theory_of ctxt) (vt, []) ts in
   3.158      dt |> repair_sorts vt |> TypeInfer.constrain HOLogic.boolT
   3.159         |> Syntax.check_term ctxt
   3.160    end
   3.161  
   3.162  fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t;
   3.163  
   3.164 -fun decode_proof_step vt0 (name, ts, deps) ctxt =
   3.165 +fun decode_line vt0 (name, ts, deps) ctxt =
   3.166    let val cl = clause_of_strees ctxt vt0 ts in
   3.167      ((name, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt)
   3.168    end
   3.169 @@ -331,102 +351,11 @@
   3.170  
   3.171  (**** Translation of TSTP files to Isar Proofs ****)
   3.172  
   3.173 -fun decode_proof_steps ctxt tuples =
   3.174 +fun decode_lines ctxt tuples =
   3.175    let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #2 tuples) in
   3.176 -    #1 (fold_map (decode_proof_step vt0) tuples ctxt)
   3.177 +    #1 (fold_map (decode_line vt0) tuples ctxt)
   3.178    end
   3.179  
   3.180 -(** Finding a matching assumption. The literals may be permuted, and variable names
   3.181 -    may disagree. We must try all combinations of literals (quadratic!) and
   3.182 -    match the variable names consistently. **)
   3.183 -
   3.184 -fun strip_alls_aux n (Const(@{const_name all}, _)$Abs(a,T,t))  =
   3.185 -      strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t))
   3.186 -  | strip_alls_aux _ t  =  t;
   3.187 -
   3.188 -val strip_alls = strip_alls_aux 0;
   3.189 -
   3.190 -exception MATCH_LITERAL of unit
   3.191 -
   3.192 -(* Remark 1: Ignore types. They are not to be trusted.
   3.193 -   Remark 2: Ignore order of arguments for equality. SPASS sometimes swaps
   3.194 -   them for no apparent reason. *)
   3.195 -fun match_literal (Const (@{const_name "op ="}, _) $ t1 $ u1)
   3.196 -                  (Const (@{const_name "op ="}, _) $ t2 $ u2) env =
   3.197 -    (env |> match_literal t1 t2 |> match_literal u1 u2
   3.198 -     handle MATCH_LITERAL () =>
   3.199 -            env |> match_literal t1 u2 |> match_literal u1 t2)
   3.200 -  | match_literal (t1 $ u1) (t2 $ u2) env =
   3.201 -    env |> match_literal t1 t2 |> match_literal u1 u2
   3.202 -  | match_literal (Abs (_,_,t1)) (Abs (_,_,t2)) env =
   3.203 -    match_literal t1 t2 env
   3.204 -  | match_literal (Bound i1) (Bound i2) env =
   3.205 -    if i1=i2 then env else raise MATCH_LITERAL ()
   3.206 -  | match_literal (Const(a1,_)) (Const(a2,_)) env =
   3.207 -    if a1=a2 then env else raise MATCH_LITERAL ()
   3.208 -  | match_literal (Free(a1,_)) (Free(a2,_)) env =
   3.209 -    if a1=a2 then env else raise MATCH_LITERAL ()
   3.210 -  | match_literal (Var(ix1,_)) (Var(ix2,_)) env = insert (op =) (ix1,ix2) env
   3.211 -  | match_literal _ _ _ = raise MATCH_LITERAL ()
   3.212 -
   3.213 -(* Checking that all variable associations are unique. The list "env" contains
   3.214 -   no repetitions, but does it contain say (x, y) and (y, y)? *)
   3.215 -fun good env =
   3.216 -  let val (xs,ys) = ListPair.unzip env
   3.217 -  in  not (has_duplicates (op=) xs orelse has_duplicates (op=) ys)  end;
   3.218 -
   3.219 -(*Match one list of literals against another, ignoring types and the order of
   3.220 -  literals. Sorting is unreliable because we don't have types or variable names.*)
   3.221 -fun matches_aux _ [] [] = true
   3.222 -  | matches_aux env (lit::lits) ts =
   3.223 -      let fun match1 us [] = false
   3.224 -            | match1 us (t::ts) =
   3.225 -                let val env' = match_literal lit t env
   3.226 -                in  (good env' andalso matches_aux env' lits (us@ts)) orelse
   3.227 -                    match1 (t::us) ts
   3.228 -                end
   3.229 -                handle MATCH_LITERAL () => match1 (t::us) ts
   3.230 -      in  match1 [] ts  end;
   3.231 -
   3.232 -(*Is this length test useful?*)
   3.233 -fun matches (lits1,lits2) =
   3.234 -  length lits1 = length lits2  andalso
   3.235 -  matches_aux [] (map Envir.eta_contract lits1) (map Envir.eta_contract lits2);
   3.236 -
   3.237 -fun permuted_clause t =
   3.238 -  let val lits = HOLogic.disjuncts t
   3.239 -      fun perm [] = NONE
   3.240 -        | perm (ctm::ctms) =
   3.241 -            if matches (lits, HOLogic.disjuncts (HOLogic.dest_Trueprop (strip_alls ctm)))
   3.242 -            then SOME ctm else perm ctms
   3.243 -  in perm end;
   3.244 -
   3.245 -(*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
   3.246 -  ATP may have their literals reordered.*)
   3.247 -fun isar_proof_body ctxt sorts ctms =
   3.248 -  let
   3.249 -    val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n")
   3.250 -    val string_of_term = 
   3.251 -      PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   3.252 -                              (print_mode_value ()))
   3.253 -                      (Syntax.string_of_term ctxt)
   3.254 -    fun have_or_show "show" _ = "  show \""
   3.255 -      | have_or_show have label = "  " ^ have ^ " " ^ label ^ ": \""
   3.256 -    fun do_line _ (label, t, []) =
   3.257 -       (* No depedencies: it's a conjecture clause, with no proof. *)
   3.258 -       (case permuted_clause t ctms of
   3.259 -          SOME u => "  assume " ^ label ^ ": \"" ^ string_of_term u ^ "\"\n"
   3.260 -        | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
   3.261 -                              [t]))
   3.262 -      | do_line have (label, t, deps) =
   3.263 -        have_or_show have label ^
   3.264 -        string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^
   3.265 -        "\"\n    by (metis " ^ space_implode " " deps ^ ")\n"
   3.266 -    fun do_lines [(label, t, deps)] = [do_line "show" (label, t, deps)]
   3.267 -      | do_lines ((label, t, deps) :: lines) =
   3.268 -        do_line "have" (label, t, deps) :: do_lines lines
   3.269 -  in setmp_CRITICAL show_sorts sorts do_lines end;
   3.270 -
   3.271  fun unequal t (_, t', _) = not (t aconv t');
   3.272  
   3.273  (*No "real" literals means only type information*)
   3.274 @@ -438,7 +367,7 @@
   3.275  
   3.276  (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
   3.277    only in type information.*)
   3.278 -fun add_proof_line thm_names (num, t, []) lines =
   3.279 +fun add_line thm_names (num, t, []) lines =
   3.280        (* No dependencies: axiom or conjecture clause *)
   3.281        if is_axiom_clause_number thm_names num then
   3.282          (* Axioms are not proof lines *)
   3.283 @@ -452,7 +381,7 @@
   3.284                 pre @ map (replace_deps (num', [num])) post)
   3.285        else
   3.286          (num, t, []) :: lines
   3.287 -  | add_proof_line _ (num, t, deps) lines =
   3.288 +  | add_line _ (num, t, deps) lines =
   3.289        if eq_types t then (num, t, deps) :: lines
   3.290        (*Type information will be deleted later; skip repetition test.*)
   3.291        else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
   3.292 @@ -463,32 +392,30 @@
   3.293             (pre @ map (replace_deps (num', [num])) post);
   3.294  
   3.295  (*Recursively delete empty lines (type information) from the proof.*)
   3.296 -fun add_nonnull_prfline ((num, t, []), lines) = (*no dependencies, so a conjecture clause*)
   3.297 -     if eq_types t (*must be type information, tfree_tcs, clsrel, clsarity: delete refs to it*)
   3.298 -     then delete_dep num lines
   3.299 -     else (num, t, []) :: lines
   3.300 -  | add_nonnull_prfline ((num, t, deps), lines) = (num, t, deps) :: lines
   3.301 +fun add_nonnull_line (num, t, []) lines = (*no dependencies, so a conjecture clause*)
   3.302 +    if eq_types t then
   3.303 +      (*must be type information, tfree_tcs, clsrel, clsarity: delete refs to it*)
   3.304 +      delete_dep num lines
   3.305 +    else
   3.306 +      (num, t, []) :: lines
   3.307 +  | add_nonnull_line (num, t, deps) lines = (num, t, deps) :: lines
   3.308  and delete_dep num lines =
   3.309 -  List.foldr add_nonnull_prfline [] (map (replace_deps (num, [])) lines);
   3.310 +  fold_rev add_nonnull_line (map (replace_deps (num, [])) lines) []
   3.311  
   3.312  fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a
   3.313    | bad_free _ = false;
   3.314  
   3.315 -(*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies.
   3.316 -  To further compress proofs, setting modulus:=n deletes every nth line, and nlines
   3.317 -  counts the number of proof lines processed so far.
   3.318 -  Deleted lines are replaced by their own dependencies. Note that the "add_nonnull_prfline"
   3.319 -  phase may delete some dependencies, hence this phase comes later.*)
   3.320 -fun add_wanted_prfline ctxt _ ((num, t, []), (nlines, lines)) =
   3.321 -      (nlines, (num, t, []) :: lines)   (*conjecture clauses must be kept*)
   3.322 -  | add_wanted_prfline ctxt modulus ((num, t, deps), (nlines, lines)) =
   3.323 -      if eq_types t orelse not (null (Term.add_tvars t [])) orelse
   3.324 -         exists_subterm bad_free t orelse
   3.325 -         (not (null lines) andalso   (*final line can't be deleted for these reasons*)
   3.326 -          (length deps < 2 orelse nlines mod modulus <> 0))
   3.327 -      then (nlines+1, map (replace_deps (num, deps)) lines) (*Delete line*)
   3.328 -      else (nlines+1, (num, t, deps) :: lines);
   3.329 +fun add_desired_line ctxt (num, t, []) (j, lines) =
   3.330 +    (j, (num, t, []) :: lines)  (* conjecture clauses must be kept *)
   3.331 +  | add_desired_line ctxt (num, t, deps) (j, lines) =
   3.332 +    (j + 1,
   3.333 +     if eq_types t orelse not (null (Term.add_tvars t [])) orelse
   3.334 +        exists_subterm bad_free t orelse length deps < 2 then
   3.335 +       map (replace_deps (num, deps)) lines  (* delete line *)
   3.336 +     else
   3.337 +       (num, t, deps) :: lines)
   3.338  
   3.339 +(* ### *)
   3.340  (*Replace numeric proof lines by strings, either from thm_names or sequential line numbers*)
   3.341  fun stringify_deps thm_names deps_map [] = []
   3.342    | stringify_deps thm_names deps_map ((num, t, deps) :: lines) =
   3.343 @@ -508,61 +435,22 @@
   3.344          stringify_deps thm_names ((num, label) :: deps_map) lines
   3.345        end
   3.346  
   3.347 -fun isar_proof_start i =
   3.348 -  (if i = 1 then "" else "prefer " ^ string_of_int i ^ "\n") ^
   3.349 -  "proof (neg_clausify)\n";
   3.350 -fun isar_fixes [] = ""
   3.351 -  | isar_fixes ts = "  fix " ^ space_implode " " ts ^ "\n";
   3.352 -fun isar_proof_end 1 = "qed"
   3.353 -  | isar_proof_end _ = "next"
   3.354 +(** EXTRACTING LEMMAS **)
   3.355  
   3.356 -fun isar_proof_from_atp_proof pool modulus sorts ctxt cnfs thm_names goal i =
   3.357 -  let
   3.358 -    val _ = trace_proof_msg (K "\nisar_proof_from_atp_proof: start\n")
   3.359 -    val tuples = map (parse_proof_line pool o explode) cnfs
   3.360 -    val _ = trace_proof_msg (fn () =>
   3.361 -      Int.toString (length tuples) ^ " tuples extracted\n")
   3.362 -    val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
   3.363 -    val raw_lines =
   3.364 -      fold_rev (add_proof_line thm_names) (decode_proof_steps ctxt tuples) []
   3.365 -    val _ = trace_proof_msg (fn () =>
   3.366 -      Int.toString (length raw_lines) ^ " raw_lines extracted\n")
   3.367 -    val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
   3.368 -    val _ = trace_proof_msg (fn () =>
   3.369 -      Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
   3.370 -    val (_, lines) = List.foldr (add_wanted_prfline ctxt modulus) (0,[]) nonnull_lines
   3.371 -    val _ = trace_proof_msg (fn () =>
   3.372 -      Int.toString (length lines) ^ " lines extracted\n")
   3.373 -    val (ccls, fixes) = neg_conjecture_clauses ctxt goal i
   3.374 -    val _ = trace_proof_msg (fn () =>
   3.375 -      Int.toString (length ccls) ^ " conjecture clauses\n")
   3.376 -    val ccls = map forall_intr_vars ccls
   3.377 -    val _ = app (fn th => trace_proof_msg
   3.378 -                              (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
   3.379 -    val body = isar_proof_body ctxt sorts (map prop_of ccls)
   3.380 -                               (stringify_deps thm_names [] lines)
   3.381 -    val n = Logic.count_prems (prop_of goal)
   3.382 -    val _ = trace_proof_msg (K "\nisar_proof_from_atp_proof: finishing\n")
   3.383 -  in
   3.384 -    isar_proof_start i ^ isar_fixes (map #1 fixes) ^ implode body ^
   3.385 -    isar_proof_end n ^ "\n"
   3.386 -  end
   3.387 -  handle STREE _ => raise Fail "Cannot parse ATP output";
   3.388 -
   3.389 -
   3.390 -(* === EXTRACTING LEMMAS === *)
   3.391  (* A list consisting of the first number in each line is returned.
   3.392     TSTP: Interesting lines have the form "cnf(108, axiom, ...)", where the
   3.393     number (108) is extracted.
   3.394     SPASS: Lines have the form "108[0:Inp] ...", where the first number (108) is
   3.395     extracted. *)
   3.396 -fun extract_clause_numbers_in_proof proof =
   3.397 +fun extract_clause_numbers_in_atp_proof atp_proof =
   3.398    let
   3.399      val tokens_of = String.tokens (not o is_ident_char)
   3.400 -    fun extract_num ("cnf" :: num :: _ :: _) = Int.fromString num
   3.401 +    fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num
   3.402 +      | extract_num ("cnf" :: num :: "negated_conjecture" :: _) =
   3.403 +        Int.fromString num
   3.404        | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
   3.405        | extract_num _ = NONE
   3.406 -  in proof |> split_lines |> map_filter (extract_num o tokens_of) end
   3.407 +  in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
   3.408    
   3.409  (* Used to label theorems chained into the Sledgehammer call (or rather
   3.410     goal?) *)
   3.411 @@ -586,24 +474,59 @@
   3.412        "To minimize the number of lemmas, try this command: " ^
   3.413        Markup.markup Markup.sendback command ^ ".\n"
   3.414  
   3.415 -fun metis_proof_text (minimize_command, proof, thm_names, goal, i) =
   3.416 +fun metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) =
   3.417    let
   3.418      val lemmas =
   3.419 -      proof |> extract_clause_numbers_in_proof
   3.420 -            |> filter (is_axiom_clause_number thm_names)
   3.421 -            |> map (fn i => Vector.sub (thm_names, i - 1))
   3.422 -            |> filter_out (fn s => s = "??.unknown" orelse s = chained_hint)
   3.423 -            |> sort_distinct string_ord
   3.424 +      atp_proof |> extract_clause_numbers_in_atp_proof
   3.425 +                |> filter (is_axiom_clause_number thm_names)
   3.426 +                |> map (fn i => Vector.sub (thm_names, i - 1))
   3.427 +                |> filter_out (fn s => s = "??.unknown" orelse s = chained_hint)
   3.428 +                |> sort_distinct string_ord
   3.429      val n = Logic.count_prems (prop_of goal)
   3.430    in (metis_line i n lemmas ^ minimize_line minimize_command lemmas, lemmas) end
   3.431  
   3.432 -val is_proof_line = String.isPrefix "cnf(" orf String.isSubstring "||"
   3.433 +val is_valid_line = String.isPrefix "cnf(" orf String.isSubstring "||"
   3.434 +
   3.435 +(** NEW PROOF RECONSTRUCTION CODE **)
   3.436 +
   3.437 +type label = string * int
   3.438 +type facts = label list * string list
   3.439 +
   3.440 +fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
   3.441 +  (union (op =) ls1 ls2, union (op =) ss1 ss2)
   3.442 +
   3.443 +datatype qualifier = Show | Then | Moreover | Ultimately
   3.444  
   3.445 -fun do_space c = if Char.isSpace c then "" else str c
   3.446 +datatype step =
   3.447 +  Fix of term list |
   3.448 +  Assume of label * term |
   3.449 +  Have of qualifier list * label * term * byline
   3.450 +and byline =
   3.451 +  Facts of facts |
   3.452 +  CaseSplit of step list list * facts
   3.453 +
   3.454 +val raw_prefix = "X"
   3.455 +val assum_prefix = "A"
   3.456 +val fact_prefix = "F"
   3.457 +
   3.458 +(* ###
   3.459 +fun add_fact_from_dep s =
   3.460 +  case Int.fromString s of
   3.461 +    SOME n => apfst (cons (raw_prefix, n))
   3.462 +  | NONE => apsnd (cons s)
   3.463 +*)
   3.464 +
   3.465 +val add_fact_from_dep = apfst o cons o pair raw_prefix
   3.466 +
   3.467 +fun step_for_tuple _ (label, t, []) = Assume ((raw_prefix, label), t)
   3.468 +  | step_for_tuple j (label, t, deps) =
   3.469 +    Have (if j = 1 then [Show] else [], (raw_prefix, label), t,
   3.470 +          Facts (fold add_fact_from_dep deps ([], [])))
   3.471  
   3.472  fun strip_spaces_in_list [] = ""
   3.473 -  | strip_spaces_in_list [c1] = do_space c1
   3.474 -  | strip_spaces_in_list [c1, c2] = do_space c1 ^ do_space c2
   3.475 +  | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
   3.476 +  | strip_spaces_in_list [c1, c2] =
   3.477 +    strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
   3.478    | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
   3.479      if Char.isSpace c1 then
   3.480        strip_spaces_in_list (c2 :: c3 :: cs)
   3.481 @@ -611,39 +534,337 @@
   3.482        if Char.isSpace c3 then
   3.483          strip_spaces_in_list (c1 :: c3 :: cs)
   3.484        else
   3.485 -        str c1 ^
   3.486 -        (if is_ident_char c1 andalso is_ident_char c3 then " " else "") ^
   3.487 +        str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
   3.488          strip_spaces_in_list (c3 :: cs)
   3.489      else
   3.490        str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
   3.491 -
   3.492  val strip_spaces = strip_spaces_in_list o String.explode
   3.493  
   3.494 -fun isar_proof_text pool debug modulus sorts ctxt
   3.495 -                    (minimize_command, proof, thm_names, goal, i) =
   3.496 +fun proof_from_atp_proof pool ctxt atp_proof thm_names frees =
   3.497 +  let
   3.498 +    val tuples =
   3.499 +      atp_proof |> split_lines |> map strip_spaces
   3.500 +                |> filter is_valid_line
   3.501 +                |> map (parse_line pool o explode)
   3.502 +                |> decode_lines ctxt
   3.503 +    val tuples = fold_rev (add_line thm_names) tuples []
   3.504 +    val tuples = fold_rev add_nonnull_line tuples []
   3.505 +    val tuples = fold_rev (add_desired_line ctxt) tuples (0, []) |> snd
   3.506 +  in
   3.507 +    (if null frees then [] else [Fix frees]) @
   3.508 +    map2 step_for_tuple (length tuples downto 1) tuples
   3.509 +  end
   3.510 +
   3.511 +val indent_size = 2
   3.512 +val no_label = ("", ~1)
   3.513 +
   3.514 +fun no_show qs = not (member (op =) qs Show)
   3.515 +
   3.516 +(* When redirecting proofs, we keep information about the labels seen so far in
   3.517 +   the "backpatches" data structure. The first component indicates which facts
   3.518 +   should be associated with forthcoming proof steps. The second component is a
   3.519 +   pair ("keep_ls", "drop_ls"), where "keep_ls" are the labels to keep and
   3.520 +   "drop_ls" are those that should be dropped in a case split. *)
   3.521 +type backpatches = (label * facts) list * (label list * label list)
   3.522 +
   3.523 +fun using_of_step (Have (_, _, _, by)) =
   3.524 +    (case by of
   3.525 +       Facts (ls, _) => ls
   3.526 +     | CaseSplit (proofs, (ls, _)) => fold (union (op =) o using_of) proofs ls)
   3.527 +  | using_of_step _ = []
   3.528 +and using_of proof = fold (union (op =) o using_of_step) proof []
   3.529 +
   3.530 +fun new_labels_of_step (Fix _) = []
   3.531 +  | new_labels_of_step (Assume (l, _)) = [l]
   3.532 +  | new_labels_of_step (Have (_, l, _, _)) = [l]
   3.533 +val new_labels_of = maps new_labels_of_step
   3.534 +
   3.535 +val join_proofs =
   3.536 +  let
   3.537 +    fun aux _ [] = NONE
   3.538 +      | aux proof_tail (proofs as (proof1 :: _)) =
   3.539 +        if exists null proofs then
   3.540 +          NONE
   3.541 +        else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
   3.542 +          aux (hd proof1 :: proof_tail) (map tl proofs)
   3.543 +        else case hd proof1 of
   3.544 +          Have ([], l, t, by) =>
   3.545 +          if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
   3.546 +                      | _ => false) (tl proofs) andalso
   3.547 +             not (exists (member (op =) (maps new_labels_of proofs))
   3.548 +                         (using_of proof_tail)) then
   3.549 +            SOME (l, t, map rev proofs, proof_tail)
   3.550 +          else
   3.551 +            NONE
   3.552 +        | _ => NONE
   3.553 +  in aux [] o map rev end
   3.554 +
   3.555 +fun case_split_qualifiers proofs =
   3.556 +  case length proofs of
   3.557 +    0 => []
   3.558 +  | 1 => [Then]
   3.559 +  | _ => [Ultimately]
   3.560 +
   3.561 +val index_in_shape = find_index o exists o curry (op =)
   3.562 +
   3.563 +fun direct_proof thy conjecture_shape hyp_ts concl_t proof =
   3.564    let
   3.565 -    val cnfs = proof |> split_lines |> map strip_spaces |> filter is_proof_line
   3.566 +    val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
   3.567 +    fun find_hyp (_, j) = nth hyp_ts (index_in_shape j conjecture_shape)
   3.568 +    fun first_pass ([], contra) = ([], contra)
   3.569 +      | first_pass ((ps as Fix _) :: proof, contra) =
   3.570 +        first_pass (proof, contra) |>> cons ps
   3.571 +      | first_pass ((ps as Assume (l, t)) :: proof, contra) =
   3.572 +        if member (op =) concl_ls l then
   3.573 +          first_pass (proof, contra ||> cons ps)
   3.574 +        else
   3.575 +          first_pass (proof, contra) |>> cons (Assume (l, find_hyp l))
   3.576 +      | first_pass ((ps as Have (qs, l, t, Facts (ls, ss))) :: proof, contra) =
   3.577 +        if exists (member (op =) (fst contra)) ls then
   3.578 +          first_pass (proof, contra |>> cons l ||> cons ps)
   3.579 +        else
   3.580 +          first_pass (proof, contra) |>> cons ps
   3.581 +      | first_pass _ = raise Fail "malformed proof"
   3.582 +    val (proof_top, (contra_ls, contra_proof)) =
   3.583 +      first_pass (proof, (concl_ls, []))
   3.584 +    val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
   3.585 +    fun backpatch_labels patches ls =
   3.586 +      fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
   3.587 +    fun second_pass end_qs ([], assums, patches) =
   3.588 +        ([Have (end_qs, no_label,
   3.589 +                if length assums < length concl_ls then
   3.590 +                  clause_for_literals thy (map (negate_term thy o fst) assums)
   3.591 +                else
   3.592 +                  concl_t,
   3.593 +                Facts (backpatch_labels patches (map snd assums)))], patches)
   3.594 +      | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
   3.595 +        second_pass end_qs (proof, (t, l) :: assums, patches)
   3.596 +      | second_pass end_qs (Have (qs, l, t, Facts (ls, ss)) :: proof, assums,
   3.597 +                            patches) =
   3.598 +        if member (op =) (snd (snd patches)) l andalso
   3.599 +           not (AList.defined (op =) (fst patches) l) then
   3.600 +          second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
   3.601 +        else
   3.602 +          (case List.partition (member (op =) contra_ls) ls of
   3.603 +             ([contra_l], co_ls) =>
   3.604 +             if no_show qs then
   3.605 +               second_pass end_qs
   3.606 +                           (proof, assums,
   3.607 +                            patches |>> cons (contra_l, (l :: co_ls, ss)))
   3.608 +               |>> cons (if member (op =) (fst (snd patches)) l then
   3.609 +                           Assume (l, negate_term thy t)
   3.610 +                         else
   3.611 +                           Have (qs, l, negate_term thy t,
   3.612 +                                 Facts (backpatch_label patches l)))
   3.613 +             else
   3.614 +               second_pass end_qs (proof, assums,
   3.615 +                                   patches |>> cons (contra_l, (co_ls, ss)))
   3.616 +           | (contra_ls as _ :: _, co_ls) =>
   3.617 +             let
   3.618 +               val proofs =
   3.619 +                 map_filter
   3.620 +                     (fn l =>
   3.621 +                         if member (op =) concl_ls l then
   3.622 +                           NONE
   3.623 +                         else
   3.624 +                           let
   3.625 +                             val drop_ls = filter (curry (op <>) l) contra_ls
   3.626 +                           in
   3.627 +                             second_pass []
   3.628 +                                 (proof, assums,
   3.629 +                                  patches ||> apfst (insert (op =) l)
   3.630 +                                          ||> apsnd (union (op =) drop_ls))
   3.631 +                             |> fst |> SOME
   3.632 +                           end) contra_ls
   3.633 +               val facts = (co_ls, [])
   3.634 +             in
   3.635 +               (case join_proofs proofs of
   3.636 +                  SOME (l, t, proofs, proof_tail) =>
   3.637 +                  Have (case_split_qualifiers proofs @
   3.638 +                        (if null proof_tail then end_qs else []), l, t,
   3.639 +                        CaseSplit (proofs, facts)) :: proof_tail
   3.640 +                | NONE =>
   3.641 +                  [Have (case_split_qualifiers proofs @ end_qs, no_label,
   3.642 +                         concl_t, CaseSplit (proofs, facts))],
   3.643 +                patches)
   3.644 +             end
   3.645 +           | _ => raise Fail "malformed proof")
   3.646 +       | second_pass _ _ = raise Fail "malformed proof"
   3.647 +    val (proof_bottom, _) =
   3.648 +      second_pass [Show] (contra_proof, [], ([], ([], [])))
   3.649 +  in proof_top @ proof_bottom end
   3.650 +
   3.651 +val kill_duplicate_assumptions_in_proof =
   3.652 +  let
   3.653 +    fun relabel_facts subst =
   3.654 +      apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
   3.655 +    fun do_step (ps as Fix _) (proof, subst, assums) =
   3.656 +        (ps :: proof, subst, assums)
   3.657 +      | do_step (ps as Assume (l, t)) (proof, subst, assums) =
   3.658 +        (case AList.lookup (op aconv) assums t of
   3.659 +           SOME l' => (proof, (l', l) :: subst, assums)
   3.660 +         | NONE => (ps :: proof, subst, (t, l) :: assums))
   3.661 +      | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
   3.662 +        (Have (qs, l, t,
   3.663 +               case by of
   3.664 +                 Facts facts => Facts (relabel_facts subst facts)
   3.665 +               | CaseSplit (proofs, facts) =>
   3.666 +                 CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
   3.667 +         proof, subst, assums)
   3.668 +    and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   3.669 +  in do_proof end
   3.670 +
   3.671 +(* FIXME: implement *)
   3.672 +fun shrink_proof shrink_factor proof = proof
   3.673 +
   3.674 +val then_chain_proof =
   3.675 +  let
   3.676 +    fun aux _ [] = []
   3.677 +      | aux _ ((ps as Fix _) :: proof) = ps :: aux no_label proof
   3.678 +      | aux _ ((ps as Assume (l, _)) :: proof) = ps :: aux l proof
   3.679 +      | aux l' (Have (qs, l, t, by) :: proof) =
   3.680 +        (case by of
   3.681 +           Facts (ls, ss) =>
   3.682 +           Have (if member (op =) ls l' then
   3.683 +                   (Then :: qs, l, t,
   3.684 +                    Facts (filter_out (curry (op =) l') ls, ss))
   3.685 +                 else
   3.686 +                   (qs, l, t, Facts (ls, ss)))
   3.687 +         | CaseSplit (proofs, facts) =>
   3.688 +           Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
   3.689 +        aux l proof
   3.690 +  in aux no_label end
   3.691 +
   3.692 +fun kill_useless_labels_in_proof proof =
   3.693 +  let
   3.694 +    val used_ls = using_of proof
   3.695 +    fun do_label l = if member (op =) used_ls l then l else no_label
   3.696 +    fun kill (Fix ts) = Fix ts
   3.697 +      | kill (Assume (l, t)) = Assume (do_label l, t)
   3.698 +      | kill (Have (qs, l, t, by)) =
   3.699 +        Have (qs, do_label l, t,
   3.700 +              case by of
   3.701 +                CaseSplit (proofs, facts) =>
   3.702 +                CaseSplit (map (map kill) proofs, facts)
   3.703 +              | _ => by)
   3.704 +  in map kill proof end
   3.705 +
   3.706 +fun prefix_for_depth n = replicate_string (n + 1)
   3.707 +
   3.708 +val relabel_proof =
   3.709 +  let
   3.710 +    fun aux _ _ _ [] = []
   3.711 +      | aux subst depth nextp ((ps as Fix _) :: proof) =
   3.712 +        ps :: aux subst depth nextp proof
   3.713 +      | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
   3.714 +        if l = no_label then
   3.715 +          Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
   3.716 +        else
   3.717 +          let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
   3.718 +            Assume (l', t) ::
   3.719 +            aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
   3.720 +          end
   3.721 +      | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
   3.722 +        let
   3.723 +          val (l', subst, next_fact) =
   3.724 +            if l = no_label then
   3.725 +              (l, subst, next_fact)
   3.726 +            else
   3.727 +              let
   3.728 +                val l' = (prefix_for_depth depth fact_prefix, next_fact)
   3.729 +              in (l', (l, l') :: subst, next_fact + 1) end
   3.730 +          val relabel_facts = apfst (map (the o AList.lookup (op =) subst))
   3.731 +          val by =
   3.732 +            case by of
   3.733 +              Facts facts => Facts (relabel_facts facts)
   3.734 +            | CaseSplit (proofs, facts) =>
   3.735 +              CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
   3.736 +                         relabel_facts facts)
   3.737 +        in
   3.738 +          Have (qs, l', t, by) ::
   3.739 +          aux subst depth (next_assum, next_fact) proof
   3.740 +        end
   3.741 +  in aux [] 0 (1, 1) end
   3.742 +
   3.743 +fun string_for_proof ctxt sorts i n =
   3.744 +  let
   3.745 +    fun do_indent ind = replicate_string (ind * indent_size) " "
   3.746 +    fun do_raw_label (s, j) = s ^ string_of_int j
   3.747 +    fun do_label l = if l = no_label then "" else do_raw_label l ^ ": "
   3.748 +    fun do_have qs =
   3.749 +      (if member (op =) qs Moreover then "moreover " else "") ^
   3.750 +      (if member (op =) qs Ultimately then "ultimately " else "") ^
   3.751 +      (if member (op =) qs Then then
   3.752 +         if member (op =) qs Show then "thus" else "hence"
   3.753 +       else
   3.754 +         if member (op =) qs Show then "show" else "have")
   3.755 +    val do_term =
   3.756 +      Nitpick_Util.maybe_quote
   3.757 +      o PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   3.758 +                                (print_mode_value ()))
   3.759 +                        (Syntax.string_of_term ctxt)
   3.760 +    fun do_using [] = ""
   3.761 +      | do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " "
   3.762 +    fun do_by_facts [] [] = "by blast"
   3.763 +      | do_by_facts _ [] = "by metis"
   3.764 +      | do_by_facts _ ss = "by (metis " ^ space_implode " " ss ^ ")"
   3.765 +    fun do_facts ind (ls, ss) =
   3.766 +      do_indent (ind + 1) ^ do_using ls ^ do_by_facts ls ss
   3.767 +    and do_step ind (Fix ts) =
   3.768 +        do_indent ind ^ "fix " ^ space_implode " and " (map do_term ts) ^ "\n"
   3.769 +      | do_step ind (Assume (l, t)) =
   3.770 +        do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
   3.771 +      | do_step ind (Have (qs, l, t, Facts facts)) =
   3.772 +        do_indent ind ^ do_have qs ^ " " ^
   3.773 +        do_label l ^ do_term t ^ "\n" ^ do_facts ind facts ^ "\n"
   3.774 +      | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
   3.775 +        space_implode (do_indent ind ^ "moreover\n")
   3.776 +                      (map (do_block ind) proofs) ^
   3.777 +        do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ "\n" ^
   3.778 +        do_facts ind facts ^ "\n"
   3.779 +    and do_steps prefix suffix ind steps =
   3.780 +      let val s = implode (map (do_step ind) steps) in
   3.781 +        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   3.782 +        String.extract (s, ind * indent_size,
   3.783 +                        SOME (size s - ind * indent_size - 1)) ^
   3.784 +        suffix ^ "\n"
   3.785 +      end
   3.786 +    and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
   3.787 +    and do_proof proof =
   3.788 +      (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   3.789 +      do_indent 0 ^ "proof -\n" ^
   3.790 +      do_steps "" "" 1 proof ^
   3.791 +      do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
   3.792 +  in setmp_CRITICAL show_sorts sorts do_proof end
   3.793 +
   3.794 +fun isar_proof_text (pool, debug, shrink_factor, sorts, ctxt, conjecture_shape)
   3.795 +                    (minimize_command, atp_proof, thm_names, goal, i) =
   3.796 +  let
   3.797 +    val thy = ProofContext.theory_of ctxt
   3.798 +    val (frees, hyp_ts, concl_t) = strip_subgoal goal i
   3.799 +    val n = Logic.count_prems (prop_of goal)
   3.800      val (one_line_proof, lemma_names) =
   3.801 -      metis_proof_text (minimize_command, proof, thm_names, goal, i)
   3.802 -    val tokens = String.tokens (fn c => c = #" ") one_line_proof
   3.803 +      metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
   3.804      fun isar_proof_for () =
   3.805 -      case isar_proof_from_atp_proof pool modulus sorts ctxt cnfs thm_names goal
   3.806 -                                     i of
   3.807 +      case proof_from_atp_proof pool ctxt atp_proof thm_names frees
   3.808 +           |> direct_proof thy conjecture_shape hyp_ts concl_t
   3.809 +           |> kill_duplicate_assumptions_in_proof
   3.810 +           |> shrink_proof shrink_factor
   3.811 +           |> then_chain_proof
   3.812 +           |> kill_useless_labels_in_proof
   3.813 +           |> relabel_proof
   3.814 +           |> string_for_proof ctxt sorts i n of
   3.815          "" => ""
   3.816 -      | isar_proof =>
   3.817 -        "\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof
   3.818 +      | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
   3.819      val isar_proof =
   3.820 -      if member (op =) tokens chained_hint then
   3.821 -        ""
   3.822 -      else if debug then
   3.823 +      if debug then
   3.824          isar_proof_for ()
   3.825        else
   3.826          try isar_proof_for ()
   3.827          |> the_default "Warning: The Isar proof construction failed.\n"
   3.828    in (one_line_proof ^ isar_proof, lemma_names) end
   3.829  
   3.830 -fun proof_text isar_proof pool debug modulus sorts ctxt =
   3.831 -  if isar_proof then isar_proof_text pool debug modulus sorts ctxt
   3.832 -  else metis_proof_text
   3.833 +fun proof_text isar_proof =
   3.834 +  if isar_proof then isar_proof_text else K metis_proof_text
   3.835  
   3.836  end;
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Apr 26 21:18:20 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Apr 26 21:20:43 2010 +0200
     4.3 @@ -38,7 +38,6 @@
     4.4          else
     4.5            aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
     4.6    in aux [] end
     4.7 -
     4.8  fun remove_all bef = replace_all bef ""
     4.9  
    4.10  val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now