encode number of skolem assumptions in them, for more efficient retrieval later
authorblanchet
Thu Sep 30 18:59:37 2010 +0200 (2010-09-30)
changeset 3989435ae5cf8c96a
parent 39893 25a339e1ff9b
child 39895 a91a84b1dfdd
encode number of skolem assumptions in them, for more efficient retrieval later
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/meson_clausify.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Thu Sep 30 00:29:37 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Thu Sep 30 18:59:37 2010 +0200
     1.3 @@ -60,6 +60,12 @@
     1.4  lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
     1.5  by auto
     1.6  
     1.7 +lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))"
     1.8 +unfolding skolem_def COMBK_def by (rule refl)
     1.9 +
    1.10 +lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff]
    1.11 +lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
    1.12 +
    1.13  text{*Theorems for translation to combinators*}
    1.14  
    1.15  lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
     2.1 --- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Thu Sep 30 00:29:37 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Thu Sep 30 18:59:37 2010 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4    val introduce_combinators_in_cterm : cterm -> thm
     2.5    val introduce_combinators_in_theorem : thm -> thm
     2.6    val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
     2.7 -  val cnf_axiom : theory -> bool -> thm -> thm option * thm list
     2.8 +  val cnf_axiom : theory -> bool -> int -> thm -> thm option * thm list
     2.9    val meson_general_tac : Proof.context -> thm list -> int -> tactic
    2.10    val setup: theory -> theory
    2.11  end;
    2.12 @@ -293,7 +293,7 @@
    2.13              val (ct, ctxt) =
    2.14                Variable.import_terms true [t] ctxt
    2.15                |>> the_single |>> cterm_of thy
    2.16 -          in (SOME (th', ct), ct |> Thm.assume, ctxt) end
    2.17 +          in (SOME (th', ct), Thm.assume ct, ctxt) end
    2.18         else
    2.19            (NONE, th, ctxt)
    2.20        end
    2.21 @@ -302,27 +302,32 @@
    2.22    end
    2.23  
    2.24  (* Convert a theorem to CNF, with additional premises due to skolemization. *)
    2.25 -fun cnf_axiom thy new_skolemizer th =
    2.26 +fun cnf_axiom thy new_skolemizer ax_no th =
    2.27    let
    2.28      val ctxt0 = Variable.global_thm_context th
    2.29      val (opt, nnf_th, ctxt) = nnf_axiom new_skolemizer th ctxt0
    2.30 -    fun aux th =
    2.31 +    fun clausify th =
    2.32        Meson.make_cnf (if new_skolemizer then
    2.33                          []
    2.34                        else
    2.35                          map (old_skolem_theorem_from_def thy)
    2.36                              (old_skolem_defs th)) th ctxt
    2.37      val (cnf_ths, ctxt) =
    2.38 -      aux nnf_th
    2.39 -      |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th)
    2.40 +      clausify nnf_th
    2.41 +      |> (fn ([], _) =>
    2.42 +             clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
    2.43             | p => p)
    2.44      val export = Variable.export ctxt ctxt0
    2.45 +    fun intr_imp ct th =
    2.46 +      Thm.instantiate ([], map (pairself (cterm_of @{theory}))
    2.47 +                               [(Var (("i", 1), @{typ nat}),
    2.48 +                                 HOLogic.mk_number @{typ nat} ax_no)])
    2.49 +                      @{thm skolem_COMBK_D}
    2.50 +      RS Thm.implies_intr ct th
    2.51    in
    2.52      (opt |> Option.map (singleton export o fst),
    2.53       cnf_ths |> map (introduce_combinators_in_theorem
    2.54 -                     #> (case opt of
    2.55 -                           SOME (_, ct) => Thm.implies_intr ct
    2.56 -                         | NONE => I))
    2.57 +                     #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
    2.58               |> export
    2.59               |> Meson.finish_cnf
    2.60               |> map Thm.close_derivation)
    2.61 @@ -333,7 +338,7 @@
    2.62    let
    2.63      val thy = ProofContext.theory_of ctxt
    2.64      val ctxt0 = Classical.put_claset HOL_cs ctxt
    2.65 -  in Meson.meson_tac ctxt0 (maps (snd o cnf_axiom thy false) ths) end
    2.66 +  in Meson.meson_tac ctxt0 (maps (snd o cnf_axiom thy false 0) ths) end
    2.67  
    2.68  val setup =
    2.69    Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
     3.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 30 00:29:37 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 30 18:59:37 2010 +0200
     3.3 @@ -147,7 +147,8 @@
     3.4                THEN TRY (REPEAT_ALL_NEW (etac @{thm allE}) 1)
     3.5                THEN match_tac [premises_imp_false] 1
     3.6                THEN DETERM_UNTIL_SOLVED
     3.7 -                       (PRIMITIVE (unify_one_prem_with_concl thy 1)
     3.8 +                       (rtac @{thm skolem_COMBK_I} 1
     3.9 +                        THEN PRIMITIVE (unify_one_prem_with_concl thy 1)
    3.10                          THEN assume_tac 1)))
    3.11      end
    3.12  
    3.13 @@ -157,8 +158,10 @@
    3.14        val type_lits = Config.get ctxt type_lits
    3.15        val new_skolemizer = Config.get ctxt new_skolemizer
    3.16        val th_cls_pairs =
    3.17 -        map (fn th => (Thm.get_name_hint th,
    3.18 -                       Meson_Clausify.cnf_axiom thy new_skolemizer th)) ths0
    3.19 +        map2 (fn j => fn th =>
    3.20 +                (Thm.get_name_hint th,
    3.21 +                 Meson_Clausify.cnf_axiom thy new_skolemizer j th))
    3.22 +             (0 upto length ths0 - 1) ths0
    3.23        val thss = map (snd o snd) th_cls_pairs
    3.24        val dischargers = map_filter (fst o snd) th_cls_pairs
    3.25        val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")