author blanchet Thu, 22 Apr 2010 10:54:56 +0200 changeset 36285 d868b34d604c parent 36284 0e24322474a4 child 36286 fa6d03d42aab
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes; this solves the unification exception that consistently was thrown for Cezary's "FSet3" theory
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 22 10:13:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 22 10:54:56 2010 +0200
@@ -115,7 +115,8 @@
SOME c' => c'
| NONE => c;

-fun make_tvar b = TVar(("'" ^ b, 0), HOLogic.typeS);
+fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS);
+fun make_tparam s = TypeInfer.param 0 (s, HOLogic.typeS)
fun make_var (b,T) = Var((b,0),T);

(*Type variables are given the basic sort, HOL.type. Some will later be constrained
@@ -136,7 +137,7 @@
| NONE =>
case strip_prefix tvar_prefix a of
SOME b => make_tvar b
-                  | NONE => make_tvar a   (*Variable from the ATP, say X1*)
+                  | NONE => make_tparam a  (* Variable from the ATP, say "X1" *)
end;

(*Invert the table of translations between Isabelle and ATPs*)
@@ -230,14 +231,14 @@
| tmsubst (t as Bound _) = t
| tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t)
| tmsubst (t \$ u) = tmsubst t \$ tmsubst u;
-  in fn t => if Vartab.is_empty vt then t else tmsubst t end;
+  in not (Vartab.is_empty vt) ? tmsubst end;

(*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
vt0 holds the initial sort constraints, from the conjecture clauses.*)
fun clause_of_strees ctxt vt0 ts =
let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in
singleton (Syntax.check_terms ctxt) (TypeInfer.constrain HOLogic.boolT (fix_sorts vt dt))
-  end;
+  end

fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t;

@@ -346,7 +347,7 @@
fun have_or_show "show" _ = "  show \""
| have_or_show have lname = "  " ^ have ^ " " ^ lname ^ ": \""
fun do_line _ (lname, t, []) =
-       (* No deps: it's a conjecture clause, with no proof. *)
+       (* No depedencies: it's a conjecture clause, with no proof. *)
(case permuted_clause t ctms of
SOME u => "  assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
| NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
@@ -570,7 +571,8 @@
fun isar_proof_for () =
case isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names of
"" => ""
-      | isar_proof => Markup.markup Markup.sendback isar_proof
+      | isar_proof =>
+        "\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof
val isar_proof =
if member (op =) tokens chained_hint then
""```