isabelle-cookbook: comparison ProgTutorial/Advanced.thy

equal deleted inserted replaced

-:1c4250bc6258
+:780100cd4060
 *}
 section {* Theories and Setups\label{sec:theories} *}
 text {*
-Theories, as said above, are a basic layer of abstraction in Isabelle. They
+Theories, as said above, are a basic layer of abstraction in
-contain definitions, syntax declarations, axioms, theorems and much more. If a
+Isabelle. They contain definitions, syntax declarations, axioms,
-definition is made, it must be stored in a theory in order to be usable
+theorems and much more.  For example, if a definition is made, it
-later on. Similar with proofs: once a proof is finished, the proved theorem
+must be stored in a theory in order to be usable later on. Similar
-needs to be stored in the theorem database of the theory in order to be
+with proofs: once a proof is finished, the proved theorem needs to
+be stored in the theorem database of the theory in order to be
 usable. All relevant data of a theory can be queried as follows.
 \begin{isabelle}
 \isacommand{print\_theory}\\
 @{text "> names: Pure Code_Generator HOL \<dots>"}\\
 Functions acting on theories often end with the suffix @{text "_global"},
 for example the function @{ML read_term_global in Syntax} in the structure
 @{ML_struct Syntax}. The reason is to set them syntactically apart from
 functions acting on contexts or local theories (which will be discussed in
-next sections). There is a tendency in the Isabelle development to prefer
+the next sections). There is a tendency in the Isabelle development to prefer
 ``non-global'' operations, because they have some advantages, as we will also
 discuss later. However, some basic management of theories will very likely
 never go away.
-In the context ML-programming, the most important command with theories
+In the context of ML-programming, the most important command with theories
 is \isacommand{setup}. In the previous chapters we used it, for
 example, to make a theorem attribute known to Isabelle or to register a theorem
 under a name. What happens behind the scenes is that \isacommand{setup}
 expects a function of type @{ML_type "theory -> theory"}: the input theory
 is the current theory and the output the theory where the attribute has been
 in
 Sign.declare_const @{context} bar_const thy
 end*}
 text {*
-If you simply write this code\footnote{Recall that ML-code needs to be enclosed in
+If you simply run this code\footnote{Recall that ML-code needs to be enclosed in
 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} with the
-intention of declaring a constant @{text "BAR"} with type @{typ nat} and run
+intention of declaring a constant @{text "BAR"} with type @{typ nat}, then
-the code, then indeed you obtain a theory as result. But if you query the
+indeed you obtain a theory as result. But if you query the
 constant on the Isabelle level using the command \isacommand{term}
 \begin{isabelle}
 \isacommand{term}~@{text BAR}\\
 @{text "> \"BAR\" :: \"'a\""}
 @{text "> ERROR \"Stale theory encountered\""}
 \end{graybox}
 \end{isabelle}
 This time we erroneously return the original theory @{text thy}, instead of
-the modified one @{text thy'}. Such programming errors with handling the
+the modified one @{text thy'}. Such buggy code will always result into
-most current theory will always result into stale theory error messages.
+a runtime error message about stale theories.
 However, sometimes it does make sense to work with two theories at the same
 time, especially in the context of parsing and typing. In the code below we
 use in Line 3 the function @{ML_ind copy in Theory} from the structure
 @{ML_struct Theory} for obtaining a new theory that contains the same
 "tmp_thy"} the constant @{text FOO} (Lines 4 and 5). The point of this code
 is that we next, in Lines 6 and 7, parse a string to become a term (both
 times the string is @{text [quotes] "FOO baz"}). But since we parse the string
 once in the context of the theory @{text tmp_thy'} in which @{text FOO} is
 declared to be a constant of type @{typ "nat \<Rightarrow>nat"} and once in the context
-of @{text thy}, we obtain two different terms, namely
+of @{text thy} where it is not, we obtain two different terms, namely
 \begin{isabelle}
 \begin{graybox}
 @{text "> Const (\"Advanced.FOO\", \"nat \<Rightarrow> nat\") $ Free (\"baz\", \"nat\")"}\isanewline
 @{text "> Free (\"FOO\", \"'a \<Rightarrow> 'b\") $ Free (\"baz\", \"'a\")"}
 \end{graybox}
 \end{isabelle}
 There are two reasons for parsing a term in a temporary theory. One is to
-obtain fully qualified names and the other is appropriate type inference.
+obtain fully qualified names for constants and the other is appropriate type
-This is relevant in situations where definitions are made later, but parsing
+inference. This is relevant in situations where definitions are made later,
-and type inference has to take already proceed as if the definitions were
+but parsing and type inference has to take already proceed as if the definitions
-already made.
+were already made.
 *}
 section {* Contexts (TBD) *}
 text {*
 Contexts are arguably more important than theories, even though they only
 contain ``short-term memory data''. The reason is that a vast number of
 functions in Isabelle depend one way or the other on contexts. Even such
 mundane operation like printing out a term make essential use of contexts.
-*}
+For this consider the following contrived proof which only purpose is to
+fix two variables
+*}
+lemma "True"
+proof -
+txt_raw {*\mbox{}\\[-6mm]*}
+ML_prf {* Variable.dest_fixes @{context} *}
+txt_raw {*\mbox{}\\[-6mm]*}
+fix x y
+txt_raw {*\mbox{}\\[-6mm]*}
+ML_prf {* Variable.dest_fixes @{context} *}
+txt_raw {*\mbox{}\\[-6mm]*}
+oops
 (*
 ML{*Proof_Context.debug := true*}
 ML{*Proof_Context.verbose := true*}
 *)

changeset 488	780100cd4060
parent 487	1c4250bc6258
child 490	b8a654eabdf0