Theory scholarly_paper

(*************************************************************************
 * Copyright (C) 
 *               2019      The University of Exeter 
 *               2018-2019 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
 *************************************************************************)

chapter‹An example ontology for scientific, MINT-oriented papers.›

theory scholarly_paper
  imports "Isabelle_DOF.Isa_COL"
  keywords "author*" "abstract*"                                :: document_body
    and    "Proposition*" "Definition*" "Lemma*" "Theorem*"     :: document_body 
    and    "Premise*" "Corollary*" "Consequence*" "Conclusion*" :: document_body
    and    "Assumption*" "Hypothesis*" "Assertion*"             :: document_body
    and    "Proof*" "Example*"                                  :: document_body
begin

define_ontology "DOF-scholarly_paper.sty" "Writing academic publications."

text‹Scholarly Paper provides a number of standard text - elements for scientific papers.
They were introduced in the following.›

section‹General Paper Structuring Elements›
doc_class title =
   short_title :: "string option"  <=  "None"
    
doc_class subtitle =
   abbrev ::      "string option"  <=  "None"
   
(* adding a contribution list and checking that it is cited as well in tech as in conclusion. ? *)

doc_class author =
   email       :: "string" <= "''''"
   http_site   :: "string" <= "''''"
   orcid       :: "string" <= "''''"
   affiliation :: "string"


doc_class abstract =
   keywordlist        :: "string list"   <= "[]" 
   principal_theorems :: "thm list"


ML‹
val _ =
  Monitor_Command_Parser.document_command command_keyword‹abstract*› "Textual Definition"
    {markdown = true, body = true}
    (Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []) [] I;

val _ =
  Monitor_Command_Parser.document_command command_keyword‹author*› "Textual Definition"
    {markdown = true, body = true}
    (Onto_Macros.enriched_document_cmd_exp (SOME "author") []) [] I;
›

text‹Scholarly Paper is oriented towards the classical domains in science:
▸ mathematics
▸ informatics
▸ natural sciences
▸ technology (= engineering)

which we formalize into:›

doc_class text_section = text_element +
   main_author :: "author option"  <=  None
   fixme_list  :: "string list"    <=  "[]" 
   level       :: "int  option"    <=  "None"
   (* this attribute enables doc-notation support section* etc.
      we follow LaTeX terminology on levels 
                part          = Some -1
                chapter       = Some 0
                section       = Some 1
                subsection    = Some 2
                subsubsection = Some 3
       ... *)
   (* for scholarly paper: invariant level > 0 *)


doc_class "conclusion" = text_section +
   main_author :: "author option"  <=  None
   invariant level    :: "(level σ) ≠ None ∧ the (level σ) > 0"
   
doc_class related_work = "conclusion" +
   main_author :: "author option"  <=  None
   invariant level    :: "(level σ) ≠ None ∧ the (level σ) > 0"

doc_class bibliography = text_section +
   style       :: "string option"  <=  "Some ''LNCS''"
   invariant level    :: "(level σ) ≠ None ∧ the (level σ) > 0"

doc_class annex = "text_section" +
   main_author :: "author option"  <=  None
   invariant level    :: "(level σ) ≠ None ∧ the (level σ) > 0"

find_consts name:"scholarly_paper.*Leeee"

(*
datatype sc_dom = math | info | natsc | eng 
*)


doc_class introduction = text_section +
   comment :: string
   claims  :: "thm list"
   invariant level    :: "(level σ) ≠ None ∧ the (level σ) > 0"

text‹Technical text-elements posses a status: they can be either an ∗‹informal explanation› /
description or a kind of introductory text to definition etc. or a ∗‹formal statement› similar
to :

❙‹Definition› 3.1: Security. 
As Security of the system we define etc...

A formal statement can, but must not have a reference to true formal Isabelle/Isar definition. 
›

doc_class background = text_section +
   comment :: string
   claims  :: "thm list"
   invariant level    :: "(level σ) ≠ None ∧ the (level σ) > 0"


section‹Technical Content and Free-form Semi-formal Formats›

datatype status = formal | semiformal | description

text‹The class ▩‹technical› regroups a number of text-elements that contain typical 
"technical content" in mathematical or engineering papers: definitions, theorems, lemmas, examples.  ›

