pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF

This commit is contained in:
Achim D. Brucker 2020-05-03 14:59:01 +01:00
parent 3de76c8023 fa931b45e2
commit 640ba5db6d
10 changed files with 416 additions and 293 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
View File

@ -538,7 +538,6 @@ text\<open>
| @@{command "text*"} | @@{command "figure*"} | @@{command "side_by_side_figure*"}
| @@{command "open_monitor*"} | @@{command "close_monitor*"}
| @@{command "Definition*"} | @@{command "Lemma*"}
| @@{command "Theorem*"} | @@{command "Conjecture*"}
)
\<newline>
'[' meta_args ']' '\<open>' text '\<close>'

168
src/DOF/Isa_COL.thy
View File

@ -13,39 +13,122 @@
chapter \<open>The Document Ontology Common Library for the Isabelle Ontology Framework\<close>
text\<open> Offering
\<^item> ...
\<^item>
\<^item> LaTeX support. \<close>
text\<open> Building a fundamental infrastructure for common document elements such as
Structuring Text-Elements (the top classes), Figures, Tables (yet todo)
\<close>
theory Isa_COL
imports Isa_DOF
keywords "title*" "subtitle*"
"chapter*" "section*" "subsection*" "subsubsection*"
"paragraph*" "subparagraph*" :: document_body
and "figure*" "side_by_side_figure*" :: document_body
begin
section\<open>Basic Text and Text-Structuring Elements\<close>
text\<open> The attribute @{term "level"} in the subsequent enables doc-notation support section* etc.
we follow LaTeX terminology on levels
\<^enum> part = Some -1
\<^enum> chapter = Some 0
\<^enum> section = Some 1
\<^enum> subsection = Some 2
\<^enum> subsubsection = Some 3
\<^enum> ...
for scholarly paper: invariant level > 0. \<close>
doc_class text_element =
level :: "int option" <= "None"
referentiable :: bool <= "False"
variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}"
doc_class "chapter" = text_element +
level :: "int option" <= "Some 0"
doc_class "section" = text_element +
level :: "int option" <= "Some 1"
doc_class "subsection" = text_element +
level :: "int option" <= "Some 2"
doc_class "subsubsection" = text_element +
level :: "int option" <= "Some 3"
subsection\<open>Ontological Macros\<close>
ML\<open> local open ODL_Command_Parser in
(* *********************************************************************** *)
(* Ontological Macro Command Support *)
(* *********************************************************************** *)
(* {markdown = true} sets the parsing process such that in the text-core markdown elements are
accepted. *)
val _ =
Outer_Syntax.command ("title*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command NONE {markdown = false} ))) ;
val _ =
Outer_Syntax.command ("subtitle*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command NONE {markdown = false} )));
val _ =
Outer_Syntax.command ("chapter*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 0)) {markdown = false} )));
val _ =
Outer_Syntax.command ("section*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 1)) {markdown = false} )));
val _ =
Outer_Syntax.command ("subsection*", @{here}) "subsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 2)) {markdown = false} )));
val _ =
Outer_Syntax.command ("subsubsection*", @{here}) "subsubsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 3)) {markdown = false} )));
val _ =
Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 4)) {markdown = false} )));
val _ =
Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 5)) {markdown = false} )));
end
\<close>
section\<open> Library of Standard Text Ontology \<close>
datatype placement = pl_h | (*here*)
pl_t | (*top*)
pl_b | (*bottom*)
pl_ht | (*here -> top*)
pl_hb (*here -> bottom*)
ML\<open>(Symtab.defined (#docclass_tab(DOF_core.get_data_global @{theory}))) "side_by_side_figure"\<close>
print_doc_classes
doc_class figure =
relative_width :: "int" (* percent of textwidth *)
src :: "string"
placement :: placement
placement :: placement
spawn_columns :: bool <= True
ML\<open>(Symtab.defined (#docclass_tab(DOF_core.get_data_global @{theory}))) "side_by_side_figure"\<close>
print_doc_classes
doc_class side_by_side_figure = figure +
anchor :: "string"
@ -57,7 +140,6 @@ doc_class side_by_side_figure = figure +
print_doc_classes
doc_class figure_group =
(* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *)
caption :: "string"
@ -67,31 +149,46 @@ doc_class figure_group =
print_doc_classes
subsection\<open>Ontological Macros\<close>
(* dito the future table *)
ML\<open> local open ODL_Command_Parser in
(* *********************************************************************** *)
(* Ontological Macro Command Support *)
(* *********************************************************************** *)
val _ =
Outer_Syntax.command ("figure*", @{here}) "figure"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command NONE {markdown = false} )));
val _ =
Outer_Syntax.command ("side_by_side_figure*", @{here}) "multiple figures"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command NONE {markdown = false} )));
end
\<close>
section\<open>Tables\<close>
(* TODO ! ! ! *)
(* dito the future monitor: table - block *)
text\<open> The attribute @{term "level"} in the subsequent enables doc-notation support section* etc.
we follow LaTeX terminology on levels
\<^enum> part = Some -1
\<^enum> chapter = Some 0
\<^enum> section = Some 1
\<^enum> subsection = Some 2
\<^enum> subsubsection = Some 3
\<^enum> ...
section\<open>Tests\<close>
ML\<open>@{term "side_by_side_figure"};
@{typ "doc_class rexp"};
DOF_core.SPY;
\<close>
for scholarly paper: invariant level > 0 \<close>
doc_class text_element =
level :: "int option" <= "None"
referentiable :: bool <= "False"
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 =
section\<open>DEPRECATED : An attempt to model Standard Isabelle Formal Content\<close>
doc_class assertions =
properties :: "term list"
doc_class "thms" =
@ -112,12 +209,5 @@ doc_class concept =
tag :: "string" <= "''''"
properties :: "thm list" <= "[]"
section\<open>Tests\<close>
ML\<open>@{term "side_by_side_figure"};
@{typ "doc_class rexp"};
DOF_core.SPY;
\<close>
end

