Add definition* command first draft

Use metalogic to generate meta term anti-quotations

The idea is for the Very_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 reading the notations
(mixfixes) of the term-antiquotations, after the metalogic
is sourced, is used.

Example:

With shallow:

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

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

You get:

find_consts name:"Isabelle_DOF_typ"

find_consts
  name: "Isabelle_DOF_typ"

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

With Deep:

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

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

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

You get:

find_consts name:"Isabelle_DOF_typ"

find_consts
  name: "Isabelle_DOF_typ"

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

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

Then new interpretation of term anti-quotations is available
for the user.

.gitignore

@@ -2,3 +2,4 @@ output
 .afp
 *~
 *#
+Isabelle_DOF-Unit-Tests/latex_test/

.woodpecker/build.yml

@@ -2,14 +2,17 @@ pipeline:
   build:
     image: docker.io/logicalhacking/isabelle2022
     commands:
+      - ./.woodpecker/check_dangling_theories
+      - ./.woodpecker/check_external_file_refs
+      - ./.woodpecker/check_quick_and_dirty -w
       - export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
       - mkdir -p $ARTIFACT_DIR
       - export `isabelle getenv ISABELLE_HOME_USER`
       - mkdir -p $ISABELLE_HOME_USER/etc
       - echo "ISABELLE_PDFLATEX=\"$LATEX --file-line-error\"" >> $ISABELLE_HOME_USER/etc/settings
-      - isabelle components -u `pwd` 
-      - isabelle build -D . -o browser_info
-      - isabelle dof_mkroot DOF_test
+      - isabelle build -v -x HOL-Proofs -x Isabelle_DOF-Proofs -D . -o browser_info
+      - isabelle components -u .
+      - isabelle dof_mkroot -q DOF_test
       - isabelle build -D DOF_test
       - cp -r $ISABELLE_HOME_USER/browser_info $ARTIFACT_DIR
       - cd $ARTIFACT_DIR

.woodpecker/check_dangling_theories

@@ -0,0 +1,33 @@
+#!/bin/bash
+
+set -e
+
+failuremsg="Error"
+failurecode=1
+
+while [ $# -gt 0 ]
+do
+    case "$1" in
+        --warning|-w)
+            failuremsg="Warning"
+            failurecode=0;;
+    esac
+    shift
+done
+
+echo "Checking for theories that are not part of an Isabelle session:"
+echo "==============================================================="
+
+PWD=`pwd`
+TMPDIR=`mktemp -d`
+isabelle build  -D . -l -n | grep $PWD | sed -e "s| *${PWD}/||" | sort -u | grep thy$ > ${TMPDIR}/sessions-thy-files.txt
+find * -type f | sort -u | grep thy$ > ${TMPDIR}/actual-thy-files.txt
+thylist=`comm -13 ${TMPDIR}/sessions-thy-files.txt ${TMPDIR}/actual-thy-files.txt`
+if [ -z "$thylist" ] ; then
+    echo "  * Success: No dangling theories found."
+    exit 0
+else
+    echo -e "$thylist"
+    echo "$failuremsg: Dangling theories found (see list above)!" 
+    exit $failurecode 
+fi

.woodpecker/check_external_file_refs

@@ -0,0 +1,45 @@
+#!/bin/sh
+
+
+
+failuremsg="Error"
+failurecode=1
+
+while [ $# -gt 0 ]
+do
+    case "$1" in
+        --warning|-w)
+            failuremsg="Warning"
+            failurecode=0;;
+    esac
+    shift
+done
+
+DIRREGEXP="\\.\\./"
+
+echo "Checking for references pointing outside of session directory:"
+echo "=============================================================="
+
+REGEXP=$DIRREGEXP
+DIR=$DIRMATCH
+failed=0
+for i in $(seq 1 10); do 
+  FILES=`find * -mindepth $((i-1)) -maxdepth $i -type f | xargs`
+  if [ -n "$FILES" ]; then 
+    grep -s ${REGEXP} ${FILES}
+    exit=$?
+    if [ "$exit" -eq 0 ] ; then
+      failed=1
+    fi
+  fi
+  REGEXP="${DIRREGEXP}${REGEXP}"
+done
+
+
+if [ "$failed" -ne 0 ] ; then
+    echo "$failuremsg: Forbidden reference to files outside of their session directory!" 
+    exit $failurecode 
+fi
+
+echo "  * Success: No relative references to files outside of their session directory found."
+exit 0

.woodpecker/check_quick_and_dirty

@@ -0,0 +1,30 @@
+#!/bin/bash
+
+set -e
+
+failuremsg="Error"
+failurecode=1
+
+while [ $# -gt 0 ]
+do
+    case "$1" in
+        --warning|-w)
+            failuremsg="Warning"
+            failurecode=0;;
+    esac
+    shift
+done
+
+echo "Checking for sessions with quick_and_dirty mode enabled:"
+echo "========================================================"
+
+rootlist=`find -name 'ROOT' -exec grep -l 'quick_and_dirty *= *true' {} \;`
+
+if [ -z "$rootlist" ] ; then
+    echo "  * Success: No sessions with quick_and_dirty mode enabled found."
+    exit 0
+else
+    echo -e "$rootlist"
+    echo "$failuremsg: Sessions with quick_and_dirty mode enabled found (see list above)!" 
+    exit $failurecode 
+fi

.woodpecker/mk_release

@@ -83,22 +83,22 @@ build_and_install_manuals()
     if [ "$DIRTY" = "true" ]; then
         if [ -z ${ARTIFACT_DIR+x} ]; then
             echo "  * Quick and Dirty Mode (local build)"
-            $ISABELLE build -d . Isabelle_DOF-Manual 2018-cicm-isabelle_dof-applications
-            mkdir -p $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
-            cp examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/document.pdf \
-               $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
-            mkdir -p $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/
-            cp examples/technical_report/Isabelle_DOF-Manual/output/document.pdf \
-               $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/;
+            $ISABELLE build -d . Isabelle_DOF Isabelle_DOF-Example-Scholarly_Paper
+            mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF-Example-Scholarly_Paper/output/
+            cp Isabelle_DOF-Example-Scholarly_Paper/output/document.pdf \
+               $ISADOF_WORK_DIR/Isabelle_DOF-Example-Scholarly_Paper/output/
+            mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF/output/
+            cp Isabelle_DOF/output/document.pdf \
+               $ISADOF_WORK_DIR/Isabelle_DOF/output/;
         else
             echo "  * Quick and Dirty Mode (running on CI)"
-            mkdir -p $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
-            cp $ARTIFACT_DIR/browser_info/Unsorted/2018-cicm-isabelle_dof-applications/document.pdf \
-               $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
+            mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF-Example-Scholarly_Paper/output/
+            cp $ARTIFACT_DIR/browser_info/Unsorted/Isabelle_DOF-Example-Scholarly_Paper/document.pdf \
+               $ISADOF_WORK_DIR/Isabelle_DOF-Example-Scholarly_Paper/output/
  
-            mkdir -p $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/
-            cp $ARTIFACT_DIR/browser_info/Unsorted/Isabelle_DOF-Manual/document.pdf \
-               $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/;
+            mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF/output/
+            cp $ARTIFACT_DIR/browser_info/Unsorted/Isabelle_DOF/document.pdf \
+               $ISADOF_WORK_DIR/Isabelle_DOF/output/;
         fi
     else
         (cd $ISADOF_WORK_DIR && $ISABELLE env ./install-afp)
@@ -107,13 +107,13 @@ build_and_install_manuals()
     mkdir -p $ISADOF_WORK_DIR/doc
     echo "Isabelle/DOF Manuals!" > $ISADOF_WORK_DIR/doc/Contents
     
-    cp $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/document.pdf \
+    cp $ISADOF_WORK_DIR/Isabelle_DOF/output/document.pdf \
         $ISADOF_WORK_DIR/doc/Isabelle_DOF-Manual.pdf
     echo "  Isabelle_DOF-Manual                       User and Implementation Manual for Isabelle/DOF" >> $ISADOF_WORK_DIR/doc/Contents
 
-    cp $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/document.pdf \
-        $ISADOF_WORK_DIR/doc/2018-cicm-isabelle_dof-applications.pdf
-    echo "  2018-cicm-isabelle_dof-applications       Example academic paper" >> $ISADOF_WORK_DIR/doc/Contents
+    cp $ISADOF_WORK_DIR/Isabelle_DOF-Example-Scholarly_Paper/output/document.pdf \
+        $ISADOF_WORK_DIR/doc/Isabelle_DOF-Example-Scholarly_Paper.pdf
+    echo "  Isabelle_DOF-Example-Scholarly_Paper       Example academic paper" >> $ISADOF_WORK_DIR/doc/Contents
 
     find $ISADOF_WORK_DIR -type d -name "output" -exec rm -rf {} \; &> /dev/null || true
     rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.woodpecker $ISADOF_WORK_DIR/.afp 
@@ -143,7 +143,6 @@ publish_archive()
     ssh 0x5f.org chmod go+u-w -R www/$DOF_ARTIFACT_HOST/htdocs/$DOF_ARTIFACT_DIR
 }
 
-
 ISABELLE=`which isabelle`
 USE_TAG="false"
 SIGN="false"
@@ -194,8 +193,8 @@ for i in $VARS; do
         export "$i"
 done
 
-ISABELLE_VERSION="Isabelle$($ISABELLE_TOOL options -g dof_isabelle)"
-DOF_VERSION="$($ISABELLE_TOOL options -g dof_version)"
+ISABELLE_VERSION="Isabelle$($ISABELLE_TOOL dof_param -b isabelle_version)"
+DOF_VERSION="$($ISABELLE_TOOL dof_param -b dof_version)"
 
 ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
 ISADOF_TAR="Isabelle_DOF-"$DOF_VERSION"_"$ISABELLE_SHORT_VERSION
@@ -221,4 +220,3 @@ fi
 
 rm -rf $BUILD_DIR
 
-exit 0 

Isabelle_DOF-Example-Extra/CC_ISO15408/PikeOS_study/PikeOS_ST.thy

@@ -1,7 +1,6 @@
 theory PikeOS_ST (*Security Target *)
 
-imports "../../../src/ontologies/CC_v3.1_R5/CC_v3_1_R5"
-        (*  Isabelle_DOF.CC_v3_1_R5 in the future.  *)
+imports "Isabelle_DOF-Ontologies.CC_v3_1_R5"
 
 begin 
 
@@ -18,18 +17,20 @@ text*[pkosstref::st_ref_cls, title="''PikeOS Security Target''", st_version ="(0
  It complies with the Common Criteria for Information Technology Security Evaluation 
  Version 3.1 Revision 4.\<close>
 
+
+
 subsection*[pkossttoerefsubsec::st_ref_cls]\<open>TOE Reference\<close>
 
 text*[pkostoeref::toe_ref_cls, dev_name="''''", toe_name="''PikeOS''",
       toe_version= "(0,3,4)", prod_name="Some ''S3725''"]
-\<open>The @{docitem toe_def} is the operating system PikeOS version 3.4 
+\<open>The @{docitem toeDef} is the operating system PikeOS version 3.4 
    running on the microprocessor family x86 hosting different applications. 
-   The @{docitem toe_def} is referenced as PikeOS 3.4 base
+   The @{docitem toeDef} is referenced as PikeOS 3.4 base
    product build S3725 for Linux and Windows development host with PikeOS 3.4
    Certification Kit build S4250 and PikeOS 3.4 Common Criteria Kit build S4388.\<close>
 
 subsection*[pkossttoeovrvwsubsec::st_ref_cls]\<open> TOE Overview \<close>
-text*[pkosovrw1::toe_ovrw_cls]\<open>The @{definition \<open>toe\<close> } is a special kind of operating 
+text*[pkosovrw1::toe_ovrw_cls]\<open>The @{docitem \<open>toeDef\<close> } is a special kind of operating 
 system, that allows to effectively separate
 different applications running on the same platform from each other. The TOE can host
 user applications that can also be operating systems. User applications can also be
@@ -87,4 +88,4 @@ open_monitor*[PikosSR::SEC_REQ_MNT]
 close_monitor*[PikosSR]
 
 close_monitor*[stpkos]
-end
+end

Isabelle_DOF-Example-Extra/CC_ISO15408/PikeOS_study/ROOT

@@ -0,0 +1,4 @@
+session "PikeOS_study" = "Isabelle_DOF-Ontologies" +
+  options [document = false]
+  theories
+    "PikeOS_ST"

Isabelle_DOF-Example-Extra/CC_ISO15408/ROOTS

@@ -0,0 +1 @@
+PikeOS_study

Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/ROOT

@@ -1,7 +1,5 @@
-session "mini_odo" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output", document_build = dof,
-           dof_ontologies = "Isabelle_DOF.technical_report Isabelle_DOF.cenelec_50128", 
-           dof_template = "Isabelle_DOF.scrreprt-modern"]
+session "mini_odo" = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof]
   sessions 
     "Physical_Quantities"
   theories

Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/mini_odo.thy

@@ -15,10 +15,12 @@
 theory 
   mini_odo
 imports  
-  "Isabelle_DOF.CENELEC_50128" 
+  "Isabelle_DOF-Ontologies.CENELEC_50128" 
   "Isabelle_DOF.technical_report"
   "Physical_Quantities.SI" "Physical_Quantities.SI_Pretty"
 begin
+use_template "scrreprt-modern"
+use_ontology technical_report and "Isabelle_DOF-Ontologies.CENELEC_50128"
 declare[[strict_monitor_checking=true]]
 define_shortcut* dof     \<rightleftharpoons> \<open>\dof\<close>
                  isadof  \<rightleftharpoons> \<open>\isadof{}\<close>
@@ -294,7 +296,7 @@ and the global model parameters such as wheel diameter, the number of teeth per
 sampling frequency etc., we can infer the maximal time of service as well the maximum distance 
 the device can measure.  As an example configuration, choosing:
 
-   \<^item> \<^term>\<open>(1 *\<^sub>Q metre)::real[m]\<close>      for  \<^term>\<open>w\<^sub>d\<close>   (wheel-diameter), 
+   \<^item> \<^term>\<open>(1 *\<^sub>Q metre):: real[m]\<close>      for  \<^term>\<open>w\<^sub>d\<close>   (wheel-diameter), 
    \<^item> \<^term>\<open>100         :: real\<close>        for  \<^term>\<open>tpw\<close> (teeth per wheel), 
    \<^item> \<^term>\<open>80 *\<^sub>Q kmh   :: real[m\<cdot>s\<^sup>-\<^sup>1]\<close>  for  \<^term>\<open>Speed\<^sub>M\<^sub>a\<^sub>x\<close>,
    \<^item> \<^term>\<open>14.4 *\<^sub>Q kHz :: real[s\<^sup>-\<^sup>1]\<close>    for the sampling frequency,
@@ -626,14 +628,14 @@ text\<open>
 \<close>
 
 text\<open>Examples for declaration of typed doc-classes "assumption" (sic!) and "hypothesis" (sic!!),
-     concepts defined in the underlying ontology @{theory "Isabelle_DOF.CENELEC_50128"}. \<close>
+     concepts defined in the underlying ontology @{theory "Isabelle_DOF-Ontologies.CENELEC_50128"}. \<close>
 text*[ass2::assumption, long_name="Some ''assumption one''"] \<open> The subsystem Y is safe. \<close>
 text*[hyp1::hypothesis] \<open> \<open>P \<noteq> NP\<close> \<close>
   
 text\<open>  
-   A real example fragment fsrom a larger project, declaring a text-element as a
+   A real example fragment from a larger project, declaring a text-element as a
    "safety-related application condition", a concept defined in the 
-   @{theory "Isabelle_DOF.CENELEC_50128"} ontology:\<close>  
+   @{theory "Isabelle_DOF-Ontologies.CENELEC_50128"} ontology:\<close>  
 
 text*[hyp2::hypothesis]\<open>Under the assumption @{assumption \<open>ass2\<close>} we establish the following: ... \<close>
 
@@ -654,9 +656,9 @@ text*[t10::test_result]
   test-execution via, \<^eg>, a makefile or specific calls to a test-environment or test-engine. \<close>
 
 
-text
-\<open>  Finally some examples of references to doc-items, i.e. text-elements 
-   with declared  meta-information and status. \<close> 
+text \<open> Finally some examples of references to doc-items, i.e. text-elements 
+       with declared  meta-information and status. \<close> 
+
 text \<open> As established by @{test_result (unchecked) \<open>t10\<close>}, 
                          @{test_result (define) \<open>t10\<close>} \<close>
 text \<open> the               @{test_result \<open>t10\<close>}                      

Isabelle_DOF-Example-Extra/ROOTS

@@ -1,3 +1,5 @@
 scholarly_paper
 technical_report
 CENELEC_50128
+cytology
+CC_ISO15408

Isabelle_DOF-Example-Extra/cytology/Cytology.thy

@@ -68,7 +68,7 @@ onto_class procaryotic_cells = cell +
 
 onto_class eucaryotic_cells = cell + 
     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"
+    invariant has_nucleus :: "\<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"
@@ -78,13 +78,10 @@ value "is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s (mk\<^sub>n\<^
 
 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>
-
-value \<open>has_nucleus_inv(eucaryotic_cells.make X Y Z Z Z [] 3 
-                         [upcast\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s (nucleus.make a b c d [])])\<close>
+value \<open>(eucaryotic_cells.organelles(eucaryotic_cells.make X Y Z Z Z [] []))\<close>
 
+value \<open>has_nucleus_inv(eucaryotic_cells.make X Y Z Z Z [] [])\<close>
 
+value \<open>has_nucleus_inv(eucaryotic_cells.make X Y Z Z Z [] [upcast\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s (nucleus.make a b c )])\<close>
 
 end

Isabelle_DOF-Example-Extra/cytology/ROOT

@@ -0,0 +1,4 @@
+session "Cytology" = "Isabelle_DOF" +
+  options [document = false]
+  theories
+    "Cytology"

Isabelle_DOF-Example-Extra/scholarly_paper/2020-iFM-CSP/ROOT

@@ -1,6 +1,5 @@
 session "2020-iFM-csp" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output", document_build = dof,
-  dof_ontologies = "Isabelle_DOF.scholarly_paper", dof_template = Isabelle_DOF.scrartcl]
+  options [document = pdf, document_output = "output", document_build = dof]
   theories
     "paper"
   document_files

Isabelle_DOF-Example-Extra/scholarly_paper/2020-iFM-CSP/document/root.bib