(* OPEN PROBLEM: connection between referentiable and status. This should be explicit 
   and computable. *)


doc_class technical = text_section +
   definition_list :: "string list" <=  "[]"
   status          :: status <= "description"
   formal_results  :: "thm list"
   invariant level  :: "(level σ) ≠ None ∧ the (level σ) > 0"

type_synonym tc = technical (* technical content *)


text ‹This a ‹doc_class› of ▩‹examples› in the broadest possible sense : they are \emph{not}
necessarily considered as technical content, but may occur in an article. 
Note that there are ‹doc_class›es of ▩‹math_example›s and ▩‹tech_example›s which 
follow a more specific regime of mathematical or engineering content.
›
(* An example for the need of multiple inheritance on classes ? *)

doc_class example  = text_section + 
   referentiable   :: bool <= True
   status          :: status <= "description"
   short_name      :: string <= "''''"
   invariant level    :: "(level σ) ≠ None ∧ the (level σ) > 0"

text‹The intended use for the ‹doc_class›es ▩‹math_motivation› (or ▩‹math_mtv› for short),
     ▩‹math_explanation› (or ▩‹math_exp› for short) and 
     ▩‹math_example› (or ▩‹math_ex› for short)
     are ∗‹informal› descriptions of semi-formal definitions (by inheritance).
     Math-Examples can be made referentiable triggering explicit, numbered presentations.›
doc_class math_motivation  = technical +  
   referentiable :: bool <= False
type_synonym math_mtv = math_motivation

doc_class math_explanation  = technical +
   referentiable :: bool <= False
type_synonym math_exp = math_explanation


subsection‹Freeform Mathematical Content›

text‹We follow in our enumeration referentiable mathematical content class the AMS style and its
provided ∗‹theorem environments› (see ▩‹texdoc amslatex›). We add, however, the concepts 
▩‹axiom›, ▩‹rule› and ▩‹assertion› to the list. A particular advantage of ▩‹texdoc amslatex› is 
that it is well-established and compatible with many LaTeX - styles.

The names for thhe following key's are deliberate non-standard abbreviations in order to avoid
future name clashes.›

datatype math_content_class = 
    "defn"       ―‹definition› 
  | "axm"        ―‹axiom›
  | "theom"      ―‹theorem› 
  | "lemm"       ―‹lemma›
  | "corr"       ―‹corollary›
  | "prpo"       ―‹proposition›
  | "rulE"       ―‹rule›
  | "assn"       ―‹assertion›    
  | "hypt"      ―‹hypothesis›    
  | "assm"       ―‹assumption›
  | "prms"       ―‹premise›  
  | "cons"       ―‹consequence›
  | "conc_stmt"  ―‹math. conclusion›
  | "prf_stmt"   ―‹math. proof›
  | "expl_stmt"  ―‹math. example› 
  | "rmrk"       ―‹remark›  
  | "notn"       ―‹notation›  
  | "tmgy"       ―‹terminology›

text‹Instances of the ‹doc_class› ▩‹math_content› are by definition @{term "semiformal"}; they may
be non-referential, but in this case they will not have a @{term "short_name"}.›

doc_class math_content = technical +
   referentiable :: bool <= False
   short_name    :: string <= "''''"
   status        :: status <= "semiformal"
   mcc           :: "math_content_class" <= "theom" 
   invariant s1  :: "¬referentiable σ ⟶ short_name σ = ''''"
   invariant s2  :: "technical.status σ = semiformal"
type_synonym math_tc = math_content

text‹The class typ‹math_content› is perhaps more adequaltely described as "math-alike content".
Sub-classes can englobe instances such as:
▪ terminological definitions such as:
  ‹Definition*[assessor::sfc, short_name="''assessor''"]‹entity that carries out an assessment››
▪ free-form mathematical definitions such as:
  ‹Definition*[process_ordering, short_name="''process ordering''"]‹
   We define ‹P ⊑ Q ≡ ψ𝒟 ∧ ψℛ ∧ ψℳ ›,  where vs‹-0.2cm›
   1) vs‹-0.2cm› ‹ψ𝒟 = 𝒟 P ⊇ 𝒟 Q ›
   2) ...
   ››
▪ semi-formal descriptions, which are free-form mathematical definitions on which finally
  an attribute with a formal Isabelle definition is attached. ›


