(* Copyright 2021 (C) Mihails Milehins *) theory IDE_Reference imports IHOL_IDE Reference_Prerequisites begin section‹Introduction› subsection‹Background› text‹ This document presents a reference manual for the framework IDE. The framework IDE can be used for the automated synthesis of the introduction, destruction and elimination rules from the definitions of predicates stated in the object logic Isabelle/HOL of the proof assistant Isabelle. The primary functionality of the framework is available via the \textit{Isabelle/Isar} \<^cite>‹"bertot_isar_1999" and "wenzel_isabelleisar_2007"› command @{command mk_ide}. Given a definition of a predicate in Isabelle/HOL, the command can synthesize introduction, destruction and elimination rules for this definition. The rules are stated in a certain predetermined format that is meant to be both natural and convenient for the end user and the tools for classical reasoning available in Isabelle/HOL. › subsection‹Related and previous work› text‹ The standard distribution of Isabelle provides the \textit{attribute} @{attribute elim_format} \<^cite>‹"wenzel_isabelle/isar_2019-1"› that can be used for the conversion of the destruction rules to the elimination rules. The primary functionality of this attribute is reused in the implementation of the command @{command mk_ide}. Furthermore, Isabelle offers several definitional packages that provide similar rules automatically for the constants created by these definitional packages \<^cite>‹"wenzel_isabelle/isar_2019-1"›. However, to the best knowledge of the author, none of these packages can generate such rules for arbitrary predicates. Perhaps, in the future, the approaches can be unified or integrated in some manner. › text‹\newpage› section‹Syntax› text‹ This subsection presents the syntactic categories that are associated with the command @{command mk_ide}. It is important to note that the presentation is only approximate. › text‹ \begin{matharray}{rcl} @{command_def "mk_ide"} & : & ‹local_theory → local_theory› \end{matharray} ┉ \<^rail>‹ @@{command mk_ide} @{element "rf"}? thm ((intro | elim | dest)*) ; intro: @@{element "|intro"} (thmdef @'|') ; dest: @@{element "|dest"} (thmdef @'|') ; elim: @@{element "|elim"} (thmdef @'|') › ➧ ⬚‹mk_ide› (⬚‹rf›) ‹def_thm› ⬚‹|intro› ‹name[attrbs]›⬚‹|› converts the definition ‹def_thm› into an introduction rule, followed by the application of the functionality associated with the optional keyword ⬚‹rf› and the attributes ‹attrbs› to this rule. The result of the application of the attributes ‹attrbs› is stored in the local context under the name ‹name›. ‹def_thm› is meant to be a fact that consists of exactly one theorem of the form \begin{center} ‹A a⇩_{1}… a⇩_{n}≃ f⇩_{1}a⇩_{1}… a⇩_{n}∧ … ∧ f⇩_{m}a⇩_{1}… a⇩_{n}›, \end{center} where ‹n› and ‹m› are natural numbers, ‹A› is a constant predicate in ‹n› arguments, ‹≃› is either the meta-logic equality or the object logic equality, ‹a⇩_{1}… a⇩_{n}› are schematic variables and ‹f⇩_{1}… f⇩_{m}› are suitable predicates in ‹n› arguments (however, there are further implicit restrictions). The resulting introduction rule is expected to be stated in the format \begin{center} ‹f⇩_{1}a⇩_{1}… a⇩_{n}⟹ … ⟹ f⇩_{m}a⇩_{1}… a⇩_{n}⟹ A a⇩_{1}… a⇩_{n}› \end{center} prior to the application of the functionality associated with the keyword ⬚‹rf› and the attributes ‹attrbs›. If the optional keyword ⬚‹rf› is passed as an argument to the command, then the output of the command (prior to the application of the attributes) is formatted using an algorithm associated with the attribute @{attribute rule_format} \<^cite>‹"wenzel_isabelle/isar_2019-1"›. ➧ ⬚‹mk_ide› (⬚‹rf›) ‹def_thm› ⬚‹|dest› ‹name[attrbs]›⬚‹|› converts the definition ‹def_thm› into one or more destruction rules, followed by the application of the functionality associated with the optional keyword ⬚‹rf› and the attributes ‹attrbs› to each destruction rule. Given the theorem ‹def_thm› in the format described above, the command provides ‹m› destruction rules of the form \begin{center} ‹A a⇩_{1}… a⇩_{n}⟹ f⇩_{i}a⇩_{1}… a⇩_{n}› \end{center} for each ‹1≤i≤m› prior to the application of the functionality associated with the keyword ⬚‹rf› and the attributes ‹attrbs›. ➧ ⬚‹mk_ide› (⬚‹rf›) ‹def_thm› ⬚‹|elim› ‹name[attrbs]›⬚‹|› converts the definition ‹def_thm› into an elimination rule, followed by the application of the functionality associated with the optional keyword ⬚‹rf› and the attributes ‹attrbs› to each destruction rule. Given the theorem ‹def_thm› in the format described above, the elimination rule has the format \begin{center} ‹A a⇩_{1}… a⇩_{n}⟹ (f⇩_{1}a⇩_{1}… a⇩_{n}⟹ … ⟹ f⇩_{m}a⇩_{1}… a⇩_{n}⟹ P) ⟹ P› \end{center} prior to the application of the functionality associated with the keyword ⬚‹rf› and the attributes ‹attrbs›. It is possible to combine the keywords ⬚‹|intro›, ⬚‹|dest› and ⬚‹|elim› in a single invocation of the command. › text‹\newpage› section‹Examples› text‹ In this section, some of the capabilities of the framework IDE are demonstrated by example. The example is based on the definition of the constant \<^const>‹monoid› from the standard library of Isabelle/HOL \<^cite>‹"noauthor_isabellehol_2020"› and given by \begin{center} @{thm monoid_def[unfolded monoid_axioms_def, no_vars]} \end{center} › mk_ide rf monoid_def[unfolded monoid_axioms_def] |intro monoidI| |dest monoidD| |elim monoidE| text‹ The invocation of the command @{command mk_ide} provides the theorem @{thm [source] monoidI} given by \begin{center} @{thm monoidI[no_vars]}, \end{center} the fact @{thm [source] monoidD} given by \begin{center} @{thm monoidD[no_vars]} \end{center} and the theorem @{thm [source] monoidE} given by \begin{center} @{thm monoidE[no_vars]}. \end{center} › end