170
src/DOF/Isa_DOF.thy
View File

@ -35,24 +35,19 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
Assert
keywords "+=" ":=" "accepts" "rejects" "invariant"
and "title*" "subtitle*"
"chapter*" "section*" "subsection*" "subsubsection*"
"paragraph*" "subparagraph*"
"text*" "text-macro*"
"figure*"
"side_by_side_figure*"
"Definition*" "Lemma*" "Theorem*" "Conjecture*"
:: document_body
and "open_monitor*" "close_monitor*" "declare_reference*"
"update_instance*" "doc_class" ::thy_decl
and (* "definition*" *) "corrollary*" "proposition*" "schematic_goal*"
and "text*" "text-macro*" :: document_body
and "print_doc_classes" "print_doc_items" "check_doc_global" :: diag
(* experimental *)
and "corrollary*" "proposition*" "schematic_goal*"
"lemma*" "theorem*" (* -- intended replacement of Isar std commands.*)
"assert*" ::thy_decl
and "print_doc_classes" "print_doc_items" "check_doc_global" :: diag
begin
@ -1245,12 +1240,29 @@ fun enriched_document_command level =
val enriched_document_command_macro = enriched_document_command (* TODO ... *)
fun enriched_formal_statement_command (tag:string) =
let fun transform doc_attrs = (("tag",@{here}),"''"^tag^"''") ::
(("properties",@{here}),"([]::thm list)")::doc_attrs
fun enriched_formal_statement_command (cat:string,tag:string) =
let fun transform doc_attrs = ((cat,@{here}),tag) ::
(("formal_results",@{here}),"([]::thm list)")::doc_attrs
in gen_enriched_document_command transform end;
fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list),
prop) =
let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy))
fun conv_attrs thy = (("properties",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]")
::doc_attrs
fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy)
fun mks thy = case DOF_core.get_object_global_opt oid thy of
SOME NONE => (error("update of declared but not created doc_item:" ^ oid))
| SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy)
| NONE => (create_and_check_docitem false oid pos cid_pos (conv_attrs thy) thy)
val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global
in
(* Toplevel.keep (check o Toplevel.context_of) *)
Toplevel.theory (fn thy => (check thy; mks thy))
end
fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : meta_args_t) =
let fun o_m_c oid pos cid_pos doc_attrs thy = create_and_check_docitem
true oid pos cid_pos doc_attrs thy
@ -1295,101 +1307,8 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
|> delete_monitor_entry
end
(* *********************************************************************** *)
(* Textual Command Support *)
(* *********************************************************************** *)
(* Core Command Definitions *)
(* {markdown = true} sets the parsing process such that in the text-core markdown elements are
accepted. *)
val _ =
Outer_Syntax.command ("Definition*", @{here}) "Textual Definition"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_formal_statement_command "definition" {markdown = true} )));
val _ =
Outer_Syntax.command ("Lemma*", @{here}) "Textual Lemma Outline"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_formal_statement_command "lemma" {markdown = true} )));
val _ =
Outer_Syntax.command ("Theorem*", @{here}) "Textual Theorem Outline"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_formal_statement_command "theorem" {markdown = true} )));
val _ =
Outer_Syntax.command ("Conjecture*", @{here}) "Textual Theorem Outline"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_formal_statement_command "conjecture" {markdown = true} )));
val _ =
Outer_Syntax.command ("title*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command NONE {markdown = false} ))) ;
val _ =
Outer_Syntax.command ("subtitle*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command NONE {markdown = false} )));
val _ =
Outer_Syntax.command ("chapter*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 0)) {markdown = false} )));
val _ =
Outer_Syntax.command ("section*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 1)) {markdown = false} )));
val _ =
Outer_Syntax.command ("subsection*", @{here}) "subsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 2)) {markdown = false} )));
val _ =
Outer_Syntax.command ("subsubsection*", @{here}) "subsubsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 3)) {markdown = false} )));
val _ =
Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 4)) {markdown = false} )));
val _ =
Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 5)) {markdown = false} )));
val _ =
Outer_Syntax.command ("figure*", @{here}) "figure"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command NONE {markdown = false} )));
val _ =
Outer_Syntax.command ("side_by_side_figure*", @{here}) "multiple figures"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command NONE {markdown = false} )));
val _ =
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
(attributes -- Parse.opt_target -- Parse.document_source
>> (Toplevel.theory o (enriched_document_command NONE {markdown = true} )));
val _ =
Outer_Syntax.command ("text-macro*", @{here}) "formal comment macro"
(attributes -- Parse.opt_target -- Parse.document_source
>> (Toplevel.theory o (enriched_document_command_macro NONE {markdown = true} )));
val _ =
Outer_Syntax.command @{command_keyword "declare_reference*"}
"declare document reference"
(attributes >> (fn (((oid,pos),cid),doc_attrs) =>
(Toplevel.theory (DOF_core.declare_object_global oid))));
val _ =
Outer_Syntax.command @{command_keyword "open_monitor*"}
@ -1408,31 +1327,32 @@ val _ =
(attributes_upd >> (Toplevel.theory o update_instance_command));
fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list),
prop) =
let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy))
fun conv_attrs thy = (("properties",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]")
::doc_attrs
fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy)
fun mks thy = case DOF_core.get_object_global_opt oid thy of
SOME NONE => (error("update of declared but not created doc_item:" ^ oid))
| SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy)
| NONE => (create_and_check_docitem false oid pos cid_pos (conv_attrs thy) thy)
val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global
in
(* Toplevel.keep (check o Toplevel.context_of) *)
Toplevel.theory (fn thy => (check thy; mks thy))
end
val _ =
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
(attributes -- Parse.opt_target -- Parse.document_source
>> (Toplevel.theory o (enriched_document_command NONE {markdown = true} )));
val _ =
Outer_Syntax.command ("text-macro*", @{here}) "formal comment macro"
(attributes -- Parse.opt_target -- Parse.document_source
>> (Toplevel.theory o (enriched_document_command_macro NONE {markdown = true} )));
val _ =
Outer_Syntax.command @{command_keyword "declare_reference*"}
"declare document reference"
(attributes >> (fn (((oid,pos),cid),doc_attrs) =>
(Toplevel.theory (DOF_core.declare_object_global oid))));
val _ =
Outer_Syntax.command @{command_keyword "assert*"}
"evaluate and print term"
(attributes -- opt_evaluator -- opt_modes -- Parse.term >> assertion_cmd');
end (* struct *)
end
\<close>
ML\<open>
structure ODL_LTX_Converter =
struct

1
src/DOF/latex/DOF-COL.sty
View File

@ -55,6 +55,7 @@
\newisadof{side_by_side_figure.Isa_COL.side_by_side_figure}%
[label=,type=%
,Isa_COL.figure.relative_width=%
,Isa_COL.figure.placement=%
,Isa_COL.figure.src=%
,Isa_COL.side_by_side_figure.anchor=%
,Isa_COL.side_by_side_figure.caption=%

124
src/ontologies/CENELEC_50128/CENELEC_50128.thy
View File

@ -25,28 +25,40 @@ identifies:
(*<<*)
theory CENELEC_50128
imports "../../DOF/Isa_COL"
imports "../technical_report/technical_report"
begin
(*>>*)
text\<open>We re-use the class @\<open>typ math_content\<close>, which provides also a framework for
semi-formal terminology, which we re-use by this definition.\<close>
doc_class semi_formal_content = math_content +
status :: status <= "semiformal"
mcc :: math_content_class <= "terminology"
type_synonym sfc = semi_formal_content
(*>>*)
text\<open> Excerpt of the BE EN 50128:2011, page 22. \<close>
section\<open>Terms and Definitions\<close>
Definition*[assessment::concept]\<open>process of analysis to determine whether software, which may include
Definition*[assessment::sfc,short_name="''assessment''"]
\<open>process of analysis to determine whether software, which may include
process, documentation, system, subsystem hardware and/or software components, meets the specified
requirements and to form a judgement as to whether the software is fit for its intended purpose.
Safety assessment is focused on but not limited to the safety properties of a system.\<close>
Definition*[assessor::concept, tag="''assessor''"]
Definition*[assessor::sfc, short_name="''assessor''"]
\<open>entity that carries out an assessment\<close>
Definition*[COTS::concept, tag="''commercial off-the-shelf software''"]
Definition*[COTS::sfc, short_name="''commercial off-the-shelf software''"]
\<open>software defined by market-driven need, commercially available and whose fitness for purpose
has been demonstrated by a broad spectrum of commercial users\<close>
Definition*[component::concept]
Definition*[component::sfc]
\<open>a constituent part of software which has well-defined interfaces and behaviour
with respect to the software architecture and design and fulfils the following
criteria:
@ -57,108 +69,108 @@ criteria:
(e. g. subsystems) which have an independent version
\<close>
Definition*[CMGR::concept, tag="''configuration manager''"]
Definition*[CMGR::sfc, short_name="''configuration manager''"]
\<open>entity that is responsible for implementing and carrying out the processes
for the configuration management of documents, software and related tools including
\<^emph>\<open>change management\<close>\<close>
Definition*[customer::concept]
Definition*[customer::sfc]
\<open>entity which purchases a railway control and protection system including the software\<close>
Definition*[designer::concept]
Definition*[designer::sfc]
\<open>entity that analyses and transforms specified requirements into acceptable design solutions
which have the required safety integrity level\<close>
Definition*[entity::concept]
Definition*[entity::sfc]
\<open>person, group or organisation who fulfils a role as defined in this European Standard\<close>
declare_reference*[fault::concept]
Definition*[error::concept]
declare_reference*[fault::sfc]
Definition*[error::sfc]
\<open>defect, mistake or inaccuracy which could result in failure or in a deviation
from the intended performance or behaviour (cf @{concept (unchecked) \<open>fault\<close>}))\<close>
from the intended performance or behaviour (cf @{semi_formal_content (unchecked) \<open>fault\<close>}))\<close>
Definition*[fault::concept]
Definition*[fault::sfc]
\<open>defect, mistake or inaccuracy which could result in failure or in a deviation
from the intended performance or behaviour (cf @{concept \<open>error\<close>})\<close>
from the intended performance or behaviour (cf @{semi_formal_content \<open>error\<close>})\<close>
Definition*[failure::concept]
Definition*[failure::sfc]
\<open>unacceptable difference between required and observed performance\<close>
Definition*[FT::concept, tag="''fault tolerance''"]
Definition*[FT::sfc, short_name="''fault tolerance''"]
\<open>built-in capability of a system to provide continued correct provision of service as specified,
in the presence of a limited number of hardware or software faults\<close>
Definition*[firmware::concept]
Definition*[firmware::sfc]
\<open>software stored in read-only memory or in semi-permanent storage such as flash memory, in a
way that is functionally independent of applicative software\<close>
Definition*[GS::concept,tag="''generic software''"]
Definition*[GS::sfc,short_name="''generic software''"]
\<open>software which can be used for a variety of installations purely by the provision of
application-specific data and/or algorithms\<close>
Definition*[implementer::concept]
Definition*[implementer::sfc]
\<open>entity that transforms specified designs into their physical realisation\<close>
Definition*[integration::concept]
Definition*[integration::sfc]
\<open>process of assembling software and/or hardware items, according to the architectural and
design specification, and testing the integrated unit\<close>
Definition*[integrator::concept]
Definition*[integrator::sfc]
\<open>entity that carries out software integration\<close>
Definition*[PES :: concept, tag="''pre-existing software''"]
Definition*[PES :: sfc, short_name="''pre-existing software''"]
\<open>software developed prior to the application currently in question, including COTS (commercial
off-the shelf) and open source software\<close>
Definition*[OSS :: concept, tag="''open source software''"]
Definition*[OSS :: sfc, short_name="''open source software''"]
\<open>source code available to the general public with relaxed or non-existent copyright restrictions\<close>
Definition*[PLC::concept, tag="''programmable logic controller''"]
Definition*[PLC::sfc, short_name="''programmable logic controller''"]
\<open>solid-state control system which has a user programmable memory for storage of instructions to
implement specific functions\<close>
Definition*[PM::concept, tag="''project management''"]
Definition*[PM::sfc, short_name="''project management''"]
\<open>administrative and/or technical conduct of a project, including safety aspects\<close>
Definition*[PGMGR::concept, tag="''project manager''"]
Definition*[PGMGR::sfc, short_name="''project manager''"]
\<open>entity that carries out project management\<close>
Definition*[reliability::concept]
Definition*[reliability::sfc]
\<open>ability of an item to perform a required function under given conditions for a given period of time\<close>
Definition*[robustness::concept]
Definition*[robustness::sfc]
\<open>ability of an item to detect and handle abnormal situations\<close>
Definition*[RMGR::concept, tag="''requirements manager''"]
Definition*[RMGR::sfc, short_name="''requirements manager''"]
\<open>entity that carries out requirements management\<close>
Definition*[RMGMT::concept, tag="''requirements management''"]
Definition*[RMGMT::sfc, short_name="''requirements management''"]
\<open>the process of eliciting, documenting, analysing, prioritising and agreeing on requirements and
then controlling change and communicating to relevant stakeholders. It is a continuous process
throughout a project\<close>
Definition*[risk::concept]
Definition*[risk::sfc]
\<open>combination of the rate of occurrence of accidents and incidents resulting in harm (caused by
a hazard) and the degree of severity of that harm\<close>
Definition*[safety::concept]
Definition*[safety::sfc]
\<open>freedom from unacceptable levels of risk of harm to people\<close>
Definition*[SA::concept, tag="''safety authority''"]
Definition*[SA::sfc, short_name="''safety authority''"]
\<open>body responsible for certifying that safety related software or services comply with relevant
statutory safety requirements\<close>
Definition*[SF::concept, tag="''safety function''"]
Definition*[SF::sfc, short_name="''safety function''"]
\<open>a function that implements a part or whole of a safety requirement\<close>
Definition*[SFRS::concept, tag= "''safety-related software''"]
Definition*[SFRS::sfc, short_name= "''safety-related software''"]
\<open>software which performs safety functions\<close>
Definition*[software::concept]
Definition*[software::sfc]
\<open>intellectual creation comprising the programs, procedures, rules, data and any associated
documentation pertaining to the operation of a system\<close>
Definition*[SB::concept, tag="''software baseline''"]
Definition*[SB::sfc, short_name="''software baseline''"]
\<open>complete and consistent set of source code, executable files, configuration files,
installation scripts and documentation that are needed for a software release. Information about
compilers, operating systems, preexisting software and dependent tools is stored as part of the
@ -169,7 +181,7 @@ released and assessed
Definition*[SWLC::concept, tag="''software life-cycle''"]
Definition*[SWLC::sfc, short_name="''software life-cycle''"]
\<open>those activities occurring during a period of time that starts when
software is conceived and ends when the software is no longer available for use. The software life
cycle typically includes a requirements phase, design phase,test phase, integration phase,
@ -177,35 +189,35 @@ deployment phase and a maintenance phase 3.1.35 software maintainability
capability of the software to be modified; to correct faults, improve to a different environment
\<close>
Definition*[SM::concept, tag="''software maintenance''"]
Definition*[SM::sfc, short_name="''software maintenance''"]
\<open> action, or set of actions, carried out on software after deployment functionality
performance or other attributes, or adapt it with the aim of enhancing or correcting its\<close>
Definition*[SOSIL::concept, tag="''software safety integrity level''"]
Definition*[SOSIL::sfc, short_name="''software safety integrity level''"]
\<open>classification number which determines the techniques and measures that have to be applied to
software NOTE Safety-related software has been classified into five safety integrity levels, where
0 is the lowest and 4 the highest.\<close>
Definition*[supplier::concept]
Definition*[supplier::sfc]
\<open>entity that designs and builds a railway control and protection system including the software
or parts thereof\<close>
Definition*[SYSIL::concept, tag="''system safety integrity level''"]
Definition*[SYSIL::sfc, short_name="''system safety integrity level''"]
\<open>classification number which indicates the required degree of confidence that an integrated
system comprising hardware and software will meet its specified safety requirements\<close>
Definition*[tester::concept]\<open>an entity that carries out testing\<close>
Definition*[tester::sfc]\<open>an entity that carries out testing\<close>
Definition*[testing::concept]
Definition*[testing::sfc]
\<open>process of executing software under controlled conditions as to ascertain its behaviour and
performance compared to the corresponding requirements specification\<close>
Definition*[TCT1::concept, tag="''tool class T1''"]
Definition*[TCT1::sfc, short_name="''tool class T1''"]
\<open>generates no outputs which can directly or indirectly contribute to the executable code
(including data) of the software NOTE 11 examples include: a text editor or a requirement or
design support tool with no automatic code generation capabilities; configuration control tools.\<close>
Definition*[TCT2::concept,tag="''tool class T2''"]
Definition*[TCT2::sfc,short_name="''tool class T2''"]
\<open>supports the test or verification of the design or executable code, where errors in the tool
can fail to reveal defects but cannot directly create errors in the executable software
NOTE T2 examples include: a test harness generator; a test coverage measurement tool; a static
@ -213,35 +225,35 @@ analysis tool. reproduce defined versions and be the input for future releases a
at upgrade in the maintenance phase
\<close>
Definition*[TCT3::concept, tag="''tool class T3''"]
Definition*[TCT3::sfc, short_name="''tool class T3''"]
\<open>generates outputs which can directly or indirectly contribute to the executable code
(including data) of the safety related system NOTE T3 examples include: a source code compiler,
a data/algorithms compiler, a tool to change set-points during system operation; an optimising
compiler where the relationship between the source code program and the generated object code is
not obvious; a compiler that incorporates an executable run-time package into the executable code.
\<close>
Definition*[traceability::concept]
Definition*[traceability::sfc, short_name="''traceability''"]
\<open>degree to which relationship can be established between two or more products of a development
process, especially those having a predecessor/successor or master/subordinate relationship to one
another\<close>
Definition*[validation::concept]
Definition*[validation::sfc, short_name="''validation''"]
\<open>process of analysis followed by a judgment based on evidence to
documentation, software or application) fits the user needs,in particular with respect to safety
and quality and determine whether an item (e.g. process, with emphasis on the suitability of its
operation in accordance to its purpose in its intended environment\<close>
Definition*[validator::concept]
Definition*[validator::sfc, short_name="''validator''"]
\<open>entity that is responsible for the validation\<close>
Definition*[verification::concept]
Definition*[verification::sfc, short_name="''verification''"]
\<open>process of examination followed by a judgment based on evidence that output items (process,
documentation, software or application) of a specific development phase fulfils the requirements of
that phase with respect to completeness, correctness and consistency.
NOTE Verification is mostly based on document reviews (design, implementation, test documents etc.).
\<close>
Definition*[verifier::concept]
Definition*[verifier::sfc, short_name="''verifier''"]
\<open>entity that is responsible for one or more verification activities\<close>
@ -388,7 +400,7 @@ doc_class SIR = requirement +
type_synonym safety_integrity_requirement = SIR
text\<open>The following class is a bit unclear about usage and seems to be in
conceptual mismatch with @{typ objectives}: \<close>
sfcual mismatch with @{typ objectives}: \<close>
doc_class SILA = requirement +
is_concerned :: "role set" <= "UNIV"
alloc :: "sil" <= "SIL0"
@ -603,7 +615,7 @@ text\<open>Objective:
The objective of software verification is to examine and arrive at a judgement based on evidence
that output items (process, documentation, software or application) of a specific development
phase fulfil the requirements and plans with respect to completeness, correctness and consistency.
These activities are managed by the @{concept \<open>verifier\<close>}.
These activities are managed by the @{semi_formal_content \<open>verifier\<close>}.
\<close>
text\<open>Outputs:
@ -705,7 +717,7 @@ doc_class test_documentation =
section\<open> META : Testing and Validation \<close>
text\<open>Test : @{concept \<open>COTS\<close>}\<close>
text\<open>Test : @{semi_formal_content \<open>COTS\<close>}\<close>
ML\<open>
DOF_core.read_cid_global @{theory} "requirement";

6
src/ontologies/math_paper/math_paper.thy
View File

@ -11,7 +11,7 @@
* SPDX-License-Identifier: BSD-2-Clause
*************************************************************************)
chapter \<open>The Document Ontology Common Library for the Isabelle Ontology Framework\<close>
chapter \<open>A Math Paper Ontology (obsolete vs. scholarly_paper)\<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
@ -26,8 +26,8 @@ proving environment after all ! So this ontology provides:
theory math_paper
imports "../../DOF/Isa_DOF"
begin
begin
section\<open>Some attempt to model standardized links to Standard Isabelle Formal Content\<close>

