Improved LaTeX support for Lemma*, Theorem*, Definition*, etc.

This commit is contained in:
Achim D. Brucker 2023-03-29 22:21:22 +01:00
parent 91ff9c67af
commit 320614004e
3 changed files with 52 additions and 364 deletions

View File

@ -81,11 +81,9 @@ text\<open>... which makes it possible to refer in a freeform definition to its
which will appear textually later. With this pragmatics, an "out-of-order-presentation"
can be achieved within \<^theory>\<open>Isabelle_DOF.scholarly_paper\<close> for the most common cases.\<close>
(*<*) (*LATEX FAILS *)
Definition*[e1bis::"definition", short_name="\<open>Nice lemma.\<close>"]
\<open>Lorem ipsum dolor sit amet, ...
This is formally defined as follows in @{definition (unchecked) "e1bisbis"}\<close>
(*>*)
definition*[e1bisbis, status=formal] e :: int where "e = 2"
section\<open>Tests for Theorems, Assertions, Assumptions, Hypothesis, etc.\<close>
@ -105,9 +103,10 @@ Theorem*[e2]\<open>... suspendisse non arcu malesuada mollis, nibh morbi, ... \<
theorem*[e2bis::"theorem", status=formal] f : "e = 1+1" unfolding e_def by simp
(*<*) (* @{theorem "e2bis"} breaks LaTeX generation ... *)
Lemma*[e3,level="Some 2"]
\<open>... phasellus amet id massa nunc, pede suscipit repellendus, ... @{theorem "e2bis"} \<close>
(*<*)(*LATEX FAILS *)
(*>*)
Proof*[d10, short_name="\<open>Induction over Tinea pedis.\<close>"]\<open>Freeform Proof\<close>
lemma*[dfgd::"lemma"] q: "All (\<lambda>x. X \<and> Y \<longrightarrow> True)" oops
@ -191,7 +190,5 @@ text*[tt10::scholarly_paper.tech_example]\<open>Lectus accumsan velit ultrices,
text*[tu8::scholarly_paper.tech_code] \<open>Lectus accumsan velit ultrices, ...\<close>
text*[tu27::scholarly_paper.engineering_content]\<open>Lectus accumsan velit ultrices, ...\<close>
text*[tu14::scholarly_paper.evaluation ]\<open>Lectus accumsan velit ultrices, ...\<close>
(*>*)
end
(*>*)

View File

@ -1,38 +0,0 @@
%% Copyright (C) 2020 The University of Paris-Saclay
%% 2020 The University of Exeter
%%
%% License:
%% This program can be redistributed and/or modified under the terms
%% of the LaTeX Project Public License Distributed from CTAN
%% archives in directory macros/latex/base/lppl.txt; either
%% version 1.3c of the License, or (at your option) any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-scholarly_paper-thm}
[00/00/0000 Document-Type Support Framework for Isabelle (LNCS).]
\RequirePackage{amsthm}
\newtheorem{example}{Example}
\newtheorem{assumption}{Assumption}
\newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem}
%\newtheorem{assertion}{Assumption} %% Hack
%Assertion*
%Proposition*
%Premise*
%Corollary*
%Consequence*
%Conclusion*
%Assumption*
%Hypothesis*
%Proof* -- A bit special ? Own local format ?

View File

