# HG changeset patch # User haftmann # Date 1115024607 -7200 # Node ID 0a4cc9b113c7a68801a3eb5f376306fa3010a184 # Parent a6fb4ddc05c7f30909049eba953243e0c78b53f4 introduced @{const ...} antiquotation diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Ifexpr/Ifexpr.thy --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Mon May 02 10:56:13 2005 +0200 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Mon May 02 11:03:27 2005 +0200 @@ -180,7 +180,7 @@ \S\ref{sec:InductionHeuristics} \begin{exercise} - We strengthen the definition of a @{term normal} If-expression as follows: + We strengthen the definition of a @{const normal} If-expression as follows: the first argument of all @{term IF}s must be a variable. Adapt the above development to this changed requirement. (Hint: you may need to formulate some of the goals as implications (@{text"\"}) rather than diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Misc/Itrev.thy --- a/doc-src/TutorialI/Misc/Itrev.thy Mon May 02 10:56:13 2005 +0200 +++ b/doc-src/TutorialI/Misc/Itrev.thy Mon May 02 11:03:27 2005 +0200 @@ -119,7 +119,7 @@ those that change in recursive calls. A final point worth mentioning is the orientation of the equation we just -proved: the more complex notion (@{term itrev}) is on the left-hand +proved: the more complex notion (@{const itrev}) is on the left-hand side, the simpler one (@{term rev}) on the right-hand side. This constitutes another, albeit weak heuristic that is not restricted to induction: \begin{quote} diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Misc/Option2.thy --- a/doc-src/TutorialI/Misc/Option2.thy Mon May 02 10:56:13 2005 +0200 +++ b/doc-src/TutorialI/Misc/Option2.thy Mon May 02 11:03:27 2005 +0200 @@ -14,7 +14,7 @@ text{*\noindent Frequently one needs to add a distinguished element to some existing type. For example, type @{text"t option"} can model the result of a computation that -may either terminate with an error (represented by @{term None}) or return +may either terminate with an error (represented by @{const None}) or return some value @{term v} (represented by @{term"Some v"}). Similarly, @{typ nat} extended with $\infty$ can be modeled by type @{typ"nat option"}. In both cases one could define a new datatype with diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Overview/LNCS/Ind.thy --- a/doc-src/TutorialI/Overview/LNCS/Ind.thy Mon May 02 10:56:13 2005 +0200 +++ b/doc-src/TutorialI/Overview/LNCS/Ind.thy Mon May 02 11:03:27 2005 +0200 @@ -21,7 +21,7 @@ subsubsection{*Rule Induction*} -text{* Rule induction for set @{term even}, @{thm[source]even.induct}: +text{* Rule induction for set @{const even}, @{thm[source]even.induct}: @{thm[display] even.induct[no_vars]}*} (*<*)thm even.induct[no_vars](*>*) diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Overview/LNCS/RECDEF.thy --- a/doc-src/TutorialI/Overview/LNCS/RECDEF.thy Mon May 02 10:56:13 2005 +0200 +++ b/doc-src/TutorialI/Overview/LNCS/RECDEF.thy Mon May 02 11:03:27 2005 +0200 @@ -29,7 +29,7 @@ "sep1(a, xs) = xs"; text{* -This is what the rules for @{term sep1} are turned into: +This is what the rules for @{const sep1} are turned into: @{thm[display,indent=5] sep1.simps[no_vars]} *} (*<*) diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Recdef/Nested1.thy --- a/doc-src/TutorialI/Recdef/Nested1.thy Mon May 02 10:56:13 2005 +0200 +++ b/doc-src/TutorialI/Recdef/Nested1.thy Mon May 02 11:03:27 2005 +0200 @@ -26,11 +26,11 @@ and @{text"term_list_size :: term list \ nat"} is an auxiliary function automatically defined by Isabelle (while processing the declaration of @{text term}). Why does the -recursive call of @{term trev} lead to this +recursive call of @{const trev} lead to this condition? Because \isacommand{recdef} knows that @{term map} -will apply @{term trev} only to elements of @{term ts}. Thus the +will apply @{const trev} only to elements of @{term ts}. Thus the condition expresses that the size of the argument @{prop"t : set ts"} of any -recursive call of @{term trev} is strictly less than @{term"size(App f ts)"}, +recursive call of @{const trev} is strictly less than @{term"size(App f ts)"}, which equals @{term"Suc(term_list_size ts)"}. We will now prove the termination condition and continue with our definition. Below we return to the question of how \isacommand{recdef} knows about @{term map}. diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Recdef/examples.thy --- a/doc-src/TutorialI/Recdef/examples.thy Mon May 02 10:56:13 2005 +0200 +++ b/doc-src/TutorialI/Recdef/examples.thy Mon May 02 11:03:27 2005 +0200 @@ -63,7 +63,7 @@ one does not match, Isabelle internally replaces the second equation by the two possibilities that are left: @{prop"sep1(a,[]) = []"} and @{prop"sep1(a, [x]) = [x]"}. Thus the functions @{term sep} and -@{term sep1} are identical. +@{const sep1} are identical. \begin{warn} \isacommand{recdef} only takes the first argument of a (curried) diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Trie/Trie.thy --- a/doc-src/TutorialI/Trie/Trie.thy Mon May 02 10:56:13 2005 +0200 +++ b/doc-src/TutorialI/Trie/Trie.thy Mon May 02 11:03:27 2005 +0200 @@ -49,7 +49,7 @@ text{* As a first simple property we prove that looking up a string in the empty -trie @{term"Trie None []"} always returns @{term None}. The proof merely +trie @{term"Trie None []"} always returns @{const None}. The proof merely distinguishes the two cases whether the search string is empty or not: *}; @@ -76,10 +76,10 @@ @{term tt} associated with the first letter @{term a} is extracted, recursively updated, and then placed in front of the association list. The old subtrie associated with @{term a} is still in the association list -but no longer accessible via @{term assoc}. Clearly, there is room here for +but no longer accessible via @{const assoc}. Clearly, there is room here for optimizations! -Before we start on any proofs about @{term update} we tell the simplifier to +Before we start on any proofs about @{const update} we tell the simplifier to expand all @{text let}s and to split all @{text case}-constructs over options: *}; @@ -88,11 +88,11 @@ text{*\noindent The reason becomes clear when looking (probably after a failed proof -attempt) at the body of @{term update}: it contains both +attempt) at the body of @{const update}: it contains both @{text let} and a case distinction over type @{text option}. -Our main goal is to prove the correct interaction of @{term update} and -@{term lookup}: +Our main goal is to prove the correct interaction of @{const update} and +@{const lookup}: *}; theorem "\t v bs. lookup (update t as v) bs = @@ -102,8 +102,8 @@ Our plan is to induct on @{term as}; hence the remaining variables are quantified. From the definitions it is clear that induction on either @{term as} or @{term bs} is required. The choice of @{term as} is -guided by the intuition that simplification of @{term lookup} might be easier -if @{term update} has already been simplified, which can only happen if +guided by the intuition that simplification of @{const lookup} might be easier +if @{const update} has already been simplified, which can only happen if @{term as} is instantiated. The start of the proof is conventional: *}; @@ -138,7 +138,7 @@ sense and solves the proof. \begin{exercise} - Modify @{term update} (and its type) such that it allows both insertion and + Modify @{const update} (and its type) such that it allows both insertion and deletion of entries with a single function. Prove the corresponding version of the main theorem above. Optimize your function such that it shrinks tries after @@ -146,10 +146,10 @@ \end{exercise} \begin{exercise} - Write an improved version of @{term update} that does not suffer from the + Write an improved version of @{const update} that does not suffer from the space leak (pointed out above) caused by not deleting overwritten entries from the association list. Prove the main theorem for your improved - @{term update}. + @{const update}. \end{exercise} \begin{exercise} diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Types/Pairs.thy --- a/doc-src/TutorialI/Types/Pairs.thy Mon May 02 10:56:13 2005 +0200 +++ b/doc-src/TutorialI/Types/Pairs.thy Mon May 02 11:03:27 2005 +0200 @@ -138,7 +138,7 @@ lemma "swap(swap p) = p" txt{*\noindent -simplification will do nothing, because the defining equation for @{term swap} +simplification will do nothing, because the defining equation for @{const swap} expects a pair. Again, we need to turn @{term p} into a pair first, but this time there is no @{term split} in sight. In this case the only thing we can do is to split the term by hand: diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Types/Records.thy --- a/doc-src/TutorialI/Types/Records.thy Mon May 02 10:56:13 2005 +0200 +++ b/doc-src/TutorialI/Types/Records.thy Mon May 02 11:03:27 2005 +0200 @@ -45,8 +45,8 @@ Ycoord :: int text {* - Records of type @{typ point} have two fields named @{text Xcoord} - and @{text Ycoord}, both of type~@{typ int}. We now define a + Records of type @{typ point} have two fields named @{const Xcoord} + and @{const Ycoord}, both of type~@{typ int}. We now define a constant of type @{typ point}: *} @@ -78,8 +78,8 @@ text {* The \emph{update}\index{update!record} operation is functional. For - example, @{term "p\Xcoord := 0\"} is a record whose @{text Xcoord} - value is zero and whose @{text Ycoord} value is copied from~@{text + example, @{term "p\Xcoord := 0\"} is a record whose @{const Xcoord} + value is zero and whose @{const Ycoord} value is copied from~@{text p}. Updates of explicit records are also simplified automatically: *} @@ -111,7 +111,7 @@ col :: colour text {* - The fields of this new type are @{text Xcoord}, @{text Ycoord} and + The fields of this new type are @{const Xcoord}, @{text Ycoord} and @{text col}, in that order. *} @@ -137,7 +137,7 @@ text {* This lemma applies to any record whose first two fields are @{text - Xcoord} and~@{text Ycoord}. Note that @{text "\Xcoord = a, Ycoord + Xcoord} and~@{const Ycoord}. Note that @{text "\Xcoord = a, Ycoord = b, \ = ()\"} is exactly the same as @{text "\Xcoord = a, Ycoord = b\"}. Selectors and updates are always polymorphic wrt.\ the @{text more} part of a record scheme, its value is just ignored (for @@ -169,7 +169,7 @@ \medskip Type @{typ point} is for fixed records having exactly the two fields - @{text Xcoord} and~@{text Ycoord}, while the polymorphic type @{typ + @{const Xcoord} and~@{text Ycoord}, while the polymorphic type @{typ "'a point_scheme"} comprises all possible extensions to those two fields. Note that @{typ "unit point_scheme"} coincides with @{typ point}, and @{typ "\col :: colour\ point_scheme"} with @{typ @@ -188,7 +188,7 @@ text {* Here is a generic method that modifies a point, incrementing its - @{text Xcoord} field. The @{text Ycoord} and @{text more} fields + @{const Xcoord} field. The @{text Ycoord} and @{text more} fields are copied across. It works for any record type scheme derived from @{typ point} (including @{typ cpoint} etc.): *} @@ -200,7 +200,7 @@ text {* Generic theorems can be proved about generic methods. This trivial - lemma relates @{text incX} to @{text getX} and @{text setX}: + lemma relates @{const incX} to @{text getX} and @{text setX}: *} lemma "incX r = setX r (getX r + 1)" @@ -272,7 +272,7 @@ text {* Here the simplifier can do nothing, since general record equality is not eliminated automatically. One way to proceed is by an explicit - forward step that applies the selector @{text Xcoord} to both sides + forward step that applies the selector @{const Xcoord} to both sides of the assumed record equality: *} @@ -376,7 +376,7 @@ "cpt2 \ point.extend pt1 (cpoint.fields Green)" text {* - The coloured points @{text cpt1} and @{text cpt2} are equal. The + The coloured points @{const cpt1} and @{text cpt2} are equal. The proof is trivial, by unfolding all the definitions. We deliberately omit the definition of~@{text pt1} in order to reveal the underlying comparison on type @{typ point}.