src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63167 0909deb8059b
child 67399 eab6ce8368fa
permissions -rw-r--r--
tuned proofs;
sultana@55596
     1
(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction.thy
sultana@55596
     2
    Author:     Nik Sultana, Cambridge University Computer Laboratory
sultana@55596
     3
sultana@55596
     4
Proof reconstruction for Leo-II.
sultana@55596
     5
sultana@55597
     6
USAGE:
sultana@55597
     7
* Simple call the "reconstruct_leo2" function.
sultana@55597
     8
* For more advanced use, you could use the component functions used in
sultana@55597
     9
  "reconstruct_leo2" -- see TPTP_Proof_Reconstruction_Test.thy for
sultana@55597
    10
  examples of this.
sultana@55597
    11
sultana@55597
    12
This file contains definitions describing how to interpret LEO-II's
sultana@55597
    13
calculus in Isabelle/HOL, as well as more general proof-handling
sultana@55597
    14
functions. The definitions in this file serve to build an intermediate
sultana@55597
    15
proof script which is then evaluated into a tactic -- both these steps
sultana@55597
    16
are independent of LEO-II, and are defined in the TPTP_Reconstruct SML
sultana@55597
    17
module.
sultana@55597
    18
sultana@55597
    19
CONFIG:
sultana@55597
    20
The following attributes are mainly useful for debugging:
sultana@55597
    21
  tptp_unexceptional_reconstruction |
sultana@55597
    22
  unexceptional_reconstruction      |-- when these are true, a low-level exception
sultana@55597
    23
                                        is allowed to float to the top (instead of
sultana@55597
    24
                                        triggering a higher-level exception, or
sultana@55597
    25
                                        simply indicating that the reconstruction failed).
sultana@55597
    26
  tptp_max_term_size                --- fail of a term exceeds this size. "0" is taken
sultana@55597
    27
                                        to mean infinity.
sultana@55597
    28
  tptp_informative_failure          |
sultana@55597
    29
  informative_failure               |-- produce more output during reconstruction.
sultana@55597
    30
  tptp_trace_reconstruction         |
sultana@55597
    31
sultana@55597
    32
There are also two attributes, independent of the code here, that
sultana@55597
    33
influence the success of reconstruction: blast_depth_limit and
sultana@55597
    34
unify_search_bound. These are documented in their respective modules,
sultana@55597
    35
but in summary, if unify_search_bound is increased then we can
sultana@55597
    36
handle larger terms (at the cost of performance), since the unification
sultana@55597
    37
engine takes longer to give up the search; blast_depth_limit is
sultana@55597
    38
a limit on proof search performed by Blast. Blast is used for
sultana@55597
    39
the limited proof search that needs to be done to interpret
sultana@55597
    40
instances of LEO-II's inference rules.
sultana@55597
    41
sultana@55596
    42
TODO:
sultana@55596
    43
  use RemoveRedundantQuantifications instead of the ad hoc use of
sultana@55596
    44
   remove_redundant_quantification_in_lit and remove_redundant_quantification
sultana@55596
    45
*)
sultana@55596
    46
sultana@55596
    47
theory TPTP_Proof_Reconstruction
sultana@55596
    48
imports TPTP_Parser TPTP_Interpret
sultana@55596
    49
(* keywords "import_leo2_proof" :: thy_decl *) (*FIXME currently unused*)
sultana@55596
    50
begin
sultana@55596
    51
sultana@55596
    52
sultana@55596
    53
section "Setup"
sultana@55596
    54
wenzelm@63167
    55
ML \<open>
sultana@55596
    56
  val tptp_unexceptional_reconstruction = Attrib.setup_config_bool @{binding tptp_unexceptional_reconstruction} (K false)
sultana@55596
    57
  fun unexceptional_reconstruction ctxt = Config.get ctxt tptp_unexceptional_reconstruction
sultana@55596
    58
  val tptp_informative_failure = Attrib.setup_config_bool @{binding tptp_informative_failure} (K false)
sultana@55596
    59
  fun informative_failure ctxt = Config.get ctxt tptp_informative_failure
sultana@55596
    60
  val tptp_trace_reconstruction = Attrib.setup_config_bool @{binding tptp_trace_reconstruction} (K false)
sultana@55596
    61
  val tptp_max_term_size = Attrib.setup_config_int @{binding tptp_max_term_size} (K 0) (*0=infinity*)
sultana@55596
    62
sultana@55596
    63
  fun exceeds_tptp_max_term_size ctxt size =
sultana@55596
    64
    let
sultana@55596
    65
      val max = Config.get ctxt tptp_max_term_size
sultana@55596
    66
    in
sultana@55596
    67
      if max = 0 then false
sultana@55596
    68
      else size > max
sultana@55596
    69
    end
wenzelm@63167
    70
\<close>
sultana@55596
    71
sultana@55596
    72
(*FIXME move to TPTP_Proof_Reconstruction_Test_Units*)
sultana@55596
    73
declare [[
sultana@55596
    74
  tptp_unexceptional_reconstruction = false, (*NOTE should be "false" while testing*)
sultana@55596
    75
  tptp_informative_failure = true
sultana@55596
    76
]]
sultana@55596
    77
sultana@55596
    78
ML_file "TPTP_Parser/tptp_reconstruct_library.ML"
sultana@55596
    79
ML "open TPTP_Reconstruct_Library"
sultana@55596
    80
ML_file "TPTP_Parser/tptp_reconstruct.ML"
sultana@55596
    81
sultana@55596
    82
(*FIXME fudge*)
sultana@55596
    83
declare [[
sultana@55596
    84
  blast_depth_limit = 10,
sultana@55596
    85
  unify_search_bound = 5
sultana@55596
    86
]]
sultana@55596
    87
sultana@55596
    88
sultana@55596
    89
section "Proof reconstruction"
wenzelm@63167
    90
text \<open>There are two parts to proof reconstruction:
sultana@55596
    91
\begin{itemize}
sultana@55596
    92
  \item interpreting the inferences
sultana@55596
    93
  \item building the skeleton, which indicates how to compose
sultana@55596
    94
    individual inferences into subproofs, and then compose the
sultana@55596
    95
    subproofs to give the proof).
sultana@55596
    96
\end{itemize}
sultana@55596
    97
sultana@55596
    98
One step detects unsound inferences, and the other step detects
sultana@55596
    99
unsound composition of inferences.  The two parts can be weakly
sultana@55596
   100
coupled. They rely on a "proof index" which maps nodes to the
sultana@55596
   101
inference information. This information consists of the (usually
sultana@55596
   102
prover-specific) name of the inference step, and the Isabelle
sultana@55596
   103
formalisation of the inference as a term. The inference interpretation
sultana@55596
   104
then maps these terms into meta-theorems, and the skeleton is used to
sultana@55596
   105
compose the inference-level steps into a proof.
sultana@55596
   106
sultana@55596
   107
Leo2 operates on conjunctions of clauses. Each Leo2 inference has the
sultana@55596
   108
following form, where Cx are clauses:
sultana@55596
   109
sultana@55596
   110
           C1 && ... && Cn
sultana@55596
   111
          -----------------
sultana@55596
   112
          C'1 && ... && C'n
sultana@55596
   113
sultana@55596
   114
Clauses consist of disjunctions of literals (shown as Px below), and might
sultana@55596
   115
have a prefix of !-bound variables, as shown below.
sultana@55596
   116
sultana@55596
   117
  ! X... { P1 || ... || Pn}
sultana@55596
   118
sultana@55596
   119
Literals are usually assigned a polarity, but this isn't always the
sultana@55596
   120
case; you can come across inferences looking like this (where A is an
sultana@55596
   121
object-level formula):
sultana@55596
   122
sultana@55596
   123
             F
sultana@55596
   124
          --------
sultana@55596
   125
          F = true
sultana@55596
   126
sultana@55596
   127
The symbol "||" represents literal-level disjunction and "&&" is
sultana@55596
   128
clause-level conjunction. Rules will typically lift formula-level
sultana@55596
   129
conjunctions; for instance the following rule lifts object-level
sultana@55596
   130
disjunction:
sultana@55596
   131
sultana@55596
   132
          {    (A | B) = true    || ... } && ...
sultana@55596
   133
          --------------------------------------
sultana@55596
   134
          { A = true || B = true || ... } && ...
sultana@55596
   135
sultana@55596
   136
sultana@55596
   137
Using this setup, efficiency might be gained by only interpreting
sultana@55596
   138
inferences once, merging identical inference steps, and merging
sultana@55596
   139
identical subproofs into single inferences thus avoiding some effort.
sultana@55596
   140
We can also attempt to minimising proof search when interpreting
sultana@55596
   141
inferences.
sultana@55596
   142
sultana@55596
   143
It is hoped that this setup can target other provers by modifying the
sultana@55596
   144
clause representation to fit them, and adapting the inference
sultana@55596
   145
interpretation to handle the rules used by the prover. It should also
sultana@55596
   146
facilitate composing together proofs found by different provers.
wenzelm@63167
   147
\<close>
sultana@55596
   148
sultana@55596
   149
sultana@55596
   150
subsection "Instantiation"
sultana@55596
   151
sultana@55596
   152
lemma polar_allE [rule_format]:
sultana@55596
   153
  "\<lbrakk>(\<forall>x. P x) = True; (P x) = True \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
sultana@55596
   154
  "\<lbrakk>(\<exists>x. P x) = False; (P x) = False \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
sultana@55596
   155
by auto
sultana@55596
   156
sultana@55596
   157
lemma polar_exE [rule_format]:
sultana@55596
   158
  "\<lbrakk>(\<exists>x. P x) = True; \<And>x. (P x) = True \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
sultana@55596
   159
  "\<lbrakk>(\<forall>x. P x) = False; \<And>x. (P x) = False \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
sultana@55596
   160
by auto
sultana@55596
   161
wenzelm@63167
   162
ML \<open>
sultana@55596
   163
(*This carries out an allE-like rule but on (polarised) literals.
sultana@55596
   164
 Instead of yielding a free variable (which is a hell for the
sultana@55596
   165
 matcher) it seeks to use one of the subgoals' parameters.
sultana@55596
   166
 This ought to be sufficient for emulating extcnf_combined,
sultana@55596
   167
 but note that the complexity of the problem can be enormous.*)
sultana@55596
   168
fun inst_parametermatch_tac ctxt thms i = fn st =>
sultana@55596
   169
  let
sultana@55596
   170
    val gls =
wenzelm@59582
   171
      Thm.prop_of st
sultana@55596
   172
      |> Logic.strip_horn
sultana@55596
   173
      |> fst
sultana@55596
   174
sultana@55596
   175
    val parameters =
sultana@55596
   176
      if null gls then []
sultana@55596
   177
      else
sultana@55596
   178
        rpair (i - 1) gls
sultana@55596
   179
        |> uncurry nth
sultana@55596
   180
        |> strip_top_all_vars []
sultana@55596
   181
        |> fst
sultana@55596
   182
        |> map fst (*just get the parameter names*)
sultana@55596
   183
  in
sultana@55596
   184
    if null parameters then no_tac st
sultana@55596
   185
    else
sultana@55596
   186
      let
sultana@55596
   187
        fun instantiate param =
wenzelm@59780
   188
          (map (Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)] []) thms
sultana@55596
   189
                   |> FIRST')
sultana@55596
   190
        val attempts = map instantiate parameters
sultana@55596
   191
      in
