restructuring Lib. Adaption LaTeX. Reorg COL.
This commit is contained in:
parent
2e0d88a3f7
commit
9496b535b7
|
@ -25,28 +25,40 @@ identifies:
|
|||
|
||||
(*<<*)
|
||||
theory CENELEC_50128
|
||||
imports "../../DOF/Isa_COL"
|
||||
imports "../technical_report/technical_report"
|
||||
begin
|
||||
(*>>*)
|
||||
|
||||
text\<open>We re-use the class @\<open>typ math_content\<close>, which provides also a framework for
|
||||
semi-formal terminology, which we re-use by this definition.\<close>
|
||||
|
||||
doc_class semi_formal_content = math_content +
|
||||
status :: status <= "semiformal"
|
||||
mcc :: math_content_class <= "terminology"
|
||||
|
||||
type_synonym sfc = semi_formal_content
|
||||
|
||||
(*>>*)
|
||||
|
||||
text\<open> Excerpt of the BE EN 50128:2011, page 22. \<close>
|
||||
|
||||
|
||||
section\<open>Terms and Definitions\<close>
|
||||
|
||||
Definition*[assessment::concept]\<open>process of analysis to determine whether software, which may include
|
||||
Definition*[assessment::sfc,short_name="''assessment''"]
|
||||
\<open>process of analysis to determine whether software, which may include
|
||||
process, documentation, system, subsystem hardware and/or software components, meets the specified
|
||||
requirements and to form a judgement as to whether the software is fit for its intended purpose.
|
||||
Safety assessment is focused on but not limited to the safety properties of a system.\<close>
|
||||
|
||||
Definition*[assessor::concept, tag="''assessor''"]
|
||||
Definition*[assessor::sfc, short_name="''assessor''"]
|
||||
\<open>entity that carries out an assessment\<close>
|
||||
|
||||
Definition*[COTS::concept, tag="''commercial off-the-shelf software''"]
|
||||
Definition*[COTS::sfc, short_name="''commercial off-the-shelf software''"]
|
||||
\<open>software defined by market-driven need, commercially available and whose fitness for purpose
|
||||
has been demonstrated by a broad spectrum of commercial users\<close>
|
||||
|
||||
|
||||
Definition*[component::concept]
|
||||
Definition*[component::sfc]
|
||||
\<open>a constituent part of software which has well-defined interfaces and behaviour
|
||||
with respect to the software architecture and design and fulfils the following
|
||||
criteria:
|
||||
|
@ -57,108 +69,108 @@ criteria:
|
|||
(e. g. subsystems) which have an independent version
|
||||
\<close>
|
||||
|
||||
Definition*[CMGR::concept, tag="''configuration manager''"]
|
||||
Definition*[CMGR::sfc, short_name="''configuration manager''"]
|
||||
\<open>entity that is responsible for implementing and carrying out the processes
|
||||
for the configuration management of documents, software and related tools including
|
||||
\<^emph>\<open>change management\<close>\<close>
|
||||
|
||||
Definition*[customer::concept]
|
||||
Definition*[customer::sfc]
|
||||
\<open>entity which purchases a railway control and protection system including the software\<close>
|
||||
|
||||
Definition*[designer::concept]
|
||||
Definition*[designer::sfc]
|
||||
\<open>entity that analyses and transforms specified requirements into acceptable design solutions
|
||||
which have the required safety integrity level\<close>
|
||||
|
||||
Definition*[entity::concept]
|
||||
Definition*[entity::sfc]
|
||||
\<open>person, group or organisation who fulfils a role as defined in this European Standard\<close>
|
||||
|
||||
declare_reference*[fault::concept]
|
||||
Definition*[error::concept]
|
||||
declare_reference*[fault::sfc]
|
||||
Definition*[error::sfc]
|
||||
\<open>defect, mistake or inaccuracy which could result in failure or in a deviation
|
||||
from the intended performance or behaviour (cf @{concept (unchecked) \<open>fault\<close>}))\<close>
|
||||
from the intended performance or behaviour (cf @{semi_formal_content (unchecked) \<open>fault\<close>}))\<close>
|
||||
|
||||
Definition*[fault::concept]
|
||||
Definition*[fault::sfc]
|
||||
\<open>defect, mistake or inaccuracy which could result in failure or in a deviation
|
||||
from the intended performance or behaviour (cf @{concept \<open>error\<close>})\<close>
|
||||
from the intended performance or behaviour (cf @{semi_formal_content \<open>error\<close>})\<close>
|
||||
|
||||
Definition*[failure::concept]
|
||||
Definition*[failure::sfc]
|
||||
\<open>unacceptable difference between required and observed performance\<close>
|
||||
|
||||
Definition*[FT::concept, tag="''fault tolerance''"]
|
||||
Definition*[FT::sfc, short_name="''fault tolerance''"]
|
||||
\<open>built-in capability of a system to provide continued correct provision of service as specified,
|
||||
in the presence of a limited number of hardware or software faults\<close>
|
||||
|
||||
Definition*[firmware::concept]
|
||||
Definition*[firmware::sfc]
|
||||
\<open>software stored in read-only memory or in semi-permanent storage such as flash memory, in a
|
||||
way that is functionally independent of applicative software\<close>
|
||||
|
||||
Definition*[GS::concept,tag="''generic software''"]
|
||||
Definition*[GS::sfc,short_name="''generic software''"]
|
||||
\<open>software which can be used for a variety of installations purely by the provision of
|
||||
application-specific data and/or algorithms\<close>
|
||||
|
||||
Definition*[implementer::concept]
|
||||
Definition*[implementer::sfc]
|
||||
\<open>entity that transforms specified designs into their physical realisation\<close>
|
||||
|
||||
Definition*[integration::concept]
|
||||
Definition*[integration::sfc]
|
||||
\<open>process of assembling software and/or hardware items, according to the architectural and
|
||||
design specification, and testing the integrated unit\<close>
|
||||
|
||||
Definition*[integrator::concept]
|
||||
Definition*[integrator::sfc]
|
||||
\<open>entity that carries out software integration\<close>
|
||||
|
||||
Definition*[PES :: concept, tag="''pre-existing software''"]
|
||||
Definition*[PES :: sfc, short_name="''pre-existing software''"]
|
||||
\<open>software developed prior to the application currently in question, including COTS (commercial
|
||||
off-the shelf) and open source software\<close>
|
||||
|
||||
Definition*[OSS :: concept, tag="''open source software''"]
|
||||
Definition*[OSS :: sfc, short_name="''open source software''"]
|
||||
\<open>source code available to the general public with relaxed or non-existent copyright restrictions\<close>
|
||||
|
||||
Definition*[PLC::concept, tag="''programmable logic controller''"]
|
||||
Definition*[PLC::sfc, short_name="''programmable logic controller''"]
|
||||
\<open>solid-state control system which has a user programmable memory for storage of instructions to
|
||||
implement specific functions\<close>
|
||||
|
||||
Definition*[PM::concept, tag="''project management''"]
|
||||
Definition*[PM::sfc, short_name="''project management''"]
|
||||
\<open>administrative and/or technical conduct of a project, including safety aspects\<close>
|
||||
|
||||
Definition*[PGMGR::concept, tag="''project manager''"]
|
||||
Definition*[PGMGR::sfc, short_name="''project manager''"]
|
||||
\<open>entity that carries out project management\<close>
|
||||
|
||||
Definition*[reliability::concept]
|
||||
Definition*[reliability::sfc]
|
||||
\<open>ability of an item to perform a required function under given conditions for a given period of time\<close>
|
||||
|
||||
Definition*[robustness::concept]
|
||||
Definition*[robustness::sfc]
|
||||
\<open>ability of an item to detect and handle abnormal situations\<close>
|
||||
|
||||
Definition*[RMGR::concept, tag="''requirements manager''"]
|
||||
Definition*[RMGR::sfc, short_name="''requirements manager''"]
|
||||
\<open>entity that carries out requirements management\<close>
|
||||
|
||||
Definition*[RMGMT::concept, tag="''requirements management''"]
|
||||
Definition*[RMGMT::sfc, short_name="''requirements management''"]
|
||||
\<open>the process of eliciting, documenting, analysing, prioritising and agreeing on requirements and
|
||||
then controlling change and communicating to relevant stakeholders. It is a continuous process
|
||||
throughout a project\<close>
|
||||
|
||||
Definition*[risk::concept]
|
||||
Definition*[risk::sfc]
|
||||
\<open>combination of the rate of occurrence of accidents and incidents resulting in harm (caused by
|
||||
a hazard) and the degree of severity of that harm\<close>
|
||||
|
||||
Definition*[safety::concept]
|
||||
Definition*[safety::sfc]
|
||||
\<open>freedom from unacceptable levels of risk of harm to people\<close>
|
||||
|
||||
Definition*[SA::concept, tag="''safety authority''"]
|
||||
Definition*[SA::sfc, short_name="''safety authority''"]
|
||||
\<open>body responsible for certifying that safety related software or services comply with relevant
|
||||
statutory safety requirements\<close>
|
||||
|
||||
Definition*[SF::concept, tag="''safety function''"]
|
||||
Definition*[SF::sfc, short_name="''safety function''"]
|
||||
\<open>a function that implements a part or whole of a safety requirement\<close>
|
||||
|
||||
Definition*[SFRS::concept, tag= "''safety-related software''"]
|
||||
Definition*[SFRS::sfc, short_name= "''safety-related software''"]
|
||||
\<open>software which performs safety functions\<close>
|
||||
|
||||
Definition*[software::concept]
|
||||
Definition*[software::sfc]
|
||||
\<open>intellectual creation comprising the programs, procedures, rules, data and any associated
|
||||
documentation pertaining to the operation of a system\<close>
|
||||
|
||||
Definition*[SB::concept, tag="''software baseline''"]
|
||||
Definition*[SB::sfc, short_name="''software baseline''"]
|
||||
\<open>complete and consistent set of source code, executable files, configuration files,
|
||||
installation scripts and documentation that are needed for a software release. Information about
|
||||
compilers, operating systems, preexisting software and dependent tools is stored as part of the
|
||||
|
@ -169,7 +181,7 @@ released and assessed
|
|||
|
||||
|
||||
|
||||
Definition*[SWLC::concept, tag="''software life-cycle''"]
|
||||
Definition*[SWLC::sfc, short_name="''software life-cycle''"]
|
||||
\<open>those activities occurring during a period of time that starts when
|
||||
software is conceived and ends when the software is no longer available for use. The software life
|
||||
cycle typically includes a requirements phase, design phase,test phase, integration phase,
|
||||
|
@ -177,35 +189,35 @@ deployment phase and a maintenance phase 3.1.35 software maintainability
|
|||
capability of the software to be modified; to correct faults, improve to a different environment
|
||||
\<close>
|
||||
|
||||
Definition*[SM::concept, tag="''software maintenance''"]
|
||||
Definition*[SM::sfc, short_name="''software maintenance''"]
|
||||
\<open> action, or set of actions, carried out on software after deployment functionality
|
||||
performance or other attributes, or adapt it with the aim of enhancing or correcting its\<close>
|
||||
|
||||
Definition*[SOSIL::concept, tag="''software safety integrity level''"]
|
||||
Definition*[SOSIL::sfc, short_name="''software safety integrity level''"]
|
||||
\<open>classification number which determines the techniques and measures that have to be applied to
|
||||
software NOTE Safety-related software has been classified into five safety integrity levels, where
|
||||
0 is the lowest and 4 the highest.\<close>
|
||||
|
||||
Definition*[supplier::concept]
|
||||
Definition*[supplier::sfc]
|
||||
\<open>entity that designs and builds a railway control and protection system including the software
|
||||
or parts thereof\<close>
|
||||
|
||||
Definition*[SYSIL::concept, tag="''system safety integrity level''"]
|
||||
Definition*[SYSIL::sfc, short_name="''system safety integrity level''"]
|
||||
\<open>classification number which indicates the required degree of confidence that an integrated
|
||||
system comprising hardware and software will meet its specified safety requirements\<close>
|
||||
|
||||
Definition*[tester::concept]\<open>an entity that carries out testing\<close>
|
||||
Definition*[tester::sfc]\<open>an entity that carries out testing\<close>
|
||||
|
||||
Definition*[testing::concept]
|
||||
Definition*[testing::sfc]
|
||||
\<open>process of executing software under controlled conditions as to ascertain its behaviour and
|
||||
performance compared to the corresponding requirements specification\<close>
|
||||
|
||||
Definition*[TCT1::concept, tag="''tool class T1''"]
|
||||
Definition*[TCT1::sfc, short_name="''tool class T1''"]
|
||||
\<open>generates no outputs which can directly or indirectly contribute to the executable code
|
||||
(including data) of the software NOTE 11 examples include: a text editor or a requirement or
|
||||
design support tool with no automatic code generation capabilities; configuration control tools.\<close>
|
||||
|
||||
Definition*[TCT2::concept,tag="''tool class T2''"]
|
||||
Definition*[TCT2::sfc,short_name="''tool class T2''"]
|
||||
\<open>supports the test or verification of the design or executable code, where errors in the tool
|
||||
can fail to reveal defects but cannot directly create errors in the executable software
|
||||
NOTE T2 examples include: a test harness generator; a test coverage measurement tool; a static
|
||||
|
@ -213,35 +225,35 @@ analysis tool. reproduce defined versions and be the input for future releases a
|
|||
at upgrade in the maintenance phase
|
||||
\<close>
|
||||
|
||||
Definition*[TCT3::concept, tag="''tool class T3''"]
|
||||
Definition*[TCT3::sfc, short_name="''tool class T3''"]
|
||||
\<open>generates outputs which can directly or indirectly contribute to the executable code
|
||||
(including data) of the safety related system NOTE T3 examples include: a source code compiler,
|
||||
a data/algorithms compiler, a tool to change set-points during system operation; an optimising
|
||||
compiler where the relationship between the source code program and the generated object code is
|
||||
not obvious; a compiler that incorporates an executable run-time package into the executable code.
|
||||
\<close>
|
||||
Definition*[traceability::concept]
|
||||
Definition*[traceability::sfc, short_name="''traceability''"]
|
||||
\<open>degree to which relationship can be established between two or more products of a development
|
||||
process, especially those having a predecessor/successor or master/subordinate relationship to one
|
||||
another\<close>
|
||||
|
||||
Definition*[validation::concept]
|
||||
Definition*[validation::sfc, short_name="''validation''"]
|
||||
\<open>process of analysis followed by a judgment based on evidence to
|
||||
documentation, software or application) fits the user needs,in particular with respect to safety
|
||||
and quality and determine whether an item (e.g. process, with emphasis on the suitability of its
|
||||
operation in accordance to its purpose in its intended environment\<close>
|
||||
|
||||
Definition*[validator::concept]
|
||||
Definition*[validator::sfc, short_name="''validator''"]
|
||||
\<open>entity that is responsible for the validation\<close>
|
||||
|
||||
Definition*[verification::concept]
|
||||
Definition*[verification::sfc, short_name="''verification''"]
|
||||
\<open>process of examination followed by a judgment based on evidence that output items (process,
|
||||
documentation, software or application) of a specific development phase fulfils the requirements of
|
||||
that phase with respect to completeness, correctness and consistency.
|
||||
NOTE Verification is mostly based on document reviews (design, implementation, test documents etc.).
|
||||
\<close>
|
||||
|
||||
Definition*[verifier::concept]
|
||||
Definition*[verifier::sfc, short_name="''verifier''"]
|
||||
\<open>entity that is responsible for one or more verification activities\<close>
|
||||
|
||||
|
||||
|
@ -388,7 +400,7 @@ doc_class SIR = requirement +
|
|||
type_synonym safety_integrity_requirement = SIR
|
||||
|
||||
text\<open>The following class is a bit unclear about usage and seems to be in
|
||||
conceptual mismatch with @{typ objectives}: \<close>
|
||||
sfcual mismatch with @{typ objectives}: \<close>
|
||||
doc_class SILA = requirement +
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
alloc :: "sil" <= "SIL0"
|
||||
|
@ -603,7 +615,7 @@ text\<open>Objective:
|
|||
The objective of software verification is to examine and arrive at a judgement based on evidence
|
||||
that output items (process, documentation, software or application) of a specific development
|
||||
phase fulfil the requirements and plans with respect to completeness, correctness and consistency.
|
||||
These activities are managed by the @{concept \<open>verifier\<close>}.
|
||||
These activities are managed by the @{semi_formal_content \<open>verifier\<close>}.
|
||||
\<close>
|
||||
|
||||
text\<open>Outputs:
|
||||
|
@ -705,7 +717,7 @@ doc_class test_documentation =
|
|||
|
||||
section\<open> META : Testing and Validation \<close>
|
||||
|
||||
text\<open>Test : @{concept \<open>COTS\<close>}\<close>
|
||||
text\<open>Test : @{semi_formal_content \<open>COTS\<close>}\<close>
|
||||
|
||||
ML\<open>
|
||||
DOF_core.read_cid_global @{theory} "requirement";
|
||||
|
|
|
@ -11,7 +11,7 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
*************************************************************************)
|
||||
|
||||
chapter \<open>The Document Ontology Common Library for the Isabelle Ontology Framework\<close>
|
||||
chapter \<open>A Math Paper Ontology (obsolete vs. scholarly_paper)\<close>
|
||||
|
||||
text\<open> Offering support for common Isabelle Elements like definitions, lemma- and theorem
|
||||
statements, proofs, etc. Isabelle is a lot of things, but it is an interactive theorem
|
||||
|
|
|
@ -160,7 +160,7 @@
|
|||
|
||||
% \newcommand{\formalMathStmt[label, mcc, ]
|
||||
% end: scholarly_paper.abstract
|
||||
|
||||
% | "rule" | "assn" | "expl" | rem | "notation" | "terminology"
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\newisadof{text.scholarly_paper.math_content}%
|
||||
[label=,type=%
|
||||
|
@ -210,16 +210,16 @@
|
|||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
|
||||
{\begin{lemma} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\label{\commandkey{label}} #1
|
||||
\end{lemma}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{ex}}
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{expl}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
|
||||
{\begin{example} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\label{\commandkey{label}} #1
|
||||
\end{example}}
|
||||
}%
|
||||
}%
|
||||
|
@ -234,24 +234,63 @@
|
|||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{prop}}
|
||||
{%
|
||||
\begin{property}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{property}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{property} \label{\commandkey{label}} #1 \end{property} }
|
||||
{\begin{property} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{property}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rule}}
|
||||
{%
|
||||
\begin{ruleX}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{ruleX}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{ruleX} \label{\commandkey{label}} #1 \end{ruleX} }
|
||||
{\begin{ruleX} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{ruleX}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rem}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{remark} \label{\commandkey{label}} #1 \end{remark} }
|
||||
{\begin{remark} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{remark}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{assn}}
|
||||
{%
|
||||
\begin{assertion}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{assertion}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{assertion} \label{\commandkey{label}} #1 \end{assertion} }
|
||||
{\begin{assertion} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{assertion}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{notation}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{notation} \label{\commandkey{label}} #1 \end{notation} }
|
||||
{\begin{notation} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{notation}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{terminology}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{terminology} \label{\commandkey{label}} #1 \end{terminology} }
|
||||
{\begin{terminology} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{terminology}}
|
||||
}%
|
||||
}%
|
||||
{%
|
||||
\typeout{Internal error: enumeration out of sync}
|
||||
\typeout{Internal error: enumeration out of sync with ontology scholarly-paper.}
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
|
|
|
@ -123,8 +123,9 @@ provided \<^emph>\<open>theorem environments\<close> (see \<^verbatim>\<open>tex
|
|||
\<^verbatim>\<open>axiom\<close>, \<^verbatim>\<open>rule\<close> and \<^verbatim>\<open>assertion\<close> to the list. A particular advantage of \<^verbatim>\<open>texdoc amslatex\<close> is
|
||||
that it is well-established and compatible with many LaTeX - styles.\<close>
|
||||
|
||||
datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop"
|
||||
| "ex" | "rule" | "assn"
|
||||
datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop"
|
||||
| "expl" | "rule" | "assn"
|
||||
| rem | "notation" | "terminology"
|
||||
|
||||
(*
|
||||
thm Theorem Italic
|
||||
|
@ -132,7 +133,7 @@ cor Corollary Italic
|
|||
lem Lemma Italic
|
||||
prop Proposition
|
||||
defn Definition
|
||||
ex Example
|
||||
expl Example
|
||||
|
||||
rem Remark
|
||||
notation
|
||||
|
@ -184,27 +185,41 @@ type_synonym math_sfc = math_semiformal
|
|||
|
||||
subsection\<open>Instances of the abstract classes Definition / Class / Lemma etc.\<close>
|
||||
|
||||
text\<open>A rough structuring is modeled as follows:\<close>
|
||||
text\<open>The key class definitions are motivated \<close>
|
||||
|
||||
doc_class "definition" = math_content +
|
||||
referentiable :: bool <= True
|
||||
mcc :: "math_content_class" <= "defn"
|
||||
invariant d1 :: "\<lambda> \<sigma>::definition. mcc \<sigma> = defn"
|
||||
|
||||
doc_class "theorem" = math_content +
|
||||
referentiable :: bool <= True
|
||||
mcc :: "math_content_class" <= "thm"
|
||||
invariant d2 :: "\<lambda> \<sigma>::theorem. mcc \<sigma> = thm"
|
||||
|
||||
text\<open>Note that the following two text-elements are currently set to no-keyword in LNCS style.\<close>
|
||||
doc_class "lemma" = math_content +
|
||||
referentiable :: bool <= "True"
|
||||
mcc :: "math_content_class" <= "lem"
|
||||
invariant d3 :: "\<lambda> \<sigma>::lemma. mcc \<sigma> = lem"
|
||||
|
||||
doc_class "corollary" = math_content +
|
||||
referentiable :: bool <= "True"
|
||||
mcc :: "math_content_class" <= "cor"
|
||||
invariant d4 :: "\<lambda> \<sigma>::corollary. mcc \<sigma> = thm"
|
||||
|
||||
doc_class "example" = math_content +
|
||||
referentiable :: bool <= "True"
|
||||
mcc :: "math_content_class" <= "expl"
|
||||
invariant d5 :: "\<lambda> \<sigma>::example. mcc \<sigma> = expl"
|
||||
|
||||
|
||||
subsection\<open>Example Statements\<close>
|
||||
|
||||
text\<open> \<^verbatim>\<open>examples\<close> are currently considered \<^verbatim>\<open>technical\<close>. Is a main category to be refined
|
||||
via inheritance. \<close>
|
||||
|
||||
doc_class example = technical +
|
||||
doc_class tech_example = technical +
|
||||
referentiable :: bool <= True
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
|
|
|
@ -11,7 +11,11 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
*************************************************************************)
|
||||
|
||||
chapter\<open>Inner Syntax Antiquotations (ISA)'s\<close>
|
||||
chapter\<open>Term Antiquotations\<close>
|
||||
|
||||
text\<open>Terms are represented by "Inner Syntax" parsed by an Earley parser in Isabelle.
|
||||
For historical reasons, term antiquotations are called therefore somewhat misleadingly
|
||||
"Inner Syntax Antiquotations". \<close>
|
||||
|
||||
theory
|
||||
InnerSyntaxAntiquotations
|
||||
|
|
Loading…
Reference in New Issue