From 97701d62d7b63cf2f73c35389bcc4a99fd9ed1e4 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 23 Jul 2019 15:26:48 +0200 Subject: [PATCH 1/2] local improvements due to remarks of Frederic. --- .../Isabelle_DOF-Manual/04_RefMan.thy | 59 ++++++++++++++++--- .../TR_MyCommentedIsabelle.thy | 7 ++- src/DOF/Isa_COL.thy | 12 +++- 3 files changed, 66 insertions(+), 12 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index c7a1767..510b27a 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -1,6 +1,7 @@ (*<*) theory "04_RefMan" - imports "03_GuidedTour" (* apparently inaccessible; for railroads "Isar_Ref.Base" *) + imports "03_GuidedTour" (* apparently inaccessible; for railroads "Isar_Ref.Base" *) + "Isabelle_DOF.Isa_COL" begin (*>*) @@ -385,13 +386,6 @@ In a high-level syntax, this type of constraints could be expressed, \eg, by: \ \ y \ Range(x@establish). (y,z) \ x@establish (* 3 *) \ x \ introduction. finite(x@authored_by) \end{isar} -%% @{cartouche [display=true] \ -%%(* 1 *) \ x \ result. x@kind = proof \ x@kind \ [] -%%(* 2 *) \ x \ conclusion. \ y \ Domain(x@establish) -%% \ \ y\ Range(x@establish). (y,z) \ x@establish -%%(* 3 *) \ x \ introduction. finite(x@authored_by) -%%\} -%% \fixme{experiment... } where \inlineisar+result+, \inlineisar+conclusion+, and %% where \result\, \conclusion\, and \inlineisar+introduction+ are the set of all possible instances of @@ -618,6 +612,55 @@ text\The syntax of toplevel \isadof commands reads as follows: \ subsection*["commonlib"::technical]\Common Ontology Library (COL)\ +text\ The COL library is used to capture a couple of text-elements +that are expected to be common to all document types, a class +that is actually not easy to define. After a lot of thought, we excluded +things like @{command "title*"} and abstract-related classes back again +to specific ontologies, for example. + +Finally, it is currently reduced to +\<^enum> the common infra-structure on text-elements (section is a text-element of a certain "level"), +\<^enum> common infrastructure to semi-formal Isabelle elements (Definitions, Assertions, Proofs), and +\<^enum> the common infra-structure for figures. + +Future extensions might include, for example, the infra-structure for tables. +\ + +text\ The super-class \<^verbatim>\text_element\ is the root of all text-elements used in \isadof. +It is defined as follows: +\begin{isar} +doc_class text_element = + level :: "int option" <= "None" + referentiable :: bool <= "False" + variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}" +\end{isar} +Of major importance is the @{term "level"} which influences, inspired by a LaTeX convention, +the following classification: +\<^enum> part = Some -1 +\<^enum> chapter = Some 0 +\<^enum> section = Some 1 +\<^enum> subsection = Some 2 +\<^enum> subsubsection = Some 3 +\<^enum> ... +for scholarly paper: invariant level > + +The attribute @{term "level"} in the subsequent enables doc-notation --- a kind of macro --- +for support of @{command "chapter*"}, @{command "section*"} etc. This class definition forms +for a number of invariants; for example, the derived ontology \scholarly_paper\ contains an +invariant that any sequence of, for example, \technical\ - elements must be introduced +by a text-element with a higher level, \ie{}, must contain a section or subsection header. +\ + +doc_class F = + property :: "term list" + r :: "thm list" + u :: "file" + s :: "typ list" + +(* +assert*[aaa::"04_RefMan.F"] "3 < (4::int)" +assert*[aaa::F] "0 < (4::int)" +*) diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index c3d95e6..429c556 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -715,8 +715,8 @@ ML\ subsection*[t235::technical]\ Theories \ -text \ This structure yields the datatype \verb*thy* which becomes the content of - \verb*Context.theory*. In a way, the LCF-Kernel registers itself into the Nano-Kernel, +text \ This structure yields the datatype \<^verbatim>\thy\ which becomes the content of + @{ML_type "Context.theory"}. In a way, the LCF-Kernel registers itself into the Nano-Kernel, which inspired me (bu) to this naming. \ ML\ @@ -2099,6 +2099,9 @@ text\ This interactive Isabelle Programming Cook-Book represents my curren \ (*<*) +paragraph\Many thanks to Frederic Tuong, who contributed some example such as the string cartouche +for Unicode Character Denotations as well as many local hints for improvements.\ + section*[bib::bibliography]\Bibliography\ close_monitor*[this] diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index 76e5469..262fd69 100644 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -16,7 +16,11 @@ section\ Library of Standard Text Ontology \ -datatype placement = pl_h | pl_t | pl_b | pl_ht | pl_hb +datatype placement = pl_h | (*here*) + pl_t | (*top*) + pl_b | (*bottom*) + pl_ht | (*here -> top*) + pl_hb (*here -> bottom*) doc_class figure = @@ -68,13 +72,17 @@ section\Some attempt to model standardized links to Standard Isabelle Form doc_class assertions = properties :: "term list" - + doc_class "thms" = properties :: "thm list" doc_class formal_item = item :: "(assertions + thms)" +doc_class definitions = + requires :: "formal_item list" + establishes :: "thms list" + doc_class formal_content = style :: "string option" accepts "\formal_item\\<^sup>+" From 6526fd2e70a9fec5c4bb479de5bf6e7f1b401e6e Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 23 Jul 2019 16:04:08 +0200 Subject: [PATCH 2/2] 04_RefMan.thy --- examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 510b27a..44ffff3 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -657,7 +657,7 @@ doc_class F = u :: "file" s :: "typ list" -(* +(* BUG BUG BUG assert*[aaa::"04_RefMan.F"] "3 < (4::int)" assert*[aaa::F] "0 < (4::int)" *)