sultana@55596
   192
        (fold (curry (op APPEND')) attempts (K no_tac)) i st
sultana@55596
   193
      end
sultana@55596
   194
  end
sultana@55596
   195
sultana@55596
   196
(*Attempts to use the polar_allE theorems on a specific subgoal.*)
sultana@55596
   197
fun forall_pos_tac ctxt = inst_parametermatch_tac ctxt @{thms polar_allE}
wenzelm@63167
   198
\<close>
sultana@55596
   199
wenzelm@63167
   200
ML \<open>
sultana@55596
   201
(*This is similar to inst_parametermatch_tac, but prefers to
sultana@55596
   202
  match variables having identical names. Logically, this is
sultana@55596
   203
  a hack. But it reduces the complexity of the problem.*)
sultana@55596
   204
fun nominal_inst_parametermatch_tac ctxt thm i = fn st =>
sultana@55596
   205
  let
sultana@55596
   206
    val gls =
wenzelm@59582
   207
      Thm.prop_of st
sultana@55596
   208
      |> Logic.strip_horn
sultana@55596
   209
      |> fst
sultana@55596
   210
sultana@55596
   211
    val parameters =
sultana@55596
   212
      if null gls then []
sultana@55596
   213
      else
sultana@55596
   214
        rpair (i - 1) gls
sultana@55596
   215
        |> uncurry nth
sultana@55596
   216
        |> strip_top_all_vars []
sultana@55596
   217
        |> fst
sultana@55596
   218
        |> map fst (*just get the parameter names*)
sultana@55596
   219
  in
sultana@55596
   220
    if null parameters then no_tac st
sultana@55596
   221
    else
sultana@55596
   222
      let
sultana@55596
   223
        fun instantiates param =
wenzelm@59780
   224
          Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)] [] thm
sultana@55596
   225
wenzelm@59533
   226
        val quantified_var = head_quantified_variable ctxt i st
sultana@55596
   227
      in
sultana@55596
   228
        if is_none quantified_var then no_tac st
sultana@55596
   229
        else
sultana@55596
   230
          if member (op =) parameters (the quantified_var |> fst) then
sultana@55596
   231
            instantiates (the quantified_var |> fst) i st
sultana@55596
   232
          else
sultana@55596
   233
            K no_tac i st
sultana@55596
   234
      end
sultana@55596
   235
  end
wenzelm@63167
   236
\<close>
sultana@55596
   237
sultana@55596
   238
sultana@55596
   239
subsection "Prefix massaging"
sultana@55596
   240
wenzelm@63167
   241
ML \<open>
sultana@55596
   242
exception NO_GOALS
sultana@55596
   243
sultana@55596
   244
(*Get quantifier prefix of the hypothesis and conclusion, reorder
sultana@55596
   245
  the hypothesis' quantifiers to have the ones appearing in the
sultana@55596
   246
  conclusion first.*)
sultana@55596
   247
fun canonicalise_qtfr_order ctxt i = fn st =>
sultana@55596
   248
  let
sultana@55596
   249
    val gls =
wenzelm@59582
   250
      Thm.prop_of st
sultana@55596
   251
      |> Logic.strip_horn
sultana@55596
   252
      |> fst
sultana@55596
   253
  in
sultana@55596
   254
    if null gls then raise NO_GOALS
sultana@55596
   255
    else
sultana@55596
   256
      let
sultana@55596
   257
        val (params, (hyp_clause, conc_clause)) =
sultana@55596
   258
          rpair (i - 1) gls
sultana@55596
   259
          |> uncurry nth
sultana@55596
   260
          |> strip_top_all_vars []
sultana@55596
   261
          |> apsnd Logic.dest_implies
sultana@55596
   262
sultana@55596
   263
        val (hyp_quants, hyp_body) =
sultana@55596
   264
          HOLogic.dest_Trueprop hyp_clause
sultana@55596
   265
          |> strip_top_All_vars
sultana@55596
   266
          |> apfst rev
sultana@55596
   267
sultana@55596
   268
        val conc_quants =
sultana@55596
   269
          HOLogic.dest_Trueprop conc_clause
sultana@55596
   270
          |> strip_top_All_vars
sultana@55596
   271
          |> fst
sultana@55596
   272
sultana@55596
   273
        val new_hyp =
sultana@55596
   274
          (* fold absfree new_hyp_prefix hyp_body *)
sultana@55596
   275
          (*HOLogic.list_all*)
sultana@55596
   276
          fold_rev (fn (v, ty) => fn t => HOLogic.mk_all (v, ty, t))
sultana@55596
   277
           (prefix_intersection_list
sultana@55596
   278
             hyp_quants conc_quants)
sultana@55596
   279
           hyp_body
sultana@55596
   280
          |> HOLogic.mk_Trueprop
sultana@55596
   281
sultana@55596
   282
         val thm = Goal.prove ctxt [] []
sultana@55596
   283
           (Logic.mk_implies (hyp_clause, new_hyp))
sultana@55596
   284
           (fn _ =>
wenzelm@60754
   285
              (REPEAT_DETERM (HEADGOAL (resolve_tac ctxt @{thms allI})))
sultana@55596
   286
              THEN (REPEAT_DETERM
sultana@55596
   287
                    (HEADGOAL
sultana@55596
   288
                     (nominal_inst_parametermatch_tac ctxt @{thm allE})))
wenzelm@60754
   289
              THEN HEADGOAL (assume_tac ctxt))
sultana@55596
   290
      in
wenzelm@60754
   291
        dresolve_tac ctxt [thm] i st
sultana@55596
   292
      end
sultana@55596
   293
    end
wenzelm@63167
   294
\<close>
sultana@55596
   295
sultana@55596
   296
sultana@55596
   297
subsection "Some general rules and congruences"
sultana@55596
   298
sultana@55596
   299
(*this isn't an actual rule used in Leo2, but it seems to be
sultana@55596
   300
  applied implicitly during some Leo2 inferences.*)
sultana@55596
   301
lemma polarise: "P ==> P = True" by auto
sultana@55596
   302
wenzelm@63167
   303
ML \<open>
sultana@55596
   304
fun is_polarised t =
sultana@55596
   305
  (TPTP_Reconstruct.remove_polarity true t; true)
sultana@55596
   306
  handle TPTP_Reconstruct.UNPOLARISED _ => false
sultana@55596
   307
wenzelm@60754
   308
fun polarise_subgoal_hyps ctxt =
wenzelm@60754
   309
  COND' (SOME #> TERMPRED is_polarised (fn _ => true)) (K no_tac) (dresolve_tac ctxt @{thms polarise})
wenzelm@63167
   310
\<close>
sultana@55596
   311
sultana@55596
   312
lemma simp_meta [rule_format]:
sultana@55596
   313
  "(A --> B) == (~A | B)"
sultana@55596
   314
  "(A | B) | C == A | B | C"
sultana@55596
   315
  "(A & B) & C == A & B & C"
sultana@55596
   316
  "(~ (~ A)) == A"
sultana@55596
   317
  (* "(A & B) == (~ (~A | ~B))" *)
sultana@55596
   318
  "~ (A & B) == (~A | ~B)"
sultana@55596
   319
  "~(A | B) == (~A) & (~B)"
sultana@55596
   320
by auto
sultana@55596
   321
sultana@55596
   322
sultana@55596
   323
subsection "Emulation of Leo2's inference rules"
sultana@55596
   324
sultana@55596
   325
(*this is not included in simp_meta since it would make a mess of the polarities*)
sultana@55596
   326
lemma expand_iff [rule_format]:
sultana@55596
   327
 "((A :: bool) = B) \<equiv> (~ A | B) & (~ B | A)"
sultana@55596
   328
by (rule eq_reflection, auto)
sultana@55596
   329
sultana@55596
   330
lemma polarity_switch [rule_format]:
sultana@55596
   331
  "(\<not> P) = True \<Longrightarrow> P = False"
sultana@55596
   332
  "(\<not> P) = False \<Longrightarrow> P = True"
sultana@55596
   333
  "P = False \<Longrightarrow> (\<not> P) = True"
sultana@55596
   334
  "P = True \<Longrightarrow> (\<not> P) = False"
sultana@55596
   335
by auto
sultana@55596
   336
sultana@55596
   337
lemma solved_all_splits: "False = True \<Longrightarrow> False" by simp
wenzelm@63167
   338
ML \<open>
wenzelm@60754
   339
fun solved_all_splits_tac ctxt =
wenzelm@60754
   340
  TRY (eresolve_tac ctxt @{thms conjE} 1)
wenzelm@60754
   341
  THEN resolve_tac ctxt @{thms solved_all_splits} 1
wenzelm@60754
   342
  THEN assume_tac ctxt 1
wenzelm@63167
   343
\<close>
sultana@55596
   344
sultana@55596
   345
lemma lots_of_logic_expansions_meta [rule_format]:
sultana@55596
   346
  "(((A :: bool) = B) = True) == (((A \<longrightarrow> B) = True) & ((B \<longrightarrow> A) = True))"
sultana@55596
   347
  "((A :: bool) = B) = False == (((~A) | B) = False) | (((~B) | A) = False)"
sultana@55596
   348
sultana@55596
   349
  "((F = G) = True) == (! x. (F x = G x)) = True"
sultana@55596
   350
  "((F = G) = False) == (! x. (F x = G x)) = False"
sultana@55596
   351
sultana@55596
   352
  "(A | B) = True == (A = True) | (B = True)"
sultana@55596
   353
  "(A & B) = False == (A = False) | (B = False)"
sultana@55596
   354
  "(A | B) = False == (A = False) & (B = False)"
sultana@55596
   355
  "(A & B) = True == (A = True) & (B = True)"
sultana@55596
   356
  "(~ A) = True == A = False"
sultana@55596
   357
  "(~ A) = False == A = True"
sultana@55596
   358
  "~ (A = True) == A = False"
sultana@55596
   359
  "~ (A = False) == A = True"
sultana@55596
   360
by (rule eq_reflection, auto)+
sultana@55596
   361
sultana@55596
   362
(*this is used in extcnf_combined handler*)
sultana@55596
   363
lemma eq_neg_bool: "((A :: bool) = B) = False ==> ((~ (A | B)) | ~ ((~ A) | (~ B))) = False"
sultana@55596
   364
by auto
sultana@55596
   365
sultana@55596
   366
lemma eq_pos_bool:
sultana@55596
   367
  "((A :: bool) = B) = True ==> ((~ (A | B)) | ~ (~ A | ~ B)) = True"
sultana@55596
   368
  "(A = B) = True \<Longrightarrow> A = True \<or> B = False"
sultana@55596
   369
  "(A = B) = True \<Longrightarrow> A = False \<or> B = True"
sultana@55596
   370
by auto
sultana@55596
   371
sultana@55596
   372
(*next formula is more versatile than
sultana@55596
   373
    "(F = G) = True \<Longrightarrow> \<forall>x. ((F x = G x) = True)"
sultana@55596
   374
  since it doesn't assume that clause is singleton. After splitqtfr,
sultana@55596
   375
  and after applying allI exhaustively to the conclusion, we can
sultana@55596
   376
  use the existing functions to find the "(F x = G x) = True"
sultana@55596
   377
  disjunct in the conclusion*)
sultana@55596
   378
lemma eq_pos_func: "\<And> x. (F = G) = True \<Longrightarrow> (F x = G x) = True"
sultana@55596
   379
by auto
sultana@55596
   380
sultana@55596
   381
(*make sure the conclusion consists of just "False"*)
sultana@55596
   382
lemma flip:
sultana@55596
   383
  "((A = True) ==> False) ==> A = False"
sultana@55596
   384
  "((A = False) ==> False) ==> A = True"
sultana@55596
   385
by auto
sultana@55596
   386
sultana@55596
   387
(*FIXME try to use Drule.equal_elim_rule1 directly for this*)
sultana@55596
   388
lemma equal_elim_rule1: "(A \<equiv> B) \<Longrightarrow> A \<Longrightarrow> B" by auto
sultana@55596
   389
lemmas leo2_rules =
sultana@55596
   390
 lots_of_logic_expansions_meta[THEN equal_elim_rule1]
sultana@55596
   391
sultana@55596
   392
(*FIXME is there any overlap with lots_of_logic_expansions_meta or leo2_rules?*)
sultana@55596
   393
lemma extuni_bool2 [rule_format]: "(A = B) = False \<Longrightarrow> (A = True) | (B = True)" by auto
sultana@55596
   394
lemma extuni_bool1 [rule_format]: "(A = B) = False \<Longrightarrow> (A = False) | (B = False)" by auto
sultana@55596
   395
lemma extuni_triv [rule_format]: "(A = A) = False \<Longrightarrow> R" by auto
sultana@55596
   396
sultana@55596
   397
(*Order (of A, B, C, D) matters*)
sultana@55596
   398
lemma dec_commut_eq [rule_format]:
sultana@55596
   399
  "((A = B) = (C = D)) = False \<Longrightarrow> (B = C) = False | (A = D) = False"
sultana@55596
   400
  "((A = B) = (C = D)) = False \<Longrightarrow> (B = D) = False | (A = C) = False"
sultana@55596
   401
by auto
sultana@55596
   402
lemma dec_commut_disj [rule_format]:
sultana@55596
   403
  "((A \<or> B) = (C \<or> D)) = False \<Longrightarrow> (B = C) = False \<or> (A = D) = False"
sultana@55596
   404
by auto
sultana@55596
   405
sultana@55596
   406
lemma extuni_func [rule_format]: "(F = G) = False \<Longrightarrow> (! X. (F X = G X)) = False" by auto
sultana@55596
   407
sultana@55596
   408
sultana@55596
   409
subsection "Emulation: tactics"
sultana@55596
   410
wenzelm@63167
   411
ML \<open>
sultana@55596
   412
(*Instantiate a variable according to the info given in the
sultana@55596
   413
  proof annotation. Through this we avoid having to come up
sultana@55596
   414
  with instantiations during reconstruction.*)
sultana@55596
   415
fun bind_tac ctxt prob_name ordered_binds =
sultana@55596
   416
  let
sultana@55596
   417
    val thy = Proof_Context.theory_of ctxt
sultana@55596
   418
    fun term_to_string t =
sultana@55596
   419
        Print_Mode.with_modes [""]
sultana@55596
   420
          (fn () => Output.output (Syntax.string_of_term ctxt t)) ()
sultana@55596
   421
    val ordered_instances =
sultana@55596
   422
      TPTP_Reconstruct.interpret_bindings prob_name thy ordered_binds []
sultana@55596
   423
      |> map (snd #> term_to_string)
sultana@55596
   424
      |> permute
sultana@55596
   425
sultana@55596
   426
    (*instantiate a list of variables, order matters*)
sultana@55596
   427
    fun instantiate_vars ctxt vars : tactic =
sultana@55596
   428
      map (fn var =>
sultana@55596
   429
            Rule_Insts.eres_inst_tac ctxt
wenzelm@59780
   430
             [((("x", 0), Position.none), var)] [] @{thm allE} 1)
sultana@55596
   431
          vars
sultana@55596
   432
      |> EVERY
sultana@55596
   433
sultana@55596
   434
    fun instantiate_tac vars =
sultana@55596
   435
      instantiate_vars ctxt vars
wenzelm@60754
   436
      THEN (HEADGOAL (assume_tac ctxt))
sultana@55596
   437
  in
sultana@55596
   438
    HEADGOAL (canonicalise_qtfr_order ctxt)
wenzelm@60754
   439
    THEN (REPEAT_DETERM (HEADGOAL (resolve_tac ctxt @{thms allI})))
sultana@55596
   440
    THEN REPEAT_DETERM (HEADGOAL (nominal_inst_parametermatch_tac ctxt @{thm allE}))
sultana@55596
   441
    (*now only the variable to instantiate should be left*)
sultana@55596
   442
    THEN FIRST (map instantiate_tac ordered_instances)
sultana@55596
   443
  end
wenzelm@63167
   444
\<close>
sultana@55596
   445
wenzelm@63167
   446
ML \<open>
sultana@55596
   447
(*Simplification tactics*)
sultana@55596
   448
local
sultana@55596
   449
  fun rew_goal_tac thms ctxt i =
sultana@55596
   450
    rewrite_goal_tac ctxt thms i
sultana@55596
   451
    |> CHANGED
sultana@55596
   452
in
sultana@55596
   453
  val expander_animal =
sultana@55596
   454
    rew_goal_tac (@{thms simp_meta} @ @{thms lots_of_logic_expansions_meta})
sultana@55596
   455
sultana@55596
   456
  val simper_animal =
sultana@55596
   457
    rew_goal_tac @{thms simp_meta}
sultana@55596
   458
end
wenzelm@63167
   459
\<close>
sultana@55596
   460
sultana@55596
   461
lemma prop_normalise [rule_format]:
sultana@55596
   462
  "(A | B) | C == A | B | C"
sultana@55596
   463
  "(A & B) & C == A & B & C"
sultana@55596
   464
  "A | B == ~(~A & ~B)"
sultana@55596
   465
  "~~ A == A"
sultana@55596
   466
by auto
wenzelm@63167
   467
ML \<open>
sultana@55596
   468
(*i.e., break_conclusion*)
sultana@55596
   469
fun flip_conclusion_tac ctxt =
sultana@55596
   470
  let
sultana@55596
   471
    val default_tac =
sultana@55596
   472
      (TRY o CHANGED o (rewrite_goal_tac ctxt @{thms prop_normalise}))
wenzelm@60754
   473
      THEN' resolve_tac ctxt @{thms notI}
wenzelm@60754
   474
      THEN' (REPEAT_DETERM o eresolve_tac ctxt @{thms conjE})
sultana@55596
   475
      THEN' (TRY o (expander_animal ctxt))
sultana@55596
   476
  in
wenzelm@59498
   477
    default_tac ORELSE' resolve_tac ctxt @{thms flip}
sultana@55596
   478
  end
wenzelm@63167
   479
\<close>
sultana@55596
   480
sultana@55596
   481
sultana@55596
   482
subsection "Skolemisation"
sultana@55596
   483
sultana@55596
   484
lemma skolemise [rule_format]:
sultana@55596
   485
  "\<forall> P. (~ (! x. P x)) \<longrightarrow> ~ (P (SOME x. ~ P x))"
sultana@55596
   486
proof -
sultana@55596
   487
  have "\<And> P. (~ (! x. P x)) \<Longrightarrow> ~ (P (SOME x. ~ P x))"
sultana@55596
   488
  proof -
sultana@55596
   489
    fix P
sultana@55596
   490
    assume ption: "~ (! x. P x)"
sultana@55596
   491
    hence a: "? x. ~ P x" by force
sultana@55596
   492
sultana@55596
   493
    have hilbert : "\<And> P. (? x. P x) \<Longrightarrow> (P (SOME x. P x))"
sultana@55596
   494
    proof -
sultana@55596
   495
      fix P
sultana@55596
   496
      assume "(? x. P x)"
sultana@55596
   497
      thus "(P (SOME x. P x))"
sultana@55596
   498
        apply auto
sultana@55596
   499
        apply (rule someI)
sultana@55596
   500
        apply auto
sultana@55596
   501
        done
sultana@55596
   502
    qed
sultana@55596
   503
sultana@55596
   504
    from a show "~ P (SOME x. ~ P x)"
sultana@55596
   505
    proof -
sultana@55596
   506
      assume "? x. ~ P x"
sultana@55596
   507
      hence "\<not> P (SOME x. \<not> P x)" by (rule hilbert)
sultana@55596
   508
      thus ?thesis .
sultana@55596
   509
    qed
sultana@55596
   510
  qed
sultana@55596
   511
  thus ?thesis by blast
sultana@55596
   512
qed
sultana@55596
   513
sultana@55596
   514
lemma polar_skolemise [rule_format]:
sultana@55596
   515
  "\<forall> P. (! x. P x) = False \<longrightarrow> (P (SOME x. ~ P x)) = False"
sultana@55596
   516
proof -
sultana@55596
   517
  have "\<And> P. (! x. P x) = False \<Longrightarrow> (P (SOME x. ~ P x)) = False"
sultana@55596
   518
  proof -
sultana@55596
   519
    fix P
sultana@55596
   520
    assume ption: "(! x. P x) = False"
sultana@55596
   521
    hence "\<not> (\<forall> x. P x)" by force
sultana@55596
   522
    hence "\<not> All P" by force
sultana@55596
   523
    hence "\<not> (P (SOME x. \<not> P x))" by (rule skolemise)
sultana@55596
   524
    thus "(P (SOME x. \<not> P x)) = False" by force
sultana@55596
   525
  qed
sultana@55596
   526
  thus ?thesis by blast
sultana@55596
   527
qed
sultana@55596
   528
sultana@55596
   529
lemma leo2_skolemise [rule_format]:
sultana@55596
   530
  "\<forall> P sk. (! x. P x) = False \<longrightarrow> (sk = (SOME x. ~ P x)) \<longrightarrow> (P sk) = False"
sultana@55596
   531
by (clarify, rule polar_skolemise)
sultana@55596
   532
sultana@55596
   533
lemma lift_forall [rule_format]:
sultana@55596
   534
  "!! x. (! x. A x) = True ==> (A x) = True"
sultana@55596
   535
  "!! x. (? x. A x) = False ==> (A x) = False"
sultana@55596
   536
by auto
sultana@55596
   537
lemma lift_exists [rule_format]:
sultana@55596
   538
  "\<lbrakk>(All P) = False; sk = (SOME x. \<not> P x)\<rbrakk> \<Longrightarrow> P sk = False"
sultana@55596
   539
  "\<lbrakk>(Ex P) = True; sk = (SOME x. P x)\<rbrakk> \<Longrightarrow> P sk = True"
sultana@55596
   540
apply (drule polar_skolemise, simp)
sultana@55596
   541
apply (simp, drule someI_ex, simp)
sultana@55596
   542
done
sultana@55596
   543
wenzelm@63167
   544
ML \<open>
sultana@55596
   545
(*FIXME LHS should be constant. Currently allow variables for testing. Probably should still allow Vars (but not Frees) since they'll act as intermediate values*)
sultana@55596
   546
fun conc_is_skolem_def t =
sultana@55596
   547
  case t of
sultana@55596
   548
      Const (@{const_name HOL.eq}, _) $ t' $ (Const (@{const_name Hilbert_Choice.Eps}, _) $ _) =>
sultana@55596
   549
      let
sultana@55596
   550
        val (h, args) =
sultana@55596
   551
          strip_comb t'
sultana@55596
   552
          |> apfst (strip_abs #> snd #> strip_comb #> fst)
sultana@55596
   553
        val get_const_name = dest_Const #> fst
sultana@55596
   554
        val h_property =
sultana@55596
   555
          is_Free h orelse
sultana@55596
   556
          is_Var h orelse
sultana@55596
   557
          (is_Const h
sultana@55596
   558
           andalso (get_const_name h <> get_const_name @{term HOL.Ex})
sultana@55596
   559
           andalso (get_const_name h <> get_const_name @{term HOL.All})
sultana@55596
   560
           andalso (h <> @{term Hilbert_Choice.Eps})
sultana@55596
   561
           andalso (h <> @{term HOL.conj})
sultana@55596
   562
           andalso (h <> @{term HOL.disj})
sultana@55596
   563
           andalso (h <> @{term HOL.eq})
sultana@55596
   564
           andalso (h <> @{term HOL.implies})
sultana@55596
   565
           andalso (h <> @{term HOL.The})
sultana@55596
   566
           andalso (h <> @{term HOL.Ex1})
sultana@55596
   567
           andalso (h <> @{term HOL.Not})
sultana@55596
   568
           andalso (h <> @{term HOL.iff})
sultana@55596
   569
           andalso (h <> @{term HOL.not_equal}))
sultana@55596
   570
        val args_property =
sultana@55596
   571
          fold (fn t => fn b =>
sultana@55596
   572
           b andalso is_Free t) args true
sultana@55596
   573
      in
sultana@55596
   574
        h_property andalso args_property
sultana@55596
   575
      end
sultana@55596
   576
    | _ => false
wenzelm@63167
   577
\<close>
sultana@55596
   578
wenzelm@63167
   579
ML \<open>
sultana@55596
   580
(*Hack used to detect if a Skolem definition, with an LHS Var, has had the LHS instantiated into an unacceptable term.*)
sultana@55596
   581
fun conc_is_bad_skolem_def t =
sultana@55596
   582
  case t of
sultana@55596
   583
      Const (@{const_name HOL.eq}, _) $ t' $ (Const (@{const_name Hilbert_Choice.Eps}, _) $ _) =>
sultana@55596
   584
      let
sultana@55596
   585
        val (h, args) = strip_comb t'
sultana@55596
   586
        val get_const_name = dest_Const #> fst
sultana@55596
   587
        val const_h_test =
sultana@55596
   588
          if is_Const h then
sultana@55596
   589
            (get_const_name h = get_const_name @{term HOL.Ex})
sultana@55596
   590
             orelse (get_const_name h = get_const_name @{term HOL.All})
sultana@55596
   591
             orelse (h = @{term Hilbert_Choice.Eps})
sultana@55596
   592
             orelse (h = @{term HOL.conj})
sultana@55596
   593
             orelse (h = @{term HOL.disj})
sultana@55596
   594
             orelse (h = @{term HOL.eq})
sultana@55596
   595
             orelse (h = @{term HOL.implies})
sultana@55596
   596
             orelse (h = @{term HOL.The})
sultana@55596
   597
             orelse (h = @{term HOL.Ex1})
sultana@55596
   598
             orelse (h = @{term HOL.Not})
sultana@55596
   599
             orelse (h = @{term HOL.iff})
sultana@55596
   600
             orelse (h = @{term HOL.not_equal})
sultana@55596
   601
          else true
sultana@55596
   602
        val h_property =
sultana@55596
   603
          not (is_Free h) andalso
sultana@55596
   604
          not (is_Var h) andalso
sultana@55596
   605
          const_h_test
sultana@55596
   606
        val args_property =
sultana@55596
   607
          fold (fn t => fn b =>
sultana@55596
   608
           b andalso is_Free t) args true
sultana@55596
   609
      in
sultana@55596
   610
        h_property andalso args_property
sultana@55596
   611
      end
sultana@55596
   612
    | _ => false
wenzelm@63167
   613
\<close>
sultana@55596
   614
wenzelm@63167
   615
ML \<open>
sultana@55596
   616
fun get_skolem_conc t =
sultana@55596
   617
  let
sultana@55596
   618
    val t' =
sultana@55596
   619
      strip_top_all_vars [] t
sultana@55596
   620
      |> snd
sultana@55596
   621
      |> try_dest_Trueprop
sultana@55596
   622
  in
sultana@55596
   623
    case t' of
sultana@55596
   624
        Const (@{const_name HOL.eq}, _) $ t' $ (Const (@{const_name Hilbert_Choice.Eps}, _) $ _) => SOME t'
sultana@55596
   625
      | _ => NONE
sultana@55596
   626
  end
sultana@55596
   627
sultana@55596
   628
fun get_skolem_conc_const t =
sultana@55596
   629
  lift_option
sultana@55596
   630
   (fn t' =>
sultana@55596
   631
     head_of t'
sultana@55596
   632
     |> strip_abs_body
sultana@55596
   633
     |> head_of
sultana@55596
   634
     |> dest_Const)
sultana@55596
   635
   (get_skolem_conc t)
wenzelm@63167
   636
\<close>
sultana@55596
   637
sultana@55596
   638
(*
sultana@55596
   639
Technique for handling quantifiers:
sultana@55596
   640
  Principles:
sultana@55596
   641
  * allE should always match with a !!
sultana@55596
   642
  * exE should match with a constant,
sultana@55596
   643
     or bind a fresh !! -- currently not doing the latter since it never seems to arised in normal Leo2 proofs.
sultana@55596
   644
*)
sultana@55596
   645
wenzelm@63167
   646
ML \<open>
sultana@55596
   647
fun forall_neg_tac candidate_consts ctxt i = fn st =>
sultana@55596
   648
  let
sultana@55596
   649
    val gls =
wenzelm@59582
   650
      Thm.prop_of st
sultana@55596
   651
      |> Logic.strip_horn
sultana@55596
   652
      |> fst
sultana@55596
   653
sultana@55596
   654
    val parameters =
sultana@55596
   655
      if null gls then ""
sultana@55596
   656
      else
sultana@55596
   657
        rpair (i - 1) gls
sultana@55596
   658
        |> uncurry nth
sultana@55596
   659
        |> strip_top_all_vars []
sultana@55596
   660
        |> fst
sultana@55596
   661
        |> map fst (*just get the parameter names*)
sultana@55596
   662
        |> (fn l =>
sultana@55596
   663
              if null l then ""
sultana@55596
   664
              else
sultana@55596
   665
                space_implode " " l
sultana@55596
   666
                |> pair " "
sultana@55596
   667
                |> op ^)
sultana@55596
   668
sultana@55596
   669
  in
sultana@55596
   670
    if null gls orelse null candidate_consts then no_tac st
sultana@55596
   671
    else
sultana@55596
   672
      let
sultana@55596
   673
        fun instantiate const_name =
wenzelm@59780
   674
          Rule_Insts.dres_inst_tac ctxt [((("sk", 0), Position.none), const_name ^ parameters)] []
wenzelm@59755
   675
            @{thm leo2_skolemise}
sultana@55596
   676
        val attempts = map instantiate candidate_consts
sultana@55596
   677
      in
sultana@55596
   678
        (fold (curry (op APPEND')) attempts (K no_tac)) i st
sultana@55596
   679
      end
sultana@55596
   680
  end
wenzelm@63167
   681
\<close>
sultana@55596
   682
wenzelm@63167
   683
ML \<open>
sultana@55596
   684
exception SKOLEM_DEF of term (*The tactic wasn't pointed at a skolem definition*)
sultana@55596
   685
exception NO_SKOLEM_DEF of (*skolem const name*)string * Binding.binding * term (*The tactic could not find a skolem definition in the theory*)
sultana@55596
   686
fun absorb_skolem_def ctxt prob_name_opt i = fn st =>
sultana@55596
   687
  let
sultana@55596
   688
    val thy = Proof_Context.theory_of ctxt
sultana@55596
   689
sultana@55596
   690
    val gls =
wenzelm@59582
   691
      Thm.prop_of st
sultana@55596
   692
      |> Logic.strip_horn
sultana@55596
   693
      |> fst
sultana@55596
   694
sultana@55596
   695
    val conclusion =
sultana@55596
   696
      if null gls then
sultana@55596
   697
        (*this should never be thrown*)
sultana@55596
   698
        raise NO_GOALS
sultana@55596
   699
      else
sultana@55596
   700
        rpair (i - 1) gls
sultana@55596
   701
        |> uncurry nth
sultana@55596
   702
        |> strip_top_all_vars []
sultana@55596
   703
        |> snd
sultana@55596
   704
        |> Logic.strip_horn
sultana@55596
   705
        |> snd
sultana@55596
   706
sultana@55596
   707
    fun skolem_const_info_of t =
sultana@55596
   708
      case t of
sultana@55596
   709
          Const (@{const_name HOL.Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t' $ (Const (@{const_name Hilbert_Choice.Eps}, _) $ _)) =>
sultana@55596
   710
          head_of t'
sultana@55596
   711
          |> strip_abs_body (*since in general might have a skolem term, so we want to rip out the prefixing lambdas to get to the constant (which should be at head position)*)
sultana@55596
   712
          |> head_of
sultana@55596
   713
          |> dest_Const
sultana@55596
   714
        | _ => raise SKOLEM_DEF t
sultana@55596
   715
sultana@55596
   716
    val const_name =
sultana@55596
   717
      skolem_const_info_of conclusion
sultana@55596
   718
      |> fst
sultana@55596
   719
sultana@55596
   720
    val def_name = const_name ^ "_def"
sultana@55596
   721
sultana@55596
   722
    val bnd_def = (*FIXME consts*)
sultana@55596
   723
      const_name
wenzelm@56220
   724
      |> Long_Name.implode o tl o Long_Name.explode (*FIXME hack to drop theory-name prefix*)
sultana@55596
   725
      |> Binding.qualified_name
sultana@55596
   726
      |> Binding.suffix_name "_def"
sultana@55596
   727
sultana@55596
   728
    val bnd_name =
sultana@55596
   729
      case prob_name_opt of
sultana@55596
   730
          NONE => bnd_def
sultana@55596
   731
        | SOME prob_name =>
sultana@55596
   732
(*            Binding.qualify false
sultana@55596
   733
             (TPTP_Problem_Name.mangle_problem_name prob_name)
sultana@55596
   734
*)
sultana@55596
   735
             bnd_def
sultana@55596
   736
sultana@55596
   737
    val thm =
wenzelm@59882
   738
      (case try (Thm.axiom thy) def_name of
wenzelm@59882
   739
        SOME thm => thm
wenzelm@59882
   740
      | NONE =>
wenzelm@59882
   741
          if is_none prob_name_opt then
wenzelm@59882
   742
            (*This mode is for testing, so we can be a bit
wenzelm@59882
   743
              looser with theories*)
wenzelm@59882
   744
            (* FIXME bad theory context!? *)
wenzelm@59882
   745
            Thm.add_axiom_global (bnd_name, conclusion) thy
wenzelm@59882
   746
            |> fst |> snd
wenzelm@59882
   747
          else
wenzelm@59882
   748
            raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion)))
sultana@55596
   749
  in
wenzelm@60754
   750
    resolve_tac ctxt [Drule.export_without_context thm] i st
sultana@55596
   751
  end
sultana@55596
   752
  handle SKOLEM_DEF _ => no_tac st
wenzelm@63167
   753
\<close>
sultana@55596
   754
wenzelm@63167
   755
ML \<open>
sultana@55596
   756
(*
sultana@55596
   757
In current system, there should only be 2 subgoals: the one where
sultana@55596
   758
the skolem definition is being built (with a Var in the LHS), and the other subgoal using Var.
sultana@55596
   759
*)
sultana@55596
   760
(*arity must be greater than 0. if arity=0 then
sultana@55596
   761
  there's no need to use this expensive matching.*)
sultana@55596
   762
fun find_skolem_term ctxt consts_candidate arity = fn st =>
sultana@55596
   763
  let
sultana@55596
   764
    val _ = @{assert} (arity > 0)
sultana@55596
   765
sultana@55596
   766
    val gls =
wenzelm@59582
   767
      Thm.prop_of st
sultana@55596
   768
      |> Logic.strip_horn
sultana@55596
   769
      |> fst
sultana@55596
   770
sultana@55596
   771
    (*extract the conclusion of each subgoal*)
sultana@55596
   772
    val conclusions =
sultana@55596
   773
      if null gls then
sultana@55596
   774
        raise NO_GOALS
sultana@55596
   775
      else
sultana@55596
   776
        map (strip_top_all_vars [] #> snd #> Logic.strip_horn #> snd) gls
sultana@55596
   777
        (*Remove skolem-definition conclusion, to avoid wasting time analysing it*)
wenzelm@58412
   778
        |> filter (try_dest_Trueprop #> conc_is_skolem_def #> not)
sultana@55596
   779
        (*There should only be a single goal*) (*FIXME this might not always be the case, in practice*)
sultana@55596
   780
        (* |> tap (fn x => @{assert} (is_some (try the_single x))) *)
sultana@55596
   781
sultana@55596
   782
    (*look for subterms headed by a skolem constant, and whose
sultana@55596
   783
      arguments are all parameter Vars*)
sultana@55596
   784
    fun get_skolem_terms args (acc : term list) t =
sultana@55596
   785
      case t of
sultana@55596
   786
          (c as Const _) $ (v as Free _) =>
sultana@55596
   787
            if c = consts_candidate andalso
sultana@55596
   788
             arity = length args + 1 then
sultana@55596
   789
              (list_comb (c, v :: args)) :: acc
sultana@55596
   790
            else acc
sultana@55596
   791
        | t1 $ (v as Free _) =>
sultana@55596
   792
            get_skolem_terms (v :: args) acc t1 @
sultana@55596
   793
             get_skolem_terms [] acc t1
sultana@55596
   794
        | t1 $ t2 =>
sultana@55596
   795
            get_skolem_terms [] acc t1 @
sultana@55596
   796
             get_skolem_terms [] acc t2
sultana@55596
   797
        | Abs (_, _, t') => get_skolem_terms [] acc t'
sultana@55596
   798
        | _ => acc
sultana@55596
   799
  in
sultana@55596
   800
    map (strip_top_All_vars #> snd) conclusions
wenzelm@58411
   801
    |> maps (get_skolem_terms [] [])
sultana@55596
   802
    |> distinct (op =)
sultana@55596
   803
  end
wenzelm@63167
   804
\<close>
sultana@55596
   805
wenzelm@63167
   806
ML \<open>
sultana@55596
   807
fun instantiate_skols ctxt consts_candidates i = fn st =>
sultana@55596
   808
  let
sultana@55596
   809
    val gls =
wenzelm@59582
   810
      Thm.prop_of st
sultana@55596
   811
      |> Logic.strip_horn
sultana@55596
   812
      |> fst
sultana@55596
   813
sultana@55596
   814
    val (params, conclusion) =
sultana@55596
   815
      if null gls then
sultana@55596
   816
        raise NO_GOALS
sultana@55596
   817
      else
sultana@55596
   818
        rpair (i - 1) gls
sultana@55596
   819
        |> uncurry nth
sultana@55596
   820
        |> strip_top_all_vars []
sultana@55596
   821
        |> apsnd (Logic.strip_horn #> snd)
sultana@55596
   822
sultana@55596
   823
    fun skolem_const_info_of t =
sultana@55596
   824
      case t of
sultana@55596
   825
          Const (@{const_name HOL.Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ lhs $ (Const (@{const_name Hilbert_Choice.Eps}, _) $ rhs)) =>
sultana@55596
   826
          let
sultana@55596
   827
            (*the parameters we will concern ourselves with*)
sultana@55596
   828
            val params' =
sultana@55596
   829
              Term.add_frees lhs []
sultana@55596
   830
              |> distinct (op =)
sultana@55596
   831
            (*check to make sure that params' <= params*)
wenzelm@58412
   832
            val _ = @{assert} (forall (member (op =) params) params')
sultana@55596
   833
            val skolem_const_ty =
sultana@55596
   834
              let
sultana@55596
   835
                val (skolem_const_prety, no_params) =
sultana@55596
   836
                  Term.strip_comb lhs
sultana@55596
   837
                  |> apfst (dest_Var #> snd) (*head of lhs consists of a logical variable. we just want its type.*)
sultana@55596
   838
                  |> apsnd length
sultana@55596
   839
sultana@55596
   840
                val _ = @{assert} (length params = no_params)
sultana@55596
   841
sultana@55596
   842
                (*get value type of a function type after n arguments have been supplied*)
sultana@55596
   843
                fun get_val_ty n ty =
sultana@55596
   844
                  if n = 0 then ty
sultana@55596
   845
                  else get_val_ty (n - 1) (dest_funT ty |> snd)
sultana@55596
   846
              in
sultana@55596
   847
                get_val_ty no_params skolem_const_prety
sultana@55596
   848
              end
sultana@55596
   849
sultana@55596
   850
          in
sultana@55596
   851
            (skolem_const_ty, params')
sultana@55596
   852
          end
sultana@55596
   853
        | _ => raise (SKOLEM_DEF t)
sultana@55596
   854
sultana@55596
   855
(*
sultana@55596
   856
find skolem const candidates which, after applying distinct members of params' we end up with, give us something of type skolem_const_ty.
sultana@55596
   857
sultana@55596
   858
given a candidate's type, skolem_const_ty, and params', we get some pemutations of params' (i.e. the order in which they can be given to the candidate in order to get skolem_const_ty). If the list of permutations is empty, then we cannot use that candidate.
sultana@55596
   859
*)
sultana@55596
   860
(*
sultana@55596
   861
only returns a single matching -- since terms are linear, and variable arguments are Vars, order shouldn't matter, so we can ignore permutations.
sultana@55596
   862
doesn't work with polymorphism (for which we'd need to use type unification) -- this is OK since no terms should be polymorphic, since Leo2 proofs aren't.
sultana@55596
   863
*)
sultana@55596
   864
    fun use_candidate target_ty params acc cur_ty =
sultana@55596
   865
      if null params then
wenzelm@58941
   866
        if cur_ty = target_ty then
sultana@55596
   867
          SOME (rev acc)
sultana@55596
   868
        else NONE
sultana@55596
   869
      else
sultana@55596
   870
        let
sultana@55596
   871
          val (arg_ty, val_ty) = Term.dest_funT cur_ty
sultana@55596
   872
          (*now find a param of type arg_ty*)
sultana@55596
   873
          val (candidate_param, params') =
wenzelm@58941
   874
            find_and_remove (snd #> pair arg_ty #> op =) params
sultana@55596
   875
        in
sultana@55596
   876
          use_candidate target_ty params' (candidate_param :: acc) val_ty
sultana@55596
   877
        end
wenzelm@62243
   878
        handle TYPE ("dest_funT", _, _) => NONE  (* FIXME fragile *)
wenzelm@62243
   879
             | _ => NONE  (* FIXME avoid catch-all handler *)
sultana@55596
   880
sultana@55596
   881
    val (skolem_const_ty, params') = skolem_const_info_of conclusion
sultana@55596
   882
sultana@55596
   883
(*
sultana@55596
   884
For each candidate, build a term and pass it to Thm.instantiate, whic in turn is chained with PRIMITIVE to give us this_tactic.
sultana@55596
   885
sultana@55596
   886
Big picture:
sultana@55596
   887
  we run the following:
sultana@55596
   888
    drule leo2_skolemise THEN' this_tactic
sultana@55596
   889
sultana@55596
   890
NOTE: remember to APPEND' instead of ORELSE' the two tactics relating to skolemisation
sultana@55596
   891
*)
sultana@55596
   892
sultana@55596
   893
    val filtered_candidates =
sultana@55596
   894
      map (dest_Const
sultana@55596
   895
           #> snd
sultana@55596
   896
           #> use_candidate skolem_const_ty params' [])
sultana@55596
   897
       consts_candidates (* prefiltered_candidates *)
sultana@55596
   898
      |> pair consts_candidates (* prefiltered_candidates *)
sultana@55596
   899
      |> ListPair.zip
sultana@55596
   900
      |> filter (snd #> is_none #> not)
sultana@55596
   901
      |> map (apsnd the)
sultana@55596
   902
sultana@55596
   903
    val skolem_terms =
sultana@55596
   904
      let
sultana@55596
   905
        fun make_result_t (t, args) =
sultana@55596
   906
          (* list_comb (t, map Free args) *)
sultana@55596
   907
          if length args > 0 then
sultana@55596
   908
            hd (find_skolem_term ctxt t (length args) st)
sultana@55596
   909
          else t
sultana@55596
   910
      in
sultana@55596
   911
        map make_result_t filtered_candidates
sultana@55596
   912
      end
sultana@55596
   913
sultana@55596
   914
    (*prefix a skolem term with bindings for the parameters*)
sultana@55596
   915
    (* val contextualise = fold absdummy (map snd params) *)
sultana@55596
   916
    val contextualise = fold absfree params
sultana@55596
   917
wenzelm@59639
   918
    val skolem_cts = map (contextualise #> Thm.cterm_of ctxt) skolem_terms
sultana@55596
   919
sultana@55596
   920
sultana@55596
   921
(*now the instantiation code*)
sultana@55596
   922
sultana@55596
   923
    (*there should only be one Var -- that is from the previous application of drule leo2_skolemise. We look for it at the head position in some equation at a conclusion of a subgoal.*)
sultana@55596
   924
    val var_opt =
sultana@55596
   925
      let
sultana@55596
   926
        val pre_var =
sultana@55596
   927
          gls
sultana@55596
   928
          |> map
sultana@55596
   929
              (strip_top_all_vars [] #> snd #>
sultana@55596
   930
               Logic.strip_horn #> snd #>
sultana@55596
   931
               get_skolem_conc)
sultana@55596
   932
          |> switch (fold (fn x => fn l => if is_some x then the x :: l else l)) []
wenzelm@58411
   933
          |> maps (switch Term.add_vars [])
sultana@55596
   934
sultana@55596
   935
        fun make_var pre_var =
sultana@55596
   936
          the_single pre_var
sultana@55596
   937
          |> Var
wenzelm@59639
   938
          |> Thm.cterm_of ctxt
sultana@55596
   939
          |> SOME
sultana@55596
   940
      in
sultana@55596
   941
        if null pre_var then NONE
sultana@55596
   942
        else make_var pre_var
sultana@55596
   943
     end
sultana@55596
   944
sultana@55596
   945
    fun instantiate_tac from to =
wenzelm@59760
   946
      PRIMITIVE (Thm.instantiate ([], [(from, to)]))
sultana@55596
   947
wenzelm@59760
   948
    val tactic =
sultana@55596
   949
      if is_none var_opt then no_tac
sultana@55596
   950
      else
wenzelm@60642
   951
        fold (curry (op APPEND))
wenzelm@60642
   952
          (map (instantiate_tac (dest_Var (Thm.term_of (the var_opt)))) skolem_cts) no_tac
sultana@55596
   953
  in
wenzelm@59760
   954
    tactic st
sultana@55596
   955
  end
wenzelm@63167
   956
\<close>
sultana@55596
   957
wenzelm@63167
   958
ML \<open>
sultana@55596
   959
fun new_skolem_tac ctxt consts_candidates =
sultana@55596
   960
  let
wenzelm@60754
   961
    fun tac thm =
wenzelm@60754
   962
      dresolve_tac ctxt [thm]
sultana@55596
   963
      THEN' instantiate_skols ctxt consts_candidates
sultana@55596
   964
  in
sultana@55596
   965
    if null consts_candidates then K no_tac
wenzelm@60754
   966
    else FIRST' (map tac @{thms lift_exists})
sultana@55596
   967
  end
wenzelm@63167
   968
\<close>
sultana@55596
   969
sultana@55596
   970
(*
sultana@55596
   971
need a tactic to expand "? x . P" to "~ ! x. ~ P"
sultana@55596
   972
*)
wenzelm@63167
   973
ML \<open>
sultana@55596
   974
fun ex_expander_tac ctxt i =
sultana@55596
   975
   let
sultana@55596
   976
     val simpset =
sultana@55596
   977
       empty_simpset ctxt (*NOTE for some reason, Bind exception gets raised if ctxt's simpset isn't emptied*)
sultana@55596
   978
       |> Simplifier.add_simp @{lemma "Ex P == (~ (! x. ~ P x))" by auto}
sultana@55596
   979
   in
sultana@55596
   980
     CHANGED (asm_full_simp_tac simpset i)
sultana@55596
   981
   end
wenzelm@63167
   982
\<close>
sultana@55596
   983
sultana@55596
   984
sultana@55596
   985
subsubsection "extuni_dec"
sultana@55596
   986
wenzelm@63167
   987
ML \<open>
sultana@55596
   988
(*n-ary decomposition. Code is based on the n-ary arg_cong generator*)
sultana@55596
   989
fun extuni_dec_n ctxt arity =
sultana@55596
   990
  let
sultana@55596
   991
    val _ = @{assert} (arity > 0)
sultana@55596
   992
    val is =
sultana@55596
   993
      upto (1, arity)
sultana@55596
   994
      |> map Int.toString
wenzelm@56252
   995
    val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", @{sort type})) is
wenzelm@56252
   996
    val res_ty = TFree ("res" ^ "_ty", @{sort type})
sultana@55596
   997
    val f_ty = arg_tys ---> res_ty
sultana@55596
   998
    val f = Free ("f", f_ty)
sultana@55596
   999
    val xs = map (fn i =>
wenzelm@56252
  1000
      Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is
sultana@55596
  1001
    (*FIXME DRY principle*)
sultana@55596
  1002
    val ys = map (fn i =>
wenzelm@56252
  1003
      Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is
sultana@55596
  1004
sultana@55596
  1005
    val hyp_lhs = list_comb (f, xs)
sultana@55596
  1006
    val hyp_rhs = list_comb (f, ys)
sultana@55596
  1007
    val hyp_eq =
sultana@55596
  1008
      HOLogic.eq_const res_ty $ hyp_lhs $ hyp_rhs
sultana@55596
  1009
    val hyp =
sultana@55596
  1010
      HOLogic.eq_const HOLogic.boolT $ hyp_eq $ @{term False}
sultana@55596
  1011
      |> HOLogic.mk_Trueprop
sultana@55596
  1012
    fun conc_eq i =
sultana@55596
  1013
      let
wenzelm@56252
  1014
        val ty = TFree ("arg" ^ i ^ "_ty", @{sort type})
sultana@55596
  1015
        val x = Free ("x" ^ i, ty)
sultana@55596
  1016
        val y = Free ("y" ^ i, ty)
sultana@55596
  1017
        val eq = HOLogic.eq_const ty $ x $ y
sultana@55596
  1018
      in
sultana@55596
  1019
        HOLogic.eq_const HOLogic.boolT $ eq $ @{term False}
sultana@55596
  1020
      end
sultana@55596
  1021
sultana@55596
  1022
    val conc_disjs = map conc_eq is
sultana@55596
  1023
sultana@55596
  1024
    val conc =
sultana@55596
  1025
      if length conc_disjs = 1 then
sultana@55596
  1026
        the_single conc_disjs
sultana@55596
  1027
      else
sultana@55596
  1028
        fold
sultana@55596
  1029
         (fn t => fn t_conc => HOLogic.mk_disj (t_conc, t))
sultana@55596
  1030
         (tl conc_disjs) (hd conc_disjs)
sultana@55596
  1031
sultana@55596
  1032
    val t =
sultana@55596
  1033
      Logic.mk_implies (hyp, HOLogic.mk_Trueprop conc)
sultana@55596
  1034
  in
sultana@55596
  1035
    Goal.prove ctxt [] [] t (fn _ => auto_tac ctxt)
sultana@55596
  1036
    |> Drule.export_without_context
sultana@55596
  1037
  end
wenzelm@63167
  1038
\<close>
sultana@55596
  1039
wenzelm@63167
  1040
ML \<open>
sultana@55596
  1041
(*Determine the arity of a function which the "dec"
sultana@55596
  1042
  unification rule is about to be applied.
sultana@55596
  1043
  NOTE:
sultana@55596
  1044
    * Assumes that there is a single hypothesis
sultana@55596
  1045
*)
sultana@55596
  1046
fun find_dec_arity i = fn st =>
sultana@55596
  1047
  let
sultana@55596
  1048
    val gls =
wenzelm@59582
  1049
      Thm.prop_of st
sultana@55596
  1050
      |> Logic.strip_horn
sultana@55596
  1051
      |> fst
sultana@55596
  1052
  in
sultana@55596
  1053
    if null gls then raise NO_GOALS
sultana@55596
  1054
    else
sultana@55596
  1055
      let
sultana@55596
  1056
        val (params, (literal, conc_clause)) =
sultana@55596
  1057
          rpair (i - 1) gls
sultana@55596
  1058
          |> uncurry nth
sultana@55596
  1059
          |> strip_top_all_vars []
sultana@55596
  1060
          |> apsnd Logic.strip_horn
sultana@55596
  1061
          |> apsnd (apfst the_single)
sultana@55596
  1062
sultana@55596
  1063
        val get_ty =
sultana@55596
  1064
          HOLogic.dest_Trueprop
sultana@55596
  1065
          #> strip_top_All_vars
sultana@55596
  1066
          #> snd
sultana@55596
  1067
          #> HOLogic.dest_eq (*polarity's "="*)
sultana@55596
  1068
          #> fst
sultana@55596
  1069
          #> HOLogic.dest_eq (*the unification constraint's "="*)
sultana@55596
  1070
          #> fst
sultana@55596
  1071
          #> head_of
sultana@55596
  1072
          #> dest_Const
sultana@55596
  1073
          #> snd
sultana@55596
  1074
sultana@55596
  1075
       fun arity_of ty =
sultana@55596
  1076
         let
sultana@55596
  1077
           val (_, res_ty) = dest_funT ty
sultana@55596
  1078
sultana@55596
  1079
         in
sultana@55596
  1080
           1 + arity_of res_ty
sultana@55596
  1081
         end
sultana@55596
  1082
         handle (TYPE ("dest_funT", _, _)) => 0
sultana@55596
  1083
sultana@55596
  1084
      in
sultana@55596
  1085
        arity_of (get_ty literal)
sultana@55596
  1086
      end
sultana@55596
  1087
  end
sultana@55596
  1088
sultana@55596
  1089
(*given an inference, it returns the parameters (i.e., we've already matched the leading & shared quantification in the hypothesis & conclusion clauses), and the "raw" inference*)
sultana@55596
  1090
fun breakdown_inference i = fn st =>
sultana@55596
  1091
  let
sultana@55596
  1092
    val gls =
wenzelm@59582
  1093
      Thm.prop_of st
sultana@55596
  1094
      |> Logic.strip_horn
sultana@55596
  1095
      |> fst
sultana@55596
  1096
  in
sultana@55596
  1097
    if null gls then raise NO_GOALS
sultana@55596
  1098
    else
sultana@55596
  1099
      rpair (i - 1) gls
sultana@55596
  1100
      |> uncurry nth
sultana@55596
  1101
      |> strip_top_all_vars []
sultana@55596
  1102
  end
sultana@55596
  1103
sultana@55596
  1104
(*build a custom elimination rule for extuni_dec, and instantiate it to match a specific subgoal*)
sultana@55596
  1105
fun extuni_dec_elim_rule ctxt arity i = fn st =>
sultana@55596
  1106
  let
sultana@55596
  1107
    val rule = extuni_dec_n ctxt arity
sultana@55596
  1108
sultana@55596
  1109
    val rule_hyp =
wenzelm@59582
  1110
      Thm.prop_of rule
sultana@55596
  1111
      |> Logic.dest_implies
sultana@55596
  1112
      |> fst (*assuming that rule has single hypothesis*)
sultana@55596
  1113
sultana@55596
  1114
    (*having run break_hypothesis earlier, we know that the hypothesis
sultana@55596
  1115
      now consists of a single literal. We can (and should)
sultana@55596
  1116
      disregard the conclusion, since it hasn't been "broken",
sultana@55596
  1117
      and it might include some unwanted literals -- the latter
sultana@55596
  1118
      could cause "diff" to fail (since they won't agree with the
sultana@55596
  1119
      rule we have generated.*)
sultana@55596
  1120
sultana@55596
  1121
    val inference_hyp =
sultana@55596
  1122
      snd (breakdown_inference i st)
sultana@55596
  1123
      |> Logic.dest_implies
sultana@55596
  1124
      |> fst (*assuming that inference has single hypothesis,
sultana@55596
  1125
               as explained above.*)
sultana@55596
  1126
  in
sultana@55596
  1127
    TPTP_Reconstruct_Library.diff_and_instantiate ctxt rule rule_hyp inference_hyp
sultana@55596
  1128
  end
sultana@55596
  1129
sultana@55596
  1130
fun extuni_dec_tac ctxt i = fn st =>
sultana@55596
  1131
  let
sultana@55596
  1132
    val arity = find_dec_arity i st
sultana@55596
  1133
sultana@55596
  1134
    fun elim_tac i st =
sultana@55596
  1135
      let
sultana@55596
  1136
        val rule =
sultana@55596
  1137
          extuni_dec_elim_rule ctxt arity i st
sultana@55596
  1138
          (*in case we itroduced free variables during
sultana@55596
  1139
            instantiation, we generalise the rule to make
sultana@55596
  1140
            those free variables into logical variables.*)
sultana@55596
  1141
          |> Thm.forall_intr_frees
sultana@55596
  1142
          |> Drule.export_without_context
wenzelm@60754
  1143
      in dresolve_tac ctxt [rule] i st end
sultana@55596
  1144
      handle NO_GOALS => no_tac st
sultana@55596
  1145
sultana@55596
  1146
    fun closure tac =
sultana@55596
  1147
     (*batter fails if there's no toplevel disjunction in the
sultana@55596
  1148
       hypothesis, so we also try atac*)
wenzelm@59533
  1149
      SOLVE o (tac THEN' (batter_tac ctxt ORELSE' assume_tac ctxt))
sultana@55596
  1150
    val search_tac =
sultana@55596
  1151
      ASAP
wenzelm@60754
  1152
        (resolve_tac ctxt @{thms disjI1} APPEND' resolve_tac ctxt @{thms disjI2})
sultana@55596
  1153
        (FIRST' (map closure
wenzelm@59498
  1154
                  [dresolve_tac ctxt @{thms dec_commut_eq},
wenzelm@60754
  1155
                   dresolve_tac ctxt @{thms dec_commut_disj},
sultana@55596
  1156
                   elim_tac]))
sultana@55596
  1157
  in
sultana@55596
  1158
    (CHANGED o search_tac) i st
sultana@55596
  1159
  end
wenzelm@63167
  1160
\<close>
sultana@55596
  1161
sultana@55596
  1162
sultana@55596
  1163
subsubsection "standard_cnf"
sultana@55596
  1164
(*Given a standard_cnf inference, normalise it
sultana@55596
  1165
     e.g. ((A & B) & C \<longrightarrow> D & E \<longrightarrow> F \<longrightarrow> G) = False
sultana@55596
  1166
     is changed to
sultana@55596
  1167
          (A & B & C & D & E & F \<longrightarrow> G) = False
sultana@55596
  1168
 then custom-build a metatheorem which validates this:
sultana@55596
  1169
          (A & B & C & D & E & F \<longrightarrow> G) = False
sultana@55596
  1170
       -------------------------------------------
sultana@55596
  1171
          (A = True) & (B = True) & (C = True) &
sultana@55596
  1172
          (D = True) & (E = True) & (F = True) & (G = False)
sultana@55596
  1173
 and apply this metatheorem.
sultana@55596
  1174
sultana@55596
  1175
There aren't any "positive" standard_cnfs in Leo2's calculus:
sultana@55596
  1176
  e.g.,  "(A \<longrightarrow> B) = True \<Longrightarrow> A = False | (A = True & B = True)"
sultana@55596
  1177
since "standard_cnf" seems to be applied at the preprocessing
sultana@55596
  1178
stage, together with splitting.
sultana@55596
  1179
*)
sultana@55596
  1180
wenzelm@63167
  1181
ML \<open>
sultana@55596
  1182
(*Conjunctive counterparts to Term.disjuncts_aux and Term.disjuncts*)
sultana@55596
  1183
fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs =
sultana@55596
  1184
     conjuncts_aux t (conjuncts_aux t' conjs)
sultana@55596
  1185
  | conjuncts_aux t conjs = t :: conjs
sultana@55596
  1186
sultana@55596
  1187
fun conjuncts t = conjuncts_aux t []
sultana@55596
  1188
sultana@55596
  1189
(*HOL equivalent of Logic.strip_horn*)
sultana@55596
  1190
local
sultana@55596
  1191
  fun imp_strip_horn' acc (Const (@{const_name HOL.implies}, _) $ A $ B) =
sultana@55596
  1192
        imp_strip_horn' (A :: acc) B
sultana@55596
  1193
    | imp_strip_horn' acc t = (acc, t)
sultana@55596
  1194
in
sultana@55596
  1195
  fun imp_strip_horn t =
sultana@55596
  1196
    imp_strip_horn' [] t
sultana@55596
  1197
    |> apfst rev
sultana@55596
  1198
end
wenzelm@63167
  1199
\<close>
sultana@55596
  1200
wenzelm@63167
  1201
ML \<open>
sultana@55596
  1202
(*Returns whether the antecedents are separated by conjunctions
sultana@55596
  1203
  or implications; the number of antecedents; and the polarity
sultana@55596
  1204
  of the original clause -- I think this will always be "false".*)
sultana@55596
  1205
fun standard_cnf_type ctxt i : thm -> (TPTP_Reconstruct.formula_kind * int * bool) option = fn st =>
sultana@55596
  1206
  let
sultana@55596
  1207
    val gls =
wenzelm@59582
  1208
      Thm.prop_of st
sultana@55596
  1209
      |> Logic.strip_horn
sultana@55596
  1210
      |> fst
sultana@55596
  1211
sultana@55596
  1212
    val hypos =
sultana@55596
  1213
      if null gls then raise NO_GOALS
sultana@55596
  1214
      else
sultana@55596
  1215
        rpair (i - 1) gls
sultana@55596
  1216
        |> uncurry nth
sultana@55596
  1217
        |> TPTP_Reconstruct.strip_top_all_vars []
sultana@55596
  1218
        |> snd
sultana@55596
  1219
        |> Logic.strip_horn
sultana@55596
  1220
        |> fst
sultana@55596
  1221
sultana@55596
  1222
    (*hypothesis clause should be singleton*)
sultana@55596
  1223
    val _ = @{assert} (length hypos = 1)
sultana@55596
  1224
sultana@55596
  1225
    val (t, pol) = the_single hypos
sultana@55596
  1226
      |> try_dest_Trueprop
sultana@55596
  1227
      |> TPTP_Reconstruct.strip_top_All_vars
sultana@55596
  1228
      |> snd
sultana@55596
  1229
      |> TPTP_Reconstruct.remove_polarity true
sultana@55596
  1230
sultana@55596
  1231
    (*literal is negative*)
sultana@55596
  1232
    val _ = @{assert} (not pol)
sultana@55596
  1233
sultana@55596
  1234
    val (antes, conc) = imp_strip_horn t
sultana@55596
  1235
sultana@55596
  1236
    val (ante_type, antes') =
sultana@55596
  1237
      if length antes = 1 then
sultana@55596
  1238
        let
sultana@55596
  1239
          val conjunctive_antes =
sultana@55596
  1240
            the_single antes
sultana@55596
  1241
            |> conjuncts
sultana@55596
  1242
        in
sultana@55596
  1243
          if length conjunctive_antes > 1 then
sultana@55596
  1244
            (TPTP_Reconstruct.Conjunctive NONE,
sultana@55596
  1245
             conjunctive_antes)
sultana@55596
  1246
          else
sultana@55596
  1247
            (TPTP_Reconstruct.Implicational NONE,
sultana@55596
  1248
             antes)
sultana@55596
  1249
        end
sultana@55596
  1250
      else
sultana@55596
  1251
        (TPTP_Reconstruct.Implicational NONE,
sultana@55596
  1252
         antes)
sultana@55596
  1253
  in
sultana@55596
  1254
    if null antes then NONE
sultana@55596
  1255
    else SOME (ante_type, length antes', pol)
sultana@55596
  1256
  end
wenzelm@63167
  1257
\<close>
sultana@55596
  1258
wenzelm@63167
  1259
ML \<open>
sultana@55596
  1260
(*Given a certain standard_cnf type, build a metatheorem that would
sultana@55596
  1261
  validate it*)
sultana@55596
  1262
fun mk_standard_cnf ctxt kind arity =
sultana@55596
  1263
  let
sultana@55596
  1264
    val _ = @{assert} (arity > 0)
sultana@55596
  1265
    val vars =
sultana@55596
  1266
      upto (1, arity + 1)
sultana@55596
  1267
      |> map (fn i => Free ("x" ^ Int.toString i, HOLogic.boolT))
sultana@55596
  1268
sultana@55596
  1269
    val consequent = hd vars
sultana@55596
  1270
    val antecedents = tl vars
sultana@55596
  1271
sultana@55596
  1272
    val conc =
sultana@55596
  1273
      fold
sultana@55596
  1274
       (curry HOLogic.mk_conj)
sultana@55596
  1275
       (map (fn var => HOLogic.mk_eq (var, @{term True})) antecedents)
sultana@55596
  1276
       (HOLogic.mk_eq (consequent, @{term False}))
sultana@55596
  1277
sultana@55596
  1278
    val pre_hyp =
sultana@55596
  1279
      case kind of
sultana@55596
  1280
          TPTP_Reconstruct.Conjunctive NONE =>
sultana@55596
  1281
            curry HOLogic.mk_imp
sultana@55596
  1282
             (if length antecedents = 1 then the_single antecedents
sultana@55596
  1283
              else
sultana@55596
  1284
                fold (curry HOLogic.mk_conj) (tl antecedents) (hd antecedents))
sultana@55596
  1285
             (hd vars)
sultana@55596
  1286
        | TPTP_Reconstruct.Implicational NONE =>
sultana@55596
  1287
            fold (curry HOLogic.mk_imp) antecedents consequent
sultana@55596
  1288
sultana@55596
  1289
    val hyp = HOLogic.mk_eq (pre_hyp, @{term False})
sultana@55596
  1290
sultana@55596
  1291
    val t =
sultana@55596
  1292
      Logic.mk_implies (HOLogic.mk_Trueprop  hyp, HOLogic.mk_Trueprop conc)
sultana@55596
  1293
  in
sultana@55596
  1294
    Goal.prove ctxt [] [] t (fn _ => HEADGOAL (blast_tac ctxt))
sultana@55596
  1295
    |> Drule.export_without_context
sultana@55596
  1296
  end
wenzelm@63167
  1297
\<close>
sultana@55596
  1298
wenzelm@63167
  1299
ML \<open>
sultana@55596
  1300
(*Applies a d-tactic, then breaks it up conjunctively.
sultana@55596
  1301
  This can be used to transform subgoals as follows:
sultana@55596
  1302
     (A \<longrightarrow> B) = False  \<Longrightarrow> R
sultana@55596
  1303
              |
sultana@55596
  1304
              v
sultana@55596
  1305
  \<lbrakk>A = True; B = False\<rbrakk> \<Longrightarrow> R
sultana@55596
  1306
*)
wenzelm@60754
  1307
fun weak_conj_tac ctxt drule =
wenzelm@60754
  1308
  dresolve_tac ctxt [drule] THEN'
wenzelm@60754
  1309
  (REPEAT_DETERM o eresolve_tac ctxt @{thms conjE})
wenzelm@63167
  1310
\<close>
sultana@55596
  1311
wenzelm@63167
  1312
ML \<open>
wenzelm@60754
  1313
fun uncurry_lit_neg_tac ctxt =
wenzelm@60754
  1314
  REPEAT_DETERM o
wenzelm@60754
  1315
    dresolve_tac ctxt [@{lemma "(A \<longrightarrow> B \<longrightarrow> C) = False \<Longrightarrow> (A & B \<longrightarrow> C) = False" by auto}]
wenzelm@63167
  1316
\<close>
sultana@55596
  1317
wenzelm@63167
  1318
ML \<open>
sultana@55596
  1319
fun standard_cnf_tac ctxt i = fn st =>
sultana@55596
  1320
  let
sultana@55596
  1321
    fun core_tactic i = fn st =>
sultana@55596
  1322
      case standard_cnf_type ctxt i st of
sultana@55596
  1323
          NONE => no_tac st
sultana@55596
  1324
        | SOME (kind, arity, _) =>
sultana@55596
  1325
            let
sultana@55596
  1326
              val rule = mk_standard_cnf ctxt kind arity;
sultana@55596
  1327
            in
wenzelm@60754
  1328
              (weak_conj_tac ctxt rule THEN' assume_tac ctxt) i st
sultana@55596
  1329
            end
sultana@55596
  1330
  in
wenzelm@60754
  1331
    (uncurry_lit_neg_tac ctxt
sultana@55596
  1332
     THEN' TPTP_Reconstruct_Library.reassociate_conjs_tac ctxt
sultana@55596
  1333
     THEN' core_tactic) i st
sultana@55596
  1334
  end
wenzelm@63167
  1335
\<close>
sultana@55596
  1336
sultana@55596
  1337
sultana@55596
  1338
subsubsection "Emulator prep"
sultana@55596
  1339
wenzelm@63167
  1340
ML \<open>
sultana@55596
  1341
datatype cleanup_feature =
sultana@55596
  1342
    RemoveHypothesesFromSkolemDefs
sultana@55596
  1343
  | RemoveDuplicates
sultana@55596
  1344
sultana@55596
  1345
datatype loop_feature =
sultana@55596
  1346
    Close_Branch
sultana@55596
  1347
  | ConjI
sultana@55596
  1348
  | King_Cong
sultana@55596
  1349
  | Break_Hypotheses
sultana@55596
  1350
  | Donkey_Cong (*simper_animal + ex_expander_tac*)
sultana@55596
  1351
  | RemoveRedundantQuantifications
sultana@55596
  1352
  | Assumption
sultana@55596
  1353
sultana@55596
  1354
  (*Closely based on Leo2 calculus*)
sultana@55596
  1355
  | Existential_Free
sultana@55596
  1356
  | Existential_Var
sultana@55596
  1357
  | Universal
sultana@55596
  1358
  | Not_pos
sultana@55596
  1359
  | Not_neg
sultana@55596
  1360
  | Or_pos
sultana@55596
  1361
  | Or_neg
sultana@55596
  1362
  | Equal_pos
sultana@55596
  1363
  | Equal_neg
sultana@55596
  1364
  | Extuni_Bool2
sultana@55596
  1365
  | Extuni_Bool1
sultana@55596
  1366
  | Extuni_Dec
sultana@55596
  1367
  | Extuni_Bind
sultana@55596
  1368
  | Extuni_Triv
sultana@55596
  1369
  | Extuni_FlexRigid
sultana@55596
  1370
  | Extuni_Func
sultana@55596
  1371
  | Polarity_switch
sultana@55596
  1372
  | Forall_special_pos
sultana@55596
  1373
sultana@55596
  1374
datatype feature =
sultana@55596
  1375
    ConstsDiff
sultana@55596
  1376
  | StripQuantifiers
sultana@55596
  1377
  | Flip_Conclusion
sultana@55596
  1378
  | Loop of loop_feature list
sultana@55596
  1379
  | LoopOnce of loop_feature list
sultana@55596
  1380
  | InnerLoopOnce of loop_feature list
sultana@55596
  1381
  | CleanUp of cleanup_feature list
sultana@55596
  1382
  | AbsorbSkolemDefs
wenzelm@63167
  1383
\<close>
sultana@55596
  1384
wenzelm@63167
  1385
ML \<open>
sultana@55596
  1386
fun can_feature x l =
sultana@55596
  1387
  let
sultana@55596
  1388
    fun sublist_of_clean_up el =
sultana@55596
  1389
      case el of
sultana@55596
  1390
          CleanUp l'' => SOME l''
sultana@55596
  1391
        | _ => NONE
sultana@55596
  1392
    fun sublist_of_loop el =
sultana@55596
  1393
      case el of
sultana@55596
  1394
          Loop l'' => SOME l''
sultana@55596
  1395
        | _ => NONE
sultana@55596
  1396
    fun sublist_of_loop_once el =
sultana@55596
  1397
      case el of
sultana@55596
  1398
          LoopOnce l'' => SOME l''
sultana@55596
  1399
        | _ => NONE
sultana@55596
  1400
    fun sublist_of_inner_loop_once el =
sultana@55596
  1401
      case el of
sultana@55596
  1402
          InnerLoopOnce l'' => SOME l''
sultana@55596
  1403
        | _ => NONE
sultana@55596
  1404
sultana@55596
  1405
    fun check_sublist sought_sublist opt_list =
wenzelm@58412
  1406
      if forall is_none opt_list then false
sultana@55596
  1407
      else
sultana@55596
  1408
        fold_options opt_list
wenzelm@58411
  1409
        |> flat
sultana@55596
  1410
        |> pair sought_sublist
sultana@55596
  1411
        |> subset (op =)
sultana@55596
  1412
  in
sultana@55596
  1413
    case x of
sultana@55596
  1414
        CleanUp l' =>
sultana@55596
  1415
          map sublist_of_clean_up l
sultana@55596
  1416
          |> check_sublist l'
sultana@55596
  1417
      | Loop l' =>
sultana@55596
  1418
          map sublist_of_loop l
sultana@55596
  1419
          |> check_sublist l'
sultana@55596
  1420
      | LoopOnce l' =>
sultana@55596
  1421
          map sublist_of_loop_once l
sultana@55596
  1422
          |> check_sublist l'
sultana@55596
  1423
      | InnerLoopOnce l' =>
sultana@55596
  1424
          map sublist_of_inner_loop_once l
sultana@55596
  1425
          |> check_sublist l'
wenzelm@58412
  1426
      | _ => exists (curry (op =) x) l
sultana@55596
  1427
  end;
sultana@55596
  1428
sultana@55596
  1429
fun loop_can_feature loop_feats l =
sultana@55596
  1430
  can_feature (Loop loop_feats) l orelse
sultana@55596
  1431
  can_feature (LoopOnce loop_feats) l orelse
sultana@55596
  1432
  can_feature (InnerLoopOnce loop_feats) l;
sultana@55596
  1433
sultana@55596
  1434
@{assert} (can_feature ConstsDiff [StripQuantifiers, ConstsDiff]);
sultana@55596
  1435
sultana@55596
  1436
@{assert}
sultana@55596
  1437
  (can_feature (CleanUp [RemoveHypothesesFromSkolemDefs])
sultana@55596
  1438
    [CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates]]);
sultana@55596
  1439
sultana@55596
  1440
@{assert}
sultana@55596
  1441
  (can_feature (Loop []) [Loop [Existential_Var]]);
sultana@55596
  1442
sultana@55596
  1443
@{assert}
sultana@55596
  1444
  (not (can_feature (Loop []) [InnerLoopOnce [Existential_Var]]));
wenzelm@63167
  1445
\<close>
sultana@55596
  1446
wenzelm@63167
  1447
ML \<open>
sultana@55596
  1448
exception NO_LOOP_FEATS
sultana@55596
  1449
fun get_loop_feats (feats : feature list) =
sultana@55596
  1450
  let
sultana@55596
  1451
    val loop_find =
sultana@55596
  1452
      fold (fn x => fn loop_feats_acc =>
sultana@55596
  1453
        if is_some loop_feats_acc then loop_feats_acc
sultana@55596
  1454
        else
sultana@55596
  1455
          case x of
sultana@55596
  1456
              Loop loop_feats => SOME loop_feats
sultana@55596
  1457
            | LoopOnce loop_feats => SOME loop_feats
sultana@55596
  1458
            | InnerLoopOnce loop_feats => SOME loop_feats
sultana@55596
  1459
            | _ => NONE)
sultana@55596
  1460
       feats
sultana@55596
  1461
       NONE
sultana@55596
  1462
  in
sultana@55596
  1463
    if is_some loop_find then the loop_find
sultana@55596
  1464
    else raise NO_LOOP_FEATS
sultana@55596
  1465
  end;
sultana@55596
  1466
sultana@55596
  1467
@{assert}
sultana@55596
  1468
  (get_loop_feats [Loop [King_Cong, Break_Hypotheses, Existential_Free, Existential_Var, Universal]] =
sultana@55596
  1469
   [King_Cong, Break_Hypotheses, Existential_Free, Existential_Var, Universal])
wenzelm@63167
  1470
\<close>
sultana@55596
  1471
sultana@55596
  1472
(*use as elim rule to remove premises*)
sultana@55596
  1473
lemma insa_prems: "\<lbrakk>Q; P\<rbrakk> \<Longrightarrow> P" by auto
wenzelm@63167
  1474
ML \<open>
wenzelm@60754
  1475
fun cleanup_skolem_defs ctxt feats =
sultana@55596
  1476
  let
sultana@55596
  1477
    (*remove hypotheses from skolem defs,
sultana@55596
  1478
     after testing that they look like skolem defs*)
sultana@55596
  1479
    val dehypothesise_skolem_defs =
sultana@55596
  1480
      COND' (SOME #> TERMPRED (fn _ => true) conc_is_skolem_def)
wenzelm@60754
  1481
        (REPEAT_DETERM o eresolve_tac ctxt @{thms insa_prems})
sultana@55596
  1482
        (K no_tac)
sultana@55596
  1483
  in
sultana@55596
  1484
    if can_feature (CleanUp [RemoveHypothesesFromSkolemDefs]) feats then
sultana@55596
  1485
      ALLGOALS (TRY o dehypothesise_skolem_defs)
sultana@55596
  1486
    else all_tac
sultana@55596
  1487
  end
wenzelm@63167
  1488
\<close>
sultana@55596
  1489
wenzelm@63167
  1490
ML \<open>
sultana@55596
  1491
fun remove_duplicates_tac feats =
sultana@55596
  1492
  (if can_feature (CleanUp [RemoveDuplicates]) feats then
sultana@55596
  1493
     ALLGOALS distinct_subgoal_tac
sultana@55596
  1494
   else all_tac)
wenzelm@63167
  1495
\<close>
sultana@55596
  1496
wenzelm@63167
  1497
ML \<open>
sultana@55596
  1498
(*given a goal state, indicates the skolem constants committed-to in it (i.e. appearing in LHS of a skolem definition)*)
wenzelm@60754
  1499
fun which_skolem_concs_used ctxt = fn st =>
sultana@55596
  1500
  let
sultana@55596
  1501
    val feats = [CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates]]
sultana@55596
  1502
    val scrubup_tac =
wenzelm@60754
  1503
      cleanup_skolem_defs ctxt feats
sultana@55596
  1504
      THEN remove_duplicates_tac feats
sultana@55596
  1505
  in
sultana@55596
  1506
    scrubup_tac st
sultana@55596
  1507
    |> break_seq
sultana@55596
  1508
    |> tap (fn (_, rest) => @{assert} (null (Seq.list_of rest)))
sultana@55596
  1509
    |> fst
sultana@55596
  1510
    |> TERMFUN (snd (*discard hypotheses*)
sultana@55596
  1511
                 #> get_skolem_conc_const) NONE
sultana@55596
  1512
    |> switch (fold (fn x => fn l => if is_some x then the x :: l else l)) []
sultana@55596
  1513
    |> map Const
sultana@55596
  1514
  end
wenzelm@63167
  1515
\<close>
sultana@55596
  1516
wenzelm@63167
  1517
ML \<open>
sultana@55596
  1518
fun exists_tac ctxt feats consts_diff =
sultana@55596
  1519
  let
sultana@55596
  1520
    val ex_var =
sultana@55596
  1521
      if loop_can_feature [Existential_Var] feats andalso consts_diff <> [] then
sultana@55596
  1522
        new_skolem_tac ctxt consts_diff
sultana@55596
  1523
        (*We're making sure that each skolem constant is used once in instantiations.*)
sultana@55596
  1524
      else K no_tac
sultana@55596
  1525
sultana@55596
  1526
    val ex_free =
sultana@55596
  1527
      if loop_can_feature [Existential_Free] feats andalso consts_diff = [] then
wenzelm@59498
  1528
        eresolve_tac ctxt @{thms polar_exE}
sultana@55596
  1529
      else K no_tac
sultana@55596
  1530
  in
sultana@55596
  1531
    ex_var APPEND' ex_free
sultana@55596
  1532
  end
sultana@55596
  1533
sultana@55596
  1534
fun forall_tac ctxt feats =
sultana@55596
  1535
  if loop_can_feature [Universal] feats then
sultana@55596
  1536
    forall_pos_tac ctxt
sultana@55596
  1537
  else K no_tac
wenzelm@63167
  1538
\<close>
sultana@55596
  1539
sultana@55596
  1540
sultana@55596
  1541
subsubsection "Finite types"
sultana@55596
  1542
(*lift quantification from a singleton literal to a singleton clause*)
sultana@55596
  1543
lemma forall_pos_lift:
sultana@55596
  1544
"\<lbrakk>(! X. P X) = True; ! X. (P X = True) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by auto
sultana@55596
  1545
sultana@55596
  1546
(*predicate over the type of the leading quantified variable*)
sultana@55596
  1547
wenzelm@63167
  1548
ML \<open>
wenzelm@60754
  1549
fun extcnf_forall_special_pos_tac ctxt =
sultana@55596
  1550
  let
sultana@55596
  1551
    val bool =
sultana@55596
  1552
      ["True", "False"]
sultana@55596
  1553
sultana@55596
  1554
    val bool_to_bool =
sultana@55596
  1555
      ["% _ . True", "% _ . False", "% x . x", "Not"]
sultana@55596
  1556
wenzelm@60754
  1557
    val tacs =
wenzelm@59763
  1558
      map (fn t_s =>  (* FIXME proper context!? *)
wenzelm@59780
  1559
       Rule_Insts.eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] [] @{thm allE}
wenzelm@60754
  1560
       THEN' assume_tac ctxt)
sultana@55596
  1561
  in
wenzelm@60754
  1562
    (TRY o eresolve_tac ctxt @{thms forall_pos_lift})
wenzelm@60754
  1563
    THEN' (assume_tac ctxt
sultana@55596
  1564
           ORELSE' FIRST'
sultana@55596
  1565
            (*FIXME could check the type of the leading quantified variable, instead of trying everything*)
wenzelm@60754
  1566
            (tacs (bool @ bool_to_bool)))
sultana@55596
  1567
  end
wenzelm@63167
  1568
\<close>
sultana@55596
  1569
sultana@55596
  1570
sultana@55596
  1571
subsubsection "Emulator"
sultana@55596
  1572
sultana@55596
  1573
lemma efq: "[|A = True; A = False|] ==> R" by auto
wenzelm@63167
  1574
ML \<open>
wenzelm@60754
  1575
fun efq_tac ctxt =
wenzelm@60754
  1576
  (eresolve_tac ctxt @{thms efq} THEN' assume_tac ctxt)
wenzelm@60754
  1577
  ORELSE' assume_tac ctxt
wenzelm@63167
  1578
\<close>
sultana@55596
  1579
wenzelm@63167
  1580
ML \<open>
sultana@55596
  1581
(*This is applied to all subgoals, repeatedly*)
sultana@55596
  1582
fun extcnf_combined_main ctxt feats consts_diff =
sultana@55596
  1583
  let
sultana@55596
  1584
    (*This is applied to subgoals which don't have a conclusion
sultana@55596
  1585
      consisting of a Skolem definition*)
sultana@55596
  1586
    fun extcnf_combined_tac' ctxt i = fn st =>
sultana@55596
  1587
      let
wenzelm@60754
  1588
        val skolem_consts_used_so_far = which_skolem_concs_used ctxt st
sultana@55596
  1589
        val consts_diff' = subtract (op =) skolem_consts_used_so_far consts_diff
sultana@55596
  1590
sultana@55596
  1591
        fun feat_to_tac feat =
sultana@55596
  1592
          case feat of
wenzelm@60754
  1593
              Close_Branch => trace_tac' ctxt "mark: closer" (efq_tac ctxt)
wenzelm@60754
  1594
            | ConjI => trace_tac' ctxt "mark: conjI" (resolve_tac ctxt @{thms conjI})
wenzelm@59533
  1595
            | King_Cong => trace_tac' ctxt "mark: expander_animal" (expander_animal ctxt)
wenzelm@59533
  1596
            | Break_Hypotheses => trace_tac' ctxt "mark: break_hypotheses" (break_hypotheses_tac ctxt)
sultana@55596
  1597
            | RemoveRedundantQuantifications => K all_tac
sultana@55596
  1598
(*
sultana@55596
  1599
FIXME Building this into the loop instead.. maybe not the ideal choice
sultana@55596
  1600
            | RemoveRedundantQuantifications =>
wenzelm@59533
  1601
                trace_tac' ctxt "mark: strip_unused_variable_hyp"
sultana@55596
  1602
                 (REPEAT_DETERM o remove_redundant_quantification_in_lit)
sultana@55596
  1603
*)
sultana@55596
  1604
wenzelm@60754
  1605
            | Assumption => assume_tac ctxt
sultana@55596
  1606
(*FIXME both Existential_Free and Existential_Var run same code*)
wenzelm@59533
  1607
            | Existential_Free => trace_tac' ctxt "mark: forall_neg" (exists_tac ctxt feats consts_diff')
wenzelm@59533
  1608
            | Existential_Var => trace_tac' ctxt "mark: forall_neg" (exists_tac ctxt feats consts_diff')
wenzelm@59533
  1609
            | Universal => trace_tac' ctxt "mark: forall_pos" (forall_tac ctxt feats)
wenzelm@60754
  1610
            | Not_pos => trace_tac' ctxt "mark: not_pos" (dresolve_tac ctxt @{thms leo2_rules(9)})
wenzelm@60754
  1611
            | Not_neg => trace_tac' ctxt "mark: not_neg" (dresolve_tac ctxt @{thms leo2_rules(10)})
wenzelm@60754
  1612
            | Or_pos => trace_tac' ctxt "mark: or_pos" (dresolve_tac ctxt @{thms leo2_rules(5)}) (*could add (6) for negated conjunction*)
wenzelm@60754
  1613
            | Or_neg => trace_tac' ctxt "mark: or_neg" (dresolve_tac ctxt @{thms leo2_rules(7)})
wenzelm@59533
  1614
            | Equal_pos => trace_tac' ctxt "mark: equal_pos" (dresolve_tac ctxt (@{thms eq_pos_bool} @ [@{thm leo2_rules(3)}, @{thm eq_pos_func}]))
wenzelm@59533
  1615
            | Equal_neg => trace_tac' ctxt "mark: equal_neg" (dresolve_tac ctxt [@{thm eq_neg_bool}, @{thm leo2_rules(4)}])
wenzelm@59533
  1616
            | Donkey_Cong => trace_tac' ctxt "mark: donkey_cong" (simper_animal ctxt THEN' ex_expander_tac ctxt)
sultana@55596
  1617
wenzelm@60754
  1618
            | Extuni_Bool2 => trace_tac' ctxt "mark: extuni_bool2" (dresolve_tac ctxt @{thms extuni_bool2})
wenzelm@60754
  1619
            | Extuni_Bool1 => trace_tac' ctxt "mark: extuni_bool1" (dresolve_tac ctxt @{thms extuni_bool1})
wenzelm@60754
  1620
            | Extuni_Bind => trace_tac' ctxt "mark: extuni_triv" (eresolve_tac ctxt @{thms extuni_triv})
wenzelm@60754
  1621
            | Extuni_Triv => trace_tac' ctxt "mark: extuni_triv" (eresolve_tac ctxt @{thms extuni_triv})
wenzelm@59533
  1622
            | Extuni_Dec => trace_tac' ctxt "mark: extuni_dec_tac" (extuni_dec_tac ctxt)
wenzelm@60754
  1623
            | Extuni_FlexRigid => trace_tac' ctxt "mark: extuni_flex_rigid" (assume_tac ctxt ORELSE' asm_full_simp_tac ctxt)
wenzelm@60754
  1624
            | Extuni_Func => trace_tac' ctxt "mark: extuni_func" (dresolve_tac ctxt @{thms extuni_func})
wenzelm@59533
  1625
            | Polarity_switch => trace_tac' ctxt "mark: polarity_switch" (eresolve_tac ctxt @{thms polarity_switch})
wenzelm@60754
  1626
            | Forall_special_pos => trace_tac' ctxt "mark: dorall_special_pos" (extcnf_forall_special_pos_tac ctxt)
sultana@55596
  1627
sultana@55596
  1628
        val core_tac =
sultana@55596
  1629
          get_loop_feats feats
sultana@55596
  1630
          |> map feat_to_tac
sultana@55596
  1631
          |> FIRST'
sultana@55596
  1632
      in
sultana@55596
  1633
        core_tac i st
sultana@55596
  1634
      end
sultana@55596
  1635
sultana@55596
  1636
    (*This is applied to all subgoals, repeatedly*)
sultana@55596
  1637
    fun extcnf_combined_tac ctxt i =
sultana@55596
  1638
      COND (TERMPRED (fn _ => true) conc_is_skolem_def (SOME i))
sultana@55596
  1639
        no_tac
sultana@55596
  1640
        (extcnf_combined_tac' ctxt i)
sultana@55596
  1641
sultana@55596
  1642
    val core_tac = CHANGED (ALLGOALS (IF_UNSOLVED o TRY o extcnf_combined_tac ctxt))
sultana@55596
  1643
sultana@55596
  1644
    val full_tac = REPEAT core_tac
sultana@55596
  1645
sultana@55596
  1646
  in
sultana@55596
  1647
    CHANGED
sultana@55596
  1648
      (if can_feature (InnerLoopOnce []) feats then
sultana@55596
  1649
         core_tac
sultana@55596
  1650
       else full_tac)
sultana@55596
  1651
  end
sultana@55596
  1652
sultana@55596
  1653
val interpreted_consts =
sultana@55596
  1654
  [@{const_name HOL.All}, @{const_name HOL.Ex},
sultana@55596
  1655
   @{const_name Hilbert_Choice.Eps},
sultana@55596
  1656
   @{const_name HOL.conj},
sultana@55596
  1657
   @{const_name HOL.disj},
sultana@55596
  1658
   @{const_name HOL.eq},
sultana@55596
  1659
   @{const_name HOL.implies},
sultana@55596
  1660
   @{const_name HOL.The},
sultana@55596
  1661
   @{const_name HOL.Ex1},
sultana@55596
  1662
   @{const_name HOL.Not},
sultana@55596
  1663
   (* @{const_name HOL.iff}, *) (*FIXME do these exist?*)
sultana@55596
  1664
   (* @{const_name HOL.not_equal}, *)
sultana@55596
  1665
   @{const_name HOL.False},
sultana@55596
  1666
   @{const_name HOL.True},
wenzelm@56245
  1667
   @{const_name Pure.imp}]
sultana@55596
  1668
sultana@55596
  1669
fun strip_qtfrs_tac ctxt =
wenzelm@60754
  1670
  REPEAT_DETERM (HEADGOAL (resolve_tac ctxt @{thms allI}))
wenzelm@60754
  1671
  THEN REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt @{thms exE}))
sultana@55596
  1672
  THEN HEADGOAL (canonicalise_qtfr_order ctxt)
sultana@55596
  1673
  THEN
sultana@55596
  1674
    ((REPEAT (HEADGOAL (nominal_inst_parametermatch_tac ctxt @{thm allE})))
sultana@55596
  1675
     APPEND (REPEAT (HEADGOAL (inst_parametermatch_tac ctxt [@{thm allE}]))))
sultana@55596
  1676
  (*FIXME need to handle "@{thm exI}"?*)
sultana@55596
  1677
sultana@55596
  1678
(*difference in constants between the hypothesis clause and the conclusion clause*)
sultana@55596
  1679
fun clause_consts_diff thm =
sultana@55596
  1680
  let
sultana@55596
  1681
    val t =
wenzelm@59582
  1682
      Thm.prop_of thm
sultana@55596
  1683
      |> Logic.dest_implies
sultana@55596
  1684
      |> fst
sultana@55596
  1685
sultana@55596
  1686
      (*This bit should not be needed, since Leo2 inferences don't have parameters*)
sultana@55596
  1687
      |> TPTP_Reconstruct.strip_top_all_vars []
sultana@55596
  1688
      |> snd
sultana@55596
  1689
sultana@55596
  1690
    val do_diff =
sultana@55596
  1691
      Logic.dest_implies
sultana@55596
  1692
      #> uncurry TPTP_Reconstruct.new_consts_between
sultana@55596
  1693
      #> filter
sultana@55596
  1694
           (fn Const (n, _) =>
sultana@55596
  1695
             not (member (op =) interpreted_consts n))
sultana@55596
  1696
  in
sultana@55596
  1697
    if head_of t = Logic.implies then do_diff t
sultana@55596
  1698
    else []
sultana@55596
  1699
  end
wenzelm@63167
  1700
\<close>
sultana@55596
  1701
wenzelm@63167
  1702
ML \<open>
sultana@55596
  1703
(*remove quantification in hypothesis clause (! X. t), if
sultana@55596
  1704
  X not free in t*)
sultana@55596
  1705
fun remove_redundant_quantification ctxt i = fn st =>
sultana@55596
  1706
  let
sultana@55596
  1707
    val gls =
wenzelm@59582
  1708
      Thm.prop_of st
sultana@55596
  1709
      |> Logic.strip_horn
sultana@55596
  1710
      |> fst
sultana@55596
  1711
  in
sultana@55596
  1712
    if null gls then raise NO_GOALS
sultana@55596
  1713
    else
sultana@55596
  1714
      let
sultana@55596
  1715
        val (params, (hyp_clauses, conc_clause)) =
sultana@55596
  1716
          rpair (i - 1) gls
sultana@55596
  1717
          |> uncurry nth
sultana@55596
  1718
          |> TPTP_Reconstruct.strip_top_all_vars []
sultana@55596
  1719
          |> apsnd Logic.strip_horn
sultana@55596
  1720
      in
sultana@55596
  1721
        (*this is to fail gracefully in case this tactic is applied to a goal which doesn't have a single hypothesis*)
sultana@55596
  1722
        if length hyp_clauses > 1 then no_tac st
sultana@55596
  1723
        else
sultana@55596
  1724
          let
sultana@55596
  1725
            val hyp_clause = the_single hyp_clauses
sultana@55596
  1726
            val sep_prefix =
sultana@55596
  1727
              HOLogic.dest_Trueprop
sultana@55596
  1728
              #> TPTP_Reconstruct.strip_top_All_vars
sultana@55596
  1729
              #> apfst rev
sultana@55596
  1730
            val (hyp_prefix, hyp_body) = sep_prefix hyp_clause
sultana@55596
  1731
            val (conc_prefix, conc_body) = sep_prefix conc_clause
sultana@55596
  1732
          in
sultana@55596
  1733
            if null hyp_prefix orelse
sultana@55596
  1734
              member (op =) conc_prefix (hd hyp_prefix) orelse
sultana@55596
  1735
              member (op =)  (Term.add_frees hyp_body []) (hd hyp_prefix) then
sultana@55596
  1736
              no_tac st
sultana@55596
  1737
            else
wenzelm@59780
  1738
              Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")] []
wenzelm@59755
  1739
                @{thm allE} i st
sultana@55596
  1740
          end
sultana@55596
  1741
     end
sultana@55596
  1742
  end
wenzelm@63167
  1743
\<close>
sultana@55596
  1744
wenzelm@63167
  1745
ML \<open>
sultana@55596
  1746
fun remove_redundant_quantification_ignore_skolems ctxt i =
sultana@55596
  1747
  COND (TERMPRED (fn _ => true) conc_is_skolem_def (SOME i))
sultana@55596
  1748
    no_tac
sultana@55596
  1749
    (remove_redundant_quantification ctxt i)
wenzelm@63167
  1750
\<close>
sultana@55596
  1751
sultana@55596
  1752
lemma drop_redundant_literal_qtfr:
sultana@55596
  1753
  "(! X. P) = True \<Longrightarrow> P = True"
sultana@55596
  1754
  "(? X. P) = True \<Longrightarrow> P = True"
sultana@55596
  1755
  "(! X. P) = False \<Longrightarrow> P = False"
sultana@55596
  1756
  "(? X. P) = False \<Longrightarrow> P = False"
sultana@55596
  1757
by auto
sultana@55596
  1758
wenzelm@63167
  1759
ML \<open>
sultana@55596
  1760
(*remove quantification in the literal "(! X. t) = True/False"
sultana@55596
  1761
  in the singleton hypothesis clause, if X not free in t*)
sultana@55596
  1762
fun remove_redundant_quantification_in_lit ctxt i = fn st =>
sultana@55596
  1763
  let
sultana@55596
  1764
    val gls =
wenzelm@59582
  1765
      Thm.prop_of st
sultana@55596
  1766
      |> Logic.strip_horn
sultana@55596
  1767
      |> fst
sultana@55596
  1768
  in
sultana@55596
  1769
    if null gls then raise NO_GOALS
sultana@55596
  1770
    else
sultana@55596
  1771
      let
sultana@55596
  1772
        val (params, (hyp_clauses, conc_clause)) =
sultana@55596
  1773
          rpair (i - 1) gls
sultana@55596
  1774
          |> uncurry nth
sultana@55596
  1775
          |> TPTP_Reconstruct.strip_top_all_vars []
sultana@55596
  1776
          |> apsnd Logic.strip_horn
sultana@55596
  1777
      in
sultana@55596
  1778
        (*this is to fail gracefully in case this tactic is applied to a goal which doesn't have a single hypothesis*)
sultana@55596
  1779
        if length hyp_clauses > 1 then no_tac st
sultana@55596
  1780
        else
sultana@55596
  1781
          let
sultana@55596
  1782
            fun literal_content (Const (@{const_name HOL.eq}, _) $ lhs $ (rhs as @{term True})) = SOME (lhs, rhs)
sultana@55596
  1783
              | literal_content (Const (@{const_name HOL.eq}, _) $ lhs $ (rhs as @{term False})) = SOME (lhs, rhs)
sultana@55596
  1784
              | literal_content t = NONE
sultana@55596
  1785
sultana@55596
  1786
            val hyp_clause =
sultana@55596
  1787
              the_single hyp_clauses
sultana@55596
  1788
              |> HOLogic.dest_Trueprop
sultana@55596
  1789
              |> literal_content
sultana@55596
  1790
sultana@55596
  1791
          in
sultana@55596
  1792
            if is_none hyp_clause then
sultana@55596
  1793
              no_tac st
sultana@55596
  1794
            else
sultana@55596
  1795
              let
sultana@55596
  1796
                val (hyp_lit_prefix, hyp_lit_body) =
sultana@55596
  1797
                  the hyp_clause
sultana@55596
  1798
                  |> (fn (t, polarity) =>
sultana@55596
  1799
                       TPTP_Reconstruct.strip_top_All_vars t
sultana@55596
  1800
                       |> apfst rev)
sultana@55596
  1801
              in
sultana@55596
  1802
                if null hyp_lit_prefix orelse
sultana@55596
  1803
                  member (op =)  (Term.add_frees hyp_lit_body []) (hd hyp_lit_prefix) then
sultana@55596
  1804
                  no_tac st
sultana@55596
  1805
                else
wenzelm@59498
  1806
                  dresolve_tac ctxt @{thms drop_redundant_literal_qtfr} i st
sultana@55596
  1807
              end
sultana@55596
  1808
          end
sultana@55596
  1809
     end
sultana@55596
  1810
  end
wenzelm@63167
  1811
\<close>
sultana@55596
  1812
wenzelm@63167
  1813
ML \<open>
sultana@55596
  1814
fun remove_redundant_quantification_in_lit_ignore_skolems ctxt i =
sultana@55596
  1815
  COND (TERMPRED (fn _ => true) conc_is_skolem_def (SOME i))
sultana@55596
  1816
    no_tac
sultana@55596
  1817
    (remove_redundant_quantification_in_lit ctxt i)
wenzelm@63167
  1818
\<close>
sultana@55596
  1819
wenzelm@63167
  1820
ML \<open>
sultana@55596
  1821
fun extcnf_combined_tac ctxt prob_name_opt feats skolem_consts = fn st =>
sultana@55596
  1822
  let
sultana@55596
  1823
    val thy = Proof_Context.theory_of ctxt
sultana@55596
  1824
sultana@55596
  1825
    (*Initially, st consists of a single goal, showing the
sultana@55596
  1826
      hypothesis clause implying the conclusion clause.
sultana@55596
  1827
      There are no parameters.*)
sultana@55596
  1828
    val consts_diff =
sultana@55596
  1829
      union (op =) skolem_consts
sultana@55596
  1830
       (if can_feature ConstsDiff feats then
sultana@55596
  1831
          clause_consts_diff st
sultana@55596
  1832
        else [])
sultana@55596
  1833
sultana@55596
  1834
    val main_tac =
sultana@55596
  1835
      if can_feature (LoopOnce []) feats orelse can_feature (InnerLoopOnce []) feats then
sultana@55596
  1836
        extcnf_combined_main ctxt feats consts_diff
sultana@55596
  1837
      else if can_feature (Loop []) feats then
sultana@55596
  1838
        BEST_FIRST (TERMPRED (fn _ => true) conc_is_skolem_def NONE, size_of_thm)
sultana@55596
  1839
(*FIXME maybe need to weaken predicate to include "solved form"?*)
sultana@55596
  1840
         (extcnf_combined_main ctxt feats consts_diff)
sultana@55596
  1841
      else all_tac (*to allow us to use the cleaning features*)
sultana@55596
  1842
sultana@55596
  1843
    (*Remove hypotheses from Skolem definitions,
sultana@55596
  1844
      then remove duplicate subgoals,
sultana@55596
  1845
      then we should be left with skolem definitions:
sultana@55596
  1846
        absorb them as axioms into the theory.*)
sultana@55596
  1847
    val cleanup =
wenzelm@60754
  1848
      cleanup_skolem_defs ctxt feats
sultana@55596
  1849
      THEN remove_duplicates_tac feats
sultana@55596
  1850
      THEN (if can_feature AbsorbSkolemDefs feats then
sultana@55596
  1851
              ALLGOALS (absorb_skolem_def ctxt prob_name_opt)
sultana@55596
  1852
            else all_tac)
sultana@55596
  1853
sultana@55596
  1854
    val have_loop_feats =
sultana@55596
  1855
      (get_loop_feats feats; true)
sultana@55596
  1856
      handle NO_LOOP_FEATS => false
sultana@55596
  1857
sultana@55596
  1858
    val tec =
sultana@55596
  1859
      (if can_feature StripQuantifiers feats then
sultana@55596
  1860
         (REPEAT (CHANGED (strip_qtfrs_tac ctxt)))
sultana@55596
  1861
       else all_tac)
sultana@55596
  1862
      THEN (if can_feature Flip_Conclusion feats then
sultana@55596
  1863
             HEADGOAL (flip_conclusion_tac ctxt)
sultana@55596
  1864
           else all_tac)
sultana@55596
  1865
sultana@55596
  1866
      (*after stripping the quantifiers any remaining quantifiers
sultana@55596
  1867
        can be simply eliminated -- they're redundant*)
sultana@55596
  1868
      (*FIXME instead of just using allE, instantiate to a silly
sultana@55596
  1869
         term, to remove opportunities for unification.*)
wenzelm@60754
  1870
      THEN (REPEAT_DETERM (eresolve_tac ctxt @{thms allE} 1))
sultana@55596
  1871
wenzelm@60754
  1872
      THEN (REPEAT_DETERM (resolve_tac ctxt @{thms allI} 1))
sultana@55596
  1873
sultana@55596
  1874
      THEN (if have_loop_feats then
sultana@55596
  1875
              REPEAT (CHANGED
wenzelm@59533
  1876
              ((ALLGOALS (TRY o clause_breaker_tac ctxt)) (*brush away literals which don't change*)
sultana@55596
  1877
               THEN
sultana@55596
  1878
                (*FIXME move this to a different level?*)
sultana@55596
  1879
                (if loop_can_feature [Polarity_switch] feats then
sultana@55596
  1880
                   all_tac
sultana@55596
  1881
                 else
sultana@55596
  1882
                   (TRY (IF_UNSOLVED (HEADGOAL (remove_redundant_quantification_ignore_skolems ctxt))))
sultana@55596
  1883
                   THEN (TRY (IF_UNSOLVED (HEADGOAL (remove_redundant_quantification_in_lit_ignore_skolems ctxt)))))
sultana@55596
  1884
               THEN (TRY main_tac)))
sultana@55596
  1885
            else
sultana@55596
  1886
              all_tac)
sultana@55596
  1887
      THEN IF_UNSOLVED cleanup
sultana@55596
  1888
sultana@55596
  1889
  in
sultana@55596
  1890
    DEPTH_SOLVE (CHANGED tec) st
sultana@55596
  1891
  end
wenzelm@63167
  1892
\<close>
sultana@55596
  1893
sultana@55596
  1894
sultana@55596
  1895
subsubsection "unfold_def"
sultana@55596
  1896
sultana@55596
  1897
(*this is used when handling unfold_tac, because the skeleton includes the definitions conjoined with the goal. it turns out that, for my tactic, the definitions are harmful. instead of modifying the skeleton (which may be nontrivial) i'm just dropping the information using this lemma. obviously, and from the name, order matters here.*)
sultana@55596
  1898
lemma drop_first_hypothesis [rule_format]: "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B" by auto
sultana@55596
  1899
sultana@55596
  1900
(*Unfold_def works by reducing the goal to a meta equation,
sultana@55596
  1901
  then working on it until it can be discharged by atac,
sultana@55596
  1902
  or reflexive, or else turned back into an object equation
sultana@55596
  1903
  and broken down further.*)
sultana@55596
  1904
lemma un_meta_polarise: "(X \<equiv> True) \<Longrightarrow> X" by auto
sultana@55596
  1905
lemma meta_polarise: "X \<Longrightarrow> X \<equiv> True" by auto
sultana@55596
  1906
wenzelm@63167
  1907
ML \<open>
sultana@55596
  1908
fun unfold_def_tac ctxt depends_on_defs = fn st =>
sultana@55596
  1909
  let
sultana@55596
  1910
    (*This is used when we end up with something like
sultana@55596
  1911
        (A & B) \<equiv> True \<Longrightarrow> (B & A) \<equiv> True.
sultana@55596
  1912
      It breaks down this subgoal until it can be trivially
sultana@55596
  1913
      discharged.
sultana@55596
  1914
     *)
sultana@55596
  1915
    val kill_meta_eqs_tac =
wenzelm@60754
  1916
      dresolve_tac ctxt @{thms un_meta_polarise}
wenzelm@60754
  1917
      THEN' resolve_tac ctxt @{thms meta_polarise}
wenzelm@60754
  1918
      THEN' (REPEAT_DETERM o (eresolve_tac ctxt @{thms conjE}))
wenzelm@60754
  1919
      THEN' (REPEAT_DETERM o (resolve_tac ctxt @{thms conjI} ORELSE' assume_tac ctxt))
sultana@55596
  1920
sultana@55596
  1921
    val continue_reducing_tac =
wenzelm@60754
  1922
      resolve_tac ctxt @{thms meta_eq_to_obj_eq} 1
sultana@55596
  1923
      THEN (REPEAT_DETERM (ex_expander_tac ctxt 1))
wenzelm@60754
  1924
      THEN TRY (polarise_subgoal_hyps ctxt 1) (*no need to REPEAT_DETERM here, since there should only be one hypothesis*)
wenzelm@60754
  1925
      THEN TRY (dresolve_tac ctxt @{thms eq_reflection} 1)
sultana@55596
  1926
      THEN (TRY ((CHANGED o rewrite_goal_tac ctxt
sultana@55596
  1927
              (@{thm expand_iff} :: @{thms simp_meta})) 1))
wenzelm@60754
  1928
      THEN HEADGOAL (resolve_tac ctxt @{thms reflexive}
wenzelm@60754
  1929
                     ORELSE' assume_tac ctxt
sultana@55596
  1930
                     ORELSE' kill_meta_eqs_tac)
sultana@55596
  1931
wenzelm@60318
  1932
    val tactic =
wenzelm@60754
  1933
      (resolve_tac ctxt @{thms polarise} 1 THEN assume_tac ctxt 1)
sultana@55596
  1934
      ORELSE
wenzelm@60754
  1935
        (REPEAT_DETERM (eresolve_tac ctxt @{thms conjE} 1 THEN
wenzelm@60754
  1936
          eresolve_tac ctxt @{thms drop_first_hypothesis} 1)
wenzelm@60319
  1937
         THEN PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion)
sultana@55596
  1938
         THEN (REPEAT_DETERM (ex_expander_tac ctxt 1))
sultana@55596
  1939
         THEN (TRY ((CHANGED o rewrite_goal_tac ctxt @{thms simp_meta}) 1))
wenzelm@60319
  1940
         THEN PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion)
sultana@55596
  1941
         THEN
wenzelm@60754
  1942
           (HEADGOAL (assume_tac ctxt)
sultana@55596
  1943
           ORELSE
sultana@55596
  1944
            (unfold_tac ctxt depends_on_defs
sultana@55596
  1945
             THEN IF_UNSOLVED continue_reducing_tac)))
sultana@55596
  1946
  in
wenzelm@60318
  1947
    tactic st
sultana@55596
  1948
  end
wenzelm@63167
  1949
\<close>
sultana@55596
  1950
sultana@55596
  1951
sultana@55596
  1952
subsection "Handling split 'preprocessing'"
sultana@55596
  1953
sultana@55596
  1954
lemma split_tranfs:
sultana@55596
  1955
  "! x. P x & Q x \<equiv> (! x. P x) & (! x. Q x)"
sultana@55596
  1956
  "~ (~ A) \<equiv> A"
sultana@55596
  1957
  "? x. A \<equiv> A"
sultana@55596
  1958
  "(A & B) & C \<equiv> A & B & C"
sultana@55596
  1959
  "A = B \<equiv> (A --> B) & (B --> A)"
sultana@55596
  1960
by (rule eq_reflection, auto)+
sultana@55596
  1961
sultana@55596
  1962
(*Same idiom as ex_expander_tac*)
wenzelm@63167
  1963
ML \<open>
sultana@55596
  1964
fun split_simp_tac (ctxt : Proof.context) i =
sultana@55596
  1965
   let
sultana@55596
  1966
     val simpset =
sultana@55596
  1967
       fold Simplifier.add_simp @{thms split_tranfs} (empty_simpset ctxt)
sultana@55596
  1968
   in
sultana@55596
  1969
     CHANGED (asm_full_simp_tac simpset i)
sultana@55596
  1970
   end
wenzelm@63167
  1971
\<close>
sultana@55596
  1972
sultana@55596
  1973
sultana@55596
  1974
subsection "Alternative reconstruction tactics"
wenzelm@63167
  1975
ML \<open>
sultana@55596
  1976
(*An "auto"-based proof reconstruction, where we attempt to reconstruct each inference
sultana@55596
  1977
  using auto_tac. A realistic tactic would inspect the inference name and act
sultana@55596
  1978
  accordingly.*)
sultana@55596
  1979
fun auto_based_reconstruction_tac ctxt prob_name n =
sultana@55596
  1980
  let
sultana@55596
  1981
    val thy = Proof_Context.theory_of ctxt
sultana@55596
  1982
    val pannot = TPTP_Reconstruct.get_pannot_of_prob thy prob_name
sultana@55596
  1983
  in
sultana@55596
  1984
    TPTP_Reconstruct.inference_at_node
sultana@55596
  1985
     thy
sultana@55596
  1986
     prob_name (#meta pannot) n
sultana@55596
  1987
      |> the
sultana@55596
  1988
      |> (fn {inference_fmla, ...} =>
sultana@55596
  1989
          Goal.prove ctxt [] [] inference_fmla
sultana@55596
  1990
           (fn pdata => auto_tac (#context pdata)))
sultana@55596
  1991
  end
wenzelm@63167
  1992
\<close>
sultana@55596
  1993
sultana@55596
  1994
(*An oracle-based reconstruction, which is only used to test the shunting part of the system*)
sultana@55596
  1995
oracle oracle_iinterp = "fn t => t"
wenzelm@63167
  1996
ML \<open>
sultana@55596
  1997
fun oracle_based_reconstruction_tac ctxt prob_name n =
sultana@55596
  1998
  let
sultana@55596
  1999
    val thy = Proof_Context.theory_of ctxt
sultana@55596
  2000
    val pannot = TPTP_Reconstruct.get_pannot_of_prob thy prob_name
sultana@55596
  2001
  in
sultana@55596
  2002
    TPTP_Reconstruct.inference_at_node
sultana@55596
  2003
     thy
sultana@55596
  2004
     prob_name (#meta pannot) n
sultana@55596
  2005
      |> the
wenzelm@59639
  2006
      |> (fn {inference_fmla, ...} => Thm.cterm_of ctxt inference_fmla)
sultana@55596
  2007
      |> oracle_iinterp
sultana@55596
  2008
  end
wenzelm@63167
  2009
\<close>
sultana@55596
  2010
sultana@55596
  2011
sultana@55596
  2012
subsection "Leo2 reconstruction tactic"
sultana@55596
  2013
wenzelm@63167
  2014
ML \<open>
sultana@55596
  2015
exception UNSUPPORTED_ROLE
sultana@55596
  2016
exception INTERPRET_INFERENCE
sultana@55596
  2017
sultana@55596
  2018
(*Failure reports can be adjusted to avoid interrupting
sultana@55596
  2019
  an overall reconstruction process*)
sultana@55596
  2020
fun fail ctxt x =
sultana@55596
  2021
  if unexceptional_reconstruction ctxt then
sultana@55596
  2022
    (warning x; raise INTERPRET_INFERENCE)
sultana@55596
  2023
  else error x
sultana@55596
  2024
sultana@55596
  2025
fun interpret_leo2_inference_tac ctxt prob_name node =
sultana@55596
  2026
  let
sultana@55596
  2027
    val thy = Proof_Context.theory_of ctxt
sultana@55596
  2028
sultana@55596
  2029
    val _ =
sultana@55596
  2030
      if Config.get ctxt tptp_trace_reconstruction then
sultana@55596
  2031
        tracing ("interpret_inference reconstructing node" ^ node ^ " of " ^ TPTP_Problem_Name.mangle_problem_name prob_name)
sultana@55596
  2032
      else ()
sultana@55596
  2033
sultana@55596
  2034
    val pannot = TPTP_Reconstruct.get_pannot_of_prob thy prob_name
sultana@55596
  2035
sultana@55596
  2036
    fun nonfull_extcnf_combined_tac feats =
sultana@55596
  2037
      extcnf_combined_tac ctxt (SOME prob_name)
sultana@55596
  2038
       [ConstsDiff,
sultana@55596
  2039
        StripQuantifiers,
sultana@55596
  2040
        InnerLoopOnce (Break_Hypotheses :: (*FIXME RemoveRedundantQuantifications :: *) feats),
sultana@55596
  2041
        AbsorbSkolemDefs]
sultana@55596
  2042
       []
sultana@55596
  2043
sultana@55596
  2044
    val source_inf_opt =
sultana@55596
  2045
      AList.lookup (op =) (#meta pannot)
sultana@55596
  2046
      #> the
sultana@55596
  2047
      #> #source_inf_opt
sultana@55596
  2048
sultana@55596
  2049
    (*FIXME integrate this with other lookup code, or in the early analysis*)
sultana@55596
  2050
    local
sultana@55596
  2051
      fun node_is_of_role role node =
sultana@55596
  2052
        AList.lookup (op =) (#meta pannot) node |> the
sultana@55596
  2053
        |> #role
sultana@55596
  2054
        |> (fn role' => role = role')
sultana@55596
  2055
sultana@55596
  2056
      fun roled_dependencies_names role =
sultana@55596
  2057
        let
sultana@55596
  2058
          fun values () =
sultana@55596
  2059
            case role of
sultana@55596
  2060
                TPTP_Syntax.Role_Definition =>
wenzelm@59858
  2061
                  map (apsnd Binding.name_of) (#defs pannot)
sultana@55596
  2062
              | TPTP_Syntax.Role_Axiom =>
wenzelm@59858
  2063
                  map (apsnd Binding.name_of) (#axs pannot)
sultana@55596
  2064
              | _ => raise UNSUPPORTED_ROLE
sultana@55596
  2065
          in
sultana@55596
  2066
            if is_none (source_inf_opt node) then []
sultana@55596
  2067
            else
sultana@55596
  2068
              case the (source_inf_opt node) of
sultana@55596
  2069
                  TPTP_Proof.Inference (_, _, parent_inf) =>
wenzelm@58412
  2070
                    map TPTP_Proof.parent_name parent_inf
wenzelm@58412
  2071
                    |> filter (node_is_of_role role)
sultana@55596
  2072
                    |> (*FIXME currently definitions are not
sultana@55596
  2073
                         included in the proof annotations, so
sultana@55596
  2074
                         i'm using all the definitions available
sultana@55596
  2075
                         in the proof. ideally i should only
sultana@55596
  2076
                         use the ones in the proof annotation.*)
sultana@55596
  2077
                       (fn x =>
sultana@55596
  2078
                         if role = TPTP_Syntax.Role_Definition then
wenzelm@59858
  2079
                           let fun values () = map (apsnd Binding.name_of) (#defs pannot)
sultana@55596
  2080
                           in
sultana@55596
  2081
                             map snd (values ())
sultana@55596
  2082
                           end
sultana@55596
  2083
                         else
sultana@55596
  2084
                         map (fn node => AList.lookup (op =) (values ()) node |> the) x)
sultana@55596
  2085
                | _ => []
sultana@55596
  2086
         end
sultana@55596
  2087
sultana@55596
  2088
      val roled_dependencies =
sultana@55596
  2089
        roled_dependencies_names
wenzelm@59858
  2090
        #> map (Global_Theory.get_thm thy)
sultana@55596
  2091
    in
sultana@55596
  2092
      val depends_on_defs = roled_dependencies TPTP_Syntax.Role_Definition
sultana@55596
  2093
      val depends_on_axs = roled_dependencies TPTP_Syntax.Role_Axiom
sultana@55596
  2094
      val depends_on_defs_names = roled_dependencies_names TPTP_Syntax.Role_Definition
sultana@55596
  2095
    end
sultana@55596
  2096
sultana@55596
  2097
    fun get_binds source_inf_opt =
sultana@55596
  2098
      case the source_inf_opt of
sultana@55596
  2099
          TPTP_Proof.Inference (_, _, parent_inf) =>
wenzelm@58411
  2100
            maps
sultana@55596
  2101
              (fn TPTP_Proof.Parent _ => []
sultana@55596
  2102
                | TPTP_Proof.ParentWithDetails (_, parent_details) => parent_details)
sultana@55596
  2103
              parent_inf
sultana@55596
  2104
        | _ => []
sultana@55596
  2105
sultana@55596
  2106
    val inference_name =
sultana@55596
  2107
      case TPTP_Reconstruct.inference_at_node thy prob_name (#meta pannot) node of
sultana@55596
  2108
          NONE => fail ctxt "Cannot reconstruct rule: no information"
sultana@55596
  2109
        | SOME {inference_name, ...} => inference_name
sultana@55596
  2110
    val default_tac = HEADGOAL (blast_tac ctxt)
sultana@55596
  2111
  in
sultana@55596
  2112
    case inference_name of
sultana@55596
  2113
      "fo_atp_e" =>
sultana@57773
  2114
        HEADGOAL (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt [])
sultana@57773
  2115
        (*NOTE To treat E as an oracle use the following line:
sultana@55596
  2116
        HEADGOAL (etac (oracle_based_reconstruction_tac ctxt prob_name node))
sultana@57773
  2117
        *)
sultana@55596
  2118
    | "copy" =>
sultana@55596
  2119
         HEADGOAL
wenzelm@60754
  2120
          (assume_tac ctxt
sultana@55596
  2121
           ORELSE'
wenzelm@60754
  2122
              (resolve_tac ctxt @{thms polarise}
wenzelm@60754
  2123
               THEN' assume_tac ctxt))
sultana@55596
  2124
    | "polarity_switch" => nonfull_extcnf_combined_tac [Polarity_switch]
wenzelm@60754
  2125
    | "solved_all_splits" => solved_all_splits_tac ctxt
sultana@55596
  2126
    | "extcnf_not_pos" => nonfull_extcnf_combined_tac [Not_pos]
sultana@55596
  2127
    | "extcnf_forall_pos" => nonfull_extcnf_combined_tac [Universal]
sultana@55596
  2128
    | "negate_conjecture" => fail ctxt "Should not handle negate_conjecture here"
sultana@55596
  2129
    | "unfold_def" => unfold_def_tac ctxt depends_on_defs
sultana@55596
  2130
    | "extcnf_not_neg" => nonfull_extcnf_combined_tac [Not_neg]
sultana@55596
  2131
    | "extcnf_or_neg" => nonfull_extcnf_combined_tac [Or_neg]
sultana@55596
  2132
    | "extcnf_equal_pos" => nonfull_extcnf_combined_tac [Equal_pos]
sultana@55596
  2133
    | "extcnf_equal_neg" => nonfull_extcnf_combined_tac [Equal_neg]
sultana@55596
  2134
    | "extcnf_forall_special_pos" =>
sultana@55596
  2135
         nonfull_extcnf_combined_tac [Forall_special_pos]
sultana@55596
  2136
         ORELSE HEADGOAL (blast_tac ctxt)
sultana@55596
  2137
    | "extcnf_or_pos" => nonfull_extcnf_combined_tac [Or_pos]
sultana@55596
  2138
    | "extuni_bool2" => nonfull_extcnf_combined_tac [Extuni_Bool2]
sultana@55596
  2139
    | "extuni_bool1" => nonfull_extcnf_combined_tac [Extuni_Bool1]
sultana@55596
  2140
    | "extuni_dec" =>
wenzelm@60754
  2141
        HEADGOAL (assume_tac ctxt)
sultana@55596
  2142
        ORELSE nonfull_extcnf_combined_tac [Extuni_Dec]
sultana@55596
  2143
    | "extuni_bind" => nonfull_extcnf_combined_tac [Extuni_Bind]
sultana@55596
  2144
    | "extuni_triv" => nonfull_extcnf_combined_tac [Extuni_Triv]
sultana@55596
  2145
    | "extuni_flex_rigid" => nonfull_extcnf_combined_tac [Extuni_FlexRigid]
sultana@55596
  2146
    | "prim_subst" => nonfull_extcnf_combined_tac [Assumption]
sultana@55596
  2147
    | "bind" =>
sultana@55596
  2148
        let
sultana@55596
  2149
          val ordered_binds = get_binds (source_inf_opt node)
sultana@55596
  2150
        in
sultana@55596
  2151
          bind_tac ctxt prob_name ordered_binds
sultana@55596
  2152
        end
sultana@55596
  2153
    | "standard_cnf" => HEADGOAL (standard_cnf_tac ctxt)
sultana@55596
  2154
    | "extcnf_forall_neg" =>
sultana@55596
  2155
        nonfull_extcnf_combined_tac
sultana@55596
  2156
         [Existential_Var(* , RemoveRedundantQuantifications *)] (*FIXME RemoveRedundantQuantifications*)
sultana@55596
  2157
    | "extuni_func" =>
sultana@55596
  2158
        nonfull_extcnf_combined_tac [Extuni_Func, Existential_Var]
sultana@55596
  2159
    | "replace_leibnizEQ" => nonfull_extcnf_combined_tac [Assumption]
sultana@55596
  2160
    | "replace_andrewsEQ" => nonfull_extcnf_combined_tac [Assumption]
sultana@55596
  2161
    | "split_preprocessing" =>
sultana@55596
  2162
         (REPEAT (HEADGOAL (split_simp_tac ctxt)))
wenzelm@60319
  2163
         THEN TRY (PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion))
wenzelm@60754
  2164
         THEN HEADGOAL (assume_tac ctxt)
sultana@55596
  2165
sultana@55596
  2166
    (*FIXME some of these could eventually be handled specially*)
sultana@55596
  2167
    | "fac_restr" => default_tac
sultana@55596
  2168
    | "sim" => default_tac
sultana@55596
  2169
    | "res" => default_tac
sultana@55596
  2170
    | "rename" => default_tac
sultana@55596
  2171
    | "flexflex" => default_tac
sultana@55596
  2172
    | other => fail ctxt ("Unknown inference rule: " ^ other)
sultana@55596
  2173
  end
wenzelm@63167
  2174
\<close>
sultana@55596
  2175
wenzelm@63167
  2176
ML \<open>
sultana@55596
  2177
fun interpret_leo2_inference ctxt prob_name node =
sultana@55596
  2178
  let
sultana@55596
  2179
    val thy = Proof_Context.theory_of ctxt
sultana@55596
  2180
    val pannot = TPTP_Reconstruct.get_pannot_of_prob thy prob_name
sultana@55596
  2181
sultana@55596
  2182
    val (inference_name, inference_fmla) =
sultana@55596
  2183
      case TPTP_Reconstruct.inference_at_node thy prob_name (#meta pannot) node of
sultana@55596
  2184
          NONE => fail ctxt "Cannot reconstruct rule: no information"
sultana@55596
  2185
        | SOME {inference_name, inference_fmla, ...} =>
sultana@55596
  2186
            (inference_name, inference_fmla)
sultana@55596
  2187
sultana@55596
  2188
    val proof_outcome =
sultana@55596
  2189
      let
sultana@55596
  2190
        fun prove () =
sultana@55596
  2191
          Goal.prove ctxt [] [] inference_fmla
sultana@55596
  2192
           (fn pdata => interpret_leo2_inference_tac
sultana@55596
  2193
            (#context pdata) prob_name node)
sultana@55596
  2194
      in
sultana@55596
  2195
        if informative_failure ctxt then SOME (prove ())
sultana@55596
  2196
        else try prove ()
sultana@55596
  2197
      end
sultana@55596
  2198
sultana@55596
  2199
  in case proof_outcome of
sultana@55596
  2200
      NONE => fail ctxt (Pretty.string_of
sultana@55596
  2201
        (Pretty.block
sultana@55596
  2202
          [Pretty.str ("Failed inference reconstruction for '" ^
sultana@55596
  2203
            inference_name ^ "' at node " ^ node ^ ":\n"),
sultana@55596
  2204
           Syntax.pretty_term ctxt inference_fmla]))
sultana@55596
  2205
    | SOME thm => thm
sultana@55596
  2206
  end
wenzelm@63167
  2207
\<close>
sultana@55596
  2208
wenzelm@63167
  2209
ML \<open>
sultana@55596
  2210
(*filter a set of nodes based on which inference rule was used to
sultana@55596
  2211
  derive a node*)
sultana@55596
  2212
fun nodes_by_inference (fms : TPTP_Reconstruct.formula_meaning list) inference_rule =
sultana@55596
  2213
  let
sultana@55596
  2214
    fun fold_fun n l =
sultana@55596
  2215
      case TPTP_Reconstruct.node_info fms #source_inf_opt n of
sultana@55596
  2216
          NONE => l
sultana@55596
  2217
        | SOME (TPTP_Proof.File _) => l
sultana@55596
  2218
        | SOME (TPTP_Proof.Inference (rule_name, _, _)) =>
sultana@55596
  2219
            if rule_name = inference_rule then n :: l
sultana@55596
  2220
            else l
sultana@55596
  2221
  in
sultana@55596
  2222
    fold fold_fun (map fst fms) []
sultana@55596
  2223
  end
wenzelm@63167
  2224
\<close>
sultana@55596
  2225
sultana@55597
  2226
sultana@55597
  2227
section "Importing proofs and reconstructing theorems"
sultana@55597
  2228
wenzelm@63167
  2229
ML \<open>
sultana@55597
  2230
(*Preprocessing carried out on a LEO-II proof.*)
sultana@55596
  2231
fun leo2_on_load (pannot : TPTP_Reconstruct.proof_annotation) thy =
sultana@55596
  2232
  let
sultana@55596
  2233
    val ctxt = Proof_Context.init_global thy
sultana@55596
  2234
    val dud = ("", Binding.empty, @{term False})
sultana@55596
  2235
    val pre_skolem_defs =
sultana@55596
  2236
      nodes_by_inference (#meta pannot) "extcnf_forall_neg" @
sultana@55596
  2237
       nodes_by_inference (#meta pannot) "extuni_func"
sultana@55596
  2238
      |> map (fn x =>
sultana@55596
  2239
              (interpret_leo2_inference ctxt (#problem_name pannot) x; dud)
sultana@55596
  2240
               handle NO_SKOLEM_DEF (s, bnd, t) => (s, bnd, t))
sultana@55596
  2241
      |> filter (fn (x, _, _) => x <> "") (*In case no skolem constants were introduced in that inference*)
sultana@55596
  2242
    val skolem_defs = map (fn (x, y, _) => (x, y)) pre_skolem_defs
sultana@55596
  2243
    val thy' =
sultana@55596
  2244
      fold (fn skolem_def => fn thy =>
sultana@55596
  2245
             let
sultana@55596
  2246
               val ((s, thm), thy') = Thm.add_axiom_global skolem_def thy
sultana@55596
  2247
               (* val _ = warning ("Added skolem definition " ^ s ^ ": " ^  @{make_string thm}) *) (*FIXME use of make_string*)
sultana@55596
  2248
             in thy' end)
sultana@55596
  2249
       (map (fn (_, y, z) => (y, z)) pre_skolem_defs)
sultana@55596
  2250
       thy
sultana@55596
  2251
  in
sultana@55596
  2252
    ({problem_name = #problem_name pannot,
sultana@55596
  2253
      skolem_defs = skolem_defs,
sultana@55596
  2254
      defs = #defs pannot,
sultana@55596
  2255
      axs = #axs pannot,
sultana@55596
  2256
      meta = #meta pannot},
sultana@55596
  2257
     thy')
sultana@55596
  2258
  end
wenzelm@63167
  2259
\<close>
sultana@55596
  2260
wenzelm@63167
  2261
ML \<open>
sultana@55597
  2262
(*Imports and reconstructs a LEO-II proof.*)
sultana@55597
  2263
fun reconstruct_leo2 path thy =
sultana@55597
  2264
  let
sultana@55597
  2265
    val prob_file = Path.base path
sultana@55597
  2266
    val dir = Path.dir path
sultana@55597
  2267
    val thy' = TPTP_Reconstruct.import_thm true [dir, prob_file] path leo2_on_load thy
sultana@55597
  2268
    val ctxt =
sultana@55597
  2269
      Context.Theory thy'
sultana@55597
  2270
      |> Context.proof_of
sultana@55597
  2271
    val prob_name =
sultana@55597
  2272
      Path.implode prob_file
sultana@55597
  2273
      |> TPTP_Problem_Name.parse_problem_name
sultana@55597
  2274
    val theorem =
sultana@55597
  2275
      TPTP_Reconstruct.reconstruct ctxt
sultana@55597
  2276
       (TPTP_Reconstruct.naive_reconstruct_tac ctxt interpret_leo2_inference)
sultana@55597
  2277
       prob_name
sultana@55597
  2278
  in
sultana@55597
  2279
    (*NOTE we could return the theorem value alone, since
sultana@55597
  2280
       users could get the thy value from the thm value.*)
sultana@55597
  2281
    (thy', theorem)
sultana@55597
  2282
  end
wenzelm@63167
  2283
\<close>
sultana@55597
  2284
sultana@57773
  2285
end