text‹Instances of the Free-form Content are Definition, Lemma, Assumption, Hypothesis, etc.
     The key class definitions are inspired by the AMS style, to which some target LaTeX's compile.›   

text‹A proposition (or: "sentence") is a central concept in philosophy of language and related 
fields, often characterized as the primary bearer of truth or falsity. Propositions are also often 
characterized as being the kind of thing that declarative sentences denote. ›

doc_class "proposition"  = math_content +
   referentiable :: bool <= True
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "prpo" 
   invariant d  :: "mcc σ = prpo" (* can not be changed anymore. *)

text‹A definition is used to give a precise meaning to a new term, by describing a 
condition which unambiguously qualifies what a mathematical term is and is not. Definitions and 
axioms form the basis on which all of modern mathematics is to be constructed.›
doc_class "definition"  = math_content +
   referentiable :: bool <= True
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "defn" 
   invariant d  :: "mcc σ = defn" (* can not be changed anymore. *)

doc_class "axiom"  = math_content +
   referentiable :: bool <= True
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "axm" 
   invariant d  :: "mcc σ = axm" (* can not be changed anymore. *)

text‹A lemma (plural lemmas or lemmata) is a generally minor, proven proposition which is used as 
a stepping stone to a larger result. For that reason, it is also known as a "helping theorem" or an 
"auxiliary theorem". In many cases, a lemma derives its importance from the theorem it aims to prove.›
doc_class "lemma"       = math_content +
   referentiable :: bool <= "True"
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "lemm" 
   invariant d  :: "mcc σ = lemm"

doc_class "theorem"     = math_content +
   referentiable :: bool <= True
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "theom" 
   invariant d  :: "mcc σ = theom"

text‹A corollary is a theorem of less importance which can be readily deduced from a previous, 
more notable lemma or theorem. A corollary could, for instance, be a proposition which is incidentally 
proved while proving another proposition.›
doc_class "corollary"   = math_content +
   referentiable :: bool <= "True"
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "corr" 
   invariant d  :: "mcc σ = corr"


text‹A premise or premiss[a] is a proposition — a true or false declarative statement—
     used in an argument to prove the truth of another proposition called the conclusion.›
doc_class "premise"     = math_content +
   referentiable :: bool <= "True"
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "prms" 
   invariant d  :: "mcc σ = prms"

text‹A consequence describes the relationship between statements that hold true when one statement 
logically follows from one or more statements. A valid logical argument is one in which the 
conclusion is entailed by the premises, because the conclusion is the consequence of the premises. 
The philosophical analysis of logical consequence involves the questions: In what sense does a 
conclusion follow from its premises?›
doc_class "consequence" = math_content +
   referentiable :: bool <= "True"
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "cons" 
   invariant d  :: "mcc σ = cons"

doc_class "conclusion_stmt" = math_content +   ― ‹not to confuse with a section element: Conclusion›
   referentiable :: bool <= "True"
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "conc_stmt" 
   invariant d  :: "mcc σ = conc_stmt"

text‹An assertion is a statement that asserts that a certain premise is true.›
doc_class "assertion"   = math_content +
   referentiable :: bool <= "True"
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "assn" 
   invariant d  :: "mcc σ = assn"

text‹An assumption is an explicit or a tacit proposition about the world or a background belief 
relating to an proposition.›
doc_class "assumption"  = math_content +
   referentiable :: bool <= "True"
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "assm" 
   invariant d  :: "mcc σ = assm"

text‹ A working hypothesis is a provisionally accepted hypothesis proposed for further research
 in a process beginning with an educated guess or thought.

 A different meaning of the term hypothesis is used in formal logic, to denote the antecedent of a 
 proposition; thus in the proposition "If ‹P›, then ‹Q›", ‹P› denotes the hypothesis (or antecedent); 
 ‹Q› can be called a consequent. ‹P› is the assumption in a (possibly counterfactual) What If question.›
doc_class "hypothesis"  = math_content +
   referentiable :: bool <= "True"
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "hypt" 
   invariant d :: "mcc σ = hypt"

doc_class "math_proof"  = math_content +
   referentiable :: bool <= "True"
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "prf_stmt" 
   invariant d :: "mcc σ = prf_stmt"