@ -31,13 +31,13 @@
\@ifclassloaded{llncs}%
{}%
{%
\RequirePackage{amsthm}
\@ifclassloaded{scrartcl}%
{%
\newcommand{\institute}[1]{}%
\newcommand{\inst}[1]{}%
\newcommand{\orcidID}[1]{}%
\newcommand{\email}[1]{}%
\RequirePackage{DOF-scholarly_paper-thm}%
}%
{%
\@ifclassloaded{lipics-v2021}%
@ -165,22 +165,47 @@
\end{isamarkuptext}%
}
\newtheorem{axiom}{Axiom}
\newtheorem{ruleX}{Rule} % apparent name-clash with s th from libraries...
\newtheorem{assertion}{Assertion}
% \newcommand{\formalMathStmt[label, mcc, ]
% end: scholarly_paper.abstract
% "defn" | "axm" | "theom" | "lemm" | "corr" | "prpo" | "rulE" | "assn" | "hypt" | "assm" | "prms" | "cons" |
% "conc_stmt" |"prf_stmt" | "expl_stmt" |"rmrk" | "notn" | "tmgy" |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\RequirePackage{amsthm}
%\newtheorem{example}{Example}
%\newtheorem{assumption}{Assumption}
%\newtheorem{definition}{Definition}
%\newtheorem{theorem}{Theorem}
\newtheorem{defn}{Definition}
\NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newtheorem{axm}{Axiom}
\newtheorem{theom}{Theorem}
\NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newtheorem{lemm}{Lemma}
\NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newtheorem{corr}{Corollary}
\NewEnviron{isamarkupCorollary*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newtheorem{prpo}{Proposition}
\NewEnviron{isamarkupProposition*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newtheorem{rulE}{Rule}
\newtheorem{assn}{Assertion}
\NewEnviron{isamarkupAssertion*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newtheorem{hypt}{Hypothesis}
\NewEnviron{isamarkupHypothesis*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newtheorem{assm}{Assumption}
\NewEnviron{isamarkupAssumption*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newtheorem{prms}{Premise}
\NewEnviron{isamarkupPremise*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newtheorem{cons}{Consequence}
\NewEnviron{isamarkupConsequence*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newtheorem{conc_stmt}{Conclusion}
\NewEnviron{isamarkupConclusion*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newtheorem{prf_stmt}{Proof}
\NewEnviron{isamarkupProof*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newtheorem{expl_stmt}{Example}
\NewEnviron{isamarkupExample*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newtheorem{rmrk}{Remark}
\newtheorem{notn}{Notation}
\newtheorem{tmgy}{Terminology}
\newisadof{text.scholarly_paper.math_content}%
[label=,type=%
, scholarly_paper.math_content.short_name ={} % {} or \relax
, scholarly_paper.math_content.mcc = % "defn" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn" | "assm"
, 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 =%
@ -193,317 +218,20 @@
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{defn}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
{\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{definition}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{axm}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{axiom} \label{\commandkey{label}} #1 \end{axiom} }
{\begin{axiom} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{axiom}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{theom}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{theorem} \label{\commandkey{label}} #1 \end{theorem} }
{\begin{theorem} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{theorem}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{lemm}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
{\begin{lemma} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{lemma}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{expl_stmt}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
{\begin{example} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{example}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{corr}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{corrollary} \label{\commandkey{label}} #1 \end{corrollary} }
{\begin{corrollary} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{corrollary}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{prpo}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{property} \label{\commandkey{label}} #1 \end{property} }
{\begin{property} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{property}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rulE}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{ruleX} \label{\commandkey{label}} #1 \end{ruleX} }
{\begin{ruleX} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{ruleX}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rmrk}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{remark} \label{\commandkey{label}} #1 \end{remark} }
{\begin{remark} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{remark}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{assn}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{assertion} \label{\commandkey{label}} #1 \end{assertion} }
{\begin{assertion} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{assertion}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{assm}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{assumption} \label{\commandkey{label}} #1 \end{assumption} }
{\begin{assumption} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{assumption}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{notn}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{notation} \label{\commandkey{label}} #1 \end{notation} }
{\begin{notation} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{notation}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{tmgy}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{terminology} \label{\commandkey{label}} #1 \end{terminology} }
{\begin{terminology} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{terminology}}
}%
}%
{%
\typeout{Internal error: enumeration out of sync with ontology scholarly-paper.}
}%
}%
}%
}%
}%
}%
}%
}%
}%
}%
}%
}%
}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{%
\begin{\commandkey{scholarly_paper.math_content.mcc}}\label{\commandkey{label}}
#1
\end{\commandkey{scholarly_paper.math_content.mcc}}
}{%
\begin{\commandkey{scholarly_paper.math_content.mcc}}[\commandkey{scholarly_paper.math_content.short_name}]\label{\commandkey{label}}
#1
\end{\commandkey{scholarly_paper.math_content.mcc}}
}
\end{isamarkuptext}%
}
% end: scholarly_paper.math_content
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Besser: Einfach durchreichen wg Vererbung !
\newisadof{text.scholarly_paper.math_example}%
[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 =%
, scholarly_paper.technical.definition_list =%
, scholarly_paper.technical.status =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{expl}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
{\begin{example} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{example}}
}{%
#1%
}%
\end{isamarkuptext}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newisadof{text.scholarly_paper.definition}%
[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 =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{defn}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
{\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{definition}}
}{%
#1%
}%
\end{isamarkuptext}%
}
% An experiment in inheritance of the default behaviour.
% \newisadof{text.scholarly_paper.definition}%
% [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 =%
% , scholarly_paper.technical.definition_list =%
% , scholarly_paper.technical.status =%
% ]
% [1]
% {%
% \cscommand{text.scholarly_paper.math_content}%
% [label=\commandkey{label},type=\commandkey{type}%
% , scholarly_paper.math_content.short_name =\commandkey{scholarly_paper.math_content.short_name}%
% , scholarly_paper.math_content.mcc =\commandkey{scholarly_paper.math_content.mcc}%
% , Isa_COL.text_element.level =\commandkey{Isa_COL.text_element.level}%
% , Isa_COL.text_element.referentiable =\commandkey{Isa_COL.text_element.referentiable}%
% , Isa_COL.text_element.variants =\commandkey{Isa_COL.text_element.variants}%
% , scholarly_paper.text_section.main_author =\commandkey{scholarly_paper.text_section.main_author}%
% , scholarly_paper.text_section.fixme_list =\commandkey{scholarly_paper.text_section.fixme_list}%
% , scholarly_paper.technical.definition_list =\commandkey{scholarly_paper.technical.definition_list}%
% , scholarly_paper.technical.status =\commandkey{scholarly_paper.technical.status}%
% ]
% {#1}%
% }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Besser: Einfach durchreichen wg Vererbung !
\NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text.scholarly_paper.lemma},#1]{\BODY}}
\newisadof{text.scholarly_paper.lemma}%
[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 =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{lem}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
{\begin{lemma} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{lemma}}
}{%
#1%
}%
\end{isamarkuptext}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Besser: Einfach durchreichen wg Vererbung !
\NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text.scholarly_paper.theorem},#1]{\BODY}}
\newisadof{text.scholarly_paper.theorem}%
[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 =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{thm}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{theorem} \label{\commandkey{label}} #1 \end{theorem} }
{\begin{theorem} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{theorem}}
}{%
#1%
}%
\end{isamarkuptext}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Generic Example. Different inheritance hierachy.
\newisadof{text.scholarly_paper.example}%
[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.example.status =%
, scholarly_paper.example.short_name =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.example.status}}{semiformal}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.example.short_name}} {} }
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
{\begin{example} [\commandkey{scholarly_paper.example.short_name}] %
\label{\commandkey{label}} #1 %
\end{example}} %
}%
{%
#1%
}%
\end{isamarkuptext}%
}
%% Miscellaneous
\usepackage{xspace}
@ -511,3 +239,4 @@
\newcommand{\eg}{e.\,g.\xspace}
\newcommand{\etc}{etc}