From a1d6431df9a34cf118946cd0337f3c3a592569c2 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 19 Dec 2018 12:05:57 +0100 Subject: [PATCH] Added discussed ontology "math_paper" and an example reffering to (some elements) of it. --- examples/conceptual/AssnsLemmaThmEtc.thy | 38 +++++++++ examples/conceptual/Attributes.thy | 9 +- ontologies/math_paper.thy | 100 +++++++++++++++++++++++ ontologies/scholarly_paper.thy | 19 ++--- 4 files changed, 150 insertions(+), 16 deletions(-) create mode 100644 examples/conceptual/AssnsLemmaThmEtc.thy create mode 100644 ontologies/math_paper.thy diff --git a/examples/conceptual/AssnsLemmaThmEtc.thy b/examples/conceptual/AssnsLemmaThmEtc.thy new file mode 100644 index 0000000..8f1a6c2 --- /dev/null +++ b/examples/conceptual/AssnsLemmaThmEtc.thy @@ -0,0 +1,38 @@ +theory AssnsLemmaThmEtc + imports "../../ontologies/Conceptual" "../../ontologies/math_paper" +begin + +section\Elementary Creation of Doc-items and Access of their Attibutes\ + +text\Current status:\ +print_doc_classes +print_doc_items + + + +section\Definitions, Lemmas, Theorems, Assertions\ +(* auxilliary *) +ML\fun assert_list_dest X = map HOLogic.dest_string + (map (fn Const ("Isa_DOF.ISA_term", _) $ s => s ) + (HOLogic.dest_list X))\ + + +text*[aa::F]\Our definition of the HOL-Logic has the following properties:\ +assert*[aa::F] "True" + +ML\assert_list_dest @{docitem_attribute property :: aa}\ +assert*[aa::F] "True & True" (* small pb: unicodes crashes here ... *) +ML\ assert_list_dest @{docitem_attribute property :: aa}\ + +text\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>\property\: \ + +text*[aaa::assertion]\Our definition of the integers has the following properties:\ +assert*[aaa::assertion] "3 < (4::int)" +assert*[aaa::assertion] "0 < (4::int)" + + +end +(*>*) diff --git a/examples/conceptual/Attributes.thy b/examples/conceptual/Attributes.thy index e0d5629..eacb904 100644 --- a/examples/conceptual/Attributes.thy +++ b/examples/conceptual/Attributes.thy @@ -126,13 +126,10 @@ ML \@{trace_attribute figs1}\ text\Resulting trace of figs as text antiquotation:\ text\@{trace_attribute figs1}\ +(*<*) text\Final Status:\ print_doc_items print_doc_classes -(*quatsch so far *) -text*[aa::figure]\dfg\ -assert*[aa] "True" - - -end \ No newline at end of file +end +(*>*) diff --git a/ontologies/math_paper.thy b/ontologies/math_paper.thy new file mode 100644 index 0000000..95c0e1d --- /dev/null +++ b/ontologies/math_paper.thy @@ -0,0 +1,100 @@ +chapter \The Document Ontology Common Library for the Isabelle Ontology Framework\ + +text\ 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. \ + + +theory math_paper + imports "../Isa_DOF" +begin + + +section\Some attempt to model standardized links to Standard Isabelle Formal Content\ + +text\ 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>\complement\ 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 ... \ + +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\Which gives rise to a presentation like:\ +(*<*) +type_notation nat ("\") +(*>*) +text*[dil_fun :: "definition"]\A dilating function for a run @{term "\"} is a function +@{typ "\ \ \"} that satisfies: +\<^enum> @{term "f"} is strictly monotonic ... +\<^enum> ... +\<^enum> ... +\ + + +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\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 \formal_content\} 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.\ + +doc_class formal_content = + relevance :: "relevance" + accepts "\definition || assertion || lemma || theorem || corrollary \\<^sup>+" + + + + + +end diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy index 328f2a9..8e2738b 100644 --- a/ontologies/scholarly_paper.thy +++ b/ontologies/scholarly_paper.thy @@ -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\ Besides subtyping, there is another relation between doc_classes: a class can be a \<^emph>\monitor\ to other ones, which is expressed by occurrence in the where clause. @@ -100,7 +99,8 @@ doc_class article = \introduction\\<^sup>+ ~~ \technical || example\\<^sup>+ ~~ \conclusion\\<^sup>+ ~~ - bibliography)" + bibliography ~~ + \annex\\<^sup>* )" ML\ @@ -154,11 +154,10 @@ end setup\ 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\ + in DOF_core.update_class_invariant "scholarly_paper.article" body end\ (* some test code *)