pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
1,625 Commits 15 Branches 8 Tags 73 MiB
Commit Graph

1625 Commits

Author SHA1 Message Date
Nicolas Méric 8513f7d267 Update doc_class rails to match accepts clause 2023-01-17 09:01:55 +01:00
Nicolas Méric 2b1a9d009e Add support invariants on attributes of attributes 
Support invariants on attributes of classes atttributes.

Example:

doc_class inv_test1 =
  a :: int

doc_class inv_test2 =
  b :: "inv_test1"
  c:: int
  invariant inv_test2 :: "c σ = 1"
  invariant inv_test2' :: "a (b σ) = 2"

doc_class inv_test3 = inv_test1 +
  b :: "inv_test1"
  c:: int
  invariant inv_test3 :: "a σ = 1"
  invariant inv_test3' :: "a (b σ) = 2"

To support invariant on attributes in attributes
and invariant on attributes of the superclasses,
we check that the type of the attribute of the subclass is ground:›
ML‹
val Type(st, [ty]) = \<^typ>‹inv_test1›
val Type(st', [ty']) = \<^typ>‹'a inv_test1_scheme›
val t = ty = \<^typ>‹unit›
›
 2023-01-13 08:27:26 +01:00
Nicolas Méric cd758d2c44 Update accepts clause syntax 2023-01-12 12:18:58 +01:00
Nicolas Méric 8496963fec Add comment for term_ and value_ ML antiquoatations 2023-01-11 14:49:29 +01:00
Nicolas Méric 72d8000f7b Further explain evaluator option syntax for value_ text antiquotation 2023-01-09 15:34:59 +01:00
Nicolas Méric 17ec11b297 Explain evaluator option syntax for value_ text antiquotation 2023-01-09 15:13:23 +01:00
Nicolas Méric a96e17abf3 Add term_ and value_ ML antiquotations 2023-01-09 11:34:40 +01:00
Nicolas Méric 74b60e47d5 Document term _ and value_ text antiquotations 2022-12-22 16:50:53 +01:00
Nicolas Méric a42dd4ea6c Implement term _ and value_ text antiquotations 2022-12-22 10:55:03 +01:00
Nicolas Méric b162a24749 Comment out hack for Assumption in scholarly_paper 2022-12-22 09:55:46 +01:00
Nicolas Méric a9432c7b52 Add a theory attribute to disable invariants checking 2022-12-22 07:53:42 +01:00
Nicolas Méric 9f28d4949e Limit scope of free class checking in examples 2022-12-22 07:32:37 +01:00
Nicolas Méric 885c23a138 Explain lazy and eager invariants 2022-12-22 07:14:29 +01:00
Nicolas Méric a589d4cd47 Update the position of the default class 
The default class must stay abtract and as such
can not have a position.
Set its position to Position.none
 2022-12-21 18:32:07 +01:00
Burkhart Wolff e1f143d151 Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF 2022-12-21 11:35:05 +01:00
Burkhart Wolff fd60cf2312 attempt to add category 'assumption' 2022-12-21 11:34:34 +01:00
Nicolas Méric 73dfcd6c1e Implement rejects clause 
- The current implementation triggers a warning when
  rejected classes are find in the monitor,
  and an error if monitor_strict_checking is enable.
  It follows these rules:
  Inside the scope of a monitor,
  all instances of classes mentioned in its accepts_clause
  (the ∗‹accept-set›) have to appear in the order specified
  by the regular expression.
  Instances not covered by an accept-set may freely occur.
  Monitors may additionally contain a rejects_clause
  with a list of class-ids (the reject-list).
  This allows specifying ranges of
  admissible instances along the class hierarchy:
  - a superclass in the reject-list and a subclass in the
    accept-expression forbids instances superior to the subclass, and
  - a subclass S in the reject-list and a superclass T in the
    accept-list allows instances of superclasses of T to occur freely,
    instances of T to occur in the specified order and forbids
    instances of S.
- No message is triggered for the free classes,
  but two theory options, free_class_in_monitor_checking
  and free_class_in_monitor_strict_checking,
  are added and can be used if we want to trigger warnings or errors,
  in the case we do not want free classes inside a monitor.
- Fix the checking warning when defining a monitor,
  as the monitor was added to the monitor table and then
  the instance of the monitor was added to the theory.
  So a monitor had the bad behavior to check itself.
 2022-12-21 10:09:17 +01:00
Nicolas Méric c0afe1105e Enable high-level invariants checking everywhere 
By default invariants checking generates warnings.
If invariants_strict_checking theory option is enabled,
the checking generates errors.

- Update 2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
  and 2020-iFM-CSP/paper.thy to pass the checking of
  the low level invariant checking function "check"
  in scholarly_paper.thy,
  which checks that the instances in a sequence of the same class
  have a growing level.
  For a sequence:
  section*[intro::introduction]‹ Introduction ›
  text*[introtext::introduction, level = "Some 1"]‹...›

  introtext must have a level >= than intro.

