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