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

Merge branch 'main' into idir-remarks
ci/woodpecker/push/build Pipeline failed Details
ci/woodpecker/pr/build Pipeline failed Details

This commit is contained in:
Achim D. Brucker 2023-05-15 06:34:34 +00:00
parent 9cc03c0816 bbac65e233
commit 1986d0bcbd
37 changed files with 554 additions and 746 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.woodpecker/build.yml
View File

@ -12,6 +12,7 @@ pipeline:
- echo "ISABELLE_PDFLATEX=\"$LATEX --file-line-error\"" >> $ISABELLE_HOME_USER/etc/settings
- isabelle build -x HOL-Proofs -x Isabelle_DOF-Proofs -D . -o browser_info
- if [ "$LATEX" = "lualatex" ]; then isabelle build -o 'timeout_scale=2' -D . -o browser_info; else echo "Skipping Isabelle_DOF-Proofs for pdflatex build."; fi
- find . -name 'root.tex' -prune -o -name 'output' -type f | xargs latexmk -$LATEX -cd -quiet -Werror
- isabelle components -u .
- isabelle dof_mkroot -q DOF_test
- isabelle build -D DOF_test

59
Isabelle_DOF-Example-I/IsaDofApplications.thy
View File

@ -206,7 +206,7 @@ The current system framework offers moreover the following features:
the most prominent and deeply integrated system component.
\<close>
figure*[architecture::figure,relative_width="100",src="''figures/isabelle-architecture''"]\<open>
figure*[architecture::figure,relative_width="100",file_src="''figures/isabelle-architecture.pdf''"]\<open>
The system architecture of Isabelle (left-hand side) and the
asynchronous communication between the Isabelle system and
the IDE (right-hand side). \<close>
@ -315,7 +315,7 @@ Isabelle users to Isabelle users only. Of course, such references can be added e
represent a particular strength of \<^isadof>.\<close>
text*["paper_onto_core"::float,
caption="\<open>The core of the ontology definition for writing scholarly papers.\<close>"]
main_caption="\<open>The core of the ontology definition for writing scholarly papers.\<close>"]
\<open>@{boxed_theory_text [display]\<open>
doc_class title =
short_title :: "string option" <= None
@ -350,7 +350,7 @@ The translation of its content to, \<^eg>, Springer's \<^LaTeX> setup for the Le
Science Series, as required by many scientific conferences, is mostly straight-forward.
\<^vs>\<open>-0.8cm\<close>\<close>
figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"]
figure*[fig1::figure,relative_width="95",file_src="''figures/Dogfood-Intro.png''"]
\<open> Ouroboros I: This paper from inside \<^dots> \<close>
(*<*)declare_reference*[paper_onto_sections::float](*>*)
@ -385,7 +385,7 @@ of the scope of this paper.
We proceed more or less conventionally by the subsequent sections (@{float (unchecked)\<open>paper_onto_sections\<close>})\<close>
text*["paper_onto_sections"::float,
caption = "''Various types of sections of a scholarly papers.''"]\<open>
main_caption = "''Various types of sections of a scholarly papers.''"]\<open>
@{boxed_theory_text [display]\<open>
doc_class example = text_section +
comment :: string
@ -403,7 +403,7 @@ doc_class bibliography =
text\<open>... and finish with a monitor class definition that enforces a textual ordering
in the document core by a regular expression (@{float (unchecked) "paper_onto_monitor"}).\<close>
text*["paper_onto_monitor"::float,
caption = "''A monitor for the scholarly paper ontology.''"]\<open>
main_caption = "''A monitor for the scholarly paper ontology.''"]\<open>
@{boxed_theory_text [display]\<open>
doc_class article =
trace :: "(title + subtitle + author+ abstract +
@ -433,7 +433,7 @@ use fractions or even mathematical reals. This must be counterbalanced by syntac
and semantic convenience. Choosing the mathematical reals, \<^eg>, would have the drawback that
attribute evaluation could be substantially more complicated.\<close>
figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figures/Dogfood-figures''"]
figure*[fig_figures::figure,relative_width="85",file_src="''figures/Dogfood-figures.png''"]
\<open> Ouroboros II: figures \<^dots> \<close>
text\<open> The document class \<^theory_text>\<open>figure\<close> --- supported by the \<^isadof> text command
@ -462,7 +462,7 @@ where for organizational reasons the execution of an exam takes place in facilit
where the author of the exam is not expected to be physically present.
Furthermore, we assume a simple grade system (thus, some calculation is required). \<close>
text*["onto_exam"::float,
caption = "''The core of the ontology modeling math exams.''"]\<open>
main_caption = "''The core of the ontology modeling math exams.''"]\<open>
@{boxed_theory_text [display]\<open>
doc_class Author = ...
datatype Subject = algebra | geometry | statistical
@ -495,7 +495,7 @@ assume familiarity of the students with Isabelle (\<^theory_text>\<open>term\<cl
parse-able and type-checkable entity), we basically model a derivation as a sequence of strings
(see @{float (unchecked)"onto_questions"}).\<close>
text*["onto_questions"::float,
caption = "''An exam can contain different types of questions.''"]\<open>
main_caption = "''An exam can contain different types of questions.''"]\<open>
@{boxed_theory_text [display]\<open>
doc_class Answer_Formal_Step = Exam_item +
justification :: string
@ -530,7 +530,7 @@ question by a sample proof validated by Isabelle (see @{float (unchecked) "onto_
In our scenario this sample proofs are completely \<^emph>\<open>intern\<close>, \<^ie>, not exposed to the
students but just additional material for the internal review process of the exam.\<close>
text*["onto_exam_monitor"::float,
caption = "''Validating exams.''"]\<open>
main_caption = "''Validating exams.''"]\<open>
@{boxed_theory_text [display]\<open>
doc_class Validation =
tests :: "term list" <="[]"
@ -555,9 +555,9 @@ exam-sheets with multiple-choice and/or free-response elements
help of the latter, it is possible that students write in a browser a formal mathematical
derivation---as part of an algebra exercise, for example---which is submitted to the examiners
electronically. \<close>
figure*[fig_qcm::figure,spawn_columns=False,
relative_width="90",src="''figures/InteractiveMathSheet''"]
\<open> A Generated QCM Fragment \<^dots> \<close>
figure*[fig_qcm::figure,
relative_width="90",file_src="''figures/InteractiveMathSheet.png''"]
\<open>A Generated QCM Fragment \<^dots> \<close>
subsection*[cenelec_onto::example]\<open> The Certification Scenario following CENELEC \<close>
text\<open> Documents to be provided in formal certifications (such as CENELEC
@ -583,7 +583,7 @@ text\<open> In the sequel, we present a simplified version of an ontological mod
case-study~ @{cite "bezzecchi.ea:making:2018"}. We start with an introduction of the concept of requirement
(see @{float (unchecked) "conceptual"}). \<close>
text*["conceptual"::float,
caption = "''Modeling requirements.''"]\<open>
main_caption = "''Modeling requirements.''"]\<open>
@{boxed_theory_text [display]\<open>
doc_class requirement = long_name :: "string option"
@ -641,18 +641,20 @@ Clicking on a document class identifier permits to hyperlink into the correspond
class definition (\<^unchecked_label>\<open>fig:Dogfood-IV-jumpInDocCLass\<close>; hovering over an attribute-definition
(which is qualified in order to disambiguate; \<^unchecked_label>\<open>fig:Dogfood-V-attribute\<close>).
\<close>
side_by_side_figure*["text-elements"::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''",
caption2="''Exploring the class of a text element.''",relative_width2="47",
src2="''figures/Dogfood-III-bgnd-text_section''"]\<open> Exploring text elements. \<close>
side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-jumpInDocCLass''",
caption="''Hyperlink to Class-Definition.''",relative_width="48",
src="''figures/Dogfood-IV-jumpInDocCLass''",anchor2="''fig:Dogfood-V-attribute''",
caption2="''Exploring an attribute.''",relative_width2="47",
src2="''figures/Dogfood-III-bgnd-text_section''"]\<open> Hyperlinks.\<close>
text*["text-elements"::float,
main_caption="\<open>Exploring text elements.\<close>"]
\<open>
@{fig_content (width=48, caption="Exploring a Reference of a Text-Element.") "figures/Dogfood-II-bgnd1.png"
}\<^hfill>@{fig_content (width=47, caption="Exploring the class of a text element.") "figures/Dogfood-III-bgnd-text_section.png"}
\<close>
text*["hyperlinks"::float,
main_caption="\<open>Hyperlinks.\<close>"]
\<open>
@{fig_content (width=48, caption="Hyperlink to Class-Definition.") "figures/Dogfood-IV-jumpInDocCLass.png"
}\<^hfill>@{fig_content (width=47, caption="Exploring an attribute.") "figures/Dogfood-III-bgnd-text_section.png"}
\<close>
(*<*)declare_reference*["figDogfoodVIlinkappl"::figure](*>*)
@ -661,8 +663,9 @@ antiquotation \<^theory_text>\<open>@{example ...}\<close> refers to the corresp
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. \<close>
figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"]
figure*[figDogfoodVIlinkappl::figure,relative_width="80",file_src="''figures/Dogfood-V-attribute.png''"]
\<open> Exploring an attribute (hyperlinked to the class). \<close>
subsection*[cenelec_pide::example]\<open> CENELEC \<close>
(*<*)declare_reference*[figfig3::figure](*>*)
text\<open> The corresponding view in @{figure (unchecked) \<open>figfig3\<close>} shows core part of a document,
@ -670,7 +673,7 @@ coherent to the @{example \<open>cenelec_onto\<close>}. The first sample shows s
@{cite "wenzel:isabelle-isar:2017"} into formal entities of a theory. This way, the informal parts
of a document get ``formal content'' and become more robust under change.\<close>
figure*[figfig3::figure,relative_width="80",src="''figures/antiquotations-PIDE''"]
figure*[figfig3::figure,relative_width="80",file_src="''figures/antiquotations-PIDE.png''"]
\<open> Standard antiquotations referring to theory elements.\<close>
(*<*)declare_reference*[figfig5::figure] (*>*)
@ -680,9 +683,9 @@ has the consequence that a certain calculation must be executed sufficiently fas
device. This condition can not be established inside the formal theory but has to be
checked by system integration tests.\<close>
figure*[figfig5::figure, relative_width="80", src="''figures/srac-definition''"]
figure*[figfig5::figure, relative_width="80", file_src="''figures/srac-definition.png''"]
\<open> Defining a SRAC reference \<^dots> \<close>
figure*[figfig7::figure, relative_width="80", src="''figures/srac-as-es-application''"]
figure*[figfig7::figure, relative_width="80", file_src="''figures/srac-as-es-application.png''"]
\<open> Using a SRAC as EC document reference. \<close>
text\<open> Now we reference in @{figure \<open>figfig7\<close>} this safety-related condition;

3
Isabelle_DOF-Example-I/document/preamble.tex
View File

@ -22,9 +22,6 @@
\usepackage{listings}
\usepackage{lstisadof-manual}
\usepackage[caption]{subfig}
\usepackage[size=footnotesize]{caption}
\providecommand{\isactrlemph}[1]{\emph{#1}}
\usepackage[LNCS,
orcidicon,

4
Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy
View File

@ -126,7 +126,7 @@ text\<open>
subsection\<open>Capturing ``System Architecture.''\<close>
figure*["three-phase"::figure,relative_width="70",src="''figures/three-phase-odo''"]
figure*["three-phase"::figure,relative_width="70",file_src="''figures/three-phase-odo.pdf''"]
\<open>An odometer with three sensors \<open>C1\<close>, \<open>C2\<close>, and \<open>C3\<close>.\<close>
text\<open>
@ -162,7 +162,7 @@ text\<open>
of the measuring device, and the required format and precision of the measurements of the odometry
function as represented (see @{figure (unchecked) "df-numerics-encshaft"}).\<close>
figure*["df-numerics-encshaft"::figure,relative_width="76",src="''figures/df-numerics-encshaft''"]
figure*["df-numerics-encshaft"::figure,relative_width="76",file_src="''figures/df-numerics-encshaft.png''"]
\<open>Real distance vs. discrete distance vs. shaft-encoder sequence\<close>

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

@ -79,7 +79,7 @@ text\<open> \<^vs>\<open>-0.5cm\<close>
maximum of formal content which makes this text re-checkable at each load and easier
maintainable. \<close>
figure*[architecture::figure,relative_width="70",src="''figures/isabelle-architecture''"]\<open>
figure*[architecture::figure,relative_width="70",file_src="''figures/isabelle-architecture.pdf''"]\<open>
The system architecture of Isabelle (left-hand side) and the asynchronous communication
between the Isabelle system and the IDE (right-hand side). \<close>
@ -148,7 +148,7 @@ text\<open> \<open>*\<open>This is a text.\<close>\<close>\<close>
text\<open>and displayed in the Isabelle/jEdit front-end at the sceen by:\<close>
figure*[fig2::figure, relative_width="60", placement="pl_h", src="''figures/text-element''"]
figure*[fig2::figure, relative_width="60", file_src="''figures/text-element.pdf''"]
\<open>A text-element as presented in Isabelle/jEdit.\<close>
text\<open>The text-commands, ML-commands (and in principle any other command) can be seen as
@ -807,18 +807,13 @@ text\<open> They reflect the Pure logic depicted in a number of presentations s
Notated as logical inference rules, these operations were presented as follows:
\<close>
side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-kernel1''",
caption="''Pure Kernel Inference Rules I ''",relative_width="48",
src="''figures/pure-inferences-I''",anchor2="''fig-kernel2''",
caption2="''Pure Kernel Inference Rules II''",relative_width2="47",
src2="''figures/pure-inferences-II''"]\<open> \<close>
text*["text-elements"::float,
main_caption="\<open>Kernel Inference Rules.\<close>"]
\<open>
@{fig_content (width=48, caption="Pure Kernel Inference Rules I.") "figures/pure-inferences-I.pdf"
}\<^hfill>@{fig_content (width=47, caption="Pure Kernel Inference Rules II.") "figures/pure-inferences-II.pdf"}
\<close>
(*
figure*[kir1::figure,relative_width="100",src="''figures/pure-inferences-I''"]
\<open> Pure Kernel Inference Rules I.\<close>
figure*[kir2::figure,relative_width="100",src="''figures/pure-inferences-II''"]
\<open> Pure Kernel Inference Rules II. \<close>
*)
text\<open>Note that the transfer rule:
\[
@ -1440,7 +1435,7 @@ text\<open>The document model forsees a number of text files, which are organize
secondary formats can be \<^verbatim>\<open>.sty\<close>,\<^verbatim>\<open>.tex\<close>, \<^verbatim>\<open>.png\<close>, \<^verbatim>\<open>.pdf\<close>, or other files processed
by Isabelle and listed in a configuration processed by the build system.\<close>
figure*[fig3::figure, relative_width="100",src="''figures/document-model''"]
figure*[fig3::figure, relative_width="100",file_src="''figures/document-model.pdf''"]
\<open>A Theory-Graph in the Document Model\<close>
text\<open>A \<^verbatim>\<open>.thy\<close> file consists of a \<^emph>\<open>header\<close>, a \<^emph>\<open>context-definition\<close> and
@ -1535,7 +1530,7 @@ text\<open> ... uses the antiquotation @{ML "@{here}"} to infer from the system
of itself in the global document, converts it to markup (a string-representation of it) and sends
it via the usual @{ML "writeln"} to the interface. \<close>
figure*[hyplinkout::figure,relative_width="40",src="''figures/markup-demo''"]
figure*[hyplinkout::figure,relative_width="40",file_src="''figures/markup-demo.png''"]
\<open>Output with hyperlinked position.\<close>
text\<open>@{figure \<open>hyplinkout\<close>} shows the produced output where the little house-like symbol in the

6
Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128_Documentation.thy
View File

@ -194,17 +194,17 @@ result communication times \ldots \<close>
text\<open>Note that this \<^pdf>-output is the result of a specific setup for \<^typ>\<open>SRAC\<close>s.\<close>
subsection*[ontopide::technical]\<open>Editing Support for CENELEC 50128\<close>
figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"]
figure*[figfig3::figure,relative_width="95",file_src="''figures/antiquotations-PIDE.png''"]
\<open> Standard antiquotations referring to theory elements.\<close>
text\<open> The corresponding view in @{docitem \<open>figfig3\<close>} shows core part of a document
conforming to the \<^verbatim>\<open>CENELEC_50128\<close> ontology. The first sample shows standard Isabelle antiquotations
@{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts
of a document get ``formal content'' and become more robust under change.\<close>
figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"]
figure*[figfig5::figure, relative_width="95", file_src="''figures/srac-definition.png''"]
\<open> Defining a \<^typ>\<open>SRAC\<close> in the integrated source ... \<close>
figure*[figfig7::figure, relative_width="95", src="''figures/srac-as-es-application''"]
figure*[figfig7::figure, relative_width="95", file_src="''figures/srac-as-es-application.png''"]
\<open> Using a \<^typ>\<open>SRAC\<close> as \<^typ>\<open>EC\<close> document element. \<close>
text\<open> The subsequent sample in @{figure \<open>figfig5\<close>} shows the definition of a
\<^emph>\<open>safety-related application condition\<close>, a side-condition of a theorem which

8
Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy
View File

@ -207,10 +207,10 @@ map fst (Name_Space.dest_table (DOF_core.get_onto_classes \<^context>));
let val class_ids_so_far = ["Conceptual.A", "Conceptual.B", "Conceptual.C", "Conceptual.D",
"Conceptual.E", "Conceptual.F", "Conceptual.G", "Conceptual.M",
"Isa_COL.float", "Isa_COL.figure", "Isa_COL.chapter", "Isa_COL.section",
"Isa_COL.paragraph", "Isa_COL.subsection", "Isa_COL.figure_group",
"Isa_COL.text_element", "Isa_COL.subsubsection",
"Isa_COL.side_by_side_figure"]
"Isa_COL.float", "Isa_COL.figure", "Isa_COL.chapter", "Isa_COL.listing",
"Isa_COL.section",
"Isa_COL.paragraph", "Isa_COL.subsection",
"Isa_COL.text_element", "Isa_COL.subsubsection"]
val docclass_tab = map fst (Name_Space.dest_table (DOF_core.get_onto_classes \<^context>));
in @{assert} (class_ids_so_far = docclass_tab) end\<close>

4
Isabelle_DOF-Ontologies/document-templates/root-sn-article-UNSUPPORTED.tex
View File

@ -38,8 +38,6 @@
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\usepackage[caption]{subfig}
\usepackage[size=footnotesize]{caption}
\let\DOFauthor\relax
\begin{document}
\selectlanguage{USenglish}%
@ -50,8 +48,6 @@
\renewcommand{\subsectionautorefname}{Sect.}
\renewcommand{\sectionautorefname}{Sect.}
\renewcommand{\figureautorefname}{Fig.}
\newcommand{\subtableautorefname}{\tableautorefname}
\newcommand{\subfigureautorefname}{\figureautorefname}
\newcommand{\lstnumberautorefname}{Line}
\maketitle

4
Isabelle_DOF-Ontologies/document-templates/root-svjour3-UNSUPPORTED.tex
View File

@ -40,8 +40,6 @@
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\usepackage[caption]{subfig}
\usepackage[size=footnotesize]{caption}
\begin{document}
\selectlanguage{USenglish}%
@ -52,8 +50,6 @@
\renewcommand{\subsectionautorefname}{Sect.}
\renewcommand{\sectionautorefname}{Sect.}
\renewcommand{\figureautorefname}{Fig.}
\newcommand{\subtableautorefname}{\tableautorefname}
\newcommand{\subfigureautorefname}{\figureautorefname}
\newcommand{\lstnumberautorefname}{Line}
\maketitle

16
Isabelle_DOF-Proofs/Reification_Test.thy
View File

@ -4,10 +4,10 @@ theory Reification_Test
begin
ML\<open>
val ty1 = ISA_core.reify_typ @{typ "int"}
val ty2 = ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
val ty3 = ISA_core.reify_typ @{typ "prop"}
val ty4 = ISA_core.reify_typ @{typ "'a list"}
val ty1 = Meta_ISA_core.reify_typ @{typ "int"}
val ty2 = Meta_ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
val ty3 = Meta_ISA_core.reify_typ @{typ "prop"}
val ty4 = Meta_ISA_core.reify_typ @{typ "'a list"}
\<close>
term*\<open>@{typ \<open>int\<close>}\<close>
@ -19,9 +19,9 @@ term*\<open>@{typ \<open>'a list\<close>}\<close>
value*\<open>@{typ \<open>'a list\<close>}\<close>
ML\<open>
val t1 = ISA_core.reify_term @{term "1::int"}
val t2 = ISA_core.reify_term @{term "\<lambda>x. x = 1"}
val t3 = ISA_core.reify_term @{term "[2, 3::int]"}
val t1 = Meta_ISA_core.reify_term @{term "1::int"}
val t2 = Meta_ISA_core.reify_term @{term "\<lambda>x. x = 1"}
val t3 = Meta_ISA_core.reify_term @{term "[2, 3::int]"}
\<close>
term*\<open>@{term \<open>1::int\<close>}\<close>
value*\<open>@{term \<open>1::int\<close>}\<close>
@ -45,7 +45,7 @@ value*\<open>@{thms-of \<open>HOL.refl\<close>}\<close>
ML\<open>
val t_schematic = TVar(("'a",0), [])
val t = @{term "Tv (Var (STR '''a'', 0)) {}"}
val rt_schematic = ISA_core.reify_typ t_schematic
val rt_schematic = Meta_ISA_core.reify_typ t_schematic
val true = rt_schematic = t
\<close>

1
Isabelle_DOF-Proofs/Very_Deep_DOF.thy
View File

@ -15,6 +15,5 @@ term "@{term \<open>\<forall>x. P x \<longrightarrow> Q\<close>}"
term "@{thm \<open>refl\<close>}"
term "@{docitem \<open>doc_ref\<close>}"
ML\<open> @{term "@{docitem \<open>doc_ref\<close>}"}\<close>
(**)
end

109
Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy
View File

@ -32,89 +32,9 @@ consts Isabelle_DOF_trace_attribute :: "string \<Rightarrow> (string * string) l
subsection\<open> Semantics \<close>
ML\<open>
structure ISA_core =
structure Meta_ISA_core =
struct
fun check_path check_file ctxt dir (name, pos) =
let
val _ = Context_Position.report ctxt pos (Markup.language_path true); (* TODO: pos should be
"lifted" to
type source *)
val path = Path.append dir (Path.explode name) handle ERROR msg => ISA_core.err msg pos;
val _ = Path.expand path handle ERROR msg => ISA_core.err msg pos;
val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
val _ =
(case check_file of
NONE => path
| SOME check => (check path handle ERROR msg => ISA_core.err msg pos));
in path end;
fun ML_isa_antiq check_file thy (name, _, pos) =
let val path = check_path check_file (Proof_Context.init_global thy) Path.current (name, pos);
in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
fun ML_isa_check_generic check thy (term, pos) =
let val name = (HOLogic.dest_string term
handle TERM(_,[t]) => error ("wrong term format: must be string constant: "
^ Syntax.string_of_term_global thy t ))
val _ = check thy (name,pos)
in SOME term end;
fun check_identity _ (term, _, _) _ = SOME term
fun ML_isa_check_typ thy (term, _, pos) _ =
let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy)
in (Syntax.check_typ ctxt o Syntax.parse_typ ctxt) name end
in ML_isa_check_generic check thy (term, pos) end
fun ML_isa_check_term thy (term, _, pos) _ =
let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy)
in (Syntax.check_term ctxt o Syntax.parse_term ctxt) name end
in ML_isa_check_generic check thy (term, pos) end
fun ML_isa_check_thm thy (term, _, pos) _ =
(* this works for long-names only *)
let fun check thy (name, _) = case Proof_Context.lookup_fact (Proof_Context.init_global thy) name of
NONE => ISA_core.err ("No Theorem:" ^name) pos
| SOME X => X
in ML_isa_check_generic check thy (term, pos) end
fun ML_isa_check_file thy (term, _, pos) _ =
let fun check thy (name, pos) = check_path (SOME File.check_file)
(Proof_Context.init_global thy)
(Path.current)
(name, pos);
in ML_isa_check_generic check thy (term, pos) end;
fun ML_isa_id thy (term,pos) = SOME term
fun ML_isa_check_docitem thy (term, req_ty, pos) _ =
let fun check thy (name, _) s =
let val DOF_core.Instance {cid,...} =
DOF_core.get_instance_global name thy
val ns = DOF_core.get_instances (Proof_Context.init_global thy)
|> Name_Space.space_of_table
val {pos=pos', ...} = Name_Space.the_entry ns name
val ctxt = (Proof_Context.init_global thy)
val req_class = case req_ty of
\<^Type>\<open>fun _ T\<close> => DOF_core.typ_to_cid T
| _ => error("can not infer type for: "^ name)
in if cid <> DOF_core.default_cid
andalso not(DOF_core.is_subclass ctxt cid req_class)
then error("reference ontologically inconsistent: "
^cid^" vs. "^req_class^ Position.here pos')
else ()
end
in ML_isa_check_generic check thy (term, pos) end
fun ML_isa_check_trace_attribute thy (term, _, pos) s =
let
val oid = (HOLogic.dest_string term
@ -123,11 +43,6 @@ fun ML_isa_check_trace_attribute thy (term, _, pos) s =
val _ = DOF_core.get_instance_global oid thy
in SOME term end
fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ =
case term_option of
NONE => error("Wrong term option. You must use a defined term")
| SOME term => Const (isa_name, ty) $ term
fun reify_typ (Type (s, typ_list)) =
\<^Const>\<open>Ty\<close> $ HOLogic.mk_literal s $ HOLogic.mk_list \<^Type>\<open>typ\<close> (map reify_typ typ_list)
| reify_typ (TFree (name, sort)) =
@ -273,16 +188,16 @@ end; (* struct *)
\<close>
ML\<open>
val ty1 = ISA_core.reify_typ @{typ "int"}
val ty2 = ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
val ty3 = ISA_core.reify_typ @{typ "prop"}
val ty4 = ISA_core.reify_typ @{typ "'a list"}
val ty1 = Meta_ISA_core.reify_typ @{typ "int"}
val ty2 = Meta_ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
val ty3 = Meta_ISA_core.reify_typ @{typ "prop"}
val ty4 = Meta_ISA_core.reify_typ @{typ "'a list"}
\<close>
ML\<open>
val t1 = ISA_core.reify_term @{term "1::int"}
val t2 = ISA_core.reify_term @{term "\<lambda>x. x = 1"}
val t3 = ISA_core.reify_term @{term "[2, 3::int]"}
val t1 = Meta_ISA_core.reify_term @{term "1::int"}
val t2 = Meta_ISA_core.reify_term @{term "\<lambda>x. x = 1"}
val t3 = Meta_ISA_core.reify_term @{term "[2, 3::int]"}
\<close>
subsection\<open> Isar - Setup\<close>
@ -290,8 +205,8 @@ subsection\<open> Isar - Setup\<close>
They must be declared in the same theory file as the one of the declaration
of Isabelle_DOF term anti-quotations !!! *)
setup\<open>
[(\<^type_name>\<open>thm\<close>, ISA_core.ML_isa_check_thm, ISA_core.ML_isa_elaborate_thm)
, (\<^type_name>\<open>thms_of\<close>, ISA_core.ML_isa_check_thm, ISA_core.ML_isa_elaborate_thms_of)
[(\<^type_name>\<open>thm\<close>, ISA_core.ML_isa_check_thm, Meta_ISA_core.ML_isa_elaborate_thm)
, (\<^type_name>\<open>thms_of\<close>, ISA_core.ML_isa_check_thm, Meta_ISA_core.ML_isa_elaborate_thms_of)
, (\<^type_name>\<open>file\<close>, ISA_core.ML_isa_check_file, ISA_core.ML_isa_elaborate_generic)]
|> fold (fn (n, check, elaborate) => fn thy =>
let val ns = Sign.tsig_of thy |> Type.type_space
@ -304,8 +219,8 @@ let val ns = Sign.tsig_of thy |> Type.type_space
in DOF_core.add_isa_transformer binding ((check, elaborate) |> DOF_core.make_isa_transformer) thy
end)
#>
([(\<^const_name>\<open>Isabelle_DOF_typ\<close>, ISA_core.ML_isa_check_typ, ISA_core.ML_isa_elaborate_typ)
,(\<^const_name>\<open>Isabelle_DOF_term\<close>, ISA_core.ML_isa_check_term, ISA_core.ML_isa_elaborate_term)
([(\<^const_name>\<open>Isabelle_DOF_typ\<close>, ISA_core.ML_isa_check_typ, Meta_ISA_core.ML_isa_elaborate_typ)
,(\<^const_name>\<open>Isabelle_DOF_term\<close>, ISA_core.ML_isa_check_term, Meta_ISA_core.ML_isa_elaborate_term)
,(\<^const_name>\<open>Isabelle_DOF_docitem\<close>,
ISA_core.ML_isa_check_docitem, ISA_core.ML_isa_elaborate_generic)
,(\<^const_name>\<open>Isabelle_DOF_trace_attribute\<close>,

20
Isabelle_DOF-Unit-Tests/Attributes.thy
View File

@ -182,29 +182,29 @@ open_monitor*[figs1::figure_group,
caption="''Sample ''"]
ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
text*[testFreeA::A]\<open>\<close>
figure*[fig_A::figure, spawn_columns=False,
figure*[fig_A::figure,
relative_width="90",
src="''figures/A.png''"]
file_src="''figures/A.png''"]
\<open> The A train \ldots \<close>
figure*[fig_B::figure,
spawn_columns=False,relative_width="90",
src="''figures/B.png''"]
relative_width="90",
file_src="''figures/B.png''"]
\<open> The B train \ldots \<close>
open_monitor*[figs2::figure_group,
caption="''Sample ''"]
ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
figure*[fig_C::figure, spawn_columns=False,
figure*[fig_C::figure,
relative_width="90",
src="''figures/A.png''"]
file_src="''figures/A.png''"]
\<open> The C train \ldots \<close>
open_monitor*[figs3::figure_group,
caption="''Sample ''"]
ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
figure*[fig_D::figure,
spawn_columns=False,relative_width="90",
src="''figures/B.png''"]
relative_width="90",
file_src="''figures/B.png''"]
\<open> The D train \ldots \<close>
close_monitor*[figs3]
@ -216,8 +216,8 @@ text*[testRejected1::figure_group, caption="''document/figures/A.png''"]
\<open> The A train \ldots \<close>
figure*[fig_E::figure,
spawn_columns=False,relative_width="90",
src="''figures/B.png''"]
relative_width="90",
file_src="''figures/B.png''"]
\<open> The E train \ldots \<close>
close_monitor*[figs4]
close_monitor*[figs2]

53
Isabelle_DOF-Unit-Tests/COL_Test.thy
View File

@ -28,59 +28,32 @@ text*[S5'::"paragraph"]\<open>Paragraph\<close>
section\<open>General Figure COL Elements\<close>
figure*[fig1_test::figure,spawn_columns=False,relative_width="95",src="''figures/A''"]
figure*[fig1_test,relative_width="95",file_src="''figures/A.png''"]
\<open> This is the label text \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<close>
text*[fig2_test::figure, spawn_columns=False, relative_width="95",src="''figures/A''"
(*<*)
text*[fig2_test::figure, relative_width="95",file_src="''figures/A.png''"
]\<open> This is the label text\<close>
(*>*)
text\<open>check @{figure fig1_test} cmp to @{figure fig2_test}\<close>
side_by_side_figure*["sbsfig1"::side_by_side_figure,
anchor="''Asub1''",
caption="''First caption.''",
relative_width="48",
src="''figures/A''",
anchor2="''Asub2''",
caption2="''Second caption.''",
relative_width2="47",
src2="''figures/B''"]\<open> Exploring text elements. \<close>
text*["sbsfig2"::side_by_side_figure,
anchor="''fig:Asub1''",
caption="''First caption.''",
relative_width="48",
src="''figures/A''",
anchor2="''fig:Asub2''",
caption2="''Second caption.''",
relative_width2="47",
src2="''figures/B''"]\<open>The global caption\<close>
text\<open>check @{side_by_side_figure sbsfig1} cmp to @{side_by_side_figure sbsfig2}
\autoref{Asub1} vs. \autoref{Asub2}
\autoref{fig:Asub1} vs. \autoref{fig:Asub2}
\<close>
(* And a side-chick ... *)
text*[inlinefig::float,
caption="\<open>The Caption.\<close>"]
\<open>@{theory_text [display, margin = 5] \<open>lemma A :: "a \<longrightarrow> b"\<close>}\<close>
main_caption="\<open>The Caption.\<close>"]
\<open>@{theory_text [display, margin = 5] \<open>lemma A :: "a \<longrightarrow> b"\<close>}\<close>
text*[fffff::float]\<open> @{fig_content [display] (scale = 80, width=80, caption=\<open>this is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<close>)
\<open>figures/A.png\<close>}\<close>
(*<*)
text*[inlinegraph::float,
caption="\<open>Another \<sigma>\<^sub>i+2 Caption.\<close>"]
\<open>@{fig_content [display] (scale = 80, width=80, caption=\<open>This is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<close>)
\<open>figures/A.png\<close>}\<close>
(*>*)
text*[dupl_graphics::float,
main_caption="\<open>The Caption.\<close>"]
\<open>
@{fig_content (width=40, height=35, caption="This is a left test") "figures/A.png"
}\<^hfill>@{fig_content (width=40, height=35, caption="This is a right \<^term>\<open>\<sigma>\<^sub>i + 1\<close> test") "figures/B.png"}
\<close>
(*<*)
end
(*>*)

45
Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy
View File

@ -131,7 +131,7 @@ text\<open>Now assume the following ontology:\<close>
doc_class title =
short_title :: "string option" <= "None"
doc_class Author =
doc_class author =
email :: "string" <= "''''"
datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
@ -141,18 +141,18 @@ doc_class abstract =
safety_level :: "classification" <= "SIL3"
doc_class text_section =
authored_by :: "Author set" <= "{}"
authored_by :: "author set" <= "{}"
level :: "int option" <= "None"
type_synonym notion = string
doc_class Introduction = text_section +
authored_by :: "Author set" <= "UNIV"
doc_class introduction = text_section +
authored_by :: "author set" <= "UNIV"
uses :: "notion set"
invariant author_finite :: "finite (authored_by \<sigma>)"
and force_level :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 1"
doc_class claim = Introduction +
doc_class claim = introduction +
based_on :: "notion list"
doc_class technical = text_section +
@ -181,7 +181,10 @@ text\<open>Next we define some instances (docitems): \<close>
declare[[invariants_checking_with_tactics = true]]
text*[church::Author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
text*[church::author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
text\<open>We can also reference instances of classes defined in parent theories:\<close>
text*[church'::scholarly_paper.author, email="\<open>church'@lambda.org\<close>"]\<open>\<close>
text*[resultProof::result, evidence = "proof", property="[@{thm \<open>HOL.refl\<close>}]"]\<open>\<close>
text*[resultArgument::result, evidence = "argument"]\<open>\<close>
@ -193,29 +196,41 @@ text\<open>The invariants \<^theory_text>\<open>author_finite\<close> and \<^the
declare[[invariants_checking_with_tactics = true]]
text*[curry::Author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
text*[introduction2::Introduction, authored_by = "{@{Author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
text*[curry::author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
text*[introduction2::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
(* When not commented, should violated the invariant:
update_instance*[introduction2::Introduction
, authored_by := "{@{Author \<open>church\<close>}}"
, level := "Some 1"]
*)
text\<open>Use of the instance @{docitem_name "church'"}
to instantiate a \<^doc_class>\<open>scholarly_paper.introduction\<close> class:\<close>
text*[introduction2'::scholarly_paper.introduction,
main_author = "Some @{scholarly-paper.author \<open>church'\<close>}", level = "Some 2"]\<open>\<close>
value*\<open>@{scholarly-paper.author \<open>church'\<close>}\<close>
value*\<open>@{author \<open>church\<close>}\<close>
value*\<open>@{Concept-High-Level-Invariants.author \<open>church\<close>}\<close>
text*[introduction3::Introduction, authored_by = "{@{Author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
text*[introduction4::Introduction, authored_by = "{@{Author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
value*\<open>@{scholarly-paper.author-instances}\<close>
value*\<open>@{author-instances}\<close>
value*\<open>@{Concept-High-Level-Invariants.author-instances}\<close>
text*[introduction3::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
text*[introduction4::introduction, authored_by = "{@{author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
text*[resultProof2::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"]\<open>\<close>
text\<open>Then we can evaluate expressions with instances:\<close>
term*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
value*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
value*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction4\<close>}\<close>
term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction4\<close>}\<close>
value*\<open>@{Introduction \<open>introduction2\<close>}\<close>
value*\<open>@{introduction \<open>introduction2\<close>}\<close>
value*\<open>{@{Author \<open>curry\<close>}} = {@{Author \<open>church\<close>}}\<close>
value*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
value*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>

5
Isabelle_DOF-Unit-Tests/Concept_MonitorTest2.thy
View File

@ -22,9 +22,12 @@ begin
section\<open>Test Purpose.\<close>
text\<open> Creation of document parts that are controlled by (nested, locally defined) monitors. \<close>
doc_class test_monitor_B =
tmB :: int
doc_class monitor_M =
tmM :: int
rejects "test_monitor_B"
rejects "Concept_MonitorTest1.test_monitor_B"
accepts "test_monitor_E ~~ test_monitor_C"
doc_class test_monitor_head =

8
Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy
View File

@ -200,10 +200,10 @@ Consequently, it has the same limitations as \<^emph>\<open>value*\<close>.
text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-Unit-Tests.Concept_High_Level_Invariants\<close>
we can check logical statements:\<close>
term*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
assert*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
assert*\<open>\<not>(authored_by @{Introduction \<open>introduction2\<close>}
= authored_by @{Introduction \<open>introduction4\<close>})\<close>
term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
assert*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
assert*\<open>\<not>(authored_by @{introduction \<open>introduction2\<close>}
= authored_by @{introduction \<open>introduction4\<close>})\<close>
text\<open>Assertions must be boolean expressions, so the following assertion triggers an error:\<close>
(* Error:

8
Isabelle_DOF-Unit-Tests/Latex_Tests.thy
View File

@ -418,16 +418,16 @@ Figure*[fff::figure,src="\<open>this is a side-by-side\<close>"]
(*<*)
text-latex\<open>
@{fig_content (width=40, scale=35, caption="This is a right test") "figures/A.png"}
@{fig_content (width=40, scale=35, caption="This is a left \<^term>\<open>\<sigma>\<^sub>i + 1\<close> test") "figures/A.png"}
Figure*[figxxx::float,main_caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
\<open> @{fig_content (width=40, height=35, caption="This is a right test") "figures/A.png"}
@{fig_content (width=40, height=35, caption="This is a left \<^term>\<open>\<sigma>\<^sub>i + 1\<close> test") "figures/A.png"}
\<close>
(* proposed syntax for sub-figure labels : text\<open> @{figure "ffff(2)"}\<close> *)
Figure*[figxxx::float,caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
Figure*[figxxxx::float,main_caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
\<open>@{boxed_theory_text [display]
\<open>lemma inv_c2_preserved : "c2_inv \<sigma> \<Longrightarrow> c1_inv (\<sigma> \<langle>Hardware\<rangle>\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e)"
unfolding c1_inv_def c2_inv_def

4
Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy
View File

@ -408,7 +408,7 @@ Figure*[fff::figure,src="\<open>this is a side-by-side\<close>"]
*)
Figure*[ffff::float, caption="\<open>this is another 2 side-by-side\<close>"]
Figure*[ffff::float, main_caption="\<open>this is another 2 side-by-side\<close>"]
\<open>@{figure_content [width=40, scale=35, caption="This is a left test"] "ROOT"}\<close>
\<open>@{figure_content [width=40, scale=35, caption="This is a right test"] "ROOT"}\<close>
@ -416,7 +416,7 @@ Figure*[ffff::float, caption="\<open>this is another 2 side-by-side\<close>"]
text\<open> @{figure "ffff(2)"}\<close>
*)
Figure*[figxxx::float,caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
Figure*[figxxx::float,main_caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
\<open>@{boxed_theory_text [display]
\<open>lemma inv_c2_preserved : "c2_inv \<sigma> \<Longrightarrow> c1_inv (\<sigma> \<langle>Hardware\<rangle>\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e)"
unfolding c1_inv_def c2_inv_def

2
Isabelle_DOF-Unit-Tests/ROOT
View File

@ -13,7 +13,7 @@ session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
"Attributes"
"AssnsLemmaThmEtc"
"Ontology_Matching_Example"
(* "Cenelec_Test" *)
"Cenelec_Test"
"OutOfOrderPresntn"
"COL_Test"
document_files

BIN
Isabelle_DOF/document/figures/isabelle-architecture.pdf
View File

Binary file not shown.

20
Isabelle_DOF/document/preamble.tex
View File

@ -1,6 +1,6 @@
%% Copyright (C) 2019 University of Exeter, UK
%% 2018 The University of Sheffield, UK
%% 2018 The University of Paris-Saclay, France
%% Copyright (C) University of Exeter, UK
%% The University of Sheffield, UK
%% The University of Paris-Saclay, France
%%
%% License:
%% This program can be redistributed and/or modified under the terms
@ -39,8 +39,8 @@
\pagestyle{headings}
\uppertitleback{
Copyright \copyright{} 2019--2022 University of Exeter, UK\\
\phantom{Copyright \copyright{}} 2018--2022 Universit\'e Paris-Saclay, France\\
Copyright \copyright{} 2019--2023 University of Exeter, UK\\
\phantom{Copyright \copyright{}} 2018--2023 Universit\'e Paris-Saclay, France\\
\phantom{Copyright \copyright{}} 2018--2019 The University of Sheffield, UK\\
\smallskip
@ -74,14 +74,11 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
}
\lowertitleback{%
This manual describes \isadof version \isadofversion. The latest official
release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}).
The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest
release. The latest development version as well as official releases are available at
This manual describes \isadof as available in the Archive of Formal Proofs (AFP). The latest development version as well as releases that can be installed as Isabelle component are available at
\url{\dofurl}.
\paragraph*{Contributors.} We would like to thank the following contributors to \isadof
(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, and Nicolas M{\'e}ric.
(in alphabetical order): Idir Ait-Sadoune and Paolo Crisafulli.
\paragraph*{Acknowledgments.} This work has been partially supported by IRT SystemX, Paris-Saclay,
France, and therefore granted with public funds of the Program ``Investissements d'Avenir.''
@ -124,5 +121,6 @@ France, and therefore granted with public funds of the Program ``Investissements
\expandafter\index\expandafter{\expanded{#2 (#1)}}%
}%
\sloppy
\raggedbottom
\AtBeginDocument{\isabellestyle{literal}\newcommand{\lstnumberautorefname}{Line}}

4
Isabelle_DOF/latex/document-templates/root-lncs.tex
View File

@ -36,7 +36,7 @@
\sloppy
\allowdisplaybreaks[4]
\usepackage[caption]{subfig}
\usepackage{subcaption}
\usepackage[size=footnotesize]{caption}
\renewcommand{\topfraction}{0.9} % max fraction of floats at top
@ -59,8 +59,6 @@
\renewcommand{\subsectionautorefname}{Sect.}
\renewcommand{\sectionautorefname}{Sect.}
\renewcommand{\figureautorefname}{Fig.}
\newcommand{\subtableautorefname}{\tableautorefname}
\newcommand{\subfigureautorefname}{\figureautorefname}
\newcommand{\lstnumberautorefname}{Line}

2
Isabelle_DOF/latex/document-templates/root-scrartcl.tex
View File

@ -26,7 +26,7 @@
\usepackage{textcomp}
\bibliographystyle{abbrvnat}
\RequirePackage[caption]{subfig}
\RequirePackage{subcaption}
\usepackage[numbers, sort&compress, sectionbib]{natbib}

4
Isabelle_DOF/latex/document-templates/root-scrreprt-modern.tex
View File

@ -43,7 +43,7 @@
\addtokomafont{paragraph}{\color{DOFsectioncolor}}
\addtokomafont{subparagraph}{\color{DOFsectioncolor}}
\RequirePackage[caption]{subfig}
\RequirePackage{subcaption}
\renewcommand{\isastyletext}{\normalsize\normalfont\sffamily}
\renewcommand{\isastyletxt}{\normalfont\sffamily}
\renewcommand{\isastylecmt}{\normalfont\sffamily}
@ -68,8 +68,6 @@
\renewcommand{\sectionautorefname}{Section}
\renewcommand{\subsectionautorefname}{Section}
\renewcommand{\subsubsectionautorefname}{Section}
\newcommand{\subtableautorefname}{\tableautorefname}
\newcommand{\subfigureautorefname}{\figureautorefname}
\begin{frontmatter}
\maketitle
\tableofcontents

4
Isabelle_DOF/latex/document-templates/root-scrreprt.tex
View File

@ -26,7 +26,7 @@
\usepackage{textcomp}
\bibliographystyle{abbrvnat}
\RequirePackage[caption]{subfig}
\RequirePackage{subcaption}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
@ -48,8 +48,6 @@
\renewcommand{\sectionautorefname}{Section}
\renewcommand{\subsectionautorefname}{Section}
\renewcommand{\subsubsectionautorefname}{Section}
\newcommand{\subtableautorefname}{\tableautorefname}
\newcommand{\subfigureautorefname}{\figureautorefname}
\maketitle
\tableofcontents
\IfFileExists{dof_session.tex}{\input{dof_session}}{\input{session}}

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

@ -18,100 +18,21 @@
\RequirePackage{DOF-core}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: figure*
\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}}
\newisadof{IsaUNDERSCORECOLDOTfigure}%
[label=,type=%
,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=%
,IsaUNDERSCORECOLDOTfigureDOTplacement=%
,IsaUNDERSCORECOLDOTfigureDOTsrc=%
,IsaUNDERSCORECOLDOTfigureDOTspawnUNDERSCOREcolumns=enum False True%
][1]{%
\begin{figure}[]
\centering
\ifcommandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}
{%
\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{IsaUNDERSCORECOLDOTfigureDOTsrc}}
\includegraphics[]{\dof@src}%
}
\caption{#1}\label{\commandkey{label}}%
\end{figure}
}
% end: figure*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: float*
\NewEnviron{isamarkupfloat*}[1][]{\isaDof[env={float},#1]{\BODY}}
\newisadof{IsaUNDERSCORECOLDOTfloat}%
[label=,type=%
,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=%
,IsaUNDERSCORECOLDOTfigureDOTplacement=%
,IsaUNDERSCORECOLDOTfigureDOTsrc=%
,IsaUNDERSCORECOLDOTfloatDOTcaption=%
,IsaUNDERSCORECOLDOTfigureDOTspawnUNDERSCOREcolumns=enum False True%
,IsaUNDERSCORECOLDOTfloatDOTplacement=%
,IsaUNDERSCORECOLDOTfloatDOTfloatUNDERSCOREkind=%
,IsaUNDERSCORECOLDOTfloatDOTmainUNDERSCOREcaption=%
,IsaUNDERSCORECOLDOTfloatDOTspawnUNDERSCOREcolumns=enum False True%
][1]{%
\begin{figure}[]
\begin{figure}
#1
\caption{\commandkey{IsaUNDERSCORECOLDOTfloatDOTcaption}}
\caption{\commandkey{IsaUNDERSCORECOLDOTfloatDOTmainUNDERSCOREcaption}}
\label{\commandkey{label}}%
\end{figure}
}
% end: float*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: side_by_side_figure*
\NewEnviron{isamarkupsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure*}[1][]{\isaDof[env={sideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure},#1]{\BODY}}
\newisadof{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure}%
[label=,type=%
,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=%
,IsaUNDERSCORECOLDOTfigureDOTplacement=%
,IsaUNDERSCORECOLDOTfigureDOTsrc=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchor=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaption=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTrelativeUNDERSCOREwidthTWO=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTsrcTWO=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchorTWO=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaptionTWO=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTplacement=%
,IsaUNDERSCORECOLDOTfigureDOTspawnUNDERSCOREcolumns=enum False True%
][1]{%
\begin{figure}[]
\subfloat[\label{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchor}}\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaption}]%
{\ifcommandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}%
{%
\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{IsaUNDERSCORECOLDOTfigureDOTsrc}}
\includegraphics[]{\dof@src}%
}%
}%
\hfill%
\subfloat[\label{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchorTWO}}\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaptionTWO}]%
{\ifcommandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTrelativeUNDERSCOREwidthTWO}%
{%
\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{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTsrcTWO}}
\includegraphics[]{\dof@src}%
}%
}%
\caption{#1}\label{\commandkey{label}}%
\end{figure}
}
% end: side_by_side_figure*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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

@ -167,7 +167,6 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{No Title Given}
\author{No Author Given}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%

2
Isabelle_DOF/ontologies/technical_report/technical_report.thy
View File

@ -75,7 +75,7 @@ doc_class report =
abstract ~~
\<lbrakk>table_of_contents\<rbrakk> ~~
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
\<lbrace>technical || figure || side_by_side_figure\<rbrace>\<^sup>+ ~~
\<lbrace>technical || figure \<rbrace>\<^sup>+ ~~
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
\<lbrace>index\<rbrace>\<^sup>* ~~
bibliography)"

295
Isabelle_DOF/thys/Isa_COL.thy
View File

@ -26,7 +26,7 @@ theory Isa_COL
keywords "title*" "subtitle*"
"chapter*" "section*" "paragraph*"
"subsection*" "subsubsection*"
"figure*" "side_by_side_figure*" :: document_body
"figure*" "listing*" :: document_body
begin
@ -141,53 +141,11 @@ val _ = heading_command \<^command_keyword>\<open>subsection*\<close> "subsectio
val _ = heading_command \<^command_keyword>\<open>subsubsection*\<close> "subsubsection heading" (SOME (SOME 3));
val _ = heading_command \<^command_keyword>\<open>paragraph*\<close> "paragraph" (SOME (SOME 4));
end
end
\<close>
section\<open> Library of Standard Text Ontology \<close>
datatype placement = pl_h | (*here*)
pl_t | (*top*)
pl_b | (*bottom*)
pl_ht | (*here -> top*)
pl_hb (*here -> bottom*)
ML\<open> "side_by_side_figure" |> Name_Space.declared (DOF_core.get_onto_classes \<^context>
|> Name_Space.space_of_table)\<close>
print_doc_classes
doc_class figure =
relative_width :: "int" (* percent of textwidth *)
src :: "string"
placement :: placement
spawn_columns :: bool <= True
doc_class float = figure +
caption :: string
doc_class side_by_side_figure = figure +
anchor :: "string"
caption :: "string"
relative_width2 :: "int" (* percent of textwidth *)
src2 :: "string"
anchor2 :: "string"
caption2 :: "string"
print_doc_classes
doc_class figure_group =
(* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *)
caption :: "string"
rejects figure_group (* this forbids recursive figure-groups not supported
by the current LaTeX style-file. *)
accepts "\<lbrace>figure\<rbrace>\<^sup>+"
print_doc_classes
section\<open>Layout Trimming Commands (with syntactic checks)\<close>
@ -225,7 +183,7 @@ end\<close>
setup\<open> DOF_lib.define_macro \<^binding>\<open>vs\<close> "\\vspace{" "}" (check_latex_measure) \<close>
setup\<open> DOF_lib.define_macro \<^binding>\<open>hs\<close> "\\hspace{" "}" (check_latex_measure) \<close>
define_shortcut* hfill \<rightleftharpoons> \<open>\hfill\<close>
(*<*)
text\<open>Tests: \<^vs>\<open>-0.14cm\<close>\<close>
@ -236,19 +194,54 @@ define_macro* hs2 \<rightleftharpoons> \<open>\hspace{\<close> _ \<open>}\<close
(*>*)
define_shortcut* clearpage \<rightleftharpoons> \<open>\clearpage{}\<close>
hf \<rightleftharpoons> \<open>\hfill\<close>
br \<rightleftharpoons> \<open>\break\<close>
section\<open> Library of Standard Figure Ontology \<close>
datatype placement = here | top | bottom
(*
ML\<open> "side_by_side_figure" |> Name_Space.declared (DOF_core.get_onto_classes \<^context>
|> Name_Space.space_of_table)\<close>
*)
datatype float_kind = listing | table | graphics
doc_class float =
placement :: "placement list"
kind :: float_kind
spawn_columns :: bool <= False
main_caption :: string <= "''''"
doc_class figure = float +
kind :: float_kind <= graphics
file_src :: string
relative_width :: int
relative_height :: int
invariant fig_kind :: "kind \<sigma> = graphics"
doc_class listing = float +
kind :: float_kind
invariant fig_kind' :: "kind \<sigma> = float_kind.listing"
(* obsolete
doc_class side_by_side_figure = figure +
anchor :: "string"
caption :: "string"
relative_width2 :: "int" (* percent of textwidth *)
src2 :: "string"
anchor2 :: "string"
caption2 :: "string"
*)
subsection\<open>Figures\<close>
ML\<open>open Args\<close>
ML\<open>
(* *********************************************************************** *)
(* Ontological Macro Command Support *)
(* *********************************************************************** *)
val _ = Onto_Macros.heading_command \<^command_keyword>\<open>figure*\<close> "figure" NONE;
val _ = Onto_Macros.heading_command \<^command_keyword>\<open>side_by_side_figure*\<close> "multiple figures" NONE;
\<close>
(*<*)
ML\<open>
@ -260,35 +253,34 @@ fun setup source =
(*>*)
subsubsection\<open>Figure Content\<close>
subsubsection\<open>The Figure Content Antiquotation\<close>
text\<open>The intermediate development goal is to separate the ontological, top-level construct
\<open>figure*\<close>, which will remain a referentiable, ontological document unit, from the more versatile
\<^emph>\<open>import\<close> of a figure. The hope is that this opens the way for more orthogonality and
abstraction from the LaTeX engine.
\<^emph>\<open>import\<close> of a figure. This opens the way for more orthogonality and abstraction from the LaTeX
engine.
\<close>
ML\<open>
ML\<open>
type fig_content = {relative_width : int, (* percent of textwidth, default 100 *)
scale : int, (* percent, default 100 *)
relative_height : int, (* percent, default 100 *)
caption : Input.source (* default empty *)}
val mt_fig_content = {relative_width = 100,
scale = 100,
relative_height = 100,
caption = Input.empty }: fig_content
fun upd_relative_width key {relative_width,scale,caption } : fig_content =
{relative_width = key,scale = scale,caption = caption}: fig_content
fun upd_relative_width key {relative_width,relative_height,caption } : fig_content =
{relative_width = key,relative_height = relative_height,caption = caption}: fig_content
fun upd_scale key {relative_width,scale,caption } : fig_content =
{relative_width = relative_width,scale = key,caption = caption}: fig_content
fun upd_relative_height key {relative_width,relative_height,caption } : fig_content =
{relative_width = relative_width,relative_height = key,caption = caption}: fig_content
fun upd_caption key {relative_width,scale,caption} : fig_content =
{relative_width = relative_width,scale = scale,caption= key}: fig_content
fun upd_caption key {relative_width,relative_height,caption} : fig_content =
{relative_width = relative_width,relative_height = relative_height,caption= key}: fig_content
val widthN = "width"
val scaleN = "scale"
val heightN = "height"
val captionN = "caption";
fun fig_content_modes (ctxt, toks) =
@ -297,8 +289,8 @@ fun fig_content_modes (ctxt, toks) =
(Parse.list1
( (Args.$$$ widthN |-- Args.$$$ "=" -- Parse.int
>> (fn (_, k) => upd_relative_width k))
|| (Args.$$$ scaleN |-- Args.$$$ "=" -- Parse.int
>> (fn (_, k) => upd_scale k))
|| (Args.$$$ heightN |-- Args.$$$ "=" -- Parse.int
>> (fn (_, k) => upd_relative_height k))
|| (Args.$$$ captionN |-- Args.$$$ "=" -- Parse.document_source
>> (fn (_, k) => upd_caption k))
))) [K mt_fig_content])
@ -314,8 +306,6 @@ fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Pat
Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source))
|> Latex.macro "isatt"));
val SPY = Unsynchronized.ref([XML.Text ""])
fun get_session_dir ctxt path =
Resources.check_session_dir ctxt
(SOME (path))
@ -329,41 +319,49 @@ fun get_document_dir ctxt =
val sess_dir = get_session_dir ctxt (Resources.master_directory thy)
in Path.append sess_dir (Path.explode "document") end;
fun generate_caption ctxt caption =
let
val cap_txt= Document_Output.output_document ctxt {markdown = false} caption
fun drop_latex_macro (XML.Elem (("latex_environment", [("name", "isabelle")]),xmlt)) = xmlt
|drop_latex_macro X = [X]
val drop_latex_macros = List.concat o map drop_latex_macro;
in
drop_latex_macros cap_txt
end
fun fig_content ctxt (cfg_trans,file:Input.source) =
let val {relative_width,relative_height,caption} = cfg_trans mt_fig_content
val _ = if relative_width < 0 orelse relative_height <0 then error("negative parameter.")
else ()
val wdth_val_s = Real.toString((Real.fromInt relative_width)
/ (Real.fromInt 100))^"\\textwidth"
val ht_s= if relative_height = 100 then ""
else "height="^Real.toString((Real.fromInt relative_height)
/ (Real.fromInt 100)) ^"\\textheight"
val arg_single = enclose "[" "]" (commas ["keepaspectratio","width="^wdth_val_s,ht_s])
val arg = enclose "[" "]" (commas ["keepaspectratio","width=\\textwidth",ht_s])
val _ = Resources.check_file ctxt (SOME (get_document_dir ctxt)) file
(* ToDo: must be declared source of type png or jpeg or pdf, ... *)
in if Input.string_of(caption) = "" then
file
|> (Latex.string o Input.string_of)
|> (XML.enclose ("\\includegraphics"^arg_single^"{") "}")
else
file
|> (Latex.string o Input.string_of)
|> (fn X => (Latex.string ("{"^wdth_val_s^"}"))
@ (Latex.string "\\centering")
@ (XML.enclose ("\\includegraphics"^arg^"{") "}" X)
@ (Latex.macro "caption" (generate_caption ctxt caption)))
|> (Latex.environment ("subcaptionblock") )
(* BUG: newline at the end of subcaptionlbock, making side-by-side a figure-below-figure setup *)
end
fun fig_content_antiquotation name scan =
(Document_Output.antiquotation_raw_embedded name
(scan : ((fig_content -> fig_content) * Input.source) context_parser)
(fn ctxt =>
(fn (cfg_trans,file:Input.source) =>
let val {relative_width,scale,caption} = cfg_trans mt_fig_content
val _ = if relative_width < 0 orelse scale<0 then error("negative parameter.")
else ()
val wdth_s = if relative_width = 100 then ""
else "width="^Real.toString((Real.fromInt relative_width)
/ (Real.fromInt 100))^"\\textwidth"
val scale_s= if scale = 100 then ""
else "scale="^Real.toString((Real.fromInt scale) / (Real.fromInt 100))
val arg = enclose "[" "]" (commas [wdth_s,scale_s])
val cap_txt= Document_Output.output_document ctxt {markdown = false} caption
fun drop_latex_macro (XML.Elem (("latex_environment", [("name", "isabelle")]),xmlt)) = xmlt
|drop_latex_macro X = [X];
val drop_latex_macros = List.concat o map drop_latex_macro;
val cap_txt = drop_latex_macros cap_txt
val path = Resources.check_file ctxt (SOME (get_document_dir ctxt)) file
(* ToDo: must be declared source of type png or jpeg or pdf, ... *)
in file
|> (Latex.string o Input.string_of)
|> (XML.enclose ("\\includegraphics"^arg^"{") "}")
|> (fn X => X @ Latex.macro "caption" cap_txt)
end
)
));
val _ = fig_content_antiquotation
: binding
-> ((fig_content -> fig_content) * Input.source) context_parser
-> theory -> theory
(fig_content : Proof.context -> (fig_content -> fig_content) * Input.source -> Latex.text));
val _ = Theory.setup
( fig_content_antiquotation \<^binding>\<open>fig_content\<close>
@ -373,36 +371,60 @@ val _ = Theory.setup
ML\<open>
val _ = Path.parent
val mdir = Resources.master_directory @{theory}
val pp = Resources.check_session_dir @{context}
(SOME (Path.dir mdir )) (Syntax.read_input ".nnn")
handle ERROR s => (if String.isPrefix "No such directory:" s then
(writeln ("MMM"^s); mdir)
else error s)
val ppp = (Path.explode "document")
fun convert_meta_args (X, (((str,_),value) :: R)) =
let fun conv_int x = snd(HOLogic.dest_number(Syntax.read_term @{context} x))
handle TERM x => error "Illegal int format."
in
(case YXML.content_of str of
"relative_width" => upd_relative_width (conv_int value)
o convert_meta_args (X, R)
| "relative_height" => upd_relative_height (conv_int value)
o convert_meta_args (X, R )
| "file_src" => convert_meta_args (X, R)
| s => error("!undefined attribute:"^s))
end
|convert_meta_args (X,[]) = I
fun get_session_dir ctxt path =
Resources.check_session_dir ctxt
(SOME (path))
(Syntax.read_input ".")
handle ERROR s => (if String.isPrefix "Bad session root directory (missing ROOT or ROOTS): " s
then get_session_dir ctxt (Path.dir path)
else error s)
fun convert_src_from_margs (X, (((str,_),value)::R)) =
(case YXML.content_of str of
"file_src" => Input.string (HOLogic.dest_string (Syntax.read_term @{context} value))
| _ => convert_src_from_margs(X,R))
|convert_src_from_margs (X, []) = error("No file_src provided.")
fun get_document_dir ctxt =
let val thy = Proof_Context.theory_of ctxt
val sess_dir = get_session_dir ctxt (Resources.master_directory thy)
in Path.append sess_dir (Path.explode "document") end;
fun float_command (name, pos) descr cid =
let fun set_default_class NONE = SOME(cid,pos)
|set_default_class (SOME X) = SOME X
fun create_instance ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) =
Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor = false}
{is_inline = true}
{define = true} oid pos (set_default_class cid_pos) doc_attrs
val opts = {markdown = false, body = true}
fun parse_and_tex _ (margs, text) ctxt = (fig_content ctxt
(convert_meta_args margs o upd_caption Input.empty,
convert_src_from_margs margs))
|> (fn X => (Latex.macro0 "centering"
@ X
@ Latex.macro "caption" (generate_caption ctxt text)))
(* TODO: add label *)
|> (Latex.environment ("figure") )
in Monitor_Command_Parser.float_command (name, pos) descr opts create_instance parse_and_tex
end
get_document_dir @{context}
(* *********************************************************************** *)
(* Ontological Macro Command Support *)
(* *********************************************************************** *)
val _ = float_command \<^command_keyword>\<open>figure*\<close> "figure" "Isa_COL.figure" ;
val _ = float_command \<^command_keyword>\<open>listing*\<close> "figure" "Isa_COL.listing" ; (* Hack ! *)
\<close>
subsection\<open>Tables\<close>
(* TODO ! ! ! *)
(* dito the future monitor: table - block *)
(* some studies *)
(* Under development *)
text\<open>Tables are (sub) document-elements represented inside the documentation antiquotation
language. The used technology is similar to the existing railroad-diagram support
@ -662,18 +684,15 @@ val _ = Theory.setup
end
\<close>
text\<open> @{file "../ROOT"} \<close>
define_shortcut* clearpage \<rightleftharpoons> \<open>\clearpage{}\<close>
hf \<rightleftharpoons> \<open>\hfill\<close>
br \<rightleftharpoons> \<open>\break\<close>
(*<*)
declare[[tab_cell_placing="left",tab_cell_height="18.0cm"]]
section\<open>Tests\<close>
(*<*)
section\<open>Some Rudimentary Tests\<close>
text\<open> @{fig_content [display] (scale = 80, width=80, caption=\<open>this is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<dots>\<close>)
text\<open> @{fig_content [display] (height = 80, width=80, caption=\<open>this is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<dots>\<close>)
\<open>figures/isabelle-architecture.pdf\<close>}\<close>
text\<open> @{table_inline [display] (cell_placing = center,cell_height =\<open>12.0cm\<close>,
cell_height =\<open>13pt\<close>, cell_width = \<open>12.0cm\<close>,
@ -685,11 +704,5 @@ text\<open> @{table_inline [display] (cell_placing = center,cell_height =\<open
(*>*)
ML\<open>@{term "side_by_side_figure"};
@{typ "doc_class rexp"};
DOF_core.SPY;
\<close>
text\<open>@{term_ \<open>3 + 4::int\<close>} @{value_ \<open>3 + 4::int\<close>} \<close>
end

182
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -670,8 +670,6 @@ fun typ_to_cid (Type(s,[\<^Type>\<open>unit\<close>])) = Long_Name.qualifier s
|typ_to_cid _ = error("type is not an ontological type.")
val SPY = Unsynchronized.ref(Bound 0)
fun check_regexps term =
let val _ = case fold_aterms Term.add_free_names term [] of
n::_ => error("No free variables allowed in monitor regexp:" ^ n)
@ -806,24 +804,24 @@ fun binding_from_onto_class_pos name thy =
fun binding_from_instance_pos name thy =
binding_from_pos get_instances get_instance_name_global name thy
fun check_invs get_ml_invs cid_long oid is_monitor thy =
fun check_invs get_ml_invs invariant_class_of invariant_check_of cid_long oid is_monitor thy =
thy |> Context.Theory
|> (fn ctxt =>
let val invs = get_ml_invs (Proof_Context.init_global thy)
|> Name_Space.dest_table
val checks = invs |> filter (fn (_, inv) => let val ML_Invariant class = inv
in class |> #class |> equal cid_long
end)
|> map (fn (_, inv) => let val ML_Invariant check = inv
in check |> #check end)
val checks = invs |> filter (fn (name, _) =>
equal (invariant_class_of name thy) cid_long)
|> map (fn (name, _) => invariant_check_of name thy)
|> map (fn check => check oid is_monitor ctxt)
in (List.all I checks) end)
in (forall I checks) end)
val check_ml_invs = check_invs get_ml_invariants
val check_ml_invs = check_invs get_ml_invariants ml_invariant_class_of ml_invariant_check_of
val check_opening_ml_invs = check_invs get_opening_ml_invariants
val check_opening_ml_invs =
check_invs get_opening_ml_invariants opening_ml_invariant_class_of opening_ml_invariant_check_of
val check_closing_ml_invs = check_invs get_closing_ml_invariants
val check_closing_ml_invs =
check_invs get_closing_ml_invariants closing_ml_invariant_class_of closing_ml_invariant_check_of
(* Output name for LaTeX macros.
Also rewrite "." to allow macros with objects long names *)
@ -833,12 +831,10 @@ val ISA_prefix = "Isabelle_DOF_"
val doc_class_prefix = ISA_prefix ^ "doc_class_"
val long_doc_class_prefix = ISA_prefix ^ "long_doc_class_"
fun is_ISA s = String.isPrefix ISA_prefix (Long_Name.base_name s)
fun get_class_name_without_prefix s = String.extract (s, String.size(doc_class_prefix), NONE)
fun get_doc_class_name_without_ISA_prefix s = String.extract (s, String.size(ISA_prefix), NONE)
fun transduce_term_global {mk_elaboration=mk_elaboration} (term,pos) thy =
(* pre: term should be fully typed in order to allow type-related term-transformations *)
@ -1066,27 +1062,6 @@ struct
fun err msg pos = error (msg ^ Position.here pos);
fun warn msg pos = warning (msg ^ Position.here pos);
fun check_path check_file ctxt dir (name, pos) =
let
val _ = Context_Position.report ctxt pos (Markup.language_path true); (* TODO: pos should be
"lifted" to
type source *)
val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
val _ = Path.expand path handle ERROR msg => err msg pos;
val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
val _ =
(case check_file of
NONE => path
| SOME check => (check path handle ERROR msg => err msg pos));
in path end;
fun ML_isa_antiq check_file thy (name, _, pos) =
let val path = check_path check_file (Proof_Context.init_global thy) Path.current (name, pos);
in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
fun ML_isa_check_generic check thy (term, pos) =
let val name = (HOLogic.dest_string term
handle TERM(_,[t]) => error ("wrong term format: must be string constant: "
@ -1115,19 +1090,20 @@ fun ML_isa_check_thm thy (term, _, pos) _ =
fun ML_isa_check_file thy (term, _, pos) _ =
let fun check thy (name, _) = name |> Syntax.read_input
|> Resources.check_file (Proof_Context.init_global thy) NONE
|> Resources.check_file (Proof_Context.init_global thy) NONE
in ML_isa_check_generic check thy (term, pos) end;
fun check_instance thy (term, _, pos) s =
let
val bname = Long_Name.base_name s;
val qual = Long_Name.qualifier s;
val class_name =
Long_Name.qualify qual (String.extract(bname , String.size(DOF_core.doc_class_prefix), NONE));
val class_name = (case try (unprefix DOF_core.doc_class_prefix) bname of
NONE => unprefix DOF_core.long_doc_class_prefix bname
| SOME name => name)
|> Long_Name.qualify qual
fun check thy (name, _) =
let
val object_cid = let val DOF_core.Instance cid = DOF_core.get_instance_global name thy
in cid |> #cid end
val object_cid = DOF_core.cid_of name thy
fun check' (class_name, object_cid) =
if class_name = object_cid then
DOF_core.value_of name thy
@ -1150,6 +1126,11 @@ fun ML_isa_check_trace_attribute thy (term, _, _) _ =
val _ = DOF_core.get_instance_global oid thy
in SOME term end
fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ =
case term_option of
NONE => error("Wrong term option. You must use a defined term")
| SOME term => Const (isa_name, ty) $ term
(* Convert excluded mixfix symbols.
Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
we can not use "_" or "'" for classes names in term antiquotation.
@ -1159,10 +1140,19 @@ val clean_string = translate_string
| "'" => "-"
| c => c);
fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ =
case term_option of
NONE => error("Wrong term option. You must use a defined term")
| SOME term => Const (isa_name, ty) $ term
fun rm_mixfix name mixfix thy =
let
val old_constants =
Consts.dest (Sign.consts_of thy) |> #constants
|> map fst
|> filter (Long_Name.base_name #> equal name)
|> map (pair mixfix)
|> map swap
|> map (apfst (Syntax.read_term_global thy))
|> map (apsnd Mixfix.mixfix)
in thy |> (Local_Theory.notation false Syntax.mode_default old_constants
|> Named_Target.theory_map)
end
fun elaborate_instance thy _ _ term_option pos =
case term_option of
@ -1177,49 +1167,64 @@ fun elaborate_instance thy _ _ term_option pos =
because the class name is already bound to "doc_class Regular_Exp.rexp" constant
by add_doc_class_cmd function
*)
fun declare_ISA_class_accessor_and_check_instance doc_class_name =
fun declare_ISA_class_accessor_and_check_instance (doc_class_name, bind_pos) thy =
let
val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name
val typestring = "string => " ^ (Binding.name_of doc_class_name)
val conv_class_name = clean_string (Binding.name_of doc_class_name)
val mixfix_string = "@{" ^ conv_class_name ^ " _}"
val bname = Long_Name.base_name doc_class_name
val bname' = prefix DOF_core.doc_class_prefix bname
val bind = bname' |> pair bind_pos |> swap |> Binding.make
val bind' = prefix DOF_core.long_doc_class_prefix bname
|> pair bind_pos |> swap |> Binding.make
val const_typ = \<^typ>\<open>string\<close> --> Syntax.read_typ (Proof_Context.init_global thy) doc_class_name
fun mixfix_enclose name = name |> enclose "@{" " _}"
val mixfix = clean_string bname |> mixfix_enclose
val mixfix' = clean_string doc_class_name |> mixfix_enclose
in
Sign.add_consts_cmd [(bind, typestring, Mixfix.mixfix(mixfix_string))]
#> DOF_core.add_isa_transformer bind ((check_instance, elaborate_instance)
|> DOF_core.make_isa_transformer)
thy |> rm_mixfix bname' mixfix
|> Sign.add_consts [(bind, const_typ, Mixfix.mixfix mixfix)]
|> DOF_core.add_isa_transformer bind ((check_instance, elaborate_instance)
|> DOF_core.make_isa_transformer)
|> Sign.add_consts [(bind', const_typ, Mixfix.mixfix mixfix')]
|> DOF_core.add_isa_transformer bind' ((check_instance, elaborate_instance)
|> DOF_core.make_isa_transformer)
end
fun elaborate_instances_list thy isa_name _ _ _ =
let
val base_name = Long_Name.base_name isa_name
fun get_isa_name_without_intances_suffix s =
String.extract (s, 0, SOME (String.size(s) - String.size(instances_of_suffixN)))
val base_name_without_suffix = get_isa_name_without_intances_suffix base_name
val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix)
val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
(base_name')
val long_class_name = DOF_core.get_onto_class_name_global base_name' thy
val qualifier = Long_Name.qualifier isa_name
val isa_name' = (case try (unprefix DOF_core.doc_class_prefix) base_name of
NONE => unprefix DOF_core.long_doc_class_prefix base_name
| SOME name => name)
|> unsuffix instances_of_suffixN
|> Long_Name.qualify qualifier
val class_typ = isa_name' |> Proof_Context.read_typ (Proof_Context.init_global thy)
val long_class_name = DOF_core.get_onto_class_name_global isa_name' thy
val values = thy |> Proof_Context.init_global |> DOF_core.get_instances
|> Name_Space.dest_table
|> filter (fn (_, instance) =>
let val DOF_core.Instance cid = instance
in (cid |> #cid) = long_class_name end)
|> filter (fn (name, _) => equal (DOF_core.cid_of name thy) long_class_name)
|> map (fn (oid, _) => DOF_core.value_of oid thy)
in HOLogic.mk_list class_typ values end
fun declare_class_instances_annotation thy doc_class_name =
fun declare_class_instances_annotation (doc_class_name, bind_pos) thy =
let
val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name
|> Binding.suffix_name instances_of_suffixN
val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
((Binding.name_of doc_class_name) ^ " List.list")
val conv_class_name' = clean_string ((Binding.name_of doc_class_name) ^ instances_of_suffixN)
val mixfix_string = "@{" ^ conv_class_name' ^ "}"
val bname = Long_Name.base_name doc_class_name
val bname' = prefix DOF_core.doc_class_prefix bname |> suffix instances_of_suffixN
val bind = bname' |> pair bind_pos |> swap |> Binding.make
val bind' = prefix DOF_core.long_doc_class_prefix bname
|> suffix instances_of_suffixN |> pair bind_pos |> swap |> Binding.make
val class_typ = doc_class_name |> Proof_Context.read_typ (Proof_Context.init_global thy)
fun mixfix_enclose name = name |> enclose "@{" "}"
val mixfix = clean_string (bname ^ instances_of_suffixN) |> mixfix_enclose
val mixfix' = clean_string (doc_class_name ^ instances_of_suffixN) |> mixfix_enclose
in
Sign.add_consts [(bind, class_list_typ, Mixfix.mixfix(mixfix_string))]
#> DOF_core.add_isa_transformer bind ((check_identity, elaborate_instances_list)
|> DOF_core.make_isa_transformer)
thy |> rm_mixfix bname' mixfix
|> Sign.add_consts [(bind, \<^Type>\<open>list class_typ\<close>, Mixfix.mixfix mixfix)]
|> DOF_core.add_isa_transformer bind ((check_identity, elaborate_instances_list)
|> DOF_core.make_isa_transformer)
|> Sign.add_consts [(bind', \<^Type>\<open>list class_typ\<close>, Mixfix.mixfix mixfix')]
|> DOF_core.add_isa_transformer bind' ((check_identity, elaborate_instances_list)
|> DOF_core.make_isa_transformer)
end
fun symbex_attr_access0 ctxt proj_term term =
@ -2172,16 +2177,32 @@ fun document_output_reports name {markdown, body} sem_attrs transform_attr meta_
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} sem_attrs transform_attr meta_args text ctxt end;
val config = {markdown = markdown, markup = markup}
in document_output config sem_attrs transform_attr meta_args text ctxt
end;
(* document output commands *)
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)
(Toplevel.presentation_context #> document_output_reports name mark sem_attrs transform_attr meta_args text #> SOME)));
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >>
(fn (meta_args, text) =>
Toplevel.theory' (fn _ => cmd meta_args)
((Toplevel.presentation_context
#> document_output_reports name mark sem_attrs transform_attr meta_args text
#> SOME): Toplevel.state -> Latex.text option)) );
fun float_command (name, pos) descr (mark: {body: bool, markdown: bool})
cmd output_figure =
Outer_Syntax.command (name, pos) descr
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >>
(fn (meta_args, text) =>
Toplevel.theory' (fn _ => cmd meta_args)
(Toplevel.presentation_context
#> (fn ctxt => (output_figure mark (meta_args, text)) ctxt)
#> SOME)))
(* Core Command Definitions *)
@ -2952,6 +2973,7 @@ fun define_inv cid_long ((lbl, pos), inv) thy =
fun add_doc_class_cmd overloaded (raw_params, binding)
raw_parent raw_fieldsNdefaults reject_Atoms regexps invariants thy =
let
val bind_pos = Binding.pos_of binding
val ctxt = Proof_Context.init_global thy;
val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
@ -3008,8 +3030,8 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
(* The function declare_ISA_class_accessor_and_check_instance uses a prefix
because the class name is already bound to "doc_class Regular_Exp.rexp" constant
by add_doc_class_cmd function *)
|> ISA_core.declare_ISA_class_accessor_and_check_instance binding
|> (fn thy => (ISA_core.declare_class_instances_annotation thy binding) thy)
|> (fn thy => ISA_core.declare_ISA_class_accessor_and_check_instance (cid thy, bind_pos) thy)
|> (fn thy => ISA_core.declare_class_instances_annotation (cid thy, bind_pos) thy)
end;

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

@ -17,6 +17,7 @@ theory "M_01_Introduction"
begin
(*>*)
chapter*[intro::introduction]\<open> Introduction \<close>
text*[introtext::introduction]\<open>
The linking of the \<^emph>\<open>formal\<close> to the \<^emph>\<open>informal\<close> is perhaps the most pervasive challenge in the
@ -149,12 +150,6 @@ text\<open>
\<^url>\<open>https://doi.org/10.1007/978-3-030-34968-4_4\<close>.
\end{quote}
\<close>
subsubsection\<open>Availability\<close>
text\<open>
The implementation of the framework is available at
\url{\<^dofurl>}. The website also provides links to the latest releases. \<^isadof> is licensed
under a 2-clause BSD license (SPDX-License-Identifier: BSD-2-Clause).
\<close>
(*<*)
end

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

@ -20,7 +20,7 @@ begin
chapter*[background::text_section]\<open> Background\<close>
section*[bgrnd1::introduction]\<open>The Isabelle System Architecture\<close>
figure*[architecture::figure,relative_width="95",src="''figures/isabelle-architecture''"]\<open>
figure*[architecture::figure,relative_width="95",file_src="''figures/isabelle-architecture.pdf''"]\<open>
The system architecture of Isabelle (left-hand side) and the
asynchronous communication between the Isabelle system and
the IDE (right-hand side). \<close>
@ -45,16 +45,15 @@ The current system framework offers moreover the following features:
the most prominent and deeply integrated system component.
\<close>
text\<open>
The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers,
The Isabelle system architecture shown in @{figure \<open>architecture\<close>} comes with many layers,
with Standard ML (SML) at the bottom layer as implementation language. The architecture actually
foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \<^boxed_sml>\<open>Context\<close>.
This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an
ancestor-list as well as typed, user-defined state for plugins such as \<^isadof>.
On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific
support for higher specification constructs were built.
\<^footnote>\<open>We use the term \<^emph>\<open>plugin\<close> for a collection of HOL-definitions, SML and Scala code in order
to distinguish it from the official Isabelle term \<^emph>\<open>component\<close> which implies a particular
format and support by the Isabelle build system.\<close>
support for higher specification constructs were built.\<^footnote>\<open>We use the term \<^emph>\<open>plugin\<close> for a collection
of HOL-definitions, SML and Scala code in order to distinguish it from the official Isabelle
term \<^emph>\<open>component\<close> which implies a particular format and support by the Isabelle build system.\<close>
\<close>
section*[dof::introduction]\<open>The Document Model Required by \<^dof>\<close>
@ -87,7 +86,7 @@ text\<open>
main sub-document type, for historical reasons, \<^emph>\<open>theory\<close>-files. A theory file\<^bindex>\<open>theory!file\<close>
consists of a \<^emph>\<open>header\<close>\<^bindex>\<open>header\<close>, a \<^emph>\<open>context definition\<close>\<^index>\<open>context\<close>, and a body
consisting of a sequence of document elements called
\<^emph>\<open>command\<close>s (see @{figure (unchecked) "docModGenConcr"}(left)). Even
\<^emph>\<open>command\<close>s (see @{figure (unchecked) "docModGenConcr"} (left-hand side)). Even
the header consists of a sequence of commands used for introductory text elements not depending on
any context. The context-definition contains an \<^boxed_theory_text>\<open>import\<close> and a
\<^boxed_theory_text>\<open>keyword\<close> section, for example:
@ -102,17 +101,18 @@ text\<open>
\<^boxed_theory_text>\<open>keywords\<close> are used to separate commands from each other.
\<close>
side_by_side_figure*[docModGenConcr::side_by_side_figure,anchor="''docModGen''",
caption="''Schematic Representation.''",relative_width="45",
src="''figures/doc-mod-generic.pdf''",anchor2="''docModIsar''",
caption2="''The Isar Instance.''",relative_width2="45",
src2="''figures/doc-mod-isar.pdf''"]\<open>A Representation of a Document Model.\<close>
text*[docModGenConcr::float,
main_caption="\<open>A Representation of a Document Model.\<close>"]
\<open>
@{fig_content (width=45, caption="Schematic Representation.") "figures/doc-mod-generic.pdf"
}\<^hfill>@{fig_content (width=45, caption="The Isar Instance.") "figures/doc-mod-isar.pdf"}
\<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
the the begin of a text that is parsed by a command-specific parser; the end of the
command-span is defined by the next keyword. Commands were used to define definitions, lemmas,
code and text-elements (see @{figure "docModGenConcr"}(right)). \<close>
code and text-elements (see @{float "docModGenConcr"} (right-hand side)). \<close>
text\<open> A simple text-element \<^index>\<open>text-element\<close> may look like this:
@ -147,8 +147,8 @@ Its Its general syntactic format reads as follows:
The sub-context may be different from the surrounding one; therefore, it is possible
to switch from a text-context to a term-context, for example. Therefore, antiquotations allow
the nesting of cartouches, albeit not all combinations are actually supported.
\<^footnote>\<open>In the literature, this concept has been referred to \<open>Cascade-Syntax\<close> and was used in the
the nesting of cartouches, albeit not all combinations are actually supported.\<^footnote>\<open>In the
literature, this concept has been referred to \<open>Cascade-Syntax\<close> and was used in the
Centaur-system and is existing in some limited form in some Emacs-implementations these days. \<close>
Isabelle comes with a number of built-in antiquotations for text- and code-contexts;
a detailed overview can be found in @{cite "wenzel:isabelle-isar:2020"}. \<^dof> reuses this general
@ -182,17 +182,18 @@ text\<open>Antiquotations seen as semantic macros are partial functions of type
typeset. They represent the device for linking formal with the informal content.
\<close>
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.pdf''",anchor2="''docModDOF''",
caption2="''Ontological References.''",relative_width2="47",
src2="''figures/doc-mod-onto-docinst.pdf''"]\<open>Documents conform to Ontologies.\<close>
text*[docModOnto::float,
main_caption="\<open>Documents conform to Ontologies.\<close>"]
\<open>
@{fig_content (width=47, caption="A Document with Ontological Annotations.") "figures/doc-mod-DOF.pdf"
}\<^hfill>@{fig_content (width=47, caption="Ontological References.") "figures/doc-mod-onto-docinst.pdf"}
\<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\<^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
specific for a given domain-specific universe of discourse (see @{float "docModOnto"}). ODL will
be described in @{text_section (unchecked) "isadof_tour"} in more detail.\<close>
section*[bgrnd21::introduction]\<open>Implementability of the Document Model in other ITP's\<close>
@ -207,13 +208,13 @@ text\<open>
in many features over-accomplishes the required features of \<^dof>.
\<close>
figure*["fig:dof-ide"::figure,relative_width="95",src="''figures/cicm2018-combined''"]\<open>
figure*["fig:dof-ide",relative_width="95",file_src="''figures/cicm2018-combined.png''"]\<open>
The \<^isadof> IDE (left) and the corresponding PDF (right), showing the first page
of~@{cite "brucker.ea:isabelle-ontologies:2018"}.\<close>
text\<open>
We call the present implementation of \<^dof> on the Isabelle platform \<^isadof> .
@{docitem "fig:dof-ide"} shows a screen-shot of an introductory paper on
@{figure "fig:dof-ide"} shows a screen-shot of an introductory paper on
\<^isadof>~@{cite "brucker.ea:isabelle-ontologies:2018"}: the \<^isadof> PIDE can be seen on the left,
while the generated presentation in PDF is shown on the right.

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

@ -30,14 +30,13 @@ section*[getting_started::technical]\<open>Getting Started\<close>
subsection*[installation::technical]\<open>Installation\<close>
text\<open>
In this section, we will show how to install \<^isadof> and its pre-requisites: Isabelle and
\<^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
In this section, we will show how to install \<^isadof>. We assume a basic familiarity with a
Linux/Unix-like command line (i.e., a shell).
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 \<^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>
\<^isadof> requires Isabelle\<^bindex>\<open>Isabelle\<close> with a recent \<^LaTeX>-distribution
(e.g., Tex Live 2022 or later).
\<close>
@ -55,14 +54,13 @@ full qualified path.
\<close>
text\<open>
Furthermore, download the latest version of the AFP from \<^url>\<open>https://www.isa-afp.org/download/\<close> and
Next, download the the AFP from \<^url>\<open>https://www.isa-afp.org/download/\<close> and
follow the instructions given at \<^url>\<open>https://www.isa-afp.org/help/\<close> for installing the AFP as an
Isabelle component.\<close>
paragraph\<open>Installing \<^TeXLive>.\<close>
text\<open>
Modern Linux distribution will allow you to install \<^TeXLive> using their respective package
managers. On a modern Debian system or a Debian derivative (\<^eg>, Ubuntu), the following command
On a Debian-based Linux system (\<^eg>, Ubuntu), the following command
should install all required \<^LaTeX> packages:
@{boxed_bash [display]\<open>ë\prompt{}ë sudo aptitude install texlive-full\<close>}
\<close>
@ -70,34 +68,23 @@ text\<open>
subsubsection*[isadof::technical]\<open>Installing \<^isadof>\<close>
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:
is currently consisting out of three AFP entries:
\<^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. The text is based on the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"};
introductory paper. The text is based on~@{cite "brucker.ea:isabelle-ontologies:2018"};
in the document, 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.
to demonstrate that \<^isadof> can be used for writing documents with very little direct use of
\<^LaTeX>.
\<^item> \<^verbatim>\<open>Isabelle_DOF-Example-II\<close>: This entry contains another example of
a mathematics-oriented academic paper. It is based on the iFM 2020 paper~@{cite "taha.ea:philosophers:2020"}.
a mathematics-oriented academic paper. It is based on~@{cite "taha.ea:philosophers:2020"}.
It represents 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, and therefore does deliberately not exploit \<^isadof> 's full potential.
\<^item> \<^verbatim>\<open>Isabelle_DOF-Examples-Extra\<close>: This sessen contains a collection of other examples;
but is only accessible at the developer git
\<^url>\<open>https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/src/branch/main/Isabelle_DOF-Examples-Extra\<close>.
% The \<^isadof> distribution contains both examples using the ontology \<^verbatim>\<open>scholarly_paper\<close> in
% the directory \<^nolinkurl>\<open>examples/scholarly_paper/2018-cicm-isabelle_dof-applications/\<close> or
% \<^nolinkurl>\<open>examples/scholarly_paper/2020-iFM-CSP\<close>.
It is recommended to follow the structure these examples.\<close>
types, terms and theorems, and therefore does deliberately not exploit \<^isadof> 's full potential.\<close>
section*[writing_doc::technical]\<open>Writing Documents\<close>
@ -116,27 +103,18 @@ session example = Isabelle_DOF +
options [document = pdf, document_output = "output", document_build = dof]
(*theories [document = false]
A
B
theories
C
D*)
B*)
\end{config}
The document template and ontology can be selected as follows:
@{boxed_theory_text [display]
\<open>
theory
C
imports
Isabelle_DOF.technical_report
Isabelle_DOF.scholarly_paper
begin
list_templates
use_template "scrreprt-modern"
list_ontologies
use_ontology "technical_report" and "scholarly_paper"
theory C imports Isabelle_DOF.technical_report Isabelle_DOF.scholarly_paper begin
list_templates
use_template "scrreprt-modern"
list_ontologies
use_ontology "technical_report" and "scholarly_paper"
end
\<close>}
@ -170,7 +148,6 @@ session example = HOL +
options [document = pdf, document_output = "output", document_build = dof]
session
Isabelle_DOF.scholarly_paper
Isabelle_DOF.technical_report
theories
C
\end{config}
@ -236,32 +213,21 @@ subsection\<open>Editing 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, for examples
using these ontologies we refer to the example sessions described in \<^technical>\<open>isadof\<close>.
engineering.
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>\<open>Isabelle_DOF-Example-I/IsaDofApplications.thy"\<close>
\<^item> starting Isabelle/jEdit from the command line by, \<^eg>, calling:
@{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë
isabelle jedit -d . Isabelle_DOF-Example-II/paper.thy \<close>}
% bu assumes a particular organisation of Isabelle_DOF, Isabelle_DOF-Example-I, ... and an according ROOTS here ...
\<close>
text\<open> You can build the \<^pdf>-document at the command line by calling:
@{boxed_bash [display] \<open>ë\prompt{}ë isabelle build -d . IsaDofApplications \<close>}
\<close>
text\<open> You can build the \<^pdf>-document at the command line by calling:
@{boxed_bash [display] \<open>ë\prompt{}ë isabelle build Isabelle_DOF-Example-I\<close>}
\<close>
subsection*[sss::technical]\<open>A Bluffers Guide to the \<^verbatim>\<open>scholarly_paper\<close> Ontology\<close>
text\<open> In this section we give a minimal overview of the ontology formalized in
\<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>.\<close>
text\<open> We start by modeling the usual text-elements of an academic paper: the title and author
information, abstract, and text section:
text\<open> In this section we give a minimal overview of the ontology formalized in
\<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>. We start by modeling the usual text-elements of an
academic paper: the title and author information, abstract, and text section:
@{boxed_theory_text [display]
\<open>doc_class title =
short_title :: "string option" <= "None"
@ -313,13 +279,9 @@ as follows:
\<^item> subsubsection \<^index>\<open>subsubsection\<close> \<open>Some 3\<close> \<^vs>\<open>-0.3cm\<close>
Additional means assure that the following invariant is maintained in a document
conforming to \<^verbatim>\<open>scholarly_paper\<close>:
\<^center>\<open>\<open>level > 0\<close>\<close>
conforming to \<^verbatim>\<open>scholarly_paper\<close>: \<open>level > 0\<close>.
\<close>
text\<open>\<^vs>\<open>1.0cm\<close>\<close>
text\<open> The rest of the ontology introduces concepts for \<^typ>\<open>introduction\<close>, \<^typ>\<open>conclusion\<close>,
\<^typ>\<open>related_work\<close>, \<^typ>\<open>bibliography\<close> etc. More details can be found in \<^verbatim>\<open>scholarly_paper\<close>
contained in the theory \<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>. \<close>
@ -332,10 +294,10 @@ which is written in the so-called free-form style: Formulas are superficially pa
type-set, but no deeper type-checking and checking with the underlying logical context
is undertaken. \<close>
figure*[fig0::figure,spawn_columns=False,relative_width="90",src="''figures/header_CSP_source.png''"]
figure*[fig0::figure,relative_width="85",file_src="''figures/header_CSP_source.png''"]
\<open> A mathematics paper as integrated document source ... \<close>
figure*[fig0B::figure,spawn_columns=False,relative_width="90",src="''figures/header_CSP_pdf.png''"]
figure*[fig0B::figure,relative_width="85",file_src="''figures/header_CSP_pdf.png''"]
\<open> ... and as corresponding \<^pdf>-output. \<close>
text\<open>The integrated source of this paper-excerpt is shown in \<^figure>\<open>fig0\<close>, while the
@ -382,7 +344,7 @@ standard inductive \<^theory_text>\<open>datatype\<close> definition mechanism i
for attribute declarations. Vice-versa, document class definitions imply a corresponding HOL type
definition. \<close>
figure*[fig01::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP.png''"]
figure*[fig01::figure,relative_width="95",file_src="''figures/definition-use-CSP.png''"]
\<open> A screenshot of the integrated source with definitions ...\<close>
text\<open>An example for a sequence of (Isabelle-formula-)texts, their ontological declarations as
\<^typ>\<open>definition\<close>s in terms of the \<^verbatim>\<open>scholarly_paper\<close>-ontology and their type-conform referencing
@ -406,7 +368,7 @@ We refrain ourselves here to briefly describe three freeform antiquotations used
\<^item> the freeform antiquotations for verbatim, emphasized, bold, or footnote text elements.
\<close>
figure*[fig02::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP-pdf.png''"]
figure*[fig02::figure,relative_width="95",file_src="''figures/definition-use-CSP-pdf.png''"]
\<open> ... and the corresponding \<^pdf>-output.\<close>
text\<open>
@ -431,7 +393,7 @@ doc_class figure = text_section +
spawn_columns :: bool <= True
\<close>}
\<close>
figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figures/Dogfood-figures''"]
figure*[fig_figures::figure,relative_width="85",file_src="''figures/Dogfood-figures.png''"]
\<open> Declaring figures in the integrated source.\<close>
text\<open>
@ -466,42 +428,40 @@ which signals to \<^isadof> begin and end of the part of the integrated source
in which the text-elements instances are expected to appear in the textual ordering
defined by \<^typ>\<open>article\<close>.
\<close>
text*[exploring::float,
main_caption="\<open>Exploring text elements.\<close>"]
\<open>
@{fig_content (width=45, caption="Exploring a reference of a text-element.") "figures/Dogfood-II-bgnd1.png"
}\<^hfill>@{fig_content (width=45, caption="Exploring the class of a text element.") "figures/Dogfood-III-bgnd-text_section.png"}
\<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''",
caption2="''Exploring the class of a text element.''",relative_width2="47",
src2="''figures/Dogfood-III-bgnd-text_section''"]\<open>Exploring text elements.\<close>
side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-jumpInDocCLass''",
caption="''Hyperlink to class-definition.''",relative_width="48",
src="''figures/Dogfood-IV-jumpInDocCLass''",
anchor2="''fig:Dogfood-V-attribute''",
caption2="''Exploring an attribute (hyperlinked to the class).''",
relative_width2="47",
src2="''figures/Dogfood-V-attribute''"]\<open>Navigation via generated hyperlinks.\<close>
text*[hyperlinks::float,
main_caption="\<open>Navigation via generated hyperlinks.\<close>"]
\<open>
@{fig_content (width=45, caption="Hyperlink to class-definition.") "figures/Dogfood-IV-jumpInDocCLass.png"
}\<^hfill>@{fig_content (width=45, caption="Exploring an attribute (hyperlinked to the class).") "figures/Dogfood-V-attribute.png"}
\<close>
text\<open>
From these class definitions, \<^isadof> also automatically generated editing
support for Isabelle/jEdit. In
@{figure "exploring"}(left)
@{float "exploring"}(left)
% \autoref{fig-Dogfood-II-bgnd1}
and
@{figure "exploring"}(right)
@{float "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 (
@{figure "hyperlinks"}(left)
@{float "hyperlinks"}(left)
%\autoref{fig:Dogfood-IV-jumpInDocCLass})
; hovering over an attribute-definition (which is qualified in order to disambiguate; cf.
@{figure "hyperlinks"}(right)
@{float "hyperlinks"}(right)
%\autoref{fig:Dogfood-V-attribute}
) shows its type.
\<close>
figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-VI-linkappl.png''"]
figure*[figDogfoodVIlinkappl::figure,relative_width="80",file_src="''figures/Dogfood-VI-linkappl.png''"]
\<open>Exploring an ontological reference.\<close>
text\<open>
@ -524,16 +484,14 @@ text\<open>The present version of \<^isadof> is the first version that supports
\<^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>
in class instances. They have the format: \<open>@{name arg\<^sub>1 ... arg\<^sub>n\<^sub>-\<^sub>1} arg\<^sub>n\<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''"]
figure*[doc_termAq::figure,relative_width="35",file_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>
@ -567,14 +525,13 @@ Isabelle/Isar \<^theory_text>\<open>theorem\<close>-command will in contrast to
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>
document comments : \<open>(*<*) ... (*>*)\<close>.\<close>
section*[tech_onto::example]\<open>Writing Technical Reports in \<^boxed_theory_text>\<open>technical_report\<close>\<close>
text\<open>While it is perfectly possible to write documents in the
\<^verbatim>\<open>technical_report\<close> ontology in freeform-style (the present manual is mostly an
example for this category), we will briefly explain here the tight-checking-style in which
\<^verbatim>\<open>technical_report\<close> ontology in freeform-style (this manual is mostly such an
example), we will briefly explain here the tight-checking-style in which
most Isabelle reference manuals themselves are written.
The idea has already been put forward by Isabelle itself; besides the general infrastructure on
@ -627,9 +584,8 @@ text\<open>They are text-contexts equivalents to the \<^theory_text>\<open>term*
for term-contexts introduced in @{technical (unchecked) \<open>subsec:onto-term-ctxt\<close>}\<close>
subsection\<open>A Technical Report with Tight Checking\<close>
text\<open>An example of tight checking is a small programming manual developed by the
second author in order to document programming trick discoveries while implementing in Isabelle.
While not necessarily a meeting standards of a scientific text, it appears to us that this information
text\<open>An example of tight checking is a small programming manual to document programming trick
discoveries while implementing in Isabelle. While not necessarily a meeting standards of a scientific text, it appears to us that this information
is often missing in the Isabelle community.
So, if this text addresses only a very limited audience and will never be famous for its style,
@ -639,13 +595,13 @@ So its value is that readers can just reuse some of these snippets and adapt the
purposes.
\<close>
figure*[strict_SS::figure, relative_width="95", src="''figures/MyCommentedIsabelle.png''"]
figure*[strict_em::figure, relative_width="95", file_src="''figures/MyCommentedIsabelle.png''"]
\<open>A table with a number of SML functions, together with their type.\<close>
text\<open>
\<open>TR_MyCommentedIsabelle\<close> is written according to the \<^verbatim>\<open>technical_report\<close> ontology in
This manual is written according to the \<^verbatim>\<open>technical_report\<close> ontology in
\<^theory>\<open>Isabelle_DOF.technical_report\<close>.
\<^figure>\<open>strict_SS\<close> shows a snippet from this integrated source and gives an idea why
\<^figure>\<open>strict_em\<close> shows a snippet from this integrated source and gives an idea why
its tight-checking allows for keeping track of underlying Isabelle changes:
Any reference to an SML operation in some library module is type-checked, and the displayed
SML-type really corresponds to the type of the operations in the underlying SML environment.
@ -673,8 +629,7 @@ 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>,
can be found in the Isabelle reference manual @{cite "wenzel:isabelle-isar:2020"},
section 4.2.
In practice, \<^isadof> documents with ambitious layout will contain a certain number of
@ -683,7 +638,7 @@ not possible. As far as possible, raw \<^LaTeX> should be restricted to the defi
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>).
(cf. @{cite "wenzel:isabelle-isar:2020"}).
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

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

@ -309,8 +309,8 @@ text\<open>
Moreover, as usual, special care has to be taken for commands that write into aux-files
that are included in a following \<^LaTeX>-run. For such complex examples, we refer the interested
reader to the style files provided in the \<^isadof> distribution. In particular
the definitions of the concepts \<^boxed_theory_text>\<open>title*\<close> and \<^boxed_theory_text>\<open>author*\<close> in the
file \<^file>\<open>../../ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close> show examples of protecting
the definitions of the concepts \<^boxed_theory_text>\<open>title*\<close> and \<^boxed_theory_text>\<open>author*\<close> in \<^LaTeX>-style
for the ontology @{theory \<open>Isabelle_DOF.scholarly_paper\<close>} shows examples of protecting
special characters in definitions that need to make use of a entries in an aux-file.
\<close>
@ -659,9 +659,9 @@ text\<open>
.2 Isa\_COL.section.
.2 Isa\_COL.subsection.
.2 Isa\_COL.subsubsection.
.1 Isa\_COL.figure.
.2 Isa\_COL.side\_by\_side\_figure.
.1 Isa\_COL.figure\_group.
.1 Isa\_COL.float{...}.
.2 Isa\_COL.figure{...}.
.2 Isa\_COL.listing{...}.
.1 \ldots.
}
\end{minipage}
@ -692,9 +692,40 @@ elements such as, \<^ie>, paragraphs (this mirrors restrictions of the target \<
The attribute \<^const>\<open>variants\<close> refers to an Isabelle-configuration attribute that permits
to steer the different versions of a \<^LaTeX>-presentation of the integrated source.
For further information of the root classes such as \<^typ>\<open>figure\<close>'s, please consult the ontology in
\<^theory>\<open>Isabelle_DOF.Isa_COL\<close> directly. \<^verbatim>\<open>COL\<close> finally provides macros that extend the command-language
of the DOF core by the following
For further information of the root classes such as \<^bindex>\<open>float\<close> \<^typ>\<open>float\<close>'s, please consult
the ontology in \<^theory>\<open>Isabelle_DOF.Isa_COL\<close> directly and consult the Example I and II for
their pragmatics. The \<^theory>\<open>Isabelle_DOF.Isa_COL\<close> also provides the subclasses
\<^typ>\<open>figure\<close> \<^bindex>\<open>figure\<close> and \<^bindex>\<open>listing\<close> \<^typ>\<open>listing\<close> which together with specific
text-antiquotations like:
\<^enum> \<open>@{theory_text [options] "path"}\<close> (Isabelle)
\<^enum> \<open>@{fig_content (width=\<dots>, height=\<dots>, caption=\<dots>) "path"}\<close> (COL)
\<^enum> \<open>@{boxed_theory_text [display] \<open> ... \<close> }\<close> (local, e.g. manual)
\<^enum> \<open>@{boxed_sml [display] \<open> ... \<close> }\<close> (local, e.g. manual)
\<^enum> \<open>@{boxed_pdf [display] \<open> ... \<close> }\<close> (local, e.g. manual)
\<^enum> \<open>@{boxed_latex [display] \<open> ... \<close> }\<close> (local, e.g. manual)
\<^enum> \<open>@{boxed_bash [display] \<open> ... \<close> }\<close> (local, e.g. manual)\<close>
(*<*)
text\<open>With these primitives, it is possible to compose listing-like text-elements or
side-by-side-figures as shown in the subsequent example:
@{boxed_theory_text [display]\<open>
text*[inlinefig::float,
main_caption="\<open>The Caption.\<close>"]
\<open>@{theory_text [display, margin = 5] \<open>lemma A :: "a \<longrightarrow> b"\<close>}\<close>
text*[dupl_graphics::float,
main_caption="\<open>The Caption.\<close>"]
\<open>
@{fig_content (width=40, height=35, caption="This is a left test") "figures/A.png"
}\<^hfill>@{fig_content (width=40, height=35, caption="This is a right \<^term>\<open>\<sigma>\<^sub>i + 1\<close> test") "figures/B.png"}
\<close>\<close>}\<close>
text\<open>The \<^theory_text>\<open>side_by_side_figure*\<close>-command \<^bindex>\<open>side\_by\_side\_figure\<close> has been deprecated.\<close>
(*>*)
text\<open>
\<^verbatim>\<open>COL\<close> finally provides macros that extend the command-language of the DOF core by the following
abbreviations:
\<^item> \<open>derived_text_element\<close> :
@ -702,7 +733,7 @@ abbreviations:
( ( @@{command "chapter*"}
| @@{command "section*"} | @@{command "subsection*"} | @@{command "subsubsection*"}
| @@{command "paragraph*"}
| @@{command "figure*"} | @@{command "side_by_side_figure*"}
| @@{command "figure*"} | @@{command "listing*"}
)
\<newline>
'[' meta_args ']' '\<open>' text '\<close>'
@ -1401,35 +1432,22 @@ text\<open>
\<^LaTeX>-packages that are (strictly) required by the used \<^LaTeX>-setup. In general, we recommend
to only add \<^LaTeX>-packages that are always necessary for this particular template, as loading
packages in the templates minimizes the freedom users have by adapting the \<^path>\<open>preample.tex\<close>.
Moreover, you might want to add/modify the template specific configuration
(\autoref{lst:config-start}-\ref{lst:config-end}). The new template should be stored in
\<^path>\<open>src/document-templates\<close> and its file name should start with the prefix \<^path>\<open>root-\<close>. After
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:
The file name of the new template should start with the prefix \<^path>\<open>root-\<close> and need to be
registered using the \<^theory_text>\<open>define_template\<close> command.
a typical \<^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
\usepackage[T1]{fontenc} % Font encoding
\usepackage[utf8]{inputenc} % UTF8 support
\usepackage{xcolor}
\usepackage{isabelle,isabellesym,amssymb} % Required (by Isabelle)
\usepackage{amsmath} % Used by some ontologies
\bibliographystyle{abbrv}
\input{dof-common} % setup shared between all Isabelle/DOF templates
\usepackage{graphicx} % Required for images.
\usepackage[caption]{subfig}
\usepackage{DOF-core}
\usepackage{subcaption}
\usepackage[size=footnotesize]{caption}
\usepackage{hyperref} % Required by Isabelle/DOF
%% Begin of template specific configuration ë\label{lst:config-start}ë
\urlstyle{rm}
\isabellestyle{it} ë\label{lst:config-end}ë
\usepackage{hyperref}
%% Main document, do not modify
\begin{document}
\maketitle\input{session}
\maketitle
\IfFileExists{dof_session.tex}{\input{dof_session}}{\input{session}}
\IfFileExists{root.bib}{\bibliography{root}}{}
\end{document}
\end{ltx}\<close>
@ -1576,9 +1594,6 @@ text\<open>
}
\end{ltx}\<close>
For a real-world example testing for multiple classes, see
\<^file>\<open>../../ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close>:
We encourage this clear and machine-checkable enforcement of restrictions while, at the same
time, we also encourage to provide a package option to overwrite them. The latter allows
inherited ontologies to overwrite these restrictions and, therefore, to provide also support

5
Isabelle_DOF/thys/manual/M_05_Implementation.thy
View File

@ -144,9 +144,10 @@ text\<open>
@{boxed_sml [display]
\<open>val _ = Theory.setup
(docitem_antiquotation @{binding "docitem"} DOF_core.default_cid #>
(docitem_antiquotation @{binding "docitem"} DOF_core.default_cid #>
ML_Antiquotation.inline @{binding "docitem_value"} ML_antiquotation_docitem_value)\<close>}
ML_Antiquotation.inline @{binding "docitem_value"}
ML_antiquotation_docitem_value)\<close>}
the text antiquotation \<^boxed_sml>\<open>docitem\<close> is declared and bounded to a parser for the argument
syntax and the overall semantics. This code defines a generic antiquotation to be used in text
elements such as

7
README.md
View File

@ -2,8 +2,6 @@
Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle.
Isabelle/DOF allows for both conventional typesetting and formal development.
The manual for [Isabelle/DOF 1.3.0/Isabelle2021-1 is available
online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.pdf)
## Pre-requisites
@ -31,13 +29,16 @@ distribution for your operating system from the [Isabelle
website](https://isabelle.in.tum.de/). Furthermore, please install the AFP
following the instructions given at <https://www.isa-afp.org/help.html>.
Isabelle/DOF is currently consisting out of two AFP entries:
Isabelle/DOF is currently consisting out of three AFP entries:
* [Isabelle_DOF:](https://www.isa-afp.org/entries/Isabelle_DOF.html) This entry
contains the Isabelle/DOF system itself, including the Isabelle/DOF manual.
* [Isabelle_DOF-Example-I:](https://www.isa-afp.org/entries/Isabelle_DOF-Example-I.html)
This entry contains an example of an academic paper written using the
Isabelle/DOF system.
* [Isabelle_DOF-Example-II:](https://www.isa-afp.org/entries/Isabelle_DOF-Example-II.html)
This entry contains an example of an academic paper written using the
Isabelle/DOF system.
-->