# HG changeset patch # User blanchet # Date 1277116301 -7200 # Node ID f6b1ee5b420bdc7c749a838f1b08d964e33b8614 # Parent d8dd5a4403d27bb366bd4ce4cd211f4205041607 try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better diff -r d8dd5a4403d2 -r f6b1ee5b420b src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jun 21 12:28:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jun 21 12:31:41 2010 +0200 @@ -611,7 +611,8 @@ (* Translation of HO Clauses *) (* ------------------------------------------------------------------------- *) -fun cnf_th thy th = hd (cnf_axiom thy th); +fun cnf_helper_theorem thy raw th = + if raw then th else the_single (cnf_axiom thy th) fun type_ext thy tms = let val subs = tfree_classes_of_terms tms @@ -661,6 +662,17 @@ | string_of_mode HO = "HO" | string_of_mode FT = "FT" +val helpers = + [("c_COMBI", (false, @{thms COMBI_def})), + ("c_COMBK", (false, @{thms COMBK_def})), + ("c_COMBB", (false, @{thms COMBB_def})), + ("c_COMBC", (false, @{thms COMBC_def})), + ("c_COMBS", (false, @{thms COMBS_def})), + ("c_fequal", (false, @{thms fequal_imp_equal equal_imp_fequal})), + ("c_True", (true, @{thms True_or_False})), + ("c_False", (true, @{thms True_or_False})), + ("c_If", (true, @{thms if_True if_False True_or_False}))] + (* Function to generate metis clauses, including comb and type clauses *) fun build_map mode0 ctxt cls ths = let val thy = ProofContext.theory_of ctxt @@ -688,17 +700,21 @@ |> add_tfrees |> fold (add_thm false) ths val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) - fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists - (*Now check for the existence of certain combinators*) - val thI = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else [] - val thK = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else [] - val thB = if used "c_COMBB" then [cnf_th @{theory} @{thm COMBB_def}] else [] - val thC = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else [] - val thS = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else [] - val thEQ = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else [] + fun is_used c = + exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists val lmap = - lmap |> mode <> FO - ? fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) + if mode = FO then + lmap + else + let + val helper_ths = + helpers |> filter (is_used o fst) + |> maps (fn (_, (raw, thms)) => + if mode = FT orelse not raw then + map (cnf_helper_theorem @{theory} raw) thms + else + []) + in lmap |> fold (add_thm false) helper_ths end in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end fun refute cls = diff -r d8dd5a4403d2 -r f6b1ee5b420b src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jun 21 12:28:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jun 21 12:31:41 2010 +0200 @@ -27,7 +27,8 @@ -> Proof.context * (thm list * 'a) -> thm list -> (thm * (string * int)) list val prepare_clauses : - bool -> thm list -> thm list -> (thm * (axiom_name * hol_clause_id)) list + bool -> bool -> thm list -> thm list + -> (thm * (axiom_name * hol_clause_id)) list -> (thm * (axiom_name * hol_clause_id)) list -> theory -> axiom_name vector * (hol_clause list * hol_clause list * hol_clause list * @@ -565,7 +566,7 @@ (* prepare for passing to writer, create additional clauses based on the information from extra_cls *) -fun prepare_clauses dfg goal_cls chained_ths axcls extra_cls thy = +fun prepare_clauses dfg full_types goal_cls chained_ths axcls extra_cls thy = let val is_FO = is_fol_goal thy goal_cls val ccls = subtract_cls extra_cls goal_cls @@ -579,7 +580,8 @@ val conjectures = make_conjecture_clauses dfg thy ccls val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls) val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls) - val helper_clauses = get_helper_clauses dfg thy is_FO conjectures extra_cls + val helper_clauses = + get_helper_clauses dfg thy is_FO full_types conjectures extra_cls val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers val classrel_clauses = make_classrel_clauses thy subs supers' in diff -r d8dd5a4403d2 -r f6b1ee5b420b src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Jun 21 12:28:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Jun 21 12:31:41 2010 +0200 @@ -111,9 +111,8 @@ in (SOME min_thms, proof_text isar_proof - (pool, debug, full_types, isar_shrink_factor, ctxt, - conjecture_shape) - (K "", proof, internal_thm_names, goal, i) |> fst) + (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) + (full_types, K "", proof, internal_thm_names, goal, i) |> fst) end | {outcome = SOME TimedOut, ...} => (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ @@ -126,7 +125,8 @@ \option (e.g., \"timeout = " ^ string_of_int (10 + msecs div 1000) ^ " s\").") | {message, ...} => (NONE, "ATP error: " ^ message)) - handle Sledgehammer_HOL_Clause.TRIVIAL => (SOME [], metis_line i n []) + handle Sledgehammer_HOL_Clause.TRIVIAL => + (SOME [], metis_line full_types i n []) | ERROR msg => (NONE, "Error: " ^ msg) end diff -r d8dd5a4403d2 -r f6b1ee5b420b src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Jun 21 12:28:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Jun 21 12:31:41 2010 +0200 @@ -111,7 +111,7 @@ fun union_all xss = fold (union (op =)) xss [] (* Readable names for the more common symbolic functions. Do not mess with the - last six entries of the table unless you know what you are doing. *) + last nine entries of the table unless you know what you are doing. *) val const_trans_table = Symtab.make [(@{const_name "op ="}, "equal"), (@{const_name "op &"}, "and"), @@ -123,7 +123,10 @@ (@{const_name COMBK}, "COMBK"), (@{const_name COMBB}, "COMBB"), (@{const_name COMBC}, "COMBC"), - (@{const_name COMBS}, "COMBS")] + (@{const_name COMBS}, "COMBS"), + (@{const_name True}, "True"), + (@{const_name False}, "False"), + (@{const_name If}, "If")] val type_const_trans_table = Symtab.make [(@{type_name "*"}, "prod"), diff -r d8dd5a4403d2 -r f6b1ee5b420b src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Jun 21 12:28:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Jun 21 12:31:41 2010 +0200 @@ -37,7 +37,7 @@ (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list val type_wrapper_name : string val get_helper_clauses : - bool -> theory -> bool -> hol_clause list + bool -> theory -> bool -> bool -> hol_clause list -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list val write_tptp_file : bool -> bool -> bool -> Path.T -> hol_clause list * hol_clause list * hol_clause list * hol_clause list * @@ -54,13 +54,13 @@ open Sledgehammer_FOL_Clause open Sledgehammer_Fact_Preprocessor -fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c); +fun min_arity_of const_min_arity c = + the_default 0 (Symtab.lookup const_min_arity c) (*True if the constant ever appears outside of the top-level position in literals. If false, the constant always receives all of its arguments and is used as a predicate.*) fun needs_hBOOL explicit_apply const_needs_hBOOL c = - explicit_apply orelse - the_default false (Symtab.lookup const_needs_hBOOL c); + explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c) (******************************************************) @@ -452,10 +452,6 @@ (* write clauses to files *) (**********************************************************************) -val init_counters = - Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0), - ("c_COMBS", 0)]; - fun count_combterm (CombConst ((c, _), _, _)) = Symtab.map_entry c (Integer.add 1) | count_combterm (CombVar _) = I @@ -465,28 +461,37 @@ fun count_clause (HOLClause {literals, ...}) = fold count_literal literals -fun cnf_helper_thms thy = cnf_rules_pairs thy o map (`Thm.get_name_hint) +val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, (name, 0))) +fun cnf_helper_thms thy raw = + map (`Thm.get_name_hint) + #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy) + +val optional_helpers = + [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})), + (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})), + (["c_COMBS"], (false, @{thms COMBS_def}))] +val optional_typed_helpers = + [(["c_True", "c_False"], (true, @{thms True_or_False})), + (["c_If"], (true, @{thms if_True if_False True_or_False}))] +val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} -fun get_helper_clauses dfg thy isFO conjectures axcls = - if isFO then - [] - else - let - val axclauses = map snd (make_axiom_clauses dfg thy axcls) - val ct = init_counters - |> fold (fold count_clause) [conjectures, axclauses] - fun needed c = the (Symtab.lookup ct c) > 0 - val IK = if needed "c_COMBI" orelse needed "c_COMBK" - then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}] - else [] - val BC = if needed "c_COMBB" orelse needed "c_COMBC" - then cnf_helper_thms thy [@{thm COMBB_def}, @{thm COMBC_def}] - else [] - val S = if needed "c_COMBS" then cnf_helper_thms thy [@{thm COMBS_def}] - else [] - val other = cnf_helper_thms thy [@{thm fequal_imp_equal}, - @{thm equal_imp_fequal}] - in map snd (make_axiom_clauses dfg thy (other @ IK @ BC @ S)) end +val init_counters = + Symtab.make (maps (maps (map (rpair 0) o fst)) + [optional_helpers, optional_typed_helpers]) + +fun get_helper_clauses dfg thy is_FO full_types conjectures axcls = + let + val axclauses = map snd (make_axiom_clauses dfg thy axcls) + val ct = fold (fold count_clause) [conjectures, axclauses] init_counters + fun is_needed c = the (Symtab.lookup ct c) > 0 + val cnfs = + (optional_helpers + |> full_types ? append optional_typed_helpers + |> maps (fn (ss, (raw, ths)) => + if exists is_needed ss then cnf_helper_thms thy raw ths + else [])) + @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers) + in map snd (make_axiom_clauses dfg thy cnfs) end (*Find the minimal arity of each function mentioned in the term. Also, note which uses are not at top level, to see if hBOOL is needed.*) diff -r d8dd5a4403d2 -r f6b1ee5b420b src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jun 21 12:28:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jun 21 12:31:41 2010 +0200 @@ -14,17 +14,17 @@ val invert_type_const: string -> string val num_type_args: theory -> string -> int val strip_prefix: string -> string -> string option - val metis_line: int -> int -> string list -> string + val metis_line: bool -> int -> int -> string list -> string val metis_proof_text: - minimize_command * string * string vector * thm * int + bool * minimize_command * string * string vector * thm * int -> string * string list val isar_proof_text: - name_pool option * bool * bool * int * Proof.context * int list list - -> minimize_command * string * string vector * thm * int + name_pool option * bool * int * Proof.context * int list list + -> bool * minimize_command * string * string vector * thm * int -> string * string list val proof_text: - bool -> name_pool option * bool * bool * int * Proof.context * int list list - -> minimize_command * string * string vector * thm * int + bool -> name_pool option * bool * int * Proof.context * int list list + -> bool * minimize_command * string * string vector * thm * int -> string * string list end; @@ -600,13 +600,15 @@ fun metis_apply _ 1 = "by " | metis_apply 1 _ = "apply " | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply " -fun metis_itself [] = "metis" - | metis_itself ss = "(metis " ^ space_implode " " ss ^ ")" -fun metis_command i n (ls, ss) = - metis_using ls ^ metis_apply i n ^ metis_itself ss -fun metis_line i n ss = +fun metis_name full_types = if full_types then "metisFT" else "metis" +fun metis_call full_types [] = metis_name full_types + | metis_call full_types ss = + "(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")" +fun metis_command full_types i n (ls, ss) = + metis_using ls ^ metis_apply i n ^ metis_call full_types ss +fun metis_line full_types i n ss = "Try this command: " ^ - Markup.markup Markup.sendback (metis_command i n ([], ss)) ^ ".\n" + Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ ".\n" fun minimize_line _ [] = "" | minimize_line minimize_command facts = case minimize_command facts of @@ -617,7 +619,8 @@ val unprefix_chained = perhaps (try (unprefix chained_prefix)) -fun metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) = +fun metis_proof_text (full_types, minimize_command, atp_proof, thm_names, goal, + i) = let val raw_lemmas = atp_proof |> extract_clause_numbers_in_atp_proof @@ -630,8 +633,8 @@ val lemmas = other_lemmas @ chained_lemmas val n = Logic.count_prems (prop_of goal) in - (metis_line i n other_lemmas ^ minimize_line minimize_command lemmas, - lemmas) + (metis_line full_types i n other_lemmas ^ + minimize_line minimize_command lemmas, lemmas) end (** Isar proof construction and manipulation **) @@ -932,7 +935,7 @@ step :: aux subst depth nextp proof in aux [] 0 (1, 1) end -fun string_for_proof ctxt i n = +fun string_for_proof ctxt full_types i n = let fun fix_print_mode f x = setmp_CRITICAL show_no_free_types true @@ -956,7 +959,7 @@ let val ls = ls |> sort_distinct (prod_ord string_ord int_ord) val ss = ss |> map unprefix_chained |> sort_distinct string_ord - in metis_command 1 1 (ls, ss) end + in metis_command full_types 1 1 (ls, ss) end and do_step ind (Fix xs) = do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" | do_step ind (Let (t1, t2)) = @@ -989,17 +992,16 @@ do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n" in do_proof end -fun isar_proof_text (pool, debug, full_types, isar_shrink_factor, ctxt, - conjecture_shape) - (minimize_command, atp_proof, thm_names, goal, i) = +fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) + (other_params as (full_types, _, atp_proof, thm_names, goal, + i)) = let val thy = ProofContext.theory_of ctxt val (params, hyp_ts, concl_t) = strip_subgoal goal i val frees = fold Term.add_frees (concl_t :: hyp_ts) [] val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] val n = Logic.count_prems (prop_of goal) - val (one_line_proof, lemma_names) = - metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) + val (one_line_proof, lemma_names) = metis_proof_text other_params fun isar_proof_for () = case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor atp_proof conjecture_shape thm_names params @@ -1009,7 +1011,7 @@ |> then_chain_proof |> kill_useless_labels_in_proof |> relabel_proof - |> string_for_proof ctxt i n of + |> string_for_proof ctxt full_types i n of "" => "" | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof val isar_proof =