author paulson Wed Jan 03 18:29:46 2007 +0100 (2007-01-03) changeset 21979 80e10f181c46 parent 21978 72c21698a055 child 21980 d22f7e3c5ad9
Improvements to proof reconstruction. Now "fixes" is inserted
```     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