src/HOL/Tools/Metis/metis_tactic.ML
changeset 47039 1b36a05a070d
parent 47015 7e2c4da9ac7d
child 47045 631adf003bb0
equal deleted inserted replaced
47038:2409b484e1cc 47039:1b36a05a070d
    10 signature METIS_TACTIC =
    10 signature METIS_TACTIC =
    11 sig
    11 sig
    12   val trace : bool Config.T
    12   val trace : bool Config.T
    13   val verbose : bool Config.T
    13   val verbose : bool Config.T
    14   val new_skolemizer : bool Config.T
    14   val new_skolemizer : bool Config.T
       
    15   val advisory_simp : bool Config.T
    15   val type_has_top_sort : typ -> bool
    16   val type_has_top_sort : typ -> bool
    16   val metis_tac :
    17   val metis_tac :
    17     string list -> string -> Proof.context -> thm list -> int -> tactic
    18     string list -> string -> Proof.context -> thm list -> int -> tactic
    18   val metis_lam_transs : string list
    19   val metis_lam_transs : string list
    19   val parse_metis_options : (string list option * string option) parser
    20   val parse_metis_options : (string list option * string option) parser
    28 open Metis_Generate
    29 open Metis_Generate
    29 open Metis_Reconstruct
    30 open Metis_Reconstruct
    30 
    31 
    31 val new_skolemizer =
    32 val new_skolemizer =
    32   Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    33   Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
       
    34 val advisory_simp =
       
    35   Attrib.setup_config_bool @{binding metis_advisory_simp} (K false)
    33 
    36 
    34 (* Designed to work also with monomorphic instances of polymorphic theorems. *)
    37 (* Designed to work also with monomorphic instances of polymorphic theorems. *)
    35 fun have_common_thm ths1 ths2 =
    38 fun have_common_thm ths1 ths2 =
    36   exists (member (Term.aconv_untyped o pairself prop_of) ths1)
    39   exists (member (Term.aconv_untyped o pairself prop_of) ths1)
    37          (map Meson.make_meta_clause ths2)
    40          (map Meson.make_meta_clause ths2)
   103       val t0 $ _ $ t2 = prop_of eq_th
   106       val t0 $ _ $ t2 = prop_of eq_th
   104       val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy
   107       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))
   108       val eq_th' = Goal.prove_internal [] eq_ct (K (Tactic.rtac eq_th 1))
   106     in Thm.equal_elim eq_th' th end
   109     in Thm.equal_elim eq_th' th end
   107 
   110 
   108 val clause_params =
   111 fun clause_params ordering =
   109   {ordering = Metis_KnuthBendixOrder.default,
   112   {ordering = ordering,
   110    orderLiterals = Metis_Clause.UnsignedLiteralOrder,
   113    orderLiterals = Metis_Clause.UnsignedLiteralOrder,
   111    orderTerms = true}
   114    orderTerms = true}
   112 val active_params =
   115 fun active_params ordering =
   113   {clause = clause_params,
   116   {clause = clause_params ordering,
   114    prefactor = #prefactor Metis_Active.default,
   117    prefactor = #prefactor Metis_Active.default,
   115    postfactor = #postfactor Metis_Active.default}
   118    postfactor = #postfactor Metis_Active.default}
   116 val waiting_params =
   119 val waiting_params =
   117   {symbolsWeight = 1.0,
   120   {symbolsWeight = 1.0,
   118    variablesWeight = 0.5,
   121    variablesWeight = 0.5,
   119    literalsWeight = 0.1,
   122    literalsWeight = 0.1,
   120    models = []}
   123    models = []}
   121 val resolution_params = {active = active_params, waiting = waiting_params}
   124 fun resolution_params ordering =
       
   125   {active = active_params ordering, waiting = waiting_params}
       
   126 
       
   127 fun kbo_advisory_simp_ordering ord_info =
       
   128   let
       
   129     fun weight (m, _) =
       
   130       AList.lookup (op =) ord_info (Metis_Name.toString m) |> the_default 1
       
   131     fun precedence p =
       
   132       case int_ord (pairself weight p) of
       
   133         EQUAL => #precedence Metis_KnuthBendixOrder.default p
       
   134       | ord => ord
       
   135   in {weight = weight, precedence = precedence} end
   122 
   136 
   123 (* Main function to start Metis proof and reconstruction *)
   137 (* Main function to start Metis proof and reconstruction *)
   124 fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
   138 fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
   125   let val thy = Proof_Context.theory_of ctxt
   139   let val thy = Proof_Context.theory_of ctxt
   126       val new_skolemizer =
   140       val new_skolemizer =
   141       val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
   155       val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
   142       val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   156       val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   143       val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
   157       val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
   144       val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
   158       val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
   145       val type_enc = type_enc_from_string Strict type_enc
   159       val type_enc = type_enc_from_string Strict type_enc
   146       val (sym_tab, axioms, concealed) =
   160       val (sym_tab, axioms, ord_info, concealed) =
   147         prepare_metis_problem ctxt type_enc lam_trans cls ths
   161         prepare_metis_problem ctxt type_enc lam_trans cls ths
   148       fun get_isa_thm mth Isa_Reflexive_or_Trivial =
   162       fun get_isa_thm mth Isa_Reflexive_or_Trivial =
   149           reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
   163           reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
   150         | get_isa_thm mth Isa_Lambda_Lifted =
   164         | get_isa_thm mth Isa_Lambda_Lifted =
   151           lam_lifted_from_metis ctxt type_enc sym_tab concealed mth
   165           lam_lifted_from_metis ctxt type_enc sym_tab concealed mth
   154       val _ = trace_msg ctxt (fn () => "ISABELLE CLAUSES")
   168       val _ = trace_msg ctxt (fn () => "ISABELLE CLAUSES")
   155       val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms
   169       val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms
   156       val _ = trace_msg ctxt (fn () => "METIS CLAUSES")
   170       val _ = trace_msg ctxt (fn () => "METIS CLAUSES")
   157       val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
   171       val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
   158       val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
   172       val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
       
   173       val ordering =
       
   174         if Config.get ctxt advisory_simp then
       
   175           kbo_advisory_simp_ordering (ord_info ())
       
   176         else
       
   177           Metis_KnuthBendixOrder.default
   159   in
   178   in
   160       case filter (fn t => prop_of t aconv @{prop False}) cls of
   179       case filter (fn t => prop_of t aconv @{prop False}) cls of
   161           false_th :: _ => [false_th RS @{thm FalseE}]
   180           false_th :: _ => [false_th RS @{thm FalseE}]
   162         | [] =>
   181         | [] =>
   163       case Metis_Resolution.new resolution_params
   182       case Metis_Resolution.new (resolution_params ordering)
   164                                 {axioms = axioms |> map fst, conjecture = []}
   183                                 {axioms = axioms |> map fst, conjecture = []}
   165            |> Metis_Resolution.loop of
   184            |> Metis_Resolution.loop of
   166           Metis_Resolution.Contradiction mth =>
   185           Metis_Resolution.Contradiction mth =>
   167             let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
   186             let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
   168                           Metis_Thm.toString mth)
   187                           Metis_Thm.toString mth)