author blanchet Thu Sep 30 18:59:37 2010 +0200 (2010-09-30) changeset 39894 35ae5cf8c96a parent 39893 25a339e1ff9b child 39895 a91a84b1dfdd
encode number of skolem assumptions in them, for more efficient retrieval later
```     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")
```