Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Merge and upgrade to development version of Isabelle/HOL.
ci/woodpecker/push/build Pipeline failed Details

This commit is contained in:
Achim D. Brucker 2023-04-24 22:26:39 +01:00
parent 480272ad86 f906d45d48
commit 0d74645d2e
25 changed files with 492 additions and 368 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Isabelle_DOF-Example-II/paper.thy
View File

@ -751,7 +751,7 @@ This normal form is closed under deterministic and communication operators.
The advantage of this format is that we can mimick the well-known product automata construction
for an arbitrary number of synchronized processes under normal form.
We only show the case of the synchronous product of two processes: \<close>
text*[T3::"theorem", short_name="\<open>Product Construction\<close>", level="Some 2"]\<open>
Theorem*[T3, short_name="\<open>Product Construction\<close>", level="Some 2"]\<open>
Parallel composition translates to normal form:
@{cartouche [display,indent=5]\<open>(P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>1,\<upsilon>\<^sub>1\<rbrakk> \<sigma>\<^sub>1) || (P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>2,\<upsilon>\<^sub>2\<rbrakk> \<sigma>\<^sub>2) =
P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2). \<tau>\<^sub>1 \<sigma>\<^sub>1 \<inter> \<tau>\<^sub>2 \<sigma>\<^sub>2 , \<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2).\<lambda>e.(\<upsilon>\<^sub>1 \<sigma>\<^sub>1 e, \<upsilon>\<^sub>2 \<sigma>\<^sub>2 e)\<rbrakk> (\<sigma>\<^sub>1,\<sigma>\<^sub>2)\<close>}

5
Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
View File

@ -347,7 +347,7 @@ text\<open>
\<^item> \<^ML>\<open>Context.proper_subthy : theory * theory -> bool\<close> subcontext test
\<^item> \<^ML>\<open>Context.Proof: Proof.context -> Context.generic \<close> A constructor embedding local contexts
\<^item> \<^ML>\<open>Context.proof_of : Context.generic -> Proof.context\<close> the inverse
\<^item> \<^ML>\<open>Context.theory_name : theory -> string\<close>
\<^item> \<^ML>\<open>Context.theory_name : {long:bool} -> theory -> string\<close>
\<^item> \<^ML>\<open>Context.map_theory: (theory -> theory) -> Context.generic -> Context.generic\<close>
\<close>
@ -358,7 +358,7 @@ text\<open>The structure \<^ML_structure>\<open>Proof_Context\<close> provides a
\<^item> \<^ML>\<open> Context.Proof: Proof.context -> Context.generic \<close>
the path to a generic Context, i.e. a sum-type of global and local contexts
in order to simplify system interfaces
\<^item> \<^ML>\<open> Proof_Context.get_global: theory -> string -> Proof.context\<close>
\<^item> \<^ML>\<open> Proof_Context.get_global: {long:bool} -> theory -> string -> Proof.context\<close>
\<close>
@ -891,7 +891,6 @@ datatype thy = Thy of
\<^item> \<^ML>\<open>Theory.axiom_space: theory -> Name_Space.T\<close>
\<^item> \<^ML>\<open>Theory.all_axioms_of: theory -> (string * term) list\<close>
\<^item> \<^ML>\<open>Theory.defs_of: theory -> Defs.T\<close>
\<^item> \<^ML>\<open>Theory.join_theory: theory list -> theory\<close>
\<^item> \<^ML>\<open>Theory.at_begin: (theory -> theory option) -> theory -> theory\<close>
\<^item> \<^ML>\<open>Theory.at_end: (theory -> theory option) -> theory -> theory\<close>
\<^item> \<^ML>\<open>Theory.begin_theory: string * Position.T -> theory list -> theory\<close>

36
Isabelle_DOF-Ontologies/CC_v3_1_R5/DOF-CC_terminology.sty
View File

@ -23,35 +23,35 @@
\newkeycommand*{\mathcc}[label=,type=%
, scholarly_paper.math_content.short_name ={}%
, scholarly_paper.math_content.mcc = %
, Isa_COL.text_element.level =%
, Isa_COL.text_element.referentiable =%
, Isa_COL.text_element.variants =%
, scholarly_paper.text_section.main_author =%
, scholarly_paper.text_section.fixme_list =%
, Isa_COL.text_element.level =%
, scholarly_paper.technical.definition_list =%
, scholarly_paper.technical.status =%
, CC_terminology.concept_definition.tag=%
, CC_terminology.concept_definition.short_tag=%
, scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname ={}%
, scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc = %
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel =%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable =%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants =%
, scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTmainUNDERSCOREauthor =%
, scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTfixmeUNDERSCORElist =%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel =%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTdefinitionUNDERSCORElist =%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTstatus =%
, CCUNDERSCOREterminologyDOTconceptUNDERSCOREdefinitionDOTtag=%
, CCUNDERSCOREterminologyDOTconceptUNDERSCOREdefinitionDOTshortUNDERSCOREtag=%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
\ifthenelse{\equal{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname}} {} }
{%
\begin{\commandkey{scholarly_paper.math_content.mcc}}\label{\commandkey{label}}
\begin{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}\label{\commandkey{label}}
#1
\end{\commandkey{scholarly_paper.math_content.mcc}}
\end{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}
}{%
\begin{\commandkey{scholarly_paper.math_content.mcc}}[\commandkey{scholarly_paper.math_content.short_name}]\label{\commandkey{label}}
\begin{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}[\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname}]\label{\commandkey{label}}
#1
\end{\commandkey{scholarly_paper.math_content.mcc}}
\end{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}
}
\end{isamarkuptext}%
}
\expandafter\def\csname isaDof.text.scholarly_paper.math_content\endcsname{\mathcc}
\expandafter\def\csname isaDofDOTtextDOTscholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent\endcsname{\mathcc}

104
Isabelle_DOF-Ontologies/CENELEC_50128/DOF-CENELEC_50128.sty
View File

