(* Title: ETTS/Manual/ETTS_Examples.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins *) section‹ETTS by example› theory ETTS_Examples imports ETTS_Syntax Complex_Main begin subsection‹Background› text‹ In this section, some of the capabilities of the extension of the framework Types-To-Sets are demonstrated by example. The examples that are presented in this section are expected to be sufficient to begin an independent exploration of the extension, but do not cover the entire spectrum of its functionality. › subsection‹First steps› subsubsection‹Problem statement› text‹ Consider the task of the relativization of the type-based theorem @{thm [source] topological_space_class.closed_Un} from the standard library of Isabelle/HOL: \begin{center} @{thm [names_short = true] topological_space_class.closed_Un[no_vars]}, \end{center} where ‹S::'a::topological_space set› and ‹T::'a::topological_space set›. › subsubsection‹Unoverloading› text‹ The constant @{const closed} that occurs in the theorem is an overloaded constant defined as \mbox{@{thm [names_short = true] closed_def[no_vars]}} for any @{term [show_sorts] "S::'a::topological_space set"}. The constant may be unoverloaded with the help of the command @{command ud} that is provided as part of the framework CTR: › ud ‹topological_space.closed› ud closed' ‹closed› text‹ This invocation declares the constant @{const closed.with} that is defined as \begin{center} @{thm closed.with_def[no_vars]} \end{center} and provides the theorems @{thm [source] closed.with} given by \begin{center} @{thm closed.with[no_vars]} \end{center} and @{thm [source] closed'.with} given by \begin{center} @{thm closed'.with[no_vars]} \end{center} These theorems are automatically added to the dynamic fact @{thm [source] ud_with}. › subsubsection‹Conditional transfer rules› text‹ Before the relativization can be performed, the transfer rules need to be available for each constant that occurs in the type-based theorem immediately after step 4 of the KERA. All binary relations that are used in the transfer rules must be at least right total and bi-unique (assuming the default order on predicates in Isabelle/HOL). For the theorem @{thm [source] topological_space_class.closed_Un}, there are two such constants: @{const class.topological_space} and @{const closed.with}. The transfer rules can be obtained with the help of the command @{command ctr} from the framework CTR. The process may involve the synthesis of further relativized constants, as described in the reference manual for the framework CTR. › ctr relativization synthesis ctr_simps assumes [transfer_domain_rule]: "Domainp A = (λx. x ∈ U)" and [transfer_rule]: "right_total A" "bi_unique A" trp (?'a A) in topological_space_ow: class.topological_space_def and closed_ow: closed.with_def subsubsection‹Relativization› text‹ As mentioned previously, the relativization of theorems can only be performed from within a suitable tts context. In setting up the tts context, the users always need to provide the RI specification elements that are compatible with the theorems that are meant to be relativized in the tts context. The set of the schematic type variables that occur in the theorem @{thm [source] topological_space_class.closed_Un} is ‹{›‹?'a›‹}›. Thus, there needs to be exactly one RI specification element of the form (‹?'a›, @{term [show_types] "U::'a set"}): › tts_context tts: (?'a to ‹U::'a set›) begin text‹ The relativization can be performed by invoking the command @{command tts_lemmas} in the following manner: › tts_lemmas? in closed_Un' = topological_space_class.closed_Un text‹ In this case, the command was invoked in the active mode, providing an active area that can be used to insert the following theorem directly into the theory file: › tts_lemma closed_Un': assumes "U ≠ {}" and "∀x∈S. x ∈ U" and "∀x∈T. x ∈ U" and "topological_space_ow U opena" and "closed_ow U opena S" and "closed_ow U opena T" shows "closed_ow U opena (S ∪ T)" is topological_space_class.closed_Un. text‹ The invocation of the command @{command tts_lemmas} in the active mode can be removed with no effect on the theorems that were generated using the command. › end text‹ While our goal was achieved, that is, the theorem @{thm [source] closed_Un'} is, indeed, a relativization of the theorem @{thm [source] topological_space_class.closed_Un}, something does not appear right. Is the assumption ‹U ≠ {}› necessary? Is it possible to simplify ‹∀x∈S. x ∈ U›? Is it necessary to use such a contrived name for the denotation of the open set predicate? Of course, all of these issues can be resolved by restating the theorem in the form that we would like to see and using @{thm [source] closed_Un'} in the proof of this theorem, e.g. › lemma closed_Un'': assumes "S ⊆ U" and "T ⊆ U" and "topological_space_ow U τ" and "closed_ow U τ S" and "closed_ow U τ T" shows "closed_ow U τ (S ∪ T)" using assms unfolding topological_space_ow_def by (cases ‹U = {}›) (auto simp: assms(3) closed_Un' subset_iff) text‹ However, having to restate the theorem presents a grave inconvenience. This can be avoided by using a different format of the @{syntax tts_addendum}: › tts_context tts: (?'a to ‹U::'a set›) begin tts_lemma closed_Un''': assumes "S ⊆ U" and "T ⊆ U" and "topological_space_ow U τ" and "closed_ow U τ S" and "closed_ow U τ T" shows "closed_ow U τ (S ∪ T)" given topological_space_class.closed_Un proof(cases ‹U = {}›) case False assume prems[OF False]: "⟦ U ≠ {}; ∀x∈S. x ∈ U; ∀x∈T. x ∈ U; topological_space_ow U τ; closed_ow U τ S; closed_ow U τ T ⟧ ⟹ closed_ow U τ (S ∪ T)" for U :: "'a set" and S T τ from prems show ?thesis using assms by blast qed simp end text‹ Nevertheless, could there still be some space for improvement? It turns out that instead of having to state the theorem in the desired form manually, often enough, it suffices to provide additional parameters for post-processing of the raw set-based theorem, as demonstrated in the code below: › tts_context tts: (?'a to ‹U::'a set›) rewriting ctr_simps eliminating ‹?U≠{}› through (auto simp: topological_space_ow_def) applying[of _ _ _ τ] begin tts_lemma closed_Un'''': assumes "S ⊆ U" and "T ⊆ U" and "topological_space_ow U τ" and "closed_ow U τ S" and "closed_ow U τ T" shows "closed_ow U τ (S ∪ T)" is topological_space_class.closed_Un. end text‹ Finding the most suitable set of parameters for post-processing of the result of the relativization is an iterative process and requires practice before fluency can be achieved. › text‹\newpage› end