Improvements to proof reconstruction. Now "fixes" is inserted
authorpaulson
Wed Jan 03 18:29:46 2007 +0100 (2007-01-03)
changeset 2197980e10f181c46
parent 21978 72c21698a055
child 21980 d22f7e3c5ad9
Improvements to proof reconstruction. Now "fixes" is inserted
src/HOL/Tools/res_reconstruct.ML
     1.1 --- a/src/HOL/Tools/res_reconstruct.ML	Wed Jan 03 11:06:52 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Wed Jan 03 18:29:46 2007 +0100
     1.3 @@ -1,10 +1,12 @@
     1.4  (*  ID:         $Id$
     1.5 -    Author:     Claire Quigley and L C Paulson
     1.6 +    Author:     L C Paulson and Claire Quigley
     1.7      Copyright   2004  University of Cambridge
     1.8  *)
     1.9  
    1.10 +(*FIXME: can we delete the "thm * int" and "th sgno" below?*)
    1.11 +
    1.12  (***************************************************************************)
    1.13 -(*  Code to deal with the transfer of proofs from a Vampire process          *)
    1.14 +(*  Code to deal with the transfer of proofs from a prover process         *)
    1.15  (***************************************************************************)
    1.16  signature RES_RECONSTRUCT =
    1.17    sig
    1.18 @@ -279,7 +281,7 @@
    1.19  (*Quantification over a list of Vars. FUXNE: for term.ML??*)
    1.20  fun list_all_var ([], t: term) = t
    1.21    | list_all_var ((v as Var(ix,T)) :: vars, t) =
    1.22 -        (all T) $ Abs(string_of_indexname ix, T, abstract_over (v,t));
    1.23 +      (all T) $ Abs(string_of_indexname ix, T, abstract_over (v, list_all_var (vars,t)));
    1.24  
    1.25  fun gen_all_vars t = list_all_var (term_vars t, t);
    1.26  
    1.27 @@ -367,7 +369,7 @@
    1.28    | stringify_deps thm_names deps_map ((lno, t, deps) :: lines) =
    1.29        if lno <= Vector.length thm_names  (*axiom*)
    1.30        then (Vector.sub(thm_names,lno-1), t, []) :: stringify_deps thm_names deps_map lines 
    1.31 -      else let val lname = "L" ^ Int.toString (length deps_map)
    1.32 +      else let val lname = Int.toString (length deps_map)
    1.33                 fun fix lno = if lno <= Vector.length thm_names  
    1.34                               then SOME(Vector.sub(thm_names,lno-1))
    1.35                               else AList.lookup op= deps_map lno;
    1.36 @@ -375,10 +377,23 @@
    1.37                 stringify_deps thm_names ((lno,lname)::deps_map) lines
    1.38             end;
    1.39  
    1.40 +val proofstart = "\nproof (rule ccontr, skolemize, make_clauses)\n";
    1.41 +
    1.42 +fun string_of_Free (Free (x,_)) = x
    1.43 +  | string_of_Free _ = "??string_of_Free??";
    1.44 +
    1.45 +fun isar_header [] = proofstart
    1.46 +  | isar_header ts = proofstart ^ "fix " ^ space_implode " " (map string_of_Free ts) ^ "\n";
    1.47 +
    1.48  fun decode_tstp_file ctxt (cnfs,thm_names) =
    1.49    let val tuples = map (dest_tstp o tstp_line o explode) cnfs
    1.50 -      val lines = foldr add_prfline [] (decode_tstp_list (ProofContext.theory_of ctxt) tuples)
    1.51 -  in  String.concat (isar_lines ctxt (stringify_deps thm_names [] lines))  end;
    1.52 +      val decoded_tuples = decode_tstp_list (ProofContext.theory_of ctxt) tuples
    1.53 +      val lines = foldr add_prfline [] decoded_tuples
    1.54 +      and fixes = foldr add_term_frees [] (map #3 decoded_tuples)
    1.55 +  in  
    1.56 +      isar_header fixes ^ 
    1.57 +      String.concat (isar_lines ctxt (stringify_deps thm_names [] lines))
    1.58 +  end;
    1.59  
    1.60  (*Could use split_lines, but it can return blank lines...*)
    1.61  val lines = String.tokens (equal #"\n");