From f9027ef3315977d3fc788c9f895ab0b2f3368d7f Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Sun, 18 Jul 2021 17:34:52 +0200 Subject: [PATCH] a section explaining the consequences of a doc-class and its shallow semantics in Isabelle records on different levels of representation --- src/ontologies/Conceptual/Conceptual.thy | 75 ++++++++++++++++++++++-- src/tests/Attributes.thy | 2 + 2 files changed, 71 insertions(+), 6 deletions(-) diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy index e34f02c..0ae6409 100755 --- a/src/ontologies/Conceptual/Conceptual.thy +++ b/src/ontologies/Conceptual/Conceptual.thy @@ -11,6 +11,8 @@ * SPDX-License-Identifier: BSD-2-Clause *************************************************************************) +section\A conceptual introduction into DOF and its features:\ + theory Conceptual imports "../../DOF/Isa_DOF" "../../DOF/Isa_COL" begin @@ -18,7 +20,61 @@ begin doc_class A = level :: "int option" - x :: int + x :: int + +subsection\Excursion: On the semantic consequences of this definition: \ + +text\This class definition leads an implicit Isabelle/HOL \<^theory_text>\record\ definition +(cf. \<^url>\https://isabelle.in.tum.de/dist/Isabelle2021/doc/isar-ref.pdf\, chapter 11.6.). +Consequently, \<^theory_text>\doc_class\'es inherit the entire theory-infrastructure from Isabelle records: +\<^enum> there is a HOL-type \<^typ>\A\ and its extensible version \<^typ>\'a A_scheme\ +\<^enum> there are HOL-terms representing \<^emph>\doc_class instances\ with the high-level syntax: + \<^enum> \<^term>\undefined\level := Some (1::int), x := 5::int \ :: A\ + (Note that this way to construct an instance is not necessarily computable + \<^enum> \<^term>\\tag_attribute = X, level = Y, x = Z\ :: A\ + \<^enum> \<^term>\\tag_attribute = X, level = Y, x = Z, \ = M\ :: ('a A_scheme)\ +\<^enum> there is an entire proof infra-structure allowing to reason about \<^emph>\doc_class instances\; + this involves the constructor, the selectors (representing the \<^emph>\attributes\ in OO lingo) + the update functions, the rules to establish equality and, if possible the code generator + setups: + \<^enum> \<^term>\A.make :: int \ int option \ int \ A\ + \<^enum> \<^term>\A.level :: 'a A_scheme \ int option\ + \<^enum> \<^term>\A.level_update :: (int option \ int option) \ 'a A_scheme \ 'a A_scheme\ + \<^enum> ... + together with the rules such as: + \<^enum> @{thm [display] A.simps(2)} + \<^enum> @{thm [display] A.simps(6)} + \<^enum> ... +\ +(* the generated theory of the \<^theory_text>\doc_class\ A can be inspectwed, of course, by *) +find_theorems (60) name:Conceptual name:A + + +text\As a consequence of the theory of the \<^theory_text>\doc_class\ \A\, the code-generator setup lets us +evaluate statements such as: \ + +value\ the(A.level (A.make 3 (Some 4) 5)) = 4\ + +text\And finally, as a consequence of the above semantic construction of \<^theory_text>\doc_class\'es, the internal +\\\-calculus representation of class instances looks as follows:\ + +ML\ +val tt = @{term \the(A.level (A.make 3 (Some 4) 5))\} +\ + +text\For the code-generation, we have the following access to values representing class instances:\ +ML\ +val A_make = @{code A.make}; +val zero = @{code "0::int"}; +val one = @{code "1::int"}; +val add = @{code "(+) :: int \ int \ int"}; + +A_make zero (SOME one) (add one one) +\ + + +subsection\An independent class-tree root: \ + doc_class B = level :: "int option" @@ -29,13 +85,17 @@ doc_class B = text\We may even use type-synonyms for class synonyms ...\ type_synonym XX = B + +subsection\Examples of inheritance \ + doc_class C = XX + z :: "A option" <= None (* A LINK, i.e. an attribute that has a type referring to a document class. Mathematical relations over document items can be modeled. *) - g :: "thm" + g :: "thm" (* a reference to the proxy-type 'thm' allowing + to denote references to theorems inside attributes *) -datatype enum = X1 | X2 | X3 +datatype enum = X1 | X2 | X3 (* we add an enumeration type ... *) doc_class D = B + x :: "string" <= "\def \\" (* overriding default *) @@ -68,15 +128,18 @@ thm br_inv_def thm br'_inv_def thm cr_inv_def +term "\F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\" + +term "br' (\F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\) " + text\Now, we can use these definitions in order to generate code for these validation functions. Note, however, that not everything that we can write in an invariant (basically: HOL) is executable, or even compilable by the code generator setup:\ ML\ val cr_inv_code = @{code "cr_inv"} \ \\works albeit thm is abstract ...\ text\while in :\ -(* -ML\ val br_inv_code = @{code "br_inv"} \ \\does not work ...\ -*) +(* ML\ val br_inv_code = @{code "br_inv"} \ \\this does not work ...\ *) + text\... the compilation fails due to the fact that nothing prevents the user to define an infinite relation between \<^typ>\A\ and \<^typ>\C\. However, the alternative variant: \ diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy index 6d3d46f..74e548b 100755 --- a/src/tests/Attributes.thy +++ b/src/tests/Attributes.thy @@ -68,6 +68,8 @@ text*[omega::E, x = "''def''"]\ Lorem ipsum ... @{thm refl} \ text\ As mentioned in @{docitem \dfgdfg\} \ text\Here is a simulation what happens on the level of the (HOL)-term representation:\ +typ \'a A_scheme\ +typ \A\ term "A.x (undefined\A.x := 3\)" term "B.x ((undefined::C)\B.y := [''sdf'']\)" term "C.z ((undefined::C)\B.y := [''sdf''], z:= Some undefined\)"