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