(* Title: ETTS/Manual/ETTS_Syntax.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins *) section‹Syntax› theory ETTS_Syntax imports ETTS_Theory begin subsection‹Background› text ‹ This section presents the syntactic categories that are associated with the commands @{command tts_context}, @{command tts_lemmas}, @{command tts_lemma}, and several other closely related auxiliary commands. It is important to note that the presentation of the syntax is approximate. › subsection‹Registration of the set-based terms› text‹ \begin{matharray}{rcl} @{command_def "tts_register_sbts"} & : & ‹local_theory → proof(prove)› \\ @{command_def "tts_find_sbts"} & : & ‹context →› \end{matharray} ┉ \<^rail>‹ @@{command tts_register_sbts} term @'|' (term + @'and') ; @@{command tts_find_sbts} (term + @'and') › ➧ ⬚‹tts_register_sbts› ‹t› ‹|› ‹U⇩_{1}› ⬚‹and› ‹…› ⬚‹and› ‹U⇩_{n}› allows for the registration of the set-based terms in the sbt-database. Generally, ‹U⇩_{i}› (‹1≤i≤n›) must be distinct fixed variables with distinct types of the form \<^typ>‹'a set›, with the set of the type variables that occur in the types of ‹U⇩_{i}› equivalent to the set of the type variables that occur in the type of ‹t›. ➧ ⬚‹tts_find_sbts› ‹t⇩_{1}› ⬚‹and› ‹…› ⬚‹and› ‹t⇩_{n}› prints the templates for the transfer rules for the set-based terms ‹t⇩_{1}…t⇩_{n}› for some positive integer ‹n›. If no arguments are provided, then the templates for all sbterms in the sbt-database are printed. › subsection‹Relativization of theorems› text‹ \begin{matharray}{rcl} @{command_def "tts_context"} & : & ‹theory → local_theory› \\ @{command_def "tts_lemmas"} & : & ‹local_theory → local_theory› \\ @{command_def "tts_lemma"} & : & ‹local_theory → proof(prove)› \\ @{command_def "tts_theorem"} & : & ‹local_theory → proof(prove)› \\ @{command_def "tts_corollary"} & : & ‹local_theory → proof(prove)› \\ @{command_def "tts_proposition"} & : & ‹local_theory → proof(prove)› \\ \end{matharray} The relativization of theorems should always be performed inside an appropriately parameterized tts context. The tts context can be set up using the command @{command tts_context}. The framework introduces two types of interfaces for the application of the extended relativization algorithm: @{command tts_lemmas} and the family of the commands with the identical functionality: @{command tts_lemma}, @{command tts_theorem}, @{command tts_corollary}, @{command tts_proposition}. Nonetheless, the primary purpose of the command @{command tts_lemmas} is the experimentation and the automated generation of the relativized results stated using the command @{command tts_lemma}. ┉ \<^rail>‹ @@{command tts_context} param @'begin' ; @@{command tts_lemmas} ((@'!' | @'?')?) tts_facts ; ( @@{command tts_lemma} | @@{command tts_theorem} | @@{command tts_corollary} | @@{command tts_proposition} ) (tts_short_statement | tts_long_statement) ; param: (sets var rewriting subst eliminating app) ; sets: (@'tts' @':' ('(' type_var @'to' term ')' + @'and')) ; var: (@'sbterms' @':' vars)? ; vars: ('(' term @'to' term ')' + @'and') ; rewriting: (@'rewriting' thm)? ; subst: (@'substituting' (thm + @'and'))? ; eliminating: (@'eliminating' elpat? @'through' method)? ; elpat: (term + @'and') ; app: (@'applying' attributes)? ; tts_short_statement: short_statement tts_addendum ; tts_long_statement: thmdecl? context tts_conclusion ; tts_conclusion: ( @'shows' (props tts_addendum + @'and') | @'obtains' obtain_clauses tts_addendum ) ; tts_addendum: (@'given' thm | @'is' thm) ; tts_facts: @'in' (thmdef? thms + @'and') ; › ➧ ⬚‹tts_context param begin› provides means for the specification of a new (unnamed) tts context. ➧ ⬚‹tts›~‹:›~‹(?a⇩_{1}› ⬚‹to› ‹U⇩_{1})› ⬚‹and› ‹…› ⬚‹and› ‹(?a⇩_{n}› ⬚‹to› ‹U⇩_{n})› provides means for the declaration of the RI specification. For each ‹i› (‹1≤i≤n›, ‹n› --- positive integer), ‹?a⇩_{i}› must be a schematic type variable that occurs in each theorem provided as an input to the commands @{command tts_lemmas} and @{command tts_lemma} invoked inside the tts context and ‹U⇩_{i}› can be any term of the type \<^typ>‹'a set›, where \<^typ>‹'a› is a fixed type variable. ➧ ⬚‹sbterms›~‹:›~‹(tbcv⇩_{1}› ⬚‹to› ‹sbt⇩_{1})› ⬚‹and› ‹…› ⬚‹and› ‹(tbcv⇩_{n}› ⬚‹to› ‹sbt⇩_{n})› can be used for the declaration of the sbterm specification. For each individual entry ‹i›, such that ‹1≤i≤n› with ‹n› being a non-negative integer, ‹tbcv⇩_{i}› has to be either an overloaded operation that occurs in every theorem that is provided as an input to the extended relativization algorithm or a schematic variable that occurs in every theorem that is provided as an input to the command, and ‹sbt⇩_{i}› has to be a term registered in the sbt-database. ➧ ⬚‹rewriting› ‹thm› provides means for the declaration of the rewrite rules for the set-based theorem. ➧ ⬚‹substituting› ‹thm⇩_{1}› ⬚‹and› ‹…› ⬚‹and› ‹thm⇩_{n}› (‹n› --- non-negative integer) provides means for the declaration of the known premises for the set-based theorem. ➧ ⬚‹eliminating› ‹term⇩_{1}› ⬚‹and› ‹…› ⬚‹and› ‹term⇩_{n}› ⬚‹through› ‹method› (‹n› --- non-negative integer) provides means for the declaration of the specification of the elimination of premises in the set-based theorem. ➧ ⬚‹applying› ‹[attr⇩_{1}, …, attr⇩_{n}]› (‹n› --- non-negative integer) provides means for the declaration of the attributes for the set-based theorem. ➧ ⬚‹tts_lemmas› applies the ERA to a list of facts and saves the resulting set-based facts in the context. The command @{command tts_lemmas} should always be invoked from within a tts context. If the statement of the command is followed immediately by the optional keyword ⬚‹!›, then it operates in the verbose mode, printing the output of the application of the individual steps of the ERA. If the statement of the command is followed immediately by the optional keyword ⬚‹?›, then the command operates in the active mode, outputting the set-based facts in the form of the ``active areas'' that can be embedded in the Isabelle theory file inside the tts context from which the command @{command tts_lemmas} was invoked. There is a further minor difference between the active mode and the other two modes of operation that is elaborated upon within the description of the keyword ⬚‹in› below. ➧ ⬚‹in› ‹sbf⇩_{1}= tbf⇩_{1}› ⬚‹and› ‹…› ⬚‹and› ‹sbf⇩_{n}= tbf⇩_{n}› is used for the specification of the type-based theorems and the output of the command. For each individual entry ‹i›, such that ‹1≤i≤n› with ‹n› being a positive integer, ‹tbf⇩_{i}› is used for the specification of the input of the extended relativization algorithm and ‹sbf⇩_{i}› is used for the specification of the name binding for the output of the extended relativization algorithm. The specification of the output is optional: if ‹sbf⇩_{i}› is omitted, then a default specification of the output is inferred automatically. ‹tbf⇩_{i}› must be a schematic fact available in the context, whereas ‹sbf⇩_{i}› can be any fresh name binding. Optionally, it is possible to provide attributes for each individual input and output, e.g., ‹sbf⇩_{i}[sbf_attrb] = tbf⇩_{i}[tbf_attrb]›. In this case, the list of the attributes ‹tbf_attrb› is applied to ‹tbf⇩_{i}› during the first part (initialization of the relativization context) of the ERA. If the command operates in the active mode, then the attributes ‹sbf_attrb› are included in the active area output, but not added to the list of the set-based attributes. For other modes of operation, the attributes ‹sbf_attrb› are added to the list of the set-based attributes and applied during the third part (post-processing) of the ERA. ➧ ⬚‹tts_lemma›~‹a: φ› @{syntax "tts_addendum"}, enters proof mode with the main goal formed by an application of a tactic that depends on the settings specified in @{syntax "tts_addendum"} to ‹φ›. Eventually, this results in some fact ‹⊢φ› to be put back into the target context. The command should always be invoked from within a tts context. ➧ A @{syntax tts_long_statement} is similar to the standard @{syntax long_statement} in that it allows to build up an initial proof context for the subsequent claim incrementally. Similarly, @{syntax tts_short_statement} can be viewed as a natural extension of the standard @{syntax short_statement}. ➧ @{syntax "tts_addendum"} is used for the specification of the pre-processing strategy of the goal ‹φ›. \mbox{‹φ› ⬚‹is› ‹thm›} applies the extended relativization algorithm to ‹thm›. If the term that is associated with the resulting set-based theorem is ‹α›-equivalent to the term associated with the goal ‹φ›, then a specialized tactic solves the main goal, leaving only a trivial goal in its place (the trivial goal can be solved using the terminal proof \mbox{step \textbf{.}}). \mbox{‹φ› ⬚‹given› ‹thm›} also applies the extended relativization algorithm to ‹thm›, but the resulting set-based theorem is merely added as a premise to the goal ‹φ›. › text‹\newpage› end