src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
author wenzelm
Fri Mar 21 20:33:56 2014 +0100 (2014-03-21)
changeset 56245 84fc7dfa3cd4
parent 56220 4c43a2881b25
child 56252 b72e0a9d62b9
permissions -rw-r--r--
more qualified names;
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
sultana@55596
    55
ML {*
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
sultana@55596
    70
*}
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"
sultana@55596
    90
text {*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.
sultana@55596
   147
*}
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
sultana@55596
   162
ML {*
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 =
sultana@55596
   171
      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 =
sultana@55596
   188
           (map (eres_inst_tac ctxt [(("x", 0), 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}
sultana@55596
   198
*}
sultana@55596
   199
sultana@55596
   200
ML {*
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 =
sultana@55596
   207
      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 =
sultana@55596
   224
           eres_inst_tac ctxt [(("x", 0), param)] thm
sultana@55596
   225
sultana@55596
   226
        val quantified_var = head_quantified_variable 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
sultana@55596
   236
*}
sultana@55596
   237
sultana@55596
   238
sultana@55596
   239
subsection "Prefix massaging"
sultana@55596
   240
sultana@55596
   241
ML {*
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 =
sultana@55596
   250
      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 _ =>
sultana@55596
   285
              (REPEAT_DETERM (HEADGOAL (rtac @{thm allI})))
sultana@55596
   286
              THEN (REPEAT_DETERM
sultana@55596
   287
                    (HEADGOAL
sultana@55596
   288
                     (nominal_inst_parametermatch_tac ctxt @{thm allE})))
sultana@55596
   289
              THEN HEADGOAL atac)
sultana@55596
   290
      in
sultana@55596
   291
        dtac thm i st
sultana@55596
   292
      end
sultana@55596
   293
    end
sultana@55596
   294
*}
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
sultana@55596
   303
ML {*
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
sultana@55596
   308
val polarise_subgoal_hyps =
sultana@55596
   309
  COND' (SOME #> TERMPRED is_polarised (fn _ => true)) (K no_tac) (dtac @{thm polarise})
sultana@55596
   310
*}
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
sultana@55596
   338
ML {*
sultana@55596
   339
val solved_all_splits_tac =
sultana@55596
   340
  TRY (etac @{thm conjE} 1)
sultana@55596
   341
  THEN rtac @{thm solved_all_splits} 1
sultana@55596
   342
  THEN atac 1
sultana@55596
   343
*}
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
sultana@55596
   411
ML {*
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
sultana@55596
   430
             [(("x", 0), 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
sultana@55596
   436
      THEN (HEADGOAL atac)
sultana@55596
   437
  in
sultana@55596
   438
    HEADGOAL (canonicalise_qtfr_order ctxt)
sultana@55596
   439
    THEN (REPEAT_DETERM (HEADGOAL (rtac @{thm 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
sultana@55596
   444
*}
sultana@55596
   445
sultana@55596
   446
ML {*
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
sultana@55596
   459
*}
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
sultana@55596
   467
ML {*
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}))
sultana@55596
   473
      THEN' rtac @{thm notI}
sultana@55596
   474
      THEN' (REPEAT_DETERM o etac @{thm conjE})
sultana@55596
   475
      THEN' (TRY o (expander_animal ctxt))
sultana@55596
   476
  in
sultana@55596
   477
    default_tac ORELSE' resolve_tac @{thms flip}
sultana@55596
   478
  end
sultana@55596
   479
*}
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
sultana@55596
   544
ML {*
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
sultana@55596
   577
*}
sultana@55596
   578
sultana@55596
   579
ML {*
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
sultana@55596
   613
*}
sultana@55596
   614
sultana@55596
   615
ML {*
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)
sultana@55596
   636
*}
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
sultana@55596
   646
ML {*
sultana@55596
   647
fun forall_neg_tac candidate_consts ctxt i = fn st =>
sultana@55596
   648
  let
sultana@55596
   649
    val thy = Proof_Context.theory_of ctxt
sultana@55596
   650
sultana@55596
   651
    val gls =
sultana@55596
   652
      prop_of st
sultana@55596
   653
      |> Logic.strip_horn
sultana@55596
   654
      |> fst
sultana@55596
   655
sultana@55596
   656
    val parameters =
sultana@55596
   657
      if null gls then ""
sultana@55596
   658
      else
sultana@55596
   659
        rpair (i - 1) gls
sultana@55596
   660
        |> uncurry nth
sultana@55596
   661
        |> strip_top_all_vars []
sultana@55596
   662
        |> fst
sultana@55596
   663
        |> map fst (*just get the parameter names*)
sultana@55596
   664
        |> (fn l =>
sultana@55596
   665
              if null l then ""
sultana@55596
   666
              else
sultana@55596
   667
                space_implode " " l
sultana@55596
   668
                |> pair " "
sultana@55596
   669
                |> op ^)
sultana@55596
   670
sultana@55596
   671
  in
sultana@55596
   672
    if null gls orelse null candidate_consts then no_tac st
sultana@55596
   673
    else
sultana@55596
   674
      let
sultana@55596
   675
        fun instantiate const_name =
sultana@55596
   676
          dres_inst_tac ctxt [(("sk", 0), const_name ^ parameters)] @{thm leo2_skolemise}
sultana@55596
   677
        val attempts = map instantiate candidate_consts
sultana@55596
   678
      in
sultana@55596
   679
        (fold (curry (op APPEND')) attempts (K no_tac)) i st
sultana@55596
   680
      end
sultana@55596
   681
  end
sultana@55596
   682
*}
sultana@55596
   683
sultana@55596
   684
ML {*
sultana@55596
   685
exception SKOLEM_DEF of term (*The tactic wasn't pointed at a skolem definition*)
sultana@55596
   686
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
   687
fun absorb_skolem_def ctxt prob_name_opt i = fn st =>
sultana@55596
   688
  let
sultana@55596
   689
    val thy = Proof_Context.theory_of ctxt
sultana@55596
   690
sultana@55596
   691
    val gls =
sultana@55596
   692
      prop_of st
sultana@55596
   693
      |> Logic.strip_horn
sultana@55596
   694
      |> fst
sultana@55596
   695
sultana@55596
   696
    val conclusion =
sultana@55596
   697
      if null gls then
sultana@55596
   698
        (*this should never be thrown*)
sultana@55596
   699
        raise NO_GOALS
sultana@55596
   700
      else
sultana@55596
   701
        rpair (i - 1) gls
sultana@55596
   702
        |> uncurry nth
sultana@55596
   703
        |> strip_top_all_vars []
sultana@55596
   704
        |> snd
sultana@55596
   705
        |> Logic.strip_horn
sultana@55596
   706
        |> snd
sultana@55596
   707
sultana@55596
   708
    fun skolem_const_info_of t =
sultana@55596
   709
      case t of
sultana@55596
   710
          Const (@{const_name HOL.Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t' $ (Const (@{const_name Hilbert_Choice.Eps}, _) $ _)) =>
sultana@55596
   711
          head_of t'
sultana@55596
   712
          |> 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
   713
          |> head_of
sultana@55596
   714
          |> dest_Const
sultana@55596
   715
        | _ => raise SKOLEM_DEF t
sultana@55596
   716
sultana@55596
   717
    val const_name =
sultana@55596
   718
      skolem_const_info_of conclusion
sultana@55596
   719
      |> fst
sultana@55596
   720
sultana@55596
   721
    val def_name = const_name ^ "_def"
sultana@55596
   722
sultana@55596
   723
    val bnd_def = (*FIXME consts*)
sultana@55596
   724
      const_name
wenzelm@56220
   725
      |> Long_Name.implode o tl o Long_Name.explode (*FIXME hack to drop theory-name prefix*)
sultana@55596
   726
      |> Binding.qualified_name
sultana@55596
   727
      |> Binding.suffix_name "_def"
sultana@55596
   728
sultana@55596
   729
    val bnd_name =
sultana@55596
   730
      case prob_name_opt of
sultana@55596
   731
          NONE => bnd_def
sultana@55596
   732
        | SOME prob_name =>
sultana@55596
   733
(*            Binding.qualify false
sultana@55596
   734
             (TPTP_Problem_Name.mangle_problem_name prob_name)
sultana@55596
   735
*)
sultana@55596
   736
             bnd_def
sultana@55596
   737
sultana@55596
   738
    val thm =
sultana@55596
   739
      if Name_Space.defined_entry (Theory.axiom_space thy) def_name then
sultana@55596
   740
        Thm.axiom thy def_name
sultana@55596
   741
      else
sultana@55596
   742
        if is_none prob_name_opt then
sultana@55596
   743
          (*This mode is for testing, so we can be a bit
sultana@55596
   744
            looser with theories*)
sultana@55596
   745
          Thm.add_axiom_global (bnd_name, conclusion) thy
sultana@55596
   746
          |> fst |> snd
sultana@55596
   747
        else
sultana@55596
   748
          raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion))
sultana@55596
   749
  in
sultana@55596
   750
    rtac (Drule.export_without_context thm) i st
sultana@55596
   751
  end
sultana@55596
   752
  handle SKOLEM_DEF _ => no_tac st
sultana@55596
   753
*}
sultana@55596
   754
sultana@55596
   755
ML {*
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 =
sultana@55596
   767
      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*)
sultana@55596
   778
        |> List.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
sultana@55596
   801
    |> map (get_skolem_terms [] [])
sultana@55596
   802
    |> List.concat
sultana@55596
   803
    |> distinct (op =)
sultana@55596
   804
  end
sultana@55596
   805
*}
sultana@55596
   806
sultana@55596
   807
ML {*
sultana@55596
   808
fun instantiate_skols ctxt consts_candidates i = fn st =>
sultana@55596
   809
  let
sultana@55596
   810
    val thy = Proof_Context.theory_of ctxt
sultana@55596
   811
sultana@55596
   812
    val gls =
sultana@55596
   813
      prop_of st
sultana@55596
   814
      |> Logic.strip_horn
sultana@55596
   815
      |> fst
sultana@55596
   816
sultana@55596
   817
    val (params, conclusion) =
sultana@55596
   818
      if null gls then
sultana@55596
   819
        raise NO_GOALS
sultana@55596
   820
      else
sultana@55596
   821
        rpair (i - 1) gls
sultana@55596
   822
        |> uncurry nth
sultana@55596
   823
        |> strip_top_all_vars []
sultana@55596
   824
        |> apsnd (Logic.strip_horn #> snd)
sultana@55596
   825
sultana@55596
   826
    fun skolem_const_info_of t =
sultana@55596
   827
      case t of
sultana@55596
   828
          Const (@{const_name HOL.Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ lhs $ (Const (@{const_name Hilbert_Choice.Eps}, _) $ rhs)) =>
sultana@55596
   829
          let
sultana@55596
   830
            (*the parameters we will concern ourselves with*)
sultana@55596
   831
            val params' =
sultana@55596
   832
              Term.add_frees lhs []
sultana@55596
   833
              |> distinct (op =)
sultana@55596
   834
            (*check to make sure that params' <= params*)
sultana@55596
   835
            val _ = @{assert} (List.all (member (op =) params) params')
sultana@55596
   836
            val skolem_const_ty =
sultana@55596
   837
              let
sultana@55596
   838
                val (skolem_const_prety, no_params) =
sultana@55596
   839
                  Term.strip_comb lhs
sultana@55596
   840
                  |> apfst (dest_Var #> snd) (*head of lhs consists of a logical variable. we just want its type.*)
sultana@55596
   841
                  |> apsnd length
sultana@55596
   842
sultana@55596
   843
                val _ = @{assert} (length params = no_params)
sultana@55596
   844
sultana@55596
   845
                (*get value type of a function type after n arguments have been supplied*)
sultana@55596
   846
                fun get_val_ty n ty =
sultana@55596
   847
                  if n = 0 then ty
sultana@55596
   848
                  else get_val_ty (n - 1) (dest_funT ty |> snd)
sultana@55596
   849
              in
sultana@55596
   850
                get_val_ty no_params skolem_const_prety
sultana@55596
   851
              end
sultana@55596
   852
sultana@55596
   853
          in
sultana@55596
   854
            (skolem_const_ty, params')
sultana@55596
   855
          end
sultana@55596
   856
        | _ => raise (SKOLEM_DEF t)
sultana@55596
   857
sultana@55596
   858
(*
sultana@55596
   859
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
   860
sultana@55596
   861
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
   862
*)
sultana@55596
   863
(*
sultana@55596
   864
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
   865
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
   866
*)
sultana@55596
   867
    fun use_candidate target_ty params acc cur_ty =
sultana@55596
   868
      if null params then
sultana@55596
   869
        if Type.eq_type Vartab.empty (cur_ty, target_ty) then
sultana@55596
   870
          SOME (rev acc)
sultana@55596
   871
        else NONE
sultana@55596
   872
      else
sultana@55596
   873
        let
sultana@55596
   874
          val (arg_ty, val_ty) = Term.dest_funT cur_ty
sultana@55596
   875
          (*now find a param of type arg_ty*)
sultana@55596
   876
          val (candidate_param, params') =
sultana@55596
   877
            find_and_remove
sultana@55596
   878
             (snd #> pair arg_ty #> Type.eq_type Vartab.empty)
sultana@55596
   879
             params
sultana@55596
   880
        in
sultana@55596
   881
          use_candidate target_ty params' (candidate_param :: acc) val_ty
sultana@55596
   882
        end
sultana@55596
   883
        handle TYPE ("dest_funT", _, _) => NONE
sultana@55596
   884
             | DEST_LIST => NONE
sultana@55596
   885
sultana@55596
   886
    val (skolem_const_ty, params') = skolem_const_info_of conclusion
sultana@55596
   887
sultana@55596
   888
(*
sultana@55596
   889
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
   890
sultana@55596
   891
Big picture:
sultana@55596
   892
  we run the following:
sultana@55596
   893
    drule leo2_skolemise THEN' this_tactic
sultana@55596
   894
sultana@55596
   895
NOTE: remember to APPEND' instead of ORELSE' the two tactics relating to skolemisation
sultana@55596
   896
*)
sultana@55596
   897
sultana@55596
   898
    val filtered_candidates =
sultana@55596
   899
      map (dest_Const
sultana@55596
   900
           #> snd
sultana@55596
   901
           #> use_candidate skolem_const_ty params' [])
sultana@55596
   902
       consts_candidates (* prefiltered_candidates *)
sultana@55596
   903
      |> pair consts_candidates (* prefiltered_candidates *)
sultana@55596
   904
      |> ListPair.zip
sultana@55596
   905
      |> filter (snd #> is_none #> not)
sultana@55596
   906
      |> map (apsnd the)
sultana@55596
   907
sultana@55596
   908
    val skolem_terms =
sultana@55596
   909
      let
sultana@55596
   910
        fun make_result_t (t, args) =
sultana@55596
   911
          (* list_comb (t, map Free args) *)
sultana@55596
   912
          if length args > 0 then
sultana@55596
   913
            hd (find_skolem_term ctxt t (length args) st)
sultana@55596
   914
          else t
sultana@55596
   915
      in
sultana@55596
   916
        map make_result_t filtered_candidates
sultana@55596
   917
      end
sultana@55596
   918
sultana@55596
   919
    (*prefix a skolem term with bindings for the parameters*)
sultana@55596
   920
    (* val contextualise = fold absdummy (map snd params) *)
sultana@55596
   921
    val contextualise = fold absfree params
sultana@55596
   922
sultana@55596
   923
    val skolem_cts = map (contextualise #> cterm_of thy) skolem_terms
sultana@55596
   924
sultana@55596
   925
sultana@55596
   926
(*now the instantiation code*)
sultana@55596
   927
sultana@55596
   928
    (*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
   929
    val var_opt =
sultana@55596
   930
      let
sultana@55596
   931
        val pre_var =
sultana@55596
   932
          gls
sultana@55596
   933
          |> map
sultana@55596
   934
              (strip_top_all_vars [] #> snd #>
sultana@55596
   935
               Logic.strip_horn #> snd #>
sultana@55596
   936
               get_skolem_conc)
sultana@55596
   937
          |> switch (fold (fn x => fn l => if is_some x then the x :: l else l)) []
sultana@55596
   938
          |> map (switch Term.add_vars [])
sultana@55596
   939
          |> List.concat
sultana@55596
   940
sultana@55596
   941
        fun make_var pre_var =
sultana@55596
   942
          the_single pre_var
sultana@55596
   943
          |> Var
sultana@55596
   944
          |> cterm_of thy
sultana@55596
   945
          |> SOME
sultana@55596
   946
      in
sultana@55596
   947
        if null pre_var then NONE
sultana@55596
   948
        else make_var pre_var
sultana@55596
   949
     end
sultana@55596
   950
sultana@55596
   951
    fun instantiate_tac from to =
sultana@55596
   952
      Thm.instantiate ([], [(from, to)])
sultana@55596
   953
      |> PRIMITIVE
sultana@55596
   954
sultana@55596
   955
    val tectic =
sultana@55596
   956
      if is_none var_opt then no_tac
sultana@55596
   957
      else
sultana@55596
   958
        fold (curry (op APPEND)) (map (instantiate_tac (the var_opt)) skolem_cts) no_tac
sultana@55596
   959
sultana@55596
   960
  in
sultana@55596
   961
    tectic st
sultana@55596
   962
  end
sultana@55596
   963
*}
sultana@55596
   964
sultana@55596
   965
ML {*
sultana@55596
   966
fun new_skolem_tac ctxt consts_candidates =
sultana@55596
   967
  let
sultana@55596
   968
    fun tec thm =
sultana@55596
   969
      dtac thm
sultana@55596
   970
      THEN' instantiate_skols ctxt consts_candidates
sultana@55596
   971
  in
sultana@55596
   972
    if null consts_candidates then K no_tac
sultana@55596
   973
    else FIRST' (map tec @{thms lift_exists})
sultana@55596
   974
  end
sultana@55596
   975
*}
sultana@55596
   976
sultana@55596
   977
(*
sultana@55596
   978
need a tactic to expand "? x . P" to "~ ! x. ~ P"
sultana@55596
   979
*)
sultana@55596
   980
ML {*
sultana@55596
   981
fun ex_expander_tac ctxt i =
sultana@55596
   982
   let
sultana@55596
   983
     val simpset =
sultana@55596
   984
       empty_simpset ctxt (*NOTE for some reason, Bind exception gets raised if ctxt's simpset isn't emptied*)
sultana@55596
   985
       |> Simplifier.add_simp @{lemma "Ex P == (~ (! x. ~ P x))" by auto}
sultana@55596
   986
   in
sultana@55596
   987
     CHANGED (asm_full_simp_tac simpset i)
sultana@55596
   988
   end
sultana@55596
   989
*}
sultana@55596
   990
sultana@55596
   991
sultana@55596
   992
subsubsection "extuni_dec"
sultana@55596
   993
sultana@55596
   994
ML {*
sultana@55596
   995
(*n-ary decomposition. Code is based on the n-ary arg_cong generator*)
sultana@55596
   996
fun extuni_dec_n ctxt arity =
sultana@55596
   997
  let
sultana@55596
   998
    val _ = @{assert} (arity > 0)
sultana@55596
   999
    val is =
sultana@55596
  1000
      upto (1, arity)
sultana@55596
  1001
      |> map Int.toString
sultana@55596
  1002
    val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", HOLogic.typeS)) is
sultana@55596
  1003
    val res_ty = TFree ("res" ^ "_ty", HOLogic.typeS)
sultana@55596
  1004
    val f_ty = arg_tys ---> res_ty
sultana@55596
  1005
    val f = Free ("f", f_ty)
sultana@55596
  1006
    val xs = map (fn i =>
sultana@55596
  1007
      Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is
sultana@55596
  1008
    (*FIXME DRY principle*)
sultana@55596
  1009
    val ys = map (fn i =>
sultana@55596
  1010
      Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is
sultana@55596
  1011
sultana@55596
  1012
    val hyp_lhs = list_comb (f, xs)
sultana@55596
  1013
    val hyp_rhs = list_comb (f, ys)
sultana@55596
  1014
    val hyp_eq =
sultana@55596
  1015
      HOLogic.eq_const res_ty $ hyp_lhs $ hyp_rhs
sultana@55596
  1016
    val hyp =
sultana@55596
  1017
      HOLogic.eq_const HOLogic.boolT $ hyp_eq $ @{term False}
sultana@55596
  1018
      |> HOLogic.mk_Trueprop
sultana@55596
  1019
    fun conc_eq i =
sultana@55596
  1020
      let
sultana@55596
  1021
        val ty = TFree ("arg" ^ i ^ "_ty", HOLogic.typeS)
sultana@55596
  1022
        val x = Free ("x" ^ i, ty)
sultana@55596
  1023
        val y = Free ("y" ^ i, ty)
sultana@55596
  1024
        val eq = HOLogic.eq_const ty $ x $ y
sultana@55596
  1025
      in
sultana@55596
  1026
        HOLogic.eq_const HOLogic.boolT $ eq $ @{term False}
sultana@55596
  1027
      end
sultana@55596
  1028
sultana@55596
  1029
    val conc_disjs = map conc_eq is
sultana@55596
  1030
sultana@55596
  1031
    val conc =
sultana@55596
  1032
      if length conc_disjs = 1 then
sultana@55596
  1033
        the_single conc_disjs
sultana@55596
  1034
      else
sultana@55596
  1035
        fold
sultana@55596
  1036
         (fn t => fn t_conc => HOLogic.mk_disj (t_conc, t))
sultana@55596
  1037
         (tl conc_disjs) (hd conc_disjs)
sultana@55596
  1038
sultana@55596
  1039
    val t =
sultana@55596
  1040
      Logic.mk_implies (hyp, HOLogic.mk_Trueprop conc)
sultana@55596
  1041
  in
sultana@55596
  1042
    Goal.prove ctxt [] [] t (fn _ => auto_tac ctxt)
sultana@55596
  1043
    |> Drule.export_without_context
sultana@55596
  1044
  end
sultana@55596
  1045
*}
sultana@55596
  1046
sultana@55596
  1047
ML {*
sultana@55596
  1048
(*Determine the arity of a function which the "dec"
sultana@55596
  1049
  unification rule is about to be applied.
sultana@55596
  1050
  NOTE:
sultana@55596
  1051
    * Assumes that there is a single hypothesis
sultana@55596
  1052
*)
sultana@55596
  1053
fun find_dec_arity i = fn st =>
sultana@55596
  1054
  let
sultana@55596
  1055
    val gls =
sultana@55596
  1056
      prop_of st
sultana@55596
  1057
      |> Logic.strip_horn
sultana@55596
  1058
      |> fst
sultana@55596
  1059
  in
sultana@55596
  1060
    if null gls then raise NO_GOALS
sultana@55596
  1061
    else
sultana@55596
  1062
      let
sultana@55596
  1063
        val (params, (literal, conc_clause)) =
sultana@55596
  1064
          rpair (i - 1) gls
sultana@55596
  1065
          |> uncurry nth
sultana@55596
  1066
          |> strip_top_all_vars []
sultana@55596
  1067
          |> apsnd Logic.strip_horn
sultana@55596
  1068
          |> apsnd (apfst the_single)
sultana@55596
  1069
sultana@55596
  1070
        val get_ty =
sultana@55596
  1071
          HOLogic.dest_Trueprop
sultana@55596
  1072
          #> strip_top_All_vars
sultana@55596
  1073
          #> snd
sultana@55596
  1074
          #> HOLogic.dest_eq (*polarity's "="*)
sultana@55596
  1075
          #> fst
sultana@55596
  1076
          #> HOLogic.dest_eq (*the unification constraint's "="*)
sultana@55596
  1077
          #> fst
sultana@55596
  1078
          #> head_of
sultana@55596
  1079
          #> dest_Const
sultana@55596
  1080
          #> snd
sultana@55596
  1081
sultana@55596
  1082
       fun arity_of ty =
sultana@55596
  1083
         let
sultana@55596
  1084
           val (_, res_ty) = dest_funT ty
sultana@55596
  1085
sultana@55596
  1086
         in
sultana@55596
  1087
           1 + arity_of res_ty
sultana@55596
  1088
         end
sultana@55596
  1089
         handle (TYPE ("dest_funT", _, _)) => 0
sultana@55596
  1090
sultana@55596
  1091
      in
sultana@55596
  1092
        arity_of (get_ty literal)
sultana@55596
  1093
      end
sultana@55596
  1094
  end
sultana@55596
  1095
sultana@55596
  1096
(*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
  1097
fun breakdown_inference i = fn st =>
sultana@55596
  1098
  let
sultana@55596
  1099
    val gls =
sultana@55596
  1100
      prop_of st
sultana@55596
  1101
      |> Logic.strip_horn
sultana@55596
  1102
      |> fst
sultana@55596
  1103
  in
sultana@55596
  1104
    if null gls then raise NO_GOALS
sultana@55596
  1105
    else
sultana@55596
  1106
      rpair (i - 1) gls
sultana@55596
  1107
      |> uncurry nth
sultana@55596
  1108
      |> strip_top_all_vars []
sultana@55596
  1109
  end
sultana@55596
  1110
sultana@55596
  1111
(*build a custom elimination rule for extuni_dec, and instantiate it to match a specific subgoal*)
sultana@55596
  1112
fun extuni_dec_elim_rule ctxt arity i = fn st =>
sultana@55596
  1113
  let
sultana@55596
  1114
    val rule = extuni_dec_n ctxt arity
sultana@55596
  1115
sultana@55596
  1116
    val rule_hyp =
sultana@55596
  1117
      prop_of rule
sultana@55596
  1118
      |> Logic.dest_implies
sultana@55596
  1119
      |> fst (*assuming that rule has single hypothesis*)
sultana@55596
  1120
sultana@55596
  1121
    (*having run break_hypothesis earlier, we know that the hypothesis
sultana@55596
  1122
      now consists of a single literal. We can (and should)
sultana@55596
  1123
      disregard the conclusion, since it hasn't been "broken",
sultana@55596
  1124
      and it might include some unwanted literals -- the latter
sultana@55596
  1125
      could cause "diff" to fail (since they won't agree with the
sultana@55596
  1126
      rule we have generated.*)
sultana@55596
  1127
sultana@55596
  1128
    val inference_hyp =
sultana@55596
  1129
      snd (breakdown_inference i st)
sultana@55596
  1130
      |> Logic.dest_implies
sultana@55596
  1131
      |> fst (*assuming that inference has single hypothesis,
sultana@55596
  1132
               as explained above.*)
sultana@55596
  1133
  in
sultana@55596
  1134
    TPTP_Reconstruct_Library.diff_and_instantiate ctxt rule rule_hyp inference_hyp
sultana@55596
  1135
  end
sultana@55596
  1136
sultana@55596
  1137
fun extuni_dec_tac ctxt i = fn st =>
sultana@55596
  1138
  let
sultana@55596
  1139
    val arity = find_dec_arity i st
sultana@55596
  1140
sultana@55596
  1141
    fun elim_tac i st =
sultana@55596
  1142
      let
sultana@55596
  1143
        val rule =
sultana@55596
  1144
          extuni_dec_elim_rule ctxt arity i st
sultana@55596
  1145
          (*in case we itroduced free variables during
sultana@55596
  1146
            instantiation, we generalise the rule to make
sultana@55596
  1147
            those free variables into logical variables.*)
sultana@55596
  1148
          |> Thm.forall_intr_frees
sultana@55596
  1149
          |> Drule.export_without_context
sultana@55596
  1150
      in dtac rule i st end
sultana@55596
  1151
      handle NO_GOALS => no_tac st
sultana@55596
  1152
sultana@55596
  1153
    fun closure tac =
sultana@55596
  1154
     (*batter fails if there's no toplevel disjunction in the
sultana@55596
  1155
       hypothesis, so we also try atac*)
sultana@55596
  1156
      SOLVE o (tac THEN' (batter ORELSE' atac))
sultana@55596
  1157
    val search_tac =
sultana@55596
  1158
      ASAP
sultana@55596
  1159
        (rtac @{thm disjI1} APPEND' rtac @{thm disjI2})
sultana@55596
  1160
        (FIRST' (map closure
sultana@55596
  1161
                  [dresolve_tac @{thms dec_commut_eq},
sultana@55596
  1162
                   dtac @{thm dec_commut_disj},
sultana@55596
  1163
                   elim_tac]))
sultana@55596
  1164
  in
sultana@55596
  1165
    (CHANGED o search_tac) i st
sultana@55596
  1166
  end
sultana@55596
  1167
*}
sultana@55596
  1168
sultana@55596
  1169
sultana@55596
  1170
subsubsection "standard_cnf"
sultana@55596
  1171
(*Given a standard_cnf inference, normalise it
sultana@55596
  1172
     e.g. ((A & B) & C \<longrightarrow> D & E \<longrightarrow> F \<longrightarrow> G) = False
sultana@55596
  1173
     is changed to
sultana@55596
  1174
          (A & B & C & D & E & F \<longrightarrow> G) = False
sultana@55596
  1175
 then custom-build a metatheorem which validates this:
sultana@55596
  1176
          (A & B & C & D & E & F \<longrightarrow> G) = False
sultana@55596
  1177
       -------------------------------------------
sultana@55596
  1178
          (A = True) & (B = True) & (C = True) &
sultana@55596
  1179
          (D = True) & (E = True) & (F = True) & (G = False)
sultana@55596
  1180
 and apply this metatheorem.
sultana@55596
  1181
sultana@55596
  1182
There aren't any "positive" standard_cnfs in Leo2's calculus:
sultana@55596
  1183
  e.g.,  "(A \<longrightarrow> B) = True \<Longrightarrow> A = False | (A = True & B = True)"
sultana@55596
  1184
since "standard_cnf" seems to be applied at the preprocessing
sultana@55596
  1185
stage, together with splitting.
sultana@55596
  1186
*)
sultana@55596
  1187
sultana@55596
  1188
ML {*
sultana@55596
  1189
(*Conjunctive counterparts to Term.disjuncts_aux and Term.disjuncts*)
sultana@55596
  1190
fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs =
sultana@55596
  1191
     conjuncts_aux t (conjuncts_aux t' conjs)
sultana@55596
  1192
  | conjuncts_aux t conjs = t :: conjs
sultana@55596
  1193
sultana@55596
  1194
fun conjuncts t = conjuncts_aux t []
sultana@55596
  1195
sultana@55596
  1196
(*HOL equivalent of Logic.strip_horn*)
sultana@55596
  1197
local
sultana@55596
  1198
  fun imp_strip_horn' acc (Const (@{const_name HOL.implies}, _) $ A $ B) =
sultana@55596
  1199
        imp_strip_horn' (A :: acc) B
sultana@55596
  1200
    | imp_strip_horn' acc t = (acc, t)
sultana@55596
  1201
in
sultana@55596
  1202
  fun imp_strip_horn t =
sultana@55596
  1203
    imp_strip_horn' [] t
sultana@55596
  1204
    |> apfst rev
sultana@55596
  1205
end
sultana@55596
  1206
*}
sultana@55596
  1207
sultana@55596
  1208
ML {*
sultana@55596
  1209
(*Returns whether the antecedents are separated by conjunctions
sultana@55596
  1210
  or implications; the number of antecedents; and the polarity
sultana@55596
  1211
  of the original clause -- I think this will always be "false".*)
sultana@55596
  1212
fun standard_cnf_type ctxt i : thm -> (TPTP_Reconstruct.formula_kind * int * bool) option = fn st =>
sultana@55596
  1213
  let
sultana@55596
  1214
    val gls =
sultana@55596
  1215
      prop_of st
sultana@55596
  1216
      |> Logic.strip_horn
sultana@55596
  1217
      |> fst
sultana@55596
  1218
sultana@55596
  1219
    val hypos =
sultana@55596
  1220
      if null gls then raise NO_GOALS
sultana@55596
  1221
      else
sultana@55596
  1222
        rpair (i - 1) gls
sultana@55596
  1223
        |> uncurry nth
sultana@55596
  1224
        |> TPTP_Reconstruct.strip_top_all_vars []
sultana@55596
  1225
        |> snd
sultana@55596
  1226
        |> Logic.strip_horn
sultana@55596
  1227
        |> fst
sultana@55596
  1228
sultana@55596
  1229
    (*hypothesis clause should be singleton*)
sultana@55596
  1230
    val _ = @{assert} (length hypos = 1)
sultana@55596
  1231
sultana@55596
  1232
    val (t, pol) = the_single hypos
sultana@55596
  1233
      |> try_dest_Trueprop
sultana@55596
  1234
      |> TPTP_Reconstruct.strip_top_All_vars
sultana@55596
  1235
      |> snd
sultana@55596
  1236
      |> TPTP_Reconstruct.remove_polarity true
sultana@55596
  1237
sultana@55596
  1238
    (*literal is negative*)
sultana@55596
  1239
    val _ = @{assert} (not pol)
sultana@55596
  1240
sultana@55596
  1241
    val (antes, conc) = imp_strip_horn t
sultana@55596
  1242
sultana@55596
  1243
    val (ante_type, antes') =
sultana@55596
  1244
      if length antes = 1 then
sultana@55596
  1245
        let
sultana@55596
  1246
          val conjunctive_antes =
sultana@55596
  1247
            the_single antes
sultana@55596
  1248
            |> conjuncts
sultana@55596
  1249
        in
sultana@55596
  1250
          if length conjunctive_antes > 1 then
sultana@55596
  1251
            (TPTP_Reconstruct.Conjunctive NONE,
sultana@55596
  1252
             conjunctive_antes)
sultana@55596
  1253
          else
sultana@55596
  1254
            (TPTP_Reconstruct.Implicational NONE,
sultana@55596
  1255
             antes)
sultana@55596
  1256
        end
sultana@55596
  1257
      else
sultana@55596
  1258
        (TPTP_Reconstruct.Implicational NONE,
sultana@55596
  1259
         antes)
sultana@55596
  1260
  in
sultana@55596
  1261
    if null antes then NONE
sultana@55596
  1262
    else SOME (ante_type, length antes', pol)
sultana@55596
  1263
  end
sultana@55596
  1264
*}
sultana@55596
  1265
sultana@55596
  1266
ML {*
sultana@55596
  1267
(*Given a certain standard_cnf type, build a metatheorem that would
sultana@55596
  1268
  validate it*)
sultana@55596
  1269
fun mk_standard_cnf ctxt kind arity =
sultana@55596
  1270
  let
sultana@55596
  1271
    val _ = @{assert} (arity > 0)
sultana@55596
  1272
    val vars =
sultana@55596
  1273
      upto (1, arity + 1)
sultana@55596
  1274
      |> map (fn i => Free ("x" ^ Int.toString i, HOLogic.boolT))
sultana@55596
  1275
sultana@55596
  1276
    val consequent = hd vars
sultana@55596
  1277
    val antecedents = tl vars
sultana@55596
  1278
sultana@55596
  1279
    val conc =
sultana@55596
  1280
      fold
sultana@55596
  1281
       (curry HOLogic.mk_conj)
sultana@55596
  1282
       (map (fn var => HOLogic.mk_eq (var, @{term True})) antecedents)
sultana@55596
  1283
       (HOLogic.mk_eq (consequent, @{term False}))
sultana@55596
  1284
sultana@55596
  1285
    val pre_hyp =
sultana@55596
  1286
      case kind of
sultana@55596
  1287
          TPTP_Reconstruct.Conjunctive NONE =>
sultana@55596
  1288
            curry HOLogic.mk_imp
sultana@55596
  1289
             (if length antecedents = 1 then the_single antecedents
sultana@55596
  1290
              else
sultana@55596
  1291
                fold (curry HOLogic.mk_conj) (tl antecedents) (hd antecedents))
sultana@55596
  1292
             (hd vars)
sultana@55596
  1293
        | TPTP_Reconstruct.Implicational NONE =>
sultana@55596
  1294
            fold (curry HOLogic.mk_imp) antecedents consequent
sultana@55596
  1295
sultana@55596
  1296
    val hyp = HOLogic.mk_eq (pre_hyp, @{term False})
sultana@55596
  1297
sultana@55596
  1298
    val t =
sultana@55596
  1299
      Logic.mk_implies (HOLogic.mk_Trueprop  hyp, HOLogic.mk_Trueprop conc)
sultana@55596
  1300
  in
sultana@55596
  1301
    Goal.prove ctxt [] [] t (fn _ => HEADGOAL (blast_tac ctxt))
sultana@55596
  1302
    |> Drule.export_without_context
sultana@55596
  1303
  end
sultana@55596
  1304
*}
sultana@55596
  1305
sultana@55596
  1306
ML {*
sultana@55596
  1307
(*Applies a d-tactic, then breaks it up conjunctively.
sultana@55596
  1308
  This can be used to transform subgoals as follows:
sultana@55596
  1309
     (A \<longrightarrow> B) = False  \<Longrightarrow> R
sultana@55596
  1310
              |
sultana@55596
  1311
              v
sultana@55596
  1312
  \<lbrakk>A = True; B = False\<rbrakk> \<Longrightarrow> R
sultana@55596
  1313
*)
sultana@55596
  1314
fun weak_conj_tac drule =
sultana@55596
  1315
  dtac drule THEN' (REPEAT_DETERM o etac @{thm conjE})
sultana@55596
  1316
*}
sultana@55596
  1317
sultana@55596
  1318
ML {*
sultana@55596
  1319
val uncurry_lit_neg_tac =
sultana@55596
  1320
  dtac @{lemma "(A \<longrightarrow> B \<longrightarrow> C) = False \<Longrightarrow> (A & B \<longrightarrow> C) = False" by auto}
sultana@55596
  1321
  #> REPEAT_DETERM
sultana@55596
  1322
*}
sultana@55596
  1323
sultana@55596
  1324
ML {*
sultana@55596
  1325
fun standard_cnf_tac ctxt i = fn st =>
sultana@55596
  1326
  let
sultana@55596
  1327
    fun core_tactic i = fn st =>
sultana@55596
  1328
      case standard_cnf_type ctxt i st of
sultana@55596
  1329
          NONE => no_tac st
sultana@55596
  1330
        | SOME (kind, arity, _) =>
sultana@55596
  1331
            let
sultana@55596
  1332
              val rule = mk_standard_cnf ctxt kind arity;
sultana@55596
  1333
            in
sultana@55596
  1334
              (weak_conj_tac rule THEN' atac) i st
sultana@55596
  1335
            end
sultana@55596
  1336
  in
sultana@55596
  1337
    (uncurry_lit_neg_tac
sultana@55596
  1338
     THEN' TPTP_Reconstruct_Library.reassociate_conjs_tac ctxt
sultana@55596
  1339
     THEN' core_tactic) i st
sultana@55596
  1340
  end
sultana@55596
  1341
*}
sultana@55596
  1342
sultana@55596
  1343
sultana@55596
  1344
subsubsection "Emulator prep"
sultana@55596
  1345
sultana@55596
  1346
ML {*
sultana@55596
  1347
datatype cleanup_feature =
sultana@55596
  1348
    RemoveHypothesesFromSkolemDefs
sultana@55596
  1349
  | RemoveDuplicates
sultana@55596
  1350
sultana@55596
  1351
datatype loop_feature =
sultana@55596
  1352
    Close_Branch
sultana@55596
  1353
  | ConjI
sultana@55596
  1354
  | King_Cong
sultana@55596
  1355
  | Break_Hypotheses
sultana@55596
  1356
  | Donkey_Cong (*simper_animal + ex_expander_tac*)
sultana@55596
  1357
  | RemoveRedundantQuantifications
sultana@55596
  1358
  | Assumption
sultana@55596
  1359
sultana@55596
  1360
  (*Closely based on Leo2 calculus*)
sultana@55596
  1361
  | Existential_Free
sultana@55596
  1362
  | Existential_Var
sultana@55596
  1363
  | Universal
sultana@55596
  1364
  | Not_pos
sultana@55596
  1365
  | Not_neg
sultana@55596
  1366
  | Or_pos
sultana@55596
  1367
  | Or_neg
sultana@55596
  1368
  | Equal_pos
sultana@55596
  1369
  | Equal_neg
sultana@55596
  1370
  | Extuni_Bool2
sultana@55596
  1371
  | Extuni_Bool1
sultana@55596
  1372
  | Extuni_Dec
sultana@55596
  1373
  | Extuni_Bind
sultana@55596
  1374
  | Extuni_Triv
sultana@55596
  1375
  | Extuni_FlexRigid
sultana@55596
  1376
  | Extuni_Func
sultana@55596
  1377
  | Polarity_switch
sultana@55596
  1378
  | Forall_special_pos
sultana@55596
  1379
sultana@55596
  1380
datatype feature =
sultana@55596
  1381
    ConstsDiff
sultana@55596
  1382
  | StripQuantifiers
sultana@55596
  1383
  | Flip_Conclusion
sultana@55596
  1384
  | Loop of loop_feature list
sultana@55596
  1385
  | LoopOnce of loop_feature list
sultana@55596
  1386
  | InnerLoopOnce of loop_feature list
sultana@55596
  1387
  | CleanUp of cleanup_feature list
sultana@55596
  1388
  | AbsorbSkolemDefs
sultana@55596
  1389
*}
sultana@55596
  1390
sultana@55596
  1391
ML {*
sultana@55596
  1392
fun can_feature x l =
sultana@55596
  1393
  let
sultana@55596
  1394
    fun sublist_of_clean_up el =
sultana@55596
  1395
      case el of
sultana@55596
  1396
          CleanUp l'' => SOME l''
sultana@55596
  1397
        | _ => NONE
sultana@55596
  1398
    fun sublist_of_loop el =
sultana@55596
  1399
      case el of
sultana@55596
  1400
          Loop l'' => SOME l''
sultana@55596
  1401
        | _ => NONE
sultana@55596
  1402
    fun sublist_of_loop_once el =
sultana@55596
  1403
      case el of
sultana@55596
  1404
          LoopOnce l'' => SOME l''
sultana@55596
  1405
        | _ => NONE
sultana@55596
  1406
    fun sublist_of_inner_loop_once el =
sultana@55596
  1407
      case el of
sultana@55596
  1408
          InnerLoopOnce l'' => SOME l''
sultana@55596
  1409
        | _ => NONE
sultana@55596
  1410
sultana@55596
  1411
    fun check_sublist sought_sublist opt_list =
sultana@55596
  1412
      if List.all is_none opt_list then false
sultana@55596
  1413
      else
sultana@55596
  1414
        fold_options opt_list
sultana@55596
  1415
        |> List.concat
sultana@55596
  1416
        |> pair sought_sublist
sultana@55596
  1417
        |> subset (op =)
sultana@55596
  1418
  in
sultana@55596
  1419
    case x of
sultana@55596
  1420
        CleanUp l' =>
sultana@55596
  1421
          map sublist_of_clean_up l
sultana@55596
  1422
          |> check_sublist l'
sultana@55596
  1423
      | Loop l' =>
sultana@55596
  1424
          map sublist_of_loop l
sultana@55596
  1425
          |> check_sublist l'
sultana@55596
  1426
      | LoopOnce l' =>
sultana@55596
  1427
          map sublist_of_loop_once l
sultana@55596
  1428
          |> check_sublist l'
sultana@55596
  1429
      | InnerLoopOnce l' =>
sultana@55596
  1430
          map sublist_of_inner_loop_once l
sultana@55596
  1431
          |> check_sublist l'
sultana@55596
  1432
      | _ => List.exists (curry (op =) x) l
sultana@55596
  1433
  end;
sultana@55596
  1434
sultana@55596
  1435
fun loop_can_feature loop_feats l =
sultana@55596
  1436
  can_feature (Loop loop_feats) l orelse
sultana@55596
  1437
  can_feature (LoopOnce loop_feats) l orelse
sultana@55596
  1438
  can_feature (InnerLoopOnce loop_feats) l;
sultana@55596
  1439
sultana@55596
  1440
@{assert} (can_feature ConstsDiff [StripQuantifiers, ConstsDiff]);
sultana@55596
  1441
sultana@55596
  1442
@{assert}
sultana@55596
  1443
  (can_feature (CleanUp [RemoveHypothesesFromSkolemDefs])
sultana@55596
  1444
    [CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates]]);
sultana@55596
  1445
sultana@55596
  1446
@{assert}
sultana@55596
  1447
  (can_feature (Loop []) [Loop [Existential_Var]]);
sultana@55596
  1448
sultana@55596
  1449
@{assert}
sultana@55596
  1450
  (not (can_feature (Loop []) [InnerLoopOnce [Existential_Var]]));
sultana@55596
  1451
*}
sultana@55596
  1452
sultana@55596
  1453
ML {*
sultana@55596
  1454
exception NO_LOOP_FEATS
sultana@55596
  1455
fun get_loop_feats (feats : feature list) =
sultana@55596
  1456
  let
sultana@55596
  1457
    val loop_find =
sultana@55596
  1458
      fold (fn x => fn loop_feats_acc =>
sultana@55596
  1459
        if is_some loop_feats_acc then loop_feats_acc
sultana@55596
  1460
        else
sultana@55596
  1461
          case x of
sultana@55596
  1462
              Loop loop_feats => SOME loop_feats
sultana@55596
  1463
            | LoopOnce loop_feats => SOME loop_feats
sultana@55596
  1464
            | InnerLoopOnce loop_feats => SOME loop_feats
sultana@55596
  1465
            | _ => NONE)
sultana@55596
  1466
       feats
sultana@55596
  1467
       NONE
sultana@55596
  1468
  in
sultana@55596
  1469
    if is_some loop_find then the loop_find
sultana@55596
  1470
    else raise NO_LOOP_FEATS
sultana@55596
  1471
  end;
sultana@55596
  1472
sultana@55596
  1473
@{assert}
sultana@55596
  1474
  (get_loop_feats [Loop [King_Cong, Break_Hypotheses, Existential_Free, Existential_Var, Universal]] =
sultana@55596
  1475
   [King_Cong, Break_Hypotheses, Existential_Free, Existential_Var, Universal])
sultana@55596
  1476
*}
sultana@55596
  1477
sultana@55596
  1478
(*use as elim rule to remove premises*)
sultana@55596
  1479
lemma insa_prems: "\<lbrakk>Q; P\<rbrakk> \<Longrightarrow> P" by auto
sultana@55596
  1480
ML {*
sultana@55596
  1481
fun cleanup_skolem_defs feats =
sultana@55596
  1482
  let
sultana@55596
  1483
    (*remove hypotheses from skolem defs,
sultana@55596
  1484
     after testing that they look like skolem defs*)
sultana@55596
  1485
    val dehypothesise_skolem_defs =
sultana@55596
  1486
      COND' (SOME #> TERMPRED (fn _ => true) conc_is_skolem_def)
sultana@55596
  1487
        (REPEAT_DETERM o etac @{thm insa_prems})
sultana@55596
  1488
        (K no_tac)
sultana@55596
  1489
  in
sultana@55596
  1490
    if can_feature (CleanUp [RemoveHypothesesFromSkolemDefs]) feats then
sultana@55596
  1491
      ALLGOALS (TRY o dehypothesise_skolem_defs)
sultana@55596
  1492
    else all_tac
sultana@55596
  1493
  end
sultana@55596
  1494
*}
sultana@55596
  1495
sultana@55596
  1496
ML {*
sultana@55596
  1497
fun remove_duplicates_tac feats =
sultana@55596
  1498
  (if can_feature (CleanUp [RemoveDuplicates]) feats then
sultana@55596
  1499
     ALLGOALS distinct_subgoal_tac
sultana@55596
  1500
   else all_tac)
sultana@55596
  1501
*}
sultana@55596
  1502
sultana@55596
  1503
ML {*
sultana@55596
  1504
(*given a goal state, indicates the skolem constants committed-to in it (i.e. appearing in LHS of a skolem definition)*)
sultana@55596
  1505
val which_skolem_concs_used = fn st =>
sultana@55596
  1506
  let
sultana@55596
  1507
    val feats = [CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates]]
sultana@55596
  1508
    val scrubup_tac =
sultana@55596
  1509
      cleanup_skolem_defs feats
sultana@55596
  1510
      THEN remove_duplicates_tac feats
sultana@55596
  1511
  in
sultana@55596
  1512
    scrubup_tac st
sultana@55596
  1513
    |> break_seq
sultana@55596
  1514
    |> tap (fn (_, rest) => @{assert} (null (Seq.list_of rest)))
sultana@55596
  1515
    |> fst
sultana@55596
  1516
    |> TERMFUN (snd (*discard hypotheses*)
sultana@55596
  1517
                 #> get_skolem_conc_const) NONE
sultana@55596
  1518
    |> switch (fold (fn x => fn l => if is_some x then the x :: l else l)) []
sultana@55596
  1519
    |> map Const
sultana@55596
  1520
  end
sultana@55596
  1521
*}
sultana@55596
  1522
sultana@55596
  1523
ML {*
sultana@55596
  1524
fun exists_tac ctxt feats consts_diff =
sultana@55596
  1525
  let
sultana@55596
  1526
    val ex_var =
sultana@55596
  1527
      if loop_can_feature [Existential_Var] feats andalso consts_diff <> [] then
sultana@55596
  1528
        new_skolem_tac ctxt consts_diff
sultana@55596
  1529
        (*We're making sure that each skolem constant is used once in instantiations.*)
sultana@55596
  1530
      else K no_tac
sultana@55596
  1531
sultana@55596
  1532
    val ex_free =
sultana@55596
  1533
      if loop_can_feature [Existential_Free] feats andalso consts_diff = [] then
sultana@55596
  1534
        eresolve_tac @{thms polar_exE}
sultana@55596
  1535
      else K no_tac
sultana@55596
  1536
  in
sultana@55596
  1537
    ex_var APPEND' ex_free
sultana@55596
  1538
  end
sultana@55596
  1539
sultana@55596
  1540
fun forall_tac ctxt feats =
sultana@55596
  1541
  if loop_can_feature [Universal] feats then
sultana@55596
  1542
    forall_pos_tac ctxt
sultana@55596
  1543
  else K no_tac
sultana@55596
  1544
*}
sultana@55596
  1545
sultana@55596
  1546
sultana@55596
  1547
subsubsection "Finite types"
sultana@55596
  1548
(*lift quantification from a singleton literal to a singleton clause*)
sultana@55596
  1549
lemma forall_pos_lift:
sultana@55596
  1550
"\<lbrakk>(! X. P X) = True; ! X. (P X = True) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by auto
sultana@55596
  1551
sultana@55596
  1552
(*predicate over the type of the leading quantified variable*)
sultana@55596
  1553
sultana@55596
  1554
ML {*
sultana@55596
  1555
val extcnf_forall_special_pos_tac =
sultana@55596
  1556
  let
sultana@55596
  1557
    val bool =
sultana@55596
  1558
      ["True", "False"]
sultana@55596
  1559
sultana@55596
  1560
    val bool_to_bool =
sultana@55596
  1561
      ["% _ . True", "% _ . False", "% x . x", "Not"]
sultana@55596
  1562
sultana@55596
  1563
    val tecs =
sultana@55596
  1564
      map (fn t_s =>
sultana@55596
  1565
       eres_inst_tac @{context} [(("x", 0), t_s)] @{thm allE}
sultana@55596
  1566
       THEN' atac)
sultana@55596
  1567
  in
sultana@55596
  1568
    (TRY o etac @{thm forall_pos_lift})
sultana@55596
  1569
    THEN' (atac
sultana@55596
  1570
           ORELSE' FIRST'
sultana@55596
  1571
            (*FIXME could check the type of the leading quantified variable, instead of trying everything*)
sultana@55596
  1572
            (tecs (bool @ bool_to_bool)))
sultana@55596
  1573
  end
sultana@55596
  1574
*}
sultana@55596
  1575
sultana@55596
  1576
sultana@55596
  1577
subsubsection "Emulator"
sultana@55596
  1578
sultana@55596
  1579
lemma efq: "[|A = True; A = False|] ==> R" by auto
sultana@55596
  1580
ML {*
sultana@55596
  1581
val efq_tac =
sultana@55596
  1582
  (etac @{thm efq} THEN' atac)
sultana@55596
  1583
  ORELSE' atac
sultana@55596
  1584
*}
sultana@55596
  1585
sultana@55596
  1586
ML {*
sultana@55596
  1587
(*This is applied to all subgoals, repeatedly*)
sultana@55596
  1588
fun extcnf_combined_main ctxt feats consts_diff =
sultana@55596
  1589
  let
sultana@55596
  1590
    (*This is applied to subgoals which don't have a conclusion
sultana@55596
  1591
      consisting of a Skolem definition*)
sultana@55596
  1592
    fun extcnf_combined_tac' ctxt i = fn st =>
sultana@55596
  1593
      let
sultana@55596
  1594
        val skolem_consts_used_so_far = which_skolem_concs_used st
sultana@55596
  1595
        val consts_diff' = subtract (op =) skolem_consts_used_so_far consts_diff
sultana@55596
  1596
sultana@55596
  1597
        fun feat_to_tac feat =
sultana@55596
  1598
          case feat of
sultana@55596
  1599
              Close_Branch => trace_tac' "mark: closer" efq_tac
sultana@55596
  1600
            | ConjI => trace_tac' "mark: conjI" (rtac @{thm conjI})
sultana@55596
  1601
            | King_Cong => trace_tac' "mark: expander_animal" (expander_animal ctxt)
sultana@55596
  1602
            | Break_Hypotheses => trace_tac' "mark: break_hypotheses" break_hypotheses
sultana@55596
  1603
            | RemoveRedundantQuantifications => K all_tac
sultana@55596
  1604
(*
sultana@55596
  1605
FIXME Building this into the loop instead.. maybe not the ideal choice
sultana@55596
  1606
            | RemoveRedundantQuantifications =>
sultana@55596
  1607
                trace_tac' "mark: strip_unused_variable_hyp"
sultana@55596
  1608
                 (REPEAT_DETERM o remove_redundant_quantification_in_lit)
sultana@55596
  1609
*)
sultana@55596
  1610
sultana@55596
  1611
            | Assumption => atac
sultana@55596
  1612
(*FIXME both Existential_Free and Existential_Var run same code*)
sultana@55596
  1613
            | Existential_Free => trace_tac' "mark: forall_neg" (exists_tac ctxt feats consts_diff')
sultana@55596
  1614
            | Existential_Var => trace_tac' "mark: forall_neg" (exists_tac ctxt feats consts_diff')
sultana@55596
  1615
            | Universal => trace_tac' "mark: forall_pos" (forall_tac ctxt feats)
sultana@55596
  1616
            | Not_pos => trace_tac' "mark: not_pos" (dtac @{thm leo2_rules(9)})
sultana@55596
  1617
            | Not_neg => trace_tac' "mark: not_neg" (dtac @{thm leo2_rules(10)})
sultana@55596
  1618
            | Or_pos => trace_tac' "mark: or_pos" (dtac @{thm leo2_rules(5)}) (*could add (6) for negated conjunction*)
sultana@55596
  1619
            | Or_neg => trace_tac' "mark: or_neg" (dtac @{thm leo2_rules(7)})
sultana@55596
  1620
            | Equal_pos => trace_tac' "mark: equal_pos" (dresolve_tac (@{thms eq_pos_bool} @ [@{thm leo2_rules(3)}, @{thm eq_pos_func}]))
sultana@55596
  1621
            | Equal_neg => trace_tac' "mark: equal_neg" (dresolve_tac [@{thm eq_neg_bool}, @{thm leo2_rules(4)}])
sultana@55596
  1622
            | Donkey_Cong => trace_tac' "mark: donkey_cong" (simper_animal ctxt THEN' ex_expander_tac ctxt)
sultana@55596
  1623
sultana@55596
  1624
            | Extuni_Bool2 => trace_tac' "mark: extuni_bool2" (dtac @{thm extuni_bool2})
sultana@55596
  1625
            | Extuni_Bool1 => trace_tac' "mark: extuni_bool1" (dtac @{thm extuni_bool1})
sultana@55596
  1626
            | Extuni_Bind => trace_tac' "mark: extuni_triv" (etac @{thm extuni_triv})
sultana@55596
  1627
            | Extuni_Triv => trace_tac' "mark: extuni_triv" (etac @{thm extuni_triv})
sultana@55596
  1628
            | Extuni_Dec => trace_tac' "mark: extuni_dec_tac" (extuni_dec_tac ctxt)
sultana@55596
  1629
            | Extuni_FlexRigid => trace_tac' "mark: extuni_flex_rigid" (atac ORELSE' asm_full_simp_tac ctxt)
sultana@55596
  1630
            | Extuni_Func => trace_tac' "mark: extuni_func" (dtac @{thm extuni_func})
sultana@55596
  1631
            | Polarity_switch => trace_tac' "mark: polarity_switch" (eresolve_tac @{thms polarity_switch})
sultana@55596
  1632
            | Forall_special_pos => trace_tac' "mark: dorall_special_pos" extcnf_forall_special_pos_tac
sultana@55596
  1633
sultana@55596
  1634
        val core_tac =
sultana@55596
  1635
          get_loop_feats feats
sultana@55596
  1636
          |> map feat_to_tac
sultana@55596
  1637
          |> FIRST'
sultana@55596
  1638
      in
sultana@55596
  1639
        core_tac i st
sultana@55596
  1640
      end
sultana@55596
  1641
sultana@55596
  1642
    (*This is applied to all subgoals, repeatedly*)
sultana@55596
  1643
    fun extcnf_combined_tac ctxt i =
sultana@55596
  1644
      COND (TERMPRED (fn _ => true) conc_is_skolem_def (SOME i))
sultana@55596
  1645
        no_tac
sultana@55596
  1646
        (extcnf_combined_tac' ctxt i)
sultana@55596
  1647
sultana@55596
  1648
    val core_tac = CHANGED (ALLGOALS (IF_UNSOLVED o TRY o extcnf_combined_tac ctxt))
sultana@55596
  1649
sultana@55596
  1650
    val full_tac = REPEAT core_tac
sultana@55596
  1651
sultana@55596
  1652
  in
sultana@55596
  1653
    CHANGED
sultana@55596
  1654
      (if can_feature (InnerLoopOnce []) feats then
sultana@55596
  1655
         core_tac
sultana@55596
  1656
       else full_tac)
sultana@55596
  1657
  end
sultana@55596
  1658
sultana@55596
  1659
val interpreted_consts =
sultana@55596
  1660
  [@{const_name HOL.All}, @{const_name HOL.Ex},
sultana@55596
  1661
   @{const_name Hilbert_Choice.Eps},
sultana@55596
  1662
   @{const_name HOL.conj},
sultana@55596
  1663
   @{const_name HOL.disj},
sultana@55596
  1664
   @{const_name HOL.eq},
sultana@55596
  1665
   @{const_name HOL.implies},
sultana@55596
  1666
   @{const_name HOL.The},
sultana@55596
  1667
   @{const_name HOL.Ex1},
sultana@55596
  1668
   @{const_name HOL.Not},
sultana@55596
  1669
   (* @{const_name HOL.iff}, *) (*FIXME do these exist?*)
sultana@55596
  1670
   (* @{const_name HOL.not_equal}, *)
sultana@55596
  1671
   @{const_name HOL.False},
sultana@55596
  1672
   @{const_name HOL.True},
wenzelm@56245
  1673
   @{const_name Pure.imp}]
sultana@55596
  1674
sultana@55596
  1675
fun strip_qtfrs_tac ctxt =
sultana@55596
  1676
  REPEAT_DETERM (HEADGOAL (rtac @{thm allI}))
sultana@55596
  1677
  THEN REPEAT_DETERM (HEADGOAL (etac @{thm exE}))
sultana@55596
  1678
  THEN HEADGOAL (canonicalise_qtfr_order ctxt)
sultana@55596
  1679
  THEN
sultana@55596
  1680
    ((REPEAT (HEADGOAL (nominal_inst_parametermatch_tac ctxt @{thm allE})))
sultana@55596
  1681
     APPEND (REPEAT (HEADGOAL (inst_parametermatch_tac ctxt [@{thm allE}]))))
sultana@55596
  1682
  (*FIXME need to handle "@{thm exI}"?*)
sultana@55596
  1683
sultana@55596
  1684
(*difference in constants between the hypothesis clause and the conclusion clause*)
sultana@55596
  1685
fun clause_consts_diff thm =
sultana@55596
  1686
  let
sultana@55596
  1687
    val t =
sultana@55596
  1688
      prop_of thm
sultana@55596
  1689
      |> Logic.dest_implies
sultana@55596
  1690
      |> fst
sultana@55596
  1691
sultana@55596
  1692
      (*This bit should not be needed, since Leo2 inferences don't have parameters*)
sultana@55596
  1693
      |> TPTP_Reconstruct.strip_top_all_vars []
sultana@55596
  1694
      |> snd
sultana@55596
  1695
sultana@55596
  1696
    val do_diff =
sultana@55596
  1697
      Logic.dest_implies
sultana@55596
  1698
      #> uncurry TPTP_Reconstruct.new_consts_between
sultana@55596
  1699
      #> filter
sultana@55596
  1700
           (fn Const (n, _) =>
sultana@55596
  1701
             not (member (op =) interpreted_consts n))
sultana@55596
  1702
  in
sultana@55596
  1703
    if head_of t = Logic.implies then do_diff t
sultana@55596
  1704
    else []
sultana@55596
  1705
  end
sultana@55596
  1706
*}
sultana@55596
  1707
sultana@55596
  1708
ML {*
sultana@55596
  1709
(*remove quantification in hypothesis clause (! X. t), if
sultana@55596
  1710
  X not free in t*)
sultana@55596
  1711
fun remove_redundant_quantification ctxt i = fn st =>
sultana@55596
  1712
  let
sultana@55596
  1713
    val gls =
sultana@55596
  1714
      prop_of st
sultana@55596
  1715
      |> Logic.strip_horn
sultana@55596
  1716
      |> fst
sultana@55596
  1717
  in
sultana@55596
  1718
    if null gls then raise NO_GOALS
sultana@55596
  1719
    else
sultana@55596
  1720
      let
sultana@55596
  1721
        val (params, (hyp_clauses, conc_clause)) =
sultana@55596
  1722
          rpair (i - 1) gls
sultana@55596
  1723
          |> uncurry nth
sultana@55596
  1724
          |> TPTP_Reconstruct.strip_top_all_vars []
sultana@55596
  1725
          |> apsnd Logic.strip_horn
sultana@55596
  1726
      in
sultana@55596
  1727
        (*this is to fail gracefully in case this tactic is applied to a goal which doesn't have a single hypothesis*)
sultana@55596
  1728
        if length hyp_clauses > 1 then no_tac st
sultana@55596
  1729
        else
sultana@55596
  1730
          let
sultana@55596
  1731
            val hyp_clause = the_single hyp_clauses
sultana@55596
  1732
            val sep_prefix =
sultana@55596
  1733
              HOLogic.dest_Trueprop
sultana@55596
  1734
              #> TPTP_Reconstruct.strip_top_All_vars
sultana@55596
  1735
              #> apfst rev
sultana@55596
  1736
            val (hyp_prefix, hyp_body) = sep_prefix hyp_clause
sultana@55596
  1737
            val (conc_prefix, conc_body) = sep_prefix conc_clause
sultana@55596
  1738
          in
sultana@55596
  1739
            if null hyp_prefix orelse
sultana@55596
  1740
              member (op =) conc_prefix (hd hyp_prefix) orelse
sultana@55596
  1741
              member (op =)  (Term.add_frees hyp_body []) (hd hyp_prefix) then
sultana@55596
  1742
              no_tac st
sultana@55596
  1743
            else
sultana@55596
  1744
              eres_inst_tac ctxt [(("x", 0), "(@X. False)")] @{thm allE} i st
sultana@55596
  1745
          end
sultana@55596
  1746
     end
sultana@55596
  1747
  end
sultana@55596
  1748
*}
sultana@55596
  1749
sultana@55596
  1750
ML {*
sultana@55596
  1751
fun remove_redundant_quantification_ignore_skolems ctxt i =
sultana@55596
  1752
  COND (TERMPRED (fn _ => true) conc_is_skolem_def (SOME i))
sultana@55596
  1753
    no_tac
sultana@55596
  1754
    (remove_redundant_quantification ctxt i)
sultana@55596
  1755
*}
sultana@55596
  1756
sultana@55596
  1757
lemma drop_redundant_literal_qtfr:
sultana@55596
  1758
  "(! X. P) = True \<Longrightarrow> P = True"
sultana@55596
  1759
  "(? X. P) = True \<Longrightarrow> P = True"
sultana@55596
  1760
  "(! X. P) = False \<Longrightarrow> P = False"
sultana@55596
  1761
  "(? X. P) = False \<Longrightarrow> P = False"
sultana@55596
  1762
by auto
sultana@55596
  1763
sultana@55596
  1764
ML {*
sultana@55596
  1765
(*remove quantification in the literal "(! X. t) = True/False"
sultana@55596
  1766
  in the singleton hypothesis clause, if X not free in t*)
sultana@55596
  1767
fun remove_redundant_quantification_in_lit ctxt i = fn st =>
sultana@55596
  1768
  let
sultana@55596
  1769
    val gls =
sultana@55596
  1770
      prop_of st
sultana@55596
  1771
      |> Logic.strip_horn
sultana@55596
  1772
      |> fst
sultana@55596
  1773
  in
sultana@55596
  1774
    if null gls then raise NO_GOALS
sultana@55596
  1775
    else
sultana@55596
  1776
      let
sultana@55596
  1777
        val (params, (hyp_clauses, conc_clause)) =
sultana@55596
  1778
          rpair (i - 1) gls
sultana@55596
  1779
          |> uncurry nth
sultana@55596
  1780
          |> TPTP_Reconstruct.strip_top_all_vars []
sultana@55596
  1781
          |> apsnd Logic.strip_horn
sultana@55596
  1782
      in
sultana@55596
  1783
        (*this is to fail gracefully in case this tactic is applied to a goal which doesn't have a single hypothesis*)
sultana@55596
  1784
        if length hyp_clauses > 1 then no_tac st
sultana@55596
  1785
        else
sultana@55596
  1786
          let
sultana@55596
  1787
            fun literal_content (Const (@{const_name HOL.eq}, _) $ lhs $ (rhs as @{term True})) = SOME (lhs, rhs)
sultana@55596
  1788
              | literal_content (Const (@{const_name HOL.eq}, _) $ lhs $ (rhs as @{term False})) = SOME (lhs, rhs)
sultana@55596
  1789
              | literal_content t = NONE
sultana@55596
  1790
sultana@55596
  1791
            val hyp_clause =
sultana@55596
  1792
              the_single hyp_clauses
sultana@55596
  1793
              |> HOLogic.dest_Trueprop
sultana@55596
  1794
              |> literal_content
sultana@55596
  1795
sultana@55596
  1796
          in
sultana@55596
  1797
            if is_none hyp_clause then
sultana@55596
  1798
              no_tac st
sultana@55596
  1799
            else
sultana@55596
  1800
              let
sultana@55596
  1801
                val (hyp_lit_prefix, hyp_lit_body) =
sultana@55596
  1802
                  the hyp_clause
sultana@55596
  1803
                  |> (fn (t, polarity) =>
sultana@55596
  1804
                       TPTP_Reconstruct.strip_top_All_vars t
sultana@55596
  1805
                       |> apfst rev)
sultana@55596
  1806
              in
sultana@55596
  1807
                if null hyp_lit_prefix orelse
sultana@55596
  1808
                  member (op =)  (Term.add_frees hyp_lit_body []) (hd hyp_lit_prefix) then
sultana@55596
  1809
                  no_tac st
sultana@55596
  1810
                else
sultana@55596
  1811
                  dresolve_tac @{thms drop_redundant_literal_qtfr} i st
sultana@55596
  1812
              end
sultana@55596
  1813
          end
sultana@55596
  1814
     end
sultana@55596
  1815
  end
sultana@55596
  1816
*}
sultana@55596
  1817
sultana@55596
  1818
ML {*
sultana@55596
  1819
fun remove_redundant_quantification_in_lit_ignore_skolems ctxt i =
sultana@55596
  1820
  COND (TERMPRED (fn _ => true) conc_is_skolem_def (SOME i))
sultana@55596
  1821
    no_tac
sultana@55596
  1822
    (remove_redundant_quantification_in_lit ctxt i)
sultana@55596
  1823
*}
sultana@55596
  1824
sultana@55596
  1825
ML {*
sultana@55596
  1826
fun extcnf_combined_tac ctxt prob_name_opt feats skolem_consts = fn st =>
sultana@55596
  1827
  let
sultana@55596
  1828
    val thy = Proof_Context.theory_of ctxt
sultana@55596
  1829
sultana@55596
  1830
    (*Initially, st consists of a single goal, showing the
sultana@55596
  1831
      hypothesis clause implying the conclusion clause.
sultana@55596
  1832
      There are no parameters.*)
sultana@55596
  1833
    val consts_diff =
sultana@55596
  1834
      union (op =) skolem_consts
sultana@55596
  1835
       (if can_feature ConstsDiff feats then
sultana@55596
  1836
          clause_consts_diff st
sultana@55596
  1837
        else [])
sultana@55596
  1838
sultana@55596
  1839
    val main_tac =
sultana@55596
  1840
      if can_feature (LoopOnce []) feats orelse can_feature (InnerLoopOnce []) feats then
sultana@55596
  1841
        extcnf_combined_main ctxt feats consts_diff
sultana@55596
  1842
      else if can_feature (Loop []) feats then
sultana@55596
  1843
        BEST_FIRST (TERMPRED (fn _ => true) conc_is_skolem_def NONE, size_of_thm)
sultana@55596
  1844
(*FIXME maybe need to weaken predicate to include "solved form"?*)
sultana@55596
  1845
         (extcnf_combined_main ctxt feats consts_diff)
sultana@55596
  1846
      else all_tac (*to allow us to use the cleaning features*)
sultana@55596
  1847
sultana@55596
  1848
    (*Remove hypotheses from Skolem definitions,
sultana@55596
  1849
      then remove duplicate subgoals,
sultana@55596
  1850
      then we should be left with skolem definitions:
sultana@55596
  1851
        absorb them as axioms into the theory.*)
sultana@55596
  1852
    val cleanup =
sultana@55596
  1853
      cleanup_skolem_defs feats
sultana@55596
  1854
      THEN remove_duplicates_tac feats
sultana@55596
  1855
      THEN (if can_feature AbsorbSkolemDefs feats then
sultana@55596
  1856
              ALLGOALS (absorb_skolem_def ctxt prob_name_opt)
sultana@55596
  1857
            else all_tac)
sultana@55596
  1858
sultana@55596
  1859
    val have_loop_feats =
sultana@55596
  1860
      (get_loop_feats feats; true)
sultana@55596
  1861
      handle NO_LOOP_FEATS => false
sultana@55596
  1862
sultana@55596
  1863
    val tec =
sultana@55596
  1864
      (if can_feature StripQuantifiers feats then
sultana@55596
  1865
         (REPEAT (CHANGED (strip_qtfrs_tac ctxt)))
sultana@55596
  1866
       else all_tac)
sultana@55596
  1867
      THEN (if can_feature Flip_Conclusion feats then
sultana@55596
  1868
             HEADGOAL (flip_conclusion_tac ctxt)
sultana@55596
  1869
           else all_tac)
sultana@55596
  1870
sultana@55596
  1871
      (*after stripping the quantifiers any remaining quantifiers
sultana@55596
  1872
        can be simply eliminated -- they're redundant*)
sultana@55596
  1873
      (*FIXME instead of just using allE, instantiate to a silly
sultana@55596
  1874
         term, to remove opportunities for unification.*)
sultana@55596
  1875
      THEN (REPEAT_DETERM (etac @{thm allE} 1))
sultana@55596
  1876
sultana@55596
  1877
      THEN (REPEAT_DETERM (rtac @{thm allI} 1))
sultana@55596
  1878
sultana@55596
  1879
      THEN (if have_loop_feats then
sultana@55596
  1880
              REPEAT (CHANGED
sultana@55596
  1881
              ((ALLGOALS (TRY o clause_breaker)) (*brush away literals which don't change*)
sultana@55596
  1882
               THEN
sultana@55596
  1883
                (*FIXME move this to a different level?*)
sultana@55596
  1884
                (if loop_can_feature [Polarity_switch] feats then
sultana@55596
  1885
                   all_tac
sultana@55596
  1886
                 else
sultana@55596
  1887
                   (TRY (IF_UNSOLVED (HEADGOAL (remove_redundant_quantification_ignore_skolems ctxt))))
sultana@55596
  1888
                   THEN (TRY (IF_UNSOLVED (HEADGOAL (remove_redundant_quantification_in_lit_ignore_skolems ctxt)))))
sultana@55596
  1889
               THEN (TRY main_tac)))
sultana@55596
  1890
            else
sultana@55596
  1891
              all_tac)
sultana@55596
  1892
      THEN IF_UNSOLVED cleanup
sultana@55596
  1893
sultana@55596
  1894
  in
sultana@55596
  1895
    DEPTH_SOLVE (CHANGED tec) st
sultana@55596
  1896
  end
sultana@55596
  1897
*}
sultana@55596
  1898
sultana@55596
  1899
sultana@55596
  1900
subsubsection "unfold_def"
sultana@55596
  1901
sultana@55596
  1902
(*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
  1903
lemma drop_first_hypothesis [rule_format]: "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B" by auto
sultana@55596
  1904
sultana@55596
  1905
(*Unfold_def works by reducing the goal to a meta equation,
sultana@55596
  1906
  then working on it until it can be discharged by atac,
sultana@55596
  1907
  or reflexive, or else turned back into an object equation
sultana@55596
  1908
  and broken down further.*)
sultana@55596
  1909
lemma un_meta_polarise: "(X \<equiv> True) \<Longrightarrow> X" by auto
sultana@55596
  1910
lemma meta_polarise: "X \<Longrightarrow> X \<equiv> True" by auto
sultana@55596
  1911
sultana@55596
  1912
ML {*
sultana@55596
  1913
fun unfold_def_tac ctxt depends_on_defs = fn st =>
sultana@55596
  1914
  let
sultana@55596
  1915
    (*This is used when we end up with something like
sultana@55596
  1916
        (A & B) \<equiv> True \<Longrightarrow> (B & A) \<equiv> True.
sultana@55596
  1917
      It breaks down this subgoal until it can be trivially
sultana@55596
  1918
      discharged.
sultana@55596
  1919
     *)
sultana@55596
  1920
    val kill_meta_eqs_tac =
sultana@55596
  1921
      dtac @{thm un_meta_polarise}
sultana@55596
  1922
      THEN' rtac @{thm meta_polarise}
sultana@55596
  1923
      THEN' (REPEAT_DETERM o (etac @{thm conjE}))
sultana@55596
  1924
      THEN' (REPEAT_DETERM o (rtac @{thm conjI} ORELSE' atac))
sultana@55596
  1925
sultana@55596
  1926
    val continue_reducing_tac =
sultana@55596
  1927
      rtac @{thm meta_eq_to_obj_eq} 1
sultana@55596
  1928
      THEN (REPEAT_DETERM (ex_expander_tac ctxt 1))
sultana@55596
  1929
      THEN TRY (polarise_subgoal_hyps 1) (*no need to REPEAT_DETERM here, since there should only be one hypothesis*)
sultana@55596
  1930
      THEN TRY (dtac @{thm eq_reflection} 1)
sultana@55596
  1931
      THEN (TRY ((CHANGED o rewrite_goal_tac ctxt
sultana@55596
  1932
              (@{thm expand_iff} :: @{thms simp_meta})) 1))
sultana@55596
  1933
      THEN HEADGOAL (rtac @{thm reflexive}
sultana@55596
  1934
                     ORELSE' atac
sultana@55596
  1935
                     ORELSE' kill_meta_eqs_tac)
sultana@55596
  1936
sultana@55596
  1937
    val tectic =
sultana@55596
  1938
      (rtac @{thm polarise} 1 THEN atac 1)
sultana@55596
  1939
      ORELSE
sultana@55596
  1940
        (REPEAT_DETERM (etac @{thm conjE} 1 THEN etac @{thm drop_first_hypothesis} 1)
sultana@55596
  1941
         THEN PRIMITIVE (Conv.fconv_rule Drule.eta_long_conversion)
sultana@55596
  1942
         THEN (REPEAT_DETERM (ex_expander_tac ctxt 1))
sultana@55596
  1943
         THEN (TRY ((CHANGED o rewrite_goal_tac ctxt @{thms simp_meta}) 1))
sultana@55596
  1944
         THEN PRIMITIVE (Conv.fconv_rule Drule.eta_long_conversion)
sultana@55596
  1945
         THEN
sultana@55596
  1946
           (HEADGOAL atac
sultana@55596
  1947
           ORELSE
sultana@55596
  1948
            (unfold_tac ctxt depends_on_defs
sultana@55596
  1949
             THEN IF_UNSOLVED continue_reducing_tac)))
sultana@55596
  1950
  in
sultana@55596
  1951
    tectic st
sultana@55596
  1952
  end
sultana@55596
  1953
*}
sultana@55596
  1954
sultana@55596
  1955
sultana@55596
  1956
subsection "Handling split 'preprocessing'"
sultana@55596
  1957
sultana@55596
  1958
lemma split_tranfs:
sultana@55596
  1959
  "! x. P x & Q x \<equiv> (! x. P x) & (! x. Q x)"
sultana@55596
  1960
  "~ (~ A) \<equiv> A"
sultana@55596
  1961
  "? x. A \<equiv> A"
sultana@55596
  1962
  "(A & B) & C \<equiv> A & B & C"
sultana@55596
  1963
  "A = B \<equiv> (A --> B) & (B --> A)"
sultana@55596
  1964
by (rule eq_reflection, auto)+
sultana@55596
  1965
sultana@55596
  1966
(*Same idiom as ex_expander_tac*)
sultana@55596
  1967
ML {*
sultana@55596
  1968
fun split_simp_tac (ctxt : Proof.context) i =
sultana@55596
  1969
   let
sultana@55596
  1970
     val simpset =
sultana@55596
  1971
       fold Simplifier.add_simp @{thms split_tranfs} (empty_simpset ctxt)
sultana@55596
  1972
   in
sultana@55596
  1973
     CHANGED (asm_full_simp_tac simpset i)
sultana@55596
  1974
   end
sultana@55596
  1975
*}
sultana@55596
  1976
sultana@55596
  1977
sultana@55596
  1978
subsection "Alternative reconstruction tactics"
sultana@55596
  1979
ML {*
sultana@55596
  1980
(*An "auto"-based proof reconstruction, where we attempt to reconstruct each inference
sultana@55596
  1981
  using auto_tac. A realistic tactic would inspect the inference name and act
sultana@55596
  1982
  accordingly.*)
sultana@55596
  1983
fun auto_based_reconstruction_tac ctxt prob_name n =
sultana@55596
  1984
  let
sultana@55596
  1985
    val thy = Proof_Context.theory_of ctxt
sultana@55596
  1986
    val pannot = TPTP_Reconstruct.get_pannot_of_prob thy prob_name
sultana@55596
  1987
  in
sultana@55596
  1988
    TPTP_Reconstruct.inference_at_node
sultana@55596
  1989
     thy
sultana@55596
  1990
     prob_name (#meta pannot) n
sultana@55596
  1991
      |> the
sultana@55596
  1992
      |> (fn {inference_fmla, ...} =>
sultana@55596
  1993
          Goal.prove ctxt [] [] inference_fmla
sultana@55596
  1994
           (fn pdata => auto_tac (#context pdata)))
sultana@55596
  1995
  end
sultana@55596
  1996
*}
sultana@55596
  1997
sultana@55596
  1998
(*An oracle-based reconstruction, which is only used to test the shunting part of the system*)
sultana@55596
  1999
oracle oracle_iinterp = "fn t => t"
sultana@55596
  2000
ML {*
sultana@55596
  2001
fun oracle_based_reconstruction_tac ctxt prob_name n =
sultana@55596
  2002
  let
sultana@55596
  2003
    val thy = Proof_Context.theory_of ctxt
sultana@55596
  2004
    val pannot = TPTP_Reconstruct.get_pannot_of_prob thy prob_name
sultana@55596
  2005
  in
sultana@55596
  2006
    TPTP_Reconstruct.inference_at_node
sultana@55596
  2007
     thy
sultana@55596
  2008
     prob_name (#meta pannot) n
sultana@55596
  2009
      |> the
sultana@55596
  2010
      |> (fn {inference_fmla, ...} => cterm_of thy inference_fmla)
sultana@55596
  2011
      |> oracle_iinterp
sultana@55596
  2012
  end
sultana@55596
  2013
*}
sultana@55596
  2014
sultana@55596
  2015
sultana@55596
  2016
subsection "Leo2 reconstruction tactic"
sultana@55596
  2017
sultana@55596
  2018
ML {*
sultana@55596
  2019
exception UNSUPPORTED_ROLE
sultana@55596
  2020
exception INTERPRET_INFERENCE
sultana@55596
  2021
sultana@55596
  2022
(*Failure reports can be adjusted to avoid interrupting
sultana@55596
  2023
  an overall reconstruction process*)
sultana@55596
  2024
fun fail ctxt x =
sultana@55596
  2025
  if unexceptional_reconstruction ctxt then
sultana@55596
  2026
    (warning x; raise INTERPRET_INFERENCE)
sultana@55596
  2027
  else error x
sultana@55596
  2028
sultana@55596
  2029
fun interpret_leo2_inference_tac ctxt prob_name node =
sultana@55596
  2030
  let
sultana@55596
  2031
    val thy = Proof_Context.theory_of ctxt
sultana@55596
  2032
sultana@55596
  2033
    val _ =
sultana@55596
  2034
      if Config.get ctxt tptp_trace_reconstruction then
sultana@55596
  2035
        tracing ("interpret_inference reconstructing node" ^ node ^ " of " ^ TPTP_Problem_Name.mangle_problem_name prob_name)
sultana@55596
  2036
      else ()
sultana@55596
  2037
sultana@55596
  2038
    val pannot = TPTP_Reconstruct.get_pannot_of_prob thy prob_name
sultana@55596
  2039
sultana@55596
  2040
    fun nonfull_extcnf_combined_tac feats =
sultana@55596
  2041
      extcnf_combined_tac ctxt (SOME prob_name)
sultana@55596
  2042
       [ConstsDiff,
sultana@55596
  2043
        StripQuantifiers,
sultana@55596
  2044
        InnerLoopOnce (Break_Hypotheses :: (*FIXME RemoveRedundantQuantifications :: *) feats),
sultana@55596
  2045
        AbsorbSkolemDefs]
sultana@55596
  2046
       []
sultana@55596
  2047
sultana@55596
  2048
    val source_inf_opt =
sultana@55596
  2049
      AList.lookup (op =) (#meta pannot)
sultana@55596
  2050
      #> the
sultana@55596
  2051
      #> #source_inf_opt
sultana@55596
  2052
sultana@55596
  2053
    (*FIXME integrate this with other lookup code, or in the early analysis*)
sultana@55596
  2054
    local
sultana@55596
  2055
      fun node_is_of_role role node =
sultana@55596
  2056
        AList.lookup (op =) (#meta pannot) node |> the
sultana@55596
  2057
        |> #role
sultana@55596
  2058
        |> (fn role' => role = role')
sultana@55596
  2059
sultana@55596
  2060
      fun roled_dependencies_names role =
sultana@55596
  2061
        let
sultana@55596
  2062
          fun values () =
sultana@55596
  2063
            case role of
sultana@55596
  2064
                TPTP_Syntax.Role_Definition =>
sultana@55596
  2065
                  map (apsnd Binding.dest) (#defs pannot)
sultana@55596
  2066
              | TPTP_Syntax.Role_Axiom =>
sultana@55596
  2067
                  map (apsnd Binding.dest) (#axs pannot)
sultana@55596
  2068
              | _ => raise UNSUPPORTED_ROLE
sultana@55596
  2069
          in
sultana@55596
  2070
            if is_none (source_inf_opt node) then []
sultana@55596
  2071
            else
sultana@55596
  2072
              case the (source_inf_opt node) of
sultana@55596
  2073
                  TPTP_Proof.Inference (_, _, parent_inf) =>
sultana@55596
  2074
                    List.map TPTP_Proof.parent_name parent_inf
sultana@55596
  2075
                    |> List.filter (node_is_of_role role)
sultana@55596
  2076
                    |> (*FIXME currently definitions are not
sultana@55596
  2077
                         included in the proof annotations, so
sultana@55596
  2078
                         i'm using all the definitions available
sultana@55596
  2079
                         in the proof. ideally i should only
sultana@55596
  2080
                         use the ones in the proof annotation.*)
sultana@55596
  2081
                       (fn x =>
sultana@55596
  2082
                         if role = TPTP_Syntax.Role_Definition then
sultana@55596
  2083
                           let fun values () = map (apsnd Binding.dest) (#defs pannot)
sultana@55596
  2084
                           in
sultana@55596
  2085
                             map snd (values ())
sultana@55596
  2086
                           end
sultana@55596
  2087
                         else
sultana@55596
  2088
                         map (fn node => AList.lookup (op =) (values ()) node |> the) x)
sultana@55596
  2089
                | _ => []
sultana@55596
  2090
         end
sultana@55596
  2091
sultana@55596
  2092
      val roled_dependencies =
sultana@55596
  2093
        roled_dependencies_names
sultana@55596
  2094
        #> map (#3 #> Global_Theory.get_thm thy)
sultana@55596
  2095
    in
sultana@55596
  2096
      val depends_on_defs = roled_dependencies TPTP_Syntax.Role_Definition
sultana@55596
  2097
      val depends_on_axs = roled_dependencies TPTP_Syntax.Role_Axiom
sultana@55596
  2098
      val depends_on_defs_names = roled_dependencies_names TPTP_Syntax.Role_Definition
sultana@55596
  2099
    end
sultana@55596
  2100
sultana@55596
  2101
    fun get_binds source_inf_opt =
sultana@55596
  2102
      case the source_inf_opt of
sultana@55596
  2103
          TPTP_Proof.Inference (_, _, parent_inf) =>
sultana@55596
  2104
            List.map
sultana@55596
  2105
              (fn TPTP_Proof.Parent _ => []
sultana@55596
  2106
                | TPTP_Proof.ParentWithDetails (_, parent_details) => parent_details)
sultana@55596
  2107
              parent_inf
sultana@55596
  2108
            |> List.concat
sultana@55596
  2109
        | _ => []
sultana@55596
  2110
sultana@55596
  2111
    val inference_name =
sultana@55596
  2112
      case TPTP_Reconstruct.inference_at_node thy prob_name (#meta pannot) node of
sultana@55596
  2113
          NONE => fail ctxt "Cannot reconstruct rule: no information"
sultana@55596
  2114
        | SOME {inference_name, ...} => inference_name
sultana@55596
  2115
    val default_tac = HEADGOAL (blast_tac ctxt)
sultana@55596
  2116
  in
sultana@55596
  2117
    case inference_name of
sultana@55596
  2118
      "fo_atp_e" =>
sultana@55596
  2119
        HEADGOAL (etac (oracle_based_reconstruction_tac ctxt prob_name node))
sultana@55596
  2120
    | "copy" =>
sultana@55596
  2121
         HEADGOAL
sultana@55596
  2122
          (atac
sultana@55596
  2123
           ORELSE'
sultana@55596
  2124
              (rtac @{thm polarise}
sultana@55596
  2125
               THEN' atac))
sultana@55596
  2126
    | "polarity_switch" => nonfull_extcnf_combined_tac [Polarity_switch]
sultana@55596
  2127
    | "solved_all_splits" => solved_all_splits_tac
sultana@55596
  2128
    | "extcnf_not_pos" => nonfull_extcnf_combined_tac [Not_pos]
sultana@55596
  2129
    | "extcnf_forall_pos" => nonfull_extcnf_combined_tac [Universal]
sultana@55596
  2130
    | "negate_conjecture" => fail ctxt "Should not handle negate_conjecture here"
sultana@55596
  2131
    | "unfold_def" => unfold_def_tac ctxt depends_on_defs
sultana@55596
  2132
    | "extcnf_not_neg" => nonfull_extcnf_combined_tac [Not_neg]
sultana@55596
  2133
    | "extcnf_or_neg" => nonfull_extcnf_combined_tac [Or_neg]
sultana@55596
  2134
    | "extcnf_equal_pos" => nonfull_extcnf_combined_tac [Equal_pos]
sultana@55596
  2135
    | "extcnf_equal_neg" => nonfull_extcnf_combined_tac [Equal_neg]
sultana@55596
  2136
    | "extcnf_forall_special_pos" =>
sultana@55596
  2137
         nonfull_extcnf_combined_tac [Forall_special_pos]
sultana@55596
  2138
         ORELSE HEADGOAL (blast_tac ctxt)
sultana@55596
  2139
    | "extcnf_or_pos" => nonfull_extcnf_combined_tac [Or_pos]
sultana@55596
  2140
    | "extuni_bool2" => nonfull_extcnf_combined_tac [Extuni_Bool2]
sultana@55596
  2141
    | "extuni_bool1" => nonfull_extcnf_combined_tac [Extuni_Bool1]
sultana@55596
  2142
    | "extuni_dec" =>
sultana@55596
  2143
        HEADGOAL atac
sultana@55596
  2144
        ORELSE nonfull_extcnf_combined_tac [Extuni_Dec]
sultana@55596
  2145
    | "extuni_bind" => nonfull_extcnf_combined_tac [Extuni_Bind]
sultana@55596
  2146
    | "extuni_triv" => nonfull_extcnf_combined_tac [Extuni_Triv]
sultana@55596
  2147
    | "extuni_flex_rigid" => nonfull_extcnf_combined_tac [Extuni_FlexRigid]
sultana@55596
  2148
    | "prim_subst" => nonfull_extcnf_combined_tac [Assumption]
sultana@55596
  2149
    | "bind" =>
sultana@55596
  2150
        let
sultana@55596
  2151
          val ordered_binds = get_binds (source_inf_opt node)
sultana@55596
  2152
        in
sultana@55596
  2153
          bind_tac ctxt prob_name ordered_binds
sultana@55596
  2154
        end
sultana@55596
  2155
    | "standard_cnf" => HEADGOAL (standard_cnf_tac ctxt)
sultana@55596
  2156
    | "extcnf_forall_neg" =>
sultana@55596
  2157
        nonfull_extcnf_combined_tac
sultana@55596
  2158
         [Existential_Var(* , RemoveRedundantQuantifications *)] (*FIXME RemoveRedundantQuantifications*)
sultana@55596
  2159
    | "extuni_func" =>
sultana@55596
  2160
        nonfull_extcnf_combined_tac [Extuni_Func, Existential_Var]
sultana@55596
  2161
    | "replace_leibnizEQ" => nonfull_extcnf_combined_tac [Assumption]
sultana@55596
  2162
    | "replace_andrewsEQ" => nonfull_extcnf_combined_tac [Assumption]
sultana@55596
  2163
    | "split_preprocessing" =>
sultana@55596
  2164
         (REPEAT (HEADGOAL (split_simp_tac ctxt)))
sultana@55596
  2165
         THEN TRY (PRIMITIVE (Conv.fconv_rule Drule.eta_long_conversion))
sultana@55596
  2166
         THEN HEADGOAL atac
sultana@55596
  2167
sultana@55596
  2168
    (*FIXME some of these could eventually be handled specially*)
sultana@55596
  2169
    | "fac_restr" => default_tac
sultana@55596
  2170
    | "sim" => default_tac
sultana@55596
  2171
    | "res" => default_tac
sultana@55596
  2172
    | "rename" => default_tac
sultana@55596
  2173
    | "flexflex" => default_tac
sultana@55596
  2174
    | other => fail ctxt ("Unknown inference rule: " ^ other)
sultana@55596
  2175
  end
sultana@55596
  2176
*}
sultana@55596
  2177
sultana@55596
  2178
ML {*
sultana@55596
  2179
fun interpret_leo2_inference ctxt prob_name node =
sultana@55596
  2180
  let
sultana@55596
  2181
    val thy = Proof_Context.theory_of ctxt
sultana@55596
  2182
    val pannot = TPTP_Reconstruct.get_pannot_of_prob thy prob_name
sultana@55596
  2183
sultana@55596
  2184
    val (inference_name, inference_fmla) =
sultana@55596
  2185
      case TPTP_Reconstruct.inference_at_node thy prob_name (#meta pannot) node of
sultana@55596
  2186
          NONE => fail ctxt "Cannot reconstruct rule: no information"
sultana@55596
  2187
        | SOME {inference_name, inference_fmla, ...} =>
sultana@55596
  2188
            (inference_name, inference_fmla)
sultana@55596
  2189
sultana@55596
  2190
    val proof_outcome =
sultana@55596
  2191
      let
sultana@55596
  2192
        fun prove () =
sultana@55596
  2193
          Goal.prove ctxt [] [] inference_fmla
sultana@55596
  2194
           (fn pdata => interpret_leo2_inference_tac
sultana@55596
  2195
            (#context pdata) prob_name node)
sultana@55596
  2196
      in
sultana@55596
  2197
        if informative_failure ctxt then SOME (prove ())
sultana@55596
  2198
        else try prove ()
sultana@55596
  2199
      end
sultana@55596
  2200
sultana@55596
  2201
  in case proof_outcome of
sultana@55596
  2202
      NONE => fail ctxt (Pretty.string_of
sultana@55596
  2203
        (Pretty.block
sultana@55596
  2204
          [Pretty.str ("Failed inference reconstruction for '" ^
sultana@55596
  2205
            inference_name ^ "' at node " ^ node ^ ":\n"),
sultana@55596
  2206
           Syntax.pretty_term ctxt inference_fmla]))
sultana@55596
  2207
    | SOME thm => thm
sultana@55596
  2208
  end
sultana@55596
  2209
*}
sultana@55596
  2210
sultana@55596
  2211
ML {*
sultana@55596
  2212
(*filter a set of nodes based on which inference rule was used to
sultana@55596
  2213
  derive a node*)
sultana@55596
  2214
fun nodes_by_inference (fms : TPTP_Reconstruct.formula_meaning list) inference_rule =
sultana@55596
  2215
  let
sultana@55596
  2216
    fun fold_fun n l =
sultana@55596
  2217
      case TPTP_Reconstruct.node_info fms #source_inf_opt n of
sultana@55596
  2218
          NONE => l
sultana@55596
  2219
        | SOME (TPTP_Proof.File _) => l
sultana@55596
  2220
        | SOME (TPTP_Proof.Inference (rule_name, _, _)) =>
sultana@55596
  2221
            if rule_name = inference_rule then n :: l
sultana@55596
  2222
            else l
sultana@55596
  2223
  in
sultana@55596
  2224
    fold fold_fun (map fst fms) []
sultana@55596
  2225
  end
sultana@55596
  2226
*}
sultana@55596
  2227
sultana@55597
  2228
sultana@55597
  2229
section "Importing proofs and reconstructing theorems"
sultana@55597
  2230
sultana@55596
  2231
ML {*
sultana@55597
  2232
(*Preprocessing carried out on a LEO-II proof.*)
sultana@55596
  2233
fun leo2_on_load (pannot : TPTP_Reconstruct.proof_annotation) thy =
sultana@55596
  2234
  let
sultana@55596
  2235
    val ctxt = Proof_Context.init_global thy
sultana@55596
  2236
    val dud = ("", Binding.empty, @{term False})
sultana@55596
  2237
    val pre_skolem_defs =
sultana@55596
  2238
      nodes_by_inference (#meta pannot) "extcnf_forall_neg" @
sultana@55596
  2239
       nodes_by_inference (#meta pannot) "extuni_func"
sultana@55596
  2240
      |> map (fn x =>
sultana@55596
  2241
              (interpret_leo2_inference ctxt (#problem_name pannot) x; dud)
sultana@55596
  2242
               handle NO_SKOLEM_DEF (s, bnd, t) => (s, bnd, t))
sultana@55596
  2243
      |> filter (fn (x, _, _) => x <> "") (*In case no skolem constants were introduced in that inference*)
sultana@55596
  2244
    val skolem_defs = map (fn (x, y, _) => (x, y)) pre_skolem_defs
sultana@55596
  2245
    val thy' =
sultana@55596
  2246
      fold (fn skolem_def => fn thy =>
sultana@55596
  2247
             let
sultana@55596
  2248
               val ((s, thm), thy') = Thm.add_axiom_global skolem_def thy
sultana@55596
  2249
               (* val _ = warning ("Added skolem definition " ^ s ^ ": " ^  @{make_string thm}) *) (*FIXME use of make_string*)
sultana@55596
  2250
             in thy' end)
sultana@55596
  2251
       (map (fn (_, y, z) => (y, z)) pre_skolem_defs)
sultana@55596
  2252
       thy
sultana@55596
  2253
  in
sultana@55596
  2254
    ({problem_name = #problem_name pannot,
sultana@55596
  2255
      skolem_defs = skolem_defs,
sultana@55596
  2256
      defs = #defs pannot,
sultana@55596
  2257
      axs = #axs pannot,
sultana@55596
  2258
      meta = #meta pannot},
sultana@55596
  2259
     thy')
sultana@55596
  2260
  end
sultana@55596
  2261
*}
sultana@55596
  2262
sultana@55597
  2263
ML {*
sultana@55597
  2264
(*Imports and reconstructs a LEO-II proof.*)
sultana@55597
  2265
fun reconstruct_leo2 path thy =
sultana@55597
  2266
  let
sultana@55597
  2267
    val prob_file = Path.base path
sultana@55597
  2268
    val dir = Path.dir path
sultana@55597
  2269
    val thy' = TPTP_Reconstruct.import_thm true [dir, prob_file] path leo2_on_load thy
sultana@55597
  2270
    val ctxt =
sultana@55597
  2271
      Context.Theory thy'
sultana@55597
  2272
      |> Context.proof_of
sultana@55597
  2273
    val prob_name =
sultana@55597
  2274
      Path.implode prob_file
sultana@55597
  2275
      |> TPTP_Problem_Name.parse_problem_name
sultana@55597
  2276
    val theorem =
sultana@55597
  2277
      TPTP_Reconstruct.reconstruct ctxt
sultana@55597
  2278
       (TPTP_Reconstruct.naive_reconstruct_tac ctxt interpret_leo2_inference)
sultana@55597
  2279
       prob_name
sultana@55597
  2280
  in
sultana@55597
  2281
    (*NOTE we could return the theorem value alone, since
sultana@55597
  2282
       users could get the thy value from the thm value.*)
sultana@55597
  2283
    (thy', theorem)
sultana@55597
  2284
  end
sultana@55597
  2285
*}
sultana@55597
  2286
sultana@55596
  2287
end