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