Moved MyCommentedIsabelle into the example/TR_my_commented isabelle
- added build structure - corrected LaTeX - ... works as a first shot TR !!!
This commit is contained in:
parent
3e6dc80445
commit
fe09c77b89
|
|
@ -1,4 +1,5 @@
|
|||
scholarly/
|
||||
technical_report/TR_my_commented_isabelle
|
||||
technical_report
|
||||
math_exam/MathExam
|
||||
math_exam/BAC2017
|
||||
|
|
|
|||
|
|
@ -34,6 +34,9 @@ text*[hyp1::hypothesis] \<open> P inequal NP \<close>
|
|||
text\<open>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:\<close>
|
||||
|
||||
text*[new_ass::hypothesis]\<open>Under the assumption @{assumption \<open>ass1\<close>} we establish the following: ... \<close>
|
||||
|
||||
text*[ass122::srac] \<open> The overall sampling frequence of the odometer
|
||||
subsystem is therefore 14 khz, which includes sampling, computing and
|
||||
result communication times... \<close>
|
||||
|
|
|
|||
|
|
@ -95,9 +95,9 @@ declare_reference*[ontopide::text_section]
|
|||
declare_reference*[conclusion::text_section]
|
||||
(*>*)
|
||||
text*[plan::introduction_elem]\<open> The plan of the paper is follows: we start by introducing the underlying
|
||||
Isabelel sytem (@{docitem_ref (unchecked) \<open>bgrnd\<close>}) followed by presenting the
|
||||
essentials of \isadof and its ontology language (@{docitem_ref (unchecked) \<open>isadof\<close>}).
|
||||
It follows @{docitem_ref (unchecked) \<open>ontomod\<close>}, where we present three application
|
||||
Isabelel sytem (@{docitem (unchecked) \<open>bgrnd\<close>}) followed by presenting the
|
||||
essentials of \isadof and its ontology language (@{docitem (unchecked) \<open>isadof\<close>}).
|
||||
It follows @{docitem (unchecked) \<open>ontomod\<close>}, where we present three application
|
||||
scenarios from the point of view of the ontology modeling. In @{docitem_ref (unchecked) \<open>ontopide\<close>}
|
||||
we discuss the user-interaction generated from the ontological definitions. Finally, we draw
|
||||
conclusions and discuss related work in @{docitem_ref (unchecked) \<open>conclusion\<close>}. \<close>
|
||||
|
|
@ -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''"]
|
||||
\<open> Ouroboros I: This paper from inside \ldots \<close>
|
||||
|
||||
text\<open> @{docitem_ref \<open>fig1\<close>} shows the corresponding view in the Isabelle/PIDE of thqqe present paper.
|
||||
text\<open> @{docitem \<open>fig1\<close>} 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
|
||||
|
|
|
|||
|
|
@ -1,16 +1,37 @@
|
|||
chapter \<open>A More Or Less Structured File with my Personal, Ecclectic Comments
|
||||
on the Isabelle 2017 Infrastructure \<close>
|
||||
|
||||
text\<open>This is a programming-tutorial, complementary to the "The Isabelle Cookbook" in
|
||||
\url{https://nms.kcl.ac.uk/christian.urban/Cookbook/}.\<close>
|
||||
|
||||
(*<*)
|
||||
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]\<open>An Account with my Personal, Ecclectic Comments on the Isabelle Architecture\<close>
|
||||
subtitle*[stit::subtitle]\<open>Version : Isabelle 2017\<close>
|
||||
text*[bu::author,
|
||||
email = "''wolff@lri.fr''",
|
||||
affiliation = "''Universit\\'e Paris-Sud, Paris, France''"]\<open>Burkhart Wolff\<close>
|
||||
|
||||
|
||||
text*[abs::abstract,
|
||||
keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\<open>
|
||||
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.
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
chapter{* SML and Fundamental SML libraries *}
|
||||
|
||||
section "Text, Antiquotations, and the Isabelle/Pure bootstrap"
|
||||
|
||||
text\<open>Isabelle is written in SML, the "Standard Meta-Language", which is
|
||||
is an impure functional programming language allowing, in principle, variables and side-effects: \<close>
|
||||
|
|
@ -52,7 +73,7 @@ text\<open>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>\<open>inside\<close> the Isabelle source.\<close>
|
||||
|
||||
subsection "Elements of the SML library";
|
||||
section "Elements of the SML library";
|
||||
text\<open>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
|
|||
\<close>
|
||||
text\<open>... where \<^verbatim>\<open>key\<close> is usually just a synonym for string.\<close>
|
||||
|
||||
chapter {* Prover Architecture *}
|
||||
|
||||
section {* The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts *}
|
||||
|
||||
text\<open> 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>\<open>begin_thy\<close> - \<^verbatim>\<open>end_thy\<close> 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\<open> The LCF-Kernel: terms, types, theories, proof_contexts, thms \<close>
|
||||
section\<open> The LCF-Kernel: terms, types, theories, proof\_contexts, thms \<close>
|
||||
text\<open>The classical LCF-style \<^emph>\<open>kernel\<close> is about
|
||||
\<^enum> Types and terms of a typed \<lambda>-Calculus including constant symbols,
|
||||
free variables, \<lambda>-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>\<open>signature\<close>,
|
||||
that also assigns to constant symbols types
|
||||
\<^enum> An abstract type of \<^emph>\<open>theorem\<close> and logical operations on them
|
||||
|
|
@ -216,7 +239,7 @@ text\<open>The classical LCF-style \<^emph>\<open>kernel\<close> is about
|
|||
subsection{* Terms and Types *}
|
||||
text \<open>A basic data-structure of the kernel is @{file "$ISABELLE_HOME/src/Pure/term.ML"} \<close>
|
||||
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\<open>Front End \<close>
|
||||
chapter\<open>Front End \<close>
|
||||
text\<open>Introduction ... TODO\<close>
|
||||
|
||||
ML\<open>Sign.add_trrules\<close>
|
||||
|
||||
subsection\<open>string, bstring and xstring\<close>
|
||||
section\<open>Basics: string, bstring and xstring\<close>
|
||||
text\<open>@{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\<open> fun dark_matter x = XML.content_of (YXML.parse_body x)\<close>
|
|||
(* MORE TO COME *)
|
||||
|
||||
|
||||
subsection{* Parsing issues *}
|
||||
section{* Parsing issues *}
|
||||
|
||||
text\<open> 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+.
|
||||
\<close>
|
||||
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 \<Rightarrow> 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\<open>
|
||||
|
|
@ -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)));
|
||||
\<close>
|
||||
|
||||
section\<open>\<close>
|
||||
ML\<open>Sign.add_trrules\<close>
|
||||
|
||||
section\<open> The PIDE Framework \<close>
|
||||
subsection\<open> Markup \<close>
|
||||
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\<open>
|
||||
Output.output; (* output is the structure for the "hooks" with the target devices. *)
|
||||
Output.output "bla_1:";
|
||||
\<close>
|
||||
|
||||
subsection {* Output: High Level *}
|
||||
section {* Output: High Level *}
|
||||
|
||||
ML\<open>
|
||||
Thy_Output.verbatim_text;
|
||||
|
|
@ -942,7 +969,7 @@ fun pretty_command (cmd as (name, Command {comment, ...})) =
|
|||
*}
|
||||
|
||||
|
||||
|
||||
section\<open>The Isar Engine\<close>
|
||||
|
||||
ML{*
|
||||
Toplevel.theory;
|
||||
|
|
@ -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"
|
||||
Loading…
Reference in New Issue