more on intro
This commit is contained in:
parent
12d33fa457
commit
77150aefe2
|
@ -108,7 +108,7 @@
|
||||||
volume = 2283,
|
volume = 2283,
|
||||||
doi = {10.1007/3-540-45949-9},
|
doi = {10.1007/3-540-45949-9},
|
||||||
abstract = {This book is a self-contained introduction to interactive
|
abstract = {This book is a self-contained introduction to interactive
|
||||||
proof in higher-order logic (\acs{hol}), using the proof
|
proof in higher-order logic HOL, using the proof
|
||||||
assistant Isabelle2002. It is a tutorial for potential
|
assistant Isabelle2002. It is a tutorial for potential
|
||||||
users rather than a monograph for researchers. The book has
|
users rather than a monograph for researchers. The book has
|
||||||
three parts.
|
three parts.
|
||||||
|
@ -121,7 +121,7 @@
|
||||||
such advanced topics as nested and mutual recursion. 2.
|
such advanced topics as nested and mutual recursion. 2.
|
||||||
Logic and Sets presents a collection of lower-level tactics
|
Logic and Sets presents a collection of lower-level tactics
|
||||||
that you can use to apply rules selectively. It also
|
that you can use to apply rules selectively. It also
|
||||||
describes Isabelle/\acs{hol}'s treatment of sets, functions
|
describes Isabelle/HOL's treatment of sets, functions
|
||||||
and relations and explains how to define sets inductively.
|
and relations and explains how to define sets inductively.
|
||||||
One of the examples concerns the theory of model checking,
|
One of the examples concerns the theory of model checking,
|
||||||
and another is drawn from a classic textbook on formal
|
and another is drawn from a classic textbook on formal
|
||||||
|
|
|
@ -4334,6 +4334,23 @@ isbn="978-3-540-48509-4"
|
||||||
acknowledgement={none}
|
acknowledgement={none}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@incollection{Tuong-IsabelleC:2019,
|
||||||
|
address = {Heidelberg},
|
||||||
|
author = {Fr\'ederic Tuong and Burkhart Wolff},
|
||||||
|
booktitle = {International Workshop on Formal Integrated Development Environments (F-IDE)},
|
||||||
|
doi = {10.4204/EPTCS.310.3},
|
||||||
|
keywords = {Isabelle, HOL, C11, Program Verification, Program Testing},
|
||||||
|
language = {USenglish},
|
||||||
|
location = {Porto, Protogal},
|
||||||
|
number = {314},
|
||||||
|
pdf = {https://www.lri.fr/~wolff/papers/conf/2019-fide-isabelle_c.pdf},
|
||||||
|
publisher = {Open Publishing Association},
|
||||||
|
series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
|
||||||
|
title = {{D}eeply {I}ntegrating {C11} {C}ode {S}upport into {I}sabelle/{PIDE}},
|
||||||
|
year = {2019}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
@InProceedings{ bishop.ea:rigorous:2005,
|
@InProceedings{ bishop.ea:rigorous:2005,
|
||||||
author = {Steve Bishop and Matthew Fairbairn and Michael Norrish and
|
author = {Steve Bishop and Matthew Fairbairn and Michael Norrish and
|
||||||
Peter Sewell and Michael Smith and Keith Wansbrough},
|
Peter Sewell and Michael Smith and Keith Wansbrough},
|
||||||
|
|
|
@ -53,29 +53,50 @@ propagation. This challenge incites numerous research efforts
|
||||||
summarized under the labels ``semantic web'', ``data mining'', or any
|
summarized under the labels ``semantic web'', ``data mining'', or any
|
||||||
form of advanced ``semantic'' text processing. Turning informal into
|
form of advanced ``semantic'' text processing. Turning informal into
|
||||||
(more) formal content is the key for advanced techniques of research,
|
(more) formal content is the key for advanced techniques of research,
|
||||||
combination, and the maintenance of consistency in the midst of data evolution.
|
combination, and the maintenance of consistency in evolving data.
|
||||||
|
|
||||||
Admittedly, Isabelle is not the first system that comes into one's mind when
|
Admittedly, Isabelle is not the first system that comes into one's mind when
|
||||||
writing a document, be it a scientific paper, a book, or a larger technical
|
writing a document, be it a scientific paper, a book, or a larger technical
|
||||||
documentation. However, it has a typesetting system inside which is in the
|
documentation. However, it has a typesetting system inside which is in the
|
||||||
tradition of document generation systems such as mkd, Document! X, Doxygen,
|
tradition of document generation systems such as mkd, Document! X, Doxygen,
|
||||||
Javadoc, etc., which embed elements of formal content such as code-snippets
|
Javadoc, etc., and which embed elements of formal content such as code-snippets
|
||||||
or generated system output into informal text. In Isabelle, these "embedders"
|
or generated system output into informal text. In Isabelle, these "embedders"
|
||||||
or meta-text elements are a form of machine-checked macro called \<^emph>\<open>antiquotations\<close>.
|
or meta-text elements are a form of machine-checked macro called \<^emph>\<open>antiquotations\<close>.
|
||||||
|
|
||||||
For example, the text element as appearing in the Isabelle frontend:
|
For example, the text element as appearing in the Isabelle frontend:
|
||||||
@{theory_text [display]
|
@{theory_text [display,indent=10, margin=70]
|
||||||
\<open> According to the reflexivity axiom @{thm refl}, we obtain in \<Gamma>
|
\<open>
|
||||||
for @{term "fac 5"} the result @{value "fac 5"}.\<close>}
|
text\<open> According to the reflexivity axiom @{thm refl}, we obtain in \<Gamma>
|
||||||
is represented in the generated LaTeX or HTML output by:
|
for @{term "fac 5"} the result @{value "fac 5"}.\<close>
|
||||||
@{theory_text [display]
|
|
||||||
|
\<close>}
|
||||||
|
is represented in the generated \<^latex>\<open>\<close> or HTML output by:
|
||||||
|
@{theory_text [display,indent=10, margin=70]
|
||||||
\<open>According to the reflexivity axiom \<open>x = x\<close>, we obtain in \<Gamma> for \<open>fac 5\<close> the result \<open>120\<close>.\<close>
|
\<open>According to the reflexivity axiom \<open>x = x\<close>, we obtain in \<Gamma> for \<open>fac 5\<close> the result \<open>120\<close>.\<close>
|
||||||
}
|
}
|
||||||
where the meta-texts \<open>@{thm refl}\<close> ("give the presentation of theorem 'refl'),
|
where the meta-texts \<open>@{thm refl}\<close> ("give the presentation of theorem 'refl'),
|
||||||
\<open>@{term "fac 5"}\<close> ("parse and type-check 'fac 5' in the previous logical context)
|
\<open>@{term "fac 5"}\<close> ("parse and type-check 'fac 5' in the previous logical context)
|
||||||
and \<open>@{value "fac 5"}\<close> ("compile and execute 'fac 5' according to its
|
and \<open>@{value "fac 5"}\<close> ("compile and execute 'fac 5' according to its
|
||||||
definitions in the previous logical context) are built-in antiquotations
|
definitions") are built-in antiquotations in \<^hol>.
|
||||||
in \<^hol>.
|
|
||||||
|
%too long !
|
||||||
|
Hence, developers are rewarded for an evolution strategy consisting in
|
||||||
|
source integration in Isabelle and replacing \<^emph>\<open>text\<close> by appropriate \<^emph>\<open>meta-text\<close>:
|
||||||
|
the resulting semantic checks increase the robustness of the document
|
||||||
|
consistency under (usually collaborative) changes.
|
||||||
|
%For example, if someone changes the theorem name, an error would result when processing
|
||||||
|
%the text. On the other hand, \<open>@{value "fac 5"}\<close> would not guard against a change of definition
|
||||||
|
%of \<open>fac\<close>. If this is desirable, an antiquotation like \<open>@{assert "fac 5 = 120"}\<close> would be more appropriate.
|
||||||
|
%too long !
|
||||||
|
Antiquotations do not only occur in text-elements in Isabelle; they are also heavily used
|
||||||
|
in the code-elements of Isabelle's SML implementation, or were specifically supported in
|
||||||
|
C-program contexts in Isabelle/C @{cite "Tuong-IsabelleC:2019"}.
|
||||||
|
|
||||||
|
However, programming antiquotations on the intern Isabelle API's is nothing for the
|
||||||
|
faint-hearted. Recently \<^dof> @{cite "10.1007/978-3-030-30446-1_15" and "10.1007/978-3-319-96812-4_3"}
|
||||||
|
has been designed as an Isabelle component that \<^emph>\<open>generates\<close> antiquotation languages
|
||||||
|
from a more abstract level, namely an \<^emph>\<open>ontology description\<close> that provides typed meta-data
|
||||||
|
and typed reference mechanisms inside text- and ML-contexts.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue