1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 17 16:47:19 2010 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 17 17:01:31 2010 +0200
1.3 @@ -63,12 +63,12 @@
1.4 | string_for_connective AIff = "<=>"
1.5 | string_for_connective ANotIff = "<~>"
1.6 fun string_for_formula (AQuant (q, xs, phi)) =
1.7 - string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
1.8 - string_for_formula phi
1.9 + "(" ^ string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
1.10 + string_for_formula phi ^ ")"
1.11 | string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
1.12 space_implode " != " (map string_for_term ts)
1.13 | string_for_formula (AConn (c, [phi])) =
1.14 - string_for_connective c ^ " " ^ string_for_formula phi
1.15 + "(" ^ string_for_connective c ^ " " ^ string_for_formula phi ^ ")"
1.16 | string_for_formula (AConn (c, phis)) =
1.17 "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
1.18 (map string_for_formula phis) ^ ")"
2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 16:47:19 2010 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 17:01:31 2010 +0200
2.3 @@ -185,7 +185,7 @@
2.4 required_execs = [],
2.5 arguments = fn _ => fn timeout =>
2.6 "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
2.7 - " --input_file ",
2.8 + " --input_file",
2.9 proof_delims =
2.10 [("=========== Refutation ==========",
2.11 "======= End of refutation ======="),
2.12 @@ -197,7 +197,7 @@
2.13 (TimedOut, "SZS status Timeout"),
2.14 (Unprovable, "Satisfiability detected"),
2.15 (OutOfResources, "Refutation not found"),
2.16 - (OldVampire, "input_file")],
2.17 + (OldVampire, "not a valid option")],
2.18 max_new_relevant_facts_per_iter = 50 (* FIXME *),
2.19 prefers_theory_relevant = false,
2.20 explicit_forall = false}
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 17 16:47:19 2010 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 17 17:01:31 2010 +0200
3.3 @@ -85,8 +85,7 @@
3.4 fun sublinear_minimize _ [] p = p
3.5 | sublinear_minimize test (x :: xs) (seen, result) =
3.6 case test (xs @ seen) of
3.7 - result as {outcome = NONE, proof, used_thm_names, ...}
3.8 - : prover_result =>
3.9 + result as {outcome = NONE, proof, used_thm_names, ...} : prover_result =>
3.10 sublinear_minimize test (filter_used_facts used_thm_names xs)
3.11 (filter_used_facts used_thm_names seen, result)
3.12 | _ => sublinear_minimize test xs (x :: seen, result)
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 17 16:47:19 2010 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 17 17:01:31 2010 +0200
4.3 @@ -279,10 +279,10 @@
4.4 | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
4.5 | add_type_constraint _ = I
4.6
4.7 -fun fix_atp_variable_name s =
4.8 +fun repair_atp_variable_name f s =
4.9 let
4.10 fun subscript_name s n = s ^ nat_subscript n
4.11 - val s = String.map Char.toLower s
4.12 + val s = String.map f s
4.13 in
4.14 case space_explode "_" s of
4.15 [_] => (case take_suffix Char.isDigit (String.explode s) of
4.16 @@ -349,9 +349,10 @@
4.17 SOME b => Var ((b, 0), T)
4.18 | NONE =>
4.19 if is_tptp_variable a then
4.20 - Var ((fix_atp_variable_name a, 0), T)
4.21 + Var ((repair_atp_variable_name Char.toLower a, 0), T)
4.22 else
4.23 - raise Fail ("Unexpected constant: " ^ quote a)
4.24 + (* Skolem constants? *)
4.25 + Var ((repair_atp_variable_name Char.toUpper a, 0), T)
4.26 in list_comb (t, ts) end
4.27 in aux (SOME HOLogic.boolT) [] end
4.28
4.29 @@ -410,7 +411,8 @@
4.30 do_formula pos (AQuant (q, xs, phi'))
4.31 #>> quantify_over_free (case q of
4.32 AForall => @{const_name All}
4.33 - | AExists => @{const_name Ex}) x
4.34 + | AExists => @{const_name Ex})
4.35 + (repair_atp_variable_name Char.toLower x)
4.36 | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
4.37 | AConn (c, [phi1, phi2]) =>
4.38 do_formula (pos |> c = AImplies ? not) phi1
4.39 @@ -834,6 +836,7 @@
4.40 second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
4.41 in proof_top @ proof_bottom end
4.42
4.43 +(* FIXME: Still needed? Probably not. *)
4.44 val kill_duplicate_assumptions_in_proof =
4.45 let
4.46 fun relabel_facts subst =
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 17 16:47:19 2010 +0200
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 17 17:01:31 2010 +0200
5.3 @@ -102,41 +102,41 @@
5.4 (0 upto length Ts - 1 ~~ Ts))
5.5
5.6 fun introduce_combinators_in_term ctxt kind t =
5.7 - let
5.8 - val thy = ProofContext.theory_of ctxt
5.9 - fun aux Ts t =
5.10 - case t of
5.11 - @{const Not} $ t1 => @{const Not} $ aux Ts t1
5.12 - | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
5.13 - t0 $ Abs (s, T, aux (T :: Ts) t')
5.14 - | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
5.15 - t0 $ Abs (s, T, aux (T :: Ts) t')
5.16 - | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
5.17 - | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
5.18 - | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
5.19 - | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
5.20 - $ t1 $ t2 =>
5.21 - t0 $ aux Ts t1 $ aux Ts t2
5.22 - | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
5.23 - t
5.24 - else
5.25 - let
5.26 - val t = t |> conceal_bounds Ts
5.27 - |> Envir.eta_contract
5.28 - val ([t], ctxt') = Variable.import_terms true [t] ctxt
5.29 - in
5.30 - t |> cterm_of thy
5.31 - |> Clausifier.introduce_combinators_in_cterm
5.32 - |> singleton (Variable.export ctxt' ctxt)
5.33 - |> prop_of |> Logic.dest_equals |> snd
5.34 - |> reveal_bounds Ts
5.35 - end
5.36 - in t |> not (Meson.is_fol_term thy t) ? aux [] end
5.37 - handle THM _ =>
5.38 - (* A type variable of sort "{}" will make abstraction fail. *)
5.39 - case kind of
5.40 - Axiom => HOLogic.true_const
5.41 - | Conjecture => HOLogic.false_const
5.42 + let val thy = ProofContext.theory_of ctxt in
5.43 + if Meson.is_fol_term thy t then
5.44 + t
5.45 + else
5.46 + let
5.47 + fun aux Ts t =
5.48 + case t of
5.49 + @{const Not} $ t1 => @{const Not} $ aux Ts t1
5.50 + | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
5.51 + t0 $ Abs (s, T, aux (T :: Ts) t')
5.52 + | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
5.53 + t0 $ Abs (s, T, aux (T :: Ts) t')
5.54 + | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
5.55 + | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
5.56 + | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
5.57 + | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
5.58 + $ t1 $ t2 =>
5.59 + t0 $ aux Ts t1 $ aux Ts t2
5.60 + | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
5.61 + t
5.62 + else
5.63 + t |> conceal_bounds Ts
5.64 + |> Envir.eta_contract
5.65 + |> cterm_of thy
5.66 + |> Clausifier.introduce_combinators_in_cterm
5.67 + |> prop_of |> Logic.dest_equals |> snd
5.68 + |> reveal_bounds Ts
5.69 + val ([t], ctxt') = Variable.import_terms true [t] ctxt
5.70 + in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
5.71 + handle THM _ =>
5.72 + (* A type variable of sort "{}" will make abstraction fail. *)
5.73 + case kind of
5.74 + Axiom => HOLogic.true_const
5.75 + | Conjecture => HOLogic.false_const
5.76 + end
5.77
5.78 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
5.79 same in Sledgehammer to prevent the discovery of unreplable proofs. *)