src/HOL/Tools/Meson/meson_clausify.ML
author paulson <lp15@cam.ac.uk>
Mon, 30 Nov 2020 22:00:23 +0000
changeset 72797 402afc68f2f9
parent 70507 06a62b29085e
child 74051 bd575b1bd9bf
permissions -rw-r--r--
A bunch of suggestions from Pedro Sánchez Terraf
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39941
02fcd9cd1eac move Meson to Plain
blanchet
parents: 39940
diff changeset
     1
(*  Title:      HOL/Tools/Meson/meson_clausify.ML
38027
505657ddb047 standardize "Author" tags
blanchet
parents: 38016
diff changeset
     2
    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
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
39941
02fcd9cd1eac move Meson to Plain
blanchet
parents: 39940
diff changeset
     5
Transformation of HOL theorems 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
39890
a1695e2169d0 finished renaming file and module
blanchet
parents: 39889
diff changeset
     8
signature MESON_CLAUSIFY =
21505
13d4dba99337 prefer Proof.context over Context.generic;
wenzelm
parents: 21470
diff changeset
     9
sig
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
    10
  val new_skolem_var_prefix : string
42098
f978caf60bbe more robust handling of variables in new Skolemizer
blanchet
parents: 42072
diff changeset
    11
  val new_nonskolem_var_prefix : string
42099
447fa058ab22 avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents: 42098
diff changeset
    12
  val is_zapped_var_name : string -> bool
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45508
diff changeset
    13
  val is_quasi_lambda_free : term -> bool
60328
9c94e6a30d29 clarified context;
wenzelm
parents: 59632
diff changeset
    14
  val introduce_combinators_in_cterm : Proof.context -> cterm -> thm
55236
8d61b0aa7a0d proper context for printing;
wenzelm
parents: 54883
diff changeset
    15
  val introduce_combinators_in_theorem : Proof.context -> thm -> thm
39932
acde1b606b0e reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents: 39931
diff changeset
    16
  val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50705
diff changeset
    17
  val ss_only : thm list -> Proof.context -> Proof.context
39897
e26d5344e1b7 compute substitutions in new skolemizer
blanchet
parents: 39896
diff changeset
    18
  val cnf_axiom :
45508
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44241
diff changeset
    19
    Proof.context -> bool -> bool -> int -> thm
b216dc1b3630 started implementing lambda-lifting in Metis
blanchet
parents: 44241
diff changeset
    20
    -> (thm * term) option * thm list
21505
13d4dba99337 prefer Proof.context over Context.generic;
wenzelm
parents: 21470
diff changeset
    21
end;
19196
62ee8c10d796 Added functions to retrieve local and global atpset rules.
mengj
parents: 19175
diff changeset
    22
39890
a1695e2169d0 finished renaming file and module
blanchet
parents: 39889
diff changeset
    23
structure Meson_Clausify : MESON_CLAUSIFY =
15997
c71031d7988c consolidation and simplification
paulson
parents: 15956
diff changeset
    24
struct
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    25
42072
1492ee6b8085 avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
blanchet
parents: 41225
diff changeset
    26
(* the extra "Meson" helps prevent clashes (FIXME) *)
1492ee6b8085 avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
blanchet
parents: 41225
diff changeset
    27
val new_skolem_var_prefix = "MesonSK"
1492ee6b8085 avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
blanchet
parents: 41225
diff changeset
    28
val new_nonskolem_var_prefix = "MesonV"
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
    29
42099
447fa058ab22 avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents: 42098
diff changeset
    30
fun is_zapped_var_name s =
447fa058ab22 avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents: 42098
diff changeset
    31
  exists (fn prefix => String.isPrefix prefix s)
447fa058ab22 avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents: 42098
diff changeset
    32
         [new_skolem_var_prefix, new_nonskolem_var_prefix]
447fa058ab22 avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents: 42098
diff changeset
    33
15997
c71031d7988c consolidation and simplification
paulson
parents: 15956
diff changeset
    34
(**** Transformation of Elimination Rules into First-Order Formulas****)
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    35
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
    36
val cfalse = Thm.cterm_of \<^theory_context>\<open>HOL\<close> \<^term>\<open>False\<close>;
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
    37
val ctp_false = Thm.cterm_of \<^theory_context>\<open>HOL\<close> (HOLogic.mk_Trueprop \<^term>\<open>False\<close>);
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
    38
38001
a9b47b85ca24 reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents: 38000
diff changeset
    39
(* Converts an elim-rule into an equivalent theorem that does not have the
a9b47b85ca24 reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents: 38000
diff changeset
    40
   predicate variable. Leaves other theorems unchanged. We simply instantiate
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42747
diff changeset
    41
   the conclusion variable to False. (Cf. "transform_elim_prop" in
38652
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38632
diff changeset
    42
   "Sledgehammer_Util".) *)
38001
a9b47b85ca24 reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents: 38000
diff changeset
    43
fun transform_elim_theorem th =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
    44
  (case Thm.concl_of th of    (*conclusion variable*)
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
    45
    \<^const>\<open>Trueprop\<close> $ (Var (v as (_, \<^typ>\<open>bool\<close>))) =>
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60328
diff changeset
    46
      Thm.instantiate ([], [(v, cfalse)]) th
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
    47
  | Var (v as (_, \<^typ>\<open>prop\<close>)) =>
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60328
diff changeset
    48
      Thm.instantiate ([], [(v, ctp_false)]) th
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
    49
  | _ => th)
15997
c71031d7988c consolidation and simplification
paulson
parents: 15956
diff changeset
    50
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
    51
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
    52
(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
    53
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39721
diff changeset
    54
fun mk_old_skolem_term_wrapper t =
37436
2d76997730a6 found missing beta-eta-contraction
blanchet
parents: 37419
diff changeset
    55
  let val T = fastype_of t in
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
    56
    Const (\<^const_name>\<open>Meson.skolem\<close>, T --> T) $ t
37436
2d76997730a6 found missing beta-eta-contraction
blanchet
parents: 37419
diff changeset
    57
  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
    58
39931
97b8051033be renamed internal function
blanchet
parents: 39908
diff changeset
    59
fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t')
97b8051033be renamed internal function
blanchet
parents: 39908
diff changeset
    60
  | beta_eta_in_abs_body 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
    61
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
    62
(*Traverse a theorem, accumulating Skolem function definitions.*)
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39721
diff changeset
    63
fun old_skolem_defs th =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37349
diff changeset
    64
  let
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
    65
    fun dec_sko (Const (\<^const_name>\<open>Ex\<close>, _) $ (body as Abs (_, T, p))) rhss =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37349
diff changeset
    66
        (*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
    67
        let
44121
44adaa6db327 old term operations are legacy;
wenzelm
parents: 43964
diff changeset
    68
          val args = Misc_Legacy.term_frees body
37500
7587b6e63454 thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents: 37498
diff changeset
    69
          (* 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
    70
          val rhs =
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44121
diff changeset
    71
            fold_rev (absfree o dest_Free) args
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44121
diff changeset
    72
              (HOLogic.choice_const T $ beta_eta_in_abs_body body)
39886
8a9f0c97d550 first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents: 39721
diff changeset
    73
            |> mk_old_skolem_term_wrapper
37518
efb0923cc098 use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code
blanchet
parents: 37512
diff changeset
    74
          val comb = list_comb (rhs, args)
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    75
        in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
    76
      | dec_sko (Const (\<^const_name>\<open>All\<close>,_) $ Abs (a, T, p)) rhss =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37349
diff changeset
    77
        (*Universal quant: insert a free variable into body and continue*)
44121
44adaa6db327 old term operations are legacy;
wenzelm
parents: 43964
diff changeset
    78
        let val fname = singleton (Name.variant_list (Misc_Legacy.add_term_names (p, []))) a
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    79
        in dec_sko (subst_bound (Free(fname,T), p)) rhss end
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
    80
      | dec_sko (\<^const>\<open>conj\<close> $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
    81
      | dec_sko (\<^const>\<open>disj\<close> $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
    82
      | dec_sko (\<^const>\<open>Trueprop\<close> $ p) rhss = dec_sko p rhss
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
    83
      | dec_sko _ rhss = rhss
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
    84
  in  dec_sko (Thm.prop_of th) []  end;
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
    85
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
    86
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
    87
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20373
diff changeset
    88
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
    89
fun is_quasi_lambda_free (Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ _) = true
37416
d5ac8280497e no point in introducing combinators for inlined Skolem functions
blanchet
parents: 37410
diff changeset
    90
  | is_quasi_lambda_free (t1 $ t2) =
d5ac8280497e no point in introducing combinators for inlined Skolem functions
blanchet
parents: 37410
diff changeset
    91
    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
    92
  | is_quasi_lambda_free (Abs _) = false
d5ac8280497e no point in introducing combinators for inlined Skolem functions
blanchet
parents: 37410
diff changeset
    93
  | is_quasi_lambda_free _ = true
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
    94
60328
9c94e6a30d29 clarified context;
wenzelm
parents: 59632
diff changeset
    95
fun abstract ctxt ct =
28544
26743a1591f5 improved performance of skolem cache, due to parallel map;
wenzelm
parents: 28262
diff changeset
    96
  let
70157
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
    97
      val Abs (_, _, body) = Thm.term_of ct
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
    98
      val (x, cbody) = Thm.dest_abs NONE ct
70159
57503fe1b0ff tuned signature;
wenzelm
parents: 70157
diff changeset
    99
      val (A, cbodyT) = Thm.dest_funT (Thm.ctyp_of_cterm ct)
70157
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   100
      fun makeK () = Thm.instantiate' [SOME A, SOME cbodyT] [SOME cbody] @{thm abs_K}
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   101
  in
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   102
      case body of
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   103
          Const _ => makeK()
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   104
        | Free _ => makeK()
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   105
        | Var _ => makeK()  (*though Var isn't expected*)
70157
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   106
        | Bound 0 => Thm.instantiate' [SOME A] [] @{thm abs_I} (*identity: I*)
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   107
        | rator$rand =>
42083
e1209fc7ecdc added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents: 42072
diff changeset
   108
            if Term.is_dependent rator then (*C or S*)
e1209fc7ecdc added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents: 42072
diff changeset
   109
               if Term.is_dependent rand then (*S*)
70157
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   110
                 let val crator = Thm.lambda x (Thm.dest_fun cbody)
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   111
                     val crand = Thm.lambda x (Thm.dest_arg cbody)
70159
57503fe1b0ff tuned signature;
wenzelm
parents: 70157
diff changeset
   112
                     val (C, B) = Thm.dest_funT (Thm.dest_ctyp1 (Thm.ctyp_of_cterm crator))
70157
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   113
                     val abs_S' = @{thm abs_S}
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   114
                       |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand]
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   115
                     val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_S')
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   116
                 in
60328
9c94e6a30d29 clarified context;
wenzelm
parents: 59632
diff changeset
   117
                   Thm.transitive abs_S' (Conv.binop_conv (abstract ctxt) rhs)
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   118
                 end
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   119
               else (*C*)
70157
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   120
                 let val crator = Thm.lambda x (Thm.dest_fun cbody)
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   121
                     val crand = Thm.dest_arg cbody
70159
57503fe1b0ff tuned signature;
wenzelm
parents: 70157
diff changeset
   122
                     val (C, B) = Thm.dest_funT (Thm.dest_ctyp1 (Thm.ctyp_of_cterm crator))
70157
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   123
                     val abs_C' = @{thm abs_C}
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   124
                       |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand]
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   125
                     val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_C')
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   126
                 in
60328
9c94e6a30d29 clarified context;
wenzelm
parents: 59632
diff changeset
   127
                   Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv (abstract ctxt)) rhs)
27179
8f29fed3dc9a ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents: 27174
diff changeset
   128
                 end
42083
e1209fc7ecdc added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents: 42072
diff changeset
   129
            else if Term.is_dependent rand then (*B or eta*)
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36603
diff changeset
   130
               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
   131
               else (*B*)
70157
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   132
                 let val crator = Thm.dest_fun cbody
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   133
                     val crand = Thm.lambda x (Thm.dest_arg cbody)
70159
57503fe1b0ff tuned signature;
wenzelm
parents: 70157
diff changeset
   134
                     val (C, B) = Thm.dest_funT (Thm.ctyp_of_cterm crator)
70157
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   135
                     val abs_B' = @{thm abs_B}
62b19f19350a meson: more cterm operations;
wenzelm
parents: 69593
diff changeset
   136
                      |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand]
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   137
                     val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_B')
60328
9c94e6a30d29 clarified context;
wenzelm
parents: 59632
diff changeset
   138
                 in Thm.transitive abs_B' (Conv.arg_conv (abstract ctxt) rhs) end
9c94e6a30d29 clarified context;
wenzelm
parents: 59632
diff changeset
   139
            else makeK ()
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   140
        | _ => raise Fail "abstract: Bad term"
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   141
  end;
20863
4ee61dbf192d improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents: 20789
diff changeset
   142
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   143
(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
60328
9c94e6a30d29 clarified context;
wenzelm
parents: 59632
diff changeset
   144
fun introduce_combinators_in_cterm ctxt ct =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   145
  if is_quasi_lambda_free (Thm.term_of ct) then
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   146
    Thm.reflexive ct
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   147
  else case Thm.term_of ct of
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   148
    Abs _ =>
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   149
    let
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   150
      val (cv, cta) = Thm.dest_abs NONE ct
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   151
      val (v, _) = dest_Free (Thm.term_of cv)
60328
9c94e6a30d29 clarified context;
wenzelm
parents: 59632
diff changeset
   152
      val u_th = introduce_combinators_in_cterm ctxt cta
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   153
      val cu = Thm.rhs_of u_th
60328
9c94e6a30d29 clarified context;
wenzelm
parents: 59632
diff changeset
   154
      val comb_eq = abstract ctxt (Thm.lambda cv cu)
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   155
    in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   156
  | _ $ _ =>
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   157
    let val (ct1, ct2) = Thm.dest_comb ct in
60328
9c94e6a30d29 clarified context;
wenzelm
parents: 59632
diff changeset
   158
        Thm.combination (introduce_combinators_in_cterm ctxt ct1)
9c94e6a30d29 clarified context;
wenzelm
parents: 59632
diff changeset
   159
                        (introduce_combinators_in_cterm ctxt ct2)
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   160
    end
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   161
55236
8d61b0aa7a0d proper context for printing;
wenzelm
parents: 54883
diff changeset
   162
fun introduce_combinators_in_theorem ctxt th =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   163
  if is_quasi_lambda_free (Thm.prop_of th) then
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   164
    th
24827
646bdc51eb7d combinator translation
paulson
parents: 24821
diff changeset
   165
  else
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   166
    let
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   167
      val th = Drule.eta_contraction_rule th
60328
9c94e6a30d29 clarified context;
wenzelm
parents: 59632
diff changeset
   168
      val eqth = introduce_combinators_in_cterm ctxt (Thm.cprop_of th)
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   169
    in Thm.equal_elim eqth th end
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   170
    handle THM (msg, _, _) =>
61268
abe08fb15a12 moved remaining display.ML to more_thm.ML;
wenzelm
parents: 60801
diff changeset
   171
           (warning ("Error in the combinator translation of " ^ Thm.string_of_thm ctxt th ^
55523
9429e7b5b827 removed final periods in messages for proof methods
blanchet
parents: 55239
diff changeset
   172
              "\nException message: " ^ msg);
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45508
diff changeset
   173
            (* A type variable of sort "{}" will make "abstraction" fail. *)
37349
3d7058e24b7a cosmetics
blanchet
parents: 37348
diff changeset
   174
            TrueI)
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   175
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   176
(*cterms are used throughout for efficiency*)
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67149
diff changeset
   177
val cTrueprop = Thm.cterm_of \<^theory_context>\<open>HOL\<close> HOLogic.Trueprop;
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   178
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   179
(*Given an abstraction over n variables, replace the bound variables by free
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   180
  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
   181
fun c_variant_abs_multi (ct0, vars) =
16009
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   182
      let val (cv,ct) = Thm.dest_abs NONE ct0
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   183
      in  c_variant_abs_multi (ct, cv::vars)  end
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   184
      handle CTERM _ => (ct0, rev vars);
a6d480e6c5f0 Skolemization of simprules and classical rules
paulson
parents: 15997
diff changeset
   185
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   186
(* 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
   187
   an existential formula by a use of that function.
18141
89e2e8bed08f Skolemization by inference, but not quite finished
paulson
parents: 18009
diff changeset
   188
   Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
57466
feb414dadfd1 use context instead of theory
blanchet
parents: 56811
diff changeset
   189
fun old_skolem_theorem_of_def ctxt rhs0 =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37349
diff changeset
   190
  let
59632
5980e75a204e clarified context;
wenzelm
parents: 59621
diff changeset
   191
    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of ctxt
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   192
    val rhs' = rhs |> Thm.dest_comb |> snd
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   193
    val (ch, frees) = c_variant_abs_multi (rhs', [])
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   194
    val (hilbert, cabs) = ch |> Thm.dest_comb |>> Thm.term_of
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   195
    val T =
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   196
      case hilbert of
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   197
        Const (_, Type (\<^type_name>\<open>fun\<close>, [_, T])) => T
57466
feb414dadfd1 use context instead of theory
blanchet
parents: 56811
diff changeset
   198
      | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"", [hilbert])
59632
5980e75a204e clarified context;
wenzelm
parents: 59621
diff changeset
   199
    val cex = Thm.cterm_of ctxt (HOLogic.exists_const T)
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 46071
diff changeset
   200
    val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
37629
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   201
    val conc =
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   202
      Drule.list_comb (rhs, frees)
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 46071
diff changeset
   203
      |> Drule.beta_conv cabs |> Thm.apply cTrueprop
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   204
    fun tacf [prem] =
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52031
diff changeset
   205
      rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
59632
5980e75a204e clarified context;
wenzelm
parents: 59621
diff changeset
   206
      THEN resolve_tac ctxt
5980e75a204e clarified context;
wenzelm
parents: 59621
diff changeset
   207
        [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
5980e75a204e clarified context;
wenzelm
parents: 59621
diff changeset
   208
          RS Global_Theory.get_thm (Proof_Context.theory_of ctxt) "Hilbert_Choice.someI_ex"] 1
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   209
  in
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   210
    Goal.prove_internal ctxt [ex_tm] conc tacf
37629
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   211
    |> forall_intr_list frees
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   212
    |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
a4f129820562 more elegant cheating
blanchet
parents: 37628
diff changeset
   213
    |> Thm.varifyT_global
37617
f73cd4069f69 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents: 37616
diff changeset
   214
  end
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 24669
diff changeset
   215
42335
cb8aa792d138 experiment with definitional CNF
blanchet
parents: 42333
diff changeset
   216
fun to_definitional_cnf_with_quantifiers ctxt th =
39036
dff91b90d74c use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents: 38864
diff changeset
   217
  let
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   218
    val eqth = CNF.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (Thm.prop_of th))
39036
dff91b90d74c use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents: 38864
diff changeset
   219
    val eqth = eqth RS @{thm eq_reflection}
dff91b90d74c use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents: 38864
diff changeset
   220
    val eqth = eqth RS @{thm TruepropI}
dff91b90d74c use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents: 38864
diff changeset
   221
  in Thm.equal_elim eqth th end
dff91b90d74c use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents: 38864
diff changeset
   222
39932
acde1b606b0e reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents: 39931
diff changeset
   223
fun zapped_var_name ((ax_no, cluster_no), skolem) index_no s =
39896
13b3a2ba9ea7 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents: 39894
diff changeset
   224
  (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
39932
acde1b606b0e reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents: 39931
diff changeset
   225
  "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^
56811
b66639331db5 optional case enforcement
haftmann
parents: 56245
diff changeset
   226
  string_of_int index_no ^ "_" ^ Name.desymbolize (SOME false) s
39896
13b3a2ba9ea7 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents: 39894
diff changeset
   227
39899
608b108ec979 compute quantifier dependency graph in new skolemizer
blanchet
parents: 39897
diff changeset
   228
fun cluster_of_zapped_var_name s =
39932
acde1b606b0e reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents: 39931
diff changeset
   229
  let val get_int = the o Int.fromString o nth (space_explode "_" s) in
acde1b606b0e reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents: 39931
diff changeset
   230
    ((get_int 1, (get_int 2, get_int 3)),
acde1b606b0e reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents: 39931
diff changeset
   231
     String.isPrefix new_skolem_var_prefix s)
acde1b606b0e reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents: 39931
diff changeset
   232
  end
39897
e26d5344e1b7 compute substitutions in new skolemizer
blanchet
parents: 39896
diff changeset
   233
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   234
fun rename_bound_vars_to_be_zapped ax_no =
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   235
  let
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   236
    fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t =
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   237
      case t of
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   238
        (t1 as Const (s, _)) $ Abs (s', T, t') =>
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   239
        if s = \<^const_name>\<open>Pure.all\<close> orelse s = \<^const_name>\<open>All\<close> orelse
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   240
           s = \<^const_name>\<open>Ex\<close> then
39932
acde1b606b0e reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents: 39931
diff changeset
   241
          let
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   242
            val skolem = (pos = (s = \<^const_name>\<open>Ex\<close>))
39932
acde1b606b0e reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents: 39931
diff changeset
   243
            val (cluster, index_no) =
acde1b606b0e reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents: 39931
diff changeset
   244
              if skolem = cluster_skolem then (cluster, index_no)
acde1b606b0e reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents: 39931
diff changeset
   245
              else ((cluster_no ||> cluster_skolem ? Integer.add 1, skolem), 0)
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   246
            val s' = zapped_var_name cluster index_no s'
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   247
          in t1 $ Abs (s', T, aux cluster (index_no + 1) pos t') end
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   248
        else
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   249
          t
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   250
      | (t1 as Const (s, _)) $ t2 $ t3 =>
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   251
        if s = \<^const_name>\<open>Pure.imp\<close> orelse s = \<^const_name>\<open>HOL.implies\<close> then
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   252
          t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   253
        else if s = \<^const_name>\<open>HOL.conj\<close> orelse
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   254
                s = \<^const_name>\<open>HOL.disj\<close> then
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   255
          t1 $ aux cluster index_no pos t2 $ aux cluster index_no pos t3
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   256
        else
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   257
          t
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   258
      | (t1 as Const (s, _)) $ t2 =>
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   259
        if s = \<^const_name>\<open>Trueprop\<close> then
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   260
          t1 $ aux cluster index_no pos t2
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   261
        else if s = \<^const_name>\<open>Not\<close> then
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   262
          t1 $ aux cluster index_no (not pos) t2
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   263
        else
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   264
          t
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   265
      | _ => t
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   266
  in aux ((ax_no, 0), true) 0 true end
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   267
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   268
fun zap pos ct =
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   269
  ct
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   270
  |> (case Thm.term_of ct of
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   271
        Const (s, _) $ Abs (s', _, _) =>
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   272
        if s = \<^const_name>\<open>Pure.all\<close> orelse s = \<^const_name>\<open>All\<close> orelse
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   273
           s = \<^const_name>\<open>Ex\<close> then
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   274
          Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos
39906
blanchet
parents: 39905
diff changeset
   275
        else
blanchet
parents: 39905
diff changeset
   276
          Conv.all_conv
blanchet
parents: 39905
diff changeset
   277
      | Const (s, _) $ _ $ _ =>
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   278
        if s = \<^const_name>\<open>Pure.imp\<close> orelse s = \<^const_name>\<open>implies\<close> then
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   279
          Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos)
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   280
        else if s = \<^const_name>\<open>conj\<close> orelse s = \<^const_name>\<open>disj\<close> then
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   281
          Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos)
39906
blanchet
parents: 39905
diff changeset
   282
        else
blanchet
parents: 39905
diff changeset
   283
          Conv.all_conv
blanchet
parents: 39905
diff changeset
   284
      | Const (s, _) $ _ =>
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   285
        if s = \<^const_name>\<open>Trueprop\<close> then Conv.arg_conv (zap pos)
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   286
        else if s = \<^const_name>\<open>Not\<close> then Conv.arg_conv (zap (not pos))
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   287
        else Conv.all_conv
39906
blanchet
parents: 39905
diff changeset
   288
      | _ => Conv.all_conv)
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   289
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50705
diff changeset
   290
fun ss_only ths ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths
39901
75d792edf634 make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents: 39900
diff changeset
   291
40261
7a02144874f3 more work on new Skolemizer without Hilbert_Choice
blanchet
parents: 40260
diff changeset
   292
val cheat_choice =
67149
e61557884799 prefer control symbol antiquotations;
wenzelm
parents: 67091
diff changeset
   293
  \<^prop>\<open>\<forall>x. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)\<close>
39901
75d792edf634 make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents: 39900
diff changeset
   294
  |> Logic.varify_global
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67149
diff changeset
   295
  |> Skip_Proof.make_thm \<^theory>
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   296
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   297
(* Converts an Isabelle theorem into NNF. *)
50705
0e943b33d907 use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
blanchet
parents: 47954
diff changeset
   298
fun nnf_axiom choice_ths new_skolem ax_no th ctxt =
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   299
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42351
diff changeset
   300
    val thy = Proof_Context.theory_of ctxt
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   301
    val th =
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   302
      th |> transform_elim_theorem
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   303
         |> zero_var_indexes
50705
0e943b33d907 use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
blanchet
parents: 47954
diff changeset
   304
         |> new_skolem ? forall_intr_vars
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   305
    val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52031
diff changeset
   306
    val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
70507
06a62b29085e do not open ML structures;
wenzelm
parents: 70494
diff changeset
   307
                |> Meson.cong_extensionalize_thm ctxt
06a62b29085e do not open ML structures;
wenzelm
parents: 70494
diff changeset
   308
                |> Meson.abs_extensionalize_thm ctxt
06a62b29085e do not open ML structures;
wenzelm
parents: 70494
diff changeset
   309
                |> Meson.make_nnf ctxt
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   310
  in
50705
0e943b33d907 use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
blanchet
parents: 47954
diff changeset
   311
    if new_skolem then
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   312
      let
39901
75d792edf634 make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents: 39900
diff changeset
   313
        fun skolemize choice_ths =
70507
06a62b29085e do not open ML structures;
wenzelm
parents: 70494
diff changeset
   314
          Meson.skolemize_with_choice_theorems ctxt choice_ths
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50705
diff changeset
   315
          #> simplify (ss_only @{thms all_simps[symmetric]} ctxt)
42347
53e444ecb525 properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
blanchet
parents: 42336
diff changeset
   316
        val no_choice = null choice_ths
39901
75d792edf634 make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents: 39900
diff changeset
   317
        val pull_out =
42347
53e444ecb525 properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
blanchet
parents: 42336
diff changeset
   318
          if no_choice then
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50705
diff changeset
   319
            simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]} ctxt)
