forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'master' into Unreleased/Isabelle2020-RC4
This commit is contained in:
commit
fa25654db9
|
|
@ -205,7 +205,8 @@ states them as three-fold differentiable function in certain bounds concerning s
|
|||
Note that violations, in particular of the constraints on speed and acceleration, \<^emph>\<open>do\<close> occur in practice.
|
||||
In such cases, the global system adapts recovery strategies that are out of the scope of our model.
|
||||
Concepts like \inlineisar+shaft_encoder_state+ (a triple with the sensor values
|
||||
\inlineisar{C1}, \inlineisar{C2}, \inlineisar{C3}) were formalized as types, while tables were defined as recursive functions:
|
||||
\inlineisar{C1}, \inlineisar{C2}, \inlineisar{C3}) were formalized as types, while tables were
|
||||
defined as recursive functions:
|
||||
\enlargethispage{2\baselineskip}\begin{isar}
|
||||
fun phase$_0$ :: "nat \<Rightarrow> shaft_encoder_state" where
|
||||
"phase$_0$ (0) = \<lparr> C1 = False, C2 = False, C3 = True \<rparr>"
|
||||
|
|
@ -561,10 +562,10 @@ to a test-environment or test-engine. \<close>
|
|||
|
||||
text\<open>Finally some examples of references to doc-items, i.e. text-elements with declared
|
||||
meta-information and status. \<close>
|
||||
text \<open> As established by @{docref (unchecked) \<open>t10\<close>},
|
||||
@{docref (define) \<open>t10\<close>} \<close>
|
||||
text \<open> the @{docref \<open>t10\<close>}
|
||||
as well as the @{docref \<open>ass122\<close>}\<close>
|
||||
text \<open> As established by @{docitem (unchecked) \<open>t10\<close>},
|
||||
@{docitem (define) \<open>t10\<close>} \<close>
|
||||
text \<open> the @{docitem \<open>t10\<close>}
|
||||
as well as the @{docitem \<open>ass122\<close>}\<close>
|
||||
text \<open> represent a justification of the safety related applicability
|
||||
condition @{SRAC \<open>ass122\<close>} aka exported constraint @{EC \<open>ass122\<close>}.\<close>
|
||||
|
||||
|
|
|
|||
|
|
@ -111,9 +111,9 @@ text*[plan::introduction]\<open> The plan of the paper is follows: we start by i
|
|||
Isabelel sytem (@{docitem (unchecked) \<open>bgrnd\<close>}) followed by presenting the
|
||||
essentials of \isadof and its ontology language (@{docitem (unchecked) \<open>isadof\<close>}).
|
||||
It follows @{docitem (unchecked) \<open>ontomod\<close>}, where we present three application
|
||||
scenarios from the point of view of the ontology modeling. In @{docitem_ref (unchecked) \<open>ontopide\<close>}
|
||||
scenarios from the point of view of the ontology modeling. In @{docitem (unchecked) \<open>ontopide\<close>}
|
||||
we discuss the user-interaction generated from the ontological definitions. Finally, we draw
|
||||
conclusions and discuss related work in @{docitem_ref (unchecked) \<open>conclusion\<close>}. \<close>
|
||||
conclusions and discuss related work in @{docitem (unchecked) \<open>conclusion\<close>}. \<close>
|
||||
|
||||
section*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"]
|
||||
\<open> Background: The Isabelle System \<close>
|
||||
|
|
@ -146,7 +146,7 @@ figure*[architecture::figure,relative_width="100",src="''figures/isabelle-archit
|
|||
asynchronous communication between the Isabelle system and
|
||||
the IDE (right-hand side). \<close>
|
||||
|
||||
text*[blug::introduction]\<open> The Isabelle system architecture shown in @{docitem_ref \<open>architecture\<close>}
|
||||
text*[blug::introduction]\<open> The Isabelle system architecture shown in @{docitem \<open>architecture\<close>}
|
||||
comes with many layers, with Standard ML (SML) at the bottom layer as implementation
|
||||
language. The architecture actually foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which
|
||||
resides in the SML structure \texttt{Context}. This structure provides a kind of container called
|
||||
|
|
@ -399,7 +399,7 @@ figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figur
|
|||
|
||||
text\<open> The document class \inlineisar+figure+ --- supported by the \isadof text command
|
||||
\inlineisar+figure*+ --- makes it possible to express the pictures and diagrams in this paper
|
||||
such as @{docitem_ref \<open>fig_figures\<close>}.
|
||||
such as @{docitem \<open>fig_figures\<close>}.
|
||||
\<close>
|
||||
|
||||
subsection*[math_exam::example]\<open> The Math-Exam Scenario \<close>
|
||||
|
|
@ -518,7 +518,7 @@ declare_reference*["fig_qcm"::figure]
|
|||
|
||||
text\<open> Using the \LaTeX{} package hyperref, it is possible to conceive an interactive
|
||||
exam-sheets with multiple-choice and/or free-response elements
|
||||
(see @{docitem_ref (unchecked) \<open>fig_qcm\<close>}). With the
|
||||
(see @{docitem (unchecked) \<open>fig_qcm\<close>}). With the
|
||||
help of the latter, it is possible that students write in a browser a formal mathematical
|
||||
derivation---as part of an algebra exercise, for example---which is submitted to the examiners
|
||||
electronically. \<close>
|
||||
|
|
@ -632,7 +632,7 @@ figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-
|
|||
\<open> Exploring an attribute (hyperlinked to the class). \<close>
|
||||
subsection*[cenelec_pide::example]\<open> CENELEC \<close>
|
||||
declare_reference*[figfig3::figure]
|
||||
text\<open> The corresponding view in @{docitem_ref (unchecked) \<open>figfig3\<close>} shows core part of a document,
|
||||
text\<open> The corresponding view in @{docitem (unchecked) \<open>figfig3\<close>} shows core part of a document,
|
||||
coherent to the @{example \<open>cenelec_onto\<close>}. The first sample shows standard Isabelle antiquotations
|
||||
@{cite "wenzel:isabelle-isar:2017"} into formal entities of a theory. This way, the informal parts
|
||||
of a document get ``formal content'' and become more robust under change.\<close>
|
||||
|
|
@ -641,7 +641,7 @@ figure*[figfig3::figure,relative_width="80",src="''figures/antiquotations-PIDE''
|
|||
\<open> Standard antiquotations referring to theory elements.\<close>
|
||||
|
||||
declare_reference*[figfig5::figure]
|
||||
text\<open> The subsequent sample in @{docitem_ref (unchecked) \<open>figfig5\<close>} shows the definition of an
|
||||
text\<open> The subsequent sample in @{docitem (unchecked) \<open>figfig5\<close>} shows the definition of an
|
||||
\<^emph>\<open>safety-related application condition\<close>, a side-condition of a theorem which
|
||||
has the consequence that a certain calculation must be executed sufficiently fast on an embedded
|
||||
device. This condition can not be established inside the formal theory but has to be
|
||||
|
|
@ -652,7 +652,7 @@ figure*[figfig5::figure, relative_width="80", src="''figures/srac-definition''"]
|
|||
figure*[figfig7::figure, relative_width="80", src="''figures/srac-as-es-application''"]
|
||||
\<open> Using a SRAC as EC document reference. \<close>
|
||||
|
||||
text\<open> Now we reference in @{docitem_ref (unchecked) \<open>figfig7\<close>} this safety-related condition;
|
||||
text\<open> Now we reference in @{docitem (unchecked) \<open>figfig7\<close>} this safety-related condition;
|
||||
however, this happens in a context where general \<^emph>\<open>exported constraints\<close> are listed.
|
||||
\isadof's checks establish that this is legal in the given ontology.
|
||||
|
||||
|
|
|
|||
|
|
@ -70,13 +70,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_ref (unchecked) \<open>isadof_tour\<close>} and, depending on their knowledge of Isabelle/HOL, also
|
||||
@{docitem_ref (unchecked) \<open>background\<close>}.
|
||||
@{docitem (unchecked) \<open>isadof_tour\<close>} and, depending on their knowledge of Isabelle/HOL, also
|
||||
@{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_ref (unchecked) \<open>isadof_ontologies\<close>}.
|
||||
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_ref (unchecked) \<open>isadof_developers\<close>}
|
||||
text-elements. These users should read @{docitem (unchecked) \<open>isadof_developers\<close>}
|
||||
\<close>
|
||||
|
||||
subsubsection\<open>Typographical Conventions\<close>
|
||||
|
|
|
|||
|
|
@ -45,7 +45,7 @@ The current system framework offers moreover the following features:
|
|||
the most prominent and deeply integrated system component.
|
||||
|
||||
|
||||
The Isabelle system architecture shown in @{docitem_ref \<open>architecture\<close>} comes with many layers,
|
||||
The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers,
|
||||
with Standard ML (SML) at the bottom layer as implementation language. The architecture actually
|
||||
foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \inlinesml{Context}.
|
||||
This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an
|
||||
|
|
|
|||
|
|
@ -389,7 +389,7 @@ figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figur
|
|||
|
||||
text\<open>
|
||||
The document class \inlineisar+figure+ (supported by the \isadof command \inlineisar+figure*+)
|
||||
makes it possible to express the pictures and diagrams such as @{docitem_ref \<open>fig_figures\<close>}.
|
||||
makes it possible to express the pictures and diagrams such as @{docitem \<open>fig_figures\<close>}.
|
||||
|
||||
Finally, we define a monitor class definition that enforces a textual ordering
|
||||
in the document core by a regular expression:
|
||||
|
|
@ -430,7 +430,7 @@ figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-
|
|||
\<open> Exploring an attribute (hyperlinked to the class). \<close>
|
||||
|
||||
text\<open>
|
||||
An ontological reference application in @{docitem_ref "figDogfoodVIlinkappl"}: the
|
||||
An ontological reference application in @{docitem "figDogfoodVIlinkappl"}: the
|
||||
ontology-dependant antiquotation \inlineisar|@ {example ...}| refers to the corresponding
|
||||
text-elements. Hovering allows for inspection, clicking for jumping to the definition. If the
|
||||
link does not exist or has a non-compatible type, the text is not validated.
|
||||
|
|
@ -550,7 +550,7 @@ result communication times \ldots \<close>
|
|||
subsection*[ontopide::technical]\<open>Editing Support for CENELEC 50128\<close>
|
||||
figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"]
|
||||
\<open> Standard antiquotations referring to theory elements.\<close>
|
||||
text\<open> The corresponding view in @{docitem_ref \<open>figfig3\<close>} shows core part of a document
|
||||
text\<open> The corresponding view in @{docitem \<open>figfig3\<close>} shows core part of a document
|
||||
conformimg to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations
|
||||
@{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts
|
||||
of a document get ``formal content'' and become more robust under change.\<close>
|
||||
|
|
@ -559,11 +559,11 @@ figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"]
|
|||
\<open> Defining a SRAC reference \ldots \<close>
|
||||
figure*[figfig7::figure, relative_width="95", src="''figures/srac-as-es-application''"]
|
||||
\<open> Using a SRAC as EC document reference. \<close>
|
||||
text\<open> The subsequent sample in @{docitem_ref \<open>figfig5\<close>} shows the definition of an
|
||||
text\<open> The subsequent sample in @{docitem \<open>figfig5\<close>} shows the definition of an
|
||||
\<^emph>\<open>safety-related application condition\<close>, a side-condition of a theorem which
|
||||
has the consequence that a certain calculation must be executed sufficiently fast on an embedded
|
||||
device. This condition can not be established inside the formal theory but has to be
|
||||
checked by system integration tests. Now we reference in @{docitem_ref \<open>figfig7\<close>} this
|
||||
checked by system integration tests. Now we reference in @{docitem \<open>figfig7\<close>} this
|
||||
safety-related condition; however, this happens in a context where general \<^emph>\<open>exported constraints\<close>
|
||||
are listed. \isadof's checks establish that this is legal in the given ontology.
|
||||
\<close>
|
||||
|
|
@ -713,7 +713,7 @@ text\<Open> This is *\<Open>emphasized\<Close> a$$nd this is a
|
|||
Clearly, this is not always possible and, in fact, often \isadof documents will contain
|
||||
\LaTeX-commands, this should be restricted to layout improvements that otherwise are (currently)
|
||||
not possible. As far as possible, the use of \LaTeX-commands should be restricted to the definition
|
||||
of ontologies and document templates (see @{docitem_ref (unchecked) \<open>isadof_ontologies\<close>}).
|
||||
of ontologies and document templates (see @{docitem (unchecked) \<open>isadof_ontologies\<close>}).
|
||||
|
||||
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
|
||||
|
|
|
|||
|
|
@ -770,7 +770,7 @@ text\<open>
|
|||
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{src/document-templates} and its file name should start with the prefix \path{root-}. After
|
||||
adding a new template, call the \inlinebash{install} script (see @{docref "infrastructure"}
|
||||
adding a new template, call the \inlinebash{install} script (see @{docitem "infrastructure"}
|
||||
The common structure of an \isadof document template looks as follows:
|
||||
|
||||
\begin{ltx}[escapechar=ë, numbers=left,numberstyle=\tiny,xleftmargin=5mm]
|
||||
|
|
|
|||
|
|
@ -188,7 +188,7 @@ text\<open>
|
|||
section\<open>Programming Class Invariants\<close>
|
||||
text\<open>
|
||||
For the moment, there is no high-level syntax for the definition of class invariants. A
|
||||
formulation, in SML, of the first class-invariant in @{docref "sec:class_inv"} is straight-forward:
|
||||
formulation, in SML, of the first class-invariant in @{docitem "sec:class_inv"} is straight-forward:
|
||||
|
||||
\begin{sml}
|
||||
fun check_result_inv oid {is_monitor:bool} ctxt =
|
||||
|
|
@ -223,7 +223,7 @@ text\<open>
|
|||
\end{sml}
|
||||
where \inlineisar+env+ is basically a map between internal automaton states and class-id's
|
||||
(\inlineisar+cid+'s). An automaton is said to be \<^emph>\<open>enabled\<close> for a class-id,
|
||||
iff it either occurs in its accept-set or its reject-set (see @{docref "sec:monitors"}). During
|
||||
iff it either occurs in its accept-set or its reject-set (see @{docitem "sec:monitors"}). During
|
||||
top-down document validation, whenever a text-element is encountered, it is checked if a monitor
|
||||
is \emph{enabled} for this class; in this case, the \inlineisar+next+-operation is executed. The
|
||||
transformed automaton recognizing the rest-language is stored in \inlineisar+docobj_tab+ if
|
||||
|
|
@ -247,9 +247,9 @@ text\<open>
|
|||
\end{ltx}
|
||||
|
||||
The \LaTeX-generator of \isadof maps each \inlineisar{doc_item} to an \LaTeX-environment (recall
|
||||
@{docref "text-elements"}). As generic \inlineisar{doc_item} are derived from the text element,
|
||||
@{docitem "text-elements"}). As generic \inlineisar{doc_item} are derived from the text element,
|
||||
the enviornment \inlineltx|{isamarkuptext*}| builds the core of \isadof's \LaTeX{} implementation.
|
||||
For example, the @{docref "ass123"} from page \pageref{ass123} is mapped to
|
||||
For example, the @{docitem "ass123"} from page \pageref{ass123} is mapped to
|
||||
|
||||
\begin{ltx}
|
||||
\begin{isamarkuptext*}%
|
||||
|
|
@ -262,7 +262,7 @@ text\<open>
|
|||
\end{isamarkuptext*}
|
||||
\end{ltx}
|
||||
|
||||
This environment is mapped to a plain \LaTeX command via (again, recall @{docref "text-elements"}):
|
||||
This environment is mapped to a plain \LaTeX command via (again, recall @{docitem "text-elements"}):
|
||||
\begin{ltx}
|
||||
\NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}}
|
||||
\end{ltx}
|
||||
|
|
|
|||
|
|
@ -90,7 +90,7 @@ doc_class text_element =
|
|||
variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}"
|
||||
|
||||
section\<open>Some attempt to model standardized links to Standard Isabelle Formal Content\<close>
|
||||
|
||||
(* Deprecated *)
|
||||
doc_class assertions =
|
||||
properties :: "term list"
|
||||
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
|||
RegExpInterface (* Interface to functional regular automata for monitoring *)
|
||||
Assert
|
||||
|
||||
keywords "+=" ":=" "accepts" "rejects" "invs"
|
||||
keywords "+=" ":=" "accepts" "rejects" "invariant"
|
||||
|
||||
and "title*" "subtitle*"
|
||||
"chapter*" "section*" "subsection*" "subsubsection*"
|
||||
|
|
@ -1597,21 +1597,25 @@ val docitem_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc
|
|||
|
||||
|
||||
val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input))
|
||||
: ({define: bool, unchecked: bool} * Input.source) context_parser;
|
||||
: ({define:bool,unchecked:bool} * Input.source) context_parser;
|
||||
|
||||
|
||||
|
||||
fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked = x, define = y}, src ) =
|
||||
let (* val _ = writeln ("ZZZ" ^ Input.source_content src ^ "::2::" ^ cid_decl) *)
|
||||
val (str,pos) = Input.source_content src
|
||||
val _ = check_and_mark ctxt cid_decl
|
||||
({strict_checking = not x}) pos str
|
||||
in
|
||||
(if y then Latex.enclose_block ("\\csname isaDof.label\\endcsname[type={"^cid_decl^"}]{") "}"
|
||||
else Latex.enclose_block ("\\csname isaDof.ref\\endcsname[type={"^cid_decl^"}]{") "}")
|
||||
[Latex.text (Input.source_content src)]
|
||||
end
|
||||
|
||||
fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked, define}, src ) =
|
||||
let (* val _ = writeln ("ZZZ" ^ Input.source_content src ^ "::2::" ^ cid_decl) *)
|
||||
val (str,pos) = Input.source_content src
|
||||
val _ = check_and_mark ctxt cid_decl ({strict_checking = not unchecked}) pos str
|
||||
val inline = Config.get ctxt Document_Antiquotation.thy_output_display
|
||||
val _ = if inline then writeln("HEUREKA") else ()
|
||||
val enc = Latex.enclose_block
|
||||
in
|
||||
(case (define,inline) of
|
||||
(true,false) => enc("\\csname isaDof.label\\endcsname[type={"^cid_decl^"}] {")"}"
|
||||
|(false,false)=> enc("\\csname isaDof.ref\\endcsname[type={"^cid_decl^"}] {")"}"
|
||||
|(true,true) => enc("\\csname isaDof.macroDef\\endcsname[type={"^cid_decl^"}]{")"}"
|
||||
|(false,true) => enc("\\csname isaDof.macroExp\\endcsname[type={"^cid_decl^"}]{")"}"
|
||||
)
|
||||
[Latex.text (Input.source_content src)]
|
||||
end
|
||||
|
||||
|
||||
fun docitem_antiquotation bind cid =
|
||||
|
|
@ -1635,33 +1639,21 @@ fun check_and_mark_term ctxt oid =
|
|||
|
||||
|
||||
fun ML_antiquotation_docitem_value (ctxt, toks) =
|
||||
(Scan.lift (Args.cartouche_input)
|
||||
>> (fn inp => (ML_Syntax.atomic o ML_Syntax.print_term)
|
||||
((check_and_mark_term ctxt o fst o Input.source_content) inp)))
|
||||
(ctxt, toks)
|
||||
(Scan.lift (Args.cartouche_input)
|
||||
>> (fn inp => (ML_Syntax.atomic o ML_Syntax.print_term)
|
||||
((check_and_mark_term ctxt o fst o Input.source_content) inp)))
|
||||
(ctxt, toks)
|
||||
|
||||
(* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*)
|
||||
(* Setup for general docitems of the global DOF_core.default_cid - class ("text")*)
|
||||
val _ = Theory.setup
|
||||
(docitem_antiquotation \<^binding>\<open>docref\<close> DOF_core.default_cid #>
|
||||
(* deprecated syntax ^^^^^^*)
|
||||
docitem_antiquotation \<^binding>\<open>docitem_ref\<close> DOF_core.default_cid #>
|
||||
(* deprecated syntax ^^^^^^^^^^^*)
|
||||
docitem_antiquotation \<^binding>\<open>docitem\<close> DOF_core.default_cid #>
|
||||
(docitem_antiquotation \<^binding>\<open>docitem\<close> DOF_core.default_cid #>
|
||||
|
||||
ML_Antiquotation.inline \<^binding>\<open>docitem_value\<close> ML_antiquotation_docitem_value)
|
||||
|
||||
end (* struct *)
|
||||
\<close>
|
||||
|
||||
|
||||
ML\<open>
|
||||
Goal.prove_global;
|
||||
Specification.theorems_cmd;
|
||||
Goal.prove_common;
|
||||
\<close>
|
||||
|
||||
ML\<open>open Proof
|
||||
\<close>
|
||||
text\<open> @{thm [] refl}\<close>
|
||||
|
||||
ML\<open>
|
||||
structure AttributeAccess =
|
||||
|
|
@ -1857,21 +1849,23 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
|
|||
|
||||
end;
|
||||
|
||||
val parse_invariants = Parse.and_list (Args.name_position --| Parse.$$$ "::" -- Parse.term)
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>doc_class\<close> "define document class"
|
||||
((Parse_Spec.overloaded
|
||||
-- (Parse.type_args_constrained -- Parse.binding)
|
||||
-- (\<^keyword>\<open>=\<close>
|
||||
|-- Scan.option (Parse.typ --| \<^keyword>\<open>+\<close>)
|
||||
|-- Scan.option (Parse.typ --| \<^keyword>\<open>+\<close>)
|
||||
-- Scan.repeat1 (Parse.const_binding -- Scan.option (\<^keyword>\<open><=\<close> |-- Parse.term))
|
||||
)
|
||||
-- ( Scan.optional (\<^keyword>\<open>rejects\<close> |-- Parse.enum1 "," Parse.term) []
|
||||
-- Scan.repeat (\<^keyword>\<open>accepts\<close> |-- Parse.term)
|
||||
-- Scan.repeats ((\<^keyword>\<open>invs\<close>) |--
|
||||
Parse.and_list (Args.name_position --| Parse.$$$ "::" -- Parse.term)))
|
||||
-- ( Scan.optional (\<^keyword>\<open>rejects\<close> |-- Parse.enum1 "," Parse.term) []
|
||||
-- Scan.repeat (\<^keyword>\<open>accepts\<close> |-- Parse.term)
|
||||
-- Scan.repeats ((\<^keyword>\<open>invariant\<close>) |-- parse_invariants))
|
||||
)
|
||||
>> (fn (((overloaded, x), (y, z)),((rejectS,accept_rex),invs)) =>
|
||||
Toplevel.theory (add_doc_class_cmd {overloaded = overloaded} x y z rejectS accept_rex invs)));
|
||||
>> (fn (((overloaded, hdr), (parent, attrs)),((rejects,accept_rex),invars)) =>
|
||||
Toplevel.theory (add_doc_class_cmd {overloaded = overloaded} hdr parent
|
||||
attrs rejects accept_rex invars)));
|
||||
|
||||
end (* struct *)
|
||||
\<close>
|
||||
|
|
@ -1900,22 +1894,5 @@ ML\<open>
|
|||
|
||||
\<close>
|
||||
*)
|
||||
ML\<open>open Thread\<close>
|
||||
|
||||
(* concurrency experiments:
|
||||
ML\<open>open Thread\<close>
|
||||
ML\<open>open Future\<close>
|
||||
ML\<open>open OS.Process\<close>
|
||||
ML\<open>ALLGOALS\<close>
|
||||
|
||||
ML\<open>open Goal\<close>
|
||||
ML \<open>future_result;\<close>
|
||||
*)
|
||||
|
||||
ML\<open> String.isSuffix "_asd" "sdfgsd_asd";
|
||||
|
||||
String.substring ("sdfgsd_asd", 0, size "sdfgsd_asd" - 4)\<close>
|
||||
ML\<open>Long_Name.qualifier "dgfdfg.dfgdfg.qwe"\<close>
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -93,7 +93,6 @@ definition YY where "YY = na2da(rexp2na example_expression)"
|
|||
value "NA.accepts (rexp2na example_expression) [0,1,1,0,0,1]"
|
||||
value "DA.accepts (na2da (rexp2na example_expression)) [0,1,1,0,0,1]"
|
||||
|
||||
|
||||
section\<open>HOL - Adaptions and Export to SML\<close>
|
||||
|
||||
definition enabled :: "('a,'\<sigma> set)da \<Rightarrow> '\<sigma> set \<Rightarrow> 'a list \<Rightarrow> 'a list"
|
||||
|
|
|
|||
|
|
@ -154,5 +154,7 @@
|
|||
% begin: label and ref
|
||||
\newisadof{label}[label=,type=][1]{\label{#1}}
|
||||
\newisadof{ref}[label=,type=][1]{\autoref{#1}}
|
||||
\newisadof{macroDef}[label=,type=][1]{MMM \label{#1}} %% place_holder
|
||||
\newisadof{macroExp}[label=,type=][1]{MMM \autoref{#1}} %% place_holder
|
||||
% end: label and ref
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
|
|
|||
|
|
@ -50,15 +50,15 @@ doc_class E = D +
|
|||
|
||||
|
||||
doc_class F =
|
||||
properties :: "term list"
|
||||
r :: "thm list"
|
||||
u :: "file"
|
||||
s :: "typ list"
|
||||
b :: "(A \<times> C) set" <= "{}" (* This is a relation link, roughly corresponding
|
||||
properties :: "term list"
|
||||
r :: "thm list"
|
||||
u :: "file"
|
||||
s :: "typ list"
|
||||
b :: "(A \<times> C) set" <= "{}" (* This is a relation link, roughly corresponding
|
||||
to an association class. It can be used to track
|
||||
claims to result - relations, for example.*)
|
||||
invs bxxx :: "\<lambda>\<sigma>. r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
|
||||
and xxx :: "\<lambda>\<sigma>. properties \<sigma> \<noteq> []"
|
||||
invariant b :: "\<lambda>\<sigma>. r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
|
||||
and c :: "\<lambda>\<sigma>. properties \<sigma> \<noteq> []"
|
||||
|
||||
|
||||
doc_class G = C +
|
||||
|
|
|
|||
|
|
@ -154,8 +154,114 @@
|
|||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
\newtheorem{axiom}{Axiom}
|
||||
\newtheorem{ruleX}{Rule} % apparent name-clash with s th from libraries...
|
||||
\newtheorem{assertion}{Assertion}
|
||||
|
||||
% end: scholarly_paper.abstract
|
||||
% "def" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn"
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\newisadof{text.scholarly_paper.math_content}%
|
||||
[label=,type=%
|
||||
, scholarly_paper.math_content.short_name ={\relax}% {} or \relax
|
||||
, scholarly_paper.math_content.mcc =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, Isa_COL.text_element.referentiable =%
|
||||
, Isa_COL.text_element.variants =%
|
||||
, scholarly_paper.text_section.main_author =%
|
||||
, scholarly_paper.text_section.fixme_list =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, scholarly_paper.technical.definition_list =%
|
||||
, scholarly_paper.technical.status =%
|
||||
]
|
||||
[1]
|
||||
{%
|
||||
\begin{isamarkuptext}%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{def}}
|
||||
{%
|
||||
\begin{definition}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{definition}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{axm}}
|
||||
{%
|
||||
\begin{axiom}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{axiom}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{thm}}
|
||||
{%
|
||||
\begin{theorem}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{theorem}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{lem}}
|
||||
{%
|
||||
\begin{lemma}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{lemma}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{prop}}
|
||||
{%
|
||||
\begin{property}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{property}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rule}}
|
||||
{%
|
||||
\begin{ruleX}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{ruleX}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{assn}}
|
||||
{%
|
||||
\begin{assertion}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{assertion}%
|
||||
}%
|
||||
{%
|
||||
ERROR CASE #1% BETTER: Since enumeration, there should be here the best possible error-msg here
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
|
||||
|
||||
% end: scholarly_paper.math_content
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\newisadof{text.scholarly_paper.math_example}%
|
||||
[label=,type=%
|
||||
, scholarly_paper.math_example.short_name =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, Isa_COL.text_element.referentiable =%
|
||||
, Isa_COL.text_element.variants =%
|
||||
, scholarly_paper.text_section.main_author =%
|
||||
, scholarly_paper.text_section.fixme_list =%
|
||||
, scholarly_paper.technical.definition_list =%
|
||||
, scholarly_paper.technical.status =%
|
||||
]
|
||||
[1]
|
||||
{%
|
||||
\begin{isamarkuptext}%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.technical.status}}{semiformal}}{
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_example.short_name}} {} }
|
||||
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
|
||||
{\begin{example} [\commandkey{scholarly_paper.math_example.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{example}}
|
||||
}{%
|
||||
#1%
|
||||
}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\newisadof{text.scholarly_paper.definition}%
|
||||
[label=,type=%
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ doc_class title =
|
|||
short_title :: "string option" <= "None"
|
||||
|
||||
doc_class subtitle =
|
||||
abbrev :: "string option" <= "None"
|
||||
abbrev :: "string option" <= "None"
|
||||
|
||||
(* adding a contribution list and checking that it is cited as well in tech as in conclusion. ? *)
|
||||
|
||||
|
|
@ -96,7 +96,6 @@ As Security of the system we define etc...
|
|||
A formal statement can, but must not have a reference to true formal Isabelle/Isar definition.
|
||||
\<close>
|
||||
|
||||
|
||||
subsection\<open>Technical Content and its Formats\<close>
|
||||
|
||||
datatype status = semiformal | description
|
||||
|
|
@ -114,34 +113,64 @@ doc_class technical = text_section +
|
|||
status :: status <= "description"
|
||||
formal_results :: "thm list"
|
||||
|
||||
type_synonym tc = technical
|
||||
type_synonym tc = technical (* technical content *)
|
||||
|
||||
|
||||
subsection\<open>Mathematical Statements\<close>
|
||||
|
||||
datatype math_statement_class =
|
||||
"definition" | "axiom" | "theorem" | "lemma" | "proposition" | "rule" | "assertion"
|
||||
subsection\<open>Mathematical Content\<close>
|
||||
|
||||
doc_class math_statement = tc +
|
||||
short_name :: string <= "''''"
|
||||
"class" :: "math_statement_class"
|
||||
status :: status
|
||||
datatype math_content_class = "def" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn"
|
||||
|
||||
doc_class math_description = math_statement +
|
||||
referentiable :: bool <= "False"
|
||||
text\<open>Instances of the \<open>doc_class\<close> \<^verbatim>\<open>math_content\<close> are by definition @{term "semiformal"}; they may
|
||||
be non-referential, but in this case they will not have a @{term "short_name"}.\<close>
|
||||
|
||||
doc_class math_semi_formal_stmt = math_statement +
|
||||
referentiable :: bool <= "True"
|
||||
doc_class math_content = tc +
|
||||
referentiable :: bool <= True
|
||||
short_name :: string <= "''''"
|
||||
status :: status <= "semiformal"
|
||||
mcc :: "math_content_class" <= "thm"
|
||||
invariant s1 :: "\<lambda> \<sigma>. \<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
|
||||
invariant s2 :: "\<lambda> \<sigma>. status \<sigma> = semiformal"
|
||||
type_synonym math_tc = math_content
|
||||
|
||||
|
||||
text\<open>The intended use for the \<open>doc_class\<close>es \<^verbatim>\<open>math_motivation\<close> (or \<^verbatim>\<open>math_mtv\<close> for short),
|
||||
\<^verbatim>\<open>math_explanation\<close> (or \<^verbatim>\<open>math_exp\<close> for short) and
|
||||
\<^verbatim>\<open>math_example\<close> (or \<^verbatim>\<open>math_ex\<close> for short)
|
||||
are \<^emph>\<open>informal\<close> descriptions of semi-formal definitions (by inheritance).
|
||||
Math-Examples can be made referentiable triggering explicit, numbered presentations.\<close>
|
||||
doc_class math_motivation = tc +
|
||||
referentiable :: bool <= False
|
||||
type_synonym math_mtv = math_motivation
|
||||
|
||||
doc_class math_explanation = tc +
|
||||
referentiable :: bool <= False
|
||||
type_synonym math_exp = math_explanation
|
||||
|
||||
doc_class math_example = tc +
|
||||
referentiable :: bool <= False
|
||||
short_name :: string <= "''''"
|
||||
invariant s1 :: "\<lambda> \<sigma>. \<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
|
||||
type_synonym math_ex = math_example
|
||||
|
||||
|
||||
text\<open>The intended use for the \<open>doc_class\<close> \<^verbatim>\<open>math_semiformal_statement\<close> (or \<^verbatim>\<open>math_sfs\<close> for short)
|
||||
are semi-formal mathematical content (definition, lemma, etc.). They are referentiable entities.
|
||||
They are NOT formal, i.e. Isabelle-checked formal content, but can be in close link to these.\<close>
|
||||
doc_class math_semiformal = math_content +
|
||||
referentiable :: bool <= True
|
||||
type_synonym math_sfc = math_semiformal
|
||||
|
||||
subsection\<open>old style onto model.\<close>
|
||||
|
||||
text\<open>A rough structuring is modeled as follows:\<close>
|
||||
(* non-evident-statement *)
|
||||
doc_class "definition" = tc +
|
||||
referentiable :: bool <= "True"
|
||||
referentiable :: bool <= True
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
doc_class "theorem" = tc +
|
||||
referentiable :: bool <= "True"
|
||||
referentiable :: bool <= True
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
text\<open>Note that the following two text-elements are currently set to no-keyword in LNCS style.\<close>
|
||||
|
|
@ -159,7 +188,7 @@ text\<open> \<^verbatim>\<open>examples\<close> are currently considered \<^verb
|
|||
via inheritance. \<close>
|
||||
|
||||
doc_class example = technical +
|
||||
referentiable :: bool <= "True"
|
||||
referentiable :: bool <= True
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
subsection\<open>Code Statement Elements\<close>
|
||||
|
|
@ -189,25 +218,28 @@ doc_class "ISAR" = code +
|
|||
doc_class "LATEX" = code +
|
||||
checked :: bool <= "False"
|
||||
|
||||
|
||||
|
||||
subsection\<open>Content in Engineering/Tech Papers \<close>
|
||||
|
||||
|
||||
doc_class eng_statement = tc +
|
||||
doc_class engineering_statement = tc +
|
||||
short_name :: string <= "''''"
|
||||
"class" :: "math_statement_class"
|
||||
status :: status
|
||||
type_synonym eng_stmt = engineering_statement
|
||||
|
||||
|
||||
doc_class "experiment" = eng_statement +
|
||||
doc_class "experiment" = eng_stmt +
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
doc_class "evaluation" = eng_statement +
|
||||
doc_class "evaluation" = eng_stmt +
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
doc_class "data" = eng_statement +
|
||||
doc_class "data" = eng_stmt +
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
|
||||
subsection\<open>Structuring Enforcement in Engineering/Math Papers \<close>
|
||||
(* todo : could be finer *)
|
||||
|
||||
text\<open> Besides subtyping, there is another relation between
|
||||
doc\_classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
|
||||
|
|
|
|||
|
|
@ -65,7 +65,7 @@ text*[dfgdfg2::C, z = "None"]\<open> Lorem ipsum ... @{thm refl} \<close>
|
|||
|
||||
text*[omega::E, x = "''def''"]\<open> Lorem ipsum ... @{thm refl} \<close>
|
||||
|
||||
text\<open> As mentioned in @{docitem_ref \<open>dfgdfg\<close>} \<close>
|
||||
text\<open> As mentioned in @{docitem \<open>dfgdfg\<close>} \<close>
|
||||
|
||||
text\<open>Here is a simulation what happens on the level of the (HOL)-term representation:\<close>
|
||||
term "A.x (undefined\<lparr>A.x := 3\<rparr>)"
|
||||
|
|
|
|||
Reference in New Issue