(*  Title:      test/HOL/Tools/Sledgehammer/Try_Sledgehammer.thy

    Author:     Florian Kammüller, Cambridge University Computer Laboratory

*)

theory Try_Sledgehammer

  imports 

    (** )Main "HOL-Library.FuncSet"( *..for HOL/Metis_Examples/Tarski.thy*)

    (** )HOL.Real "HOL-Library.Quotient_Product"( *..for HOL/Nitpick_Examples/Manual_Nits.thy*)

    (** )"HOL-Decision_Procs.Dense_Linear_Order" "HOL-Library.Function_Algebras"

      "HOL-Library.Set_Algebras"( *..for HOL/Metis_Examples/Big_O.thy*)

    (**)"~~/src/HOL/Metis_Examples/Type_Encodings"(*..for HOL/Metis_Examples/Proxies.thy*)

begin

section \<open>Notes during development\<close>

text \<open>

  Main question at the beginning:

  How present a structure comprising keywords and terms via PIDE?

  Preliminary conclusion:

  The above main question could not yet be answered due to the complexity of Isabelle:

  * typing "sledgehammer" into a theory, e.g. in lemma "inc \<noteq> (\<lambda>y. 0)" below

    creates an instance of isar_proofs.

  * this proof is displayed in an <Output> window

  * clicking the proof transfers to the theory, i.e. below lemma "inc \<noteq> (\<lambda>y. 0)"

  The latter is what we are interested in, but we cannot find the respective code,

  which we expect somewhere far off from Outer_Syntax.command..sledgehammer.

\<close>

subsection \<open>Documentation and papers\<close>

text \<open>

  implementation.pdf

    Proof_Syntax.read_proof thy b1 b2 s reads in a proof term. The Boolean

    flags indicate the use of sort and type information. Usually, typing

    information is left implicit and is inferred during proof reconstruction.

  sledgehammer.pdf

    • verit: veriT [6] is an SMT solver developed by David Déharbe,

    Pascal Fontaine, and their colleagues. It is specifically designed

    to produce detailed proofs for reconstruction in proof assistants.

    To use veriT, set the environment variable VERIT_SOLVER to the

    complete path of the executable, including the file name. Sledge-

    hammer has been tested with version smtcomp2019. (..NOT Mathias Fleury)

  isar-ref.pdf //

  Reconstructing veriT Proofs in Isabelle/HOL

    https://arxiv.org/pdf/1908.09480.pdf

    http://fmv.jku.at/fleury/papers/Fleury-thesis.pdf

\<close>

subsection \<open>code\<close>

subsubsection \<open>1st approach\<close>

text \<open>

  HOL/ex/Sketch_and_Explore.thy by Haftmann

    |> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt

  HOL/List.thy

    imports Sledgehammer

  HOL/Metis_Examples/Proxies.thy

    :

    HOL/Metis_Examples/Type_Encodings.thy

  HOL/Tools/Sledgehammer/sledgehammer_isar.ML

    :

  HOL/Sledgehammer.thy

    keywords "sledgehammer" :: diag and

\<close>

subsubsection \<open>survey search: "sledgehammer" , search: "isar_proofs"\<close>

text \<open>

  ALL hits concerning ML only (no calls from thy in proofs):

    src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML           "isar_proofs"    "sledgehammer" 

    src/HOL/Mutabelle/mutabelle_extra.ML                                         "sledgehammer"

    src/HOL/Tools/Sledgehammer/sledgehammer.ML                                   "sledgehammer"

    src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML         "isar_proofs"    "sledgehammer"

    src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML             "isar_proofs"

    src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML       "isar_proofs"

    src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML  "isar_proofs"

    src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML           "isar_proofs"

    src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML       "isar_proofs"

    src/HOL/Tools/Sledgehammer/sledgehammer_util.ML                              "sledgehammer"

\<close>

subsubsection \<open>Try to trace code from keywords down to isar_proofs\<close>

text \<open>

  HOL/Sledgehammer.thy

    "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl

  HOL/Tools/Sledgehammer/sledgehammer_commands.ML

    Outer_Syntax.command

    val isar_proofs = lookup_option lookup_bool "isar_proofs"

    in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end

    val hammer_away: (string * string list) list -> (string -> unit) option -> string ->

      int option -> fact_override -> Proof.state -> unit

                                     ^^^^^^^^^^^

    .. called by (exclusively)

        Outer_Syntax.command command_keyword>\<open>sledgehammer\<close>

        Query_Operation.register {name = sledgehammerN, pri = 0}

  HOL/Tools/Sledgehammer/sledgehammer.ML

    val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->

      Proof.state -> bool * (string * string list)

      ^^^^^^^^^^^

  HOL/Tools/Sledgehammer/sledgehammer_isar.ML

    fun isar_proof_text

    val ///

    fun proof_text

    val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->

      int -> one_line_params -> string

        ^^^^^^^^^^ is called in ..

  HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

    fun run_atp                   ..calls fun proof_text

  HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML

    fun run_smt_solver            ..calls fun proof_text

  DIFFICULTY: see conclusion below section \<open>Notes during development\<close>