@ -60,26 +60,26 @@
}
\newcommand{\SRACautorefname}{SRAC}
\newisadof{text.CENELEC_50128.SRAC}%
\newisadof{textDOTCENELECUNDERSCORE50128DOTSRAC}%
[label=,type=%
,Isa_COL.text_element.level=%
,Isa_COL.text_element.referentiable=%
,Isa_COL.text_element.variants=%
,CENELEC_50128.requirement.is_concerned=%
,CENELEC_50128.requirement.long_name=%
,CENELEC_50128.SRAC.formal_repr=%
,CENELEC_50128.SRAC.assumption_kind=%
,CENELEC_50128.EC.assumption_kind=%
,CENELEC_50128.assumption.assumption_kind=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
,CENELECUNDERSCORE50128DOTrequirementDOTisUNDERSCOREconcerned=%
,CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname=%
,CENELECUNDERSCORE50128DOTSRACDOTformalUNDERSCORErepr=%
,CENELECUNDERSCORE50128DOTSRACDOTassumptionUNDERSCOREkind=%
,CENELECUNDERSCORE50128DOTECDOTassumptionUNDERSCOREkind=%
,CENELECUNDERSCORE50128DOTassumptionDOTassumptionUNDERSCOREkind=%
][1]{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%
\ifthenelse{\equal{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}{}}{%
\begin{SRAC}%
\addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}}%
}{%
\begin{SRAC}[\commandkey{CENELEC_50128.requirement.long_name}]%
\addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}: \commandkey{CENELEC_50128.requirement.long_name}}%
\DOFindex{SRAC}{\commandkey{CENELEC_50128.requirement.long_name}}%
\begin{SRAC}[\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}]%
\addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}: \commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
\DOFindex{SRAC}{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
}\label{\commandkey{label}}%
#1%
\end{SRAC}
@ -113,26 +113,26 @@
}
\newcommand{\ECautorefname}{EC}
\newisadof{text.CENELEC_50128.EC}%
\newisadof{textDOTCENELECUNDERSCORE50128DOTEC}%
[label=,type=%
,Isa_COL.text_element.level=%
,Isa_COL.text_element.referentiable=%
,Isa_COL.text_element.variants=%
,CENELEC_50128.requirement.is_concerned=%
,CENELEC_50128.requirement.long_name=%
,CENELEC_50128.SRAC.formal_repr=%
,CENELEC_50128.SRAC.assumption_kind=%
,CENELEC_50128.EC.assumption_kind=%
,CENELEC_50128.assumption.assumption_kind=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
,CENELECUNDERSCORE50128DOTrequirementDOTisUNDERSCOREconcerned=%
,CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname=%
,CENELECUNDERSCORE50128DOTSRACDOTformalUNDERSCORErepr=%
,CENELECUNDERSCORE50128DOTSRACDOTassumptionUNDERSCOREkind=%
,CENELECUNDERSCORE50128DOTECDOTassumptionUNDERSCOREkind=%
,CENELECUNDERSCORE50128DOTassumptionDOTassumptionUNDERSCOREkind=%
][1]{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%
\ifthenelse{\equal{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}{}}{%
\begin{EC}%
\addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}}%
}{%
\begin{EC}[\commandkey{CENELEC_50128.requirement.long_name}]%
\addxcontentsline{toe}{chapter}[]{\autoref{\commandkey{label}}: \commandkey{CENELEC_50128.requirement.long_name}}%
\DOFindex{EC}{\commandkey{CENELEC_50128.requirement.long_name}}%
\begin{EC}[\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}]%
\addxcontentsline{toe}{chapter}[]{\autoref{\commandkey{label}}: \commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
\DOFindex{EC}{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
}\label{\commandkey{label}}%
#1%
\end{EC}
@ -155,23 +155,23 @@
}
\newcommand{\assumptionautorefname}{assumption}
\newisadof{text.CENELEC_50128.assumption}%
\newisadof{textDOTCENELECUNDERSCORE50128DOTassumption}%
[label=,type=%
,Isa_COL.text_element.level=%
,Isa_COL.text_element.referentiable=%
,Isa_COL.text_element.variants=%
,CENELEC_50128.requirement.is_concerned=%
,CENELEC_50128.requirement.long_name=%
,CENELEC_50128.SRAC.formal_repr=%
,CENELEC_50128.SRAC.assumption_kind=%
,CENELEC_50128.assumption.assumption_kind=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
,CENELECUNDERSCORE50128DOTrequirementDOTisUNDERSCOREconcerned=%
,CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname=%
,CENELECUNDERSCORE50128DOTSRACDOTformalUNDERSCORErepr=%
,CENELECUNDERSCORE50128DOTSRACDOTassumptionUNDERSCOREkind=%
,CENELECUNDERSCORE50128DOTassumptionDOTassumptionUNDERSCOREkind=%
][1]{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%
\ifthenelse{\equal{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}{}}{%
\begin{assumption}%
}{%
\begin{assumption}[\commandkey{CENELEC_50128.requirement.long_name}]%
\DOFindex{assumption}{\commandkey{CENELEC_50128.requirement.long_name}}%
\begin{assumption}[\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}]%
\DOFindex{assumption}{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
}\label{\commandkey{label}}%
#1%
\end{assumption}
@ -196,23 +196,23 @@
\newcommand{\hypothesisautorefname}{hypothesis}
\newisadof{text.CENELEC_50128.hypothesis}%
\newisadof{textDOTCENELECUNDERSCORE50128DOThypothesis}%
[label=,type=%
,Isa_COL.text_element.level=%
,Isa_COL.text_element.referentiable=%
,Isa_COL.text_element.variants=%
,CENELEC_50128.requirement.is_concerned=%
,CENELEC_50128.requirement.long_name=%
,CENELEC_50128.SRAC.formal_repr=%
,CENELEC_50128.SRAC.hypothesis_kind=%
,CENELEC_50128.hypothesis.hyp_type=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
,CENELECUNDERSCORE50128DOTrequirementDOTisUNDERSCOREconcerned=%
,CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname=%
,CENELECUNDERSCORE50128DOTSRACDOTformalUNDERSCORErepr=%
,CENELECUNDERSCORE50128DOTSRACDOThypothesisUNDERSCOREkind=%
,CENELECUNDERSCORE50128DOThypothesisDOThypUNDERSCOREtype=%
][1]{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%
\ifthenelse{\equal{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}{}}{%
\begin{hypothesis}%
}{%
\begin{hypothesis}[\commandkey{CENELEC_50128.requirement.long_name}]%
\DOFindex{hypothesis}{\commandkey{CENELEC_50128.requirement.long_name}}%
\begin{hypothesis}[\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}]%
\DOFindex{hypothesis}{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
}\label{\commandkey{label}}%
#1%
\end{hypothesis}

41
Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy
View File

@ -180,7 +180,6 @@ text*[tu15::scholarly_paper.experiment ]\<open>Lectus accumsan velit ultrices, .
text*[tu16::scholarly_paper.hypothesis ]\<open>Lectus accumsan velit ultrices, ...\<close>
text*[tu17::scholarly_paper.math_proof ]\<open>Lectus accumsan velit ultrices, ...\<close>
text*[tu18::scholarly_paper.consequence]\<open>Lectus accumsan velit ultrices, ...\<close>
text*[tu26::scholarly_paper.math_explanation]\<open>Lectus accumsan velit ultrices, ...\<close>
text*[tu19::scholarly_paper.math_formal]\<open>Lectus accumsan velit ultrices, ...\<close>
text*[tu20::scholarly_paper.proposition]\<open>Lectus accumsan velit ultrices, ...\<close>
text*[tu21::scholarly_paper.math_content ]\<open>Lectus accumsan velit ultrices, ...\<close>
@ -194,4 +193,44 @@ text*[tu8::scholarly_paper.tech_code] \<open>Lectus accumsan velit ultric
text*[tu27::scholarly_paper.engineering_content]\<open>Lectus accumsan velit ultrices, ...\<close>
text*[tu14::scholarly_paper.evaluation ]\<open>Lectus accumsan velit ultrices, ...\<close>
text\<open> @{axiom tu1} @{lemma tu2} @{example tu3} @{premise tu4} @{theorem tu5} @{assertion tu6}
@{technical tu9} @{assumption tu10 } @{definition tu13 }
@{experiment tu15 } @{hypothesis tu16 } @{math_proof tu17 }
@{consequence tu18 } @{math_formal tu19 } @{proposition tu20 }
@{math_content tu21 } @{math_example tu22 } @{conclusion_stmt tu23 }
@{math_motivation tu24 } @{tech_definition tu25 } @{eng_example tu28 }
@{tech_example tt10 } @{tech_code tu8 } @{engineering_content tu27 }
@{evaluation tu14 }
\<close>
subsection\<open>The Use in Macros\<close>
Lemma*[ttu2::scholarly_paper.lemma ]\<open>Lectus accumsan velit ultrices, ...\<close>
Example*[ttu3::scholarly_paper.math_example ]\<open>Lectus accumsan velit ultrices, ...\<close>
Premise*[ttu4::scholarly_paper.premise ]\<open>Lectus accumsan velit ultrices, ...\<close>
Theorem*[ttu5::scholarly_paper.theorem ]\<open>Lectus accumsan velit ultrices, ...\<close>
Assertion*[ttu6::scholarly_paper.assertion]\<open>Lectus accumsan velit ultrices, ...\<close>
Corollary*[ttu7::scholarly_paper.corollary]\<open>Lectus accumsan velit ultrices, ...\<close>
Assumption*[ttu10::scholarly_paper.assumption ]\<open>Lectus accumsan velit ultrices, ...\<close>
Definition*[ttu13::scholarly_paper.definition ]\<open>Lectus accumsan velit ultrices, ...\<close>
Hypothesis*[ttu16::scholarly_paper.hypothesis ]\<open>Lectus accumsan velit ultrices, ...\<close>
Proof*[ttu17::scholarly_paper.math_proof ]\<open>Lectus accumsan velit ultrices, ...\<close>
Consequence*[ttu18::scholarly_paper.consequence]\<open>Lectus accumsan velit ultrices, ...\<close>
Proposition*[ttu20::scholarly_paper.proposition]\<open>Lectus accumsan velit ultrices, ...\<close>
Conclusion*[ttu23::scholarly_paper.conclusion_stmt ]\<open>Lectus accumsan velit ultrices, ...\<close>
(* Definition*[ttu25::scholarly_paper.tech_definition ]\<open>Lectus accumsan velit ultrices, ...\<close>
interesting modeling bug.
*)
(*Example*[ttu28::scholarly_paper.eng_example ]\<open>Lectus accumsan velit ultrices, ...\<close>
interesting modeling bug.
*)
text\<open> @{lemma ttu2} @{math_example ttu3} @{premise ttu4} @{theorem ttu5} @{assertion ttu6}
@{assumption ttu10 } @{definition ttu13 }
@{hypothesis ttu16 } @{math_proof ttu17 }
@{consequence ttu18 } @{proposition ttu20 }
@{math_content tu21 } @{conclusion_stmt ttu23 }
@ \<open>{eng_example ttu28 }\<close>
@ \<open>{tech_example tt10 }\<close>
\<close>
end

10
Isabelle_DOF/ROOT
View File

@ -46,11 +46,11 @@ session "Isabelle_DOF" (AFP) = "Functional-Automata" +
"figures/definition-use-CSP-pdf.png"
"figures/definition-use-CSP.png"
"figures/MyCommentedIsabelle.png"
"figures/doc-mod-generic.png"
"figures/doc-mod-isar.png"
"figures/doc-mod-onto-docinst.png"
"figures/doc-mod-DOF.png"
"figures/doc-mod-term-aq.png"
"figures/doc-mod-generic.pdf"
"figures/doc-mod-isar.pdf"
"figures/doc-mod-onto-docinst.pdf"
"figures/doc-mod-DOF.pdf"
"figures/doc-mod-term-aq.pdf"
export_classpath

BIN
Isabelle_DOF/document/figures/doc-mod-DOF.pdf Normal file
View File

Binary file not shown.

BIN
Isabelle_DOF/document/figures/doc-mod-generic.pdf Normal file
View File

Binary file not shown.

BIN
Isabelle_DOF/document/figures/doc-mod-isar.pdf Normal file
View File

Binary file not shown.

BIN
Isabelle_DOF/document/figures/doc-mod-onto-docinst.pdf Normal file
View File

Binary file not shown.

BIN
Isabelle_DOF/document/figures/doc-mod-term-aq.pdf Normal file
View File

Binary file not shown.

BIN
Isabelle_DOF/document/figures/document-model.key
View File

Binary file not shown.

BIN
Isabelle_DOF/document/figures/document-model.pptx
View File

Binary file not shown.

2
Isabelle_DOF/document/root.bib
View File

@ -20,7 +20,7 @@
@Manual{ wenzel:isabelle-isar:2020,
title = {The Isabelle/Isar Reference Manual},
author = {Makarius Wenzel},
year = 2020,
year = 2022,
note = {Part of the Isabelle distribution.}
}

64
Isabelle_DOF/latex/styles/DOF-COL.sty
View File

@ -21,23 +21,23 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: figure*
\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}}
\newisadof{figure.Isa_COL.figure}%
\newisadof{figureDOTIsaUNDERSCORECOLDOTfigure}%
[label=,type=%
,Isa_COL.figure.relative_width=%
,Isa_COL.figure.placement=%
,Isa_COL.figure.src=%
,Isa_COL.figure.spawn_columns=enum False True%
,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=%
,IsaUNDERSCORECOLDOTfigureDOTplacement=%
,IsaUNDERSCORECOLDOTfigureDOTsrc=%
,IsaUNDERSCORECOLDOTfigureDOTspawnUNDERSCOREcolumns=enum False True%
][1]{%
\begin{figure}[]
\centering
\ifcommandkey{Isa_COL.figure.relative_width}
\ifcommandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}
{%
\gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
\gdef\dof@width{\commandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}}
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTfigureDOTsrc}}
\FPdiv\scale{\dof@width}{100}%
\includegraphics[width=\scale\textwidth]{\dof@src}%
}{%
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTfigureDOTsrc}}
\includegraphics[]{\dof@src}%
}
\caption{#1}\label{\commandkey{label}}%
@ -50,44 +50,44 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: side_by_side_figure*
\NewEnviron{isamarkupsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}}
\newisadof{side_by_side_figure.Isa_COL.side_by_side_figure}%
\NewEnviron{isamarkupsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure*}[1][]{\isaDof[env={sideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure},#1]{\BODY}}
\newisadof{sideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTIsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure}%
[label=,type=%
,Isa_COL.figure.relative_width=%
,Isa_COL.figure.placement=%
,Isa_COL.figure.src=%
,Isa_COL.side_by_side_figure.anchor=%
,Isa_COL.side_by_side_figure.caption=%
,Isa_COL.side_by_side_figure.relative_width2=%
,Isa_COL.side_by_side_figure.src2=%
,Isa_COL.side_by_side_figure.anchor2=%
,Isa_COL.side_by_side_figure.caption2=%
,Isa_COL.side_by_side_figure.placement=%
,Isa_COL.figure.spawn_columns=enum False True%
,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=%
,IsaUNDERSCORECOLDOTfigureDOTplacement=%
,IsaUNDERSCORECOLDOTfigureDOTsrc=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchor=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaption=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTrelativeUNDERSCOREwidthTWO=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTsrcTWO=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchorTWO=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaptionTWO=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTplacement=%
,IsaUNDERSCORECOLDOTfigureDOTspawnUNDERSCOREcolumns=enum False True%
][1]{%
\begin{figure}[]
\subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor}}\commandkey{Isa_COL.side_by_side_figure.caption}]%
{\ifcommandkey{Isa_COL.figure.relative_width}%
\subfloat[\label{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchor}}\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaption}]%
{\ifcommandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}%
{%
\gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
\gdef\dof@width{\commandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}}
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTfigureDOTsrc}}
\FPdiv\scale{\dof@width}{100}%
\includegraphics[width=\scale\textwidth]{\dof@src}%
}{%
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTfigureDOTsrc}}
\includegraphics[]{\dof@src}%
}%
}%
\hfill%
\subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor2}}\commandkey{Isa_COL.side_by_side_figure.caption2}]%
{\ifcommandkey{Isa_COL.side_by_side_figure.relative_width2}%
\subfloat[\label{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchorTWO}}\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaptionTWO}]%
{\ifcommandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTrelativeUNDERSCOREwidthTWO}%
{%
\gdef\dof@width{\commandkey{Isa_COL.side_by_side_figure.relative_width2}}
\gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
\gdef\dof@width{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTrelativeUNDERSCOREwidthTWO}}
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTsrcTWO}}
\FPdiv\scale{\dof@width}{100}%
\includegraphics[width=\scale\textwidth]{\dof@src}%
}{%
\gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTsrcTWO}}
\includegraphics[]{\dof@src}%
}%
}%

