1.1 --- a/.hgtags Thu Feb 21 10:52:14 2013 +0100
1.2 +++ b/.hgtags Thu Feb 21 16:00:48 2013 +0100
1.3 @@ -5,7 +5,6 @@
1.4 23ceb1dc9755a8ad6f0230697d0cc52f54102bf4 Isabelle94-5
1.5 2cf13a72e1704d0094d21e7dc68e7271a282ed31 Isabelle2008
1.6 33b9b5da3e6faee6ca6969d17e79634d49e5b46a Isabelle94-1
1.7 -35fba71ec6ef550178e5f5e44d95d96c6f36eae6 nominal_01
1.8 3e47692e3a3e4c695f6345b3534ed0c36817fd40 Isabelle99-2
1.9 50be659d4222b68f95e9c966097e59091f26acf3 Isabelle99-1
1.10 67692db44c7099ad8789f088003213aeb095e914 Isabelle94-2
1.11 @@ -16,11 +15,8 @@
1.12 831a9a7ab9f352c65b0f449630b428304c89362b Isabelle93
1.13 836950047d8508e3c200edc1e07a46c2c5e09cd7 Isabelle94-6
1.14 8d42a7bccf0b0880dff8e46c71c4811be8b2e7ec Isabelle94-7
1.15 -a23af144eb47f12354dff090813c796f278e2eb8 nominal_03
1.16 be6b5edbca9ffeb3bace5f4bac5c6478bf8cbdb2 Isabelle98
1.17 -cd41a57221d07441647284e239b8d8d77d498ef5 isa94
1.18 ce180e5b7fa056003791fff19cc5cefba193b135 Isabelle2002
1.19 -dde117622dace696123b023d1f06cf8d8ef9eb46 nominal_02
1.20 f9eb0f819642b2ad77119dbf8935bf13248f205d Isabelle94
1.21 fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005
1.22 5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009
2.1 --- a/src/Doc/Sledgehammer/document/root.tex Thu Feb 21 10:52:14 2013 +0100
2.2 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Feb 21 16:00:48 2013 +0100
2.3 @@ -223,7 +223,7 @@
2.4 for Alt-Ergo, set the
2.5 environment variable \texttt{WHY3\_HOME} to the directory that contains the
2.6 \texttt{why3} executable.
2.7 -Sledgehammer has been tested with Alt-Ergo 0.93 and 0.94, CVC3 2.2 and 2.4.1,
2.8 +Sledgehammer has been tested with Alt-Ergo 0.95, CVC3 2.2 and 2.4.1,
2.9 Yices 1.0.28 and 1.0.33, and Z3 3.0 to 4.0. Since the SMT solvers' output
2.10 formats are somewhat unstable, other versions of the solvers might not work well
2.11 with Sledgehammer. Ideally, also set \texttt{CVC3\_VERSION},
2.12 @@ -308,7 +308,7 @@
2.13 \textit{smt} method call. Rough timings are shown in parentheses, indicating how
2.14 fast the call is. You can click the proof to insert it into the theory text.
2.15
2.16 -In addition, you can ask Sledgehammer for an Isar text proof by passing the
2.17 +In addition, you can ask Sledgehammer for an Isar text proof by enabling the
2.18 \textit{isar\_proofs} option (\S\ref{output-format}):
2.19
2.20 \prew
2.21 @@ -367,7 +367,7 @@
2.22 if that helps.
2.23
2.24 \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
2.25 -that Isar proofs should be generated, instead of one-liner \textit{metis} or
2.26 +that Isar proofs should be generated, in addition to one-liner \textit{metis} or
2.27 \textit{smt} proofs. The length of the Isar proofs can be controlled by setting
2.28 \textit{isar\_compress} (\S\ref{output-format}).
2.29
2.30 @@ -501,15 +501,15 @@
2.31 using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are
2.32 strongly encouraged to report this to the author at \authoremail.
2.33
2.34 -\point{Why are the generated Isar proofs so ugly/broken?}
2.35 -
2.36 -The current implementation of the Isar proof feature,
2.37 -enabled by the \textit{isar\_proofs} option (\S\ref{output-format}),
2.38 -is highly experimental. Work on a new implementation has begun. There is a large body of
2.39 -research into transforming resolution proofs into natural deduction proofs (such
2.40 -as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
2.41 -set the \textit{isar\_compress} option (\S\ref{output-format}) to a larger
2.42 -value or to try several provers and keep the nicest-looking proof.
2.43 +%\point{Why are the generated Isar proofs so ugly/broken?}
2.44 +%
2.45 +%The current implementation of the Isar proof feature,
2.46 +%enabled by the \textit{isar\_proofs} option (\S\ref{output-format}),
2.47 +%is experimental. Work on a new implementation has begun. There is a large body of
2.48 +%research into transforming resolution proofs into natural deduction proofs (such
2.49 +%as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
2.50 +%set the \textit{isar\_compress} option (\S\ref{output-format}) to a larger
2.51 +%value or to try several provers and keep the nicest-looking proof.
2.52
2.53 \point{How can I tell whether a suggested proof is sound?}
2.54
2.55 @@ -843,7 +843,7 @@
2.56 It supports the TPTP polymorphic typed first-order format (TFF1) via Why3
2.57 \cite{why3}. It is included for experimental purposes. To use Alt-Ergo, set the
2.58 environment variable \texttt{WHY3\_HOME} to the directory that contains the
2.59 -\texttt{why3} executable. Sledgehammer has been tested with Alt-Ergo 0.93 and an
2.60 +\texttt{why3} executable. Sledgehammer has been tested with Alt-Ergo 0.95 and an
2.61 unidentified development version of Why3.
2.62
2.63 \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
2.64 @@ -1296,16 +1296,22 @@
2.65 \nopagebreak
2.66 {\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
2.67
2.68 -\opfalse{isar\_proofs}{no\_isar\_proofs}
2.69 +\opsmart{isar\_proofs}{no\_isar\_proofs}
2.70 Specifies whether Isar proofs should be output in addition to one-liner
2.71 -\textit{metis} proofs. Isar proof construction is still experimental and often
2.72 -fails; however, they are usually faster and sometimes more robust than
2.73 -\textit{metis} proofs.
2.74 +\textit{metis} proofs. The construction of Isar proof is still experimental and
2.75 +may sometimes fail; however, when they succeed they are usually faster and more
2.76 +intelligible than \textit{metis} proofs. If the option is set to \textit{smart}
2.77 +(the default), Isar proofs are only generated when no working one-liner
2.78 +\textit{metis} proof is available.
2.79
2.80 \opdefault{isar\_compress}{int}{\upshape 10}
2.81 Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
2.82 -is enabled. A value of $n$ indicates that each Isar proof step should correspond
2.83 -to a group of up to $n$ consecutive proof steps in the ATP proof.
2.84 +is explicitly enabled. A value of $n$ indicates that each Isar proof step should
2.85 +correspond to a group of up to $n$ consecutive proof steps in the ATP proof.
2.86 +
2.87 +\optrueonly{dont\_compress\_isar}
2.88 +Alias for ``\textit{isar\_compress} = 0''.
2.89 +
2.90 \end{enum}
2.91
2.92 \subsection{Authentication}
3.1 --- a/src/HOL/Int.thy Thu Feb 21 10:52:14 2013 +0100
3.2 +++ b/src/HOL/Int.thy Thu Feb 21 16:00:48 2013 +0100
3.3 @@ -1656,7 +1656,7 @@
3.4 int.id_abs_transfer int.rel_eq_transfer zero_int.transfer one_int.transfer
3.5 plus_int.transfer uminus_int.transfer minus_int.transfer times_int.transfer
3.6 int_transfer less_eq_int.transfer less_int.transfer of_int.transfer
3.7 - nat.transfer
3.8 + nat.transfer int.right_unique int.right_total int.bi_total
3.9
3.10 declare Quotient_int [quot_del]
3.11
4.1 --- a/src/HOL/Library/Cardinality.thy Thu Feb 21 10:52:14 2013 +0100
4.2 +++ b/src/HOL/Library/Cardinality.thy Thu Feb 21 16:00:48 2013 +0100
4.3 @@ -234,8 +234,6 @@
4.4 dest!: finite_imageD intro: inj_onI)
4.5 end
4.6
4.7 -declare [[show_consts]]
4.8 -
4.9 instantiation integer :: card_UNIV begin
4.10 definition "finite_UNIV = Phantom(integer) False"
4.11 definition "card_UNIV = Phantom(integer) 0"
5.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Feb 21 10:52:14 2013 +0100
5.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Feb 21 16:00:48 2013 +0100
5.3 @@ -50,7 +50,7 @@
5.4
5.5 (*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*)
5.6 (*defaults used in this Mirabelle action*)
5.7 -val preplay_timeout_default = "4"
5.8 +val preplay_timeout_default = "3"
5.9 val lam_trans_default = "smart"
5.10 val uncurried_aliases_default = "smart"
5.11 val fact_filter_default = "smart"
5.12 @@ -377,18 +377,22 @@
5.13 fun learn prover =
5.14 Sledgehammer_MaSh.mash_learn_proof ctxt params prover (prop_of goal) all_facts
5.15 in
5.16 - Sledgehammer_Minimize.get_minimizing_isar_prover ctxt Sledgehammer_Provers.Normal
5.17 + Sledgehammer_Minimize.get_minimizing_prover ctxt Sledgehammer_Provers.Normal
5.18 learn name
5.19 end
5.20
5.21 type stature = ATP_Problem_Generate.stature
5.22
5.23 -(* hack *)
5.24 +(* Fragile hack *)
5.25 fun reconstructor_from_msg args msg =
5.26 (case AList.lookup (op =) args reconstructorK of
5.27 SOME name => name
5.28 | NONE =>
5.29 - if String.isSubstring "metis (" msg then
5.30 + if (String.isSubstring " ms)" msg orelse String.isSubstring " s)" msg)
5.31 + andalso not (String.isSubstring "(> " msg)
5.32 + andalso not (String.isSubstring ", > " msg) then
5.33 + "none" (* trust the preplayed proof *)
5.34 + else if String.isSubstring "metis (" msg then
5.35 msg |> Substring.full
5.36 |> Substring.position "metis ("
5.37 |> snd |> Substring.position ")"
5.38 @@ -605,7 +609,7 @@
5.39 true 1 (Sledgehammer_Util.subgoal_count st)
5.40 val _ = log separator
5.41 val (used_facts, (preplay, message, message_tail)) =
5.42 - minimize st (these (!named_thms))
5.43 + minimize st NONE (these (!named_thms))
5.44 val msg = message (Lazy.force preplay) ^ message_tail
5.45 in
5.46 case used_facts of
6.1 --- a/src/HOL/Rat.thy Thu Feb 21 10:52:14 2013 +0100
6.2 +++ b/src/HOL/Rat.thy Thu Feb 21 16:00:48 2013 +0100
6.3 @@ -1129,7 +1129,7 @@
6.4 rat.All_transfer rat.Ex_transfer rat.rel_eq_transfer forall_rat_transfer
6.5 Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer
6.6 uminus_rat.transfer times_rat.transfer inverse_rat.transfer
6.7 - positive.transfer of_rat.transfer
6.8 + positive.transfer of_rat.transfer rat.right_unique rat.right_total
6.9
6.10 text {* De-register @{text "rat"} as a quotient type: *}
6.11
7.1 --- a/src/HOL/RealDef.thy Thu Feb 21 10:52:14 2013 +0100
7.2 +++ b/src/HOL/RealDef.thy Thu Feb 21 16:00:48 2013 +0100
7.3 @@ -933,7 +933,8 @@
7.4 lemmas [transfer_rule del] =
7.5 real.All_transfer real.Ex_transfer real.rel_eq_transfer forall_real_transfer
7.6 zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer
7.7 - times_real.transfer inverse_real.transfer positive.transfer
7.8 + times_real.transfer inverse_real.transfer positive.transfer real.right_unique
7.9 + real.right_total
7.10
7.11 subsection{*More Lemmas*}
7.12
8.1 --- a/src/HOL/TPTP/MaSh_Eval.thy Thu Feb 21 10:52:14 2013 +0100
8.2 +++ b/src/HOL/TPTP/MaSh_Eval.thy Thu Feb 21 16:00:48 2013 +0100
8.3 @@ -28,6 +28,7 @@
8.4 val do_it = false (* switch to "true" to generate the files *)
8.5 val params = Sledgehammer_Isar.default_params @{context} []
8.6 val range = (1, NONE)
8.7 +val linearize = false
8.8 val dir = "List"
8.9 val prefix = "/tmp/" ^ dir ^ "/"
8.10 val prob_dir = prefix ^ "mash_problems"
8.11 @@ -42,7 +43,7 @@
8.12
8.13 ML {*
8.14 if do_it then
8.15 - evaluate_mash_suggestions @{context} params range
8.16 + evaluate_mash_suggestions @{context} params range linearize
8.17 [MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
8.18 (SOME prob_dir)
8.19 (prefix ^ "mepo_suggestions")
9.1 --- a/src/HOL/TPTP/MaSh_Export.thy Thu Feb 21 10:52:14 2013 +0100
9.2 +++ b/src/HOL/TPTP/MaSh_Export.thy Thu Feb 21 16:00:48 2013 +0100
9.3 @@ -33,6 +33,7 @@
9.4 val prover = hd provers
9.5 val range = (1, NONE)
9.6 val step = 1
9.7 +val linearize = false
9.8 val max_suggestions = 1024
9.9 val dir = "List"
9.10 val prefix = "/tmp/" ^ dir ^ "/"
9.11 @@ -47,21 +48,22 @@
9.12
9.13 ML {*
9.14 if do_it then
9.15 - generate_accessibility @{context} thys false (prefix ^ "mash_accessibility")
9.16 + generate_accessibility @{context} thys linearize
9.17 + (prefix ^ "mash_accessibility")
9.18 else
9.19 ()
9.20 *}
9.21
9.22 ML {*
9.23 if do_it then
9.24 - generate_features @{context} prover thys false (prefix ^ "mash_features")
9.25 + generate_features @{context} prover thys (prefix ^ "mash_features")
9.26 else
9.27 ()
9.28 *}
9.29
9.30 ML {*
9.31 if do_it then
9.32 - generate_isar_dependencies @{context} thys false
9.33 + generate_isar_dependencies @{context} thys linearize
9.34 (prefix ^ "mash_dependencies")
9.35 else
9.36 ()
9.37 @@ -70,7 +72,7 @@
9.38 ML {*
9.39 if do_it then
9.40 generate_isar_commands @{context} prover (range, step) thys
9.41 - (prefix ^ "mash_commands")
9.42 + linearize (prefix ^ "mash_commands")
9.43 else
9.44 ()
9.45 *}
9.46 @@ -78,7 +80,7 @@
9.47 ML {*
9.48 if do_it then
9.49 generate_mepo_suggestions @{context} params (range, step) thys
9.50 - max_suggestions (prefix ^ "mepo_suggestions")
9.51 + linearize max_suggestions (prefix ^ "mepo_suggestions")
9.52 else
9.53 ()
9.54 *}
9.55 @@ -93,7 +95,7 @@
9.56
9.57 ML {*
9.58 if do_it then
9.59 - generate_prover_dependencies @{context} params range thys false
9.60 + generate_prover_dependencies @{context} params range thys linearize
9.61 (prefix ^ "mash_prover_dependencies")
9.62 else
9.63 ()
9.64 @@ -102,7 +104,7 @@
9.65 ML {*
9.66 if do_it then
9.67 generate_prover_commands @{context} params (range, step) thys
9.68 - (prefix ^ "mash_prover_commands")
9.69 + linearize (prefix ^ "mash_prover_commands")
9.70 else
9.71 ()
9.72 *}
10.1 --- a/src/HOL/TPTP/mash_eval.ML Thu Feb 21 10:52:14 2013 +0100
10.2 +++ b/src/HOL/TPTP/mash_eval.ML Thu Feb 21 16:00:48 2013 +0100
10.3 @@ -16,8 +16,9 @@
10.4 val MeSh_ProverN : string
10.5 val IsarN : string
10.6 val evaluate_mash_suggestions :
10.7 - Proof.context -> params -> int * int option -> string list -> string option
10.8 - -> string -> string -> string -> string -> string -> string -> unit
10.9 + Proof.context -> params -> int * int option -> bool -> string list
10.10 + -> string option -> string -> string -> string -> string -> string -> string
10.11 + -> unit
10.12 end;
10.13
10.14 structure MaSh_Eval : MASH_EVAL =
10.15 @@ -39,7 +40,7 @@
10.16 fun in_range (from, to) j =
10.17 j >= from andalso (to = NONE orelse j <= the to)
10.18
10.19 -fun evaluate_mash_suggestions ctxt params range methods prob_dir_name
10.20 +fun evaluate_mash_suggestions ctxt params range linearize methods prob_dir_name
10.21 mepo_file_name mash_isar_file_name mash_prover_file_name
10.22 mesh_isar_file_name mesh_prover_file_name report_file_name =
10.23 let
10.24 @@ -111,7 +112,10 @@
10.25 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
10.26 val isar_deps = isar_dependencies_of name_tabs th
10.27 val facts =
10.28 - facts |> filter (fn (_, th') => crude_thm_ord (th', th) = LESS)
10.29 + facts
10.30 + |> filter (fn (_, th') =>
10.31 + if linearize then crude_thm_ord (th', th) = LESS
10.32 + else thm_less (th', th))
10.33 val find_suggs =
10.34 find_suggested_facts ctxt facts #> map fact_of_raw_fact
10.35 fun get_facts [] compute = compute facts
11.1 --- a/src/HOL/TPTP/mash_export.ML Thu Feb 21 10:52:14 2013 +0100
11.2 +++ b/src/HOL/TPTP/mash_export.ML Thu Feb 21 16:00:48 2013 +0100
11.3 @@ -12,21 +12,21 @@
11.4 val generate_accessibility :
11.5 Proof.context -> theory list -> bool -> string -> unit
11.6 val generate_features :
11.7 - Proof.context -> string -> theory list -> bool -> string -> unit
11.8 + Proof.context -> string -> theory list -> string -> unit
11.9 val generate_isar_dependencies :
11.10 Proof.context -> theory list -> bool -> string -> unit
11.11 val generate_prover_dependencies :
11.12 Proof.context -> params -> int * int option -> theory list -> bool -> string
11.13 -> unit
11.14 val generate_isar_commands :
11.15 - Proof.context -> string -> (int * int option) * int -> theory list -> string
11.16 - -> unit
11.17 + Proof.context -> string -> (int * int option) * int -> theory list -> bool
11.18 + -> string -> unit
11.19 val generate_prover_commands :
11.20 - Proof.context -> params -> (int * int option) * int -> theory list -> string
11.21 - -> unit
11.22 + Proof.context -> params -> (int * int option) * int -> theory list -> bool
11.23 + -> string -> unit
11.24 val generate_mepo_suggestions :
11.25 - Proof.context -> params -> (int * int option) * int -> theory list -> int
11.26 - -> string -> unit
11.27 + Proof.context -> params -> (int * int option) * int -> theory list -> bool
11.28 + -> int -> string -> unit
11.29 val generate_mesh_suggestions : int -> string -> string -> string -> unit
11.30 end;
11.31
11.32 @@ -51,28 +51,30 @@
11.33 |> sort (crude_thm_ord o pairself snd)
11.34 end
11.35
11.36 -fun generate_accessibility ctxt thys include_thys file_name =
11.37 +fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th))
11.38 +
11.39 +fun generate_accessibility ctxt thys linearize file_name =
11.40 let
11.41 val path = file_name |> Path.explode
11.42 val _ = File.write path ""
11.43 - fun do_fact fact prevs =
11.44 + fun do_fact (parents, fact) prevs =
11.45 let
11.46 - val s = encode_str fact ^ ": " ^ encode_strs prevs ^ "\n"
11.47 + val parents = if linearize then prevs else parents
11.48 + val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n"
11.49 val _ = File.append path s
11.50 in [fact] end
11.51 val facts =
11.52 all_facts ctxt
11.53 - |> not include_thys ? filter_out (has_thys thys o snd)
11.54 - |> map (snd #> nickname_of_thm)
11.55 + |> filter_out (has_thys thys o snd)
11.56 + |> attach_parents_to_facts []
11.57 + |> map (apsnd (nickname_of_thm o snd))
11.58 in fold do_fact facts []; () end
11.59
11.60 -fun generate_features ctxt prover thys include_thys file_name =
11.61 +fun generate_features ctxt prover thys file_name =
11.62 let
11.63 val path = file_name |> Path.explode
11.64 val _ = File.write path ""
11.65 - val facts =
11.66 - all_facts ctxt
11.67 - |> not include_thys ? filter_out (has_thys thys o snd)
11.68 + val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
11.69 fun do_fact ((_, stature), th) =
11.70 let
11.71 val name = nickname_of_thm th
11.72 @@ -109,20 +111,22 @@
11.73 | NONE => (omitted_marker, [])
11.74 end
11.75
11.76 -fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys
11.77 +fun generate_isar_or_prover_dependencies ctxt params_opt range thys linearize
11.78 file_name =
11.79 let
11.80 val path = file_name |> Path.explode
11.81 - val facts =
11.82 - all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd)
11.83 + val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
11.84 val name_tabs = build_name_tables nickname_of_thm facts
11.85 fun do_fact (j, (_, th)) =
11.86 if in_range range j then
11.87 let
11.88 val name = nickname_of_thm th
11.89 val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
11.90 + val access_facts =
11.91 + if linearize then take (j - 1) facts
11.92 + else facts |> filter_accessible_from th
11.93 val (marker, deps) =
11.94 - smart_dependencies_of ctxt params_opt facts name_tabs th NONE
11.95 + smart_dependencies_of ctxt params_opt access_facts name_tabs th NONE
11.96 in encode_str name ^ ": " ^ marker ^ " " ^ encode_strs deps ^ "\n" end
11.97 else
11.98 ""
11.99 @@ -142,25 +146,29 @@
11.100 is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
11.101
11.102 fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
11.103 - file_name =
11.104 + linearize file_name =
11.105 let
11.106 val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
11.107 val path = file_name |> Path.explode
11.108 val facts = all_facts ctxt
11.109 val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
11.110 val name_tabs = build_name_tables nickname_of_thm facts
11.111 - fun do_fact (j, ((name, ((_, stature), th)), prevs)) =
11.112 + fun do_fact (j, ((name, (parents, ((_, stature), th))), prevs)) =
11.113 if in_range range j then
11.114 let
11.115 val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
11.116 val feats =
11.117 features_of ctxt prover (theory_of_thm th) stature [prop_of th]
11.118 val isar_deps = isar_dependencies_of name_tabs th
11.119 + val access_facts =
11.120 + (if linearize then take (j - 1) new_facts
11.121 + else new_facts |> filter_accessible_from th) @ old_facts
11.122 val (marker, deps) =
11.123 - smart_dependencies_of ctxt params_opt facts name_tabs th
11.124 + smart_dependencies_of ctxt params_opt access_facts name_tabs th
11.125 (SOME isar_deps)
11.126 + val parents = if linearize then prevs else parents
11.127 val core =
11.128 - encode_str name ^ ": " ^ encode_strs prevs ^ "; " ^
11.129 + encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
11.130 encode_features (sort_wrt fst feats)
11.131 val query =
11.132 if is_bad_query ctxt ho_atp step j th isar_deps then ""
11.133 @@ -170,10 +178,12 @@
11.134 in query ^ update end
11.135 else
11.136 ""
11.137 - val parents =
11.138 + val new_facts =
11.139 + new_facts |> attach_parents_to_facts old_facts
11.140 + |> map (`(nickname_of_thm o snd o snd))
11.141 + val hd_prevs =
11.142 map (nickname_of_thm o snd) (the_list (try List.last old_facts))
11.143 - val new_facts = new_facts |> map (`(nickname_of_thm o snd))
11.144 - val prevss = fst (split_last (parents :: map (single o fst) new_facts))
11.145 + val prevss = fst (split_last (hd_prevs :: map (single o fst) new_facts))
11.146 val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss))
11.147 in File.write_list path lines end
11.148
11.149 @@ -184,7 +194,7 @@
11.150 generate_isar_or_prover_commands ctxt prover (SOME params)
11.151
11.152 fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...})
11.153 - (range, step) thys max_suggs file_name =
11.154 + (range, step) thys linearize max_suggs file_name =
11.155 let
11.156 val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
11.157 val path = file_name |> Path.explode
11.158 @@ -206,6 +216,7 @@
11.159 let
11.160 val suggs =
11.161 old_facts
11.162 + |> linearize ? filter_accessible_from th
11.163 |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
11.164 max_suggs NONE hyp_ts concl_t
11.165 |> map (nickname_of_thm o snd)
12.1 --- a/src/HOL/Tools/ATP/atp_proof.ML Thu Feb 21 10:52:14 2013 +0100
12.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Feb 21 16:00:48 2013 +0100
12.3 @@ -36,10 +36,7 @@
12.4 UnknownError of string
12.5
12.6 type step_name = string * string list
12.7 -
12.8 - datatype 'a step =
12.9 - Definition_Step of step_name * 'a * 'a |
12.10 - Inference_Step of step_name * formula_role * 'a * string * step_name list
12.11 + type 'a step = step_name * formula_role * 'a * string * step_name list
12.12
12.13 type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
12.14
12.15 @@ -210,15 +207,10 @@
12.16 | (SOME i, SOME j) => int_ord (i, j)
12.17 end
12.18
12.19 -datatype 'a step =
12.20 - Definition_Step of step_name * 'a * 'a |
12.21 - Inference_Step of step_name * formula_role * 'a * string * step_name list
12.22 +type 'a step = step_name * formula_role * 'a * string * step_name list
12.23
12.24 type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
12.25
12.26 -fun step_name (Definition_Step (name, _, _)) = name
12.27 - | step_name (Inference_Step (name, _, _, _, _)) = name
12.28 -
12.29 (**** PARSING OF TSTP FORMAT ****)
12.30
12.31 (* Strings enclosed in single quotes (e.g., file names) *)
12.32 @@ -421,18 +413,14 @@
12.33 phi), "", [])
12.34 | Inference_Source (rule, deps) => (((num, []), phi), rule, deps)
12.35 fun mk_step () =
12.36 - Inference_Step (name, role_of_tptp_string role, phi, rule,
12.37 - map (rpair []) deps)
12.38 + (name, role_of_tptp_string role, phi, rule, map (rpair []) deps)
12.39 in
12.40 case role_of_tptp_string role of
12.41 Definition =>
12.42 (case phi of
12.43 - AConn (AIff, [phi1 as AAtom _, phi2]) =>
12.44 - Definition_Step (name, phi1, phi2)
12.45 - | AAtom (ATerm (("equal", []), _)) =>
12.46 + AAtom (ATerm (("equal", []), _)) =>
12.47 (* Vampire's equality proxy axiom *)
12.48 - Inference_Step (name, Definition, phi, rule,
12.49 - map (rpair []) deps)
12.50 + (name, Definition, phi, rule, map (rpair []) deps)
12.51 | _ => mk_step ())
12.52 | _ => mk_step ()
12.53 end)
12.54 @@ -472,14 +460,14 @@
12.55 (* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>.
12.56 derived from formulae <ident>* *)
12.57 fun parse_spass_line x =
12.58 - (parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":"
12.59 - -- Symbol.scan_ascii_id -- parse_spass_annotations --| $$ "]"
12.60 + (parse_spass_debug |-- scan_general_id --| $$ "[" --|
12.61 + Scan.many1 Symbol.is_digit --| $$ ":" -- Symbol.scan_ascii_id
12.62 + -- parse_spass_annotations --| $$ "]"
12.63 -- parse_horn_clause --| $$ "."
12.64 -- Scan.option (Scan.this_string "derived from formulae "
12.65 |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
12.66 >> (fn ((((num, rule), deps), u), names) =>
12.67 - Inference_Step ((num, these names), Unknown, u, rule,
12.68 - map (rpair []) deps))) x
12.69 + ((num, these names), Unknown, u, rule, map (rpair []) deps))) x
12.70
12.71 val satallax_coreN = "__satallax_core" (* arbitrary *)
12.72 val z3_tptp_coreN = "__z3_tptp_core" (* arbitrary *)
12.73 @@ -488,14 +476,12 @@
12.74 fun parse_z3_tptp_line x =
12.75 (scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]"
12.76 >> (fn (name, names) =>
12.77 - Inference_Step (("", name :: names), Unknown, dummy_phi,
12.78 - z3_tptp_coreN, []))) x
12.79 + (("", name :: names), Unknown, dummy_phi, z3_tptp_coreN, []))) x
12.80
12.81 (* Syntax: <name> *)
12.82 fun parse_satallax_line x =
12.83 (scan_general_id --| Scan.option ($$ " ")
12.84 - >> (fn s => Inference_Step ((s, [s]), Unknown, dummy_phi, satallax_coreN,
12.85 - []))) x
12.86 + >> (fn s => ((s, [s]), Unknown, dummy_phi, satallax_coreN, []))) x
12.87
12.88 fun parse_line problem =
12.89 parse_tstp_line problem || parse_spass_line || parse_z3_tptp_line
12.90 @@ -512,16 +498,12 @@
12.91 | atp_proof_from_tstplike_proof problem tstp =
12.92 tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
12.93 |> parse_proof problem
12.94 - |> sort (step_name_ord o pairself step_name)
12.95 + |> sort (step_name_ord o pairself #1)
12.96
12.97 fun clean_up_dependencies _ [] = []
12.98 - | clean_up_dependencies seen
12.99 - ((step as Definition_Step (name, _, _)) :: steps) =
12.100 - step :: clean_up_dependencies (name :: seen) steps
12.101 - | clean_up_dependencies seen
12.102 - (Inference_Step (name, role, u, rule, deps) :: steps) =
12.103 - Inference_Step (name, role, u, rule,
12.104 - map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
12.105 + | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =
12.106 + (name, role, u, rule,
12.107 + map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
12.108 clean_up_dependencies (name :: seen) steps
12.109
12.110 fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
12.111 @@ -533,10 +515,8 @@
12.112 AQuant (q, map (apfst f) xs, do_formula phi)
12.113 | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
12.114 | do_formula (AAtom t) = AAtom (do_term t)
12.115 - fun do_step (Definition_Step (name, phi1, phi2)) =
12.116 - Definition_Step (name, do_formula phi1, do_formula phi2)
12.117 - | do_step (Inference_Step (name, role, phi, rule, deps)) =
12.118 - Inference_Step (name, role, do_formula phi, rule, deps)
12.119 + fun do_step (name, role, phi, rule, deps) =
12.120 + (name, role, do_formula phi, rule, deps)
12.121 in map do_step end
12.122
12.123 fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s
13.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Feb 21 10:52:14 2013 +0100
13.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Feb 21 16:00:48 2013 +0100
13.3 @@ -158,6 +158,10 @@
13.4
13.5 fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT
13.6
13.7 +(* Cope with "tt(X) = X" atoms, where "X" is existentially quantified. *)
13.8 +fun loose_aconv (Free (s, _), Free (s', _)) = s = s'
13.9 + | loose_aconv (t, t') = t aconv t'
13.10 +
13.11 val vampire_skolem_prefix = "sK"
13.12
13.13 (* First-order translation. No types are known for variables. "HOLogic.typeT"
13.14 @@ -178,8 +182,7 @@
13.15 else if s = tptp_equal then
13.16 let val ts = map (do_term [] NONE) us in
13.17 if textual andalso length ts = 2 andalso
13.18 - hd ts aconv List.last ts then
13.19 - (* Vampire is keen on producing these. *)
13.20 + loose_aconv (hd ts, List.last ts) then
13.21 @{const True}
13.22 else
13.23 list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
14.1 --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Thu Feb 21 10:52:14 2013 +0100
14.2 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Thu Feb 21 16:00:48 2013 +0100
14.3 @@ -32,7 +32,7 @@
14.4
14.5 type direct_proof = direct_inference list
14.6
14.7 - val make_refute_graph : (atom list * atom) list -> refute_graph
14.8 + val make_refute_graph : atom -> (atom list * atom) list -> refute_graph
14.9 val axioms_of_refute_graph : refute_graph -> atom list -> atom list
14.10 val tainted_atoms_of_refute_graph : refute_graph -> atom list -> atom list
14.11 val sequents_of_refute_graph : refute_graph -> ref_sequent list
14.12 @@ -67,19 +67,22 @@
14.13
14.14 type direct_proof = direct_inference list
14.15
14.16 -fun atom_eq p = (Atom.ord p = EQUAL)
14.17 -fun clause_eq (c, d) = (length c = length d andalso forall atom_eq (c ~~ d))
14.18 -fun direct_sequent_eq ((gamma, c), (delta, d)) =
14.19 - clause_eq (gamma, delta) andalso clause_eq (c, d)
14.20 +val atom_eq = is_equal o Atom.ord
14.21 +val clause_ord = dict_ord Atom.ord
14.22 +val clause_eq = is_equal o clause_ord
14.23 +val direct_sequent_ord = prod_ord clause_ord clause_ord
14.24 +val direct_sequent_eq = is_equal o direct_sequent_ord
14.25
14.26 -fun make_refute_graph infers =
14.27 +fun make_refute_graph bot infers =
14.28 let
14.29 fun add_edge to from =
14.30 Atom_Graph.default_node (from, ())
14.31 #> Atom_Graph.default_node (to, ())
14.32 #> Atom_Graph.add_edge_acyclic (from, to)
14.33 fun add_infer (froms, to) = fold (add_edge to) froms
14.34 - in Atom_Graph.empty |> fold add_infer infers end
14.35 + val graph = fold add_infer infers Atom_Graph.empty
14.36 + val reachable = Atom_Graph.all_preds graph [bot]
14.37 + in graph |> Atom_Graph.restrict (member (is_equal o Atom.ord) reachable) end
14.38
14.39 fun axioms_of_refute_graph refute_graph conjs =
14.40 subtract atom_eq conjs (Atom_Graph.minimals refute_graph)
14.41 @@ -165,7 +168,10 @@
14.42 val provable =
14.43 filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs
14.44 val horn_provable = filter (fn (_, [_]) => true | _ => false) provable
14.45 - val seq as (gamma, c) = hd (horn_provable @ provable)
14.46 + val seq as (gamma, c) =
14.47 + case horn_provable @ provable of
14.48 + [] => raise Fail "ill-formed refutation graph"
14.49 + | next :: _ => next
14.50 in
14.51 Have (map single gamma, c) ::
14.52 redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs)
15.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Feb 21 10:52:14 2013 +0100
15.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Feb 21 16:00:48 2013 +0100
15.3 @@ -207,7 +207,7 @@
15.4 val alt_ergo_config : atp_config =
15.5 {exec = (["WHY3_HOME"], ["why3"]),
15.6 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
15.7 - "--format tff1 --prover alt-ergo --timelimit " ^
15.8 + "--format tptp --prover 'Alt-Ergo,0.95,' --timelimit " ^
15.9 string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
15.10 proof_delims = [],
15.11 known_failures =
15.12 @@ -339,9 +339,9 @@
15.13 [(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)),
15.14 (0.15, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)),
15.15 (0.15, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)),
15.16 - (0.15, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN)),
15.17 (0.15, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)),
15.18 - (0.25, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN))]
15.19 + (0.15, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN)),
15.20 + (0.25, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN))]
15.21 else
15.22 [(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))]
15.23 end,
15.24 @@ -543,7 +543,10 @@
15.25 "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
15.26 " --proof tptp --output_axiom_names on" ^
15.27 (if is_vampire_at_least_1_8 () then
15.28 - " --forced_options propositional_to_bdd=off"
15.29 + (* Cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
15.30 + " --forced_options propositional_to_bdd=off:splitting=off:\
15.31 + \equality_proxy=off:general_splitting=off:inequality_splitting=0:\
15.32 + \naming=0"
15.33 else
15.34 "") ^
15.35 " --thanks \"Andrei and Krystof\" --input_file " ^ file_name
16.1 --- a/src/HOL/Tools/ATP/atp_util.ML Thu Feb 21 10:52:14 2013 +0100
16.2 +++ b/src/HOL/Tools/ATP/atp_util.ML Thu Feb 21 16:00:48 2013 +0100
16.3 @@ -287,15 +287,23 @@
16.4 | s_not t = @{const Not} $ t
16.5 fun s_conj (@{const True}, t2) = t2
16.6 | s_conj (t1, @{const True}) = t1
16.7 - | s_conj p = HOLogic.mk_conj p
16.8 + | s_conj (@{const False}, _) = @{const False}
16.9 + | s_conj (_, @{const False}) = @{const False}
16.10 + | s_conj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_conj (t1, t2)
16.11 fun s_disj (@{const False}, t2) = t2
16.12 | s_disj (t1, @{const False}) = t1
16.13 - | s_disj p = HOLogic.mk_disj p
16.14 + | s_disj (@{const True}, _) = @{const True}
16.15 + | s_disj (_, @{const True}) = @{const True}
16.16 + | s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2)
16.17 fun s_imp (@{const True}, t2) = t2
16.18 | s_imp (t1, @{const False}) = s_not t1
16.19 + | s_imp (@{const False}, _) = @{const True}
16.20 + | s_imp (_, @{const True}) = @{const True}
16.21 | s_imp p = HOLogic.mk_imp p
16.22 fun s_iff (@{const True}, t2) = t2
16.23 | s_iff (t1, @{const True}) = t1
16.24 + | s_iff (@{const False}, t2) = s_not t2
16.25 + | s_iff (t1, @{const False}) = s_not t1
16.26 | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
16.27
16.28 (* cf. "close_form" in "refute.ML" *)
17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 21 10:52:14 2013 +0100
17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 21 16:00:48 2013 +0100
17.3 @@ -94,7 +94,7 @@
17.4 ("fact_thresholds", "0.45 0.85"),
17.5 ("max_mono_iters", "smart"),
17.6 ("max_new_mono_instances", "smart"),
17.7 - ("isar_proofs", "false"),
17.8 + ("isar_proofs", "smart"),
17.9 ("isar_compress", "10"),
17.10 ("slice", "true"),
17.11 ("minimize", "smart"),
17.12 @@ -102,7 +102,8 @@
17.13
17.14 val alias_params =
17.15 [("prover", ("provers", [])), (* undocumented *)
17.16 - ("dont_preplay", ("preplay_timeout", ["0"]))]
17.17 + ("dont_preplay", ("preplay_timeout", ["0"])),
17.18 + ("dont_compress_isar", ("isar_compress", ["0"]))]
17.19 val negated_alias_params =
17.20 [("no_debug", "debug"),
17.21 ("quiet", "verbose"),
17.22 @@ -188,20 +189,6 @@
17.23 fun merge data : T = AList.merge (op =) (K true) data
17.24 )
17.25
17.26 -fun remotify_prover_if_supported_and_not_already_remote ctxt name =
17.27 - if String.isPrefix remote_prefix name then
17.28 - SOME name
17.29 - else
17.30 - let val remote_name = remote_prefix ^ name in
17.31 - if is_prover_supported ctxt remote_name then SOME remote_name else NONE
17.32 - end
17.33 -
17.34 -fun remotify_prover_if_not_installed ctxt name =
17.35 - if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
17.36 - SOME name
17.37 - else
17.38 - remotify_prover_if_supported_and_not_already_remote ctxt name
17.39 -
17.40 fun avoid_too_many_threads _ _ [] = []
17.41 | avoid_too_many_threads _ (0, 0) _ = []
17.42 | avoid_too_many_threads ctxt (0, max_remote) provers =
17.43 @@ -312,7 +299,7 @@
17.44 val max_mono_iters = lookup_option lookup_int "max_mono_iters"
17.45 val max_new_mono_instances =
17.46 lookup_option lookup_int "max_new_mono_instances"
17.47 - val isar_proofs = lookup_bool "isar_proofs"
17.48 + val isar_proofs = lookup_option lookup_bool "isar_proofs"
17.49 val isar_compress = Real.max (1.0, lookup_real "isar_compress")
17.50 val slice = mode <> Auto_Try andalso lookup_bool "slice"
17.51 val minimize =
18.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Feb 21 10:52:14 2013 +0100
18.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Feb 21 16:00:48 2013 +0100
18.3 @@ -56,6 +56,7 @@
18.4 ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
18.5 -> 'a list
18.6 val crude_thm_ord : thm * thm -> order
18.7 + val thm_less : thm * thm -> bool
18.8 val goal_of_thm : theory -> thm -> thm
18.9 val run_prover_for_mash :
18.10 Proof.context -> params -> string -> fact list -> thm -> prover_result
18.11 @@ -80,6 +81,8 @@
18.12 val mash_learn_proof :
18.13 Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
18.14 -> unit
18.15 + val attach_parents_to_facts :
18.16 + ('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list
18.17 val mash_learn :
18.18 Proof.context -> params -> fact_override -> thm list -> bool -> unit
18.19 val is_mash_enabled : unit -> bool
18.20 @@ -555,8 +558,8 @@
18.21 {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
18.22 factss = [("", facts)]}
18.23 in
18.24 - get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
18.25 - problem
18.26 + get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
18.27 + problem
18.28 end
18.29
18.30 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
18.31 @@ -902,6 +905,8 @@
18.32 (true, "")
18.33 end)
18.34
18.35 +(* In the following functions, chunks are risers w.r.t. "thm_less_eq". *)
18.36 +
18.37 fun chunks_and_parents_for chunks th =
18.38 let
18.39 fun insert_parent new parents =
18.40 @@ -925,27 +930,30 @@
18.41 in
18.42 fold_rev do_chunk chunks ([], [])
18.43 |>> cons []
18.44 + ||> map nickname_of_thm
18.45 end
18.46
18.47 -fun attach_parents_to_facts facts =
18.48 - let
18.49 - fun do_facts _ _ [] = []
18.50 - | do_facts _ parents [fact] = [(parents, fact)]
18.51 - | do_facts chunks parents ((fact as (_, th)) :: (facts as (_, th') :: _)) =
18.52 - let
18.53 - val chunks = app_hd (cons th) chunks
18.54 - val (chunks', parents') =
18.55 - (if thm_less_eq (th, th') andalso
18.56 - thy_name_of_thm th = thy_name_of_thm th' then
18.57 - (chunks, [th])
18.58 - else
18.59 - chunks_and_parents_for chunks th')
18.60 - ||> map nickname_of_thm
18.61 - in (parents, fact) :: do_facts chunks' parents' facts end
18.62 - in
18.63 - facts |> sort (crude_thm_ord o pairself snd)
18.64 - |> do_facts [[]] []
18.65 - end
18.66 +fun attach_parents_to_facts _ [] = []
18.67 + | attach_parents_to_facts old_facts (facts as (_, th) :: _) =
18.68 + let
18.69 + fun do_facts _ [] = []
18.70 + | do_facts (_, parents) [fact] = [(parents, fact)]
18.71 + | do_facts (chunks, parents)
18.72 + ((fact as (_, th)) :: (facts as (_, th') :: _)) =
18.73 + let
18.74 + val chunks = app_hd (cons th) chunks
18.75 + val chunks_and_parents' =
18.76 + if thm_less_eq (th, th') andalso
18.77 + thy_name_of_thm th = thy_name_of_thm th' then
18.78 + (chunks, [nickname_of_thm th])
18.79 + else
18.80 + chunks_and_parents_for chunks th'
18.81 + in (parents, fact) :: do_facts chunks_and_parents' facts end
18.82 + in
18.83 + old_facts @ facts
18.84 + |> do_facts (chunks_and_parents_for [[]] th)
18.85 + |> drop (length old_facts)
18.86 + end
18.87
18.88 fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
18.89
18.90 @@ -1046,12 +1054,13 @@
18.91 0
18.92 else
18.93 let
18.94 - val facts =
18.95 - facts |> attach_parents_to_facts
18.96 + val new_facts =
18.97 + facts |> sort (crude_thm_ord o pairself snd)
18.98 + |> attach_parents_to_facts []
18.99 |> filter_out (is_in_access_G o snd)
18.100 val (learns, (n, _, _)) =
18.101 ([], (0, next_commit_time (), false))
18.102 - |> fold learn_new_fact facts
18.103 + |> fold learn_new_fact new_facts
18.104 in commit true learns [] []; n end
18.105 fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
18.106 | relearn_old_fact ((_, (_, status)), th)
19.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Feb 21 10:52:14 2013 +0100
19.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Feb 21 16:00:48 2013 +0100
19.3 @@ -18,10 +18,11 @@
19.4 val auto_minimize_max_time : real Config.T
19.5 val minimize_facts :
19.6 (string -> thm list -> unit) -> string -> params -> bool -> int -> int
19.7 - -> Proof.state -> ((string * stature) * thm list) list
19.8 + -> Proof.state -> play Lazy.lazy option
19.9 + -> ((string * stature) * thm list) list
19.10 -> ((string * stature) * thm list) list option
19.11 * (play Lazy.lazy * (play -> string) * string)
19.12 - val get_minimizing_isar_prover :
19.13 + val get_minimizing_prover :
19.14 Proof.context -> mode -> (string -> thm list -> unit) -> string -> prover
19.15 val run_minimize :
19.16 params -> (string -> thm list -> unit) -> int
19.17 @@ -34,6 +35,7 @@
19.18 open ATP_Util
19.19 open ATP_Proof
19.20 open ATP_Problem_Generate
19.21 +open ATP_Systems
19.22 open Sledgehammer_Util
19.23 open Sledgehammer_Fact
19.24 open Sledgehammer_Reconstruct
19.25 @@ -190,7 +192,7 @@
19.26 end
19.27
19.28 fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent
19.29 - i n state facts =
19.30 + i n state preplay0 facts =
19.31 let
19.32 val ctxt = Proof.context_of state
19.33 val prover =
19.34 @@ -221,7 +223,12 @@
19.35 0 => ""
19.36 | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
19.37 (if learn then do_learn prover_name (maps snd min_facts) else ());
19.38 - (SOME min_facts, (preplay, message, message_tail))
19.39 + (SOME min_facts,
19.40 + (if is_some preplay0 andalso length min_facts = length facts then
19.41 + the preplay0
19.42 + else
19.43 + preplay,
19.44 + message, message_tail))
19.45 end
19.46 | {outcome = SOME TimedOut, preplay, ...} =>
19.47 (NONE,
19.48 @@ -287,20 +294,26 @@
19.49 <= Config.get ctxt auto_minimize_max_time
19.50 fun prover_fast_enough () = can_min_fast_enough run_time
19.51 in
19.52 - if isar_proofs then
19.53 - ((prover_fast_enough (), (name, params)), preplay)
19.54 - else
19.55 - (case Lazy.force preplay of
19.56 - Played (reconstr, timeout) =>
19.57 - if can_min_fast_enough timeout then
19.58 - (true, extract_reconstructor params reconstr
19.59 - ||> (fn override_params =>
19.60 - adjust_reconstructor_params
19.61 - override_params params))
19.62 - else
19.63 - (prover_fast_enough (), (name, params))
19.64 - | _ => (prover_fast_enough (), (name, params)),
19.65 - preplay)
19.66 + (case Lazy.force preplay of
19.67 + Played (reconstr as Metis _, timeout) =>
19.68 + if isar_proofs = SOME true then
19.69 + (* Cheat: Assume the selected ATP is as fast as "metis" for
19.70 + the goal it proved itself. *)
19.71 + (can_min_fast_enough timeout,
19.72 + (isar_proof_reconstructor ctxt name, params))
19.73 + else if can_min_fast_enough timeout then
19.74 + (true, extract_reconstructor params reconstr
19.75 + ||> (fn override_params =>
19.76 + adjust_reconstructor_params override_params
19.77 + params))
19.78 + else
19.79 + (prover_fast_enough (), (name, params))
19.80 + | Played (SMT, timeout) =>
19.81 + (* Cheat: Assume the original prover is as fast as "smt" for
19.82 + the goal it proved itself *)
19.83 + (can_min_fast_enough timeout, (name, params))
19.84 + | _ => (prover_fast_enough (), (name, params)),
19.85 + preplay)
19.86 end
19.87 else
19.88 ((false, (name, params)), preplay)
19.89 @@ -309,6 +322,7 @@
19.90 if minimize then
19.91 minimize_facts do_learn minimize_name params
19.92 (mode <> Normal orelse not verbose) subgoal subgoal_count state
19.93 + (SOME preplay)
19.94 (filter_used_facts true used_facts (map (apsnd single) used_from))
19.95 |>> Option.map (map fst)
19.96 else
19.97 @@ -322,14 +336,10 @@
19.98 | NONE => result
19.99 end
19.100
19.101 -(* TODO: implement *)
19.102 -fun maybe_regenerate_isar_proof result = result
19.103 -
19.104 -fun get_minimizing_isar_prover ctxt mode do_learn name params minimize_command
19.105 - problem =
19.106 +fun get_minimizing_prover ctxt mode do_learn name params minimize_command
19.107 + problem =
19.108 get_prover ctxt mode name params minimize_command problem
19.109 |> maybe_minimize ctxt mode do_learn name params problem
19.110 - |> maybe_regenerate_isar_proof
19.111
19.112 fun run_minimize (params as {provers, ...}) do_learn i refs state =
19.113 let
19.114 @@ -347,7 +357,7 @@
19.115 [] => error "No prover is set."
19.116 | prover :: _ =>
19.117 (kill_provers ();
19.118 - minimize_facts do_learn prover params false i n state facts
19.119 + minimize_facts do_learn prover params false i n state NONE facts
19.120 |> (fn (_, (preplay, message, message_tail)) =>
19.121 message (Lazy.force preplay) ^ message_tail
19.122 |> Output.urgent_message))
20.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Feb 21 10:52:14 2013 +0100
20.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Feb 21 16:00:48 2013 +0100
20.3 @@ -34,7 +34,7 @@
20.4 fact_thresholds : real * real,
20.5 max_mono_iters : int option,
20.6 max_new_mono_instances : int option,
20.7 - isar_proofs : bool,
20.8 + isar_proofs : bool option,
20.9 isar_compress : real,
20.10 slice : bool,
20.11 minimize : bool option,
20.12 @@ -110,6 +110,10 @@
20.13 val is_unit_equational_atp : Proof.context -> string -> bool
20.14 val is_prover_supported : Proof.context -> string -> bool
20.15 val is_prover_installed : Proof.context -> string -> bool
20.16 + val remotify_prover_if_supported_and_not_already_remote :
20.17 + Proof.context -> string -> string option
20.18 + val remotify_prover_if_not_installed :
20.19 + Proof.context -> string -> string option
20.20 val default_max_facts_for_prover : Proof.context -> bool -> string -> int
20.21 val is_unit_equality : term -> bool
20.22 val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool
20.23 @@ -129,6 +133,7 @@
20.24 val filter_used_facts :
20.25 bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
20.26 ((''a * stature) * 'b) list
20.27 + val isar_proof_reconstructor : Proof.context -> string -> string
20.28 val get_prover : Proof.context -> mode -> string -> prover
20.29 end;
20.30
20.31 @@ -186,17 +191,33 @@
20.32 is_reconstructor orf is_smt_prover ctxt orf
20.33 is_atp_installed (Proof_Context.theory_of ctxt)
20.34
20.35 +fun remotify_prover_if_supported_and_not_already_remote ctxt name =
20.36 + if String.isPrefix remote_prefix name then
20.37 + SOME name
20.38 + else
20.39 + let val remote_name = remote_prefix ^ name in
20.40 + if is_prover_supported ctxt remote_name then SOME remote_name else NONE
20.41 + end
20.42 +
20.43 +fun remotify_prover_if_not_installed ctxt name =
20.44 + if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
20.45 + SOME name
20.46 + else
20.47 + remotify_prover_if_supported_and_not_already_remote ctxt name
20.48 +
20.49 fun get_slices slice slices =
20.50 (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
20.51
20.52 val reconstructor_default_max_facts = 20
20.53
20.54 +fun slice_max_facts (_, (_, ( ((max_facts, _), _, _, _, _), _))) = max_facts
20.55 +
20.56 fun default_max_facts_for_prover ctxt slice name =
20.57 let val thy = Proof_Context.theory_of ctxt in
20.58 if is_reconstructor name then
20.59 reconstructor_default_max_facts
20.60 else if is_atp thy name then
20.61 - fold (Integer.max o fst o #1 o fst o snd o snd)
20.62 + fold (Integer.max o slice_max_facts)
20.63 (get_slices slice (#best_slices (get_atp thy name ()) ctxt)) 0
20.64 else (* is_smt_prover ctxt name *)
20.65 SMT_Solver.default_max_relevant ctxt name
20.66 @@ -321,7 +342,7 @@
20.67 fact_thresholds : real * real,
20.68 max_mono_iters : int option,
20.69 max_new_mono_instances : int option,
20.70 - isar_proofs : bool,
20.71 + isar_proofs : bool option,
20.72 isar_compress : real,
20.73 slice : bool,
20.74 minimize : bool option,
20.75 @@ -596,19 +617,26 @@
20.76 #> type_enc_from_string soundness
20.77 #> adjust_type_enc format
20.78
20.79 -val metis_minimize_max_time = seconds 2.0
20.80 +fun isar_proof_reconstructor ctxt name =
20.81 + let val thy = Proof_Context.theory_of ctxt in
20.82 + if is_atp thy name then name
20.83 + else remotify_prover_if_not_installed ctxt eN |> the_default name
20.84 + end
20.85
20.86 -fun choose_minimize_command params minimize_command name preplay =
20.87 +(* See the analogous logic in the function "maybe_minimize" in
20.88 + "sledgehammer_minimize.ML". *)
20.89 +fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command
20.90 + name preplay =
20.91 let
20.92 - val (name, override_params) =
20.93 + val maybe_isar_name =
20.94 + name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt
20.95 + val (min_name, override_params) =
20.96 case preplay of
20.97 - Played (reconstr, time) =>
20.98 - if Time.<= (time, metis_minimize_max_time) then
20.99 - extract_reconstructor params reconstr
20.100 - else
20.101 - (name, [])
20.102 - | _ => (name, [])
20.103 - in minimize_command override_params name end
20.104 + Played (reconstr, _) =>
20.105 + if isar_proofs = SOME true then (maybe_isar_name, [])
20.106 + else extract_reconstructor params reconstr
20.107 + | _ => (maybe_isar_name, [])
20.108 + in minimize_command override_params min_name end
20.109
20.110 fun repair_monomorph_context max_iters best_max_iters max_new_instances
20.111 best_max_new_instances =
20.112 @@ -630,6 +658,10 @@
20.113
20.114 val mono_max_privileged_facts = 10
20.115
20.116 +(* For low values of "max_facts", this fudge value ensures that most slices are
20.117 + invoked with a nontrivial amount of facts. *)
20.118 +val max_fact_factor_fudge = 5
20.119 +
20.120 fun run_atp mode name
20.121 ({exec, arguments, proof_delims, known_failures, prem_role, best_slices,
20.122 best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
20.123 @@ -692,6 +724,13 @@
20.124 time available. *)
20.125 val actual_slices = get_slices slice (best_slices ctxt)
20.126 val num_actual_slices = length actual_slices
20.127 + val max_fact_factor =
20.128 + case max_facts of
20.129 + NONE => 1.0
20.130 + | SOME max =>
20.131 + Real.fromInt max
20.132 + / Real.fromInt (fold (Integer.max o slice_max_facts)
20.133 + actual_slices 0)
20.134 fun monomorphize_facts facts =
20.135 let
20.136 val ctxt =
20.137 @@ -724,7 +763,9 @@
20.138 fact_filter |> the_default best_fact_filter
20.139 val facts = get_facts_for_filter effective_fact_filter factss
20.140 val num_facts =
20.141 - length facts |> is_none max_facts ? Integer.min best_max_facts
20.142 + Real.ceil (max_fact_factor * Real.fromInt best_max_facts) +
20.143 + max_fact_factor_fudge
20.144 + |> Integer.min (length facts)
20.145 val soundness = if strict then Strict else Non_Strict
20.146 val type_enc =
20.147 type_enc |> choose_type_enc soundness best_type_enc format
20.148 @@ -780,7 +821,8 @@
20.149 fun sel_weights () = atp_problem_selection_weights atp_problem
20.150 fun ord_info () = atp_problem_term_order_info atp_problem
20.151 val ord = effective_term_order ctxt name
20.152 - val full_proof = debug orelse isar_proofs
20.153 + val full_proof =
20.154 + debug orelse (isar_proofs |> the_default (mode = Minimize))
20.155 val args =
20.156 arguments ctxt full_proof extra
20.157 (slice_timeout |> the_default one_day)
20.158 @@ -894,7 +936,7 @@
20.159 let
20.160 val _ =
20.161 if verbose then
20.162 - Output.urgent_message "Generating proof text..."
20.163 + Output.urgent_message "Generating structured proof..."
20.164 else
20.165 ()
20.166 val isar_params =
20.167 @@ -902,7 +944,8 @@
20.168 pool, fact_names, sym_tab, atp_proof, goal)
20.169 val one_line_params =
20.170 (preplay, proof_banner mode name, used_facts,
20.171 - choose_minimize_command params minimize_command name preplay,
20.172 + choose_minimize_command ctxt params minimize_command name
20.173 + preplay,
20.174 subgoal, subgoal_count)
20.175 val num_chained = length (#facts (Proof.goal state))
20.176 in
20.177 @@ -1022,10 +1065,8 @@
20.178 val birth = Timer.checkRealTimer timer
20.179 val _ =
20.180 if debug then Output.urgent_message "Invoking SMT solver..." else ()
20.181 - val state_facts = these (try (#facts o Proof.goal) state)
20.182 val (outcome, used_facts) =
20.183 - SMT_Solver.smt_filter_preprocess ctxt state_facts goal weighted_facts
20.184 - i
20.185 + SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
20.186 |> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day)
20.187 |> (fn {outcome, used_facts} => (outcome, used_facts))
20.188 handle exn => if Exn.is_interrupt exn then
20.189 @@ -1112,7 +1153,8 @@
20.190 let
20.191 val one_line_params =
20.192 (preplay, proof_banner mode name, used_facts,
20.193 - choose_minimize_command params minimize_command name preplay,
20.194 + choose_minimize_command ctxt params minimize_command name
20.195 + preplay,
20.196 subgoal, subgoal_count)
20.197 val num_chained = length (#facts (Proof.goal state))
20.198 in one_line_proof_text num_chained one_line_params end,
21.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 21 10:52:14 2013 +0100
21.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 21 16:00:48 2013 +0100
21.3 @@ -38,9 +38,10 @@
21.4 string list option
21.5 val one_line_proof_text : int -> one_line_params -> string
21.6 val isar_proof_text :
21.7 - Proof.context -> bool -> isar_params -> one_line_params -> string
21.8 + Proof.context -> bool option -> isar_params -> one_line_params -> string
21.9 val proof_text :
21.10 - Proof.context -> bool -> isar_params -> int -> one_line_params -> string
21.11 + Proof.context -> bool option -> isar_params -> int -> one_line_params
21.12 + -> string
21.13 end;
21.14
21.15 structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
21.16 @@ -118,8 +119,7 @@
21.17 val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)
21.18
21.19 fun is_axiom_used_in_proof pred =
21.20 - exists (fn Inference_Step ((_, ss), _, _, _, []) => exists pred ss
21.21 - | _ => false)
21.22 + exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
21.23
21.24 fun lam_trans_from_atp_proof atp_proof default =
21.25 case (is_axiom_used_in_proof is_combinator_def atp_proof,
21.26 @@ -154,24 +154,23 @@
21.27 val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
21.28 val leo2_unfold_def_rule = "unfold_def"
21.29
21.30 -fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, _, rule, deps)) =
21.31 - (if rule = leo2_extcnf_equal_neg_rule then
21.32 - insert (op =) (ext_name ctxt, (Global, General))
21.33 - else if rule = leo2_unfold_def_rule then
21.34 - (* LEO 1.3.3 does not record definitions properly, leading to missing
21.35 - dependencies in the TSTP proof. Remove the next line once this is
21.36 - fixed. *)
21.37 - add_non_rec_defs fact_names
21.38 - else if rule = satallax_coreN then
21.39 - (fn [] =>
21.40 - (* Satallax doesn't include definitions in its unsatisfiable cores,
21.41 - so we assume the worst and include them all here. *)
21.42 - [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
21.43 - | facts => facts)
21.44 - else
21.45 - I)
21.46 - #> (if null deps then union (op =) (resolve_fact fact_names ss) else I)
21.47 - | add_fact _ _ _ = I
21.48 +fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) =
21.49 + (if rule = leo2_extcnf_equal_neg_rule then
21.50 + insert (op =) (ext_name ctxt, (Global, General))
21.51 + else if rule = leo2_unfold_def_rule then
21.52 + (* LEO 1.3.3 does not record definitions properly, leading to missing
21.53 + dependencies in the TSTP proof. Remove the next line once this is
21.54 + fixed. *)
21.55 + add_non_rec_defs fact_names
21.56 + else if rule = satallax_coreN then
21.57 + (fn [] =>
21.58 + (* Satallax doesn't include definitions in its unsatisfiable cores, so
21.59 + we assume the worst and include them all here. *)
21.60 + [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
21.61 + | facts => facts)
21.62 + else
21.63 + I)
21.64 + #> (if null deps then union (op =) (resolve_fact fact_names ss) else I)
21.65
21.66 fun used_facts_in_atp_proof ctxt fact_names atp_proof =
21.67 if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
21.68 @@ -298,9 +297,6 @@
21.69 else
21.70 s
21.71
21.72 -fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
21.73 - | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
21.74 -
21.75 fun infer_formula_types ctxt =
21.76 Type.constraint HOLogic.boolT
21.77 #> Syntax.check_term
21.78 @@ -325,41 +321,22 @@
21.79 | aux t = t
21.80 in aux end
21.81
21.82 -fun decode_line sym_tab (Definition_Step (name, phi1, phi2)) ctxt =
21.83 - let
21.84 - val thy = Proof_Context.theory_of ctxt
21.85 - val t1 = prop_from_atp ctxt true sym_tab phi1
21.86 - val vars = snd (strip_comb t1)
21.87 - val frees = map unvarify_term vars
21.88 - val unvarify_args = subst_atomic (vars ~~ frees)
21.89 - val t2 = prop_from_atp ctxt true sym_tab phi2
21.90 - val (t1, t2) =
21.91 - HOLogic.eq_const HOLogic.typeT $ t1 $ t2
21.92 - |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt
21.93 - |> HOLogic.dest_eq
21.94 - in
21.95 - (Definition_Step (name, t1, t2),
21.96 - fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt)
21.97 - end
21.98 - | decode_line sym_tab (Inference_Step (name, role, u, rule, deps)) ctxt =
21.99 - let
21.100 - val thy = Proof_Context.theory_of ctxt
21.101 - val t = u |> prop_from_atp ctxt true sym_tab
21.102 - |> uncombine_term thy |> infer_formula_types ctxt
21.103 - in
21.104 - (Inference_Step (name, role, t, rule, deps),
21.105 - fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
21.106 - end
21.107 +fun decode_line sym_tab (name, role, u, rule, deps) ctxt =
21.108 + let
21.109 + val thy = Proof_Context.theory_of ctxt
21.110 + val t = u |> prop_from_atp ctxt true sym_tab
21.111 + |> uncombine_term thy |> infer_formula_types ctxt
21.112 + in
21.113 + ((name, role, t, rule, deps),
21.114 + fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
21.115 + end
21.116 fun decode_lines ctxt sym_tab lines =
21.117 fst (fold_map (decode_line sym_tab) lines ctxt)
21.118
21.119 fun replace_one_dependency (old, new) dep =
21.120 if is_same_atp_step dep old then new else [dep]
21.121 -fun replace_dependencies_in_line _ (line as Definition_Step _) = line
21.122 - | replace_dependencies_in_line p
21.123 - (Inference_Step (name, role, t, rule, deps)) =
21.124 - Inference_Step (name, role, t, rule,
21.125 - fold (union (op =) o replace_one_dependency p) deps [])
21.126 +fun replace_dependencies_in_line p (name, role, t, rule, deps) =
21.127 + (name, role, t, rule, fold (union (op =) o replace_one_dependency p) deps [])
21.128
21.129 (* No "real" literals means only type information (tfree_tcs, clsrel, or
21.130 clsarity). *)
21.131 @@ -367,19 +344,16 @@
21.132
21.133 fun s_maybe_not role = role <> Conjecture ? s_not
21.134
21.135 -fun is_same_inference _ (Definition_Step _) = false
21.136 - | is_same_inference (role, t) (Inference_Step (_, role', t', _, _)) =
21.137 - s_maybe_not role t aconv s_maybe_not role' t'
21.138 +fun is_same_inference (role, t) (_, role', t', _, _) =
21.139 + s_maybe_not role t aconv s_maybe_not role' t'
21.140
21.141 (* Discard facts; consolidate adjacent lines that prove the same formula, since
21.142 they differ only in type information.*)
21.143 -fun add_line _ (line as Definition_Step _) lines = line :: lines
21.144 - | add_line fact_names (Inference_Step (name as (_, ss), role, t, rule, []))
21.145 - lines =
21.146 +fun add_line fact_names (name as (_, ss), role, t, rule, []) lines =
21.147 (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
21.148 definitions. *)
21.149 if is_conjecture ss then
21.150 - Inference_Step (name, role, t, rule, []) :: lines
21.151 + (name, role, t, rule, []) :: lines
21.152 else if is_fact fact_names ss then
21.153 (* Facts are not proof lines. *)
21.154 if is_only_type_information t then
21.155 @@ -388,35 +362,30 @@
21.156 lines
21.157 else
21.158 map (replace_dependencies_in_line (name, [])) lines
21.159 - | add_line _ (line as Inference_Step (name, role, t, rule, deps)) lines =
21.160 + | add_line _ (line as (name, role, t, _, _)) lines =
21.161 (* Type information will be deleted later; skip repetition test. *)
21.162 if is_only_type_information t then
21.163 line :: lines
21.164 (* Is there a repetition? If so, replace later line by earlier one. *)
21.165 else case take_prefix (not o is_same_inference (role, t)) lines of
21.166 - (* FIXME: Doesn't this code risk conflating proofs involving different
21.167 - types? *)
21.168 (_, []) => line :: lines
21.169 - | (pre, Inference_Step (name', _, _, _, _) :: post) =>
21.170 + | (pre, (name', _, _, _, _) :: post) =>
21.171 line :: pre @ map (replace_dependencies_in_line (name', [name])) post
21.172 - | _ => raise Fail "unexpected inference"
21.173
21.174 val waldmeister_conjecture_num = "1.0.0.0"
21.175
21.176 val repair_waldmeister_endgame =
21.177 let
21.178 - fun do_tail (Inference_Step (name, _, t, rule, deps)) =
21.179 - Inference_Step (name, Negated_Conjecture, s_not t, rule, deps)
21.180 - | do_tail line = line
21.181 + fun do_tail (name, _, t, rule, deps) =
21.182 + (name, Negated_Conjecture, s_not t, rule, deps)
21.183 fun do_body [] = []
21.184 - | do_body ((line as Inference_Step ((num, _), _, _, _, _)) :: lines) =
21.185 + | do_body ((line as ((num, _), _, _, _, _)) :: lines) =
21.186 if num = waldmeister_conjecture_num then map do_tail (line :: lines)
21.187 else line :: do_body lines
21.188 - | do_body (line :: lines) = line :: do_body lines
21.189 in do_body end
21.190
21.191 (* Recursively delete empty lines (type information) from the proof. *)
21.192 -fun add_nontrivial_line (line as Inference_Step (name, _, t, _, [])) lines =
21.193 +fun add_nontrivial_line (line as (name, _, t, _, [])) lines =
21.194 if is_only_type_information t then delete_dependency name lines
21.195 else line :: lines
21.196 | add_nontrivial_line line lines = line :: lines
21.197 @@ -435,25 +404,23 @@
21.198 val is_skolemize_rule =
21.199 member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
21.200
21.201 -fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) =
21.202 - (j, line :: map (replace_dependencies_in_line (name, [])) lines)
21.203 - | add_desired_line fact_names frees
21.204 - (Inference_Step (name as (_, ss), role, t, rule, deps)) (j, lines) =
21.205 - (j + 1,
21.206 - if is_fact fact_names ss orelse
21.207 - is_conjecture ss orelse
21.208 - is_skolemize_rule rule orelse
21.209 - (* the last line must be kept *)
21.210 - j = 0 orelse
21.211 - (not (is_only_type_information t) andalso
21.212 - null (Term.add_tvars t []) andalso
21.213 - not (exists_subterm (is_bad_free frees) t) andalso
21.214 - length deps >= 2 andalso
21.215 - (* kill next to last line, which usually results in a trivial step *)
21.216 - j <> 1) then
21.217 - Inference_Step (name, role, t, rule, deps) :: lines (* keep line *)
21.218 - else
21.219 - map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
21.220 +fun add_desired_line fact_names frees (name as (_, ss), role, t, rule, deps)
21.221 + (j, lines) =
21.222 + (j + 1,
21.223 + if is_fact fact_names ss orelse
21.224 + is_conjecture ss orelse
21.225 + is_skolemize_rule rule orelse
21.226 + (* the last line must be kept *)
21.227 + j = 0 orelse
21.228 + (not (is_only_type_information t) andalso
21.229 + null (Term.add_tvars t []) andalso
21.230 + not (exists_subterm (is_bad_free frees) t) andalso
21.231 + length deps >= 2 andalso
21.232 + (* kill next to last line, which usually results in a trivial step *)
21.233 + j <> 1) then
21.234 + (name, role, t, rule, deps) :: lines (* keep line *)
21.235 + else
21.236 + map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
21.237
21.238 val indent_size = 2
21.239
21.240 @@ -537,18 +504,20 @@
21.241 add_step_pre ind qs subproofs
21.242 #> add_suffix (of_prove qs (length subproofs) ^ " ")
21.243 #> add_step_post ind l t facts ""
21.244 - | add_step ind (Obtain (qs, Fix xs, l, t,
21.245 - By_Metis (subproofs, facts))) =
21.246 + | add_step ind (Obtain (qs, Fix xs, l, t, By_Metis (subproofs, facts))) =
21.247 add_step_pre ind qs subproofs
21.248 #> add_suffix (of_obtain qs (length subproofs) ^ " ")
21.249 #> add_frees xs
21.250 #> add_suffix " where "
21.251 (* The new skolemizer puts the arguments in the same order as the ATPs
21.252 - (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
21.253 - Vampire). *)
21.254 - #> add_step_post ind l t facts "using [[metis_new_skolem]] "
21.255 - and add_steps ind steps =
21.256 - fold (add_step ind) steps
21.257 + (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
21.258 + Vampire). *)
21.259 + #> add_step_post ind l t facts
21.260 + (if exists (fn (_, T) => length (binder_types T) > 1) xs then
21.261 + "using [[metis_new_skolem]] "
21.262 + else
21.263 + "")
21.264 + and add_steps ind = fold (add_step ind)
21.265 and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) =
21.266 ("", ctxt)
21.267 |> add_fix ind xs
21.268 @@ -566,12 +535,11 @@
21.269 end
21.270
21.271 fun add_labels_of_step step =
21.272 - (case byline_of_step step of
21.273 - NONE => I
21.274 - | SOME (By_Metis (subproofs, (ls, _))) =>
21.275 - union (op =) (add_labels_of_proofs subproofs ls))
21.276 + case byline_of_step step of
21.277 + NONE => I
21.278 + | SOME (By_Metis (subproofs, (ls, _))) =>
21.279 + union (op =) ls #> fold add_labels_of_proof subproofs
21.280 and add_labels_of_proof proof = fold add_labels_of_step (steps_of_proof proof)
21.281 -and add_labels_of_proofs proofs = fold add_labels_of_proof proofs
21.282
21.283 fun kill_useless_labels_in_proof proof =
21.284 let
21.285 @@ -617,17 +585,13 @@
21.286 val (l, subst, next) =
21.287 (l, subst, next) |> fresh_label depth have_prefix
21.288 val by = by |> do_byline subst depth
21.289 - in
21.290 - Obtain (qs, xs, l, t, by) :: do_steps subst depth next steps
21.291 - end
21.292 + in Obtain (qs, xs, l, t, by) :: do_steps subst depth next steps end
21.293 | do_steps subst depth next (Prove (qs, l, t, by) :: steps) =
21.294 let
21.295 val (l, subst, next) =
21.296 (l, subst, next) |> fresh_label depth have_prefix
21.297 val by = by |> do_byline subst depth
21.298 - in
21.299 - Prove (qs, l, t, by) :: do_steps subst depth next steps
21.300 - end
21.301 + in Prove (qs, l, t, by) :: do_steps subst depth next steps end
21.302 | do_steps subst depth next (step :: steps) =
21.303 step :: do_steps subst depth next steps
21.304 and do_proof subst depth (Proof (fix, assms, steps)) =
21.305 @@ -646,7 +610,7 @@
21.306 if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0)
21.307 else ([], lfs)
21.308 fun chain_step lbl (Obtain (qs, xs, l, t,
21.309 - By_Metis (subproofs, (lfs, gfs)))) =
21.310 + By_Metis (subproofs, (lfs, gfs)))) =
21.311 let val (qs', lfs) = do_qs_lfs lbl lfs in
21.312 Obtain (qs' @ qs, xs, l, t,
21.313 By_Metis (chain_proofs subproofs, (lfs, gfs)))
21.314 @@ -701,31 +665,30 @@
21.315 val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
21.316 val conjs =
21.317 atp_proof |> map_filter
21.318 - (fn Inference_Step (name as (_, ss), _, _, _, []) =>
21.319 + (fn (name as (_, ss), _, _, _, []) =>
21.320 if member (op =) ss conj_name then SOME name else NONE
21.321 | _ => NONE)
21.322 val assms =
21.323 atp_proof |> map_filter
21.324 - (fn Inference_Step (name as (_, ss), _, _, _, []) =>
21.325 + (fn (name as (_, ss), _, _, _, []) =>
21.326 (case resolve_conjecture ss of
21.327 [j] =>
21.328 if j = length hyp_ts then NONE
21.329 else SOME (raw_label_for_name name, nth hyp_ts j)
21.330 | _ => NONE)
21.331 | _ => NONE)
21.332 - fun dep_of_step (Definition_Step _) = NONE
21.333 - | dep_of_step (Inference_Step (name, _, _, _, from)) =
21.334 - SOME (from, name)
21.335 + val bot = atp_proof |> List.last |> #1
21.336 val refute_graph =
21.337 - atp_proof |> map_filter dep_of_step |> make_refute_graph
21.338 + atp_proof
21.339 + |> map (fn (name, _, _, _, from) => (from, name))
21.340 + |> make_refute_graph bot
21.341 + |> fold (Atom_Graph.default_node o rpair ()) conjs
21.342 val axioms = axioms_of_refute_graph refute_graph conjs
21.343 val tainted = tainted_atoms_of_refute_graph refute_graph conjs
21.344 val is_clause_tainted = exists (member (op =) tainted)
21.345 - val bot = atp_proof |> List.last |> dep_of_step |> the |> snd
21.346 val steps =
21.347 Symtab.empty
21.348 - |> fold (fn Definition_Step _ => I (* FIXME *)
21.349 - | Inference_Step (name as (s, _), role, t, rule, _) =>
21.350 + |> fold (fn (name as (s, _), role, t, rule, _) =>
21.351 Symtab.update_new (s, (rule,
21.352 t |> (if is_clause_tainted [name] then
21.353 s_maybe_not role
21.354 @@ -750,9 +713,8 @@
21.355 in
21.356 case List.partition (can HOLogic.dest_not) lits of
21.357 (negs as _ :: _, pos as _ :: _) =>
21.358 - HOLogic.mk_imp
21.359 - (Library.foldr1 s_conj (map HOLogic.dest_not negs),
21.360 - Library.foldr1 s_disj pos)
21.361 + s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs),
21.362 + Library.foldr1 s_disj pos)
21.363 | _ => fold (curry s_disj) lits @{term False}
21.364 end
21.365 |> HOLogic.mk_Trueprop |> close_form
21.366 @@ -831,7 +793,7 @@
21.367 else
21.368 compress_proof debug ctxt type_enc lam_trans preplay
21.369 preplay_timeout
21.370 - (if isar_proofs then isar_compress else 1000.0))
21.371 + (if isar_proofs = SOME true then isar_compress else 1000.0))
21.372 |>> cleanup_labels_in_proof
21.373 val isar_text =
21.374 string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
21.375 @@ -839,25 +801,23 @@
21.376 in
21.377 case isar_text of
21.378 "" =>
21.379 - if isar_proofs then
21.380 + if isar_proofs = SOME true then
21.381 "\nNo structured proof available (proof too simple)."
21.382 else
21.383 ""
21.384 | _ =>
21.385 let
21.386 val msg =
21.387 + (if verbose then
21.388 + let
21.389 + val num_steps = add_metis_steps (steps_of_proof isar_proof) 0
21.390 + in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end
21.391 + else
21.392 + []) @
21.393 (if preplay then
21.394 [(if preplay_fail then "may fail, " else "") ^
21.395 Sledgehammer_Preplay.string_of_preplay_time preplay_time]
21.396 else
21.397 - []) @
21.398 - (if verbose then
21.399 - let
21.400 - val num_steps = add_metis_steps (steps_of_proof isar_proof) 0
21.401 - in
21.402 - [string_of_int num_steps ^ " step" ^ plural_s num_steps]
21.403 - end
21.404 - else
21.405 [])
21.406 in
21.407 "\n\nStructured proof "
21.408 @@ -870,15 +830,22 @@
21.409 isar_proof_of ()
21.410 else case try isar_proof_of () of
21.411 SOME s => s
21.412 - | NONE => if isar_proofs then
21.413 + | NONE => if isar_proofs = SOME true then
21.414 "\nWarning: The Isar proof construction failed."
21.415 else
21.416 ""
21.417 in one_line_proof ^ isar_proof end
21.418
21.419 +fun isar_proof_would_be_a_good_idea preplay =
21.420 + case preplay of
21.421 + Played (reconstr, _) => reconstr = SMT
21.422 + | Trust_Playable _ => true
21.423 + | Failed_to_Play _ => true
21.424 +
21.425 fun proof_text ctxt isar_proofs isar_params num_chained
21.426 (one_line_params as (preplay, _, _, _, _, _)) =
21.427 - (if case preplay of Failed_to_Play _ => true | _ => isar_proofs then
21.428 + (if isar_proofs = SOME true orelse
21.429 + (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
21.430 isar_proof_text ctxt isar_proofs isar_params
21.431 else
21.432 one_line_proof_text num_chained) one_line_params
22.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Feb 21 10:52:14 2013 +0100
22.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Feb 21 16:00:48 2013 +0100
22.3 @@ -98,7 +98,7 @@
22.4 |> Output.urgent_message
22.5 fun really_go () =
22.6 problem
22.7 - |> get_minimizing_isar_prover ctxt mode learn name params minimize_command
22.8 + |> get_minimizing_prover ctxt mode learn name params minimize_command
22.9 |> verbose
22.10 ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
22.11 print_used_facts used_facts used_from