doc_class "math_example"= math_content +
   referentiable :: bool <= "True"
   level         :: "int option"         <= "Some 2"
   mcc           :: "math_content_class" <= "expl_stmt" 
   invariant d :: "mcc σ = expl_stmt"



subsection‹Support of Command Macros ▩‹Definition*› , ▩‹Lemma**›, ▩‹Theorem*› ... ›

text‹These ontological macros allow notations are defined for the class 
  typ‹math_content› in order to allow for a variety of free-form formats;
  in order to provide specific sub-classes, default options can be set
  in order to support more succinct notations and avoid constructs
  such as :

  ⬚‹Definition*[l::"definition"]‹...››.

  Instead, the more convenient global declaration 
  ⬚‹declare[[Definition_default_class="definition"]]›
  supports subsequent abbreviations:

    ⬚‹Definition*[l]‹...››.

  Via the default classes, it is also possible to specify the precise concept
  that are not necessarily in the same inheritance hierarchy: for example:
  ▪ mathematical definition vs terminological setting
  ▪ mathematical example vs. technical example. 
  ▪ mathematical proof vs. some structured argument
  ▪ mathematical hypothesis vs. philosophical/metaphysical assumption
  ▪ ... 

By setting the default classes, it is possible to reuse these syntactic support and give them
different interpretations in an underlying ontological class-tree.

›

ML‹

val (Proposition_default_class, Proposition_default_class_setup) 
     = Attrib.config_string binding‹Proposition_default_class› (K "");
val (Definition_default_class, Definition_default_class_setup) 
     = Attrib.config_string binding‹Definition_default_class› (K "");
val (Axiom_default_class, Axiom_default_class_setup) 
     = Attrib.config_string binding‹Axiom_default_class› (K "");
val (Lemma_default_class, Lemma_default_class_setup) 
     = Attrib.config_string binding‹Lemma_default_class› (K "");
val (Theorem_default_class, Theorem_default_class_setup) 
     = Attrib.config_string binding‹Theorem_default_class› (K "");
val (Corollary_default_class, Corollary_default_class_setup) 
     = Attrib.config_string binding‹Corollary_default_class› (K "");
val (Assumption_default_class, Assumption_default_class_setup) 
     = Attrib.config_string binding‹Assumption_default_class› (K "");
val (Assertion_default_class, Assertion_default_class_setup) 
     = Attrib.config_string binding‹Assertion_default_class› (K "");
val (Consequence_default_class, Consequence_default_class_setup) 
     = Attrib.config_string binding‹Consequence_default_class› (K "");
val (Conclusion_default_class, Conclusion_default_class_setup) 
     = Attrib.config_string binding‹Conclusion_default_class› (K "");
val (Premise_default_class, Premise_default_class_setup) 
     = Attrib.config_string binding‹Premise_default_class› (K "");
val (Hypothesis_default_class, Hypothesis_default_class_setup) 
     = Attrib.config_string binding‹Hypothesis_default_class› (K "");
val (Proof_default_class, Proof_default_class_setup) 
     = Attrib.config_string binding‹Proof_default_class› (K "");
val (Example_default_class, Example_default_class_setup) 
     = Attrib.config_string binding‹Example_default_class› (K "");
val (Remark_default_class, Remark_default_class_setup) 
     = Attrib.config_string binding‹Remark_default_class› (K "");
val (Notation_default_class, Notation_default_class_setup) 
     = Attrib.config_string binding‹Notation_default_class› (K "");

›

setup‹   Proposition_default_class_setup 
      #> Definition_default_class_setup 
      #> Axiom_default_class_setup 
      #> Lemma_default_class_setup 
      #> Theorem_default_class_setup 
      #> Corollary_default_class_setup 
      #> Assertion_default_class_setup 
      #> Assumption_default_class_setup 
      #> Premise_default_class_setup 
      #> Hypothesis_default_class_setup
      #> Consequence_default_class_setup 
      #> Conclusion_default_class_setup 
      #> Proof_default_class_setup 
      #> Remark_default_class_setup 
      #> Example_default_class_setup›

ML‹ 
local open ODL_Meta_Args_Parser in

