Added discussed ontology "math_paper" and an example reffering to (some elements) of it.
This commit is contained in:
parent
6fec11c152
commit
a1d6431df9
|
|
@ -0,0 +1,38 @@
|
|||
theory AssnsLemmaThmEtc
|
||||
imports "../../ontologies/Conceptual" "../../ontologies/math_paper"
|
||||
begin
|
||||
|
||||
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
|
||||
|
||||
text\<open>Current status:\<close>
|
||||
print_doc_classes
|
||||
print_doc_items
|
||||
|
||||
|
||||
|
||||
section\<open>Definitions, Lemmas, Theorems, Assertions\<close>
|
||||
(* auxilliary *)
|
||||
ML\<open>fun assert_list_dest X = map HOLogic.dest_string
|
||||
(map (fn Const ("Isa_DOF.ISA_term", _) $ s => s )
|
||||
(HOLogic.dest_list X))\<close>
|
||||
|
||||
|
||||
text*[aa::F]\<open>Our definition of the HOL-Logic has the following properties:\<close>
|
||||
assert*[aa::F] "True"
|
||||
|
||||
ML\<open>assert_list_dest @{docitem_attribute property :: aa}\<close>
|
||||
assert*[aa::F] "True & True" (* small pb: unicodes crashes here ... *)
|
||||
ML\<open> assert_list_dest @{docitem_attribute property :: aa}\<close>
|
||||
|
||||
text\<open>An example for the ontology specification character of the short-cuts such as
|
||||
@{command "assert*"}: in the following, we use the same notation referring to a completely
|
||||
different class. "F" and "assertion" have only in common that they posses the attribute
|
||||
\<^verbatim>\<open>property\<close>: \<close>
|
||||
|
||||
text*[aaa::assertion]\<open>Our definition of the integers has the following properties:\<close>
|
||||
assert*[aaa::assertion] "3 < (4::int)"
|
||||
assert*[aaa::assertion] "0 < (4::int)"
|
||||
|
||||
|
||||
end
|
||||
(*>*)
|
||||
|
|
@ -126,13 +126,10 @@ ML \<open>@{trace_attribute figs1}\<close>
|
|||
text\<open>Resulting trace of figs as text antiquotation:\<close>
|
||||
text\<open>@{trace_attribute figs1}\<close>
|
||||
|
||||
(*<*)
|
||||
text\<open>Final Status:\<close>
|
||||
print_doc_items
|
||||
print_doc_classes
|
||||
|
||||
(*quatsch so far *)
|
||||
text*[aa::figure]\<open>dfg\<close>
|
||||
assert*[aa] "True"
|
||||
|
||||
|
||||
end
|
||||
end
|
||||
(*>*)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,100 @@
|
|||
chapter \<open>The Document Ontology Common Library for the Isabelle Ontology Framework\<close>
|
||||
|
||||
text\<open> Offering support for common Isabelle Elements like definitions, lemma- and theorem
|
||||
statements, proofs, etc. Isabelle is a lot of things, but it is an interactive theorem
|
||||
proving environment after all !
|
||||
\<^item>
|
||||
\<^item>
|
||||
\<^item> LaTeX support. \<close>
|
||||
|
||||
|
||||
theory math_paper
|
||||
imports "../Isa_DOF"
|
||||
begin
|
||||
|
||||
|
||||
section\<open>Some attempt to model standardized links to Standard Isabelle Formal Content\<close>
|
||||
|
||||
text\<open> These document classes are intended to present a number of key-elements
|
||||
in mathematical papers and generate LaTeX in the style of, for example:
|
||||
\begin{verbatim}
|
||||
\begin{definition}[Dilating function]
|
||||
A dilating function for a run \(\rho'\) is a function \(\mathbb{N} \longrightarrow \mathbb{N}\)
|
||||
that satisfies:
|
||||
\begin{enumerate}
|
||||
\item \(f\) is strictly monotonic, so that the order of the instants in not changed in \(\rho'\);
|
||||
\item \(\forall n.~f(n) \geq n\), so that instants are inserted into \(\rho\);
|
||||
\item \(f(0) = 0\), so that no instant is inserted before the first one;
|
||||
\item \(\forall n.~(\not\exists n_0.~f(n_0) = n) \Longrightarrow
|
||||
(\forall c.~\neg\mathsf{ticks}(\rho'_{n}(c))\),
|
||||
there is no tick in stuttering instants;
|
||||
\item \(\forall n.~(\not\exists n_0.~f(n_0) = n+1) \Longrightarrow
|
||||
(\forall c.~\mathsf{time}(\rho'_{n+1}(c)) = \mathsf{time}(\rho'_{n}(c)))\),
|
||||
time does not elapse during stuttering instants;
|
||||
\end{enumerate}
|
||||
\end{definition}
|
||||
\end{verbatim}
|
||||
which are intended to \<^emph>\<open>complement\<close> Isabelle's formal content elements such as definitions,
|
||||
lemmas and formal proofs.
|
||||
|
||||
We are aware that there is a certain tension between the interest to have more formal checking in
|
||||
a definition as the above one and the interest in a notationally more liberal presentation that hides
|
||||
technical details imposed by strict formality (even at the price that a chosen notation may be
|
||||
intuitive, but an abstraction that is, fi donc, technically incorrect).
|
||||
|
||||
We argue that it should be up to the user to decide in each individual case how to draw this line ... \<close>
|
||||
|
||||
doc_class formal_stmt =
|
||||
property :: "term list"
|
||||
|
||||
datatype relevance = key | vital | working | auxilliary | alternative
|
||||
|
||||
doc_class "definition" = formal_stmt +
|
||||
relevance :: "relevance option"
|
||||
property :: "term list" <= "[]"
|
||||
|
||||
text\<open>Which gives rise to a presentation like:\<close>
|
||||
(*<*)
|
||||
type_notation nat ("\<nat>")
|
||||
(*>*)
|
||||
text*[dil_fun :: "definition"]\<open>A dilating function for a run @{term "\<rho>"} is a function
|
||||
@{typ "\<nat> \<Rightarrow> \<nat>"} that satisfies:
|
||||
\<^enum> @{term "f"} is strictly monotonic ...
|
||||
\<^enum> ...
|
||||
\<^enum> ...
|
||||
\<close>
|
||||
|
||||
|
||||
doc_class assertion = formal_stmt +
|
||||
relevance :: "relevance option"
|
||||
property :: "term list" <= "[]"
|
||||
|
||||
doc_class "lemma" = formal_stmt +
|
||||
relevance :: "relevance"
|
||||
property :: "term list" <= "[]"
|
||||
|
||||
doc_class "theorem" = formal_stmt +
|
||||
relevance :: "relevance"
|
||||
property :: "term list" <= "[]"
|
||||
|
||||
|
||||
doc_class "corrollary" = formal_stmt +
|
||||
relevance :: "relevance"
|
||||
property :: "term list" <= "[]"
|
||||
|
||||
text\<open>This monitor is used to group formal content in a way to classify the
|
||||
relevance. On the presentation level, this gives the possibility to adapt or omit
|
||||
Isabelle/Isar lemma and theorem commands according to their relevance level.
|
||||
By using inheritance, the document class @{text \<open>formal_content\<close>} can also be used
|
||||
to introduce organisational information (for example: developer or tester or validator )
|
||||
as a systematic means to produce documents oriented to specific needs of user (sub-)groups.\<close>
|
||||
|
||||
doc_class formal_content =
|
||||
relevance :: "relevance"
|
||||
accepts "\<lbrace>definition || assertion || lemma || theorem || corrollary \<rbrace>\<^sup>+"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
end
|
||||
|
|
@ -26,7 +26,8 @@ doc_class text_section =
|
|||
main_author :: "author option" <= None
|
||||
fixme_list :: "string list" <= "[]"
|
||||
level :: "int option" <= "None"
|
||||
(* we follow LaTeX terminology on levels
|
||||
(* this attribute enables doc-notation support section* etc.
|
||||
we follow LaTeX terminology on levels
|
||||
part = Some -1
|
||||
chapter = Some 0
|
||||
section = Some 1
|
||||
|
|
@ -55,15 +56,13 @@ doc_class "conclusion" = text_section +
|
|||
doc_class related_work = "conclusion" +
|
||||
main_author :: "author option" <= None
|
||||
|
||||
(* There is no consensus if this is a good classification *)
|
||||
datatype formal_content_kind = "definition" | "axiom" | aux_lemma | "lemma" | "corrollary" | "theorem"
|
||||
|
||||
doc_class "thm_elements" = "thms" +
|
||||
kind :: "formal_content_kind option"
|
||||
|
||||
doc_class bibliography = text_section +
|
||||
style :: "string option" <= "Some ''LNCS''"
|
||||
|
||||
doc_class annex = "text_section" +
|
||||
main_author :: "author option" <= None
|
||||
|
||||
|
||||
text\<open> Besides subtyping, there is another relation between
|
||||
doc_classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
|
||||
which is expressed by occurrence in the where clause.
|
||||
|
|
@ -100,7 +99,8 @@ doc_class article =
|
|||
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
|
||||
bibliography)"
|
||||
bibliography ~~
|
||||
\<lbrace>annex\<rbrace>\<^sup>* )"
|
||||
|
||||
|
||||
ML\<open>
|
||||
|
|
@ -154,11 +154,10 @@ end
|
|||
|
||||
setup\<open> let val cidS = ["scholarly_paper.introduction","scholarly_paper.technical",
|
||||
"scholarly_paper.example", "scholarly_paper.conclusion"];
|
||||
val upd = DOF_core.update_class_invariant "scholarly_paper.article"
|
||||
fun body moni_oid _ ctxt = (Scholarly_paper_trace_invariant.check
|
||||
ctxt cidS moni_oid @{here};
|
||||
true)
|
||||
in upd body end\<close>
|
||||
in DOF_core.update_class_invariant "scholarly_paper.article" body end\<close>
|
||||
|
||||
|
||||
(* some test code *)
|
||||
|
|
|
|||
Loading…
Reference in New Issue