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