42347
53e444ecb525 properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
blanchet
parents: 42336
diff changeset
   320
          else
53e444ecb525 properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
blanchet
parents: 42336
diff changeset
   321
            skolemize choice_ths
53e444ecb525 properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
blanchet
parents: 42336
diff changeset
   322
        val discharger_th = th |> pull_out
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   323
        val discharger_th =
70507
06a62b29085e do not open ML structures;
wenzelm
parents: 70494
diff changeset
   324
          discharger_th |> Meson.has_too_many_clauses ctxt (Thm.concl_of discharger_th)
42347
53e444ecb525 properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
blanchet
parents: 42336
diff changeset
   325
                           ? (to_definitional_cnf_with_quantifiers ctxt
53e444ecb525 properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
blanchet
parents: 42336
diff changeset
   326
                              #> pull_out)
42099
447fa058ab22 avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents: 42098
diff changeset
   327
        val zapped_th =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   328
          discharger_th |> Thm.prop_of |> rename_bound_vars_to_be_zapped ax_no
40263
51ed7a5ad4c5 restructure Skolemization code slightly
blanchet
parents: 40262
diff changeset
   329
          |> (if no_choice then
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   330
                Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> Thm.cprop_of
40263
51ed7a5ad4c5 restructure Skolemization code slightly
blanchet
parents: 40262
diff changeset
   331
              else
59632
5980e75a204e clarified context;
wenzelm
parents: 59621
diff changeset
   332
                Thm.cterm_of ctxt)
42099
447fa058ab22 avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents: 42098
diff changeset
   333
          |> zap true
447fa058ab22 avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents: 42098
diff changeset
   334
        val fixes =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   335
          [] |> Term.add_free_names (Thm.prop_of zapped_th)
42335
cb8aa792d138 experiment with definitional CNF
blanchet
parents: 42333
diff changeset
   336
             |> filter is_zapped_var_name
42269
554e90f9db0c tuned comment
blanchet
parents: 42122
diff changeset
   337
        val ctxt' = ctxt |> Variable.add_fixes_direct fixes
42099
447fa058ab22 avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents: 42098
diff changeset
   338
        val fully_skolemized_t =
42333
23bb0784b5d0 try to repair out-of-sync situations in Metis
blanchet
parents: 42269
diff changeset
   339
          zapped_th |> singleton (Variable.export ctxt' ctxt)
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   340
                    |> Thm.cprop_of |> Thm.dest_equals |> snd |> Thm.term_of
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   341
      in
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   342
        if exists_subterm (fn Var ((s, _), _) =>
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   343
                              String.isPrefix new_skolem_var_prefix s
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   344
                            | _ => false) fully_skolemized_t then
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   345
          let
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   346
            val (fully_skolemized_ct, ctxt) =
70326
wenzelm
parents: 70320
diff changeset
   347
              yield_singleton (Variable.import_terms true) fully_skolemized_t ctxt
wenzelm
parents: 70320
diff changeset
   348
              |>> Thm.cterm_of ctxt
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   349
          in
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   350
            (SOME (discharger_th, fully_skolemized_ct),
40262
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 40261
diff changeset
   351
             (Thm.assume fully_skolemized_ct, ctxt))
40260
73ecbe2d432b fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents: 39962
diff changeset
   352
          end
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   353
       else
40262
8403085384eb ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents: 40261
diff changeset
   354
         (NONE, (th, ctxt))
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   355
      end
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   356
    else
70507
06a62b29085e do not open ML structures;
wenzelm
parents: 70494
diff changeset
   357
      (NONE, (th |> Meson.has_too_many_clauses ctxt (Thm.concl_of th)
42347
53e444ecb525 properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
blanchet
parents: 42336
diff changeset
   358
                    ? to_definitional_cnf_with_quantifiers ctxt, ctxt))
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   359
  end
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   360
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   361
(* Convert a theorem to CNF, with additional premises due to skolemization. *)
50705
0e943b33d907 use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
blanchet
parents: 47954
diff changeset
   362
fun cnf_axiom ctxt0 new_skolem combinators ax_no th =
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   363
  let
70507
06a62b29085e do not open ML structures;
wenzelm
parents: 70494
diff changeset
   364
    val choice_ths = Meson.choice_theorems (Proof_Context.theory_of ctxt0)
70320
59258a3192bf misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents: 70159
diff changeset
   365
    val (opt, (nnf_th, ctxt1)) =
50705
0e943b33d907 use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
blanchet
parents: 47954
diff changeset
   366
      nnf_axiom choice_ths new_skolem ax_no th ctxt0
39894
35ae5cf8c96a encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents: 39891
diff changeset
   367
    fun clausify th =
70507
06a62b29085e do not open ML structures;
wenzelm
parents: 70494
diff changeset
   368
      Meson.make_cnf
59165
115965966e15 proper context;
wenzelm
parents: 59058
diff changeset
   369
       (if new_skolem orelse null choice_ths then []
70320
59258a3192bf misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents: 70159
diff changeset
   370
        else map (old_skolem_theorem_of_def ctxt1) (old_skolem_defs th))
59258a3192bf misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents: 70159
diff changeset
   371
       th ctxt1
59258a3192bf misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents: 70159
diff changeset
   372
    val (cnf_ths, ctxt2) = clausify nnf_th
39894
35ae5cf8c96a encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents: 39891
diff changeset
   373
    fun intr_imp ct th =
70320
59258a3192bf misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents: 70159
diff changeset
   374
      Thm.instantiate ([], [((("i", 0), \<^typ>\<open>nat\<close>), Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no))])
39962
d42ddd7407ca qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
blanchet
parents: 39950
diff changeset
   375
                      (zero_var_indexes @{thm skolem_COMBK_D})
39894
35ae5cf8c96a encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents: 39891
diff changeset
   376
      RS Thm.implies_intr ct th
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   377
  in
70320
59258a3192bf misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents: 70159
diff changeset
   378
    (opt |> Option.map (I #>> singleton (Variable.export ctxt2 ctxt0)
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59498
diff changeset
   379
                        ##> (Thm.term_of #> HOLogic.dest_Trueprop
70320
59258a3192bf misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents: 70159
diff changeset
   380
                             #> singleton (Variable.export_terms ctxt2 ctxt0))),
59258a3192bf misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents: 70159
diff changeset
   381
     cnf_ths |> map (combinators ? introduce_combinators_in_theorem ctxt2
39894
35ae5cf8c96a encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents: 39891
diff changeset
   382
                     #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
70320
59258a3192bf misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents: 70159
diff changeset
   383
             |> Variable.export ctxt2 ctxt0
70507
06a62b29085e do not open ML structures;
wenzelm
parents: 70494
diff changeset
   384
             |> Meson.finish_cnf
70494
41108e3e9ca5 formal position for PThm nodes;
wenzelm
parents: 70326
diff changeset
   385
             |> map (Thm.close_derivation \<^here>))
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37620
diff changeset
   386
  end
39887
74939e2afb95 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents: 39886
diff changeset
   387
  handle THM _ => (NONE, [])
27184
b1483d423512 export just one setup function;
wenzelm
parents: 27179
diff changeset
   388
20461
d689ad772b2c skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents: 20457
diff changeset
   389
end;