forked from Isabelle_DOF/Isabelle_DOF
corrected bugs.
This commit is contained in:
parent
9fae991ea0
commit
8e4ac3f118
|
@ -84,11 +84,12 @@ text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit r
|
||||||
text\<open>Not only text-elements are "ontology-aware", proofs and code can this be too !\<close>
|
text\<open>Not only text-elements are "ontology-aware", proofs and code can this be too !\<close>
|
||||||
references\<close>
|
references\<close>
|
||||||
\<comment> \<open>Referencing from and to a ML-code context:\<close>
|
\<comment> \<open>Referencing from and to a ML-code context:\<close>
|
||||||
|
(*<*)
|
||||||
ML*[c4::C, z = "Some @{A \<open>a1\<close>}"]\<open>
|
ML*[c4::C, z = "Some @{A \<open>a1\<close>}"]\<open>
|
||||||
fun fac x = if x = 0 then 1 else x * (fac(x-1))
|
fun fac x = if x = 0 then 1 else x * (fac(x-1))
|
||||||
val v = \<^value_>\<open>A.x (the (z @{C \<open>c4\<close>}))\<close> |> HOLogic.dest_number |> snd |> fac
|
val v = \<^value_>\<open>A.x (the (z @{C \<open>c4\<close>}))\<close> |> HOLogic.dest_number |> snd |> fac
|
||||||
\<close>
|
\<close>
|
||||||
|
(*>*)
|
||||||
definition*[a2::A, x=5, level="Some 1"] xx' where "xx' \<equiv> A.x @{A \<open>a1\<close>}" if "A.x @{A \<open>a1\<close>} = 5"
|
definition*[a2::A, x=5, level="Some 1"] xx' where "xx' \<equiv> A.x @{A \<open>a1\<close>}" if "A.x @{A \<open>a1\<close>} = 5"
|
||||||
|
|
||||||
lemma*[e5::E] testtest : "xx + A.x @{A \<open>a1\<close>} = yy + A.x @{A \<open>a1\<close>} \<Longrightarrow> xx = yy" by simp
|
lemma*[e5::E] testtest : "xx + A.x @{A \<open>a1\<close>} = yy + A.x @{A \<open>a1\<close>} \<Longrightarrow> xx = yy" by simp
|
||||||
|
@ -140,7 +141,7 @@ update_instance*[f::F,b:="{(@{docitem \<open>a\<close>}::A,@{docitem \<open>c1
|
||||||
section\<open>Closing the Monitor and testing the Results.\<close>
|
section\<open>Closing the Monitor and testing the Results.\<close>
|
||||||
|
|
||||||
close_monitor*[struct]
|
close_monitor*[struct]
|
||||||
text\<open>@{A a0}\<close>
|
|
||||||
text\<open>And the trace of the monitor is:\<close>
|
text\<open>And the trace of the monitor is:\<close>
|
||||||
ML\<open>val trace = @{trace_attribute struct}\<close>
|
ML\<open>val trace = @{trace_attribute struct}\<close>
|
||||||
ML\<open>@{assert} (trace =
|
ML\<open>@{assert} (trace =
|
||||||
|
|
|
@ -1,11 +1,52 @@
|
||||||
|
(*************************************************************************
|
||||||
|
* 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>High level syntax Invariants\<close>
|
chapter\<open>High level syntax Invariants\<close>
|
||||||
|
|
||||||
theory High_Level_Syntax_Invariants
|
theory High_Level_Syntax_Invariants
|
||||||
imports "Isabelle_DOF.Isa_DOF"
|
imports "Isabelle_DOF.Isa_DOF"
|
||||||
"Isabelle_DOF-Unit-Tests_document"
|
"Isabelle_DOF-Unit-Tests_document"
|
||||||
|
TestKit
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
section\<open>Test Purpose.\<close>
|
||||||
|
text\<open>
|
||||||
|
Without invariants, ontological classes as such are too liberal in many situations.
|
||||||
|
Similarly to UML constraints, invariants or hand-programmed checking functions
|
||||||
|
can be added in ODL ontologies in order to constrain class instances or
|
||||||
|
(via monitor traces) impose structural constraints over an entire document.
|
||||||
|
|
||||||
|
While hand-programmed checking functions were tested in test-case
|
||||||
|
\<^verbatim>\<open>Concept_Example_Low_Level_Invariant\<close>, in this text case, we test
|
||||||
|
high-level invariants, i.e. data-constraints speicified as executable
|
||||||
|
HOL-predicates in the @{theory_text \<open>invariant\<close>} clause of ODL definitions.
|
||||||
|
|
||||||
|
To enable the checking of the invariants, the \<open>invariants_checking\<close>
|
||||||
|
theory attribute must be set:\<close>
|
||||||
|
|
||||||
|
|
||||||
|
section\<open>The Scenario.\<close>
|
||||||
|
|
||||||
|
text\<open> This is merely an example that shows that the generated invariants
|
||||||
|
fit nicely together; i.e. allow for sensible consistency and invariant
|
||||||
|
preservation proofs related to ontological matchings. \<close>
|
||||||
|
|
||||||
|
|
||||||
|
text\<open>Using HOL, we can define a mapping between two ontologies.
|
||||||
|
It is called ontology matching or ontology alignment.
|
||||||
|
Here is an example which show how to map two classes.
|
||||||
|
HOL also allows us to map the invariants (ontological rules) of the classes!\<close>
|
||||||
|
|
||||||
text\<open>
|
text\<open>
|
||||||
Ontological classes as described so far are too liberal in many situations.
|
Ontological classes as described so far are too liberal in many situations.
|
||||||
There is a first high-level syntax implementation for class invariants.
|
There is a first high-level syntax implementation for class invariants.
|
||||||
|
|
Loading…
Reference in New Issue