Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
This commit is contained in:
commit
d0306e62bc
|
@ -1,6 +1,7 @@
|
||||||
(*<*)
|
(*<*)
|
||||||
theory "04_RefMan"
|
theory "04_RefMan"
|
||||||
imports "03_GuidedTour" (* apparently inaccessible; for railroads "Isar_Ref.Base" *)
|
imports "03_GuidedTour" (* apparently inaccessible; for railroads "Isar_Ref.Base" *)
|
||||||
|
"Isabelle_DOF.Isa_COL"
|
||||||
|
|
||||||
begin
|
begin
|
||||||
(*>*)
|
(*>*)
|
||||||
|
@ -385,13 +386,6 @@ In a high-level syntax, this type of constraints could be expressed, \eg, by:
|
||||||
\<rightarrow> \<exists> y \<in> Range(x@establish). (y,z) \<in> x@establish
|
\<rightarrow> \<exists> y \<in> Range(x@establish). (y,z) \<in> x@establish
|
||||||
(* 3 *) \<forall> x \<in> introduction. finite(x@authored_by)
|
(* 3 *) \<forall> x \<in> introduction. finite(x@authored_by)
|
||||||
\end{isar}
|
\end{isar}
|
||||||
%% @{cartouche [display=true] \<open>
|
|
||||||
%%(* 1 *) \<forall> x \<in> result. x@kind = proof \<leftrightarrow> x@kind \<noteq> []
|
|
||||||
%%(* 2 *) \<forall> x \<in> conclusion. \<forall> y \<in> Domain(x@establish)
|
|
||||||
%% \<rightarrow> \<exists> y\<in> Range(x@establish). (y,z) \<in> x@establish
|
|
||||||
%%(* 3 *) \<forall> x \<in> introduction. finite(x@authored_by)
|
|
||||||
%%\<close>}
|
|
||||||
%% \fixme{experiment... }
|
|
||||||
where \inlineisar+result+, \inlineisar+conclusion+, and
|
where \inlineisar+result+, \inlineisar+conclusion+, and
|
||||||
%% where \<open>result\<close>, \<open>conclusion\<close>, and
|
%% where \<open>result\<close>, \<open>conclusion\<close>, and
|
||||||
\inlineisar+introduction+ are the set of all possible instances of
|
\inlineisar+introduction+ are the set of all possible instances of
|
||||||
|
@ -619,6 +613,55 @@ text\<open>The syntax of toplevel \isadof commands reads as follows:
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
subsection*["commonlib"::technical]\<open>Common Ontology Library (COL)\<close>
|
subsection*["commonlib"::technical]\<open>Common Ontology Library (COL)\<close>
|
||||||
|
text\<open> The COL library is used to capture a couple of text-elements
|
||||||
|
that are expected to be common to all document types, a class
|
||||||
|
that is actually not easy to define. After a lot of thought, we excluded
|
||||||
|
things like @{command "title*"} and abstract-related classes back again
|
||||||
|
to specific ontologies, for example.
|
||||||
|
|
||||||
|
Finally, it is currently reduced to
|
||||||
|
\<^enum> the common infra-structure on text-elements (section is a text-element of a certain "level"),
|
||||||
|
\<^enum> common infrastructure to semi-formal Isabelle elements (Definitions, Assertions, Proofs), and
|
||||||
|
\<^enum> the common infra-structure for figures.
|
||||||
|
|
||||||
|
Future extensions might include, for example, the infra-structure for tables.
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
text\<open> The super-class \<^verbatim>\<open>text_element\<close> is the root of all text-elements used in \isadof.
|
||||||
|
It is defined as follows:
|
||||||
|
\begin{isar}
|
||||||
|
doc_class text_element =
|
||||||
|
level :: "int option" <= "None"
|
||||||
|
referentiable :: bool <= "False"
|
||||||
|
variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}"
|
||||||
|
\end{isar}
|
||||||
|
Of major importance is the @{term "level"} which influences, inspired by a LaTeX convention,
|
||||||
|
the following classification:
|
||||||
|
\<^enum> part = Some -1
|
||||||
|
\<^enum> chapter = Some 0
|
||||||
|
\<^enum> section = Some 1
|
||||||
|
\<^enum> subsection = Some 2
|
||||||
|
\<^enum> subsubsection = Some 3
|
||||||
|
\<^enum> ...
|
||||||
|
for scholarly paper: invariant level >
|
||||||
|
|
||||||
|
The attribute @{term "level"} in the subsequent enables doc-notation --- a kind of macro ---
|
||||||
|
for support of @{command "chapter*"}, @{command "section*"} etc. This class definition forms
|
||||||
|
for a number of invariants; for example, the derived ontology \<open>scholarly_paper\<close> contains an
|
||||||
|
invariant that any sequence of, for example, \<open>technical\<close> - elements must be introduced
|
||||||
|
by a text-element with a higher level, \ie{}, must contain a section or subsection header.
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
doc_class F =
|
||||||
|
property :: "term list"
|
||||||
|
r :: "thm list"
|
||||||
|
u :: "file"
|
||||||
|
s :: "typ list"
|
||||||
|
|
||||||
|
(* BUG BUG BUG
|
||||||
|
assert*[aaa::"04_RefMan.F"] "3 < (4::int)"
|
||||||
|
assert*[aaa::F] "0 < (4::int)"
|
||||||
|
*)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -715,8 +715,8 @@ ML\<open>
|
||||||
|
|
||||||
subsection*[t235::technical]\<open> Theories \<close>
|
subsection*[t235::technical]\<open> Theories \<close>
|
||||||
|
|
||||||
text \<open> This structure yields the datatype \verb*thy* which becomes the content of
|
text \<open> This structure yields the datatype \<^verbatim>\<open>thy\<close> which becomes the content of
|
||||||
\verb*Context.theory*. In a way, the LCF-Kernel registers itself into the Nano-Kernel,
|
@{ML_type "Context.theory"}. In a way, the LCF-Kernel registers itself into the Nano-Kernel,
|
||||||
which inspired me (bu) to this naming. \<close>
|
which inspired me (bu) to this naming. \<close>
|
||||||
|
|
||||||
ML\<open>
|
ML\<open>
|
||||||
|
@ -2099,6 +2099,9 @@ text\<open> This interactive Isabelle Programming Cook-Book represents my curren
|
||||||
\<close>
|
\<close>
|
||||||
(*<*)
|
(*<*)
|
||||||
|
|
||||||
|
paragraph\<open>Many thanks to Frederic Tuong, who contributed some example such as the string cartouche
|
||||||
|
for Unicode Character Denotations as well as many local hints for improvements.\<close>
|
||||||
|
|
||||||
section*[bib::bibliography]\<open>Bibliography\<close>
|
section*[bib::bibliography]\<open>Bibliography\<close>
|
||||||
|
|
||||||
close_monitor*[this]
|
close_monitor*[this]
|
||||||
|
|
|
@ -16,7 +16,11 @@ section\<open> Library of Standard Text Ontology \<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
datatype placement = pl_h | pl_t | pl_b | pl_ht | pl_hb
|
datatype placement = pl_h | (*here*)
|
||||||
|
pl_t | (*top*)
|
||||||
|
pl_b | (*bottom*)
|
||||||
|
pl_ht | (*here -> top*)
|
||||||
|
pl_hb (*here -> bottom*)
|
||||||
|
|
||||||
|
|
||||||
doc_class figure =
|
doc_class figure =
|
||||||
|
@ -68,13 +72,17 @@ section\<open>Some attempt to model standardized links to Standard Isabelle Form
|
||||||
|
|
||||||
doc_class assertions =
|
doc_class assertions =
|
||||||
properties :: "term list"
|
properties :: "term list"
|
||||||
|
|
||||||
doc_class "thms" =
|
doc_class "thms" =
|
||||||
properties :: "thm list"
|
properties :: "thm list"
|
||||||
|
|
||||||
doc_class formal_item =
|
doc_class formal_item =
|
||||||
item :: "(assertions + thms)"
|
item :: "(assertions + thms)"
|
||||||
|
|
||||||
|
doc_class definitions =
|
||||||
|
requires :: "formal_item list"
|
||||||
|
establishes :: "thms list"
|
||||||
|
|
||||||
doc_class formal_content =
|
doc_class formal_content =
|
||||||
style :: "string option"
|
style :: "string option"
|
||||||
accepts "\<lbrace>formal_item\<rbrace>\<^sup>+"
|
accepts "\<lbrace>formal_item\<rbrace>\<^sup>+"
|
||||||
|
|
Loading…
Reference in New Issue