1.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML Fri Sep 02 14:43:20 2011 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,268 +0,0 @@
1.4 -(* Title: HOL/Tools/Metis/metis_tactics.ML
1.5 - Author: Kong W. Susanto, Cambridge University Computer Laboratory
1.6 - Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
1.7 - Author: Jasmin Blanchette, TU Muenchen
1.8 - Copyright Cambridge University 2007
1.9 -
1.10 -HOL setup for the Metis prover.
1.11 -*)
1.12 -
1.13 -signature METIS_TACTICS =
1.14 -sig
1.15 - val metisN : string
1.16 - val full_typesN : string
1.17 - val partial_typesN : string
1.18 - val no_typesN : string
1.19 - val really_full_type_enc : string
1.20 - val full_type_enc : string
1.21 - val partial_type_enc : string
1.22 - val no_type_enc : string
1.23 - val full_type_syss : string list
1.24 - val partial_type_syss : string list
1.25 - val trace : bool Config.T
1.26 - val verbose : bool Config.T
1.27 - val new_skolemizer : bool Config.T
1.28 - val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
1.29 - val setup : theory -> theory
1.30 -end
1.31 -
1.32 -structure Metis_Tactics : METIS_TACTICS =
1.33 -struct
1.34 -
1.35 -open ATP_Translate
1.36 -open Metis_Translate
1.37 -open Metis_Reconstruct
1.38 -
1.39 -val metisN = "metis"
1.40 -
1.41 -val full_typesN = "full_types"
1.42 -val partial_typesN = "partial_types"
1.43 -val no_typesN = "no_types"
1.44 -
1.45 -val really_full_type_enc = "mono_tags_uniform"
1.46 -val full_type_enc = "poly_guards_uniform_query"
1.47 -val partial_type_enc = "poly_args"
1.48 -val no_type_enc = "erased"
1.49 -
1.50 -val full_type_syss = [full_type_enc, really_full_type_enc]
1.51 -val partial_type_syss = partial_type_enc :: full_type_syss
1.52 -
1.53 -val type_enc_aliases =
1.54 - [(full_typesN, full_type_syss),
1.55 - (partial_typesN, partial_type_syss),
1.56 - (no_typesN, [no_type_enc])]
1.57 -
1.58 -fun method_call_for_type_enc type_syss =
1.59 - metisN ^ " (" ^
1.60 - (case AList.find (op =) type_enc_aliases type_syss of
1.61 - [alias] => alias
1.62 - | _ => hd type_syss) ^ ")"
1.63 -
1.64 -val new_skolemizer =
1.65 - Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
1.66 -
1.67 -(* Designed to work also with monomorphic instances of polymorphic theorems. *)
1.68 -fun have_common_thm ths1 ths2 =
1.69 - exists (member (Term.aconv_untyped o pairself prop_of) ths1)
1.70 - (map Meson.make_meta_clause ths2)
1.71 -
1.72 -(*Determining which axiom clauses are actually used*)
1.73 -fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
1.74 - | used_axioms _ _ = NONE
1.75 -
1.76 -(* Lightweight predicate type information comes in two flavors, "t = t'" and
1.77 - "t => t'", where "t" and "t'" are the same term modulo type tags.
1.78 - In Isabelle, type tags are stripped away, so we are left with "t = t" or
1.79 - "t => t". Type tag idempotence is also handled this way. *)
1.80 -fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth =
1.81 - let val thy = Proof_Context.theory_of ctxt in
1.82 - case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of
1.83 - Const (@{const_name HOL.eq}, _) $ _ $ t =>
1.84 - let
1.85 - val ct = cterm_of thy t
1.86 - val cT = ctyp_of_term ct
1.87 - in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
1.88 - | Const (@{const_name disj}, _) $ t1 $ t2 =>
1.89 - (if can HOLogic.dest_not t1 then t2 else t1)
1.90 - |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
1.91 - | _ => raise Fail "unexpected tags sym clause"
1.92 - end
1.93 - |> Meson.make_meta_clause
1.94 -
1.95 -val clause_params =
1.96 - {ordering = Metis_KnuthBendixOrder.default,
1.97 - orderLiterals = Metis_Clause.UnsignedLiteralOrder,
1.98 - orderTerms = true}
1.99 -val active_params =
1.100 - {clause = clause_params,
1.101 - prefactor = #prefactor Metis_Active.default,
1.102 - postfactor = #postfactor Metis_Active.default}
1.103 -val waiting_params =
1.104 - {symbolsWeight = 1.0,
1.105 - variablesWeight = 0.0,
1.106 - literalsWeight = 0.0,
1.107 - models = []}
1.108 -val resolution_params = {active = active_params, waiting = waiting_params}
1.109 -
1.110 -(* Main function to start Metis proof and reconstruction *)
1.111 -fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
1.112 - let val thy = Proof_Context.theory_of ctxt
1.113 - val new_skolemizer =
1.114 - Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
1.115 - val th_cls_pairs =
1.116 - map2 (fn j => fn th =>
1.117 - (Thm.get_name_hint th,
1.118 - Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
1.119 - (0 upto length ths0 - 1) ths0
1.120 - val ths = maps (snd o snd) th_cls_pairs
1.121 - val dischargers = map (fst o snd) th_cls_pairs
1.122 - val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
1.123 - val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
1.124 - val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
1.125 - val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
1.126 - val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
1.127 - val type_enc = type_enc_from_string Sound type_enc
1.128 - val (sym_tab, axioms, old_skolems) =
1.129 - prepare_metis_problem ctxt type_enc cls ths
1.130 - fun get_isa_thm mth Isa_Reflexive_or_Trivial =
1.131 - reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth
1.132 - | get_isa_thm _ (Isa_Raw ith) = ith
1.133 - val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
1.134 - val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
1.135 - val thms = axioms |> map fst
1.136 - val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
1.137 - val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
1.138 - in
1.139 - case filter (fn t => prop_of t aconv @{prop False}) cls of
1.140 - false_th :: _ => [false_th RS @{thm FalseE}]
1.141 - | [] =>
1.142 - case Metis_Resolution.new resolution_params
1.143 - {axioms = thms, conjecture = []}
1.144 - |> Metis_Resolution.loop of
1.145 - Metis_Resolution.Contradiction mth =>
1.146 - let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
1.147 - Metis_Thm.toString mth)
1.148 - val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
1.149 - (*add constraints arising from converting goal to clause form*)
1.150 - val proof = Metis_Proof.proof mth
1.151 - val result =
1.152 - axioms
1.153 - |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof
1.154 - val used = map_filter (used_axioms axioms) proof
1.155 - val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
1.156 - val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
1.157 - val names = th_cls_pairs |> map fst
1.158 - val used_names =
1.159 - th_cls_pairs
1.160 - |> map_filter (fn (name, (_, cls)) =>
1.161 - if have_common_thm used cls then SOME name
1.162 - else NONE)
1.163 - val unused_names = names |> subtract (op =) used_names
1.164 - in
1.165 - if not (null cls) andalso not (have_common_thm used cls) then
1.166 - verbose_warning ctxt "The assumptions are inconsistent"
1.167 - else
1.168 - ();
1.169 - if not (null unused_names) then
1.170 - "Unused theorems: " ^ commas_quote unused_names
1.171 - |> verbose_warning ctxt
1.172 - else
1.173 - ();
1.174 - case result of
1.175 - (_,ith)::_ =>
1.176 - (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
1.177 - [discharge_skolem_premises ctxt dischargers ith])
1.178 - | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
1.179 - end
1.180 - | Metis_Resolution.Satisfiable _ =>
1.181 - (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
1.182 - if null fallback_type_syss then
1.183 - ()
1.184 - else
1.185 - raise METIS ("FOL_SOLVE",
1.186 - "No first-order proof with the lemmas supplied");
1.187 - [])
1.188 - end
1.189 - handle METIS (loc, msg) =>
1.190 - case fallback_type_syss of
1.191 - [] => error ("Failed to replay Metis proof in Isabelle." ^
1.192 - (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
1.193 - else ""))
1.194 - | _ =>
1.195 - (verbose_warning ctxt
1.196 - ("Falling back on " ^
1.197 - quote (method_call_for_type_enc fallback_type_syss) ^ "...");
1.198 - FOL_SOLVE fallback_type_syss ctxt cls ths0)
1.199 -
1.200 -fun neg_clausify ctxt =
1.201 - single
1.202 - #> Meson.make_clauses_unsorted ctxt
1.203 - #> map Meson_Clausify.introduce_combinators_in_theorem
1.204 - #> Meson.finish_cnf
1.205 -
1.206 -fun preskolem_tac ctxt st0 =
1.207 - (if exists (Meson.has_too_many_clauses ctxt)
1.208 - (Logic.prems_of_goal (prop_of st0) 1) then
1.209 - Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
1.210 - THEN cnf.cnfx_rewrite_tac ctxt 1
1.211 - else
1.212 - all_tac) st0
1.213 -
1.214 -val type_has_top_sort =
1.215 - exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
1.216 -
1.217 -fun generic_metis_tac type_syss ctxt ths i st0 =
1.218 - let
1.219 - val _ = trace_msg ctxt (fn () =>
1.220 - "Metis called with theorems\n" ^
1.221 - cat_lines (map (Display.string_of_thm ctxt) ths))
1.222 - fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1
1.223 - in
1.224 - if exists_type type_has_top_sort (prop_of st0) then
1.225 - verbose_warning ctxt "Proof state contains the universal sort {}"
1.226 - else
1.227 - ();
1.228 - Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0
1.229 - end
1.230 -
1.231 -fun metis_tac [] = generic_metis_tac partial_type_syss
1.232 - | metis_tac type_syss = generic_metis_tac type_syss
1.233 -
1.234 -(* Whenever "X" has schematic type variables, we treat "using X by metis" as
1.235 - "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
1.236 - We don't do it for nonschematic facts "X" because this breaks a few proofs
1.237 - (in the rare and subtle case where a proof relied on extensionality not being
1.238 - applied) and brings few benefits. *)
1.239 -val has_tvar =
1.240 - exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
1.241 -
1.242 -fun method default_type_syss (override_type_syss, ths) ctxt facts =
1.243 - let
1.244 - val _ =
1.245 - if default_type_syss = full_type_syss then
1.246 - legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead"
1.247 - else
1.248 - ()
1.249 - val (schem_facts, nonschem_facts) = List.partition has_tvar facts
1.250 - val type_syss = override_type_syss |> the_default default_type_syss
1.251 - in
1.252 - HEADGOAL (Method.insert_tac nonschem_facts THEN'
1.253 - CHANGED_PROP
1.254 - o generic_metis_tac type_syss ctxt (schem_facts @ ths))
1.255 - end
1.256 -
1.257 -fun setup_method (binding, type_syss) =
1.258 - ((Args.parens (Scan.repeat Parse.short_ident)
1.259 - >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s]))
1.260 - |> Scan.option |> Scan.lift)
1.261 - -- Attrib.thms >> (METHOD oo method type_syss)
1.262 - |> Method.setup binding
1.263 -
1.264 -val setup =
1.265 - [((@{binding metis}, partial_type_syss),
1.266 - "Metis for FOL and HOL problems"),
1.267 - ((@{binding metisFT}, full_type_syss),
1.268 - "Metis for FOL/HOL problems with fully-typed translation")]
1.269 - |> fold (uncurry setup_method)
1.270 -
1.271 -end;