added define_macros, corrections in 02_Background

This commit is contained in:
Burkhart Wolff 2020-08-26 14:38:39 +02:00
parent 00c4d15259
commit 41a1eaed44
7 changed files with 83 additions and 62 deletions

View File

@ -1,7 +1,7 @@
theory PikeOS_ST (*Security Target *)
imports "../../../src/ontologies/CC_v3.1_R5/CC_v3_1_R5"
(* Isabelle_DOF.CommonCriteria_15408 *)
(* Isabelle_DOF.CC_v3_1_R5 in the future. *)
begin
@ -14,7 +14,7 @@ subsection*[pkosstrefsubsec::st_ref_cls]\<open> ST Reference \<close>
text*[pkosstref::st_ref_cls, title="''PikeOS Security Target''", st_version ="(0,4,5)",
authors= "[]", st_date= "''29072020''"]
\<open>This document is the @{docitem st_def} for the Common Criteria evaluation of PikeOS.
\<open>This document is the @{docitem st} for the Common Criteria evaluation of PikeOS.
It complies with the Common Criteria for Information Technology Security Evaluation
Version 3.1 Revision 4.\<close>
@ -29,7 +29,7 @@ text*[pkostoeref::toe_ref_cls, dev_name="''''", toe_name="''PikeOS''",
Certification Kit build S4250 and PikeOS 3.4 Common Criteria Kit build S4388.\<close>
subsection*[pkossttoeovrvwsubsec::st_ref_cls]\<open> TOE Overview \<close>
text*[pkosovrw1::toe_ovrw_cls]\<open>The @{definition \<open>toe_def\<close> } is a special kind of operating
text*[pkosovrw1::toe_ovrw_cls]\<open>The @{definition \<open>toe\<close> } is a special kind of operating
system, that allows to effectively separate
different applications running on the same platform from each other. The TOE can host
user applications that can also be operating systems. User applications can also be

View File

@ -19,13 +19,13 @@ begin
section\<open>Document Local Setup.\<close>
text\<open>Some internal setup, introducing document specific abbreviations and macros.\<close>
setup \<open>DOF_lib.define_shortcut ("dof",\<^here>) "\\dof"\<close>
setup \<open>DOF_lib.define_shortcut ("isadof",\<^here>) "\\isadof"\<close>
setup \<open> DOF_lib.define_shortcut ("eg",\<^here>) "\\eg"
#> DOF_lib.define_shortcut ("ie",\<^here>) "\\ie"\<close>
setup \<open>DOF_lib.define_shortcut \<^binding>\<open>dof\<close> "\\dof"\<close>
setup \<open>DOF_lib.define_shortcut \<^binding>\<open>isadof\<close> "\\isadof"\<close>
setup \<open> DOF_lib.define_shortcut \<^binding>\<open>eg\<close> "\\eg"
#> DOF_lib.define_shortcut \<^binding>\<open>ie\<close> "\\ie"\<close>
(* this is an alternative style for macro definitions eauivalent to setup ... setup ...*)
setup \<open> DOF_lib.define_shortcut ("TeXLive",\<^here>) "\\TeXLife"
#> DOF_lib.define_shortcut ("LaTeX",\<^here>) "\\LaTeX{}"\<close>
setup \<open> DOF_lib.define_shortcut \<^binding>\<open>TeXLive\<close>"\\TeXLife"
#> DOF_lib.define_shortcut \<^binding>\<open>LaTeX\<close> "\\LaTeX{}"\<close>
text\<open>Note that these setups assume that the \<^LaTeX> macros are defined in the
document prelude. \<close>

View File

@ -23,7 +23,7 @@ The linking of the \<^emph>\<open>formal\<close> to the \<^emph>\<open>informal\
digitization of knowledge and its propagation. This challenge incites numerous research efforts
summarized under the labels ``semantic web,'' ``data mining,'' or any form of advanced ``semantic''
text processing. A key role in structuring this linking play \<^emph>\<open>document ontologies\<close> (also called
\<^emph>\<open>vocabulary\<close> in the semantic web community~@{cite "w3c:ontologies:2015"}), \ie, a machine-readable
\<^emph>\<open>vocabulary\<close> in the semantic web community~@{cite "w3c:ontologies:2015"}), \<^ie>, a machine-readable
form of the structure of documents as well as the document discourse.
Such ontologies can be used for the scientific discourse within scholarly articles, mathematical
@ -42,21 +42,21 @@ In general, an ontology is a formal explicit description of \<^emph>\<open>conce
as \<^emph>\<open>links\<close> between them. A particular link between concepts is the \<^emph>\<open>is-a\<close> relation declaring
the instances of a subclass to be instances of the super-class.
To adress this challenge, we present the Document Ontology Framework (\dof) and an
implementation of \dof called \isadof. \dof is designed for building scalable and user-friendly
tools on top of interactive theorem provers. \isadof is an instance of this novel framework,
To address this challenge, we present the Document Ontology Framework (\<^dof>) and an
implementation of \<^dof> called \<^isadof>. \<^dof> is designed for building scalable and user-friendly
tools on top of interactive theorem provers. \<^isadof> is an instance of this novel framework,
implemented as extension of Isabelle/HOL, to \<^emph>\<open>model\<close> typed ontologies and to \<^emph>\<open>enforce\<close> them
during document evolution. Based on Isabelle's infrastructures, ontologies may refer to types,
terms, proven theorems, code, or established assertions. Based on a novel adaption of the Isabelle
IDE (called PIDE, @{cite "wenzel:asynchronous:2014"}), a document is checked to be
\<^emph>\<open>conform\<close> to a particular ontology---\isadof is designed to give fast user-feedback \<^emph>\<open>during the
\<^emph>\<open>conform\<close> to a particular ontology---\<^isadof> is designed to give fast user-feedback \<^emph>\<open>during the
capture of content\<close>. This is particularly valuable in case of document evolution, where the
\<^emph>\<open>coherence\<close> between the formal and the informal parts of the content can be mechanically checked.
To avoid any misunderstanding: \isadof is \<^emph>\<open>not a theory in HOL\<close> on ontologies and operations to
To avoid any misunderstanding: \<^isadof> is \<^emph>\<open>not a theory in HOL\<close> on ontologies and operations to
track and trace links in texts, it is an \<^emph>\<open>environment to write structured text\<close> which
\<^emph>\<open>may contain\<close> Isabelle/HOL definitions and proofs like mathematical articles, tech-reports and
scientific papers---as the present one, which is written in \isadof itself. \isadof is a plugin
scientific papers---as the present one, which is written in \<^isadof> itself. \<^isadof> is a plugin
into the Isabelle/Isar framework in the style of~@{cite "wenzel.ea:building:2007"}.\<close>
subsubsection\<open>How to Read This Manual\<close>
@ -69,28 +69,28 @@ declare_reference*[isadof_developers::text_section]
text\<open>
This manual can be read in different ways, depending on what you want to accomplish. We see three
different main user groups:
\<^enum> \<^emph>\<open>\isadof users\<close>, \ie, users that just want to edit a core document, be it for a paper or a
\<^enum> \<^emph>\<open>\<^isadof> users\<close>, \<^ie>, users that just want to edit a core document, be it for a paper or a
technical report, using a given ontology. These users should focus on
@{docitem (unchecked) \<open>isadof_tour\<close>} and, depending on their knowledge of Isabelle/HOL, also
@{docitem (unchecked) \<open>background\<close>}.
\<^enum> \<^emph>\<open>Ontology developers\<close>, \ie, users that want to develop new ontologies or modify existing
\<^enum> \<^emph>\<open>Ontology developers\<close>, \<^ie>, users that want to develop new ontologies or modify existing
document ontologies. These users should, after having gained acquaintance as a user, focus
on @{docitem (unchecked) \<open>isadof_ontologies\<close>}.
\<^enum> \<^emph>\<open>\isadof developers\<close>, \ie, users that want to extend or modify \isadof, \eg, by adding new
\<^enum> \<^emph>\<open>\<^isadof> developers\<close>, \<^ie>, users that want to extend or modify \<^isadof>, \<^eg>, by adding new
text-elements. These users should read @{docitem (unchecked) \<open>isadof_developers\<close>}
\<close>
subsubsection\<open>Typographical Conventions\<close>
text\<open>
We acknowledge that understanding \isadof and its implementation in all details requires
We acknowledge that understanding \<^isadof> and its implementation in all details requires
separating multiple technological layers or languages. To help the reader with this, we
will type-set the different languages in different styles. In particular, we will use
\<^item> a light-blue background for input written in Isabelle's Isar language, \eg:
\<^item> a light-blue background for input written in Isabelle's Isar language, \<^eg>:
\begin{isar}
lemma refl: "x = x"
by simp
\end{isar}
\<^item> a green background for examples of generated document fragments (\ie, PDF output):
\<^item> a green background for examples of generated document fragments (\<^ie>, PDF output):
\begin{out}
The axiom refl
\end{out}
@ -111,8 +111,8 @@ text\<open>
subsubsection\<open>How to Cite \isadof\<close>
text\<open>
If you use or extend \isadof in your publications, please use
\<^item> for the \isadof system~@{cite "brucker.ea:isabelle-ontologies:2018"}:
If you use or extend \<^isadof> in your publications, please use
\<^item> for the \<^isadof> system~@{cite "brucker.ea:isabelle-ontologies:2018"}:
\begin{quote}\small
A.~D. Brucker, I.~Ait-Sadoune, P.~Crisafulli, and B.~Wolff. Using the {Isabelle} ontology
framework: Linking the formal with the informal. In \<^emph>\<open>Conference on Intelligent Computer
@ -122,9 +122,9 @@ text\<open>
\end{quote}
A \BibTeX-entry is available at:
\url{https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018}.
\<^item> for the implementation of \isadof~@{cite "brucker.ea:isabelledof:2019"}:
\<^item> for the implementation of \<^isadof>~@{cite "brucker.ea:isabelledof:2019"}:
\begin{quote}\small
A.~D. Brucker and B.~Wolff. \isadof: Design and implementation. In P.C.~{\"O}lveczky and
A.~D. Brucker and B.~Wolff. \<^isadof>: Design and implementation. In P.C.~{\"O}lveczky and
G.~Sala{\"u}n, editors, \<^emph>\<open>Software Engineering and Formal Methods (SEFM)\<close>, number 11724 in
Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
\href{https://doi.org/10.1007/978-3-030-30446-1_15}{10.1007/978-3-030-30446-1\_15}.
@ -136,7 +136,7 @@ text\<open>
subsubsection\<open>Availability\<close>
text\<open>
The implementation of the framework is available at
\url{\dofurl}. The website also provides links to the latest releases. \isadof is licensed
\url{\dofurl}. The website also provides links to the latest releases. \<^isadof> is licensed
under a 2-clause BSD license (SPDX-License-Identifier: BSD-2-Clause).
\<close>

View File

@ -1,7 +1,7 @@
(*************************************************************************
* Copyright (C)
* 2019 The University of Exeter
* 2018-2019 The University of Paris-Saclay
* 2019-2020 The University of Exeter
* 2018-2020 The University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
@ -49,14 +49,14 @@ The Isabelle system architecture shown in @{docitem \<open>architecture\<close>}
with Standard ML (SML) at the bottom layer as implementation language. The architecture actually
foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \inlinesml{Context}.
This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an
ancestor-list as well as typed, user-defined state for components (plugins) such as \isadof.
ancestor-list as well as typed, user-defined state for components (plugins) such as \<^isadof>.
On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific
support for higher specification constructs were built.\<close>
section*[dof::introduction]\<open>The Document Model Required by \dof\<close>
section*[dof::introduction]\<open>The Document Model Required by \<^dof> \<close>
text\<open>
In this section, we explain the assumed document model underlying our Document Ontology Framework
(\dof) in general. In particular we discuss the concepts \<^emph>\<open>integrated document\<close>, \<^emph>\<open>sub-document\<close>,
(\<^dof>) in general. In particular we discuss the concepts \<^emph>\<open>integrated document\<close>, \<^emph>\<open>sub-document\<close>,
\<^emph>\<open>text-element\<close> and \<^emph>\<open>semantic macros\<close> occurring inside text-elements. Furthermore, we assume two
different levels of parsers (for \<^emph>\<open>outer\<close> and \<^emph>\<open>inner syntax\<close>) where the inner-syntax is basically
a typed \inlineisar|\<lambda>|-calculus and some Higher-order Logic (HOL).
@ -68,7 +68,7 @@ declare_reference*["fig:dependency"::text_section]
text\<open>
We assume a hierarchical document model\index{document model}, \ie, an \<^emph>\<open>integrated\<close> document
We assume a hierarchical document model\index{document model}, \<^ie>, an \<^emph>\<open>integrated\<close> document
consist of a hierarchy \<^emph>\<open>sub-documents\<close> (files) that can depend acyclically on each other.
Sub-documents can have different document types in order to capture documentations consisting of
documentation, models, proofs, code of various forms and other technical artifacts. We call the
@ -91,9 +91,9 @@ text\<open>
separate commands from each other.
We distinguish fundamentally two different syntactic levels:
\<^item> the *\<open>outer-syntax\<close>\bindex{syntax!outer}\index{outer syntax|see {syntax, outer}} (\ie, the
\<^item> the *\<open>outer-syntax\<close>\bindex{syntax!outer}\index{outer syntax|see {syntax, outer}} (\<^ie>, the
syntax for commands) is processed by a lexer-library and parser combinators built on top, and
\<^item> the *\<open>inner-syntax\<close>\bindex{syntax!inner}\index{inner syntax|see {syntax, inner}} (\ie, the
\<^item> the *\<open>inner-syntax\<close>\bindex{syntax!inner}\index{inner syntax|see {syntax, inner}} (\<^ie>, the
syntax for \inlineisar|\<lambda>|-terms in HOL) with its own parametric polymorphism type
checking.
@ -101,19 +101,19 @@ text\<open>
On the semantic level, we assume a validation process for an integrated document, where the
semantics of a command is a transformation \inlineisar+\<theta> \<rightarrow> \<theta>+ for some system state
\inlineisar+\<theta>+. This document model can be instantiated with outer-syntax commands for common
text elements, \eg, \inlineisar+section{*...*}+ or \inlineisar+text{*...*}+. Thus, users can add
text elements, \<^eg>, \inlineisar+section{*...*}+ or \inlineisar+text{*...*}+. Thus, users can add
informal text to a sub-document using a text command:
\begin{isar}
text\<Open>This is a description.\<Close>
\end{isar}
This will type-set the corresponding text in, for example, a PDF document. However, this
translation is not necessarily one-to-one: text elements can be enriched by formal, \ie,
translation is not necessarily one-to-one: text elements can be enriched by formal, \<^ie>,
machine-checked content via *\<open>semantic macros\<close>, called antiquotations\bindex{antiquotation}:
\begin{isar}
text\<Open>According to the *\<Open>reflexivity\<Close> axiom <@>{thm refl}, we obtain in \<Gamma>
for <@>{term "fac 5"} the result <@>{value "fac 5"}.\<Close>
\end{isar}
which is represented in the final document (\eg, a PDF) by:
which is represented in the final document (\<^eg>, a PDF) by:
\begin{out}
According to the \emph{reflexivity} axiom $\mathrm{x = x}$, we obtain in $\Gamma$ for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.
\end{out}
@ -132,41 +132,41 @@ figure*["fig:dependency"::figure,relative_width="70",src="''figures/document-hie
section*[bgrnd21::introduction]\<open>Implementability of the Required Document Model.\<close>
text\<open>
Batch-mode checkers for \dof can be implemented in all systems of the LCF-style prover family,
\ie, systems with a type-checked \inlinesml{term}, and abstract \inlinesml{thm}-type for
theorems (protected by a kernel). This includes, \eg, ProofPower, HOL4, HOL-light, Isabelle, or
Coq and its derivatives. \dof is, however, designed for fast interaction in an IDE. If a user wants
Batch-mode checkers for \<^dof> can be implemented in all systems of the LCF-style prover family,
\<^ie>, systems with a type-checked \inlinesml{term}, and abstract \inlinesml{thm}-type for
theorems (protected by a kernel). This includes, \<^eg>, ProofPower, HOL4, HOL-light, Isabelle, or
Coq and its derivatives. \<^dof> is, however, designed for fast interaction in an IDE. If a user wants
to benefit from this experience, only Isabelle and Coq have the necessary infrastructure of
asynchronous proof-processing and support by a PIDE~@{cite "wenzel:asynchronous:2014" and
"wenzel:system:2014" and "barras.ea:pervasive:2013"
and "faithfull.ea:coqoon:2018"} which in many features over-accomplishes the required
features of \dof. For example, current Isabelle versions offer cascade-syntaxes (different
features of \<^dof>. For example, current Isabelle versions offer cascade-syntaxes (different
syntaxes and even parser-technologies which can be nested along the
\inlineisar+\<Open> ... \<Close> + barriers, while \dof actually only requires a two-level
\inlineisar+\<Open> ... \<Close> + barriers, while \<^dof> actually only requires a two-level
syntax model.
\<close>
figure*["fig:dof-ide"::figure,relative_width="95",src="''figures/cicm2018-combined''"]\<open>
The \isadof IDE (left) and the corresponding PDF (right), showing the first page
The \<^isadof> IDE (left) and the corresponding PDF (right), showing the first page
of~\cite{brucker.ea:isabelle-ontologies:2018}.\<close>
text\<open>
We call the present implementation of \dof on the Isabelle platform \isadof.
We call the present implementation of \<^dof> on the Isabelle platform \<^isadof> .
@{docitem "fig:dof-ide"} shows a screen-shot of an introductory paper on
\isadof~@{cite "brucker.ea:isabelle-ontologies:2018"}: the \isadof PIDE can be seen on the left,
\<^isadof>~@{cite "brucker.ea:isabelle-ontologies:2018"}: the \<^isadof> PIDE can be seen on the left,
while the generated presentation in PDF is shown on the right.
Isabelle provides, beyond the features required for \dof, a lot of additional benefits. For
Isabelle provides, beyond the features required for \<^dof>, a lot of additional benefits. For
example, it also allows the asynchronous evaluation and checking of the document
content~@{cite "wenzel:asynchronous:2014" and "wenzel:system:2014" and
"barras.ea:pervasive:2013"} and is dynamically extensible. Its PIDE provides a
\<^emph>\<open>continuous build, continuous check\<close> functionality, syntax highlighting, and auto-completion.
It also provides infrastructure for displaying meta-information (\eg, binding and type annotation)
It also provides infrastructure for displaying meta-information (\<^eg>, binding and type annotation)
as pop-ups, while hovering over sub-expressions. A fine-grained dependency analysis allows the
processing of individual parts of theory files asynchronously, allowing Isabelle to interactively
process large (hundreds of theory files) documents. Isabelle can group sub-documents into sessions,
\ie, sub-graphs of the document-structure that can be ``pre-compiled'' and loaded
instantaneously, \ie, without re-processing. \<close>
\<^ie>, sub-graphs of the document-structure that can be ``pre-compiled'' and loaded
instantaneously, \<^ie>, without re-processing. \<close>
(*<*)
end

View File

@ -228,14 +228,22 @@ end
section\<open>Shortcuts, Macros, Environments\<close>
text\<open>This is actually \<^emph>\<open>not\<close> a real DOF feature, rather a slightly more abstract layer over
slightly buried standard features of the Isabelle document generator ... \<close>
somewhat buried standard features of the Isabelle document generator ... \<close>
ML\<open>
structure DOF_lib =
struct
fun define_shortcut (name, pos) latexshcut =
Thy_Output.antiquotation_raw (Binding.make(name,pos)) (Scan.succeed ())
fun define_shortcut name latexshcut =
Thy_Output.antiquotation_raw name (Scan.succeed ())
(fn _ => fn () => Latex.string latexshcut)
(* This is just a copy of Isabelle2020 function "control_antiquotation" from
document_antiquotations.ML, where it is unfortunately not exported. (Thanks Makarius!)
*)
fun define_macro name s1 s2 =
Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input)
(fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_document ctxt {markdown = false});
end
\<close>

View File

@ -323,7 +323,7 @@ Definition* [sr_def::concept, tag="''security requirement''", short_tag="Some(''
\<open>requirement, stated in a standardised language, which is meant to contribute
to achieving the security objectives for a TOE\<close>
text \<open>@{docitem toe_def}\<close>
Definition* [st_def::concept, tag="''Security Target''", short_tag="Some(''ST'')"]
Definition* [st::concept, tag="''Security Target''", short_tag="Some(''ST'')"]
\<open>implementation-dependent statement of security needs for a specific i\<section>dentified @{docitem toe_def}\<close>
Definition* [slct_def::concept, tag="''selection''"]
@ -350,7 +350,7 @@ Definition* [st_eval_def::concept, tag="''ST evaluation''"]
Definition* [subj_def::concept, tag="''subject''"]
\<open>active entity in the TOE that performs operations on objects\<close>
Definition* [toe_def::concept, tag= "''target of evaluation''"]
Definition* [toe::concept, tag= "''target of evaluation''"]
\<open>set of software, firmware and/or hardware possibly accompanied by guidance\<close>
Definition* [thrt_agnt_def::concept, tag="''threat agent''"]
@ -417,7 +417,7 @@ Definition* [dev_def::concept, tag="''Developer''"]
\<open>who respond to actual or perceived consumer security requirements in
constructing a @{docitem toe_def}, reference this CC_Part_3
when interpreting statements of assurance requirements and determining
assurance approaches of @{docitem toe_def}s.\<close>
assurance approaches of @{docitem toe}s.\<close>
Definition*[evalu_def::concept, tag="'' Evaluator''"]
\<open>who use the assurance requirements defined in CC_Part_3

View File

@ -148,11 +148,15 @@ textN\<open>... and here is its application macro expansion:
textN\<open> \<^theory_text>\<open>definition df = ...
\<close>
@{ML [display] \<open> let val x = 3 + 4 in true end \<close>}
@{ML [display] \<open> let val x = 3 + 4 in true end
\<close>}
@{ML_text [display] \<open> val x = ...
\<close>}
@{verbatim [display] \<open> Lorem ipsum ... @{thm refl} _
Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>}
@{theory_text [display] \<open>definition df = ...
@{theory_text [display] \<open>definition df = ... \<lambda>x.
\<close>}
@{cartouche [display] \<open> @{figure "cfgdfg"}\<close>} \<close>
@ -180,10 +184,19 @@ val _ =
textN\<open> \<^doof> \<^LATEX> \<close>
(* the same effect is achieved with : *)
setup \<open>DOF_lib.define_shortcut ("bla",\<^here>) "\\blabla"\<close>
(* Note that this assumes that the generated LaTeX macro "blabla" is defined somewhere in the
target document, for example, in the tex prelude. *)
setup \<open>DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\<close>
(* Note that this assumes that the generated LaTeX macro call "\blabla" is defined somewhere in the
target document, for example, in the tex prelude. Note that the "Binding.make" can be avoided
using the alternative \<^binding> notation (see above).*)
ML\<open>
fun control_antiquotation name s1 s2 =
Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input)
(fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_document ctxt {markdown = false});
\<close>
end
(*>*)