(* Title: CTR/CTR_Reference.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins Reference manual for the CTR. *) section‹CTR› theory CTR_Reference imports CTR "../UD/UD_Reference" begin subsection‹Introduction› subsubsection‹Background› text‹ This section presents a reference manual for the sub-framework CTR that can be used for the automated synthesis of conditional transfer rules. The CTR evolved from the frameworks \textit{Conditional Parametricity} (CP) \<^cite>‹"gilcher_conditional_2017"› and Types-To-Sets that are available as part of the main distribution of Isabelle. However, it does not require either the axiom LT or the axiom UO associated with the Types-To-Sets for its operation. The CTR introduces the following Isabelle/Isar commands: \[ \begin{array}{rcl} @{command ctr} & : & ‹local_theory → local_theory›\\ @{command ctr_relator} & : & ‹local_theory → local_theory›\\ \end{array} \] › subsubsection‹Purpose and scope› text‹ The primary functionality of the CTR is available via the command @{command ctr}. The command @{command ctr}, given a definition of a constant, attempts to provide a conditional transfer rule for this constant, possibly under arbitrary user-defined side conditions. The process of the synthesis of a transfer rule for a constant may or may not involve the declaration and synthesis of a definition of a new (\textit{relativized}) constant. The command provides an interface for the application of two plausible algorithms for the synthesis of the transfer rules that have a restricted and overlapping scope of applicability. The first algorithm (\textit{CTR I}) was developed and implemented in \<^cite>‹"gilcher_conditional_2017"›. An outline of the second algorithm (\textit{CTR II}) was proposed in \<^cite>‹"lammich_automatic_2013"› and \<^cite>‹"immler_smooth_2019"›: CTR II relies on the functionality of the @{method transfer_prover} (see subsection 4.6 in \<^cite>‹"kuncar_types_2015"›). More details about CTR II are given in the next subsection. The command @{command ctr_relator} can be used for the registration of the, so-called, \textit{ctr-relators} that need to be provided for every non-nullary type constructor that occurs in the type of the constant-instance whose definition is passed as an argument to CTR II. However, as a fallback solution, the command @{command ctr} may use the \textit{relators} that are associated with the standard \textit{BNF} infrastructure of Isabelle/HOL (e.g., see \<^cite>‹"traytel_foundational_2012"›). The only necessary condition for the registration of the ctr-relators is that they must satisfy the type-constraint associated with the action of a BNF on relations (e.g., see \<^cite>‹"traytel_foundational_2012"› or \<^cite>‹"blanchette_bindings_2019"›). › subsubsection‹Related and previous work› text‹ As already mentioned, the CTR evolved from the framework CP that is available as part of the main distribution of Isabelle. Furthermore, CTR provides an interface to the main functionality associated with the framework CP and builds upon many ideas that could be associated with it. The primary reason for the development of the command @{command ctr} instead of extending the implementation of the existing command @{command parametric_constant} provided as part of the CP was the philosophy of non-intervention with the development version of Isabelle that was adopted at the onset of the design of the CTR. Perhaps, in the future, the functionality of the aforementioned commands can be integrated. It should also be mentioned that the Isabelle/ML code from the main distribution of Isabelle was frequently reused during the development of CTR. Lastly, it should be mentioned that the framework SpecCheck \<^cite>‹"kappelmann_speccheck_2021"› was used for unit testing the framework CTR. › subsection‹Theory› text‹ Assume the existence of an underlying well-formed definitional theory $D$ and a context $\Gamma$; assume the existence of a map $\mathsf{ctr}_{\mathsf{Rel}}$ from a finite set of non-nullary type constructors to relators, mapping each non-nullary type constructor in its domain to a valid relator for this type constructor. The inputs to CTR II are a constant-instance definition $\vdash c_{?\bar{\gamma}\ K} = \phi\left[?\bar{\gamma}\right] $ of the constant-instance $c_{?\bar{\gamma}\ K}$ and the map $\mathsf{trp}$ from the set of all schematic type variables in ?$\bar{\gamma}$ to the set of (fixed) binary relations $x_{\alpha\rightarrow\beta\rightarrow\mathbb{B}}$ in $\Gamma$ with non-overlapping type variables ($?\bar{\gamma}$ corresponds to a sequence of all distinct type variables that occur in the type $?\bar{\gamma}\ K$, while $K$, applied using a postfix notation, contains all information about the type constructors of the type $?\bar{\gamma}\ K$, such that the non-nullary type constructors associated with $K$ form a subset of the domain of $\mathsf{ctr}_{\mathsf{Rel}}$). CTR II consists of three parts: \textit{synthesis of a parametricity relation}, \textit{synthesis of a transfer rule} and \textit{post-processing}. \textbf{Synthesis of a parametricity relation}. An outline of an algorithm for the conversion of a type to a \textit{parametricity relation} is given in subsection 4.1.1 in \<^cite>‹"kuncar_types_2015"›. Thus, every nullary type constructor in $?\bar{\gamma}\ K$ is replaced by the identity relation $=$, every non-nullary type constructor $\kappa$ in $?\bar{\gamma}\ K$ is replaced by its corresponding relator $\mathsf{ctr}_{\mathsf{Rel}}\left(\kappa\right)$ and every type variable $?\gamma$ in $?\bar{\gamma}\ K$ is replaced by $\mathsf{trp}\left(?\gamma\right)$, obtaining the parametricity relation $R_{\bar{\alpha}\ K \rightarrow \bar{\beta}\ K \rightarrow\mathbb{B}}$. \textbf{Synthesis of a transfer rule}. First, the goal $R\ \phi\left[\bar{\alpha}\right]\ \phi\left[\bar{\beta}\right]$ is created in $\Gamma$ and an attempt to prove it is made using the algorithm associated with the method @{method transfer_prover}. If the proof is successful, nothing else needs to be done in this part. Otherwise, an attempt to find a solution for $?a$ in $R\ \left(?a_{\bar{\alpha}\ K}\right)\ \phi\left[\bar{\beta}\right]$ is made, once again, using the @{method transfer_prover}. The result of the successful completion of the synthesis is a transfer rule $\Gamma \vdash R\ \psi\left[\bar{\alpha},\bar{x}\right]\ \phi\left[\bar{\beta}\right]$, where $\bar{x}$ is used to denote a sequence of typed variables, each of which occurs free in the context $\Gamma$ (the success of this part is not guaranteed). \textbf{Post-processing}. If $\psi\left[\bar{\alpha},\bar{x}\right] = \phi\left[\bar{\alpha}\right]$ after the successful completion of part 2 of the algorithm, then the definitions of the constant-instances $c_{\bar{\alpha}\ K}$ and $c_{\bar{\beta}\ K}$ are folded, resulting in the deduction \mbox{$\Gamma \vdash R\ c_{\bar{\alpha}\ K}\ c_{\bar{\beta}\ K}$}. Otherwise, if \mbox{$\psi\left[\bar{\alpha},\bar{x}\right]\ \neq \phi\left[\bar{\alpha}\right]$}, then a new constant $d$ is declared such that \mbox{$\vdash d_{\sigma\left[?\bar{\alpha}\right]} = \left(\lambda \bar{x}.\ \psi\left[?\bar{\alpha},\bar{x}\right]\right)$}, where $\sigma$ is determined uniquely by $\bar{x}$ and $?\bar{\alpha}\ K$. In this case, \mbox{$\Gamma \vdash R\ \psi\left[\bar{\alpha},\bar{x}\right]\ \phi\left[\bar{\beta}\right]$} can be restated as \mbox{$\Gamma \vdash R\ \left(d_{\sigma\left[\bar{\alpha}\right]}\ \bar{x}\right)\ c_{\bar{\beta}\ K}$}. This result can be exported to the global theory context and forms a conditional transfer rule for $c_{?\bar{\gamma}\ K}$. CTR II can perform the synthesis of the transfer rules for constants under arbitrary user-defined side conditions automatically. However, the algorithm guarantees neither that it can identify whether a transfer rule exists for a given constant under a given set of side conditions, nor that it will be found if it does exist. › subsection‹Syntax› subsubsection‹Background› text‹ This subsection presents the syntactic categories that are associated with the command @{command ctr} and closely related auxiliary commands and attributes. It is important to note that the presentation is only approximate. › subsubsection‹‹ctr_relator›› text‹ \begin{matharray}{rcl} @{command_def ctr_relator} & : & ‹local_theory → local_theory› \end{matharray} ┉ \<^rail>‹@@{command ctr_relator} term› ➧ ⬚‹ctr_relator› ‹c› saves the ctr-relator ‹c› to a database of ctr-relators for future reference. A ctr-relator is defined as any constant that has the type of the form \begin{center} ‹(α⇩_{1}⇒β⇩_{1}⇒𝔹)⇒…⇒(α⇩_{n}⇒β⇩_{n}⇒𝔹)⇒(α⇩_{1}…α⇩_{n})κ⇒(β⇩_{1}…β⇩_{n})κ⇒𝔹›, \end{center} where ‹α⇩_{1}…α⇩_{n}› and ‹β⇩_{1}…β⇩_{n}› are distinct type variables, ‹n› is a positive integer and ‹κ› is a type constructor. › subsubsection‹‹ctr›› (* Certain elements of the content presented below were copied from the theory Doc/Isar_Rel/Spec.thy in the main library of Isabelle. *) text‹ \begin{matharray}{rcl} @{command_def ctr} & : & ‹local_theory → local_theory› \\ \end{matharray} ┉ \<^rail>‹ @@{command ctr} (@'parametricity' | @'relativization' rlt) in_def ; rlt: (synthesis*) (cce*) trp ; synthesis: @'synthesis' (thm*) ; cce: @'fixes' vars | @'assumes' (props + @'and') ; trp: (@'trp' ('(' type_var term ')' + @'and'))? ; in_def: ((binding @':')? thm mixfix?) + and › ➧ ⬚‹ctr› provides access to two algorithms for the automated synthesis of the transfer rules and the relativization of constants based on their definitions. ➧ ⬚‹parametricity› indicates that CTR I needs to be invoked by the command. ➧ ⬚‹relativization› indicates that CTR II needs to be invoked by the command. ➧ ⬚‹synthesis› ‹thm› indicates that the relativization of the inputs needs to be performed and post-processed using the simplifier with the collection of rewrite rules stated as the fact ‹thm›. If the optional argument ‹thm› is not provided, then the default ‹simpset› is used for post-processing. If the keyword ⬚‹synthesis› is omitted, then no attempt to perform the relativization is made. The keyword ⬚‹synthesis› is relevant only for CTR II. ➧ ⬚‹trp› ‹(?a⇩_{1}A⇩_{1})› ⬚‹and› ‹…› ⬚‹and› ‹(?a⇩_{n}A⇩_{n})› indicates that the type variable that has the indexname ‹?a⇩_{i}› (‹1≤i≤n›, ‹n› is a non-negative integer) is meant to correspond to the binary relation ‹A⇩_{i}› in the parametricity relation constructed by the command prior to the statement of the transfer rule (for further information see subsection 4.1 in \<^cite>‹"kuncar_types_2015"›). This is relevant only for CTR II. ➧ ⬚‹in› ‹(b:) def_thm (mixfix)› is used for the specification of the input to the algorithms that are associated with the command @{command ctr}. ‹def_thm› is meant to be a fact that consists of exactly one theorem of the form ‹A ?a⇩_{1}…?a⇩_{n}≃ f ?a⇩_{1}…?a⇩_{n}›, where ‹A› is a constant, ‹≃› is either meta- or object-equality, ‹n› is a non-negative integer, ‹?a⇩_{1}…?a⇩_{n}› are schematic variables and ‹f› is a suitable formula in ‹n› arguments (however, there are further implicit restrictions). If a new constant is introduced by the command, then the optional argument ‹mixfix› is used for the specification of the concrete inner syntax for the constant in the usual manner (e.g. see \<^cite>‹"wenzel_isabelle/isar_2019-1"›). The optional binding ‹b› is used for the specification of the names of the entities that are provided after the successful execution of the command. It is hoped that the algorithm chosen for the specification of the names is sufficiently intuitive and does not require further explanation. If either ‹b› or ‹mixfix› are not specified by the user, then the command introduces sensible defaults. Multiple theorems may be provided after the keyword ⬚‹in›, employing the keyword ⬚‹and› as a separator. In this case, the parameterized algorithm associated with the command is applied repeatedly to each input theorem in the order of their specification from left to right and the local context is augmented incrementally. › subsection‹Examples\label{sec:ctr_ex}› text‹ In this subsection, some of the capabilities of the CTR are demonstrated by example. The examples that are presented in this subsection are expected to be sufficient to begin an independent exploration of the framework, but do not cover the entire spectrum of the functionality and the problems that one may encounter while using it. The examples that are presented in this subsection continue the example of the application of the command @{command ud} to the definition of the constant @{const mono} that was presented in subsection \ref{sec:ud_ex}. › subsubsection‹CTR I› text‹ As already explained, the command @{command ctr} can be used to invoke the algorithm associated with the command @{command parametric_constant} for the synthesis of a transfer rule for a given constant. For example, the invocation of › ctr parametricity in mono: mono.with_def text‹ generates the transfer rule @{thm [source] mono_transfer}: \begin{center} @{thm [display, mode=IfThenNoBox] mono_transfer[no_vars]} \end{center} A detailed explanation of the underlying algorithm can be found in \<^cite>‹"gilcher_conditional_2017"›. › subsubsection‹CTR II› text‹ The first example in this subsection demonstrates how CTR II can be used to produce a parametricity property identical to the one produced by CTR I above: › ctr relativization fixes A1 :: "'a ⇒ 'b ⇒ bool" and A2 :: "'c ⇒ 'd ⇒ bool" assumes [transfer_rule]: "bi_total A1" trp (?'a A1) and (?'b A2) in mono': mono.with_def text‹ This produces the theorem @{thm [source] mono'.transfer}: @{thm [display, mode=IfThenNoBox] mono'.transfer[no_vars]} which is identical to the theorem @{thm [source] mono_transfer} generated by CTR I. › text‹ Of course, there is very little value in trying to establish a parametricity property using CTR II due to the availability of CTR I. However, it is often the case that the constant is not parametric under a given set of side conditions. Nonetheless, in this case, it is often possible to define a new \textit{relativized constant} that is related to the original constant under the parametricity relation associated with the original constant. It is expected that the most common application of CTR II will be the synthesis of the relativized constants. For example, suppose one desires to find a conditional transfer rule for the constant @{const mono.with} such that (using the conventions from the previous example) the relation ‹A1› is right total, but not, necessarily, left total. While, under such restriction on the involved relations, the constant @{const mono.with} is no longer conditionally parametric, its relativization exists and can be found using the transfer prover. To automate the relativization process, the user merely needs to add the keyword ⬚‹synthesis› immediately after the keyword ⬚‹relativization›: › ctr relativization synthesis ctr_simps fixes A1 :: "'a ⇒ 'b ⇒ bool" and A2 :: "'c ⇒ 'd ⇒ bool" assumes [transfer_domain_rule]: "Domainp A1 = (λx. x ∈ U1)" and [transfer_rule]: "right_total A1" trp (?'a A1) and (?'b A2) in mono_ow: mono.with_def text‹ This produces the definition @{thm [source] mono_ow_def}: @{thm [display, mode=IfThenNoBox] mono_ow_def[no_vars]} and the theorem @{thm [source] mono_ow.transfer}: @{thm [display, mode=IfThenNoBox] mono_ow.transfer[no_vars]} It should be noted that, given that the keyword ⬚‹synthesis› was followed by the name of the named collection of theorems @{thm [source] ctr_simps}, this collection was used in post-processing of the result of the relativization. The users can omit simplification entirely by specifying the collection @{thm [source] ctr_blank} instead of @{thm [source] ctr_simps}. › text‹\newpage› end