# HG changeset patch # User Christian Urban # Date 1258856009 -3600 # Node ID 7675427e311f4a9a316de22124c84ae844f84c59 # Parent d7d55a5030b59b9d2ecf89d9d9f4dc7b00c14359 tuning diff -r d7d55a5030b5 -r 7675427e311f ProgTutorial/Advanced.thy --- a/ProgTutorial/Advanced.thy Sat Nov 21 00:29:43 2009 +0100 +++ b/ProgTutorial/Advanced.thy Sun Nov 22 03:13:29 2009 +0100 @@ -14,18 +14,27 @@ chapter {* Advanced Isabelle *} text {* - TBD + While terms, types and theorems are the most basic data structures in + Isabelle, there are a number of layers built on top of them. Most of these + layers are concerned with storing and manipulating data. Handling + them properly is an essential skill for Isabelle programming. The most basic + layer are theories. They contain global data and can be seen as the + ``long-term memory'' of Isabelle. There is usually only one theory + active at each moment. Proof contexts and local theories, on the + other hand, store local data for a task at hand. They act like the + ``short-term memory'' and there can be many of them that are active + in parallel. *} section {* Theories\label{sec:theories} (TBD) *} text {* - Theories are the most fundamental building blocks in Isabelle. They - contain definitions, syntax declarations, axioms, proofs etc. If a definition - is stated, it must be stored in a theory in order to be usable later - on. Similar 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 theort can be querried as follows. + As said above, theories are the most basic layer in Isabelle. They contain + definitions, syntax declarations, axioms, proofs etc. If a definition is + stated, it must be stored in a theory in order to be usable later + on. Similar 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}\\ @@ -43,23 +52,14 @@ @{text "> theorems: \"} \end{isabelle} + + \begin{center} \begin{tikzpicture} \node[top color=white, bottom color=gray!30, draw=black!100, drop shadow] {A}; \end{tikzpicture} \end{center} - - In contrast to an ordinary theory, which simply consists of a type - signature, as well as tables for constants, axioms and theorems, a local - theory contains additional context information, such as locally fixed - variables and local assumptions that may be used by the package. The type - @{ML_type local_theory} is identical to the type of \emph{proof contexts} - @{ML_type "Proof.context"}, although not every proof context constitutes a - valid local theory. - - @{ML "Context.>> o Context.map_theory"} - \footnote{\bf FIXME: list append in merge operations can cause exponential blowups.} *} @@ -124,6 +124,15 @@ section {* Local Theories (TBD) *} text {* + In contrast to an ordinary theory, which simply consists of a type + signature, as well as tables for constants, axioms and theorems, a local + theory contains additional context information, such as locally fixed + variables and local assumptions that may be used by the package. The type + @{ML_type local_theory} is identical to the type of \emph{proof contexts} + @{ML_type "Proof.context"}, although not every proof context constitutes a + valid local theory. + + @{ML "Context.>> o Context.map_theory"} @{ML_ind "Local_Theory.declaration"} *} diff -r d7d55a5030b5 -r 7675427e311f ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Sat Nov 21 00:29:43 2009 +0100 +++ b/ProgTutorial/Essential.thy Sun Nov 22 03:13:29 2009 +0100 @@ -1169,7 +1169,8 @@ complete typing annotations, especially in cases where the typing information is redundant. A short-cut is to use the ``place-holder'' type @{ML_ind dummyT in Term} and then let type-inference figure out the - complete type. An example is as follows: + complete type. The type inference can be invoked with the function + @{ML_ind check_term in Syntax}. An example is as follows: @{ML_response_fake [display,gray] "let @@ -1325,7 +1326,7 @@ |> implies_intr assm1 end*} -text {* +text {* If we print out the value of @{ML my_thm} then we see only the final statement of the theorem. @@ -1424,8 +1425,6 @@ fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))*} text {* - \footnote{\bf explain @{ML_ind add_thm in Thm} and @{ML_ind eq_thm_prop in Thm}.} - The function @{ML update} allows us to update the theorem list, for example by adding the theorem @{thm [source] TrueI}. *} @@ -1466,10 +1465,18 @@ @{text "> True"} \end{isabelle} - There is a multitude of functions in the structures @{ML_struct Thm} and @{ML_struct Drule} - for managing or manipulating theorems. For example - we can test theorems for alpha equality. Suppose you proved the following three - theorems. + Note that if we add the theorem @{thm [source] FalseE} again to the list +*} + +setup %gray {* update @{thm FalseE} *} + +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 + corresponding testing function is @{ML_ind eq_thm_prop in Thm}. + Suppose you proved the following three theorems. *} lemma @@ -1478,11 +1485,11 @@ and thm3: "\y. Q y" sorry text {* - Testing them for alpha equality using the function @{ML_ind eq_thm in Thm} produces: + Testing them for alpha equality produces: @{ML_response [display,gray] -"(Thm.eq_thm (@{thm thm1}, @{thm thm2}), - Thm.eq_thm (@{thm thm2}, @{thm thm3}))" +"(Thm.eq_thm_prop (@{thm thm1}, @{thm thm2}), + Thm.eq_thm_prop (@{thm thm2}, @{thm thm3}))" "(true, false)"} Many functions destruct theorems into @{ML_type cterm}s. For example @@ -1746,7 +1753,7 @@ install this function as the theorem style named @{text "my_strip_allq"}. *} -setup %gray {* +setup %gray{* Term_Style.setup "my_strip_allq" (Scan.succeed (K strip_allq)) *} @@ -1771,7 +1778,7 @@ \begin{isabelle} @{text "@{thm (my_strip_allq) style_test}"}\\ - @{text ">"}~@{thm (my_strip_allq) style_test}\\ + @{text ">"}~@{thm (my_strip_allq) style_test} \end{isabelle} without the leading quantifiers. We can improve this theorem style by explicitly diff -r d7d55a5030b5 -r 7675427e311f ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Sat Nov 21 00:29:43 2009 +0100 +++ b/ProgTutorial/FirstSteps.thy Sun Nov 22 03:13:29 2009 +0100 @@ -838,7 +838,7 @@ theorem lists; see Section \ref{sec:storing}). It is also possible to prove lemmas with the antiquotation @{text "@{lemma \ by \}"} - whose first argument is a statement (possibly many of them separated by @{text "and"}, + whose first argument is a statement (possibly many of them separated by @{text "and"}) and the second is a proof. For example *} diff -r d7d55a5030b5 -r 7675427e311f progtutorial.pdf Binary file progtutorial.pdf has changed