123
src/ontologies/scholarly_paper/DOF-scholarly_paper.sty
View File

@ -160,7 +160,7 @@
% \newcommand{\formalMathStmt[label, mcc, ]
% end: scholarly_paper.abstract
% | "rule" | "assn" | "expl" | rem | "notation" | "terminology"
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newisadof{text.scholarly_paper.math_content}%
[label=,type=%
@ -210,16 +210,16 @@
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
{\begin{lemma} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\label{\commandkey{label}} #1
\end{lemma}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{ex}}
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{expl}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
{\begin{example} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\label{\commandkey{label}} #1
\end{example}}
}%
}%
@ -234,24 +234,63 @@
}%
{\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.short_name}} {} }
{\begin{property} \label{\commandkey{label}} #1 \end{property} }
{\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.short_name}} {} }
{\begin{ruleX} \label{\commandkey{label}} #1 \end{ruleX} }
{\begin{ruleX} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{ruleX}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rem}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{remark} \label{\commandkey{label}} #1 \end{remark} }
{\begin{remark} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{remark}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{assn}}
{%
\begin{assertion}[\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{assertion}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{assertion} \label{\commandkey{label}} #1 \end{assertion} }
{\begin{assertion} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{assertion}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{notation}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{notation} \label{\commandkey{label}} #1 \end{notation} }
{\begin{notation} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{notation}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{terminology}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{terminology} \label{\commandkey{label}} #1 \end{terminology} }
{\begin{terminology} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{terminology}}
}%
}%
{%
\typeout{Internal error: enumeration out of sync}
\typeout{Internal error: enumeration out of sync with ontology scholarly-paper.}
}%
}%
}%
}%
}%
}%
@ -269,9 +308,11 @@
% end: scholarly_paper.math_content
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Besser: Einfach durchreichen wg Vererbung !
\newisadof{text.scholarly_paper.math_example}%
[label=,type=%
, scholarly_paper.math_example.short_name =%
, scholarly_paper.math_content.short_name =%
, scholarly_paper.math_content.mcc =%
, Isa_COL.text_element.level =%
, Isa_COL.text_element.referentiable =%
, Isa_COL.text_element.variants =%
@ -283,10 +324,10 @@
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.technical.status}}{semiformal}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_example.short_name}} {} }
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{expl}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
{\begin{example} [\commandkey{scholarly_paper.math_example.short_name}]
{\begin{example} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{example}}
}{%
@ -296,9 +337,11 @@
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Besser: Einfach durchreichen wg Vererbung !
\newisadof{text.scholarly_paper.definition}%
[label=,type=%
, scholarly_paper.definition.tag =%
, scholarly_paper.math_content.short_name =%
, scholarly_paper.math_content.mcc =%
, Isa_COL.text_element.level =%
, Isa_COL.text_element.referentiable =%
, Isa_COL.text_element.variants =%
@ -311,19 +354,21 @@
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.technical.status}}{semiformal}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.definition.tag}} {} }
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{defn}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
{\begin{definition} [\commandkey{scholarly_paper.definition.tag}] \label{\commandkey{label}} #1 \end{definition}}
{\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{definition}}
}{%
#1%
}%
\end{isamarkuptext}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Besser: Einfach durchreichen wg Vererbung !
\newisadof{text.scholarly_paper.lemma}%
[label=,type=%
, scholarly_paper.lemma.tag =%
, scholarly_paper.math_content.short_name =%
, scholarly_paper.math_content.mcc =%
, Isa_COL.text_element.level =%
, Isa_COL.text_element.referentiable =%
, Isa_COL.text_element.variants =%
@ -336,19 +381,21 @@
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.technical.status}}{semiformal}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.lemma.tag}} {} }
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{lem}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
{\begin{lemma} [\commandkey{scholarly_paper.theorem.tag}] \label{\commandkey{label}} #1 \end{lemma}}
{\begin{lemma} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{lemma}}
}{%
#1%
}%
\end{isamarkuptext}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Besser: Einfach durchreichen wg Vererbung !
\newisadof{text.scholarly_paper.theorem}%
[label=,type=%
, scholarly_paper.theorem.tag =%
, scholarly_paper.math_content.short_name =%
, scholarly_paper.math_content.mcc =%
, Isa_COL.text_element.level =%
, Isa_COL.text_element.referentiable =%
, Isa_COL.text_element.variants =%
@ -361,35 +408,39 @@
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.technical.status}}{semiformal}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.theorem.tag}} {} }
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{thm}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{theorem} \label{\commandkey{label}} #1 \end{theorem} }
{\begin{theorem} [\commandkey{scholarly_paper.theorem.tag}] \label{\commandkey{label}} #1 \end{theorem}}
{\begin{theorem} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{theorem}}
}{%
#1%
}%
\end{isamarkuptext}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Generic Example. Different inheritance hierachy.
\newisadof{text.scholarly_paper.example}%
[label=,type=%
, scholarly_paper.example.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 =%
, scholarly_paper.technical.definition_list =%
, scholarly_paper.technical.status =%
, scholarly_paper.example.status =%
, scholarly_paper.example.short_name =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.technical.status}}{semiformal}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.example.tag}} {} }
\ifthenelse{\equal{\commandkey{scholarly_paper.example.status}}{semiformal}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.example.short_name}} {} }
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
{\begin{example} [\commandkey{scholarly_paper.example.tag}] \label{\commandkey{label}} #1 \end{example}}
}{%
{\begin{example} [\commandkey{scholarly_paper.example.short_name}] %
\label{\commandkey{label}} #1 %
\end{example}} %
}%
{%
#1%
}%
\end{isamarkuptext}%

