forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
This commit is contained in:
commit
eef8170e40
|
@ -11,6 +11,8 @@
|
||||||
* SPDX-License-Identifier: BSD-2-Clause
|
* SPDX-License-Identifier: BSD-2-Clause
|
||||||
*************************************************************************)
|
*************************************************************************)
|
||||||
|
|
||||||
|
section\<open>A conceptual introduction into DOF and its features:\<close>
|
||||||
|
|
||||||
theory Conceptual
|
theory Conceptual
|
||||||
imports "../../DOF/Isa_DOF" "../../DOF/Isa_COL"
|
imports "../../DOF/Isa_DOF" "../../DOF/Isa_COL"
|
||||||
begin
|
begin
|
||||||
|
@ -18,7 +20,61 @@ begin
|
||||||
|
|
||||||
doc_class A =
|
doc_class A =
|
||||||
level :: "int option"
|
level :: "int option"
|
||||||
x :: int
|
x :: int
|
||||||
|
|
||||||
|
subsection\<open>Excursion: On the semantic consequences of this definition: \<close>
|
||||||
|
|
||||||
|
text\<open>This class definition leads an implicit Isabelle/HOL \<^theory_text>\<open>record\<close> definition
|
||||||
|
(cf. \<^url>\<open>https://isabelle.in.tum.de/dist/Isabelle2021/doc/isar-ref.pdf\<close>, chapter 11.6.).
|
||||||
|
Consequently, \<^theory_text>\<open>doc_class\<close>'es inherit the entire theory-infrastructure from Isabelle records:
|
||||||
|
\<^enum> there is a HOL-type \<^typ>\<open>A\<close> and its extensible version \<^typ>\<open>'a A_scheme\<close>
|
||||||
|
\<^enum> there are HOL-terms representing \<^emph>\<open>doc_class instances\<close> with the high-level syntax:
|
||||||
|
\<^enum> \<^term>\<open>undefined\<lparr>level := Some (1::int), x := 5::int \<rparr> :: A\<close>
|
||||||
|
(Note that this way to construct an instance is not necessarily computable
|
||||||
|
\<^enum> \<^term>\<open>\<lparr>tag_attribute = X, level = Y, x = Z\<rparr> :: A\<close>
|
||||||
|
\<^enum> \<^term>\<open>\<lparr>tag_attribute = X, level = Y, x = Z, \<dots> = M\<rparr> :: ('a A_scheme)\<close>
|
||||||
|
\<^enum> there is an entire proof infra-structure allowing to reason about \<^emph>\<open>doc_class instances\<close>;
|
||||||
|
this involves the constructor, the selectors (representing the \<^emph>\<open>attributes\<close> in OO lingo)
|
||||||
|
the update functions, the rules to establish equality and, if possible the code generator
|
||||||
|
setups:
|
||||||
|
\<^enum> \<^term>\<open>A.make :: int \<Rightarrow> int option \<Rightarrow> int \<Rightarrow> A\<close>
|
||||||
|
\<^enum> \<^term>\<open>A.level :: 'a A_scheme \<Rightarrow> int option\<close>
|
||||||
|
\<^enum> \<^term>\<open>A.level_update :: (int option \<Rightarrow> int option) \<Rightarrow> 'a A_scheme \<Rightarrow> 'a A_scheme\<close>
|
||||||
|
\<^enum> ...
|
||||||
|
together with the rules such as:
|
||||||
|
\<^enum> @{thm [display] A.simps(2)}
|
||||||
|
\<^enum> @{thm [display] A.simps(6)}
|
||||||
|
\<^enum> ...
|
||||||
|
\<close>
|
||||||
|
(* the generated theory of the \<^theory_text>\<open>doc_class\<close> A can be inspectwed, of course, by *)
|
||||||
|
find_theorems (60) name:Conceptual name:A
|
||||||
|
|
||||||
|
|
||||||
|
text\<open>As a consequence of the theory of the \<^theory_text>\<open>doc_class\<close> \<open>A\<close>, the code-generator setup lets us
|
||||||
|
evaluate statements such as: \<close>
|
||||||
|
|
||||||
|
value\<open> the(A.level (A.make 3 (Some 4) 5)) = 4\<close>
|
||||||
|
|
||||||
|
text\<open>And finally, as a consequence of the above semantic construction of \<^theory_text>\<open>doc_class\<close>'es, the internal
|
||||||
|
\<open>\<lambda>\<close>-calculus representation of class instances looks as follows:\<close>
|
||||||
|
|
||||||
|
ML\<open>
|
||||||
|
val tt = @{term \<open>the(A.level (A.make 3 (Some 4) 5))\<close>}
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
text\<open>For the code-generation, we have the following access to values representing class instances:\<close>
|
||||||
|
ML\<open>
|
||||||
|
val A_make = @{code A.make};
|
||||||
|
val zero = @{code "0::int"};
|
||||||
|
val one = @{code "1::int"};
|
||||||
|
val add = @{code "(+) :: int \<Rightarrow> int \<Rightarrow> int"};
|
||||||
|
|
||||||
|
A_make zero (SOME one) (add one one)
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
subsection\<open>An independent class-tree root: \<close>
|
||||||
|
|
||||||
|
|
||||||
doc_class B =
|
doc_class B =
|
||||||
level :: "int option"
|
level :: "int option"
|
||||||
|
@ -29,13 +85,17 @@ doc_class B =
|
||||||
text\<open>We may even use type-synonyms for class synonyms ...\<close>
|
text\<open>We may even use type-synonyms for class synonyms ...\<close>
|
||||||
type_synonym XX = B
|
type_synonym XX = B
|
||||||
|
|
||||||
|
|
||||||
|
subsection\<open>Examples of inheritance \<close>
|
||||||
|
|
||||||
doc_class C = XX +
|
doc_class C = XX +
|
||||||
z :: "A option" <= None (* A LINK, i.e. an attribute that has a type
|
z :: "A option" <= None (* A LINK, i.e. an attribute that has a type
|
||||||
referring to a document class. Mathematical
|
referring to a document class. Mathematical
|
||||||
relations over document items can be modeled. *)
|
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 +
|
doc_class D = B +
|
||||||
x :: "string" <= "\<open>def \<longrightarrow>\<close>" (* overriding default *)
|
x :: "string" <= "\<open>def \<longrightarrow>\<close>" (* overriding default *)
|
||||||
|
@ -68,15 +128,18 @@ thm br_inv_def
|
||||||
thm br'_inv_def
|
thm br'_inv_def
|
||||||
thm cr_inv_def
|
thm cr_inv_def
|
||||||
|
|
||||||
|
term "\<lparr>F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\<rparr>"
|
||||||
|
|
||||||
|
term "br' (\<lparr>F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\<rparr>) "
|
||||||
|
|
||||||
text\<open>Now, we can use these definitions in order to generate code for these validation functions.
|
text\<open>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,
|
Note, however, that not everything that we can write in an invariant (basically: HOL) is executable,
|
||||||
or even compilable by the code generator setup:\<close>
|
or even compilable by the code generator setup:\<close>
|
||||||
|
|
||||||
ML\<open> val cr_inv_code = @{code "cr_inv"} \<close> \<comment>\<open>works albeit thm is abstract ...\<close>
|
ML\<open> val cr_inv_code = @{code "cr_inv"} \<close> \<comment>\<open>works albeit thm is abstract ...\<close>
|
||||||
text\<open>while in :\<close>
|
text\<open>while in :\<close>
|
||||||
(*
|
(* ML\<open> val br_inv_code = @{code "br_inv"} \<close> \<comment>\<open>this does not work ...\<close> *)
|
||||||
ML\<open> val br_inv_code = @{code "br_inv"} \<close> \<comment>\<open>does not work ...\<close>
|
|
||||||
*)
|
|
||||||
text\<open>... the compilation fails due to the fact that nothing prevents the user
|
text\<open>... the compilation fails due to the fact that nothing prevents the user
|
||||||
to define an infinite relation between \<^typ>\<open>A\<close> and \<^typ>\<open>C\<close>. However, the alternative
|
to define an infinite relation between \<^typ>\<open>A\<close> and \<^typ>\<open>C\<close>. However, the alternative
|
||||||
variant: \<close>
|
variant: \<close>
|
||||||
|
|
|
@ -68,6 +68,8 @@ text*[omega::E, x = "''def''"]\<open> Lorem ipsum ... @{thm refl} \<close>
|
||||||
text\<open> As mentioned in @{docitem \<open>dfgdfg\<close>} \<close>
|
text\<open> As mentioned in @{docitem \<open>dfgdfg\<close>} \<close>
|
||||||
|
|
||||||
text\<open>Here is a simulation what happens on the level of the (HOL)-term representation:\<close>
|
text\<open>Here is a simulation what happens on the level of the (HOL)-term representation:\<close>
|
||||||
|
typ \<open>'a A_scheme\<close>
|
||||||
|
typ \<open>A\<close>
|
||||||
term "A.x (undefined\<lparr>A.x := 3\<rparr>)"
|
term "A.x (undefined\<lparr>A.x := 3\<rparr>)"
|
||||||
term "B.x ((undefined::C)\<lparr>B.y := [''sdf'']\<rparr>)"
|
term "B.x ((undefined::C)\<lparr>B.y := [''sdf'']\<rparr>)"
|
||||||
term "C.z ((undefined::C)\<lparr>B.y := [''sdf''], z:= Some undefined\<rparr>)"
|
term "C.z ((undefined::C)\<lparr>B.y := [''sdf''], z:= Some undefined\<rparr>)"
|
||||||
|
|
Loading…
Reference in New Issue