Theory IDE_Reference

(* 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⇩₁ … a⇩_n ≃ f⇩₁ a⇩₁ … a⇩_n ∧ … ∧ f⇩_m a⇩₁ … 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⇩₁ … a⇩_n› are schematic variables and ‹f⇩₁ … 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⇩₁ a⇩₁ … a⇩_n ⟹ … ⟹ f⇩_m a⇩₁ … a⇩_n ⟹ A a⇩₁ … 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⇩₁ … a⇩_n ⟹ f⇩_i a⇩₁ … 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⇩₁ … a⇩_n ⟹ (f⇩₁ a⇩₁ … a⇩_n ⟹ … ⟹ f⇩_m a⇩₁ … 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