18
Isabelle_DOF/latex/styles/DOF-core.sty
View File

@ -53,27 +53,27 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: newcommand wrapper
\newcommand\newisadof[1]{\expandafter\newkeycommand\csname isaDof.#1\endcsname}%
\newcommand\renewisadof[1]{\expandafter\renewkeycommand\csname isaDof.#1\endcsname}%
\newcommand\provideisadof[1]{\expandafter\providekeycommand\csname isaDof.#1\endcsname}%
\newcommand\newisadof[1]{\expandafter\newkeycommand\csname isaDofDOT#1\endcsname}%
\newcommand\renewisadof[1]{\expandafter\renewkeycommand\csname isaDofDOT#1\endcsname}%
\newcommand\provideisadof[1]{\expandafter\providekeycommand\csname isaDofDOT#1\endcsname}%
% end: newcommand wrapper
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: generic dispatcher
\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{%
\ifcsname isaDof.\commandkey{type}\endcsname%
\csname isaDof.\commandkey{type}\endcsname%
\ifcsname isaDofDOT\commandkey{type}\endcsname%
\csname isaDofDOT\commandkey{type}\endcsname%
[label=\commandkey{label},\commandkey{args}]{#1}%
\else%
\ifcsname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
\csname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
\ifcsname isaDofDOT\commandkey{env}DOT\commandkey{type}\endcsname%
\csname isaDofDOT\commandkey{env}DOT\commandkey{type}\endcsname%
[label=\commandkey{label},\commandkey{args}]{#1}%
\else%
\message{Isabelle/DOF: Using default LaTeX representation for concept %
"\commandkey{env}.\commandkey{type}".}%
\ifcsname isaDof.\commandkey{env}\endcsname%
\csname isaDof.\commandkey{env}\endcsname%
\ifcsname isaDofDOT\commandkey{env}\endcsname%
\csname isaDofDOT\commandkey{env}\endcsname%
[label=\commandkey{label}]{#1}%
\else%
\errmessage{Isabelle/DOF: No LaTeX representation for concept %

114
Isabelle_DOF/ontologies/scholarly_paper/DOF-scholarly_paper.sty
View File

@ -73,9 +73,9 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: title*
\NewEnviron{isamarkuptitle*}[1][]{\isaDof[env={title},#1]{\BODY}}
\newisadof{title.scholarly_paper.title}%
\newisadof{titleDOTscholarlyUNDERSCOREpaperDOTtitle}%
[label=,type=%
,scholarly_paper.title.short_title=%
,scholarlyUNDERSCOREpaperDOTtitleDOTshortUNDERSCOREtitle=%
][1]{%
\immediate\write\@auxout{\noexpand\title{#1}}%
}
@ -85,9 +85,9 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: subtitle*
\NewEnviron{isamarkupsubtitle*}[1][]{\isaDof[env={subtitle},#1]{\BODY}}
\newisadof{subtitle.scholarly_paper.subtitle}%
\newisadof{subtitleDOTscholarlyUNDERSCOREpaperDOTsubtitle}%
[label=,type=%
,scholarly_paper.subtitle.abbrev=%
,scholarlyUNDERSCOREpaperDOTsubtitleDOTabbrev=%
][1]{%
\immediate\write\@auxout{\noexpand\subtitle{#1}}%
}
@ -128,21 +128,21 @@
}
\NewEnviron{isamarkupauthor*}[1][]{\isaDof[env={text},#1]{\BODY}}
\provideisadof{text.scholarly_paper.author}%
\provideisadof{textDOTscholarlyUNDERSCOREpaperDOTauthor}%
[label=,type=%
,scholarly_paper.author.email=%
,scholarly_paper.author.affiliation=%
,scholarly_paper.author.orcid=%
,scholarly_paper.author.http_site=%
,scholarlyUNDERSCOREpaperDOTauthorDOTemail=%
,scholarlyUNDERSCOREpaperDOTauthorDOTaffiliation=%
,scholarlyUNDERSCOREpaperDOTauthorDOTorcid=%
,scholarlyUNDERSCOREpaperDOTauthorDOThttpUNDERSCOREsite=%
][1]{%
\stepcounter{dof@cnt@author}
\def\dof@a{\commandkey{scholarly_paper.author.affiliation}}
\ifthenelse{\equal{\commandkey{scholarly_paper.author.orcid}}{}}{%
\def\dof@a{\commandkey{scholarlyUNDERSCOREpaperDOTauthorDOTaffiliation}}
\ifthenelse{\equal{\commandkey{scholarlyUNDERSCOREpaperDOTauthorDOTorcid}}{}}{%
\protected@write\@auxout{}{\string\addauthor{#1\string\inst{\thedof@cnt@author}}}%
}{%
\protected@write\@auxout{}{\string\addauthor{#1\string\inst{\thedof@cnt@author}\string\orcidID{\commandkey{scholarly_paper.author.orcid}}}}%
\protected@write\@auxout{}{\string\addauthor{#1\string\inst{\thedof@cnt@author}\string\orcidID{\commandkey{scholarlyUNDERSCOREpaperDOTauthorDOTorcid}}}}%
}
\protected@write\@auxout{}{\string\addaffiliation{\dof@a\\\string\email{\commandkey{scholarly_paper.author.email}}}}%
\protected@write\@auxout{}{\string\addaffiliation{\dof@a\\\string\email{\commandkey{scholarlyUNDERSCOREpaperDOTauthorDOTemail}}}}%
}
% end: scholarly_paper.author
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@ -151,15 +151,15 @@
% begin: scholarly_paper.abstract
\providecommand{\keywords}[1]{\mbox{}\\[2ex]\mbox{}\noindent{\textbf{Keywords:}} #1}
\NewEnviron{isamarkupabstract*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newisadof{text.scholarly_paper.abstract}%
\newisadof{textDOTscholarlyUNDERSCOREpaperDOTabstract}%
[label=,type=%
,scholarly_paper.abstract.keywordlist=%
,scholarlyUNDERSCOREpaperDOTabstractDOTkeywordlist=%
][1]{%
\begin{isamarkuptext}%
\begin{abstract}%
#1%
\ifthenelse{\equal{\commandkey{scholarly_paper.abstract.keywordlist}}{}}{}{%
\keywords{\commandkey{scholarly_paper.abstract.keywordlist}}%
\ifthenelse{\equal{\commandkey{scholarlyUNDERSCOREpaperDOTabstractDOTkeywordlist}}{}}{}{%
\keywords{\commandkey{scholarlyUNDERSCOREpaperDOTabstractDOTkeywordlist}}%
}%
\end{abstract}%
\end{isamarkuptext}%
@ -172,84 +172,84 @@
%\newtheorem{theorem}{Theorem}
\newtheorem{defn}{Definition}
\newcommand{\defnautorefname}{Definition}
\NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{axm}{Axiom}
\newcommand{\axmautorefname}{Axiom}
\NewEnviron{isamarkupAxiom*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupAxiom*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{theom}{Theorem}
\newcommand{\theomautorefname}{Theorem}
\NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{lemm}{Lemma}
\newcommand{\lemmautorefname}{Lemma}
\NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{corr}{Corollary}
\newcommand{\corrautorefname}{Corollary}
\NewEnviron{isamarkupCorollary*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupCorollary*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{prpo}{Proposition}
\newcommand{\prpoautorefname}{Proposition}
\NewEnviron{isamarkupProposition*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupProposition*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{rulE}{Rule}
\newcommand{\rulEautorefname}{Rule}
\NewEnviron{isamarkupRule*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupRule*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{assn}{Assertion}
\newcommand{\assnautorefname}{Assertion}
\NewEnviron{isamarkupAssertion*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupAssertion*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{hypt}{Hypothesis}
\newcommand{\hyptautorefname}{Hypothesis}
\NewEnviron{isamarkupHypothesis*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupHypothesis*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{assm}{Assumption}
\newcommand{\assmautorefname}{Assumption}
\NewEnviron{isamarkupAssumption*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupAssumption*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{prms}{Premise}
\newcommand{\prmsautorefname}{Premise}
\NewEnviron{isamarkupPremise*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupPremise*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{cons}{Consequence}
\newcommand{\consautorefname}{Consequence}
\NewEnviron{isamarkupConsequence*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\newtheorem{conc_stmt}{Conclusion}
\newcommand{\concstmtautorefname}{Conclusion}
\NewEnviron{isamarkupConclusion*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\newtheorem{prf_stmt}{Proof}
\newcommand{\prfstmtautorefname}{Proof}
\NewEnviron{isamarkupProof*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\newtheorem{expl_stmt}{Example}
\newcommand{\explstmtautorefname}{Example}
\NewEnviron{isamarkupExample*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupConsequence*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{concUNDERSCOREstmt}{Conclusion}
\newcommand{\concUNDERSCOREstmtautorefname}{Conclusion}
\NewEnviron{isamarkupConclusion*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{prfUNDERSCOREstmt}{Proof}
\newcommand{\prfUNDERSCOREstmtautorefname}{Proof}
\NewEnviron{isamarkupProof*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{explUNDERSCOREstmt}{Example}
\newcommand{\explUNDERSCOREstmtautorefname}{Example}
\NewEnviron{isamarkupExample*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{rmrk}{Remark}
\newcommand{\rmrkautorefname}{Remark}
\NewEnviron{isamarkupRemark*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupRemark*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{notn}{Notation}
\newcommand{\notnautorefname}{Notation}
\NewEnviron{isamarkupNotation*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupNotation*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{tmgy}{Terminology}
\newcommand{\tmgyautorefname}{Terminology}
\NewEnviron{isamarkupTerminology*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupTerminology*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newisadof{text.scholarly_paper.math_content}%
\newisadof{textDOTscholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}%
[label=,type=%
, scholarly_paper.math_content.short_name ={}%
, scholarly_paper.math_content.mcc = %
, Isa_COL.text_element.level =%
, Isa_COL.text_element.referentiable =%
, Isa_COL.text_element.variants =%
, scholarly_paper.text_section.main_author =%
, scholarly_paper.text_section.fixme_list =%
, Isa_COL.text_element.level =%
, scholarly_paper.technical.definition_list =%
, scholarly_paper.technical.status =%
, scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname ={}%
, scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc = %
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel =%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable =%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants =%
, scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTmainUNDERSCOREauthor =%
, scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTfixmeUNDERSCORElist =%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel =%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTdefinitionUNDERSCORElist =%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTstatus =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
\ifthenelse{\equal{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname}} {} }
{%
\begin{\commandkey{scholarly_paper.math_content.mcc}}\label{\commandkey{label}}
\begin{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}\label{\commandkey{label}}
#1
\end{\commandkey{scholarly_paper.math_content.mcc}}
\end{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}
}{%
\begin{\commandkey{scholarly_paper.math_content.mcc}}[\commandkey{scholarly_paper.math_content.short_name}]\label{\commandkey{label}}
\begin{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}[\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname}]\label{\commandkey{label}}
#1
\end{\commandkey{scholarly_paper.math_content.mcc}}
\end{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}
}
\end{isamarkuptext}%
}

34
Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy
View File

@ -53,12 +53,12 @@ ML\<open>
val _ =
Monitor_Command_Parser.document_command \<^command_keyword>\<open>abstract*\<close> "Textual Definition"
{markdown = true, body = true}
(Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []) (K(K I));
(Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []) [] I;
val _ =
Monitor_Command_Parser.document_command \<^command_keyword>\<open>author*\<close> "Textual Definition"
{markdown = true, body = true}
(Onto_Macros.enriched_document_cmd_exp (SOME "author") []) (K(K I));
(Onto_Macros.enriched_document_cmd_exp (SOME "author") []) [] I;
\<close>
text\<open>Scholarly Paper is oriented towards the classical domains in science:
@ -203,7 +203,6 @@ datatype math_content_class =
| "notn" \<comment>\<open>notation\<close>
| "tmgy" \<comment>\<open>terminology\<close>
text\<open>Instances of the \<open>doc_class\<close> \<^verbatim>\<open>math_content\<close> are by definition @{term "semiformal"}; they may
be non-referential, but in this case they will not have a @{term "short_name"}.\<close>
@ -444,49 +443,50 @@ fun doc_cmd kwd txt flag key =
in
Onto_Macros.enriched_formal_statement_command default [("mcc",key)] meta_args thy
end)
(Onto_Macros.transform_attr [("mcc",key)])
[\<^const_name>\<open>mcc\<close>]
(Onto_Macros.transform_attr [(\<^const_name>\<open>mcc\<close>,key)])
in
val _ = doc_cmd \<^command_keyword>\<open>Definition*\<close> "Freeform Definition"
Definition_default_class "defn";
Definition_default_class \<^const_name>\<open>defn\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Lemma*\<close> "Freeform Lemma Description"
Lemma_default_class "lemm";
Lemma_default_class \<^const_name>\<open>lemm\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Theorem*\<close> "Freeform Theorem"
Theorem_default_class "theom";
Theorem_default_class \<^const_name>\<open>theom\<close>;
(* cut and paste to make it runnable, but nonsensical so far: *)
val _ = doc_cmd \<^command_keyword>\<open>Proposition*\<close> "Freeform Proposition"
Proposition_default_class "prpo";
Proposition_default_class \<^const_name>\<open>prpo\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Premise*\<close> "Freeform Premise"
Premise_default_class "prms";
Premise_default_class \<^const_name>\<open>prms\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Corollary*\<close> "Freeform Corollary"
Corollary_default_class "corr";
Corollary_default_class \<^const_name>\<open>corr\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Consequence*\<close> "Freeform Consequence"
Consequence_default_class "cons";
Consequence_default_class \<^const_name>\<open>cons\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Conclusion*\<close> "Freeform Conclusion"
Conclusion_default_class "conc_stmt";
Conclusion_default_class \<^const_name>\<open>conc_stmt\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Assumption*\<close> "Freeform Assumption"
Assumption_default_class "assm";
Assumption_default_class \<^const_name>\<open>assm\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Hypothesis*\<close> "Freeform Hypothesis"
Hypothesis_default_class "prpo";
Hypothesis_default_class \<^const_name>\<open>prpo\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Assertion*\<close> "Freeform Assertion"
Assertion_default_class "assn";
Assertion_default_class \<^const_name>\<open>assn\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Proof*\<close> "Freeform Proof"
Proof_default_class "prf_stmt";
Proof_default_class \<^const_name>\<open>prf_stmt\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Example*\<close> "Freeform Example"
Example_default_class "expl_stmt";
Example_default_class \<^const_name>\<open>expl_stmt\<close>;
end
end
\<close>

20
Isabelle_DOF/ontologies/technical_report/DOF-technical_report.sty
View File

@ -34,16 +34,16 @@
\newisadof{text.technical_report.SML}%
[ label=,type=%
, Isa_COL.text_element.level=%
, Isa_COL.text_element.referentiable=%
, Isa_COL.text_element.variants=%
, scholarly_paper.text_section.main_author=%
, scholarly_paper.text_section.fixme_list=%
, scholarly_paper.technical.definition_list=%
, scholarly_paper.technical.status=%
, scholarly_paper.technical.formal_results=%
, technical_report.code.checked=%
, technical_report.code.caption=%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
, scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTmainUNDERSCOREauthor=%
, scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTfixmeUNDERSCORElist=%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTdefinitionUNDERSCORElist=%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTstatus=%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTformalUNDERSCOREresults=%
, technicalUNDERSCOREreportDOTcodeDOTchecked=%
, technicalUNDERSCOREreportDOTcodeDOTcaption=%
]
[1]
{%

12
Isabelle_DOF/thys/Isa_COL.thy
View File

@ -103,17 +103,11 @@ fun transform_cid thy NONE X = X
end
in
fun transform_attr S cid_long thy doc_attrs =
fun transform_attr S doc_attrs =
let
fun transform_attr' [] doc_attrs = doc_attrs
| transform_attr' (s::S) (doc_attrs) =
let fun markup2string s = s |> YXML.content_of
|> Symbol.explode
|> List.filter (fn c => c <> Symbol.DEL)
|> String.concat
fun toLong n = DOF_core.get_attribute_info cid_long (markup2string n) thy
|> the |> #long_name
val (name', value) = s |> (fn (n, v) => (toLong n, v))
let val (name', value) = s
val doc_attrs' = doc_attrs
|> map (fn (name, term) => if name = name'
then (name, value)
@ -154,7 +148,7 @@ end (* local *)
fun heading_command (name, pos) descr level =
Monitor_Command_Parser.document_command (name, pos) descr
{markdown = false, body = true} (enriched_text_element_cmd level) (K(K I));
{markdown = false, body = true} (enriched_text_element_cmd level) [] I;
val _ = heading_command \<^command_keyword>\<open>title*\<close> "section heading" NONE;
val _ = heading_command \<^command_keyword>\<open>subtitle*\<close> "section heading" NONE;

67
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -841,6 +841,10 @@ val check_opening_ml_invs = check_invs get_opening_ml_invariants
val check_closing_ml_invs = check_invs get_closing_ml_invariants
(* Output name for LaTeX macros.
Also rewrite "." to allow macros with objects long names *)
val output_name = Latex.output_name o translate_string (fn "." => "DOT" | s => s)
val ISA_prefix = "Isabelle_DOF_"
val doc_class_prefix = ISA_prefix ^ "doc_class_"
@ -2134,19 +2138,21 @@ fun close_monitor_command (args as (((oid, pos), cid_pos),
end
fun meta_args_2_latex thy transform_attr
fun meta_args_2_latex thy sem_attrs transform_attr
((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) =
(* for the moment naive, i.e. without textual normalization of
attribute names and adapted term printing *)
let val l = DOF_core.get_instance_name_global lab thy |> enclose "{" "}"
let val l = DOF_core.get_instance_name_global lab thy |> DOF_core.output_name
|> enclose "{" "}"
|> prefix "label = "
(* val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *)
val cid_long = case cid_opt of
NONE => DOF_core.cid_of lab thy
| SOME(cid,_) => DOF_core.get_onto_class_name_global' cid thy
(* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *)
val cid_txt = "type = " ^ (enclose "{" "}" cid_long);
val cid_txt = cid_long |> DOF_core.output_name
|> enclose "{" "}"
|> prefix "type = "
fun ltx_of_term _ _ (c as \<^Const_>\<open>Cons \<^Type>\<open>char\<close> for _ _\<close>) = HOLogic.dest_string c
| ltx_of_term _ _ \<^Const_>\<open>Nil _\<close> = ""
| ltx_of_term _ _ \<^Const_>\<open>numeral _ for t\<close> = Int.toString(HOLogic.dest_numeral t)
@ -2191,8 +2197,24 @@ fun meta_args_2_latex thy transform_attr
val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a)
(map (fn (c,_) => c) actual_args))) default_args
val transformed_args = (actual_args@default_args_filtered)
|> transform_attr cid_long thy
val str_args = transformed_args
|> transform_attr
fun update_sem_std_attrs [] attrs = attrs
| update_sem_std_attrs (attr::attrs) attrs' =
let val attrs'' = attrs' |> map (fn (name, value) =>
let val value' = value |> Long_Name.base_name
in
if name = attr
then if value' (*|> Symbol_Pos.is_identifier*)
|> Symbol.is_ascii_identifier
then (name, DOF_core.output_name value')
else ISA_core.err ("Bad name of semantic attribute"
^ name ^ ": " ^ value
^ ". Name must be ASCII") pos
else (name, value') end)
in update_sem_std_attrs attrs attrs'' end
val updated_sem_std_attrs = update_sem_std_attrs sem_attrs transformed_args
val updated_sem_std_attrs' = updated_sem_std_attrs |> map (apfst DOF_core.output_name)
val str_args = updated_sem_std_attrs'
|> map (fn (lhs,rhs) => lhs^" = "^(enclose "{" "}" rhs))
val label_and_type = String.concat [ l, ",", cid_txt]
@ -2218,15 +2240,15 @@ fun gen_enriched_document_cmd' {inline} cid_transform attr_transform
(* {markdown = true} sets the parsing process such that in the text-core
markdown elements are accepted. *)
fun document_output {markdown: bool, markup: Latex.text -> Latex.text} transform_attr meta_args text ctxt =
fun document_output {markdown: bool, markup: Latex.text -> Latex.text} sem_attrs transform_attr meta_args text ctxt =
let
val thy = Proof_Context.theory_of ctxt;
val _ = Context_Position.reports ctxt (Document_Output.document_reports text);
val output_meta = meta_args_2_latex thy transform_attr meta_args;
val output_meta = meta_args_2_latex thy sem_attrs transform_attr meta_args;
val output_text = Document_Output.output_document ctxt {markdown = markdown} text;
in markup (output_meta @ output_text) end;
fun document_output_reports name {markdown, body} transform_attr meta_args text ctxt =
fun document_output_reports name {markdown, body} sem_attrs transform_attr meta_args text ctxt =
let
(*val pos = Input.pos_of text;
val _ =
@ -2236,16 +2258,16 @@ fun document_output_reports name {markdown, body} transform_attr meta_args text
fun markup xml =
let val m = if body then Markup.latex_body else Markup.latex_heading
in [XML.Elem (m (Latex.output_name name), xml)] end;
in document_output {markdown = markdown, markup = markup} transform_attr meta_args text ctxt end;
in document_output {markdown = markdown, markup = markup} sem_attrs transform_attr meta_args text ctxt end;
(* document output commands *)
fun document_command (name, pos) descr mark cmd transform_attr =
fun document_command (name, pos) descr mark cmd sem_attrs transform_attr =
Outer_Syntax.command (name, pos) descr
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >> (fn (meta_args, text) =>
Toplevel.theory' (fn _ => cmd meta_args)
(SOME (Toplevel.presentation_context #> document_output_reports name mark transform_attr meta_args text))));
(SOME (Toplevel.presentation_context #> document_output_reports name mark sem_attrs transform_attr meta_args text))));
(* Core Command Definitions *)
@ -2271,14 +2293,14 @@ val _ =
val _ =
document_command \<^command_keyword>\<open>text*\<close> "formal comment (primary style)"
{markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I) (K(K I));
{markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I) [] I;
(* This is just a stub at present *)
val _ =
document_command \<^command_keyword>\<open>text-macro*\<close> "formal comment macro"
{markdown = true, body = true}
(gen_enriched_document_cmd {inline=false} (* declare as macro *) I I) (K(K I));
(gen_enriched_document_cmd {inline=false} (* declare as macro *) I I) [] I;
val (declare_reference_default_class, declare_reference_default_class_setup)
@ -2553,6 +2575,9 @@ ML\<open>
local
fun elaborate stmt ctxt = stmt |> map (apsnd (map (apfst (DOF_core.elaborate_term ctxt)
#> apsnd (map (DOF_core.elaborate_term ctxt)))))
fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
let
val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt;
@ -2562,11 +2587,7 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
(case raw_stmt of
Element.Shows _ =>
let val stmt' = Attrib.map_specs (map prep_att) stmt
val stmt'' = stmt' |> map (fn (b, ts) =>
(b, ts |> map (fn (t', t's) =>
(DOF_core.elaborate_term ctxt t',
t's |> map (fn t'' =>
DOF_core.elaborate_term ctxt t'')))))
val stmt'' = elaborate stmt' ctxt
in (([], prems, stmt'', NONE), stmt_ctxt) end
| Element.Obtains raw_obtains =>
let
@ -2581,11 +2602,7 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
||> Proof_Context.restore_stmt asms_ctxt;
val stmt' = [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])];
val stmt'' = stmt' |> map (fn (b, ts) =>
(b, ts |> map (fn (t', t's) =>
(DOF_core.elaborate_term ctxt t',
t's |> map (fn t'' =>
DOF_core.elaborate_term ctxt t'')))))
val stmt'' = elaborate stmt' ctxt
in ((Obtain.obtains_attribs raw_obtains, prems, stmt'', SOME that'), that_ctxt) end)
end;
@ -2826,7 +2843,7 @@ fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked, define}, src
|(true,true) => XML.enclose("{\\isaDofmacroDef[type={"^cid_decl^"}]{")"}}"
|(false,true) => XML.enclose("{\\isaDofmacroExp[type={"^cid_decl^"}]{")"}}"
)
(Latex.text (str, pos))
(Latex.text (DOF_core.output_name str, pos))
end

7
Isabelle_DOF/thys/manual/M_00_Frontmatter.thy
View File

@ -36,8 +36,11 @@ define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
text\<open>Note that these setups assume that the associated \<^LaTeX> macros
are defined, \<^eg>, in the document prelude. \<close>
define_macro* index \<rightleftharpoons> \<open>\index{\<close> _ \<open>}\<close>
define_macro* bindex \<rightleftharpoons> \<open>\bindex{\<close> _ \<open>}\<close>
define_macro* index \<rightleftharpoons> \<open>\index{\<close> _ \<open>}\<close>
define_macro* bindex \<rightleftharpoons> \<open>\bindex{\<close> _ \<open>}\<close>
define_macro* nolinkurl \<rightleftharpoons> \<open>\nolinkurl{\<close> _ \<open>}\<close>
define_macro* center \<rightleftharpoons> \<open>\center{\<close> _ \<open>}\<close>
define_macro* ltxinline \<rightleftharpoons> \<open>\inlineltx|\<close> _ \<open>|\<close>
ML\<open>

10
Isabelle_DOF/thys/manual/M_02_Background.thy
View File

@ -106,9 +106,9 @@ text\<open>
side_by_side_figure*[docModGenConcr::side_by_side_figure,anchor="''docModGen''",
caption="''Schematic Representation.''",relative_width="45",
src="''figures/doc-mod-generic.png''",anchor2="''docModIsar''",
src="''figures/doc-mod-generic.pdf''",anchor2="''docModIsar''",
caption2="''The Isar Instance.''",relative_width2="45",
src2="''figures/doc-mod-isar.png''"]\<open>A Representation of a Document Model.\<close>
src2="''figures/doc-mod-isar.pdf''"]\<open>A Representation of a Document Model.\<close>
text\<open>The body of a theory file consists of a sequence of \<^emph>\<open>commands\<close> that must be introduced
by a command keyword such as \<^boxed_theory_text>\<open>requirement\<close> above. Command keywords may mark
@ -184,13 +184,13 @@ text\<open>Antiquotations seen as semantic macros are partial functions of type
side_by_side_figure*[docModOnto::side_by_side_figure,anchor="''docModGen''",
caption="''A Document with Ontological Annotations.''",relative_width="47",
src="''figures/doc-mod-DOF.png''",anchor2="''docModDOF''",
src="''figures/doc-mod-DOF.pdf''",anchor2="''docModDOF''",
caption2="''Ontological References.''",relative_width2="47",
src2="''figures/doc-mod-onto-docinst.png''"]\<open>Documents conform to Ontologies.\<close>
src2="''figures/doc-mod-onto-docinst.pdf''"]\<open>Documents conform to Ontologies.\<close>
text\<open>Since Isabelle's commands are freely programmable, it is possible to implement \<^dof> as an
extension of the system. In particular, the ontology language of \<^dof> provides an ontology
definition language ODL that \<^emph>\<open>generates\<close> anti-quotations and the infrastructure to check and evaluate
definition language ODL\<^bindex>\<open>ODL\<close> that \<^emph>\<open>generates\<close> anti-quotations and the infrastructure to check and evaluate
them. This allows for checking an annotated document with respect to a given ontology, which may be
specific for a given domain-specific universe of discourse (see @{figure "docModOnto"}). ODL will
be described in @{text_section (unchecked) "isadof_tour"} in more detail.\<close>

168
Isabelle_DOF/thys/manual/M_03_GuidedTour.thy
View File

@ -23,7 +23,7 @@ chapter*[isadof_tour::text_section]\<open>\<^isadof>: A Guided Tour\<close>
text\<open>
In this chapter, we will give an introduction into using \<^isadof> for users that want to create and
maintain documents following an existing document ontology.
maintain documents following an existing document ontology\<^bindex>\<open>ontology\<close> in ODL\<^bindex>\<open>ODL\<close>.
\<close>
section*[getting_started::technical]\<open>Getting Started\<close>
@ -34,7 +34,7 @@ text\<open>
\<^LaTeX>. We assume a basic familiarity with a Linux/Unix-like command line (i.e., a shell).
Furthermore, we focus on the installation of the latest official release of \<^isadof> as
available in the Archive of Formal Proofs (AFP).\<^footnote>\<open>If you want to work with the development version
of Isabelle/DOF, please obtain its source code from the Isabelle/DOF Git repostitory
of \<^isadof>, please obtain its source code from the \<^isadof> Git repostitory
(\<^url>\<open>https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF\<close> and follow the instructions
in provided \<^verbatim>\<open>README.MD\<close> file.\<close>
@ -72,11 +72,12 @@ text\<open>
By installing the AFP in the previous steps, you already installed \<^isadof>. In fact, \<^isadof>
is currently consisting out of two AFP entries:
\<^item> Isabelle\_DOF: This entry
contains the Isabelle/DOF system itself, including the Isabelle/DOF manual.
\<^item> Isabelle\_DOF-Example-I: This entry contains an example of
an academic paper written using the Isabelle/DOF system oriented towards
\<^item> Isabelle\_DOF-Example-II: This entry contains another example of
\<^item> \<^verbatim>\<open>Isabelle_DOF\<close>: This entry
contains the \<^isadof> system itself, including the \<^isadof> manual.
\<^item> \<^verbatim>\<open>Isabelle_DOF-Example-I\<close>: This entry contains an example of
an academic paper written using the \<^isadof> system oriented towards an
introductory paper.
\<^item> \<^verbatim>\<open>Isabelle_DOF-Example-II\<close>: This entry contains another example of
a mathematics-oriented academic paper.
It is recommended to follow structure one of these papers.\<close>
@ -143,10 +144,10 @@ want to use. Otherwise, they will not be available.
paragraph\<open>Warning.\<close>
text\<open>
Note that the session @{session "Isabelle_DOF"} needs to be part of the ``main'' session
hierarchy. Loading the Isabelle/DOF theories as part of a session section, e.g.,
Note that the session \<^session>\<open>Isabelle_DOF\<close> needs to be part of the ``main'' session
hierarchy. Loading the \<^isadof> theories as part of a session section, e.g.,
\<close>
text\<open>
text\<open>\<^latex>\<open>
\begin{config}{ROOT}
session example = HOL +
options [document = pdf, document_output = "output", document_build = dof]
@ -156,7 +157,7 @@ session example = HOL +
theories
C
\end{config}
\<close>
\<close>\<close>
text\<open>
will not work. Trying to build a document using such a setup will result in the
following error message:
@ -214,35 +215,31 @@ text\<open>At times, this causes idiosyncrasies like the ones cited in the follo
\<close>
section*[scholar_onto::example]\<open>Writing Academic Publications in \<^boxed_theory_text>\<open>scholarly_paper\<close>\<close>
subsection\<open>Writing Academic Papers\<close>
subsection\<open>A Selection of major Examples\<close>
text\<open>
The ontology \<^verbatim>\<open>scholarly_paper\<close>
\<^index>\<open>ontology!scholarly\_paper\<close> is an ontology modeling
academic/scientific papers, with a slight bias towards texts in the domain of mathematics and engineering.
We explain first the principles of its underlying ontology, and then we present two ``real''
examples from our own publication practice.
\<close>
text\<open>
\<^enum> The iFM 2020 paper~@{cite "taha.ea:philosophers:2020"} is a typical mathematical text,
heavy in definitions with complex mathematical notation and a lot of non-trivial cross-referencing
between statements, definitions and proofs which are ontologically tracked. However, wrt.
the possible linking between the underlying formal theory and this mathematical presentation,
it follows a pragmatic path without any ``deep'' linking to types, terms and theorems,
deliberately not exploiting \<^isadof> 's full potential with this regard.
\<^enum> In the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}, we deliberately
refrain from integrating references to formal content in order to demonstrate that \<^isadof> is not
a framework from Isabelle users to Isabelle users only, but people just avoiding as much as
possible \<^LaTeX> notation.
The ontology \<^verbatim>\<open>scholarly_paper\<close> \<^index>\<open>ontology!scholarly\_paper\<close> is an ontology modeling
academic/scientific papers, with a slight bias towards texts in the domain of mathematics and
engineering. We explain first the principles of its underlying ontology, and then we present two
``real'' examples from our own publication practice.
\<^enum> The iFM 2020 paper~@{cite "taha.ea:philosophers:2020"} is a typical mathematical text,
heavy in definitions with complex mathematical notation and a lot of non-trivial cross-referencing
between statements, definitions and proofs which are ontologically tracked. However, wrt.
the possible linking between the underlying formal theory and this mathematical presentation, it follows a pragmatic path without any ``deep'' linking to types, terms and theorems,
deliberately not exploiting \<^isadof> 's full potential with this regard.
\<^enum> In the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}, we deliberately
refrain from integrating references to formal content in order to demonstrate that \<^isadof> is not
a framework from Isabelle users to Isabelle users only, but people just avoiding as much as
possible \<^LaTeX> notation.
The \<^isadof> distribution contains both examples using the ontology \<^verbatim>\<open>scholarly_paper\<close> in
the directory \nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/} or
\nolinkurl{examples/scholarly_paper/2020-iFM-CSP}.
the directory \<^nolinkurl>\<open>examples/scholarly_paper/2018-cicm-isabelle_dof-applications/\<close> or
\<^nolinkurl>\<open>examples/scholarly_paper/2020-iFM-CSP\<close>.
You can inspect/edit the example in Isabelle's IDE, by either
\<^item> starting Isabelle/jEdit using your graphical user interface (\<^eg>, by clicking on the
Isabelle-Icon provided by the Isabelle installation) and loading the file
\nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy},
\<^item> starting Isabelle/jEdit from the command line by, \<^eg>, calling:
\<^item> starting Isabelle/jEdit using your graphical user interface (\<^eg>, by clicking on the
Isabelle-Icon provided by the Isabelle installation) and loading the file
\<^nolinkurl>\<open>examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy"\<close>
\<^item> starting Isabelle/jEdit from the command line by, \<^eg>, calling:
@{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë
isabelle jedit -d . examples/scholarly_paper/2020-iFM-CSP/paper.thy \<close>}
@ -312,7 +309,7 @@ as follows:
Additional means assure that the following invariant is maintained in a document
conforming to \<^verbatim>\<open>scholarly_paper\<close>:
\center {\<open>level > 0\<close>}
\<^center>\<open>\<open>level > 0\<close>\<close>
\<close>
text\<open>\<^vs>\<open>1.0cm\<close>\<close>
@ -464,10 +461,6 @@ in which the text-elements instances are expected to appear in the textual order
defined by \<^typ>\<open>article\<close>.
\<close>
figure*[doc_termAq::figure,relative_width="80",src="''figures/doc-mod-term-aq.png''"]
\<open>Term-Antiquotations Referencing to Annotated Elements\<close>
side_by_side_figure*[exploring::side_by_side_figure,anchor="''fig-Dogfood-II-bgnd1''",
caption="''Exploring a reference of a text-element.''",relative_width="48",
src="''figures/Dogfood-II-bgnd1''",anchor2="''fig-bgnd-text_section''",
@ -485,12 +478,21 @@ side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-
text\<open>
From these class definitions, \<^isadof> also automatically generated editing
support for Isabelle/jEdit. In \autoref{fig-Dogfood-II-bgnd1} and
\autoref{fig-bgnd-text_section} we show how hovering over links permits to explore its
support for Isabelle/jEdit. In
@{figure "exploring"}(left)
% \autoref{fig-Dogfood-II-bgnd1}
and
@{figure "exploring"}(right)
% \autoref{fig-bgnd-text_section}
we show how hovering over links permits to explore its
meta-information. Clicking on a document class identifier permits to hyperlink into the
corresponding class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an
attribute-definition (which is qualified in order to disambiguate;
\autoref{fig:Dogfood-V-attribute}) shows its type.
corresponding class definition (
@{figure "hyperlinks"}(left)
%\autoref{fig:Dogfood-IV-jumpInDocCLass})
; hovering over an attribute-definition (which is qualified in order to disambiguate; cf.
@{figure "hyperlinks"}(right)
%\autoref{fig:Dogfood-V-attribute}
) shows its type.
\<close>
figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-VI-linkappl.png''"]
@ -499,17 +501,68 @@ figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-
text\<open>
An ontological reference application in @{figure "figDogfoodVIlinkappl"}: the
ontology-dependant antiquotation \<^boxed_theory_text>\<open>@{example \<open>ex1\<close>}\<close> refers to the corresponding
text-element \<^boxed_theory_text>\<open>ex1\<close>.
Hovering allows for inspection, clicking for jumping to the definition.
If the link does not exist or has a non-compatible type, the text is not validated, \<^ie>,
Isabelle/jEdit will respond with an error.\<close>
text-element \<^boxed_theory_text>\<open>ex1\<close>. Hovering allows for inspection, clicking for jumping to the
definition. If the link does not exist or has a non-compatible type, the text is not validated,
\<^ie>, Isabelle/jEdit will respond with an error.\<close>
text\<open>We advise users to experiment with different notation variants.
Note, further, that the Isabelle \<^latex>\<open>@\{cite ...\}\<close>-text-anti-quotation makes its checking
on the level of generated \<^verbatim>\<open>.aux\<close>-files, which are not necessarily up-to-date. Ignoring the PIDE
error-message and compiling a with a consistent bibtex usually makes disappear this behavior.
error-message and compiling it with a consistent bibtex usually makes disappear this behavior.
\<close>
subsection*["using-term-aq"::technical, main_author = "Some @{author ''bu''}"]
\<open>Using Term-Antiquotations\<close>
text\<open>The present version of \<^isadof> is the first version that supports the novel feature of
\<^dof>-generated term-antiquotations\<^bindex>\<open>term-antiquotations\<close>, \<^ie>, antiquotations embedded
in HOL-\<open>\<lambda>\<close>-terms possessing arguments that were validated in the ontological context.
These \<open>\<lambda>\<close>-terms may occur in definitions, lemmas, or in values to define attributes
in class instances. They have the format:\<close>
text\<open>\<^center>\<open>\<open>@{name arg\<^sub>1 ... arg\<^sub>n\<^sub>-\<^sub>1} arg\<^sub>n\<close>\<close>\<close>
text\<open>Logically, they are defined as an identity in the last argument \<open>arg\<^sub>n\<close>; thus,
ontologically checked prior arguments \<open>arg\<^sub>1 ... arg\<^sub>n\<^sub>-\<^sub>1\<close> can be ignored during a proof
process; ontologically, they can be used to assure the traceability of, \<^eg>, semi-formal
assumptions throughout their way to formalisation and use in lemmas and proofs. \<close>
figure*[doc_termAq::figure,relative_width="50",src="''figures/doc-mod-term-aq.pdf''"]
\<open>Term-Antiquotations Referencing to Annotated Elements\<close>
text\<open>As shown in @{figure \<open>doc_termAq\<close>}, this feature of \<^isadof> substantially increases
the expressibility of links between the formal and the informal in \<^dof> documents.\<close>
text\<open> In the following, we describe a common scenario linking semi-formal assumptions and
formal ones:
@{boxed_theory_text [display]
\<open>
declare_reference*[e2::"definition"]
Assumption*[a1::"assumption", short_name="\<open>safe environment.\<close>"]
\<open>The system shall only be used in the temperature range from 0 to 60 degrees Celsius.
Formally, this is stated as follows in @{definition (unchecked) \<open>e2\<close>}.\<close>
definition*[e2, status=formal] safe_env :: "state \<Rightarrow> bool"
where "safe_env \<sigma> \<equiv> (temp \<sigma> \<in> {0 .. 60})"
theorem*[e3::"theorem"] safety_preservation::" @{assumption \<open>a1\<close>} (safe_env \<sigma>) \<Longrightarrow> ... "
\<close>}
\<close>
text\<open>Note that Isabelle procedes in a strict ``declaration-before-use''-manner, \<^ie> assumes
linear visibility on all references. This also holds for the declaration of ontological
references. In order to represent cyclic dependencies, it is therefore necessary to
start with the forward declaration \<^theory_text>\<open>declare_reference*\<close>. From there on, this reference
can be used in text, term, and code-contexts, albeit its definition appears textually later.
The corresponding freeform-formulation of this assumption can be explicitly referred in the
assumption of a theorem establishing the link. The \<^theory_text>\<open>theorem*\<close>-variant of the common
Isabelle/Isar \<^theory_text>\<open>theorem\<close>-command will in contrast to the latter not ignore \<open>\<open>a1\<close>\<close>,
\<^ie> parse just as string, but also validate it in the previous context.
Note that the \<^theory_text>\<open>declare_reference*\<close> command will appear in the \<^LaTeX> generated from this
document fragment. In order to avoid this, one has to enclose this command into the
document comments :\<close>
text\<open>\<^center>\<open>\<open>(*<*) ... (*>*)\<close>\<close>\<close>
section*[tech_onto::example]\<open>Writing Technical Reports in \<^boxed_theory_text>\<open>technical_report\<close>\<close>
@ -595,7 +648,7 @@ In the \<^pdf> output, these text-fragments were displayed verbatim.
section\<open>Style Guide\<close>
section\<open>Some Recommendations: A little Style Guide\<close>
text\<open>
The document generation of \<^isadof> is based on Isabelle's document generation framework,
using \<^LaTeX>{} as the underlying back-end. As Isabelle's document generation framework, it is
@ -613,11 +666,18 @@ text\<open> This is \emph{emphasized} and this is a
text\<open> This is *\<open>emphasized\<close> and this is a
citation @{cite "brucker.ea:isabelle-ontologies:2018"}.\<close>
\<close>}
The list of standard Isabelle document antiquotations, as well as their options and styles,
can be found in the Isabelle reference manual @{cite "wenzel:isabelle-isar:2020"}, also be found
under \<^url>\<open>https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2022/doc/isar-ref.pdf\<close>,
section 4.2.
Clearly, this is not always possible and, in fact, often \<^isadof> documents will contain
In practice, \<^isadof> documents with ambitious layout will contain a certain number of
\<^LaTeX>-commands, but this should be restricted to layout improvements that otherwise are (currently)
not possible. As far as possible, the use of \<^LaTeX>-commands should be restricted to the definition
of ontologies and document templates (see @{docitem (unchecked) \<open>isadof_ontologies\<close>}).
not possible. As far as possible, raw \<^LaTeX> should be restricted to the definition
of ontologies and macros (see @{docitem (unchecked) \<open>isadof_ontologies\<close>}). If raw
\<^LaTeX> commands can not be avoided, it is recommended to use the Isabelle document comment
\<^latex>\<open>\verb+\+\verb+<^latex>+\<close>\<open>\<open>argument\<close>\<close> to isolate these parts
(cf. \<^url>\<open>https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2022/doc/isar-ref.pdf\<close>).
Restricting the use of \<^LaTeX> has two advantages: first, \<^LaTeX> commands can circumvent the
consistency checks of \<^isadof> and, hence, only if no \<^LaTeX> commands are used, \<^isadof> can

146
Isabelle_DOF/thys/manual/M_04_RefMan.thy
View File

@ -43,7 +43,7 @@ text\<open>
\<^boxed_theory_text>\<open>text*\<close>, \<^boxed_theory_text>\<open>declare_reference*\<close>, \<^etc>.;
They allow for the annotation of text-elements with meta-information defined in ODL,
\<^item> the \<^isadof> library \<^theory>\<open>Isabelle_DOF.Isa_COL\<close> providing
ontological basic (documents) concepts as well as supporting infrastructure,
ontological basic (documents) concepts \<^bindex>\<open>ontology\<close> as well as supporting infrastructure,
\<^item> an infrastructure for ontology-specific \<^emph>\<open>layout definitions\<close>, exploiting this meta-information,
and
\<^item> an infrastructure for generic \<^emph>\<open>layout definitions\<close> for documents following, \<^eg>, the format
@ -51,27 +51,29 @@ text\<open>
\<close>
text\<open>
Similarly to Isabelle, which is based on a core logic \<^theory>\<open>Pure\<close> and then extended by libraries
to major systems like \<^verbatim>\<open>HOL\<close>, \<^isadof> has a generic core infrastructure \<^dof> and then
presents itself to users via major library extensions, which add domain-specific
system-extensions. Ontologies in \<^isadof> are not just a sequence of descriptions in
\<^isadof>'s Ontology Definition Language (ODL). Rather, they are themselves presented as integrated
to major systems like \<^verbatim>\<open>HOL\<close>, \<^isadof> has a generic core infrastructure \<^dof> and then presents
itself to users via major library extensions, which add domain-specific system-extensions.
Ontologies\<^bindex>\<open>ontology\<close> in \<^isadof> are not just a sequence of descriptions in \<^isadof>'s Ontology
Definition Language (ODL)\<^bindex>\<open>ODL\<close>. Rather, they are themselves presented as integrated
sources that provide textual descriptions, abbreviations, macro-support and even ML-code.
Conceptually, the library of \<^isadof> is currently organized as follows\<^footnote>\<open>The \<^emph>\<open>technical\<close>
organization is slightly different and shown in
@{technical (unchecked) \<open>infrastructure\<close>}.\<close>:
@{technical (unchecked) \<open>infrastructure\<close>}.\<close>
\<^bindex>\<open>COL\<close>\<^bindex>\<open>scholarly\_paper\<close>\<^bindex>\<open>technical\_report\<close> \<^bindex>\<open>CENELEC\<close>:
%
\<^latex>\<open>
\begin{center}
\begin{minipage}{.9\textwidth}\footnotesize
\dirtree{%
.1 COL\DTcomment{The Common Ontology Library}.
.2 scholarly\_paper\DTcomment{Scientific Papers}.
.3 technical\_report\DTcomment{Extended Papers}.
.3 technical\_report\DTcomment{Extended Papers, Technical Reports}.
.4 CENELEC\_50128\DTcomment{Papers according to CENELEC\_50128}.
.4 CC\_v3\_1\_R5\DTcomment{Papers according to Common Criteria}.
.4 \ldots.
}
\end{minipage}
\end{center}
\end{center}\<close>
These libraries not only provide ontological concepts, but also syntactic sugar in Isabelle's
command language Isar that is of major importance for users (and may be felt as \<^isadof> key
@ -95,27 +97,25 @@ text\<open>
section\<open>The Ontology Definition Language (ODL)\<close>
text\<open>
ODL shares some similarities with meta-modeling languages such as UML class
models: It builds upon concepts like class, inheritance, class-instances, attributes, references
to instances, and class-invariants. Some concepts like advanced type-checking, referencing to
formal entities of Isabelle, and monitors are due to its specific application in the
Isabelle context. Conceptually, ontologies specified in ODL consist of:
\<^item> \<^emph>\<open>document classes\<close> (\<^boxed_theory_text>\<open>doc_class\<close>) \<^index>\<open>doc\_class\<close> that describe concepts,
the keyword (\<^boxed_theory_text>\<open>onto_class\<close>) \<^index>\<open>onto\_class\<close> is accepted equally,
\<^item> an optional document base class expressing single inheritance
class extensions,
\<^item> \<^emph>\<open>attributes\<close> specific to document classes, where
\<^item> attributes are HOL-typed,
\<^item> attributes of instances of document elements are mutable,
\<^item> attributes can refer to other document classes, thus, document
classes must also be HOL-types (such attributes are called
\<^emph>\<open>links\<close>),
\<^item> attribute values were denoted by HOL-terms,
\<^item> a special link, the reference to a super-class, establishes an
\<^emph>\<open>is-a\<close> relation between classes,
\<^item> classes may refer to other classes via a regular expression in an
\<^emph>\<open>accepts\<close> clause, or via a list in a \<^emph>\<open>rejects\<close> clause,
\<^item> attributes may have default values in order to facilitate notation.
ODL shares some similarities with meta-modeling languages such as UML class
models: It builds upon concepts like class, inheritance, class-instances, attributes, references
to instances, and class-invariants. Some concepts like advanced type-checking, referencing to
formal entities of Isabelle, and monitors are due to its specific application in the
Isabelle context. Conceptually, ontologies specified in ODL consist of:
\<^item> \<^emph>\<open>document classes\<close> (\<^boxed_theory_text>\<open>doc_class\<close>) \<^index>\<open>doc\_class\<close> that describe concepts,
the keyword (\<^boxed_theory_text>\<open>onto_class\<close>) \<^index>\<open>onto\_class\<close> is accepted equally,
\<^item> an optional document base class expressing single inheritance class extensions,
\<^item> \<^emph>\<open>attributes\<close> specific to document classes, where
\<^item> attributes are HOL-typed,
\<^item> attributes of instances of document elements are mutable,
\<^item> attributes can refer to other document classes, thus, document
classes must also be HOL-types (such attributes are called \<^emph>\<open>links\<close>),
\<^item> attribute values were denoted by HOL-terms,
\<^item> a special link, the reference to a super-class, establishes an
\<^emph>\<open>is-a\<close> relation between classes,
\<^item> classes may refer to other classes via a regular expression in an
\<^emph>\<open>accepts\<close> clause, or via a list in a \<^emph>\<open>rejects\<close> clause,
\<^item> attributes may have default values in order to facilitate notation.
\<close>
text\<open>
@ -262,13 +262,14 @@ A document class\<^bindex>\<open>document class\<close> can be defined using the
text\<open>
\<^isadof> provides a default document representation (\<^ie>, content and layout of the generated
\<^pdf>) that only prints the main text, omitting all attributes. \<^isadof> provides the
\inlineltx|\newisadof[]{}|\<^index>\<open>newisadof@\<^boxed_latex>\<open>\newisadof\<close>\<close>\<^index>\<open>document class!PDF\<close>
\<^ltxinline>\<open>\newisadof[]{}\<close>\<^index>\<open>newisadof@\<^boxed_latex>\<open>\newisadof\<close>\<close>\<^index>\<open>document class!PDF\<close>
command for defining a dedicated layout for a document class in \<^LaTeX>. Such a document
class-specific \<^LaTeX>-definition can not only provide a specific layout (\<^eg>, a specific
highlighting, printing of certain attributes), it can also generate entries in the table of
contents or an index. Overall, the \inlineltx|\newisadof[]{}| command follows the structure
contents or an index. Overall, the \<^ltxinline>\<open>\newisadof[]{}\<close> command follows the structure
of the \<^boxed_theory_text>\<open>doc_class\<close>-command:
% bu: not embeddable macro: too many guillemots ...
\begin{ltx}[escapechar=ë]
\newisadof{ë\<open>class_id\<close>ë}[label=,type=, ë\<open>attribute_decl\<close>ë][1]{%
% ë\LaTeXë-definition of the document class representation
@ -282,17 +283,17 @@ text\<open>
needs to declare all attributes of the document class. Within the \<^LaTeX>-definition of the document
class representation, the identifier \<^boxed_latex>\<open>#1\<close> refers to the content of the main text of the
document class (written in \<^boxed_theory_text>\<open>\<open> ... \<close>\<close>) and the attributes can be referenced
by their name using the \inlineltx|\commandkey{...}|-command (see the documentation of the
by their name using the \<^ltxinline>\<open>\commandkey{...}\<close>-command (see the documentation of the
\<^LaTeX>-package ``keycommand''~@{cite "chervet:keycommand:2010"} for details). Usually, the
representations definition needs to be wrapped in a
\inlineltx|\begin{isarmarkup}...\end{isamarkup}|-environment, to ensure the correct context
\<^ltxinline>\<open>\begin{isarmarkup}...\end{isamarkup}\<close>-environment, to ensure the correct context
within Isabelle's \<^LaTeX>-setup.
% TODO:
% Clarify \newisadof signature: \newisadof[]{} vs \newisadof{}[]{}.
Moreover, \<^isadof> also provides the following two variants of \inlineltx|\newisadof{}[]{}|:
\<^item> \inlineltx|\renewisadof{}[]{}|\<^index>\<open>renewisadof@\<^boxed_latex>\<open>\renewisadof\<close>\<close> for re-defining
\<^item> \<^ltxinline>\<open>\renewisadof{}[]{}\<close>\<^index>\<open>renewisadof@\<^boxed_latex>\<open>\renewisadof\<close>\<close> for re-defining
(over-writing) an already defined command, and
\<^item> \inlineltx|\provideisadof{}[]{}|\<^index>\<open>provideisadof@\<^boxed_latex>\<open>\provideisadof\<close>\<close> for providing
\<^item> \<^ltxinline>\<open>\provideisadof{}[]{}\<close>\<^index>\<open>provideisadof@\<^boxed_latex>\<open>\provideisadof\<close>\<close> for providing
a definition if it is not yet defined.
\<close>
text\<open>
@ -451,9 +452,7 @@ term*\<open>@{B--test- \<open>b\<close>}\<close>
declare_reference*["text-elements-expls"::technical]
(*>*)
ML\<open>
\<close>
subsection*["subsec:onto-term-ctxt"::technical]\<open>Ontological Term-Contexts and their Management\<close>
text\<open>
\<^item> \<open>annotated_term_element\<close>
@ -634,6 +633,7 @@ text\<open>
\<^bindex>\<open>COL\<close> \<^footnote>\<open>contained in \<^theory>\<open>Isabelle_DOF.Isa_COL\<close>\<close>
that introduces several ontology concepts; its overall class-tree it provides looks as follows:
%
\<^latex>\<open>
\begin{center}
\begin{minipage}{.9\textwidth}\footnotesize
\dirtree{%
@ -649,7 +649,7 @@ text\<open>
.1 \ldots.
}
\end{minipage}
\end{center}\<close>
\end{center}\<close>\<close>
text\<open>
In particular it defines the super-class \<^typ>\<open>text_element\<close>: the root of all
@ -709,6 +709,7 @@ text\<open> The \<^verbatim>\<open>scholarly_paper\<close> ontology is oriented
mathematics, informatics, natural sciences, technology, or engineering.
It extends \<^verbatim>\<open>COL\<close> by the following concepts:
\<^latex>\<open>
\begin{center}
\begin{minipage}{.9\textwidth}\footnotesize
\dirtree{%
@ -733,7 +734,7 @@ It extends \<^verbatim>\<open>COL\<close> by the following concepts:
.5 scholarly\_paper.corollary\DTcomment{Freeform}.
.5 scholarly\_paper.math\_example\DTcomment{Freeform}.
.5 scholarly\_paper.math\_semiformal\DTcomment{Freeform}.
.5 scholarly\_paper.math\_formal\DTcomment{Formal(=Checked) Content}.
.5 scholarly\_paper.math\_formal\DTcomment{Formal Content}.
.6 scholarly\_paper.assertion\DTcomment{Assertions}.
.4 scholarly\_paper.tech\_example\DTcomment{...}.
.4 scholarly\_paper.math\_motivation\DTcomment{...}.
@ -749,10 +750,10 @@ It extends \<^verbatim>\<open>COL\<close> by the following concepts:
}
\end{minipage}
\end{center}
\<close>
(*
TODO: There are some slight problems in the hierarchy ...
*)
\<close>\<close>
text\<open>Recall that \<^emph>\<open>Formal Content\<close> means \<^emph>\<open>machine-checked, validated content\<close>.\<close>
text\<open>A pivotal abstract class in the hierarchy is:
@{boxed_theory_text [display]
@ -789,9 +790,12 @@ of the \<^isadof> language:
\<^item> \<open>derived_text_elements \<close> :
\<^rail>\<open>
( ( @@{command "author*"}
| @@{command "abstract*"}
| @@{command "Definition*"} | @@{command "Lemma*"} | @@{command "Theorem*"}
( ( @@{command "author*"} | @@{command "abstract*"}
| @@{command "Definition*"} | @@{command "Lemma*"} | @@{command "Theorem*"}
| @@{command "Proposition*"}| @@{command "Proof*"} | @@{command "Example*"}
| @@{command "Premise*"} | @@{command "Assumption*"} | @@{command "Hypothesis*"}
| @@{command "Corollary*"} | @@{command "Consequence*"}| @@{command "Assertion*"}
| @@{command "Conclusion*"}
)
\<newline>
'[' meta_args ']' '\<open>' text '\<close>'
@ -800,6 +804,9 @@ of the \<^isadof> language:
\<close>
\<close>
text\<open>Usually, command macros for text elements will assign the generated instance
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
@ -876,12 +883,14 @@ ML\<open>writeln (DOF_core.print_doc_class_tree
orelse String.isPrefix "Isa_COL" l *))
toLaTeX)\<close>
(*>*)
text\<open> The \<^verbatim>\<open>technical_report\<close> ontology in \<^theory>\<open>Isabelle_DOF.technical_report\<close> extends
\<^verbatim>\<open>scholarly_paper\<close> by concepts needed
text\<open> The \<^verbatim>\<open>technical_report\<close> \<^bindex>\<open>technical\_report\<close> ontology in
\<^theory>\<open>Isabelle_DOF.technical_report\<close> extends
\<^verbatim>\<open>scholarly_paper\<close> \<^bindex>\<open>scholarly\_paper\<close> \<^bindex>\<open>ontology\<close> by concepts needed
for larger reports in the domain of mathematics and engineering. The concepts are fairly
high-level arranged at root-class level,
%
\<^latex>\<open>
\begin{center}
\begin{minipage}{.9\textwidth}\footnotesize
\dirtree{%
@ -900,7 +909,7 @@ high-level arranged at root-class level,
}
\end{minipage}
\end{center}
\<close>
\<close>\<close>
@ -931,21 +940,21 @@ end
Second, given an implementation of the functionality of the new keyword (implemented in SML),
the new keyword needs to be registered, together with its parser, as outer syntax:
\<^latex>\<open>
\begin{sml}
val _ =
Outer_Syntax.command ("section*", <@>{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 1))
{markdown = false} )));
\end{sml}
\end{sml}\<close>
\<close>
text\<open>
Finally, for the document generation, a new dispatcher has to be defined in \<^LaTeX>---this is
mandatory, otherwise the document generation will break. These dispatchers always follow the same
schemata:
\<^latex>\<open>
\begin{ltx}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: section*-dispatcher
@ -953,17 +962,17 @@ schemata:
% end: section*-dispatcher
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{ltx}
\<close>
After the definition of the dispatcher, one can, optionally, define a custom representation
using the \<^boxed_latex>\<open>\newisadof\<close>-command, as introduced in the previous section:
\<^latex>\<open>
\begin{ltx}
\newisadof{section}[label=,type=][1]{%
\isamarkupfalse%
\isamarkupsection{#1}\label{\commandkey{label}}%
\isamarkuptrue%
}
\end{ltx}
\end{ltx}\<close>
\<close>
@ -1300,6 +1309,7 @@ text\<open>
Technically, ontologies\<^index>\<open>ontology!directory structure\<close> are stored in a directory
\<^boxed_bash>\<open>ontologies\<close> and consist of an Isabelle theory file and a \<^LaTeX>-style file:
%
\<^latex>\<open>
\begin{center}
\begin{minipage}{.9\textwidth}\footnotesize
\dirtree{%
@ -1314,7 +1324,7 @@ text\<open>
.4 DOF-technical\_report.sty.
}
\end{minipage}
\end{center}
\end{center}\<close>
\<close>
text\<open>
Developing a new ontology ``\<^boxed_bash>\<open>foo\<close>'' requires the
@ -1334,6 +1344,7 @@ text\<open>
etc.) of the generated documents. Document-templates
are stored in a directory
\<^path>\<open>src/document-templates\<close>:\<^index>\<open>document template!directory structure\<close>
\<^latex>\<open>
\begin{center}
\begin{minipage}{.9\textwidth}\footnotesize
\dirtree{%
@ -1345,7 +1356,7 @@ text\<open>
.3 root-scrreprt.tex.
}
\end{minipage}
\end{center}
\end{center}\<close>
\<close>
text\<open>
@ -1380,6 +1391,7 @@ text\<open>
adding a new template, call the \<^boxed_bash>\<open>install\<close> script (see \<^technical>\<open>infrastructure\<close>).
The common structure of an \<^isadof> document template looks as follows:
\<^latex>\<open>
\begin{ltx}[escapechar=ë, numbers=left,numberstyle=\tiny,xleftmargin=5mm]
\documentclass{article} % The LaTeX-class of your template ë\label{lst:dc}ë
%% The following part is (mostly) required by Isabelle/DOF, do not modify
@ -1404,7 +1416,7 @@ text\<open>
\maketitle\input{session}
\IfFileExists{root.bib}{\bibliography{root}}{}
\end{document}
\end{ltx}
\end{ltx}\<close>
\<close>
subsection\<open>Tips, Tricks, and Known Limitations\<close>
@ -1470,7 +1482,7 @@ text\<open>
information into an \<^boxed_latex>\<open>\author\<close> and a \<^boxed_latex>\<open>\institution\<close> statement, each of
which containing the information for all authors. The collection of the author information
is provided by the following \<^LaTeX>-code:
\<^latex>\<open>
\begin{ltx}
\def\dof@author{}%
\newcommand{\DOFauthor}{\author{\dof@author}}
@ -1485,7 +1497,7 @@ text\<open>
\leftadd\dof@author{\protect\and #1}%
}
}
\end{ltx}
\end{ltx}\<close>
The new command \<^boxed_latex>\<open>\addauthor\<close> and a similarly defined command \<^boxed_latex>\<open>\addaffiliation\<close>
can now be used in the definition of the representation of the concept
@ -1494,6 +1506,7 @@ job's aux-file. The intermediate step of writing this information into the job's
as the author and affiliation information is required right at the beginning of the document
while \<^isadof> allows defining authors at any place within a document:
\<^latex>\<open>
\begin{ltx}
\provideisadof{text.scholarly_paper.author}%
[label=,type=%
@ -1517,19 +1530,18 @@ while \<^isadof> allows defining authors at any place within a document:
\string\addaffiliation{\dof@a\\\string\email{%
\commandkey{scholarly_paper.author.email}}}}%
}
\end{ltx}
\end{ltx}\<close>
Finally, the collected information is used in the \<^boxed_latex>\<open>\author\<close> command using the
\<^boxed_latex>\<open>AtBeginDocument\<close>-hook:
\<^latex>\<open>
\begin{ltx}
\newcommand{\DOFauthor}{\author{\dof@author}}
\AtBeginDocument{%
\DOFauthor
}
\end{ltx}
\end{ltx}\<close>
\<close>
@ -1538,15 +1550,15 @@ subsubsection\<open>Restricting the Use of Ontologies to Specific Templates\<clo
text\<open>
As ontology representations might rely on features only provided by certain templates
(\<^LaTeX>-classes), authors of ontology representations might restrict their use to
specific classes. This can, \<^eg>, be done using the \inlineltx|\@ifclassloaded{}| command:
specific classes. This can, \<^eg>, be done using the \<^ltxinline>\<open>\@ifclassloaded{}\<close> command:
\<^latex>\<open>
\begin{ltx}
\@ifclassloaded{llncs}{}%
{% LLNCS class not loaded
\PackageError{DOF-scholarly_paper}
{Scholarly Paper only supports LNCS as document class.}{}\stop%
}
\end{ltx}
\end{ltx}\<close>
For a real-world example testing for multiple classes, see
\<^file>\<open>../../ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close>: