Enable high-level invariants checking everywhere

By default invariants checking generates warnings.
If invariants_strict_checking theory option is enabled,
the checking generates errors.

- Update 2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
  and 2020-iFM-CSP/paper.thy to pass the checking of
  the low level invariant checking function "check"
  in scholarly_paper.thy,
  which checks that the instances in a sequence of the same class
  have a growing level.
  For a sequence:
  section*[intro::introduction]‹ Introduction ›
  text*[introtext::introduction, level = "Some 1"]‹...›

  introtext must have a level >= than intro.

- Bypass the checking of high-level invariants
  when the class default_cid = "text",
  the top (default) document class.
  We want the class default_cid to stay abstract
  and not have the capability to be defined with attribute,
  invariants, etc.
  Hence this bypass handles docitem without a class associated,
  for example when you just want a document element to be referenceable
  without using the burden of ontology classes.
  ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close>

  The functions get_doc_class_global and get_doc_class_local trigger
  an error when the class is "text" (default_cid),
  then the functions like check_invariants which use it will fail
  if the checking is enabled by default for all the theories.

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy

@@ -74,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
@@ -123,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 
@@ -133,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:
@@ -162,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 
@@ -194,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>

examples/scholarly_paper/2020-iFM-CSP/paper.thy

@@ -52,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>. 
@@ -154,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>
@@ -354,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>  
@@ -530,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*[X22 ::math_content, level="Some 2"  ]\<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>
+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]\<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*[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"]\<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 
@@ -541,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*[X2, level="Some 2"]\<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*[X3, level="Some 2"]\<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*[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]\<open>\<open>DF A \<equiv> \<mu> X. (\<sqinter> 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]\<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*[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.
@@ -607,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 
@@ -630,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>
@@ -797,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>}
@@ -817,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>}

examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy

@@ -1041,10 +1041,11 @@ text\<open>
   Ontological classes as described so far are too liberal in many situations.
   There is a first high-level syntax implementation for class invariants.
   These invariants can be checked when an instance of the class is defined.
