diff --git a/examples/ROOTS b/examples/ROOTS index 8a4f5ea..9c90882 100644 --- a/examples/ROOTS +++ b/examples/ROOTS @@ -1,4 +1,5 @@ scholarly/ +technical_report/TR_my_commented_isabelle technical_report math_exam/MathExam math_exam/BAC2017 diff --git a/examples/cenelec/Example.thy b/examples/cenelec/Example.thy index 7d4a667..34bcaeb 100644 --- a/examples/cenelec/Example.thy +++ b/examples/cenelec/Example.thy @@ -34,6 +34,9 @@ text*[hyp1::hypothesis] \ P inequal NP \ text\A real example fragment from a larger project, declaring a text-element as a "safety-related application condition", a concept defined in the @{theory "CENELEC_50126"} ontology:\ + +text*[new_ass::hypothesis]\Under the assumption @{assumption \ass1\} we establish the following: ... \ + text*[ass122::srac] \ The overall sampling frequence of the odometer subsystem is therefore 14 khz, which includes sampling, computing and result communication times... \ diff --git a/examples/scholarly/IsaDofApplications.thy b/examples/scholarly/IsaDofApplications.thy index 7b74bbe..df09a46 100644 --- a/examples/scholarly/IsaDofApplications.thy +++ b/examples/scholarly/IsaDofApplications.thy @@ -95,9 +95,9 @@ declare_reference*[ontopide::text_section] declare_reference*[conclusion::text_section] (*>*) text*[plan::introduction_elem]\ The plan of the paper is follows: we start by introducing the underlying -Isabelel sytem (@{docitem_ref (unchecked) \bgrnd\}) followed by presenting the -essentials of \isadof and its ontology language (@{docitem_ref (unchecked) \isadof\}). -It follows @{docitem_ref (unchecked) \ontomod\}, where we present three application +Isabelel sytem (@{docitem (unchecked) \bgrnd\}) followed by presenting the +essentials of \isadof and its ontology language (@{docitem (unchecked) \isadof\}). +It follows @{docitem (unchecked) \ontomod\}, where we present three application scenarios from the point of view of the ontology modeling. In @{docitem_ref (unchecked) \ontopide\} we discuss the user-interaction generated from the ontological definitions. Finally, we draw conclusions and discuss related work in @{docitem_ref (unchecked) \conclusion\}. \ @@ -295,7 +295,7 @@ Science Series, as required by many scientific conferences, is mostly straight-f figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"] \ Ouroboros I: This paper from inside \ldots \ -text\ @{docitem_ref \fig1\} shows the corresponding view in the Isabelle/PIDE of thqqe present paper. +text\ @{docitem \fig1\} shows the corresponding view in the Isabelle/PIDE of thqqe present paper. Note that the text uses \isadof's own text-commands containing the meta-information provided by the underlying ontology. We proceed by a definition of \inlineisar+introduction+'s, which we define as the extension of diff --git a/MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy similarity index 94% rename from MyCommentedIsabelle.thy rename to examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy index 017faac..ba968a4 100644 --- a/MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy @@ -1,16 +1,37 @@ -chapter \A More Or Less Structured File with my Personal, Ecclectic Comments - on the Isabelle 2017 Infrastructure \ - -text\This is a programming-tutorial, complementary to the "The Isabelle Cookbook" in - \url{https://nms.kcl.ac.uk/christian.urban/Cookbook/}.\ - +(*<*) theory MyCommentedIsabelle - imports Main + imports "../../../ontologies/technical_report" begin - -section{* SML and Fundamental SML libraries *} -subsection "Text, Antiquotations, and the Isabelle/Pure bootstrap" +open_monitor*[this::article] +(*>*) + +title*[tit::title]\An Account with my Personal, Ecclectic Comments on the Isabelle Architecture\ +subtitle*[stit::subtitle]\Version : Isabelle 2017\ +text*[bu::author, + email = "''wolff@lri.fr''", + affiliation = "''Universit\\'e Paris-Sud, Paris, France''"]\Burkhart Wolff\ + + +text*[abs::abstract, + keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\ +While Isabelle is mostly known as part of Isabelle/HOL (an interactive +theorem prover), it actually provides a system framework for developing a wide +spectrum of applications. A particular strength of the Isabelle framework is the +combination of text editing, formal verification, and code generation. + +This is a programming-tutorial of Isabelle and Isabelle/HOL, a complementary +text to the unfortunately somewhat outdated "The Isabelle Cookbook" in +\url{https://nms.kcl.ac.uk/christian.urban/Cookbook/}. The reader is encouraged +not only to consider the generated .pdf, but also consult the loadable version in Isabelle/jedit +in order to make experiments on the running code. +\ + + + +chapter{* SML and Fundamental SML libraries *} + +section "Text, Antiquotations, and the Isabelle/Pure bootstrap" text\Isabelle is written in SML, the "Standard Meta-Language", which is is an impure functional programming language allowing, in principle, variables and side-effects: \ @@ -52,7 +73,7 @@ text\It is instructive to study the fundamental Boot Order of the Isabelle command key in Isabelle/jedit and activating it) allows the Isabelle IDE to support hyperlinking \<^emph>\inside\ the Isabelle source.\ -subsection "Elements of the SML library"; +section "Elements of the SML library"; text\Elements of the @{file "$ISABELLE_HOME/src/Pure/General/basics.ML"} SML library are basic exceptions. Note that exceptions should be catched individually, uncatched exceptions except those generated by the specific "error" function are discouraged in Isabelle @@ -116,13 +137,14 @@ end \ text\... where \<^verbatim>\key\ is usually just a synonym for string.\ +chapter {* Prover Architecture *} section {* The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts *} text\ What I call the 'Nano-Kernel' in Isabelle can also be seen as an acyclic theory graph. The meat of it can be found in the file @{file "$ISABELLE_HOME/src/Pure/context.ML"}. My notion is a bit criticisable since this component, which provides the type of @{ML_type theory} -and @{ML_type proof_context}, is not that Nano after all. +and @{ML_type Proof.context}, is not that Nano after all. However, these type are pretty empty place-holders at that level and the content of @{file "$ISABELLE_HOME/src/Pure/theory.ML"} is registered much later. The sources themselves mention it as "Fundamental Structure". @@ -155,7 +177,7 @@ A context comes in form of three 'flavours': \<^item> Generic: @{ML_type Context.generic }, i.e. the sum of both. All context have to be seen as mutable; so there are usually transformations defined on them -which are possible as long as a particular protocol (begin_thy - end_thy etc) are respected. +which are possible as long as a particular protocol (\<^verbatim>\begin_thy\ - \<^verbatim>\end_thy\ etc) are respected. Contexts come with type user-defined data which is mutable through the entire lifetime of a context. @@ -195,16 +217,17 @@ structure Data = Generic_Data ); - Data.get : generic -> Data.T; - Data.put : Data.T -> generic -> generic; - Data.map : (Data.T -> Data.T) -> generic -> generic; + Data.get : Context.generic -> Data.T; + Data.put : Data.T -> Context.generic -> Context.generic; + Data.map : (Data.T -> Data.T) -> Context.generic -> Context.generic; + (* there are variants to do this on theories ... *) *} -section\ The LCF-Kernel: terms, types, theories, proof_contexts, thms \ +section\ The LCF-Kernel: terms, types, theories, proof\_contexts, thms \ text\The classical LCF-style \<^emph>\kernel\ is about -\<^enum> Types and terms of a typed \-Calculus including constant symbols, - free variables, \-Binder and application, +\<^enum> Types and terms of a typed $\lambda$-Calculus including constant symbols, + free variables, $\lambda$-binder and application, \<^enum> An infrastructure to define types and terms, a \<^emph>\signature\, that also assigns to constant symbols types \<^enum> An abstract type of \<^emph>\theorem\ and logical operations on them @@ -216,7 +239,7 @@ text\The classical LCF-style \<^emph>\kernel\ is about subsection{* Terms and Types *} text \A basic data-structure of the kernel is @{file "$ISABELLE_HOME/src/Pure/term.ML"} \ ML{* open Term; -(* +signature TERM' = sig type indexname = string * int type class = string type sort = class list @@ -234,7 +257,7 @@ ML{* open Term; $ of term * term exception TYPE of string * typ list * term list exception TERM of string * term list -*) +end *} ML{* Type.typ_instance: Type.tsig -> typ * typ -> bool (* raises TYPE_MATCH *) *} @@ -475,6 +498,7 @@ At the very very end in @{file "~~/src/Pure/Syntax/syntax_phases.ML"}, it sets (the hooks) via: *} + (* val _ = Theory.setup @@ -493,7 +517,7 @@ val _ = uncheck_terms = uncheck_terms}); *) -text{* Thus, Syntax_Phases does the actual work, including +text{* Thus, Syntax\_Phases does the actual work, including markup generation and generation of reports. Look at: *} (* @@ -538,11 +562,10 @@ As one can see, check-routines internally generate the markup. *) -section\Front End \ +chapter\Front End \ +text\Introduction ... TODO\ -ML\Sign.add_trrules\ - -subsection\string, bstring and xstring\ +section\Basics: string, bstring and xstring\ text\@{ML_type "string"} is the basic library type from the SML library in structure @{ML_structure "String"}. Many Isabelle operations produce or require formats thereof introduced as type synonyms @@ -574,10 +597,10 @@ ML\ fun dark_matter x = XML.content_of (YXML.parse_body x)\ (* MORE TO COME *) -subsection{* Parsing issues *} +section{* Parsing issues *} text\ Parsing combinators represent the ground building blocks of both generic input engines -as well as the specific Isar framework. They are implemented in the structure \verb*Token* +as well as the specific Isar framework. They are implemented in the structure \verb+Token+ providing core type \verb+Token.T+. \ ML{* open Token*} @@ -653,7 +676,7 @@ Scan.lift (Parse.position Args.cartouche_input); text{* "parsers" are actually interpreters; an 'a parser is a function that parses an input stream and computes(=evaluates, computes) it into 'a. Since the semantics of an Isabelle command is a transition => transition - or theory \ theory function, i.e. a global system transition. + or theory $\Rightarrow$ theory function, i.e. a global system transition. parsers of that type can be constructed and be bound as call-back functions to a table in the Toplevel-structure of Isar. @@ -667,7 +690,7 @@ text{* Syntax operations : Interface for parsing, type-checking, "reading" Encapsulates the data structure "syntax" --- the table with const symbols, print and ast translations, ... The latter is accessible, e.g. from a Proof - context via Proof_Context.syn_of. + context via @{ML Proof_Context.syn_of}. *} ML\ @@ -745,8 +768,12 @@ val Z = let val attribute = Parse.position Parse.name -- fn name => (Thy_Output.antiquotation name (Scan.lift (Parse.position Args.cartouche_input))); \ +section\\ +ML\Sign.add_trrules\ + +section\ The PIDE Framework \ subsection\ Markup \ -text{* Markup Operations, and reporting. Diag in Isa_DOF Foundations Paper. +text{* Markup Operations, and reporting. Diag in Isa\_DOF Foundations TR. Markup operation send via side-effect annotations to the GUI (precisely: to the PIDE Framework) that were used for hyperlinking applicating to binding occurrences, info for hovering, ... *} @@ -855,13 +882,13 @@ fun check ctxt (name, pos) = -subsection {* Output: Very Low Level *} +section {* Output: Very Low Level *} ML\ Output.output; (* output is the structure for the "hooks" with the target devices. *) Output.output "bla_1:"; \ -subsection {* Output: High Level *} +section {* Output: High Level *} ML\ Thy_Output.verbatim_text; @@ -942,7 +969,7 @@ fun pretty_command (cmd as (name, Command {comment, ...})) = *} - +section\The Isar Engine\ ML{* Toplevel.theory; diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT new file mode 100644 index 0000000..88a1b88 --- /dev/null +++ b/examples/technical_report/TR_my_commented_isabelle/ROOT @@ -0,0 +1,12 @@ +session MyCommentedIsabelle = "Functional-Automata" + + options [document = pdf, document_output = "output",quick_and_dirty = true] + theories [document = false] + "../../../ontologies/scholarly_paper" + "../../../ontologies/technical_report" + theories + "MyCommentedIsabelle" + document_files + "root.tex" + "preamble.tex" + "ontologies.tex" + "build"