From eb292a695bb5ec22505b03a54d54ac93a9a0270a Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Mon, 4 Oct 2021 15:11:29 +0200
Subject: [PATCH] added poor man's encoding of inheritance in Cyto-Model.

---
 examples/cytology/Cytology.thy | 54 +++++++++++++++++++++++-----------
 1 file changed, 37 insertions(+), 17 deletions(-)

diff --git a/examples/cytology/Cytology.thy b/examples/cytology/Cytology.thy
index 825cdae..2ad907c 100644
--- a/examples/cytology/Cytology.thy
+++ b/examples/cytology/Cytology.thy
@@ -8,33 +8,43 @@ text\<open>A small example ontology for demonstration purposes.
 
 datatype protein = filaments | motor_proteins | rna |dna |nucleolus
 
+type_synonym desc = "string"
 
-onto_class organelles =   description :: string
+onto_class organelles   =   description :: desc
 
-onto_class ribosomes = organelles +       description :: string
+onto_class ribosomes    = organelles +    description :: desc
    
-onto_class mytochondria = organelles +    description :: string
+onto_class mytochondria = organelles +    description :: desc
 
-onto_class golgi_apparatus = organelles + description :: string
-
-onto_class lysosome = organelles + description :: string
+onto_class golgi_apparatus = organelles + description :: desc
 
+onto_class lysosome    = organelles +     description :: desc
 
 text\<open>the control center of the cell:\<close>
 onto_class nucleus = organelles +  
-       description :: string
+       description :: desc
        components  :: "protein list" <= "[nucleolus]" 
 
-definition is_nucleus 
-  where "is_nucleus org \<equiv>  \<exists> tg d ta da . org  =  nucleus.make tg d ta da"
+(* Not so nice construction to mimick inheritance on types useds in attribute positions. *)
+datatype organelles' = mk\<^sub>r\<^sub>i\<^sub>b\<^sub>o\<^sub>s\<^sub>o\<^sub>m\<^sub>e\<^sub>s     (get_ribosomes:ribosomes)
+                     | mk\<^sub>m\<^sub>y\<^sub>t\<^sub>o\<^sub>c\<^sub>h\<^sub>o\<^sub>n\<^sub>d\<^sub>r\<^sub>i\<^sub>a   (get_mytochondria:mytochondria)
+                     | mk\<^sub>g\<^sub>o\<^sub>l\<^sub>g\<^sub>i\<^sub>_\<^sub>a\<^sub>p\<^sub>p\<^sub>a\<^sub>r\<^sub>a\<^sub>t\<^sub>u\<^sub>s (get_golgi_apparatus: golgi_apparatus)
+                     | mk\<^sub>l\<^sub>y\<^sub>s\<^sub>o\<^sub>s\<^sub>o\<^sub>m\<^sub>e      (get_lysosome : lysosome)
+                     | mk\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s       (get_nucleus : nucleus)
+
+fun is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s where "is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s (mk\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s X) = True" | "is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s ( _) = False"
+
+
+definition is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s 
+  where "is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s org \<equiv>  \<exists> tg d ta da . org  =  nucleus.make tg d ta da"
 find_theorems (300) name:"Cytology" name:"nucleus"
 
 
 onto_class cell = 
     name             :: string
-    membrane         :: string   <= "\<open>The outer boundary of the cell\<close>"
-    cytoplasm        :: string   <= "\<open>The outer boundary of the cell\<close>"
-    cytoskeleton     :: string   <= "\<open>includes the thread-like microfilaments\<close>"
+    membrane         :: desc   <= "\<open>The outer boundary of the cell\<close>"
+    cytoplasm        :: desc   <= "\<open>The liquid in the cell\<close>"
+    cytoskeleton     :: desc   <= "\<open>includes the thread-like microfilaments\<close>"
     genetic_material :: "protein list" <= "[rna, dna]"
 
 text\<open>Cells are devided into two categories: \<^emph>\<open>procaryotic\<close> cells (unicellular organisms some 
@@ -45,9 +55,19 @@ onto_class procaryotic_cells = cell +
     name :: string
 
 onto_class eucaryotic_cells = cell + 
-    organelles :: "organelles list"
-(*
-invariant has_nucleus :: "\<lambda>\<sigma>::eucaryotic_cells. \<exists> org \<in> set (organelles \<sigma>). is_nucleus org"
-*)
- 
+    organelles :: "organelles' list"
+    invariant has_nucleus :: "\<lambda>\<sigma>::eucaryotic_cells. \<exists> org \<in> set (organelles \<sigma>). is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s org"
+    \<comment>\<open>Cells must have at least one nucleus. However, this should be executable.\<close>
+
+find_theorems (70)name:"eucaryotic_cells"
+find_theorems name:has_nucleus
+
+value "is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s (mk\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s X)"
+
+term \<open>eucaryotic_cells.organelles\<close>
+
+value \<open>(eucaryotic_cells.organelles(eucaryotic_cells.make X Y Z Z Z [] 3 []))\<close>
+value \<open>has_nucleus_inv(eucaryotic_cells.make X Y Z Z Z [] 3 [])\<close>
+
+
 end