Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
This commit is contained in:
commit
b43de570a4
|
|
@ -43,7 +43,7 @@ text\<open>For now, as the term annotation is not bound to a meta logic which wi
|
|||
\<^term>\<open>[@{term ''True''}]\<close> to \<^term>\<open>[True]\<close>, we can not use the HOL \<^const>\<open>True\<close> constant
|
||||
in the assertion.\<close>
|
||||
|
||||
ML\<open> @{term "[@{term \<open>True \<longrightarrow> True \<close>}]"}; (* with isa-check *) \<close>
|
||||
ML\<open> @{term_ "[@{term \<open>True \<longrightarrow> True \<close>}]"}; (* with isa-check *) \<close>
|
||||
|
||||
ML\<open>
|
||||
(* Checking the default classes which should be in a neutral(unset) state. *)
|
||||
|
|
@ -64,7 +64,7 @@ ML\<open>
|
|||
\<close>
|
||||
|
||||
|
||||
Definition*[e1::"definition"]\<open>Lorem ipsum dolor sit amet, ... \<close>
|
||||
Definition*[e1]\<open>Lorem ipsum dolor sit amet, ... \<close>
|
||||
text\<open>Note that this should yield a warning since \<^theory_text>\<open>Definition*\<close> uses as "implicit default" the class
|
||||
\<^doc_class>\<open>math_content\<close> which has no \<^term>\<open>text_element.level\<close> set, however in this context,
|
||||
it is required to be a positive number since it is \<^term>\<open>text_element.referentiable\<close> .
|
||||
|
|
|
|||
|
|
@ -73,6 +73,33 @@
|
|||
public = {yes}
|
||||
}
|
||||
|
||||
@InCollection{ brucker.ea:deep-ontologies:2023,
|
||||
author = {Achim D. Brucker and Idir Ait-Sadoune and Nicolas Meric and Burkhart Wolff},
|
||||
booktitle = {9th International Conference on Rigorous State-Based Methods (ABZ 2023)},
|
||||
language = {USenglish},
|
||||
publisher = {Springer-Verlag},
|
||||
address = {Heidelberg},
|
||||
series = {Lecture Notes in Computer Science},
|
||||
number = {XXXXX},
|
||||
title = {{U}sing {D}eep {O}ntologies in {F}ormal {S}oftware {E}ngineering},
|
||||
year = {2023},
|
||||
abstract = {Isabelle/DOF is an ontology framework on top of Isabelle Isabelle/DOF allows for the
|
||||
formal development of ontologies as well as continuous conformity-checking of
|
||||
integrated documents annotated by ontological data. An integrated document may
|
||||
contain text, code, definitions, proofs and user-programmed constructs supporting a
|
||||
wide range of Formal Methods. Isabelle/DOF is designed to leverage traceability in
|
||||
integrated documents by supporting navigation in Isabelle’s IDE as well as the
|
||||
document generation process.
|
||||
In this paper we extend Isabelle/DOF with annotations of terms, a pervasive
|
||||
data-structure underlying Isabelle used to syntactically rep- resent expressions
|
||||
and formulas. Rather than introducing an own pro- gramming language for meta-data,
|
||||
we use Higher-order Logic (HOL) for expressions, data-constraints, ontological
|
||||
invariants, and queries via code-generation and reflection. This allows both for
|
||||
powerful query languages and logical reasoning over ontologies in, for example,
|
||||
ontological mappings. Our application examples cover documents targeting formal
|
||||
certifications such as CENELEC, Common Criteria, etc.}
|
||||
}
|
||||
|
||||
@InCollection{ brucker.ea:isabelle-ontologies:2018,
|
||||
abstract = {While Isabelle is mostly known as part of Isabelle/HOL (an
|
||||
interactive theorem prover), it actually provides a
|
||||
|
|
|
|||
|
|
@ -53,12 +53,12 @@ ML\<open>
|
|||
val _ =
|
||||
Monitor_Command_Parser.document_command \<^command_keyword>\<open>abstract*\<close> "Textual Definition"
|
||||
{markdown = true, body = true}
|
||||
(Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []);
|
||||
(Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []) (K(K I));
|
||||
|
||||
val _ =
|
||||
Monitor_Command_Parser.document_command \<^command_keyword>\<open>author*\<close> "Textual Definition"
|
||||
{markdown = true, body = true}
|
||||
(Onto_Macros.enriched_document_cmd_exp (SOME "author") []);
|
||||
(Onto_Macros.enriched_document_cmd_exp (SOME "author") []) (K(K I));
|
||||
\<close>
|
||||
|
||||
text\<open>Scholarly Paper is oriented towards the classical domains in science:
|
||||
|
|
@ -444,48 +444,49 @@ fun doc_cmd kwd txt flag key =
|
|||
in
|
||||
Onto_Macros.enriched_formal_statement_command default [("mcc",key)] meta_args thy
|
||||
end)
|
||||
(Onto_Macros.transform_attr [("mcc",key)])
|
||||
|
||||
in
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Definition*\<close> "Freeform Definition"
|
||||
Definition_default_class \<^const_name>\<open>defn\<close>;
|
||||
Definition_default_class "defn";
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Lemma*\<close> "Freeform Lemma Description"
|
||||
Lemma_default_class \<^const_name>\<open>lemm\<close>;
|
||||
Lemma_default_class "lemm";
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Theorem*\<close> "Freeform Theorem"
|
||||
Theorem_default_class \<^const_name>\<open>theom\<close>;
|
||||
Theorem_default_class "theom";
|
||||
|
||||
(* cut and paste to make it runnable, but nonsensical so far: *)
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Proposition*\<close> "Freeform Proposition"
|
||||
Proposition_default_class \<^const_name>\<open>prpo\<close>;
|
||||
Proposition_default_class "prpo";
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Premise*\<close> "Freeform Premise"
|
||||
Premise_default_class \<^const_name>\<open>prms\<close>;
|
||||
Premise_default_class "prms";
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Corollary*\<close> "Freeform Corollary"
|
||||
Corollary_default_class \<^const_name>\<open>corr\<close>;
|
||||
Corollary_default_class "corr";
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Consequence*\<close> "Freeform Consequence"
|
||||
Consequence_default_class \<^const_name>\<open>cons\<close>;
|
||||
Consequence_default_class "cons";
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Conclusion*\<close> "Freeform Conclusion"
|
||||
Conclusion_default_class \<^const_name>\<open>conc_stmt\<close>;
|
||||
Conclusion_default_class "conc_stmt";
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Assumption*\<close> "Freeform Assumption"
|
||||
Assumption_default_class \<^const_name>\<open>assm\<close>;
|
||||
Assumption_default_class "assm";
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Hypothesis*\<close> "Freeform Hypothesis"
|
||||
Hypothesis_default_class \<^const_name>\<open>prpo\<close>;
|
||||
Hypothesis_default_class "prpo";
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Assertion*\<close> "Freeform Assertion"
|
||||
Assertion_default_class \<^const_name>\<open>assn\<close>;
|
||||
Assertion_default_class "assn";
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Proof*\<close> "Freeform Proof"
|
||||
Proof_default_class \<^const_name>\<open>prf_stmt\<close>;
|
||||
Proof_default_class "prf_stmt";
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Example*\<close> "Freeform Example"
|
||||
Example_default_class \<^const_name>\<open>expl_stmt\<close>;
|
||||
Example_default_class "expl_stmt";
|
||||
end
|
||||
end
|
||||
\<close>
|
||||
|
|
@ -554,6 +555,7 @@ print_doc_classes
|
|||
print_doc_class_template "definition" (* just a sample *)
|
||||
print_doc_class_template "lemma" (* just a sample *)
|
||||
print_doc_class_template "theorem" (* just a sample *)
|
||||
print_doc_class_template "premise" (* just a sample *)
|
||||
|
||||
|
||||
subsection\<open>Structuring Enforcement in Engineering/Math Papers \<close>
|
||||
|
|
|
|||
|
|
@ -103,13 +103,44 @@ fun transform_cid thy NONE X = X
|
|||
end
|
||||
in
|
||||
|
||||
fun enriched_formal_statement_command ncid (S: (string * string) list) =
|
||||
let fun transform_attr doc_attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @
|
||||
(("formal_results",@{here}),"([]::thm list)")::doc_attrs
|
||||
in fn margs => fn thy =>
|
||||
fun transform_attr S cid_long thy doc_attrs =
|
||||
let
|
||||
fun transform_attr' [] doc_attrs = doc_attrs
|
||||
| transform_attr' (s::S) (doc_attrs) =
|
||||
let fun markup2string s = s |> YXML.content_of
|
||||
|> Symbol.explode
|
||||
|> List.filter (fn c => c <> Symbol.DEL)
|
||||
|> String.concat
|
||||
fun toLong n = DOF_core.get_attribute_info cid_long (markup2string n) thy
|
||||
|> the |> #long_name
|
||||
val (name', value) = s |> (fn (n, v) => (toLong n, v))
|
||||
val doc_attrs' = doc_attrs
|
||||
|> map (fn (name, term) => if name = name'
|
||||
then (name, value)
|
||||
else (name, term))
|
||||
in if doc_attrs' = doc_attrs
|
||||
then transform_attr' S doc_attrs' |> cons (name', value)
|
||||
else transform_attr' S doc_attrs'
|
||||
end
|
||||
in transform_attr' S doc_attrs end
|
||||
|
||||
(*fun update_meta_args_attrs S
|
||||
((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) =
|
||||
(((oid, pos),cid_pos), transform_attr S doc_attrs)
|
||||
*)
|
||||
(*fun enriched_formal_statement_command ncid (S: (string * string) list) =
|
||||
fn margs => fn thy =>
|
||||
Monitor_Command_Parser.gen_enriched_document_cmd {inline=true}
|
||||
(transform_cid thy ncid) transform_attr margs thy
|
||||
end;
|
||||
(transform_cid thy ncid) (transform_attr S) margs thy
|
||||
*)
|
||||
|
||||
fun enriched_formal_statement_command ncid (S: (string * string) list) =
|
||||
let fun transform_attr doc_attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @
|
||||
(("formal_results",@{here}),"([]::thm list)")::doc_attrs
|
||||
in fn margs => fn thy =>
|
||||
Monitor_Command_Parser.gen_enriched_document_cmd {inline=true}
|
||||
(transform_cid thy ncid) transform_attr margs thy
|
||||
end;
|
||||
|
||||
fun enriched_document_cmd_exp ncid (S: (string * string) list) =
|
||||
(* expands ncid into supertype-check. *)
|
||||
|
|
@ -123,7 +154,7 @@ end (* local *)
|
|||
|
||||
fun heading_command (name, pos) descr level =
|
||||
Monitor_Command_Parser.document_command (name, pos) descr
|
||||
{markdown = false, body = true} (enriched_text_element_cmd level);
|
||||
{markdown = false, body = true} (enriched_text_element_cmd level) (K(K I));
|
||||
|
||||
val _ = heading_command \<^command_keyword>\<open>title*\<close> "section heading" NONE;
|
||||
val _ = heading_command \<^command_keyword>\<open>subtitle*\<close> "section heading" NONE;
|
||||
|
|
|
|||
|
|
@ -2137,17 +2137,15 @@ fun close_monitor_command (args as (((oid, pos), cid_pos),
|
|||
end
|
||||
|
||||
|
||||
fun meta_args_2_latex thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) =
|
||||
fun meta_args_2_latex thy transform_attr
|
||||
((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) =
|
||||
(* for the moment naive, i.e. without textual normalization of
|
||||
attribute names and adapted term printing *)
|
||||
let val l = DOF_core.get_instance_name_global lab thy |> enclose "{" "}"
|
||||
|> prefix "label = "
|
||||
(* val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *)
|
||||
val cid_long = case cid_opt of
|
||||
NONE => let val DOF_core.Instance cid =
|
||||
DOF_core.get_instance_global lab thy
|
||||
in cid |> #cid end
|
||||
|
||||
NONE => DOF_core.cid_of lab thy
|
||||
| SOME(cid,_) => DOF_core.get_onto_class_name_global' cid thy
|
||||
(* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *)
|
||||
val cid_txt = "type = " ^ (enclose "{" "}" cid_long);
|
||||
|
|
@ -2195,8 +2193,11 @@ fun meta_args_2_latex thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Pa
|
|||
|
||||
val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a)
|
||||
(map (fn (c,_) => c) actual_args))) default_args
|
||||
val str_args = map (fn (lhs,rhs) => lhs^" = "^(enclose "{" "}" rhs))
|
||||
(actual_args@default_args_filtered)
|
||||
val transformed_args = (actual_args@default_args_filtered)
|
||||
|> transform_attr cid_long thy
|
||||
val str_args = transformed_args
|
||||
|> map (fn (lhs,rhs) => lhs^" = "^(enclose "{" "}" rhs))
|
||||
|
||||
val label_and_type = String.concat [ l, ",", cid_txt]
|
||||
val str_args = label_and_type::str_args
|
||||
in
|
||||
|
|
@ -2220,15 +2221,15 @@ fun gen_enriched_document_cmd' {inline} cid_transform attr_transform
|
|||
(* {markdown = true} sets the parsing process such that in the text-core
|
||||
markdown elements are accepted. *)
|
||||
|
||||
fun document_output {markdown: bool, markup: Latex.text -> Latex.text} meta_args text ctxt =
|
||||
fun document_output {markdown: bool, markup: Latex.text -> Latex.text} transform_attr meta_args text ctxt =
|
||||
let
|
||||
val thy = Proof_Context.theory_of ctxt;
|
||||
val _ = Context_Position.reports ctxt (Document_Output.document_reports text);
|
||||
val output_meta = meta_args_2_latex thy meta_args;
|
||||
val output_meta = meta_args_2_latex thy transform_attr meta_args;
|
||||
val output_text = Document_Output.output_document ctxt {markdown = markdown} text;
|
||||
in markup (output_meta @ output_text) end;
|
||||
|
||||
fun document_output_reports name {markdown, body} meta_args text ctxt =
|
||||
fun document_output_reports name {markdown, body} transform_attr meta_args text ctxt =
|
||||
let
|
||||
(*val pos = Input.pos_of text;
|
||||
val _ =
|
||||
|
|
@ -2238,16 +2239,16 @@ fun document_output_reports name {markdown, body} meta_args text ctxt =
|
|||
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} meta_args text ctxt end;
|
||||
in document_output {markdown = markdown, markup = markup} transform_attr meta_args text ctxt end;
|
||||
|
||||
|
||||
(* document output commands *)
|
||||
|
||||
fun document_command (name, pos) descr mark cmd =
|
||||
fun document_command (name, pos) descr mark cmd 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 meta_args text #> SOME)));
|
||||
(Toplevel.presentation_context #> document_output_reports name mark transform_attr meta_args text #> SOME)));
|
||||
|
||||
|
||||
(* Core Command Definitions *)
|
||||
|
|
@ -2273,14 +2274,14 @@ val _ =
|
|||
|
||||
val _ =
|
||||
document_command \<^command_keyword>\<open>text*\<close> "formal comment (primary style)"
|
||||
{markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I);
|
||||
{markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I) (K(K I));
|
||||
|
||||
|
||||
(* This is just a stub at present *)
|
||||
val _ =
|
||||
document_command \<^command_keyword>\<open>text-macro*\<close> "formal comment macro"
|
||||
{markdown = true, body = true}
|
||||
(gen_enriched_document_cmd {inline=false} (* declare as macro *) I I);
|
||||
(gen_enriched_document_cmd {inline=false} (* declare as macro *) I I) (K(K I));
|
||||
|
||||
|
||||
val (declare_reference_default_class, declare_reference_default_class_setup)
|
||||
|
|
|
|||
|
|
@ -30,6 +30,7 @@ define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
|
|||
BibTeX \<rightleftharpoons> \<open>\BibTeX{}\<close>
|
||||
LaTeX \<rightleftharpoons> \<open>\LaTeX{}\<close>
|
||||
TeX \<rightleftharpoons> \<open>\TeX{}\<close>
|
||||
dofurl \<rightleftharpoons> \<open>\dofurl\<close>
|
||||
pdf \<rightleftharpoons> \<open>PDF\<close>
|
||||
|
||||
text\<open>Note that these setups assume that the associated \<^LaTeX> macros
|
||||
|
|
|
|||
|
|
@ -38,26 +38,34 @@ and their logical contexts).
|
|||
|
||||
Further applications are the domain-specific discourse in juridical texts or medical reports.
|
||||
In general, an ontology is a formal explicit description of \<^emph>\<open>concepts\<close> in a domain of discourse
|
||||
(called \<^emph>\<open>classes\<close>), properties of each concept describing \<^emph>\<open>attributes\<close> of the concept, as well
|
||||
as \<^emph>\<open>links\<close> between them. A particular link between concepts is the \<^emph>\<open>is-a\<close> relation declaring
|
||||
(called \<^emph>\<open>classes\<close>), components (called \<^emph>\<open>attributes\<close>) of the concept, and properties (called
|
||||
\<^emph>\<open>invariants\<close>) on concepts. Logically, classes are represented by a type (the class type) and
|
||||
particular terms representing \<^emph>\<open>instances\<close> of them. Since components are typed, it is therefore
|
||||
possible to express \<^emph>\<open>links\<close> like \<open>m\<close>-to-\<open>n\<close> relations between classes.
|
||||
Another form of link between concepts is the \<^emph>\<open>is-a\<close> relation declaring
|
||||
the instances of a subclass to be instances of the super-class.
|
||||
|
||||
To address this challenge, 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, 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 evolution, where the
|
||||
\<^emph>\<open>coherence\<close> between the formal and the informal parts of the content can be mechanically checked.
|
||||
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
|
||||
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,
|
||||
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
|
||||
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
|
||||
\<^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"}.\<close>
|
||||
into the Isabelle/Isar framework in the style of~@{cite "wenzel.ea:building:2007"}. However,
|
||||
\<^isadof> will generate from ontologies a theory infrastructure consisting of types, terms, theorems
|
||||
and code that allows both interactive checking as well as formal reasoning over meta-data
|
||||
related to annotated documents.\<close>
|
||||
|
||||
subsubsection\<open>How to Read This Manual\<close>
|
||||
(*<*)
|
||||
|
|
@ -91,9 +99,9 @@ text\<open>
|
|||
by simp\<close>}
|
||||
\<^item> a green background for examples of generated document fragments (\<^ie>, PDF output):
|
||||
@{boxed_pdf [display] \<open>The axiom refl\<close>}
|
||||
\<^item> a red background for (S)ML-code:
|
||||
\<^item> a red background for SML-code:
|
||||
@{boxed_sml [display] \<open>fun id x = x\<close>}
|
||||
\<^item> a yellow background for \LaTeX-code:
|
||||
\<^item> a yellow background for \<^LaTeX>-code:
|
||||
@{boxed_latex [display] \<open>\newcommand{\refl}{$x = x$}\<close>}
|
||||
\<^item> a grey background for shell scripts and interactive shell sessions:
|
||||
@{boxed_bash [display]\<open>ë\prompt{}ë ls
|
||||
|
|
@ -104,6 +112,15 @@ subsubsection\<open>How to Cite \<^isadof>\<close>
|
|||
text\<open>
|
||||
If you use or extend \<^isadof> in your publications, please use
|
||||
\<^item> for the \<^isadof> system~@{cite "brucker.ea:isabelle-ontologies:2018"}:
|
||||
\begin{quote}\small
|
||||
A.~D. Brucker, I.~Ait-Sadoune, N. Méric, and B.~Wolff. Using Deep Ontologies in Formal
|
||||
Software Engineering. In \<^emph>\<open>International Conference on Rigorous State-Based Methods (ABZ 2023)\<close>,
|
||||
To appear in Lecture Notes in Computer Science. Springer-Verlag,
|
||||
Heidelberg, 2023. \href{https://doi.org/???} {10.1007/????????}.
|
||||
\end{quote}
|
||||
A \<^BibTeX>-entry is available at:
|
||||
\<^url>\<open>https://www.lri.fr/~wolff/bibtex/wolff.html\<close>.
|
||||
\<^item> an older description of the system~@{cite "brucker.ea:isabelle-ontologies:2018"}:
|
||||
\begin{quote}\small
|
||||
A.~D. Brucker, I.~Ait-Sadoune, P.~Crisafulli, and B.~Wolff. Using the {Isabelle} ontology
|
||||
framework: Linking the formal with the informal. In \<^emph>\<open>Conference on Intelligent Computer
|
||||
|
|
@ -128,13 +145,13 @@ text\<open>
|
|||
Using Ontologies in Formal Developments Targeting Certification.
|
||||
In W. Ahrendt and S. Tarifa, editors. \<^emph>\<open>Integrated Formal Methods (IFM)\<close>, number 11918.
|
||||
Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
|
||||
\href{https://doi.org/10.1007/978-3-030-34968-4\_4}.
|
||||
\<^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
|
||||
\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>
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019-2022 The University of Exeter
|
||||
* 2018-2022 The University of Paris-Saclay
|
||||
* 2019-2023 The University of Exeter
|
||||
* 2018-2023 The University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -30,8 +30,8 @@ While Isabelle is widely perceived as an interactive theorem
|
|||
prover for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we would like to emphasize
|
||||
the view that Isabelle is far more than that: it is the \<^emph>\<open>Eclipse of Formal Methods Tools\<close>. This
|
||||
refers to the ``\<^emph>\<open>generic system framework of Isabelle/Isar underlying recent versions of Isabelle.
|
||||
Among other things, Isar provides an infrastructure for Isabelle plug-ins, comprising extensible
|
||||
state components and extensible syntax that can be bound to ML programs. Thus, the Isabelle/Isar
|
||||
Among other things, Isabelle provides an infrastructure for Isabelle plug-ins, comprising extensible
|
||||
state components and extensible syntax that can be bound to SML programs. Thus, the Isabelle
|
||||
architecture may be understood as an extension and refinement of the traditional `LCF approach',
|
||||
with explicit infrastructure for building derivative systems.\<close>''~@{cite "wenzel.ea:building:2007"}
|
||||
|
||||
|
|
@ -49,9 +49,13 @@ The Isabelle system architecture shown in @{docitem \<open>architecture\<close>}
|
|||
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 components (plugins) such as \<^isadof>.
|
||||
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.\<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>
|
||||
text\<open>
|
||||
|
|
@ -72,13 +76,13 @@ declare_reference*["fig:dependency"::figure]
|
|||
text\<open>
|
||||
The Isabelle Framework is based on a \<^emph>\<open>document-centric view\<close>\<^bindex>\<open>document-centric view\<close> of
|
||||
a document, treating the input in its integrality as set of (user-programmable) \<^emph>\<open>document element\<close>
|
||||
that may mutually depend on and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured in a set of
|
||||
\<^verbatim>\<open>ROOT\<close>- and \<^verbatim>\<open>ROOTS\<close>-files.
|
||||
that may mutually depend on and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured
|
||||
in a set of \<^verbatim>\<open>ROOT\<close>- and \<^verbatim>\<open>ROOTS\<close>-files.
|
||||
|
||||
Isabelle assumes a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document
|
||||
consist of a hierarchy of \<^emph>\<open>sub-documents\<close> (files); dependencies are restricted to be
|
||||
acyclic at this level.
|
||||
Sub-documents can have different document types in order to capture documentations consisting of
|
||||
Document parts can have different document types in order to capture documentations consisting of
|
||||
documentation, models, proofs, code of various forms and other technical artifacts. We call the
|
||||
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
|
||||
|
|
@ -108,9 +112,9 @@ contains characters and a special notation for semantic macros \<^bindex>\<open>
|
|||
(here \<^theory_text>\<open>@{term "fac 5"}).\<close>
|
||||
\<close>
|
||||
|
||||
text\<open>While we concentrate in this manual on \<^theory_text>\<open>text\<close>-document elements --- this is the main
|
||||
use of \<^dof> in its current stage --- it is important to note that there are actually three
|
||||
families of ``ontology aware'' document elements with analogous
|
||||
text\<open>While \<^theory_text>\<open>text\<close>- elements play a major role in this manual on
|
||||
--- this is the main use of \<^dof> in its current stage --- it is important to note that there
|
||||
are actually three families of ``ontology aware'' document elements with analogous
|
||||
syntax to standard ones. The difference is a bracket with meta-data of the form:
|
||||
@{theory_text [display,indent=5, margin=70]
|
||||
\<open>
|
||||
|
|
@ -123,7 +127,8 @@ Depending on the family, we will speak about \<^emph>\<open>(formal) text-contex
|
|||
\<^emph>\<open>(ML) code-contexts\<close>\<^index>\<open>code-contexts\<close> and \<^emph>\<open>term-contexts\<close>\<^index>\<open>term-contexts\<close> if we refer
|
||||
to sub-elements inside the \<open>\<open>...\<close>\<close> cartouches of these command families. Note that the Isabelle
|
||||
framework allows for nesting cartouches that permits to support switching into a different
|
||||
context. In general, this has also the effect that the evaluation of antiquotations changes.
|
||||
context, albeit not all combinations are actually supported.
|
||||
In general, nesting contexts has the effect that the evaluation of antiquotations changes.
|
||||
\<^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>
|
||||
\<close>
|
||||
|
|
|
|||
Loading…
Reference in New Issue