Theory M_04_Document_Ontology

(*************************************************************************
 * Copyright (C) 
 *               2019-2022 University of Exeter 
 *               2018-2022 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_04_Document_Ontology"
  imports 
    "M_03_GuidedTour"
  keywords "class_synonym" :: thy_defn
begin

(*>*)


(*<*)
definition combinator1 :: "'a ⇒ ('a ⇒ 'b) ⇒ 'b" (infixl "|>" 65)
  where "x |> f = f x"


ML‹
local
val _ =
  Outer_Syntax.local_theory \<^command_keyword>‹class_synonym› "declare type abbreviation"
    (Parse.type_args -- Parse.binding --
      (\<^keyword>‹=› |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
      >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));

in end
›

(*>*)


(*<*)

doc_class "title"  = short_title :: "string option" <= "None"


doc_class elsevier =
  organization :: string
  address_line :: string
  postcode :: int
  city :: string
  
(*doc_class elsevier_affiliation = affiliation +*) 

doc_class acm =
  position :: string
  institution :: string
  department :: int
  street_address :: string
  city :: string
  state :: int
  country :: string
  postcode :: int

(*doc_class acm_affiliation = affiliation +*)

doc_class lncs =
  institution :: string

(*doc_class lncs_affiliation = affiliation +*)


doc_class author =
    name        :: string
    email       :: "string"   <= "''''"
    invariant ne_name :: "name σ ≠ ''''"

doc_class elsevier_author = "author" +
  affiliations :: "elsevier list"
  short_author :: string
  url :: string
  footnote :: string

text*[el1:: "elsevier"]‹›
(*text*[el_aff1:: "affiliation", journal_style = "@{elsevier ‹el1›}"]‹›*)
term*‹@{elsevier ‹el1›}›
text*[el_auth1:: "elsevier_author", affiliations = "[@{elsevier ‹el1›}]"]‹›

doc_class acm_author = "author" +
  affiliations :: "acm list"
  orcid :: int
  footnote :: string

text*[acm1:: "acm"]‹›
(*text*[acm_aff1:: "acm affiliation", journal_style = "@{acm ‹acm1›}"]‹›*)
text*[acm_auth1:: "acm_author", affiliations = "[@{acm ‹acm1›}]"]‹›

doc_class lncs_author = "author" +
  affiliations :: "lncs list"
  orcid :: int
  short_author :: string
  footnote :: string

text*[lncs1:: "lncs"]‹›
(*text*[lncs_aff1:: "lncs affiliation", journal_style = "@{lncs ‹lncs1›}"]‹›*)
text*[lncs_auth1:: "lncs_author", affiliations = "[@{lncs ‹lncs1›}]"]‹›


doc_class  "text_element" =
    authored_by :: "author set"  <= "{}"
    level       :: "int  option"  <= "None"
    invariant authors_req :: "authored_by σ ≠ {}" 
    and       level_req   :: "the (level σ) > 1"

doc_class "introduction" = "text_element" +
    authored_by :: "(author) set"  <= "UNIV"

doc_class  "technical" = "text_element" +
    formal_results  :: "thm list"

doc_class "definition" = "technical" +
    is_formal   :: "bool"

doc_class "theorem" = "technical" +
    is_formal   :: "bool"
    assumptions :: "term list"        <= "[]"
    statement   :: "term option"      <= "None"

doc_class "conclusion" = "text_element" +
    resumee     :: "(definition set × theorem set)"
    invariant is_form :: "(∃x∈(fst (resumee σ)). definition.is_formal x) ⟶ 
                  (∃y∈(snd (resumee σ)). is_formal y)"

text*[def::"definition", is_formal = "True"]‹›
text*[theo::"theorem", is_formal = "False"]‹›
text*[conc::"conclusion", resumee="({@{definition ‹def›}}, {@{theorem ‹theo›}})"]‹›

value*‹resumee @{conclusion ‹conc›} |> fst›
value*‹resumee @{conclusion ‹conc›} |> snd›

doc_class "article" =
    style_id    :: string   <= "''LNCS''"
    accepts "(title ~~ ⦃author⦄⇧+ ~~ ⦃introduction⦄⇧+  
             ~~ ⦃⦃definition ~~ example⦄⇧+ || theorem⦄⇧+ ~~ ⦃conclusion⦄⇧+)"


datatype kind = expert_opinion | argument | "proof"

onto_class  result = " technical" +
  evidence :: kind
  property :: " theorem list" <= "[]"
  invariant has_property :: "evidence σ = proof ⟷ property σ ≠ []"

(*>*)

text*[paper_m::float, main_caption="‹A Basic Document Ontology: paper$^m$›"]‹
 @{boxed_theory_text [display,indent=5] 
   ‹doc_class "title"  = short_title :: "string option" <= "None"
doc_class affiliation =
  journal_style :: 'α
doc_class author =
    affiliations :: "'α affiliation list"
    name        :: string
    email       :: "string"   <= "''''"
    invariant ne_name :: "name σ ≠ ''''"
doc_class "text_element" =
    authored_by :: "('α author) set"  <= "{}"
    level       :: "int  option"  <= "None"
    invariant authors_req :: "authored_by ≠ {}" 
    and        level_req    :: "the (level) > 1"
doc_class "introduction" = text_element +
    authored_by :: "('α author) set"  <= "UNIV"
doc_class "technical" = text_element +
    formal_results  :: "thm list"
doc_class "definition" = technical +
    is_formal   :: "bool"
doc_class "theorem" = technical +
    assumptions :: "term list"        <= "[]"
    statement   :: "term option"      <= "None"
doc_class "conclusion" = text_element +
    resumee     :: "(definition set × theorem set)"
    invariant (∀x∈fst resumee. is_formal x)
                  ⟶ (∃y∈snd resumee. is_formal y)
doc_class "article" = 
    style_id    :: string   <= "''LNCS''"
    accepts "(title ~~ ⦃author⦄⇧+ ~~ ⦃introduction⦄⇧+  
             ~~ ⦃⦃definition ~~ example⦄⇧+ || theorem⦄⇧+ ~~ ⦃conclusion⦄⇧+)"›}
›


(*<*)
datatype role =  PM     ― ‹Program Manager›
              |  RQM    ― ‹Requirements Manager› 
              |  DES    ― ‹Designer›
              |  IMP    ― ‹Implementer› 
              |  ASR    ― ‹Assessor› 
              |  INT    ― ‹Integrator› 
              |  TST    ― ‹Tester›
              |  VER    ― ‹Verifier›
              |  VnV    ― ‹Verification and Validation›
              |  VAL    ― ‹Validator›

abbreviation developer where "developer ==   DES"
abbreviation validator where "validator ==   VAL"
abbreviation verifier where "verifier ==   VER"

doc_class requirement = Isa_COL.text_element +
  long_name :: "string option"
  is_concerned :: "role set"

text*[req1::requirement,
      is_concerned="{developer, validator}"]
‹The operating system shall provide secure
memory separation.›

text‹
The recurring issue of the certification
is @{requirement ‹req1›} ...›

term "⦇long_name = None,is_concerned = {developer,validator}⦈"
(*>*)

(*<*)
end
(*>*)