forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
This commit is contained in:
commit
54c9bc2d74
|
|
@ -119,10 +119,17 @@ text\<open>
|
|||
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}.
|
||||
|
||||
\end{quote}
|
||||
A \<^BibTeX>-entry is available at:
|
||||
\<^url>\<open>https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019\<close>.
|
||||
\<^item> for an application of \<^isadof> in the context of certifications:
|
||||
\begin{quote}\small
|
||||
A.~D. Brucker and B.~Wolff.
|
||||
Using Ontologies in Formal Developments Targeting Certification.
|
||||
In W. Ahrendt and S. Tarifa, editors. \<^emph>\<open>Integrated Formal Methods (IFM)\<close>, number 11918.
|
||||
Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
|
||||
\href{https://doi.org/10.1007/978-3-030-34968-4\_4}.
|
||||
\end{quote}
|
||||
\<close>
|
||||
subsubsection\<open>Availability\<close>
|
||||
text\<open>
|
||||
|
|
|
|||
|
|
@ -43,11 +43,11 @@ The current system framework offers moreover the following features:
|
|||
\<^item> an extensible front-end language Isabelle/Isar, and,
|
||||
\<^item> last but not least, an LCF style, generic theorem prover kernel as
|
||||
the most prominent and deeply integrated system component.
|
||||
|
||||
|
||||
\<close>
|
||||
text\<open>
|
||||
The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers,
|
||||
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\<^boxed_sml>\<open>Context\<close>.
|
||||
foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \<^boxed_sml>\<open>Context\<close>.
|
||||
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>.
|
||||
On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific
|
||||
|
|
@ -70,13 +70,20 @@ declare_reference*["fig:dependency"::text_section]
|
|||
|
||||
|
||||
text\<open>
|
||||
We assume a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document
|
||||
consist of a hierarchy \<^emph>\<open>sub-documents\<close> (files) that can depend acyclically on each other.
|
||||
The Isabelle Framework is based on a \<^emph>\<open>document-centric view\<close> bindex>\<open>document-centric view\<close> of
|
||||
a document, treating the input in its integrality as set of (user-programmable) \<^emph>\<open>document element\<close>
|
||||
that may mutually depend and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured in a set of
|
||||
\<^verbatim>\<open>ROOT\<close>- and \<^verbatim>\<open>ROOTS\<close>-files.
|
||||
|
||||
Isabelle assumes a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document
|
||||
consist of a hierarchy \<^emph>\<open>sub-documents\<close> (files); dependencies are restricted to be
|
||||
acyclic at this level.
|
||||
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
|
||||
main sub-document type, for historical reasons, \<^emph>\<open>theory\<close>-files. A theory file\<^bindex>\<open>theory!file\<close>
|
||||
consists of a \<^emph>\<open>header\<close>\<^bindex>\<open>header\<close>, a \<^emph>\<open>context definition\<close>\<^index>\<open>context\<close>, and a body
|
||||
consisting of a sequence of \<^emph>\<open>command\<close>s (see @{figure (unchecked) "fig:dependency"}). Even
|
||||
consisting of a sequence of document elements called
|
||||
\<^emph>\<open>command\<close>s (see @{figure (unchecked) "fig:dependency"}). Even
|
||||
the header consists of a sequence of commands used for introductory text elements not depending on
|
||||
any context. The context-definition contains an \<^boxed_theory_text>\<open>import\<close> and a
|
||||
\<^boxed_theory_text>\<open>keyword\<close> section, for example:
|
||||
|
|
@ -96,30 +103,43 @@ text\<open> A text-element \<^index>\<open>text-element\<close> may look like th
|
|||
@{boxed_theory_text [display]\<open>
|
||||
text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl},
|
||||
we obtain in \<Gamma> for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>}
|
||||
so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in \<open>\<open> ... \<close>\<close> paranthesis) which
|
||||
... so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in \<open>\<open> ... \<close>\<close> paranthesis) which
|
||||
contains characters and and a special notation for semantic macros \<^bindex>\<open>semantic macros\<close>
|
||||
(here \<^theory_text>\<open>@{term "fac 5"}).\<close>
|
||||
\<close>
|
||||
|
||||
text\<open>
|
||||
We distinguish fundamentally two different syntactic levels:
|
||||
\<^item> the \<^emph>\<open>outer-syntax\<close>\<^bindex>\<open>syntax!outer\<close>\<^index>\<open>outer syntax|see {syntax, outer}\<close> (\<^ie>, the
|
||||
syntax for commands) is processed by a lexer-library and parser combinators built on top, and
|
||||
\<^item> the \<^emph>\<open>inner-syntax\<close>\<^bindex>\<open>syntax!inner\<close>\<^index>\<open>inner syntax|see {syntax, inner}\<close> (\<^ie>, the
|
||||
syntax for \<open>\<lambda>\<close>-terms in HOL) with its own parametric polymorphism type checking.
|
||||
text\<open>While we concentrate in this manual on \<^theory_text>\<open>text\<close>-document elements --- this is the main
|
||||
use of \<^dof> in its current stage --- it is important to note that there are actually three
|
||||
families of ``ontology aware'' document elements with analogous
|
||||
syntax to standard ones. The difference is a bracket with meta-data of the form:
|
||||
@{theory_text [display,indent=5, margin=70]
|
||||
\<open>
|
||||
text*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some semi-formal text \<close>
|
||||
ML*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some SML code \<close>
|
||||
value*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some annotated \<lambda>-term \<close>
|
||||
\<close>}
|
||||
|
||||
Depending on the family, we will speak about \<^emph>\<open>(formal) text-contexts\<close>,\<^index>\<open>formal text-contexts\<close>
|
||||
\<^emph>\<open>(ML) code-contexts\<close>\<^index>\<open>code-contexts\<close> and \<^emph>\<open>term-contexts\<close>\<^index>\<open>term-contexts\<close> if we refer
|
||||
to sub-elements inside the \<open>\<open>...\<close>\<close> cartouches of these command families. Note that the Isabelle
|
||||
framework allows for nesting cartouches that permits to support to switch into a different
|
||||
context. In general, this has also the effect that the evaluation of antiquotations changes.
|
||||
\<^footnote>\<open>In the literature, this concept has been referred to \<open>Cascade-Syntax\<close> and was used in the
|
||||
Centaur-system and is existing in some limited form in some Emacs-implementations these days. \<close>
|
||||
\<close>
|
||||
text\<open>
|
||||
On the semantic level, we assume a validation process for an integrated document, where the
|
||||
semantics of a command is a transformation \<open>\<theta> \<rightarrow> \<theta>\<close> for some system state \<open>\<theta>\<close>.
|
||||
This document model can be instantiated with outer-syntax commands for common
|
||||
text elements, \<^eg>, \<^theory_text>\<open>section\<open>...\<close>\<close> or \<^theory_text>\<open>text\<open>...\<close>\<close>.
|
||||
Thus, users can add informal text to a sub-document using a text command:
|
||||
This document model can be instantiated depending on the text-code-, or term-contexts.
|
||||
For common text elements, \<^eg>, \<^theory_text>\<open>section\<open>...\<close>\<close> or \<^theory_text>\<open>text\<open>...\<close>\<close>,
|
||||
users can add informal text to a sub-document using a text command:
|
||||
@{boxed_theory_text [display] \<open>text\<open>This is a description.\<close>\<close> }
|
||||
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>,
|
||||
machine-checked content via \<^emph>\<open>semantic macros\<close>, called antiquotations\<^bindex>\<open>antiquotation\<close>:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl}, we obtain in \<Gamma>
|
||||
for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>
|
||||
\<open>text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm "refl"}, we obtain in \<Gamma>
|
||||
for @{term \<open>fac 5\<close>} the result @{value \<open>fac 5\<close>}.\<close>\<close>
|
||||
}
|
||||
which is represented in the final document (\<^eg>, a PDF) by:
|
||||
@{boxed_pdf [display]
|
||||
|
|
@ -137,10 +157,12 @@ for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.\<cl
|
|||
typeset. They represent the device for linking the formal with the informal.
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
figure*["fig:dependency"::figure,relative_width="70",src="''figures/document-hierarchy''"]
|
||||
\<open>A Theory-Graph in the Document Model. \<close>
|
||||
|
||||
section*[bgrnd21::introduction]\<open>Implementability of the Required Document Model\<close>
|
||||
section*[bgrnd21::introduction]\<open>Implementability of the Document Model in other ITP's\<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 \<open>term\<close>, and abstract \<open>thm\<close>-type for theorems
|
||||
|
|
|
|||
|
|
@ -100,7 +100,8 @@ text\<open>
|
|||
to instances, and class-invariants. Some concepts like advanced type-checking, referencing to
|
||||
formal entities of Isabelle, and monitors are due to its specific application in the
|
||||
Isabelle context. Conceptually, ontologies specified in ODL consist of:
|
||||
\<^item> \<^emph>\<open>document classes\<close> (\<^boxed_theory_text>\<open>doc_class\<close>) that describe concepts;
|
||||
\<^item> \<^emph>\<open>document classes\<close> (\<^boxed_theory_text>\<open>doc_class\<close>) \<^index>\<open>doc\_class\<close> that describe concepts;
|
||||
the keyword (\<^boxed_theory_text>\<open>onto_class\<close>) \<^index>\<open>onto\_class\<close> is accpted equally;
|
||||
\<^item> an optional document base class expressing single inheritance
|
||||
class extensions;
|
||||
\<^item> \<^emph>\<open>attributes\<close> specific to document classes, where
|
||||
|
|
@ -233,7 +234,7 @@ A document class\<^bindex>\<open>document class\<close> can be defined using the
|
|||
\<^item> \<open>doc_class_specification\<close>:\<^index>\<open>doc\_class\_specification@\<open>doc_class_specification\<close>\<close>
|
||||
We call document classes with an \<open>accepts_clause\<close>
|
||||
\<^emph>\<open>monitor classes\<close> or \<^emph>\<open>monitors\<close> for short.
|
||||
\<^rail>\<open> @@{command "doc_class"} class_id '=' (class_id '+')? (attribute_decl+) \<newline>
|
||||
\<^rail>\<open> (@@{command "doc_class"}| @@{command "onto_class"}) class_id '=' (class_id '+')? (attribute_decl+) \<newline>
|
||||
(invariant_decl *)
|
||||
(accepts_clause rejects_clause?)?\<close>
|
||||
\<^item> \<open>attribute_decl\<close>:\<^index>\<open>attribute\_decl@\<open>attribute_decl\<close>\<close>
|
||||
|
|
@ -319,12 +320,17 @@ supported on the Isabelle/Isar level. Note that some more advanced functionality
|
|||
is currently only available in the SML API's of the kernel.
|
||||
|
||||
\<^item> \<open>meta_args\<close> :
|
||||
\<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' term) *) \<close>
|
||||
\<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \<close>
|
||||
\<^item> \<open>upd_meta_args\<close> :
|
||||
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') term) * ))\<close>
|
||||
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close>
|
||||
\<^item> \<open>annotated_text_element\<close> :
|
||||
\<^rail>\<open>
|
||||
( @@{command "text*"}'[' meta_args ']' '\<open>' text '\<close>' |
|
||||
\<^rail>\<open>
|
||||
( ( @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
|
||||
| @@{command "ML*"} '[' meta_args ']' '\<open>' SML_code '\<close>'
|
||||
| @@{command "term*"} '[' meta_args ']' '\<open>' HOL_term '\<close>'
|
||||
| @@{command "value*"}'[' meta_args ']' '\<open>' HOL_term '\<close>'
|
||||
)
|
||||
|
|
||||
( @@{command "open_monitor*"}
|
||||
| @@{command "close_monitor*"}
|
||||
| @@{command "declare_reference*"}
|
||||
|
|
@ -350,10 +356,14 @@ text\<open>Recall that with the exception of \<^theory_text>\<open>text* \<dots>
|
|||
layout (such as \<^LaTeX>); these commands have to be wrapped into
|
||||
\<^verbatim>\<open>(*<*) ... (*>*)\<close> brackets if this is undesired. \<close>
|
||||
|
||||
subsection\<open>Ontologic Text-Elements and their Management\<close>
|
||||
text\<open> \<^theory_text>\<open>text*[oid::cid, ...] \<open> \<dots> text \<dots> \<close> \<close> is the core-command of \<^isadof>: it permits to create
|
||||
subsection\<open>Ontologic Text-Contexts and their Management\<close>
|
||||
text\<open> With respect to the family of text elements,
|
||||
\<^theory_text>\<open>text*[oid::cid, ...] \<open> \<dots> text \<dots> \<close> \<close> is the core-command of \<^isadof>: it permits to create
|
||||
an object of meta-data belonging to the class \<^theory_text>\<open>cid\<close>. This is viewed as the \<^emph>\<open>definition\<close> of
|
||||
an instance of a document class. This instance object is attached to the text-element
|
||||
an instance of a document class. The class invariants were checked for all attribute values
|
||||
at creation time if not specified otherwise. Unspecified attributed values were represented
|
||||
by fresh free variables.
|
||||
This instance object is attached to the text-element
|
||||
and makes it thus "trackable" for \<^isadof>, \<^ie>, it can be referenced via the \<^theory_text>\<open>oid\<close>, its attributes
|
||||
can be set by defaults in the class-definitions, or set at creation time, or modified at any
|
||||
point after creation via \<^theory_text>\<open>update_instance*[oid, ...]\<close>. The \<^theory_text>\<open>class_id\<close> is syntactically optional;
|
||||
|
|
@ -374,6 +384,35 @@ The precise presentation is decided in the \<^emph>\<open>layout definitions\<cl
|
|||
pragma in order to enforce a relaxed checking \<^theory_text>\<open> @{cid (unchecked) \<open>oid\<close>} \<close>.
|
||||
\<close>
|
||||
|
||||
subsection\<open>Ontologic Code-Contexts and their Management\<close>
|
||||
|
||||
text\<open>The \<^theory_text>\<open>ML*[oid::cid, ...] \<open> \<dots> SML-code \<dots> \<close>\<close>-document elements proceed similarly :
|
||||
a referentiable meta-object of class \<^theory_text>\<open>cid\<close> is created, initialized with the optional
|
||||
attributes and bound to \<^theory_text>\<open>oid\<close>. The SML-code is type-checked and executed
|
||||
in the context of the SML toplevel of the Isabelle system as in the corresponding
|
||||
\<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command.
|
||||
\<close>
|
||||
|
||||
subsection\<open>Ontologic Term-Contexts and their Management\<close>
|
||||
text\<open>The major commands providing term-contexts are
|
||||
\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
|
||||
\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>Note that the meta-argument list is optional.\<close>.
|
||||
Wrt. to creation, track-ability and checking they are analogous to the ontological text and
|
||||
code-commands. However the argument terms may contain term-antiquotations stemming from an
|
||||
ontology definition. Both term-contexts ware type-checked and \<^emph>\<open>validated\<close> against
|
||||
the global context (so: in the term \<open>@{A \<open>oid\<close>}\<close>, \<open>oid\<close> is indeed a string which refers
|
||||
to a meta-object belonging to the document class \<open>A\<close>, for example).
|
||||
The term-context in the \<open>value*\<close>-command is additionally expanded (\<^eg> replaced) by a term
|
||||
denoting the meta-object. This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
|
||||
executable HOL-functions to interact with meta-objects.
|
||||
|
||||
Note unspecified attribute values were represented by free fresh variables which constrains \<^dof>
|
||||
to choose either to the normalisation-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or to a proof attempt via
|
||||
the \<^theory_text>\<open>auto\<close>. A failure of these strategies will be reported and regarded as non-validation
|
||||
of this meta-object. The latter leads to a failure of the entire command.
|
||||
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
declare_reference*["sec:advanced"::technical]
|
||||
(*>*)
|
||||
|
|
@ -901,7 +940,6 @@ schemata:
|
|||
|
||||
|
||||
section*["sec:advanced"::technical]\<open>Advanced ODL Concepts\<close>
|
||||
text\<open>This section will be based on the following example.\<close>
|
||||
|
||||
subsection*["sec:example"::technical]\<open>Example\<close>
|
||||
text\<open>Assume the following local ontology:
|
||||
|
|
@ -1117,16 +1155,19 @@ text\<open>
|
|||
|
||||
\begin{sml}
|
||||
fun check_result_inv oid {is_monitor:bool} ctxt =
|
||||
let val kind = AttributeAccess.compute_attr_access ctxt "evidence" oid <@>{here} <@>{here}
|
||||
val prop = AttributeAccess.compute_attr_access ctxt "property" oid <@>{here} <@>{here}
|
||||
val tS = HOLogic.dest_list prop
|
||||
let
|
||||
val kind =
|
||||
AttributeAccess.compute_attr_access ctxt "evidence" oid <@>{here} <@>{here}
|
||||
val prop =
|
||||
AttributeAccess.compute_attr_access ctxt "property" oid <@>{here} <@>{here}
|
||||
val tS = HOLogic.dest_list prop
|
||||
in case kind of
|
||||
<@>{term "proof"} => if not(null tS) then true
|
||||
else error("class result invariant violation")
|
||||
| _ => false
|
||||
end
|
||||
val _ = Theory.setup (DOF_core.update_class_invariant
|
||||
"Low_Level_Syntax_Invariants.result" check_result_inv)
|
||||
"Low_Level_Syntax_Invariants.result" check_result_inv)
|
||||
\end{sml}
|
||||
|
||||
The \<^ML>\<open>Theory.setup\<close>-command (last line) registers the \<^boxed_theory_text>\<open>check_result_inv\<close> function
|
||||
|
|
@ -1136,7 +1177,34 @@ fun check_result_inv oid {is_monitor:bool} ctxt =
|
|||
\<^boxed_theory_text>\<open>oid\<close> is bound to a variable here and can therefore not be statically expanded.
|
||||
\<close>
|
||||
|
||||
subsection*["sec:queries_on_instances"::technical]\<open>Queries On Instances\<close>
|
||||
|
||||
text\<open>
|
||||
Any class definition generates term antiquotations checking a class instance or
|
||||
the set of instances in a particular logical context; these references were
|
||||
elaborated to objects they refer to.
|
||||
This paves the way for a new mechanism to query the ``current'' instances presented as a
|
||||
list of HOL \<^type>\<open>list\<close>.
|
||||
Arbitrarily complex queries can therefore be defined inside the logical language.
|
||||
Thus, to get the list of the properties of the instances of the class \<open>result\<close>,
|
||||
or to get the list of the authors of the instances of the \<open>introduction\<close> class,
|
||||
it suffices to treat this meta-data as usual:
|
||||
@{theory_text [display,indent=5, margin=70] \<open>
|
||||
value*\<open>map (result.property) @{result-instances}\<close>
|
||||
value*\<open>map (text_section.authored_by) @{introduction-instances}\<close>
|
||||
\<close>}
|
||||
In order to get the list of the instances of the class \<open>myresult\<close>
|
||||
whose \<open>evidence\<close> is a \<open>proof\<close>, one can use the command:
|
||||
@{theory_text [display,indent=5, margin=70] \<open>
|
||||
value*\<open>filter (\<lambda>\<sigma>. result.evidence \<sigma> = proof) @{result-instances}\<close>
|
||||
\<close>}
|
||||
Analogously, the list of the instances of the class \<open>introduction\<close> whose \<open>level\<close> > 1,
|
||||
can be filtered by:
|
||||
@{theory_text [display,indent=5, margin=70] \<open>
|
||||
value*\<open>filter (\<lambda>\<sigma>. the (text_section.level \<sigma>) > 1)
|
||||
@{introduction-instances}\<close>
|
||||
\<close>}
|
||||
\<close>
|
||||
|
||||
section*[infrastructure::technical]\<open>Technical Infrastructure\<close>
|
||||
|
||||
|
|
|
|||
|
|
@ -41,8 +41,8 @@
|
|||
\pagestyle{headings}
|
||||
|
||||
\uppertitleback{
|
||||
Copyright \copyright{} 2019--2021 University of Exeter, UK\\
|
||||
\phantom{Copyright \copyright{}} 2018--2021 Universit\'e Paris-Saclay, France\\
|
||||
Copyright \copyright{} 2019--2022 University of Exeter, UK\\
|
||||
\phantom{Copyright \copyright{}} 2018--2022 Universit\'e Paris-Saclay, France\\
|
||||
\phantom{Copyright \copyright{}} 2018--2019 The University of Sheffield, UK\\
|
||||
|
||||
\smallskip
|
||||
|
|
@ -77,11 +77,13 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
|||
|
||||
\lowertitleback{%
|
||||
This manual describes \isadof version \isadofversion. The latest official
|
||||
release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}). The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest release. The latest development version as well as official releases are available at
|
||||
release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}).
|
||||
The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest
|
||||
release. The latest development version as well as official releases are available at
|
||||
\url{\dofurl}.
|
||||
|
||||
\paragraph*{Contributors.} We would like to thank the following contributors to \isadof
|
||||
(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, Chantal Keller, and Nicolas M{\'e}ric.
|
||||
(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, and Nicolas M{\'e}ric.
|
||||
|
||||
\paragraph*{Acknowledgments.} This work has been partially supported by IRT SystemX, Paris-Saclay,
|
||||
France, and therefore granted with public funds of the Program ``Investissements d'Avenir.''
|
||||
|
|
@ -107,7 +109,7 @@ France, and therefore granted with public funds of the Program ``Investissements
|
|||
\hfill
|
||||
\begin{minipage}{8cm}
|
||||
\raggedleft\normalsize
|
||||
Laboratoire en Recherche en Informatique (LRI)\\
|
||||
Laboratoire des Methodes Formelles (LMF)\\
|
||||
Universit\'e Paris-Saclay\\
|
||||
91405 Orsay Cedex\\
|
||||
France
|
||||
|
|
|
|||
|
|
@ -1039,7 +1039,7 @@ fun ML_isa_check_docitem thy (term, req_ty, pos) _ =
|
|||
else err ("faulty reference to docitem: "^name) pos
|
||||
in ML_isa_check_generic check thy (term, pos) end
|
||||
|
||||
fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option pos =
|
||||
fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ =
|
||||
case term_option of
|
||||
NONE => error("Wrong term option. You must use a defined term")
|
||||
| SOME term => Const (isa_name, ty) $ term
|
||||
|
|
@ -1048,17 +1048,10 @@ fun elaborate_instance thy _ _ term_option pos =
|
|||
case term_option of
|
||||
NONE => error ("Malformed term annotation")
|
||||
| SOME term => let val instance_name = HOLogic.dest_string term
|
||||
(*val _ = writeln("In elaborate_instance term: " ^ @{make_string} term)
|
||||
val _ = writeln("In elaborate_instance term: " ^ Syntax.string_of_term_global thy term)
|
||||
val _ = writeln("In elaborate_instance instance_name: " ^ instance_name)*)
|
||||
in case DOF_core.get_value_global instance_name thy of
|
||||
NONE => error ("No class instance: " ^ instance_name)
|
||||
| SOME(value) =>
|
||||
let
|
||||
(*val _ = writeln("In elaborate_instance value: " ^ @{make_string} value)
|
||||
val _ = writeln("In elaborate_instance value: " ^ Syntax.string_of_term_global thy value)*)
|
||||
(*in value end*)
|
||||
in DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy end
|
||||
DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy
|
||||
end
|
||||
(*DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy*)
|
||||
|
||||
|
|
@ -1091,7 +1084,7 @@ fun declare_ISA_class_accessor_and_check_instance doc_class_name =
|
|||
end)
|
||||
end
|
||||
|
||||
fun elaborate_instances_list thy isa_name _ _ pos =
|
||||
fun elaborate_instances_list thy isa_name _ _ _ =
|
||||
let
|
||||
val base_name = Long_Name.base_name isa_name
|
||||
fun get_isa_name_without_intances_suffix s =
|
||||
|
|
@ -1746,7 +1739,8 @@ signature VALUE_COMMAND =
|
|||
sig
|
||||
val value: Proof.context -> term -> term
|
||||
val value_select: string -> Proof.context -> term -> term
|
||||
val value_cmd: xstring -> string list -> string -> Toplevel.state -> Toplevel.transition -> unit
|
||||
val value_cmd: (ODL_Command_Parser.meta_args_t option) -> xstring -> string list -> string
|
||||
-> Toplevel.state -> Toplevel.transition -> unit
|
||||
val add_evaluator: binding * (Proof.context -> term -> term)
|
||||
-> theory -> string * theory
|
||||
end;
|
||||
|
|
@ -1788,9 +1782,15 @@ fun value_select name ctxt =
|
|||
fun value ctxt term = value_select "" ctxt
|
||||
(DOF_core.transduce_term_global {mk_elaboration=true} (term , \<^here>)
|
||||
(Proof_Context.theory_of ctxt))
|
||||
fun meta_args_exec NONE thy = thy
|
||||
|meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) thy =
|
||||
thy |> (ODL_Command_Parser.create_and_check_docitem
|
||||
{is_monitor = false} {is_inline = false}
|
||||
oid pos (I cid_pos) (I doc_attrs))
|
||||
|
||||
fun value_cmd raw_name modes raw_t state trans =
|
||||
fun value_cmd meta_args_opt raw_name modes raw_t state trans =
|
||||
let
|
||||
val _ = meta_args_exec meta_args_opt
|
||||
val ctxt = Toplevel.context_of state;
|
||||
val name = intern_evaluator ctxt raw_name;
|
||||
val t = Syntax.read_term ctxt raw_t;
|
||||
|
|
@ -1817,22 +1817,19 @@ val opt_evaluator =
|
|||
|
||||
val opt_attributes = Scan.option ODL_Command_Parser.attributes
|
||||
|
||||
fun meta_args_exec NONE thy = thy
|
||||
|meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) thy =
|
||||
thy |> (ODL_Command_Parser.create_and_check_docitem
|
||||
{is_monitor = false} {is_inline = false}
|
||||
oid pos (I cid_pos) (I doc_attrs))
|
||||
fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans =
|
||||
Toplevel.keep (fn state => value_cmd meta_args_opt name modes t state trans) trans
|
||||
|
||||
fun pass_trans_to_value_cmd ((name, modes), t) trans =
|
||||
Toplevel.keep (fn state => value_cmd name modes t state trans) trans
|
||||
\<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/isar_cmd.ML\<close>\<close>
|
||||
|
||||
(*
|
||||
term* command uses the same code as term command
|
||||
and adds the possibility to check Term Annotation Antiquotations (TA)
|
||||
with the help of DOF_core.transduce_term_global function
|
||||
*)
|
||||
fun string_of_term ctxt s trans =
|
||||
fun string_of_term meta_args_opt ctxt s trans =
|
||||
let
|
||||
val _ = meta_args_exec meta_args_opt
|
||||
val t = Syntax.read_term ctxt s;
|
||||
val T = Term.type_of t;
|
||||
val ctxt' = Proof_Context.augment t ctxt;
|
||||
|
|
@ -1851,25 +1848,21 @@ Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
|
|||
We want to have the current position to pass it to transduce_term_global in
|
||||
string_of_term, so we pass the Toplevel.transition
|
||||
*)
|
||||
fun print_term (string_list, string) trans = print_item
|
||||
(fn state => fn string => string_of_term (Toplevel.context_of state) string trans)
|
||||
(string_list, string) trans;
|
||||
fun print_term meta_args_opt (string_list, string) trans = print_item
|
||||
(fn state =>
|
||||
fn string =>
|
||||
string_of_term meta_args_opt (Toplevel.context_of state) string trans)
|
||||
(string_list, string) trans;
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>term*\<close> "read and print term"
|
||||
(opt_attributes -- (opt_modes -- Parse.term)
|
||||
>> (fn (meta_args_opt, eval_args ) =>
|
||||
Toplevel.theory (meta_args_exec meta_args_opt)
|
||||
#>
|
||||
print_term eval_args));
|
||||
>> (fn (meta_args_opt, eval_args ) => print_term meta_args_opt eval_args));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>value*\<close> "evaluate and print term"
|
||||
(opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term)
|
||||
>> (fn (meta_args_opt, eval_args ) =>
|
||||
Toplevel.theory (meta_args_exec meta_args_opt)
|
||||
#>
|
||||
pass_trans_to_value_cmd eval_args));
|
||||
>> (fn (meta_args_opt, eval_args ) => pass_trans_to_value_cmd meta_args_opt eval_args));
|
||||
|
||||
val _ = Theory.setup
|
||||
(Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>value*\<close>
|
||||
|
|
@ -1885,18 +1878,17 @@ end;
|
|||
\<close>
|
||||
|
||||
|
||||
|
||||
ML \<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/outer_syntax.ML\<close>\<close>
|
||||
\<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/outer_syntax.ML\<close>\<close>
|
||||
(*
|
||||
The ML* generates an "ontology-aware" version of the SML code-execution command.
|
||||
*)
|
||||
\<open>
|
||||
ML\<open>
|
||||
structure ML_star_Command =
|
||||
struct
|
||||
|
||||
fun meta_args_exec NONE thy = thy
|
||||
|meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) thy =
|
||||
thy |> (ODL_Command_Parser.create_and_check_docitem
|
||||
fun meta_args_exec NONE = I:generic_theory -> generic_theory
|
||||
|meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) =
|
||||
Context.map_theory (ODL_Command_Parser.create_and_check_docitem
|
||||
{is_monitor = false} {is_inline = false}
|
||||
oid pos (I cid_pos) (I doc_attrs))
|
||||
|
||||
|
|
@ -1906,12 +1898,13 @@ val _ =
|
|||
Outer_Syntax.command ("ML*", \<^here>) "ODL annotated ML text within theory or local theory"
|
||||
((attributes_opt -- Parse.ML_source)
|
||||
>> (fn (meta_args_opt, source) =>
|
||||
Toplevel.theory (meta_args_exec meta_args_opt)
|
||||
#>
|
||||
(*Toplevel.theory (meta_args_exec meta_args_opt)
|
||||
#>*)
|
||||
Toplevel.generic_theory
|
||||
(ML_Context.exec (fn () =>
|
||||
ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
|
||||
Local_Theory.propagate_ml_env)));
|
||||
(ML_Context.exec (fn () =>
|
||||
(ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))
|
||||
#> (meta_args_exec meta_args_opt)
|
||||
#>Local_Theory.propagate_ml_env)));
|
||||
|
||||
end
|
||||
\<close>
|
||||
|
|
|
|||
|
|
@ -8,6 +8,18 @@ imports
|
|||
"Isabelle_DOF-tests.TermAntiquotations"
|
||||
begin
|
||||
|
||||
section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close>
|
||||
ML*[the_function::C,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1);
|
||||
val t = @{const_name "List.Nil"}\<close>
|
||||
ML\<open>fac 5; t\<close> \<comment> \<open>this is a test that ML* is actually evaluated and the
|
||||
resulting toplevel state is preserved.\<close>
|
||||
ML*\<open>3+4\<close> \<comment> \<open>meta-args are optional\<close>
|
||||
|
||||
text\<open>... and here we reference @{B [display] \<open>the_function\<close>}.\<close>
|
||||
|
||||
section\<open>\<^theory_text>\<open>value*\<close>-Annotated evaluation-commands\<close>
|
||||
|
||||
|
||||
text\<open>The value* command uses the same code as the value command
|
||||
and adds the possibility to evaluate Term Annotation Antiquotations (TA).
|
||||
For that an elaboration of the term referenced by a TA must be done before
|
||||
|
|
@ -47,6 +59,8 @@ Here the evualuation of the TA will return the HOL.String which references the t
|
|||
\<close>
|
||||
value*\<open>@{thm \<open>HOL.refl\<close>}\<close>
|
||||
|
||||
value*[a::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> (* using the option *)
|
||||
|
||||
text\<open>An instance class is an object which allows us to define the concepts we want in an ontology.
|
||||
It is a concept which will be used to implement an ontology. It has roughly the same meaning as
|
||||
an individual in an OWL ontology.
|
||||
|
|
@ -155,4 +169,5 @@ to update the instance @{docitem \<open>xcv4\<close>}:
|
|||
(* Error:
|
||||
update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{G ''xcv5''})}"]*)
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -66,6 +66,7 @@ doc_class introduction = text_section +
|
|||
authored_by :: "author set" <= "UNIV"
|
||||
uses :: "notion set"
|
||||
invariant author_finite :: "finite (authored_by \<sigma>)"
|
||||
and force_level :: "the (level \<sigma>) > 1"
|
||||
|
||||
doc_class claim = introduction +
|
||||
based_on :: "notion list"
|
||||
|
|
@ -83,32 +84,54 @@ doc_class result = technical +
|
|||
evidence :: kind
|
||||
property :: "thm list" <= "[]"
|
||||
invariant has_property :: "evidence \<sigma> = proof \<longleftrightarrow> property \<sigma> \<noteq> []"
|
||||
|
||||
doc_class example = technical +
|
||||
referring_to :: "(notion + definition) set" <= "{}"
|
||||
|
||||
doc_class conclusion = text_section +
|
||||
establish :: "(claim \<times> result) set"
|
||||
invariant total_rel :: "\<forall> x. x \<in> Domain (establish \<sigma>)
|
||||
\<longrightarrow> (\<exists> y \<in> Range (establish \<sigma>). (x, y) \<in> establish \<sigma>)"
|
||||
invariant establish_defined :: "\<forall> x. x \<in> Domain (establish \<sigma>)
|
||||
\<longrightarrow> (\<exists> y \<in> Range (establish \<sigma>). (x, y) \<in> establish \<sigma>)"
|
||||
|
||||
text\<open>Next we define some instances (docitems): \<close>
|
||||
|
||||
declare[[invariants_checking_with_tactics = true]]
|
||||
|
||||
text*[church::author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
|
||||
(*text*[introduction1::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 0"]\<open>\<close>*)
|
||||
|
||||
text*[resultProof::result, evidence = "proof", property="[@{thm \<open>HOL.refl\<close>}]"]\<open>\<close>
|
||||
text*[resultArgument::result, evidence = "argument"]\<open>\<close>
|
||||
|
||||
text\<open>The invariants \<open>author_finite\<close> and \<open>total_rel\<close> can not be checked directly
|
||||
text\<open>The invariants \<^theory_text>\<open>author_finite\<close> and \<^theory_text>\<open>establish_defined\<close> can not be checked directly
|
||||
and need a little help.
|
||||
We can set the \<open>invariants_checking_with_tactics\<close> theory attribute to help the checking.
|
||||
It will enable a basic tactic, using unfold and auto:\<close>
|
||||
|
||||
declare[[invariants_checking_with_tactics = true]]
|
||||
|
||||
text*[introductionTest::introduction, authored_by = "{@{author \<open>church\<close>}}"]\<open>\<close>
|
||||
text*[curry::author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
|
||||
text*[introduction2::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
|
||||
text*[introduction3::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
|
||||
text*[introduction4::introduction, authored_by = "{@{author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
|
||||
|
||||
text*[claimNotion::claim, authored_by = "{@{author \<open>church\<close>}}", based_on= "[\<open>Notion1\<close>, \<open>Notion2\<close>]"]\<open>\<close>
|
||||
text*[resultProof2::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"]\<open>\<close>
|
||||
|
||||
text*[conclusionProof::conclusion,
|
||||
establish = "{(@{claim \<open>claimNotion\<close>}, @{result \<open>resultProof\<close>})}"]\<open>\<close>
|
||||
text\<open>Then we can evaluate expressions with instances:\<close>
|
||||
|
||||
term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction4\<close>}\<close>
|
||||
|
||||
value*\<open>@{introduction \<open>introduction2\<close>}\<close>
|
||||
|
||||
value*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>
|
||||
|
||||
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||
value*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||
|
||||
value*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
||||
|
||||
declare[[invariants_checking_with_tactics = false]]
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue