- Warning: the current implementation does yet not support
some use-cases, like invariant on monitors,
or the initialization of docitem without a class associated.
- Add first draft of the checking of invariants.
For now, it is disabled by default because some cases
are not yet supported, like the initialization of docitem
without a class associated.
ex: text*[sdf]‹ Lorem ipsum @{thm refl}›
- To enable the checking, one can use the theory attribute
"invariants_checking" by declaring it in a theory like this:
declare [[invariants_strict_checking = true]]
- A checking using basic tactics (unfolding and auto) can be enable
with the "invariants_checking_with_tactics" theory attribute
for specific use-cases
- The specification of invariants is now automatically abstracted,
so one must define an invariant like this now:
doc_class W =
w::"int"
invariant w :: "w σ ≥ 3"
The old form:
doc_class W =
w::"int"
invariant w :: "λσ. w σ ≥ 3"
is now deprecated.
The specification of the invariant still uses the σ-notation
and is defined globally by the name component "invariantN"
- Update the invariants definition in the theories to match
the new implementation
- Update the manual to explain this new feature
- Add small examples in src/tests/High_Level_Syntax_Invariants.thy
and src/tests/Ontology_Matching_Example.thy
- Add a new Term Annotation Antiquotation (TA)
to allow requests on instances.
Example:
@{C-instances} will return all the instances of the class "C"
defined in the generated theory
- Update ISA_transformers elaborate function signature to
take into account the case where the term argument
of a TA is irrelevant, for example when a TA has no argument.
Example with the TA of the instances of a class:
@{A-instances}
Here the TA has no argument and none second level type checking is
wished, so its associated check function can be the identity function
with respect to the ISA_transformers chek function type.
- Add some request examples in Evaluation.thy
- Fix typos
This commit restructures the file hierarchy:
1) implementation is moved into src/ directory to clean up
the main directory and to make it easier for users to
find the README.md.
2) ontologies (both, the Isabelle-part and the LaTeX-part) are
now structured into directories.
Achim D. Brucker
Nicolas Méric
Burkhart Wolff
Burkhart Wolff