try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
authorblanchet
Mon Jun 21 12:31:41 2010 +0200 (2010-06-21 ago)
changeset 37479f6b1ee5b420b
parent 37478 d8dd5a4403d2
child 37480 d5a85d35ef62
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Jun 21 12:28:46 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Jun 21 12:31:41 2010 +0200
     1.3 @@ -611,7 +611,8 @@
     1.4  (* Translation of HO Clauses                                                 *)
     1.5  (* ------------------------------------------------------------------------- *)
     1.6  
     1.7 -fun cnf_th thy th = hd (cnf_axiom thy th);
     1.8 +fun cnf_helper_theorem thy raw th =
     1.9 +  if raw then th else the_single (cnf_axiom thy th)
    1.10  
    1.11  fun type_ext thy tms =
    1.12    let val subs = tfree_classes_of_terms tms
    1.13 @@ -661,6 +662,17 @@
    1.14    | string_of_mode HO = "HO"
    1.15    | string_of_mode FT = "FT"
    1.16  
    1.17 +val helpers =
    1.18 +  [("c_COMBI", (false, @{thms COMBI_def})),
    1.19 +   ("c_COMBK", (false, @{thms COMBK_def})),
    1.20 +   ("c_COMBB", (false, @{thms COMBB_def})),
    1.21 +   ("c_COMBC", (false, @{thms COMBC_def})),
    1.22 +   ("c_COMBS", (false, @{thms COMBS_def})),
    1.23 +   ("c_fequal", (false, @{thms fequal_imp_equal equal_imp_fequal})),
    1.24 +   ("c_True", (true, @{thms True_or_False})),
    1.25 +   ("c_False", (true, @{thms True_or_False})),
    1.26 +   ("c_If", (true, @{thms if_True if_False True_or_False}))]
    1.27 +
    1.28  (* Function to generate metis clauses, including comb and type clauses *)
    1.29  fun build_map mode0 ctxt cls ths =
    1.30    let val thy = ProofContext.theory_of ctxt
    1.31 @@ -688,17 +700,21 @@
    1.32          |> add_tfrees
    1.33          |> fold (add_thm false) ths
    1.34        val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
    1.35 -      fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
    1.36 -      (*Now check for the existence of certain combinators*)
    1.37 -      val thI  = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else []
    1.38 -      val thK  = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else []
    1.39 -      val thB   = if used "c_COMBB" then [cnf_th @{theory} @{thm COMBB_def}] else []
    1.40 -      val thC   = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else []
    1.41 -      val thS   = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else []
    1.42 -      val thEQ  = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
    1.43 +      fun is_used c =
    1.44 +        exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
    1.45        val lmap =
    1.46 -        lmap |> mode <> FO
    1.47 -                ? fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI)
    1.48 +        if mode = FO then
    1.49 +          lmap
    1.50 +        else
    1.51 +          let
    1.52 +            val helper_ths =
    1.53 +              helpers |> filter (is_used o fst)
    1.54 +                      |> maps (fn (_, (raw, thms)) =>
    1.55 +                                  if mode = FT orelse not raw then
    1.56 +                                    map (cnf_helper_theorem @{theory} raw) thms
    1.57 +                                  else
    1.58 +                                    [])
    1.59 +          in lmap |> fold (add_thm false) helper_ths end
    1.60    in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
    1.61  
    1.62  fun refute cls =
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Jun 21 12:28:46 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Jun 21 12:31:41 2010 +0200
     2.3 @@ -27,7 +27,8 @@
     2.4      -> Proof.context * (thm list * 'a) -> thm list
     2.5      -> (thm * (string * int)) list
     2.6    val prepare_clauses :
     2.7 -    bool -> thm list -> thm list -> (thm * (axiom_name * hol_clause_id)) list
     2.8 +    bool -> bool -> thm list -> thm list
     2.9 +    -> (thm * (axiom_name * hol_clause_id)) list
    2.10      -> (thm * (axiom_name * hol_clause_id)) list -> theory
    2.11      -> axiom_name vector
    2.12         * (hol_clause list * hol_clause list * hol_clause list *
    2.13 @@ -565,7 +566,7 @@
    2.14  
    2.15  (* prepare for passing to writer,
    2.16     create additional clauses based on the information from extra_cls *)
    2.17 -fun prepare_clauses dfg goal_cls chained_ths axcls extra_cls thy =
    2.18 +fun prepare_clauses dfg full_types goal_cls chained_ths axcls extra_cls thy =
    2.19    let
    2.20      val is_FO = is_fol_goal thy goal_cls
    2.21      val ccls = subtract_cls extra_cls goal_cls
    2.22 @@ -579,7 +580,8 @@
    2.23      val conjectures = make_conjecture_clauses dfg thy ccls
    2.24      val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls)
    2.25      val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls)
    2.26 -    val helper_clauses = get_helper_clauses dfg thy is_FO conjectures extra_cls
    2.27 +    val helper_clauses =
    2.28 +      get_helper_clauses dfg thy is_FO full_types conjectures extra_cls
    2.29      val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers
    2.30      val classrel_clauses = make_classrel_clauses thy subs supers'
    2.31    in
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Jun 21 12:28:46 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Jun 21 12:31:41 2010 +0200
     3.3 @@ -111,9 +111,8 @@
     3.4          in
     3.5            (SOME min_thms,
     3.6             proof_text isar_proof
     3.7 -               (pool, debug, full_types, isar_shrink_factor, ctxt,
     3.8 -                conjecture_shape)
     3.9 -               (K "", proof, internal_thm_names, goal, i) |> fst)
    3.10 +               (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
    3.11 +               (full_types, K "", proof, internal_thm_names, goal, i) |> fst)
    3.12          end
    3.13      | {outcome = SOME TimedOut, ...} =>
    3.14          (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
    3.15 @@ -126,7 +125,8 @@
    3.16                 \option (e.g., \"timeout = " ^
    3.17                 string_of_int (10 + msecs div 1000) ^ " s\").")
    3.18      | {message, ...} => (NONE, "ATP error: " ^ message))
    3.19 -    handle Sledgehammer_HOL_Clause.TRIVIAL => (SOME [], metis_line i n [])
    3.20 +    handle Sledgehammer_HOL_Clause.TRIVIAL =>
    3.21 +           (SOME [], metis_line full_types i n [])
    3.22           | ERROR msg => (NONE, "Error: " ^ msg)
    3.23    end
    3.24  
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Jun 21 12:28:46 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Jun 21 12:31:41 2010 +0200
     4.3 @@ -111,7 +111,7 @@
     4.4  fun union_all xss = fold (union (op =)) xss []
     4.5  
     4.6  (* Readable names for the more common symbolic functions. Do not mess with the
     4.7 -   last six entries of the table unless you know what you are doing. *)
     4.8 +   last nine entries of the table unless you know what you are doing. *)
     4.9  val const_trans_table =
    4.10    Symtab.make [(@{const_name "op ="}, "equal"),
    4.11                 (@{const_name "op &"}, "and"),
    4.12 @@ -123,7 +123,10 @@
    4.13                 (@{const_name COMBK}, "COMBK"),
    4.14                 (@{const_name COMBB}, "COMBB"),
    4.15                 (@{const_name COMBC}, "COMBC"),
    4.16 -               (@{const_name COMBS}, "COMBS")]
    4.17 +               (@{const_name COMBS}, "COMBS"),
    4.18 +               (@{const_name True}, "True"),
    4.19 +               (@{const_name False}, "False"),
    4.20 +               (@{const_name If}, "If")]
    4.21  
    4.22  val type_const_trans_table =
    4.23    Symtab.make [(@{type_name "*"}, "prod"),
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Jun 21 12:28:46 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Jun 21 12:31:41 2010 +0200
     5.3 @@ -37,7 +37,7 @@
     5.4         (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
     5.5    val type_wrapper_name : string
     5.6    val get_helper_clauses :
     5.7 -    bool -> theory -> bool -> hol_clause list
     5.8 +    bool -> theory -> bool -> bool -> hol_clause list
     5.9        -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list
    5.10    val write_tptp_file : bool -> bool -> bool -> Path.T ->
    5.11      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    5.12 @@ -54,13 +54,13 @@
    5.13  open Sledgehammer_FOL_Clause
    5.14  open Sledgehammer_Fact_Preprocessor
    5.15  
    5.16 -fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
    5.17 +fun min_arity_of const_min_arity c =
    5.18 +  the_default 0 (Symtab.lookup const_min_arity c)
    5.19  
    5.20  (*True if the constant ever appears outside of the top-level position in literals.
    5.21    If false, the constant always receives all of its arguments and is used as a predicate.*)
    5.22  fun needs_hBOOL explicit_apply const_needs_hBOOL c =
    5.23 -  explicit_apply orelse
    5.24 -    the_default false (Symtab.lookup const_needs_hBOOL c);
    5.25 +  explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c)
    5.26  
    5.27  
    5.28  (******************************************************)
    5.29 @@ -452,10 +452,6 @@
    5.30  (* write clauses to files                                             *)
    5.31  (**********************************************************************)
    5.32  
    5.33 -val init_counters =
    5.34 -  Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0),
    5.35 -               ("c_COMBS", 0)];
    5.36 -
    5.37  fun count_combterm (CombConst ((c, _), _, _)) =
    5.38      Symtab.map_entry c (Integer.add 1)
    5.39    | count_combterm (CombVar _) = I
    5.40 @@ -465,28 +461,37 @@
    5.41  
    5.42  fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
    5.43  
    5.44 -fun cnf_helper_thms thy = cnf_rules_pairs thy o map (`Thm.get_name_hint)
    5.45 +val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, (name, 0)))
    5.46 +fun cnf_helper_thms thy raw =
    5.47 +  map (`Thm.get_name_hint)
    5.48 +  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
    5.49 +
    5.50 +val optional_helpers =
    5.51 +  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
    5.52 +   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
    5.53 +   (["c_COMBS"], (false, @{thms COMBS_def}))]
    5.54 +val optional_typed_helpers =
    5.55 +  [(["c_True", "c_False"], (true, @{thms True_or_False})),
    5.56 +   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
    5.57 +val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
    5.58  
    5.59 -fun get_helper_clauses dfg thy isFO conjectures axcls =
    5.60 -  if isFO then
    5.61 -    []
    5.62 -  else
    5.63 -    let
    5.64 -        val axclauses = map snd (make_axiom_clauses dfg thy axcls)
    5.65 -        val ct = init_counters
    5.66 -                 |> fold (fold count_clause) [conjectures, axclauses]
    5.67 -        fun needed c = the (Symtab.lookup ct c) > 0
    5.68 -        val IK = if needed "c_COMBI" orelse needed "c_COMBK"
    5.69 -                 then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
    5.70 -                 else []
    5.71 -        val BC = if needed "c_COMBB" orelse needed "c_COMBC"
    5.72 -                 then cnf_helper_thms thy [@{thm COMBB_def}, @{thm COMBC_def}]
    5.73 -                 else []
    5.74 -        val S = if needed "c_COMBS" then cnf_helper_thms thy [@{thm COMBS_def}]
    5.75 -                else []
    5.76 -        val other = cnf_helper_thms thy [@{thm fequal_imp_equal},
    5.77 -                                         @{thm equal_imp_fequal}]
    5.78 -    in map snd (make_axiom_clauses dfg thy (other @ IK @ BC @ S)) end
    5.79 +val init_counters =
    5.80 +  Symtab.make (maps (maps (map (rpair 0) o fst))
    5.81 +                    [optional_helpers, optional_typed_helpers])
    5.82 +
    5.83 +fun get_helper_clauses dfg thy is_FO full_types conjectures axcls =
    5.84 +  let
    5.85 +    val axclauses = map snd (make_axiom_clauses dfg thy axcls)
    5.86 +    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
    5.87 +    fun is_needed c = the (Symtab.lookup ct c) > 0
    5.88 +    val cnfs =
    5.89 +      (optional_helpers
    5.90 +       |> full_types ? append optional_typed_helpers
    5.91 +       |> maps (fn (ss, (raw, ths)) =>
    5.92 +                   if exists is_needed ss then cnf_helper_thms thy raw ths
    5.93 +                   else []))
    5.94 +      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
    5.95 +  in map snd (make_axiom_clauses dfg thy cnfs) end
    5.96  
    5.97  (*Find the minimal arity of each function mentioned in the term. Also, note which uses
    5.98    are not at top level, to see if hBOOL is needed.*)
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Jun 21 12:28:46 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Jun 21 12:31:41 2010 +0200
     6.3 @@ -14,17 +14,17 @@
     6.4    val invert_type_const: string -> string
     6.5    val num_type_args: theory -> string -> int
     6.6    val strip_prefix: string -> string -> string option
     6.7 -  val metis_line: int -> int -> string list -> string
     6.8 +  val metis_line: bool -> int -> int -> string list -> string
     6.9    val metis_proof_text:
    6.10 -    minimize_command * string * string vector * thm * int
    6.11 +    bool * minimize_command * string * string vector * thm * int
    6.12      -> string * string list
    6.13    val isar_proof_text:
    6.14 -    name_pool option * bool * bool * int * Proof.context * int list list
    6.15 -    -> minimize_command * string * string vector * thm * int
    6.16 +    name_pool option * bool * int * Proof.context * int list list
    6.17 +    -> bool * minimize_command * string * string vector * thm * int
    6.18      -> string * string list
    6.19    val proof_text:
    6.20 -    bool -> name_pool option * bool * bool * int * Proof.context * int list list
    6.21 -    -> minimize_command * string * string vector * thm * int
    6.22 +    bool -> name_pool option * bool * int * Proof.context * int list list
    6.23 +    -> bool * minimize_command * string * string vector * thm * int
    6.24      -> string * string list
    6.25  end;
    6.26  
    6.27 @@ -600,13 +600,15 @@
    6.28  fun metis_apply _ 1 = "by "
    6.29    | metis_apply 1 _ = "apply "
    6.30    | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply "
    6.31 -fun metis_itself [] = "metis"
    6.32 -  | metis_itself ss = "(metis " ^ space_implode " " ss ^ ")"
    6.33 -fun metis_command i n (ls, ss) =
    6.34 -  metis_using ls ^ metis_apply i n ^ metis_itself ss
    6.35 -fun metis_line i n ss =
    6.36 +fun metis_name full_types = if full_types then "metisFT" else "metis"
    6.37 +fun metis_call full_types [] = metis_name full_types
    6.38 +  | metis_call full_types ss =
    6.39 +    "(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")"
    6.40 +fun metis_command full_types i n (ls, ss) =
    6.41 +  metis_using ls ^ metis_apply i n ^ metis_call full_types ss
    6.42 +fun metis_line full_types i n ss =
    6.43    "Try this command: " ^
    6.44 -  Markup.markup Markup.sendback (metis_command i n ([], ss)) ^ ".\n"
    6.45 +  Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ ".\n"
    6.46  fun minimize_line _ [] = ""
    6.47    | minimize_line minimize_command facts =
    6.48      case minimize_command facts of
    6.49 @@ -617,7 +619,8 @@
    6.50  
    6.51  val unprefix_chained = perhaps (try (unprefix chained_prefix))
    6.52  
    6.53 -fun metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) =
    6.54 +fun metis_proof_text (full_types, minimize_command, atp_proof, thm_names, goal,
    6.55 +                      i) =
    6.56    let
    6.57      val raw_lemmas =
    6.58        atp_proof |> extract_clause_numbers_in_atp_proof
    6.59 @@ -630,8 +633,8 @@
    6.60      val lemmas = other_lemmas @ chained_lemmas
    6.61      val n = Logic.count_prems (prop_of goal)
    6.62    in
    6.63 -    (metis_line i n other_lemmas ^ minimize_line minimize_command lemmas,
    6.64 -     lemmas)
    6.65 +    (metis_line full_types i n other_lemmas ^
    6.66 +     minimize_line minimize_command lemmas, lemmas)
    6.67    end
    6.68  
    6.69  (** Isar proof construction and manipulation **)
    6.70 @@ -932,7 +935,7 @@
    6.71          step :: aux subst depth nextp proof
    6.72    in aux [] 0 (1, 1) end
    6.73  
    6.74 -fun string_for_proof ctxt i n =
    6.75 +fun string_for_proof ctxt full_types i n =
    6.76    let
    6.77      fun fix_print_mode f x =
    6.78        setmp_CRITICAL show_no_free_types true
    6.79 @@ -956,7 +959,7 @@
    6.80        let
    6.81          val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
    6.82          val ss = ss |> map unprefix_chained |> sort_distinct string_ord
    6.83 -      in metis_command 1 1 (ls, ss) end
    6.84 +      in metis_command full_types 1 1 (ls, ss) end
    6.85      and do_step ind (Fix xs) =
    6.86          do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
    6.87        | do_step ind (Let (t1, t2)) =
    6.88 @@ -989,17 +992,16 @@
    6.89          do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
    6.90    in do_proof end
    6.91  
    6.92 -fun isar_proof_text (pool, debug, full_types, isar_shrink_factor, ctxt,
    6.93 -                     conjecture_shape)
    6.94 -                    (minimize_command, atp_proof, thm_names, goal, i) =
    6.95 +fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
    6.96 +                    (other_params as (full_types, _, atp_proof, thm_names, goal,
    6.97 +                                      i)) =
    6.98    let
    6.99      val thy = ProofContext.theory_of ctxt
   6.100      val (params, hyp_ts, concl_t) = strip_subgoal goal i
   6.101      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   6.102      val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
   6.103      val n = Logic.count_prems (prop_of goal)
   6.104 -    val (one_line_proof, lemma_names) =
   6.105 -      metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
   6.106 +    val (one_line_proof, lemma_names) = metis_proof_text other_params
   6.107      fun isar_proof_for () =
   6.108        case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
   6.109                                  atp_proof conjecture_shape thm_names params
   6.110 @@ -1009,7 +1011,7 @@
   6.111             |> then_chain_proof
   6.112             |> kill_useless_labels_in_proof
   6.113             |> relabel_proof
   6.114 -           |> string_for_proof ctxt i n of
   6.115 +           |> string_for_proof ctxt full_types i n of
   6.116          "" => ""
   6.117        | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
   6.118      val isar_proof =