diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 324606e..9354119 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -1860,6 +1860,16 @@ ML\ \ *) +ML\open Thread\ +(* concurrency experiments: +ML\open Thread\ +ML\open Future\ +ML\open OS.Process\ +ML\ALLGOALS\ + +ML\open Goal\ +ML \future_result;\ +*) end diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty index eee9c44..a8313a3 100644 --- a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty +++ b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty @@ -182,6 +182,82 @@ \end{isamarkuptext}% } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newisadof{text.scholarly_paper.theorem}% +[label=,type=% + , scholarly_paper.theorem.tag =% + , 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.technical.status}}{semiformal}}{ + \ifthenelse{\equal{\commandkey{scholarly_paper.theorem.tag}} {} } + {\begin{theorem} \label{\commandkey{label}} #1 \end{theorem} } + {\begin{theorem} [\commandkey{scholarly_paper.theorem.tag}] \label{\commandkey{label}} #1 \end{theorem}} + }{% + #1% + }% + \end{isamarkuptext}% + } +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newisadof{text.scholarly_paper.lemma}% +[label=,type=% + , scholarly_paper.lemma.tag =% + , 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.technical.status}}{semiformal}}{ + \ifthenelse{\equal{\commandkey{scholarly_paper.lemma.tag}} {} } + {\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} } + {\begin{{} [\commandkey{scholarly_paper.lemma.tag}] \label{\commandkey{label}} #1 \end{{}} + }{% + #1% + }% + \end{isamarkuptext}% + } +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\newisadof{text.scholarly_paper.corollary}% +[label=,type=% + , scholarly_paper.corollary.tag =% + , 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.technical.status}}{semiformal}}{ + \ifthenelse{\equal{\commandkey{scholarly_paper.corollary.tag}} {} } + {\begin{corollary} \label{\commandkey{label}} #1 \end{corollary} } + {\begin{corollary} [\commandkey{scholarly_paper.corollary.tag}] \label{\commandkey{label}} #1 \end{corollary}} + }{% + #1% + }% + \end{isamarkuptext}% + } + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newisadof{text.scholarly_paper.example}% [label=,type=% , scholarly_paper.example.tag =% diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 8e4127e..718de0f 100644 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -65,19 +65,20 @@ A formal statement can, but must not have a reference to true formal Isabelle/Is \ datatype status = semiformal | description +text\The class \<^verbatim>\technical\ regroups a number of text-elements that contain typical +"technical content" in mathematical or engineering papers: definitions, theorems, lemmas, examples. \ + +(* OPEN PROBLEM: connection between referentiable and status. This should be explicit + and computable. *) + +(* TODO : RENAME "tag" by "short_name" *) + doc_class technical = text_section + definition_list :: "string list" <= "[]" status :: status <= "description" formal_results :: "thm list" -text\A very rough formatting style could be modeled as follows:\ - - -doc_class "experiment" = technical + - tag :: "string" <= "''''" - -doc_class example = technical + - tag :: "string" <= "''''" +text\A rough structuring is modeled as follows:\ doc_class "definition" = technical + tag :: "string" <= "''''" @@ -85,10 +86,39 @@ doc_class "definition" = technical + doc_class "theorem" = technical + tag :: "string" <= "''''" +text\Note that the following two text-elements are currently set to no-keyword in LNCS style.\ +doc_class "lemma" = technical + + tag :: "string" <= "''''" + +doc_class "corollary" = technical + + tag :: "string" <= "''''" + + +text\ \<^verbatim>\examples\ are currently considered \<^verbatim>\technical\. Another alternative would be to group the + following classes into an own class: "evaluation" or "explanation" or ... \ + +doc_class example = technical + + tag :: "string" <= "''''" + +doc_class assertion = technical + + tag :: "string" <= "''''" + + +(* TODO :*) +(* attention : no LaTeX support yet >>> *) doc_class "code" = technical + checked :: bool <= "False" tag :: "string" <= "''''" +doc_class "experiment" = technical + + tag :: "string" <= "''''" + +doc_class "evaluation" = technical + + tag :: "string" <= "''''" + +doc_class "data" = technical + + tag :: "string" <= "''''" + text\The @{doc_class "code"} is a general stub for free-form and type-checked code-fragments such as: \<^enum> SML code @@ -143,14 +173,14 @@ text \underlying idea: a monitor class automatically receives a doc_class article = style_id :: string <= "''LNCS''" version :: "(int \ int \ int)" <= "(0,0,0)" - accepts "(title ~~ - \subtitle\ ~~ - \author\\<^sup>+ ~~ - abstract ~~ + accepts "(title ~~ + \subtitle\ ~~ + \author\\<^sup>+ ~~ + abstract ~~ \introduction\\<^sup>+ ~~ - \technical || example\\<^sup>+ ~~ - \conclusion\\<^sup>+ ~~ - bibliography ~~ + \technical\\<^sup>+ ~~ + \conclusion\\<^sup>+ ~~ + bibliography ~~ \annex\\<^sup>* )" diff --git a/src/tests/InnerSyntaxAntiquotations.thy b/src/tests/InnerSyntaxAntiquotations.thy index 1e8c512..34b8bcf 100644 --- a/src/tests/InnerSyntaxAntiquotations.thy +++ b/src/tests/InnerSyntaxAntiquotations.thy @@ -29,8 +29,10 @@ They are the key-mechanism to denote \<^item> Ontological Links, i.e. attributes refering to document classes defined by the ontology \<^item> Ontological F-Links, i.e. attributes referring to formal entities inside Isabelle (such as thm's) -This file contains a number of examples resulting from the @{theory "Isabelle_DOF-tests.Conceptual"} - ontology; -the emphasis of this presentation is to present the expressivity of ODL on a paradigmatical example. +This file contains a number of examples resulting from the +% @ {theory "Isabelle_DOF-tests.Conceptual"} does not work here --- why ? +\<^theory_text>\Conceptual\ - ontology; the emphasis of this presentation is to present the expressivity of +ODL on a paradigmatical example. \ @@ -56,20 +58,20 @@ text\Example for a meta-attribute of ODL-type @{typ "typ"} with an appropr theorem @{thm "refl"}}\ text*[xcv2::C, g="@{thm ''HOL.refl''}"]\Lorem ipsum ...\ -text\Major sample: test-item of doc-class \verb+F+ with a relational link, and links to formal - Isabelle items. \ +text\Major sample: test-item of doc-class \F\ with a relational link between class instances, + and links to formal Isabelle items like \typ\, \term\ and \thm\. \ text*[xcv4::F, r="[@{thm ''HOL.refl''}, - @{thm ''InnerSyntaxAntiquotations.murks''}]", - b="{(@{docitem ''xcv1''},@{docitem ''xcv2''})}", - s="[@{typ ''int list''}]", - properties = "[@{term ''H --> H''}]" + @{thm \InnerSyntaxAntiquotations.murks\}]", (* long names required *) + b="{(@{docitem ''xcv1''},@{docitem \xcv2\})}", (* notations \...\ vs. ''...'' *) + s="[@{typ \int list\}]", + properties = "[@{term \H \ H\}]" (* notation \...\ required for UTF8*) ]\Lorem ipsum ...\ -text*[xcv5::G, g="@{thm ''HOL.sym''}"]\Lorem ipsum ...\ +text*[xcv5::G, g="@{thm \HOL.sym\}"]\Lorem ipsum ...\ text\... and here we add a relation between @{docitem \xcv3\} and @{docitem \xcv2\} into the relation \verb+b+ of @{docitem \xcv5\}. Note that in the link-relation, -a @{typ "C"}-type is required, but a @{typ "G"}-type is offered which is leagal in +a @{typ "C"}-type is required, but a @{typ "G"}-type is offered which is legal in \verb+Isa_DOF+ because of the sub-class relation between those classes: \ update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"]