forked from Isabelle_DOF/Isabelle_DOF
More markdown in the IsaDofApplications example.
The new setup is now checked on a Mac for the first time.
This commit is contained in:
parent
61d69394c3
commit
e4bb874d86
|
@ -108,7 +108,7 @@ figure*[fig_B::figure, spawn_columns=False,relative_width="''90''",
|
||||||
\<open> The B train \ldots \<close>
|
\<open> The B train \ldots \<close>
|
||||||
update_instance*[figs1::figure_group, trace+="[figure]"]
|
update_instance*[figs1::figure_group, trace+="[figure]"]
|
||||||
|
|
||||||
close_monitor*[fig1]
|
close_monitor*[figs1]
|
||||||
|
|
||||||
ML\<open> map (fn Const(s,_) => s) (HOLogic.dest_list @{docitem_attr trace::figs1}) \<close>
|
ML\<open> map (fn Const(s,_) => s) (HOLogic.dest_list @{docitem_attr trace::figs1}) \<close>
|
||||||
|
|
||||||
|
|
|
@ -46,7 +46,7 @@ text*[xcv4::F, r="[@{thm ''HOL.refl''},
|
||||||
text*[xcv5::G, g="@{thm ''HOL.sym''}"]\<open>Lorem ipsum ...\<close>
|
text*[xcv5::G, g="@{thm ''HOL.sym''}"]\<open>Lorem ipsum ...\<close>
|
||||||
|
|
||||||
text\<open>... and here we add a relation between @{docitem \<open>xcv3\<close>} and @{docitem \<open>xcv2\<close>}
|
text\<open>... and here we add a relation between @{docitem \<open>xcv3\<close>} and @{docitem \<open>xcv2\<close>}
|
||||||
into the relation \verb+b+ of @{docitem_ref \<open>xcv5\<close>}. Note that in the link-relation,
|
into the relation \verb+b+ of @{docitem \<open>xcv5\<close>}. Note that in the link-relation,
|
||||||
a @{typ "C"}-type is required, but a @{typ "G"}-type is offered which is leagal in
|
a @{typ "C"}-type is required, but a @{typ "G"}-type is offered which is leagal in
|
||||||
\verb+Isa_DOF+ because of the sub-class relation between those classes: \<close>
|
\verb+Isa_DOF+ because of the sub-class relation between those classes: \<close>
|
||||||
update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"]
|
update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"]
|
||||||
|
|
|
@ -74,12 +74,13 @@ framework in the style of~\cite{wenzel.ea:building:2007}.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
(* declaring the forward references used in the subsequent section *)
|
(* declaring the forward references used in the subsequent section *)
|
||||||
|
(*<*)
|
||||||
declare_reference*[bgrnd::text_section]
|
declare_reference*[bgrnd::text_section]
|
||||||
declare_reference*[isadof::text_section]
|
declare_reference*[isadof::text_section]
|
||||||
declare_reference*[ontomod::text_section]
|
declare_reference*[ontomod::text_section]
|
||||||
declare_reference*[ontopide::text_section]
|
declare_reference*[ontopide::text_section]
|
||||||
declare_reference*[conclusion::text_section]
|
declare_reference*[conclusion::text_section]
|
||||||
|
(*>*)
|
||||||
text*[plan::introduction]\<open> The plan of the paper is follows: we start by introducing the underlying
|
text*[plan::introduction]\<open> The plan of the paper is follows: we start by introducing the underlying
|
||||||
Isabelel sytem (@{docitem_ref (unchecked) \<open>bgrnd\<close>}) followed by presenting the
|
Isabelel sytem (@{docitem_ref (unchecked) \<open>bgrnd\<close>}) followed by presenting the
|
||||||
essentials of \isadof and its ontology language (@{docitem_ref (unchecked) \<open>isadof\<close>}).
|
essentials of \isadof and its ontology language (@{docitem_ref (unchecked) \<open>isadof\<close>}).
|
||||||
|
@ -104,19 +105,18 @@ it is the \emph{Eclipse of Formal Methods Tools}. This refers to the
|
||||||
explicit infrastructure for building derivative
|
explicit infrastructure for building derivative
|
||||||
\emph{systems}.}''~\cite{wenzel.ea:building:2007}
|
\emph{systems}.}''~\cite{wenzel.ea:building:2007}
|
||||||
|
|
||||||
The current system framework offers moreover the following features:
|
The current system framework offers moreover the following features:
|
||||||
\begin{itemize}
|
|
||||||
\item a build management grouping components into to pre-compiled sessions,
|
\<^item> a build management grouping components into to pre-compiled sessions,
|
||||||
\item a prover IDE (PIDE) framework~\cite{wenzel:asynchronous:2014} with
|
\<^item> a prover IDE (PIDE) framework~\cite{wenzel:asynchronous:2014} with various front-ends
|
||||||
various front-ends
|
\<^item> documentation - and code generators,
|
||||||
\item documentation - and code generators,
|
\<^item> an extensible front-end language Isabelle/Isar, and,
|
||||||
\item an extensible front-end language Isabelle/Isar, and,
|
\<^item> last but not least, an LCF style, generic theorem prover kernel as
|
||||||
\item last but not least, an LCF style, generic theorem prover kernel as
|
|
||||||
the most prominent and deeply integrated system component.
|
the most prominent and deeply integrated system component.
|
||||||
\end{itemize}
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
figure*[architecture::figure,relative_width="100",src="''figures/isabelle-architecture''"]\<open> The system architecture of Isabelle (left-hand side) and the
|
figure*[architecture::figure,relative_width="100",src="''figures/isabelle-architecture''"]\<open>
|
||||||
|
The system architecture of Isabelle (left-hand side) and the
|
||||||
asynchronous communication between the Isabelle system and
|
asynchronous communication between the Isabelle system and
|
||||||
the IDE (right-hand side). \<close>
|
the IDE (right-hand side). \<close>
|
||||||
|
|
||||||
|
@ -145,8 +145,7 @@ Now, \emph{inside} the textual content, it is possible to embed a \emph{text-ant
|
||||||
\end{isar}
|
\end{isar}
|
||||||
which is represented in the generated output by:
|
which is represented in the generated output by:
|
||||||
\begin{out}
|
\begin{out}
|
||||||
According to the reflexivity axiom $x = x$, we obtain in $\Gamma$ for $\operatorname{fac} 5$
|
According to the reflexivity axiom $x = x$, we obtain in $\Gamma$ for $\operatorname{fac} 5$ the result $120$.
|
||||||
the result $120$.
|
|
||||||
\end{out}
|
\end{out}
|
||||||
where \inlineisar+refl+ is actually the reference to the axiom of reflexivity in HOL.
|
where \inlineisar+refl+ is actually the reference to the axiom of reflexivity in HOL.
|
||||||
For the antiquotation \inlineisar+\at{value "fac 5"}+ we assume the usual definition for
|
For the antiquotation \inlineisar+\at{value "fac 5"}+ we assume the usual definition for
|
||||||
|
@ -161,16 +160,15 @@ Isabelle's PIDE offers auto-completion and error-messages while typing the above
|
||||||
section*[isadof::technical,main_author="Some(@{docitem ''adb''}::author)"]\<open> \isadof \<close>
|
section*[isadof::technical,main_author="Some(@{docitem ''adb''}::author)"]\<open> \isadof \<close>
|
||||||
|
|
||||||
text\<open> An \isadof document consists of three components:
|
text\<open> An \isadof document consists of three components:
|
||||||
\begin{itemize}
|
\<^item> the @{emph \<open>ontology definition\<close>} which is an Isabelle theory file with definitions
|
||||||
\item the @{emph \<open>ontology definition\<close>} which is an Isabelle theory file with definitions
|
|
||||||
for document-classes and all auxiliary datatypes.
|
for document-classes and all auxiliary datatypes.
|
||||||
\item the @{emph \<open>core\<close>} of the document itself which is an Isabelle theory
|
\<^item> the @{emph \<open>core\<close>} of the document itself which is an Isabelle theory
|
||||||
importing the ontology definition. \isadof provides an own family of text-element
|
importing the ontology definition. \isadof provides an own family of text-element
|
||||||
commands such as \inlineisar+title*+, \inlineisar+section*+, \inlineisar+text*+, etc.,
|
commands such as \inlineisar+title*+, \inlineisar+section*+, \inlineisar+text*+, etc.,
|
||||||
which can be annotated with meta-information defined in the underlying ontology definition.
|
which can be annotated with meta-information defined in the underlying ontology definition.
|
||||||
\item the @{emph \<open>layout definition\<close>} for the given ontology exploiting this meta-information.
|
\<^item> the @{emph \<open>layout definition\<close>} for the given ontology exploiting this meta-information.
|
||||||
\end{itemize}
|
\<close>
|
||||||
\isadof is a novel Isabelle system component providing specific support for all these three parts.
|
text\<open>\isadof is a novel Isabelle system component providing specific support for all these three parts.
|
||||||
Note that the document core @{emph \<open>may\<close>}, but @{emph \<open>must\<close>} not
|
Note that the document core @{emph \<open>may\<close>}, but @{emph \<open>must\<close>} not
|
||||||
use Isabelle definitions or proofs for checking the formal content---the
|
use Isabelle definitions or proofs for checking the formal content---the
|
||||||
present paper is actually an example of a document not containing any proof.
|
present paper is actually an example of a document not containing any proof.
|
||||||
|
@ -194,14 +192,14 @@ by terms HOL-terms, \ie, the actual parsers and type-checkers of the Isabelle sy
|
||||||
This has the particular advantage that \isadof commands can be arbitrarily mixed with
|
This has the particular advantage that \isadof commands can be arbitrarily mixed with
|
||||||
Isabelle/HOL commands providing the machinery for type declarations and term specifications such
|
Isabelle/HOL commands providing the machinery for type declarations and term specifications such
|
||||||
as enumerations. In particular, document class definitions provide:
|
as enumerations. In particular, document class definitions provide:
|
||||||
\begin{itemize}
|
\<^item> a HOL-type for each document class as well as inheritance,
|
||||||
\item a HOL-type for each document class as well as inheritance,
|
\<^item> support for attributes with HOL-types and optional default values,
|
||||||
\item support for attributes with HOL-types and optional default values,
|
\<^item> support for overriding of attribute defaults but not overloading, and
|
||||||
\item support for overriding of attribute defaults but not overloading, and
|
\<^item> text-elements annotated with document classes; they are mutable
|
||||||
\item text-elements annotated with document classes; they are mutable
|
|
||||||
instances of document classes.
|
instances of document classes.
|
||||||
\end{itemize}
|
\<close>
|
||||||
Attributes referring to other ontological concepts are called \emph{links}.
|
text\<open>
|
||||||
|
Attributes referring to other ontological concepts are called \emph{links}.
|
||||||
The HOL-types inside the document specification language support built-in types for Isabelle/HOL \inlineisar+typ+'s,
|
The HOL-types inside the document specification language support built-in types for Isabelle/HOL \inlineisar+typ+'s,
|
||||||
\inlineisar+term+'s, and \inlineisar+thm+'s reflecting internal Isabelle's internal types
|
\inlineisar+term+'s, and \inlineisar+thm+'s reflecting internal Isabelle's internal types
|
||||||
for these entities; when denoted in HOL-terms to instantiate an attribute, for example, there is a
|
for these entities; when denoted in HOL-terms to instantiate an attribute, for example, there is a
|
||||||
|
@ -388,16 +386,16 @@ during the exam and the preparation requires a very rigorous process, as the fre
|
||||||
\emph{baccaleaureat} and exams at The University of Sheffield.
|
\emph{baccaleaureat} and exams at The University of Sheffield.
|
||||||
|
|
||||||
We assume that the content has four different types of addressees, which have a different
|
We assume that the content has four different types of addressees, which have a different
|
||||||
\emph{view} on the integrated document
|
\emph{view} on the integrated document:
|
||||||
\begin{itemize}
|
|
||||||
\item the @{emph \<open>setter\<close>}, \ie, the author of the exam,
|
\<^item> the @{emph \<open>setter\<close>}, \ie, the author of the exam,
|
||||||
\item the @{emph \<open>checker\<close>}, \ie, an internal person that checks the exam for feasibility
|
\<^item> the @{emph \<open>checker\<close>}, \ie, an internal person that checks the exam for feasibility
|
||||||
and non-ambiguity,
|
and non-ambiguity,
|
||||||
\item the @{emph \<open>external examiner\<close>}, \ie, an external person that checks the exam for
|
\<^item> the @{emph \<open>external examiner\<close>}, \ie, an external person that checks the exam for
|
||||||
feasibility and non-ambiguity, and
|
feasibility and non-ambiguity, and
|
||||||
\item the @{emph \<open>student\<close>}, \ie, the addressee of the exam.
|
\<^item> the @{emph \<open>student\<close>}, \ie, the addressee of the exam.
|
||||||
\end{itemize}
|
\<close>
|
||||||
The latter quality assurance mechanism is used in many universities,
|
text\<open> The latter quality assurance mechanism is used in many universities,
|
||||||
where for organizational reasons the execution of an exam takes place in facilities
|
where for organizational reasons the execution of an exam takes place in facilities
|
||||||
where the author of the exam is not expected to be physically present.
|
where the author of the exam is not expected to be physically present.
|
||||||
Furthermore, we assume a simple grade system (thus, some calculation is required).
|
Furthermore, we assume a simple grade system (thus, some calculation is required).
|
||||||
|
@ -468,9 +466,9 @@ doc_class Exercise = Exam_item +
|
||||||
In many institutions, it makes sense to have a rigorous process of validation
|
In many institutions, it makes sense to have a rigorous process of validation
|
||||||
for exam subjects: is the initial question correct? Is a proof in the sense of the
|
for exam subjects: is the initial question correct? Is a proof in the sense of the
|
||||||
question possible? We model the possibility that the @{term examiner} validates a
|
question possible? We model the possibility that the @{term examiner} validates a
|
||||||
question by a sample proof validated by Isabelle (see \autoref{fig:onto-exam-monitor}). In our scenario this sample proofs
|
question by a sample proof validated by Isabelle (see \autoref{fig:onto-exam-monitor}).
|
||||||
are completely @{emph \<open>intern\<close>}, \ie, not exposed to the students but just additional
|
In our scenario this sample proofs are completely @{emph \<open>intern\<close>}, \ie, not exposed to the
|
||||||
material for the internal review process of the exam.
|
students but just additional material for the internal review process of the exam.
|
||||||
\begin{figure}
|
\begin{figure}
|
||||||
\begin{isar}
|
\begin{isar}
|
||||||
doc_class Validation =
|
doc_class Validation =
|
||||||
|
@ -637,10 +635,10 @@ in which instances of monitored classes may occur. \<close>
|
||||||
|
|
||||||
text\<open>
|
text\<open>
|
||||||
The control of monitors is done by the commands:
|
The control of monitors is done by the commands:
|
||||||
\begin{itemize}
|
\<^item> \inlineisar+open_monitor* + <doc-class>
|
||||||
\item \inlineisar+open_monitor* + <doc-class>
|
\<^item> \inlineisar+close_monitor* + <doc-class>
|
||||||
\item \inlineisar+close_monitor* + <doc-class>
|
\<close>
|
||||||
\end{itemize}
|
text\<open>
|
||||||
where the automaton of the monitor class is expected
|
where the automaton of the monitor class is expected
|
||||||
to be in a final state. In the final state, user-defined SML
|
to be in a final state. In the final state, user-defined SML
|
||||||
Monitors can be nested, so it is possible to "overlay" one or more monitoring
|
Monitors can be nested, so it is possible to "overlay" one or more monitoring
|
||||||
|
@ -653,15 +651,14 @@ may occur freely. \<close>
|
||||||
section*[conclusion::conclusion]\<open> Conclusion and Related Work\<close>
|
section*[conclusion::conclusion]\<open> Conclusion and Related Work\<close>
|
||||||
text\<open> We have demonstrated the use of \isadof, a novel ontology modeling and enforcement
|
text\<open> We have demonstrated the use of \isadof, a novel ontology modeling and enforcement
|
||||||
IDE deeply integrated into the Isabelle/Isar Framework. The two most distinguishing features are
|
IDE deeply integrated into the Isabelle/Isar Framework. The two most distinguishing features are
|
||||||
\begin{itemize}
|
\<^item> \isadof and its ontology language are a strongly typed language that allows
|
||||||
\item \isadof and its ontology language are a strongly typed language that allows
|
|
||||||
for referring (albeit not reasoning) to entities of Isabelle/HOL, most notably types, terms,
|
for referring (albeit not reasoning) to entities of Isabelle/HOL, most notably types, terms,
|
||||||
and (formally proven) theorems, and
|
and (formally proven) theorems, and
|
||||||
\item \isadof is supported by the Isabelle/PIDE framework; thus, the advantages of an IDE for
|
\<^item> \isadof is supported by the Isabelle/PIDE framework; thus, the advantages of an IDE for
|
||||||
text-exploration (which is the type of this link? To which text element does this link refer?
|
text-exploration (which is the type of this link? To which text element does this link refer?
|
||||||
Which are the syntactic alternatives here?) were available during editing
|
Which are the syntactic alternatives here?) were available during editing
|
||||||
instead of a post-hoc validation process.
|
instead of a post-hoc validation process.
|
||||||
\end{itemize} \<close>
|
\<close>
|
||||||
|
|
||||||
text\<open> Of course, a conventional batch-process also exists which can be used
|
text\<open> Of course, a conventional batch-process also exists which can be used
|
||||||
for the validation of large document bases in a conventional continuous build process.
|
for the validation of large document bases in a conventional continuous build process.
|
||||||
|
@ -710,8 +707,7 @@ text\<open> The implementation of the framework, the discussed ontology definiti
|
||||||
\url{https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF/}.\<close>
|
\url{https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF/}.\<close>
|
||||||
paragraph\<open> Acknowledgement. \<close>
|
paragraph\<open> Acknowledgement. \<close>
|
||||||
text\<open> This work was partly supported by the framework of IRT SystemX, Paris-Saclay, France,
|
text\<open> This work was partly supported by the framework of IRT SystemX, Paris-Saclay, France,
|
||||||
and therefore granted with public funds within the scope of the
|
and therefore granted with public funds within the scope of the Program ``Investissements d’Avenir''.\<close>
|
||||||
Program ``Investissements d’Avenir''.\<close>
|
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
end
|
end
|
||||||
|
|
Reference in New Issue