src/HOL/Tools/Metis/metis_tactic.ML
author blanchet
Mon Jan 23 17:40:32 2012 +0100 (2012-01-23)
changeset 46320 0b8b73b49848
parent 46301 e2e52c7d25c9
child 46365 547d1a1dcaf6
permissions -rw-r--r--
renamed two files to make room for a new file
     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_skolemizer : bool Config.T
    15   val type_has_top_sort : typ -> bool
    16   val metis_tac :
    17     string list -> string -> Proof.context -> thm list -> int -> tactic
    18   val metis_lam_transs : string list
    19   val parse_metis_options : (string list option * string option) parser
    20   val setup : theory -> theory
    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_skolemizer =
    32   Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    33 
    34 (* Designed to work also with monomorphic instances of polymorphic theorems. *)
    35 fun have_common_thm ths1 ths2 =
    36   exists (member (Term.aconv_untyped o pairself prop_of) ths1)
    37          (map Meson.make_meta_clause 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_from_metis ctxt type_enc sym_tab concealed mth =
    48   let val thy = Proof_Context.theory_of ctxt in
    49     case hol_clause_from_metis ctxt type_enc sym_tab concealed mth of
    50       Const (@{const_name HOL.eq}, _) $ _ $ t =>
    51       let
    52         val ct = cterm_of thy t
    53         val cT = ctyp_of_term ct
    54       in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
    55     | Const (@{const_name disj}, _) $ t1 $ t2 =>
    56       (if can HOLogic.dest_not t1 then t2 else t1)
    57       |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
    58     | _ => raise Fail "expected reflexive or trivial clause"
    59   end
    60   |> Meson.make_meta_clause
    61 
    62 fun lam_lifted_from_metis ctxt type_enc sym_tab concealed mth =
    63   let
    64     val thy = Proof_Context.theory_of ctxt
    65     val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1
    66     val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth
    67     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    68   in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
    69 
    70 fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
    71   | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t
    72   | add_vars_and_frees (t as Var _) = insert (op =) t
    73   | add_vars_and_frees (t as Free _) = insert (op =) t
    74   | add_vars_and_frees _ = I
    75 
    76 fun introduce_lam_wrappers ctxt th =
    77   if Meson_Clausify.is_quasi_lambda_free (prop_of th) then
    78     th
    79   else
    80     let
    81       val thy = Proof_Context.theory_of ctxt
    82       fun conv first ctxt ct =
    83         if Meson_Clausify.is_quasi_lambda_free (term_of ct) then
    84           Thm.reflexive ct
    85         else case term_of ct of
    86           Abs (_, _, u) =>
    87           if first then
    88             case add_vars_and_frees u [] of
    89               [] =>
    90               Conv.abs_conv (conv false o snd) ctxt ct
    91               |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
    92             | v :: _ =>
    93               Abs (Name.uu, fastype_of v, abstract_over (v, term_of ct)) $ v
    94               |> cterm_of thy
    95               |> Conv.comb_conv (conv true ctxt)
    96           else
    97             Conv.abs_conv (conv false o snd) ctxt ct
    98         | Const (@{const_name Meson.skolem}, _) $ _ => Thm.reflexive ct
    99         | _ => Conv.comb_conv (conv true ctxt) ct
   100       val eq_th = conv true ctxt (cprop_of th)
   101       (* We replace the equation's left-hand side with a beta-equivalent term
   102          so that "Thm.equal_elim" works below. *)
   103       val t0 $ _ $ t2 = prop_of eq_th
   104       val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy
   105       val eq_th' = Goal.prove_internal [] eq_ct (K (Tactic.rtac eq_th 1))
   106     in Thm.equal_elim eq_th' th end
   107 
   108 val clause_params =
   109   {ordering = Metis_KnuthBendixOrder.default,
   110    orderLiterals = Metis_Clause.UnsignedLiteralOrder,
   111    orderTerms = true}
   112 val active_params =
   113   {clause = clause_params,
   114    prefactor = #prefactor Metis_Active.default,
   115    postfactor = #postfactor Metis_Active.default}
   116 val waiting_params =
   117   {symbolsWeight = 1.0,
   118    variablesWeight = 0.0,
   119    literalsWeight = 0.0,
   120    models = []}
   121 val resolution_params = {active = active_params, waiting = waiting_params}
   122 
   123 (* Main function to start Metis proof and reconstruction *)
   124 fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
   125   let val thy = Proof_Context.theory_of ctxt
   126       val new_skolemizer =
   127         Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
   128       val do_lams = lam_trans = lam_liftingN ? introduce_lam_wrappers ctxt
   129       val th_cls_pairs =
   130         map2 (fn j => fn th =>
   131                 (Thm.get_name_hint th,
   132                  th |> Drule.eta_contraction_rule
   133                     |> Meson_Clausify.cnf_axiom ctxt new_skolemizer
   134                                                 (lam_trans = combinatorsN) j
   135                     ||> map do_lams))
   136              (0 upto length ths0 - 1) ths0
   137       val ths = maps (snd o snd) th_cls_pairs
   138       val dischargers = map (fst o snd) th_cls_pairs
   139       val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
   140       val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   141       val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
   142       val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
   143       val type_enc = type_enc_from_string Strict type_enc
   144       val (sym_tab, axioms, concealed) =
   145         prepare_metis_problem ctxt type_enc lam_trans cls ths
   146       fun get_isa_thm mth Isa_Reflexive_or_Trivial =
   147           reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
   148         | get_isa_thm mth Isa_Lambda_Lifted =
   149           lam_lifted_from_metis ctxt type_enc sym_tab concealed mth
   150         | get_isa_thm _ (Isa_Raw ith) = ith
   151       val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
   152       val _ = trace_msg ctxt (fn () => "ISABELLE CLAUSES")
   153       val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms
   154       val _ = trace_msg ctxt (fn () => "METIS CLAUSES")
   155       val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
   156       val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
   157   in
   158       case filter (fn t => prop_of t aconv @{prop False}) cls of
   159           false_th :: _ => [false_th RS @{thm FalseE}]
   160         | [] =>
   161       case Metis_Resolution.new resolution_params
   162                                 {axioms = axioms |> map fst, conjecture = []}
   163            |> Metis_Resolution.loop of
   164           Metis_Resolution.Contradiction mth =>
   165             let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
   166                           Metis_Thm.toString mth)
   167                 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
   168                              (*add constraints arising from converting goal to clause form*)
   169                 val proof = Metis_Proof.proof mth
   170                 val result =
   171                   axioms
   172                   |> fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof
   173                 val used = proof |> map_filter (used_axioms axioms)
   174                 val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
   175                 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
   176                 val names = th_cls_pairs |> map fst
   177                 val used_names =
   178                   th_cls_pairs
   179                   |> map_filter (fn (name, (_, cls)) =>
   180                                     if have_common_thm used cls then SOME name
   181                                     else NONE)
   182                 val unused_names = names |> subtract (op =) used_names
   183             in
   184                 if not (null cls) andalso not (have_common_thm used cls) then
   185                   verbose_warning ctxt "The assumptions are inconsistent"
   186                 else
   187                   ();
   188                 if not (null unused_names) then
   189                   "Unused theorems: " ^ commas_quote unused_names
   190                   |> verbose_warning ctxt
   191                 else
   192                   ();
   193                 case result of
   194                     (_,ith)::_ =>
   195                         (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
   196                          [discharge_skolem_premises ctxt dischargers ith])
   197                   | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
   198             end
   199         | Metis_Resolution.Satisfiable _ =>
   200             (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
   201              if null fallback_type_encs then
   202                ()
   203              else
   204                raise METIS ("FOL_SOLVE",
   205                             "No first-order proof with the lemmas supplied");
   206              [])
   207   end
   208   handle METIS (loc, msg) =>
   209          case fallback_type_encs of
   210            [] => error ("Failed to replay Metis proof in Isabelle." ^
   211                         (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
   212                          else ""))
   213          | first_fallback :: _ =>
   214            (verbose_warning ctxt
   215                 ("Falling back on " ^
   216                  quote (metis_call first_fallback lam_trans) ^ "...");
   217             FOL_SOLVE fallback_type_encs lam_trans ctxt cls ths0)
   218 
   219 fun neg_clausify ctxt combinators =
   220   single
   221   #> Meson.make_clauses_unsorted ctxt
   222   #> combinators ? map Meson_Clausify.introduce_combinators_in_theorem
   223   #> Meson.finish_cnf
   224 
   225 fun preskolem_tac ctxt st0 =
   226   (if exists (Meson.has_too_many_clauses ctxt)
   227              (Logic.prems_of_goal (prop_of st0) 1) then
   228      Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
   229      THEN cnf.cnfx_rewrite_tac ctxt 1
   230    else
   231      all_tac) st0
   232 
   233 val type_has_top_sort =
   234   exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
   235 
   236 fun generic_metis_tac type_encs lam_trans ctxt ths i st0 =
   237   let
   238     val _ = trace_msg ctxt (fn () =>
   239         "Metis called with theorems\n" ^
   240         cat_lines (map (Display.string_of_thm ctxt) ths))
   241     val type_encs = type_encs |> maps unalias_type_enc
   242     fun tac clause =
   243       resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1
   244   in
   245     if exists_type type_has_top_sort (prop_of st0) then
   246       verbose_warning ctxt "Proof state contains the universal sort {}"
   247     else
   248       ();
   249     Meson.MESON (preskolem_tac ctxt)
   250         (maps (neg_clausify ctxt (lam_trans = combinatorsN))) tac ctxt i st0
   251   end
   252 
   253 fun metis_tac [] = generic_metis_tac partial_type_encs
   254   | metis_tac type_encs = generic_metis_tac type_encs
   255 
   256 (* Whenever "X" has schematic type variables, we treat "using X by metis" as
   257    "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
   258    We don't do it for nonschematic facts "X" because this breaks a few proofs
   259    (in the rare and subtle case where a proof relied on extensionality not being
   260    applied) and brings few benefits. *)
   261 val has_tvar =
   262   exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
   263 
   264 fun method default_type_encs ((override_type_encs, lam_trans), ths) ctxt facts =
   265   let
   266     val _ =
   267       if default_type_encs = full_type_encs then
   268         legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead"
   269       else
   270         ()
   271     val (schem_facts, nonschem_facts) = List.partition has_tvar facts
   272     val type_encs = override_type_encs |> the_default default_type_encs
   273     val lam_trans = lam_trans |> the_default metis_default_lam_trans
   274   in
   275     HEADGOAL (Method.insert_tac nonschem_facts THEN'
   276               CHANGED_PROP o generic_metis_tac type_encs lam_trans ctxt
   277                                                (schem_facts @ ths))
   278   end
   279 
   280 val metis_lam_transs = [hide_lamsN, lam_liftingN, combinatorsN]
   281 
   282 fun set_opt _ x NONE = SOME x
   283   | set_opt get x (SOME x0) =
   284     error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x) ^
   285            ".")
   286 fun consider_opt s =
   287   if member (op =) metis_lam_transs s then apsnd (set_opt I s)
   288   else apfst (set_opt hd [s])
   289 
   290 val parse_metis_options =
   291   Scan.optional
   292       (Args.parens (Parse.short_ident
   293                     -- Scan.option (Parse.$$$ "," |-- Parse.short_ident))
   294        >> (fn (s, s') =>
   295               (NONE, NONE) |> consider_opt s
   296                            |> (case s' of SOME s' => consider_opt s' | _ => I)))
   297       (NONE, NONE)
   298 
   299 fun setup_method (binding, type_encs) =
   300   Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo method type_encs)
   301   |> Method.setup binding
   302 
   303 val setup =
   304   [((@{binding metis}, partial_type_encs),
   305     "Metis for FOL and HOL problems"),
   306    ((@{binding metisFT}, full_type_encs),
   307     "Metis for FOL/HOL problems with fully-typed translation")]
   308   |> fold (uncurry setup_method)
   309 
   310 end;