Browse Source

a first imprfect solution for the assert* problem; 4th chapter roughly completed.

master^2
Burkhart Wolff 3 weeks ago
parent
commit
d86e708154
6 changed files with 161 additions and 82 deletions
  1. +2
    -2
      examples/CENELEC_50128/mini_odo/mini_odo.thy
  2. +94
    -49
      examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
  3. +0
    -25
      src/DOF/Isa_COL.thy
  4. +1
    -1
      src/ontologies/Conceptual/Conceptual.thy
  5. +63
    -5
      src/ontologies/scholarly_paper/scholarly_paper.thy
  6. +1
    -0
      src/tests/AssnsLemmaThmEtc.thy

+ 2
- 2
examples/CENELEC_50128/mini_odo/mini_odo.thy View File

@@ -534,14 +534,14 @@ text\<open>

text\<open>Examples for declaration of typed doc-items "assumption" and "hypothesis",
concepts defined in the underlying ontology @{theory "Isabelle_DOF.CENELEC_50128"}. \<close>
text*[ass1::assumption, long_name="Some ''assumption one''"] \<open> The subsystem Y is safe. \<close>
text*[ass2::assumption, long_name="Some ''assumption one''"] \<open> The subsystem Y is safe. \<close>
text*[hyp1::hypothesis] \<open> P not equal NP \<close>
text\<open>A real example fragment from a larger project, declaring a text-element as a
"safety-related application condition", a concept defined in the
@{theory "Isabelle_DOF.CENELEC_50128"} ontology:\<close>

text*[hyp2::hypothesis]\<open>Under the assumption @{assumption \<open>ass1\<close>} we establish the following: ... \<close>
text*[hyp2::hypothesis]\<open>Under the assumption @{assumption \<open>ass2\<close>} we establish the following: ... \<close>

text*[ass122::SRAC, long_name="Some ''ass122''"] \<open> The overall sampling frequence of the odometer
subsystem is therefore 14 khz, which includes sampling, computing and


+ 94
- 49
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy View File

@@ -16,7 +16,7 @@ theory
"04_RefMan"
imports
"03_GuidedTour"
"Isabelle_DOF.Isa_COL"
"Isabelle_DOF.technical_report"
begin

declare_reference*[infrastructure::technical]
@@ -539,6 +539,8 @@ It extends \<^verbatim>\<open>COL\<close> by the following concepts:
.5 scholarly\_paper.corollary\DTcomment{Freeform}.
.5 scholarly\_paper.math\_example\DTcomment{Freeform}.
.5 scholarly\_paper.math\_semiformal\DTcomment{Freeform}.
.5 scholarly\_paper.math\_formal\DTcomment{Formal(=Checked) Content}.
.6 scholarly\_paper.assertion\DTcomment{Assertions}.
.4 scholarly\_paper.tech\_example\DTcomment{...}.
.4 scholarly\_paper.math\_motivation\DTcomment{...}.
.4 scholarly\_paper.math\_explanation\DTcomment{...}.
@@ -554,6 +556,8 @@ It extends \<^verbatim>\<open>COL\<close> by the following concepts:
\end{minipage}
\end{center}

TODO: There are some slight problems in the hierarchy ...

\<close>

text\<open>A pivotal abstract class in the hierarchy is:
@@ -599,6 +603,7 @@ of the \<^isadof> language:
\<newline>
'[' meta_args ']' '\<open>' text '\<close>'
)
| @@{command "assert*"} '[' meta_args ']' '\<open>' term '\<close>'
\<close>
\<close>

@@ -613,6 +618,11 @@ of @{typ \<open>math_content\<close>} might be introduced in a derived ontology
definition.
\<close>

text\<open>While this library is intended to give a lot of space to freeform text elements in
order to counterbalance Isabelle's standard view, it should not be forgot that the real strength
of Isabelle is its ability to handle both - and to establish links between both worlds.
Therefore the formal assertion command has been integrated to capture some form of formal content.\<close>


subsubsection*["text-elements-expls"::example]\<open>Examples\<close>

@@ -634,6 +644,21 @@ text\<open>

\<close>

text\<open>Assertions allow for logical statements to be checked in the global context).
This is particularly useful to explore formal definitions wrt. to their border cases. \<close>

assert*[ass1::assertion, short_name = "\<open>This is an assertion\<close>"] \<open>last [3] < (4::int)\<close>

text\<open>We want to check the consequences of this definition and can add the following statements:
@{boxed_theory_text [display]\<open>
text*[claim::assertion]\<open>For non-empty lists, our definition yields indeed
the last element of a list.\<close>
assert*[claim1::assertion] "last[4::int] = 4"
assert*[claim2::assertion] "last[1,2,3,4::int] = 4"
\<close>}
\<close>


