more preparations towards hijacking Metis
authorblanchet
Mon Jun 06 20:36:35 2011 +0200 (2011-06-06)
changeset 4320523b81469499f
parent 43204 ac02112a208e
child 43206 831d28439b3a
more preparations towards hijacking Metis
src/HOL/Metis_Examples/Proxies.thy
src/HOL/Metis_Examples/Type_Encodings.thy
src/HOL/Mirabelle/Tools/mirabelle_metis.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Metis/metis_tactics.ML
src/HOL/Tools/Metis/metis_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/ex/CASC_Setup.thy
src/HOL/ex/sledgehammer_tactics.ML
     1.1 --- a/src/HOL/Metis_Examples/Proxies.thy	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Proxies.thy	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -24,24 +24,24 @@
     1.4  
     1.5  lemma "inc \<noteq> (\<lambda>y. 0)"
     1.6  sledgehammer [expect = some] (inc_def plus_1_not_0)
     1.7 -by (metis_eXhaust inc_def plus_1_not_0)
     1.8 +by (new_metis_exhaust inc_def plus_1_not_0)
     1.9  
    1.10  lemma "inc = (\<lambda>y. y + 1)"
    1.11  sledgehammer [expect = some] (inc_def)
    1.12 -by (metis_eXhaust inc_def)
    1.13 +by (new_metis_exhaust inc_def)
    1.14  
    1.15  definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    1.16  "add_swap = (\<lambda>x y. y + x)"
    1.17  
    1.18  lemma "add_swap m n = n + m"
    1.19  sledgehammer [expect = some] (add_swap_def)
    1.20 -by (metis_eXhaust add_swap_def)
    1.21 +by (new_metis_exhaust add_swap_def)
    1.22  
    1.23  definition "A = {xs\<Colon>'a list. True}"
    1.24  
    1.25  lemma "xs \<in> A"
    1.26  sledgehammer [expect = some]
    1.27 -by (metis_eXhaust A_def Collect_def mem_def)
    1.28 +by (new_metis_exhaust A_def Collect_def mem_def)
    1.29  
    1.30  definition "B (y::int) \<equiv> y \<le> 0"
    1.31  definition "C (y::int) \<equiv> y \<le> 1"
    1.32 @@ -51,7 +51,7 @@
    1.33  
    1.34  lemma "B \<subseteq> C"
    1.35  sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
    1.36 -by (metis_eXhaust B_def C_def int_le_0_imp_le_1 predicate1I)
    1.37 +by (new_metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
    1.38  
    1.39  
    1.40  text {* Proxies for logical constants *}
    1.41 @@ -78,7 +78,7 @@
    1.42  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.43  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.44  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.45 -by (metis_eXhaust id_apply)
    1.46 +by (new_metis_exhaust id_apply)
    1.47  
    1.48  lemma "\<not> id False"
    1.49  sledgehammer [type_sys = erased, expect = some] (id_apply)
    1.50 @@ -90,7 +90,7 @@
    1.51  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.52  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.53  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.54 -by (metis_eXhaust id_apply)
    1.55 +by (new_metis_exhaust id_apply)
    1.56  
    1.57  lemma "x = id True \<or> x = id False"
    1.58  sledgehammer [type_sys = erased, expect = some] (id_apply)
    1.59 @@ -102,7 +102,7 @@
    1.60  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.61  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.62  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.63 -by (metis_eXhaust id_apply)
    1.64 +by (new_metis_exhaust id_apply)
    1.65  
    1.66  lemma "id x = id True \<or> id x = id False"
    1.67  sledgehammer [type_sys = erased, expect = some] (id_apply)
    1.68 @@ -114,7 +114,7 @@
    1.69  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.70  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.71  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.72 -by (metis_eXhaust id_apply)
    1.73 +by (new_metis_exhaust id_apply)
    1.74  
    1.75  lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
    1.76  sledgehammer [type_sys = erased, expect = none] ()
    1.77 @@ -139,7 +139,7 @@
    1.78  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.79  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.80  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.81 -by (metis_eXhaust id_apply)
    1.82 +by (new_metis_exhaust id_apply)
    1.83  
    1.84  lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
    1.85  sledgehammer [type_sys = erased, expect = some] (id_apply)
    1.86 @@ -151,7 +151,7 @@
    1.87  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.88  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.89  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.90 -by (metis_eXhaust id_apply)
    1.91 +by (new_metis_exhaust id_apply)
    1.92  
    1.93  lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
    1.94  sledgehammer [type_sys = erased, expect = some] (id_apply)
    1.95 @@ -163,7 +163,7 @@
    1.96  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.97  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.98  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.99 -by (metis_eXhaust id_apply)
   1.100 +by (new_metis_exhaust id_apply)
   1.101  
   1.102  lemma "id (a \<and> b) \<Longrightarrow> id a"
   1.103  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.104 @@ -175,7 +175,7 @@
   1.105  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.106  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.107  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.108 -by (metis_eXhaust id_apply)
   1.109 +by (new_metis_exhaust id_apply)
   1.110  
   1.111  lemma "id (a \<and> b) \<Longrightarrow> id b"
   1.112  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.113 @@ -187,7 +187,7 @@
   1.114  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.115  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.116  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.117 -by (metis_eXhaust id_apply)
   1.118 +by (new_metis_exhaust id_apply)
   1.119  
   1.120  lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
   1.121  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.122 @@ -199,7 +199,7 @@
   1.123  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.124  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.125  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.126 -by (metis_eXhaust id_apply)
   1.127 +by (new_metis_exhaust id_apply)
   1.128  
   1.129  lemma "id a \<Longrightarrow> id (a \<or> b)"
   1.130  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.131 @@ -211,7 +211,7 @@
   1.132  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.133  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.134  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.135 -by (metis_eXhaust id_apply)
   1.136 +by (new_metis_exhaust id_apply)
   1.137  
   1.138  lemma "id b \<Longrightarrow> id (a \<or> b)"
   1.139  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.140 @@ -223,7 +223,7 @@
   1.141  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.142  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.143  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.144 -by (metis_eXhaust id_apply)
   1.145 +by (new_metis_exhaust id_apply)
   1.146  
   1.147  lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
   1.148  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.149 @@ -235,7 +235,7 @@
   1.150  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.151  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.152  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.153 -by (metis_eXhaust id_apply)
   1.154 +by (new_metis_exhaust id_apply)
   1.155  
   1.156  lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
   1.157  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.158 @@ -247,7 +247,7 @@
   1.159  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.160  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.161  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.162 -by (metis_eXhaust id_apply)
   1.163 +by (new_metis_exhaust id_apply)
   1.164  
   1.165  lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
   1.166  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.167 @@ -259,6 +259,6 @@
   1.168  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.169  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.170  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.171 -by (metis_eXhaust id_apply)
   1.172 +by (new_metis_exhaust id_apply)
   1.173  
   1.174  end
     2.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Jun 06 20:36:35 2011 +0200
     2.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Jun 06 20:36:35 2011 +0200
     2.3 @@ -40,47 +40,47 @@
     2.4                        constr (poly, level, heaviness))
     2.5                    [Preds, Tags])
     2.6  
     2.7 -fun metis_eXhaust_tac ctxt ths =
     2.8 +fun new_metis_exhaust_tac ctxt ths =
     2.9    let
    2.10      fun tac [] st = all_tac st
    2.11        | tac (type_sys :: type_syss) st =
    2.12          st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *)
    2.13             |> ((if null type_syss then all_tac else rtac @{thm fork} 1)
    2.14 -               THEN Metis_Tactics.metisX_tac ctxt (SOME type_sys) ths 1
    2.15 +               THEN Metis_Tactics.new_metis_tac [type_sys] ctxt ths 1
    2.16                 THEN COND (has_fewer_prems 2) all_tac no_tac
    2.17                 THEN tac type_syss)
    2.18    in tac end
    2.19  *}
    2.20  
    2.21 -method_setup metis_eXhaust = {*
    2.22 +method_setup new_metis_exhaust = {*
    2.23    Attrib.thms >>
    2.24 -    (fn ths => fn ctxt => SIMPLE_METHOD (metis_eXhaust_tac ctxt ths type_syss))
    2.25 +    (fn ths => fn ctxt => SIMPLE_METHOD (new_metis_exhaust_tac ctxt ths type_syss))
    2.26  *} "exhaustively run the new Metis with all type encodings"
    2.27  
    2.28  
    2.29  text {* Miscellaneous tests *}
    2.30  
    2.31  lemma "x = y \<Longrightarrow> y = x"
    2.32 -by metis_eXhaust
    2.33 +by new_metis_exhaust
    2.34  
    2.35  lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)"
    2.36 -by (metis_eXhaust last.simps)
    2.37 +by (new_metis_exhaust last.simps)
    2.38  
    2.39  lemma "map Suc [0] = [Suc 0]"
    2.40 -by (metis_eXhaust map.simps)
    2.41 +by (new_metis_exhaust map.simps)
    2.42  
    2.43  lemma "map Suc [1 + 1] = [Suc 2]"
    2.44 -by (metis_eXhaust map.simps nat_1_add_1)
    2.45 +by (new_metis_exhaust map.simps nat_1_add_1)
    2.46  
    2.47  lemma "map Suc [2] = [Suc (1 + 1)]"
    2.48 -by (metis_eXhaust map.simps nat_1_add_1)
    2.49 +by (new_metis_exhaust map.simps nat_1_add_1)
    2.50  
    2.51  definition "null xs = (xs = [])"
    2.52  
    2.53  lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []"
    2.54 -by (metis_eXhaust null_def)
    2.55 +by (new_metis_exhaust null_def)
    2.56  
    2.57  lemma "(0::nat) + 0 = 0"
    2.58 -by (metis_eXhaust arithmetic_simps(38))
    2.59 +by (new_metis_exhaust arithmetic_simps(38))
    2.60  
    2.61  end
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Mon Jun 06 20:36:35 2011 +0200
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Mon Jun 06 20:36:35 2011 +0200
     3.3 @@ -18,7 +18,7 @@
     3.4  
     3.5      val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
     3.6  
     3.7 -    fun metis ctxt = Metis_Tactics.metis_tac ctxt (thms @ facts)
     3.8 +    fun metis ctxt = Metis_Tactics.new_metis_tac [] ctxt (thms @ facts)
     3.9    in
    3.10      (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
    3.11      |> prefix (metis_tag id)
     4.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 06 20:36:35 2011 +0200
     4.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 06 20:36:35 2011 +0200
     4.3 @@ -542,9 +542,9 @@
     4.4         else if !reconstructor = "smt" then
     4.5           SMT_Solver.smt_tac
     4.6         else if full orelse !reconstructor = "metisFT" then
     4.7 -         Metis_Tactics.metisFT_tac
     4.8 +         Metis_Tactics.old_metisFT_tac
     4.9         else
    4.10 -         Metis_Tactics.metis_tac) ctxt thms
    4.11 +         Metis_Tactics.old_metis_tac) ctxt thms
    4.12      fun apply_reconstructor thms =
    4.13        Mirabelle.can_apply timeout (do_reconstructor thms) st
    4.14  
     5.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
     5.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
     5.3 @@ -230,7 +230,8 @@
     5.4  fun hol_term_from_metis ctxt FO _ = hol_term_from_metis_PT ctxt
     5.5    | hol_term_from_metis ctxt HO _ = hol_term_from_metis_PT ctxt
     5.6    | hol_term_from_metis ctxt FT _ = hol_term_from_metis_FT ctxt
     5.7 -  | hol_term_from_metis ctxt MX sym_tab = hol_term_from_metis_MX ctxt sym_tab
     5.8 +  | hol_term_from_metis ctxt (Type_Sys _) sym_tab =
     5.9 +    hol_term_from_metis_MX ctxt sym_tab
    5.10  
    5.11  fun atp_literal_from_metis (pos, atom) =
    5.12    atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot
    5.13 @@ -514,10 +515,10 @@
    5.14        val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
    5.15        fun replace_item_list lx 0 (_::ls) = lx::ls
    5.16          | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
    5.17 -      fun path_finder_fail mode tm ps t =
    5.18 +      fun path_finder_fail tm ps t =
    5.19          raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
    5.20 -                    "equality_inference, path_finder_" ^ string_of_mode mode ^
    5.21 -                    ": path = " ^ space_implode " " (map string_of_int ps) ^
    5.22 +                    "equality_inference, path_finder: path = " ^
    5.23 +                    space_implode " " (map string_of_int ps) ^
    5.24                      " isa-term: " ^ Syntax.string_of_term ctxt tm ^
    5.25                      (case t of
    5.26                         SOME t => " fol-term: " ^ Metis_Term.toString t
    5.27 @@ -542,7 +543,7 @@
    5.28        fun path_finder_HO tm [] = (tm, Bound 0)
    5.29          | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
    5.30          | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
    5.31 -        | path_finder_HO tm ps = path_finder_fail HO tm ps NONE
    5.32 +        | path_finder_HO tm ps = path_finder_fail tm ps NONE
    5.33        fun path_finder_FT tm [] _ = (tm, Bound 0)
    5.34          | path_finder_FT tm (0::ps) (Metis_Term.Fn (":", [t1, _])) =
    5.35              path_finder_FT tm ps t1
    5.36 @@ -550,7 +551,7 @@
    5.37              (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
    5.38          | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
    5.39              (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
    5.40 -        | path_finder_FT tm ps t = path_finder_fail FT tm ps (SOME t)
    5.41 +        | path_finder_FT tm ps t = path_finder_fail tm ps (SOME t)
    5.42        fun path_finder_MX tm [] _ = (tm, Bound 0)
    5.43          | path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
    5.44            let
    5.45 @@ -575,16 +576,16 @@
    5.46                  val (tm1, args) = strip_comb tm
    5.47                  val adjustment = length ts - length args
    5.48                  val p' = if adjustment > p then p else p - adjustment
    5.49 -                val tm_p = nth args p'
    5.50 -                  handle Subscript =>
    5.51 -                         path_finder_fail MX tm (p :: ps) (SOME t)
    5.52 +                val tm_p =
    5.53 +                  nth args p'
    5.54 +                  handle Subscript => path_finder_fail tm (p :: ps) (SOME t)
    5.55                  val _ = trace_msg ctxt (fn () =>
    5.56                      "path_finder: " ^ string_of_int p ^ "  " ^
    5.57                      Syntax.string_of_term ctxt tm_p)
    5.58                  val (r, t) = path_finder_MX tm_p ps (nth ts p)
    5.59                in (r, list_comb (tm1, replace_item_list t p' args)) end
    5.60            end
    5.61 -        | path_finder_MX tm ps t = path_finder_fail MX tm ps (SOME t)
    5.62 +        | path_finder_MX tm ps t = path_finder_fail tm ps (SOME t)
    5.63        fun path_finder FO tm ps _ = path_finder_FO tm ps
    5.64          | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
    5.65               (*equality: not curried, as other predicates are*)
    5.66 @@ -604,7 +605,7 @@
    5.67          | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
    5.68               (*if not equality, ignore head to skip the hBOOL predicate*)
    5.69          | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
    5.70 -        | path_finder MX tm ps t = path_finder_MX tm ps t
    5.71 +        | path_finder (Type_Sys _) tm ps t = path_finder_MX tm ps t
    5.72        val (tm_subst, body) = path_finder mode i_atom fp m_tm
    5.73        val tm_abs = Abs ("x", type_of tm_subst, body)
    5.74        val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
     6.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
     6.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
     6.3 @@ -9,18 +9,17 @@
     6.4  
     6.5  signature METIS_TACTICS =
     6.6  sig
     6.7 -  type type_sys = ATP_Translate.type_sys
     6.8 -
     6.9    val metisN : string
    6.10    val metisFT_N : string
    6.11    val trace : bool Config.T
    6.12    val verbose : bool Config.T
    6.13    val new_skolemizer : bool Config.T
    6.14 -  val metis_tac : Proof.context -> thm list -> int -> tactic
    6.15 -  val metisF_tac : Proof.context -> thm list -> int -> tactic
    6.16 -  val metisH_tac : Proof.context -> thm list -> int -> tactic
    6.17 -  val metisFT_tac : Proof.context -> thm list -> int -> tactic
    6.18 -  val metisX_tac : Proof.context -> type_sys option -> thm list -> int -> tactic
    6.19 +  val old_metis_tac : Proof.context -> thm list -> int -> tactic
    6.20 +  val old_metisF_tac : Proof.context -> thm list -> int -> tactic
    6.21 +  val old_metisH_tac : Proof.context -> thm list -> int -> tactic
    6.22 +  val old_metisFT_tac : Proof.context -> thm list -> int -> tactic
    6.23 +  val new_metis_tac : string list -> Proof.context -> thm list -> int -> tactic
    6.24 +  val new_metisFT_tac : Proof.context -> thm list -> int -> tactic
    6.25    val setup : theory -> theory
    6.26  end
    6.27  
    6.28 @@ -31,15 +30,22 @@
    6.29  open Metis_Translate
    6.30  open Metis_Reconstruct
    6.31  
    6.32 -fun method_binding_for_mode HO = @{binding metis}
    6.33 -  | method_binding_for_mode FO = @{binding metisF}
    6.34 -  | method_binding_for_mode FT = @{binding metisFT}
    6.35 -  | method_binding_for_mode MX = @{binding metisX}
    6.36 +val full_typesN = "full_types"
    6.37 +val default_unsound_type_sys = "poly_args"
    6.38 +val default_sound_type_sys = "poly_preds_query"
    6.39  
    6.40 -val metisN = Binding.qualified_name_of (method_binding_for_mode HO)
    6.41 -val metisF_N = Binding.qualified_name_of (method_binding_for_mode FO)
    6.42 -val metisFT_N = Binding.qualified_name_of (method_binding_for_mode FT)
    6.43 -val metisX_N = Binding.qualified_name_of (method_binding_for_mode MX)
    6.44 +fun method_call_for_mode HO = (@{binding metis}, "")
    6.45 +  | method_call_for_mode FO = (@{binding metisF}, "")
    6.46 +  | method_call_for_mode FT = (@{binding metisFT}, "")
    6.47 +  | method_call_for_mode (Type_Sys type_sys) =
    6.48 +    if type_sys = default_sound_type_sys then
    6.49 +      (@{binding new_metisFT}, "")
    6.50 +    else
    6.51 +      (@{binding new_metis},
    6.52 +       if type_sys = default_unsound_type_sys then "" else type_sys)
    6.53 +
    6.54 +val metisN = Binding.qualified_name_of @{binding metis}
    6.55 +val metisFT_N = Binding.qualified_name_of @{binding metisFT}
    6.56  
    6.57  val new_skolemizer =
    6.58    Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    6.59 @@ -85,7 +91,7 @@
    6.60  val resolution_params = {active = active_params, waiting = waiting_params}
    6.61  
    6.62  (* Main function to start Metis proof and reconstruction *)
    6.63 -fun FOL_SOLVE type_sys (mode :: fallback_modes) ctxt cls ths0 =
    6.64 +fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 =
    6.65    let val thy = Proof_Context.theory_of ctxt
    6.66        val new_skolemizer =
    6.67          Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
    6.68 @@ -101,7 +107,7 @@
    6.69        val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
    6.70        val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
    6.71        val (mode, sym_tab, {axioms, old_skolems, ...}) =
    6.72 -        prepare_metis_problem ctxt mode type_sys cls ths
    6.73 +        prepare_metis_problem ctxt mode cls ths
    6.74        fun get_isa_thm mth Isa_Reflexive_or_Trivial =
    6.75            reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
    6.76          | get_isa_thm _ (Isa_Raw ith) = ith
    6.77 @@ -167,11 +173,13 @@
    6.78                          (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
    6.79                           else ""))
    6.80           | mode :: _ =>
    6.81 -           (verbose_warning ctxt
    6.82 -                ("Falling back on " ^
    6.83 -                 quote (Binding.qualified_name_of
    6.84 -                            (method_binding_for_mode mode)) ^ "...");
    6.85 -            FOL_SOLVE type_sys fallback_modes ctxt cls ths0)
    6.86 +           let val (binding, arg) = method_call_for_mode mode in
    6.87 +             (verbose_warning ctxt
    6.88 +                  ("Falling back on " ^
    6.89 +                   quote (Binding.qualified_name_of binding ^
    6.90 +                          (arg |> arg <> "" ? enclose " (" ")")) ^ "...");
    6.91 +              FOL_SOLVE fallback_modes ctxt cls ths0)
    6.92 +            end
    6.93  
    6.94  val neg_clausify =
    6.95    single
    6.96 @@ -190,12 +198,12 @@
    6.97  val type_has_top_sort =
    6.98    exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
    6.99  
   6.100 -fun generic_metis_tac modes type_sys ctxt ths i st0 =
   6.101 +fun generic_metis_tac modes ctxt ths i st0 =
   6.102    let
   6.103      val _ = trace_msg ctxt (fn () =>
   6.104          "Metis called with theorems\n" ^
   6.105          cat_lines (map (Display.string_of_thm ctxt) ths))
   6.106 -    fun tac clause = resolve_tac (FOL_SOLVE type_sys modes ctxt clause ths) 1
   6.107 +    fun tac clause = resolve_tac (FOL_SOLVE modes ctxt clause ths) 1
   6.108    in
   6.109      if exists_type type_has_top_sort (prop_of st0) then
   6.110        (verbose_warning ctxt "Proof state contains the universal sort {}";
   6.111 @@ -204,17 +212,21 @@
   6.112        Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
   6.113    end
   6.114  
   6.115 -val metis_modes = [HO, FT]
   6.116 -val metisF_modes = [FO, FT]
   6.117 -val metisH_modes = [HO]
   6.118 -val metisFT_modes = [FT]
   6.119 -val metisX_modes = [MX]
   6.120 +val old_metis_modes = [HO, FT]
   6.121 +val old_metisF_modes = [FO, FT]
   6.122 +val old_metisH_modes = [HO]
   6.123 +val old_metisFT_modes = [FT]
   6.124 +val new_metis_default_modes =
   6.125 +  map Type_Sys [default_unsound_type_sys, default_sound_type_sys]
   6.126 +val new_metisFT_modes = [Type_Sys default_sound_type_sys]
   6.127  
   6.128 -val metis_tac = generic_metis_tac metis_modes NONE
   6.129 -val metisF_tac = generic_metis_tac metisF_modes NONE
   6.130 -val metisH_tac = generic_metis_tac metisH_modes NONE
   6.131 -val metisFT_tac = generic_metis_tac metisFT_modes NONE
   6.132 -fun metisX_tac ctxt type_sys = generic_metis_tac metisX_modes type_sys ctxt
   6.133 +val old_metis_tac = generic_metis_tac old_metis_modes
   6.134 +val old_metisF_tac = generic_metis_tac old_metisF_modes
   6.135 +val old_metisH_tac = generic_metis_tac old_metisH_modes
   6.136 +val old_metisFT_tac = generic_metis_tac old_metisFT_modes
   6.137 +fun new_metis_tac [] = generic_metis_tac new_metis_default_modes
   6.138 +  | new_metis_tac type_syss = generic_metis_tac (map Type_Sys type_syss)
   6.139 +val new_metisFT_tac = generic_metis_tac new_metisFT_modes
   6.140  
   6.141  (* Whenever "X" has schematic type variables, we treat "using X by metis" as
   6.142     "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
   6.143 @@ -227,26 +239,30 @@
   6.144  fun method modes (type_sys, ths) ctxt facts =
   6.145    let
   6.146      val (schem_facts, nonschem_facts) = List.partition has_tvar facts
   6.147 -    val type_sys = type_sys |> Option.map type_sys_from_string
   6.148 +    val modes = type_sys |> Option.map (single o Type_Sys) |> the_default modes
   6.149    in
   6.150      HEADGOAL (Method.insert_tac nonschem_facts THEN'
   6.151 -              CHANGED_PROP
   6.152 -              o generic_metis_tac modes type_sys ctxt (schem_facts @ ths))
   6.153 +              CHANGED_PROP o generic_metis_tac modes ctxt (schem_facts @ ths))
   6.154    end
   6.155  
   6.156  fun setup_method (modes as mode :: _) =
   6.157 -  Method.setup (method_binding_for_mode mode)
   6.158 -               ((if mode = MX then
   6.159 -                   Scan.lift (Scan.option (Args.parens Parse.short_ident))
   6.160 -                 else
   6.161 -                   Scan.succeed NONE)
   6.162 -                -- Attrib.thms >> (METHOD oo method modes))
   6.163 +  (if modes = new_metis_default_modes then
   6.164 +     (Args.parens Parse.short_ident
   6.165 +      >> (fn s => if s = full_typesN then default_sound_type_sys else s))
   6.166 +     |> Scan.option |> Scan.lift
   6.167 +   else
   6.168 +     Scan.succeed NONE)
   6.169 +  -- Attrib.thms >> (METHOD oo method modes)
   6.170 +  |> Method.setup (fst (method_call_for_mode mode))
   6.171  
   6.172  val setup =
   6.173 -  [(metis_modes, "Metis for FOL and HOL problems"),
   6.174 -   (metisF_modes, "Metis for FOL problems"),
   6.175 -   (metisFT_modes, "Metis for FOL/HOL problems with fully-typed translation"),
   6.176 -   (metisX_modes, "Metis for FOL and HOL problems (experimental)")]
   6.177 +  [(old_metis_modes, "Metis for FOL and HOL problems"),
   6.178 +   (old_metisF_modes, "Metis for FOL problems (legacy)"),
   6.179 +   (old_metisFT_modes,
   6.180 +    "Metis for FOL/HOL problems with fully-typed translation"),
   6.181 +   (new_metis_default_modes, "Metis for FOL and HOL problems (experimental)"),
   6.182 +   (new_metisFT_modes,
   6.183 +    "Metis for FOL/HOL problems with fully-typed translation (experimental)")]
   6.184    |> fold (uncurry setup_method)
   6.185  
   6.186  end;
     7.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     7.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     7.3 @@ -10,9 +10,8 @@
     7.4  signature METIS_TRANSLATE =
     7.5  sig
     7.6    type type_literal = ATP_Translate.type_literal
     7.7 -  type type_sys = ATP_Translate.type_sys
     7.8  
     7.9 -  datatype mode = FO | HO | FT | MX
    7.10 +  datatype mode = FO | HO | FT | Type_Sys of string
    7.11  
    7.12    datatype isa_thm =
    7.13      Isa_Reflexive_or_Trivial |
    7.14 @@ -32,7 +31,7 @@
    7.15    val reveal_old_skolem_terms : (string * term) list -> term -> term
    7.16    val string_of_mode : mode -> string
    7.17    val prepare_metis_problem :
    7.18 -    Proof.context -> mode -> type_sys option -> thm list -> thm list
    7.19 +    Proof.context -> mode -> thm list -> thm list
    7.20      -> mode * int Symtab.table * metis_problem
    7.21  end
    7.22  
    7.23 @@ -118,13 +117,13 @@
    7.24  (* HOL to FOL  (Isabelle to Metis)                                           *)
    7.25  (* ------------------------------------------------------------------------- *)
    7.26  
    7.27 -(* first-order, higher-order, fully-typed, mode X (fleXible) *)
    7.28 -datatype mode = FO | HO | FT | MX
    7.29 +(* first-order, higher-order, fully-typed, ATP type system *)
    7.30 +datatype mode = FO | HO | FT | Type_Sys of string
    7.31  
    7.32  fun string_of_mode FO = "FO"
    7.33    | string_of_mode HO = "HO"
    7.34    | string_of_mode FT = "FT"
    7.35 -  | string_of_mode MX = "MX"
    7.36 +  | string_of_mode (Type_Sys type_sys) = "Type_Sys " ^ type_sys
    7.37  
    7.38  fun fn_isa_to_met_sublevel "equal" = "c_fequal"
    7.39    | fn_isa_to_met_sublevel "c_False" = "c_fFalse"
    7.40 @@ -346,13 +345,11 @@
    7.41      end
    7.42    | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
    7.43  
    7.44 -(* FIXME: put in "Metis_Tactics" as string *)
    7.45 -val default_type_sys = Preds (Polymorphic, Const_Arg_Types, Lightweight)
    7.46 -
    7.47  (* Function to generate metis clauses, including comb and type clauses *)
    7.48 -fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses =
    7.49 +fun prepare_metis_problem ctxt (mode as Type_Sys type_sys) conj_clauses
    7.50 +                          fact_clauses =
    7.51      let
    7.52 -      val type_sys = type_sys |> the_default default_type_sys
    7.53 +      val type_sys = type_sys_from_string type_sys
    7.54        val explicit_apply = NONE
    7.55        val clauses =
    7.56          conj_clauses @ fact_clauses
    7.57 @@ -382,9 +379,9 @@
    7.58        val axioms =
    7.59          atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
    7.60      in
    7.61 -      (MX, sym_tab, {axioms = axioms, tfrees = [], old_skolems = old_skolems})
    7.62 +      (mode, sym_tab, {axioms = axioms, tfrees = [], old_skolems = old_skolems})
    7.63      end
    7.64 -  | prepare_metis_problem ctxt mode _ conj_clauses fact_clauses =
    7.65 +  | prepare_metis_problem ctxt mode conj_clauses fact_clauses =
    7.66      let
    7.67        val thy = Proof_Context.theory_of ctxt
    7.68        (* The modes FO and FT are sticky. HO can be downgraded to FO. *)
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 20:36:35 2011 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 20:36:35 2011 +0200
     8.3 @@ -416,8 +416,8 @@
     8.4      val full_tac = Method.insert_tac facts i THEN tac ctxt i
     8.5    in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
     8.6  
     8.7 -fun tac_for_reconstructor Metis = Metis_Tactics.metisH_tac
     8.8 -  | tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac
     8.9 +fun tac_for_reconstructor Metis = Metis_Tactics.old_metisH_tac
    8.10 +  | tac_for_reconstructor MetisFT = Metis_Tactics.old_metisFT_tac
    8.11    | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
    8.12  
    8.13  fun timed_reconstructor reconstructor debug timeout ths =
     9.1 --- a/src/HOL/ex/CASC_Setup.thy	Mon Jun 06 20:36:35 2011 +0200
     9.2 +++ b/src/HOL/ex/CASC_Setup.thy	Mon Jun 06 20:36:35 2011 +0200
     9.3 @@ -51,7 +51,8 @@
     9.4     SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
     9.5         THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
     9.6     ORELSE
     9.7 -   SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac ctxt []))
     9.8 +   SOLVE_TIMEOUT (max_secs div 10) "metis"
     9.9 +       (ALLGOALS (Metis_Tactics.new_metis_tac ctxt NONE []))
    9.10     ORELSE
    9.11     SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
    9.12     ORELSE
    10.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
    10.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
    10.3 @@ -70,7 +70,7 @@
    10.4    in
    10.5      case run_atp false timeout i i ctxt th atp of
    10.6        SOME facts =>
    10.7 -      Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
    10.8 +      Metis_Tactics.new_metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
    10.9      | NONE => Seq.empty
   10.10    end
   10.11