Update file hierarchy with Bu proposition

The idea is for the Deep_Interpretation to source the shallow material,
and then update the checking and elaboration functions
of the term anti-quotations.
To achieve this, the mechanism of removing and readding the notations
(mixfixes) of the term-antiquotations after the metalogic
is sourced is used.

Example:

With shallow:

datatype "typ" = ISA_typ string  ("@{typ _}")

Generate a datatype whose Constructor ISA_typ has
the notation @{typ ...}.

You get:

find_consts name:"ISA_typ"

find_consts
  name: "ISA_typ"

found 1 constant(s):
  Shallow_Interpretation.typ.ISA_typ :: "char list ⇒ typ"

With Deep:

no_notation "ISA_typ" ("@{typ _}")

consts ISA_typ :: "string ⇒ typ" ("@{typ _}")

The notation is removed and then added to the new ISA_typ constant.

You get:

find_consts name:"ISA_typ"

find_consts
  name: "ISA_typ"

found 2 constant(s):
  Deep_Interpretation.ISA_typ :: "char list ⇒ Core.typ"
  Shallow_Interpretation.typ.ISA_typ :: "char list ⇒ Shallow_Interpretation.typ"

But only the Deep_Interpretation constant has the notation (mixfix).

src/DOF/DOF_Shallow.thy

@@ -1,6 +1,6 @@
 theory DOF_Shallow
-  imports "Isabelle_DOF.Isa_DOF"
-          "Isabelle_DOF.Shallow_Interpretation"
+  imports Isabelle_DOF.Isa_COL
+          Isabelle_DOF.Shallow_Interpretation
 
 begin
 
@@ -18,4 +18,4 @@ term "@{docitem  \<open>doc_ref\<close>}"
 ML\<open>   @{term "@{docitem  \<open>doc_ref\<close>}"}\<close>
 (**)
 
-end
+end

src/DOF/Isa_COL.thy

@@ -22,7 +22,7 @@ text\<open> Building a fundamental infrastructure for common document elements s
     \<close> 
 
 theory Isa_COL   
-  imports  DOF_Shallow
+  imports  Isa_DOF
   keywords "title*"        "subtitle*"      
            "chapter*"      "section*"   
            "subsection*"   "subsubsection*" 

src/ROOT

@@ -2,7 +2,6 @@ session "Isabelle_DOF" = "Functional-Automata" +
   options [document = pdf, document_output = "output", document_build = dof]
   sessions
     "Regular-Sets"
-    "Metalogic_ProofChecker"
   directories 
     "DOF"
     "DOF/meta_interpretation"
@@ -15,8 +14,5 @@ session "Isabelle_DOF" = "Functional-Automata" +
     "ontologies/CC_v3_1_R5"
   theories
     "DOF/DOF_Shallow"
-    "DOF/DOF_Deep"
     "ontologies/ontologies"
   export_classpath
-
-

src/ROOTS

@@ -1 +1,2 @@
 tests
+deep

src/deep/DOF_Deep.thy

@@ -1,6 +1,5 @@
 theory DOF_Deep
-  imports "Isabelle_DOF.Isa_DOF"
-          "Isabelle_DOF.Deep_Interpretation"
+  imports Deep_Interpretation
 
 begin
 

src/deep/Deep_Interpretation.thy

@@ -1,5 +1,5 @@
 theory Deep_Interpretation
-  imports Isabelle_DOF.DOF_Core
+  imports Isabelle_DOF.DOF_Shallow
           Metalogic_ProofChecker.ProofTerm
           
 begin
@@ -8,6 +8,17 @@ subsection\<open> Syntax \<close>
 
 \<comment> \<open>and others in the future : file, http, thy, ...\<close> 
 
+(* Delete shallow interpretation notations (mixfixes) of the term anti-quotations,
+  so we can use them for the deep interpretation *)
+no_notation "ISA_typ" ("@{typ _}")
+no_notation "ISA_term" ("@{term _}")
+no_notation "ISA_thm" ("@{thm _}")
+no_notation "ISA_file" ("@{file _}")
+no_notation "ISA_thy" ("@{thy _}")
+no_notation "ISA_docitem" ("@{docitem _}")
+no_notation "ISA_docitem_attr" ("@{docitemattr (_) :: (_)}")
+no_notation "ISA_trace_attribute" ("@{trace-attribute _}")
+
 consts ISA_typ :: "string \<Rightarrow> typ" ("@{typ _}")
 consts ISA_term :: "string \<Rightarrow> term" ("@{term _}")
 consts ISA_term_repr    :: "string \<Rightarrow> term"              ("@{termrepr _}")

src/deep/ROOT

@@ -0,0 +1,10 @@
+session "Isabelle_DOF-Deep" = Isabelle_DOF + 
+  options [document = pdf, document_output = "output", document_build = dof]
+  sessions
+    "Metalogic_ProofChecker"
+  directories
+    "tests"
+  theories
+    "DOF_Deep"
+    "tests/Reification_Test"
+  export_classpath

src/deep/tests/Reification_Test.thy

@@ -1,5 +1,5 @@
 theory Reification_Test
-  imports "Isabelle_DOF.DOF_Deep"
+  imports "../DOF_Deep"
   
 begin
 

src/ontologies/Conceptual/Conceptual.thy

@@ -17,7 +17,7 @@ theory
   Conceptual
 imports 
   "Isabelle_DOF.DOF_Shallow"
-  "Isabelle_DOF.Isa_COL"
+
 begin
 
 

src/ontologies/scholarly_paper/scholarly_paper.thy

@@ -14,7 +14,7 @@
 section\<open>An example ontology for scientific, MINT-oriented papers.\<close>
 
 theory scholarly_paper
-  imports "Isabelle_DOF.Isa_COL"
+  imports "Isabelle_DOF.DOF_Shallow"
   keywords "author*" "abstract*"
            "Definition*" "Lemma*" "Theorem*"  :: document_body
 begin

src/ontologies/small_math/small_math.thy

@@ -14,7 +14,7 @@
 section\<open>An example ontology for a math paper\<close>
 
 theory small_math
-   imports "Isabelle_DOF.Isa_COL"
+   imports "Isabelle_DOF.DOF_Shallow"
 begin
 
 doc_class title =

src/tests/ROOT

@@ -9,6 +9,5 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" +
     "Evaluation"
     "High_Level_Syntax_Invariants"
     "Ontology_Matching_Example"
-    "Reification_Test"
   theories [condition = ISABELLE_DOF_HOME]
     "Isabelle2022"