--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 17 16:47:19 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 17 17:01:31 2010 +0200
@@ -63,12 +63,12 @@
| string_for_connective AIff = "<=>"
| string_for_connective ANotIff = "<~>"
fun string_for_formula (AQuant (q, xs, phi)) =
- string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
- string_for_formula phi
+ "(" ^ string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
+ string_for_formula phi ^ ")"
| string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
space_implode " != " (map string_for_term ts)
| string_for_formula (AConn (c, [phi])) =
- string_for_connective c ^ " " ^ string_for_formula phi
+ "(" ^ string_for_connective c ^ " " ^ string_for_formula phi ^ ")"
| string_for_formula (AConn (c, phis)) =
"(" ^ space_implode (" " ^ string_for_connective c ^ " ")
(map string_for_formula phis) ^ ")"
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 16:47:19 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 17:01:31 2010 +0200
@@ -185,7 +185,7 @@
required_execs = [],
arguments = fn _ => fn timeout =>
"--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
- " --input_file ",
+ " --input_file",
proof_delims =
[("=========== Refutation ==========",
"======= End of refutation ======="),
@@ -197,7 +197,7 @@
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
(OutOfResources, "Refutation not found"),
- (OldVampire, "input_file")],
+ (OldVampire, "not a valid option")],
max_new_relevant_facts_per_iter = 50 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 17 16:47:19 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 17 17:01:31 2010 +0200
@@ -85,8 +85,7 @@
fun sublinear_minimize _ [] p = p
| sublinear_minimize test (x :: xs) (seen, result) =
case test (xs @ seen) of
- result as {outcome = NONE, proof, used_thm_names, ...}
- : prover_result =>
+ result as {outcome = NONE, proof, used_thm_names, ...} : prover_result =>
sublinear_minimize test (filter_used_facts used_thm_names xs)
(filter_used_facts used_thm_names seen, result)
| _ => sublinear_minimize test xs (x :: seen, result)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 17 16:47:19 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 17 17:01:31 2010 +0200
@@ -279,10 +279,10 @@
| add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
| add_type_constraint _ = I
-fun fix_atp_variable_name s =
+fun repair_atp_variable_name f s =
let
fun subscript_name s n = s ^ nat_subscript n
- val s = String.map Char.toLower s
+ val s = String.map f s
in
case space_explode "_" s of
[_] => (case take_suffix Char.isDigit (String.explode s) of
@@ -349,9 +349,10 @@
SOME b => Var ((b, 0), T)
| NONE =>
if is_tptp_variable a then
- Var ((fix_atp_variable_name a, 0), T)
+ Var ((repair_atp_variable_name Char.toLower a, 0), T)
else
- raise Fail ("Unexpected constant: " ^ quote a)
+ (* Skolem constants? *)
+ Var ((repair_atp_variable_name Char.toUpper a, 0), T)
in list_comb (t, ts) end
in aux (SOME HOLogic.boolT) [] end
@@ -410,7 +411,8 @@
do_formula pos (AQuant (q, xs, phi'))
#>> quantify_over_free (case q of
AForall => @{const_name All}
- | AExists => @{const_name Ex}) x
+ | AExists => @{const_name Ex})
+ (repair_atp_variable_name Char.toLower x)
| AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
| AConn (c, [phi1, phi2]) =>
do_formula (pos |> c = AImplies ? not) phi1
@@ -834,6 +836,7 @@
second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
in proof_top @ proof_bottom end
+(* FIXME: Still needed? Probably not. *)
val kill_duplicate_assumptions_in_proof =
let
fun relabel_facts subst =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 17 16:47:19 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 17 17:01:31 2010 +0200
@@ -102,41 +102,41 @@
(0 upto length Ts - 1 ~~ Ts))
fun introduce_combinators_in_term ctxt kind t =
- let
- val thy = ProofContext.theory_of ctxt
- fun aux Ts t =
- case t of
- @{const Not} $ t1 => @{const Not} $ aux Ts t1
- | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
- $ t1 $ t2 =>
- t0 $ aux Ts t1 $ aux Ts t2
- | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
- t
- else
- let
- val t = t |> conceal_bounds Ts
- |> Envir.eta_contract
- val ([t], ctxt') = Variable.import_terms true [t] ctxt
- in
- t |> cterm_of thy
- |> Clausifier.introduce_combinators_in_cterm
- |> singleton (Variable.export ctxt' ctxt)
- |> prop_of |> Logic.dest_equals |> snd
- |> reveal_bounds Ts
- end
- in t |> not (Meson.is_fol_term thy t) ? aux [] end
- handle THM _ =>
- (* A type variable of sort "{}" will make abstraction fail. *)
- case kind of
- Axiom => HOLogic.true_const
- | Conjecture => HOLogic.false_const
+ let val thy = ProofContext.theory_of ctxt in
+ if Meson.is_fol_term thy t then
+ t
+ else
+ let
+ fun aux Ts t =
+ case t of
+ @{const Not} $ t1 => @{const Not} $ aux Ts t1
+ | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
+ $ t1 $ t2 =>
+ t0 $ aux Ts t1 $ aux Ts t2
+ | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
+ t
+ else
+ t |> conceal_bounds Ts
+ |> Envir.eta_contract
+ |> cterm_of thy
+ |> Clausifier.introduce_combinators_in_cterm
+ |> prop_of |> Logic.dest_equals |> snd
+ |> reveal_bounds Ts
+ val ([t], ctxt') = Variable.import_terms true [t] ctxt
+ in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
+ handle THM _ =>
+ (* A type variable of sort "{}" will make abstraction fail. *)
+ case kind of
+ Axiom => HOLogic.true_const
+ | Conjecture => HOLogic.false_const
+ end
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
same in Sledgehammer to prevent the discovery of unreplable proofs. *)