nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Merge branch 'main' into isabelle_nightly

This commit is contained in:
Achim D. Brucker 2023-05-15 10:20:12 +02:00
parent a93046beac 7e698a9e69
commit 4adbe4ce81
20 changed files with 238 additions and 338 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.woodpecker/build.yml
View File

@ -14,6 +14,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

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

@ -209,9 +209,8 @@ let val class_ids_so_far = ["Conceptual.A", "Conceptual.B", "Conceptual.C", "Co
"Conceptual.E", "Conceptual.F", "Conceptual.G", "Conceptual.M",
"Isa_COL.float", "Isa_COL.figure", "Isa_COL.chapter", "Isa_COL.listing",
"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.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>

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

@ -178,69 +178,30 @@ section\<open>Simulation of a Monitor\<close>
declare[[free_class_in_monitor_checking]]
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,
relative_width="90",
file_src="''figures/A.png''"]
\<open> The A train \ldots \<close>
figure*[fig_B::figure,
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,
relative_width="90",
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,
relative_width="90",
file_src="''figures/B.png''"]
\<open> The D train \ldots \<close>
close_monitor*[figs3]
open_monitor*[figs4::figure_group,
caption="''Sample ''"]
ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
text*[testRejected1::figure_group, caption="''document/figures/A.png''"]
\<open> The A train \ldots \<close>
figure*[fig_E::figure,
relative_width="90",
file_src="''figures/B.png''"]
\<open> The E train \ldots \<close>
close_monitor*[figs4]
close_monitor*[figs2]
text*[testRejected2::figure_group, caption="''document/figures/A.png''"]
\<open> The A train \ldots \<close>
close_monitor*[figs1]
declare[[free_class_in_monitor_checking = false]]
text\<open>Resulting trace of figs1 as ML antiquotation: \<close>
ML \<open>@{trace_attribute figs1}\<close>
text\<open>Resulting trace of figs as text antiquotation:\<close>
text\<open>@{trace_attribute figs1}\<close>
section\<open>A Complex Evaluation involving Automatas\<close>
text\<open>Test trace\_attribute term antiquotation:\<close>
term*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
value*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
definition example_expression where "example_expression \<equiv> \<lbrace>\<lfloor>''Conceptual.A''\<rfloor> || \<lfloor>''Conceptual.F''\<rfloor>\<rbrace>\<^sup>*"
value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \<open>aaa\<close>}) \<close>

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

@ -56,3 +56,4 @@ text*[dupl_graphics::float,
end
(*>*)

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

Binary file not shown.

18
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,4 @@ France, and therefore granted with public funds of the Program ``Investissements
\expandafter\index\expandafter{\expanded{#2 (#1)}}%
}%
\AtBeginDocument{\isabellestyle{literal}\newcommand{\lstnumberautorefname}{Line}}

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

@ -44,7 +44,7 @@
\allowdisplaybreaks[4]
\newenvironment{frontmatter}{}{}
\raggedbottom
\begin{document}
\begin{frontmatter}
\maketitle

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

@ -59,6 +59,7 @@
,plainpages=false
} % more detailed digital TOC (aka bookmarks)
\sloppy
\raggedbottom
\allowdisplaybreaks[4]
\newenvironment{frontmatter}{}{}

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

@ -41,6 +41,7 @@
,plainpages=false
} % more detailed digital TOC (aka bookmarks)
\sloppy
\raggedbottom
\allowdisplaybreaks[4]
\begin{document}

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)"

