# HG changeset patch # User wenzelm # Date 1565257242 -7200 # Node ID 12d1e6e2c1d07c6babdc05ad50a3f6fad66b353e # Parent c7ef6685c943010066b3ae5a66d2df32b3af4be2 tuned whitespace -- slightly more readable; diff -r c7ef6685c943 -r 12d1e6e2c1d0 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Thu Aug 08 11:25:29 2019 +0200 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu Aug 08 11:40:42 2019 +0200 @@ -49,13 +49,13 @@ fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth = (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of Const (\<^const_name>\HOL.eq\, _) $ _ $ t => - let - val ct = Thm.cterm_of ctxt t - val cT = Thm.ctyp_of_cterm ct - in refl |> Thm.instantiate' [SOME cT] [SOME ct] end + let + val ct = Thm.cterm_of ctxt t + val cT = Thm.ctyp_of_cterm ct + in refl |> Thm.instantiate' [SOME cT] [SOME ct] end | Const (\<^const_name>\disj\, _) $ t1 $ t2 => - (if can HOLogic.dest_not t1 then t2 else t1) - |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial + (if can HOLogic.dest_not t1 then t2 else t1) + |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial | _ => raise Fail "expected reflexive or trivial clause") |> Meson.make_meta_clause ctxt @@ -64,7 +64,10 @@ val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac ctxt [refl] 1 val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t) - in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause ctxt end + in + Goal.prove_internal ctxt [] ct (K tac) + |> Meson.make_meta_clause ctxt + end fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u] | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t @@ -73,27 +76,24 @@ | add_vars_and_frees _ = I fun introduce_lam_wrappers ctxt th = - if Meson_Clausify.is_quasi_lambda_free (Thm.prop_of th) then - th + if Meson_Clausify.is_quasi_lambda_free (Thm.prop_of th) then th else let fun conv first ctxt ct = - if Meson_Clausify.is_quasi_lambda_free (Thm.term_of ct) then - Thm.reflexive ct + if Meson_Clausify.is_quasi_lambda_free (Thm.term_of ct) then Thm.reflexive ct else (case Thm.term_of ct of Abs (_, _, u) => - if first then - (case add_vars_and_frees u [] of - [] => - Conv.abs_conv (conv false o snd) ctxt ct - |> (fn th => Meson.first_order_resolve ctxt th @{thm Metis.eq_lambdaI}) - | v :: _ => - Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v - |> Thm.cterm_of ctxt - |> Conv.comb_conv (conv true ctxt)) - else - Conv.abs_conv (conv false o snd) ctxt ct + if first then + (case add_vars_and_frees u [] of + [] => + Conv.abs_conv (conv false o snd) ctxt ct + |> (fn th => Meson.first_order_resolve ctxt th @{thm Metis.eq_lambdaI}) + | v :: _ => + Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v + |> Thm.cterm_of ctxt + |> Conv.comb_conv (conv true ctxt)) + else Conv.abs_conv (conv false o snd) ctxt ct | Const (\<^const_name>\Meson.skolem\, _) $ _ => Thm.reflexive ct | _ => Conv.comb_conv (conv true ctxt) ct) val eq_th = conv true ctxt (Thm.cprop_of th) @@ -145,94 +145,98 @@ (* Main function to start Metis proof and reconstruction *) fun FOL_SOLVE unused type_encs lam_trans ctxt cls ths0 = - let val thy = Proof_Context.theory_of ctxt - val type_enc :: fallback_type_encs = type_encs - val new_skolem = - Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy) - val do_lams = - (lam_trans = liftingN orelse lam_trans = lam_liftingN) - ? introduce_lam_wrappers ctxt - val th_cls_pairs = - map2 (fn j => fn th => - (Thm.get_name_hint th, - th |> Drule.eta_contraction_rule - |> Meson_Clausify.cnf_axiom ctxt new_skolem (lam_trans = combsN) j - ||> map do_lams)) - (0 upto length ths0 - 1) ths0 - val ths = maps (snd o snd) th_cls_pairs - val dischargers = map (fst o snd) th_cls_pairs - val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) - val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES") - val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls - val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) - val type_enc = type_enc_of_string Strict type_enc - val (sym_tab, axioms, ord_info, concealed) = - generate_metis_problem ctxt type_enc lam_trans cls ths - fun get_isa_thm mth Isa_Reflexive_or_Trivial = + let + val thy = Proof_Context.theory_of ctxt + + val new_skolem = Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy) + val do_lams = + (lam_trans = liftingN orelse lam_trans = lam_liftingN) ? introduce_lam_wrappers ctxt + val th_cls_pairs = + map2 (fn j => fn th => + (Thm.get_name_hint th, + th + |> Drule.eta_contraction_rule + |> Meson_Clausify.cnf_axiom ctxt new_skolem (lam_trans = combsN) j + ||> map do_lams)) + (0 upto length ths0 - 1) ths0 + val ths = maps (snd o snd) th_cls_pairs + val dischargers = map (fst o snd) th_cls_pairs + val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) + val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES") + val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls + + val type_enc :: fallback_type_encs = type_encs + val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) + val type_enc = type_enc_of_string Strict type_enc + + val (sym_tab, axioms, ord_info, concealed) = + generate_metis_problem ctxt type_enc lam_trans cls ths + fun get_isa_thm mth Isa_Reflexive_or_Trivial = reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth - | get_isa_thm mth Isa_Lambda_Lifted = + | get_isa_thm mth Isa_Lambda_Lifted = lam_lifted_of_metis ctxt type_enc sym_tab concealed mth - | get_isa_thm _ (Isa_Raw ith) = ith - val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) - val _ = trace_msg ctxt (K "ISABELLE CLAUSES") - val _ = List.app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms - val _ = trace_msg ctxt (K "METIS CLAUSES") - val _ = List.app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms - val _ = trace_msg ctxt (K "START METIS PROVE PROCESS") - val ordering = - if Config.get ctxt advisory_simp then - kbo_advisory_simp_ordering (ord_info ()) - else - Metis_KnuthBendixOrder.default + | get_isa_thm _ (Isa_Raw ith) = ith + val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) + val _ = trace_msg ctxt (K "ISABELLE CLAUSES") + val _ = List.app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms + val _ = trace_msg ctxt (K "METIS CLAUSES") + val _ = List.app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms + + val _ = trace_msg ctxt (K "START METIS PROVE PROCESS") + val ordering = + if Config.get ctxt advisory_simp + then kbo_advisory_simp_ordering (ord_info ()) + else Metis_KnuthBendixOrder.default + fun fall_back () = (verbose_warning ctxt - ("Falling back on " ^ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "..."); + ("Falling back on " ^ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "..."); FOL_SOLVE unused fallback_type_encs lam_trans ctxt cls ths0) in (case filter (fn t => Thm.prop_of t aconv \<^prop>\False\) cls of - false_th :: _ => [false_th RS @{thm FalseE}] - | [] => - (case Metis_Resolution.loop (Metis_Resolution.new (resolution_params ordering) - {axioms = axioms |> map fst, conjecture = []}) of - Metis_Resolution.Contradiction mth => - let - val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ Metis_Thm.toString mth) - val ctxt' = fold Variable.declare_constraints (map Thm.prop_of cls) ctxt - (*add constraints arising from converting goal to clause form*) - val proof = Metis_Proof.proof mth - val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms - val used = map_filter (used_axioms axioms) proof - val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:") - val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used - val (used_th_cls_pairs, unused_th_cls_pairs) = - List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs - val unused_ths = maps (snd o snd) unused_th_cls_pairs - val unused_names = map fst unused_th_cls_pairs - in - unused := unused_ths; - if not (null unused_names) then - verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused_names) - else - (); - if not (null cls) andalso not (have_common_thm ctxt used cls) then - verbose_warning ctxt "The assumptions are inconsistent" - else - (); - (case result of - (_, ith) :: _ => - (trace_msg ctxt (fn () => "Success: " ^ Thm.string_of_thm ctxt ith); - [discharge_skolem_premises ctxt dischargers ith]) - | _ => (trace_msg ctxt (K "Metis: No result"); [])) - end - | Metis_Resolution.Satisfiable _ => - (trace_msg ctxt (K "Metis: No first-order proof with the supplied lemmas"); - raise METIS_UNPROVABLE ())) - handle METIS_UNPROVABLE () => if null fallback_type_encs then [] else fall_back () - | METIS_RECONSTRUCT (loc, msg) => - if null fallback_type_encs then - (verbose_warning ctxt ("Failed to replay Metis proof\n" ^ loc ^ ": " ^ msg); []) - else - fall_back ()) + false_th :: _ => [false_th RS @{thm FalseE}] + | [] => + (case Metis_Resolution.loop (Metis_Resolution.new (resolution_params ordering) + {axioms = axioms |> map fst, conjecture = []}) of + Metis_Resolution.Contradiction mth => + let + val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ Metis_Thm.toString mth) + val ctxt' = fold Variable.declare_constraints (map Thm.prop_of cls) ctxt + (*add constraints arising from converting goal to clause form*) + val proof = Metis_Proof.proof mth + val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms + val used = map_filter (used_axioms axioms) proof + val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:") + val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used + val (used_th_cls_pairs, unused_th_cls_pairs) = + List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs + val unused_ths = maps (snd o snd) unused_th_cls_pairs + val unused_names = map fst unused_th_cls_pairs + + val _ = unused := unused_ths; + val _ = + if not (null unused_names) then + verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused_names) + else (); + val _ = + if not (null cls) andalso not (have_common_thm ctxt used cls) then + verbose_warning ctxt "The assumptions are inconsistent" + else (); + in + (case result of + (_, ith) :: _ => + (trace_msg ctxt (fn () => "Success: " ^ Thm.string_of_thm ctxt ith); + [discharge_skolem_premises ctxt dischargers ith]) + | _ => (trace_msg ctxt (K "Metis: No result"); [])) + end + | Metis_Resolution.Satisfiable _ => + (trace_msg ctxt (K "Metis: No first-order proof with the supplied lemmas"); + raise METIS_UNPROVABLE ())) + handle METIS_UNPROVABLE () => if null fallback_type_encs then [] else fall_back () + | METIS_RECONSTRUCT (loc, msg) => + if null fallback_type_encs then + (verbose_warning ctxt ("Failed to replay Metis proof\n" ^ loc ^ ": " ^ msg); []) + else fall_back ()) end fun neg_clausify ctxt combinators =