local 
fun doc_cmd kwd txt flag key = 
    Monitor_Command_Parser.document_command kwd txt {markdown = true, body = true}
    (fn meta_args => fn thy =>
      let
        val ddc = Config.get_global thy flag 
        val default = SOME(((ddc = "") ? (K const_name‹math_content›)) ddc)
      in
        Onto_Macros.enriched_formal_statement_command  default [("mcc",key)] meta_args thy
      end)
      [const_name‹mcc›]
      (Onto_Macros.transform_attr [(const_name‹mcc›,key)])

in

val _ = doc_cmd command_keyword‹Definition*› "Freeform Definition" 
                Definition_default_class const_name‹defn›;

val _ = doc_cmd command_keyword‹Lemma*›      "Freeform Lemma Description" 
                 Lemma_default_class const_name‹lemm›;

val _ = doc_cmd command_keyword‹Theorem*›    "Freeform Theorem" 
                 Theorem_default_class const_name‹theom›;

val _ = doc_cmd command_keyword‹Proposition*› "Freeform Proposition"
                  Proposition_default_class const_name‹prpo›;

val _ = doc_cmd command_keyword‹Premise*› "Freeform Premise"
                  Premise_default_class const_name‹prms›;

val _ = doc_cmd command_keyword‹Corollary*› "Freeform Corollary"
                  Corollary_default_class const_name‹corr›;

val _ = doc_cmd command_keyword‹Consequence*› "Freeform Consequence"
                  Consequence_default_class const_name‹cons›;
                      
val _ = doc_cmd command_keyword‹Conclusion*› "Freeform Conclusion"
                  Conclusion_default_class const_name‹conc_stmt›;
                           
val _ = doc_cmd command_keyword‹Assumption*› "Freeform Assumption"
                  Assumption_default_class const_name‹assm›;

val _ = doc_cmd command_keyword‹Hypothesis*› "Freeform Hypothesis"
                  Hypothesis_default_class const_name‹prpo›;

val _ = doc_cmd command_keyword‹Assertion*› "Freeform Assertion"
                  Assertion_default_class const_name‹assn›;

val _ = doc_cmd command_keyword‹Proof*› "Freeform Proof"
                  Proof_default_class const_name‹prf_stmt›;

val _ = doc_cmd command_keyword‹Example*› "Freeform Example"
                  Example_default_class const_name‹expl_stmt›;
end
end 
›


subsection‹Formal Mathematical Content›
text‹While this library is intended to give a lot of space to freeform text elements in
order to counterbalance Isabelle's standard view, it should not be forgot that the real strength
of Isabelle is its ability to handle both - and to establish links between both worlds. Therefore:›

doc_class math_formal  = math_content +
   referentiable :: bool <= False
   status        :: status <= "formal"
   properties    :: "term list"
type_synonym math_fc = math_formal



subsubsection*[ex_ass::example]‹Logical Assertions›

text‹Logical assertions allow for logical statements to be checked in the global context). ›

assert*[ass1::assertion, short_name = "‹This is an assertion›"] ‹(3::int) < 4›


subsection‹Content in Engineering/Tech Papers ›
text‹This section is currently experimental and not supported by the documentation 
     generation backend.›

doc_class engineering_content = technical +
   short_name :: string <= "''''"
   status     :: status
type_synonym eng_content = engineering_content


doc_class "experiment"  = engineering_content +
   tag :: "string" <=  "''''"

doc_class "evaluation"  = engineering_content +
   tag :: "string" <=  "''''"

doc_class "data"  = engineering_content +
   tag :: "string" <=  "''''"

doc_class tech_definition = engineering_content +
   referentiable :: bool <= True
   tag :: "string" <=  "''''"

doc_class tech_code = engineering_content +
   referentiable :: bool <= True
   tag :: "string" <=  "''''"

doc_class tech_example = engineering_content +
   referentiable :: bool <= True
   tag :: "string" <=  "''''"

doc_class eng_example = engineering_content +
   referentiable :: bool <= True
   tag :: "string" <=  "''''"


subsection‹Some Summary›

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 ›
(* todo : could be finer *)

text‹ Besides subtyping, there is another relation between
doc\_classes: a class can be a ∗‹monitor› to other ones,
which is expressed by occurrence in the where clause.
While sub-classing refers to data-inheritance of attributes,
a monitor captures structural constraints -- the order --
in which instances of monitored classes may occur.

The control of monitors is done by the commands:
▪ ▩‹ monitor <oid::class_type, <attributes-defs> > ›
▪ ▩‹ close_monitor <oid[::class_type],<attributes-updates>> ›

