forked from Isabelle_DOF/Isabelle_DOF
76612ae6f3
- 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
|
||
|---|---|---|
| .. | ||
| figures | ||
| AssnsLemmaThmEtc.thy | ||
| Attributes.thy | ||
| Concept_Example.thy | ||
| Concept_Example_Low_Level_Invariant.thy | ||
| Evaluation.thy | ||
| High_Level_Syntax_Invariants.thy | ||
| Ontology_Matching_Example.thy | ||
| OutOfOrderPresntn.thy | ||
| ROOT | ||
| TermAntiquotations.thy | ||