Theory M_00_Frontmatter

(*************************************************************************
 * Copyright (C) 
 *               2019-2022 The University of Exeter 
 *               2018-2022 The University of Paris-Saclay
 *               2018      The University of Sheffield
 *
 * License:
 *   This program can be redistributed and/or modified under the terms
 *   of the 2-clause BSD-style license.
 *
 *   SPDX-License-Identifier: BSD-2-Clause
 *************************************************************************)

(*<*)
theory "M_00_Frontmatter"
  imports 
    "Isabelle_DOF.technical_report"
begin
 
use_template "scrreprt-modern"
use_ontology "technical_report"

section‹Local Document Setup.›
text‹Introducing document specific abbreviations and macros:›

define_shortcut* dof     ⇌ ‹\dof›
                 isadof  ⇌ ‹\isadof{}›

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 
     are defined, eg, in the document prelude. ›

define_macro* index     ⇌ ‹\index{› _ ‹}›
define_macro* bindex    ⇌ ‹\bindex{› _ ‹}›
define_macro* nolinkurl ⇌ ‹\nolinkurl{› _ ‹}›
define_macro* center    ⇌ ‹\center{› _ ‹}›
define_macro* ltxinline ⇌ ‹\inlineltx|› _ ‹|›

ML‹

fun boxed_text_antiquotation name (* redefined in these more abstract terms *) =
    DOF_lib.gen_text_antiquotation name DOF_lib.report_text 
                           (fn ctxt => DOF_lib.string_2_text_antiquotation ctxt
                                       #> DOF_lib.enclose_env false ctxt "isarbox")

val neant = K(Latex.text("",⌂))

fun boxed_theory_text_antiquotation name (* redefined in these more abstract terms *) =
    DOF_lib.gen_text_antiquotation name DOF_lib.report_theory_text 
                           (fn ctxt => DOF_lib.string_2_theory_text_antiquotation ctxt 
                                        #> DOF_lib.enclose_env false ctxt "isarbox"
                                        (* #> neant *)) (*debugging *)

fun boxed_sml_text_antiquotation name  =
    DOF_lib.gen_text_antiquotation name (K(K())) 
                           (fn ctxt => Input.source_content 
                                        #> Latex.text 
                                        #> DOF_lib.enclose_env true ctxt "sml") 
                           (* the simplest conversion possible *)

fun boxed_pdf_antiquotation name =
    DOF_lib.gen_text_antiquotation name (K(K())) 
                           (fn ctxt => Input.source_content 
                                        #> Latex.text 
                                        #> DOF_lib.enclose_env true ctxt "out") 
                           (* the simplest conversion possible *)

fun boxed_latex_antiquotation name =
    DOF_lib.gen_text_antiquotation name (K(K())) 
                           (fn ctxt => Input.source_content 
                                        #> Latex.text 
                                        #> DOF_lib.enclose_env true ctxt "ltx") 
                           (* the simplest conversion possible *)

fun boxed_bash_antiquotation name =
    DOF_lib.gen_text_antiquotation name (K(K())) 
                           (fn ctxt => Input.source_content 
                                        #> Latex.text 
                                        #> DOF_lib.enclose_env true ctxt "bash") 
                           (* the simplest conversion possible *)
›

setup‹boxed_text_antiquotation         binding‹boxed_text› #>
      boxed_text_antiquotation         binding‹boxed_cartouche› #>
      boxed_theory_text_antiquotation  binding‹boxed_theory_text› #>

      boxed_sml_text_antiquotation     binding‹boxed_sml› #>
      boxed_pdf_antiquotation          binding‹boxed_pdf› #>
      boxed_latex_antiquotation        binding‹boxed_latex›#>
      boxed_bash_antiquotation         binding‹boxed_bash› 
     ›

open_monitor*[this::report] 

(*>*)

title*[title::title]         ‹Isabelle/DOF› 
subtitle*[subtitle::subtitle]‹User and Implementation Manual› 
author*[  adb,
          email       ="‹a.brucker@exeter.ac.uk›",
          orcid       ="‹0000-0002-6355-1200›",
          http_site   ="‹https://www.brucker.ch/›",
          affiliation ="‹University of Exeter, Exeter, UK›"]‹Achim D. Brucker›
author*[  nico,
          email       = "‹nicolas.meric@lri.fr›",
          affiliation = "‹Université Paris-Saclay, LRI, Paris, France›"]‹Nicolas Méric›
author*[  bu,
          email       = "‹wolff@lri.fr›",
          affiliation = "‹Université Paris-Saclay, LRI, Paris, France›"]‹Burkhart Wolff›
 
abstract*[abs, keywordlist="[‹Ontology›, ‹Ontological Modeling›, ‹Document Management›, 
                             ‹Formal Document Development›,‹Isabelle/DOF›]"]
‹   isadof provides an implementation of dof on top of Isabelle/HOL. 
    dof itself is a novel framework for ∗‹defining› ontologies
    and ∗‹enforcing› them during document development and document
    evolution. isadof targets use-cases such as mathematical texts referring
    to a theory development or technical reports requiring a particular structure.
    A major application of dof is the integrated development of
    formal certification documents (eg, for Common Criteria or CENELEC
    50128) that require consistency across both formal and informal
    arguments.

    isadof is integrated into Isabelle's IDE, which
    allows for smooth ontology development as well as immediate
    ontological feedback during the editing of a document.
    Its checking facilities leverage the collaborative 
    development of documents required to be consistent with an
    underlying ontological structure.
    
    In this user-manual, we give an in-depth presentation of the design
    concepts of dof's Ontology Definition Language (ODL) and describe
    comprehensively its major commands. Many examples show typical best-practice
    applications of the system.
  
    It is a unique feature of  isadof  that ontologies may be used to control
    the link between formal and informal content in documents inan automatic-checked way. 
    These links can connect both text elements and formal
    modeling elements such as terms, definitions, code  and logical formulas,
    altogether ∗‹integrated› into a state-of-the-art interactive theorem prover.

›

(*<*) 
end
(*>*)