src/HOL/Tools/res_reconstruct.ML
changeset 31037 ac8669134e7a
parent 30874 34927a1e0ae8
child 31038 887298ab70dc
     1.1 --- a/src/HOL/Tools/res_reconstruct.ML	Mon May 04 14:49:51 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Mon May 04 23:37:39 2009 +0200
     1.3 @@ -16,10 +16,10 @@
     1.4    val setup: Context.theory -> Context.theory
     1.5    (* extracting lemma list*)
     1.6    val find_failure: string -> string option
     1.7 -  val lemma_list_dfg: string * string vector * Proof.context * Thm.thm * int -> string
     1.8 -  val lemma_list_tstp: string * string vector * Proof.context * Thm.thm * int -> string
     1.9 +  val lemma_list_dfg: string -> string * string vector * Proof.context * Thm.thm * int -> string
    1.10 +  val lemma_list_tstp: string -> string * string vector * Proof.context * Thm.thm * int -> string
    1.11    (* structured proofs *)
    1.12 -  val structured_proof: string * string vector * Proof.context * Thm.thm * int -> string
    1.13 +  val structured_proof: string -> string * string vector * Proof.context * Thm.thm * int -> string
    1.14  end;
    1.15  
    1.16  structure ResReconstruct : RES_RECONSTRUCT =
    1.17 @@ -514,7 +514,7 @@
    1.18      in  List.mapPartial (inputno o toks) lines  end
    1.19      
    1.20    (*extracting lemmas from tstp-output between the lines from above*)                         
    1.21 -  fun extract_lemmas get_step_nums (proof, thm_names, _, _, _) = 
    1.22 +  fun extract_lemmas get_step_nums (proof, thm_names, _, _, _) =
    1.23      let
    1.24      (* get the names of axioms from their numbers*)
    1.25      fun get_axiom_names thm_names step_nums =
    1.26 @@ -532,24 +532,33 @@
    1.27      (* metis-command *)
    1.28      fun metis_line [] = "apply metis"
    1.29        | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
    1.30 +
    1.31 +    (* atp_minimize [atp=<prover>] <lemmas> *)
    1.32 +    fun minimize_line _ [] = ""
    1.33 +      | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
    1.34 +            (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^ space_implode " " lemmas)
    1.35      
    1.36      (*Used to label theorems chained into the sledgehammer call*)
    1.37      val chained_hint = "CHAINED";
    1.38      fun sendback_metis_nochained lemmas = 
    1.39        let val nochained = filter_out (fn y => y = chained_hint)
    1.40        in (Markup.markup Markup.sendback o metis_line) (nochained lemmas) end
    1.41 -    fun lemma_list_tstp result = sendback_metis_nochained (extract_lemmas get_step_nums_tstp result);
    1.42 -    fun lemma_list_dfg result = sendback_metis_nochained (extract_lemmas get_step_nums_dfg result);
    1.43 -           
    1.44 +    fun lemma_list_tstp name result =
    1.45 +      let val lemmas = extract_lemmas get_step_nums_tstp result
    1.46 +      in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end;
    1.47 +    fun lemma_list_dfg name result =
    1.48 +      let val lemmas = extract_lemmas get_step_nums_dfg result
    1.49 +      in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end;
    1.50 +
    1.51      (* === Extracting structured Isar-proof === *)
    1.52 -    fun structured_proof (result as (proof, thm_names, ctxt, goal, subgoalno)) = 
    1.53 +    fun structured_proof name (result as (proof, thm_names, ctxt, goal, subgoalno)) =
    1.54        let
    1.55        (*Could use split_lines, but it can return blank lines...*)
    1.56        val lines = String.tokens (equal #"\n");
    1.57        val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
    1.58        val proofextract = get_proof_extract proof
    1.59        val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
    1.60 -      val one_line_proof = lemma_list_tstp result
    1.61 +      val one_line_proof = lemma_list_tstp name result
    1.62        val structured = if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
    1.63                    else decode_tstp_file cnfs ctxt goal subgoalno thm_names
    1.64        in