src/HOL/Tools/Metis/metis_tactic.ML
author wenzelm
Tue Jun 02 09:16:19 2015 +0200 (2015-06-02)
changeset 60358 aebfbcab1eb8
parent 59632 5980e75a204e
child 60362 befdc10ebb42
permissions -rw-r--r--
clarified context;
     1 (*  Title:      HOL/Tools/Metis/metis_tactic.ML
     2     Author:     Kong W. Susanto, Cambridge University Computer Laboratory
     3     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     4     Author:     Jasmin Blanchette, TU Muenchen
     5     Copyright   Cambridge University 2007
     6 
     7 HOL setup for the Metis prover.
     8 *)
     9 
    10 signature METIS_TACTIC =
    11 sig
    12   val trace : bool Config.T
    13   val verbose : bool Config.T
    14   val new_skolem : bool Config.T
    15   val advisory_simp : bool Config.T
    16   val metis_tac_unused : string list -> string -> Proof.context -> thm list -> int -> thm ->
    17     thm list * thm Seq.seq
    18   val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic
    19   val metis_lam_transs : string list
    20   val parse_metis_options : (string list option * string option) parser
    21 end
    22 
    23 structure Metis_Tactic : METIS_TACTIC =
    24 struct
    25 
    26 open ATP_Problem_Generate
    27 open ATP_Proof_Reconstruct
    28 open Metis_Generate
    29 open Metis_Reconstruct
    30 
    31 val new_skolem = Attrib.setup_config_bool @{binding metis_new_skolem} (K false)
    32 val advisory_simp = Attrib.setup_config_bool @{binding metis_advisory_simp} (K true)
    33 
    34 (* Designed to work also with monomorphic instances of polymorphic theorems. *)
    35 fun have_common_thm ctxt ths1 ths2 =
    36   exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1)
    37     (map (Meson.make_meta_clause ctxt) ths2)
    38 
    39 (*Determining which axiom clauses are actually used*)
    40 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
    41   | used_axioms _ _ = NONE
    42 
    43 (* Lightweight predicate type information comes in two flavors, "t = t'" and
    44    "t => t'", where "t" and "t'" are the same term modulo type tags.
    45    In Isabelle, type tags are stripped away, so we are left with "t = t" or
    46    "t => t". Type tag idempotence is also handled this way. *)
    47 fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth =
    48   (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
    49     Const (@{const_name HOL.eq}, _) $ _ $ t =>
    50     let
    51       val ct = Thm.cterm_of ctxt t
    52       val cT = Thm.ctyp_of_cterm ct
    53     in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
    54   | Const (@{const_name disj}, _) $ t1 $ t2 =>
    55     (if can HOLogic.dest_not t1 then t2 else t1)
    56     |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
    57   | _ => raise Fail "expected reflexive or trivial clause")
    58   |> Meson.make_meta_clause ctxt
    59 
    60 fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
    61   let
    62     val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac ctxt [refl] 1
    63     val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
    64     val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
    65   in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause ctxt end
    66 
    67 fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
    68   | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t
    69   | add_vars_and_frees (t as Var _) = insert (op =) t
    70   | add_vars_and_frees (t as Free _) = insert (op =) t
    71   | add_vars_and_frees _ = I
    72 
    73 fun introduce_lam_wrappers ctxt th =
    74   if Meson_Clausify.is_quasi_lambda_free (Thm.prop_of th) then
    75     th
    76   else
    77     let
    78       fun conv first ctxt ct =
    79         if Meson_Clausify.is_quasi_lambda_free (Thm.term_of ct) then
    80           Thm.reflexive ct
    81         else
    82           (case Thm.term_of ct of
    83             Abs (_, _, u) =>
    84             if first then
    85               (case add_vars_and_frees u [] of
    86                 [] =>
    87                 Conv.abs_conv (conv false o snd) ctxt ct
    88                 |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
    89               | v :: _ =>
    90                 Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v
    91                 |> Thm.cterm_of ctxt
    92                 |> Conv.comb_conv (conv true ctxt))
    93             else
    94               Conv.abs_conv (conv false o snd) ctxt ct
    95           | Const (@{const_name Meson.skolem}, _) $ _ => Thm.reflexive ct
    96           | _ => Conv.comb_conv (conv true ctxt) ct)
    97       val eq_th = conv true ctxt (Thm.cprop_of th)
    98       (* We replace the equation's left-hand side with a beta-equivalent term
    99          so that "Thm.equal_elim" works below. *)
   100       val t0 $ _ $ t2 = Thm.prop_of eq_th
   101       val eq_ct = t0 $ Thm.prop_of th $ t2 |> Thm.cterm_of ctxt
   102       val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (resolve_tac ctxt [eq_th] 1))
   103     in Thm.equal_elim eq_th' th end
   104 
   105 fun clause_params ordering =
   106   {ordering = ordering,
   107    orderLiterals = Metis_Clause.UnsignedLiteralOrder,
   108    orderTerms = true}
   109 fun active_params ordering =
   110   {clause = clause_params ordering,
   111    prefactor = #prefactor Metis_Active.default,
   112    postfactor = #postfactor Metis_Active.default}
   113 val waiting_params =
   114   {symbolsWeight = 1.0,
   115    variablesWeight = 0.05,
   116    literalsWeight = 0.01,
   117    models = []}
   118 fun resolution_params ordering =
   119   {active = active_params ordering, waiting = waiting_params}
   120 
   121 fun kbo_advisory_simp_ordering ord_info =
   122   let
   123     fun weight (m, _) =
   124       AList.lookup (op =) ord_info (Metis_Name.toString m) |> the_default 1
   125     fun precedence p =
   126       (case int_ord (apply2 weight p) of
   127         EQUAL => #precedence Metis_KnuthBendixOrder.default p
   128       | ord => ord)
   129   in {weight = weight, precedence = precedence} end
   130 
   131 fun metis_call type_enc lam_trans =
   132   let
   133     val type_enc =
   134       (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
   135         [alias] => alias
   136       | _ => type_enc)
   137     val opts =
   138       [] |> type_enc <> partial_typesN ? cons type_enc
   139          |> lam_trans <> default_metis_lam_trans ? cons lam_trans
   140   in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
   141 
   142 exception METIS_UNPROVABLE of unit
   143 
   144 (* Main function to start Metis proof and reconstruction *)
   145 fun FOL_SOLVE unused (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
   146   let val thy = Proof_Context.theory_of ctxt
   147       val new_skolem =
   148         Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy)
   149       val do_lams =
   150         (lam_trans = liftingN orelse lam_trans = lam_liftingN)
   151         ? introduce_lam_wrappers ctxt
   152       val th_cls_pairs =
   153         map2 (fn j => fn th =>
   154                 (Thm.get_name_hint th,
   155                  th |> Drule.eta_contraction_rule
   156                     |> Meson_Clausify.cnf_axiom ctxt new_skolem (lam_trans = combsN) j
   157                     ||> map do_lams))
   158              (0 upto length ths0 - 1) ths0
   159       val ths = maps (snd o snd) th_cls_pairs
   160       val dischargers = map (fst o snd) th_cls_pairs
   161       val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
   162       val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES")
   163       val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
   164       val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
   165       val type_enc = type_enc_of_string Strict type_enc
   166       val (sym_tab, axioms, ord_info, concealed) =
   167         generate_metis_problem ctxt type_enc lam_trans cls ths
   168       fun get_isa_thm mth Isa_Reflexive_or_Trivial =
   169           reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth
   170         | get_isa_thm mth Isa_Lambda_Lifted =
   171           lam_lifted_of_metis ctxt type_enc sym_tab concealed mth
   172         | get_isa_thm _ (Isa_Raw ith) = ith
   173       val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
   174       val _ = trace_msg ctxt (K "ISABELLE CLAUSES")
   175       val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms
   176       val _ = trace_msg ctxt (K "METIS CLAUSES")
   177       val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
   178       val _ = trace_msg ctxt (K "START METIS PROVE PROCESS")
   179       val ordering =
   180         if Config.get ctxt advisory_simp then
   181           kbo_advisory_simp_ordering (ord_info ())
   182         else
   183           Metis_KnuthBendixOrder.default
   184     fun fall_back () =
   185       (verbose_warning ctxt
   186            ("Falling back on " ^ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "...");
   187        FOL_SOLVE unused fallback_type_encs lam_trans ctxt cls ths0)
   188   in
   189     (case filter (fn t => Thm.prop_of t aconv @{prop False}) cls of
   190        false_th :: _ => [false_th RS @{thm FalseE}]
   191      | [] =>
   192      (case Metis_Resolution.loop (Metis_Resolution.new (resolution_params ordering)
   193          {axioms = axioms |> map fst, conjecture = []}) of
   194        Metis_Resolution.Contradiction mth =>
   195        let
   196          val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ Metis_Thm.toString mth)
   197          val ctxt' = fold Variable.declare_constraints (map Thm.prop_of cls) ctxt
   198                       (*add constraints arising from converting goal to clause form*)
   199          val proof = Metis_Proof.proof mth
   200          val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms
   201          val used = map_filter (used_axioms axioms) proof
   202          val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
   203          val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
   204          val (used_th_cls_pairs, unused_th_cls_pairs) =
   205            List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs
   206          val unused_ths = maps (snd o snd) unused_th_cls_pairs
   207          val unused_names = map fst unused_th_cls_pairs
   208        in
   209          unused := unused_ths;
   210          if not (null unused_names) then
   211            verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused_names)
   212          else
   213            ();
   214          if not (null cls) andalso not (have_common_thm ctxt used cls) then
   215            verbose_warning ctxt "The assumptions are inconsistent"
   216          else
   217            ();
   218          (case result of
   219            (_, ith) :: _ =>
   220            (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
   221             [discharge_skolem_premises ctxt dischargers ith])
   222          | _ => (trace_msg ctxt (K "Metis: No result"); []))
   223        end
   224      | Metis_Resolution.Satisfiable _ =>
   225        (trace_msg ctxt (K "Metis: No first-order proof with the supplied lemmas");
   226         raise METIS_UNPROVABLE ()))
   227     handle METIS_UNPROVABLE () => if null fallback_type_encs then [] else fall_back ()
   228          | METIS_RECONSTRUCT (loc, msg) =>
   229            if null fallback_type_encs then
   230              (verbose_warning ctxt ("Failed to replay Metis proof\n" ^ loc ^ ": " ^ msg); [])
   231            else
   232              fall_back ())
   233   end
   234 
   235 fun neg_clausify ctxt combinators =
   236   single
   237   #> Meson.make_clauses_unsorted ctxt
   238   #> combinators ? map (Meson_Clausify.introduce_combinators_in_theorem ctxt)
   239   #> Meson.finish_cnf
   240 
   241 fun preskolem_tac ctxt st0 =
   242   (if exists (Meson.has_too_many_clauses ctxt)
   243              (Logic.prems_of_goal (Thm.prop_of st0) 1) then
   244      Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex} ctxt) 1
   245      THEN CNF.cnfx_rewrite_tac ctxt 1
   246    else
   247      all_tac) st0
   248 
   249 fun metis_tac_unused type_encs0 lam_trans ctxt ths i st0 =
   250   let
   251     val unused = Unsynchronized.ref []
   252     val type_encs = if null type_encs0 then partial_type_encs else type_encs0
   253     val _ = trace_msg ctxt (fn () =>
   254       "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   255     val type_encs = type_encs |> maps unalias_type_enc
   256     val combs = (lam_trans = combsN)
   257     fun tac clause = resolve_tac ctxt (FOL_SOLVE unused type_encs lam_trans ctxt clause ths) 1
   258     val seq = Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt combs)) tac ctxt i st0
   259   in
   260     (!unused, seq)
   261   end
   262 
   263 fun metis_tac type_encs lam_trans ctxt ths i = snd o metis_tac_unused type_encs lam_trans ctxt ths i
   264 
   265 (* Whenever "X" has schematic type variables, we treat "using X by metis" as "by (metis X)" to
   266    prevent "Subgoal.FOCUS" from freezing the type variables. We don't do it for nonschematic facts
   267    "X" because this breaks a few proofs (in the rare and subtle case where a proof relied on
   268    extensionality not being applied) and brings few benefits. *)
   269 val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o Thm.prop_of
   270 
   271 fun metis_method ((override_type_encs, lam_trans), ths) ctxt facts =
   272   let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in
   273     HEADGOAL (Method.insert_tac nonschem_facts THEN'
   274       CHANGED_PROP o metis_tac (these override_type_encs)
   275         (the_default default_metis_lam_trans lam_trans) ctxt (schem_facts @ ths))
   276   end
   277 
   278 val metis_lam_transs = [hide_lamsN, liftingN, combsN]
   279 
   280 fun set_opt _ x NONE = SOME x
   281   | set_opt get x (SOME x0) =
   282     error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x))
   283 
   284 fun consider_opt s =
   285   if member (op =) metis_lam_transs s then apsnd (set_opt I s) else apfst (set_opt hd [s])
   286 
   287 val parse_metis_options =
   288   Scan.optional
   289       (Args.parens (Args.name -- Scan.option (@{keyword ","} |-- Args.name))
   290        >> (fn (s, s') =>
   291               (NONE, NONE) |> consider_opt s
   292                            |> (case s' of SOME s' => consider_opt s' | _ => I)))
   293       (NONE, NONE)
   294 
   295 val _ =
   296   Theory.setup
   297     (Method.setup @{binding metis}
   298       (Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo metis_method))
   299       "Metis for FOL and HOL problems")
   300 
   301 end;