--- a/src/HOL/Metis_Examples/BigO.thy Thu Sep 09 17:58:11 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy Thu Sep 09 20:58:46 2010 +0200
@@ -253,10 +253,9 @@
apply (rule abs_triangle_ineq)
apply (metis add_nonneg_nonneg)
apply (rule add_mono)
-using [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq_simpler" ]]
-(*Found by SPASS; SLOW*)
-apply (metis le_maxI2 linorder_linear linorder_not_le min_max.sup_absorb1 mult_le_cancel_right order_trans)
-apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
+using [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq_simpler" ]]
+ apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
+ apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
done
declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt" ]]
@@ -619,9 +618,25 @@
prefer 2
apply simp
apply (simp add: mult_assoc [symmetric] abs_mult)
- (*couldn't get this proof without the step above; SLOW*)
- apply (metis mult_assoc abs_ge_zero mult_left_mono)
-done
+ (* couldn't get this proof without the step above *)
+proof -
+ fix g :: "'b \<Rightarrow> 'a" and d :: 'a
+ assume A1: "c \<noteq> (0\<Colon>'a)"
+ assume A2: "\<forall>x\<Colon>'b. \<bar>g x\<bar> \<le> d * \<bar>f x\<bar>"
+ have F1: "inverse \<bar>c\<bar> = \<bar>inverse c\<bar>" using A1 by (metis nonzero_abs_inverse)
+ have F2: "(0\<Colon>'a) < \<bar>c\<bar>" using A1 by (metis zero_less_abs_iff)
+ have "(0\<Colon>'a) < \<bar>c\<bar> \<longrightarrow> (0\<Colon>'a) < \<bar>inverse c\<bar>" using F1 by (metis positive_imp_inverse_positive)
+ hence "(0\<Colon>'a) < \<bar>inverse c\<bar>" using F2 by metis
+ hence F3: "(0\<Colon>'a) \<le> \<bar>inverse c\<bar>" by (metis order_le_less)
+ have "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar>"
+ using A2 by metis
+ hence F4: "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<and> (0\<Colon>'a) \<le> \<bar>inverse c\<bar>"
+ using F3 by metis
+ hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^isub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^isub>7 (u * v))\<bar>)"
+ by (metis comm_mult_left_mono)
+ thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
+ using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono)
+qed
declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult6" ]]
--- a/src/HOL/Metis_Examples/Message.thy Thu Sep 09 17:58:11 2010 +0200
+++ b/src/HOL/Metis_Examples/Message.thy Thu Sep 09 20:58:46 2010 +0200
@@ -85,7 +85,7 @@
text{*Equations hold because constructors are injective.*}
lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
-by (metis agent.inject imageI image_iff)
+by (metis agent.inject image_iff)
lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x \<in> A)"
by (metis image_iff msg.inject(4))
@@ -241,7 +241,7 @@
lemma parts_trans: "[| X\<in> parts G; G \<subseteq> parts H |] ==> X\<in> parts H"
by (blast dest: parts_mono);
-lemma parts_cut: "[|Y\<in> parts(insert X G); X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
+lemma parts_cut: "[|Y\<in> parts (insert X G); X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI)
@@ -745,15 +745,12 @@
by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un
analz_mono analz_synth_Un insert_absorb)
-(* Simpler problems? BUT METIS CAN'T PROVE THE LAST STEP
lemma Fake_analz_insert_simpler:
"X \<in> synth (analz G) ==>
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
apply (rule subsetI)
apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
apply (metis Un_commute analz_analz_Un analz_synth_Un)
-apply (metis Un_commute Un_upper1 Un_upper2 analz_cut analz_increasing analz_mono insert_absorb insert_mono insert_subset)
-done
-*)
+by (metis Un_upper1 Un_upper2 analz_mono insert_absorb insert_subset)
end
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Sep 09 17:58:11 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Sep 09 20:58:46 2010 +0200
@@ -10,7 +10,8 @@
datatype failure =
Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
- MalformedInput | MalformedOutput | UnknownError
+ MalformedInput | MalformedOutput | Interrupted | InternalError |
+ UnknownError
type prover_config =
{exec: string * string,
@@ -42,7 +43,7 @@
datatype failure =
Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
- MalformedOutput | UnknownError
+ MalformedOutput | Interrupted | InternalError | UnknownError
type prover_config =
{exec: string * string,
@@ -85,6 +86,8 @@
"The ATP problem is malformed. Please report this to the Isabelle \
\developers."
| string_for_failure MalformedOutput = "The ATP output is malformed."
+ | string_for_failure Interrupted = "The ATP was interrupted."
+ | string_for_failure InternalError = "An internal ATP error occurred."
| string_for_failure UnknownError = "An unknown ATP error occurred."
fun known_failure_in_output output =
@@ -182,7 +185,8 @@
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
- (SpassTooOld, "tptp2dfg")],
+ (SpassTooOld, "tptp2dfg"),
+ (InternalError, "Please report this error")],
default_max_relevant = 350 (* FUDGE *),
explicit_forall = true,
use_conjecture_for_hypotheses = true}
@@ -211,7 +215,8 @@
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
(Unprovable, "Termination reason: Satisfiable"),
- (VampireTooOld, "not a valid option")],
+ (VampireTooOld, "not a valid option"),
+ (Interrupted, "Aborted by signal SIGINT")],
default_max_relevant = 400 (* FUDGE *),
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -285,7 +290,7 @@
val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
val remote_vampire = remotify_prover vampire "Vampire" ["9.0", "1.0", "0.6"]
val remote_sine_e =
- remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
+ remote_prover "sine_e" "SInE" [] [] [(IncompleteUnprovable, "says Unknown")]
800 (* FUDGE *) true
val remote_snark =
remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Thu Sep 09 17:58:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Thu Sep 09 20:58:46 2010 +0200
@@ -241,9 +241,13 @@
let
val ctxt0 = Variable.global_thm_context th
val (nnf_th, ctxt) = to_nnf th ctxt0
- val def_th = (* FIXME: to_definitional_cnf_with_quantifiers thy *) nnf_th
- val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs def_th)
- val (cnf_ths, ctxt) = Meson.make_cnf sko_ths def_th ctxt
+ fun aux th =
+ Meson.make_cnf (map (skolem_theorem_of_def thy) (assume_skolem_funs th))
+ th ctxt
+ val (cnf_ths, ctxt) =
+ aux nnf_th
+ |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th)
+ | p => p)
in
cnf_ths |> map introduce_combinators_in_theorem
|> Variable.export ctxt ctxt0
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 09 17:58:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 09 20:58:46 2010 +0200
@@ -432,21 +432,44 @@
(* INFERENCE RULE: RESOLVE *)
-(*Like RSN, but we rename apart only the type variables. Vars here typically have an index
- of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
- could then fail. See comment on mk_var.*)
-fun resolve_inc_tyvars(tha,i,thb) =
+(* Like RSN, but we rename apart only the type variables. Vars here typically
+ have an index of 1, and the use of RSN would increase this typically to 3.
+ Instantiations of those Vars could then fail. See comment on "mk_var". *)
+fun resolve_inc_tyvars thy tha i thb =
let
- val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
- val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
+ val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
+ fun aux tha thb =
+ case Thm.bicompose false (false, tha, nprems_of tha) i thb
+ |> Seq.list_of |> distinct Thm.eq_thm of
+ [th] => th
+ | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
+ [tha, thb])
in
- case distinct Thm.eq_thm ths of
- [th] => th
- | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
+ aux tha thb
+ handle TERM z =>
+ (* The unifier, which is invoked from "Thm.bicompose", will sometimes
+ refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
+ "TERM" exception (with "add_ffpair" as first argument). We then
+ perform unification of the types of variables by hand and try
+ again. We could do this the first time around but this error
+ occurs seldom and we don't want to break existing proofs in subtle
+ ways or slow them down needlessly. *)
+ case [] |> fold (Term.add_vars o prop_of) [tha, thb]
+ |> AList.group (op =)
+ |> maps (fn ((s, _), T :: Ts) =>
+ map (fn T' => (Free (s, T), Free (s, T'))) Ts)
+ |> rpair (Envir.empty ~1)
+ |-> fold (Pattern.unify thy)
+ |> Envir.type_env |> Vartab.dest
+ |> map (fn (x, (S, T)) =>
+ pairself (ctyp_of thy) (TVar (x, S), T)) of
+ [] => raise TERM z
+ | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
end
fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =
let
+ val thy = ProofContext.theory_of ctxt
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
@@ -466,7 +489,10 @@
val index_th2 = get_index i_atm prems_th2
handle Empty => raise Fail "Failed to find literal in th2"
val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2)
- in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end
+ in
+ resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2
+ i_th2
+ end
end;
(* INFERENCE RULE: REFL *)
@@ -790,6 +816,13 @@
#> map Clausifier.introduce_combinators_in_theorem
#> Meson.finish_cnf
+fun preskolem_tac ctxt st0 =
+ (if exists (Meson.has_too_many_clauses ctxt)
+ (Logic.prems_of_goal (prop_of st0) 1) then
+ cnf.cnfx_rewrite_tac ctxt 1
+ else
+ all_tac) st0
+
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
@@ -802,8 +835,7 @@
if exists_type type_has_top_sort (prop_of st0) then
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
else
- Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *)
- (maps neg_clausify)
+ Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
ctxt i st0
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Sep 09 17:58:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Sep 09 20:58:46 2010 +0200
@@ -162,7 +162,10 @@
output =
case known_failure_in_output output known_failures of
NONE => (case extract_proof proof_delims output of
- "" => ("", SOME MalformedOutput)
+ "" => ("", SOME (if res_code = 0 andalso output = "" then
+ Interrupted
+ else
+ UnknownError))
| proof => if res_code = 0 then (proof, NONE)
else ("", SOME UnknownError))
| SOME failure =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Sep 09 17:58:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Sep 09 20:58:46 2010 +0200
@@ -91,12 +91,11 @@
val bracket =
implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg)
^ "]") args)
- val space_bracket = if bracket = "" then "" else " " ^ bracket
val name =
case xref of
- Facts.Fact s => "`" ^ s ^ "`" ^ space_bracket
+ Facts.Fact s => "`" ^ s ^ "`" ^ bracket
| Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
- | _ => Facts.string_of_ref xref ^ space_bracket
+ | _ => Facts.string_of_ref xref ^ bracket
val multi = length ths > 1
in
(ths, (1, []))
@@ -686,6 +685,26 @@
val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
+fun all_prefixes_of s =
+ map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
+
+(* This is a terrible hack. Free variables are sometimes code as "M__" when they
+ are displayed as "M" and we want to avoid clashes with these. But sometimes
+ it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all
+ free variables. In the worse case scenario, where the fact won't be resolved
+ correctly, the user can fix it manually, e.g., by naming the fact in
+ question. Ideally we would need nothing of it, but backticks just don't work
+ with schematic variables. *)
+fun close_form t =
+ (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
+ |> fold (fn ((s, i), T) => fn (t', taken) =>
+ let val s' = Name.variant taken s in
+ (Term.all T $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
+ s' :: taken)
+ end)
+ (Term.add_vars t [] |> sort_wrt (fst o fst))
+ |> fst
+
fun all_name_thms_pairs ctxt reserved full_types add_ths chained_ths =
let
val thy = ProofContext.theory_of ctxt
@@ -700,11 +719,8 @@
clasimpset_rules_of ctxt
else
(Termtab.empty, Termtab.empty, Termtab.empty)
- (* Unnamed nonchained formulas with schematic variables are omitted, because
- they are rejected by the backticks (`...`) parser for some reason. *)
fun is_good_unnamed_local th =
not (Thm.has_name_hint th) andalso
- (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) andalso
forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
val unnamed_locals =
union Thm.eq_thm (Facts.props local_facts) chained_ths
@@ -724,8 +740,10 @@
let
val multi = length ths > 1
fun backquotify th =
- "`" ^ Print_Mode.setmp [Print_Mode.input]
- (Syntax.string_of_term ctxt) (prop_of th) ^ "`"
+ "`" ^ Print_Mode.setmp (Print_Mode.input ::
+ filter (curry (op =) Symbol.xsymbolsN)
+ (print_mode_value ()))
+ (Syntax.string_of_term ctxt) (close_form (prop_of th)) ^ "`"
|> String.translate (fn c => if Char.isPrint c then str c else "")
|> simplify_spaces
fun check_thms a =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Sep 09 17:58:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Sep 09 20:58:46 2010 +0200
@@ -31,6 +31,7 @@
fun string_for_failure Unprovable = "Unprovable."
| string_for_failure TimedOut = "Timed out."
+ | string_for_failure Interrupted = "Interrupted."
| string_for_failure _ = "Unknown error."
fun n_theorems names =
--- a/src/HOL/Tools/meson.ML Thu Sep 09 17:58:11 2010 +0200
+++ b/src/HOL/Tools/meson.ML Thu Sep 09 20:58:46 2010 +0200
@@ -11,7 +11,8 @@
val term_pair_of: indexname * (typ * 'a) -> term * 'a
val flexflex_first_order: thm -> thm
val size_of_subgoals: thm -> int
- val too_many_clauses: Proof.context option -> term -> bool
+ val estimated_num_clauses: Proof.context -> int -> term -> int
+ val has_too_many_clauses: Proof.context -> term -> bool
val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
val finish_cnf: thm list -> thm list
val presimplify: thm -> thm
@@ -26,8 +27,8 @@
val gocls: thm list -> thm list
val skolemize_prems_tac: Proof.context -> thm list -> int -> tactic
val MESON:
- (int -> tactic) -> (thm list -> thm list) -> (thm list -> tactic)
- -> Proof.context -> int -> tactic
+ tactic -> (thm list -> thm list) -> (thm list -> tactic) -> Proof.context
+ -> int -> tactic
val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
val safe_best_meson_tac: Proof.context -> int -> tactic
val depth_meson_tac: Proof.context -> int -> tactic
@@ -262,13 +263,10 @@
(*** The basic CNF transformation ***)
-fun too_many_clauses ctxto t =
+fun estimated_num_clauses ctxt bound t =
let
- val max_cl = case ctxto of SOME ctxt => Config.get ctxt max_clauses
- | NONE => max_clauses_default
-
- fun sum x y = if x < max_cl andalso y < max_cl then x+y else max_cl;
- fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
+ fun sum x y = if x < bound andalso y < bound then x+y else bound
+ fun prod x y = if x < bound andalso y < bound then x*y else bound
(*Estimate the number of clauses in order to detect infeasible theorems*)
fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t
@@ -292,9 +290,12 @@
| signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t
| signed_nclauses b (Const(@{const_name All},_) $ Abs (_,_,t)) = signed_nclauses b t
| signed_nclauses _ _ = 1; (* literal *)
- in
- signed_nclauses true t >= max_cl
- end;
+ in signed_nclauses true t end
+
+fun has_too_many_clauses ctxt t =
+ let val max_cl = Config.get ctxt max_clauses in
+ estimated_num_clauses ctxt (max_cl + 1) t > max_cl
+ end
(*Replaces universally quantified variables by FREE variables -- because
assumptions may not contain scheme variables. Later, generalize using Variable.export. *)
@@ -355,8 +356,8 @@
in Seq.list_of (tac (th RS disj_forward)) @ ths end
| _ => nodups ctxt th :: ths (*no work to do*)
and cnf_nil th = cnf_aux (th,[])
- val cls =
- if too_many_clauses (SOME ctxt) (concl_of th)
+ val cls =
+ if has_too_many_clauses ctxt (concl_of th)
then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
else cnf_aux (th,ths)
in (cls, !ctxtr) end;
@@ -605,9 +606,9 @@
SELECT_GOAL
(EVERY [Object_Logic.atomize_prems_tac 1,
rtac ccontr 1,
+ preskolem_tac,
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
- EVERY1 [preskolem_tac,
- skolemize_prems_tac ctxt negs,
+ EVERY1 [skolemize_prems_tac ctxt negs,
Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
@@ -616,7 +617,7 @@
(*ths is a list of additional clauses (HOL disjunctions) to use.*)
fun best_meson_tac sizef =
- MESON (K all_tac) make_clauses
+ MESON all_tac make_clauses
(fn cls =>
THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
(has_fewer_prems 1, sizef)
@@ -630,7 +631,7 @@
(** Depth-first search version **)
val depth_meson_tac =
- MESON (K all_tac) make_clauses
+ MESON all_tac make_clauses
(fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
@@ -650,7 +651,7 @@
fun iter_deepen_prolog_tac horns =
ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
-fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON (K all_tac) make_clauses
+fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac make_clauses
(fn cls =>
(case (gocls (cls @ ths)) of
[] => no_tac (*no goal clauses*)