# HG changeset patch # User blanchet # Date 1282057291 -7200 # Node ID 8a7ff1c257737fdbebfe0e3873c95e432559307b # Parent 1f51486da674f8467a5d436d42ae14f9c089b43a# Parent f7e51d981a9fd296506359b039bdcc32f3e50f33 merged diff -r 1f51486da674 -r 8a7ff1c25773 src/HOL/Tools/ATP/atp_problem.ML --- 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) ^ ")" diff -r 1f51486da674 -r 8a7ff1c25773 src/HOL/Tools/ATP/atp_systems.ML --- 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} diff -r 1f51486da674 -r 8a7ff1c25773 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- 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) diff -r 1f51486da674 -r 8a7ff1c25773 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- 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 = diff -r 1f51486da674 -r 8a7ff1c25773 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- 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. *)