# HG changeset patch # User Christian Urban # Date 1254907720 -7200 # Node ID 163ac06622117a13061297a73f931a834a36c9d3 # Parent 4ae1ecb7153978cadfff2e9126572946e8493ed7 reorganised the certified terms section; tuned diff -r 4ae1ecb71539 -r 163ac0662211 ProgTutorial/General.thy --- a/ProgTutorial/General.thy Wed Oct 07 09:54:01 2009 +0200 +++ b/ProgTutorial/General.thy Wed Oct 07 11:28:40 2009 +0200 @@ -9,7 +9,6 @@ theorem proving where there is a small trusted core and everything else is build on top of this trusted core. The central data structures involved in this core are certified terms and types as well as theorems. - *} @@ -185,7 +184,7 @@ text {* While antiquotations are very convenient for constructing terms, they can only construct fixed terms (remember they are ``linked'' at compile-time). - However, you often need to construct terms dynamically. For example, a + However, you often need to construct terms manually. For example, a function that returns the implication @{text "\(x::nat). P x \ Q x"} taking @{term P} and @{term Q} as arguments can only be written as: @@ -573,62 +572,6 @@ section {* Type-Checking\label{sec:typechecking} *} text {* - - You can freely construct and manipulate @{ML_type "term"}s and @{ML_type - typ}es, since they are just arbitrary unchecked trees. However, you - eventually want to see if a term is well-formed, or type-checks, relative to - a theory. Type-checking is done via the function @{ML_ind cterm_of}, which - converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} - term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are - abstract objects that are guaranteed to be type-correct, and they can only - be constructed via ``official interfaces''. - - - Type-checking is always relative to a theory context. For now we use - the @{ML "@{theory}"} antiquotation to get hold of the current theory. - For example you can write: - - @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"(a::nat) + b = c\"}" "a + b = c"} - - This can also be written with an antiquotation: - - @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"} - - Attempting to obtain the certified term for - - @{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \"} - - yields an error (since the term is not typable). A slightly more elaborate - example that type-checks is: - -@{ML_response_fake [display,gray] -"let - val natT = @{typ \"nat\"} - val zero = @{term \"0::nat\"} -in - cterm_of @{theory} - (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero) -end" "0 + 0"} - - In Isabelle not just terms need to be certified, but also types. For example, - you obtain the certified type for the Isabelle type @{typ "nat \ bool"} on - the ML-level as follows: - - @{ML_response_fake [display,gray] - "ctyp_of @{theory} (@{typ nat} --> @{typ bool})" - "nat \ bool"} - - or with the antiquotation: - - @{ML_response_fake [display,gray] - "@{ctyp \"nat \ bool\"}" - "nat \ bool"} - - \begin{readmore} - For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see - the file @{ML_file "Pure/thm.ML"}. - \end{readmore} - Remember Isabelle follows the Church-style typing for terms, i.e., a term contains enough typing information (constants, free variables and abstractions all have typing information) so that it is always clear what the type of a term is. @@ -689,6 +632,7 @@ \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 @@ -698,6 +642,88 @@ \end{exercise} *} +section {* Certified Terms and Certified Types *} + +text {* + You can freely construct and manipulate @{ML_type "term"}s and @{ML_type + typ}es, since they are just arbitrary unchecked trees. However, you + eventually want to see if a term is well-formed, or type-checks, relative to + a theory. Type-checking is done via the function @{ML_ind cterm_of}, which + converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} + term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are + abstract objects that are guaranteed to be type-correct, and they can only + be constructed via ``official interfaces''. + + Certification is always relative to a theory context. For example you can + write: + + @{ML_response_fake [display,gray] + "cterm_of @{theory} @{term \"(a::nat) + b = c\"}" + "a + b = c"} + + This can also be written with an antiquotation: + + @{ML_response_fake [display,gray] + "@{cterm \"(a::nat) + b = c\"}" + "a + b = c"} + + Attempting to obtain the certified term for + + @{ML_response_fake_both [display,gray] + "@{cterm \"1 + True\"}" + "Type unification failed \"} + + yields an error (since the term is not typable). A slightly more elaborate + example that type-checks is: + +@{ML_response_fake [display,gray] +"let + val natT = @{typ \"nat\"} + val zero = @{term \"0::nat\"} +in + cterm_of @{theory} + (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero) +end" "0 + 0"} + + In Isabelle not just terms need to be certified, but also types. For example, + you obtain the certified type for the Isabelle type @{typ "nat \ bool"} on + the ML-level as follows: + + @{ML_response_fake [display,gray] + "ctyp_of @{theory} (@{typ nat} --> @{typ bool})" + "nat \ bool"} + + or with the antiquotation: + + @{ML_response_fake [display,gray] + "@{ctyp \"nat \ bool\"}" + "nat \ bool"} + + Since certified terms are, unlike terms, abstract objects, we cannot + pattern-match against them. However, we can construct them. For example + the function @{ML_ind capply in Thm} produces a certified application. + + @{ML_response_fake [display,gray] + "Thm.capply @{cterm \"P::nat \ bool\"} @{cterm \"3::nat\"}" + "P 3"} + + Similarly @{ML_ind list_comb in Drule} applies a list of @{ML_type cterm}s. + + @{ML_response_fake [display,gray] + "let + val chead = @{cterm \"P::unit \ nat \ bool\"} + val cargs = [@{cterm \"()\"}, @{cterm \"3::nat\"}] +in + Drule.list_comb (chead, cargs) +end" + "P () 3"} + + \begin{readmore} + For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see + the files @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and + @{ML_file "Pure/drule.ML"}. + \end{readmore} +*} section {* Theorems *} @@ -1445,7 +1471,7 @@ -section {* Name Space Issues (TBD) *} +section {* Managing Name Spaces (TBD) *} end diff -r 4ae1ecb71539 -r 163ac0662211 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Wed Oct 07 09:54:01 2009 +0200 +++ b/ProgTutorial/Intro.thy Wed Oct 07 11:28:40 2009 +0200 @@ -229,7 +229,7 @@ \vspace{5cm} {\Large\bf - This document is still in the process of being written! All of the + This tutorial is still in the process of being written! All of the text is still under construction. Sections and chapters that are under \underline{heavy} construction are marked with TBD.} diff -r 4ae1ecb71539 -r 163ac0662211 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Wed Oct 07 09:54:01 2009 +0200 +++ b/ProgTutorial/Tactical.thy Wed Oct 07 11:28:40 2009 +0200 @@ -2206,7 +2206,7 @@ where "id2 \ \x. x" text {* - Both definitions define the same function, although the theorems @{thm + Although both definitions define the same function, the theorems @{thm [source] id1_def} and @{thm [source] id2_def} are different. However it is easy to transform one theorem into the other. The function @{ML_ind abs_def in Drule} can automatically transform theorem @{thm [source] id1_def} diff -r 4ae1ecb71539 -r 163ac0662211 progtutorial.pdf Binary file progtutorial.pdf has changed