Theory ETTS_Syntax

(* 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› |› U1 and …› and Un allows for the
registration of the set-based terms in the sbt-database.
Generally, Ui (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 Ui equivalent to the set of the type variables that occur in 
the type of t›.

   tts_find_sbts t1 and …› and tn prints the
templates for the transfer rules for the set-based terms t1…tn
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~:›~(?a1 to U1)› and …› and 
(?an to Un)› provides means for the declaration of the RI specification. 
For each i› (1≤i≤n›, n› --- positive integer), ?ai 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 Ui can be any term of the type typ'a set, where typ'a 
is a fixed type variable.
     sbterms~:›~(tbcv1 to sbt1)› and …› and
(tbcvn to sbtn)› 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, tbcvi 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 sbti 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 thm1 and …› and thmn 
(n› --- non-negative integer) provides means for the declaration of the 
known premises for the set-based theorem.
     eliminating term1 and …› and termn 
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 [attr1, …, attrn]› (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 sbf1 = tbf1 and …› and sbfn = tbfn 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, tbfi is used for
the specification of the input of the extended relativization algorithm and
sbfi 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 sbfi is omitted, then a 
default specification of the output is inferred automatically. tbfi must 
be a schematic fact available in the context, whereas sbfi can be any
fresh name binding. Optionally, it is possible to provide attributes for 
each individual input and output, e.g., sbfi[sbf_attrb] = tbfi[tbf_attrb]›. 
In this case, the list of the attributes tbf_attrb› is applied to tbfi 
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