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