Theory ETTS_Examples
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