text\<open>
As mentioned before, the command macros of \<^theory_text>\<open>Definition*\<close>, \<^theory_text>\<open>Lemma*\<close> and \<^theory_text>\<open>Theorem*\<close>
set the default class to the super-class of @{typ \<open>definition\<close>}.
@@ -653,33 +678,17 @@ which allows the above example be shortened to:
\<close>}
\<close>


subsection\<open>ASSERTIONS : NEED TO BE INTEGRATED. TODO.\<close>

text\<open>
Similarly, we provide "minimal" instances of the \<^boxed_theory_text>\<open>ASSERTION_ALIKES\<close>
and \<^boxed_theory_text>\<open>FORMAL_STATEMENT_ALIKE\<close> shadow classes:
@{boxed_theory_text [display]\<open>
doc_class assertions =
properties :: "term list"
doc_class "thms" =
properties :: "thm list"
\<close>}

\<close>


subsection\<open>The Ontology \<^theory>\<open>Isabelle_DOF.technical_report\<close>\<close>
(*<*)
ML\<open>val toLaTeX = String.translate (fn c => if c = #"_" then "\\_" else String.implode[c])\<close>
ML\<open>writeln (DOF_core.print_doc_class_tree
@{context} (fn (n,l) => String.isPrefix "technical_report" l
orelse String.isPrefix "Isa_COL" l)
@{context} (fn (n,l) => true (* String.isPrefix "technical_report" l
orelse String.isPrefix "Isa_COL" l *))
toLaTeX)\<close>
(*>*)
text\<open> The \<^verbatim>\<open>technical_report\<close> ontology extends \<^verbatim>\<open>scholarly_paper\<close> by concepts needed
for larger reports in the domain of mathematics and engineering.
for larger reports in the domain of mathematics and engineering. The concepts are fairly
high-level arranged at root-class level,

%
\begin{center}
@@ -688,6 +697,12 @@ for larger reports in the domain of mathematics and engineering.
.0 .
.1 technical\_report.front\_matter\DTcomment{...}.
.1 technical\_report.table\_of\_contents\DTcomment{...}.
.1 Isa\_COL.text\_element\DTcomment{...}.
.2 scholarly\_paper.text\_section\DTcomment{...}.
.4 technical\_report.code\DTcomment{...}.
.5 technical\_report.SML\DTcomment{...}.
.5 technical\_report.ISAR\DTcomment{...}.
.5 technical\_report.LATEX\DTcomment{...}.
.1 technical\_report.index\DTcomment{...}.
.1 ...
.1 technical\_report.report\DTcomment{...}.
@@ -698,10 +713,67 @@ for larger reports in the domain of mathematics and engineering.


subsection\<open>A Domain-Specific Ontology: \<^theory>\<open>Isabelle_DOF.CENELEC_50128\<close>\<close>
(*<*)
ML\<open>val toLaTeX = String.translate (fn c => if c = #"_" then "\\_" else String.implode[c])\<close>
ML\<open>writeln (DOF_core.print_doc_class_tree
@{context} (fn (n,l) => true (* String.isPrefix "technical_report" l
orelse String.isPrefix "Isa_COL" l *))
toLaTeX)\<close>
(*>*)
text\<open> The \<^verbatim>\<open>CENELEC_50128\<close> is qn exqmple of q domqin-specific ontology. It
is based on \<^verbatim>\<open>technical_report\<close> since we assume that this kind of format will be most
appropriate for this type of long-and-tedious documents,

%
\begin{center}
\begin{minipage}{.9\textwidth}
\dirtree{%
.0 .
.1 CENELEC\_50128.judgement\DTcomment{...}.
.1 CENELEC\_50128.test\_item\DTcomment{...}.
.2 CENELEC\_50128.test\_case\DTcomment{...}.
.2 CENELEC\_50128.test\_tool\DTcomment{...}.
.2 CENELEC\_50128.test\_result\DTcomment{...}.
.2 CENELEC\_50128.test\_adm\_role\DTcomment{...}.
.2 CENELEC\_50128.test\_environment\DTcomment{...}.
.2 CENELEC\_50128.test\_requirement\DTcomment{...}.
.2 CENELEC\_50128.test\_specification\DTcomment{...}.
.1 CENELEC\_50128.objectives\DTcomment{...}.
.1 CENELEC\_50128.design\_item\DTcomment{...}.
.2 CENELEC\_50128.interface\DTcomment{...}.
.1 CENELEC\_50128.sub\_requirement\DTcomment{...}.
.1 CENELEC\_50128.test\_documentation\DTcomment{...}.
.1 Isa\_COL.text\_element\DTcomment{...}.
.2 CENELEC\_50128.requirement\DTcomment{...}.
.3 CENELEC\_50128.AC\DTcomment{...}.
.4 CENELEC\_50128.EC\DTcomment{...}.
.5 CENELEC\_50128.SRAC\DTcomment{...}.
.3 CENELEC\_50128.TC\DTcomment{...}.
.3 CENELEC\_50128.FnI\DTcomment{...}.
.3 CENELEC\_50128.SIR\DTcomment{...}.
.3 CENELEC\_50128.CoAS\DTcomment{...}.
.3 CENELEC\_50128.HtbC\DTcomment{...}.
.3 CENELEC\_50128.SILA\DTcomment{...}.
.3 CENELEC\_50128.assumption\DTcomment{...}.
.3 CENELEC\_50128.hypothesis\DTcomment{...}.
.4 CENELEC\_50128.security\_hyp\DTcomment{...}.
.3 CENELEC\_50128.safety\_requirement\DTcomment{...}.
.2 CENELEC\_50128.cenelec\_text\DTcomment{...}.
.3 CENELEC\_50128.SWAS\DTcomment{...}.
.3 [...].
.2 scholarly\_paper.text\_section\DTcomment{...}.
.3 scholarly\_paper.technical\DTcomment{...}.
.4 scholarly\_paper.math\_content\DTcomment{...}.
.5 CENELEC\_50128.semi\_formal\_content\DTcomment{...}.
.1 ...
}
\end{minipage}
\end{center}
\<close>

(* TODO : Rearrange ontology hierarchies. *)

subsubsection\<open>Example: Text Elemens with Levels\<close>
subsubsection\<open>Examples\<close>
text\<open>
The category ``exported constraint (EC)'' is, in the file
\<^file>\<open>../../../src/ontologies/CENELEC_50128/CENELEC_50128.thy\<close> defined as follows:
@@ -757,33 +829,6 @@ can now be defined as follows:
\end{ltx}
\<close>

subsubsection\<open>Example: Assertions\<close>
text\<open>Assertions are a common feature to validate properties of models, presented as a collection
of Isabelle/HOL definitions. They are particularly relevant for highlighting corner cases of a
formal model. For example, assume a definition: \<close>

definition last :: "'a list \<Rightarrow> 'a" where "last S = hd(rev S)"

(* Old stuff using abstract classes.
(*<*)
text*[claim::assertions]\<open>For non-empty lists, our definition yields indeed the last element of a list.\<close>
assert*[claim::assertions] "last[4::int] = 4"
assert*[claim::assertions] "last[1,2,3,4::int] = 4"
(*>*)
*)
text\<open>We want to check the consequences of this definition and can add the following statements:
@{boxed_theory_text [display]\<open>
text*[claim::assertions]\<open>For non-empty lists, our definition yields indeed
the last element of a list.\<close>
assert*[claim1::assertions] "last[4::int] = 4"
assert*[claim2::assertions] "last[1,2,3,4::int] = 4"
\<close>}
\<close>

text\<open>As an \<^boxed_theory_text>\<open>ASSERTION_ALIKES\<close>, the \<^boxed_theory_text>\<open>assertions\<close> class possesses a
\<^boxed_theory_text>\<open>properties\<close> attribute. The \<^boxed_theory_text>\<open>assert*\<close> command evaluates its argument;
in case it evaluates to true the property is added to the property list of the \<^boxed_theory_text>\<open>claim\<close> -
text-element. Commands like \<^boxed_theory_text>\<open>Definitions*\<close> or \<^boxed_theory_text>\<open>Theorem*\<close> work analogously.\<close>


subsubsection\<open>For Isabelle Hackers: Defining New Top-Level Commands\<close>


+ 0
- 25
src/DOF/Isa_COL.thy View File

@@ -28,7 +28,6 @@ theory Isa_COL
"subsection*" "subsubsection*"
"paragraph*" "subparagraph*"
"figure*" "side_by_side_figure*" :: document_body
and "assert*" :: thy_decl

begin
@@ -120,30 +119,6 @@ fun enriched_document_cmd_exp ncid (S: (string * string) list) =
end;
end (* local *)

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
{is_monitor = false} {is_inline = 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 @{command_keyword "assert*"}
"evaluate and print term"
(attributes -- opt_evaluator -- opt_modes -- Parse.term >> assertion_cmd');


val _ =
Outer_Syntax.command ("title*", @{here}) "section heading"


+ 1
- 1
src/ontologies/Conceptual/Conceptual.thy View File

@@ -49,7 +49,7 @@ doc_class E = D +



doc_class F =
doc_class F =
properties :: "term list"
r :: "thm list"
u :: "file"


+ 63
- 5
src/ontologies/scholarly_paper/scholarly_paper.thy View File

@@ -11,12 +11,13 @@
* SPDX-License-Identifier: BSD-2-Clause
*************************************************************************)

section\<open>An example ontology for a scholarly paper\<close>
section\<open>An example ontology for scientific, MINT-oriented papers.\<close>

theory scholarly_paper
imports "../../DOF/Isa_COL"
keywords "author*" "abstract*"
"Definition*" "Lemma*" "Theorem*" :: document_body
and "assert*" :: thy_decl


begin
@@ -123,7 +124,7 @@ A formal statement can, but must not have a reference to true formal Isabelle/Is

subsection\<open>Technical Content and its Formats\<close>

datatype status = semiformal | description
datatype status = formal | semiformal | description

text\<open>The class \<^verbatim>\<open>technical\<close> regroups a number of text-elements that contain typical
"technical content" in mathematical or engineering papers: definitions, theorems, lemmas, examples. \<close>
@@ -154,7 +155,7 @@ doc_class example = text_section +
short_name :: string <= "''''"


subsection\<open>Mathematical Content\<close>
subsection\<open>Freeform Mathematical Content\<close>

text\<open>We follow in our enumeration referentiable mathematical content class the AMS style and its
provided \<^emph>\<open>theorem environments\<close> (see \<^verbatim>\<open>texdoc amslatex\<close>). We add, however, the concepts
@@ -258,7 +259,7 @@ doc_class "math_example" = math_content +
invariant d5 :: "\<lambda> \<sigma>::math_example. mcc \<sigma> = expl"


subsection\<open>Ontological Macros \<^verbatim>\<open>Definition*\<close> , \<^verbatim>\<open>Lemma**\<close>, \<^verbatim>\<open>Theorem*\<close> ... \<close>
subsubsection\<open>Ontological Macros \<^verbatim>\<open>Definition*\<close> , \<^verbatim>\<open>Lemma**\<close>, \<^verbatim>\<open>Theorem*\<close> ... \<close>

text\<open>These ontological macros allow notations are defined for the class
\<^typ>\<open>math_content\<close> in order to allow for a variety of free-form formats;
@@ -334,6 +335,62 @@ val _ = let fun use_Theorem_default thy =
end
\<close>


subsection\<open>Formal Mathematical Content\<close>
text\<open>While this library is intended to give a lot of space to freeform text elements in
order to counterbalance Isabelle's standard view, it should not be forgot that the real strength
of Isabelle is its ability to handle both - and to establish links between both worlds. Therefore:\<close>

doc_class math_formal = math_content +
referentiable :: bool <= False
status :: status <= "formal"
properties :: "term list"
type_synonym math_fc = math_formal

doc_class assertion = math_formal +
referentiable :: bool <= True (* No support in Backend yet. *)
status :: status <= "formal"
properties :: "term list"


ML\<open>
(* TODO : Rework this code and make it closer to Definition*. There is still
a rest of "abstract classes in it: any class possessing a properties attribute
is admissible to this command, not just ... *)
local open ODL_Command_Parser in

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
{is_monitor = false} {is_inline = 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 attributes = attributes (* re-export *)

end
val _ =
Outer_Syntax.command @{command_keyword "assert*"}
"evaluate and print term"
(attributes -- opt_evaluator -- opt_modes -- Parse.term >> assertion_cmd');

\<close>

subsubsection*[ex_ass::example]\<open>Example\<close>
text\<open>Assertions allow for logical statements to be checked in the global context). \<close>
assert*[ass1::assertion, short_name = "\<open>This is an assertion\<close>"] \<open>(3::int) < 4\<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
@@ -347,7 +404,8 @@ doc_class tech_example = technical +


subsection\<open>Content in Engineering/Tech Papers \<close>

text\<open>This section is currently experimental and not supported by the documentation
generation backend.\<close>

doc_class engineering_content = tc +
short_name :: string <= "''''"


+ 1
- 0
src/tests/AssnsLemmaThmEtc.thy View File

@@ -16,6 +16,7 @@ theory
imports
"Isabelle_DOF.Conceptual"
"Isabelle_DOF.math_paper"
"Isabelle_DOF.scholarly_paper" (* for assert notation *)
begin

section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>


Loading…
Cancel
Save