Add checking of invariants for class instances #8
Loading…
Reference in New Issue
No description provided.
Delete Branch "nicolas.meric/Isabelle_DOF:check-invariants-first-draft"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
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
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
- 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