where the automaton of the monitor class is expected
to be in a final state.

Monitors can be nested.

Classes neither directly or  indirectly (via inheritance)
mentioned in the monitor clause are ∗‹independent› from
the monitor and may occur freely, \ie{} in arbitrary order.n ›


text ‹underlying idea: a monitor class automatically receives a  
    ▩‹trace› attribute in which a list of observed class-ids is maintained.
    The ▩‹trace› is a ∗‹`predefined id`› like ▩‹main› in C. It can be accessed
    like any other attribute of a class instance, \ie{} a document item.›

doc_class article = 
   style_id :: string                <= "''LNCS''"
   version  :: "(int × int × int)"  <= "(0,0,0)"
   accepts "(title                   ~~ 
            ⟦subtitle⟧                ~~
            ⦃author⦄+                 ~~ 
            abstract                  ~~
            ⦃introduction⦄+           ~~ 
            ⦃background⦄*             ~~ 
            ⦃technical || example || float ⦄+      ~~
            ⦃conclusion⦄+             ~~  
            bibliography              ~~
            ⦃annex⦄* )"


ML‹
structure Scholarly_paper_trace_invariant =
struct 
local

fun group _ _ _ [] = []
   |group f g cidS (a::S) = case find_first (f a) cidS of
                            NONE => [a] :: group f g cidS S
                          | SOME cid => let val (pref,suff) =  chop_prefix  (g cid) S
                                        in (a::pref)::(group f g cidS suff) end;

fun partition ctxt cidS trace = 
    let fun find_lead (x,_) = DOF_core.is_subclass ctxt x;
        fun find_cont cid (cid',_) =  DOF_core.is_subclass ctxt cid' cid
    in group find_lead find_cont cidS trace end;

fun dest_option _ (Const (@{const_name "None"}, _)) = NONE
  | dest_option f (Const (@{const_name "Some"}, _) $ t) = SOME (f t)

in 

fun check ctxt cidS mon_id pos_opt =
    let val trace  = AttributeAccess.compute_trace_ML ctxt mon_id pos_opt @{here}
        val groups = partition (Context.proof_of ctxt) cidS trace
        fun get_level_raw oid = ISA_core.compute_attr_access ctxt "level" oid NONE @{here};
        fun get_level oid = dest_option (snd o HOLogic.dest_number) (get_level_raw (oid));
        fun check_level_hd a = case (get_level (snd a)) of
                                  NONE => error("Invariant violation: leading section " ^ snd a ^ 
                                                " must have lowest level")
                                | SOME X => X
        fun check_group_elem level_hd a = case (get_level (snd a)) of
                                              NONE => true
                                            | SOME y => if level_hd <= y then true
                                                        (* or < ? But this is too strong ... *)
                                                        else error("Invariant violation: "^
                                                                   "subsequent section " ^ snd a ^ 
                                                                   " must have higher level.");
        fun check_group [] = true
           |check_group [_] = true
           |check_group (a::S) = forall (check_group_elem (check_level_hd a)) (S)
    in if forall check_group groups then () 
       else error"Invariant violation: leading section must have lowest level" 
    end
end

end
›

setup‹
(fn thy => 
let val cidS = ["scholarly_paper.introduction","scholarly_paper.technical", 
                       "scholarly_paper.example", "scholarly_paper.conclusion"];
    fun body moni_oid _ ctxt = (Scholarly_paper_trace_invariant.check ctxt cidS moni_oid NONE; true)
    val ctxt = Proof_Context.init_global thy
    val cid = "article"
    val binding = DOF_core.binding_from_onto_class_pos cid thy
    val cid_long = DOF_core.get_onto_class_name_global cid thy
in  DOF_core.add_ml_invariant binding (DOF_core.make_ml_invariant (body, cid_long)) thy end)
›

term‹float›
section‹Miscelleous›

subsection‹Common Abbreviations›

define_shortcut* eg  ⇌ ‹\eg›  (* Latin: „exempli gratia“  meaning  „for example“. *)
                 ie  ⇌ ‹\ie›  (* Latin: „id est“  meaning „that is to say“. *)
                 etc ⇌ ‹\etc› (* Latin : „et cetera“ meaning „et cetera“ *)

print_doc_classes

end