108
src/ontologies/scholarly_paper/scholarly_paper.thy
View File

@ -14,7 +14,10 @@
section\<open>An example ontology for a scholarly paper\<close>
theory scholarly_paper
imports "../../DOF/Isa_COL"
imports "../../DOF/Isa_COL"
keywords "Definition*" "Lemma*" "Theorem*" :: document_body
begin
text\<open>Scholarly Paper provides a number of standard text - elements for scientific papers.
@ -106,16 +109,28 @@ text\<open>The class \<^verbatim>\<open>technical\<close> regroups a number of t
(* 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"
status :: status <= "description"
formal_results :: "thm list"
invariant L1 :: "\<lambda>\<sigma>::technical. the (level \<sigma>) > 0"
type_synonym tc = technical (* technical content *)
text \<open>This a \<open>doc_class\<close> of \<^verbatim>\<open>examples\<close> in the broadest possible sense : they are \emph{not}
necessarily considered as technical content, but may occur in an article.
Note that there are \<open>doc_class\<close>es of \<^verbatim>\<open>math_example\<close>s and \<^verbatim>\<open>tech_example\<close>s which
follow a more specific regime of mathematical or engineering content.
\<close>
(* An example for the need of multiple inheritance on classes ? *)
doc_class example = text_section +
referentiable :: bool <= True
status :: status <= "description"
short_name :: string <= "''''"
subsection\<open>Mathematical Content\<close>
@ -124,8 +139,9 @@ provided \<^emph>\<open>theorem environments\<close> (see \<^verbatim>\<open>tex
\<^verbatim>\<open>axiom\<close>, \<^verbatim>\<open>rule\<close> and \<^verbatim>\<open>assertion\<close> to the list. A particular advantage of \<^verbatim>\<open>texdoc amslatex\<close> is
that it is well-established and compatible with many LaTeX - styles.\<close>
datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop"
| "ex" | "rule" | "assn"
datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop"
| "expl" | "rule" | "assn"
| rem | "notation" | "terminology"
(*
thm Theorem Italic
@ -133,7 +149,7 @@ cor Corollary Italic
lem Lemma Italic
prop Proposition
defn Definition
ex Example
expl Example
rem Remark
notation
@ -169,12 +185,6 @@ 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 s3 :: "\<lambda> \<sigma>::math_example. \<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.
@ -183,33 +193,68 @@ doc_class math_semiformal = math_content +
referentiable :: bool <= True
type_synonym math_sfc = math_semiformal
subsection\<open>old style onto model.\<close>
subsection\<open>Instances of the abstract classes Definition / Class / Lemma etc.\<close>
text\<open>A rough structuring is modeled as follows:\<close>
(* non-evident-statement *)
doc_class "definition" = tc +
text\<open>The key class definitions are motivated by the AMS style.\<close>
doc_class "definition" = math_content +
referentiable :: bool <= True
tag :: "string" <= "''''"
mcc :: "math_content_class" <= "defn"
invariant d1 :: "\<lambda> \<sigma>::definition. mcc \<sigma> = defn"
doc_class "theorem" = tc +
doc_class "theorem" = math_content +
referentiable :: bool <= True
tag :: "string" <= "''''"
mcc :: "math_content_class" <= "thm"
invariant d2 :: "\<lambda> \<sigma>::theorem. mcc \<sigma> = thm"
text\<open>Note that the following two text-elements are currently set to no-keyword in LNCS style.\<close>
doc_class "lemma" = tc +
doc_class "lemma" = math_content +
referentiable :: bool <= "True"
tag :: "string" <= "''''"
mcc :: "math_content_class" <= "lem"
invariant d3 :: "\<lambda> \<sigma>::lemma. mcc \<sigma> = lem"
doc_class "corollary" = tc +
doc_class "corollary" = math_content +
referentiable :: bool <= "True"
tag :: "string" <= "''''"
mcc :: "math_content_class" <= "cor"
invariant d4 :: "\<lambda> \<sigma>::corollary. mcc \<sigma> = thm"
doc_class "math_example" = math_content +
referentiable :: bool <= "True"
mcc :: "math_content_class" <= "expl"
invariant d5 :: "\<lambda> \<sigma>::math_example. mcc \<sigma> = expl"
subsection\<open>Ontological Macros\<close>
ML\<open> local open ODL_Command_Parser in
(* *********************************************************************** *)
(* Ontological Macro Command Support *)
(* *********************************************************************** *)
(* {markdown = true} sets the parsing process such that in the text-core markdown elements are
accepted. *)
val _ =
Outer_Syntax.command ("Definition*", @{here}) "Textual Definition"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_formal_statement_command ("mcc","defn") {markdown = true} )));
val _ =
Outer_Syntax.command ("Lemma*", @{here}) "Textual Lemma Outline"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_formal_statement_command ("mcc","lem") {markdown = true} )));
val _ =
Outer_Syntax.command ("Theorem*", @{here}) "Textual Theorem Outline"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_formal_statement_command ("mcc","thm") {markdown = true} )));
end
\<close>
subsection\<open>Example Statements\<close>
text\<open> \<^verbatim>\<open>examples\<close> are currently considered \<^verbatim>\<open>technical\<close>. Is a main category to be refined
via inheritance. \<close>
doc_class example = technical +
doc_class tech_example = technical +
referentiable :: bool <= True
tag :: "string" <= "''''"
@ -245,18 +290,18 @@ doc_class "LATEX" = code +
subsection\<open>Content in Engineering/Tech Papers \<close>
doc_class engineering_statement = tc +
doc_class engineering_content = tc +
short_name :: string <= "''''"
status :: status
type_synonym eng_stmt = engineering_statement
type_synonym eng_c = engineering_content
doc_class "experiment" = eng_stmt +
doc_class "experiment" = eng_c +
tag :: "string" <= "''''"
doc_class "evaluation" = eng_stmt +
doc_class "evaluation" = eng_c +
tag :: "string" <= "''''"
doc_class "data" = eng_stmt +
doc_class "data" = eng_c +
tag :: "string" <= "''''"
@ -297,7 +342,7 @@ doc_class article =
\<lbrace>author\<rbrace>\<^sup>+ ~~
abstract ~~
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
\<lbrace>technical\<rbrace>\<^sup>+ ~~
\<lbrace>technical || example \<rbrace>\<^sup>+ ~~
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
bibliography ~~
\<lbrace>annex\<rbrace>\<^sup>* )"
@ -385,5 +430,6 @@ fun check_group a = map (check_group_elem (check_level_hd (hd a))) (tl a) ;
\<close>
end

2
src/ontologies/technical_report/technical_report.thy
View File

@ -40,7 +40,7 @@ doc_class report =
abstract ~~
\<lbrakk>table_of_contents\<rbrakk> ~~
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
\<lbrace>technical || figure || side_by_side_figure\<rbrace>\<^sup>+ ~~
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
\<lbrace>index\<rbrace>\<^sup>* ~~
bibliography)"

6
src/tests/InnerSyntaxAntiquotations.thy
View File

@ -11,7 +11,11 @@
* SPDX-License-Identifier: BSD-2-Clause
*************************************************************************)
chapter\<open>Inner Syntax Antiquotations (ISA)'s\<close>
chapter\<open>Term Antiquotations\<close>
text\<open>Terms are represented by "Inner Syntax" parsed by an Earley parser in Isabelle.
For historical reasons, term antiquotations are called therefore somewhat misleadingly
"Inner Syntax Antiquotations". \<close>
theory
InnerSyntaxAntiquotations