@@ -6870,7 +6870,7 @@ isbn="978-3-540-48509-4"
   title		= {{Isabelle's} Logic: {HOL}},
   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
   year		= 2009,
-  misc		= {\url{http://isabelle.in.tum.de/library/HOL/}}
+  misc		= {\url{https://isabelle.in.tum.de/library/HOL/}}
 }
 
 @InProceedings{	  garson.ea:security:2008,
@@ -11000,7 +11000,7 @@ isbn="978-1-4471-3182-3"
   journal = {Archive of Formal Proofs},
   month   = apr,
   year    = 2019,
-  note    = {\url{http://isa-afp.org/entries/HOL-CSP.html}},
+  note    = {\url{https://isa-afp.org/entries/HOL-CSP.html}},
   ISSN    = {2150-914x},
 }
 

Isabelle_DOF-Example-Extra/scholarly_paper/2020-iFM-CSP/paper.thy

@@ -3,6 +3,8 @@ theory "paper"
   imports "Isabelle_DOF.scholarly_paper"
 begin
 
+use_template "scrartcl"
+use_ontology "scholarly_paper"
 
 open_monitor*[this::article]
 
@@ -50,7 +52,7 @@ abstract*[abs, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Alg
 \<close>
 text\<open>\<close>
 section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]\<open> Introduction \<close> 
-text*[introtext::introduction]\<open>
+text*[introtext::introduction, level="Some 1"]\<open>
 Communicating Sequential Processes (\<^csp>) is a language 
 to specify and verify patterns of interaction of concurrent systems.
 Together with CCS and LOTOS, it belongs to the family of \<^emph>\<open>process algebras\<close>. 
@@ -152,7 +154,7 @@ processes \<open>Skip\<close> (successful termination) and \<open>Stop\<close> (
 \<open>\<T>(Skip) = \<T>(Stop) = {[]}\<close>.
 Note that the trace sets, representing all \<^emph>\<open>partial\<close> history, is in general prefix closed.\<close>
 
-text*[ex1::math_example, status=semiformal] \<open>
+text*[ex1::math_example, status=semiformal, level="Some 1"] \<open>
 Let two processes be defined as follows:
 
   \<^enum>  \<open>P\<^sub>d\<^sub>e\<^sub>t = (a \<rightarrow> Stop) \<box> (b \<rightarrow> Stop)\<close>
@@ -352,7 +354,7 @@ Roscoe and Brooks @{cite "Roscoe1992AnAO"} finally proposed another ordering, ca
 that completeness could at least be assured for read-operations. This more complex ordering 
 is based on the concept \<^emph>\<open>refusals after\<close> a trace \<open>s\<close> and defined by \<open>\<R> P s \<equiv> {X | (s, X) \<in> \<F> P}\<close>.\<close>
 
-Definition*[process_ordering, short_name="''process ordering''"]\<open>
+Definition*[process_ordering, level= "Some 2", short_name="''process ordering''"]\<open>
 We define \<open>P \<sqsubseteq> Q \<equiv> \<psi>\<^sub>\<D> \<and> \<psi>\<^sub>\<R> \<and> \<psi>\<^sub>\<M> \<close>,  where 
 \<^enum>  \<open>\<psi>\<^sub>\<D> = \<D> P \<supseteq> \<D> Q \<close>
 \<^enum> \<open>\<psi>\<^sub>\<R> = s \<notin> \<D> P \<Rightarrow> \<R> P s = \<R> Q s\<close>  
@@ -528,10 +530,10 @@ To handle termination better, we added two new processes \<open>CHAOS\<^sub>S\<^
 \<close>
 
 (*<*) (* a test ...*)
-text*[X22 ::math_content   ]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close>                           \<close>
-text*[X32::"definition", mcc=defn]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>        \<close>
-Definition*[X42]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>  \<close>
-Definition*[X52::"definition"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
+text*[X22 ::math_content, level="Some 2"  ]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close>                           \<close>
+text*[X32::"definition", level="Some 2", mcc=defn]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>        \<close>
+Definition*[X42, level="Some 2"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>  \<close>
+Definition*[X52::"definition", level="Some 2"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
 
 text\<open> The \<open>RUN\<close>-process defined @{math_content X22} represents the process that accepts all 
 events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in two variants shown in 
@@ -539,11 +541,11 @@ events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in
 stops or accepts any offered event, whereas \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<close> can additionally terminate.\<close>
 (*>*)
 
-Definition*[X2]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close>                    \<close>
-Definition*[X3]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>         \<close>
-Definition*[X4]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>\<close>
-Definition*[X5]\<open>\<open>DF A \<equiv> \<mu> X. (\<sqinter> x \<in> A \<rightarrow> X)\<close>                       \<close>
-Definition*[X6]\<open>\<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. ((\<sqinter> x \<in> A \<rightarrow> X) \<sqinter> SKIP)\<close>          \<close> 
+Definition*[X2, level="Some 2"]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close>                    \<close>
+Definition*[X3, level="Some 2"]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>         \<close>
+Definition*[X4, level="Some 2"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>\<close>
+Definition*[X5, level="Some 2"]\<open>\<open>DF A \<equiv> \<mu> X. (\<sqinter> x \<in> A \<rightarrow> X)\<close>                       \<close>
+Definition*[X6, level="Some 2"]\<open>\<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. ((\<sqinter> x \<in> A \<rightarrow> X) \<sqinter> SKIP)\<close>          \<close> 
 
 text\<open>In the following, we denote \<open> \<R>\<P> = {DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\<close>. 
 All five  reference processes are divergence-free.
@@ -605,16 +607,16 @@ handled separately. One contribution of our work is establish their precise rela
 the Failure/Divergence Semantics of \<^csp>.\<close>
 
 (* bizarre: Definition* does not work for this single case *)
-text*[X10::"definition"]\<open> \<open>deadlock\<^sub>-free P \<equiv>  DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close>  \<close>
+text*[X10::"definition", level="Some 2"]\<open> \<open>deadlock\<^sub>-free P \<equiv>  DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close>  \<close>
 
 text\<open>\<^noindent> A process \<open>P\<close> is deadlock-free if and only if after any trace \<open>s\<close> without \<open>\<surd>\<close>, the union of \<open>\<surd>\<close> 
 and all events of \<open>P\<close> can never be a refusal set associated to \<open>s\<close>, which means that \<open>P\<close> cannot 
 be deadlocked after any non-terminating trace.   
 \<close>
 
-Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"]
+Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>", level="Some 2"]
 \<open> \hfill \break \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<close>   
-Definition*[X11]\<open>  \<open>livelock\<^sub>-free P \<equiv> \<D> P = {} \<close>   \<close>
+Definition*[X11, level="Some 2"]\<open>  \<open>livelock\<^sub>-free P \<equiv> \<D> P = {} \<close>   \<close>
 
 text\<open> Recall that all five reference processes are livelock-free. 
 We also have the following lemmas about the 
@@ -628,7 +630,7 @@ text\<open>
 Finally, we proved the following theorem that confirms the relationship between the two vital
 properties:
 \<close>
-Theorem*[T2, short_name="''DF implies LF''"]
+Theorem*[T2, short_name="''DF implies LF''", level="Some 2"]
   \<open>  \<open>deadlock_free P \<longrightarrow> livelock_free P\<close>   \<close>
 
 text\<open>
@@ -795,7 +797,7 @@ This normal form is closed under deterministic and  communication operators.
 The advantage of this format is that we can mimick the well-known product automata construction
 for an arbitrary number of synchronized processes under normal form.
 We only show the case of the synchronous product of two processes: \<close>
-text*[T3::"theorem", short_name="\<open>Product Construction\<close>"]\<open>
+text*[T3::"theorem", short_name="\<open>Product Construction\<close>", level="Some 2"]\<open>
 Parallel composition translates to normal form:
 @{cartouche [display,indent=5]\<open>(P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>1,\<upsilon>\<^sub>1\<rbrakk> \<sigma>\<^sub>1) || (P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>2,\<upsilon>\<^sub>2\<rbrakk> \<sigma>\<^sub>2) = 
     P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2). \<tau>\<^sub>1 \<sigma>\<^sub>1 \<inter> \<tau>\<^sub>2 \<sigma>\<^sub>2 , \<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2).\<lambda>e.(\<upsilon>\<^sub>1 \<sigma>\<^sub>1 e, \<upsilon>\<^sub>2 \<sigma>\<^sub>2 e)\<rbrakk> (\<sigma>\<^sub>1,\<sigma>\<^sub>2)\<close>}
@@ -815,7 +817,7 @@ states via the closure \<open>\<RR>\<close>, which is defined inductively over:
 Thus, normalization leads to a new characterization of deadlock-freeness inspired 
 from automata theory. We formally proved the following theorem:\<close>
 
-text*[T4::"theorem", short_name="\<open>DF vs. Reacheability\<close>"]
+text*[T4::"theorem", short_name="\<open>DF vs. Reacheability\<close>", level="Some 2"]
 \<open> If each reachable state \<open>s \<in> (\<RR> \<tau> \<upsilon>)\<close> has outgoing transitions,
 the \<^csp> process is deadlock-free: 
 @{cartouche [display,indent=10] \<open>\<forall>\<sigma> \<in> (\<RR> \<tau> \<upsilon> \<sigma>\<^sub>0). \<tau> \<sigma> \<noteq> {} \<Longrightarrow> deadlock_free (P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>,\<upsilon>\<rbrakk> \<sigma>\<^sub>0)\<close>}

Isabelle_DOF-Example-Extra/scholarly_paper/ROOTS

@@ -0,0 +1 @@
+2020-iFM-CSP

Isabelle_DOF-Example-Extra/technical_report/ROOTS

@@ -1,2 +1 @@
-Isabelle_DOF-Manual
 TR_my_commented_isabelle

Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/ROOT

@@ -1,7 +1,5 @@
 session "TR_MyCommentedIsabelle" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output", document_build = dof,
-           dof_ontologies = "Isabelle_DOF.technical_report", dof_template = Isabelle_DOF.scrreprt,
-    quick_and_dirty = true]
+  options [document = pdf, document_output = "output", document_build = dof]
   theories
     "TR_MyCommentedIsabelle"
   document_files

Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy

@@ -14,9 +14,11 @@
 (*<*)
 theory TR_MyCommentedIsabelle
   imports "Isabelle_DOF.technical_report" 
-
 begin
 
+use_template "scrreprt"
+use_ontology "technical_report"
+
 define_shortcut* isabelle \<rightleftharpoons> \<open>Isabelle/HOL\<close>
 
 open_monitor*[this::report] 
@@ -62,7 +64,7 @@ text\<open> \<^vs>\<open>-0.5cm\<close>
   Isabelle and Isabelle/HOL, a complementary text to the unfortunately somewhat outdated 
   "The Isabelle Cookbook" in \<^url>\<open>https://nms.kcl.ac.uk/christian.urban/Cookbook/\<close>. 
   The present text is also complementary to the current version of 
-  \<^url>\<open>https://isabelle.in.tum.de/dist/Isabelle2021/doc/isar-ref.pdf\<close>
+  \<^url>\<open>https://isabelle.in.tum.de/doc/isar-ref.pdf\<close>
   "The Isabelle/Isar Implementation" by Makarius Wenzel in that it focusses on subjects
   not covered there, or presents alternative explanations for which I believe, based on my 
   experiences with students and Phds, that they are helpful.
@@ -364,7 +366,7 @@ subsection*[t213::example]\<open>Mechanism 2 : Extending the Global Context \<op
 
 text\<open>A central mechanism for constructing user-defined data is by the \<^ML_functor>\<open>Generic_Data\<close>-functor.
   A plugin needing some data \<^verbatim>\<open>T\<close> and providing it with implementations for an 
-  \<^verbatim>\<open>empty\<close>, and operations  \<^verbatim>\<open>merge\<close> and \<^verbatim>\<open>extend\<close>, can construct a lense with operations
+  \<^verbatim>\<open>empty\<close>, and operation \<^verbatim>\<open>merge\<close>, can construct a lense with operations
   \<^verbatim>\<open>get\<close> and \<^verbatim>\<open>put\<close> that attach this data into the generic system context. Rather than using
   unsynchronized SML mutable variables, this is the mechanism to introduce component local
   data in Isabelle, which allows to manage this data for the necessary backtrack and synchronization
@@ -373,14 +375,12 @@ text\<open>A central mechanism for constructing user-defined data is by the \<^M
 ML \<open>
      datatype X = mt
      val init = mt;
-     val ext = I
      fun merge (X,Y) = mt
      
      structure Data = Generic_Data
      (
        type T = X
        val empty  = init
-       val extend = ext
        val merge  = merge
      );  
 \<close>
@@ -1637,7 +1637,7 @@ val data = \<comment> \<open>Derived from Yakoub's example ;-)\<close>
   , (\<open>Frédéric II\<close>,   \<open>King of Sicily\<close>)
   , (\<open>Frédéric III\<close>,  \<open>the Handsome\<close>)
   , (\<open>Frédéric IV\<close>,   \<open>of the Empty Pockets\<close>)
-  , (\<open>Frédéric V\<close>,    \<open>King of Denmark–Norway\<close>)
+  , (\<open>Frédéric V\<close>,    \<open>King of Denmark-Norway\<close>)
   , (\<open>Frédéric VI\<close>,   \<open>the Knight\<close>)
   , (\<open>Frédéric VII\<close>,  \<open>Count of Toggenburg\<close>)
   , (\<open>Frédéric VIII\<close>, \<open>Count of Zollern\<close>)

Isabelle_DOF-Example-Scholarly_Paper/IsaDofApplications.thy

@@ -16,6 +16,9 @@ theory IsaDofApplications
   imports "Isabelle_DOF.scholarly_paper"
 begin
 
+use_template "lncs"
+use_ontology "Isabelle_DOF.scholarly_paper"
+
 open_monitor*[this::article] 
 declare[[strict_monitor_checking=false]]
 
@@ -71,7 +74,7 @@ abstract*[abs::abstract, keywordlist="[''Ontology'',''Ontological Modeling'',''I
 \<close>
 
 section*[intro::introduction]\<open> Introduction \<close>  
-text*[introtext::introduction]\<open> 
+text*[introtext::introduction, level = "Some 1"]\<open> 
 The linking of the \<^emph>\<open>formal\<close> to the \<^emph>\<open>informal\<close> is perhaps the
 most pervasive challenge in the digitization of knowledge and its
 propagation. This challenge incites numerous research efforts
@@ -120,7 +123,7 @@ declare_reference*[ontomod::text_section]
 declare_reference*[ontopide::text_section]
 declare_reference*[conclusion::text_section]
 (*>*)
-text*[plan::introduction]\<open> The plan of the paper is follows: we start by introducing  the underlying 
+text*[plan::introduction, level="Some 1"]\<open> The plan of the paper is follows: we start by introducing  the underlying 
 Isabelle system (@{text_section (unchecked) \<open>bgrnd\<close>}) followed by presenting the 
 essentials of  \<^isadof> and its ontology language (@{text_section (unchecked) \<open>isadof\<close>}). 
 It follows @{text_section (unchecked) \<open>ontomod\<close>}, where we present three application 
@@ -130,7 +133,7 @@ conclusions and discuss related work in @{text_section (unchecked) \<open>conclu
 
 section*[bgrnd::text_section,main_author="Some(@{docitem ''bu''}::author)"]
         \<open> Background: The Isabelle System \<close>
-text*[background::introduction]\<open>
+text*[background::introduction, level="Some 1"]\<open>
 While Isabelle is widely perceived as an interactive theorem prover
 for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we
 would like to emphasize the view that Isabelle is far more than that:
@@ -159,7 +162,7 @@ figure*[architecture::figure,relative_width="100",src="''figures/isabelle-archit
      asynchronous communication between the Isabelle system and 
      the IDE (right-hand side). \<close>
 
-text*[blug::introduction]\<open> The Isabelle system architecture shown in @{figure \<open>architecture\<close>}
+text*[blug::introduction, level="Some 1"]\<open> The Isabelle system architecture shown in @{figure \<open>architecture\<close>}
  comes with many layers, with Standard ML (SML) at the bottom layer as implementation 
 language. The architecture actually foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which 
 resides in the SML structure \<^ML_structure>\<open>Context\<close>. This structure provides a kind of container called 
@@ -191,7 +194,7 @@ For the antiquotation \inlineisar+\at{value "fac 5"}+  we assume the usual defin
 \inlineisar+fac+ in HOL.
 \<close>
 
-text*[anti]\<open> Thus, antiquotations can refer to formal content, can be type-checked before being 
+text*[anti::introduction, level = "Some 1"]\<open> Thus, antiquotations can refer to formal content, can be type-checked before being 
 displayed and can be used for calculations before actually being typeset. When editing, 
 Isabelle's PIDE offers auto-completion and error-messages while typing the above 
 \<^emph>\<open>semi-formal\<close> content.  \<close>

Isabelle_DOF-Example-Scholarly_Paper/ROOT

@@ -1,7 +1,5 @@
-session "2018-cicm-isabelle_dof-applications" = "Isabelle_DOF" + 
-  options  [document = pdf, document_output = "output", document_build = dof,
-   dof_ontologies = "Isabelle_DOF.scholarly_paper", dof_template = Isabelle_DOF.lncs, 
-   quick_and_dirty = true]
+session "Isabelle_DOF-Example-Scholarly_Paper" (AFP) = "Isabelle_DOF" + 
+  options [document = pdf, document_output = "output", document_build = dof]
   theories
     IsaDofApplications
   document_files
@@ -9,7 +7,6 @@ session "2018-cicm-isabelle_dof-applications" = "Isabelle_DOF" +
     "authorarchive.sty"
     "preamble.tex"
     "lstisadof.sty"
-    "vector_iD_icon.pdf"
     "figures/isabelle-architecture.pdf"
     "figures/Dogfood-Intro.png"
     "figures/InteractiveMathSheet.png"

Isabelle_DOF-Example-Scholarly_Paper/document/authorarchive.sty

@@ -1,4 +1,4 @@
-%% Copyright (C) 2008-2019 Achim D. Brucker, https://www.brucker.ch
+%% Copyright (C) 2008-2023 Achim D. Brucker, https://www.brucker.ch
 %%
 %% License:
 %%   This program can be redistributed and/or modified under the terms
@@ -11,21 +11,22 @@
 %%   SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
 \NeedsTeXFormat{LaTeX2e}\relax
 \ProvidesPackage{authorarchive}
-  [0000/00/00 Unreleased v1.1.1+%
+  [2023/02/10 v1.3.0
   Self-archiving information for scientific publications.]
 %
 \PassOptionsToPackage{hyphens}{url}
 %
 \RequirePackage{ifthen}
 \RequirePackage[inline]{enumitem}
-\RequirePackage{graphicx}
+\RequirePackage{orcidlink}
 \RequirePackage{eso-pic}
 \RequirePackage{intopdf}
 \RequirePackage{kvoptions}
 \RequirePackage{hyperref}
 \RequirePackage{calc}
 \RequirePackage{qrcode}
-\RequirePackage{hvlogos}
+\RequirePackage{etoolbox}
+\newrobustcmd\BibTeX{Bib\TeX}
 %
 %Better url breaking
 \g@addto@macro{\UrlBreaks}{\UrlOrds}
@@ -80,31 +81,51 @@
 }
 \ProcessKeyvalOptions*
 
-% Provide command for dynamic configuration seutp
-\def\authorsetup{\kvsetkeys{AA}}
+\newcommand{\AA@defIncludeFiles}{
+  \def\AA@bibBibTeX{\AA@bibtexdir/\AA@key.bib}
+  \def\AA@bibBibTeXLong{\AA@bibtexdir/\AA@key.bibtex}
+  \def\AA@bibWord{\AA@bibtexdir/\AA@key.word.xml}
+  \def\AA@bibEndnote{\AA@bibtexdir/\AA@key.enw}
+  \def\AA@bibRIS{\AA@bibtexdir/\AA@key.ris}
+}
+\AA@defIncludeFiles
+
+\newboolean{AA@bibExists}
+\setboolean{AA@bibExists}{false}
+\newcommand{\AA@defIncludeSwitches}{
+  \IfFileExists{\AA@bibBibTeX}{\setboolean{AA@bibExists}{true}}{}
+  \IfFileExists{\AA@bibBibTeXLong}{\setboolean{AA@bibExists}{true}}{}
+  \IfFileExists{\AA@bibWord}{\setboolean{AA@bibExists}{true}}{}
+  \IfFileExists{\AA@bibEndnote}{\setboolean{AA@bibExists}{true}}{}
+  \IfFileExists{\AA@bibRIS}{\setboolean{AA@bibExists}{true}}{}
+}
+\AA@defIncludeSwitches
+
+
+% Provide command for dynamic configuration setup
+% \def\authorsetup{\kvsetkeys{AA}}
+\newcommand{\authorsetup}[1]{%
+  \kvsetkeys{AA}{#1}
+  \AA@defIncludeFiles
+  \AA@defIncludeSwitches
+}
 
 % Load local configuration
 \InputIfFileExists{authorarchive.config}{}{}
 
+%  define proxy command for setting PDF attributes
+\ExplSyntaxOn
+\@ifundefined{pdfmanagement_add:nnn}{%
+    \newcommand{\AA@pdfpagesattribute}[2]{\pdfpagesattr{/#1 #2}}%
+ }{%
+    \newcommand{\AA@pdfpagesattribute}[2]{\pdfmanagement_add:nnn{Pages}{#1}{#2}}%
+ }%
+\ExplSyntaxOff
 
 \newlength\AA@x
 \newlength\AA@y
 \newlength\AA@width
 
-\def\AA@bibBibTeX{\AA@bibtexdir/\AA@key.bib}
-\def\AA@bibBibTeXLong{\AA@bibtexdir/\AA@key.bibtex}
-\def\AA@bibWord{\AA@bibtexdir/\AA@key.word.xml}
-\def\AA@bibEndnote{\AA@bibtexdir/\AA@key.enw}
-\def\AA@bibRIS{\AA@bibtexdir/\AA@key.ris}
-
-\newboolean{AA@bibExists}
-\setboolean{AA@bibExists}{false}
-\IfFileExists{\AA@bibBibTeX}{\setboolean{AA@bibExists}{true}}{}
-\IfFileExists{\AA@bibBibTeXLong}{\setboolean{AA@bibExists}{true}}{}
-\IfFileExists{\AA@bibWord}{\setboolean{AA@bibExists}{true}}{}
-\IfFileExists{\AA@bibEndnote}{\setboolean{AA@bibExists}{true}}{}
-\IfFileExists{\AA@bibRIS}{\setboolean{AA@bibExists}{true}}{}
-
 \setlength\AA@x{1in+\hoffset+\oddsidemargin}
 
 \newcommand{\authorcrfont}{\footnotesize}
@@ -148,8 +169,7 @@
 %%%% LNCS
 \ifAA@LNCS%
   \ifAA@orcidicon%
-    \renewcommand{\orcidID}[1]{\href{https://orcid.org/#1}{%
-      \textsuperscript{\,\includegraphics[height=2\fontcharht\font`A]{vector_iD_icon}}}}
+    \renewcommand{\orcidID}[1]{\orcidlink{#1}}
   \else\relax\fi%
 %  
   \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
@@ -157,23 +177,11 @@
   }{}
   \renewcommand{\authorcrfont}{\scriptsize}
   \@ifclasswith{llncs}{a4paper}{%
-    \ExplSyntaxOn
-    \@ifundefined{pdfmanagement_add:nnn}{%
-      \pdfpagesattr{/CropBox [92 114 523 780]}%
-    }{%
-      \pdfmanagement_add:nnn {Pages}{CropBox}{[92~114~523~780]}
-    }%
-    \ExplSyntaxOff
+    \AA@pdfpagesattribute{CropBox}{[92 114 523 780]}%
     \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},40){#1}}%
   }{%
-    \ExplSyntaxOn
-    \@ifundefined{pdfmanagement_add:nnn}{%
-      \pdfpagesattr{/CropBox [92 65 523 731]}% LNCS page: 152x235 mm
-    }{%
-      \pdfmanagement_add:nnn {Pages}{CropBox}{[92~62~523~731]}
-    }%
-    \ExplSyntaxOff
-    \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},23){#1}}
+    \AA@pdfpagesattribute{CropBox}{[92 65 523 731]}%
+    \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},23){#1}}%
   }
   \setlength{\AA@width}{\textwidth}
   \setcounter{tocdepth}{2}
@@ -186,7 +194,7 @@
   }{}
   \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},35){#1}}
   \renewcommand{\authorcrfont}{\scriptsize}
-  \pdfpagesattr{/CropBox [70 65 526.378 748.15]} % TODO
+  \AA@pdfpagesattribute{CropBox}{[70 65 526.378 748.15]}
   \setlength{\AA@width}{\textwidth}
   \setcounter{tocdepth}{2}
 \fi
@@ -218,8 +226,6 @@
   draft         = false,
   bookmarksopen = true,
   bookmarksnumbered= true,
-  pdfauthor     = {\@author},
-  pdftitle      = {\@title},
 }
 
 \@ifpackageloaded{totpages}{%
@@ -305,26 +311,26 @@
           \hfill
           \begin{itemize*}[label={}, itemjoin={,}]
             \IfFileExists{\AA@bibBibTeX}{%
-              \item \attachandlink{\AA@bibBibTeX}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}%
+              \item \expanded{\attachandlink[\AA@key.bib]{\AA@bibBibTeX}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}}%
             }{%
               \IfFileExists{\AA@bibBibTeXLong}{%
-                \item \attachandlink[\AA@key.bib]{\AA@bibBibTeXLong}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}%
+                \item \expanded{\attachandlink[\AA@key.bib]{\AA@bibBibTeXLong}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}}%
               }{%
                 \typeout{No file \AA@bibBibTeX{} (and no \AA@bibBibTeXLong) found. Not embedded reference in BibTeX format.}%
               }%
             }%
             \IfFileExists{\AA@bibWord}{%
-              \item \attachandlink{\AA@bibWord}[application/xml]{XML entry of this paper (e.g., for Word 2007 and later)}{Word}%
+              \item \expanded{\attachandlink[\AA@key.word.xml]{\AA@bibWord}[application/xml]{XML entry of this paper (e.g., for Word 2007 and later)}{Word}}%
             }{%
               \typeout{No file \AA@bibWord{} found. Not embedded reference for Word 2007 and later.}%
             }%
             \IfFileExists{\AA@bibEndnote}{%
-              \item \attachandlink{\AA@bibEndnote}[application/x-endnote-refer]{Endnote entry of this paper}{EndNote}%
+              \item \expanded{\attachandlink[\AA@key.enw]{\AA@bibEndnote}[application/x-endnote-refer]{Endnote entry of this paper}{EndNote}}%
             }{%
               \typeout{No file \AA@bibEndnote{} found. Not embedded reference in Endnote format.}%
             }%
             \IfFileExists{\AA@bibRIS}{%
-              \item \attachandlink{\AA@bibRIS}[application/x-research-info-systems]{RIS entry of this paper}{RIS}%
+              \item \expanded{\attachandlink[\AA@key.ris]{\AA@bibRIS}[application/x-research-info-systems]{RIS entry of this paper}{RIS}}%
             }{%
               \typeout{No file \AA@bibRIS{} found. Not embedded reference in RIS format.}%
             }%

Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy

@@ -10,15 +10,17 @@
  *   SPDX-License-Identifier: BSD-2-Clause
  *************************************************************************)
 
-chapter\<open>Common Criteria Definitions\<close>
+chapter\<open>Common Criteria\<close>
+section\<open>Terminology\<close>
 
 (*<<*)
 theory CC_terminology
 
-imports  "Isabelle_DOF.technical_report" 
+imports  
+"Isabelle_DOF.technical_report" 
 
 begin
-
+(*>>*)
 text\<open>We re-use the class @\<open>typ math_content\<close>, which provides also a framework for
 semi-formal terminology, which we re-use by this definition.\<close>
 
@@ -35,20 +37,19 @@ type_synonym concept = concept_definition
 declare[[ Definition_default_class="concept_definition"]]
 
 
-(*>>*)
 
-section \<open>Terminology\<close>
+subsection \<open>Terminology\<close>
 
 
-subsection \<open>Terms and definitions common in the CC\<close>
+subsubsection \<open>Terms and definitions common in the CC\<close>
 
 Definition* [aas_def, tag= "''adverse actions''"]
  \<open>actions performed by a threat agent on an asset\<close>
 
-declare_reference*[toe_def]
+declare_reference*[toeDef]
 
 Definition* [assts_def, tag="''assets''"]
- \<open>entities that the owner of the @{docitem toe_def} presumably places value upon \<close>
+ \<open>entities that the owner of the @{docitem toeDef} presumably places value upon \<close>
 
 Definition* [asgn_def, tag="''assignment''"]
 \<open>the specification of an identified parameter in a component (of the CC) or requirement.\<close>
@@ -56,7 +57,7 @@ Definition* [asgn_def, tag="''assignment''"]
 declare_reference*[sfrs_def]
 
 Definition* [assrc_def, tag="''assurance''"]
-  \<open>grounds for confidence that a @{docitem toe_def} meets the @{docitem sfrs_def}\<close>
+  \<open>grounds for confidence that a @{docitem toeDef} meets the @{docitem sfrs_def}\<close>
 
 Definition* [attptl_def, tag="''attack potential''"] 
   \<open>measure of the effort to be expended in attacking a TOE, expressed in terms of 
@@ -69,9 +70,9 @@ Definition* [authdata_def, tag="''authentication data''"]
   \<open>information used to verify the claimed identity of a user\<close>
 
 Definition* [authusr_def, tag = "''authorised user''"] 
-\<open>@{docitem toe_def} user who may, in accordance with the @{docitem sfrs_def}, perform an operation\<close>
+\<open>@{docitem toeDef} user who may, in accordance with the @{docitem sfrs_def}, perform an operation\<close>
 
-Definition* [bpp_def, tag="''Base Protection Profile''"] 
+Definition* [bppDef, tag="''Base Protection Profile''"] 
 \<open>Protection Profile used as a basis to build a Protection Profile Configuration\<close>
 
 Definition* [cls_def,tag="''class''"]
@@ -104,8 +105,8 @@ Definition* [cfrm_def,tag="''confirm''"]
  term is only applied to evaluator actions.\<close>
 
 Definition* [cnnctvty_def, tag="''connectivity''"]
-\<open>property of the @{docitem toe_def} allowing interaction with IT entities external to the 
- @{docitem toe_def}
+\<open>property of the @{docitem toeDef} allowing interaction with IT entities external to the 
+ @{docitem toeDef}
 
  This includes exchange of data by wire or by wireless means, over any
  distance in any environment or configuration.\<close>
@@ -118,17 +119,17 @@ Definition* [cnt_vrb_def, tag="''counter, verb''"]
 \<open>meet an attack where the impact of a particular threat is mitigated 
  but not necessarily eradicated\<close>
 
-declare_reference*[st_def]
-declare_reference*[pp_def]
+declare_reference*[stDef]
+declare_reference*[ppDef]
 
 Definition* [dmnst_conf_def, tag="''demonstrable conformance''"] 
-\<open>relation between an @{docitem st_def} and a @{docitem pp_def}, where the @{docitem st_def} 
+\<open>relation between an @{docitem stDef} and a @{docitem ppDef}, where the @{docitem stDef} 
  provides a solution which solves the generic security problem in the PP
 
-The @{docitem pp_def} and the @{docitem st_def} may contain entirely different statements that discuss
+The @{docitem ppDef} and the @{docitem stDef} may contain entirely different statements that discuss
 different entities, use different concepts etc. Demonstrable conformance is
-also suitable for a @{docitem toe_def} type where several similar @{docitem pp_def}s already exist, thus
-allowing the ST author to claim conformance to these @{docitem pp_def}s simultaneously,
+also suitable for a @{docitem toeDef} type where several similar @{docitem ppDef}s already exist, thus
+allowing the ST author to claim conformance to these @{docitem ppDef}s simultaneously,
 thereby saving work.\<close>
 
 Definition* [dmstrt_def, tag="''demonstrate''"] 
@@ -136,9 +137,9 @@ Definition* [dmstrt_def, tag="''demonstrate''"]
 
 Definition* [dpndcy, tag="''dependency''"] 
 \<open>relationship between components such that if a requirement based on the depending 
- component is included in a @{docitem pp_def}, ST or package, a requirement based on 
- the component that is depended upon must normally also be included in the @{docitem pp_def}, 
- @{docitem st_def} or package\<close>
+ component is included in a @{docitem ppDef}, ST or package, a requirement based on 
+ the component that is depended upon must normally also be included in the @{docitem ppDef}, 
+ @{docitem stDef} or package\<close>
 
 Definition* [dscrb_def, tag="''describe''"] 
 \<open>provide specific details of an entity\<close>
@@ -153,7 +154,7 @@ Definition* [dtrmn_def, tag="''determine''"]
  performed which needs to be reviewed\<close>
 
 Definition* [devenv_def, tag="''development environment''"] 
-\<open>environment in which the @{docitem toe_def} is developed\<close>
+\<open>environment in which the @{docitem toeDef} is developed\<close>
 
 Definition* [elmnt_def, tag="''element''"] 
 \<open>indivisible statement of a security need\<close>
@@ -165,7 +166,7 @@ Definition* [ensr_def, tag="''ensure''"]
  consequence is not fully certain, on the basis of that action alone.\<close>
 
 Definition* [eval_def, tag="''evaluation''"] 
-\<open>assessment of a @{docitem pp_def}, an @{docitem st_def} or a @{docitem toe_def}, 
+\<open>assessment of a @{docitem ppDef}, an @{docitem stDef} or a @{docitem toeDef}, 
  against defined criteria.\<close>
 
 Definition* [eal_def, tag= "''evaluation assurance level''"] 
@@ -173,18 +174,19 @@ Definition* [eal_def, tag= "''evaluation assurance level''"]
  CC predefined assurance scale, that form an assurance package\<close>
 
 Definition* [eval_auth_def, tag="''evaluation authority''"] 
-\<open>body that sets the standards and monitors the quality of evaluations conducted by bodies within a specific community and
- implements the CC for that community by means of an evaluation scheme\<close>
+\<open>body that sets the standards and monitors the quality of evaluations conducted 
+ by bodies within a specific community and implements the CC for that community 
+ by means of an evaluation scheme\<close>
 
 Definition* [eval_schm_def, tag="''evaluation scheme''"] 
 \<open>administrative and regulatory framework under which the CC is applied by an 
  evaluation authority within a specific community\<close>
 
-Definition* [exst_def, tag="''exhaustive''"]
+Definition* [exstDef, tag="''exhaustive''"]
 \<open>characteristic of a methodical approach taken to perform an
 analysis or activity according to an unambiguous plan
 This term is used in the CC with respect to conducting an analysis or other
-activity. It is related to “systematic” but is considerably stronger, in that it
+activity. It is related to ``systematic'' but is considerably stronger, in that it
 indicates not only that a methodical approach has been taken to perform the
 analysis or activity according to an unambiguous plan, but that the plan that
 was followed is sufficient to ensure that all possible avenues have been
@@ -235,7 +237,7 @@ Definition* [intl_com_chan_def, tag ="''internal communication channel''"]
 Definition* [int_toe_trans, tag="''internal TOE transfer''"] 
   \<open>communicating data between separated parts of the TOE\<close>
 
-Definition* [inter_consist_def, tag="''internally consistent''"] 
+Definition* [inter_consistDef, tag="''internally consistent''"] 
   \<open>no apparent contradictions exist between any aspects of an entity
 
    In terms of documentation, this means that there can be no statements within
@@ -270,7 +272,7 @@ Definition* [org_sec_po_def, tag="''organisational security policy''"]
 
 Definition* [pckg_def, tag="''package''"] 
 \<open>named set of either security functional or security assurance requirements 
- An example of a package is “EAL 3”.\<close>
+ An example of a package is ``EAL 3''.\<close>
 
 Definition* [pp_config_def, tag="''Protection Profile Configuration''"] 
 \<open>Protection Profile composed of Base Protection Profiles and Protection Profile Module\<close>
@@ -278,7 +280,7 @@ Definition* [pp_config_def, tag="''Protection Profile Configuration''"]
 Definition* [pp_eval_def, tag="''Protection Profile evaluation''"]
 \<open> assessment of a PP against defined criteria \<close>
 
-Definition* [pp_def, tag="''Protection Profile''"] 
+Definition* [ppDef, tag="''Protection Profile''"] 
 \<open>implementation-independent statement of security needs for a TOE type\<close>
 
 Definition* [ppm_def, tag="''Protection Profile Module''"] 
@@ -298,7 +300,7 @@ Definition* [ref_def, tag="''refinement''"]
 
 Definition* [role_def, tag="''role''"] 
 \<open>predefined set of rules establishing the allowed interactions between
- a user and the @{docitem toe_def}\<close>
+ a user and the @{docitem toeDef}\<close>
 
 declare_reference*[sfp_def]
 
@@ -308,7 +310,7 @@ Definition* [scrt_def, tag="''secret''"]
 
 declare_reference*[sfr_def]
 
-Definition* [sec_st_def, tag="''secure state''"] 
+Definition* [sec_stDef, tag="''secure state''"] 
 \<open>state in which the @{docitem tsf_def} data are consistent and the  @{docitem tsf_def} 
  continues correct enforcement of the  @{docitem sfr_def}s\<close>
 
@@ -328,18 +330,20 @@ Definition* [sec_obj_def, tag="''security objective''"]
 Definition* [sec_prob_def, tag ="''security problem''"] 
 \<open>statement which in a formal manner defines the nature and scope of the security that 
 the TOE is intended to address This statement consists of a combination of:
-  \begin{itemize}
- \item threats to be countered by the TOE and its operational environment,
- \item the OSPs enforced by the TOE and its operational environment, and
- \item the assumptions that are upheld for the operational environment of the TOE.
- \end{itemize}\<close>
+\begin{itemize}
+\item threats to be countered by the TOE and its operational environment,
+\item the OSPs enforced by the TOE and its operational environment, and
+\item the assumptions that are upheld for the operational environment of the TOE.
+\end{itemize}\<close>
 
 Definition* [sr_def, tag="''security requirement''", short_tag="Some(''SR'')"] 
 \<open>requirement, stated in a standardised language, which is meant to contribute 
  to achieving the security objectives for a TOE\<close>
-text \<open>@{docitem toe_def}\<close>
-Definition* [st, tag="''Security Target''", short_tag="Some(''ST'')"] 
-\<open>implementation-dependent statement of security needs for a specific i\<section>dentified @{docitem toe_def}\<close>
+(*<*)
+text \<open>@{docitem toeDef}\<close>
+(*>*)
+Definition* [st, tag="''Security Target''", short_tag="Some(''ST'')"]
+\<open>implementation-dependent statement of security needs for a specific identified @{docitem toeDef}\<close>
 
 Definition* [slct_def, tag="''selection''"] 
 \<open>specification of one or more items from a list in a component\<close>
@@ -385,7 +389,7 @@ Definition* [tr_vrb_def, tag="''trace, verb''"]
 \<open>perform an informal correspondence analysis between two entities with only a 
  minimal level of rigour\<close>
 
-Definition* [trnsfs_out_toe_def, tag="''transfers outside of the TOE''"] 
+Definition* [trnsfs_out_toeDef, tag="''transfers outside of the TOE''"] 
 \<open>TSF mediated communication of data to entities not under the control of the TSF\<close>
 
 Definition* [transl_def, tag= "''translation''"]
@@ -430,13 +434,13 @@ effort is required of the evaluator.\<close>
 
 Definition* [dev_def, tag="''Developer''"]
 \<open>who respond to actual or perceived consumer security requirements in 
- constructing a @{docitem toe_def}, reference this  CC_Part_3 
+ constructing a @{docitem toeDef}, reference this  CC\_Part\_3 
  when interpreting statements of assurance requirements and determining
  assurance approaches of @{docitem toe}s.\<close>
 
 Definition*[evalu_def, tag="'' Evaluator''"]
-\<open>who use the assurance requirements defined in CC_Part_3 
+\<open>who use the assurance requirements defined in CC\_Part\_3 
  as mandatory statement of evaluation criteria when determining the assurance 
- of @{docitem toe_def}s and when evaluating @{docitem pp_def}s and @{docitem st_def}s.\<close>
+ of @{docitem toeDef}s and when evaluating @{docitem ppDef}s and @{docitem stDef}s.\<close>
 
 end

Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy

@@ -10,16 +10,18 @@
  *   SPDX-License-Identifier: BSD-2-Clause
  *************************************************************************)
 
+section\<open>CC 3.1.R5\<close>
 (*<*)
 theory  "CC_v3_1_R5"
-  imports  "Isabelle_DOF.technical_report" 
+  imports 
+ "Isabelle_DOF.technical_report" 
            "CC_terminology"
 
 
 begin
 (*>*)
 
-section \<open>General Infrastructure on CC Evaluations\<close>
+subsection \<open>General Infrastructure on CC Evaluations\<close>
 
 datatype EALs = EAL1 |  EAL2 |  EAL3 |  EAL4 |  EAL5 |  EAL6 | EAL7
 
@@ -30,7 +32,7 @@ doc_class CC_structure_element =(* text_element + *)
 doc_class CC_text_element = text_element +
           eval_level :: EALs
 
-section \<open>Security target ontology\<close>
+subsection \<open>Security target ontology\<close>
 
 
 doc_class st_ref_cls = CC_text_element +
@@ -53,12 +55,11 @@ doc_class toe_ovrw_cls = CC_text_element +
     firmeware_req:: "CC_text_element list" <= "[]"
     features_req :: "CC_text_element list" <= "[]"
     invariant  eal_consistency:: 
-                 "\<lambda> X::toe_ovrw_cls . 
-                        (case eval_level X  of 
-                           EAL1 \<Rightarrow> software_req  X \<noteq> [] 
-                      |    EAL2 \<Rightarrow> software_req  X \<noteq> [] 
-                      |    EAL3 \<Rightarrow> software_req  X \<noteq> [] 
-                      |    EAL4 \<Rightarrow> software_req  X \<noteq> [] 
+                 "(case eval_level \<sigma>  of 
+                           EAL1 \<Rightarrow> software_req  \<sigma> \<noteq> [] 
+                      |    EAL2 \<Rightarrow> software_req  \<sigma> \<noteq> [] 
+                      |    EAL3 \<Rightarrow> software_req  \<sigma> \<noteq> [] 
+                      |    EAL4 \<Rightarrow> software_req  \<sigma> \<noteq> [] 
                       |    _ \<Rightarrow>  undefined)"
 
 thm eal_consistency_inv_def

Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128.thy

@@ -24,10 +24,14 @@ identifies:
  \<close> 
 
 (*<<*)  
-theory CENELEC_50128
-  imports  "Isabelle_DOF.technical_report"
+theory 
+  CENELEC_50128
+  imports  
+  "Isabelle_DOF.technical_report" 
 begin
 
+define_ontology "DOF-CENELEC_50128.sty" "CENELEC 50128"
+
 (* this is a hack and should go into an own ontology, providing thingsd like:
   - Assumption*
   - Hypothesis*
@@ -155,10 +159,10 @@ which have the required safety integrity level.\<close>
 Definition*[entity]
 \<open>person, group or organisation who fulfils a role as defined in this European Standard.\<close>
 
-declare_reference*[fault]
+declare_reference*[fault::cenelec_term]
 Definition*[error]
 \<open>defect, mistake or inaccuracy which could result in failure or in a deviation 
-from the intended performance or behaviour (cf. @{cenelec_term (unchecked) \<open>fault\<close>})).\<close>
+from the intended performance or behaviour (cf. @{cenelec_term (unchecked) \<open>fault\<close>}).\<close>
 
 Definition*[fault]
 \<open>defect, mistake or inaccuracy which could result in failure or in a deviation 
@@ -521,9 +525,11 @@ text\<open>Figure 3 in Chapter 5: Illustrative Development Lifecycle 1\<close>
 
 text\<open>Global Overview\<close>
 
+(*
 figure*[fig3::figure, relative_width="100", 
  src="''examples/CENELEC_50128/mini_odo/document/figures/CENELEC-Fig.3-docStructure.png''"]
 \<open>Illustrative Development Lifecycle 1\<close>
+*)
 
 text\<open>Actually, the Figure 4 in Chapter 5: Illustrative Development Lifecycle 2 is more fidele
 to the remaining document: Software Architecture and Design phases are merged, like in 7.3.\<close>
@@ -614,9 +620,10 @@ doc_class cenelec_report = text_element +
    invariant must_be_chapter :: "text_element.level \<sigma> = Some(0)" 
    invariant three_eyes_prcpl:: "  written_by \<sigma> \<noteq> fst_check \<sigma> 
                                  \<and> written_by \<sigma> \<noteq> snd_check \<sigma>"
-   
+  
+(* 
 text\<open>see \<^figure>\<open>fig3\<close> and Fig 4 in Chapter 5: Illustrative Development Lifecycle 2\<close>
-
+*)
 doc_class external_specification =
   phase        :: "phase"  <= "SYSDEV_ext"
 
@@ -1007,14 +1014,16 @@ ML\<open>
 fun check_sil oid _ ctxt =
   let
     val ctxt' = Proof_Context.init_global(Context.theory_of ctxt)
-    val monitor_record_value = #value (the (DOF_core.get_object_local oid ctxt'))
+    val DOF_core.Instance {value = monitor_record_value, ...} =
+                          DOF_core.get_instance_global oid (Context.theory_of ctxt)
     val Const _ $ _ $ monitor_sil $ _ = monitor_record_value
-    val traces = AttributeAccess.compute_trace_ML ctxt oid \<^here> \<^here>
+    val traces = AttributeAccess.compute_trace_ML ctxt oid NONE \<^here>
     fun check_sil'' [] = true
       | check_sil'' (x::xs) =
           let
             val (_, doc_oid) = x
-            val doc_record_value = #value (the (DOF_core.get_object_local doc_oid ctxt'))
+            val DOF_core.Instance {value = doc_record_value, ...} =
+                      DOF_core.get_instance_global doc_oid (Context.theory_of ctxt)
             val Const _ $ _ $ _ $ _ $ _ $ cenelec_document_ext = doc_record_value
             val Const _ $ _ $ _ $ doc_sil $ _ $ _ $ _ $ _ $ _ $ _ = cenelec_document_ext
           in 
@@ -1026,27 +1035,35 @@ fun check_sil oid _ ctxt =
   in check_sil'' traces end
 \<close>
 
-setup\<open>DOF_core.update_class_invariant "CENELEC_50128.monitor_SIL0" check_sil\<close>
+setup\<open>
+(fn thy =>
+let val ctxt = Proof_Context.init_global thy
+    val binding = DOF_core.binding_from_onto_class_pos "monitor_SIL0" thy
+in  DOF_core.add_ml_invariant binding check_sil thy end)
+\<close>
 
 text\<open>
-A more generic example of check_sil which can be generalized:
+A more generic example of check\_sil which can be generalized:
 it is decoupled from the CENELEC current implementation
 but is much less efficient regarding time computation by relying on Isabelle evaluation mechanism.\<close>
 ML\<open>
 fun check_sil_slow oid _ ctxt =
   let 
     val ctxt' = Proof_Context.init_global(Context.theory_of ctxt)
-    val monitor_record_value = #value (the (DOF_core.get_object_local oid ctxt'))
-    val monitor_cid = #cid (the (DOF_core.get_object_local oid ctxt'))
+    val DOF_core.Instance {value = monitor_record_value, ...} =
+                          DOF_core.get_instance_global oid (Context.theory_of ctxt)
+    val DOF_core.Instance {cid = monitor_cid, ...} =
+                          DOF_core.get_instance_global oid (Context.theory_of ctxt)
     val monitor_sil_typ = (Syntax.read_typ ctxt' monitor_cid) --> @{typ "sil"}
     val monitor_sil = Value_Command.value ctxt'
                     (Const("CENELEC_50128.monitor_SIL.sil", monitor_sil_typ) $ monitor_record_value)
-    val traces = AttributeAccess.compute_trace_ML ctxt oid \<^here> \<^here>
+    val traces = AttributeAccess.compute_trace_ML ctxt oid NONE \<^here>
     fun check_sil'  [] = true
       | check_sil' (x::xs) =
           let
             val (doc_cid, doc_oid) = x
-            val doc_record_value = #value (the (DOF_core.get_object_local doc_oid ctxt'))
+            val DOF_core.Instance {value = doc_record_value, ...} =
+                    DOF_core.get_instance_global doc_oid (Context.theory_of ctxt)
             val doc_sil_typ = (Syntax.read_typ ctxt' doc_cid) --> @{typ "sil"} 
             val doc_sil = Value_Command.value ctxt'
                     (Const ("CENELEC_50128.cenelec_document.sil", doc_sil_typ) $ doc_record_value)
@@ -1059,20 +1076,25 @@ fun check_sil_slow oid _ ctxt =
   in check_sil' traces end
 \<close>
 
-(*setup\<open>DOF_core.update_class_invariant "CENELEC_50128.monitor_SIL0" check_sil_slow\<close>*)
+(*setup\<open>
+(fn thy =>
+let val ctxt = Proof_Context.init_global thy
+    val binding = DOF_core.binding_from_onto_class_pos "monitor_SIL0" thy
+in  DOF_core.add_ml_invariant binding check_sil_slow thy end)
+\<close>*)
 
 (* As traces of monitor instances (docitems) are updated each time an instance is declared
-  (with text*, section*, etc.), invariants checking functions which use traces must
-  be declared as lazy invariants, to be checked only when closing a monitor, i.e.,
-  after the monitor traces are populated.
+  (with text*, section*, etc.), invariants checking functions which check the full list of traces
+  must be declared as lazy invariants, to be checked only when closing a monitor, i.e.,
+  after all the monitor traces are populated.
 *)
 ML\<open>
 fun check_required_documents oid _ ctxt = 
   let
     val ctxt' = Proof_Context.init_global(Context.theory_of ctxt)
-    val {monitor_tab,...} = DOF_core.get_data ctxt'
-    val {accepted_cids, ...} = the (Symtab.lookup monitor_tab oid)
-    val traces = AttributeAccess.compute_trace_ML ctxt oid \<^here> \<^here>
+    val DOF_core.Monitor_Info {accepted_cids, ...} =
+                      DOF_core.get_monitor_info_global oid (Context.theory_of ctxt)
+    val traces = AttributeAccess.compute_trace_ML ctxt oid NONE \<^here>
     fun check_required_documents' [] = true
       | check_required_documents' (cid::cids) =
           if exists (fn (doc_cid, _) => equal cid doc_cid) traces
@@ -1080,7 +1102,8 @@ fun check_required_documents oid _ ctxt =
           else
             let
               val ctxt' = Proof_Context.init_global(Context.theory_of ctxt)
-              val monitor_record_value = #value (the (DOF_core.get_object_local oid ctxt'))
+              val DOF_core.Instance {value = monitor_record_value, ...} =
+                          DOF_core.get_instance_global oid (Context.theory_of ctxt)
               val Const _ $ _ $ monitor_sil $ _ = monitor_record_value
             in error ("A " ^ cid ^ " cenelec document is required with "
                       ^ Syntax.string_of_term ctxt' monitor_sil)
@@ -1088,7 +1111,12 @@ fun check_required_documents oid _ ctxt =
   in check_required_documents' accepted_cids end
 \<close>
 
-setup\<open>DOF_core.update_class_lazy_invariant "CENELEC_50128.monitor_SIL0" check_required_documents\<close>
+setup\<open>
+fn thy =>
+let val ctxt = Proof_Context.init_global thy
+    val binding = DOF_core.binding_from_onto_class_pos "monitor_SIL0" thy
+in  DOF_core.add_closing_ml_invariant binding check_required_documents thy end
+\<close>
 
 (* Test pattern matching for the records of the current CENELEC implementation classes,
    and used by checking functions.
@@ -1099,11 +1127,11 @@ text*[MonitorPatternMatchingTest::monitor_SIL0]\<open>\<close>
 text*[CenelecClassPatternMatchingTest::SQAP, sil = "SIL0"]\<open>\<close>
 ML\<open>
 val thy = @{theory}
-val monitor_record_value =
-      #value (the (DOF_core.get_object_global "MonitorPatternMatchingTest" thy))
+val DOF_core.Instance {value = monitor_record_value, ...} =
+                                        DOF_core.get_instance_global "MonitorPatternMatchingTest" thy
 val Const _ $ _ $ monitor_sil $ _ = monitor_record_value
-val doc_record_value = #value (the (DOF_core.get_object_global
-                                              "CenelecClassPatternMatchingTest" thy))
+val DOF_core.Instance {value = doc_record_value, ...} =
+                                    DOF_core.get_instance_global "CenelecClassPatternMatchingTest" thy
 val Const _ $ _ $ _ $ _ $ _ $ cenelec_document_ext = doc_record_value
 val Const _ $ _ $ _ $ doc_sil $ _ $ _ $ _ $ _ $ _ $ _ = cenelec_document_ext
 \<close>
@@ -1236,15 +1264,16 @@ doc_class test_documentation =    (* OUTDATED ? *)
 
 
 section\<open>Global Documentation Structure\<close>
-
+(*<<*)
 doc_class global_documentation_structure = text_element +
    level :: "int option" <= "Some(-1::int)"  \<comment> \<open>document must be a chapter\<close>
-   accepts "SYSREQS      ~~                  \<comment> \<open>system_requirements_specification\<close>
-            SYSSREQS     ~~                  \<comment> \<open>system_safety_requirements_specification\<close> 
-            SYSAD        ~~                  \<comment> \<open>system_architecture description\<close>
+   accepts "SYSREQS      ~~                  \<comment> \<open>system requiremens specification\<close>
+            SYSSREQS     ~~                  \<comment> \<open>system safety requirements specification\<close> 
+            SYSAD        ~~                  \<comment> \<open>system architecture description\<close>
             SYSS_pl      ~~                  \<comment> \<open>system safety plan\<close> 
             (SWRS || OSWTS)  "                \<comment> \<open>software requirements specification OR
                                                  overall software test specification\<close> 
+(*>>*)
 (* MORE TO COME : *)
 
 section\<open> META : Testing and Validation \<close>
@@ -1252,10 +1281,10 @@ section\<open> META : Testing and Validation \<close>
 text\<open>Test : @{semi_formal_content \<open>COTS\<close>}\<close>
 
 ML
-\<open> DOF_core.read_cid_global @{theory} "requirement";
-  DOF_core.read_cid_global @{theory} "SRAC";
-  DOF_core.is_defined_cid_global "SRAC" @{theory};
-  DOF_core.is_defined_cid_global "EC" @{theory}; \<close>
+\<open> DOF_core.get_onto_class_name_global "requirement" @{theory};
+  DOF_core.get_onto_class_name_global "SRAC" @{theory};
+  DOF_core.get_onto_class_global "SRAC" @{theory};
+  DOF_core.get_onto_class_global "EC" @{theory}; \<close>
 
 ML
 \<open> DOF_core.is_subclass @{context} "CENELEC_50128.EC"   "CENELEC_50128.EC";
@@ -1264,18 +1293,19 @@ ML
   DOF_core.is_subclass @{context} "CENELEC_50128.EC"   "CENELEC_50128.test_requirement"; \<close>
 
 ML
-\<open> val {docobj_tab={maxano, tab=ref_tab},docclass_tab=class_tab,...} = DOF_core.get_data @{context};
-  Symtab.dest ref_tab;
-  Symtab.dest class_tab; \<close>
+\<open> val ref_tab = DOF_core.get_instances \<^context> 
+  val docclass_tab = DOF_core.get_onto_classes @{context};
+  Name_Space.dest_table ref_tab;
+  Name_Space.dest_table docclass_tab; \<close>
 
 ML
 \<open> val internal_data_of_SRAC_definition = DOF_core.get_attributes_local "SRAC" @{context} \<close> 
 
 ML
-\<open> DOF_core.read_cid_global         @{theory}  "requirement";
+\<open> DOF_core.get_onto_class_name_global "requirement" @{theory};
   Syntax.parse_typ                 @{context} "requirement";
   val Type(t,_) = Syntax.parse_typ @{context} "requirement" handle ERROR _ => dummyT; 
   Syntax.read_typ                  @{context} "hypothesis"  handle  _ => dummyT;
   Proof_Context.init_global; \<close>
 
-end
+end

Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128_Documentation.thy

@@ -0,0 +1,397 @@
+(*************************************************************************
+ * Copyright (C) 
+ *               2019-2023      The University of Exeter 
+ *               2018-2023 The University of Paris-Saclay
+ *               2018      The University of Sheffield
+ *
+ * License:
+ *   This program can be redistributed and/or modified under the terms
+ *   of the 2-clause BSD-style license.
+ *
+ *   SPDX-License-Identifier: BSD-2-Clause
+ *************************************************************************)
+
+(*<<*)  
+theory 
+  CENELEC_50128_Documentation
+  imports  
+  CENELEC_50128
+           
+begin
+
+define_shortcut* dof     \<rightleftharpoons> \<open>\dof\<close>
+                 isadof  \<rightleftharpoons> \<open>\isadof{}\<close>
+define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
+                 BibTeX  \<rightleftharpoons> \<open>\BibTeX{}\<close> 
+                 LaTeX   \<rightleftharpoons> \<open>\LaTeX{}\<close>
+                 TeX     \<rightleftharpoons> \<open>\TeX{}\<close>
+                 pdf     \<rightleftharpoons> \<open>PDF\<close>
+
+ML\<open>
+
+fun boxed_text_antiquotation name (* redefined in these more abstract terms *) =
+    DOF_lib.gen_text_antiquotation name DOF_lib.report_text
+                           (fn ctxt => DOF_lib.string_2_text_antiquotation ctxt
+                                       #> DOF_lib.enclose_env false ctxt "isarbox")
+
+val neant = K(Latex.text("",\<^here>))
+
+fun boxed_theory_text_antiquotation name (* redefined in these more abstract terms *) =
+    DOF_lib.gen_text_antiquotation name DOF_lib.report_theory_text
+                           (fn ctxt => DOF_lib.string_2_theory_text_antiquotation ctxt
+                                        #> DOF_lib.enclose_env false ctxt "isarbox"
+                                        (* #> neant *)) (*debugging *)
+
+fun boxed_sml_text_antiquotation name  =
+    DOF_lib.gen_text_antiquotation name (K(K()))
+                           (fn ctxt => Input.source_content
+                                        #> Latex.text
+                                        #> DOF_lib.enclose_env true ctxt "sml")
+                           (* the simplest conversion possible *)
+
+fun boxed_pdf_antiquotation name =
+    DOF_lib.gen_text_antiquotation name (K(K()))
+                           (fn ctxt => Input.source_content
+                                        #> Latex.text
+                                        #> DOF_lib.enclose_env true ctxt "out")
+                           (* the simplest conversion possible *)
+
+fun boxed_latex_antiquotation name =
+    DOF_lib.gen_text_antiquotation name (K(K()))
+                           (fn ctxt => Input.source_content
+                                        #> Latex.text
+                                        #> DOF_lib.enclose_env true ctxt "ltx")
+                           (* the simplest conversion possible *)
+
+fun boxed_bash_antiquotation name =
+    DOF_lib.gen_text_antiquotation name (K(K()))
+                           (fn ctxt => Input.source_content
+                                        #> Latex.text
+                                        #> DOF_lib.enclose_env true ctxt "bash")
+                           (* the simplest conversion possible *)
+\<close>
+
+setup\<open>(* std_text_antiquotation        \<^binding>\<open>my_text\<close> #> *)
+      boxed_text_antiquotation         \<^binding>\<open>boxed_text\<close> #>
+      (* std_text_antiquotation        \<^binding>\<open>my_cartouche\<close> #> *)
+      boxed_text_antiquotation         \<^binding>\<open>boxed_cartouche\<close> #>
+      (* std_theory_text_antiquotation \<^binding>\<open>my_theory_text\<close>#> *)
+      boxed_theory_text_antiquotation  \<^binding>\<open>boxed_theory_text\<close> #>
+
+      boxed_sml_text_antiquotation     \<^binding>\<open>boxed_sml\<close> #>
+      boxed_pdf_antiquotation          \<^binding>\<open>boxed_pdf\<close> #>
+      boxed_latex_antiquotation        \<^binding>\<open>boxed_latex\<close>#>
+      boxed_bash_antiquotation         \<^binding>\<open>boxed_bash\<close>
+     \<close>
+
+
+
+(*>>*)  
+
+section*[cenelec_onto::example]\<open>Writing Certification Documents \<^boxed_theory_text>\<open>CENELEC_50128\<close>\<close>
+subsection\<open>The CENELEC 50128 Example\<close>
+text\<open> 
+  The ontology \<^verbatim>\<open>CENELEC_50128\<close>\index{ontology!CENELEC\_50128} is a small ontology modeling 
+  documents for a certification following CENELEC 50128~@{cite "boulanger:cenelec-50128:2015"}.
+  The \<^isadof> distribution contains a small example  using the ontology ``CENELEC\_50128'' in 
+  the directory \nolinkurl{examples/CENELEC_50128/mini_odo/}. You can inspect/edit the 
+  integrated source example by either 
+  \<^item> starting Isabelle/jEdit using your graphical user interface (\<^eg>, by clicking on the 
+    Isabelle-Icon provided by the Isabelle installation) and loading the file 
+    \nolinkurl{examples/CENELEC_50128/mini_odo/mini_odo.thy}.
+  \<^item> starting Isabelle/jEdit from the command line by calling:
+
+@{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë 
+  isabelle jedit examples/CENELEC_50128/mini_odo/mini_odo.thy \<close>}
+\<close>
+text\<open>\<^noindent> Finally, you
+  \<^item>   can build the \<^pdf>-document by calling:
+@{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë isabelle build mini_odo \<close>}
+\<close>
+ 
+subsection\<open>Modeling CENELEC 50128\<close>
+
+text\<open>
+  Documents to be provided in formal certifications (such as CENELEC 
+  50128~@{cite "boulanger:cenelec-50128:2015"} or Common Criteria~@{cite "cc:cc-part3:2006"}) can 
+  much profit from the control of ontological consistency:  a substantial amount of the work
+  of evaluators in formal certification processes consists in  tracing down the links from 
+  requirements over assumptions down to elements of evidence, be it in form of semi-formal 
+  documentation, models, code, or tests.  In a certification process, traceability becomes a major 
+  concern; and providing mechanisms to ensure complete traceability already at the development of 
+  the integrated source can in our view increase the speed and reduce the risk certification 
+  processes. Making the link-structure machine-checkable, be it between requirements, assumptions, 
+  their implementation and their discharge by evidence (be it tests, proofs, or authoritative 
+  arguments), has the potential in our view to decrease the cost of software developments 
+  targeting certifications. 
+
+  As in many other cases, formal certification documents come with an own terminology and pragmatics
+  of what has to be demonstrated and where, and how the traceability of requirements through 
+  design-models over code to system environment assumptions has to be assured.  
+
+  In the sequel, we present a simplified version of an ontological model used in a 
+  case-study~@{cite "bezzecchi.ea:making:2018"}. We start with an introduction of the concept of 
+  requirement:
+
+@{boxed_theory_text [display]\<open>
+doc_class requirement = long_name :: "string option"
+
+doc_class hypothesis = requirement +
+      hyp_type :: hyp_type <= physical  (* default *)
+  
+datatype ass_kind = informal | semiformal | formal
+  
+doc_class assumption = requirement +
+     assumption_kind :: ass_kind <= informal 
+\<close>}
+
+Such ontologies can be enriched by larger explanations and examples, which may help
+the team of engineers substantially when developing the central document for a certification, 
+like an explication of what is precisely the difference between an \<^typ>\<open>hypothesis\<close> and an 
+\<^typ>\<open>assumption\<close> in the context of the evaluation standard. Since the PIDE makes for each 
+document class its definition available by a simple mouse-click, this kind on meta-knowledge 
+can be made far more accessible during the document evolution.
+
+For example, the term of category \<^typ>\<open>assumption\<close> is used for domain-specific assumptions. 
+It has \<^const>\<open>formal\<close>, \<^const>\<open>semiformal\<close> and \<^const>\<open>informal\<close> sub-categories. They have to be 
+tracked and discharged by appropriate validation procedures within a 
+certification process, be it by test or proof. It is different from a \<^typ>\<open>hypothesis\<close>, which is
+globally assumed and accepted.
+
+In the sequel, the category \<^typ>\<open>exported_constraint\<close> (or \<^typ>\<open>EC\<close> for short)
+is used for formal assumptions, that arise during the analysis,
+design or implementation and have to be tracked till the final
+evaluation target, and discharged by appropriate validation procedures 
+within the certification process, be it by test or proof.  A particular class of interest 
+is the category \<^typ>\<open>safety_related_application_condition\<close> (or \<^typ>\<open>SRAC\<close> 
+for short) which is used for \<^typ>\<open>EC\<close>'s that establish safety properties
+of the evaluation target. Their traceability throughout the certification
+is therefore particularly critical. This is naturally modeled as follows:
+@{boxed_theory_text [display]\<open>  
+doc_class EC = assumption  +
+     assumption_kind :: ass_kind <= (*default *) formal
+                        
+doc_class SRAC = EC  +
+     assumption_kind :: ass_kind <= (*default *) formal
+\<close>}
+
+We now can, \<^eg>, write 
+
+@{boxed_theory_text [display]\<open>
+text*[ass123::SRAC]\<open> 
+  The overall sampling frequence of the odometer subsystem is therefore 
+  14 khz, which includes sampling, computing and result communication 
+  times \ldots
+\<close>
+\<close>}
+
+This will be shown in the \<^pdf> as follows:
+\<close>
+text*[ass123::SRAC] \<open> The overall sampling frequency of the odometer
+subsystem is therefore 14 khz, which includes sampling, computing and
+result communication times \ldots \<close>
+
+text\<open>Note that this \<^pdf>-output is the result of a specific setup for \<^typ>\<open>SRAC\<close>s.\<close>
+
+subsection*[ontopide::technical]\<open>Editing Support for CENELEC 50128\<close>  
+figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"]
+\<open> Standard antiquotations referring to theory elements.\<close>
+text\<open> The corresponding view in @{docitem  \<open>figfig3\<close>} shows core part of a document 
+conforming to the \<^verbatim>\<open>CENELEC_50128\<close> ontology. The first sample shows standard Isabelle antiquotations 
+@{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts 
+of a document get ``formal content'' and become more robust under change.\<close>
+
+figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"]
+        \<open> Defining a \<^typ>\<open>SRAC\<close> in the integrated source ... \<close>
+
+figure*[figfig7::figure, relative_width="95", src="''figures/srac-as-es-application''"]
+        \<open> Using a \<^typ>\<open>SRAC\<close> as \<^typ>\<open>EC\<close> document element. \<close>
+text\<open> The subsequent sample in @{figure \<open>figfig5\<close>} shows the definition of a
+\<^emph>\<open>safety-related application condition\<close>, a side-condition of a theorem which 
+has the consequence that a certain calculation must be executed sufficiently fast on an embedded 
+device. This condition can not be established inside the formal theory but has to be 
+checked by system integration tests. Now we reference in @{figure  \<open>figfig7\<close>} this 
+safety-related condition; however, this happens in a context where general \<^emph>\<open>exported constraints\<close> 
+are listed. \<^isadof>'s checks and establishes that this is legal in the given ontology. 
+\<close>    
+
+text\<open>
+\<^item> \<^theory_text>\<open>@{term_ \<open>term\<close> }\<close> parses and type-checks \<open>term\<close> with term antiquotations,
+  for instance \<^theory_text>\<open>@{term_ \<open>@{cenelec-term \<open>FT\<close>}\<close>}\<close> will parse and check
+  that \<open>FT\<close> is indeed an instance of the class \<^typ>\<open>cenelec_term\<close>,
+\<close>
+
+subsection\<open>A Domain-Specific Ontology: \<^verbatim>\<open>CENELEC_50128\<close>\<close>
+(*<*)
+ML\<open>val toLaTeX = String.translate (fn c => if c = #"_" then "\\_" else String.implode[c])\<close>     
+ML\<open>writeln (DOF_core.print_doc_class_tree 
+                 @{context} (fn (n,l) =>  true (*     String.isPrefix "technical_report" l 
+                                         orelse String.isPrefix "Isa_COL" l *)) 
+                 toLaTeX)\<close>
+(*>*)
+text\<open> The \<^verbatim>\<open>CENELEC_50128\<close> ontology in \<^theory>\<open>Isabelle_DOF-Ontologies.CENELEC_50128\<close>
+is an example of a domain-specific ontology.
+It is based on  \<^verbatim>\<open>technical_report\<close> since we assume that this kind of format will be most
+appropriate for this type of long-and-tedious documents,
+
+%
+\begin{center}
+\begin{minipage}{.9\textwidth}\footnotesize
+\dirtree{%
+.0 .
+.1 CENELEC\_50128.judgement\DTcomment{...}.
+.1 CENELEC\_50128.test\_item\DTcomment{...}.
+.2 CENELEC\_50128.test\_case\DTcomment{...}.
+.2 CENELEC\_50128.test\_tool\DTcomment{...}.
+.2 CENELEC\_50128.test\_result\DTcomment{...}.
+.2 CENELEC\_50128.test\_adm\_role\DTcomment{...}.
+.2 CENELEC\_50128.test\_environment\DTcomment{...}.
+.2 CENELEC\_50128.test\_requirement\DTcomment{...}.
+.2 CENELEC\_50128.test\_specification\DTcomment{...}.
+.1 CENELEC\_50128.objectives\DTcomment{...}.
+.1 CENELEC\_50128.design\_item\DTcomment{...}.
+.2 CENELEC\_50128.interface\DTcomment{...}.
+.1 CENELEC\_50128.sub\_requirement\DTcomment{...}.
+.1 CENELEC\_50128.test\_documentation\DTcomment{...}.
+.1 Isa\_COL.text\_element\DTcomment{...}.
+.2 CENELEC\_50128.requirement\DTcomment{...}.
+.3 CENELEC\_50128.TC\DTcomment{...}.
+.3 CENELEC\_50128.FnI\DTcomment{...}.
+.3 CENELEC\_50128.SIR\DTcomment{...}.
+.3 CENELEC\_50128.CoAS\DTcomment{...}.
+.3 CENELEC\_50128.HtbC\DTcomment{...}.
+.3 CENELEC\_50128.SILA\DTcomment{...}.
+.3 CENELEC\_50128.assumption\DTcomment{...}.
+.4 CENELEC\_50128.AC\DTcomment{...}.
+.5 CENELEC\_50128.EC\DTcomment{...}.
+.6 CENELEC\_50128.SRAC\DTcomment{...}.
+.3 CENELEC\_50128.hypothesis\DTcomment{...}.
+.4 CENELEC\_50128.security\_hyp\DTcomment{...}.
+.3 CENELEC\_50128.safety\_requirement\DTcomment{...}.
+.2 CENELEC\_50128.cenelec\_text\DTcomment{...}.
+.3 CENELEC\_50128.SWAS\DTcomment{...}.
+.3 [...].
+.2 scholarly\_paper.text\_section\DTcomment{...}.
+.3 scholarly\_paper.technical\DTcomment{...}.
+.4 scholarly\_paper.math\_content\DTcomment{...}.
+.5 CENELEC\_50128.semi\_formal\_content\DTcomment{...}.
+.1 ...
+}
+\end{minipage}
+\end{center}
+\<close>
+
+(* TODO : Rearrange ontology hierarchies. *)
+
+subsubsection\<open>Examples\<close>
+
+text\<open>
+The category ``exported constraint (EC)'' is, in the file 
+\<^file>\<open>CENELEC_50128.thy\<close> defined as follows:
+
+@{boxed_theory_text [display]\<open>
+doc_class requirement = text_element +
+   long_name    :: "string option"
+   is_concerned :: "role set"
+doc_class assumption = requirement +
+     assumption_kind :: ass_kind <= informal 
+doc_class AC = assumption +
+   is_concerned :: "role set" <= "UNIV"
+doc_class EC = AC  +
+     assumption_kind :: ass_kind <= (*default *) formal
+\<close>}
+\<close>
+text\<open>
+We now define the document representations, in the file 
+\<^file>\<open>DOF-CENELEC_50128.sty\<close>. Let us assume that we want to 
+register the definition of EC's in a dedicated table of contents (\<^boxed_latex>\<open>tos\<close>) 
+and use an earlier defined environment \inlineltx|\begin{EC}...\end{EC}| for their graphical 
+representation. Note that the \inlineltx|\newisadof{}[]{}|-command requires the 
+full-qualified names, \<^eg>, \<^boxed_theory_text>\<open>text.CENELEC_50128.EC\<close> for the document class and 
+\<^boxed_theory_text>\<open>CENELEC_50128.requirement.long_name\<close> for the  attribute \<^const>\<open>long_name\<close>, 
+inherited from the document class \<^typ>\<open>requirement\<close>. The representation of \<^typ>\<open>EC\<close>'s
+can now be defined as follows:
+% TODO:
+% Explain the text qualifier of the long_name text.CENELEC_50128.EC
+
+\begin{ltx}
+\newisadof{text.CENELEC_50128.EC}%
+[label=,type=%
+,Isa_COL.text_element.level=%
+,Isa_COL.text_element.referentiable=%
+,Isa_COL.text_element.variants=%
+,CENELEC_50128.requirement.is_concerned=%
+,CENELEC_50128.requirement.long_name=%
+,CENELEC_50128.EC.assumption_kind=][1]{%
+\begin{isamarkuptext}%
+   \ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%
+      % If long_name is not defined, we only create an entry in the table tos
+      % using the auto-generated number of the EC 
+      \begin{EC}%
+          \addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}}%
+    }{%
+      % If long_name is defined, we use the long_name as title in the 
+      % layout of the EC, in the table "tos" and as index entry. .
+      \begin{EC}[\commandkey{CENELEC_50128.requirement.long_name}]%
+        \addxcontentsline{toe}{chapter}[]{\autoref{\commandkey{label}}: %
+              \commandkey{CENELEC_50128.requirement.long_name}}%
+        \DOFindex{EC}{\commandkey{CENELEC_50128.requirement.long_name}}%
+    }%
+    \label{\commandkey{label}}% we use the label attribute as anchor 
+    #1% The main text of the EC
+  \end{EC}
+\end{isamarkuptext}%
+}
+\end{ltx}
+\<close>
+text\<open>
+  For example, the @{docitem "ass123"} from page \pageref{ass123} is mapped to
+
+@{boxed_latex [display]
+\<open>\begin{isamarkuptext*}%
+[label = {ass122},type = {CENELEC_50128.SRAC}, 
+ args={label = {ass122}, type = {CENELEC_50128.SRAC}, 
+       CENELEC_50128.EC.assumption_kind = {formal}}
+] The overall sampling frequence of the odometer subsystem is therefore 
+ 14 khz, which includes sampling, computing and result communication 
+ times ...
+\end{isamarkuptext*}\<close>}
+
+This environment is mapped to a plain \<^LaTeX> command via:
+@{boxed_latex [display]
+\<open> \NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}} \<close>}
+\<close>
+text\<open>
+For the command-based setup, \<^isadof> provides a dispatcher that selects the most specific 
+implementation for a given \<^boxed_theory_text>\<open>doc_class\<close>:
+
+@{boxed_latex [display]
+\<open>%% The Isabelle/DOF dispatcher:
+\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{%
+  \ifcsname isaDof.\commandkey{type}\endcsname%
+      \csname isaDof.\commandkey{type}\endcsname%
+              [label=\commandkey{label},\commandkey{args}]{#1}%
+  \else\relax\fi%
+  \ifcsname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
+      \csname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
+              [label=\commandkey{label},\commandkey{args}]{#1}%
+  \else%
+      \message{Isabelle/DOF: Using default LaTeX representation for concept %
+        "\commandkey{env}.\commandkey{type}".}%
+      \ifcsname isaDof.\commandkey{env}\endcsname%
+         \csname isaDof.\commandkey{env}\endcsname%
+                [label=\commandkey{label}]{#1}%
+      \else%
+      \errmessage{Isabelle/DOF: No LaTeX representation for concept %
+        "\commandkey{env}.\commandkey{type}" defined and no default %
+        definition for "\commandkey{env}" available either.}%
+      \fi%
+  \fi%
+}\<close>}
+\<close>
+
+
+
+(*<<*)  
+end 
+(*>>*)  

Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy

@@ -11,7 +11,7 @@
  *   SPDX-License-Identifier: BSD-2-Clause
  *************************************************************************)
 
-section\<open>A conceptual introduction into DOF and its features:\<close>
+chapter\<open>A conceptual introduction into DOF and its features:\<close>
 
 theory 
   Conceptual
@@ -20,23 +20,25 @@ imports
   "Isabelle_DOF.Isa_COL"
 begin
 
+section\<open>Excursion: On the semantic consequences of this definition: \<close>
+
+text\<open>Consider the following document class definition and its consequences:\<close>
 
 doc_class A =
    level :: "int option"
    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.).
+(cf. \<^url>\<open>https://isabelle.in.tum.de/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> 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>;
+\<^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:
@@ -49,23 +51,61 @@ Consequently, \<^theory_text>\<open>doc_class\<close>'es inherit the entire theo
     \<^enum> @{thm [display] A.simps(6)}
     \<^enum> ...
 \<close>
-(* the generated theory of the \<^theory_text>\<open>doc_class\<close> A can be inspected, of course, by *)
+
+text\<open>The generated theory of the \<^theory_text>\<open>doc_class\<close> A can be inspected, of course, by:\<close>  
 find_theorems (60) name:Conceptual name:A
 
+text\<open>A more abstract view on the state of the DOF machine can be found here:\<close>
+
+print_doc_classes
+
+print_doc_items
+
+text\<open>... and an ML-level output:\<close>
+
+ML\<open>
+val docitem_tab = DOF_core.get_instances \<^context>;
+val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>;
+val docclass_tab = DOF_core.get_onto_classes \<^context>;
+
+\<close>
+
+ML\<open>
+Name_Space.dest_table docitem_tab;
+Name_Space.dest_table isa_transformer_tab;
+Name_Space.dest_table docclass_tab;
+\<close>
+text\<open>... or as ML assertion: \<close>
+ML\<open> 
+@{assert} (Name_Space.dest_table docitem_tab = []);
+fun match ("Conceptual.A", (* the long-name *)
+            DOF_core.Onto_Class {params, name, virtual,inherits_from=NONE, 
+                                 attribute_decl, rejectS=[],rex=[], invs=[]}) 
+            = (Binding.name_of name = "A")
+  | match _ = false;
+
+@{assert} (exists match (Name_Space.dest_table docclass_tab))
+\<close>
 
 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
+text\<open>And further, 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>}
+@{term \<open>the(A.level (A.make 3 (Some 4) 5))\<close>};
+fun match (Const("Option.option.the",_) $ 
+      (Const ("Conceptual.A.level",_) $  
+         (Const ("Conceptual.A.make", _) $ u $ v $ w))) = true
+   |match _ = false;
+@{assert} (match @{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>
+text\<open>And finally, via the code-generation, we have the following programmable 
+     access to values representing class instances:\<close>
 ML\<open>
 val A_make = @{code A.make};
 val zero   = @{code "0::int"};
@@ -75,9 +115,9 @@ val add    = @{code "(+) :: int \<Rightarrow> int \<Rightarrow> int"};
 A_make zero (SOME one) (add one one)
 \<close>
 
+section\<open>Building up a conceptual class hierarchy:\<close>
 
-subsection\<open>An independent class-tree root: \<close>
-
+text\<open>An independent class-tree root: \<close>
 
 doc_class B =
    level :: "int option"
@@ -89,7 +129,7 @@ text\<open>We may even use type-synonyms for class synonyms ...\<close>
 type_synonym XX = B
 
 
-subsection\<open>Examples of inheritance \<close>
+section\<open>Examples of inheritance \<close>
 
 doc_class C = XX +                           
    z :: "A option"             <= None      (* A LINK, i.e. an attribute that has a type
@@ -125,7 +165,7 @@ doc_class F  =
         and  br':: "r \<sigma> \<noteq> [] \<and> length(b' \<sigma>) \<ge> 3"
         and  cr :: "properties \<sigma> \<noteq> []"
 
-text\<open>The effect of the invariant declaration is to provide intern definitions for validation 
+text\<open>The effect of the invariant declaration is to provide intern HOL definitions for validation 
 functions of this invariant. They can be referenced as follows:\<close>
 thm br_inv_def
 thm br'_inv_def
@@ -133,7 +173,7 @@ 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>) "
+term "br'_inv (\<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.
 Note, however, that not everything that we can write in an invariant (basically: HOL) is executable,
@@ -141,7 +181,7 @@ 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>
 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>this does not work ...\<close> 
 
 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
@@ -151,22 +191,27 @@ ML\<open> val br'_inv_code = @{code "br'_inv"} \<close> \<comment> \<open>does w
 
 text\<open>... is compilable ...\<close>
 
-
-
 doc_class G = C +
-   g :: "thm"  <= "@{thm \<open>HOL.refl\<close>}"
+   g :: "thm"  <= "@{thm \<open>HOL.refl\<close>}"  (* warning overriding attribute expected*)
 
 doc_class M = 
    ok :: "unit"
    accepts "A ~~ \<lbrace>C || D\<rbrace>\<^sup>* ~~ \<lbrakk>F\<rbrakk>"
 
+text\<open>The final class and item tables look like this:\<close>
+print_doc_classes
+print_doc_items
+
+ML\<open>
+let  val class_ids_so_far = ["Conceptual.A", "Conceptual.B", "Conceptual.C", "Conceptual.D", 
+                             "Conceptual.E", "Conceptual.F", "Conceptual.G", "Conceptual.M", 
+                             "Isa_COL.figure", "Isa_COL.chapter", "Isa_COL.figure2", "Isa_COL.section", 
+                             "Isa_COL.subsection", "Isa_COL.figure_group", "Isa_COL.text_element", 
+                             "Isa_COL.subsubsection", "Isa_COL.side_by_side_figure"]
+     val docclass_tab = map fst (Name_Space.dest_table (DOF_core.get_onto_classes \<^context>));
+in @{assert} (class_ids_so_far = docclass_tab) end\<close>
+
 
-(*
-ML\<open> Document.state();\<close>
-ML\<open> Session.get_keywords(); (* this looks to be really session global. *)
-    Outer_Syntax.command; \<close>
-ML\<open> Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \<close>
-*)
 
 open_monitor*[aaa::M]
 section*[test::A]\<open>Test and Validation\<close>
@@ -177,4 +222,49 @@ text*[ sdfg :: F] \<open> Lorem ipsum @{thm refl}\<close>
 text*[ xxxy ] \<open> Lorem ipsum @{F \<open>sdfg\<close>} rate @{thm refl}\<close>  
 close_monitor*[aaa]
 
-end     
+doc_class test_monitor_free =
+  tmhd :: int
+doc_class test_monitor_head =
+  tmhd :: int
+doc_class test_monitor_A = test_monitor_head +
+  tmA :: int
+doc_class test_monitor_B = test_monitor_A +
+  tmB :: int
+doc_class test_monitor_C = test_monitor_A +
+  tmC :: int
+doc_class test_monitor_D = test_monitor_B +
+  tmD :: int
+doc_class test_monitor_E = test_monitor_D +
+  tmE :: int
+
+doc_class monitor_M =
+  tmM :: int
+  rejects "test_monitor_A"
+  accepts "test_monitor_head ~~ test_monitor_B ~~ test_monitor_C"
+
+declare[[free_class_in_monitor_checking]]
+
+open_monitor*[test_monitor_M::monitor_M]
+
+text*[testFree::test_monitor_free]\<open>\<close>
+
+open_monitor*[test_monitor_M2::monitor_M]
+
+text*[test_monitor_A1::test_monitor_A]\<open>\<close>
+text*[testFree2::test_monitor_free]\<open>\<close>
+text*[test_monitor_head1::test_monitor_head]\<open>\<close>
+text*[testFree3::test_monitor_free]\<open>\<close>
+text*[test_monitor_B1::test_monitor_B]\<open>\<close>
+text*[testFree4::test_monitor_free]\<open>\<close>
+text*[test_monitor_D1::test_monitor_D]\<open>\<close>
+text*[testFree5::test_monitor_free]\<open>\<close>
+text*[test_monitor_C1::test_monitor_C]\<open>\<close>
+text*[testFree6::test_monitor_free]\<open>\<close>
+
+close_monitor*[test_monitor_M2]
+
+close_monitor*[test_monitor_M]
+
+declare[[free_class_in_monitor_checking = false]]
+
+end

Isabelle_DOF-Ontologies/ROOT

@@ -0,0 +1,23 @@
+session "Isabelle_DOF-Ontologies" = "Isabelle_DOF" + 
+  options  [document = pdf, document_output = "output", document_build = dof]
+  directories
+    "CC_v3_1_R5"
+    "Conceptual"
+    "small_math"
+    "CENELEC_50128"
+  theories
+    "document_setup"
+    "document-templates"
+    "CC_v3_1_R5/CC_v3_1_R5"
+    "CC_v3_1_R5/CC_terminology"  
+    "Conceptual/Conceptual"
+    "small_math/small_math"
+    "CENELEC_50128/CENELEC_50128"
+    "CENELEC_50128/CENELEC_50128_Documentation"
+  document_files
+    "root.bib"
+    "lstisadof-manual.sty"
+    "preamble.tex"
+    "figures/antiquotations-PIDE.png"
+    "figures/srac-as-es-application.png"
+    "figures/srac-definition.png"

Isabelle_DOF-Ontologies/document-templates.thy

@@ -0,0 +1,27 @@
+(*************************************************************************
+ * Copyright (C) 
+ *               2019      The University of Exeter 
+ *               2018-2019 The University of Paris-Saclay
+ *               2018      The University of Sheffield
+ *
+ * License:
+ *   This program can be redistributed and/or modified under the terms
+ *   of the 2-clause BSD-style license.
+ *
+ *   SPDX-License-Identifier: BSD-2-Clause
+ *************************************************************************)
+
+theory 
+  "document-templates"
+imports
+  "Isabelle_DOF.Isa_DOF"
+begin
+
+define_template "./document-templates/root-eptcs-UNSUPPORTED.tex" 
+                "Unsupported template for the EPTCS class. Not for general use."
+define_template "./document-templates/root-lipics-v2021-UNSUPPORTED.tex" 
+                "Unsupported template for LIPICS (v2021). Not for general use."
+define_template "./document-templates/root-svjour3-UNSUPPORTED.tex" 
+                "Unsupported template for SVJOUR. Not for general use."
+
+end

Isabelle_DOF-Ontologies/document-templates/root-eptcs-UNSUPPORTED.tex

@@ -66,7 +66,7 @@
 
 \begin{document}
 \maketitle
-\input{session}
+\IfFileExists{dof_session.tex}{\input{dof_session}}{\input{session}}
 % optional bibliography
 \IfFileExists{root.bib}{%
     \bibliography{root}

Isabelle_DOF-Ontologies/document-templates/root-lipics-v2021-UNSUPPORTED.tex

@@ -19,8 +19,6 @@
 %% you need to download lipics.cls from 
 %% https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/
 %% and add it manually to the praemble.tex and the ROOT file.
-%% Moreover, the option "document_comment_latex=true" needs to be set 
-%% in the ROOT file.
 %%
 %% All customization and/or additional packages should be added to the file
 %% preamble.tex.
@@ -64,7 +62,7 @@
 
 \begin{document}
 \maketitle
-\input{session}
+\IfFileExists{dof_session.tex}{\input{dof_session}}{\input{session}}
 % optional bibliography
 \IfFileExists{root.bib}{%
 \small  

Isabelle_DOF-Ontologies/document-templates/root-svjour3-UNSUPPORTED.tex

@@ -57,7 +57,7 @@
 \newcommand{\lstnumberautorefname}{Line}
 
 \maketitle
-\input{session}
+\IfFileExists{dof_session.tex}{\input{dof_session}}{\input{session}}
 % optional bibliography
 \IfFileExists{root.bib}{{\bibliography{root}}}{}
 \end{document}

Isabelle_DOF-Ontologies/document/lstisadof-manual.sty

@@ -296,3 +296,34 @@
   }%
 %% </bash>
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%% <config>
+\providecolor{config}{named}{gray}
+\newtcblisting{config}[2][]{%
+      listing only%
+     ,boxrule=0pt
+     ,boxsep=0pt
+     ,colback=white!90!config
+     ,enhanced jigsaw
+     ,borderline west={2pt}{0pt}{config!60!black}
+     ,sharp corners
+     % ,before skip=10pt
+     % ,after skip=10pt
+     ,enlarge top by=0mm
+     ,enhanced
+     ,overlay={\node[draw,fill=config!60!black,xshift=0pt,anchor=north
+       east,font=\bfseries\footnotesize\color{white}]
+                at (frame.north east) {#2};}
+        ,listing options={
+           breakatwhitespace=true
+          ,columns=flexible%
+          ,basicstyle=\small\ttfamily
+          ,mathescape
+          ,#1
+      }
+  }%
+%% </config>
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+

Isabelle_DOF-Ontologies/document/preamble.tex

@@ -0,0 +1,4 @@
+\usepackage{dirtree}
+\renewcommand*\DTstylecomment{\ttfamily\itshape}
+
+\usepackage{lstisadof-manual}

Isabelle_DOF-Ontologies/document/root.bib

@@ -451,7 +451,7 @@
   journal	= {Archive of Formal Proofs},
   month		= may,
   year		= 2010,
-  note		= {\url{http://isa-afp.org/entries/Regular-Sets.html}, Formal
+  note		= {\url{https://isa-afp.org/entries/Regular-Sets.html}, Formal
 		  proof development},
   issn		= {2150-914x}
 }
@@ -462,7 +462,7 @@
   journal	= {Archive of Formal Proofs},
   month		= mar,
   year		= 2004,
-  note		= {\url{http://isa-afp.org/entries/Functional-Automata.html},
+  note		= {\url{https://isa-afp.org/entries/Functional-Automata.html},
 		  Formal proof development},
   issn		= {2150-914x}
 }

Isabelle_DOF-Ontologies/document_setup.thy

@@ -0,0 +1,18 @@
+(*<*)
+theory "document_setup"
+  imports
+  "Isabelle_DOF.technical_report"
+  "Isabelle_DOF-Ontologies.CENELEC_50128"
+begin
+
+use_template "scrreprt-modern"
+use_ontology "Isabelle_DOF.technical_report" and "Isabelle_DOF-Ontologies.CENELEC_50128"
+
+(*>*)
+
+title*[title::title]         \<open>Isabelle/DOF\<close>
+subtitle*[subtitle::subtitle]\<open>Ontologies\<close>
+
+(*<*)
+end
+(*>*)

Isabelle_DOF-Ontologies/small_math/small_math.thy

@@ -11,10 +11,11 @@
  *   SPDX-License-Identifier: BSD-2-Clause
  *************************************************************************)
 
-section\<open>An example ontology for a math paper\<close>
+chapter\<open>An example ontology for a math paper\<close>
 
 theory small_math
-   imports "Isabelle_DOF.Isa_COL"
+   imports 
+"Isabelle_DOF.Isa_COL"
 begin
 
 doc_class title =
@@ -64,18 +65,22 @@ doc_class result = technical +
 
 
 
-ML\<open>fun check_invariant_invariant oid {is_monitor:bool} ctxt =
-      let val kind_term = AttributeAccess.compute_attr_access ctxt "kind" oid @{here} @{here} 
-          val property_termS = AttributeAccess.compute_attr_access ctxt "property" oid @{here} @{here} 
+ML\<open>
+fn thy =>
+let fun check_invariant_invariant oid {is_monitor:bool} ctxt =
+      let val kind_term = ISA_core.compute_attr_access ctxt "kind" oid NONE @{here} 
+          val property_termS = ISA_core.compute_attr_access ctxt "property" oid NONE @{here} 
           val tS = HOLogic.dest_list property_termS
       in  case kind_term of
             @{term "proof"} => if not(null tS) then true
                                else error("class class invariant violation") 
            | _ => false
       end
+      val binding = DOF_core.binding_from_onto_class_pos "result" thy
+in DOF_core.add_ml_invariant binding check_invariant_invariant thy end
 \<close>
 
-setup\<open>DOF_core.update_class_invariant "small_math.result" check_invariant_invariant\<close>
+(*setup\<open>DOF_core.add_ml_invariant "small_math.result" check_invariant_invariant\<close>*)
 
 
 doc_class example    = technical +
@@ -85,7 +90,7 @@ doc_class "conclusion" = text_section +
     establish   :: "(contribution_claim \<times> result) set"
 
 text\<open> Besides subtyping, there is another relation between
-doc_classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
+doc\_classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
 which is expressed by occurrence in the where clause.
 While sub-classing refers to data-inheritance of attributes,
 a monitor captures structural constraints -- the order --
@@ -137,10 +142,10 @@ fun dest_option _ (Const (@{const_name "None"}, _)) = NONE
 
 in 
 
-fun check ctxt cidS mon_id pos =
-    let val trace  = AttributeAccess.compute_trace_ML ctxt mon_id pos @{here}
+fun check ctxt cidS mon_id pos_opt =
+    let val trace  = AttributeAccess.compute_trace_ML ctxt mon_id pos_opt @{here}
         val groups = partition (Context.proof_of ctxt) cidS trace
-        fun get_level_raw oid = AttributeAccess.compute_attr_access ctxt "level" oid @{here} @{here};
+        fun get_level_raw oid = ISA_core.compute_attr_access ctxt "level" oid NONE @{here};
         fun get_level oid = dest_option (snd o HOLogic.dest_number) (get_level_raw (oid));
         fun check_level_hd a = case (get_level (snd a)) of
                                   NONE => error("Invariant violation: leading section" ^ snd a ^ 
@@ -164,10 +169,15 @@ end
 end
 \<close>
 
-setup\<open> let val cidS = ["small_math.introduction","small_math.technical", "small_math.conclusion"];
-           fun body moni_oid _ ctxt = (Small_Math_trace_invariant.check  ctxt cidS moni_oid @{here};
+setup\<open>
+fn thy =>
+let val cidS = ["small_math.introduction","small_math.technical", "small_math.conclusion"];
+           fun body moni_oid _ ctxt = (Small_Math_trace_invariant.check  ctxt cidS moni_oid NONE;
                                        true)
-       in  DOF_core.update_class_invariant "small_math.article" body end\<close>
+    val ctxt = Proof_Context.init_global thy
+    val binding = DOF_core.binding_from_onto_class_pos "article" thy
+in DOF_core.add_ml_invariant binding body thy end
+\<close>
 
 end
 

Isabelle_DOF-Proofs/ROOT

@@ -0,0 +1,10 @@
+session "Isabelle_DOF-Proofs" (proofs) = "HOL-Proofs" +
+  options [document = false,  record_proofs = 2, parallel_limit = 500, document_build = dof]
+  sessions
+    "Isabelle_DOF"
+    Metalogic_ProofChecker
+  theories
+    Isabelle_DOF.ontologies
+    Isabelle_DOF.Isa_DOF
+    Very_Deep_DOF
+    Reification_Test

Isabelle_DOF-Proofs/Reification_Test.thy

@@ -0,0 +1,739 @@
+theory Reification_Test
+  imports "Isabelle_DOF-Proofs.Very_Deep_DOF"
+
+begin
+
+ML\<open>
+val ty1 = ISA_core.reify_typ @{typ "int"}
+val ty2 = ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
+val ty3 = ISA_core.reify_typ @{typ "prop"}
+val ty4 = ISA_core.reify_typ @{typ "'a list"}
+\<close>
+
+term*\<open>@{typ \<open>int\<close>}\<close>
+value*\<open>@{typ \<open>int\<close>}\<close>
+value*\<open>@{typ \<open>int \<Rightarrow> bool\<close>}\<close>
+term*\<open>@{typ \<open>prop\<close>}\<close>
+value*\<open>@{typ \<open>prop\<close>}\<close>
+term*\<open>@{typ \<open>'a list\<close>}\<close>
+value*\<open>@{typ \<open>'a list\<close>}\<close>
+
+ML\<open>
+val t1 = ISA_core.reify_term @{term "1::int"}
+val t2 = ISA_core.reify_term @{term "\<lambda>x. x = 1"}
+val t3 = ISA_core.reify_term @{term "[2, 3::int]"}
+\<close>
+term*\<open>@{term \<open>1::int\<close>}\<close>
+value*\<open>@{term \<open>1::int\<close>}\<close>
+term*\<open>@{term \<open>\<lambda>x. x = 1\<close>}\<close>
+value*\<open>@{term \<open>\<lambda>x. x = 1\<close>}\<close>
+term*\<open>@{term \<open>[2, 3::int]\<close>}\<close>
+value*\<open>@{term \<open>[2, 3::int]\<close>}\<close>
+
+prf refl
+full_prf refl
+
+term*\<open>@{thm \<open>HOL.refl\<close>}\<close>
+value*\<open>proof @{thm \<open>HOL.refl\<close>}\<close>
+value*\<open>proof @{thm \<open>HOL.refl\<close>}\<close>
+value*\<open>depth (proof @{thm \<open>HOL.refl\<close>})\<close>
+value*\<open>size (proof @{thm \<open>HOL.refl\<close>})\<close>
+value*\<open>fv_Proof (proof @{thm \<open>HOL.refl\<close>})\<close>
+term*\<open>@{thms-of \<open>HOL.refl\<close>}\<close>
+value*\<open>@{thms-of \<open>HOL.refl\<close>}\<close>
+
+ML\<open>
+val t_schematic = TVar(("'a",0), [])
+val t = @{term "Tv (Var (STR '''a'', 0)) {}"}
+val rt_schematic = ISA_core.reify_typ t_schematic
+val true = rt_schematic = t
+\<close>
+
+lemma test : "A \<and> B \<longrightarrow> B \<and> A"
+  by auto
+
+lemma test2 : "A \<and> B \<Longrightarrow> B \<and> A"
+  by auto
+
+lemma test3: "A \<and> B \<longrightarrow> B \<and> A"
+proof
+  assume "A \<and> B"
+  then obtain B and A ..
+  then show "B \<and> A" ..
+qed
+
+lemma test4:
+  assumes "(A \<and> B)"
+  shows "B \<and> A"
+  apply (insert assms)
+  by auto
+
+lemma test_subst : "\<lbrakk>x = f x; odd(f x)\<rbrakk> \<Longrightarrow> odd x"
+  by (erule ssubst)
+
+inductive_set even' :: "nat set" where
+    "0 \<in> even'"
+  | "n \<in> even' \<Longrightarrow> (Suc (Suc n)) \<in> even'"
+
+find_theorems name:"even'.induct"
+
+
+(*lemma even_dvd : "n \<in> even' \<Longrightarrow> 2 dvd n"
+proof(induct n)
+  case 0 then show ?case by simp
+next 
+  case (Suc n) then show ?case
+    apply (simp add: dvd_def)
+    apply (rule_tac x ="Suc k" in exI)
+    apply clarify*)
+
+theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
+proof
+  assume "(A \<longrightarrow> B) \<longrightarrow> A"
+  show A
+  proof (rule classical)
+    assume "\<not> A"
+    have "A \<longrightarrow> B"
+    proof
+      assume A
+      with \<open>\<not> A\<close> show B by contradiction
+    qed
+    with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..
+  qed
+qed
+
+(*lemma even_dvd : "n \<in> even' \<Longrightarrow> 2 dvd n"
+using [[simp_trace]]
+  apply (induct n)
+   apply (subst even_zero)
+  apply(rule TrueI)
+
+  apply(simp)*)
+
+lemma even_dvd : "n \<in> even' \<Longrightarrow> 2 dvd n"
+  apply (erule even'.induct)
+   apply (simp_all add: dvd_def)
+  using [[simp_trace]]
+  apply clarify
+  find_theorems name:"_ = 2 * _"
+  apply (rule_tac x ="Suc k" in exI)
+using [[simp_trace]]
+  apply simp
+  done
+
+(*
+lemma even_dvd : "n \<in> even' \<Longrightarrow> 2 dvd n"
+apply (induct_tac rule:even'.induct)*)
+
+inductive ev :: " nat \<Rightarrow> bool " where
+  ev0: " ev 0 " |
+  evSS: " ev n \<Longrightarrow> ev (n + 2) "
+
+fun evn :: " nat \<Rightarrow> bool " where
+  " evn 0 = True " |
+  " evn (Suc 0) = False " |
+  " evn (Suc (Suc n)) = evn n "
+
+(*lemma assumes a: " ev (Suc(Suc m)) " shows" ev m "
+proof(induction  "Suc (Suc m)" arbitrary: " m " rule: ev.induct)*)
+
+(*lemma " ev (Suc (Suc m)) \<Longrightarrow> ev m " 
+proof(induction " Suc (Suc m) " arbitrary: " m " rule: ev.induct)
+  case ev0
+  then show ?case sorry
+next
+  case (evSS n)
+  then show ?case sorry
+qed*)
+
+(* And neither of these can apply the induction *)
+(*
+lemma assumes a1: " ev n " and a2: " n = (Suc (Suc m)) " shows " ev m "
+proof (induction " n " arbitrary: " m " rule: ev.induct)
+
+lemma assumes a1: " n = (Suc (Suc m)) " and a2: "ev n " shows " ev m "
+proof (induction " n " arbitrary: " m " rule: ev.induct)
+*)
+
+(* But this one can ?! *)
+(*
+lemma assumes a1: " ev n " and a2: " n = (Suc (Suc m)) " shows " ev m "
+proof -
+  from a1 and a2 show " ev m "
+  proof (induction " n " arbitrary: " m " rule: ev.induct)
+    case ev0
+    then show ?case by simp
+  next
+    case (evSS n) thus ?case by simp
+  qed
+qed
+*)
+
+inductive_set even :: "int set" where
+zero[intro!]: "0 \<in> even" |
+plus[intro!]: "n \<in> even \<Longrightarrow> n+2 \<in> even " |
+min[intro!]: "n \<in> even \<Longrightarrow> n-2 \<in> even "
+
+lemma a : "2+2=4" by simp
+
+lemma b : "(0::int)+2=2" by simp
+
+lemma test_subst_2 : "4 \<in> even"
+  apply (subst a[symmetric])
+  apply (rule plus)
+  apply (subst b[symmetric])
+  apply (rule plus)
+  apply (rule zero)
+  done
+
+
+(*lemma "\<lbrakk>P x y z; Suc x < y\<rbrakk> \<Longrightarrow> f z = x * y"
+  (*using [[simp_trace]]*)
+  (*apply (simp add: mult.commute)*)
+  apply (subst mult.commute)
+  apply (rule mult.commute [THEN ssubst])*)
+
+datatype 'a seq = Empty | Seq 'a "'a seq"
+find_consts name:"Reification_Test*seq*"
+fun conc :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq"
+where
+  c1 :  "conc Empty ys = ys"
+| c2 : "conc (Seq x xs) ys = Seq x (conc xs ys)"
+
+lemma seq_not_eq : "Seq x xs \<noteq> xs"
+using [[simp_trace]]
+proof (induct xs arbitrary: x)
+  case Empty
+  show "Seq x Empty \<noteq> Empty" by simp
+next
+  case (Seq y ys)
+  show "Seq x (Seq y ys) \<noteq> Seq y ys"
+    using \<open>Seq y ys \<noteq> ys\<close> by simp
+qed
+
+lemma identity_conc : "conc xs Empty = xs"
+  using [[simp_trace]]
+  using[[simp_trace_depth_limit=8]]
+  using [[unify_trace_simp]]
+  using[[unify_trace_types]]
+  using [[unify_trace_bound=0]]
+  (* using [[simp_trace_new depth=10]] *)
+  apply (induct xs)
+   apply (subst c1)
+   apply (rule refl)
+  apply (subst c2)
+  apply (rule_tac s="xs" and P="\<lambda>X. Seq x1 X = Seq x1 xs" in subst)
+   apply (rule sym)
+   apply assumption
+  apply (rule refl)
+  done
+
+lemma imp_ex : "(\<exists>x. \<forall>y. P x y) \<longrightarrow> (\<forall>y. \<exists>x. P x y)"
+  using [[simp_trace]]
+  using[[simp_trace_depth_limit=8]]
+  apply (auto)
+done
+
+lemma length_0_conv' [iff]: "(length [] = 0)"
+  apply (subst List.list.size(3))
+  apply (rule refl)
+  done
+
+lemma cons_list : "a#xs = [a]@xs"
+  using [[simp_trace]]
+  apply (subst List.append.append_Cons)
+  apply (subst List.append.append_Nil)
+  apply (rule refl)
+  done
+lemma replacement: "\<lbrakk> a = b; c = d \<rbrakk> \<Longrightarrow> f a c = f b d"
+apply (erule ssubst)+
+apply (rule refl )
+ done
+lemma assoc_append : "k @ (l @ m) = (k @ l ) @ m"
+apply (induct_tac k )
+apply (subst append_Nil )+
+apply (rule refl )
+apply (subst append_Cons)
+apply (subst append_Cons)
+apply (subst append_Cons)
+apply (rule_tac f ="Cons" in replacement)
+apply (rule refl)
+apply assumption
+  done
+
+lemma length_cons : "length (xs @ ys) = length xs + length ys"
+  using [[simp_trace]]
+  apply (subst List.length_append)
+  apply (rule refl)
+  done
+lemma length_plus : "(length [a] + length xs = 0) = ([a] @ xs = [])"
+  using [[simp_trace]]
+  apply (subst List.list.size(4))
+  apply (subst List.list.size(3))
+  apply (subst Nat.add_Suc_right)
+  apply (subst Groups.monoid_add_class.add.right_neutral)
+  apply (subst Nat.plus_nat.add_Suc)
+  apply (subst Groups.monoid_add_class.add.left_neutral)
+apply (subst Nat.old.nat.distinct(2))
+  by simp
+lemma empty_list : "(length [] = 0) = ([] = []) = True"
+  using [[simp_trace]]
+  by simp
+lemma TrueI: True
+using [[simp_trace]]
+  unfolding True_def
+  by (rule refl)
+
+lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"
+  using [[simp_trace]]
+  apply (induct xs)
+   apply (subst List.list.size(3))
+   apply(subst HOL.simp_thms(6))
+   apply(subst HOL.simp_thms(6))
+   apply(rule refl)
+
+  apply (subst cons_list)
+  apply (subst(2) cons_list)
+  apply (subst length_cons)
+  apply (subst length_plus)
+  apply (subst HOL.simp_thms(6))
+  apply (rule TrueI)
+  done
+(*by (induct xs) auto*)
+
+find_theorems (50) name:"HOL.simp_thms"
+find_theorems (50) name:"List.list*size"
+find_theorems (50) name:"List.list*length"
+find_theorems "_ @ _"
+find_theorems (500) "List.length [] = 0"
+find_theorems (550) "length _ = length _ + length _"
+
+
+lemma identity_list : "xs @ [] = xs"
+  using [[simp_trace]]
+  using[[simp_trace_depth_limit=8]]
+  using [[unify_trace_simp]]
+  using[[unify_trace_types]]
+  using [[unify_trace_bound=0]]
+  apply (induct xs)
+  apply (subst List.append_Nil2)
+   apply (subst HOL.simp_thms(6))
+  apply(rule TrueI)
+  apply (subst List.append_Nil2)
+  apply (subst HOL.simp_thms(6))
+  apply(rule TrueI)
+  done
+
+lemma identity_list' : "xs @ [] = xs"
+  using [[simp_trace]]
+  using[[simp_trace_depth_limit=8]]
+  using [[unify_trace_simp]]
+  using[[unify_trace_types]]
+  using [[unify_trace_bound=0]]
+  (* using [[simp_trace_new depth=10]] *)
+  apply (induct "length xs")
+  apply (subst (asm) zero_reorient)
+  apply(subst(asm) length_0_conv)
+   apply (subst List.append_Nil2)
+   apply (subst HOL.simp_thms(6))
+  apply (rule TrueI)
+     apply (subst List.append_Nil2)
+  apply (subst HOL.simp_thms(6))
+  apply (rule TrueI)
+  done
+
+lemma conj_test : "A \<and> B \<and> C \<longrightarrow> B \<and> A"
+  apply (rule impI)
+  apply (rule conjI)
+  apply (drule conjunct2)
+   apply (drule conjunct1)
+   apply assumption
+    apply (drule conjunct1)
+  apply assumption
+  done
+
+declare[[show_sorts]]
+declare[[ML_print_depth = 20]]
+
+ML\<open>
+val full = true
+val thm = @{thm "test"}
+val hyps = Thm.hyps_of thm
+val prems = Thm.prems_of thm
+val reconstruct_proof = Thm.reconstruct_proof_of thm
+val standard_proof = Proof_Syntax.standard_proof_of
+          {full = full, expand_name = Thm.expand_name thm} thm
+val term_of_proof = Proof_Syntax.term_of_proof standard_proof
+\<close>
+
+lemma identity_conc' : "conc xs Empty = xs"
+  using [[simp_trace]]
+  using[[simp_trace_depth_limit=8]]
+  using [[unify_trace_simp]]
+  using[[unify_trace_types]]
+  using [[unify_trace_bound=0]]
+  (* using [[simp_trace_new depth=10]] *)
+  apply (induct xs)
+   apply (subst c1)
+   apply (rule refl)
+  apply (subst c2)
+  apply (rule_tac s="xs" and P="\<lambda>X. Seq x1 X = Seq x1 xs" in subst)
+   apply (rule sym)
+   apply assumption
+  apply (rule refl)
+  done
+
+declare[[show_sorts = false]]
+
+ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
+ML\<open>
+  val thm = @{thm "identity_conc'"};
+
+  (*proof body with digest*)
+  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
+
+  (*proof term only*)
+  val prf = Proofterm.proof_of body;
+
+  (*clean output*)
+  Pretty.writeln (Proof_Syntax.pretty_proof \<^context> prf);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
+
+  (*all theorems used in the graph of nested proofs*)
+  val all_thms =
+    Proofterm.fold_body_thms
+      (fn {name, ...} => insert (op =) name) [body] [];
+\<close>
+
+term*\<open>@{thm \<open>Reification_Test.identity_conc\<close>}\<close>
+value*\<open>proof @{thm \<open>Reification_Test.identity_conc\<close>}\<close>
+
+lemma cons_list' : "a#xs = [a]@xs"
+  using [[simp_trace]]
+  apply (subst List.append.append_Cons)
+  apply (subst List.append.append_Nil)
+  apply (rule refl)
+  done
+
+ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
+ML\<open>
+  val thm = @{thm "cons_list'"};
+
+  (*proof body with digest*)
+  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
+
+  (*proof term only*)
+  val prf = Proofterm.proof_of body;
+
+  (*clean output*)
+  Pretty.writeln (Proof_Syntax.pretty_proof \<^context> prf);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
+
+  (*all theorems used in the graph of nested proofs*)
+  val all_thms =
+    Proofterm.fold_body_thms
+      (fn {name, ...} => insert (op =) name) [body] [];
+\<close>
+
+declare[[show_sorts = false]]
+declare[[ML_print_depth = 20]]
+
+ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
+ML\<open>
+  val thm = @{thm "test"};
+
+  (*proof body with digest*)
+  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
+
+  (*proof term only*)
+  val prf = Proofterm.proof_of body;
+
+  (*clean output*)
+  Pretty.writeln (Proof_Syntax.pretty_proof \<^context> prf);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
+
+  (*all theorems used in the graph of nested proofs*)
+  val all_thms =
+    Proofterm.fold_body_thms
+      (fn {name, ...} => insert (op =) name) [body] [];
+\<close>
+
+prf test
+full_prf test
+term*\<open>@{thm \<open>Reification_Test.test\<close>}\<close>
+value*\<open>proof @{thm \<open>Reification_Test.test\<close>}\<close>
+term*\<open>@{thms-of \<open>Reification_Test.test\<close>}\<close>
+value*\<open>@{thms-of \<open>Reification_Test.test\<close>}\<close>
+
+ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
+ML\<open>
+  val thm = @{thm test2};
+
+  (*proof body with digest*)
+  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
+
+  (*proof term only*)
+  val prf = Proofterm.proof_of body;
+
+  (*clean output*)
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
+
+  (*all theorems used in the graph of nested proofs*)
+  val all_thms =
+    Proofterm.fold_body_thms
+      (fn {name, ...} => insert (op =) name) [body] [];
+\<close>
+
+prf test2
+full_prf test2
+term*\<open>@{thm \<open>Reification_Test.test2\<close>}\<close>
+value*\<open>proof @{thm \<open>Reification_Test.test2\<close>}\<close>
+
+ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
+ML\<open>
+  val thm = @{thm test3};
+
+  (*proof body with digest*)
+  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
+
+  (*proof term only*)
+  val prf = Proofterm.proof_of body;
+
+  (*clean output*)
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
+
+  (*all theorems used in the graph of nested proofs*)
+  val all_thms =
+    Proofterm.fold_body_thms
+      (fn {name, ...} => insert (op =) name) [body] [];
+\<close>
+
+prf test3
+full_prf test3
+term*\<open>@{thm \<open>Reification_Test.test3\<close>}\<close>
+value*\<open>@{thm \<open>Reification_Test.test3\<close>}\<close>
+
+ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
+ML\<open>
+  val thm = @{thm test4};
+
+  (*proof body with digest*)
+  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
+
+  (*proof term only*)
+  val prf = Proofterm.proof_of body;
+
+  (*clean output*)
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
+
+  (*all theorems used in the graph of nested proofs*)
+  val all_thms =
+    Proofterm.fold_body_thms
+      (fn {name, ...} => insert (op =) name) [body] [];
+\<close>
+
+prf test4
+full_prf test4
+term*\<open>@{thm \<open>Reification_Test.test4\<close>}\<close>
+value*\<open>@{thm \<open>Reification_Test.test4\<close>}\<close>
+
+ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
+ML\<open>
+  val thm = @{thm Pure.symmetric};
+
+  (*proof body with digest*)
+  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
+
+  (*proof term only*)
+  val prf = Proofterm.proof_of body;
+
+  (*clean output*)
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
+
+  (*all theorems used in the graph of nested proofs*)
+  val all_thms =
+    Proofterm.fold_body_thms
+      (fn {name, ...} => insert (op =) name) [body] [];
+\<close>
+
+prf symmetric
+full_prf symmetric
+term*\<open>@{thm \<open>Pure.symmetric\<close>}\<close>
+value*\<open>proof @{thm \<open>Pure.symmetric\<close>}\<close>
+
+ML\<open>
+val full = true
+val thm = @{thm "Groups.minus_class.super"}
+val standard_proof = Proof_Syntax.standard_proof_of
+          {full = full, expand_name = Thm.expand_name thm} thm
+val term_of_proof = Proof_Syntax.term_of_proof standard_proof
+\<close>
+
+ML\<open>
+val thm = Proof_Context.get_thm \<^context> "Groups.minus_class.super"
+val prop = Thm.prop_of thm
+val proof = Thm.proof_of thm
+\<close>
+
+prf Groups.minus_class.super
+full_prf Groups.minus_class.super
+term*\<open>@{thm \<open>Groups.minus_class.super\<close>}\<close>
+value*\<open>@{thm \<open>Groups.minus_class.super\<close>}\<close>
+
+(*ML\<open>
+val full = true
+val thm = @{thm "Homotopy.starlike_imp_contractible"}
+val standard_proof = Proof_Syntax.standard_proof_of
+          {full = full, expand_name = Thm.expand_name thm} thm
+val term_of_proof = Proof_Syntax.term_of_proof standard_proof
+\<close>
+
+ML\<open>
+val thm = Proof_Context.get_thm \<^context> "Homotopy.starlike_imp_contractible"
+val prop = Thm.prop_of thm
+val proof = Thm.proof_of thm
+\<close>
+
+prf Homotopy.starlike_imp_contractible
+full_prf Homotopy.starlike_imp_contractible
+term*\<open>@{thm \<open>Homotopy.starlike_imp_contractible\<close>}\<close>
+value*\<open>@{thm \<open>Homotopy.starlike_imp_contractible\<close>}\<close>*)
+
+(* stefan bergofer phd thesis example proof construction 2.3.2 *)
+
+lemma stefan_example : "(\<exists>x. \<forall>y. P x y) \<longrightarrow> (\<forall>y. \<exists>x. P x y)"
+  apply (rule impI)
+  apply(rule allI)
+  apply (erule exE)
+   apply(rule exI)
+  apply(erule allE)
+  apply (assumption)
+  done
+
+ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
+ML\<open>
+  val thm = @{thm stefan_example};
+
+  (*proof body with digest*)
+  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
+
+  (*proof term only*)
+  val prf = Proofterm.proof_of body;
+
+  (*clean output*)
+  Pretty.writeln (Proof_Syntax.pretty_proof \<^context> prf);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
+
+  (*all theorems used in the graph of nested proofs*)
+  val all_thms =
+    Proofterm.fold_body_thms
+      (fn {name, ...} => insert (op =) name) [body] [];
+\<close>
+ML\<open>
+val thy = \<^theory>;
+  val prf =
+    Proof_Syntax.read_proof thy true false
+      "mp \<cdot> _ \<cdot> _ \<bullet> (impI \<cdot> _ \<cdot> _ \<bullet> (conjI \<cdot> _ \<cdot> _ ))";
+      (*"conjI \<cdot> _ \<cdot> _ ";*)
+      (*"(\<^bold>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H)";*)
+(*val t = Proofterm.reconstruct_proof thy \<^prop>\<open>(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B\<close> prf*)
+(*  val thm =  
+    Proofterm.reconstruct_proof thy \<^prop>\<open>A \<Longrightarrow> B\<close> prf
+    |> Proof_Checker.thm_of_proof thy
+    |> Drule.export_without_context
+val pretty =  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);*)
+\<close>
+
+extract_type
+  "typeof (Trueprop P) \<equiv> typeof P"
+
+realizers
+  impI (P, Q): "\<lambda>pq. pq"
+    "\<^bold>\<lambda>(c: _) (d: _) P Q pq (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<^bold>\<lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
+find_consts name:"MinProof"
+
+ML_val \<open>
+  val thy = \<^theory>;
+  val prf =
+    Proof_Syntax.read_proof thy true false
+      "impI \<cdot> _ \<cdot> _ \<bullet> \
+      \   (\<^bold>\<lambda>H: _. \
+      \     conjE \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> H \<bullet> \
+      \       (\<^bold>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
+  val thm =
+    Proofterm.reconstruct_proof thy \<^prop>\<open>A \<and> B \<longrightarrow> B \<and> A\<close> prf
+    |> Proof_Checker.thm_of_proof thy
+    |> Drule.export_without_context;
+val pretty =  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
+\<close>
+ML_file "~~/src/Provers/classical.ML"
+lemma testtest : "A \<and> B \<longrightarrow> B \<and> A"
+  apply (rule impI)
+  apply (erule conjE)
+  apply(erule conjI)
+  apply assumption
+  done
+
+ML\<open> (*See: *) \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close>\<close>
+ML\<open>
+  val thm = @{thm testtest};
+
+  (*proof body with digest*)
+  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
+
+  (*proof term only*)
+  val prf = Proofterm.proof_of body;
+
+  (*clean output*)
+  Pretty.writeln (Proof_Syntax.pretty_proof \<^context> prf);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
+  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
+
+  (*all theorems used in the graph of nested proofs*)
+  val all_thms =
+    Proofterm.fold_body_thms
+      (fn {name, ...} => insert (op =) name) [body] [];
+\<close>
+
+ML\<open>
+val thy = \<^theory>
+val prf =
+    Proof_Syntax.read_proof thy true false
+      "impI \<cdot> _ \<cdot> _ \<bullet> \
+      \   (\<^bold>\<lambda>H: _. \
+      \     conjE \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> H \<bullet> \
+      \       (\<^bold>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
+\<close>
+
+ML\<open>
+val thy = \<^theory>
+val prf =
+    Proof_Syntax.read_proof thy true false
+      "\<^bold>\<lambda>(H: A \<and> B). conjE \<cdot> A \<cdot> B \<cdot> A \<and> B \<bullet> H";
+(*  val thm =
+    Proofterm.reconstruct_proof thy \<^prop>\<open>A \<Longrightarrow> B \<Longrightarrow> B \<and> A\<close> prf
+    |> Proof_Checker.thm_of_proof thy
+    |> Drule.export_without_context;
+val pretty =  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);*)
+\<close>
+ML\<open>
+val thy = \<^theory>
+val prf =
+    Proof_Syntax.read_proof thy true false
+      "\<^bold>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H";
+  val thm =
+    Proofterm.reconstruct_proof thy \<^prop>\<open>A \<Longrightarrow> B \<Longrightarrow> B \<and> A\<close> prf
+    |> Proof_Checker.thm_of_proof thy
+    |> Drule.export_without_context;
+val pretty =  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
+\<close>
+ 
+end

Isabelle_DOF-Proofs/Very_Deep_DOF.thy

@@ -0,0 +1,20 @@
+theory Very_Deep_DOF
+  imports "Isabelle_DOF-Proofs.Very_Deep_Interpretation"
+
+begin
+
+(* tests *)
+term "@{typ  ''int => int''}"  
+term "@{term ''Bound 0''}"  
+term "@{thm  ''refl''}"  
+term "@{docitem  ''<doc_ref>''}"
+ML\<open>   @{term "@{docitem  ''<doc_ref>''}"}\<close>
+
+term "@{typ  \<open>int \<Rightarrow> int\<close>}"  
+term "@{term \<open>\<forall>x. P x \<longrightarrow> Q\<close>}"  
+term "@{thm  \<open>refl\<close>}"  
+term "@{docitem  \<open>doc_ref\<close>}"
+ML\<open>   @{term "@{docitem  \<open>doc_ref\<close>}"}\<close>
+(**)
+
+end

Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy

@@ -0,0 +1,331 @@
+theory Very_Deep_Interpretation
+  imports "Isabelle_DOF.Isa_COL"
+          Metalogic_ProofChecker.ProofTerm
+
+begin
+
+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 "Isabelle_DOF_typ" ("@{typ _}")
+no_notation "Isabelle_DOF_term" ("@{term _}")
+no_notation "Isabelle_DOF_thm" ("@{thm _}")
+no_notation "Isabelle_DOF_file" ("@{file _}")
+no_notation "Isabelle_DOF_thy" ("@{thy _}")
+no_notation "Isabelle_DOF_docitem" ("@{docitem _}")
+no_notation "Isabelle_DOF_docitem_attr" ("@{docitemattr (_) :: (_)}")
+no_notation "Isabelle_DOF_trace_attribute" ("@{trace-attribute _}")
+
+consts Isabelle_DOF_typ :: "string \<Rightarrow> typ" ("@{typ _}")
+consts Isabelle_DOF_term :: "string \<Rightarrow> term" ("@{term _}")
+consts Isabelle_DOF_term_repr    :: "string \<Rightarrow> term"              ("@{termrepr _}")
+datatype "thm" = Isabelle_DOF_thm string ("@{thm _}") | Thm_content ("proof":proofterm)
+datatype "thms_of" = Isabelle_DOF_thms_of string ("@{thms-of _}")
+datatype "file" = Isabelle_DOF_file string  ("@{file _}")
+datatype "thy" = Isabelle_DOF_thy string  ("@{thy _}")
+consts Isabelle_DOF_docitem      :: "string \<Rightarrow> 'a"                ("@{docitem _}")
+datatype "docitem_attr" = Isabelle_DOF_docitem_attr string  string ("@{docitemattr (_) :: (_)}")
+consts Isabelle_DOF_trace_attribute :: "string \<Rightarrow> (string * string) list" ("@{trace-attribute _}")
+
+subsection\<open> Semantics \<close>
+
+ML\<open>
+structure ISA_core = 
+struct
+
+fun check_path check_file ctxt dir (name, pos) =
+  let
+    val _ = Context_Position.report ctxt pos (Markup.language_path true); (* TODO: pos should be 
+                                                                                   "lifted" to 
+                                                                                   type source *)
+
+    val path = Path.append dir (Path.explode name) handle ERROR msg => ISA_core.err msg pos;
+    val _ = Path.expand path handle ERROR msg => ISA_core.err msg pos;
+    val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
+    val _ =
+      (case check_file of
+        NONE => path
+      | SOME check => (check path handle ERROR msg => ISA_core.err msg pos));
+  in path end;
+
+
+fun ML_isa_antiq check_file thy (name, _, pos) =
+  let val path = check_path check_file (Proof_Context.init_global thy) Path.current (name, pos);
+  in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
+
+
+fun ML_isa_check_generic check thy (term, pos) =
+  let val name = (HOLogic.dest_string term
+                  handle TERM(_,[t]) => error ("wrong term format: must be string constant: " 
+                                               ^ Syntax.string_of_term_global thy t ))
+      val _ = check thy (name,pos)
+  in  SOME term end;  
+
+fun check_identity _ (term, _, _) _ = SOME term
+
+fun ML_isa_check_typ thy (term, _, pos) _ =
+  let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy)
+                                in (Syntax.check_typ ctxt o Syntax.parse_typ ctxt) name end
+  in  ML_isa_check_generic check thy (term, pos) end
+
+
+fun ML_isa_check_term thy (term, _, pos) _ =
+  let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy)
+                                in (Syntax.check_term ctxt o Syntax.parse_term ctxt) name end 
+  in  ML_isa_check_generic check thy (term, pos) end
+
+
+fun ML_isa_check_thm thy (term, _, pos) _ =
+  (* this works for long-names only *)
+  let fun check thy (name, _) = case Proof_Context.lookup_fact (Proof_Context.init_global thy) name of
+                                  NONE => ISA_core.err ("No Theorem:" ^name) pos
+                                | SOME X => X
+  in   ML_isa_check_generic check thy (term, pos) end
+
+
+fun ML_isa_check_file thy (term, _, pos) _ =
+  let fun check thy (name, pos) = check_path (SOME File.check_file) 
+                                             (Proof_Context.init_global thy) 
+                                             (Path.current) 
+                                             (name, pos);
+  in  ML_isa_check_generic check thy (term, pos) end;
+
+fun ML_isa_id thy (term,pos) = SOME term
+
+
+fun ML_isa_check_docitem thy (term, req_ty, pos) _ =
+  let fun check thy (name, _) s =
+            let val DOF_core.Instance {cid,...} =
+                                              DOF_core.get_instance_global name thy
+                val ns = DOF_core.get_instances (Proof_Context.init_global thy)
+                               |> Name_Space.space_of_table 
+                val {pos=pos', ...} = Name_Space.the_entry ns name
+                val ctxt = (Proof_Context.init_global thy)
+                val req_class = case req_ty of 
+                                    \<^Type>\<open>fun _ T\<close> => DOF_core.typ_to_cid T
+                                  | _ => error("can not infer type for: "^ name)
+            in if cid <> DOF_core.default_cid 
+                  andalso not(DOF_core.is_subclass ctxt cid req_class)
+               then error("reference ontologically inconsistent: "
+                          ^cid^" vs. "^req_class^ Position.here pos')
+               else ()
+            end
+  in  ML_isa_check_generic check thy (term, pos) end
+
+
+fun ML_isa_check_trace_attribute thy (term, _, pos) s =
+  let
+    val oid = (HOLogic.dest_string term
+                  handle TERM(_,[t]) => error ("wrong term format: must be string constant: " 
+                                               ^ Syntax.string_of_term_global thy t ))
+    val _ = DOF_core.get_instance_global oid thy
+  in SOME term end
+
+fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ =
+  case term_option of
+      NONE => error("Wrong term option. You must use a defined term")
+    | SOME term => Const (isa_name, ty) $ term
+
+fun reify_typ (Type (s, typ_list)) =
+      \<^Const>\<open>Ty\<close> $ HOLogic.mk_literal s $ HOLogic.mk_list \<^Type>\<open>typ\<close> (map reify_typ typ_list)
+  | reify_typ (TFree (name, sort)) =
+      \<^Const>\<open>Tv\<close> $(\<^Const>\<open>Free\<close> $ HOLogic.mk_literal name)
+      $ (HOLogic.mk_set \<^typ>\<open>class\<close> (map HOLogic.mk_literal sort))
+  | reify_typ (TVar (indexname, sort)) =
+      let val (name, index_value) = indexname
+      in  \<^Const>\<open>Tv\<close>
+          $ (\<^Const>\<open>Var\<close>
+             $ HOLogic.mk_prod (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\<open>int\<close> index_value))
+          $ (HOLogic.mk_set \<^typ>\<open>class\<close> (map HOLogic.mk_literal sort)) end
+
+fun ML_isa_elaborate_typ (thy:theory) _ _ term_option _ =
+  case term_option of
+      NONE => error("Wrong term option. You must use a defined term")
+    | SOME term => let 
+                     val typ_name = HOLogic.dest_string term
+                     val typ = Syntax.read_typ_global thy typ_name
+                   in reify_typ typ end
+
+fun reify_term (Const (name, typ)) =\<^Const>\<open>Ct\<close> $ HOLogic.mk_literal name $ reify_typ typ
+  | reify_term (Free (name, typ)) =
+      \<^Const>\<open>Fv\<close> $ (\<^Const>\<open>Free\<close> $ HOLogic.mk_literal name) $ reify_typ typ
+  | reify_term (Var (indexname, typ)) =
+      let val (name, index_value) = indexname
+      in  \<^Const>\<open>Fv\<close>
+          $ (\<^Const>\<open>Var\<close>
+             $ HOLogic.mk_prod (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\<open>int\<close> index_value))
+          $ reify_typ typ end
+  | reify_term (Bound i) = \<^Const>\<open>Bv\<close> $ HOLogic.mk_nat i
+  | reify_term (Abs (_, typ, term)) = \<^Const>\<open>Abs\<close> $ reify_typ typ $ reify_term term
+  | reify_term (Term.$ (t1, t2)) = \<^Const>\<open>App\<close> $ reify_term t1 $ reify_term t2
+
+fun ML_isa_elaborate_term (thy:theory) _ _ term_option _ =
+  case term_option of
+      NONE => error("Wrong term option. You must use a defined term")
+    | SOME term => let 
+                     val term_name = HOLogic.dest_string term
+                     val term = Syntax.read_term_global thy term_name
+                   in reify_term term end
+
+fun reify_proofterm (PBound i) =\<^Const>\<open>PBound\<close> $ (HOLogic.mk_nat i)
+  | reify_proofterm (Abst (_, typ_option, proof)) =
+      \<^Const>\<open>Abst\<close> $ reify_typ (the typ_option) $ reify_proofterm proof
+  | reify_proofterm (AbsP (_, term_option, proof)) =
+      \<^Const>\<open>AbsP\<close> $ reify_term (the term_option) $ reify_proofterm proof
+  | reify_proofterm (op % (proof, term_option)) =
+      \<^Const>\<open>Appt\<close> $ reify_proofterm proof $ reify_term (the term_option)
+  | reify_proofterm (op %% (proof1, proof2)) =
+      \<^Const>\<open>AppP\<close> $ reify_proofterm proof1 $ reify_proofterm proof2
+  | reify_proofterm (Hyp term) = \<^Const>\<open>Hyp\<close> $ (reify_term term)
+  | reify_proofterm (PAxm (_, term, typ_list_option)) =
+      let 
+          val tvars = rev (Term.add_tvars term [])
+          val meta_tvars = map (fn ((name, index_value), sort) =>
+                HOLogic.mk_prod
+                  (\<^Const>\<open>Var\<close>                    
+                   $ HOLogic.mk_prod
+                      (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\<open>int\<close> index_value)
+                       , HOLogic.mk_set \<^typ>\<open>class\<close> (map HOLogic.mk_literal sort))) tvars
+          val meta_typ_list = 
+            HOLogic.mk_list @{typ "tyinst"} (map2 (fn x => fn y => HOLogic.mk_prod (x, y))
+                                              meta_tvars (map reify_typ (the typ_list_option)))
+      in \<^Const>\<open>PAxm\<close> $ reify_term term $ meta_typ_list end
+  | reify_proofterm (PClass (typ, class)) =
+      \<^Const>\<open>OfClass\<close> $ reify_typ typ $ HOLogic.mk_literal class
+  | reify_proofterm (PThm ({prop = prop, types = types, ...}, _)) =
+      let
+        val tvars = rev (Term.add_tvars prop [])
+        val meta_tvars = map (fn ((name, index_value), sort) =>
+                HOLogic.mk_prod
+                  (\<^Const>\<open>Var\<close>                    
+                  $ HOLogic.mk_prod
+                      (HOLogic.mk_literal name, HOLogic.mk_number \<^Type>\<open>int\<close> index_value)
+                  , HOLogic.mk_set \<^typ>\<open>class\<close> (map HOLogic.mk_literal sort))) tvars
+        val meta_typ_list = 
+            HOLogic.mk_list \<^typ>\<open>tyinst\<close> (map2 (fn x => fn y => HOLogic.mk_prod (x, y))
+                                          meta_tvars (map reify_typ (the types)))
+      in \<^Const>\<open>PAxm\<close> $ reify_term prop $ meta_typ_list end
+
+fun ML_isa_elaborate_thm (thy:theory) _ _ term_option pos =
+  case term_option of
+      NONE => ISA_core.err ("Malformed term annotation") pos
+    | SOME term =>
+        let
+          val thm_name = HOLogic.dest_string term
+          val _ = writeln ("In ML_isa_elaborate_thm thm_name: " ^ \<^make_string> thm_name)
+          val thm = Proof_Context.get_thm (Proof_Context.init_global thy) thm_name
+          val _ = writeln ("In ML_isa_elaborate_thm thm: " ^ \<^make_string> thm)
+          val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
+          val prf = Proofterm.proof_of body;
+          (* Proof_Syntax.standard_proof_of reconstructs the proof and seems to rewrite
+             the option arguments (with a value NONE) of the proof datatype constructors,
+             at least for PAxm, with "SOME (typ/term)",
+             allowing us the use the projection function "the".
+             Maybe the function can deal with
+             all the option types of the proof datatype constructors *)
+          val proof = Proof_Syntax.standard_proof_of
+                                   {full = true, expand_name = Thm.expand_name thm} thm
+          val _ = writeln ("In ML_isa_elaborate_thm proof: " ^ \<^make_string> proof)
+          (* After a small discussion with Simon Roßkopf, It seems preferable to use
+             Thm.reconstruct_proof_of instead of Proof_Syntax.standard_proof_of
+             whose operation is not well known.
+             Thm.reconstruct_proof_of seems sufficient to have a reifiable PAxm
+             in the metalogic. *)
+          val proof' = Thm.reconstruct_proof_of thm 
+        (*in \<^Const>\<open>Thm_content\<close> $ reify_proofterm prf end*)        
+        (*in \<^Const>\<open>Thm_content\<close> $ reify_proofterm proof end*)
+        in \<^Const>\<open>Thm_content\<close> $ reify_proofterm proof end
+
+
+fun ML_isa_elaborate_thms_of (thy:theory) _ _ term_option pos =
+  case term_option of
+      NONE => ISA_core.err ("Malformed term annotation") pos
+    | SOME term =>
+        let
+          val thm_name = HOLogic.dest_string term
+          val thm = Proof_Context.get_thm (Proof_Context.init_global thy) thm_name
+          val body = Proofterm.strip_thm_body (Thm.proof_body_of thm)
+          val all_thms_name = Proofterm.fold_body_thms (fn {name, ...} => insert (op =) name) [body] []
+          (*val all_thms = map (Proof_Context.get_thm (Proof_Context.init_global thy)) all_thms_name*)
+          (*val all_proofs = map (Proof_Syntax.standard_proof_of
+                                   {full = true, expand_name = Thm.expand_name thm}) all_thms*)
+        (*in HOLogic.mk_list \<^Type>\<open>thm\<close> (map (fn proof => \<^Const>\<open>Thm_content\<close> $ reify_proofterm proof) all_proofs) end*)
+        in HOLogic.mk_list \<^typ>\<open>string\<close> (map HOLogic.mk_string all_thms_name) end
+
+fun ML_isa_elaborate_trace_attribute (thy:theory) _ _ term_option pos =
+case term_option of
+    NONE => ISA_core.err ("Malformed term annotation") pos
+  | SOME term => 
+      let
+        val oid = HOLogic.dest_string term
+        val traces = ISA_core.compute_attr_access (Context.Theory thy) "trace" oid NONE pos
+        fun conv (\<^Const>\<open>Pair \<^typ>\<open>doc_class rexp\<close> \<^typ>\<open>string\<close>\<close>
+                    $ (\<^Const>\<open>Atom \<^typ>\<open>doc_class\<close>\<close> $ (\<^Const>\<open>mk\<close> $ s)) $ S) =
+          let val s' =  DOF_core.get_onto_class_name_global (HOLogic.dest_string s) thy 
+          in \<^Const>\<open>Pair \<^typ>\<open>string\<close> \<^typ>\<open>string\<close>\<close> $ HOLogic.mk_string s' $ S end
+        val traces' = map conv (HOLogic.dest_list traces)
+      in HOLogic.mk_list \<^Type>\<open>prod \<^typ>\<open>string\<close> \<^typ>\<open>string\<close>\<close> traces' end
+
+(* utilities *)
+
+fun property_list_dest ctxt X =
+  map (fn \<^Const_>\<open>Isabelle_DOF_term for s\<close> => HOLogic.dest_string s
+         |\<^Const_>\<open>Isabelle_DOF_term_repr for s\<close> => holstring_to_bstring ctxt (HOLogic.dest_string s))
+    (HOLogic.dest_list X)
+
+end; (* struct *)
+
+\<close>
+
+ML\<open>
+val ty1 = ISA_core.reify_typ @{typ "int"}
+val ty2 = ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
+val ty3 = ISA_core.reify_typ @{typ "prop"}
+val ty4 = ISA_core.reify_typ @{typ "'a list"}
+\<close>
+
+ML\<open>
+val t1 = ISA_core.reify_term @{term "1::int"}
+val t2 = ISA_core.reify_term @{term "\<lambda>x. x = 1"}
+val t3 = ISA_core.reify_term @{term "[2, 3::int]"}
+\<close>
+
+subsection\<open> Isar - Setup\<close>
+(* Isa_transformers declaration for Isabelle_DOF term anti-quotations (typ, term, thm, etc.).
+   They must be declared in the same theory file as the one of the declaration
+   of Isabelle_DOF term anti-quotations !!! *)
+setup\<open>
+[(\<^type_name>\<open>thm\<close>, ISA_core.ML_isa_check_thm, ISA_core.ML_isa_elaborate_thm)
+ , (\<^type_name>\<open>thms_of\<close>, ISA_core.ML_isa_check_thm, ISA_core.ML_isa_elaborate_thms_of)
+ , (\<^type_name>\<open>file\<close>, ISA_core.ML_isa_check_file, ISA_core.ML_isa_elaborate_generic)]
+|> fold (fn (n, check, elaborate) => fn thy =>
+let val ns = Sign.tsig_of thy |> Type.type_space
+    val name = n
+    val {pos, ...} = Name_Space.the_entry ns name
+    val bname = Long_Name.base_name name
+    val binding = Binding.make (bname, pos)
+                   |> Binding.prefix_name DOF_core.ISA_prefix
+                   |> Binding.prefix false bname
+in  DOF_core.add_isa_transformer binding ((check, elaborate) |> DOF_core.make_isa_transformer) thy
+end)
+#>
+([(\<^const_name>\<open>Isabelle_DOF_typ\<close>, ISA_core.ML_isa_check_typ, ISA_core.ML_isa_elaborate_typ)
+  ,(\<^const_name>\<open>Isabelle_DOF_term\<close>, ISA_core.ML_isa_check_term, ISA_core.ML_isa_elaborate_term)
+  ,(\<^const_name>\<open>Isabelle_DOF_term_repr\<close>, ISA_core.check_identity, ISA_core.ML_isa_elaborate_generic)
+  ,(\<^const_name>\<open>Isabelle_DOF_docitem\<close>,
+      ISA_core.ML_isa_check_docitem, ISA_core.ML_isa_elaborate_generic)
+  ,(\<^const_name>\<open>Isabelle_DOF_trace_attribute\<close>,
+      ISA_core.ML_isa_check_trace_attribute, ISA_core.ML_isa_elaborate_trace_attribute)]
+|> fold (fn (n, check, elaborate) => fn thy =>
+let val ns = Sign.consts_of thy |> Consts.space_of
+    val name = n
+    val {pos, ...} = Name_Space.the_entry ns name
+    val bname =  Long_Name.base_name name
+    val binding = Binding.make (bname, pos)
+in  DOF_core.add_isa_transformer binding ((check, elaborate) |> DOF_core.make_isa_transformer) thy
+end))
+\<close>
+end

Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy

@@ -14,8 +14,9 @@
 theory 
   AssnsLemmaThmEtc
 imports 
-  "Isabelle_DOF.Conceptual"  
+  "Isabelle_DOF-Ontologies.Conceptual"  
   "Isabelle_DOF.scholarly_paper"
+  "Isabelle_DOF-Unit-Tests_document"
 begin
 
 section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>

Isabelle_DOF-Unit-Tests/Attributes.thy

@@ -13,11 +13,12 @@
 
 theory 
   Attributes
-imports 
-  "Isabelle_DOF.Conceptual"
+  imports 
+  "Isabelle_DOF-Unit-Tests_document"
+  "Isabelle_DOF-Ontologies.Conceptual"
 begin
-
-section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
+ML\<open>@{assert} (1 = 1)\<close>
+section\<open>Elementar Creation of Doc-items and Access of their Attibutes\<close>
 
 text\<open>Current status:\<close>
 print_doc_classes
@@ -25,25 +26,30 @@ print_doc_items
 
 (* this corresponds to low-level accesses : *)
 ML\<open>  
-val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab,...} 
-    = DOF_core.get_data @{context};
-Symtab.dest docitem_tab;
-Symtab.dest docclass_tab;
+val docitem_tab = DOF_core.get_instances \<^context>
+val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>
+val docclass_tab = DOF_core.get_onto_classes @{context};
 \<close>
 ML\<open>
-#value(the(the(Symtab.lookup docitem_tab "aaa")))
+map fst (Name_Space.dest_table docitem_tab);
+Name_Space.dest_table docclass_tab;
 
 \<close>
 
+ML\<open>
+val (oid, DOF_core.Instance {value, ...}) =
+    Name_Space.check (Context.Proof \<^context>) (DOF_core.get_instances \<^context>) ("aaa", Position.none)
+\<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 [simp]"M.trace(M.make undefined [] ())"
+value "M.ok(M.make undefined_AAA [] ())"
+value "M.trace(M.make undefined_AAA [] ())"
+value "M.tag_attribute(M.make undefined_AAA [] ())"
 
 
-value "ok(M.make 0 [] ())"
+value "M.ok(M.make 0 [] ())"
 (*
 value "ok(M.make undefined [] ())"
 value "ok(M.make 0 [] undefined)"
@@ -168,14 +174,17 @@ update_instance*[omega::E, y+="[''en'']"]
 ML\<open> val s =  map HOLogic.dest_string (HOLogic.dest_list @{docitem_attribute y::omega}); \<close>
 
 subsection\<open> Example text antiquotation:\<close>
-text\<open> @{docitem_attribute omega::y}  \<close>
+text\<open> @{docitem_attribute y::omega}  \<close>
 
 
 section\<open>Simulation of a Monitor\<close>
 
+declare[[free_class_in_monitor_checking]]
+
 open_monitor*[figs1::figure_group, 
               caption="''Sample ''"]  
-
+ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
+text*[testFreeA::A]\<open>\<close>
 figure*[fig_A::figure, spawn_columns=False,
         relative_width="90",
         src="''figures/A.png''"]
@@ -185,14 +194,66 @@ figure*[fig_B::figure,
         spawn_columns=False,relative_width="90",
         src="''figures/B.png''"]
        \<open> The B train \ldots \<close>  
+open_monitor*[figs2::figure_group, 
+              caption="''Sample ''"]
+ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
+figure*[fig_C::figure, spawn_columns=False,
+        relative_width="90",
+        src="''figures/A.png''"]
+       \<open> The C train \ldots \<close>
+open_monitor*[figs3::figure_group, 
+              caption="''Sample ''"]
+ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
+
+figure*[fig_D::figure, 
+        spawn_columns=False,relative_width="90",
+        src="''figures/B.png''"]
+       \<open> The D train \ldots \<close>
+close_monitor*[figs3]
+
+open_monitor*[figs4::figure_group, 
+              caption="''Sample ''"]
+ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
+
+text*[testRejected1::figure_group, caption="''document/figures/A.png''"]
+       \<open> The A train \ldots \<close>
+
+figure*[fig_E::figure,
+        spawn_columns=False,relative_width="90",
+        src="''figures/B.png''"]
+       \<open> The E train \ldots \<close>
+close_monitor*[figs4]
+close_monitor*[figs2]
+text*[testRejected2::figure_group, caption="''document/figures/A.png''"]
+       \<open> The A train \ldots \<close>
 
 close_monitor*[figs1]  
 
+declare[[free_class_in_monitor_checking = false]]
+
 text\<open>Resulting trace of figs1 as ML antiquotation: \<close>
 ML  \<open>@{trace_attribute figs1}\<close>
 text\<open>Resulting trace of figs as text antiquotation:\<close>
 text\<open>@{trace_attribute figs1}\<close>
 
+text\<open>Test trace\_attribute term antiquotation:\<close>
+
+term*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
+value*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
+term*\<open>map fst @{trace-attribute \<open>aaa\<close>}\<close>
+value*\<open>map fst @{trace-attribute \<open>aaa\<close>}\<close>
+term*\<open>map fst @{trace-attribute \<open>test_monitor_M\<close>}\<close>
+value*\<open>map fst @{trace-attribute \<open>test_monitor_M\<close>}\<close>
+
+definition example_expression where "example_expression \<equiv> \<lbrace>\<lfloor>''Conceptual.A''\<rfloor> || \<lfloor>''Conceptual.F''\<rfloor>\<rbrace>\<^sup>*"
+value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \<open>aaa\<close>}) \<close>
+
+definition word_test  :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> bool" (infix "is-in" 60)
+  where " w is-in rexp \<equiv>  DA.accepts (na2da (rexp2na rexp)) (w)"
+
+value* \<open> (map fst @{trace-attribute \<open>aaa\<close>}) is-in example_expression \<close>
+
+
 (*<*)
 text\<open>Final Status:\<close>
 print_doc_items

Isabelle_DOF-Unit-Tests/Cenelec_Test.thy

@@ -0,0 +1,70 @@
+theory 
+  Cenelec_Test
+imports 
+  "Isabelle_DOF-Unit-Tests_document"
+  "Isabelle_DOF-Ontologies.CENELEC_50128"
+begin
+
+declare[[strict_monitor_checking = true]]
+declare[[invariants_checking = true]]
+declare[[invariants_checking_with_tactics = true]]
+
+print_doc_items
+print_doc_classes
+
+open_monitor*[SIL0Test::monitor_SIL0]
+
+text*[sqap_instance::SQAP, sil="SIL0", written_by="Some RQM", fst_check="Some VER", snd_check="Some VAL"]\<open>\<close>
+text*[sqavr_instance::SQAVR, sil= "SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[scmp_instance::SCMP, sil="SIL0", written_by="Some CM", fst_check="Some VER", snd_check="Some VAL"]\<open>\<close>
+text*[svp_instance::SVP, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[svap_instance::SVAP, sil="SIL0", written_by="Some VAL", fst_check="Some VER", snd_check="None"]\<open>\<close>
+text*[swrs_instance::SWRS, sil="SIL0", written_by="Some RQM", fst_check="Some VER", snd_check="Some VAL"]\<open>\<close>
+text*[oswts_instance::OSWTS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swrvr_instance::SWRVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swas_instance::SWAS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swds_instance::SWDS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swis_instance::SWIS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swits_instance::SWITS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swhits_instance::SWHITS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swadvr_instance::SWADVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swcds_instance::SWCDS, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swcts_instance::SWCTS, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swcdvr_instance::SWCDVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swscd_instance::SWSCD, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swctr_instance::SWCTR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swscvr_instance::SWSCVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[switr_instance::SWITR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swhaitr_instance::SWHAITR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swivr_instance::SWIVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[oswtr_instance::OSWTR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swvalr_instance::SWVALR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[tvalr_instance::TVALR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swvrn_instance::SWVRN, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[ars_instance::ARS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[app_instance::APP, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[ats_instance::ATS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[aad_instance::AAD, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[apvr_instance::APVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[atr_instance::ATR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[socoada_instance::SOCOADA, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[adavr_instance::ADAVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swrdp_instance::SWRDP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swdm_instance::SWDM, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swdrn_instance::SWDRN, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swdr_instance::SWDR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swdvr_instance::SWDVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swmp_instance::SWMP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swcr_instance::SWCR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swmr_instance::SWMR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swmvr_instance::SWMVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swap_instance::SWAP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+text*[swar_instance::SWAR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\<open>\<close>
+
+close_monitor*[SIL0Test]
+
+declare[[strict_monitor_checking = true]]
+declare[[invariants_checking = true]]
+declare[[invariants_checking_with_tactics = true]]
+
+end 

Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy

@@ -15,8 +15,9 @@ chapter\<open>Setting and modifying attributes of doc-items\<close>
 
 theory 
   Concept_Example_Low_Level_Invariant
-imports 
-  "Isabelle_DOF.Conceptual" (* we use the generic "Conceptual" ontology *)
+  imports 
+  "Isabelle_DOF-Unit-Tests_document"
+  "Isabelle_DOF-Ontologies.Conceptual" (* we use the generic "Conceptual" ontology *)
 begin
 
 section\<open>Example: Standard Class Invariant\<close>
@@ -34,24 +35,30 @@ The implementor of an ontology must know what he does ...
 \<close>
 
 text\<open>Setting a sample invariant, which simply produces some side-effect:\<close>
-setup\<open>DOF_core.update_class_invariant "Conceptual.A" (fn oid => 
-                                                       fn {is_monitor = b} =>
-                                                        fn ctxt => 
-                                                           (writeln ("sample echo : "^oid); true))\<close>
+setup\<open>
+fn thy =>
+let val ctxt = Proof_Context.init_global thy
+    val binding = DOF_core.binding_from_onto_class_pos "A" thy
+in DOF_core.add_ml_invariant binding (fn oid =>
+                                         fn {is_monitor = b} =>
+                                            fn ctxt => 
+                                               (writeln ("sample echo : "^oid); true)) thy end
+\<close>
 
 subsection*[b::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
 
 
 text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
-ML\<open>fun check_A_invariant oid {is_monitor:bool} ctxt = 
-      let val term =  AttributeAccess.compute_attr_access ctxt "x" oid @{here} @{here} 
+ML\<open>
+fn thy =>
+let fun check_A_invariant oid {is_monitor:bool} ctxt =
+      let val term =  ISA_core.compute_attr_access ctxt "x" oid NONE @{here} 
           val (@{typ "int"},x_value) = HOLogic.dest_number term
-      in  if x_value > 5 then error("class A invariant violation") else true end
+    in  if x_value > 5 then error("class A invariant violation") else true end
+    val binding = DOF_core.binding_from_onto_class_pos "A" thy
+in DOF_core.add_ml_invariant binding check_A_invariant thy end
 \<close>
 
-setup\<open>DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\<close>
-
-
 
 subsection*[d::A, x = "4"] \<open> Lorem ipsum dolor sit amet, ... \<close>
 
@@ -79,9 +86,14 @@ that instances of class C occur more often as those of class D; note that this i
 to take sub-classing into account:
 \<close>
 
-ML\<open>fun check_M_invariant oid {is_monitor} ctxt = 
-      let val term =  AttributeAccess.compute_attr_access ctxt "trace" oid @{here} @{here} 
-          fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
+ML\<open>
+fn thy =>
+let fun check_M_invariant oid {is_monitor} ctxt =
+      let val term =  ISA_core.compute_attr_access ctxt "trace" oid NONE @{here} 
+          fun conv (\<^Const>\<open>Pair \<^typ>\<open>doc_class rexp\<close> \<^typ>\<open>string\<close>\<close>
+                      $ (\<^Const>\<open>Atom \<^typ>\<open>doc_class\<close>\<close> $ (\<^Const>\<open>mk\<close> $ s)) $ S) =
+            let val s' =  DOF_core.get_onto_class_name_global' (HOLogic.dest_string s) thy
+            in (s', HOLogic.dest_string S) end
           val string_pair_list = map conv (HOLogic.dest_list term) 
           val cid_list = map fst string_pair_list
           val ctxt' = Proof_Context.init_global(Context.theory_of ctxt)
@@ -90,10 +102,10 @@ ML\<open>fun check_M_invariant oid {is_monitor} ctxt =
           val n = length (filter is_C cid_list)
           val m = length (filter is_D cid_list)
       in  if m > n then error("class M invariant violation") else true end
+    val binding = DOF_core.binding_from_onto_class_pos "M" thy
+in DOF_core.add_ml_invariant binding check_M_invariant thy end
 \<close>
 
-setup\<open>DOF_core.update_class_invariant "Conceptual.M" check_M_invariant\<close>
-
 
 section\<open>Example: Monitor Class Invariant\<close>
 
@@ -107,16 +119,22 @@ text*[d1::E, a1 = "X3"]          \<open> ... phasellus amet id massa nunc, pede
     
 text*[c2:: C, x = "''delta''"]   \<open> ... in ut tortor eleifend augue pretium consectetuer...  \<close>
 
-subsection*[f::E]                \<open> Lectus accumsan velit ultrices, ... }\<close>
+subsection*[f::E]                \<open> Lectus accumsan velit ultrices, ... \<close>
 
 (*
-section*[f2::E]                  \<open> Lectus accumsan velit ultrices, ... }\<close>
+section*[f2::E]                  \<open> Lectus accumsan velit ultrices, ... \<close>
 *)
 
-ML\<open>val term = AttributeAccess.compute_attr_access 
-                  (Context.Proof @{context}) "trace" "struct" @{here} @{here} ;
+ML\<open>val ctxt = @{context}
+   val term = ISA_core.compute_attr_access 
+                  (Context.Proof ctxt) "trace" "struct" NONE @{here} ;
    fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
-   val string_pair_list = map conv (HOLogic.dest_list term)
+   fun conv' (\<^Const>\<open>Pair \<^typ>\<open>doc_class rexp\<close> \<^typ>\<open>string\<close>\<close>
+                      $ (\<^Const>\<open>Atom \<^typ>\<open>doc_class\<close>\<close> $ (\<^Const>\<open>mk\<close> $ s)) $ S) =
+     let val s' =  DOF_core.get_onto_class_name_global' (HOLogic.dest_string s)
+                                                                    (Proof_Context.theory_of ctxt)
+     in (s', HOLogic.dest_string S) end
+   val string_pair_list = map conv' (HOLogic.dest_list term)
   \<close>
 
 

Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy

@@ -0,0 +1,142 @@
+(*************************************************************************
+ * Copyright (C) 
+ *               2019      The University of Exeter 
+ *               2018-2019 The University of Paris-Saclay
+ *               2018      The University of Sheffield
+ *
+ * License:
+ *   This program can be redistributed and/or modified under the terms
+ *   of the 2-clause BSD-style license.
+ *
+ *   SPDX-License-Identifier: BSD-2-Clause
+ *************************************************************************)
+
+chapter\<open>Setting and modifying attributes of doc-items\<close>
+
+theory 
+  Concept_OntoReferencing
+  imports 
+  "Isabelle_DOF-Unit-Tests_document"
+  "Isabelle_DOF-Ontologies.Conceptual" 
+  "TestKit"
+begin
+
+section\<open>Setting up a monitor.\<close>
+text\<open>\<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close> provides a monitor \<^typ>\<open>M\<close>  enforcing a 
+     particular document structure. Here, we say: From now on, this structural rules are 
+     respected wrt. all \<^theory_text>\<open>doc_classes M\<close> is enabled for.\<close>
+
+open_monitor*[struct::M]  
+
+section\<open>Defining Text Elements and Referring to them... \<close>
+
+text\<open> This uses elements of two ontologies, notably 
+      \<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close> and \<^theory>\<open>Isabelle_DOF.Isa_COL\<close>.\<close>
+
+(*<*)
+title*[abbb::title, short_title="Some\<open>ooups.\<close>"]\<open>Lorem ipsum dolor sit amet ...\<close>
+subtitle*[abbbb::subtitle, abbrev = "Some\<open>ooups-oups.\<close>"]\<open>Lorem ipsum dolor sit amet ...\<close>
+chapter*[abbbbbb::A, x = "3"]   \<open> Lorem ipsum dolor sit amet ... \<close>
+section*[a::A, x = "3"]         \<open> Lorem ipsum dolor sit amet, ... \<close>
+subsection*[ab::A, x = "3"]     \<open> Lorem ipsum dolor sit amet, ... 
+                                  As mentioned in the @{title \<open>abbb\<close>}... \<close> \<comment> \<open>old-style and ...\<close>
+subsubsection*[abb::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... 
+                                  As mentioned in the \<^title>\<open>abbb\<close>\<close>    \<comment> \<open>new-style references to
+                                                                          ontological instances 
+                                                                          assigned to text 
+                                                                          elements ...\<close>
+(*>*)
+
+
+
+text\<open>Meta-Objects are typed, and references have to respect this : \<close>
+(*<*)
+text-assert-error[ac]\<open> \<^title>\<open>a\<close> \<close>    \<open>reference ontologically inconsistent\<close>
+text-assert-error[ad]\<open> \<^title>\<open>abbbb\<close> \<close>\<open>reference ontologically inconsistent\<close> 
+                       \<comment> \<open>erroneous reference: please consider class hierarchy!\<close>
+(*>*)
+
+text\<open>References to Meta-Objects can be forward-declared:\<close>
+
+text-assert-error[ae1]\<open>@{C \<open>c1\<close>} \<close>\<open>Undefined instance:\<close>
+
+declare_reference*[c1::C] \<comment> \<open>forward declaration\<close>
+
+text\<open>@{C \<open>c1\<close>} \<close>   \<comment> \<open>THIS IS A  BUG !!! OVERLY SIMPLISTIC BEHAVIOUR. THIS SHOULD FAIL! \<close>
+
+text\<open>@{C (unchecked) \<open>c1\<close>} \<close>   \<comment> \<open>THIS SHOULD BE THE CORRECT BEHAVIOUR! \<close>
+
+
+text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ...  \<close>
+
+text-assert-error[c1::C, x = "''gamma''"] 
+                             \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ...  \<close>
+                             \<open>Duplicate instance declaration\<close>
+
+text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus, 
+                         ... @{C "c1"} or @{C \<open>c1\<close>} or \<^C>\<open>c1\<close>
+                             similar to @{thm "refl"} and \<^thm>"refl"\<close>  \<comment> \<open>ontological and built-in
+                                                                          references\<close>
+
+text\<open>Not only text-elements are "ontology-aware", proofs and code can this be too !\<close>
+
+ML*[ddddd2::E]\<open>fun fac x = if x = 0 then 1 else x * (fac(x-1))\<close> (* TODO : BUG *)
+(* TODO BUG : lemma*[ddddd3::E] asd: "True" *)
+
+text\<open>Ontological information ("class instances") is mutable: \<close>
+
+update_instance*[d::D, a1 := X2]
+
+text\<open> ... in ut tortor ... @{docitem \<open>a\<close>} ... @{A \<open>a\<close>} ... \<close> \<comment> \<open>untyped or typed referencing \<close>
+
+(* THIS IS A BUG \<And>\<And>! *)
+text-assert-error[ae::text_element]\<open>the function @{E "ddddd2"} \<close>\<open>referred text-element is macro!\<close>
+
+text*[c2::C, x = "\<open>delta\<close>"]  \<open> ... in ut tortor eleifend augue pretium consectetuer.  \<close>
+
+text\<open>Note that both the notations @{term "''beta''"} and @{term "\<open>beta\<close>"} are possible;
+the former is a more ancient format only supporting pure ascii, while the latter also supports
+fancy unicode such as: @{term "\<open>\<beta>\<^sub>i''\<close>"} \<close>
+
+text*[f::F] \<open> Lectus accumsan velit ultrices, ... \<close>
+  
+theorem some_proof : "True" by simp
+
+text\<open>This is an example where we add a theorem into a kind of "result-list" of the doc-item f.\<close>
+update_instance*[f::F,r:="[@{thm ''Concept_OntoReferencing.some_proof''}]"]
+
+text\<open> ..., mauris amet, id elit aliquam aptent id,  ... @{docitem \<open>a\<close>} \<close>
+
+text\<open>Here we add and maintain a link that is actually modeled as m-to-n relation ...\<close>
+update_instance*[f::F,b:="{(@{docitem  \<open>a\<close>}::A,@{docitem  \<open>c1\<close>}::C), 
+                           (@{docitem  \<open>a\<close>},   @{docitem  \<open>c2\<close>})}"] 
+
+close_monitor*[struct]
+
+text\<open>And the trace of the monitor is:\<close>
+ML\<open>val trace = @{trace_attribute struct}\<close>
+ML\<open>@{assert} (trace = [("Conceptual.A", "abbbbbb"), ("Conceptual.A", "a"), ("Conceptual.A", "ab"), 
+                       ("Conceptual.A", "abb"),("Conceptual.C", "c1"),("Conceptual.C", "c1"), ("Conceptual.D", "d"), 
+                       ("Conceptual.E", "ddddd2"), ("Conceptual.C", "c2"), ("Conceptual.F", "f")]) \<close>
+(* SHOULD BE:
+ML\<open>@{assert} (trace = [("Conceptual.A", "abbbbbb"), ("Conceptual.A", "a"), ("Conceptual.A", "ab"), 
+                       ("Conceptual.A", "abb"),("Conceptual.C", "c1"), ("Conceptual.D", "d"), 
+                       ("Conceptual.E", "ddddd2"), ("Conceptual.C", "c2"), ("Conceptual.F", "f")]) \<close>
+
+   FAILURE DUE TO DUPLICATE DEFINITION BUG 
+*)
+
+text\<open>Note that the monitor \<^typ>\<open>M\<close> of the ontology \<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close> does
+     not observe the common entities of \<^theory>\<open>Isabelle_DOF.Isa_COL\<close>, but just those defined in the 
+     accept- clause of \<^typ>\<open>M\<close>.\<close>
+
+text\<open>One final check of the status DOF core: observe that no new classes have been defined,
+     just a couple of new document elements have been introduced.\<close>
+
+print_doc_classes
+print_doc_items
+
+
+
+end 
+  

Isabelle_DOF-Unit-Tests/Evaluation.thy

@@ -5,20 +5,23 @@ text\<open>Term Annotation Antiquotations (TA) can be evaluated with the help of
 theory 
   Evaluation
 imports 
-  "Isabelle_DOF-tests.TermAntiquotations"
-  "Isabelle_DOF-tests.High_Level_Syntax_Invariants"
+  "Isabelle_DOF-Unit-Tests.TermAntiquotations"
+  "Isabelle_DOF-Unit-Tests.High_Level_Syntax_Invariants"
+
 begin
 
+(*
 section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close>
-ML*[the_function::B,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1);
-                               val t = @{const_name "List.Nil"}\<close>
+
+ML*[thefunction::B,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1);
+                               val t = \<^value_>\<open>x @{B \<open>thefunction\<close>}\<close>\<close>
 ML\<open>fac 5; t\<close> \<comment> \<open>this is a test that ML* is actually evaluated and the 
                  resulting toplevel state is preserved.\<close>
-ML*\<open>3+4\<close>     \<comment> \<open>meta-args are optional\<close> 
+text-macro*[the::C]\<open> @{B [display] "thefunction"} \<close>
 
-text-macro*[the::C]\<open> @{B [display] "the_function"} \<close>
+text\<open>... and here we reference @{B [display] \<open>thefunction\<close>}.\<close>
 
-text\<open>... and here we reference @{B [display] \<open>the_function\<close>}.\<close>
+*)
 
 section\<open>\<^theory_text>\<open>value*\<close>-Annotated evaluation-commands\<close>
 
@@ -36,13 +39,13 @@ Some built-ins remain as unspecified constants:
 \<^item> the termrepr TA is left as unspecified constant for now.
    A major refactoring of code should be done to enable
   referential equivalence for termrepr, by changing the dependency
-  between the Isa_DOF theory and the Assert theory.
-  The assert_cmd function in Assert should use the value* command
+  between the Isa-DOF theory and the Assert theory.
+  The assert-cmd function in Assert should use the value* command
   functions, which make the elaboration of the term
   referenced by the TA before passing it to the evaluator
 
 We also have the possibility to make some requests on classes instances, i.e. on docitems
-by specifying the doc_class.
+by specifying the doc class.
 The TA denotes the HOL list of the values of the instances.
 The value of an instance is the record of every attributes of the instance.
 This way, we can use the usual functions on lists to make our request.
@@ -78,9 +81,9 @@ term*\<open>@{A \<open>xcv1\<close>}\<close>
 
 text\<open>The instance class @{docitem \<open>xcv1\<close>} is not an instance of the class @{doc_class B}:
 \<close>
-(* Error:
-term*\<open>@{B \<open>xcv1\<close>}\<close>*)
-
+(* Error: 
+term*\<open>@{B \<open>xcv1\<close>}\<close>
+*)
 text\<open>We can evaluate the instance class. The current implementation returns
 the value of the instance, i.e. a collection of every attribute of the instance: 
 \<close>
@@ -102,7 +105,7 @@ text\<open>Some terms can be validated, i.e. the term will be checked,
 and the existence of every object referenced by a TA will be checked,
 and can be evaluated by using referential equivalence.
 The existence of the instance @{docitem \<open>xcv4\<close>} can be validated,
-and the fact that it is an instance of the class @{doc_class F} } will be checked:\<close>
+and the fact that it is an instance of the class @{doc_class F} will be checked:\<close>
 term*\<open>@{F \<open>xcv4\<close>}\<close>
 
 text\<open>We can also evaluate the instance @{docitem \<open>xcv4\<close>}.
@@ -113,12 +116,13 @@ used in the \<open>b\<close> attribute will be checked, and the type of these cl
 \<close>
 value* \<open>@{F \<open>xcv4\<close>}\<close>
 
+(*
 text\<open>If we want the classes to be checked,
 we can use the TA which will also check the type of the instances.
 The instance @{A \<open>xcv3\<close>} is of type @{typ "A"} and the instance @{C \<open>xcv2\<close>} is of type @{typ "C"}:
 \<close>
 update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{C ''xcv2''})}"]
-
+*)
 text\<open>Using a TA in terms is possible, and the term is evaluated:\<close>
 value*\<open>[@{thm \<open>HOL.refl\<close>}, @{thm \<open>HOL.refl\<close>}]\<close>
 value*\<open>@{thm ''HOL.refl''} = @{thm (''HOL.refl'')}\<close>
@@ -154,7 +158,7 @@ value*\<open>@{A-instances}\<close>
 text\<open>Warning: If you make a request on attributes that are undefined in some instances,
 you will get a result which includes these unresolved cases.
 In the following example, we request the instances of the @{doc_class A}.
-But we have defined an instance @{docitem \<open>test\<close>} in theory @{theory Isabelle_DOF.Conceptual}
+But we have defined an instance @{docitem \<open>test\<close>} in theory @{theory "Isabelle_DOF-Ontologies.Conceptual"}
 whose our theory inherits from, and this docitem instance does not initialize its attribute \<^emph>\<open>x\<close>.
 So in the request result we get an unresolved case because the evaluator can not get
 the value of the \<^emph>\<open>x\<close> attribute of the instance @{docitem \<open>test\<close>}:\<close>
@@ -183,14 +187,14 @@ text\<open>The \<^emph>\<open>assert*\<close>-command allows for logical stateme
 It uses the same implementation as the \<^emph>\<open>value*\<close>-command and has the same limitations.
 \<close>
 
-text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-tests.High_Level_Syntax_Invariants\<close>
+text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-Unit-Tests.High_Level_Syntax_Invariants\<close>
 we can check logical statements:\<close>
-
+(*
 term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
 assert*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
 assert*\<open>\<not>(authored_by @{introduction \<open>introduction2\<close>}
           = authored_by @{introduction \<open>introduction4\<close>})\<close>
-
+*)
 text\<open>Assertions must be boolean expressions, so the following assertion triggers an error:\<close>
 (* Error:
 assert*\<open>@{introduction \<open>introduction2\<close>}\<close>*)
@@ -198,7 +202,7 @@ assert*\<open>@{introduction \<open>introduction2\<close>}\<close>*)
 text\<open>Assertions must be true, hence the error:\<close>
 (* Error:
 assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*)
-
+(*
 term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
 assert*[assertionA::A]\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
 
@@ -206,5 +210,11 @@ text-macro*[assertionAA::A]\<open>@{A [display] "assertionA"}\<close>
 text\<open>... and here we reference @{A [display] \<open>assertionA\<close>}.\<close>
 
 assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
-
+*)
+text\<open>The optional evaluator of \<open>value*\<close> and \<open>assert*\<close> must be specified after the meta arguments:\<close>
+value* [optional_test_A::A, x=6] [nbe] \<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A-instances}\<close>
+(*
+assert* [resultProof3::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"] [nbe]
+        \<open>evidence @{result \<open>resultProof3\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
+*)
 end

Isabelle_DOF-Unit-Tests/High_Level_Syntax_Invariants.thy

@@ -2,6 +2,8 @@ chapter\<open>High level syntax Invariants\<close>
 
 theory High_Level_Syntax_Invariants
   imports "Isabelle_DOF.Isa_DOF"
+  "Isabelle_DOF-Unit-Tests_document"
+
 begin
 
 text\<open>
@@ -12,7 +14,7 @@ text\<open>
   theory attribute must be set:\<close>
 
 
-declare[[invariants_checking = true]]
+declare[[invariants_strict_checking = true]]
 
 text\<open>For example, let's define the following two classes:\<close>
 
@@ -47,12 +49,48 @@ text\<open>
   it inherits @{doc_class class_inv1} invariants.
   Hence the \<^term>\<open>int1\<close> invariant is checked when the instance @{docitem testinv2} is defined.\<close>
 
+text\<open>Test invariant for attributes of attributes: \<close>
+
+doc_class inv_test1 =
+  a :: int
+
+doc_class inv_test2 =
+  b :: "inv_test1"
+  c:: int
+  invariant inv_test2 :: "c \<sigma> = 1"
+  invariant inv_test2' :: "a (b \<sigma>) = 2"
+
+doc_class inv_test3 = inv_test1 +
+  b :: "inv_test1"
+  c:: int
+  invariant inv_test3 :: "a \<sigma> = 2"
+  invariant inv_test3' :: "a (b \<sigma>) = 2"
+
+doc_class inv_test4 = inv_test2 +
+  d :: "inv_test3"
+  invariant inv_test4 :: "a (inv_test2.b \<sigma>) = 2"
+  invariant inv_test4' :: "a (d \<sigma>) = 2"
+
+text*[inv_test1_instance::inv_test1, a=2]\<open>\<close>
+text*[inv_test3_instance::inv_test3, a=2, b="@{inv-test1 \<open>inv_test1_instance\<close>}" ]\<open>\<close>
+text*[inv_test4_instance::inv_test4, b="@{inv-test1 \<open>inv_test1_instance\<close>}"
+                                   , c=1, d="@{inv-test3 \<open>inv_test3_instance\<close>}"]\<open>\<close>
+
+text\<open>To support invariant on attributes in attributes
+and invariant on attributes of the superclasses,
+we check that the type of the attribute of the subclass is ground:\<close>
+ML\<open>
+val Type(st, [ty]) = \<^typ>\<open>inv_test1\<close>
+val Type(st', [ty']) = \<^typ>\<open>'a inv_test1_scheme\<close>
+val t = ty = \<^typ>\<open>unit\<close>
+\<close>
+
 text\<open>Now assume the following ontology:\<close>
 
 doc_class title =
   short_title :: "string option" <= "None"
 
-doc_class author =
+doc_class Author =
   email :: "string" <= "''''"
 
 datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
@@ -62,18 +100,18 @@ doc_class abstract =
   safety_level :: "classification" <= "SIL3"
 
 doc_class text_section =
-  authored_by :: "author set" <= "{}"
+  authored_by :: "Author set" <= "{}"
   level :: "int option" <= "None"
 
 type_synonym notion = string
 
-doc_class introduction = text_section +
-  authored_by :: "author set"  <= "UNIV" 
+doc_class Introduction = text_section +
+  authored_by :: "Author set"  <= "UNIV" 
   uses :: "notion set"
   invariant author_finite :: "finite (authored_by \<sigma>)"
-  and force_level :: "the (level \<sigma>) > 1"
+  and force_level :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 1"
 
-doc_class claim = introduction +
+doc_class claim = Introduction +
   based_on :: "notion list"
 
 doc_class technical = text_section +
@@ -102,7 +140,7 @@ text\<open>Next we define some instances (docitems): \<close>
 
 declare[[invariants_checking_with_tactics = true]]
 
-text*[church::author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
+text*[church::Author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
 
 text*[resultProof::result, evidence = "proof", property="[@{thm \<open>HOL.refl\<close>}]"]\<open>\<close>
 text*[resultArgument::result, evidence = "argument"]\<open>\<close>
@@ -114,28 +152,29 @@ text\<open>The invariants \<^theory_text>\<open>author_finite\<close> and \<^the
 
 declare[[invariants_checking_with_tactics = true]]
 
-text*[curry::author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
-text*[introduction2::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
+text*[curry::Author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
+text*[introduction2::Introduction, authored_by = "{@{Author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
 (* When not commented, should violated the invariant:
-update_instance*[introduction2::introduction
-                  , authored_by := "{@{author \<open>church\<close>}}"
+update_instance*[introduction2::Introduction
+                  , authored_by := "{@{Author \<open>church\<close>}}"
                   , level := "Some 1"]
 *)
 
-text*[introduction3::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
-text*[introduction4::introduction, authored_by = "{@{author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
+
+text*[introduction3::Introduction, authored_by = "{@{Author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
+text*[introduction4::Introduction, authored_by = "{@{Author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
 
 text*[resultProof2::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"]\<open>\<close>
 
 text\<open>Then we can evaluate expressions with instances:\<close>
 
-term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
-value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
-value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction4\<close>}\<close>
+term*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
+value*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
+value*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction4\<close>}\<close>
 
-value*\<open>@{introduction \<open>introduction2\<close>}\<close>
+value*\<open>@{Introduction \<open>introduction2\<close>}\<close>
 
-value*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>
+value*\<open>{@{Author \<open>curry\<close>}} = {@{Author \<open>church\<close>}}\<close>
 
 term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
 value*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
@@ -144,6 +183,6 @@ value*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \
 
 declare[[invariants_checking_with_tactics = false]]
 
-declare[[invariants_checking = false]]
+declare[[invariants_strict_checking = false]]
 
 end

Isabelle_DOF-Unit-Tests/Isabelle_DOF-Unit-Tests_document.thy

@@ -0,0 +1,20 @@
+(*<*)
+theory "Isabelle_DOF-Unit-Tests_document"
+  imports
+    "Isabelle_DOF.technical_report"
+    "Isabelle_DOF-Ontologies.CENELEC_50128"
+  
+begin
+
+use_template "scrreprt-modern"
+use_ontology "technical_report" and "Isabelle_DOF-Ontologies.CENELEC_50128"
+
+(*>*)
+(* BUG: Invariant checking should not go across sessions boundaries.
+
+title*[title::title]         \<open>Isabelle/DOF\<close>
+subtitle*[subtitle::subtitle]\<open>Unit Tests\<close>
+*)
+(*<*)
+end
+(*>*)

Isabelle_DOF-Unit-Tests/Latex_Tests.thy

@@ -0,0 +1,435 @@
+(*************************************************************************
+ * Copyright (C) 
+ *               2019-2023 The University of Exeter 
+ *               2018-2023 The University of Paris-Saclay
+ *               2018      The University of Sheffield
+ *
+ * License:
+ *   This program can be redistributed and/or modified under the terms
+ *   of the 2-clause BSD-style license.
+ *
+ *   SPDX-License-Identifier: BSD-2-Clause
+ *************************************************************************)
+
+theory 
+  Latex_Tests
+imports 
+  "Isabelle_DOF-Unit-Tests_document"
+  "TestKit"
+keywords   "Figure*"          :: document_body  (* still experimental feature *)
+
+begin
+
+section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
+
+
+text\<open>Output status:\<close>
+print_doc_classes
+print_doc_items
+
+
+text\<open>And here a tex - text macro.\<close>
+text\<open>Pythons ReStructuredText (RST). 
+     @{url \<open>https://de.wikipedia.org/wiki/ReStructuredText\<close>}. Tool: Sphinx.
+    \<close>
+
+text*[aaaa::B]\<open>dfg @{thm [display] refl}\<close>
+                            
+text-[dfgdfg::B]
+\<open> Lorem ipsum ...  @{thm [display] refl}  Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
+
+text-latex\<open> Lorem ipsum ...  @{thm [display] refl}  Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
+
+text-[asd::B]
+\<open>... and here is its application macro expansion: 
+     @{B [display] "dfgdfg"} 
+     \textbf{TEST}
+     @{cartouche [display] 
+         \<open>text*[dfgdfg::B]
+           \<open> Lorem ipsum ...  @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
+          \<close>}
+\<close>
+
+text-latex\<open>... and here is its application macro expansion: 
+     @{B [display] "dfgdfg"} 
+     \textbf{TEST}
+     @{cartouche [display] 
+         \<open>text*[dfgdfg::B]
+           \<open> Lorem ipsum ...  @{thm refl}  Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
+          \<close>}\<close>
+
+(*<*)
+text-latex\<open> \<^theory_text>\<open>definition df = ...  
+        \<close>
+       @{ML      [display] \<open> let val x = 3 + 4 in true end 
+                           \<close>}
+
+       @{ML_text [display] \<open> val x = ...  
+                           \<close>}
+
+       @{verbatim [display] \<open> Lorem ipsum ...  @{thm refl} 
+                              Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>}
+       @{theory_text [display] \<open>definition df = ... \<lambda>x.  
+                               \<close>}
+       @{cartouche [display]   \<open> @{figure "cfgdfg"}\<close>} \<close>
+
+(*>*)
+text\<open>Final Status:\<close>
+print_doc_items
+print_doc_classes 
+
+section\<open>Experiments on Inline-Textelements\<close>
+text\<open>Std Abbreviations. Inspired by the block *\<open>control spacing\<close> 
+     in @{file \<open>$ISABELLE_HOME/src/Pure/Thy/document_antiquotations.ML\<close>}.
+     We mechanize the table-construction and even attach the LaTeX 
+     quirks to be dumped into the prelude.  \<close>
+
+ML\<open>
+val _ =
+  Theory.setup
+   (   Document_Output.antiquotation_raw \<^binding>\<open>doof\<close> (Scan.succeed ())
+          (fn _ => fn () => Latex.string "\\emph{doof}")
+    #> Document_Output.antiquotation_raw \<^binding>\<open>LATEX\<close> (Scan.succeed ())
+          (fn _ => fn () => Latex.string "\\textbf{LaTeX}") 
+   )
+\<close>
+
+text-latex\<open> \<^doof> \<^LATEX> \<close>
+
+(* the same effect is achieved with : *)
+setup \<open>DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\<close>
+(* Note that this assumes that the generated LaTeX macro call "\blabla" is defined somewhere in the
+   target document, for example, in the tex prelude. Note that the "Binding.make" can be avoided
+   using the alternative \<^binding> notation (see above).*)
+
+
+setup\<open>DOF_lib.define_macro (Binding.make("blong",\<^here>)) "\\blong{" "}" (K(K()))\<close>
+
+(*<*)
+text-latex\<open> \<^blong>\<open>asd\<close> outer  \<^blong>\<open>syntax| ! see {syntax, outer}\<close> \<close>
+(*>*)
+
+ML\<open>
+
+fun report_text ctxt text =
+    let val pos = Input.pos_of text in
+       Context_Position.reports ctxt
+         [(pos, Markup.language_text (Input.is_delimited text)),
+          (pos, Markup.raw_text)]
+    end;
+
+fun report_theory_text ctxt text =
+    let val keywords = Thy_Header.get_keywords' ctxt;
+        val _ = report_text ctxt text;
+        val _ =
+          Input.source_explode text
+          |> Token.tokenize keywords {strict = true}
+          |> maps (Token.reports keywords)
+          |> Context_Position.reports_text ctxt;
+    in () end
+
+fun prepare_text ctxt =
+  Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt;
+(* This also produces indent-expansion and changes space to "\_" and the introduction of "\newline",
+   I believe. Otherwise its in Thy_Output.output_source, the compiler from string to LaTeX.text. *)
+
+fun string_2_text_antiquotation ctxt text = 
+        prepare_text ctxt text
+        |> Document_Output.output_source ctxt
+        |> Document_Output.isabelle ctxt
+
+fun string_2_theory_text_antiquotation ctxt text =
+      let
+        val keywords = Thy_Header.get_keywords' ctxt;
+      in
+        prepare_text ctxt text
+        |> Token.explode0 keywords
+        |> maps (Document_Output.output_token ctxt)
+        |> Document_Output.isabelle ctxt
+      end
+
+fun gen_text_antiquotation name reportNcheck compile =
+  Document_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
+    (fn ctxt => fn text:Input.source =>
+      let
+        val _ = reportNcheck ctxt text;
+      in
+        compile ctxt text    
+      end);
+
+fun std_text_antiquotation name (* redefined in these more abstract terms *) =
+    gen_text_antiquotation name report_text string_2_text_antiquotation
+
+(* should be the same as (2020):
+fun text_antiquotation name =
+  Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
+    (fn ctxt => fn text =>
+      let
+        val _ = report_text ctxt text;
+      in
+        prepare_text ctxt text
+        |> Thy_Output.output_source ctxt
+        |> Thy_Output.isabelle ctxt
+      end);
+*)
+
+fun std_theory_text_antiquotation name (* redefined in these more abstract terms *) =
+    gen_text_antiquotation name report_theory_text string_2_theory_text_antiquotation
+
+(* should be the same as (2020):
+fun theory_text_antiquotation name =
+  Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
+    (fn ctxt => fn text =>
+      let
+        val keywords = Thy_Header.get_keywords' ctxt;
+
+        val _ = report_text ctxt text;
+        val _ =
+          Input.source_explode text
+          |> Token.tokenize keywords {strict = true}
+          |> maps (Token.reports keywords)
+          |> Context_Position.reports_text ctxt;
+      in
+        prepare_text ctxt text
+        |> Token.explode0 keywords
+        |> maps (Thy_Output.output_token ctxt)
+        |> Thy_Output.isabelle ctxt
+        |> enclose_env ctxt "isarbox"
+      end);
+*)
+
+
+
+fun enclose_env ctxt block_env body =
+  if Config.get ctxt Document_Antiquotation.thy_output_display
+  then Latex.environment block_env body
+  else body;
+
+
+fun boxed_text_antiquotation name (* redefined in these more abstract terms *) =
+    gen_text_antiquotation name report_text 
+                           (fn ctxt => string_2_text_antiquotation ctxt
+                                       #> enclose_env ctxt "isarbox")
+
+
+fun boxed_theory_text_antiquotation name (* redefined in these more abstract terms *) =
+    gen_text_antiquotation name report_theory_text 
+                           (fn ctxt => string_2_theory_text_antiquotation ctxt 
+                                        #> enclose_env ctxt "isarbox")
+
+
+(*   #> enclose_env ctxt "isarbox" *)
+
+val _ = Theory.setup
+   (std_text_antiquotation          \<^binding>\<open>my_text\<close> #>
+    boxed_text_antiquotation        \<^binding>\<open>boxed_text\<close> #>
+    std_text_antiquotation          \<^binding>\<open>my_cartouche\<close> #>
+    boxed_text_antiquotation        \<^binding>\<open>boxed_cartouche\<close> #>
+    std_theory_text_antiquotation   \<^binding>\<open>my_theory_text\<close>#>
+    boxed_theory_text_antiquotation \<^binding>\<open>boxed_theory_text\<close>); (* is overriding possible ?*)
+
+\<close>
+(*<*)
+text-latex\<open> 
+      @{boxed_cartouche   [display] \<open>definition dfg = \<lambda>x. x\<close>}
+      @{boxed_theory_text [display] \<open>doc_class dfg = \<lambda>x... \<Gamma>\<close>}  \<close>
+(*>*)
+
+
+
+section\<open>Section Experiments of picture-content\<close>
+
+
+ML\<open>
+
+val thy_output_display = Attrib.setup_option_bool ("thy_output_display", \<^here>);
+
+val caption_param = Config.declare_string ("caption", \<^here>) (K "");
+val width_param   = Config.declare_int    ("width", \<^here>)   (K 80);  \<comment> \<open>char per line\<close>
+val scale_param   = Config.declare_int    ("scale", \<^here>)   (K 100); \<comment> \<open>in percent\<close>
+
+Config.put caption_param;
+Config.put_global;
+Config.get ;
+
+(*
+      Latex.string (enclose "[" "]" (String.concat [ label_and_type, ", args={", (commas str_args), "}"]))
+*)
+
+(*
+\begin{figure}[h]
+     \centering
+
+     \includegraphics[scale=0.5]{graph_a}
+     \caption{An example graph}
+
+     \label{fig:x cubed graph}
+\end{figure}
+
+
+\begin{figure}
+     \centering
+
+     \begin{subfigure}[b]{0.3\textwidth}
+
+         \centering
+         \includegraphics[width=\textwidth]{graph1}
+         \caption{$y=x$}
+
+         \label{fig:y equals x}   (* PROBLEM *)
+     \end{subfigure}
+
+     \hfill
+
+     \begin{subfigure}[b]{0.3\textwidth}
+
+         \centering
+         \includegraphics[width=\textwidth]{graph2}
+         \caption{$y=3sinx$}
+
+         \label{fig:three sin x}  (* PROBLEM *)
+     \end{subfigure}
+
+     \hfill
+
+     \begin{subfigure}[b]{0.3\textwidth}
+
+         \centering
+         \includegraphics[width=\textwidth]{graph3}
+         \caption{$y=5/x$}
+
+         \label{fig:five over x} (* PROBLEM *)
+     \end{subfigure}
+
+  \caption{Three simple graphs}
+  \label{fig:three graphs}
+\end{figure}
+
+
+\begin{wrapfigure}{l}{0.5\textwidth}
+
+     \centering
+     \includegraphics[width=1.5cm]{logo.png}
+     \caption{$y=5/x$}
+
+\end{wrapfigure}
+
+*)
+
+datatype figure_type   = single | subfigure | float_embedded
+
+(* to check if this can be done more properly: user-state or attributes ??? *)
+val figure_mode        = Unsynchronized.ref(float_embedded)
+val figure_label       = Unsynchronized.ref(NONE:string option)
+val figure_proportions = Unsynchronized.ref([]:int list)
+(* invariant : !figure_mode = subfigure_embedded ==> length(!figure_proportions) > 1 *)
+
+fun figure_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) =
+  Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) =>
+   (check ctxt NONE source;
+    let val cap = Config.get ctxt caption_param
+        val cap_txt = if cap = "" then "" else (Library.enclose "\n\\caption{" "}\n" cap)
+                      \<comment> \<open>this is naive. one should add an evaluation of doc antiquotations here\<close>
+        val wdth= Config.get ctxt width_param
+        val wdth_ltx = (if wdth = 100 then "" 
+                       else if 10<=wdth andalso wdth<=99 
+                            then "width=0."^(Int.toString wdth)
+                            else if 1<=wdth then "width=0.0"^(Int.toString wdth)
+                                 else error "width out of range (must be between 1 and 100"
+                       )^"\\textwidth"
+        val scl = Config.get ctxt scale_param
+        val scl_ltx = if scl = 100 then "" 
+                       else if 10<=scl andalso scl<=99 then "scale=0."^(Int.toString scl)
+                            else if 1<=scl then "scale=0.0"^(Int.toString scl)
+                                 else error "scale out of range (must be between 1 and 100"
+        val fig_args = Library.enclose "[" "]" (commas [wdth_ltx,scl_ltx])
+        val _ = writeln cap
+        fun proportion () = "0."^ (Int.toString (100 div List.length(!figure_proportions)))
+                             \<comment> \<open>naive: assumes equal proportions\<close>
+        fun core arg = "\n\\centering\n"
+                       ^"\\includegraphics"
+                       ^fig_args^(Library.enclose "{" "}" arg)
+                       ^cap_txt
+                       \<comment> \<open>add internal labels here\<close>
+        fun pat arg = case !figure_mode of
+                       single => core arg   
+                      |subfigure =>   "\n\\begin{subfigure}[b]{"^proportion ()^"\\textwidth}"
+                                     ^ core arg 
+                                     ^"\n\\end{subfigure}\n"
+                      |float_embedded => "\n\\begin{wrapfigure}{r}{"^wdth_ltx^"}"
+                                         ^ core arg 
+                                         ^"\n\\end{wrapfigure}\n"
+                   
+    in   (Latex.output_ascii_breakable "/" (Input.string_of source))
+        |> pat
+        |> Latex.string
+    end));
+
+val _ = Theory.setup
+ (Document_Antiquotation.setup_option \<^binding>\<open>width\<close> 
+       (Config.put width_param o Document_Antiquotation.integer) #>
+  Document_Antiquotation.setup_option \<^binding>\<open>scale\<close> 
+       (Config.put scale_param o Document_Antiquotation.integer) #>
+  Document_Antiquotation.setup_option \<^binding>\<open>caption\<close> 
+       (Config.put caption_param) #>
+  Document_Output.antiquotation_raw_embedded \<^binding>\<open>figure_content\<close> 
+       (figure_antiq Resources.check_file) (K I)
+
+ );
+\<close>
+
+(*<*)
+text-latex\<open>
+@{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"}
+\<close>
+(*>*)
+ML\<open>
+
+fun gen_enriched_document_command3 name {body} cid_transform attr_transform markdown
+                                  (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
+                                     xstring_opt:(xstring * Position.T) option),
+                                    toks:Input.source list)
+= gen_enriched_document_command2 name {body=body} cid_transform attr_transform markdown
+                                  (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
+                                     xstring_opt:(xstring * Position.T) option),
+                                     toks) \<comment> \<open>Hack : drop second and thrd args.\<close>
+
+val _ =
+  Outer_Syntax.command ("Figure*", @{here}) "multiple figure"
+    (ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source 
+      >> (Toplevel.theory o (gen_enriched_document_command2 "TTT" {body=true} I I {markdown = true} )));
+
+
+\<close>
+(*
+Figure*[fff::figure,src="\<open>this is a side-by-side\<close>"]
+   \<open>@{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"}\<close> 
+   \<open> \<^doof> \<^LATEX> \<close>  
+   \<open> \<^theory_text>\<open>definition df = ... \<close>
+     @{ML        [display]   \<open> let val x = 3 + 4 in true end\<close>}
+     @{cartouche [display]   \<open> @{figure "cfgdfg"}\<close>}
+   \<close>  
+*)
+
+(*<*)
+Figure*[ffff::figure2, caption="\<open>this is another 2 side-by-side\<close>"]
+   \<open>@{figure_content [width=40, scale=35, caption="This is a left test"] "ROOT"}\<close> 
+   \<open>@{figure_content [width=40, scale=35, caption="This is a right test"] "ROOT"}\<close>  
+
+(* proposed syntax for sub-figure labels : text\<open> @{figure "ffff(2)"}\<close> *)
+
+Figure*[figxxx::figure2,caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
+\<open>@{boxed_theory_text [display]
+\<open>lemma inv_c2_preserved :  "c2_inv \<sigma> \<Longrightarrow> c1_inv (\<sigma> \<langle>Hardware\<rangle>\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e)"
+  unfolding c1_inv_def c2_inv_def 
+            Computer_Hardware_to_Hardware_morphism_def
+            Product_to_Component_morphism_def  
+  by (auto simp: comp_def)
+
+lemma Computer_Hardware_to_Hardware_total :
+         "Computer_Hardware_to_Hardware_morphism ` ({X. c2_inv X}) 
+      \<subseteq> ({X::Hardware. c1_inv X})"
+  using inv_c2_preserved by auto\<close>}\<close> 
+
+end
+(*>*)

Isabelle_DOF-Unit-Tests/Ontology_Matching_Example.thy

@@ -2,6 +2,8 @@ chapter\<open>Ontologys Mathing\<close>
 
 theory Ontology_Matching_Example
   imports "Isabelle_DOF.Isa_DOF"
+  "Isabelle_DOF-Unit-Tests_document"
+
 begin
 
 text\<open>Using HOL, we can define a mapping between two ontologies.

Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy

@@ -14,117 +14,16 @@
 theory 
   OutOfOrderPresntn
 imports 
-  "Isabelle_DOF.Conceptual"
-keywords "text-" "textN"    :: document_body  
-    and  "Figure*"          :: document_body 
+  "Isabelle_DOF-Unit-Tests_document"
+  "TestKit"
+  "Isabelle_DOF-Ontologies.Conceptual"
+keywords  "Figure*"          :: document_body 
 
 begin
 
 section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
 
 
-text\<open>Current status:\<close>
-print_doc_classes
-print_doc_items
-
-(* this corresponds to low-level accesses : *)
-ML\<open>  
-val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab,...} 
-    = DOF_core.get_data @{context};
-Symtab.dest docitem_tab;
-Symtab.dest docclass_tab;
-app;
-\<close>
-
-
-ML\<open> 
-
-val _ = Document_Output.document_output
-
-fun gen_enriched_document_command2 name {body} cid_transform attr_transform markdown
-                                  (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
-                                     xstring_opt:(xstring * Position.T) option),
-                                    toks_list:Input.source list) 
-                                  : theory -> theory =
-  let  val toplvl = Toplevel.theory_toplevel
-
-       (* as side-effect, generates markup *)
-       fun check_n_tex_text thy toks = let val ctxt = Toplevel.presentation_context (toplvl thy);
-                                      val pos = Input.pos_of toks;
-                                      val _ =   Context_Position.reports ctxt
-                                                [(pos, Markup.language_document (Input.is_delimited toks)),
-                                                 (pos, Markup.plain_text)];
-                                      fun markup xml = let val m = if body then Markup.latex_body 
-                                                                   else Markup.latex_heading
-                                                       in [XML.Elem (m (Latex.output_name name), 
-                                                           xml)] end;
-
-                                      val text = Document_Output.output_document 
-                                                                 (Proof_Context.init_global thy) 
-                                                                 markdown toks
-(*   type file = {path: Path.T, pos: Position.T, content: string} *) 
-
-                                      val strg = XML.string_of (hd (Latex.output text))
-                                      val file = {path = Path.make [oid ^ "_snippet.tex"],
-                                                  pos = @{here}, 
-                                                  content = strg}
-                                      
-                                      val _ = Generated_Files.write_file (Path.make ["latex_test"]) 
-                                                                         file
-                                      val _ = writeln (strg)
-                                  in  () end \<comment> \<open>important observation: thy is not modified.
-                                                  This implies that several text block can be 
-                                                  processed in parallel in a future, as long
-                                                  as they are associated to one meta arg.\<close>
-       
-       (* ... generating the level-attribute syntax *)
-  in   
-       (   Value_Command.Docitem_Parser.create_and_check_docitem 
-                              {is_monitor = false} {is_inline = false} 
-                              oid pos (cid_transform cid_pos) (attr_transform doc_attrs)
-        #> (fn thy => (app (check_n_tex_text thy) toks_list; thy))) 
-  end;
-
-val _ =
-  Outer_Syntax.command ("text-", @{here}) "formal comment macro"
-    (ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source 
-      >> (Toplevel.theory o (gen_enriched_document_command2 "TTT" {body=true} I I {markdown = true} )));
-
-(* copied from Pure_syn for experiments *)
-
-fun output_document2 state markdown txt =
-  let
-    val ctxt = Toplevel.presentation_context state;
-    val pos = Input.pos_of txt;
-    val _ =
-      Context_Position.reports ctxt
-        [(pos, Markup.language_document (Input.is_delimited txt)),
-         (pos, Markup.plain_text)];
-    val txt' = Document_Output.output_document ctxt markdown txt
-    val strg = XML.string_of (hd (Latex.output txt'))
-
-    val _ = writeln (strg)
-  in Document_Output.output_document ctxt markdown txt end;
-
-fun document_command2 markdown (loc, txt) =
-  Toplevel.keep (fn state =>
-                    (case loc of
-                      NONE => ignore (output_document2 state markdown txt)
-                    | SOME (_, pos) =>
-                        error ("Illegal target specification -- not a theory context" 
-                               ^ Position.here pos))) 
- o 
-  Toplevel.present_local_theory loc 
-                (fn state =>  (output_document2 state markdown txt));
-
-
-val _ =
-  Outer_Syntax.command ("textN", \<^here>) "formal comment (primary style)"
-    (Parse.opt_target -- Parse.document_source >> document_command2 {markdown = true});
-
-
-\<close>
-
 
 text\<open>And here a tex - text macro.\<close>
 text\<open>Pythons ReStructuredText (RST). 
@@ -132,11 +31,13 @@ text\<open>Pythons ReStructuredText (RST).
     \<close>
 
 text*[aaaa::B]\<open>dfg @{thm [display] refl}\<close>
+
+(*<*)
                             
 text-[dfgdfg::B]
-\<open> Lorem ipsum ...  @{thm [display] refl} _ Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
+\<open> Lorem ipsum ...  @{thm [display] refl}  Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
 
-textN\<open> Lorem ipsum ...  @{thm [display] refl} _ Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
+text-latex\<open> Lorem ipsum ...  @{thm [display] refl}  Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
 
 text-[asd::B]
 \<open>... and here is its application macro expansion: 
@@ -144,19 +45,19 @@ text-[asd::B]
      \textbf{TEST}
      @{cartouche [display] 
          \<open>text*[dfgdfg::B]
-           \<open> Lorem ipsum ...  @{thm refl} _ Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
+           \<open> Lorem ipsum ...  @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
           \<close>}
 \<close>
 
-textN\<open>... and here is its application macro expansion: 
+text-latex\<open>... and here is its application macro expansion: 
      @{B [display] "dfgdfg"} 
      \textbf{TEST}
      @{cartouche [display] 
          \<open>text*[dfgdfg::B]
-           \<open> Lorem ipsum ...  @{thm refl} _ Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
+           \<open> Lorem ipsum ...  @{thm refl}  Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
           \<close>}\<close>
 
-textN\<open> \<^theory_text>\<open>definition df = ...  
+text-latex\<open> \<^theory_text>\<open>definition df = ...  
         \<close>
        @{ML      [display] \<open> let val x = 3 + 4 in true end 
                            \<close>}
@@ -164,13 +65,13 @@ textN\<open> \<^theory_text>\<open>definition df = ...
        @{ML_text [display] \<open> val x = ...  
                            \<close>}
 
-       @{verbatim [display] \<open> Lorem ipsum ...  @{thm refl} _ 
+       @{verbatim [display] \<open> Lorem ipsum ...  @{thm refl} 
                               Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>}
        @{theory_text [display] \<open>definition df = ... \<lambda>x.  
                                \<close>}
        @{cartouche [display]   \<open> @{figure "cfgdfg"}\<close>} \<close>
 
-(*<*)
+
 text\<open>Final Status:\<close>
 print_doc_items
 print_doc_classes 
@@ -191,7 +92,7 @@ val _ =
    )
 \<close>
 
-textN\<open> \<^doof> \<^LATEX> \<close>
+text-latex\<open> \<^doof> \<^LATEX> \<close>
 
 (* the same effect is achieved with : *)
 setup \<open>DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\<close>
@@ -199,10 +100,10 @@ setup \<open>DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\<
    target document, for example, in the tex prelude. Note that the "Binding.make" can be avoided
    using the alternative \<^binding> notation (see above).*)
 
-
 setup\<open>DOF_lib.define_macro (Binding.make("blong",\<^here>)) "\\blong{" "}" (K(K()))\<close>
 
-textN\<open> \<^blong>\<open>asd\<close> outer  \<^blong>\<open>syntax| ! see {syntax, outer}\<close> \<close>
+text-latex\<open> \<^blong>\<open>asd\<close> outer  \<^blong>\<open>syntax| ! see {syntax, outer}\<close> \<close>
+(*>*)
 
 ML\<open>
 
@@ -325,14 +226,16 @@ val _ = Theory.setup
 
 \<close>
 
-textN\<open> 
+(*<*)
+text-latex\<open> 
       @{boxed_cartouche   [display] \<open>definition dfg = \<lambda>x. x\<close>}
       @{boxed_theory_text [display] \<open>doc_class dfg = \<lambda>x... \<Gamma>\<close>}  \<close>
-
+(*>*)
 
 
 section\<open>Section Experiments of picture-content\<close>
 
+(*<*)
 
 ML\<open>
 
@@ -352,8 +255,8 @@ Config.get ;
 
 (*
 \begin{figure}[h]
-
      \centering
+
      \includegraphics[scale=0.5]{graph_a}
      \caption{An example graph}
 
@@ -362,35 +265,37 @@ Config.get ;
 
 
 \begin{figure}
-
      \centering
+
      \begin{subfigure}[b]{0.3\textwidth}
 
          \centering
          \includegraphics[width=\textwidth]{graph1}
          \caption{$y=x$}
 
-         \label{fig:y equals x}
+         \label{fig:y equals x}   (* PROBLEM *)
      \end{subfigure}
 
      \hfill
+
      \begin{subfigure}[b]{0.3\textwidth}
 
          \centering
          \includegraphics[width=\textwidth]{graph2}
          \caption{$y=3sinx$}
 
-         \label{fig:three sin x}
+         \label{fig:three sin x}  (* PROBLEM *)
      \end{subfigure}
 
      \hfill
+
      \begin{subfigure}[b]{0.3\textwidth}
 
          \centering
          \includegraphics[width=\textwidth]{graph3}
          \caption{$y=5/x$}
 
-         \label{fig:five over x}
+         \label{fig:five over x} (* PROBLEM *)
      \end{subfigure}
 
   \caption{Three simple graphs}
@@ -436,7 +341,7 @@ fun figure_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.
                                  else error "scale out of range (must be between 1 and 100"
         val fig_args = Library.enclose "[" "]" (commas [wdth_ltx,scl_ltx])
         val _ = writeln cap
-        fun proportion () = "0."^ (Int.toString (100 div length(!figure_proportions)))
+        fun proportion () = "0."^ (Int.toString (100 div List.length(!figure_proportions)))
                              \<comment> \<open>naive: assumes equal proportions\<close>
         fun core arg = "\n\\centering\n"
                        ^"\\includegraphics"
@@ -470,8 +375,8 @@ val _ = Theory.setup
  );
 \<close>
 
-textN\<open>
-@{figure_content [width=40, scale=35, caption="This is a test"] "../ROOT"}
+text-latex\<open>
+@{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"}
 \<close>
 
 ML\<open>
@@ -492,23 +397,37 @@ val _ =
 
 
 \<close>
-
+(*
 Figure*[fff::figure,src="\<open>this is a side-by-side\<close>"]
-   \<open>@{figure_content [width=40, scale=35, caption="This is a test"] "../ROOT"}\<close> 
+   \<open>@{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"}\<close> 
    \<open> \<^doof> \<^LATEX> \<close>  
    \<open> \<^theory_text>\<open>definition df = ... \<close>
      @{ML        [display]   \<open> let val x = 3 + 4 in true end\<close>}
      @{cartouche [display]   \<open> @{figure "cfgdfg"}\<close>}
    \<close>  
+*)
 
 
-Figure*[ffff::figure,(* caption *) src="\<open>this is another 2 side-by-side\<close>"]
-   \<open>@{figure_content [width=40, scale=35, caption="This is a left test"] "../ROOT"}\<close> 
-   \<open>@{figure_content [width=40, scale=35, caption="This is a right test"] "../ROOT"}\<close>  
+Figure*[ffff::figure2, caption="\<open>this is another 2 side-by-side\<close>"]
+   \<open>@{figure_content [width=40, scale=35, caption="This is a left test"] "ROOT"}\<close> 
+   \<open>@{figure_content [width=40, scale=35, caption="This is a right test"] "ROOT"}\<close>  
 
 (* proposed syntax for sub-figure labels :
 text\<open> @{figure "ffff(2)"}\<close>
  *)
 
+Figure*[figxxx::figure2,caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
+\<open>@{boxed_theory_text [display]
+\<open>lemma inv_c2_preserved :  "c2_inv \<sigma> \<Longrightarrow> c1_inv (\<sigma> \<langle>Hardware\<rangle>\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e)"
+  unfolding c1_inv_def c2_inv_def 
+            Computer_Hardware_to_Hardware_morphism_def
+            Product_to_Component_morphism_def  
+  by (auto simp: comp_def)
+
+lemma Computer_Hardware_to_Hardware_total :
+         "Computer_Hardware_to_Hardware_morphism ` ({X. c2_inv X}) 
+      \<subseteq> ({X::Hardware. c1_inv X})"
+  using inv_c2_preserved by auto\<close>}\<close> 
+
 end
 (*>*)

Isabelle_DOF-Unit-Tests/ROOT

@@ -0,0 +1,19 @@
+session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" + 
+  options [document = pdf, document_output = "output", document_build = dof]
+  theories
+    "TestKit"
+    "Latex_Tests"
+    "Concept_OntoReferencing"
+    "Concept_Example_Low_Level_Invariant"
+    "TermAntiquotations"
+    "Attributes"
+    "Evaluation"
+    "AssnsLemmaThmEtc" 
+    "High_Level_Syntax_Invariants"
+    "Ontology_Matching_Example"
+    "Cenelec_Test"
+    "OutOfOrderPresntn"
+  document_files
+    "root.bib"
+    "figures/A.png"
+    "figures/B.png"

Isabelle_DOF-Unit-Tests/TermAntiquotations.thy

@@ -0,0 +1,523 @@
+(*************************************************************************
+ * Copyright (C) 
+ *               2019      The University of Exeter 
+ *               2018-2019 The University of Paris-Saclay
+ *               2018      The University of Sheffield
+ *
+ * License:
+ *   This program can be redistributed and/or modified under the terms
+ *   of the 2-clause BSD-style license.
+ *
+ *   SPDX-License-Identifier: BSD-2-Clause
+ *************************************************************************)
+
+chapter\<open>Term Antiquotations\<close>
+
+text\<open>Terms are represented by "Inner Syntax" parsed by an Earley parser in Isabelle.
+For historical reasons, \<^emph>\<open>term antiquotations\<close> are called therefore somewhat misleadingly
+"Inner Syntax Antiquotations". \<close>
+
+theory 
+  TermAntiquotations
+imports 
+  "Isabelle_DOF-Unit-Tests_document"
+  "Isabelle_DOF-Ontologies.Conceptual"
+keywords "definition*" :: thy_defn
+and "theorem*" "lemma*" "corollary*" "proposition*" :: thy_goal_stmt
+and "schematic_goal*" :: thy_goal_stmt
+
+begin
+
+
+record AA =
+aa :: int
+bb :: nat
+record BB = AA +
+cc :: int
+
+typ "AA"
+ML\<open>
+val Type(s, t) = \<^typ>\<open>AA\<close>
+\<close>
+ML\<open>
+val thy = \<^theory>
+val ns = Sign.tsig_of thy |> Type.type_space
+val Type(name, t) = \<^typ>\<open>AA\<close>
+val {pos, ...} = Name_Space.the_entry ns name
+\<close>
+find_consts name:"AA"
+find_theorems (50) name:"AA"
+ML\<open>
+val t = Record.get_info \<^theory> 
+\<close>
+print_record AA
+ML\<open>
+val t = Record.string_of_record \<^context> "AA" |> YXML.parse_body |> XML.content_of
+\<close>
+ML\<open>
+val t = Syntax.read_typ \<^context> "AA" |> Record.pretty_recT \<^context>
+\<close>
+ML\<open>
+val t = Record.get_recT_fields \<^theory> \<^typ>\<open>AA\<close>
+\<close>
+ML\<open>
+val t = Record.get_recT_fields \<^theory> \<^typ>\<open>BB\<close>
+\<close>
+ML\<open>
+val t = Record.dest_recTs \<^typ>\<open>BB\<close>
+\<close>
+ML\<open>
+val Type(s, t) = \<^typ>\<open>AA\<close>
+\<close>
+ML\<open>
+val t = Record.get_info \<^theory> "TermAntiquotations.BB"
+\<close>
+print_record "BB"
+
+
+ML\<open>
+
+(* definition *)
+
+fun get_positions ctxt x =
+  let
+    fun get Cs (Const ("_type_constraint_", C) $ t) = get (C :: Cs) t
+      | get Cs (Free (y, T)) =
+          if x = y then
+            map_filter Term_Position.decode_positionT
+              (T :: map (Type.constraint_type ctxt) Cs)
+          else []
+      | get _ (t $ u) = get [] t @ get [] u
+      | get _ (Abs (_, _, t)) = get [] t
+      | get _ _ = [];
+  in get [] end;
+
+fun prep_decls prep_var raw_vars ctxt =
+  let
+    val (vars, ctxt') = fold_map prep_var raw_vars ctxt;
+    val (xs, ctxt'') = ctxt'
+      |> Context_Position.set_visible false
+      |> Proof_Context.add_fixes vars
+      ||> Context_Position.restore_visible ctxt';
+    val _ =
+      Context_Position.reports ctxt''
+        (map (Binding.pos_of o #1) vars ~~
+          map (Variable.markup_entity_def ctxt'' ##> Properties.remove Markup.kindN) xs);
+  in ((vars, xs), ctxt'') end;
+
+fun dummy_frees ctxt xs tss =
+  let
+    val names =
+      Variable.names_of ((fold o fold) Variable.declare_term tss ctxt)
+      |> fold Name.declare xs;
+    val (tss', _) = (fold_map o fold_map) Term.free_dummy_patterns tss names;
+  in tss' end;
+
+fun prep_spec_open prep_var parse_prop raw_vars raw_params raw_prems raw_concl ctxt =
+  let
+    val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
+    val (ys, params_ctxt) = vars_ctxt |> fold_map prep_var raw_params |-> Proof_Context.add_fixes;
+
+    val props =
+      map (parse_prop params_ctxt) (raw_concl :: raw_prems)
+      |> singleton (dummy_frees params_ctxt (xs @ ys));
+    val concl :: prems = Syntax.check_props params_ctxt props;
+    val spec = Logic.list_implies (prems, concl);
+    val spec' = DOF_core.transduce_term_global {mk_elaboration=true}
+                                               (spec , Position.none)
+                                               (Proof_Context.theory_of ctxt)
+    (*val spec_ctxt = Variable.declare_term spec params_ctxt;*)
+    val spec_ctxt = Variable.declare_term spec' params_ctxt;
+
+    fun get_pos x = maps (get_positions spec_ctxt x) props;
+  (*in ((vars, xs, get_pos, spec), spec_ctxt) end;*)
+    in ((vars, xs, get_pos, spec'), spec_ctxt) end;
+
+val read_spec_open = prep_spec_open Proof_Context.read_var Syntax.parse_prop;
+
+fun gen_def prep_spec prep_att raw_var raw_params raw_prems ((a, raw_atts), raw_spec) int lthy =
+  let
+    val atts = map (prep_att lthy) raw_atts;
+
+    val ((vars, xs, get_pos, spec), _) = lthy
+      |> prep_spec (the_list raw_var) raw_params raw_prems raw_spec;
+    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy get_pos {conditional = true} spec;
+    val _ = Name.reject_internal (x, []);
+    val (b, mx) =
+      (case (vars, xs) of
+        ([], []) => (Binding.make (x, (case get_pos x of [] => Position.none | p :: _ => p)), NoSyn)
+      | ([(b, _, mx)], [y]) =>
+          if x = y then (b, mx)
+          else
+            error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
+              Position.here (Binding.pos_of b)));
+
+    val name = Thm.def_binding_optional b a;
+    val ((lhs, (_, raw_th)), lthy2) = lthy
+      |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
+
+    val th = prove lthy2 raw_th;
+    val lthy3 = lthy2 |> Spec_Rules.add name Spec_Rules.equational [lhs] [th];
+
+    val ([(def_name, [th'])], lthy4) = lthy3
+      |> Local_Theory.notes [((name, atts), [([th], [])])];
+
+    val lthy5 = lthy4
+      |> Code.declare_default_eqns [(th', true)];
+
+    val lhs' = Morphism.term (Local_Theory.target_morphism lthy5) lhs;
+
+    val _ =
+      Proof_Display.print_consts int (Position.thread_data ()) lthy5
+        (Frees.defined (Frees.build (Frees.add_frees lhs'))) [(x, T)];
+  in ((lhs, (def_name, th')), lthy5) end;
+
+val definition_cmd = gen_def read_spec_open Attrib.check_src;
+
+fun definition_cmd' meta_args_opt decl params prems spec bool ctxt =
+  Local_Theory.background_theory (Value_Command.meta_args_exec meta_args_opt) ctxt
+  |> definition_cmd decl params prems spec bool
+
+val _ =
+  Outer_Syntax.local_theory' \<^command_keyword>\<open>definition*\<close> "constant definition"
+    (ODL_Meta_Args_Parser.opt_attributes --
+      (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
+        Parse_Spec.if_assumes -- Parse.for_fixes)
+     >> (fn (meta_args_opt, (((decl, spec), prems), params)) => 
+                                    #2 oo definition_cmd' meta_args_opt decl params prems spec));
+
+\<close>
+
+
+ML\<open>
+local
+
+fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
+  let
+    val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt;
+    val _ = writeln ("In prep_statement stmt: " ^ \<^make_string> stmt)
+    val prems = Assumption.local_prems_of elems_ctxt ctxt;
+    val stmt_ctxt = fold (fold (Proof_Context.augment o fst) o snd) stmt elems_ctxt;
+  in
+    (case raw_stmt of
+      Element.Shows _ =>
+        let val stmt' = Attrib.map_specs (map prep_att) stmt
+            val _ = writeln ("In prep_statement case Element.Shows stmt': " ^ \<^make_string> stmt')
+            val stmt'' = map (fn (b, ts) =>
+                         (b, map (fn (t', t's) =>
+                         (DOF_core.transduce_term_global {mk_elaboration=true}
+                                                         (t' , Position.none)
+                                                         (Proof_Context.theory_of ctxt),
+                         map (fn t'' => 
+                         DOF_core.transduce_term_global {mk_elaboration=true}
+                                                        (t'' , Position.none)
+                                                        (Proof_Context.theory_of ctxt))
+                         t's)) ts)) stmt'
+        (*in (([], prems, stmt', NONE), stmt_ctxt) end*)
+        in (([], prems, stmt'', NONE), stmt_ctxt) end
+    | Element.Obtains raw_obtains =>
+        let
+          val asms_ctxt = stmt_ctxt
+            |> fold (fn ((name, _), asm) =>
+                snd o Proof_Context.add_assms Assumption.assume_export
+                  [((name, [Context_Rules.intro_query NONE]), asm)]) stmt;
+          val that = Assumption.local_prems_of asms_ctxt stmt_ctxt;
+          val ([(_, that')], that_ctxt) = asms_ctxt
+            |> Proof_Context.set_stmt true
+            |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])]
+            ||> Proof_Context.restore_stmt asms_ctxt;
+
+          val stmt' = [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])];
+          val stmt'' = map (fn (b, ts) =>
+                         (b, map (fn (t', t's) =>
+                         (DOF_core.transduce_term_global {mk_elaboration=true}
+                                                         (t' , Position.none)
+                                                         (Proof_Context.theory_of ctxt),
+                         map (fn t'' => 
+                         DOF_core.transduce_term_global {mk_elaboration=true}
+                                                        (t'' , Position.none)
+                                                        (Proof_Context.theory_of ctxt))
+                         t's)) ts)) stmt'
+          val _ = writeln ("In prep_statement case Element.Obtains stmt': " ^ \<^make_string> stmt')
+        (*in ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'), that_ctxt) end)*)
+        in ((Obtain.obtains_attribs raw_obtains, prems, stmt'', SOME that'), that_ctxt) end)
+  end;
+
+fun gen_theorem schematic bundle_includes prep_att prep_stmt
+    long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
+  let
+    val _ = Local_Theory.assert lthy;
+
+    val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy));
+    val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy
+      |> bundle_includes raw_includes
+      |> prep_statement (prep_att lthy) prep_stmt elems raw_concl;
+    val atts = more_atts @ map (prep_att lthy) raw_atts;
+
+    val pos = Position.thread_data ();
+    fun after_qed' results goal_ctxt' =
+      let
+        val results' =
+          burrow (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy) results;
+        val (res, lthy') =
+          if forall (Binding.is_empty_atts o fst) stmt then (map (pair "") results', lthy)
+          else
+            Local_Theory.notes_kind kind
+              (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
+        val lthy'' =
+          if Binding.is_empty_atts (name, atts) then
+            (Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy')
+          else
+            let
+              val ([(res_name, _)], lthy'') =
+                Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
+              val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res);
+            in lthy'' end;
+      in after_qed results' lthy'' end;
+
+    val prems_name = if long then Auto_Bind.assmsN else Auto_Bind.thatN;
+  in
+    goal_ctxt
+    |> not (null prems) ?
+      (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd)
+    |> Proof.theorem before_qed after_qed' (map snd stmt)
+    |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
+    |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
+        error "Illegal schematic goal statement")
+  end;
+
+in
+
+val theorem_cmd =
+  gen_theorem false Bundle.includes_cmd Attrib.check_src Expression.read_statement;
+
+fun theorem_cmd' meta_args_opt long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
+  Local_Theory.background_theory (Value_Command.meta_args_exec meta_args_opt) lthy
+  |> theorem_cmd long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int;
+
+val schematic_theorem_cmd =
+  gen_theorem true Bundle.includes_cmd Attrib.check_src Expression.read_statement;
+
+fun schematic_theorem_cmd' meta_args_opt long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
+  Local_Theory.background_theory (Value_Command.meta_args_exec meta_args_opt) lthy
+  |> schematic_theorem_cmd long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int;
+
+end;
+
+local
+val long_keyword =
+  Parse_Spec.includes >> K "" ||
+  Parse_Spec.long_statement_keyword;
+
+val long_statement =
+  ODL_Meta_Args_Parser.opt_attributes --
+  Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts --
+  Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
+    >> (fn (((meta_args_opt, binding), includes), (elems, concl)) => (meta_args_opt, true, binding, includes, elems, concl));
+
+val short_statement =
+  ODL_Meta_Args_Parser.opt_attributes --
+  Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
+    >> (fn (((meta_args_opt, shows), assumes), fixes) =>
+      (meta_args_opt, false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes],
+        Element.Shows shows));
+
+fun theorem spec schematic descr =
+  Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
+    ((long_statement || short_statement) >> (fn (meta_args_opt, long, binding, includes, elems, concl) =>
+      ((if schematic then schematic_theorem_cmd' else theorem_cmd')
+        meta_args_opt long Thm.theoremK NONE (K I) binding includes elems concl)));
+
+val _ = theorem \<^command_keyword>\<open>theorem*\<close> false "theorem";
+val _ = theorem \<^command_keyword>\<open>lemma*\<close> false "lemma";
+val _ = theorem \<^command_keyword>\<open>corollary*\<close> false "corollary";
+val _ = theorem \<^command_keyword>\<open>proposition*\<close> false "proposition";
+val _ = theorem \<^command_keyword>\<open>schematic_goal*\<close> true "schematic goal";
+in end
+\<close>
+
+declare [[ML_print_depth=40]]
+lemma* conj : "xx \<Longrightarrow> yy \<Longrightarrow> zz \<Longrightarrow> (xx \<and> yy) \<and> zz"
+  apply (rule conjI)
+  apply (rule conjI)
+  apply assumption
+  apply assumption
+  apply assumption
+  done
+
+lemma* "xx \<Longrightarrow> yy \<Longrightarrow> zz \<Longrightarrow> (xx \<and> yy) \<and> zz"
+  apply (rule conjI)
+  apply (rule conjI)
+  apply assumption
+  apply assumption
+  apply assumption
+  done
+
+text\<open>Since the syntax chosen for values of doc-class attributes is HOL-syntax --- requiring
+a fast read on the ``What's in Main''-documentation, but not additional knowledge on, say, SML --- 
+an own syntax for references to types, terms, theorems, etc. are necessary. These are the
+``Inner Syntax Antiquotations'' since they make only sense \emph{inside} the Inner-Syntax
+of Isabelle/Isar, so inside the \verb+" ... "+ parenthesis.
+
+They are the key-mechanism to denote 
+\<^item> Ontological Links, i.e. attributes refering to document classes defined by the ontology
+\<^item> Ontological F-Links, i.e. attributes referring to formal entities inside Isabelle (such as thm's)
+
+This file contains a number of examples resulting from the 
+% @ {theory "Isabelle_DOF-Unit-Tests.Conceptual"} does not work here --- why ?
+\<^theory_text>\<open>Conceptual\<close> - ontology; the emphasis of this presentation is to present the expressivity of 
+ODL on a paradigmatical example.
+\<close>
+
+
+text\<open>Voila the content of the Isabelle/DOF environment so far:\<close>
+ML\<open>
+val x = DOF_core.get_instances \<^context>
+val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>
+val docclass_tab = DOF_core.get_onto_classes \<^context>; 
+Name_Space.dest_table isa_transformer_tab; 
+\<close>
+
+text\<open>Some sample lemma:\<close>
+lemma murks : "Example=Example" by simp
+
+text\<open>Example for a meta-attribute of ODL-type @{typ "file"} with an appropriate ISA for the
+     file @{file "TermAntiquotations.thy"}\<close>
+(* not working: 
+text*[xcv::F, u="@{file ''InnerSyntaxAntiquotations.thy''}"]\<open>Lorem ipsum ...\<close>
+*)
+
+text*[xcv1::A, x=5]\<open>Lorem ipsum ...\<close>
+text*[xcv3::A, x=7]\<open>Lorem ipsum ...\<close>
+
+
+term\<open>
+cpo
+\<close>
+text*[xcv10::A, x=5, level= "Some 1"]\<open>Lorem ipsum ...\<close>
+ML\<open>
+val t = Local_Theory.level \<^context>
+\<close>
+doc_class AAA = 
+aaa :: "int list"
+definition xxx where "xxx \<equiv> 2 + 3::int"
+definition*[xcv11::A, x=5, level="Some 1"] xx' where "xx' \<equiv> A.x @{A \<open>xcv11\<close>}" if "A.x @{A \<open>xcv11\<close>} = 5"
+definition* xx where "xx \<equiv> A.x @{A \<open>xcv10\<close>}"
+(*definition* xx where "xx \<equiv> A.x @{A \<open>xcv10\<close>}" if "A.x @{A \<open>xcv10\<close>} = 5"*)
+value*\<open>xxx\<close>
+value*\<open>xx\<close>
+find_theorems name:"xx'"
+find_consts name:"xx'"
+find_theorems name:"xx"
+find_consts name:"xx"
+find_theorems name:"some"
+
+lemma* [xcv12::A, x=5, level="Some 1"] testtest : "xx + A.x @{A \<open>xcv12\<close>} = yy + A.x @{A \<open>xcv12\<close>} \<Longrightarrow> xx = yy"
+  by auto
+
+text\<open>Example for a meta-attribute of ODL-type @{typ "typ"} with an appropriate ISA for the
+     theorem @{thm "refl"}\<close>
+text*[xcv2::C, g="@{thm ''HOL.refl''}"]\<open>Lorem ipsum ...\<close>
+
+text\<open>A warning about the usage of the \<open>docitem\<close> TA:
+The \<open>docitem\<close> TA offers a way to check the reference of class instances
+without checking the instances type.
+So one will be able to reference \<open>docitem\<close>s (class instances) and have them checked,
+without the burden of the type checking required otherwise.
+But it may give rise to unwanted behaviors, due to its polymorphic type.
+It must not be used for certification.
+\<close>
+
+text\<open>Major sample: test-item of doc-class \<open>F\<close> with a relational link between class instances, 
+     and links to formal Isabelle items like \<open>typ\<close>, \<open>term\<close> and \<open>thm\<close>. \<close>
+text*[xcv4::F, r="[@{thm ''HOL.refl''}, 
+                   @{thm \<open>TermAntiquotations.murks\<close>}]", (* long names required *)
+               b="{(@{docitem ''xcv1''},@{docitem \<open>xcv2\<close>})}",  (* notations \<open>...\<close> vs. ''...'' *)
+               s="[@{typ \<open>int list\<close>}]",                        
+               properties = "[@{term \<open>H \<longrightarrow> H\<close>}]"              (* notation \<open>...\<close> required for UTF8*)
+]\<open>Lorem ipsum ...\<close>
+
+text*[xcv5::G, g="@{thm \<open>HOL.sym\<close>}"]\<open>Lorem ipsum ...\<close>
+
+text\<open>... and here we add a relation between @{docitem \<open>xcv3\<close>} and @{docitem \<open>xcv2\<close>} 
+into the relation \verb+b+ of @{docitem \<open>xcv5\<close>}. Note that in the link-relation,
+a @{typ "C"}-type is required, but a  @{typ "G"}-type is offered which is legal in
+\verb+Isa_DOF+ because of the sub-class relation between those classes: \<close>
+update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"]
+
+text\<open>And here is the results of some ML-term antiquotations:\<close>
+ML\<open> @{docitem_attribute b::xcv4} \<close>
+ML\<open> @{docitem xcv4}              \<close>
+ML\<open> @{docitem_name xcv4}         \<close>
+ML\<open> @{trace_attribute aaa}       \<close>
+
+text\<open>Now we might need to reference a class instance in a term command and we would like
+Isabelle to check that this instance is indeed an instance of this class.
+Here, we want to reference the instance @{docitem_name "xcv4"} previously defined.
+We can use the term* command which extends the classic term command
+and does the appropriate checking.\<close>
+term*\<open>@{F \<open>xcv4\<close>}\<close>
+
+text\<open>We can also reference an attribute of the instance.
+Here we reference the attribute r of the class F which has the type @{typ \<open>thm list\<close>}.\<close>
+term*\<open>r @{F \<open>xcv4\<close>}\<close>
+
+text\<open>We declare a new text element. Note that the class name contains an underscore "\_".\<close>
+text*[te::text_element]\<open>Lorem ipsum...\<close>
+
+text\<open>Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
+     this term antiquotation has to be denoted like this: @{term_ \<open>@{text-element \<open>te\<close>}\<close>}.
+     We need to substitute an hyphen "-" for the underscore "\_".\<close>
+term*\<open>@{text-element \<open>te\<close>}\<close>
+
+text\<open>Terms containing term antiquotations can be checked and evaluated
+using \<^theory_text>\<open>term_\<close> and \<^theory_text>\<open>value_\<close> text antiquotations respectively:
+We can print the term @{term_ \<open>r @{F \<open>xcv4\<close>}\<close>} with \<open>@{term_ \<open>r @{F \<open>xcv4\<close>}\<close>}\<close>
+or get the value of the \<^const>\<open>F.r\<close> attribute of @{docitem \<open>xcv4\<close>} with \<open>@{value_ \<open>r @{F \<open>xcv4\<close>}\<close>}\<close>
+\<^theory_text>\<open>value_\<close> may have an optional argument between square brackets to specify the evaluator but this
+argument must be specified after a default optional argument already defined
+by the text antiquotation implementation.
+So one must use the following syntax if he does not want to specify the first optional argument:
+\<open>@{value_ [] [nbe] \<open>r @{F \<open>xcv4\<close>}\<close>}\<close>. Note the empty brackets.
+
+\<close>
+
+text\<open>There also are \<^theory_text>\<open>term_\<close> and \<^theory_text>\<open>value_\<close> ML antiquotations:
+\<^ML>\<open>@{term_ \<open>r @{F \<open>xcv4\<close>}\<close>}\<close> will return the ML representation of the term \<^term_>\<open>r @{F \<open>xcv4\<close>}\<close>,
+and \<^ML>\<open>@{value_ \<open>r @{F \<open>xcv4\<close>}\<close>}\<close> will return the ML representation
+of the value of the \<^const>\<open>F.r\<close> attribute of @{docitem \<open>xcv4\<close>}.
+\<^theory_text>\<open>value_\<close> may have an optional argument between square brackets to specify the evaluator:
+\<close>
+
+ML\<open>
+val t = @{term_ \<open>r @{F \<open>xcv4\<close>}\<close>}
+val tt = @{value_ [nbe] \<open>r @{F \<open>xcv4\<close>}\<close>}
+\<close>
+
+record BBB =
+bbb ::int
+
+record cc = BBB +
+cc :: int
+
+definition BB1 :: BBB where "BB1 \<equiv> \<lparr> bbb = 2\<rparr>"
+
+find_consts name:"bb"
+
+ML\<open>
+val t = \<^Const>\<open>bb \<^typ>\<open>BB\<close>\<close> 
+\<close>
+
+ML\<open>
+val (Const(s, _), _) = Consts.check_const (Context.Proof \<^context>)
+                            (Sign.consts_of \<^theory>)
+                            ("bb", [Position.none])
+val ns = Consts.space_of (Sign.consts_of \<^theory>)
+val {pos, ...} = Name_Space.the_entry ns s
+\<close>
+term*\<open>
+A.x @{A \<open>xcv1\<close>} = 5
+
+\<close>
+end
+

Isabelle_DOF-Unit-Tests/TestKit.thy

@@ -0,0 +1,165 @@
+(*************************************************************************
+ * Copyright (C) 
+ *               2019-2023 The University of Exeter 
+ *               2018-2023 The University of Paris-Saclay
+ *               2018      The University of Sheffield
+ *
+ * License:
+ *   This program can be redistributed and/or modified under the terms
+ *   of the 2-clause BSD-style license.
+ *
+ *   SPDX-License-Identifier: BSD-2-Clause
+ *************************************************************************)
+
+theory 
+  TestKit
+imports 
+  "Isabelle_DOF-Unit-Tests_document"
+  "Isabelle_DOF-Ontologies.Conceptual"
+keywords "text-" "text-latex"    :: document_body
+    and  "text-assert-error":: document_body
+
+begin
+
+section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
+
+
+text\<open>Current status:\<close>
+print_doc_classes
+print_doc_items
+
+(* this corresponds to low-level accesses : *)
+ML\<open>
+val docitem_tab = DOF_core.get_instances \<^context>;
+val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>;
+val docclass_tab = DOF_core.get_onto_classes \<^context>;
+
+Name_Space.dest_table docitem_tab;
+Name_Space.dest_table isa_transformer_tab;
+Name_Space.dest_table docclass_tab;
+app;
+\<close>
+
+
+ML\<open> 
+
+val _ = Document_Output.document_output
+
+fun gen_enriched_document_command2 name {body} cid_transform attr_transform markdown
+                                  (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
+                                     xstring_opt:(xstring * Position.T) option),
+                                    toks_list:Input.source list) 
+                                  : theory -> theory =
+  let  val toplvl = Toplevel.theory_toplevel
+
+       (* as side-effect, generates markup *)
+       fun check_n_tex_text thy toks = let val ctxt = Toplevel.presentation_context (toplvl thy);
+                                      val pos = Input.pos_of toks;
+                                      val _ =   Context_Position.reports ctxt
+                                                [(pos, Markup.language_document (Input.is_delimited toks)),
+                                                 (pos, Markup.plain_text)];
+                                      fun markup xml = let val m = if body then Markup.latex_body 
+                                                                   else Markup.latex_heading
+                                                       in [XML.Elem (m (Latex.output_name name), 
+                                                           xml)] end;
+
+                                      val text = Document_Output.output_document 
+                                                                 (Proof_Context.init_global thy) 
+                                                                 markdown toks
+(*   type file = {path: Path.T, pos: Position.T, content: string} *) 
+
+                                      val strg = XML.string_of (hd (Latex.output text))
+                                      val file = {path = Path.make [oid ^ "_snippet.tex"],
+                                                  pos = @{here}, 
+                                                  content = Bytes.string strg}
+                                      
+                                      val _ = Generated_Files.write_file (Path.make ["latex_test"]) 
+                                                                         file
+                                      val _ = writeln (strg)
+                                  in  () end \<comment> \<open>important observation: thy is not modified.
+                                                  This implies that several text block can be 
+                                                  processed in parallel in a future, as long
+                                                  as they are associated to one meta arg.\<close>
+       
+       (* ... generating the level-attribute syntax *)
+  in   
+       (   Value_Command.Docitem_Parser.create_and_check_docitem 
+                              {is_monitor = false} {is_inline = false} {define = true}
+                              oid pos (cid_transform cid_pos) (attr_transform doc_attrs)
+        #> (fn thy => (app (check_n_tex_text thy) toks_list; thy))) 
+  end;
+
+val _ =
+  Outer_Syntax.command ("text-", @{here}) "formal comment macro"
+    (ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source 
+      >> (Toplevel.theory o (gen_enriched_document_command2 "TTT" {body=true} I I {markdown = true} )));
+
+(* copied from Pure_syn for experiments *)
+
+fun output_document2 state markdown txt =
+  let
+    val ctxt = Toplevel.presentation_context state;
+    val pos = Input.pos_of txt;
+    val _ =
+      Context_Position.reports ctxt
+        [(pos, Markup.language_document (Input.is_delimited txt)),
+         (pos, Markup.plain_text)];
+    val txt' = Document_Output.output_document ctxt markdown txt
+    val strg = XML.string_of (hd (Latex.output txt'))
+
+    val _ = writeln (strg)
+  in Document_Output.output_document ctxt markdown txt end;
+
+fun document_command2 markdown (loc, txt) =
+  Toplevel.keep (fn state =>
+                    (case loc of
+                      NONE => ignore (output_document2 state markdown txt)
+                    | SOME (_, pos) =>(ISA_core.err 
+                                           "Illegal target specification -- not a theory context" 
+                                           pos))) 
+ o 
+  Toplevel.present_local_theory loc                           
+                (fn state =>  (output_document2 state markdown txt));
+
+fun document_command3 markdown (loc, txt) trns = (document_command2 markdown (loc, txt) trns
+                                                  handle exn => ((writeln "AAA"); trns))
+
+fun gen_enriched_document_command3 assert name body cid_transform attr_transform markdown
+                                  (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
+                                     xstring_opt:(xstring * Position.T) option),
+                                    src_list:Input.source list) thy
+ = (gen_enriched_document_command2 name body cid_transform attr_transform markdown 
+                                  (((((oid,pos),cid_pos), doc_attrs), xstring_opt), src_list) 
+                                  thy)
+   handle ERROR msg => (if assert src_list msg then (writeln ("Correct error:"^msg^":reported.");thy)
+                                               else error"Wrong error reported")
+
+fun  error_match [_, src] msg = (writeln((Input.string_of src));
+                                 String.isPrefix (Input.string_of src) msg )
+   | error_match _ _ = error "Wrong text-assertion-error. Argument format <arg><match> required."
+
+
+val _ =
+  Outer_Syntax.command ("text-assert-error", @{here}) "formal comment macro"
+    (ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source 
+      >> (Toplevel.theory o (gen_enriched_document_command3 error_match "TTT" {body=true}
+                                                            I I {markdown = true}) 
+                            ));
+
+
+val _ =
+  Outer_Syntax.command ("text-latex", \<^here>) "formal comment (primary style)"
+    (Parse.opt_target -- Parse.document_source >> document_command2 {markdown = true});
+
+
+\<close>
+
+(* auto-tests *)
+text-latex\<open>dfg\<close>
+
+text-assert-error[aaaa::A]\<open> @{A \<open>sdf\<close>}\<close>\<open>reference ontologically inconsistent\<close>
+
+ML\<open>String.isPrefix "ab" "abc"\<close>
+
+end
+(*>*)