-  To enable the checking of the invariants, the \<^boxed_theory_text>\<open>invariants_checking\<close>
+  To enable the strict checking of the invariants,
+  the \<^boxed_theory_text>\<open>invariants_strict_checking\<close>
   theory attribute must be set:
   @{boxed_theory_text [display]\<open>
-  declare[[invariants_checking = true]]\<close>}
+  declare[[invariants_strict_checking = true]]\<close>}
 
   For example, let's define the following two classes:
   @{boxed_theory_text [display]\<open>
@@ -1104,6 +1105,12 @@ text\<open>
   All specified constraints are already checked in the IDE of \<^dof> while editing.
   The invariant \<^boxed_theory_text>\<open>author_finite\<close> enforces that the user sets the 
   \<^boxed_theory_text>\<open>authored_by\<close> set.
+  The invariants \<^theory_text>\<open>author_finite\<close> and \<^theory_text>\<open>establish_defined\<close> can not be checked directly
+  and need a little help.
+  We can set the \<open>invariants_checking_with_tactics\<close> theory attribute to help the checking.
+  It will enable a basic tactic, using unfold and auto:
+  @{boxed_theory_text [display]\<open>
+  declare[[invariants_checking_with_tactics = true]]\<close>}
   There are still some limitations with this high-level syntax.
   For now, the high-level syntax does not support  monitors (see \<^technical>\<open>sec:monitors\<close>).
   For example, one would like to delay a final error message till the

src/DOF/Isa_DOF.thy

@@ -813,8 +813,8 @@ fun print_doc_class_tree ctxt P T =
 val (strict_monitor_checking, strict_monitor_checking_setup)
      = Attrib.config_bool \<^binding>\<open>strict_monitor_checking\<close> (K false);
 
-val (invariants_checking, invariants_checking_setup) 
+val (invariants_strict_checking, invariants_strict_checking_setup) 
-     = Attrib.config_bool \<^binding>\<open>invariants_checking\<close> (K false);
+     = Attrib.config_bool \<^binding>\<open>invariants_strict_checking\<close> (K false);
 
 val (invariants_checking_with_tactics, invariants_checking_with_tactics_setup) 
      = Attrib.config_bool \<^binding>\<open>invariants_checking_with_tactics\<close> (K false);
@@ -825,7 +825,7 @@ end (* struct *)
 \<close>
 
 setup\<open>DOF_core.strict_monitor_checking_setup
-      #> DOF_core.invariants_checking_setup
+      #> DOF_core.invariants_strict_checking_setup
       #> DOF_core.invariants_checking_with_tactics_setup\<close>
 
 section\<open> Syntax for Term Annotation Antiquotations (TA)\<close>
@@ -948,6 +948,7 @@ structure ISA_core =
 struct
 
 fun err msg pos = error (msg ^ Position.here pos);
+fun warn msg pos = warning (msg ^ Position.here pos);
 
 fun check_path check_file ctxt dir (name, pos) =
   let
@@ -1600,11 +1601,12 @@ fun check_invariants thy oid =
       end
     fun check_invariants' ((inv_name, pos), term) =
       let val ctxt = Proof_Context.init_global thy
+          val trivial_true = \<^term>\<open>True\<close> |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
           val evaluated_term = value ctxt term
                 handle ERROR e =>
                   if (String.isSubstring "Wellsortedness error" e)
                       andalso (Config.get_global thy DOF_core.invariants_checking_with_tactics)
-                   then (warning("Invariants checking uses proof tactics");
+                  then (warning("Invariants checking uses proof tactics");
                          let val prop_term = HOLogic.mk_Trueprop term
                              val thms = Proof_Context.get_thms ctxt (inv_name ^ def_suffixN)
                              (* Get the make definition (def(1) of the record) *)
@@ -1614,22 +1616,37 @@ fun check_invariants thy oid =
                                                   (K ((unfold_tac ctxt thms') THEN (auto_tac ctxt)))
                                      |> Thm.close_derivation \<^here>
                                      handle ERROR e =>
-                                       ISA_core.err ("Invariant "
+                                       let
+                                         val msg_intro = "Invariant "
                                                       ^ inv_name
                                                       ^ " failed to be checked using proof tactics"
-                                                      ^ " with error: "
+                                                      ^ " with error:\n"
-                                                      ^ e) pos
+                                       in 
+                                         if Config.get_global thy DOF_core.invariants_strict_checking
+                                         then ISA_core.err (msg_intro ^ e) pos
+                                         else (ISA_core.warn (msg_intro ^ e) pos; trivial_true) end
                          (* If Goal.prove does not fail, then the evaluation is considered True,
                             else an error is triggered by Goal.prove *)
                          in @{term True} end)
-                   else ISA_core.err ("Fail to check invariant "
+                  else \<^term>\<open>True \<Longrightarrow> True\<close>
-                                      ^ inv_name
+      in case evaluated_term of
-                                      ^ ". Try to activate invariants_checking_with_tactics.") pos
+             \<^term>\<open>True\<close> => ((inv_name, pos), term)
-      in (if evaluated_term = \<^term>\<open>True\<close>
+           | \<^term>\<open>True \<Longrightarrow> True\<close> =>
-          then ((inv_name, pos), term)
+                let val msg_intro = "Fail to check invariant "
-          else ISA_core.err ("Invariant " ^ inv_name ^ " violated") pos)
+                                    ^ inv_name
+                                    ^ ".\nMaybe you can try "
+                                    ^ "to activate invariants_checking_with_tactics\n"
+                                    ^ "if your invariant is checked against doc_class algebraic "
+                                    ^ "types like 'doc_class list' or 'doc_class set'"
+                in if Config.get_global thy DOF_core.invariants_strict_checking
+                   then ISA_core.err (msg_intro) pos
+                   else (ISA_core.warn (msg_intro) pos; ((inv_name, pos), term)) end
+           | _ => let val msg_intro = "Invariant " ^ inv_name ^ " violated"
+                  in if Config.get_global thy DOF_core.invariants_strict_checking
+                     then ISA_core.err msg_intro pos
+                     else  (ISA_core.warn msg_intro pos; ((inv_name, pos), term)) end
       end
-    val _ = map check_invariants' inv_and_apply_list 
+    val _ = map check_invariants' inv_and_apply_list
   in thy end
 
 fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos doc_attrs thy = 
@@ -1639,20 +1656,19 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
     (* creates a markup label for this position and reports it to the PIDE framework;
      this label is used as jump-target for point-and-click feature. *)
     val cid_long = check_classref is_monitor cid_pos thy
+    val default_cid = cid_long = DOF_core.default_cid
     val vcid = case cid_pos of   NONE => NONE
                                | SOME (cid,_) => if (DOF_core.is_virtual cid thy)
                                                  then SOME (DOF_core.parse_cid_global thy cid)
                                                  else NONE
-    val value_terms = if (cid_long = DOF_core.default_cid)
+    val value_terms = if default_cid
                       then let
-                            val undefined_value = Free ("Undefined_Value", \<^Type>\<open>unit\<close>)
+                             val undefined_value = Free ("Undefined_Value", \<^Type>\<open>unit\<close>)
                            in (undefined_value, undefined_value) end
-                          (* 
+                            (* Handle initialization of docitem without a class associated,
-                             Handle initialization of docitem without a class associated,
+                               for example when you just want a document element to be referenceable
-                             for example when you just want a document element to be referenceable
+                               without using the burden of ontology classes.
-                             without using the burden of ontology classes.
+                               ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close> *)
-                             ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close>
-                          *)
                      else let
                             val defaults_init = create_default_object thy cid_long
                             fun conv (na, _(*ty*), term) =(Binding.name_of na, Binding.pos_of na, "=", term);
@@ -1684,9 +1700,15 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
                                o Context.Theory) thy; thy)
                        else thy)
          |> (fn thy => (check_inv thy; thy))
-         |> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
+         (* Bypass checking of high-level invariants when the class default_cid = "text",
-                       then check_invariants thy oid
+            the top (default) document class.
-                       else thy)
+            We want the class default_cid to stay abstract
+            and not have the capability to be defined with attribute, invariants, etc.
+            Hence this bypass handles docitem without a class associated,
+            for example when you just want a document element to be referenceable
+            without using the burden of ontology classes.
+            ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close> *)
+         |> (fn thy => if default_cid then thy else check_invariants thy oid)
   end
 
 end (* structure Docitem_Parser *)
@@ -1870,9 +1892,7 @@ fun update_instance_command  (((oid:string,pos),cid_pos),
             in     
                 thy |> DOF_core.update_value_global oid def_trans_input_term def_trans_value
                     |> check_inv
-                    |> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
+                    |> (fn thy => Value_Command.Docitem_Parser.check_invariants thy oid)
-                                  then Value_Command.Docitem_Parser.check_invariants thy oid
-                                  else thy)
             end
 
 
@@ -1932,9 +1952,7 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
     in  thy |> (fn thy => (check_lazy_inv thy; thy))
             |> update_instance_command args
             |> (fn thy => (check_inv thy; thy))
-            |> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
+            |> (fn thy => Value_Command.Docitem_Parser.check_invariants thy oid)
-                          then Value_Command.Docitem_Parser.check_invariants thy oid
-                          else thy)
             |> delete_monitor_entry
     end 
 

src/ontologies/scholarly_paper/scholarly_paper.thy

@@ -69,7 +69,7 @@ which we formalize into:\<close>
 doc_class text_section = text_element +
    main_author :: "author option"  <=  None
    fixme_list  :: "string list"    <=  "[]" 
-   level       :: "int  option"    <=  "None"   
+   level       :: "int  option"    <=  "None"
    (* this attribute enables doc-notation support section* etc.
       we follow LaTeX terminology on levels 
                 part          = Some -1

src/tests/High_Level_Syntax_Invariants.thy

@@ -12,7 +12,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>
 
@@ -144,6 +144,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