add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
authorblanchet
Mon May 21 10:39:32 2012 +0200 (2012-05-21)
changeset 4794633afcfad3f8d
parent 47945 4073e51293cf
child 47947 7b482cc7473e
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
src/HOL/ATP.thy
src/HOL/Metis.thy
src/HOL/TPTP/atp_problem_import.ML
src/HOL/TPTP/atp_theory_export.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/Metis/metis_generate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/ATP.thy	Mon May 21 10:39:31 2012 +0200
     1.2 +++ b/src/HOL/ATP.thy	Mon May 21 10:39:32 2012 +0200
     1.3 @@ -29,6 +29,9 @@
     1.4  definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
     1.5  "fNot P \<longleftrightarrow> \<not> P"
     1.6  
     1.7 +definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
     1.8 +"fComp P = (\<lambda>x. \<not> P x)"
     1.9 +
    1.10  definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    1.11  "fconj P Q \<longleftrightarrow> P \<and> Q"
    1.12  
    1.13 @@ -47,6 +50,86 @@
    1.14  definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
    1.15  "fEx P \<longleftrightarrow> Ex P"
    1.16  
    1.17 +lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
    1.18 +unfolding fFalse_def fTrue_def by simp
    1.19 +
    1.20 +lemma fNot_table:
    1.21 +"fNot fFalse = fTrue"
    1.22 +"fNot fTrue = fFalse"
    1.23 +unfolding fFalse_def fTrue_def fNot_def by auto
    1.24 +
    1.25 +lemma fconj_table:
    1.26 +"fconj fFalse P = fFalse"
    1.27 +"fconj P fFalse = fFalse"
    1.28 +"fconj fTrue fTrue = fTrue"
    1.29 +unfolding fFalse_def fTrue_def fconj_def by auto
    1.30 +
    1.31 +lemma fdisj_table:
    1.32 +"fdisj fTrue P = fTrue"
    1.33 +"fdisj P fTrue = fTrue"
    1.34 +"fdisj fFalse fFalse = fFalse"
    1.35 +unfolding fFalse_def fTrue_def fdisj_def by auto
    1.36 +
    1.37 +lemma fimplies_table:
    1.38 +"fimplies P fTrue = fTrue"
    1.39 +"fimplies fFalse P = fTrue"
    1.40 +"fimplies fTrue fFalse = fFalse"
    1.41 +unfolding fFalse_def fTrue_def fimplies_def by auto
    1.42 +
    1.43 +lemma fequal_table:
    1.44 +"fequal x x = fTrue"
    1.45 +"x = y \<or> fequal x y = fFalse"
    1.46 +unfolding fFalse_def fTrue_def fequal_def by auto
    1.47 +
    1.48 +lemma fAll_table:
    1.49 +"Ex (fComp P) \<or> fAll P = fTrue"
    1.50 +"All P \<or> fAll P = fFalse"
    1.51 +unfolding fFalse_def fTrue_def fComp_def fAll_def by auto
    1.52 +
    1.53 +lemma fEx_table:
    1.54 +"All (fComp P) \<or> fEx P = fTrue"
    1.55 +"Ex P \<or> fEx P = fFalse"
    1.56 +unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
    1.57 +
    1.58 +lemma fNot_law:
    1.59 +"fNot P \<noteq> P"
    1.60 +unfolding fNot_def by auto
    1.61 +
    1.62 +lemma fComp_law:
    1.63 +"fComp P x \<longleftrightarrow> \<not> P x"
    1.64 +unfolding fComp_def ..
    1.65 +
    1.66 +lemma fconj_laws:
    1.67 +"fconj P P \<longleftrightarrow> P"
    1.68 +"fconj P Q \<longleftrightarrow> fconj Q P"
    1.69 +"fNot (fconj P Q) \<longleftrightarrow> fdisj (fNot P) (fNot Q)"
    1.70 +unfolding fNot_def fconj_def fdisj_def by auto
    1.71 +
    1.72 +lemma fdisj_laws:
    1.73 +"fdisj P P \<longleftrightarrow> P"
    1.74 +"fdisj P Q \<longleftrightarrow> fdisj Q P"
    1.75 +"fNot (fdisj P Q) \<longleftrightarrow> fconj (fNot P) (fNot Q)"
    1.76 +unfolding fNot_def fconj_def fdisj_def by auto
    1.77 +
    1.78 +lemma fimplies_laws:
    1.79 +"fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q"
    1.80 +"fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
    1.81 +unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
    1.82 +
    1.83 +lemma fequal_laws:
    1.84 +"fequal x y = fequal y x"
    1.85 +"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
    1.86 +"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
    1.87 +unfolding fFalse_def fTrue_def fequal_def by auto
    1.88 +
    1.89 +lemma fAll_law:
    1.90 +"fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
    1.91 +unfolding fNot_def fComp_def fAll_def fEx_def by auto
    1.92 +
    1.93 +lemma fEx_law:
    1.94 +"fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
    1.95 +unfolding fNot_def fComp_def fAll_def fEx_def by auto
    1.96 +
    1.97  subsection {* Setup *}
    1.98  
    1.99  use "Tools/ATP/atp_problem_generate.ML"
     2.1 --- a/src/HOL/Metis.thy	Mon May 21 10:39:31 2012 +0200
     2.2 +++ b/src/HOL/Metis.thy	Mon May 21 10:39:32 2012 +0200
     2.3 @@ -47,10 +47,13 @@
     2.4  
     2.5  setup {* Metis_Tactic.setup *}
     2.6  
     2.7 -hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select lambda
     2.8 -hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
     2.9 -    fequal_def select_def not_atomize atomize_not_select not_atomize_select
    2.10 -    select_FalseI lambda_def eq_lambdaI
    2.11 +hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fequal
    2.12 +    lambda
    2.13 +hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select
    2.14 +    select_FalseI fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
    2.15 +    fequal_def fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table
    2.16 +    fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws
    2.17 +    fimplies_laws fequal_laws fAll_law fEx_law lambda_def eq_lambdaI
    2.18  
    2.19  
    2.20  subsection {* Try0 *}
     3.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Mon May 21 10:39:31 2012 +0200
     3.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Mon May 21 10:39:32 2012 +0200
     3.3 @@ -15,7 +15,8 @@
     3.4    val can_tac : Proof.context -> tactic -> term -> bool
     3.5    val SOLVE_TIMEOUT :  int -> string -> tactic -> tactic
     3.6    val atp_tac :
     3.7 -    Proof.context -> (string * string) list -> int -> string -> int -> tactic
     3.8 +    Proof.context -> int -> (string * string) list -> int -> string -> int
     3.9 +    -> tactic
    3.10    val smt_solver_tac : string -> Proof.context -> int -> tactic
    3.11    val freeze_problem_consts : theory -> term -> term
    3.12    val make_conj : term list * term list -> term list -> term
    3.13 @@ -177,31 +178,51 @@
    3.14        in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end
    3.15    end
    3.16  
    3.17 -fun atp_tac ctxt override_params timeout prover =
    3.18 -  Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
    3.19 -      ([("debug", if debug then "true" else "false"),
    3.20 -        ("overlord", if overlord then "true" else "false"),
    3.21 -        ("provers", prover),
    3.22 -        ("timeout", string_of_int timeout)] @ override_params)
    3.23 -      {add = [(Facts.named (Thm.derivation_name ext), [])],
    3.24 -       del = [], only = true}
    3.25 +fun atp_tac ctxt aggressivity override_params timeout prover =
    3.26 +  let
    3.27 +    val ctxt =
    3.28 +      ctxt |> Config.put Sledgehammer_Provers.aggressive (aggressivity > 0)
    3.29 +  in
    3.30 +    Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
    3.31 +        ([("debug", if debug then "true" else "false"),
    3.32 +          ("overlord", if overlord then "true" else "false"),
    3.33 +          ("provers", prover),
    3.34 +          ("timeout", string_of_int timeout)] @
    3.35 +         (if aggressivity > 0 then
    3.36 +            [("type_enc",
    3.37 +              if aggressivity = 1 then "mono_native" else "poly_guards??"),
    3.38 +             ("slicing", "false")]
    3.39 +          else
    3.40 +            []) @
    3.41 +         override_params)
    3.42 +        {add = [(Facts.named (Thm.derivation_name ext), [])],
    3.43 +         del = [], only = true}
    3.44 +  end
    3.45  
    3.46  fun sledgehammer_tac demo ctxt timeout i =
    3.47    let
    3.48 -    val frac = if demo then 6 else 4
    3.49 -    fun slice prover =
    3.50 -      SOLVE_TIMEOUT (timeout div frac) prover
    3.51 -                    (atp_tac ctxt [] (timeout div frac) prover i)
    3.52 +    val frac = if demo then 16 else 12
    3.53 +    fun slice mult aggressivity prover =
    3.54 +      SOLVE_TIMEOUT (mult * timeout div frac)
    3.55 +          (prover ^
    3.56 +           (if aggressivity > 0 then "(" ^ string_of_int aggressivity ^ ")"
    3.57 +            else ""))
    3.58 +          (atp_tac ctxt aggressivity [] (timeout div frac) prover i)
    3.59    in
    3.60 -    (if demo then
    3.61 -       slice ATP_Systems.satallaxN
    3.62 -       ORELSE slice ATP_Systems.leo2N
    3.63 -     else
    3.64 -       no_tac)
    3.65 -    ORELSE slice ATP_Systems.spassN
    3.66 -    ORELSE slice ATP_Systems.vampireN
    3.67 -    ORELSE slice ATP_Systems.eN
    3.68 -    ORELSE slice ATP_Systems.z3_tptpN
    3.69 +    slice 2 0 ATP_Systems.spassN
    3.70 +    ORELSE slice 2 0 ATP_Systems.vampireN
    3.71 +    ORELSE slice 2 0 ATP_Systems.eN
    3.72 +    ORELSE slice 2 0 ATP_Systems.z3_tptpN
    3.73 +    ORELSE slice 1 1 ATP_Systems.spassN
    3.74 +    ORELSE slice 1 2 ATP_Systems.eN
    3.75 +    ORELSE slice 1 1 ATP_Systems.vampireN
    3.76 +    ORELSE slice 1 2 ATP_Systems.vampireN
    3.77 +    ORELSE
    3.78 +      (if demo then
    3.79 +         slice 2 0 ATP_Systems.satallaxN
    3.80 +         ORELSE slice 2 0 ATP_Systems.leo2N
    3.81 +       else
    3.82 +         no_tac)
    3.83    end
    3.84  
    3.85  fun smt_solver_tac solver ctxt =
    3.86 @@ -212,15 +233,15 @@
    3.87  fun auto_etc_tac ctxt timeout i =
    3.88    SOLVE_TIMEOUT (timeout div 20) "nitpick"
    3.89        (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
    3.90 -  ORELSE SOLVE_TIMEOUT (timeout div 20) "simp"
    3.91 +  ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
    3.92        (asm_full_simp_tac (simpset_of ctxt) i)
    3.93    ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
    3.94    ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
    3.95        (auto_tac ctxt
    3.96 -       THEN ALLGOALS (atp_tac ctxt [] (timeout div 5) ATP_Systems.spassN))
    3.97 -  ORELSE SOLVE_TIMEOUT (timeout div 10) "z3" (smt_solver_tac "z3" ctxt i)
    3.98 -  ORELSE SOLVE_TIMEOUT (timeout div 10) "cvc3" (smt_solver_tac "cvc3" ctxt i)
    3.99 -  ORELSE SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i)
   3.100 +       THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) ATP_Systems.spassN))
   3.101 +  ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
   3.102 +  ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
   3.103 +  ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc3" (smt_solver_tac "cvc3" ctxt i)
   3.104    ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
   3.105    ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
   3.106    ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i)
   3.107 @@ -264,11 +285,11 @@
   3.108      val (conjs, assms, ctxt) =
   3.109        read_tptp_file thy (freeze_problem_consts thy) file_name
   3.110      val conj = make_conj assms conjs
   3.111 -    val last_hope = if demo then ATP_Systems.satallaxN else ATP_Systems.spassN
   3.112 +    val last_hope = if demo then ATP_Systems.satallaxN else ATP_Systems.vampireN
   3.113    in
   3.114      (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
   3.115       can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
   3.116 -     can_tac ctxt (atp_tac ctxt [] timeout last_hope 1) conj)
   3.117 +     can_tac ctxt (atp_tac ctxt 2 [] timeout last_hope 1) conj)
   3.118      |> print_szs_from_success conjs
   3.119    end
   3.120  
     4.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Mon May 21 10:39:31 2012 +0200
     4.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Mon May 21 10:39:32 2012 +0200
     4.3 @@ -183,8 +183,8 @@
     4.4        |> map (fn ((_, loc), th) =>
     4.5                   ((Thm.get_name_hint th, loc),
     4.6                     th |> prop_of |> mono ? monomorphize_term ctxt))
     4.7 -      |> prepare_atp_problem ctxt format Axiom type_enc true combsN false false
     4.8 -                             true [] @{prop False}
     4.9 +      |> prepare_atp_problem ctxt format Axiom type_enc Exporter combsN false
    4.10 +                             false true [] @{prop False}
    4.11        |> #1
    4.12      val atp_problem =
    4.13        atp_problem
     5.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon May 21 10:39:31 2012 +0200
     5.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon May 21 10:39:32 2012 +0200
     5.3 @@ -15,6 +15,8 @@
     5.4    type formula_kind = ATP_Problem.formula_kind
     5.5    type 'a problem = 'a ATP_Problem.problem
     5.6  
     5.7 +  datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter
     5.8 +
     5.9    datatype scope = Global | Local | Assum | Chained
    5.10    datatype status =
    5.11      General | Induction | Intro | Inductive | Elim | Simp | Def
    5.12 @@ -95,12 +97,12 @@
    5.13      connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
    5.14    val unmangled_const : string -> string * (string, 'b) ho_term list
    5.15    val unmangled_const_name : string -> string list
    5.16 -  val helper_table : ((string * bool) * thm list) list
    5.17 +  val helper_table : ((string * bool) * (status * thm) list) list
    5.18    val trans_lams_from_string :
    5.19      Proof.context -> type_enc -> string -> term list -> term list * term list
    5.20    val factsN : string
    5.21    val prepare_atp_problem :
    5.22 -    Proof.context -> atp_format -> formula_kind -> type_enc -> bool -> string
    5.23 +    Proof.context -> atp_format -> formula_kind -> type_enc -> mode -> string
    5.24      -> bool -> bool -> bool -> term list -> term
    5.25      -> ((string * stature) * term) list
    5.26      -> string problem * string Symtab.table * (string * stature) list vector
    5.27 @@ -117,6 +119,8 @@
    5.28  
    5.29  type name = string * string
    5.30  
    5.31 +datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter
    5.32 +
    5.33  datatype scope = Global | Local | Assum | Chained
    5.34  datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
    5.35  type stature = scope * status
    5.36 @@ -1587,12 +1591,21 @@
    5.37      pred_sym andalso min_ary = max_ary
    5.38    | NONE => false
    5.39  
    5.40 -val app_op = `(make_fixed_const NONE) app_op_name
    5.41 -val predicator_combconst =
    5.42 +val fTrue_iconst =
    5.43 +  IConst ((const_prefix ^ "fTrue", @{const_name ATP.fTrue}), @{typ bool}, [])
    5.44 +val predicator_iconst =
    5.45    IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
    5.46  
    5.47 +fun predicatify aggressive tm =
    5.48 +  if aggressive then
    5.49 +    IApp (IApp (IConst (`I tptp_equal, @{typ "bool => bool => bool"}, []), tm),
    5.50 +          fTrue_iconst)
    5.51 +  else
    5.52 +    IApp (predicator_iconst, tm)
    5.53 +
    5.54 +val app_op = `(make_fixed_const NONE) app_op_name
    5.55 +
    5.56  fun list_app head args = fold (curry (IApp o swap)) args head
    5.57 -fun predicator tm = IApp (predicator_combconst, tm)
    5.58  
    5.59  fun mk_app_op type_enc head arg =
    5.60    let
    5.61 @@ -1603,7 +1616,8 @@
    5.62        |> mangle_type_args_in_iterm type_enc
    5.63    in list_app app [head, arg] end
    5.64  
    5.65 -fun firstorderize_fact thy monom_constrs type_enc sym_tab uncurried_aliases =
    5.66 +fun firstorderize_fact thy monom_constrs type_enc sym_tab uncurried_aliases
    5.67 +                       aggressive =
    5.68    let
    5.69      fun do_app arg head = mk_app_op type_enc head arg
    5.70      fun list_app_ops head args = fold do_app args head
    5.71 @@ -1625,8 +1639,8 @@
    5.72      fun introduce_predicators tm =
    5.73        case strip_iterm_comb tm of
    5.74          (IConst ((s, _), _, _), _) =>
    5.75 -        if is_pred_sym sym_tab s then tm else predicator tm
    5.76 -      | _ => predicator tm
    5.77 +        if is_pred_sym sym_tab s then tm else predicatify aggressive tm
    5.78 +      | _ => predicatify aggressive tm
    5.79      val do_iterm =
    5.80        not (is_type_enc_higher_order type_enc)
    5.81        ? (introduce_app_ops #> introduce_predicators)
    5.82 @@ -1639,45 +1653,75 @@
    5.83  val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
    5.84  
    5.85  (* The Boolean indicates that a fairly sound type encoding is needed. *)
    5.86 +val base_helper_table =
    5.87 +  [(("COMBI", false), [(Def, @{thm Meson.COMBI_def})]),
    5.88 +   (("COMBK", false), [(Def, @{thm Meson.COMBK_def})]),
    5.89 +   (("COMBB", false), [(Def, @{thm Meson.COMBB_def})]),
    5.90 +   (("COMBC", false), [(Def, @{thm Meson.COMBC_def})]),
    5.91 +   (("COMBS", false), [(Def, @{thm Meson.COMBS_def})]),
    5.92 +   ((predicator_name, false), [(General, not_ffalse), (General, ftrue)]),
    5.93 +   (("fFalse", false), [(General, not_ffalse)]),
    5.94 +   (("fFalse", true), [(General, @{thm True_or_False})]),
    5.95 +   (("fTrue", false), [(General, ftrue)]),
    5.96 +   (("fTrue", true), [(General, @{thm True_or_False})]),
    5.97 +   (("If", true),
    5.98 +    [(Def, @{thm if_True}), (Def, @{thm if_False}),
    5.99 +     (General, @{thm True_or_False})])]
   5.100 +
   5.101  val helper_table =
   5.102 -  [(("COMBI", false), @{thms Meson.COMBI_def}),
   5.103 -   (("COMBK", false), @{thms Meson.COMBK_def}),
   5.104 -   (("COMBB", false), @{thms Meson.COMBB_def}),
   5.105 -   (("COMBC", false), @{thms Meson.COMBC_def}),
   5.106 -   (("COMBS", false), @{thms Meson.COMBS_def}),
   5.107 -   ((predicator_name, false), [not_ffalse, ftrue]),
   5.108 -   ((predicator_name, true), @{thms True_or_False}),
   5.109 -(* FIXME: Metis doesn't like existentials in helpers
   5.110 -   ((app_op_name, true), [@{lemma "EX x. ~ f x = g x | f = g" by blast}]),
   5.111 -*)
   5.112 -   (("fFalse", false), [not_ffalse]),
   5.113 -   (("fFalse", true), @{thms True_or_False}),
   5.114 -   (("fTrue", false), [ftrue]),
   5.115 -   (("fTrue", true), @{thms True_or_False}),
   5.116 -   (("fNot", false),
   5.117 +  base_helper_table @
   5.118 +  [(("fNot", false),
   5.119      @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
   5.120 -           fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
   5.121 +           fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
   5.122 +    |> map (pair Def)),
   5.123     (("fconj", false),
   5.124      @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
   5.125 -        by (unfold fconj_def) fast+}),
   5.126 +        by (unfold fconj_def) fast+}
   5.127 +    |> map (pair General)),
   5.128     (("fdisj", false),
   5.129      @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
   5.130 -        by (unfold fdisj_def) fast+}),
   5.131 +        by (unfold fdisj_def) fast+}
   5.132 +    |> map (pair General)),
   5.133     (("fimplies", false),
   5.134      @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
   5.135 -        by (unfold fimplies_def) fast+}),
   5.136 +        by (unfold fimplies_def) fast+}
   5.137 +    |> map (pair General)),
   5.138     (("fequal", true),
   5.139      (* This is a lie: Higher-order equality doesn't need a sound type encoding.
   5.140         However, this is done so for backward compatibility: Including the
   5.141         equality helpers by default in Metis breaks a few existing proofs. *)
   5.142      @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
   5.143 -           fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
   5.144 +           fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
   5.145 +    |> map (pair General)),
   5.146     (* Partial characterization of "fAll" and "fEx". A complete characterization
   5.147        would require the axiom of choice for replay with Metis. *)
   5.148 -   (("fAll", false), [@{lemma "~ fAll P | P x" by (auto simp: fAll_def)}]),
   5.149 -   (("fEx", false), [@{lemma "~ P x | fEx P" by (auto simp: fEx_def)}]),
   5.150 -   (("If", true), @{thms if_True if_False True_or_False})]
   5.151 -  |> map (apsnd (map zero_var_indexes))
   5.152 +   (("fAll", false),
   5.153 +    [(General, @{lemma "~ fAll P | P x" by (auto simp: fAll_def)})]),
   5.154 +   (("fEx", false),
   5.155 +    [(General, @{lemma "~ P x | fEx P" by (auto simp: fEx_def)})])]
   5.156 +  |> map (apsnd (map (apsnd zero_var_indexes)))
   5.157 +
   5.158 +val aggressive_helper_table =
   5.159 +  base_helper_table @
   5.160 +  [((predicator_name, true),
   5.161 +    @{thms True_or_False fTrue_ne_fFalse} |> map (pair General)),
   5.162 +   ((app_op_name, true),
   5.163 +    [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast})]),
   5.164 +   (("fconj", false),
   5.165 +    @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Def)),
   5.166 +   (("fdisj", false),
   5.167 +    @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Def)),
   5.168 +   (("fimplies", false),
   5.169 +    @{thms fimplies_table fconj_laws fdisj_laws fimplies_laws}
   5.170 +    |> map (pair Def)),
   5.171 +   (("fequal", false),
   5.172 +    (@{thms fequal_table} |> map (pair Def)) @
   5.173 +    (@{thms fequal_laws} |> map (pair General))),
   5.174 +   (("fAll", false),
   5.175 +    @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Def)),
   5.176 +   (("fEx", false),
   5.177 +    @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
   5.178 +  |> map (apsnd (map (apsnd zero_var_indexes)))
   5.179  
   5.180  fun atype_of_type_vars (Native (_, Polymorphic, _)) = SOME atype_of_types
   5.181    | atype_of_type_vars _ = NONE
   5.182 @@ -1705,19 +1749,22 @@
   5.183  
   5.184  val type_tag = `(make_fixed_const NONE) type_tag_name
   5.185  
   5.186 -fun should_specialize_helper type_enc t =
   5.187 +fun could_specialize_helpers type_enc =
   5.188    polymorphism_of_type_enc type_enc <> Polymorphic andalso
   5.189 -  level_of_type_enc type_enc <> No_Types andalso
   5.190 +  level_of_type_enc type_enc <> No_Types
   5.191 +fun should_specialize_helper type_enc t =
   5.192 +  could_specialize_helpers type_enc andalso
   5.193    not (null (Term.hidden_polymorphism t))
   5.194  
   5.195 -fun add_helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
   5.196 +fun add_helper_facts_for_sym ctxt format type_enc aggressive
   5.197 +                             (s, {types, ...} : sym_info) =
   5.198    case unprefix_and_unascii const_prefix s of
   5.199      SOME mangled_s =>
   5.200      let
   5.201        val thy = Proof_Context.theory_of ctxt
   5.202        val unmangled_s = mangled_s |> unmangled_const_name |> hd
   5.203        fun dub needs_fairly_sound j k =
   5.204 -        unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
   5.205 +        ascii_of unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
   5.206          (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
   5.207          (if needs_fairly_sound then typed_helper_suffix
   5.208           else untyped_helper_suffix)
   5.209 @@ -1729,30 +1776,35 @@
   5.210            in monomorphic_term tyenv t end
   5.211          else
   5.212            specialize_type thy (invert_const unmangled_s, T) t
   5.213 -      fun dub_and_inst needs_fairly_sound (t, j) =
   5.214 +      fun dub_and_inst needs_fairly_sound ((status, t), j) =
   5.215          (if should_specialize_helper type_enc t then
   5.216 -           map (specialize_helper t) types
   5.217 +           map_filter (try (specialize_helper t)) types
   5.218           else
   5.219             [t])
   5.220          |> tag_list 1
   5.221 -        |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Def)), t))
   5.222 +        |> map (fn (k, t) =>
   5.223 +                   ((dub needs_fairly_sound j k, (Global, status)), t))
   5.224        val make_facts = map_filter (make_fact ctxt format type_enc false)
   5.225        val fairly_sound = is_type_enc_fairly_sound type_enc
   5.226 +      val could_specialize = could_specialize_helpers type_enc
   5.227      in
   5.228        fold (fn ((helper_s, needs_fairly_sound), ths) =>
   5.229 -               if helper_s <> unmangled_s orelse
   5.230 -                  (needs_fairly_sound andalso not fairly_sound) then
   5.231 +               if (needs_fairly_sound andalso not fairly_sound) orelse
   5.232 +                  (helper_s <> unmangled_s andalso
   5.233 +                   (not aggressive orelse could_specialize)) then
   5.234                   I
   5.235                 else
   5.236                   ths ~~ (1 upto length ths)
   5.237 -                 |> maps (dub_and_inst needs_fairly_sound o apfst prop_of)
   5.238 +                 |> maps (dub_and_inst needs_fairly_sound
   5.239 +                          o apfst (apsnd prop_of))
   5.240                   |> make_facts
   5.241                   |> union (op = o pairself #iformula))
   5.242 -           helper_table
   5.243 +           (if aggressive then aggressive_helper_table else helper_table)
   5.244      end
   5.245    | NONE => I
   5.246 -fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
   5.247 -  Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc) sym_tab []
   5.248 +fun helper_facts_for_sym_table ctxt format type_enc aggressive sym_tab =
   5.249 +  Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc aggressive)
   5.250 +                  sym_tab []
   5.251  
   5.252  (***************************************************************)
   5.253  (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   5.254 @@ -2602,7 +2654,7 @@
   5.255  
   5.256  val app_op_and_predicator_threshold = 50
   5.257  
   5.258 -fun prepare_atp_problem ctxt format prem_kind type_enc exporter lam_trans
   5.259 +fun prepare_atp_problem ctxt format prem_kind type_enc mode lam_trans
   5.260                          uncurried_aliases readable_names preproc hyp_ts concl_t
   5.261                          facts =
   5.262    let
   5.263 @@ -2613,11 +2665,16 @@
   5.264         ruin everything. Hence we do it only if there are few facts (which is
   5.265         normally the case for "metis" and the minimizer). *)
   5.266      val app_op_level =
   5.267 -      if length facts > app_op_and_predicator_threshold then
   5.268 +      if mode = Sledgehammer_Aggressive then
   5.269 +        Full_App_Op_And_Predicator
   5.270 +      else if length facts + length hyp_ts
   5.271 +              > app_op_and_predicator_threshold then
   5.272          if polymorphism_of_type_enc type_enc = Polymorphic then Min_App_Op
   5.273          else Sufficient_App_Op
   5.274        else
   5.275          Sufficient_App_Op_And_Predicator
   5.276 +    val exporter = (mode = Exporter)
   5.277 +    val aggressive = (mode = Sledgehammer_Aggressive)
   5.278      val lam_trans =
   5.279        if lam_trans = keep_lamsN andalso
   5.280           not (is_type_enc_higher_order type_enc) then
   5.281 @@ -2637,7 +2694,7 @@
   5.282        |>> map (make_fixed_const (SOME type_enc))
   5.283      fun firstorderize in_helper =
   5.284        firstorderize_fact thy monom_constrs type_enc sym_tab0
   5.285 -                         (uncurried_aliases andalso not in_helper)
   5.286 +          (uncurried_aliases andalso not in_helper) aggressive
   5.287      val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
   5.288      val (ho_stuff, sym_tab) =
   5.289        sym_table_for_facts ctxt type_enc Min_App_Op conjs facts
   5.290 @@ -2649,7 +2706,7 @@
   5.291        |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
   5.292                uncurried_alias_eq_tms
   5.293      val helpers =
   5.294 -      sym_tab |> helper_facts_for_sym_table ctxt format type_enc
   5.295 +      sym_tab |> helper_facts_for_sym_table ctxt format type_enc aggressive
   5.296                |> map (firstorderize true)
   5.297      val mono_Ts =
   5.298        helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
     6.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 21 10:39:31 2012 +0200
     6.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 21 10:39:32 2012 +0200
     6.3 @@ -363,7 +363,7 @@
     6.4            |> try (single o hd) |> the_default []
     6.5  
     6.6  fun commute_eq (AAtom (ATerm (s, tms))) = AAtom (ATerm (s, rev tms))
     6.7 -  | commute_eq t = raise Fail "expected equation"
     6.8 +  | commute_eq _ = raise Fail "expected equation"
     6.9  
    6.10  (* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>,
    6.11              <formula> <extra_arguments>\).
     7.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Mon May 21 10:39:31 2012 +0200
     7.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Mon May 21 10:39:32 2012 +0200
     7.3 @@ -176,10 +176,10 @@
     7.4          case (String.isSuffix typed_helper_suffix ident,
     7.5                space_explode "_" ident) of
     7.6            (needs_fairly_sound, _ :: const :: j :: _) =>
     7.7 -          nth ((const, needs_fairly_sound)
     7.8 -               |> AList.lookup (op =) helper_table |> the)
     7.9 +          nth (AList.lookup (op =) helper_table (const, needs_fairly_sound)
    7.10 +               |> the)
    7.11                (the (Int.fromString j) - 1)
    7.12 -          |> prepare_helper
    7.13 +          |> snd |> prepare_helper
    7.14            |> Isa_Raw |> some
    7.15          | _ => raise Fail ("malformed helper identifier " ^ quote ident)
    7.16        else case try (unprefix fact_prefix) ident of
    7.17 @@ -242,7 +242,7 @@
    7.18      *)
    7.19      val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
    7.20      val (atp_problem, _, _, lifted, sym_tab) =
    7.21 -      prepare_atp_problem ctxt CNF Hypothesis type_enc false lam_trans false
    7.22 +      prepare_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false
    7.23                            false false [] @{prop False} props
    7.24      (*
    7.25      val _ = tracing ("ATP PROBLEM: " ^
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 21 10:39:31 2012 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 21 10:39:32 2012 +0200
     8.3 @@ -65,6 +65,7 @@
     8.4  
     8.5    val dest_dir : string Config.T
     8.6    val problem_prefix : string Config.T
     8.7 +  val aggressive : bool Config.T
     8.8    val atp_full_names : bool Config.T
     8.9    val smt_triggers : bool Config.T
    8.10    val smt_weights : bool Config.T
    8.11 @@ -334,6 +335,8 @@
    8.12    Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
    8.13  val problem_prefix =
    8.14    Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
    8.15 +val aggressive =
    8.16 +  Attrib.setup_config_bool @{binding sledgehammer_aggressive} (K false)
    8.17  
    8.18  (* In addition to being easier to read, readable names are often much shorter,
    8.19     especially if types are mangled in names. This makes a difference for some
    8.20 @@ -589,6 +592,9 @@
    8.21    let
    8.22      val thy = Proof.theory_of state
    8.23      val ctxt = Proof.context_of state
    8.24 +    val atp_mode =
    8.25 +      if Config.get ctxt aggressive then Sledgehammer_Aggressive
    8.26 +      else Sledgehammer
    8.27      val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
    8.28      val (dest_dir, problem_prefix) =
    8.29        if overlord then overlord_file_location_for_prover name
    8.30 @@ -710,9 +716,9 @@
    8.31                      |> polymorphism_of_type_enc type_enc <> Polymorphic
    8.32                         ? monomorphize_facts
    8.33                      |> map (apsnd prop_of)
    8.34 -                    |> prepare_atp_problem ctxt format prem_kind type_enc false
    8.35 -                           lam_trans uncurried_aliases readable_names true
    8.36 -                           hyp_ts concl_t
    8.37 +                    |> prepare_atp_problem ctxt format prem_kind type_enc
    8.38 +                                           atp_mode lam_trans uncurried_aliases
    8.39 +                                           readable_names true hyp_ts concl_t
    8.40                  fun sel_weights () = atp_problem_selection_weights atp_problem
    8.41                  fun ord_info () = atp_problem_term_order_info atp_problem
    8.42                  val ord = effective_term_order ctxt name