2018-04-05 10:09:58 +00:00
|
|
|
section{* An example ontology for a scholarly paper*}
|
2018-03-27 07:41:39 +00:00
|
|
|
|
2018-04-05 10:09:58 +00:00
|
|
|
theory scholarly_paper
|
2018-03-28 19:08:37 +00:00
|
|
|
imports "../Isa_DOF"
|
2018-03-21 10:59:27 +00:00
|
|
|
begin
|
|
|
|
|
|
|
|
doc_class title =
|
2018-04-17 13:08:01 +00:00
|
|
|
short_title :: "string option" <= "None"
|
|
|
|
|
2018-03-21 10:59:27 +00:00
|
|
|
doc_class subtitle =
|
2018-04-17 15:39:16 +00:00
|
|
|
abbrev :: "string option" <= "None"
|
2018-03-27 07:41:39 +00:00
|
|
|
|
|
|
|
-- \<open>adding a contribution list and checking that it is cited as well in tech as in conclusion. ? \<close>
|
2018-03-21 10:59:27 +00:00
|
|
|
|
|
|
|
doc_class author =
|
2018-04-27 08:34:24 +00:00
|
|
|
email :: "string"
|
2018-04-28 20:45:02 +00:00
|
|
|
orcid :: "string"
|
2018-03-21 10:59:27 +00:00
|
|
|
affiliation :: "string"
|
|
|
|
|
|
|
|
doc_class abstract =
|
2018-04-30 08:48:14 +00:00
|
|
|
keywordlist :: "string list" <= "[]"
|
|
|
|
principal_theorems :: "thm list"
|
2018-04-27 08:34:24 +00:00
|
|
|
|
2018-03-27 07:41:39 +00:00
|
|
|
doc_class text_section =
|
2018-04-05 10:09:58 +00:00
|
|
|
main_author :: "author option" <= None
|
2018-05-01 09:38:56 +00:00
|
|
|
fixme_list :: "string list" <= "[]"
|
2018-04-27 08:34:24 +00:00
|
|
|
|
2018-03-27 07:41:39 +00:00
|
|
|
doc_class introduction = text_section +
|
2018-04-27 15:12:42 +00:00
|
|
|
comment :: string
|
2018-05-01 09:38:56 +00:00
|
|
|
claims :: "thm list"
|
2018-03-21 10:59:27 +00:00
|
|
|
|
2018-03-27 07:41:39 +00:00
|
|
|
doc_class technical = text_section +
|
2018-04-05 10:09:58 +00:00
|
|
|
definition_list :: "string list" <= "[]"
|
2018-04-30 08:48:14 +00:00
|
|
|
formal_results :: "thm list"
|
2018-04-27 08:34:24 +00:00
|
|
|
|
2018-04-17 13:58:11 +00:00
|
|
|
text{* A very rough formatting style could be modeled as follows:*}
|
|
|
|
|
2018-06-05 00:05:41 +00:00
|
|
|
|
|
|
|
datatype placement = h | t | b | ht | hb
|
2018-04-17 13:58:11 +00:00
|
|
|
doc_class figure = text_section +
|
2018-06-05 00:05:41 +00:00
|
|
|
relative_width :: "string" (* percent of textwidth *)
|
|
|
|
src :: "string"
|
|
|
|
placement :: placement
|
|
|
|
spawn_columns :: bool <= True
|
2018-04-17 13:58:11 +00:00
|
|
|
|
|
|
|
(* something similar on tables ? Idea: rough abstraction of table attributes in LaTeX *)
|
|
|
|
|
|
|
|
doc_class example = text_section +
|
|
|
|
comment :: "string"
|
2018-03-27 07:41:39 +00:00
|
|
|
|
2018-05-15 07:11:17 +00:00
|
|
|
doc_class "conclusion" = text_section +
|
2018-04-05 10:09:58 +00:00
|
|
|
main_author :: "author option" <= None
|
2018-03-28 07:24:27 +00:00
|
|
|
|
2018-05-15 07:11:17 +00:00
|
|
|
doc_class related_work = "conclusion" +
|
2018-04-05 10:09:58 +00:00
|
|
|
main_author :: "author option" <= None
|
2018-03-21 10:59:27 +00:00
|
|
|
|
|
|
|
doc_class bibliography =
|
2018-04-17 15:39:16 +00:00
|
|
|
style :: "string option" <= "Some ''LNCS''"
|
2018-03-21 10:59:27 +00:00
|
|
|
|
|
|
|
text{* Besides subtyping, there is another relation between
|
|
|
|
doc_classes: a class can be a \emph{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:
|
2018-05-21 09:16:20 +00:00
|
|
|
\<^item> monitor <doc-class>
|
|
|
|
\<^item> close_monitor <doc-class>
|
|
|
|
|
2018-03-21 10:59:27 +00:00
|
|
|
where the automaton of the monitor class is expected
|
|
|
|
to be in a final state.
|
|
|
|
|
|
|
|
Monitors can be nested.
|
|
|
|
|
|
|
|
Classes neither directly or via inheritance indirectly
|
|
|
|
mentioned in the monitor are \emph{independent} from
|
|
|
|
a monitor and may occur freely.
|
|
|
|
*}
|
|
|
|
|
|
|
|
|
2018-04-05 10:09:58 +00:00
|
|
|
-- \<open>underlying idea: capture the essence of a monitor class as trace.
|
2018-05-21 09:16:20 +00:00
|
|
|
trace would be `predefined id` like `main` in C. \<close>
|
2018-03-28 07:24:27 +00:00
|
|
|
text{* @{cite bla} *}
|
2018-03-21 10:59:27 +00:00
|
|
|
|
2018-04-05 10:09:58 +00:00
|
|
|
doc_class article =
|
2018-04-27 08:34:24 +00:00
|
|
|
style_id :: string <= "''LNCS''"
|
|
|
|
version :: "(int \<times> int \<times> int)" <= "(0,0,0)"
|
|
|
|
trace :: "(title + subtitle + author+ abstract +
|
|
|
|
introduction + technical + example +
|
|
|
|
conclusion + bibliography) list"
|
2018-05-21 09:16:20 +00:00
|
|
|
where "(title ~~
|
|
|
|
\<lbrakk>subtitle\<rbrakk> ~~
|
|
|
|
\<lbrace>author\<rbrace>\<^sup>+ ~~
|
|
|
|
abstract ~~
|
2018-05-11 13:51:26 +00:00
|
|
|
introduction ~~
|
|
|
|
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
|
2018-05-21 09:16:20 +00:00
|
|
|
conclusion ~~
|
2018-03-21 10:59:27 +00:00
|
|
|
bibliography)"
|
|
|
|
|
|
|
|
end
|
|
|
|
|