From 3c90e19d110bbddbe3384e9cfb0a8eb561ef6aee Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 25 Feb 2020 12:38:59 +0100 Subject: [PATCH] added lemma into sty; fresh discussion with ADB on scholarly_paper onto. --- src/SI/SI_Dimensions.thy | 1 + .../scholarly_paper/DOF-scholarly_paper.sty | 76 +++++-------- .../scholarly_paper/scholarly_paper.thy | 106 +++++++++++++----- 3 files changed, 101 insertions(+), 82 deletions(-) diff --git a/src/SI/SI_Dimensions.thy b/src/SI/SI_Dimensions.thy index ce4214eb..c35c58c7 100644 --- a/src/SI/SI_Dimensions.thy +++ b/src/SI/SI_Dimensions.thy @@ -172,6 +172,7 @@ class dim_type = finite + fixes dim_ty_sem :: "'a itself \ Dimension" assumes unitary_unit_pres: "card (UNIV::'a set) = 1" + syntax "_SI" :: "type \ logic" ("SI'(_')") diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty index a8313a38..794dac6d 100644 --- a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty +++ b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty @@ -182,6 +182,31 @@ \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{lemma} [\commandkey{scholarly_paper.theorem.tag}] \label{\commandkey{label}} #1 \end{lemma}} + }{% + #1% + }% + \end{isamarkuptext}% + } +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newisadof{text.scholarly_paper.theorem}% [label=,type=% , scholarly_paper.theorem.tag =% @@ -207,57 +232,6 @@ \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 840a5f88..0e30aaa6 100644 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -20,6 +20,7 @@ begin text\Scholarly Paper provides a number of standard text - elements for scientific papers. They were introduced in the following.\ +subsection\General Paper Structuring Elements\ doc_class title = short_title :: "string option" <= "None" @@ -47,8 +48,6 @@ text\Scholarly Paper is oriented towards the classical domains in science: which we formalize into:\ -datatype sc_dom = math | info | natsc | eng - doc_class text_section = text_element + main_author :: "author option" <= None fixme_list :: "string list" <= "[]" @@ -63,6 +62,26 @@ doc_class text_section = text_element + ... *) (* for scholarly paper: invariant level > 0 *) + +doc_class "conclusion" = text_section + + main_author :: "author option" <= None + +doc_class related_work = "conclusion" + + main_author :: "author option" <= None + +doc_class bibliography = text_section + + style :: "string option" <= "Some ''LNCS''" + +doc_class annex = "text_section" + + main_author :: "author option" <= None + +(* +datatype sc_dom = math | info | natsc | eng +*) + + +subsection\Introductions\ + doc_class introduction = text_section + comment :: string claims :: "thm list" @@ -76,6 +95,10 @@ As Security of the system we define etc... A formal statement can, but must not have a reference to true formal Isabelle/Isar definition. \ + + +subsection\Technical Content and its Formats\ + datatype status = semiformal | description text\The class \<^verbatim>\technical\ regroups a number of text-elements that contain typical @@ -91,10 +114,28 @@ doc_class technical = text_section + status :: status <= "description" formal_results :: "thm list" -type_synonym tc = technical - -text\A rough structuring is modeled as follows:\ +type_synonym tc = technical + +subsection\Mathematical Statements\ + +datatype math_statement_class = + "definition" | "axiom" | "theorem" | "lemma" | "proposition" | "rule" | "assertion" + +doc_class math_statement = tc + + short_name :: string <= "''''" + "class" :: "math_statement_class" + status :: status + +doc_class math_description = math_statement + + referentiable :: bool <= "False" + +doc_class math_semi_formal_stmt = math_statement + + referentiable :: bool <= "True" + + +text\A rough structuring is modeled as follows:\ +(* non-evident-statement *) doc_class "definition" = tc + referentiable :: bool <= "True" tag :: "string" <= "''''" @@ -112,34 +153,21 @@ doc_class "corollary" = tc + referentiable :: bool <= "True" tag :: "string" <= "''''" +subsection\Example Statements\ -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 ... \ +text\ \<^verbatim>\examples\ are currently considered \<^verbatim>\technical\. Is a main category to be refined + via inheritance. \ doc_class example = technical + referentiable :: bool <= "True" tag :: "string" <= "''''" -doc_class assertion = technical + - referentiable :: bool <= "True" - tag :: "string" <= "''''" +subsection\Code Statement Elements\ - -(* 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 @@ -152,17 +180,33 @@ own content checking and, of course, presentation styles. \ -doc_class "conclusion" = text_section + - main_author :: "author option" <= None - -doc_class related_work = "conclusion" + - main_author :: "author option" <= None +doc_class "SML" = code + + checked :: bool <= "False" -doc_class bibliography = text_section + - style :: "string option" <= "Some ''LNCS''" +doc_class "ISAR" = code + + checked :: bool <= "False" + +doc_class "LATEX" = code + + checked :: bool <= "False" + +subsection\Content in Engineering/Tech Papers \ + + +doc_class eng_statement = tc + + short_name :: string <= "''''" + "class" :: "math_statement_class" + status :: status + + +doc_class "experiment" = eng_statement + + tag :: "string" <= "''''" + +doc_class "evaluation" = eng_statement + + tag :: "string" <= "''''" + +doc_class "data" = eng_statement + + tag :: "string" <= "''''" -doc_class annex = "text_section" + - main_author :: "author option" <= None text\ Besides subtyping, there is another relation between