From 873eda8ee0b3ed817355c1ece537cb342aba1992 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Fri, 25 Sep 2020 13:38:34 +0200 Subject: [PATCH] stiluebungen --- .../TR_MyCommentedIsabelle.thy | 152 +++++++++--------- 1 file changed, 75 insertions(+), 77 deletions(-) diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index a2e5db4..fdb7d67 100755 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -40,7 +40,7 @@ text*[abs::abstract, 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 - @{cite "DBLP:journals/corr/Wenzel14"}in order to make experiments on the running code. + @{cite "DBLP:journals/corr/Wenzel14"} in order to make experiments on the running code. This text is written itself in Isabelle/Isar using a specific document ontology for technical reports. It is intended to be a "living document", i.e. it is not only @@ -75,7 +75,7 @@ figure*[architecture::figure,relative_width="80",src="''figures/isabelle-archite the IDE (right-hand side). \ text\This programming roughly follows the Isabelle system architecture shown in - @{figure "architecture"}, and, to be more precise, more or less in the bottom-up order. + \<^figure>\architecture\, and, to be more precise, more or less in the bottom-up order. We start from the basic underlying SML platform over the Kernels to the tactical layer and end with a discussion over the front-end technologies. @@ -299,13 +299,13 @@ text\ What I call the 'Nano-Kernel' in Isabelle can also be seen as an acy A context comes in form of three 'flavours': - \<^item> theories : @{ML_type theory}'s, containing a syntax and axioms, but also + \<^item> theories : \<^ML_type>\theory\'s, containing a syntax and axioms, but also user-defined data and configuration information. - \<^item> Proof-Contexts: @{ML_type Proof.context} + \<^item> Proof-Contexts: \<^ML_type>\Proof.context\ containing theories but also additional information if Isar goes into prove-mode. In general a richer structure than theories coping also with fixes, facts, goals, in order to support the structured Isar proof-style. - \<^item> Generic: @{ML_type Context.generic }, i.e. the sum of both. + \<^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 (\<^verbatim>\begin_thy\ - \<^verbatim>\end_thy\ etc) are respected. @@ -477,66 +477,67 @@ text\Note, furthermore, that there is a programming API for the HOL-instan it is contained in @{file "$ISABELLE_HOME/src/HOL/Tools/hologic.ML"}. It offers for many operators of the HOL logic specific constructors and destructors:\ -ML\ - HOLogic.boolT : typ; - HOLogic.mk_Trueprop : term -> term; (* the embedder of bool to prop fundamenyal for HOL *) - HOLogic.dest_Trueprop : term -> term; - HOLogic.Trueprop_conv : conv -> conv; - HOLogic.mk_setT : typ -> typ; (* ML level type constructor set *) - HOLogic.dest_setT : typ -> typ; - HOLogic.Collect_const : typ -> term; - HOLogic.mk_Collect : string * typ * term -> term; - HOLogic.mk_mem : term * term -> term; - HOLogic.dest_mem : term -> term * term; - HOLogic.mk_set : typ -> term list -> term; - HOLogic.conj_intr : Proof.context -> thm -> thm -> thm; (* some HOL-level derived-inferences *) - HOLogic.conj_elim : Proof.context -> thm -> thm * thm; - HOLogic.conj_elims : Proof.context -> thm -> thm list; - HOLogic.conj : term; (* some ML level logical constructors *) - HOLogic.disj : term; - HOLogic.imp : term; - HOLogic.Not : term; - HOLogic.mk_not : term -> term; - HOLogic.mk_conj : term * term -> term; - HOLogic.dest_conj : term -> term list; - HOLogic.conjuncts : term -> term list; - (* ... *) +text*[T2::technical]\ +\<^enum> \<^ML>\HOLogic.boolT : typ\ +\<^enum> \<^ML>\HOLogic.mk_Trueprop : term -> term\, the embedder of bool to prop fundamental for HOL +\<^enum> \<^ML>\HOLogic.dest_Trueprop : term -> term\ +\<^enum> \<^ML>\HOLogic.Trueprop_conv : conv -> conv\ +\<^enum> \<^ML>\HOLogic.mk_setT : typ -> typ\, the ML level type constructor set +\<^enum> \<^ML>\HOLogic.dest_setT : typ -> typ\, the ML level type destructor for set +\<^enum> \<^ML>\HOLogic.Collect_const : typ -> term\ +\<^enum> \<^ML>\HOLogic.mk_Collect : string * typ * term -> term\ +\<^enum> \<^ML>\HOLogic.mk_mem : term * term -> term\ +\<^enum> \<^ML>\HOLogic.dest_mem : term -> term * term\ +\<^enum> \<^ML>\HOLogic.mk_set : typ -> term list -> term\ +\<^enum> \<^ML>\HOLogic.conj_intr : Proof.context -> thm -> thm -> thm\, some HOL-level derived-inferences +\<^enum> \<^ML>\HOLogic.conj_elim : Proof.context -> thm -> thm * thm\ +\<^enum> \<^ML>\HOLogic.conj_elims : Proof.context -> thm -> thm list\ +\<^enum> \<^ML>\HOLogic.conj : term\ , some ML level logical constructors +\<^enum> \<^ML>\HOLogic.disj : term\ +\<^enum> \<^ML>\HOLogic.imp : term\ +\<^enum> \<^ML>\HOLogic.Not : term\ +\<^enum> \<^ML>\HOLogic.mk_not : term -> term\ +\<^enum> \<^ML>\HOLogic.mk_conj : term * term -> term\ +\<^enum> \<^ML>\HOLogic.dest_conj : term -> term list\ +\<^enum> \<^ML>\HOLogic.conjuncts : term -> term list\ +\<^enum> ... \ -text\In this style, extensions can be defined such as:\ +text*[T3::technical]\In this style, extensions can be defined such as:\ ML\fun optionT t = Type(@{type_name "Option.option"},[t]); \ subsection\ Type-Certification (=checking that a type annotation is consistent) \ -ML\ Type.typ_instance: Type.tsig -> typ * typ -> bool (* raises TYPE_MATCH *) \ -text\ there is a joker type that can be added as place-holder during term construction. - Jokers can be eliminated by the type inference. \ - -text\ \<^ML>\ Term.dummyT : typ \ \ - text\ +\<^enum> \<^ML>\Type.typ_instance: Type.tsig -> typ * typ -> bool (* raises TYPE_MATCH *) \ +\<^enum> \<^ML>\ Term.dummyT : typ \ is a joker type that can be added as place-holder during term + construction. Jokers can be eliminated by the type inference. \ + + +text*[T4::technical]\ \<^enum> \<^ML>\Sign.typ_instance: theory -> typ * typ -> bool\ \<^enum> \<^ML>\Sign.typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv\ -\<^enum> \<^ML>\ Sign.typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int\ +\<^enum> \<^ML>\Sign.typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int\ \<^enum> \<^ML>\Sign.const_type: theory -> string -> typ option\ -\<^enum> \<^ML>\Sign.certify_term: theory -> term -> term * typ * int\ (* core routine for CERTIFICATION of types*) -\<^enum> \<^ML>\Sign.cert_term: theory -> term -> term\ (* short-cut for the latter *) -\<^enum> \<^ML>\Sign.tsig_of: theory -> Type.tsig\ (* projects the type signature *) +\<^enum> \<^ML>\Sign.certify_term: theory -> term -> term * typ * int\, the function for CERTIFICATION of types +\<^enum> \<^ML>\Sign.cert_term: theory -> term -> term\, short-cut for the latter +\<^enum> \<^ML>\Sign.tsig_of: theory -> Type.tsig\, projects from a theory the type signature \ text\ - @{ML "Sign.typ_match"} etc. is actually an abstract wrapper on the structure - @{ML_structure "Type"} - which contains the heart of the type inference. - It also contains the type substitution type @{ML_type "Type.tyenv"} which is - is actually a type synonym for @{ML_type "(sort * typ) Vartab.table"} - which in itself is a synonym for @{ML_type "'a Symtab.table"}, so - possesses the usual @{ML "Symtab.empty"} and @{ML "Symtab.dest"} operations. \ + \<^ML>\Sign.typ_match\ etc. is actually an abstract wrapper on the structure + \<^ML_structure>\Type\ which contains the heart of the type inference. + It also contains the type substitution type \<^ML_type>\Type.tyenv\ which is + is actually a type synonym for \<^ML_type>\(sort * typ) Vartab.table\ + which in itself is a synonym for \<^ML_type>\'a Symtab.table\, so + possesses the usual \<^ML>\Symtab.empty\ and \<^ML>\Symtab.dest\ operations. \ text\Note that \<^emph>\polymorphic variables\ are treated like constant symbols in the type inference; thus, the following test, that one type is an instance of the other, yields false:\ +subsubsection*[exo4::example]\ Example:\ + ML\ val ty = @{typ "'a option"}; val ty' = @{typ "int option"}; @@ -545,16 +546,16 @@ val Type("List.list",[S]) = @{typ "('a) list"}; (* decomposition example *) val false = Sign.typ_instance @{theory}(ty', ty); \ -text\In order to make the type inference work, one has to consider @{emph \schematic\} +text\In order to make the type inference work, one has to consider \<^emph>\schematic\ type variables, which are more and more hidden from the Isar interface. Consequently, the typ antiquotation above will not work for schematic type variables and we have to construct them by hand on the SML level: \ ML\ val t_schematic = Type("List.list",[TVar(("'a",0),@{sort "HOL.type"})]); \ -text\ MIND THE "'" !!!\ +text\ MIND THE "'" !!! Ommitting it leads at times to VERY strange behaviour ...\ -text \On this basis, the following @{ML_type "Type.tyenv"} is constructed: \ +text \On this basis, the following \<^ML_type>\Type.tyenv\ is constructed: \ ML\ val tyenv = Sign.typ_match ( @{theory}) (t_schematic, @{typ "int list"}) @@ -564,7 +565,7 @@ val [(("'a", 0), (["HOL.type"], @{typ "int"}))] = Vartab.dest tyenv; text\ Type generalization --- the conversion between free type variables and schematic type variables --- is apparently no longer part of the standard API (there is a slightly - more general replacement in @{ML "Term_Subst.generalizeT_same"}, however). Here is a way to + more general replacement in \<^ML>\Term_Subst.generalizeT_same\, however). Here is a way to overcome this by a self-baked generalization function:\ ML\ @@ -575,13 +576,15 @@ val true = Sign.typ_instance @{theory} (ty', generalize_typ ty) text\... or more general variants thereof that are parameterized by the indexes for schematic type variables instead of assuming just @{ML "0"}. \ -text*[exo4::example]\ Example:\ +text\ Example:\ ML\val t = generalize_term @{term "[]"}\ text\Now we turn to the crucial issue of type-instantiation and with a given type environment \<^ML>\tyenv\. For this purpose, one has to switch to the low-level interface \<^ML_structure>\Term_Subst\. \ +subsection\More operations on types\ + text\ \<^item> \<^ML>\Term_Subst.map_types_same : (typ -> typ) -> term -> term\ \<^item> \<^ML>\Term_Subst.map_aterms_same : (term -> term) -> term -> term\ @@ -1262,6 +1265,7 @@ text\The toplevel also provides an infrastructure for managing configurati and building the parametric configuration types @{ML_type "'a Config.T" } and the instance \<^verbatim>\type raw = value T\, for all registered configurations the protocol:\ ML\ + Config.get: Proof.context -> 'a Config.T -> 'a; Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context; Config.put: 'a Config.T -> 'a -> Proof.context -> Proof.context; @@ -1271,7 +1275,7 @@ ML\ text\... etc. is defined.\ -text\Example registration of an config attribute XS232: \ +subsubsection*[ex::example]\Example registration of an config attribute XS232 initialized to false: \ ML\ val (XS232, XS232_setup) = Attrib.config_bool \<^binding>\XS232\ (K false); @@ -1477,31 +1481,25 @@ text\This picture is less and less true for a number of reasons: 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 +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 - @{ML_type "bstring"} (defined in structure @{ML_structure "Binding"} - and @{ML_type "xstring"} (defined in structure @{ML_structure "Name_Space"}. + \<^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 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 misleading to believe it is just a string. -\ +ML\val b = Binding.name_of @{binding \here\}\ +text\... produces the system output \<^verbatim>\val it = "here": bstring\, + but note that it is misleading to believe it is just a string.\ ML\String.explode b\ (* is harmless, but *) ML\String.explode(Binding.name_of -(Binding.conglomerate[Binding.qualified_name "X.x", - @{binding "here"}] ))\ -(* Somehow it is possible to smuggle markup into bstrings; and this leads - ML\(((String.explode(!ODL_Command_Parser.SPY6))))\ - to something like - val it = [#"\^E", #"\^F", #"i", #"n", #"p", #"u", #"t", #"\^F", #"d", #"e", #"l", #"i", #"m", #"i", #"t", #"e", #"d", #"=", #"f", #"a", ...]: char list -*) + (Binding.conglomerate[Binding.qualified_name "X.x", @{binding "here"}] ))\ +text\... whioch leads to the output \<^verbatim>\val it = [#"x", #"_", #"h", #"e", #"r", #"e"]: char list\\ + +text\ However, there is an own XML parser for this format. See Section Markup. \ -text\ However, there is an own XML parser for this format. See Section Markup. -\ ML\ fun dark_matter x = XML.content_of (YXML.parse_body x)\ (* MORE TO COME *) @@ -1515,7 +1513,7 @@ val pos = @{here}; val markup = Position.here pos; writeln ("And a link to the declaration of 'here' is "^markup)\ -(* \<^here> *) +(* \<^here> *) text\ ... uses the antiquotation @{ML "@{here}"} to infer from the system lexer the actual position of itself in the global document, converts it to markup (a string-representation of it) and sends it via the usual @{ML "writeln"} to the interface. \ @@ -1523,7 +1521,7 @@ text\ ... uses the antiquotation @{ML "@{here}"} to infer from the system figure*[hyplinkout::figure,relative_width="40",src="''figures/markup-demo''"] \Output with hyperlinked position.\ -text\@{docitem \hyplinkout\} shows the produced output where the little house-like symbol in the +text\@{figure \hyplinkout\} shows the produced output where the little house-like symbol in the display is hyperlinked to the position of @{ML "@{here}"} in the ML sample above.\ section\Markup and Low-level Markup Reporting\ @@ -1837,7 +1835,7 @@ local open Args - (* some more combinaotrs *) + (* some more combinators *) val _ = symbolic: Token.T parser val _ = $$$ : string -> string parser val _ = maybe: 'a parser -> 'a option parser @@ -1910,16 +1908,16 @@ in val _ = () end subsection\ Bindings \ -text\ The structure @{ML_structure "Binding"} serves as +text\ The structure @{ML_structure \Binding\} serves as \structured name bindings\, as says the description, i.e. a mechanism to basically associate an input string-fragment to its position. This concept is vital in all parsing processes and the interaction with PIDE. Key are two things: -\<^enum> the type-synonym @{ML_type "bstring"} which is synonym to @{ML_type "string"} +\<^enum> the type-synonym @{ML_type \bstring\} which is synonym to @{ML_type \string\} and intended for "primitive names to be bound" -\<^enum> the projection @{ML "Binding.pos_of : Binding.binding -> Position.T"} -\<^enum> the constructor establishing a binding @{ML "Binding.make: bstring * Position.T -> Binding.binding"} +\<^enum> the projection @{ML \Binding.pos_of : Binding.binding -> Position.T\} +\<^enum> the constructor establishing a binding @{ML \Binding.make: bstring * Position.T -> Binding.binding\} \