1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Dec 05 14:26:56 2015 +0100
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Dec 05 16:09:41 2015 +0100
1.3 @@ -16,7 +16,7 @@
1.4 val trace : bool Config.T
1.5
1.6 type isar_params =
1.7 - bool * (string option * string option) * Time.time * real * bool * bool
1.8 + bool * (string option * string option) * Time.time * real option * bool * bool
1.9 * (term, string) atp_step list * thm
1.10
1.11 val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
1.12 @@ -30,6 +30,7 @@
1.13 open ATP_Problem
1.14 open ATP_Proof
1.15 open ATP_Proof_Reconstruct
1.16 +open ATP_Waldmeister
1.17 open Sledgehammer_Util
1.18 open Sledgehammer_Proof_Methods
1.19 open Sledgehammer_Isar_Proof
1.20 @@ -46,88 +47,121 @@
1.21
1.22 val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
1.23
1.24 +val e_definition_rule = "definition"
1.25 val e_skolemize_rule = "skolemize"
1.26 -val spass_pirate_datatype_rule = "DT"
1.27 +val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg"
1.28 +val pirate_datatype_rule = "DT"
1.29 +val satallax_skolemize_rule = "tab_ex"
1.30 val vampire_skolemisation_rule = "skolemisation"
1.31 -(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
1.32 -val z3_skolemize_rule = "sk"
1.33 -val z3_th_lemma_rule = "th-lemma"
1.34 +val veriT_la_generic_rule = "la_generic"
1.35 +val veriT_simp_arith_rule = "simp_arith"
1.36 +val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
1.37 +val veriT_tmp_skolemize_rule = "tmp_skolemize"
1.38 +val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize
1.39 +val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "")
1.40 +val zipperposition_cnf_rule = "cnf"
1.41
1.42 val skolemize_rules =
1.43 - [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
1.44 + [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
1.45 + spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_ite_elim_rule,
1.46 + veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule]
1.47 +
1.48 +fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule)
1.49 +val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix
1.50
1.51 val is_skolemize_rule = member (op =) skolemize_rules
1.52 -val is_arith_rule = String.isPrefix z3_th_lemma_rule
1.53 -val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule
1.54 +fun is_arith_rule rule =
1.55 + String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse
1.56 + rule = veriT_la_generic_rule
1.57 +val is_datatype_rule = String.isPrefix pirate_datatype_rule
1.58
1.59 fun raw_label_of_num num = (num, 0)
1.60
1.61 fun label_of_clause [(num, _)] = raw_label_of_num num
1.62 | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)
1.63
1.64 -fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
1.65 - | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))
1.66 +fun add_global_fact ss = apsnd (union (op =) ss)
1.67 +
1.68 +fun add_fact_of_dependency [(_, ss as _ :: _)] = add_global_fact ss
1.69 + | add_fact_of_dependency names = apfst (insert (op =) (label_of_clause names))
1.70
1.71 fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
1.72 (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
1.73 definitions. *)
1.74 - if role = Conjecture orelse role = Negated_Conjecture then line :: lines
1.75 - else if t aconv @{prop True} then map (replace_dependencies_in_line (name, [])) lines
1.76 - else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines
1.77 - else if role = Axiom then lines (* axioms (facts) need no proof lines *)
1.78 - else map (replace_dependencies_in_line (name, [])) lines
1.79 + if role = Conjecture orelse role = Negated_Conjecture then
1.80 + line :: lines
1.81 + else if t aconv @{prop True} then
1.82 + map (replace_dependencies_in_line (name, [])) lines
1.83 + else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then
1.84 + line :: lines
1.85 + else if role = Axiom then
1.86 + lines (* axioms (facts) need no proof lines *)
1.87 + else
1.88 + map (replace_dependencies_in_line (name, [])) lines
1.89 | add_line_pass1 line lines = line :: lines
1.90
1.91 -fun add_lines_pass2 res _ [] = rev res
1.92 - | add_lines_pass2 res prev_t ((line as (name, role, t, rule, deps)) :: lines) =
1.93 +fun add_lines_pass2 res [] = rev res
1.94 + | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) =
1.95 let
1.96 - fun looks_boring () =
1.97 - t aconv @{prop True} orelse t aconv @{prop False} orelse t aconv prev_t orelse
1.98 - length deps < 2
1.99 + fun normalize role =
1.100 + role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop)
1.101 +
1.102 + val norm_t = normalize role t
1.103 + val is_duplicate =
1.104 + exists (fn (prev_name, prev_role, prev_t, _, _) =>
1.105 + (prev_role = Hypothesis andalso prev_t aconv t) orelse
1.106 + (member (op =) deps prev_name andalso
1.107 + Term.aconv_untyped (normalize prev_role prev_t, norm_t)))
1.108 + res
1.109 +
1.110 + fun looks_boring () = t aconv @{prop False} orelse length deps < 2
1.111
1.112 fun is_skolemizing_line (_, _, _, rule', deps') =
1.113 is_skolemize_rule rule' andalso member (op =) deps' name
1.114 +
1.115 fun is_before_skolemize_rule () = exists is_skolemizing_line lines
1.116 in
1.117 - if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
1.118 - is_datatype_rule rule orelse null lines orelse not (looks_boring ()) orelse
1.119 - is_before_skolemize_rule () then
1.120 - add_lines_pass2 (line :: res) t lines
1.121 + if is_duplicate orelse
1.122 + (role = Plain andalso not (is_skolemize_rule rule) andalso
1.123 + not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso
1.124 + not (is_datatype_rule rule) andalso not (null lines) andalso looks_boring () andalso
1.125 + not (is_before_skolemize_rule ())) then
1.126 + add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
1.127 else
1.128 - add_lines_pass2 res t (map (replace_dependencies_in_line (name, deps)) lines)
1.129 + add_lines_pass2 (line :: res) lines
1.130 end
1.131
1.132 type isar_params =
1.133 - bool * (string option * string option) * Time.time * real * bool * bool
1.134 + bool * (string option * string option) * Time.time * real option * bool * bool
1.135 * (term, string) atp_step list * thm
1.136
1.137 val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
1.138 -val simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
1.139 +val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
1.140 val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
1.141
1.142 -val arith_methods = basic_arith_methods @ simp_based_methods @ basic_systematic_methods
1.143 +val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods
1.144 val datatype_methods = [Simp_Method, Simp_Size_Method]
1.145 -val systematic_methods0 = basic_systematic_methods @ basic_arith_methods @ simp_based_methods @
1.146 - [Metis_Method (SOME no_typesN, NONE)]
1.147 -val rewrite_methods = simp_based_methods @ basic_systematic_methods @ basic_arith_methods
1.148 -val skolem_methods = basic_systematic_methods
1.149 +val systematic_methods =
1.150 + basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @
1.151 + [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)]
1.152 +val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods
1.153 +val skolem_methods = Moura_Method :: systematic_methods
1.154
1.155 fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
1.156 - (one_line_params as ((_, one_line_play), banner, used_facts, minimize_command, subgoal,
1.157 - subgoal_count)) =
1.158 + (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
1.159 let
1.160 - val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
1.161 + val _ = if debug then writeln "Constructing Isar proof..." else ()
1.162
1.163 fun generate_proof_text () =
1.164 let
1.165 - val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof, goal) =
1.166 + val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) =
1.167 isar_params ()
1.168
1.169 - val systematic_methods = insert (op =) (Metis_Method alt_metis_args) systematic_methods0
1.170 + val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods
1.171
1.172 fun massage_methods (meths as meth :: _) =
1.173 if not try0 then [meth]
1.174 - else if smt_proofs = SOME true then SMT2_Method :: meths
1.175 + else if smt_proofs = SOME true then SMT_Method :: meths
1.176 else meths
1.177
1.178 val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
1.179 @@ -135,7 +169,10 @@
1.180 val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
1.181
1.182 val do_preplay = preplay_timeout <> Time.zeroTime
1.183 - val compress = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress
1.184 + val compress =
1.185 + (case compress of
1.186 + NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0
1.187 + | SOME n => n)
1.188
1.189 fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
1.190 fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
1.191 @@ -144,9 +181,8 @@
1.192 if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
1.193
1.194 val atp_proof =
1.195 - atp_proof
1.196 - |> rpair [] |-> fold_rev add_line_pass1
1.197 - |> add_lines_pass2 [] Term.dummy
1.198 + fold_rev add_line_pass1 atp_proof0 []
1.199 + |> add_lines_pass2 []
1.200
1.201 val conjs =
1.202 map_filter (fn (name, role, _, _, _) =>
1.203 @@ -169,7 +205,7 @@
1.204 val (lems, _) =
1.205 fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt
1.206
1.207 - val bot = atp_proof |> List.last |> #1
1.208 + val bot = #1 (List.last atp_proof)
1.209
1.210 val refute_graph =
1.211 atp_proof
1.212 @@ -194,28 +230,63 @@
1.213 I))))
1.214 atp_proof
1.215
1.216 + fun is_referenced_in_step _ (Let _) = false
1.217 + | is_referenced_in_step l (Prove (_, _, _, _, subs, (ls, _), _, _)) =
1.218 + member (op =) ls l orelse exists (is_referenced_in_proof l) subs
1.219 + and is_referenced_in_proof l (Proof (_, _, steps)) =
1.220 + exists (is_referenced_in_step l) steps
1.221 +
1.222 + fun insert_lemma_in_step lem
1.223 + (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, comment)) =
1.224 + let val l' = the (label_of_isar_step lem) in
1.225 + if member (op =) ls l' then
1.226 + [lem, step]
1.227 + else
1.228 + let val refs = map (is_referenced_in_proof l') subs in
1.229 + if length (filter I refs) = 1 then
1.230 + let
1.231 + val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs subs
1.232 + in
1.233 + [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)]
1.234 + end
1.235 + else
1.236 + [lem, step]
1.237 + end
1.238 + end
1.239 + and insert_lemma_in_steps lem [] = [lem]
1.240 + | insert_lemma_in_steps lem (step :: steps) =
1.241 + if is_referenced_in_step (the (label_of_isar_step lem)) step then
1.242 + insert_lemma_in_step lem step @ steps
1.243 + else
1.244 + step :: insert_lemma_in_steps lem steps
1.245 + and insert_lemma_in_proof lem (Proof (fix, assms, steps)) =
1.246 + Proof (fix, assms, insert_lemma_in_steps lem steps)
1.247 +
1.248 val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
1.249
1.250 - fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form
1.251 + val finish_off = close_form #> rename_bound_vars
1.252 +
1.253 + fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off
1.254 | prop_of_clause names =
1.255 let
1.256 - val lits = map (HOLogic.dest_Trueprop o snd)
1.257 - (map_filter (Symtab.lookup steps o fst) names)
1.258 + val lits =
1.259 + map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
1.260 in
1.261 (case List.partition (can HOLogic.dest_not) lits of
1.262 (negs as _ :: _, pos as _ :: _) =>
1.263 s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
1.264 | _ => fold (curry s_disj) lits @{term False})
1.265 end
1.266 - |> HOLogic.mk_Trueprop |> close_form
1.267 + |> HOLogic.mk_Trueprop |> finish_off
1.268
1.269 - fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show
1.270 + fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else []
1.271
1.272 fun isar_steps outer predecessor accum [] =
1.273 accum
1.274 |> (if tainted = [] then
1.275 + (* e.g., trivial, empty proof by Z3 *)
1.276 cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
1.277 - (the_list predecessor, []), massage_methods systematic_methods, ""))
1.278 + sort_facts (the_list predecessor, []), massage_methods systematic_methods', ""))
1.279 else
1.280 I)
1.281 |> rev
1.282 @@ -226,22 +297,28 @@
1.283 val rule = rule_of_clause_id id
1.284 val skolem = is_skolemize_rule rule
1.285
1.286 - val deps = fold add_fact_of_dependencies gamma ([], [])
1.287 + val deps = ([], [])
1.288 + |> fold add_fact_of_dependency gamma
1.289 + |> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext]
1.290 + |> sort_facts
1.291 val meths =
1.292 (if skolem then skolem_methods
1.293 else if is_arith_rule rule then arith_methods
1.294 else if is_datatype_rule rule then datatype_methods
1.295 - else systematic_methods)
1.296 + else systematic_methods')
1.297 |> massage_methods
1.298
1.299 - fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths, "")
1.300 + fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "")
1.301 fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
1.302 in
1.303 if is_clause_tainted c then
1.304 (case gamma of
1.305 [g] =>
1.306 if skolem andalso is_clause_tainted g then
1.307 - let val subproof = Proof (skolems_of ctxt (prop_of_clause g), [], rev accum) in
1.308 + let
1.309 + val skos = skolems_of ctxt (prop_of_clause g)
1.310 + val subproof = Proof (skos, [], rev accum)
1.311 + in
1.312 isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
1.313 end
1.314 else
1.315 @@ -249,8 +326,12 @@
1.316 | _ => steps_of_rest (prove [] deps))
1.317 else
1.318 steps_of_rest
1.319 - (if skolem then Prove ([], skolems_of ctxt t, l, t, [], deps, meths, "")
1.320 - else prove [] deps)
1.321 + (if skolem then
1.322 + (case skolems_of ctxt t of
1.323 + [] => prove [] deps
1.324 + | skos => Prove ([], skos, l, t, [], deps, meths, ""))
1.325 + else
1.326 + prove [] deps)
1.327 end
1.328 | isar_steps outer predecessor accum (Cases cases :: infs) =
1.329 let
1.330 @@ -260,23 +341,24 @@
1.331 val l = label_of_clause c
1.332 val t = prop_of_clause c
1.333 val step =
1.334 - Prove (maybe_show outer c [], [], l, t,
1.335 + Prove (maybe_show outer c, [], l, t,
1.336 map isar_case (filter_out (null o snd) cases),
1.337 - (the_list predecessor, []), massage_methods systematic_methods, "")
1.338 + sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")
1.339 in
1.340 isar_steps outer (SOME l) (step :: accum) infs
1.341 end
1.342 and isar_proof outer fix assms lems infs =
1.343 - Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
1.344 + Proof (fix, assms, fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs))
1.345
1.346 val trace = Config.get ctxt trace
1.347
1.348 val canonical_isar_proof =
1.349 refute_graph
1.350 - |> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
1.351 + |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph)
1.352 |> redirect_graph axioms tainted bot
1.353 - |> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
1.354 + |> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof)
1.355 |> isar_proof true params assms lems
1.356 + |> postprocess_isar_proof_remove_show_stuttering
1.357 |> postprocess_isar_proof_remove_unreferenced_steps I
1.358 |> relabel_isar_proof_canonically
1.359
1.360 @@ -318,18 +400,12 @@
1.361 (keep_fastest_method_of_isar_step (!preplay_data)
1.362 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
1.363 |> tap (trace_isar_proof "Minimized")
1.364 - (* It's not clear whether this is worth the trouble (and if so, "compress" has an
1.365 - unnatural semantics): *)
1.366 -(*
1.367 - |> minimize
1.368 - ? (compress_isar_proof ctxt compress preplay_timeout preplay_data
1.369 - #> tap (trace_isar_proof "Compressed again"))
1.370 -*)
1.371 |> `(preplay_outcome_of_isar_proof (!preplay_data))
1.372 ||> (comment_isar_proof comment_of
1.373 #> chain_isar_proof
1.374 #> kill_useless_labels_in_isar_proof
1.375 - #> relabel_isar_proof_nicely)
1.376 + #> relabel_isar_proof_nicely
1.377 + #> rationalize_obtains_in_isar_proofs ctxt)
1.378 in
1.379 (case add_isar_steps (steps_of_isar_proof isar_proof) 0 of
1.380 1 =>
1.381 @@ -338,12 +414,11 @@
1.382 (case isar_proof of
1.383 Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
1.384 let val used_facts' = filter (member (op =) gfs o fst) used_facts in
1.385 - ((meth, play_outcome), banner, used_facts', minimize_command, subgoal,
1.386 - subgoal_count)
1.387 + ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
1.388 end)
1.389 else
1.390 one_line_params) ^
1.391 - (if isar_proofs = SOME true then "\n(No structured proof available -- proof too simple.)"
1.392 + (if isar_proofs = SOME true then "\n(No Isar proof available.)"
1.393 else "")
1.394 | num_steps =>
1.395 let
1.396 @@ -352,7 +427,7 @@
1.397 (if do_preplay then [string_of_play_outcome play_outcome] else [])
1.398 in
1.399 one_line_proof_text ctxt 0 one_line_params ^
1.400 - "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
1.401 + "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
1.402 Active.sendback_markup [Markup.padding_command]
1.403 (string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
1.404 end)
1.405 @@ -370,12 +445,12 @@
1.406
1.407 fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
1.408 (case play of
1.409 - Played _ => meth = SMT2_Method andalso smt_proofs <> SOME true
1.410 + Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
1.411 | Play_Timed_Out time => Time.> (time, Time.zeroTime)
1.412 | Play_Failed => true)
1.413
1.414 fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
1.415 - (one_line_params as (preplay, _, _, _, _, _)) =
1.416 + (one_line_params as ((_, preplay), _, _, _)) =
1.417 (if isar_proofs = SOME true orelse
1.418 (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
1.419 isar_proof_text ctxt debug isar_proofs smt_proofs isar_params