- Bypass the checking of high-level invariants
  when the class default_cid = "text",
  the top (default) document class.
  We want the class default_cid to stay abstract
  and not have the capability to be defined with attribute,
  invariants, etc.
  Hence this bypass handles docitem without a class associated,
  for example when you just want a document element to be referenceable
  without using the burden of ontology classes.
  ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close>

  The functions get_doc_class_global and get_doc_class_local trigger
  an error when the class is "text" (default_cid),
  then the functions like check_invariants which use it will fail
  if the checking is enabled by default for all the theories.
 2022-12-20 16:31:09 +01:00
Burkhart Wolff e414b97afb rephrasing invariant for core scholarly_paper classes 2022-12-19 12:14:30 +01:00
Nicolas Méric 0b2d28b547 Update error message for invariant checking 2022-12-09 16:11:57 +01:00
Nicolas Méric 37d7ed7d17 Update rails for annotated text element in manual 2022-12-09 15:13:22 +01:00
Nicolas Méric 312734afbd Update Attributes examples 2022-12-09 15:12:38 +01:00
Burkhart Wolff 8cee80d78e advanced example on trace-attribute term-antiquotations 2022-12-07 16:01:38 +01:00
Makarius Wenzel ec0d525426 Tuned messages, following Isabelle/d6a2a8bc40e1 2022-12-05 15:21:26 +01:00
Makarius Wenzel 791990039b Tuned messages and options, following Isabelle/c7f3e94fce7b 2022-12-05 12:37:59 +01:00
Makarius Wenzel 78d61390fe Prefer Isar command, instead of its underlying ML implementation 2022-12-05 11:50:12 +01:00
Makarius Wenzel ffcf1f3240 Add missing file (amending 5471d873a9) 2022-12-04 19:26:28 +01:00
Makarius Wenzel 5471d873a9 Isabelle/Scala module within session context supports document_build = "dof" without component setup 2022-12-04 19:13:08 +01:00
Makarius Wenzel df37250a00 Simplified args, following README.md 2022-12-04 19:00:23 +01:00
Makarius Wenzel 185daeb577 Tuned 2022-12-04 18:25:29 +01:00
Makarius Wenzel 8037fd15f2 Tuned messages, following isabelle.Export.message 2022-12-04 18:20:54 +01:00
Makarius Wenzel afcd78610b More concise export artifact 2022-12-04 18:03:53 +01:00
Makarius Wenzel b8a9ef5118 Tuned comments 2022-12-04 16:38:56 +01:00
Makarius Wenzel a4e75c8b12 Clarified export name for the sake of low-level errors 2022-12-04 16:35:55 +01:00
Makarius Wenzel d20e9ccd22 Proper session qualifier for theory imports (amending 44cae2e631) 2022-12-04 00:45:07 +01:00
Makarius Wenzel f2ee5d3780 Tuned 2022-12-04 00:10:43 +01:00
Makarius Wenzel 44cae2e631 More formal management of ontologies in Isabelle/ML/Isar with output via Isabelle/Scala exports 2022-12-04 00:09:29 +01:00
Makarius Wenzel 7b2bf35353 More strict treatment of document export artifacts 2022-12-03 14:54:14 +01:00
Makarius Wenzel e8c7fa6018 Clarified signature 2022-12-03 14:44:04 +01:00
Makarius Wenzel b12e61511d Discourage etc/options 2022-12-03 13:55:56 +01:00
Makarius Wenzel 3cac42e6cb Clarified order 2022-12-03 12:39:00 +01:00
Makarius Wenzel aee8ba1df1 Prefer DOF parameters over Isabelle options 2022-12-03 12:37:58 +01:00
Makarius Wenzel d93e1383d4 Afford full-scale command-line tool 2022-12-03 12:29:24 +01:00
Makarius Wenzel 3d5d1e7476 Further attempts at woodpecker environment 2022-12-02 22:54:02 +01:00
Makarius Wenzel 4264e7cd15 Build Scala/Java components to get proper ISABELLE_CLASSPATH 2022-12-02 21:40:59 +01:00
Makarius Wenzel 96f4077c53 Tuned message 2022-12-02 21:29:45 +01:00
Makarius Wenzel d7fb39d7eb Adhoc command-line tool replaces old options 2022-12-02 21:14:55 +01:00
Makarius Wenzel b95826962f Tuned documentation 2022-12-02 20:29:40 +01:00
Makarius Wenzel 912d4bb49e Maintain document template in Isabelle/ML via Isar commands: 
result becomes export artifact, which is harvested by Isabelle/Scala build engine
 2022-12-02 20:05:15 +01:00
Makarius Wenzel a6c1a2baa4 Removed obsolete "extend" operation 2022-12-02 15:31:23 +01:00