src/HOL/Tools/Sledgehammer/clausifier.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 37629 a4f129820562
child 37995 06f02b15ef8a
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37574
b8c1f4c46983 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents: 37572
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/clausifier.ML
33311
49cd8abb2863 proper header;
wenzelm
parents: 33306
diff changeset
     2
    Author:     Jia Meng, Cambridge University Computer Laboratory
36393
be73a2b2443b support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents: 36228
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
     4
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
     5
Transformation of axiom rules (elim/intro/etc) into CNF forms.
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
     6
*)
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
     7
37574
b8c1f4c46983 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents: 37572
diff changeset
     8
signature CLAUSIFIER =
21505
13d4dba99337 prefer Proof.context over Context.generic;
wenzelm
parents: 21470
diff changeset
     9
sig
37628
78334f400ae6 Sledgehammer can save some msecs by cheating
blanchet
parents: 37626
diff changeset
    10
  val cnf_axiom: theory -> bool -> thm -> thm list
37620
537beae999d7 remove obsolete component of CNF clause tuple (and reorder it)
blanchet
parents: 37618
diff changeset
    11
  val cnf_rules_pairs :
37628
78334f400ae6 Sledgehammer can save some msecs by cheating
blanchet
parents: 37626
diff changeset
    12
    theory -> bool -> (string * thm) list -> ((string * int) * thm) list
36398
de8522a5cbae make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet
parents: 36394
diff changeset
    13
  val neg_clausify: thm -> thm list
de8522a5cbae make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet
parents: 36394
diff changeset
    14
  val neg_conjecture_clauses:
de8522a5cbae make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet
parents: 36394
diff changeset
    15
    Proof.context -> thm -> int -> thm list list * (string * typ) list
21505
13d4dba99337 prefer Proof.context over Context.generic;
wenzelm
parents: 21470
diff changeset
    16
end;
19196
62ee8c10d796 Added functions to retrieve local and global atpset rules.
mengj
parents: 19175
diff changeset
    17
37574
b8c1f4c46983 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents: 37572
diff changeset
    18
structure Clausifier : CLAUSIFIER =
15997
c71031d7988c consolidation and simplification
paulson
parents: 15956
diff changeset
    19
struct
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    20
15997
c71031d7988c consolidation and simplification
paulson
parents: 15956
diff changeset
    21
(**** Transformation of Elimination Rules into First-Order Formulas****)
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    22
29064
70a61d58460e more antiquotations;
wenzelm
parents: 28965
diff changeset
    23
val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
70a61d58460e more antiquotations;
wenzelm
parents: 28965
diff changeset
    24
val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
    25
21430
77651b6d9d6c New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents: 21290
diff changeset
    26
(*Converts an elim-rule into an equivalent theorem that does not have the
77651b6d9d6c New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents: 21290
diff changeset
    27
  predicate variable.  Leaves other theorems unchanged.  We simply instantiate the
77651b6d9d6c New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents: 21290
diff changeset
    28
  conclusion variable to False.*)
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
    29
fun transform_elim th =
21430
77651b6d9d6c New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents: 21290
diff changeset
    30
  case concl_of th of    (*conclusion variable*)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35870
diff changeset
    31
       @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
29064
70a61d58460e more antiquotations;
wenzelm
parents: 28965
diff changeset
    32
           Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35870
diff changeset
    33
    | v as Var(_, @{typ prop}) =>
29064
70a61d58460e more antiquotations;
wenzelm
parents: 28965
diff changeset
    34
           Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
21430
77651b6d9d6c New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents: 21290
diff changeset
    35
    | _ => th;
15997
c71031d7988c consolidation and simplification
paulson
parents: 15956
diff changeset
    36
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
    37
(*To enforce single-threading*)
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
    38
exception Clausify_failure of theory;
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
    39
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
    40
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
    41