\<close>

section \<open>Search for an appropriate example\<close>

text \<open>

  Conclusion: from the locations checked the best example is lemma "inc \<noteq> (\<lambda>y. 0)"

  here at the bottom.

\<close>

subsection \<open>sledgehammer.pdf\<close>

text \<open>

  Summary: There are only two examples and only one is working.

  And there are no differences between sledgehammer with [isar_proofs] and without.

\<close>

subsubsection \<open>WITHOUT <Isar proofs> checked in Sledgehammer panel\<close>

(*p.5*)

lemma "[a] = [b] \<Longrightarrow> a = b"

(** )sledgehammer( **)

  by blast

(*/----------------------- these tests run into: all provers timed out --------------------\* )

(*p.23*)

lemma "\<exists>xs. xs 6 = []"

(**)sledgehammer [strict] (add: list.distinct)(** ) ..all provers timed out( **)

  sorry

subsubsection \<open>with <Isar proofs> checked in Sledgehammer panel\<close>

(*p.5*)

lemma "[a] = [b] \<Longrightarrow> a = b"

(** )sledgehammer(**)[isar_proofs]( **)

  by simp(** ) ..Check <Isar proofs>: (No Isar proof available.)( **)

(*p.23*)

lemma "\<exists>xs. xs 6 = []"

(**)sledgehammer [strict] (add: list.distinct)(** ) ..all provers timed out( **)

  sorry

( *\----------------------- these tests run into: all provers timed out --------------------/*)

subsection \<open>HOL/Metis_Examples/Tarski.thy\<close>

text \<open>

  Summary: We use sledgehammer [isar_proofs] + <Isar proofs> checked in Sledgehammer panel.

  Little knowledge required: Main + FuncSet.thy (\<in> HOL-Library)

  -- but the first "sledgehammer" is after ca.10 pages.

\<close>

subsection \<open>HOL/Nitpick_Examples/Manual_Nits.thy\<close>

text \<open>

  Summary: We use sledgehammer [isar_proofs] + <Isar proofs> checked in Sledgehammer panel.

  Little knowledge required: HOL.Real + "HOL-Library.Quotient_Product"

  -- and the first "sledgehammer" is already on 2nd page.

  Works with Big_O.thy, Proxies.thy,

  Summary: preparation is simple, and the output has 2 keywords.

\<close>

(*/------------------------------ preparing the subsequent example ---------------------------\*)

(*NONE*)

(*\------------------------------ preparing the subsequent example ---------------------------/*)

lemma "\<exists>!x. x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"

nitpick [expect = none]

nitpick [card 'a = 1-50, expect = none]

(** )sledgehammer( **)

  using the_equality by fastforce

subsection \<open>HOL/Metis_Examples/Big_O.thy\<close>

text \<open>

  We use sledgehammer [isar_proofs] + <Isar proofs> checked in Sledgehammer panel.

  Little knowledge required: HOL-Library.Set_Algebras

  -- and the first "sledgehammer" is on 5th page.

  Summary: sledgehammer does NOT work in the 1st example, NOT even in the original theory.

\<close>

subsection \<open>HOL/Metis_Examples/Proxies.thy\<close>

text \<open>

  We use sledgehammer [isar_proofs] + <Isar proofs> checked in Sledgehammer panel.

  Little knowledge required: session "HOL-Metis_Examples" =

    "HOL-Library" + "HOL-Decision_Procs" + "HOL-Algebra" + "HOL-Cardinals"

  -- and the first "sledgehammer" is on 1st page.

  Summary: preparations are simple, and the output is structured perfectly !!

\<close>

(*/------------------------------ preparing the subsequent example ---------------------------\*)

sledgehammer_params [prover = spass, fact_filter = mepo, timeout = 30, preplay_timeout = 0,

  dont_minimize]

lemma plus_1_not_0: "n + (1::nat) \<noteq> 0"

by simp

definition inc :: "nat \<Rightarrow> nat" where

"inc x = x + 1"

(*\------------------------------ preparing the subsequent example ---------------------------/*)

lemma "inc \<noteq> (\<lambda>y. 0)"

(** )sledgehammer [isar_proofs, expect = some] (inc_def plus_1_not_0)( **)

proof -

have "\<exists>n. (n::nat) + 1 \<noteq> 0"

  by (metis plus_1_not_0)

  then show ?thesis

    by (metis inc_def)

qed

end