# HG changeset patch # User blanchet # Date 1284058726 -7200 # Node ID d67e8537eae5a090c0b0d66773f2b8ec21af767e # Parent 1ff57c8ea8f90d8c932346ee9f334f4ecee0ef80# Parent c2795d8a24614ddd5953922ea878802ecaaab4b2 merged diff -r 1ff57c8ea8f9 -r d67e8537eae5 src/HOL/Metis_Examples/BigO.thy --- 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 \ 'a" and d :: 'a + assume A1: "c \ (0\'a)" + assume A2: "\x\'b. \g x\ \ d * \f x\" + have F1: "inverse \c\ = \inverse c\" using A1 by (metis nonzero_abs_inverse) + have F2: "(0\'a) < \c\" using A1 by (metis zero_less_abs_iff) + have "(0\'a) < \c\ \ (0\'a) < \inverse c\" using F1 by (metis positive_imp_inverse_positive) + hence "(0\'a) < \inverse c\" using F2 by metis + hence F3: "(0\'a) \ \inverse c\" by (metis order_le_less) + have "\(u\'a) SKF\<^isub>7\'a \ 'b. \g (SKF\<^isub>7 (\inverse c\ * u))\ \ u * \f (SKF\<^isub>7 (\inverse c\ * u))\" + using A2 by metis + hence F4: "\(u\'a) SKF\<^isub>7\'a \ 'b. \g (SKF\<^isub>7 (\inverse c\ * u))\ \ u * \f (SKF\<^isub>7 (\inverse c\ * u))\ \ (0\'a) \ \inverse c\" + using F3 by metis + hence "\(v\'a) (u\'a) SKF\<^isub>7\'a \ 'b. \inverse c\ * \g (SKF\<^isub>7 (u * v))\ \ u * (v * \f (SKF\<^isub>7 (u * v))\)" + by (metis comm_mult_left_mono) + thus "\ca\'a. \x\'b. \inverse c\ * \g x\ \ ca * \f x\" + 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" ]] diff -r 1ff57c8ea8f9 -r d67e8537eae5 src/HOL/Metis_Examples/Message.thy --- 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 \ Friend`A) = (x:A)" -by (metis agent.inject imageI image_iff) +by (metis agent.inject image_iff) lemma Key_image_eq [simp]: "(Key x \ Key`A) = (x \ A)" by (metis image_iff msg.inject(4)) @@ -241,7 +241,7 @@ lemma parts_trans: "[| X\ parts G; G \ parts H |] ==> X\ parts H" by (blast dest: parts_mono); -lemma parts_cut: "[|Y\ parts(insert X G); X\ parts H|] ==> Y\ parts(G \ H)" +lemma parts_cut: "[|Y\ parts (insert X G); X\ parts H|] ==> Y\ parts(G \ 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 \ synth (analz G) ==> analz (insert X H) \ synth (analz G) \ analz (G \ H)" apply (rule subsetI) apply (subgoal_tac "x \ analz (synth (analz G) \ 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 diff -r 1ff57c8ea8f9 -r d67e8537eae5 src/HOL/Tools/ATP/atp_systems.ML --- 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.")] [] diff -r 1ff57c8ea8f9 -r d67e8537eae5 src/HOL/Tools/Sledgehammer/clausifier.ML --- 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 diff -r 1ff57c8ea8f9 -r d67e8537eae5 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- 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 diff -r 1ff57c8ea8f9 -r d67e8537eae5 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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 => diff -r 1ff57c8ea8f9 -r d67e8537eae5 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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 = diff -r 1ff57c8ea8f9 -r d67e8537eae5 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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 = diff -r 1ff57c8ea8f9 -r d67e8537eae5 src/HOL/Tools/meson.ML --- 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*)