# HG changeset patch # User blanchet # Date 1350406253 -7200 # Node ID d9d73ebf9274738b1aedefa04d0975e4ef4c016c # Parent d7917ec162888bf0f21acb19e1993690ad988c93 added proof minimization code from Steffen Smolka diff -r d7917ec16288 -r d9d73ebf9274 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Tue Oct 16 18:07:59 2012 +0200 +++ b/src/HOL/Sledgehammer.thy Tue Oct 16 18:50:53 2012 +0200 @@ -14,6 +14,7 @@ ML_file "Tools/Sledgehammer/async_manager.ML" ML_file "Tools/Sledgehammer/sledgehammer_util.ML" ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" +ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML" ML_file "Tools/Sledgehammer/sledgehammer_provers.ML" ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML" ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML" diff -r d7917ec16288 -r d9d73ebf9274 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Oct 16 18:07:59 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Oct 16 18:50:53 2012 +0200 @@ -13,6 +13,8 @@ type 'a proof = 'a ATP_Proof.proof type stature = ATP_Problem_Generate.stature + structure String_Redirect : ATP_PROOF_REDIRECT + datatype reconstructor = Metis of string * string | SMT @@ -61,10 +63,50 @@ val prop_from_atp : Proof.context -> bool -> int Symtab.table -> (string, string, (string, string) ho_term, string) formula -> term - val isar_proof_text : - Proof.context -> bool -> isar_params -> one_line_params -> string - val proof_text : - Proof.context -> bool -> isar_params -> int -> one_line_params -> string + + type label + type facts = label list * string list + + datatype isar_qualifier = Show | Then | Moreover | Ultimately + + datatype isar_step = + Fix of (string * typ) list | + Let of term * term | + Assume of label * term | + Prove of isar_qualifier list * label * term * byline + and byline = + By_Metis of facts | + Case_Split of isar_step list list * facts + + val string_for_label : label -> string + val decode_lines : + Proof.context -> int Symtab.table + -> (string, string, (string, string) ATP_Problem.ho_term, string) + ATP_Problem.formula ATP_Proof.step list -> term ATP_Proof.step list + val add_line : + (string * 'a) list vector -> term ATP_Proof.step + -> term ATP_Proof.step list -> term ATP_Proof.step list + val repair_waldmeister_endgame : term ATP_Proof.step list -> term ATP_Proof.step list + val add_desired_line : + int -> (string * 'a) list vector -> (string * typ) list -> term ATP_Proof.step + -> int * term ATP_Proof.step list -> int * term ATP_Proof.step list + val add_nontrivial_line : + term ATP_Proof.step -> term ATP_Proof.step list -> term ATP_Proof.step list + val forall_of : term -> term -> term + val raw_label_for_name : string * string list -> string * int + + val no_label : label + val indent_size : int + val reconstructor_command : + reconstructor -> int -> int -> string list -> int + -> (string * int) list * string list -> string + val repair_name : string -> string + val add_fact_from_dependency : + (string * 'a) list vector -> string * string list + -> (string * int) list * string list -> (string * int) list * string list + val kill_duplicate_assumptions_in_proof : isar_step list -> isar_step list + val kill_useless_labels_in_proof : isar_step list -> isar_step list + val relabel_proof : isar_step list -> isar_step list end; structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT = @@ -833,313 +875,4 @@ step :: aux subst depth nextp proof in aux [] 0 (1, 1) end - -(** Type annotations **) - -fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s - | post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s - | post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s - | post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s - | post_traverse_term_type' f env (Abs (x, T1, b)) s = - let - val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s - in f (Abs (x, T1, b')) (T1 --> T2) s' end - | post_traverse_term_type' f env (u $ v) s = - let - val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s - val ((v', s''), _) = post_traverse_term_type' f env v s' - in f (u' $ v') T s'' end - -fun post_traverse_term_type f s t = - post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst -fun post_fold_term_type f s t = - post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd - -(* Data structures, orders *) -val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord) - -structure Var_Set_Tab = Table( - type key = indexname list - val ord = list_ord Term_Ord.fast_indexname_ord) - -(* (1) Generalize Types *) -fun generalize_types ctxt t = - t |> map_types (fn _ => dummyT) - |> Syntax.check_term - (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) - -(* (2) Typing-spot Table *) -local -fun key_of_atype (TVar (idxn, _)) = - Ord_List.insert Term_Ord.fast_indexname_ord idxn - | key_of_atype _ = I -fun key_of_type T = fold_atyps key_of_atype T [] -fun update_tab t T (tab, pos) = - (case key_of_type T of - [] => tab - | key => - let val cost = (size_of_typ T, (size_of_term t, pos)) in - case Var_Set_Tab.lookup tab key of - NONE => Var_Set_Tab.update_new (key, cost) tab - | SOME old_cost => - (case cost_ord (cost, old_cost) of - LESS => Var_Set_Tab.update (key, cost) tab - | _ => tab) - end, - pos + 1) -in -val typing_spot_table = - post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst -end - -(* (3) Reverse-Greedy *) -fun reverse_greedy typing_spot_tab = - let - fun update_count z = - fold (fn tvar => fn tab => - let val c = Vartab.lookup tab tvar |> the_default 0 in - Vartab.update (tvar, c + z) tab - end) - fun superfluous tcount = - forall (fn tvar => the (Vartab.lookup tcount tvar) > 1) - fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) = - if superfluous tcount tvars then (spots, update_count ~1 tvars tcount) - else (spot :: spots, tcount) - val (typing_spots, tvar_count_tab) = - Var_Set_Tab.fold - (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k)) - typing_spot_tab ([], Vartab.empty) - |>> sort_distinct (rev_order o cost_ord o pairself snd) - in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end - -(* (4) Introduce Annotations *) -fun introduce_annotations thy spots t t' = - let - val get_types = post_fold_term_type (K cons) [] - fun match_types tp = - fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty - fun unica' b x [] = if b then [x] else [] - | unica' b x (y :: ys) = - if x = y then unica' false x ys - else unica' true y ys |> b ? cons x - fun unica ord xs = - case sort ord xs of x :: ys => unica' true x ys | [] => [] - val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x | _ => I) - fun erase_unica_tfrees env = - let - val unica = - Vartab.fold (add_all_tfree_namesT o snd o snd) env [] - |> unica fast_string_ord - val erase_unica = map_atyps - (fn T as TFree (s, _) => - if Ord_List.member fast_string_ord unica s then dummyT else T - | T => T) - in Vartab.map (K (apsnd erase_unica)) env end - val env = match_types (t', t) |> erase_unica_tfrees - fun get_annot env (TFree _) = (false, (env, dummyT)) - | get_annot env (T as TVar (v, S)) = - let val T' = Envir.subst_type env T in - if T' = dummyT then (false, (env, dummyT)) - else (true, (Vartab.update (v, (S, dummyT)) env, T')) - end - | get_annot env (Type (S, Ts)) = - (case fold_rev (fn T => fn (b, (env, Ts)) => - let - val (b', (env', T)) = get_annot env T - in (b orelse b', (env', T :: Ts)) end) - Ts (false, (env, [])) of - (true, (env', Ts)) => (true, (env', Type (S, Ts))) - | (false, (env', _)) => (false, (env', dummyT))) - fun post1 _ T (env, cp, ps as p :: ps', annots) = - if p <> cp then - (env, cp + 1, ps, annots) - else - let val (_, (env', T')) = get_annot env T in - (env', cp + 1, ps', (p, T') :: annots) - end - | post1 _ _ accum = accum - val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t' - fun post2 t _ (cp, annots as (p, T) :: annots') = - if p <> cp then (t, (cp + 1, annots)) - else (Type.constraint T t, (cp + 1, annots')) - | post2 t _ x = (t, x) - in post_traverse_term_type post2 (0, rev annots) t |> fst end - -(* (5) Annotate *) -fun annotate_types ctxt t = - let - val thy = Proof_Context.theory_of ctxt - val t' = generalize_types ctxt t - val typing_spots = - t' |> typing_spot_table - |> reverse_greedy - |> sort int_ord - in introduce_annotations thy typing_spots t t' end - -fun string_for_proof ctxt type_enc lam_trans i n = - let - fun fix_print_mode f x = - Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) - (print_mode_value ())) f x - fun do_indent ind = replicate_string (ind * indent_size) " " - fun do_free (s, T) = - maybe_quote s ^ " :: " ^ - maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T) - fun do_label l = if l = no_label then "" else string_for_label l ^ ": " - fun do_have qs = - (if member (op =) qs Moreover then "moreover " else "") ^ - (if member (op =) qs Ultimately then "ultimately " else "") ^ - (if member (op =) qs Then then - if member (op =) qs Show then "thus" else "hence" - else - if member (op =) qs Show then "show" else "have") - val do_term = - maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) - o annotate_types ctxt - val reconstr = Metis (type_enc, lam_trans) - fun do_facts (ls, ss) = - reconstructor_command reconstr 1 1 [] 0 - (ls |> sort_distinct (prod_ord string_ord int_ord), - ss |> sort_distinct string_ord) - and do_step ind (Fix xs) = - do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" - | do_step ind (Let (t1, t2)) = - do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" - | do_step ind (Assume (l, t)) = - do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" - | do_step ind (Prove (qs, l, t, By_Metis facts)) = - do_indent ind ^ do_have qs ^ " " ^ - do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n" - | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) = - implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind) - proofs) ^ - do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^ - do_facts facts ^ "\n" - and do_steps prefix suffix ind steps = - let val s = implode (map (do_step ind) steps) in - replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ - String.extract (s, ind * indent_size, - SOME (size s - ind * indent_size - 1)) ^ - suffix ^ "\n" - end - and do_block ind proof = do_steps "{ " " }" (ind + 1) proof - (* One-step proofs are pointless; better use the Metis one-liner - directly. *) - and do_proof [Prove (_, _, _, By_Metis _)] = "" - | do_proof proof = - (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ - do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^ - (if n <> 1 then "next" else "qed") - in do_proof end - -fun isar_proof_text ctxt isar_proof_requested - (debug, isar_shrink_factor, pool, fact_names, sym_tab, atp_proof, goal) - (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = - let - val isar_shrink_factor = - (if isar_proof_requested then 1 else 2) * isar_shrink_factor - val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal - val frees = fold Term.add_frees (concl_t :: hyp_ts) [] - val one_line_proof = one_line_proof_text 0 one_line_params - val type_enc = - if is_typed_helper_used_in_atp_proof atp_proof then full_typesN - else partial_typesN - val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans - - fun isar_proof_of () = - let - val atp_proof = - atp_proof - |> clean_up_atp_proof_dependencies - |> nasty_atp_proof pool - |> map_term_names_in_atp_proof repair_name - |> decode_lines ctxt sym_tab - |> rpair [] |-> fold_rev (add_line fact_names) - |> repair_waldmeister_endgame - |> rpair [] |-> fold_rev add_nontrivial_line - |> rpair (0, []) - |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees) - |> snd - val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts) - val conjs = - atp_proof - |> map_filter (fn Inference_Step (name as (_, ss), _, _, []) => - if member (op =) ss conj_name then SOME name else NONE - | _ => NONE) - fun dep_of_step (Definition_Step _) = NONE - | dep_of_step (Inference_Step (name, _, _, from)) = SOME (from, name) - val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph - val axioms = axioms_of_ref_graph ref_graph conjs - val tainted = tainted_atoms_of_ref_graph ref_graph conjs - val props = - Symtab.empty - |> fold (fn Definition_Step _ => I (* FIXME *) - | Inference_Step ((s, _), t, _, _) => - Symtab.update_new (s, - t |> fold forall_of (map Var (Term.add_vars t [])) - |> member (op = o apsnd fst) tainted s ? s_not)) - atp_proof - fun prop_of_clause c = - fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c) - @{term False} - fun label_of_clause [name] = raw_label_for_name name - | label_of_clause c = (space_implode "___" (map fst c), 0) - fun maybe_show outer c = - (outer andalso length c = 1 andalso subset (op =) (c, conjs)) - ? cons Show - fun do_have outer qs (gamma, c) = - Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c, - By_Metis (fold (add_fact_from_dependency fact_names - o the_single) gamma ([], []))) - fun do_inf outer (Have z) = do_have outer [] z - | do_inf outer (Hence z) = do_have outer [Then] z - | do_inf outer (Cases cases) = - let val c = succedent_of_cases cases in - Prove (maybe_show outer c [Ultimately], label_of_clause c, - prop_of_clause c, - Case_Split (map (do_case false) cases, ([], []))) - end - and do_case outer (c, infs) = - Assume (label_of_clause c, prop_of_clause c) :: - map (do_inf outer) infs - val isar_proof = - (if null params then [] else [Fix params]) @ - (ref_graph - |> redirect_graph axioms tainted - |> chain_direct_proof - |> map (do_inf true) - |> kill_duplicate_assumptions_in_proof - |> kill_useless_labels_in_proof - |> relabel_proof) - |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count - in - case isar_proof of - "" => - if isar_proof_requested then - "\nNo structured proof available (proof too short)." - else - "" - | _ => - "\n\n" ^ (if isar_proof_requested then "Structured proof" - else "Perhaps this will work") ^ - ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_proof - end - val isar_proof = - if debug then - isar_proof_of () - else case try isar_proof_of () of - SOME s => s - | NONE => if isar_proof_requested then - "\nWarning: The Isar proof construction failed." - else - "" - in one_line_proof ^ isar_proof end - -fun proof_text ctxt isar_proof isar_params num_chained - (one_line_params as (preplay, _, _, _, _, _)) = - (if case preplay of Failed_to_Play _ => true | _ => isar_proof then - isar_proof_text ctxt isar_proof isar_params - else - one_line_proof_text num_chained) one_line_params - end; diff -r d7917ec16288 -r d9d73ebf9274 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Oct 16 18:07:59 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Oct 16 18:50:53 2012 +0200 @@ -149,6 +149,7 @@ open ATP_Proof_Reconstruct open Metis_Tactic open Sledgehammer_Util +open Sledgehammer_Reconstruct (** The Sledgehammer **)