(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
    42
37410
2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents: 37403
diff changeset
    43
fun mk_skolem_id t =
37436
2d76997730a6 found missing beta-eta-contraction
blanchet
parents: 37419
diff changeset
    44
  let val T = fastype_of t in
37496
9ae78e12e126 reintroduce new Sledgehammer polymorphic handling code;
blanchet
parents: 37488
diff changeset
    45
    Const (@{const_name skolem_id}, T --> T) $ t
37436
2d76997730a6 found missing beta-eta-contraction
blanchet
parents: 37419
diff changeset
    46
  end
37410
2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents: 37403
diff changeset
    47
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    48
fun beta_eta_under_lambdas (Abs (s, T, t')) =
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    49
    Abs (s, T, beta_eta_under_lambdas t')
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    50
  | beta_eta_under_lambdas t = Envir.beta_eta_contract t
37512
ff72d3ddc898 this looks like the most appropriate place to do the beta-eta-contraction
blanchet
parents: 37511
diff changeset
    51
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
    52
(*Traverse a theorem, accumulating Skolem function definitions.*)
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    53
fun assume_skolem_funs th =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37349
diff changeset
    54
  let
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    55
    fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) rhss =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37349
diff changeset
    56
        (*Existential: declare a Skolem function, then insert into body and continue*)
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37349
diff changeset
    57
        let
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    58
          val args = OldTerm.term_frees body
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37349
diff changeset
    59
          val Ts = map type_of args
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37349
diff changeset
    60
          val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
37500
7587b6e63454 thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents: 37498
diff changeset
    61
          (* Forms a lambda-abstraction over the formal parameters *)
7587b6e63454 thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents: 37498
diff changeset
    62
          val rhs =
7587b6e63454 thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents: 37498
diff changeset
    63
            list_abs_free (map dest_Free args,
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    64
                           HOLogic.choice_const T $ beta_eta_under_lambdas body)
37518
efb0923cc098 use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code
blanchet
parents: 37512
diff changeset
    65
            |> mk_skolem_id
efb0923cc098 use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code
blanchet
parents: 37512
diff changeset
    66
          val comb = list_comb (rhs, args)
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    67
        in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    68
      | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37349
diff changeset
    69
        (*Universal quant: insert a free variable into body and continue*)
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37349
diff changeset
    70
        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    71
        in dec_sko (subst_bound (Free(fname,T), p)) rhss end
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    72
      | dec_sko (@{const "op &"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    73
      | dec_sko (@{const "op |"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    74
      | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    75
      | dec_sko _ rhss = rhss
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
    76
  in  dec_sko (prop_of th) []  end;
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
    77
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
    78
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
    79
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
    80
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
    81
(*Returns the vars of a theorem*)
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
    82
fun vars_of_thm th =
22691
290454649b8c Thm.fold_terms;
wenzelm
parents: 22644
diff changeset
    83
  map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
    84
37540
48273d1ea331 better eta-expansion in Sledgehammer's clausification;
blanchet
parents: 37518
diff changeset
    85
val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
    86
37540
48273d1ea331 better eta-expansion in Sledgehammer's clausification;
blanchet
parents: 37518
diff changeset
    87
(* Removes the lambdas from an equation of the form t = (%x. u). *)
48273d1ea331 better eta-expansion in Sledgehammer's clausification;
blanchet
parents: 37518
diff changeset
    88
fun extensionalize th =
48273d1ea331 better eta-expansion in Sledgehammer's clausification;
blanchet
parents: 37518
diff changeset
    89
  case prop_of th of
48273d1ea331 better eta-expansion in Sledgehammer's clausification;
blanchet
parents: 37518
diff changeset
    90
    _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
48273d1ea331 better eta-expansion in Sledgehammer's clausification;
blanchet
parents: 37518
diff changeset
    91
         $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
48273d1ea331 better eta-expansion in Sledgehammer's clausification;
blanchet
parents: 37518
diff changeset
    92
  | _ => th
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
    93
37416
d5ac8280497e no point in introducing combinators for inlined Skolem functions
blanchet
parents: 37410
diff changeset
    94
fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
d5ac8280497e no point in introducing combinators for inlined Skolem functions
blanchet
parents: 37410
diff changeset
    95
  | is_quasi_lambda_free (t1 $ t2) =
d5ac8280497e no point in introducing combinators for inlined Skolem functions
blanchet
parents: 37410
diff changeset
    96
    is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
d5ac8280497e no point in introducing combinators for inlined Skolem functions
blanchet
parents: 37410
diff changeset
    97
  | is_quasi_lambda_free (Abs _) = false
d5ac8280497e no point in introducing combinators for inlined Skolem functions
blanchet
parents: 37410
diff changeset
    98
  | is_quasi_lambda_free _ = true
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
    99
32010
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 31794
diff changeset
   100
val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 31794
diff changeset
   101
val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 31794
diff changeset
   102
val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
20863
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
   103
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   104
(*FIXME: requires more use of cterm constructors*)
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   105
fun abstract ct =
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   106
  let
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
   107
      val thy = theory_of_cterm ct
25256
fe467fdf129a Catch exceptions arising during the abstraction operation.
paulson
parents: 25243
diff changeset
   108
      val Abs(x,_,body) = term_of ct
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents: 35870
diff changeset
   109
      val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   110
      val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   111
      fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   112
  in
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   113
      case body of
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   114
          Const _ => makeK()
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   115
        | Free _ => makeK()
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   116
        | Var _ => makeK()  (*though Var isn't expected*)
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   117
        | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   118
        | rator$rand =>
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   119
            if loose_bvar1 (rator,0) then (*C or S*)
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   120
               if loose_bvar1 (rand,0) then (*S*)
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   121
                 let val crator = cterm_of thy (Abs(x,xT,rator))
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   122
                     val crand = cterm_of thy (Abs(x,xT,rand))
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   123
                     val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   124
                     val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   125
                 in
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   126
                   Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   127
                 end
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   128
               else (*C*)
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   129
                 let val crator = cterm_of thy (Abs(x,xT,rator))
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   130
                     val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   131
                     val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   132
                 in
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   133
                   Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   134
                 end
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   135
            else if loose_bvar1 (rand,0) then (*B or eta*)
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36603
diff changeset
   136
               if rand = Bound 0 then Thm.eta_conversion ct
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   137
               else (*B*)
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   138
                 let val crand = cterm_of thy (Abs(x,xT,rand))
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   139
                     val crator = cterm_of thy rator
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   140
                     val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   141
                     val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   142
                 in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   143
            else makeK()
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   144
        | _ => raise Fail "abstract: Bad term"
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   145
  end;
20863
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
   146
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   147
(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   148
fun do_introduce_combinators ct =
37416
d5ac8280497e no point in introducing combinators for inlined Skolem functions
blanchet
parents: 37410
diff changeset
   149
  if is_quasi_lambda_free (term_of ct) then
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   150
    Thm.reflexive ct
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   151
  else case term_of ct of
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   152
    Abs _ =>
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   153
    let
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   154
      val (cv, cta) = Thm.dest_abs NONE ct
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   155
      val (v, _) = dest_Free (term_of cv)
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   156
      val u_th = do_introduce_combinators cta
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   157
      val cu = Thm.rhs_of u_th
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   158
      val comb_eq = abstract (Thm.cabs cv cu)
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   159
    in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   160
  | _ $ _ =>
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   161
    let val (ct1, ct2) = Thm.dest_comb ct in
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   162
        Thm.combination (do_introduce_combinators ct1)
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   163
                        (do_introduce_combinators ct2)
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   164
    end
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   165
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   166
fun introduce_combinators th =
37416
d5ac8280497e no point in introducing combinators for inlined Skolem functions
blanchet
parents: 37410
diff changeset
   167
  if is_quasi_lambda_free (prop_of th) then
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   168
    th
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   169
  else
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   170
    let
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   171
      val th = Drule.eta_contraction_rule th
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   172
      val eqth = do_introduce_combinators (cprop_of th)
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   173
    in Thm.equal_elim eqth th end
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   174
    handle THM (msg, _, _) =>
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   175
           (warning ("Error in the combinator translation of " ^
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   176
                     Display.string_of_thm_without_context th ^
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   177
                     "\nException message: " ^ msg ^ ".");
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   178
            (* A type variable of sort "{}" will make abstraction fail. *)
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   179
            TrueI)
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   180
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   181
(*cterms are used throughout for efficiency*)
29064
70a61d58460e more antiquotations;
wenzelm
parents: 28965
diff changeset
   182
val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   183
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   184
(*Given an abstraction over n variables, replace the bound variables by free
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   185
  ones. Return the body, along with the list of free variables.*)
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   186
fun c_variant_abs_multi (ct0, vars) =
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   187
      let val (cv,ct) = Thm.dest_abs NONE ct0
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   188
      in  c_variant_abs_multi (ct, cv::vars)  end
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   189
      handle CTERM _ => (ct0, rev vars);
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   190
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   191
val skolem_id_def_raw = @{thms skolem_id_def_raw}
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   192
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   193
(* Given the definition of a Skolem function, return a theorem to replace
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   194
   an existential formula by a use of that function.
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   195
   Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
37628
78334f400ae6 Sledgehammer can save some msecs by cheating
blanchet
parents: 37626
diff changeset
   196
fun skolem_theorem_of_def thy cheat rhs0 =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37349
diff changeset
   197
  let
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   198
    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of thy
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   199
    val rhs' = rhs |> Thm.dest_comb |> snd
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   200
    val (ch, frees) = c_variant_abs_multi (rhs', [])
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   201
    val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   202
    val T =
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   203
      case hilbert of
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   204
        Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   205
      | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert])
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   206
    val cex = Thm.cterm_of thy (HOLogic.exists_const T)
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   207
    val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
37629
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   208
    val conc =
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   209
      Drule.list_comb (rhs, frees)
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   210
      |> Drule.beta_conv cabs |> Thm.capply cTrueprop
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   211
    fun tacf [prem] =
37629
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   212
      if cheat then
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   213
        Skip_Proof.cheat_tac thy
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   214
      else
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   215
        rewrite_goals_tac skolem_id_def_raw
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   216
        THEN rtac ((prem |> rewrite_rule skolem_id_def_raw)
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   217
                   RS @{thm someI_ex}) 1
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   218
  in
37629
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   219
    Goal.prove_internal [ex_tm] conc tacf
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   220
    |> forall_intr_list frees
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   221
    |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   222
    |> Thm.varifyT_global
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   223
  end
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
   224
20863
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
   225
(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24854
diff changeset
   226
fun to_nnf th ctxt0 =
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   227
  let val th1 = th |> transform_elim |> zero_var_indexes
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32257
diff changeset
   228
      val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
37540
48273d1ea331 better eta-expansion in Sledgehammer's clausification;
blanchet
parents: 37518
diff changeset
   229
      val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
48273d1ea331 better eta-expansion in Sledgehammer's clausification;
blanchet
parents: 37518
diff changeset
   230
                    |> extensionalize
48273d1ea331 better eta-expansion in Sledgehammer's clausification;
blanchet
parents: 37518
diff changeset
   231
                    |> Meson.make_nnf ctxt
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24854
diff changeset
   232
  in  (th3, ctxt)  end;
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   233
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   234
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
37628
78334f400ae6 Sledgehammer can save some msecs by cheating
blanchet
parents: 37626
diff changeset
   235
fun skolemize_theorem thy cheat th =
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   236
  let
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   237
    val ctxt0 = Variable.global_thm_context th
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   238
    val (nnfth, ctxt) = to_nnf th ctxt0
37628
78334f400ae6 Sledgehammer can save some msecs by cheating
blanchet
parents: 37626
diff changeset
   239
    val sko_ths = map (skolem_theorem_of_def thy cheat)
78334f400ae6 Sledgehammer can save some msecs by cheating
blanchet
parents: 37626
diff changeset
   240
                      (assume_skolem_funs nnfth)
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   241
    val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   242
  in
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   243
    cnfs |> map introduce_combinators
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   244
         |> Variable.export ctxt ctxt0
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   245
         |> Meson.finish_cnf
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   246
         |> map Thm.close_derivation
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   247
  end
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   248
  handle THM _ => []
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   249
36228
df47dc6c0e03 got rid of somewhat pointless "pairname" function in Sledgehammer
blanchet
parents: 36106
diff changeset
   250
(* Convert Isabelle theorems into axiom clauses. *)
37618
fa57a87f92a0 get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents: 37617
diff changeset
   251
(* FIXME: is transfer necessary? *)
37628
78334f400ae6 Sledgehammer can save some msecs by cheating
blanchet
parents: 37626
diff changeset
   252
fun cnf_axiom thy cheat = skolemize_theorem thy cheat o Thm.transfer thy
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   253
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   254
22471
7c51f1a799f3 Removal of axiom names from the theorem cache
paulson
parents: 22360
diff changeset
   255
(**** Translate a set of theorems into CNF ****)
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   256
21290
33b6bb5d6ab8 Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents: 21254
diff changeset
   257
(*The combination of rev and tail recursion preserves the original order*)
37628
78334f400ae6 Sledgehammer can save some msecs by cheating
blanchet
parents: 37626
diff changeset
   258
fun cnf_rules_pairs thy cheat =
37416
d5ac8280497e no point in introducing combinators for inlined Skolem functions
blanchet
parents: 37410
diff changeset
   259
  let
37500
7587b6e63454 thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents: 37498
diff changeset
   260
    fun do_one _ [] = []
7587b6e63454 thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents: 37498
diff changeset
   261
      | do_one ((name, k), th) (cls :: clss) =
37620
537beae999d7 remove obsolete component of CNF clause tuple (and reorder it)
blanchet
parents: 37618
diff changeset
   262
        ((name, k), cls) :: do_one ((name, k + 1), th) clss
37500
7587b6e63454 thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents: 37498
diff changeset
   263
    fun do_all pairs [] = pairs
7587b6e63454 thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents: 37498
diff changeset
   264
      | do_all pairs ((name, th) :: ths) =
37416
d5ac8280497e no point in introducing combinators for inlined Skolem functions
blanchet
parents: 37410
diff changeset
   265
        let
37628
78334f400ae6 Sledgehammer can save some msecs by cheating
blanchet
parents: 37626
diff changeset
   266
          val new_pairs = do_one ((name, 0), th) (cnf_axiom thy cheat th)
37570
de5feddaa95c got rid of needless exception
blanchet
parents: 37567
diff changeset
   267
                          handle THM _ => []
37500
7587b6e63454 thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents: 37498
diff changeset
   268
        in do_all (new_pairs @ pairs) ths end
7587b6e63454 thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents: 37498
diff changeset
   269
  in do_all [] o rev end
19353
36b6b15ee670 added another function for CNF.
mengj
parents: 19232
diff changeset
   270
19196
62ee8c10d796 Added functions to retrieve local and global atpset rules.
mengj
parents: 19175
diff changeset
   271
21999
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   272
(*** Converting a subgoal into negated conjecture clauses. ***)
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   273
32262
73cd8f74cf2a Meson.first_order_resolve: avoid handle _;
wenzelm
parents: 32257
diff changeset
   274
fun neg_skolemize_tac ctxt =
37332
51d99ba6fc4d don't raise Option.Option if assumptions contain schematic variables
blanchet
parents: 37171
diff changeset
   275
  EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
36398
de8522a5cbae make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet
parents: 36394
diff changeset
   276
35869
cac366550624 start work on direct proof reconstruction for Sledgehammer
blanchet
parents: 35865
diff changeset
   277
val neg_clausify =
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   278
  single
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   279
  #> Meson.make_clauses_unsorted
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   280
  #> map introduce_combinators
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   281
  #> Meson.finish_cnf
21999
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   282
32257
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32231
diff changeset
   283
fun neg_conjecture_clauses ctxt st0 n =
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32231
diff changeset
   284
  let
37332
51d99ba6fc4d don't raise Option.Option if assumptions contain schematic variables
blanchet
parents: 37171
diff changeset
   285
    (* "Option" is thrown if the assumptions contain schematic variables. *)
51d99ba6fc4d don't raise Option.Option if assumptions contain schematic variables
blanchet
parents: 37171
diff changeset
   286
    val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0
51d99ba6fc4d don't raise Option.Option if assumptions contain schematic variables
blanchet
parents: 37171
diff changeset
   287
    val ({params, prems, ...}, _) =
51d99ba6fc4d don't raise Option.Option if assumptions contain schematic variables
blanchet
parents: 37171
diff changeset
   288
      Subgoal.focus (Variable.set_body false ctxt) n st
51d99ba6fc4d don't raise Option.Option if assumptions contain schematic variables
blanchet
parents: 37171
diff changeset
   289
  in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
21999
0cf192e489e2 improvements to proof reconstruction. Some files loaded in a different order
paulson
parents: 21900
diff changeset
   290
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   291
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   292
end;