From 9b08e9258874cbac2d28d40c91f1e40e8e85f556 Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Fri, 8 Oct 2021 16:00:57 +0200
Subject: [PATCH] Experiments with the code generator for Isa_DOF class
 objects.

---
 examples/cytology/Cytology.thy |  2 +-
 src/tests/Attributes.thy       | 24 ++++++++++++++++++++++++
 2 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/examples/cytology/Cytology.thy b/examples/cytology/Cytology.thy
index d7d5f9a..d29b3c4 100644
--- a/examples/cytology/Cytology.thy
+++ b/examples/cytology/Cytology.thy
@@ -6,7 +6,7 @@ text\<open>A small example ontology for demonstration purposes.
      The presentation follows closely: \<^url>\<open>https://www.youtube.com/watch?v=URUJD5NEXC8\<close>.\<close>
 
 
-datatype protein = filaments | motor_proteins | rna |dna |nucleolus
+datatype protein = filaments | motor_proteins | rna | dna |nucleolus
 
 type_synonym desc = "string"
 
diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy
index 74e548b..fd6aaa3 100755
--- a/src/tests/Attributes.thy
+++ b/src/tests/Attributes.thy
@@ -30,6 +30,30 @@ val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, moni
 Symtab.dest docitem_tab;
 Symtab.dest docclass_tab;
 \<close>
+ML\<open>
+#value(the(the(Symtab.lookup docitem_tab "aaa")))
+
+\<close>
+
+find_theorems (60) name:"Conceptual.M." 
+
+value [simp]"trace(M.make undefined [] ())"
+value "ok(M.make undefined_AAA [] ())"
+value "trace(M.make undefined_AAA [] ())"
+value "tag_attribute(M.make undefined_AAA [] ())"
+
+
+value "ok(M.make 0 [] ())"
+(*
+value "ok(M.make 0 [] undefined)"
+*)
+
+value [simp] \<open> M.ok 
+                   (Conceptual.M.trace_update (\<lambda>x. [])
+                    (Conceptual.M.tag_attribute_update (\<lambda>x. 0)
+                     (Conceptual.M.ok_update (\<lambda>x. ())
+                   (undefined::M)) 
+                   ))\<close>
 
 
 ML\<open>