isabelle-cookbook: comparison ProgTutorial/General.thy

equal deleted inserted replaced

-:01e71cddf6a3
+:2f2018927f2a
 text {*
 If we print out the value of @{ML my_thm} then we see only the
 final statement of the theorem.
 @{ML_response_fake [display, gray]
-"string_of_thm @{context} my_thm
+"tracing (string_of_thm @{context} my_thm)"
-|> tracing"
 "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
 However, internally the code-snippet constructs the following
 proof.
 }
 \]
 While we obtained a theorem as result, this theorem is not
 yet stored in Isabelle's theorem database. Consequently, it cannot be
-referenced later on. One way to store it in the theorem database is
+referenced on the user level. One way to store it in the theorem database is
 by using the function @{ML_ind note in LocalTheory}.
 *}
 local_setup %gray {*
 LocalTheory.note Thm.theoremK
 ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
 text {*
 The first argument @{ML_ind theoremK in Thm} is a kind indicator, which
-classifies the theorem. For a theorem arising from a definition we should
+classifies the theorem. There are several such kind indicators: for a
-use @{ML_ind definitionK in Thm}, for an axiom @{ML_ind axiomK in Thm}, for
+theorem arising from a definition we should use @{ML_ind definitionK in
-``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK
+Thm}, for an axiom @{ML_ind axiomK in Thm}, for ``normal'' theorems the
-in Thm}.  The second argument is the name under which we store the theorem
+kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK in Thm}.  The second
-or theorems. The third can contain a list of (theorem) attributes. We will
+argument of @{ML note in LocalTheory} is the name under which we store the
-explain them in detail in Section~\ref{sec:attributes}. Below we
+theorem or theorems. The third argument can contain a list of (theorem)
-use such an attribute in order add the theorem to the simpset.
+attributes. We will explain them in detail in
-have to declare:
+Section~\ref{sec:attributes}. Below we just use one such attribute in order add
+the theorem to the simpset:
 *}
 local_setup %gray {*
 LocalTheory.note Thm.theoremK
 ((@{binding "my_thm_simp"},
 [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}
 text {*
-Note that we have to use another name for the theorem, since Isabelle does
+Note that we have to use another name under which the theorem is stored,
-not allow to store another theorem under the same name. The attribute needs to
+since Isabelle does not allow us to store another theorem under the same
-be wrapped inside the function @{ML_ind internal in Attrib}. If we use the
+name. The attribute needs to be wrapped inside the function @{ML_ind
-function @{ML get_thm_names_from_ss} from the previous chapter, we can check
+internal in Attrib}. If we use the function @{ML get_thm_names_from_ss} from
-whether the theorem has actually been added.
+the previous chapter, we can check whether the theorem has actually been
+added.
 @{ML_response [display,gray]
 "let
 fun pred s = match_string \"my_thm_simp\" s
 in
 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
 \end{isabelle}
 or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. As can be seen
 the theorem does not have any meta-variables that would be present if we proved
-this theorem on the user-level. We will see later on, we have to construct
+this theorem on the user-level. We will see later on that usually we have to
-meta-variables in a theorem explicitly.
+construct meta-variables in theorems explicitly.
 *}
 text {*
 There is a multitude of functions that manage or manipulate theorems. For example
-we can test theorems for (alpha) equality. Suppose you proved the following three
+we can test theorems for alpha equality. Suppose you proved the following three
-facts.
+theorems.
 *}
 lemma
 shows thm1: "\<forall>x. P x"
 and   thm2: "\<forall>y. P y"
 and   thm3: "\<forall>y. Q y" sorry
 text {*
-Testing for equality using the function @{ML_ind eq_thm in Thm} produces:
+Testing them for alpha equality using the function @{ML_ind eq_thm in Thm} produces:
 @{ML_response [display,gray]
 "(Thm.eq_thm (@{thm thm1}, @{thm thm2}),
 Thm.eq_thm (@{thm thm2}, @{thm thm3}))"
 "(true, false)"}
 @{ML_response_fake [display,gray]
 "let
 val eq = @{thm True_def}
 in
 (Thm.lhs_of eq, Thm.rhs_of eq)
-|> pairself (tracing o string_of_cterm @{context})
+|> pairself (string_of_cterm @{context})
 end"
-"True
+"(True, (\<lambda>x. x) = (\<lambda>x. x))"}
-(\<lambda>x. x) = (\<lambda>x. x)"}
 Other function produce terms that can be pattern-matched.
 Suppose the following two theorems.
 *}
 lemma
 shows foo_test1: "A \<Longrightarrow> B \<Longrightarrow> C"
 and   foo_test2: "A \<longrightarrow> B \<longrightarrow> C" sorry
 text {*
-We can deconstruct them into premises and conclusions as follows.
+We can destruct them into premises and conclusions as follows.
 @{ML_response_fake [display,gray]
 "let
 val ctxt = @{context}
 fun prems_and_concl thm =
-[\"Premises: \" ^
+[\"Premises: \"   ^ (string_of_terms ctxt (Thm.prems_of thm))] @
-(string_of_terms ctxt (Thm.prems_of thm))] @
+[\"Conclusion: \" ^ (string_of_term ctxt (Thm.concl_of thm))]
-[\"Conclusion: \" ^
-(string_of_term ctxt (Thm.concl_of thm))]
 |> cat_lines
 |> tracing
 in
 prems_and_concl @{thm foo_test1};
 prems_and_concl @{thm foo_test2}
 shows "A \<Longrightarrow> B"
 and   "C \<Longrightarrow> D"
 oops
-section {* Setups (TBD) *}
-text {*
-In the previous section we used \isacommand{setup} in order to make
-a theorem attribute known to Isabelle. 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 theory attribute has been stored.
-This is a fundamental principle in Isabelle. A similar situation occurs
-for example with declaring constants. The function that declares a
-constant on the ML-level is @{ML_ind  add_consts_i in Sign}.
-If you write\footnote{Recall that ML-code  needs to be
-enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.}
-*}
-ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}
-text {*
-for declaring the constant @{text "BAR"} with type @{typ nat} and
-run the code, then you indeed 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 [quotes] "BAR"}\\
-@{text "> \"BAR\" :: \"'a\""}
-\end{isabelle}
-you do not obtain a constant of type @{typ nat}, but a free variable (printed in
-blue) of polymorphic type. The problem is that the ML-expression above did
-not register the declaration with the current theory. This is what the command
-\isacommand{setup} is for. The constant is properly declared with
-*}
-setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}
-text {*
-Now
-\begin{isabelle}
-\isacommand{term}~@{text [quotes] "BAR"}\\
-@{text "> \"BAR\" :: \"nat\""}
-\end{isabelle}
-returns a (black) constant with the type @{typ nat}.
-A similar command is \isacommand{local\_setup}, which expects a function
-of type @{ML_type "local_theory -> local_theory"}. Later on we will also
-use the commands \isacommand{method\_setup} for installing methods in the
-current theory and \isacommand{simproc\_setup} for adding new simprocs to
-the current simpset.
-*}
 section {* Theorem Attributes\label{sec:attributes} *}
 text {*
 Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text
 "[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
 @{ML_file "Pure/Isar/attrib.ML"}...also explained in the chapter about
 parsing.
 \end{readmore}
 *}
+section {* Setups (TBD) *}
+text {*
+In the previous section we used \isacommand{setup} in order to make
+a theorem attribute known to Isabelle. 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 theory attribute has been stored.
+This is a fundamental principle in Isabelle. A similar situation occurs
+for example with declaring constants. The function that declares a
+constant on the ML-level is @{ML_ind  add_consts_i in Sign}.
+If you write\footnote{Recall that ML-code  needs to be
+enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.}
+*}
+ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}
+text {*
+for declaring the constant @{text "BAR"} with type @{typ nat} and
+run the code, then you indeed 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 [quotes] "BAR"}\\
+@{text "> \"BAR\" :: \"'a\""}
+\end{isabelle}
+you do not obtain a constant of type @{typ nat}, but a free variable (printed in
+blue) of polymorphic type. The problem is that the ML-expression above did
+not register the declaration with the current theory. This is what the command
+\isacommand{setup} is for. The constant is properly declared with
+*}
+setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}
+text {*
+Now
+\begin{isabelle}
+\isacommand{term}~@{text [quotes] "BAR"}\\
+@{text "> \"BAR\" :: \"nat\""}
+\end{isabelle}
+returns a (black) constant with the type @{typ nat}.
+A similar command is \isacommand{local\_setup}, which expects a function
+of type @{ML_type "local_theory -> local_theory"}. Later on we will also
+use the commands \isacommand{method\_setup} for installing methods in the
+current theory and \isacommand{simproc\_setup} for adding new simprocs to
+the current simpset.
+*}
 section {* Theories (TBD) *}
 text {*
 There are theories, proof contexts and local theories (in this order, if you

changeset 348	2f2018927f2a
parent 347	01e71cddf6a3
child 349	9e374cd891e1