190
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
@ -147,56 +147,6 @@ end
\<close>
section\<open> Library of Standard Text 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"
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>
ML\<open>
@ -244,6 +194,52 @@ 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>
(*<*)
@ -257,11 +253,11 @@ 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>
@ -304,14 +300,6 @@ fun fig_content_modes (ctxt, toks) =
(toks)
in (y, (ctxt, toks')) end
fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) =
Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) =>
(check ctxt NONE source;
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))
@ -343,6 +331,7 @@ fun fig_content ctxt (cfg_trans,file:Input.source) =
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, ... *)
@ -350,13 +339,13 @@ fun fig_content ctxt (cfg_trans,file:Input.source) =
in if Input.string_of(caption) = "" then
file
|> (Latex.string o Input.string_of)
|> (XML.enclose ("\\includegraphics"^arg^"{") "}")
|> Latex.macro ("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.macro0 "centering")
@ (Latex.macro ("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 *)
@ -377,35 +366,26 @@ val _ = Theory.setup
ML\<open>
(*
type fig_content = {relative_width : int, (* percent of textwidth, default 100 *)
relative_height : int, (* percent, default 100 *)
caption : Input.source (* default empty *)}
*)
val SPY = Unsynchronized.ref("")
(* ML\<open>snd(HOLogic.dest_number(Syntax.read_term @{context} (!SPY)))\<close>
*)
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."
fun convert_meta_args ctxt (X, (((str,_),value) :: R)) =
let fun conv_int x = snd(HOLogic.dest_number(Syntax.read_term ctxt x))
handle TERM _ => 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)
o convert_meta_args ctxt (X, R)
| "relative_height" => upd_relative_height (conv_int value)
o convert_meta_args (X, R )
| "file_src" => convert_meta_args (X, R)
o convert_meta_args ctxt (X, R )
| "file_src" => convert_meta_args ctxt (X, R)
| s => error("!undefined attribute:"^s))
end
|convert_meta_args (X,[]) = I
|convert_meta_args _ (_,[]) = I
fun convert_src_from_margs (X, (((str,_),value)::R)) =
fun convert_src_from_margs ctxt (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.")
"file_src" => Input.string (HOLogic.dest_string (Syntax.read_term ctxt value))
| _ => convert_src_from_margs ctxt (X,R))
|convert_src_from_margs _ (_, []) = error("No file_src provided.")
fun float_command (name, pos) descr cid =
let fun set_default_class NONE = SOME(cid,pos)
@ -415,33 +395,29 @@ fun float_command (name, pos) descr cid =
{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 opts (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)))
|> (Latex.environment ("figure") )
in Monitor_Command_Parser.float_command (name, pos) descr opts create_instance parse_and_tex
fun parse_and_tex (margs, text) ctxt = (convert_src_from_margs ctxt margs)
|> pair (upd_caption Input.empty #> convert_meta_args ctxt margs)
|> fig_content ctxt
|> (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 create_instance parse_and_tex
end
\<close>
ML\<open>
(* *********************************************************************** *)
(* Ontological Macro Command Support *)
(* *********************************************************************** *)
float_command \<^command_keyword>\<open>figure*\<close> "figure" "Isa_COL.figure" ;
val _ = Onto_Macros.heading_command \<^command_keyword>\<open>side_by_side_figure*\<close> "multiple figures" NONE;
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
@ -701,16 +677,13 @@ 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] (height = 80, width=80, caption=\<open>this is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<dots>\<close>)
\<open>figures/isabelle-architecture.pdf\<close>}\<close>
@ -725,5 +698,4 @@ text\<open> @{table_inline [display] (cell_placing = center,cell_height =\<open
(*>*)
text\<open>@{term_ \<open>3 + 4::int\<close>} @{value_ \<open>3 + 4::int\<close>} \<close>
end

13
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -2004,7 +2004,7 @@ fun update_instance_command (((oid, pos), cid_pos),
(* General criticism : attributes like "level" were treated here in the kernel instead of dragging
them out into the COL -- bu *)
fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) =
fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy =
let fun o_m_c oid pos cid_pos doc_attrs thy =
Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor=true} (* this is a monitor *)
@ -2016,7 +2016,7 @@ fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Par
val DOF_core.Onto_Class X = DOF_core.get_onto_class_global' cid thy
val ralph = RegExpInterface.alphabet (#rejectS X)
val aalph = RegExpInterface.alphabet (#rex X)
in (aalph, ralph, map (RegExpInterface.rexp_term2da aalph)(#rex X)) end
in (aalph, ralph, map (RegExpInterface.rexp_term2da thy aalph)(#rex X)) end
fun create_monitor_entry oid thy =
let val cid = case cid_pos of
NONE => ISA_core.err ("You must specified a monitor class.") pos
@ -2026,7 +2026,7 @@ fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Par
(DOF_core.make_monitor_info (accS, rejectS, aS)) thy
end
in
o_m_c oid pos cid_pos doc_attrs #> create_monitor_entry oid
thy |> o_m_c oid pos cid_pos doc_attrs |> create_monitor_entry oid
end;
@ -2187,15 +2187,16 @@ fun document_command (name, pos) descr mark cmd sem_attrs transform_attr =
Toplevel.theory' (fn _ => cmd meta_args)
(SOME (Toplevel.presentation_context #> document_output_reports name mark sem_attrs transform_attr meta_args text))));
fun float_command (name, pos) descr (mark: {body: bool, markdown: bool})
fun float_command (name, pos) descr
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)
(SOME (Toplevel.presentation_context
#> (fn ctxt => (output_figure mark (meta_args, text)) ctxt)
))))
#> output_figure (meta_args, text)
))))
(* Core Command Definitions *)

24
Isabelle_DOF/thys/RegExpInterface.thy
View File

@ -161,8 +161,8 @@ structure RegExpInterface : sig
type cid
val alphabet : term list -> env
val ext_alphabet: env -> term list -> env
val conv : term -> env -> int RegExpChecker.rexp (* for debugging *)
val rexp_term2da: env -> term -> automaton
val conv : theory -> term -> env -> int RegExpChecker.rexp (* for debugging *)
val rexp_term2da: theory -> env -> term -> automaton
val enabled : automaton -> env -> cid list
val next : automaton -> env -> cid -> automaton
val final : automaton -> bool
@ -187,23 +187,23 @@ local open RegExpChecker in
else ()
in res end;
fun conv \<^Const_>\<open>Regular_Exp.rexp.Zero _\<close> _ = Zero
|conv \<^Const_>\<open>Regular_Exp.rexp.One _\<close> _ = Onea
|conv \<^Const_>\<open>Regular_Exp.rexp.Times _ for X Y\<close> env = Times(conv X env, conv Y env)
|conv \<^Const_>\<open>Regular_Exp.rexp.Plus _ for X Y\<close> env = Plus(conv X env, conv Y env)
|conv \<^Const_>\<open>Regular_Exp.rexp.Star _ for X\<close> env = Star(conv X env)
|conv \<^Const_>\<open>RegExpInterface.opt _ for X\<close> env = Plus(conv X env, Onea)
|conv \<^Const_>\<open>RegExpInterface.rep1 _ for X\<close> env = Times(conv X env, Star(conv X env))
|conv (Const (s, \<^Type>\<open>rexp _\<close>)) env =
fun conv _ \<^Const_>\<open>Regular_Exp.rexp.Zero _\<close> _ = Zero
|conv _ \<^Const_>\<open>Regular_Exp.rexp.One _\<close> _ = Onea
|conv thy \<^Const_>\<open>Regular_Exp.rexp.Times _ for X Y\<close> env = Times(conv thy X env, conv thy Y env)
|conv thy \<^Const_>\<open>Regular_Exp.rexp.Plus _ for X Y\<close> env = Plus(conv thy X env, conv thy Y env)
|conv thy \<^Const_>\<open>Regular_Exp.rexp.Star _ for X\<close> env = Star(conv thy X env)
|conv thy \<^Const_>\<open>RegExpInterface.opt _ for X\<close> env = Plus(conv thy X env, Onea)
|conv thy \<^Const_>\<open>RegExpInterface.rep1 _ for X\<close> env = Times(conv thy X env, Star(conv thy X env))
|conv _ (Const (s, \<^Type>\<open>rexp _\<close>)) env =
let val n = find_index (fn x => x = s) env
val _ = if n<0 then error"conversion error of regexp." else ()
in Atom(n) end
|conv S _ = error("conversion error of regexp:" ^ (Syntax.string_of_term (@{context})S))
|conv thy S _ = error("conversion error of regexp:" ^ (Syntax.string_of_term_global thy S))
val eq_int = {equal = curry(op =) : Int.int -> Int.int -> bool};
val eq_bool_list = {equal = curry(op =) : bool list -> bool list -> bool};
fun rexp_term2da env term = let val rexp = conv term env;
fun rexp_term2da thy env term = let val rexp = conv thy term env;
val nda = RegExpChecker.rexp2na eq_int rexp;
val da = RegExpChecker.na2da eq_bool_list nda;
in da end;

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

@ -138,11 +138,11 @@ abstract*[abs, keywordlist="[\<open>Ontology\<close>, \<open>Ontological Modelin
comprehensively its major commands. Many examples show typical best-practice
applications of the system.
It is an unique feature of \<^isadof> that ontologies may be used to control
the link between formal and informal content in documents in a machine
checked way. These links can connect both text elements and formal
It is a unique feature of \<^isadof> that ontologies may be used to control
the link between formal and informal content in documents inan automatic-checked way.
These links can connect both text elements and formal
modeling elements such as terms, definitions, code and logical formulas,
altogether \<^emph>\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
altogether \<^emph>\<open>integrated\<close> into a state-of-the-art interactive theorem prover.
\<close>

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

@ -23,7 +23,7 @@ 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
digitization of knowledge and its propagation. This challenge incites numerous research efforts
summarized under the labels ``semantic web,'' ``data mining,'' or any form of advanced ``semantic''
text processing. A key role in structuring this linking play \<^emph>\<open>document ontologies\<close> (also called
text processing. A key role in structuring this linking plays is \<^emph>\<open>document ontologies\<close> (also called
\<^emph>\<open>vocabulary\<close> in the semantic web community~@{cite "w3c:ontologies:2015"}), \<^ie>, a machine-readable
form of the structure of documents as well as the document discourse.
@ -31,9 +31,9 @@ Such ontologies can be used for the scientific discourse within scholarly articl
libraries, and in the engineering discourse of standardized software certification
documents~@{cite "boulanger:cenelec-50128:2015" and "cc:cc-part3:2006"}. All these
documents contain formal content and have to follow a given structure. In practice, large groups of developers have to produce a substantial
set of documents where the consistency is notoriously difficult to maintain. In particular,
certifications are centered around the \<^emph>\<open>traceability\<close> of requirements throughout the entire
set of documents. While technical solutions for the traceability problem exists (most notably:
set of documents where consistency is notoriously difficult to maintain. In particular,
certifications are centred around the \<^emph>\<open>traceability\<close> of requirements throughout the entire
set of documents. While technical solutions for the traceability problem exist (most notably:
DOORS~@{cite "ibm:doors:2019"}), they are weak in the treatment of formal entities (such as formulas
and their logical contexts).
@ -47,20 +47,20 @@ Another form of link between concepts is the \<^emph>\<open>is-a\<close> relatio
the instances of a subclass to be instances of the super-class.
Engineering an ontological language for documents that contain both formal and informal elements
as occuring in formal theories is a particular challenge. To address this latter, we present
as occurring in formal theories is a particular challenge. To address this latter, we present
the Document Ontology Framework (\<^dof>) and an implementation of \<^dof> called \<^isadof>.
\<^dof> is designed for building scalable and user-friendly tools on top of interactive theorem
provers. \<^isadof> is an instance of this novel framework, implemented as extension of Isabelle/HOL,
provers. \<^isadof> is an instance of this novel framework, implemented as an extension of Isabelle/HOL,
to \<^emph>\<open>model\<close> typed ontologies and to \<^emph>\<open>enforce\<close> them during document evolution. Based on Isabelle's
infrastructures, ontologies may refer to types, terms, proven theorems, code, or established
assertions. Based on a novel adaption of the Isabelle IDE (called PIDE, @{cite "wenzel:asynchronous:2014"}),
a document is checked to be \<^emph>\<open>conform\<close> to a particular ontology---\<^isadof> is designed to give fast
user-feedback \<^emph>\<open>during the capture of content\<close>. This is particularly valuable in case of document
user-feedback \<^emph>\<open>during the capture of content\<close>. This is particularly valuable in the case of document
evolution, where the \<^emph>\<open>coherence\<close> between the formal and the informal parts of the content can
be mechanically checked.
To avoid any misunderstanding: \<^isadof> is \<^emph>\<open>not a theory in HOL\<close> on ontologies and operations to
track and trace links in texts, it is an \<^emph>\<open>environment to write structured text\<close> which
track and trace links in texts. It is an \<^emph>\<open>environment to write structured text\<close> which
\<^emph>\<open>may contain\<close> Isabelle/HOL definitions and proofs like mathematical articles, tech-reports and
scientific papers---as the present one, which is written in \<^isadof> itself. \<^isadof> is a plugin
into the Isabelle/Isar framework in the style of~@{cite "wenzel.ea:building:2007"}. However,
@ -81,13 +81,13 @@ This manual can be read in different ways, depending on what you want to accompl
different main user groups:
\<^enum> \<^emph>\<open>\<^isadof> users\<close>, \<^ie>, users that just want to edit a core document, be it for a paper or a
technical report, using a given ontology. These users should focus on
@{docitem (unchecked) \<open>isadof_tour\<close>} and, depending on their knowledge of Isabelle/HOL, also
@{docitem (unchecked) \<open>isadof_tour\<close>} and, depending on their knowledge of Isabelle/HOL, also on
@{docitem (unchecked) \<open>background\<close>}.
\<^enum> \<^emph>\<open>Ontology developers\<close>, \<^ie>, users that want to develop new ontologies or modify existing
document ontologies. These users should, after having gained acquaintance as a user, focus
on @{docitem (unchecked) \<open>isadof_ontologies\<close>}.
\<^enum> \<^emph>\<open>\<^isadof> developers\<close>, \<^ie>, users that want to extend or modify \<^isadof>, \<^eg>, by adding new
text-elements. These users should read @{docitem (unchecked) \<open>isadof_developers\<close>}
text-elements. These users should read @{docitem (unchecked) \<open>isadof_developers\<close>}.
\<close>
subsubsection\<open>Typographical Conventions\<close>
@ -150,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

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

@ -51,10 +51,9 @@ foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in
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:
@ -113,7 +112,7 @@ text\<open>The body of a theory file consists of a sequence of \<^emph>\<open>co
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 @{float "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:
@ -148,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

129
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,relative_width="90",file_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,relative_width="90",file_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
@ -469,15 +431,15 @@ defined by \<^typ>\<open>article\<close>.
text*[exploring::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"}
@{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>
text*[hyperlinks::float,
main_caption="\<open>Navigation via generated 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 (hyperlinked to the class).") "figures/Dogfood-V-attribute.png"}
@{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>
@ -522,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",file_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>
@ -565,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
@ -625,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,
@ -637,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", file_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.
@ -671,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
@ -681,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.
-->