From 4157954506fe2b70dcc9883b58d4c099d625cfd9 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Tue, 11 Apr 2023 23:15:32 +0200 Subject: [PATCH] revision of front, intro and bachgrnd (incomplete) --- .../scholarly_paper/scholarly_paper.thy | 3 +- Isabelle_DOF/thys/manual/M_00_Frontmatter.thy | 1 + .../thys/manual/M_01_Introduction.thy | 51 ++++++++++++------- Isabelle_DOF/thys/manual/M_02_Background.thy | 31 ++++++----- 4 files changed, 55 insertions(+), 31 deletions(-) diff --git a/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy b/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy index 56d9c28..8d7d689 100644 --- a/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy +++ b/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy @@ -448,7 +448,7 @@ fun doc_cmd kwd txt flag key = in val _ = doc_cmd \<^command_keyword>\Definition*\ "Freeform Definition" - Definition_default_class \<^const_name>\defn\; + Definition_default_class \<^const_name>\defn\; val _ = doc_cmd \<^command_keyword>\Lemma*\ "Freeform Lemma Description" Lemma_default_class \<^const_name>\lemm\; @@ -554,6 +554,7 @@ print_doc_classes print_doc_class_template "definition" (* just a sample *) print_doc_class_template "lemma" (* just a sample *) print_doc_class_template "theorem" (* just a sample *) +print_doc_class_template "premise" (* just a sample *) subsection\Structuring Enforcement in Engineering/Math Papers \ diff --git a/Isabelle_DOF/thys/manual/M_00_Frontmatter.thy b/Isabelle_DOF/thys/manual/M_00_Frontmatter.thy index 130df9a..9110c16 100644 --- a/Isabelle_DOF/thys/manual/M_00_Frontmatter.thy +++ b/Isabelle_DOF/thys/manual/M_00_Frontmatter.thy @@ -30,6 +30,7 @@ define_shortcut* TeXLive \ \\TeXLive\ BibTeX \ \\BibTeX{}\ LaTeX \ \\LaTeX{}\ TeX \ \\TeX{}\ + dofurl \ \\dofurl\ pdf \ \PDF\ text\Note that these setups assume that the associated \<^LaTeX> macros diff --git a/Isabelle_DOF/thys/manual/M_01_Introduction.thy b/Isabelle_DOF/thys/manual/M_01_Introduction.thy index 92c2be4..b80035f 100644 --- a/Isabelle_DOF/thys/manual/M_01_Introduction.thy +++ b/Isabelle_DOF/thys/manual/M_01_Introduction.thy @@ -38,26 +38,34 @@ and their logical contexts). Further applications are the domain-specific discourse in juridical texts or medical reports. In general, an ontology is a formal explicit description of \<^emph>\concepts\ in a domain of discourse -(called \<^emph>\classes\), properties of each concept describing \<^emph>\attributes\ of the concept, as well -as \<^emph>\links\ between them. A particular link between concepts is the \<^emph>\is-a\ relation declaring +(called \<^emph>\classes\), components (called \<^emph>\attributes\) of the concept, and properties (called +\<^emph>\invariants\) on concepts. Logically, classes are represented by a type (the class type) and +particular terms representing \<^emph>\instances\ of them. Since components are typed, it is therefore +possible to express \<^emph>\links\ like \m\-to-\n\ relations between classes. +Another form of link between concepts is the \<^emph>\is-a\ relation declaring the instances of a subclass to be instances of the super-class. -To address this challenge, we present the Document Ontology Framework (\<^dof>) and an -implementation of \<^dof> called \<^isadof>. \<^dof> is designed for building scalable and user-friendly -tools on top of interactive theorem provers. \<^isadof> is an instance of this novel framework, -implemented as extension of Isabelle/HOL, to \<^emph>\model\ typed ontologies and to \<^emph>\enforce\ them -during document evolution. Based on Isabelle's infrastructures, ontologies may refer to types, -terms, proven theorems, code, or established assertions. Based on a novel adaption of the Isabelle -IDE (called PIDE, @{cite "wenzel:asynchronous:2014"}), a document is checked to be -\<^emph>\conform\ to a particular ontology---\<^isadof> is designed to give fast user-feedback \<^emph>\during the -capture of content\. This is particularly valuable in case of document evolution, where the -\<^emph>\coherence\ between the formal and the informal parts of the content can be mechanically checked. +Engineering an ontological language for documents that contain both formal and informal elements +as occuring in formal theories is a particular challenge. To address this latter, we present +the Document Ontology Framework (\<^dof>) and an implementation of \<^dof> called \<^isadof>. + \<^dof> is designed for building scalable and user-friendly tools on top of interactive theorem +provers. \<^isadof> is an instance of this novel framework, implemented as extension of Isabelle/HOL, +to \<^emph>\model\ typed ontologies and to \<^emph>\enforce\ them during document evolution. Based on Isabelle's +infrastructures, ontologies may refer to types, terms, proven theorems, code, or established +assertions. Based on a novel adaption of the Isabelle IDE (called PIDE, @{cite "wenzel:asynchronous:2014"}), +a document is checked to be \<^emph>\conform\ to a particular ontology---\<^isadof> is designed to give fast +user-feedback \<^emph>\during the capture of content\. This is particularly valuable in case of document +evolution, where the \<^emph>\coherence\ between the formal and the informal parts of the content can +be mechanically checked. To avoid any misunderstanding: \<^isadof> is \<^emph>\not a theory in HOL\ on ontologies and operations to track and trace links in texts, it is an \<^emph>\environment to write structured text\ which \<^emph>\may contain\ Isabelle/HOL definitions and proofs like mathematical articles, tech-reports and scientific papers---as the present one, which is written in \<^isadof> itself. \<^isadof> is a plugin -into the Isabelle/Isar framework in the style of~@{cite "wenzel.ea:building:2007"}.\ +into the Isabelle/Isar framework in the style of~@{cite "wenzel.ea:building:2007"}. However, + \<^isadof> will generate from ontologies a theory infrastructure consisting of types, terms, theorems +and code that allows both interactive checking as well as formal reasoning over meta-data +related to annotated documents.\ subsubsection\How to Read This Manual\ (*<*) @@ -91,9 +99,9 @@ text\ by simp\} \<^item> a green background for examples of generated document fragments (\<^ie>, PDF output): @{boxed_pdf [display] \The axiom refl\} - \<^item> a red background for (S)ML-code: + \<^item> a red background for SML-code: @{boxed_sml [display] \fun id x = x\} - \<^item> a yellow background for \LaTeX-code: + \<^item> a yellow background for \<^LaTeX>-code: @{boxed_latex [display] \\newcommand{\refl}{$x = x$}\} \<^item> a grey background for shell scripts and interactive shell sessions: @{boxed_bash [display]\ë\prompt{}ë ls @@ -104,6 +112,15 @@ subsubsection\How to Cite \<^isadof>\ text\ If you use or extend \<^isadof> in your publications, please use \<^item> for the \<^isadof> system~@{cite "brucker.ea:isabelle-ontologies:2018"}: + \begin{quote}\small + A.~D. Brucker, I.~Ait-Sadoune, N. Méric, and B.~Wolff. Using Deep Ontologies in Formal + Software Engineering. In \<^emph>\International Conference on Rigorous State-Based Methods (ABZ 2023)\, + To appear in Lecture Notes in Computer Science. Springer-Verlag, + Heidelberg, 2023. \href{https://doi.org/???} {10.1007/????????}. + \end{quote} + A \<^BibTeX>-entry is available at: + \<^url>\https://www.lri.fr/~wolff/bibtex/wolff.html\. + \<^item> an older description of the system~@{cite "brucker.ea:isabelle-ontologies:2018"}: \begin{quote}\small A.~D. Brucker, I.~Ait-Sadoune, P.~Crisafulli, and B.~Wolff. Using the {Isabelle} ontology framework: Linking the formal with the informal. In \<^emph>\Conference on Intelligent Computer @@ -128,13 +145,13 @@ text\ Using Ontologies in Formal Developments Targeting Certification. In W. Ahrendt and S. Tarifa, editors. \<^emph>\Integrated Formal Methods (IFM)\, number 11918. Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019. - \href{https://doi.org/10.1007/978-3-030-34968-4\_4}. + \<^url>\https://doi.org/10.1007/978-3-030-34968-4_4\. \end{quote} \ subsubsection\Availability\ text\ The implementation of the framework is available at - \url{\dofurl}. The website also provides links to the latest releases. \<^isadof> is licensed + \url{\<^dofurl>}. The website also provides links to the latest releases. \<^isadof> is licensed under a 2-clause BSD license (SPDX-License-Identifier: BSD-2-Clause). \ diff --git a/Isabelle_DOF/thys/manual/M_02_Background.thy b/Isabelle_DOF/thys/manual/M_02_Background.thy index 4f09888..990ff1b 100644 --- a/Isabelle_DOF/thys/manual/M_02_Background.thy +++ b/Isabelle_DOF/thys/manual/M_02_Background.thy @@ -1,7 +1,7 @@ (************************************************************************* * Copyright (C) - * 2019-2022 The University of Exeter - * 2018-2022 The University of Paris-Saclay + * 2019-2023 The University of Exeter + * 2018-2023 The University of Paris-Saclay * 2018 The University of Sheffield * * License: @@ -30,8 +30,8 @@ While Isabelle is widely perceived as an interactive theorem prover for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we would like to emphasize the view that Isabelle is far more than that: it is the \<^emph>\Eclipse of Formal Methods Tools\. This refers to the ``\<^emph>\generic system framework of Isabelle/Isar underlying recent versions of Isabelle. -Among other things, Isar provides an infrastructure for Isabelle plug-ins, comprising extensible -state components and extensible syntax that can be bound to ML programs. Thus, the Isabelle/Isar +Among other things, Isabelle provides an infrastructure for Isabelle plug-ins, comprising extensible +state components and extensible syntax that can be bound to SML programs. Thus, the Isabelle architecture may be understood as an extension and refinement of the traditional `LCF approach', with explicit infrastructure for building derivative systems.\''~@{cite "wenzel.ea:building:2007"} @@ -49,9 +49,13 @@ The Isabelle system architecture shown in @{docitem \architecture\} with Standard ML (SML) at the bottom layer as implementation language. The architecture actually foresees a \<^emph>\Nano-Kernel\ (our terminology) which resides in the SML structure \<^boxed_sml>\Context\. This structure provides a kind of container called \<^emph>\context\ providing an identity, an -ancestor-list as well as typed, user-defined state for components (plugins) such as \<^isadof>. +ancestor-list as well as typed, user-defined state for plugins such as \<^isadof>. On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific -support for higher specification constructs were built.\ +support for higher specification constructs were built. +\<^footnote>\We use the term \<^emph>\plugin\ for a collection of HOL-definitions, SML and Scala code in order +to distinguish it from the official Isabelle term \<^emph>\component\ which implies a particular +format and support by the Isabelle build system.\ +\ section*[dof::introduction]\The Document Model Required by \<^dof>\ text\ @@ -72,13 +76,13 @@ declare_reference*["fig:dependency"::figure] text\ The Isabelle Framework is based on a \<^emph>\document-centric view\\<^bindex>\document-centric view\ of a document, treating the input in its integrality as set of (user-programmable) \<^emph>\document element\ - that may mutually depend on and link to each other; A \<^emph>\document\ in our sense is what is configured in a set of - \<^verbatim>\ROOT\- and \<^verbatim>\ROOTS\-files. + that may mutually depend on and link to each other; A \<^emph>\document\ in our sense is what is configured + in a set of \<^verbatim>\ROOT\- and \<^verbatim>\ROOTS\-files. Isabelle assumes a hierarchical document model\<^index>\document model\, \<^ie>, an \<^emph>\integrated\ document consist of a hierarchy of \<^emph>\sub-documents\ (files); dependencies are restricted to be acyclic at this level. - Sub-documents can have different document types in order to capture documentations consisting of + Document parts can have different document types in order to capture documentations consisting of documentation, models, proofs, code of various forms and other technical artifacts. We call the main sub-document type, for historical reasons, \<^emph>\theory\-files. A theory file\<^bindex>\theory!file\ consists of a \<^emph>\header\\<^bindex>\header\, a \<^emph>\context definition\\<^index>\context\, and a body @@ -108,9 +112,9 @@ contains characters and a special notation for semantic macros \<^bindex>\ (here \<^theory_text>\@{term "fac 5"}).\ \ -text\While we concentrate in this manual on \<^theory_text>\text\-document elements --- this is the main -use of \<^dof> in its current stage --- it is important to note that there are actually three -families of ``ontology aware'' document elements with analogous +text\While \<^theory_text>\text\- elements play a major role in this manual on +--- this is the main use of \<^dof> in its current stage --- it is important to note that there +are actually three families of ``ontology aware'' document elements with analogous syntax to standard ones. The difference is a bracket with meta-data of the form: @{theory_text [display,indent=5, margin=70] \ @@ -123,7 +127,8 @@ Depending on the family, we will speak about \<^emph>\(formal) text-contex \<^emph>\(ML) code-contexts\\<^index>\code-contexts\ and \<^emph>\term-contexts\\<^index>\term-contexts\ if we refer to sub-elements inside the \\...\\ cartouches of these command families. Note that the Isabelle framework allows for nesting cartouches that permits to support switching into a different -context. In general, this has also the effect that the evaluation of antiquotations changes. +context, albeit not all combinations are actually supported. +In general, nesting contexts has the effect that the evaluation of antiquotations changes. \<^footnote>\In the literature, this concept has been referred to \Cascade-Syntax\ and was used in the Centaur-system and is existing in some limited form in some Emacs-implementations these days. \ \