2023-03-21 13:33:21 +00:00
|
|
|
(*************************************************************************
|
|
|
|
* Copyright (C)
|
|
|
|
* 2019-2023 The University of Exeter
|
|
|
|
* 2018-2023 The University of Paris-Saclay
|
|
|
|
* 2018 The University of Sheffield
|
|
|
|
*
|
|
|
|
* License:
|
|
|
|
* This program can be redistributed and/or modified under the terms
|
|
|
|
* of the 2-clause BSD-style license.
|
|
|
|
*
|
|
|
|
* SPDX-License-Identifier: BSD-2-Clause
|
|
|
|
*************************************************************************)
|
|
|
|
|
|
|
|
chapter\<open>Term-Antiquotation Expansions and Evaluation\<close>
|
2021-10-20 07:10:11 +00:00
|
|
|
|
|
|
|
theory
|
2023-03-24 07:28:14 +00:00
|
|
|
Concept_TermEvaluation
|
2021-10-20 07:10:11 +00:00
|
|
|
imports
|
2023-03-21 13:33:21 +00:00
|
|
|
"Isabelle_DOF-Unit-Tests.Concept_TermAntiquotations"
|
2023-03-06 15:53:57 +00:00
|
|
|
"Isabelle_DOF-Unit-Tests.Concept_High_Level_Invariants"
|
|
|
|
TestKit
|
2023-03-21 13:33:21 +00:00
|
|
|
begin
|
|
|
|
|
|
|
|
section\<open>Test Purpose.\<close>
|
|
|
|
text\<open> Creation of ontological instances along the \<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close>
|
|
|
|
Ontology. Emphasis is put on type-safe (ontologically consistent) referencing of text, code and
|
|
|
|
proof elements. Some tests cover also the critical cases concerning name spaces of oid's. \<close>
|
2021-10-20 07:10:11 +00:00
|
|
|
|
2023-03-20 15:50:23 +00:00
|
|
|
|
2022-03-14 11:23:54 +00:00
|
|
|
section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close>
|
2023-05-15 15:55:52 +00:00
|
|
|
(*<*)
|
2023-02-22 09:52:05 +00:00
|
|
|
ML*[thefunction::B,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1);
|
|
|
|
val t = \<^value_>\<open>x @{B \<open>thefunction\<close>}\<close>\<close>
|
2022-03-16 12:25:56 +00:00
|
|
|
ML\<open>fac 5; t\<close> \<comment> \<open>this is a test that ML* is actually evaluated and the
|
|
|
|
resulting toplevel state is preserved.\<close>
|
2023-03-20 15:50:23 +00:00
|
|
|
text*[the::C]\<open> @{B "thefunction"} \<close>
|
|
|
|
text\<open>... and here we reference @{B \<open>thefunction\<close>}.\<close>
|
2023-05-15 15:55:52 +00:00
|
|
|
(*>*)
|
2022-03-14 11:23:54 +00:00
|
|
|
|
2022-03-30 15:54:02 +00:00
|
|
|
|
2022-03-14 11:23:54 +00:00
|
|
|
|
2023-03-24 07:08:55 +00:00
|
|
|
section\<open>Term-Annotation and its Evaluation\<close>
|
2022-03-14 11:23:54 +00:00
|
|
|
|
2023-03-21 13:33:21 +00:00
|
|
|
text\<open>Term Annotation Antiquotations (TA) can be evaluated with the help of the value* command.\<close>
|
|
|
|
|
2021-10-20 07:10:11 +00:00
|
|
|
text\<open>The value* command uses the same code as the value command
|
|
|
|
and adds the possibility to evaluate Term Annotation Antiquotations (TA).
|
|
|
|
For that an elaboration of the term referenced by a TA must be done before
|
|
|
|
passing it to the evaluator.
|
2021-11-04 14:10:02 +00:00
|
|
|
The current implementation is based on referential equality, syntactically, and
|
|
|
|
with the help of HOL, on referential equivalence, semantically:
|
|
|
|
Some built-ins remain as unspecified constants:
|
|
|
|
\<^item> the docitem TA offers a way to check the reference of class instances
|
|
|
|
without checking the instances type.
|
|
|
|
It must be avoided for certification
|
2021-12-09 08:57:21 +00:00
|
|
|
|
|
|
|
We also have the possibility to make some requests on classes instances, i.e. on docitems
|
2023-02-22 09:52:05 +00:00
|
|
|
by specifying the doc class.
|
2021-12-09 08:57:21 +00:00
|
|
|
The TA denotes the HOL list of the values of the instances.
|
|
|
|
The value of an instance is the record of every attributes of the instance.
|
|
|
|
This way, we can use the usual functions on lists to make our request.
|
|
|
|
|
2021-10-20 07:10:11 +00:00
|
|
|
The emphasis of this presentation is to present the evaluation possibilities and limitations
|
|
|
|
of the current implementation.
|
|
|
|
\<close>
|
|
|
|
|
2021-12-09 08:57:21 +00:00
|
|
|
section\<open>Term Annotation evaluation\<close>
|
2023-05-15 15:55:52 +00:00
|
|
|
(*<*)
|
2021-10-20 07:10:11 +00:00
|
|
|
text\<open>We can validate a term with TA:\<close>
|
2022-03-31 04:57:18 +00:00
|
|
|
term*[axx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close>
|
|
|
|
|
2023-03-06 15:13:22 +00:00
|
|
|
text\<open>check : @{A "axx"}\<close>
|
2021-10-20 07:10:11 +00:00
|
|
|
|
|
|
|
text\<open>Now we can evaluate a term with TA:
|
|
|
|
the current implementation return the term which references the object referenced by the TA.
|
|
|
|
Here the evualuation of the TA will return the HOL.String which references the theorem:
|
|
|
|
\<close>
|
2022-03-31 08:12:46 +00:00
|
|
|
value*\<open>@{thm \<open>HOL.refl\<close>}\<close> \<comment> \<open>syntax check\<close>
|
2021-10-20 07:10:11 +00:00
|
|
|
|
2022-03-31 08:12:46 +00:00
|
|
|
value*[axxx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> \<comment> \<open>defining a reference of class A\<close>
|
2022-03-30 15:54:02 +00:00
|
|
|
|
2023-03-06 15:13:22 +00:00
|
|
|
text\<open>check : @{A "axxx"}\<close> \<comment> \<open>using it\<close>
|
2023-05-15 15:55:52 +00:00
|
|
|
(*>*)
|
2021-10-20 07:10:11 +00:00
|
|
|
text\<open>An instance class is an object which allows us to define the concepts we want in an ontology.
|
|
|
|
It is a concept which will be used to implement an ontology. It has roughly the same meaning as
|
|
|
|
an individual in an OWL ontology.
|
|
|
|
The validation process will check that the instance class @{docitem \<open>xcv1\<close>} is indeed
|
|
|
|
an instance of the class @{doc_class A}:
|
|
|
|
\<close>
|
|
|
|
term*\<open>@{A \<open>xcv1\<close>}\<close>
|
|
|
|
|
2023-03-24 07:08:55 +00:00
|
|
|
text\<open>The instance class @{docitem \<open>xcv1\<close>} is not an instance of the class @{doc_class B}:\<close>
|
|
|
|
value-assert-error\<open>@{B \<open>xcv1\<close>}\<close>\<open>xcv1 is not an instance of Conceptual.B\<close>
|
|
|
|
|
2021-10-20 07:10:11 +00:00
|
|
|
text\<open>We can evaluate the instance class. The current implementation returns
|
2023-03-24 07:08:55 +00:00
|
|
|
the value of the instance, i.e. a collection of every attribute of the instance: \<close>
|
2021-10-20 07:10:11 +00:00
|
|
|
value*\<open>@{A \<open>xcv1\<close>}\<close>
|
|
|
|
|
|
|
|
text\<open>We can also get the value of an attribute of the instance:\<close>
|
|
|
|
value*\<open>A.x @{A \<open>xcv1\<close>}\<close>
|
|
|
|
|
|
|
|
text\<open>If the attribute of the instance is not initialized, we get an undefined value,
|
|
|
|
whose type is the type of the attribute:\<close>
|
2022-03-30 05:54:38 +00:00
|
|
|
term*\<open>B.level @{C \<open>xcv2\<close>}\<close>
|
|
|
|
value*\<open>B.level @{C \<open>xcv2\<close>}\<close>
|
2021-10-20 07:10:11 +00:00
|
|
|
|
|
|
|
text\<open>The value of a TA is the term itself:\<close>
|
|
|
|
term*\<open>C.g @{C \<open>xcv2\<close>}\<close>
|
|
|
|
value*\<open>C.g @{C \<open>xcv2\<close>}\<close>
|
|
|
|
|
|
|
|
text\<open>Some terms can be validated, i.e. the term will be checked,
|
2021-11-04 14:10:02 +00:00
|
|
|
and the existence of every object referenced by a TA will be checked,
|
|
|
|
and can be evaluated by using referential equivalence.
|
2021-10-20 07:10:11 +00:00
|
|
|
The existence of the instance @{docitem \<open>xcv4\<close>} can be validated,
|
2023-02-22 09:52:05 +00:00
|
|
|
and the fact that it is an instance of the class @{doc_class F} will be checked:\<close>
|
2021-10-20 07:10:11 +00:00
|
|
|
term*\<open>@{F \<open>xcv4\<close>}\<close>
|
|
|
|
|
2021-11-04 14:10:02 +00:00
|
|
|
text\<open>We can also evaluate the instance @{docitem \<open>xcv4\<close>}.
|
2021-10-20 07:10:11 +00:00
|
|
|
The attribute \<open>b\<close> of the instance @{docitem \<open>xcv4\<close>} is of type @{typ "(A \<times> C) set"}
|
2021-11-04 14:10:02 +00:00
|
|
|
but the instance @{docitem \<open>xcv4\<close>} initializes the attribute by using the \<open>docitem\<close> TA.
|
|
|
|
Then the instance can be evaluate but only the references of the classes of the set
|
2023-03-24 07:08:55 +00:00
|
|
|
used in the \<open>b\<close> attribute will be checked, and the type of these classes will not:\<close>
|
2021-11-04 14:10:02 +00:00
|
|
|
value* \<open>@{F \<open>xcv4\<close>}\<close>
|
|
|
|
|
2023-03-20 15:50:23 +00:00
|
|
|
|
2021-11-04 14:10:02 +00:00
|
|
|
text\<open>If we want the classes to be checked,
|
|
|
|
we can use the TA which will also check the type of the instances.
|
2023-03-24 07:08:55 +00:00
|
|
|
The instance @{A \<open>xcv3\<close>} is of type @{typ "A"} and the instance @{C \<open>xcv2\<close>} is of type @{typ "C"}:\<close>
|
2021-11-04 14:10:02 +00:00
|
|
|
update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{C ''xcv2''})}"]
|
2023-03-20 15:50:23 +00:00
|
|
|
|
2021-11-04 14:10:02 +00:00
|
|
|
text\<open>Using a TA in terms is possible, and the term is evaluated:\<close>
|
|
|
|
value*\<open>[@{thm \<open>HOL.refl\<close>}, @{thm \<open>HOL.refl\<close>}]\<close>
|
|
|
|
value*\<open>@{thm ''HOL.refl''} = @{thm (''HOL.refl'')}\<close>
|
|
|
|
|
2023-03-24 07:08:55 +00:00
|
|
|
ML\<open>@{thm "refl"}\<close>
|
2021-11-04 14:10:02 +00:00
|
|
|
|
2021-12-09 08:57:21 +00:00
|
|
|
section\<open>Request on instances\<close>
|
|
|
|
|
|
|
|
text\<open>We define a new class Z:\<close>
|
|
|
|
doc_class Z =
|
|
|
|
z::"int"
|
|
|
|
|
|
|
|
text\<open>And some instances:\<close>
|
|
|
|
text*[test1Z::Z, z=1]\<open>lorem ipsum...\<close>
|
|
|
|
text*[test2Z::Z, z=4]\<open>lorem ipsum...\<close>
|
|
|
|
text*[test3Z::Z, z=3]\<open>lorem ipsum...\<close>
|
|
|
|
|
|
|
|
text\<open>We want to get all the instances of the @{doc_class Z}:\<close>
|
|
|
|
value*\<open>@{Z-instances}\<close>
|
|
|
|
|
|
|
|
text\<open>Now we want to get the instances of the @{doc_class Z} whose attribute z > 2:\<close>
|
|
|
|
value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z-instances}\<close>
|
|
|
|
|
|
|
|
text\<open>We can check that we have the list of instances we wanted:\<close>
|
|
|
|
value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z-instances} = [@{Z \<open>test3Z\<close>}, @{Z \<open>test2Z\<close>}]
|
|
|
|
\<or> filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z-instances} = [@{Z \<open>test2Z\<close>}, @{Z \<open>test3Z\<close>}]\<close>
|
|
|
|
|
|
|
|
text\<open>Now, we want to get all the instances of the @{doc_class A}\<close>
|
|
|
|
value*\<open>@{A-instances}\<close>
|
|
|
|
|
2023-05-15 15:55:52 +00:00
|
|
|
(*<*)
|
2021-12-09 08:57:21 +00:00
|
|
|
text\<open>Warning: If you make a request on attributes that are undefined in some instances,
|
|
|
|
you will get a result which includes these unresolved cases.
|
|
|
|
In the following example, we request the instances of the @{doc_class A}.
|
2023-03-04 08:57:14 +00:00
|
|
|
But we have defined an instance @{docitem \<open>sdf\<close>} in theory @{theory "Isabelle_DOF-Ontologies.Conceptual"}
|
2021-12-09 08:57:21 +00:00
|
|
|
whose our theory inherits from, and this docitem instance does not initialize its attribute \<^emph>\<open>x\<close>.
|
|
|
|
So in the request result we get an unresolved case because the evaluator can not get
|
2023-03-04 08:57:14 +00:00
|
|
|
the value of the \<^emph>\<open>x\<close> attribute of the instance @{docitem \<open>sdf\<close>}:\<close>
|
2021-12-09 08:57:21 +00:00
|
|
|
value*\<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A-instances}\<close>
|
2023-05-15 15:55:52 +00:00
|
|
|
(*>*)
|
2021-12-09 08:57:21 +00:00
|
|
|
section\<open>Limitations\<close>
|
|
|
|
|
2021-11-04 14:10:02 +00:00
|
|
|
text\<open>There are still some limitations.
|
2023-03-24 07:08:55 +00:00
|
|
|
The terms passed as arguments to a TA are not simplified \<open>before\<close> expansion
|
|
|
|
and their evaluation therefore fails:
|
2021-10-20 07:10:11 +00:00
|
|
|
\<close>
|
2023-03-24 07:08:55 +00:00
|
|
|
|
|
|
|
value\<open>@{thm (''HOL.re'' @ ''fl'')}\<close>
|
|
|
|
value-assert-error\<open>@{thm (''HOL.re'' @ ''fl'')}\<close>
|
|
|
|
\<open>wrong term format: must be string constant\<close>
|
|
|
|
value-assert-error\<open>@{thm ''HOL.refl''} = @{thm (''HOL.re'' @ ''fl'')}\<close>
|
|
|
|
\<open>wrong term format: must be string constant\<close>
|
2021-10-20 07:10:11 +00:00
|
|
|
|
2021-11-04 14:10:02 +00:00
|
|
|
text\<open>The type checking is unaware that a class is subclass of another one.
|
|
|
|
The @{doc_class "G"} is a subclass of the class @{doc_class "C"}, but one can not use it
|
|
|
|
to update the instance @{docitem \<open>xcv4\<close>}:
|
|
|
|
\<close>
|
2023-03-24 07:08:55 +00:00
|
|
|
|
|
|
|
update_instance-assert-error[xcv4::F, b+="{(@{A ''xcv3''},@{G ''xcv5''})}"]
|
|
|
|
\<open>type of attribute: Conceptual.F.b does not fit to term\<close>
|
2021-10-20 07:10:11 +00:00
|
|
|
|
2022-03-14 11:23:54 +00:00
|
|
|
|
2022-03-30 05:54:38 +00:00
|
|
|
section\<open>\<^theory_text>\<open>assert*\<close>-Annotated assertion-commands\<close>
|
|
|
|
|
|
|
|
text\<open>The \<^emph>\<open>assert*\<close>-command allows for logical statements to be checked in the global context.
|
2023-03-24 07:08:55 +00:00
|
|
|
Recall that it uses the same mechanism as the \<^emph>\<open>value*\<close>-command but requires that the evaluation
|
|
|
|
reduces the argument term to true.
|
|
|
|
Consequently, it has the same limitations as \<^emph>\<open>value*\<close>.
|
2022-03-30 05:54:38 +00:00
|
|
|
\<close>
|
|
|
|
|
2023-03-06 15:53:57 +00:00
|
|
|
text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-Unit-Tests.Concept_High_Level_Invariants\<close>
|
2022-03-30 05:54:38 +00:00
|
|
|
we can check logical statements:\<close>
|
2023-03-20 15:50:23 +00:00
|
|
|
|
2023-05-24 10:38:29 +00:00
|
|
|
term*\<open>authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction2\<close>}
|
|
|
|
= authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction3\<close>}\<close>
|
|
|
|
assert*\<open>authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction2\<close>}
|
|
|
|
= authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction3\<close>}\<close>
|
|
|
|
assert*\<open>\<not>(authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction2\<close>}
|
|
|
|
= authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction4\<close>})\<close>
|
2023-03-20 15:50:23 +00:00
|
|
|
|
2022-03-30 05:54:38 +00:00
|
|
|
text\<open>Assertions must be boolean expressions, so the following assertion triggers an error:\<close>
|
|
|
|
(* Error:
|
|
|
|
assert*\<open>@{introduction \<open>introduction2\<close>}\<close>*)
|
|
|
|
|
|
|
|
text\<open>Assertions must be true, hence the error:\<close>
|
|
|
|
(* Error:
|
|
|
|
assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*)
|
2023-03-20 15:50:23 +00:00
|
|
|
|
2022-03-30 05:54:38 +00:00
|
|
|
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
2022-04-19 12:05:52 +00:00
|
|
|
assert*[assertionA::A]\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
|
|
|
|
2023-05-15 15:55:52 +00:00
|
|
|
(*<*)
|
2023-03-20 15:50:23 +00:00
|
|
|
text*[assertionAA::A]\<open>@{A "assertionA"}\<close>
|
|
|
|
text\<open>... and here we reference @{A \<open>assertionA\<close>}.\<close>
|
2023-05-15 15:55:52 +00:00
|
|
|
(*>*)
|
2022-03-30 05:54:38 +00:00
|
|
|
assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
2023-03-20 15:50:23 +00:00
|
|
|
|
2023-01-23 07:50:36 +00:00
|
|
|
text\<open>The optional evaluator of \<open>value*\<close> and \<open>assert*\<close> must be specified after the meta arguments:\<close>
|
2023-01-09 14:13:23 +00:00
|
|
|
value* [optional_test_A::A, x=6] [nbe] \<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A-instances}\<close>
|
2023-03-20 15:50:23 +00:00
|
|
|
|
2023-01-09 14:13:23 +00:00
|
|
|
assert* [resultProof3::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"] [nbe]
|
|
|
|
\<open>evidence @{result \<open>resultProof3\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
2023-03-20 15:50:23 +00:00
|
|
|
|
2023-05-24 10:38:29 +00:00
|
|
|
text\<open>
|
|
|
|
Evaluation of \<open>assert*\<close> can be disabled using the *\<open>disable_assert_evaluation\<close> theory attribute.
|
|
|
|
Then only the checking of the term is done:
|
|
|
|
\<close>
|
|
|
|
declare[[disable_assert_evaluation]]
|
|
|
|
assert*\<open>evidence @{result \<open>resultProof3\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
|
|
|
declare[[disable_assert_evaluation = false]]
|
|
|
|
|
2021-11-04 14:10:02 +00:00
|
|
|
end
|