isabelle-cookbook: comparison ProgTutorial/Essential.thy

equal deleted inserted replaced

-:5fc2fb34c323
+:dc76ba24e81b
 In Line 3 we obtain the higher-order matcher. We assume there is a finite
 number of them and select the one we are interested in via the parameter
 @{text i} in the next line. In Lines 5 and 6 we destruct the resulting
 environments using the function @{ML_ind dest in Vartab}. Finally, we need
 to map the functions @{ML prep_trm} and @{ML prep_ty} over the respective
 environments (Line 8). As a simple example we instantiate the
-@{thm [source] conjI}-rule as follows
+@{thm [source] spec} rule so that its conclusion is of the form
+@{term "Q True"}.
-@{ML_response_fake [gray,display]
+@{ML_response_fake [gray,display,linenos]
 "let
 val pat = Logic.strip_imp_concl (prop_of @{thm spec})
-val trm = @{term \"Trueprop (P True)\"}
+val trm = @{term \"Trueprop (Q True)\"}
 val inst = matcher_inst @{theory} pat trm 1
 in
-Drule.instantiate inst @{thm conjI}
+Drule.instantiate inst @{thm spec}
 end"
-"\<forall>x. P x \<Longrightarrow> P True"}
+"\<forall>x. Q x \<Longrightarrow> Q True"}
+Note that we had to insert a @{text "Trueprop"}-coercion in Line 3 since the
+conclusion of @{thm [source] spec} contains one.
 \begin{readmore}
 Unification and matching of higher-order patterns is implemented in
 @{ML_file "Pure/pattern.ML"}. This file also contains a first-order matcher
 for terms. Full higher-order unification is implemented
 in @{ML_file "Pure/unify.ML"}. It uses lazy sequences which are implemented
 checking and pretty-printing of terms are defined. Functions related to
 type-inference are implemented in @{ML_file "Pure/type.ML"} and
 @{ML_file "Pure/type_infer.ML"}.
 \end{readmore}
-\footnote{\bf FIXME: say something about sorts.}
-\footnote{\bf FIXME: give a ``readmore''.}
 \begin{exercise}
 Check that the function defined in Exercise~\ref{fun:revsum} returns a
 result that type-checks. See what happens to the  solutions of this
 exercise given in Appendix \ref{ch:solutions} when they receive an
 text {*
 The corresponding ML-code is as follows:
 *}
-ML{*val my_thm =
+ML %linenosgray{*val my_thm =
 let
 val assm1 = @{cprop "\<And>(x::nat). P x \<Longrightarrow> Q x"}
 val assm2 = @{cprop "(P::nat \<Rightarrow> bool) t"}
 val Pt_implies_Qt =
 |> implies_intr assm2
 |> implies_intr assm1
 end*}
 text {*
+Note that in Line 3 and 4 we use the antiquotation @{text "@{cprop \<dots>}"}, which
+inserts necessary @{text "Trueprop"}s.
 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]
 "tracing (string_of_thm @{context} my_thm)"
 While we obtained a theorem as result, this theorem is not
 yet stored in Isabelle's theorem database. Consequently, it cannot be
 referenced on the user level. One way to store it in the theorem database is
 by using the function @{ML_ind note in Local_Theory}.\footnote{\bf FIXME: make sure a pointer
-to the section about local-setup is given earlier.}
+to the section about local-setup is given here.}
 *}
 local_setup %gray {*
 Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
 [source] my_thm_simp} is that they can now also be referenced with the
 \isacommand{thm}-command on the user-level of Isabelle
 \begin{isabelle}
-\isacommand{thm}~@{text "my_thm"}\isanewline
+\isacommand{thm}~@{text "my_thm my_thm_simp"}\isanewline
-@{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
+@{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}\isanewline
+@{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. Otherwise the
 user has no access to these theorems.
 text {*
 we still obtain the same list. The reason is that we used the function @{ML_ind
 add_thm in Thm} in our update function. This is a dedicated function which
 tests whether the theorem is already in the list.  This test is done
-according to alpha-equivalence of the proposition behind the theorem. The
+according to alpha-equivalence of the proposition of the theorem. The
 corresponding testing function is @{ML_ind eq_thm_prop in Thm}.
 Suppose you proved the following three theorems.
 *}
 lemma
 "Premises: ?A, ?B
 Conclusion: ?C
 Premises:
 Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C"}
-Note that in the second case, there is no premise.
+Note that in the second case, there is no premise. The reason is that @{text "\<Longrightarrow>"}
+separates premises and conclusion, while @{text "\<longrightarrow>"} is the object implication
+from HOL, which just constructs a formula.
 \begin{readmore}
 The basic functions for theorems are defined in
 @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}.
 \end{readmore}
 reasons. An example of this function is as follows:
 @{ML_response_fake [display, gray]
 "Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"
 "True = False"}
+\begin{readmore}
+Functions that setup goal states and prove theorems are implemented in
+@{ML_file "Pure/goal.ML"}. A function and a tactic that allow one to
+skip proofs of theorems are implemented in @{ML_file "Pure/Isar/skip_proof.ML"}.
+\end{readmore}
 Theorems also contain auxiliary data, such as the name of the theorem, its
 kind, the names for cases and so on. This data is stored in a string-string
 list and can be retrieved with the function @{ML_ind get_tags in
 Thm}. Assume you prove the following lemma.

changeset 415	dc76ba24e81b
parent 414	5fc2fb34c323
child 416	c6b5d1e25cdd