forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF
This commit is contained in:
commit
61d69394c3
|
@ -1,10 +1,29 @@
|
|||
chapter\<open>Inner Syntax Antiquotations (ISA)'s\<close>
|
||||
|
||||
theory InnerSyntaxAntiquotations
|
||||
imports "../../ontologies/Conceptual"
|
||||
begin
|
||||
|
||||
text\<open>Since the syntax chosen for values of doc-class attributes is HOL-syntax --- requiring
|
||||
a fast read on the ``What's in Main''-documentation, but not additional knowledge on, say, SML ---
|
||||
an own syntax for references to types, terms, theorems, etc. are necessary. These are the
|
||||
``Inner Syntax Antiquotations'' since they make only sense \emph{inside} the Inner-Syntax
|
||||
of Isabelle/Isar, so inside the \verb+" ... "+ parenthesis.
|
||||
|
||||
They are the key-mechanism to denote
|
||||
\<^item> Ontological Links, i.e. attributes refering to document classes defined by the ontology
|
||||
\<^item> Ontological F-Links, i.e. attributes referring to formal entities inside Isabelle (such as thm's)
|
||||
|
||||
This file contains a number of examples resulting from the @{theory "Conceptual"} - ontology;
|
||||
the emphasis of this presentation is to present the expressivity of ODL on a paradigmatical example.
|
||||
\<close>
|
||||
|
||||
|
||||
text\<open>Voila the content of the Isabelle_DOF environment so far:\<close>
|
||||
ML\<open> val ({tab = x, ...},y,z)= DOF_core.get_data @{context}; Symtab.dest z; \<close>
|
||||
|
||||
lemma murks : "T = {ert,dfg}" sorry
|
||||
text\<open>Some sample lemma:\<close>
|
||||
lemma murks : "Example" sorry
|
||||
|
||||
text\<open>Example for a meta-attribute of ODL-type @{typ "file"} with an appropriate ISA for the
|
||||
file @{file "./Attributes.thy"}\<close>
|
||||
|
@ -24,9 +43,13 @@ text*[xcv4::F, r="[@{thm ''HOL.refl''},
|
|||
b="{(@{docitem ''xcv1''},@{docitem ''xcv2''})}",
|
||||
s="[@{typ ''int list''}]"]\<open>Lorem ipsum ...\<close>
|
||||
|
||||
text*[xcv5::G, g="@{thm ''HOL.sym''}"]\<open>Lorem ipsum ...\<close>
|
||||
|
||||
text\<open>... and here we add a relation between @{docitem \<open>xcv3\<close>} and @{docitem \<open>xcv2\<close>}
|
||||
into the relation \verb+b+ of @{docitem_ref \<open>xcv4\<close>} \<close>
|
||||
update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv2''})}"]
|
||||
into the relation \verb+b+ of @{docitem_ref \<open>xcv5\<close>}. Note that in the link-relation,
|
||||
a @{typ "C"}-type is required, but a @{typ "G"}-type is offered which is leagal in
|
||||
\verb+Isa_DOF+ because of the sub-class relation between those classes: \<close>
|
||||
update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"]
|
||||
|
||||
text\<open>And here is the result on term level:\<close>
|
||||
ML\<open> @{docitem_attr b::xcv4} \<close>
|
||||
|
|
|
@ -32,7 +32,11 @@ doc_class F =
|
|||
r :: "thm list"
|
||||
u :: "file"
|
||||
s :: "typ list"
|
||||
b :: "(A \<times> C) set" <= "{}"
|
||||
b :: "(A \<times> C) set" <= "{}" (* This is a relation link, roughly corresponding
|
||||
to an association class. It can be used to track
|
||||
claims to result - relations, for example.*)
|
||||
doc_class G = C +
|
||||
g :: "thm" <= "@{thm ''HOL.refl''}"
|
||||
|
||||
doc_class M =
|
||||
trace :: "(A + C + D + F) list"
|
||||
|
|
Loading…
Reference in New Issue