diff --git a/Isa_COL.thy b/Isa_COL.thy index 12a81fe..460d055 100644 --- a/Isa_COL.thy +++ b/Isa_COL.thy @@ -13,6 +13,9 @@ begin section\ Library of Standard Text Ontology \ + + + datatype placement = pl_h | pl_t | pl_b | pl_ht | pl_hb @@ -45,6 +48,19 @@ doc_class figure_group = (* dito the future monitor: table - block *) +text\ The attribute @{term "level"} in the subsequent enables doc-notation support section* etc. +we follow LaTeX terminology on levels +\<^enum> part = Some -1 +\<^enum> chapter = Some 0 +\<^enum> section = Some 1 +\<^enum> subsection = Some 2 +\<^enum> subsubsection = Some 3 +\<^enum> ... + +for scholarly paper: invariant level > 0 \ + +doc_class text_element = + level :: "int option" <= "None" section\Some attempt to model standardized links to Standard Isabelle Formal Content\ @@ -64,7 +80,7 @@ doc_class formal_content = doc_class concept = tag :: "string" <= "''''" - properties :: "thm list" + properties :: "thm list" <= "[]" section\Tests\ diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 554954a..5068f01 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -63,6 +63,45 @@ val docclass_markup = docref_markup_gen docclassN \ +section\String Utilities\ + +ML\ +fun spy x y = (writeln (x ^ y); y) + +fun markup2string x = XML.content_of (YXML.parse_body x) + +(* a hacky, but save encoding of unicode comming from the interface to the string format + that can be parsed by the inner-syntax string parser ''dfdf''. *) +fun bstring_to_holstring ctxt x (* (x:bstring) *) : string = + let val term = Syntax.parse_term ctxt (markup2string x) + fun hpp x = if x = #"\\" then "@" else + if x = #"@" then "@@" else String.implode [x] + in term |> Sledgehammer_Util.hackish_string_of_term ctxt + |> map hpp o String.explode |> String.concat + end; + + +fun chopper p (x:string) = + let fun hss buff [] = rev buff + |hss buff (S as a::R) = if p a then let val (front,rest) = take_prefix p S + in hss (String.implode front :: buff) rest end + else let val (front,rest) = take_prefix (not o p) S + in hss (String.implode front ::buff) rest end + in hss [] (String.explode x) end; + + +fun holstring_to_bstring ctxt (x:string) : bstring = + let fun collapse "" = "" + |collapse S = if String.sub(S,0) = #"@" + then let val n = String.size S + val front = replicate (n div 2) #"@" + val back = if (n mod 2)=1 then [#"\\"] else [] + in String.implode (front @ back) end + else S; + val t = String.concat (map collapse (chopper (fn x => x = #"@") x)); + in t |> Syntax.string_of_term ctxt o Syntax.parse_term ctxt end; + +\ section\ A HomeGrown Document Type Management (the ''Model'') \ @@ -401,17 +440,17 @@ fun declare_anoobject_local ctxt cid = end -fun get_object_global oid thy = let val {tab,...} = #docobj_tab(get_data_global thy) - in case Symtab.lookup tab oid of - NONE => error("undefined reference: "^oid) - |SOME(bbb) => bbb - end +fun get_object_global_opt oid thy = Symtab.lookup (#tab(#docobj_tab(get_data_global thy))) oid -fun get_object_local oid ctxt = let val {tab,...} = #docobj_tab(get_data ctxt) - in case Symtab.lookup tab oid of +fun get_object_global oid thy = case get_object_global_opt oid thy of + NONE => error("undefined reference: "^oid) + |SOME(bbb) => bbb + +fun get_object_local_opt oid ctxt = Symtab.lookup (#tab(#docobj_tab(get_data ctxt))) oid + +fun get_object_local oid ctxt = case get_object_local_opt oid ctxt of NONE => error("undefined reference: "^oid) |SOME(bbb) => bbb - end fun get_doc_class_global cid thy = if cid = default_cid then error("default doc class acces") (* TODO *) @@ -511,15 +550,15 @@ fun update_isa_global (isa, trans) thy = fun transduce_term_global (term,pos) thy = - (* pre: term should be fully typed in order to allow type-relqted term-transformations *) + (* pre: term should be fully typed in order to allow type-related term-transformations *) let val tab = #ISA_transformer_tab(get_data_global thy) fun T(Const(s,ty) $ t) = if String.isPrefix ISA_prefix s then case Symtab.lookup tab s of NONE => error("undefined inner syntax antiquotation: "^s) - | SOME(trans) => case trans thy (t,ty,pos) of + | SOME(trans) => (case trans thy (t,ty,pos) of NONE => Const(s,ty) $ t (* checking isa, may raise error though. *) - | SOME t => Const(s,ty) $ t + | SOME t => Const(s,ty) $ t) (* transforming isa *) else (Const(s,ty) $ (T t)) |T(t1 $ t2) = T(t1) $ T(t2) @@ -695,6 +734,7 @@ typedecl "thy" consts ISA_typ :: "string \ typ" ("@{typ _}") consts ISA_term :: "string \ term" ("@{term _}") +consts ISA_term_repr :: "string \ term" ("@{termrepr _}") consts ISA_thm :: "string \ thm" ("@{thm _}") consts ISA_file :: "string \ file" ("@{file _}") consts ISA_thy :: "string \ thy" ("@{thy _}") @@ -796,8 +836,9 @@ fun ML_isa_check_docitem thy (term, req_ty, pos) = (* utilities *) -fun property_list_dest X = map HOLogic.dest_string - (map (fn Const ("Isa_DOF.ISA_term", _) $ s => s ) +fun property_list_dest ctxt X = (map (fn Const ("Isa_DOF.ISA_term", _) $ s => HOLogic.dest_string s + |Const ("Isa_DOF.ISA_term_repr",_) $ s + => holstring_to_bstring ctxt (HOLogic.dest_string s)) (HOLogic.dest_list X)) end; (* struct *) @@ -805,11 +846,12 @@ end; (* struct *) \ subsection\ Isar - Setup\ -setup\DOF_core.update_isa_global("typ" ,ISA_core.ML_isa_check_typ) \ -setup\DOF_core.update_isa_global("term" ,ISA_core.ML_isa_check_term) \ -setup\DOF_core.update_isa_global("thm" ,ISA_core.ML_isa_check_thm) \ -setup\DOF_core.update_isa_global("file" ,ISA_core.ML_isa_check_file) \ -setup\DOF_core.update_isa_global("docitem",ISA_core.ML_isa_check_docitem)\ +setup\DOF_core.update_isa_global("typ" ,ISA_core.ML_isa_check_typ) \ +setup\DOF_core.update_isa_global("term" ,ISA_core.ML_isa_check_term) \ +setup\DOF_core.update_isa_global("term_repr",fn _ => fn (t,_,_) => SOME t) \ +setup\DOF_core.update_isa_global("thm" ,ISA_core.ML_isa_check_thm) \ +setup\DOF_core.update_isa_global("file" ,ISA_core.ML_isa_check_file) \ +setup\DOF_core.update_isa_global("docitem" ,ISA_core.ML_isa_check_docitem)\ section\ Syntax for Annotated Documentation Commands (the '' View'' Part I) \ @@ -830,10 +872,6 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) = | SOME(cid,_) => DOF_core.name2doc_class_name thy cid val cid_txt = "type = " ^ (enclose "{" "}" cid_long); - (* TODO: temp. hack *) - fun unquote_string s = if String.isPrefix "''" s then - String.substring(s,2,(String.size s)-4) - else s fun ltx_of_term _ (((Const ("List.list.Cons", t1) $ (Const ("String.Char", t2 ) $ t))) $ t') = (HOLogic.dest_string (((Const ("List.list.Cons", t1) $ (Const ("String.Char", t2 ) $ t))) $ t')) | ltx_of_term _ (@{term "numeral :: _ \ _"} $ t) = Int.toString(HOLogic.dest_numeral t) @@ -951,8 +989,7 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t fun instantiate_term S t = Term_Subst.map_types_same (Term_Subst.instantiateT S) (t) fun read_assn (lhs, pos:Position.T, opr, rhs) term = - let val info_opt = DOF_core.get_attribute_info cid_long - (Long_Name.base_name lhs) thy + let val info_opt = DOF_core.get_attribute_info cid_long (Long_Name.base_name lhs) thy val (ln,lnt,lnu,lnut) = case info_opt of NONE => error ("unknown attribute >" ^((Long_Name.base_name lhs)) @@ -962,9 +999,9 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) (typ --> typ) --> cid_ty --> cid_ty) val tyenv = Sign.typ_match thy ((generalize_typ 0)(type_of rhs), lnt) (Vartab.empty) - handle Type.TYPE_MATCH => error ("type of attribute: " ^ ln + handle Type.TYPE_MATCH => (error ("type of attribute: " ^ ln ^ " does not fit to term: " - ^ toString rhs); + ^ toString rhs)); val tyenv' = (map (fn (s,(t,u)) => ((s,t),u)) (Vartab.dest tyenv)) val _ = if Long_Name.base_name lhs = lhs orelse ln = lhs then () else error("illegal notation for attribute of "^cid_long) @@ -1019,7 +1056,6 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy = end in (moid,map check_for_cid indexed_autoS) end val enabled_monitors = List.mapPartial is_enabled (Symtab.dest monitor_tab) - fun markup2string x = XML.content_of (YXML.parse_body x) fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn, Syntax.read_term_global thy rhs) val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")] @@ -1058,7 +1094,6 @@ fun create_and_check_docitem is_monitor oid pos cid_pos doc_attrs thy = fun conv (na, _(*ty*), term) = (Binding.name_of na, Binding.pos_of na, "=", term); val S = map conv (DOF_core.get_attribute_defaults cid_long thy); val (defaults, _(*ty*), _) = calc_update_term thy cid_long S defaults_init; - fun markup2string x = XML.content_of (YXML.parse_body x) fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs) val assns' = map conv_attrs doc_attrs val (value_term, _(*ty*), _) = calc_update_term thy cid_long assns' defaults @@ -1089,14 +1124,14 @@ fun update_instance_command (((oid:string,pos),cid_pos), val _ = if cid_long = DOF_core.default_cid orelse cid = cid_long then () else error("incompatible classes:"^cid^":"^cid_long) - fun markup2string x = XML.content_of (YXML.parse_body x) - fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn, + fun conv_attrs (((lhs, pos), opn), rhs) = ((markup2string lhs),pos,opn, Syntax.read_term_global thy rhs) val assns' = map conv_attrs doc_attrs - val def_trans = #1 o (calc_update_term thy cid_long assns') + val def_trans = (#1 o (calc_update_term thy cid_long assns')) fun check_inv thy =((DOF_core.get_class_invariant cid_long thy oid {is_monitor=false} - o Context.Theory ) thy ; thy) + o Context.Theory ) thy ; + thy) in thy |> DOF_core.update_value_global oid (def_trans) |> check_inv @@ -1158,7 +1193,8 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos), let val {monitor_tab,...} = DOF_core.get_data_global thy fun check_if_final aS = let val i = find_index (not o RegExpInterface.final) aS in if i >= 0 - then error("monitor number "^Int.toString i^" not in final state.") + then msg thy ("monitor number "^Int.toString i^ + " not in final state.") else () end val _ = case Symtab.lookup monitor_tab oid of @@ -1283,30 +1319,21 @@ val _ = (attributes_upd >> (Toplevel.theory o update_instance_command)); -fun assert_cmd'((((((oid,pos),cid_pos),doc_attrs),some_name:string option),modes : string list), +fun assert_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list), prop) = - let fun markup2string x = XML.content_of (YXML.parse_body x) - fun parse_convert thy = (let val ctxt = (Proof_Context.init_global thy) - val term = Syntax.parse_term ctxt prop - val str = Sledgehammer_Util.hackish_string_of_term ctxt term - fun hpp x = if x = #"\\" then "\\\\" else String.implode [x] - val str' = map hpp (String.explode str) - val str'' = String.concatWith " " str' - in str'' - end) - val _ = writeln ("XXX" ^ markup2string prop) - fun conv_attrs thy = (("property",pos),"[@{term ''"^markup2string prop ^"''}]")::doc_attrs + let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy)) + fun conv_attrs thy = (("property",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]") + ::doc_attrs (* fun conv_attrs thy = (("property",pos),"[@{term ''"^parse_convert thy ^"''}]")::doc_attrs *) fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy) - fun mks thy = case DOF_core.get_object_global oid thy of - SOME _ => (writeln "SOME"; update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy) - | NONE => (writeln "NONE"; create_and_check_docitem false oid pos cid_pos (conv_attrs thy) thy) - val check = (assert_cmd some_name modes prop) o Proof_Context.init_global + fun mks thy = case DOF_core.get_object_global_opt oid thy of + SOME NONE => (error("update of declared but not created doc_item:" ^ oid)) + | SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy) + | NONE => (create_and_check_docitem false oid pos cid_pos (conv_attrs thy) thy) + val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global in (* Toplevel.keep (check o Toplevel.context_of) *) - Toplevel.theory (fn thy => (check thy; - (* writeln ("YYY" ^ parse_convert thy); *) - mks thy)) + Toplevel.theory (fn thy => (check thy; mks thy)) end val _ = @@ -1680,6 +1707,17 @@ writeln (DOF_core.toStringDocItemRef "scholarly_paper.introduction" "XX" []); \ *) -lemma X : "True" oops + +ML\ + +\ +(* +ML\ +val h = bstring_to_holstring @{context} (Syntax.string_of_term @{context} @{term "A \ A"}); +holstring_to_bstring @{context} h +\ +*) + + end diff --git a/examples/cenelec/mini_odo/mini_odo.thy b/examples/cenelec/mini_odo/mini_odo.thy index d2a6759..12dd136 100644 --- a/examples/cenelec/mini_odo/mini_odo.thy +++ b/examples/cenelec/mini_odo/mini_odo.thy @@ -37,7 +37,7 @@ text\A real example fragment from a larger project, declaring a text-eleme text*[new_ass::hypothesis]\Under the assumption @{assumption \ass1\} we establish the following: ... \ -text*[ass122::srac] \ The overall sampling frequence of the odometer +text*[ass122::SRAC] \ The overall sampling frequence of the odometer subsystem is therefore 14 khz, which includes sampling, computing and result communication times... \ @@ -54,7 +54,7 @@ text \ As established by @{docref (unchecked) \t10\}, text \ the @{docref \t10\} as well as the @{docref \ass122\}\ text \ represent a justification of the safety related applicability - condition @{srac \ass122\} aka exported constraint @{ec \ass122\}.\ + condition @{SRAC \ass122\} aka exported constraint @{EC \ass122\}.\ @@ -65,11 +65,8 @@ declare_reference* [lalala::requirement, alpha="main", beta=42] declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1] - - - -section*[h::example]\ Some global inspection commands for the status of docitem and doc-class tables ... \ - +section*[h::example]\ Some global inspection commands for the status of docitem and + doc-class tables ... \ section*[i::example]\ Text Antiquotation Infrastructure ... \ @@ -79,7 +76,7 @@ text\ @{docitem (unchecked) \lalala\} -- produces no warning. text\ @{docitem \ass122\} -- global reference to a text-item in another file. \ -text\ @{ec \ass122\} -- global reference to a exported constraint in another file. +text\ @{EC \ass122\} -- global reference to a exported constraint in another file. Note that the link is actually a srac, which, according to the ontology, happens to be an "ec". \ diff --git a/examples/conceptual/AssnsLemmaThmEtc.thy b/examples/conceptual/AssnsLemmaThmEtc.thy index 0d351da..57a64ea 100644 --- a/examples/conceptual/AssnsLemmaThmEtc.thy +++ b/examples/conceptual/AssnsLemmaThmEtc.thy @@ -16,18 +16,37 @@ section\Definitions, Lemmas, Theorems, Assertions\ text*[aa::F, property = "[@{term ''True''}]"]\Our definition of the HOL-Logic has the following properties:\ assert*[aa::F] "True" -ML\ ISA_core.property_list_dest @{docitem_attribute property :: aa}\ -assert*[aa::F] "True --> True" (* small pb: unicodes crashes here ... *) +(* sample for accessing a property filled with previous assert's of "aa" *) +ML\ ISA_core.property_list_dest @{context} @{docitem_attribute property :: aa};\ + +assert*[aa::F] " X \ Y \ True" (*example with uni-code *) +ML\ ISA_core.property_list_dest @{context} @{docitem_attribute property :: aa}; + app writeln (tl (rev it));\ + +assert*[aa::F] "\x::bool. X \ Y \ True" (*problem with uni-code *) + +ML\ +Syntax.read_term_global @{theory} "[@{termrepr ''True @ True''}]"; +(* this only works because the isa check is not activated in "term" !!! *) +@{term "[@{term '' True @ True ''}]"}; (* with isa-check *) +@{term "[@{termrepr '' True @ True ''}]"}; (* without isa check *) +\ + +ML\val [_,_,Const _ $ s,_] = (HOLogic.dest_list @{docitem_attribute property :: aa}); +val t = HOLogic.dest_string s; +holstring_to_bstring @{context} t +\ + +lemma "All (\x. X \ Y \ True)" oops -ML\ ISA_core.property_list_dest @{docitem_attribute property :: aa}\ text\An example for the ontology specification character of the short-cuts such as @{command "assert*"}: in the following, we use the same notation referring to a completely different class. "F" and "assertion" have only in common that they posses the attribute \<^verbatim>\property\: \ -text*[aaa::assertion]\Our definition of the integers has the following properties:\ +text\Creation just like that: \ assert*[aaa::assertion] "3 < (4::int)" assert*[aaa::assertion] "0 < (4::int)" diff --git a/examples/simple/Concept_Example.thy b/examples/simple/Concept_Example.thy index e12e7e2..2e609d5 100644 --- a/examples/simple/Concept_Example.thy +++ b/examples/simple/Concept_Example.thy @@ -14,7 +14,7 @@ section*[a::A, x = "3"] \ Lorem ipsum dolor sit amet, ... \ text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \ text*[d::D, a1 = "X3"] \ ... phasellus amet id massa nunc, pede suscipit repellendus, - ... @{docitem \c1\} @{thm "refl"}\ + ... @{C \c1\} @{thm "refl"}\ update_instance*[d::D, a1 := X2] diff --git a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy index 21a207a..6520b25 100644 --- a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy @@ -1053,8 +1053,77 @@ fun output ctxt prts = *) \ -chapter\Front End \ -text\Introduction ... TODO\ +chapter\Front-End \ +text\In the following chapter, we turn to the right part of the system architecture +shown in @{docitem \architecture\}: +The PIDE ("Prover-IDE") layer consisting of a part written in SML and another in SCALA. +Roughly speaking, PIDE implements "continuous build - continuous check" - functionality +over a textual, albeit generic document model. It transforms user modifications +of text elements in an instance of this model into increments (edits) and communicates +them to the Isabelle system. The latter reacts by the creation of a multitude of light-weight +reevaluation threads resulting in an asynchronous stream of markup that is used to annotate text +elements. Such markup is used to highlight, e.g., variables +or keywords with specific colors, to hyper-linking bound variables to their defining occurrences, +or to annotate type-information to terms which becomes displayed by specific +user-gestures on demand (hovering), etc. +Note that PIDE is not an editor, it is the framework that +coordinates these asynchronous information streams and optimizes it to a certain +extent (outdated markup referring to modified text is dropped, and +corresponding re-calculations are oriented to the user focus, for example). +Four concrete editors --- also called PIDE applications --- have been implemented: +\<^enum>an Eclipse plugin (developped by an Edinburg-group, based on an very old PIDE version), +\<^enum>a Visual-Studio Code plugin (developed by Makarius Wenzel), + currently based on a fairly old PIDE version, +\<^enum>clide, a web-client supporting javascript and HTML5 + (developed by a group at University Bremen, based on a very old PIDE version), and +\<^enum>the most commonly used: the plugin in JEdit - Editor, + (developed by Makarius Wenzel, current PIDE version.) +\ + +text\The document model forsees a number of text files, which are organized in form of an acyclic graph. Such graphs can be +grouped into \<^emph>\sessions\ and "frozen" to binaries in order to avoid long compilation +times. Text files have an abstract name serving as identity (the mapping to file-paths +in an underlying file-system is done in an own build management). +The primary format of the text files is \<^verbatim>\.thy\ (historically for: theory), +secondary formats can be \<^verbatim>\.sty\,\<^verbatim>\.tex\, \<^verbatim>\.png\, \<^verbatim>\.pdf\, or other files processed +by Isabelle and listed in a configuration processed by the build system. +\ +figure*[fig3::figure, relative_width="100",src="''figures/document-model''"] + \A Theory-Graph in the Document Model\ +text\A \<^verbatim>\.thy\ file consists of a \<^emph>\header\, a \<^emph>\context-definition\ and +a \<^emph>\body\ consisting of a sequence of \<^emph>\commands\. Even the header consists of +a sequence of commands used for introductory text elements not depending on any context +information (so: practically excluding any form of text antiquotation (see above)). +The context-definition contains an \<^emph>\import\ and a \<^emph>\keyword\ section; +for example: +\begin{verbatim} +theory Isa_DOF (* Isabelle Document Ontology Framework *) + imports Main + RegExpInterface (* Interface to functional regular automata for monitoring *) + Assert + + keywords "+=" ":=" "accepts" "rejects" +\end{verbatim} +where \<^verbatim>\Isa_DOF\ is the abstract name of the text-file, \<^verbatim>\Main\ etc. refer to imported +text files (recall that the import relation must be acyclic). \<^emph>\keyword\s are used to separate +commands form each other; +predefined commands allow for the dynamic creation of new commands similarly +to the definition of new functions in an interpreter shell (or: toplevel, see above.). +A command starts with a pre-declared keyword and specific syntax of this command; +the declaration of a keyword is only allowed in the same \<^verbatim>\.thy\-file where the +the corresponding new command is defined. The semantics of the command is expressed +in ML and consists of a @{ML_type "Toplevel.transition -> Toplevel.transition"} +function. Thus, the Isar-toplevel supports the generic document model +and allows for user-programmed extensions. +\ + +text\Isabelle \<^verbatim>\.thy\-files were processed by two types of parsers: +\<^enum> the "outer-syntax" (i.e. the syntax for commands) is processed + by a lexer-library and parser combinators built on top, and +\<^enum> the "inner-syntax" (i.e. the syntax for @{term \\\} - terms) + with an evolved, eight-layer parsing and pretty-printing process. +\ + section\Basics: string, bstring and xstring\ text\@{ML_type "string"} is the basic library type from the SML library @@ -1063,12 +1132,12 @@ or require formats thereof introduced as type synonyms @{ML_type "bstring"} (defined in structure @{ML_structure "Binding"} and @{ML_type "xstring"} (defined in structure @{ML_structure "Name_Space"}. Unfortunately, the abstraction is not tight and combinations with -elementary routines might produce quire crappy results. +elementary routines might produce quite crappy results. \ ML\val b = Binding.name_of@{binding "here"}\ text\... produces the system output \verb+val it = "here": bstring+, - but note that it is trappy to believe it is just a string. + but note that it is misleading to believe it is just a string. \ ML\String.explode b\ (* is harmless, but *) diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT index ce596f7..bf9d816 100644 --- a/examples/technical_report/TR_my_commented_isabelle/ROOT +++ b/examples/technical_report/TR_my_commented_isabelle/ROOT @@ -11,4 +11,6 @@ session "TR_mycommentedisabelle" = "Isabelle_DOF" + "figures/isabelle-architecture.pdf" "figures/pure-inferences-I.pdf" "figures/pure-inferences-II.pdf" + "figures/document-model.pdf" + diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf new file mode 100644 index 0000000..55e99a8 Binary files /dev/null and b/examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf differ diff --git a/ontologies/CENELEC_50128.thy b/ontologies/CENELEC_50128.thy index 0b2b846..b9a6ef4 100644 --- a/ontologies/CENELEC_50128.thy +++ b/ontologies/CENELEC_50128.thy @@ -28,7 +28,7 @@ Safety assessment is focused on but not limited to the safety properties of a sy Definition*[assessor::concept, tag="''assessor''"] \entity that carries out an assessment\ -Definition*[cots::concept, tag="''commercial off-the-shelf (COTS) software''"] +Definition*[COTS::concept, tag="''commercial off-the-shelf software''"] \software defined by market-driven need, commercially available and whose fitness for purpose has been demonstrated by a broad spectrum of commercial users\ @@ -44,7 +44,7 @@ criteria: (e. g. subsystems) which have an independent version \ -Definition*[cmgr::concept, tag="''configuration manager''"] +Definition*[CMGR::concept, tag="''configuration manager''"] \entity that is responsible for implementing and carrying out the processes for the configuration management of documents, software and related tools including \<^emph>\change management\\ @@ -71,7 +71,7 @@ from the intended performance or behaviour (cf @{concept \error\})\ Definition*[failure::concept] \unacceptable difference between required and observed performance\ -Definition*[ft::concept, tag="''fault tolerance''"] +Definition*[FT::concept, tag="''fault tolerance''"] \built-in capability of a system to provide continued correct provision of service as specified, in the presence of a limited number of hardware or software faults\ @@ -79,7 +79,7 @@ Definition*[firmware::concept] \software stored in read-only memory or in semi-permanent storage such as flash memory, in a way that is functionally independent of applicative software\ -Definition*[gen_soft::concept,tag="''generic software''"] +Definition*[GS::concept,tag="''generic software''"] \software which can be used for a variety of installations purely by the provision of application-specific data and/or algorithms\ @@ -231,27 +231,33 @@ NOTE Verification is mostly based on document reviews (design, implementation, t Definition*[verifier::concept] \entity that is responsible for one or more verification activities\ +section\Organization, Roles and Responsabilities\ +text\see also section \<^emph>\Software management and organization\.\ datatype role = PM (* Program Manager *) | RQM (* Requirements Manager *) | DES (* Designer *) | IMP (* Implementer *) | ASR (* Assessor *) - | Ne (* Integrator *) + | INT (* Integrator *) | TST (* Tester *) | VER (* Verifier *) + | VnV (* Verification and Validation *) | VAL (* Validator *) -datatype phase = SR (* Software Requirement *) - | SA (* Software Architecture *) - | SDES (* Software Design *) - | SCDES (* Software Component Design *) - | CInT (* Component Implementation and Testing *) - | SI (* Software Integration *) - | SV (* Software Validation *) - | SD (* Software Deployment *) - | SM (* Software Maintenance *) + +datatype phase = SYSDEV_ext (* System Development Phase (external) *) + | SPl (* Software Planning *) + | SR (* Software Requirement *) + | SA (* Software Architecture *) + | SDES (* Software Design *) + | SCDES (* Software Component Design *) + | CInT (* Component Implementation and Testing *) + | SI (* Software Integration *) + | SV (* Software Validation *) + | SD (* Software Deployment *) + | SM (* Software Maintenance *) abbreviation software_requirement :: "phase" where "software_requirement \ SR" abbreviation software_architecture :: "phase" where "software_architecture \ SA" @@ -264,24 +270,30 @@ abbreviation software_validation :: "phase" where "software_validation \ SD" abbreviation software_maintenance :: "phase" where "software_maintenance \ SM" -term "SR" +term "SR" (* meta-test *) + + +section\Objectives, Conformance and Software Integrity Levels\ + +datatype sil = SIL0 | SIL1 | SIL2 | SIL3 | SIL4 + +type_synonym saftety_integraytion_level = sil + doc_class objectives = long_name :: "string option" is_concerned :: "role set" -section\ Requirements-Analysis related Categories \ - -doc_class requirement = +doc_class requirement = text_element + long_name :: "string option" is_concerned :: "role set" - +(* doc_class requirement_analysis = no :: "nat" accepts "\requirement\\<^sup>+" - +*) text\The category @{emph \hypothesis\} is used for assumptions from the foundational mathematical or physical domain, so for example: @@ -304,12 +316,21 @@ doc_class hypothesis = requirement + text\ The following sub-class of security related hypothesis might comprise, for example: \<^item> @{term "P \ NP"}, \<^item> or the computational hardness of certain functions - relevant for cryptography (like prime-factorization).\ + relevant for cryptography (like prime-factorization). + (* speculation bu, not 50128 *)\ doc_class security_hyp = hypothesis + hyp_type :: hyp_type <= physical (* default *) +doc_class FnI = requirement + + is_concerned :: "role set" <= "UNIV" + type_synonym functions_and_interfaces = FnI + +doc_class AC = requirement + + is_concerned :: "role set" <= "UNIV" + type_synonym application_conditions = AC + text\The category \<^emph>\assumption\ is used for domain-specific assumptions. It has formal, semi-formal and informal sub-categories. They have to be tracked and discharged by appropriate validation procedures within a certification process, by it by test or proof. \ @@ -319,24 +340,282 @@ datatype ass_kind = informal | semiformal | formal doc_class assumption = requirement + assumption_kind :: ass_kind <= informal -text\ The category \<^emph>\exported constraint\ (or \<^emph>\ec\ for short) is used for formal assumptions, ... \ +text\ The category \<^emph>\exported constraint\ (or \<^emph>\EC\ for short) is used for formal application +conditions; They represent in particular \<^emph>\derived constraints\, i.e. constraints that arrive +as side-conditions during refinement proofs or implementation decisions and must be tracked.\ -doc_class ec = assumption + +doc_class EC = AC + assumption_kind :: ass_kind <= (*default *) formal + type_synonym exported_constraint = EC -text\ The category \<^emph>\safety related application condition\ (or \<^emph>\srac\ for short) is used ... \ +text\ The category \<^emph>\safety related application condition\ (or \<^emph>\SRAC\ for short) is used +for exported constraints assuring in judgements safety requirements of the system. \ -doc_class srac = ec + +doc_class SRAC = EC + assumption_kind :: ass_kind <= (*default *) formal + type_synonym safety_related_application_condition = SRAC -doc_class timing = ec + - assumption_kind :: ass_kind <= (*default *) formal -doc_class energy = ec + - assumption_kind :: ass_kind <= (*default *) formal +doc_class CoAS = requirement + + is_concerned :: "role set" <= "UNIV" + type_synonym configuration_or_architecture_of_system = CoAS -doc_class security = ec + - assumption_kind :: ass_kind <= (*default *) formal +doc_class HtbC = requirement + + is_concerned :: "role set" <= "UNIV" + type_synonym hazard_to_be_controlled = HtbC + +doc_class SIR = requirement + + is_concerned :: "role set" <= "UNIV" + type_synonym safety_integrity_requirement = SIR + +text\The following class is a bit unclear about usage and seems to be in +conceptual mismatch with @{typ objectives}: \ +doc_class SILA = requirement + + is_concerned :: "role set" <= "UNIV" + alloc :: "sil" <= "SIL0" + type_synonym allocation_of_SIL = SILA + +doc_class TC = requirement + + is_concerned :: "role set" <= "UNIV" + type_synonym timing_constraint = TC + +section\Software Assurance related Entities and Concepts\ + + +text{* subcategories are : *} +text\Table A.5: Verification and Testing\ +datatype vnt_technique = + formal_proof + | stat_analysis + | dyn_analysis (* Refinedin Table A.13: + -- Test Case Execution from Boundary Analysis + -- Test Case Execution from Error Guessing + -- Test Case Execution from Error Seeding + -- Performance Modeling + -- Equivalence Classes and Input Partition Testing + -- Structure-Based Testing + *) + | metrics + | traceability + | sw_error_effect_analysis + | test_coverage_for_code + | functional_testing + (* Refined in Table A.14: + -- Test Case Execution from Cause Consequence Diagrams + -- Prototyping / Animation + -- Boundary Value Analysis + -- Equivalence Classes and Input Partition Testing + -- Process Simulation + *) + | perf_testing + | interface_testing + | model_based_testing (* 'modeling' unclear *) + +type_synonym verification_and_testing_technique = vnt_technique + +datatype test_coverage_criterion = + allpathk nat nat (* depth, test_coverage_degree *) + | mcdc nat (* depth, test_coverage_degree *) + | exhaustive + | dnf_E_d string nat (* equivalence class testing *) + | other string + +text\The objective of software verification is to examine and arrive at a \<^emph>\judgement\ based on +\<^emph>\evidence\ that output items (process, documentation, software or application) of a specific +development phase fulfil the requirements and plans with respect to completeness, correctness +and consistency. \ +doc_class judgement = + evidence :: "vnt_technique list" + is_concerned :: "role set" <= "{VER,ASR,VAL}" + +section\ Design and Test Documents \ + +doc_class cenelec_text = text_element + + phase :: "phase" + is_concerned :: "role set" <= "UNIV" + + + +doc_class SYSREQS = cenelec_text + + phase :: "phase" <= "SYSDEV_ext" + accepts "\objectives||requirement||cenelec_text\\<^sup>+ " + type_synonym system_requirements_specification = SYSREQS + +doc_class SYSSREQS = cenelec_text + + phase :: "phase" <= "SYSDEV_ext" + type_synonym system_safety_requirements_specification = SYSSREQS + +doc_class SYSAD = cenelec_text + + phase :: "phase" <= "SYSDEV_ext" + type_synonym system_architecture_description = SYSAD + +doc_class SYSS_pl = cenelec_text + + phase :: "phase" <= "SPl" + type_synonym system_safety_plan = SYSS_pl + +doc_class SYS_VnV_pl = cenelec_text + + phase :: "phase" <= "SPl" + type_synonym system_VnV_plan = SYS_VnV_pl + +doc_class SWRS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_requirements_specification = SWRS + +doc_class SWRVR = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_requirements_verification_report = SWRVR + + +doc_class SWTS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_test_specification = SWTS + +doc_class SWAS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_architecture_specification = SWAS + +doc_class SWDS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_design_specification = SWDS + +doc_class SWIS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_interface_specification = SWIS + +doc_class SWITS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_integration_test_specification = SWITS + +doc_class SWHITS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_hardware_integration_test_specification = SWHITS + +doc_class SWADVR = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_architecture_and_design_verification_report = SWADVR + +doc_class SWCDS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_component_design_specification = SWCDS + +doc_class SWCTS = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_component_test_specification = SWCTS + +doc_class SWCDVR = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_component_design_verification_report = SWCDVR + + +doc_class SWSCD = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_source_code_and_documentation = SWSCD + +doc_class SWCTR = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_component_test_report = SWCTR + +doc_class SWSCVR = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_source_code_verification_report = SWSCVR + +doc_class SWHAITR = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_hardware_integration_test_report = SWHAITR + +doc_class SWIVR = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_integration_verification_report = SWIVR + +doc_class SWTR_global = cenelec_text + + phase :: "phase" <= "SD" + type_synonym overall_software_test_report = SWTR_global + +doc_class SWVALR = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_validation_report = SWVALR + +doc_class SWDD = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_deployment_documents = SWDD + +doc_class SWMD = cenelec_text + + phase :: "phase" <= "SD" + type_synonym software_maintenance_documents = SWMD + + +section\ Software Assurance \ + +subsection\ Software Testing \ +text\Objective: +The objective of software testing, as performed by the Tester and/or Integrator, +is to ascertain the behaviour or performance of software against the corresponding test +specification to the extent achievable by the selected test coverage. +\ + +text\Outputs: +\<^enum> @{typ overall_software_test_report} +\<^enum> @{typ software_test_specification} Overall Software Test Specification +\<^enum> Overall Software Test Report +\<^enum> Software Integration Test Specification +\<^enum> Software Integration Test Report +\<^enum> Software/Hardware Integration Test Specification +\<^enum> Software/Hardware Integration Test Report +\<^enum> Software Component Test Specification +\<^enum> Software Component Test Report +\ + +subsection\ Software Verification \ +text\Objective: +The objective of software verification is to examine and arrive at a judgement based on evidence +that output items (process, documentation, software or application) of a specific development +phase fulfil the requirements and plans with respect to completeness, correctness and consistency. +These activities are managed by the @{concept \verifier\}. +\ + +text\Outputs: +\<^enum> Software Verification Plan +\<^enum> Software Verification Report(s) +\<^enum> Software Quality Assurance Verification Report +\ + +subsection\ Software Validation \ +text\Objective: +\<^enum>The objective of software validation is to demonstrate that the processes and their outputs are +such that the software is of the defined software safety integrity level, fulfils the software +requirements and is fit for its intended application. This activity is performed by the Validator. +\<^enum>The main validation activities are to demonstrate by analysis and/or testing that all the software +requirements are specified, implemented, tested and fulfilled as required by the applicable SIL, +and to evaluate the safety criticality of all anomalies and non-conformities based on the results +of reviews, analyses and tests. +\ +text\Output documents: +\<^enum> Software Validation Plan +\<^enum> Software Validation Report +\<^enum> Software Validation Verification Report +\ + +subsection\ Software Assessment \ (* other word for : formal evaluation. *) +text\Objective: +\<^enum>To evaluate that the lifecycle processes and their outputs are such that the software is of the +defined software safety integrity levels 1-4 andis fit for its intended application. +\<^enum> For SIL 0 software, requirements of this standard shall be fulfilled but where a certificate stating +compliance with EN ISO 9001 is available, no assessment will be required. +\ + +subsection\ Software Quality Assurance \ +text\Objectives: To identify, monitor and control all those activities, both technical and +managerial, which are necessary to ensure that the software achieves the quality required. +This is necessary to provide the required qualitative defence against systematic faults and +to ensure that an audit trail can be established to allow +verification and validation activities to be undertaken effectively.\ +(* So : pretty much META *) + + + + + +(* DEATH ZONE FROM HERE ... >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> *) section\ Design related Categories \ @@ -354,23 +633,11 @@ section\ Requirements-Analysis related Categories \ doc_class test_item = nn :: "string option" - -text{* subcategories are : *} - -datatype test_kind = blackbox | whitebox | greybox | fuzz | pertubation - -datatype test_coverage_criterion = - allpathk nat nat (* depth, test_coverage_degree *) - | mcdc nat (* depth, test_coverage_degree *) - | exhaustive - | dnf_E_d string nat (* equivalence class testing *) - | other string doc_class test_specification = test_item + short_goal :: string doc_class test_case = test_item + - kind :: test_kind descr :: string doc_class test_result = test_item + @@ -403,21 +670,22 @@ doc_class test_documentation = -section\ Testing and Validation \ +section\ META : Testing and Validation \ -text\Test : @{concept \cots\}\ + +text\Test : @{concept \COTS\}\ ML\ DOF_core.name2doc_class_name @{theory} "requirement"; -DOF_core.name2doc_class_name @{theory} "srac"; -DOF_core.is_defined_cid_global "srac" @{theory}; -DOF_core.is_defined_cid_global "ec" @{theory}; +DOF_core.name2doc_class_name @{theory} "SRAC"; +DOF_core.is_defined_cid_global "SRAC" @{theory}; +DOF_core.is_defined_cid_global "EC" @{theory}; "XXXXXXXXXXXXXXXXX"; -DOF_core.is_subclass @{context} "CENELEC_50128.ec" "CENELEC_50128.ec"; -DOF_core.is_subclass @{context} "CENELEC_50128.srac" "CENELEC_50128.ec"; -DOF_core.is_subclass @{context} "CENELEC_50128.ec" "CENELEC_50128.srac"; -DOF_core.is_subclass @{context} "CENELEC_50128.ec" "CENELEC_50128.test_requirement"; +DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.EC"; +DOF_core.is_subclass @{context} "CENELEC_50128.SRAC" "CENELEC_50128.EC"; +DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.SRAC"; +DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.test_requirement"; "XXXXXXXXXXXXXXXXX"; val {docobj_tab={maxano, tab=ref_tab},docclass_tab=class_tab,...} = DOF_core.get_data @{context}; Symtab.dest ref_tab; @@ -428,7 +696,7 @@ Symtab.dest class_tab; ML\ "XXXXXXXXXXXXXXXXX"; -DOF_core.get_attributes_local "srac" @{context}; +DOF_core.get_attributes_local "SRAC" @{context}; @{term assumption_kind} \ diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy index 8e2738b..eb125e0 100644 --- a/ontologies/scholarly_paper.thy +++ b/ontologies/scholarly_paper.thy @@ -22,18 +22,18 @@ doc_class abstract = keywordlist :: "string list" <= "[]" principal_theorems :: "thm list" -doc_class text_section = +doc_class text_section = text_element + main_author :: "author option" <= None fixme_list :: "string list" <= "[]" level :: "int option" <= "None" - (* this attribute enables doc-notation support section* etc. - we follow LaTeX terminology on levels - part = Some -1 - chapter = Some 0 - section = Some 1 - subsection = Some 2 - subsubsection = Some 3 - ... *) + (* this attribute enables doc-notation support section* etc. + we follow LaTeX terminology on levels + part = Some -1 + chapter = Some 0 + section = Some 1 + subsection = Some 2 + subsubsection = Some 3 + ... *) (* for scholarly paper: invariant level > 0 *) doc_class introduction = text_section + diff --git a/ontologies/small_math.thy b/ontologies/small_math.thy new file mode 100644 index 0000000..c9b6705 --- /dev/null +++ b/ontologies/small_math.thy @@ -0,0 +1,150 @@ +section{* An example ontology for a math paper*} + +theory small_math + imports "../Isa_COL" +begin + +doc_class title = + short_title :: "string option" <= "None" + +doc_class author = + email :: "string" <= "''''" + +datatype classification = algebra | geometry | graph_theory + +doc_class abstract = + keyword_list :: "classification list" <= "[]" + +doc_class text_section = + authored_by :: "author set" <= "{}" + level :: "int option" <= "None" + (* this attribute enables doc-notation support section* etc. + we follow LaTeX terminology on levels + part = Some -1 + chapter = Some 0 + section = Some 1 + subsection = Some 2 + subsubsection = Some 3 + ... *) + (* for scholarly paper: invariant level > 0 *) + +type_synonym notion = string + +doc_class introduction = text_section + + uses :: "notion set" + +doc_class contribution_claim = introduction + + based_on :: "notion list" + +doc_class technical = text_section + + formal_results :: "thm list" + +doc_class "definition" = technical + + is_formal :: "bool" + property :: "term list" <= "[]" + +datatype kind = expert_opinion | argument | "proof" + +doc_class result = technical + + evidence :: kind + property :: "thm list" <= "[]" + +doc_class example = technical + + referring_to :: "(notion + definition) set" <= "{}" + +doc_class "conclusion" = text_section + + establish :: "(contribution_claim \ result) set" + +text\ Besides subtyping, there is another relation between +doc_classes: a class can be a \<^emph>\monitor\ 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 -- +in which instances of monitored classes may occur. + +The control of monitors is done by the commands: +\<^item> \<^verbatim>\ monitor > \ +\<^item> \<^verbatim>\ close_monitor > \ + +where the automaton of the monitor class is expected +to be in a final state. + +Monitors can be nested. + +Classes neither directly or indirectly (via inheritance) +mentioned in the monitor clause are \<^emph>\independent\ from +the monitor and may occur freely, \ie{} in arbitrary order.n \ + + +text \underlying idea: a monitor class automatically receives a + \<^verbatim>\trace\ attribute in which a list of observed class-ids is maintained. + The \<^verbatim>\trace\ is a \<^emph>\`predefined id`\ like \<^verbatim>\main\ in C. It can be accessed + like any other attribute of a class instance, \ie{} a document item.\ + +doc_class article = + style_id :: string <= "''LNCS''" + accepts "(title ~~ \author\\<^sup>+ ~~ abstract ~~ + \introduction\\<^sup>+ ~~ \technical || example\\<^sup>+ ~~ \conclusion\\<^sup>+)" + + +ML\ +structure Small_Math_trace_invariant = +struct +local + +fun group f g cidS [] = [] + |group f g cidS (a::S) = case find_first (f a) cidS of + NONE => [a] :: group f g cidS S + | SOME cid => let val (pref,suff) = take_prefix (g cid) S + in (a::pref)::(group f g cidS suff) end; + +fun partition ctxt cidS trace = + let fun find_lead (x,_) = DOF_core.is_subclass ctxt x; + fun find_cont cid (cid',_) = DOF_core.is_subclass ctxt cid' cid + in group find_lead find_cont cidS trace end; + +fun dest_option _ (Const (@{const_name "None"}, _)) = NONE + | dest_option f (Const (@{const_name "Some"}, _) $ t) = SOME (f t) + +in + +fun check ctxt cidS mon_id pos = + let val trace = AttributeAccess.compute_trace_ML ctxt mon_id pos @{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 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 ^ + " must have lowest level") + | SOME X => X + fun check_group_elem level_hd a = case (get_level (snd a)) of + NONE => true + | SOME y => if level_hd <= y then true + (* or < ? But this is too strong ... *) + else error("Invariant violation: "^ + "subsequent section " ^ snd a ^ + " must have higher level."); + fun check_group [] = true + |check_group [_] = true + |check_group (a::S) = forall (check_group_elem (check_level_hd a)) (S) + in if forall check_group groups then () + else error"Invariant violation: leading section must have lowest level" + end +end + +end +\ + +setup\ 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}; + true) + in DOF_core.update_class_invariant "small_math.article" body end\ + + + + +gen_sty_template + + +end +