Eliminated deprecated abstract class residuals; lifted Definition* to math_content.
This commit is contained in:
parent
2ecb62a80e
commit
efeee1e863
|
@ -996,8 +996,7 @@ restrictions on the structure of components. None of our paradigmatic examples c
|
||||||
be automatically proven with any of the discussed SMT techniques without restrictions.
|
be automatically proven with any of the discussed SMT techniques without restrictions.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
section*["conclusion"::conclusion,main_author="Some(@{docitem ''bu''}::author)"]
|
section*["conclusion"::conclusion,main_author="Some(@{docitem ''bu''}::author)"]\<open>Conclusion\<close>
|
||||||
\<open>Conclusion\<close>
|
|
||||||
text\<open>We presented a formalisation of the most comprehensive semantic model for \<^csp>, a 'classical'
|
text\<open>We presented a formalisation of the most comprehensive semantic model for \<^csp>, a 'classical'
|
||||||
language for the specification and analysis of concurrent systems studied in a rich body of
|
language for the specification and analysis of concurrent systems studied in a rich body of
|
||||||
literature. For this purpose, we ported @{cite "tej.ea:corrected:1997"} to a modern version
|
literature. For this purpose, we ported @{cite "tej.ea:corrected:1997"} to a modern version
|
||||||
|
|
|
@ -487,11 +487,13 @@ formal model. For example, assume a definition: \<close>
|
||||||
|
|
||||||
definition last :: "'a list \<Rightarrow> 'a" where "last S = hd(rev S)"
|
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>
|
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[4::int] = 4"
|
||||||
assert*[claim::assertions] "last[1,2,3,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:
|
text\<open>We want to check the consequences of this definition and can add the following statements:
|
||||||
@{boxed_theory_text [display]\<open>
|
@{boxed_theory_text [display]\<open>
|
||||||
text*[claim::assertions]\<open>For non-empty lists, our definition yields indeed
|
text*[claim::assertions]\<open>For non-empty lists, our definition yields indeed
|
||||||
|
|
|
@ -97,10 +97,10 @@ fun transform_cid thy NONE X = X
|
||||||
val sub_cid_long = DOF_core.read_cid_global thy sub_cid
|
val sub_cid_long = DOF_core.read_cid_global thy sub_cid
|
||||||
in if DOF_core.is_subclass_global thy sub_cid_long cid_long
|
in if DOF_core.is_subclass_global thy sub_cid_long cid_long
|
||||||
then (SOME (sub_cid,pos))
|
then (SOME (sub_cid,pos))
|
||||||
else (SOME (sub_cid,pos))
|
else (* (SOME (sub_cid,pos)) *)
|
||||||
(* BUG : check reveals problem of Definition* misuse.
|
(* BUG : check reveals problem of Definition* misuse. *)
|
||||||
error("class "^sub_cid_long^
|
error("class "^sub_cid_long^
|
||||||
" must be sub-class of "^cid_long) *)
|
" must be sub-class of "^cid_long)
|
||||||
end
|
end
|
||||||
in
|
in
|
||||||
|
|
||||||
|
@ -427,28 +427,4 @@ ML\<open>@{term "side_by_side_figure"};
|
||||||
DOF_core.SPY;\<close>
|
DOF_core.SPY;\<close>
|
||||||
|
|
||||||
|
|
||||||
section\<open>DEPRECATED : An attempt to model Standard Isabelle Formal Content\<close>
|
|
||||||
|
|
||||||
doc_class assertions =
|
|
||||||
properties :: "term list"
|
|
||||||
|
|
||||||
doc_class "thms" =
|
|
||||||
properties :: "thm list"
|
|
||||||
|
|
||||||
doc_class formal_item =
|
|
||||||
item :: "(assertions + thms)"
|
|
||||||
|
|
||||||
doc_class definitions =
|
|
||||||
requires :: "formal_item list"
|
|
||||||
establishes :: "thms list"
|
|
||||||
|
|
||||||
doc_class formal_content =
|
|
||||||
style :: "string option"
|
|
||||||
accepts "\<lbrace>formal_item\<rbrace>\<^sup>+"
|
|
||||||
|
|
||||||
doc_class concept =
|
|
||||||
tag :: "string" <= "''''"
|
|
||||||
properties :: "thm list" <= "[]"
|
|
||||||
|
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
@ -44,6 +44,7 @@ text\<open> Excerpt of the BE EN 50128:2011, page 22. \<close>
|
||||||
|
|
||||||
section\<open>Terms and Definitions\<close>
|
section\<open>Terms and Definitions\<close>
|
||||||
|
|
||||||
|
typ "sfc"
|
||||||
Definition*[assessment::sfc,short_name="''assessment''"]
|
Definition*[assessment::sfc,short_name="''assessment''"]
|
||||||
\<open>process of analysis to determine whether software, which may include
|
\<open>process of analysis to determine whether software, which may include
|
||||||
process, documentation, system, subsystem hardware and/or software components, meets the specified
|
process, documentation, system, subsystem hardware and/or software components, meets the specified
|
||||||
|
@ -68,6 +69,7 @@ criteria:
|
||||||
configuration management system or is a part of a collection of components
|
configuration management system or is a part of a collection of components
|
||||||
(e. g. subsystems) which have an independent version
|
(e. g. subsystems) which have an independent version
|
||||||
\<close>
|
\<close>
|
||||||
|
typ "sfc"
|
||||||
|
|
||||||
Definition*[CMGR::sfc, short_name="''configuration manager''"]
|
Definition*[CMGR::sfc, short_name="''configuration manager''"]
|
||||||
\<open>entity that is responsible for implementing and carrying out the processes
|
\<open>entity that is responsible for implementing and carrying out the processes
|
||||||
|
|
|
@ -257,7 +257,7 @@ val _ =
|
||||||
Outer_Syntax.command ("Definition*", @{here}) "Textual Definition"
|
Outer_Syntax.command ("Definition*", @{here}) "Textual Definition"
|
||||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||||
>> (Toplevel.theory o (Onto_Macros.enriched_formal_statement_command
|
>> (Toplevel.theory o (Onto_Macros.enriched_formal_statement_command
|
||||||
(SOME "definition")
|
(SOME "math_content") (* should be (SOME "definition") *)
|
||||||
[("mcc","defn")]
|
[("mcc","defn")]
|
||||||
{markdown = true} )));
|
{markdown = true} )));
|
||||||
|
|
||||||
|
|
|
@ -14,7 +14,7 @@
|
||||||
chapter\<open>Term Antiquotations\<close>
|
chapter\<open>Term Antiquotations\<close>
|
||||||
|
|
||||||
text\<open>Terms are represented by "Inner Syntax" parsed by an Earley parser in Isabelle.
|
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
|
For historical reasons, \<^emph>\<open>term antiquotations\<close> are called therefore somewhat misleadingly
|
||||||
"Inner Syntax Antiquotations". \<close>
|
"Inner Syntax Antiquotations". \<close>
|
||||||
|
|
||||||
theory
|
theory
|
||||||
|
|
Loading…
Reference in New Issue