1(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar.ML 2 Author: Jasmin Blanchette, TU Muenchen 3 Author: Steffen Juilf Smolka, TU Muenchen 4 5Isar proof reconstruction from ATP proofs. 6*) 7 8signature SLEDGEHAMMER_ISAR = 9sig 10 type atp_step_name = ATP_Proof.atp_step_name 11 type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step 12 type 'a atp_proof = 'a ATP_Proof.atp_proof 13 type stature = ATP_Problem_Generate.stature 14 type one_line_params = Sledgehammer_Proof_Methods.one_line_params 15 16 val trace : bool Config.T 17 18 type isar_params = 19 bool * (string option * string option) * Time.time * real option * bool * bool 20 * (term, string) atp_step list * thm 21 22 val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) -> 23 int -> one_line_params -> string 24end; 25 26structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = 27struct 28 29open ATP_Util 30open ATP_Problem 31open ATP_Problem_Generate 32open ATP_Proof 33open ATP_Proof_Reconstruct 34open Sledgehammer_Util 35open Sledgehammer_Proof_Methods 36open Sledgehammer_Isar_Proof 37open Sledgehammer_Isar_Preplay 38open Sledgehammer_Isar_Compress 39open Sledgehammer_Isar_Minimize 40 41structure String_Redirect = ATP_Proof_Redirect( 42 type key = atp_step_name 43 val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') 44 val string_of = fst) 45 46open String_Redirect 47 48val trace = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_isar_trace\<close> (K false) 49 50val e_definition_rule = "definition" 51val e_skolemize_rule = "skolemize" 52val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg" 53val pirate_datatype_rule = "DT" 54val satallax_skolemize_rule = "tab_ex" 55val vampire_skolemisation_rule = "skolemisation" 56val veriT_la_generic_rule = "la_generic" 57val veriT_simp_arith_rule = "simp_arith" 58val veriT_tmp_skolemize_rule = "tmp_skolemize" 59val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize 60val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "") 61val zipperposition_cnf_rule = "cnf" 62 63val skolemize_rules = 64 [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, 65 spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule, 66 zipperposition_cnf_rule] 67 68fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule) 69val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix 70 71val is_skolemize_rule = member (op =) skolemize_rules 72fun is_arith_rule rule = 73 String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse 74 rule = veriT_la_generic_rule 75val is_datatype_rule = String.isPrefix pirate_datatype_rule 76 77fun raw_label_of_num num = (num, 0) 78 79fun label_of_clause [(num, _)] = raw_label_of_num num 80 | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) 81 82fun add_global_fact ss = apsnd (union (op =) ss) 83 84fun add_fact_of_dependency [(_, ss as _ :: _)] = add_global_fact ss 85 | add_fact_of_dependency names = apfst (insert (op =) (label_of_clause names)) 86 87fun add_line_pass1 (line as (name, role, t, rule, [])) lines = 88 (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or 89 definitions. *) 90 if role = Conjecture orelse role = Negated_Conjecture then 91 line :: lines 92 else if t aconv \<^prop>\<open>True\<close> then 93 map (replace_dependencies_in_line (name, [])) lines 94 else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then 95 line :: lines 96 else if role = Axiom then 97 lines (* axioms (facts) need no proof lines *) 98 else 99 map (replace_dependencies_in_line (name, [])) lines 100 | add_line_pass1 line lines = line :: lines 101 102fun add_lines_pass2 res [] = rev res 103 | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) = 104 let 105 fun normalize role = 106 role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop) 107 108 val norm_t = normalize role t 109 val is_duplicate = 110 exists (fn (prev_name, prev_role, prev_t, _, _) => 111 (prev_role = Hypothesis andalso prev_t aconv t) orelse 112 (member (op =) deps prev_name andalso 113 Term.aconv_untyped (normalize prev_role prev_t, norm_t))) 114 res 115 116 fun looks_boring () = t aconv \<^prop>\<open>False\<close> orelse length deps < 2 117 118 fun is_skolemizing_line (_, _, _, rule', deps') = 119 is_skolemize_rule rule' andalso member (op =) deps' name 120 121 fun is_before_skolemize_rule () = exists is_skolemizing_line lines 122 in 123 if is_duplicate orelse 124 (role = Plain andalso not (is_skolemize_rule rule) andalso 125 not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso 126 not (is_datatype_rule rule) andalso not (null lines) andalso looks_boring () andalso 127 not (is_before_skolemize_rule ())) then 128 add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines) 129 else 130 add_lines_pass2 (line :: res) lines 131 end 132 133type isar_params = 134 bool * (string option * string option) * Time.time * real option * bool * bool 135 * (term, string) atp_step list * thm 136 137val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method] 138val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method] 139val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method] 140 141val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods 142val datatype_methods = [Simp_Method, Simp_Size_Method] 143val systematic_methods = 144 basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ 145 [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)] 146val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods 147val skolem_methods = Moura_Method :: systematic_methods 148 149fun isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params 150 (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = 151 let 152 val _ = if debug then writeln "Constructing Isar proof..." else () 153 154 fun generate_proof_text () = 155 let 156 val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) = 157 isar_params () 158 in 159 if null atp_proof0 then 160 one_line_proof_text ctxt 0 one_line_params 161 else 162 let 163 val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods 164 165 fun massage_methods (meths as meth :: _) = 166 if not try0 then [meth] 167 else if smt_proofs = SOME true then SMT_Method :: meths 168 else meths 169 170 val (params, _, concl_t) = strip_subgoal goal subgoal ctxt 171 val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params 172 val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd 173 174 val do_preplay = preplay_timeout <> Time.zeroTime 175 val compress = 176 (case compress of 177 NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0 178 | SOME n => n) 179 180 fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem 181 fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev 182 183 fun get_role keep_role ((num, _), role, t, rule, _) = 184 if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE 185 186 val atp_proof = 187 fold_rev add_line_pass1 atp_proof0 [] 188 |> add_lines_pass2 [] 189 190 val conjs = 191 map_filter (fn (name, role, _, _, _) => 192 if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE) 193 atp_proof 194 val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof 195 196 fun add_lemma ((l, t), rule) ctxt = 197 let 198 val (skos, meths) = 199 (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods) 200 else if is_arith_rule rule then ([], arith_methods) 201 else ([], rewrite_methods)) 202 ||> massage_methods 203 in 204 (Prove ([], skos, l, t, [], ([], []), meths, ""), 205 ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd)) 206 end 207 208 val (lems, _) = 209 fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt 210 211 val bot = #1 (List.last atp_proof) 212 213 val refute_graph = 214 atp_proof 215 |> map (fn (name, _, _, _, from) => (from, name)) 216 |> make_refute_graph bot 217 |> fold (Atom_Graph.default_node o rpair ()) conjs 218 219 val axioms = axioms_of_refute_graph refute_graph conjs 220 221 val tainted = tainted_atoms_of_refute_graph refute_graph conjs 222 val is_clause_tainted = exists (member (op =) tainted) 223 val steps = 224 Symtab.empty 225 |> fold (fn (name as (s, _), role, t, rule, _) => 226 Symtab.update_new (s, (rule, t 227 |> (if is_clause_tainted [name] then 228 HOLogic.dest_Trueprop 229 #> role <> Conjecture ? s_not 230 #> fold exists_of (map Var (Term.add_vars t [])) 231 #> HOLogic.mk_Trueprop 232 else 233 I)))) 234 atp_proof 235 236 fun is_referenced_in_step _ (Let _) = false 237 | is_referenced_in_step l (Prove (_, _, _, _, subs, (ls, _), _, _)) = 238 member (op =) ls l orelse exists (is_referenced_in_proof l) subs 239 and is_referenced_in_proof l (Proof (_, _, steps)) = 240 exists (is_referenced_in_step l) steps 241 242 fun insert_lemma_in_step lem 243 (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, comment)) = 244 let val l' = the (label_of_isar_step lem) in 245 if member (op =) ls l' then 246 [lem, step] 247 else 248 let val refs = map (is_referenced_in_proof l') subs in 249 if length (filter I refs) = 1 then 250 let 251 val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs 252 subs 253 in 254 [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)] 255 end 256 else 257 [lem, step] 258 end 259 end 260 and insert_lemma_in_steps lem [] = [lem] 261 | insert_lemma_in_steps lem (step :: steps) = 262 if is_referenced_in_step (the (label_of_isar_step lem)) step then 263 insert_lemma_in_step lem step @ steps 264 else 265 step :: insert_lemma_in_steps lem steps 266 and insert_lemma_in_proof lem (Proof (fix, assms, steps)) = 267 Proof (fix, assms, insert_lemma_in_steps lem steps) 268 269 val rule_of_clause_id = fst o the o Symtab.lookup steps o fst 270 271 val finish_off = close_form #> rename_bound_vars 272 273 fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off 274 | prop_of_clause names = 275 let 276 val lits = 277 map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names) 278 in 279 (case List.partition (can HOLogic.dest_not) lits of 280 (negs as _ :: _, pos as _ :: _) => 281 s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), 282 Library.foldr1 s_disj pos) 283 | _ => fold (curry s_disj) lits \<^term>\<open>False\<close>) 284 end 285 |> HOLogic.mk_Trueprop |> finish_off 286 287 fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else [] 288 289 fun isar_steps outer predecessor accum [] = 290 accum 291 |> (if tainted = [] then 292 (* e.g., trivial, empty proof by Z3 *) 293 cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], 294 sort_facts (the_list predecessor, []), massage_methods systematic_methods', 295 "")) 296 else 297 I) 298 |> rev 299 | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = 300 let 301 val l = label_of_clause c 302 val t = prop_of_clause c 303 val rule = rule_of_clause_id id 304 val skolem = is_skolemize_rule rule 305 306 val deps = ([], []) 307 |> fold add_fact_of_dependency gamma 308 |> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext] 309 |> sort_facts 310 val meths = 311 (if skolem then skolem_methods 312 else if is_arith_rule rule then arith_methods 313 else if is_datatype_rule rule then datatype_methods 314 else systematic_methods') 315 |> massage_methods 316 317 fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "") 318 fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs 319 in 320 if is_clause_tainted c then 321 (case gamma of 322 [g] => 323 if skolem andalso is_clause_tainted g then 324 let 325 val skos = skolems_of ctxt (prop_of_clause g) 326 val subproof = Proof (skos, [], rev accum) 327 in 328 isar_steps outer (SOME l) [prove [subproof] ([], [])] infs 329 end 330 else 331 steps_of_rest (prove [] deps) 332 | _ => steps_of_rest (prove [] deps)) 333 else 334 steps_of_rest 335 (if skolem then 336 (case skolems_of ctxt t of 337 [] => prove [] deps 338 | skos => Prove ([], skos, l, t, [], deps, meths, "")) 339 else 340 prove [] deps) 341 end 342 | isar_steps outer predecessor accum (Cases cases :: infs) = 343 let 344 fun isar_case (c, subinfs) = 345 isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs 346 val c = succedent_of_cases cases 347 val l = label_of_clause c 348 val t = prop_of_clause c 349 val step = 350 Prove (maybe_show outer c, [], l, t, 351 map isar_case (filter_out (null o snd) cases), 352 sort_facts (the_list predecessor, []), massage_methods systematic_methods', 353 "") 354 in 355 isar_steps outer (SOME l) (step :: accum) infs 356 end 357 and isar_proof outer fix assms lems infs = 358 Proof (fix, assms, 359 fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs)) 360 361 val trace = Config.get ctxt trace 362 363 val canonical_isar_proof = 364 refute_graph 365 |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph) 366 |> redirect_graph axioms tainted bot 367 |> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof) 368 |> isar_proof true params assms lems 369 |> postprocess_isar_proof_remove_show_stuttering 370 |> postprocess_isar_proof_remove_unreferenced_steps I 371 |> relabel_isar_proof_canonically 372 373 val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof 374 375 val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty 376 377 val _ = fold_isar_steps (fn meth => 378 K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) 379 (steps_of_isar_proof canonical_isar_proof) () 380 381 fun str_of_preplay_outcome outcome = 382 if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?" 383 fun str_of_meth l meth = 384 string_of_proof_method ctxt [] meth ^ " " ^ 385 str_of_preplay_outcome 386 (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) 387 fun comment_of l = map (str_of_meth l) #> commas 388 389 fun trace_isar_proof label proof = 390 if trace then 391 tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ 392 string_of_isar_proof ctxt subgoal subgoal_count 393 (comment_isar_proof comment_of proof) ^ "\n") 394 else 395 () 396 397 fun comment_of l (meth :: _) = 398 (case (verbose, 399 Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of 400 (false, Played _) => "" 401 | (_, outcome) => string_of_play_outcome outcome) 402 403 val (play_outcome, isar_proof) = 404 canonical_isar_proof 405 |> tap (trace_isar_proof "Original") 406 |> compress_isar_proof ctxt compress preplay_timeout preplay_data 407 |> tap (trace_isar_proof "Compressed") 408 |> postprocess_isar_proof_remove_unreferenced_steps 409 (keep_fastest_method_of_isar_step (!preplay_data) 410 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data) 411 |> tap (trace_isar_proof "Minimized") 412 |> `(preplay_outcome_of_isar_proof (!preplay_data)) 413 ||> (comment_isar_proof comment_of 414 #> chain_isar_proof 415 #> kill_useless_labels_in_isar_proof 416 #> relabel_isar_proof_nicely 417 #> rationalize_obtains_in_isar_proofs ctxt) 418 in 419 (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of 420 (0, 1) => 421 one_line_proof_text ctxt 0 422 (if is_less (play_outcome_ord (play_outcome, one_line_play)) then 423 (case isar_proof of 424 Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) => 425 let 426 val used_facts' = 427 map_filter (fn s => 428 if exists (fn (s', (sc, _)) => s' = s andalso sc = Chained) 429 used_facts then 430 NONE 431 else 432 SOME (s, (Global, General))) gfs 433 in 434 ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count) 435 end) 436 else 437 one_line_params) ^ 438 (if isar_proofs = SOME true then "\n(No Isar proof available.)" else "") 439 | (_, num_steps) => 440 let 441 val msg = 442 (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] 443 else []) @ 444 (if do_preplay then [string_of_play_outcome play_outcome] else []) 445 in 446 one_line_proof_text ctxt 0 one_line_params ^ 447 "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ 448 Active.sendback_markup_command 449 (string_of_isar_proof ctxt subgoal subgoal_count isar_proof) 450 end) 451 end 452 end 453 in 454 if debug then 455 generate_proof_text () 456 else 457 (case try generate_proof_text () of 458 SOME s => s 459 | NONE => 460 one_line_proof_text ctxt 0 one_line_params ^ 461 (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else "")) 462 end 463 464fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) = 465 (case play of 466 Played _ => meth = SMT_Method andalso smt_proofs <> SOME true 467 | Play_Timed_Out time => time > Time.zeroTime 468 | Play_Failed => true) 469 470fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained 471 (one_line_params as ((_, preplay), _, _, _)) = 472 (if isar_proofs = SOME true orelse 473 (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then 474 isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params 475 else 476 one_line_proof_text ctxt num_chained) one_line_params 477 478end; 479