renaming ISA's; new shortcuts; more content in the RefMan.
This commit is contained in:
parent
b71be9c4a8
commit
aee1d33709
|
|
@ -616,7 +616,7 @@ be deadlocked after any non-terminating trace.
|
|||
\<^vs>\<open>-0.2cm\<close>\<close>
|
||||
|
||||
Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"]
|
||||
\<open> \hfill \break \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<^vs>\<open>-0.4cm\<close>\<close>
|
||||
\<open> \<^hf> \<^br> \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<^vs>\<open>-0.4cm\<close>\<close>
|
||||
|
||||
|
||||
Definition*[X11]\<open> \<open>livelock\<^sub>-free P \<equiv> \<D> P = {} \<close> \<^vs>\<open>-0.2cm\<close>\<close>
|
||||
|
|
@ -634,7 +634,7 @@ Finally, we proved the following theorem that confirms the relationship between
|
|||
properties:\<^vs>\<open>-0.3cm\<close>
|
||||
\<close>
|
||||
Theorem*[T2, short_name="''DF implies LF''"]
|
||||
\<open> \hspace{0.5cm} \<open>deadlock_free P \<longrightarrow> livelock_free P\<close> \<^vs>\<open>-0.3cm\<close>\<close>
|
||||
\<open> \<^hs>\<open>0.5cm\<close> \<open>deadlock_free P \<longrightarrow> livelock_free P\<close> \<^vs>\<open>-0.3cm\<close>\<close>
|
||||
|
||||
text\<open>
|
||||
This is totally natural, at a first glance, but surprising as the proof of deadlock-freeness only
|
||||
|
|
|
|||
|
|
@ -16,6 +16,7 @@ theory
|
|||
"03_GuidedTour"
|
||||
imports
|
||||
"02_Background"
|
||||
"Isabelle_DOF.technical_report"
|
||||
"Isabelle_DOF.CENELEC_50128"
|
||||
begin
|
||||
(*>*)
|
||||
|
|
|
|||
|
|
@ -508,45 +508,83 @@ ML\<open>writeln (DOF_core.print_doc_class_tree
|
|||
orelse String.isPrefix "Isa_COL" l)
|
||||
toLaTeX)\<close>
|
||||
(*>*)
|
||||
text\<open>The \<^verbatim>\<open>scholarly_paper\<close> ontology extends \<^verbatim>\<open>COL\<close> by the following concepts:
|
||||
text\<open> The \<^verbatim>\<open>scholarly_paper\<close> ontology is oriented towards the classical domains in science:
|
||||
\<^enum> mathematics
|
||||
\<^enum> informatics
|
||||
\<^enum> natural sciences
|
||||
\<^enum> technology and/or engineering
|
||||
|
||||
It extends \<^verbatim>\<open>COL\<close> by the following concepts:
|
||||
\begin{center}
|
||||
\begin{minipage}{.9\textwidth}
|
||||
\dirtree{%
|
||||
.0 .
|
||||
.1 scholarly\_paper.title.
|
||||
.1 scholarly\_paper.subtitle.
|
||||
.1 scholarly\_paper.author{An Author Entity Declaration}.
|
||||
.1 scholarly\_paper.author\DTcomment{An Author Entity Declaration}.
|
||||
.1 scholarly\_paper.abstract.
|
||||
.1 Isa\_COL.text\_element.
|
||||
.2 scholarly\_paper.text\_section{A Subclass for Major Paper Text-Elements}.
|
||||
.3 scholarly\_paper.introduction{...}.
|
||||
.3 scholarly\_paper.conclusion{...}.
|
||||
.4 scholarly\_paper.related\_work{...}.
|
||||
.3 scholarly\_paper.bibliography{...}.
|
||||
.3 scholarly\_paper.annex{...}.
|
||||
.3 scholarly\_paper.example{...}.
|
||||
.3 scholarly\_paper.technical{Freeform Class for Technical Content}.
|
||||
.4 scholarly\_paper.math\_content{...}.
|
||||
.5 scholarly\_paper.definition{Freeform}.
|
||||
.5 scholarly\_paper.lemma{Freeform}.
|
||||
.5 scholarly\_paper.theorem{Freeform}.
|
||||
.5 scholarly\_paper.corollary{Freeform}.
|
||||
.5 scholarly\_paper.math\_example{...}.
|
||||
.5 scholarly\_paper.math\_semiformal{...}.
|
||||
.4 scholarly\_paper.tech\_example{...}.
|
||||
.4 scholarly\_paper.math\_motivation{...}.
|
||||
.4 scholarly\_paper.math\_explanation{...}.
|
||||
.4 scholarly\_paper.engineering\_content{...}.
|
||||
.5 scholarly\_paper.data{...}.
|
||||
.5 scholarly\_paper.evaluation{...}.
|
||||
.5 scholarly\_paper.experiment{...}.
|
||||
.2 scholarly\_paper.text\_section\DTcomment{Major Paper Text-Elements}.
|
||||
.3 scholarly\_paper.introduction\DTcomment{...}.
|
||||
.3 scholarly\_paper.conclusion\DTcomment{...}.
|
||||
.4 scholarly\_paper.related\_work\DTcomment{...}.
|
||||
.3 scholarly\_paper.bibliography\DTcomment{...}.
|
||||
.3 scholarly\_paper.annex\DTcomment{...}.
|
||||
.3 scholarly\_paper.example\DTcomment{Example in General Sense}.
|
||||
.3 scholarly\_paper.technical\DTcomment{Root for Technical Content}.
|
||||
.4 scholarly\_paper.math\_content\DTcomment{...}.
|
||||
.5 scholarly\_paper.definition\DTcomment{Freeform}.
|
||||
.5 scholarly\_paper.lemma\DTcomment{Freeform}.
|
||||
.5 scholarly\_paper.theorem\DTcomment{Freeform}.
|
||||
.5 scholarly\_paper.corollary\DTcomment{Freeform}.
|
||||
.5 scholarly\_paper.math\_example\DTcomment{Freeform}.
|
||||
.5 scholarly\_paper.math\_semiformal\DTcomment{Freeform}.
|
||||
.4 scholarly\_paper.tech\_example\DTcomment{...}.
|
||||
.4 scholarly\_paper.math\_motivation\DTcomment{...}.
|
||||
.4 scholarly\_paper.math\_explanation\DTcomment{...}.
|
||||
.4 scholarly\_paper.engineering\_content\DTcomment{...}.
|
||||
.5 scholarly\_paper.data.
|
||||
.5 scholarly\_paper.evaluation.
|
||||
.5 scholarly\_paper.experiment.
|
||||
.4 ...
|
||||
.1 ...
|
||||
.1 scholarly\_paper.article{The Paper Monitor}.
|
||||
.1 scholarly\_paper.article\DTcomment{The Paper Monitor}.
|
||||
.1 \ldots.
|
||||
}
|
||||
\end{minipage}
|
||||
\end{center}
|
||||
|
||||
\<close>
|
||||
|
||||
text\<open>A pivotal abstract class in the hierarchy is:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>
|
||||
doc_class text_section = text_element +
|
||||
main_author :: "author option" <= None
|
||||
fixme_list :: "string list" <= "[]"
|
||||
level :: "int option" <= "None"
|
||||
\<close>}
|
||||
|
||||
Besides attributes of more practical considerations like a fixme-list, that can be modified during
|
||||
the editing process but is only visible in the integrated source but usually ignored in the
|
||||
\<^LaTeX>, this class also introduces the possibility to assign an "ownership" or "responsibility" of
|
||||
a text-element to a specific author. Note that this is possible since \<^isadof> assigns to each
|
||||
document class also a class-type which is declared in the HOL environment.\<close>
|
||||
|
||||
(*<*)
|
||||
declare_reference*["text-elements-expls"::example]
|
||||
(*>*)
|
||||
text*[s23::example, main_author = "Some(@{docitem \<open>bu\<close>}::author)"]\<open>
|
||||
Recall that concrete authors can be denoted by term-antiquotations generated by \<^isadof>; for example,
|
||||
this may be for a text fragment like
|
||||
@{boxed_theory_text [display]
|
||||
\<open>text*[\<dots>::example, main_author = "Some(@{docitem ''bu''}::author)"] \<open>\<open>\<close> \<dots> \<open>\<close>\<close>\<close>}
|
||||
or
|
||||
@{boxed_theory_text [display]
|
||||
\<open>text*[\<dots>::example, main_author = "Some(@{docitem \<open>bu\<close>}::author)"] \<open>\<open>\<close> \<dots> \<open>\<close>\<close>\<close>}
|
||||
|
||||
where \<^boxed_theory_text>\<open>"''bu''"\<close> is a string presentation of the reference to the author
|
||||
text element (see below in @{docitem (unchecked) \<open>text-elements-expls\<close>}).
|
||||
\<close>
|
||||
|
||||
text\<open>Some of these concepts were supported as command-abbreviations leading to the extension
|
||||
|
|
@ -564,7 +602,19 @@ of the \<^isadof> language:
|
|||
\<close>
|
||||
\<close>
|
||||
|
||||
subsubsection*["text-elements-expls"::technical]\<open>Examples\<close>
|
||||
text\<open>Usually, command macros for text elements will assign to the default class corresponding for this
|
||||
class. For pragmatic reasons, \<^theory_text>\<open>Definition*\<close>, \<^theory_text>\<open>Lemma*\<close> and \<^theory_text>\<open>Theorem*\<close> represent an exception
|
||||
of this rule and are set up such that the default class is the super class @{typ \<open>math_content\<close>}
|
||||
(rather than to the class @{typ \<open>definition\<close>}).
|
||||
This way, it is possible to use these macros for several different sorts of the very generic
|
||||
concept "definition", which can be used as a freeform mathematical definition but also for a
|
||||
freeform terminological definition as used in certification standards. Moreover, new subclasses
|
||||
of @{typ \<open>math_content\<close>} might be introduced in a derived ontology with an own specific layout
|
||||
definition.
|
||||
\<close>
|
||||
|
||||
|
||||
subsubsection*["text-elements-expls"::example]\<open>Examples\<close>
|
||||
|
||||
text\<open>
|
||||
While the default user interface for class definitions via the
|
||||
|
|
@ -572,7 +622,6 @@ text\<open>
|
|||
class, \<^isadof> provides short-hands for certain, widely-used, concepts such as
|
||||
\<^boxed_theory_text>\<open>title*\<open> ... \<close>\<close> or \<^boxed_theory_text>\<open>section*\<open> ... \<close>\<close>, \<^eg>:
|
||||
|
||||
|
||||
@{boxed_theory_text [display]\<open>
|
||||
title*[title::title]\<open>Isabelle/DOF\<close>
|
||||
subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<close>
|
||||
|
|
@ -583,54 +632,29 @@ text\<open>
|
|||
affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>
|
||||
\<close>}
|
||||
|
||||
In general, all standard text-elements from the Isabelle document model such
|
||||
as \<^theory_text>\<open>chapter\<close>, \<^theory_text>\<open>section\<close>, \<^theory_text>\<open>text\<close>, have in the \<^isadof>
|
||||
implementation their counterparts in the family of text-elements that are ontology-aware,
|
||||
\<^ie>, they dispose on a meta-argument list that allows to define that a test-element
|
||||
that has an identity as a text-object labelled as \<open>obj_id\<close>, belongs to a document class
|
||||
\<open>class_id\<close> that has been defined earlier, and has its class-attributes set with particular
|
||||
values (which are denotable in Isabelle/HOL mathematical term syntax).
|
||||
\<^item> \<open>annotated_text_element\<close> :
|
||||
\<^rail>\<open>
|
||||
( ( @@{command "title*"}
|
||||
| @@{command "subtitle*"}
|
||||
| @@{command "author*"}
|
||||
| @@{command "abstract*"})
|
||||
\<newline>
|
||||
'[' meta_args ']' '\<open>' text '\<close>'
|
||||
)
|
||||
\<close>
|
||||
\<close>
|
||||
|
||||
text\<open>
|
||||
As mentioned before, the command macros of \<^theory_text>\<open>Definition*\<close>, \<^theory_text>\<open>Lemma*\<close> and \<^theory_text>\<open>Theorem*\<close>
|
||||
set the default class to the super-class of @{typ \<open>definition\<close>}.
|
||||
However, in order to avoid the somewhat tedious consequence:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>Theorem*[T1::"theorem", short_name="\<open>DF definition captures deadlock-freeness\<close>"] \<open>\<open>\<close> \<dots> \<open>\<close>\<close>\<close>}
|
||||
|
||||
the choice of the default class can be influenced by setting globally an attribute such as
|
||||
@{boxed_theory_text [display]
|
||||
\<open>declare[[ Definition_default_class = "definition"]]
|
||||
declare[[ Theorem_default_class = "theorem"]]
|
||||
\<close>}
|
||||
|
||||
which allows the above example be shortened to:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"] \<open>\<open>\<close> \<dots> \<open>\<close>\<close>
|
||||
\<close>}
|
||||
\<close>
|
||||
|
||||
|
||||
text\<open>\<^isadof> uses the concept of implicit abstract classes (or: \<^emph>\<open>shadow classes\<close>).
|
||||
These refer to the set of possible \<^boxed_theory_text>\<open>doc_class\<close> declarations that posses a number
|
||||
of attributes with their types in common. Shadow classes represent an implicit requirement
|
||||
(or pre-condition) on a given class to posses these attributes in order to work properly
|
||||
for certain \<^isadof> commands.
|
||||
|
||||
shadow classes will find concrete instances in COL, but \<^isadof> text elements do not \<^emph>\<open>depend\<close>
|
||||
on our COL definitions: Ontology developers are free to build own class instances for these
|
||||
shadow classes, with own attributes and, last not least, own definitions of invariants independent
|
||||
from ours.
|
||||
|
||||
In particular, these shadow classes are used at present in \<^isadof>:
|
||||
@{boxed_theory_text [display]\<open>
|
||||
DOCUMENT_ALIKES =
|
||||
level :: "int option" <= "None"
|
||||
|
||||
ASSERTION_ALIKES =
|
||||
properties :: "term list"
|
||||
|
||||
FORMAL_STATEMENT_ALIKE =
|
||||
properties :: "thm list"
|
||||
\<close>}
|
||||
|
||||
These shadow-classes correspond to semantic macros
|
||||
\<^ML>\<open>Onto_Macros.enriched_document_cmd_exp\<close>,
|
||||
\<^ML>\<open>Onto_Macros.assertion_cmd'\<close>, and
|
||||
\<^ML>\<open>Onto_Macros.enriched_formal_statement_command\<close>.\<close>
|
||||
|
||||
subsection\<open>ASSERTIONS : NEED TO BE INTEGRATED. TODO.\<close>
|
||||
|
||||
text\<open>
|
||||
Similarly, we provide "minimal" instances of the \<^boxed_theory_text>\<open>ASSERTION_ALIKES\<close>
|
||||
|
|
@ -642,12 +666,41 @@ doc_class assertions =
|
|||
doc_class "thms" =
|
||||
properties :: "thm list"
|
||||
\<close>}
|
||||
|
||||
\<close>
|
||||
|
||||
|
||||
subsection\<open>The Ontology \<^theory>\<open>Isabelle_DOF.technical_report\<close>\<close>
|
||||
(*<*)
|
||||
ML\<open>val toLaTeX = String.translate (fn c => if c = #"_" then "\\_" else String.implode[c])\<close>
|
||||
ML\<open>writeln (DOF_core.print_doc_class_tree
|
||||
@{context} (fn (n,l) => String.isPrefix "technical_report" l
|
||||
orelse String.isPrefix "Isa_COL" l)
|
||||
toLaTeX)\<close>
|
||||
(*>*)
|
||||
text\<open> The \<^verbatim>\<open>technical_report\<close> ontology extends \<^verbatim>\<open>scholarly_paper\<close> by concepts needed
|
||||
for larger reports in the domain of mathematics and engineering.
|
||||
|
||||
%
|
||||
\begin{center}
|
||||
\begin{minipage}{.9\textwidth}
|
||||
\dirtree{%
|
||||
.0 .
|
||||
.1 technical\_report.front\_matter\DTcomment{...}.
|
||||
.1 technical\_report.table\_of\_contents\DTcomment{...}.
|
||||
.1 technical\_report.index\DTcomment{...}.
|
||||
.1 ...
|
||||
.1 technical\_report.report\DTcomment{...}.
|
||||
}
|
||||
\end{minipage}
|
||||
\end{center}
|
||||
\<close>
|
||||
|
||||
|
||||
subsection\<open>A Domain-Specific Ontology: \<^theory>\<open>Isabelle_DOF.CENELEC_50128\<close>\<close>
|
||||
|
||||
|
||||
|
||||
subsubsection\<open>Example: Text Elemens with Levels\<close>
|
||||
text\<open>
|
||||
The category ``exported constraint (EC)'' is, in the file
|
||||
|
|
|
|||
|
|
@ -521,7 +521,8 @@ define_macro* hs2 \<rightleftharpoons> \<open>\hspace{\<close> _ \<open>}\<close
|
|||
(*>*)
|
||||
|
||||
define_shortcut* clearpage \<rightleftharpoons> \<open>\clearpage{}\<close>
|
||||
|
||||
hf \<rightleftharpoons> \<open>\hfill\<close>
|
||||
br \<rightleftharpoons> \<open>\break\<close>
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ doc_class index =
|
|||
section\<open>Code Statement Elements\<close>
|
||||
|
||||
doc_class "code" = technical +
|
||||
checked :: bool <= "False"
|
||||
checked :: bool <= "False"
|
||||
caption :: "string" <= "''''"
|
||||
|
||||
|
||||
|
|
@ -79,251 +79,3 @@ doc_class report =
|
|||
|
||||
|
||||
end
|
||||
|
||||
(*
|
||||
=====================================
|
||||
docclass: Isa_COL.thms
|
||||
name: "thms"
|
||||
origin: Isa_COL
|
||||
attrs: "properties"
|
||||
invs:
|
||||
docclass: Isa_COL.figure
|
||||
name: "figure"
|
||||
origin: Isa_COL
|
||||
attrs: "relative_width", "src", "placement", "spawn_columns"(True)
|
||||
invs:
|
||||
docclass: Isa_COL.chapter = Isa_COL.text_element +
|
||||
name: "chapter"
|
||||
origin: Isa_COL
|
||||
attrs: "level"(Some 0)
|
||||
invs:
|
||||
docclass: Isa_COL.concept
|
||||
name: "concept"
|
||||
origin: Isa_COL
|
||||
attrs: "tag"([]), "properties"([])
|
||||
invs:
|
||||
docclass: Isa_COL.section = Isa_COL.text_element +
|
||||
name: "section"
|
||||
origin: Isa_COL
|
||||
attrs: "level"(Some 1)
|
||||
invs:
|
||||
docclass: Isa_COL.assertions
|
||||
name: "assertions"
|
||||
origin: Isa_COL
|
||||
attrs: "properties"
|
||||
invs:
|
||||
docclass: Isa_COL.subsection = Isa_COL.text_element +
|
||||
name: "subsection"
|
||||
origin: Isa_COL
|
||||
attrs: "level"(Some 2)
|
||||
invs:
|
||||
docclass: Isa_COL.definitions
|
||||
name: "definitions"
|
||||
origin: Isa_COL
|
||||
attrs: "requires", "establishes"
|
||||
invs:
|
||||
docclass: Isa_COL.formal_item
|
||||
name: "formal_item"
|
||||
origin: Isa_COL
|
||||
attrs: "item"
|
||||
invs:
|
||||
docclass: Isa_COL.figure_group
|
||||
name: "figure_group"
|
||||
origin: Isa_COL
|
||||
attrs: "trace"([]), "caption"
|
||||
invs:
|
||||
docclass: Isa_COL.text_element
|
||||
name: "text_element"
|
||||
origin: Isa_COL
|
||||
attrs: "level"(None), "referentiable"(False), "variants"({STR ''outline'', STR ''document''})
|
||||
invs:
|
||||
docclass: scholarly_paper.data = scholarly_paper.engineering_content +
|
||||
name: "data"
|
||||
origin: scholarly_paper
|
||||
attrs: "tag"([])
|
||||
invs:
|
||||
docclass: technical_report.SML = technical_report.code +
|
||||
name: "SML"
|
||||
origin: technical_report
|
||||
attrs: "checked"(False)
|
||||
invs:
|
||||
docclass: Isa_COL.subsubsection = Isa_COL.text_element +
|
||||
name: "subsubsection"
|
||||
origin: Isa_COL
|
||||
attrs: "level"(Some 3)
|
||||
invs:
|
||||
docclass: scholarly_paper.annex = scholarly_paper.text_section +
|
||||
name: "annex"
|
||||
origin: scholarly_paper
|
||||
attrs: "main_author"(None)
|
||||
invs:
|
||||
docclass: scholarly_paper.lemma = scholarly_paper.math_content +
|
||||
name: "lemma"
|
||||
origin: scholarly_paper
|
||||
attrs: "referentiable"(True), "mcc"(lem)
|
||||
invs: d3::\<lambda>\<sigma>. lemma.mcc \<sigma> = lem
|
||||
docclass: scholarly_paper.title
|
||||
name: "title"
|
||||
origin: scholarly_paper
|
||||
attrs: "short_title"(None)
|
||||
invs:
|
||||
docclass: technical_report.ISAR = technical_report.code +
|
||||
name: "ISAR"
|
||||
origin: technical_report
|
||||
attrs: "checked"(False)
|
||||
invs:
|
||||
docclass: technical_report.code = scholarly_paper.technical +
|
||||
name: "code"
|
||||
origin: technical_report
|
||||
attrs: "checked"(False), "label"([])
|
||||
invs:
|
||||
docclass: Isa_COL.formal_content
|
||||
name: "formal_content"
|
||||
origin: Isa_COL
|
||||
attrs: "trace"([]), "style"
|
||||
invs:
|
||||
docclass: scholarly_paper.author
|
||||
name: "author"
|
||||
origin: scholarly_paper
|
||||
attrs: "email"([]), "http_site"([]), "orcid"([]), "affiliation"
|
||||
invs:
|
||||
docclass: technical_report.LATEX = technical_report.code +
|
||||
name: "LATEX"
|
||||
origin: technical_report
|
||||
attrs: "checked"(False)
|
||||
invs:
|
||||
docclass: technical_report.index
|
||||
name: "index"
|
||||
origin: technical_report
|
||||
attrs: "kind", "level"
|
||||
invs:
|
||||
docclass: scholarly_paper.article
|
||||
name: "article"
|
||||
origin: scholarly_paper
|
||||
attrs: "trace"([]), "style_id"(''LNCS''), "version"((0, 0, 0))
|
||||
invs:
|
||||
docclass: scholarly_paper.example = scholarly_paper.text_section +
|
||||
name: "example"
|
||||
origin: scholarly_paper
|
||||
attrs: "referentiable"(True), "status"(description), "short_name"([])
|
||||
invs:
|
||||
docclass: scholarly_paper.theorem = scholarly_paper.math_content +
|
||||
name: "theorem"
|
||||
origin: scholarly_paper
|
||||
attrs: "referentiable"(True), "mcc"(thm)
|
||||
invs: d2::\<lambda>\<sigma>. theorem.mcc \<sigma> = thm
|
||||
docclass: scholarly_paper.abstract
|
||||
name: "abstract"
|
||||
origin: scholarly_paper
|
||||
attrs: "keywordlist"([]), "principal_theorems"
|
||||
invs:
|
||||
docclass: scholarly_paper.subtitle
|
||||
name: "subtitle"
|
||||
origin: scholarly_paper
|
||||
attrs: "abbrev"(None)
|
||||
invs:
|
||||
docclass: scholarly_paper.corollary = scholarly_paper.math_content +
|
||||
name: "corollary"
|
||||
origin: scholarly_paper
|
||||
attrs: "referentiable"(True), "mcc"(cor)
|
||||
invs: d4::\<lambda>\<sigma>. corollary.mcc \<sigma> = thm
|
||||
docclass: scholarly_paper.technical = scholarly_paper.text_section +
|
||||
name: "technical"
|
||||
origin: scholarly_paper
|
||||
attrs: "definition_list"([]), "status"(description), "formal_results"
|
||||
invs: L1::\<lambda>\<sigma>. 0 < the (text_section.level \<sigma>)
|
||||
docclass: scholarly_paper.conclusion = scholarly_paper.text_section +
|
||||
name: "conclusion"
|
||||
origin: scholarly_paper
|
||||
attrs: "main_author"(None)
|
||||
invs:
|
||||
docclass: scholarly_paper.definition = scholarly_paper.math_content +
|
||||
name: "definition"
|
||||
origin: scholarly_paper
|
||||
attrs: "referentiable"(True), "mcc"(defn)
|
||||
invs: d1::\<lambda>\<sigma>. definition.mcc \<sigma> = defn
|
||||
docclass: scholarly_paper.evaluation = scholarly_paper.engineering_content +
|
||||
name: "evaluation"
|
||||
origin: scholarly_paper
|
||||
attrs: "tag"([])
|
||||
invs:
|
||||
docclass: scholarly_paper.experiment = scholarly_paper.engineering_content +
|
||||
name: "experiment"
|
||||
origin: scholarly_paper
|
||||
attrs: "tag"([])
|
||||
invs:
|
||||
docclass: Isa_COL.side_by_side_figure = Isa_COL.figure +
|
||||
name: "side_by_side_figure"
|
||||
origin: Isa_COL
|
||||
attrs: "anchor", "caption", "relative_width2", "src2", "anchor2", "caption2"
|
||||
invs:
|
||||
docclass: scholarly_paper.bibliography = scholarly_paper.text_section +
|
||||
name: "bibliography"
|
||||
origin: scholarly_paper
|
||||
attrs: "style"(Some ''LNCS'')
|
||||
invs:
|
||||
docclass: scholarly_paper.introduction = scholarly_paper.text_section +
|
||||
name: "introduction"
|
||||
origin: scholarly_paper
|
||||
attrs: "comment", "claims"
|
||||
invs:
|
||||
docclass: scholarly_paper.math_content = scholarly_paper.technical +
|
||||
name: "math_content"
|
||||
origin: scholarly_paper
|
||||
attrs: "referentiable"(True), "short_name"([]), "status"(semiformal), "mcc"(thm)
|
||||
invs: s1::\<lambda>\<sigma>. \<not> math_content.referentiable \<sigma> \<longrightarrow>
|
||||
math_content.short_name \<sigma> = [], s2::\<lambda>\<sigma>. math_content.status \<sigma> = semiformal
|
||||
docclass: scholarly_paper.math_example = scholarly_paper.math_content +
|
||||
name: "math_example"
|
||||
origin: scholarly_paper
|
||||
attrs: "referentiable"(True), "mcc"(expl)
|
||||
invs: d5::\<lambda>\<sigma>. math_example.mcc \<sigma> = expl
|
||||
docclass: scholarly_paper.related_work = scholarly_paper.conclusion +
|
||||
name: "related_work"
|
||||
origin: scholarly_paper
|
||||
attrs: "main_author"(None)
|
||||
invs:
|
||||
docclass: scholarly_paper.tech_example = scholarly_paper.technical +
|
||||
name: "tech_example"
|
||||
origin: scholarly_paper
|
||||
attrs: "referentiable"(True), "tag"([])
|
||||
invs:
|
||||
docclass: scholarly_paper.text_section = Isa_COL.text_element +
|
||||
name: "text_section"
|
||||
origin: scholarly_paper
|
||||
attrs: "main_author"(None), "fixme_list"([]), "level"(None)
|
||||
invs:
|
||||
docclass: technical_report.front_matter
|
||||
name: "front_matter"
|
||||
origin: technical_report
|
||||
attrs: "front_matter_style"
|
||||
invs:
|
||||
docclass: scholarly_paper.math_motivation = scholarly_paper.technical +
|
||||
name: "math_motivation"
|
||||
origin: scholarly_paper
|
||||
attrs: "referentiable"(False)
|
||||
invs:
|
||||
docclass: scholarly_paper.math_semiformal = scholarly_paper.math_content +
|
||||
name: "math_semiformal"
|
||||
origin: scholarly_paper
|
||||
attrs: "referentiable"(True)
|
||||
invs:
|
||||
docclass: scholarly_paper.math_explanation = scholarly_paper.technical +
|
||||
name: "math_explanation"
|
||||
origin: scholarly_paper
|
||||
attrs: "referentiable"(False)
|
||||
invs:
|
||||
docclass: technical_report.table_of_contents
|
||||
name: "table_of_contents"
|
||||
origin: technical_report
|
||||
attrs: "bookmark_depth"(3), "depth"(3)
|
||||
invs:
|
||||
docclass: scholarly_paper.engineering_content = scholarly_paper.technical +
|
||||
name: "engineering_content"
|
||||
origin: scholarly_paper
|
||||
attrs: "short_name"([]), "status"
|
||||
invs:
|
||||
=====================================
|
||||
|
||||
|
||||
*)
|
||||
|
|
|
|||
|
|
@ -4,5 +4,5 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" +
|
|||
"AssnsLemmaThmEtc"
|
||||
"Concept_ExampleInvariant"
|
||||
"Concept_Example"
|
||||
"InnerSyntaxAntiquotations"
|
||||
"TermAntiquotations"
|
||||
"Attributes"
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ For historical reasons, \<^emph>\<open>term antiquotations\<close> are called th
|
|||
"Inner Syntax Antiquotations". \<close>
|
||||
|
||||
theory
|
||||
InnerSyntaxAntiquotations
|
||||
TermAntiquotations
|
||||
imports
|
||||
"Isabelle_DOF.Conceptual"
|
||||
begin
|
||||
|
|
@ -50,7 +50,7 @@ text\<open>Some sample lemma:\<close>
|
|||
lemma murks : "Example=Example" by simp
|
||||
|
||||
text\<open>Example for a meta-attribute of ODL-type @{typ "file"} with an appropriate ISA for the
|
||||
file @{file "InnerSyntaxAntiquotations.thy"}\<close>
|
||||
file @{file "TermAntiquotations.thy"}\<close>
|
||||
(* not working:
|
||||
text*[xcv::F, u="@{file ''InnerSyntaxAntiquotations.thy''}"]\<open>Lorem ipsum ...\<close>
|
||||
*)
|
||||
|
|
@ -65,7 +65,7 @@ text*[xcv2::C, g="@{thm ''HOL.refl''}"]\<open>Lorem ipsum ...\<close>
|
|||
text\<open>Major sample: test-item of doc-class \<open>F\<close> with a relational link between class instances,
|
||||
and links to formal Isabelle items like \<open>typ\<close>, \<open>term\<close> and \<open>thm\<close>. \<close>
|
||||
text*[xcv4::F, r="[@{thm ''HOL.refl''},
|
||||
@{thm \<open>InnerSyntaxAntiquotations.murks\<close>}]", (* long names required *)
|
||||
@{thm \<open>TermAntiquotations.murks\<close>}]", (* long names required *)
|
||||
b="{(@{docitem ''xcv1''},@{docitem \<open>xcv2\<close>})}", (* notations \<open>...\<close> vs. ''...'' *)
|
||||
s="[@{typ \<open>int list\<close>}]",
|
||||
properties = "[@{term \<open>H \<longrightarrow> H\<close>}]" (* notation \<open>...\<close> required for UTF8*)
|
||||
Loading…
Reference in New Issue