Added invariants - and changes of invariant syntax.
Modified scholarly_paper onto wrt to future concepts of referential semi_formal items (according to discussion with Achim).
This commit is contained in:
parent
4cba4bbdc8
commit
aa4e1acf84
|
@ -34,7 +34,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
||||||
RegExpInterface (* Interface to functional regular automata for monitoring *)
|
RegExpInterface (* Interface to functional regular automata for monitoring *)
|
||||||
Assert
|
Assert
|
||||||
|
|
||||||
keywords "+=" ":=" "accepts" "rejects" "invs"
|
keywords "+=" ":=" "accepts" "rejects" "invariant"
|
||||||
|
|
||||||
and "title*" "subtitle*"
|
and "title*" "subtitle*"
|
||||||
"chapter*" "section*" "subsection*" "subsubsection*"
|
"chapter*" "section*" "subsection*" "subsubsection*"
|
||||||
|
@ -1867,7 +1867,7 @@ val _ =
|
||||||
)
|
)
|
||||||
-- ( Scan.optional (\<^keyword>\<open>rejects\<close> |-- Parse.enum1 "," Parse.term) []
|
-- ( Scan.optional (\<^keyword>\<open>rejects\<close> |-- Parse.enum1 "," Parse.term) []
|
||||||
-- Scan.repeat (\<^keyword>\<open>accepts\<close> |-- Parse.term)
|
-- Scan.repeat (\<^keyword>\<open>accepts\<close> |-- Parse.term)
|
||||||
-- Scan.repeats ((\<^keyword>\<open>invs\<close>) |--
|
-- Scan.repeats ((\<^keyword>\<open>invariant\<close>) |--
|
||||||
Parse.and_list (Args.name_position --| Parse.$$$ "::" -- Parse.term)))
|
Parse.and_list (Args.name_position --| Parse.$$$ "::" -- Parse.term)))
|
||||||
)
|
)
|
||||||
>> (fn (((overloaded, x), (y, z)),((rejectS,accept_rex),invs)) =>
|
>> (fn (((overloaded, x), (y, z)),((rejectS,accept_rex),invs)) =>
|
||||||
|
|
|
@ -93,7 +93,6 @@ definition YY where "YY = na2da(rexp2na example_expression)"
|
||||||
value "NA.accepts (rexp2na example_expression) [0,1,1,0,0,1]"
|
value "NA.accepts (rexp2na example_expression) [0,1,1,0,0,1]"
|
||||||
value "DA.accepts (na2da (rexp2na example_expression)) [0,1,1,0,0,1]"
|
value "DA.accepts (na2da (rexp2na example_expression)) [0,1,1,0,0,1]"
|
||||||
|
|
||||||
|
|
||||||
section\<open>HOL - Adaptions and Export to SML\<close>
|
section\<open>HOL - Adaptions and Export to SML\<close>
|
||||||
|
|
||||||
definition enabled :: "('a,'\<sigma> set)da \<Rightarrow> '\<sigma> set \<Rightarrow> 'a list \<Rightarrow> 'a list"
|
definition enabled :: "('a,'\<sigma> set)da \<Rightarrow> '\<sigma> set \<Rightarrow> 'a list \<Rightarrow> 'a list"
|
||||||
|
|
|
@ -57,8 +57,8 @@ doc_class F =
|
||||||
b :: "(A \<times> C) set" <= "{}" (* This is a relation link, roughly corresponding
|
b :: "(A \<times> C) set" <= "{}" (* This is a relation link, roughly corresponding
|
||||||
to an association class. It can be used to track
|
to an association class. It can be used to track
|
||||||
claims to result - relations, for example.*)
|
claims to result - relations, for example.*)
|
||||||
invs bxxx :: "\<lambda>\<sigma>. r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
|
invariant b :: "\<lambda>\<sigma>. r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
|
||||||
and xxx :: "\<lambda>\<sigma>. properties \<sigma> \<noteq> []"
|
and c :: "\<lambda>\<sigma>. properties \<sigma> \<noteq> []"
|
||||||
|
|
||||||
|
|
||||||
doc_class G = C +
|
doc_class G = C +
|
||||||
|
|
|
@ -156,6 +156,40 @@
|
||||||
|
|
||||||
|
|
||||||
% end: scholarly_paper.abstract
|
% end: scholarly_paper.abstract
|
||||||
|
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
\newisadof{text.scholarly_paper.math_content}%
|
||||||
|
[label=,type=%
|
||||||
|
, 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 =%
|
||||||
|
, 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.math_content.mcc}}{def}}{
|
||||||
|
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||||
|
{\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
|
||||||
|
{\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||||
|
\label{\commandkey{label}} #1
|
||||||
|
\end{definition}}
|
||||||
|
}{%
|
||||||
|
#1%
|
||||||
|
}%
|
||||||
|
\end{isamarkuptext}%
|
||||||
|
}
|
||||||
|
|
||||||
|
% end: scholarly_paper.abstract
|
||||||
|
|
||||||
|
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
\newisadof{text.scholarly_paper.definition}%
|
\newisadof{text.scholarly_paper.definition}%
|
||||||
[label=,type=%
|
[label=,type=%
|
||||||
|
|
|
@ -96,7 +96,6 @@ As Security of the system we define etc...
|
||||||
A formal statement can, but must not have a reference to true formal Isabelle/Isar definition.
|
A formal statement can, but must not have a reference to true formal Isabelle/Isar definition.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
subsection\<open>Technical Content and its Formats\<close>
|
subsection\<open>Technical Content and its Formats\<close>
|
||||||
|
|
||||||
datatype status = semiformal | description
|
datatype status = semiformal | description
|
||||||
|
@ -114,34 +113,60 @@ doc_class technical = text_section +
|
||||||
status :: status <= "description"
|
status :: status <= "description"
|
||||||
formal_results :: "thm list"
|
formal_results :: "thm list"
|
||||||
|
|
||||||
type_synonym tc = technical
|
type_synonym tc = technical (* technical content *)
|
||||||
|
|
||||||
|
|
||||||
subsection\<open>Mathematical Statements\<close>
|
|
||||||
|
|
||||||
datatype math_statement_class =
|
subsection\<open>Mathematical Content\<close>
|
||||||
"definition" | "axiom" | "theorem" | "lemma" | "proposition" | "rule" | "assertion"
|
|
||||||
|
|
||||||
doc_class math_statement = tc +
|
datatype math_content_class =
|
||||||
|
"def" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn"
|
||||||
|
|
||||||
|
text\<open>Instances of the \<open>doc_class\<close> \<^verbatim>\<open>math_content\<close> are by definition @{term "semiformal"}; they may
|
||||||
|
be non-referential, but in this case they will not have a @{term "short_name"}.\<close>
|
||||||
|
|
||||||
|
doc_class math_content = tc +
|
||||||
|
referentiable :: bool <= True
|
||||||
short_name :: string <= "''''"
|
short_name :: string <= "''''"
|
||||||
"class" :: "math_statement_class"
|
status :: status <= "semiformal"
|
||||||
status :: status
|
mcc :: "math_content_class"
|
||||||
|
invariant s1 :: "\<lambda> \<sigma>. \<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
|
||||||
|
invariant s2 :: "\<lambda> \<sigma>. status \<sigma> = semiformal"
|
||||||
|
|
||||||
doc_class math_description = math_statement +
|
text\<open>The intended use for the \<open>doc_class\<close>es \<^verbatim>\<open>math_motivation\<close> (or \<^verbatim>\<open>math_mtv\<close> for short),
|
||||||
referentiable :: bool <= "False"
|
\<^verbatim>\<open>math_explanation\<close> (or \<^verbatim>\<open>math_exp\<close> for short) and
|
||||||
|
\<^verbatim>\<open>math_example\<close> (or \<^verbatim>\<open>math_ex\<close> for short)
|
||||||
|
are \<^emph>\<open>informal\<close> descriptions of semi-formal definitions (by inheritance).\<close>
|
||||||
|
doc_class math_motivation = tc +
|
||||||
|
referentiable :: bool <= False
|
||||||
|
type_synonym math_mtv = math_motivation
|
||||||
|
|
||||||
doc_class math_semi_formal_stmt = math_statement +
|
doc_class math_explanation = tc +
|
||||||
referentiable :: bool <= "True"
|
referentiable :: bool <= False
|
||||||
|
type_synonym math_exp = math_explanation
|
||||||
|
|
||||||
|
doc_class math_example = tc +
|
||||||
|
referentiable :: bool <= False
|
||||||
|
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.
|
||||||
|
They are NOT formal, i.e. Isabelle-checked formal content, but can be in close link to these.\<close>
|
||||||
|
doc_class math_semiformal = math_content +
|
||||||
|
referentiable :: bool <= True
|
||||||
|
type_synonym math_sfc = math_semiformal
|
||||||
|
|
||||||
|
subsection\<open>old style onto model.\<close>
|
||||||
|
|
||||||
text\<open>A rough structuring is modeled as follows:\<close>
|
text\<open>A rough structuring is modeled as follows:\<close>
|
||||||
(* non-evident-statement *)
|
(* non-evident-statement *)
|
||||||
doc_class "definition" = tc +
|
doc_class "definition" = tc +
|
||||||
referentiable :: bool <= "True"
|
referentiable :: bool <= True
|
||||||
tag :: "string" <= "''''"
|
tag :: "string" <= "''''"
|
||||||
|
|
||||||
doc_class "theorem" = tc +
|
doc_class "theorem" = tc +
|
||||||
referentiable :: bool <= "True"
|
referentiable :: bool <= True
|
||||||
tag :: "string" <= "''''"
|
tag :: "string" <= "''''"
|
||||||
|
|
||||||
text\<open>Note that the following two text-elements are currently set to no-keyword in LNCS style.\<close>
|
text\<open>Note that the following two text-elements are currently set to no-keyword in LNCS style.\<close>
|
||||||
|
@ -159,7 +184,7 @@ text\<open> \<^verbatim>\<open>examples\<close> are currently considered \<^verb
|
||||||
via inheritance. \<close>
|
via inheritance. \<close>
|
||||||
|
|
||||||
doc_class example = technical +
|
doc_class example = technical +
|
||||||
referentiable :: bool <= "True"
|
referentiable :: bool <= True
|
||||||
tag :: "string" <= "''''"
|
tag :: "string" <= "''''"
|
||||||
|
|
||||||
subsection\<open>Code Statement Elements\<close>
|
subsection\<open>Code Statement Elements\<close>
|
||||||
|
@ -189,25 +214,28 @@ doc_class "ISAR" = code +
|
||||||
doc_class "LATEX" = code +
|
doc_class "LATEX" = code +
|
||||||
checked :: bool <= "False"
|
checked :: bool <= "False"
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
subsection\<open>Content in Engineering/Tech Papers \<close>
|
subsection\<open>Content in Engineering/Tech Papers \<close>
|
||||||
|
|
||||||
|
|
||||||
doc_class eng_statement = tc +
|
doc_class engineering_statement = tc +
|
||||||
short_name :: string <= "''''"
|
short_name :: string <= "''''"
|
||||||
"class" :: "math_statement_class"
|
|
||||||
status :: status
|
status :: status
|
||||||
|
type_synonym eng_stmt = engineering_statement
|
||||||
|
|
||||||
|
doc_class "experiment" = eng_stmt +
|
||||||
doc_class "experiment" = eng_statement +
|
|
||||||
tag :: "string" <= "''''"
|
tag :: "string" <= "''''"
|
||||||
|
|
||||||
doc_class "evaluation" = eng_statement +
|
doc_class "evaluation" = eng_stmt +
|
||||||
tag :: "string" <= "''''"
|
tag :: "string" <= "''''"
|
||||||
|
|
||||||
doc_class "data" = eng_statement +
|
doc_class "data" = eng_stmt +
|
||||||
tag :: "string" <= "''''"
|
tag :: "string" <= "''''"
|
||||||
|
|
||||||
|
|
||||||
|
subsection\<open>Structuring Enforcement in Engineering/Math Papers \<close>
|
||||||
|
(* todo : could be finer *)
|
||||||
|
|
||||||
text\<open> Besides subtyping, there is another relation between
|
text\<open> Besides subtyping, there is another relation between
|
||||||
doc\_classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
|
doc\_classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
|
||||||
|
|
Loading…
Reference in New Issue