diff -r ebbd0dd008c8 -r fee4942c4770 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Thu Jan 29 09:46:17 2009 +0000 +++ b/CookBook/FirstSteps.thy Thu Jan 29 09:46:36 2009 +0000 @@ -7,7 +7,7 @@ text {* Isabelle programming is done in ML. Just like lemmas and proofs, ML-code - in Isabelle is part of a theory. If you want to follow the code written in + in Isabelle is part of a theory. If you want to follow the code given in this chapter, we assume you are working inside the theory starting with \begin{center} @@ -26,7 +26,7 @@ text {* The easiest and quickest way to include code in a theory is - by using the \isacommand{ML}-command. For example\smallskip + by using the \isacommand{ML}-command. For example: \begin{isabelle} \begin{graybox} @@ -37,17 +37,17 @@ \end{graybox} \end{isabelle} - Like ``normal'' Isabelle proof scripts, + Like normal Isabelle proof scripts, \isacommand{ML}-commands can be evaluated by using the advance and undo buttons of your Isabelle environment. The code inside the \isacommand{ML}-command can also contain value and function bindings, and even those can be undone when the proof script is retracted. As mentioned earlier, we will drop the \isacommand{ML}~@{text "\ \ \"} - whenever we show code. + scaffolding whenever we show code. Once a portion of code is relatively stable, one usually wants to export it to a separate ML-file. Such files can then be included in a - theory by using \isacommand{uses} in the header of the theory, like + theory by using the \isacommand{uses}-command in the header of the theory, like: \begin{center} \begin{tabular}{@ {}l} @@ -85,7 +85,7 @@ output this function generates will be overwritten as soon as an error is raised. For printing anything more serious and elaborate, the function @{ML tracing} is more appropriate. This function writes all output into - a separate tracing buffer. For example + a separate tracing buffer. For example: @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""} @@ -111,7 +111,7 @@ Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} will cause that all tracing information is printed into the file @{text "foo.bar"}. - Error messages can be printed using the function @{ML error}, as in + You can print out error messages with the function @{ML error}, as in: @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""} @@ -134,10 +134,10 @@ where @{text "@{theory}"} is an antiquotation that is substituted with the current theory (remember that we assumed we are inside the theory - @{text FirstSteps}). The name of this theory can be extracted with + @{text FirstSteps}). The name of this theory can be extracted using the function @{ML "Context.theory_name"}. - Note, however, that antiquotations are statically scoped, that is their value is + Note, however, that antiquotations are statically linked, that is their value is determined at ``compile-time'', not ``run-time''. For example the function *} @@ -145,7 +145,7 @@ text {* - does, as its name suggest, \emph{not} return the name of the current theory, if it is run in a + does \emph{not} return the name of the current theory, if it is run in a different theory. Instead, the code above defines the constant function that always returns the string @{text [quotes] "FirstSteps"}, no matter where the function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is @@ -161,12 +161,12 @@ @{ML_response_fake [display,gray] "let - val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset} + val ({rules,...}, _) = MetaSimplifier.rep_ss @{simpset} in map #name (Net.entries rules) end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \]"} - The code about simpsets extracts the theorem names that are stored in the + The code about simpsets extracts the theorem names stored in the current simpset. We get hold of the current simpset with the antiquotation @{text "@{simpset}"}. The function @{ML rep_ss in MetaSimplifier} returns a record containing all information about the simpset. The rules of a simpset are @@ -182,20 +182,20 @@ \end{readmore} While antiquotations have many applications, they were originally introduced in order - to avoid explicit bindings for theorems such as + to avoid explicit bindings for theorems such as: *} ML{*val allI = thm "allI" *} text {* These bindings are difficult to maintain and also can be accidentally - overwritten by the user. This often breakes definitional + overwritten by the user. This often breakes Isabelle packages. Antiquotations solve this problem, since they are ``linked'' - statically at compile-time. However, this static linkage also limits their - usefulness in cases where data needs to be build up dynamically. In the course of - this introduction, we will learn more about - these antiquotations: they greatly simplify Isabelle programming since one - can directly access all kinds of logical elements from ML. + statically at compile-time. However, this static linkage also limits their + usefulness in cases where data needs to be build up dynamically. In the + course of this introduction, we will learn more about these antiquotations: + they greatly simplify Isabelle programming since one can directly access all + kinds of logical elements from th ML-level. *} @@ -203,7 +203,7 @@ text {* One way to construct terms of Isabelle on the ML-level is by using the antiquotation - \mbox{@{text "@{term \}"}}. For example + \mbox{@{text "@{term \}"}}. For example: @{ML_response [display,gray] "@{term \"(a::nat) + b = c\"}" @@ -231,7 +231,7 @@ \begin{exercise} Look at the internal term representation of the following terms, and - find out why they are represented like this. + find out why they are represented like this: \begin{itemize} \item @{term "case x of 0 \ 0 | Suc y \ y"} @@ -261,7 +261,7 @@ where it is not (since it is already constructed by a meta-implication). - Types can be constructed using the antiquotation @{text "@{typ \}"}. For example + Types can be constructed using the antiquotation @{text "@{typ \}"}. For example: @{ML_response_fake [display,gray] "@{typ \"bool \ nat\"}" "bool \ nat"} @@ -279,11 +279,11 @@ While antiquotations are very convenient for constructing terms, they can only construct fixed terms (remember they are ``linked'' at compile-time). See Recipe~\ref{rec:external} on Page~\pageref{rec:external} - for a function that pattern-matches over terms and where the pattern are - constructed from antiquotations. However, one often needs to construct + for a function that pattern-matches over terms and where the patterns are + constructed using antiquotations. However, one often needs to construct terms dynamically. For example, a function that returns the implication @{text "\(x::\). P x \ Q x"} taking @{term P}, @{term Q} and the type @{term - "\"} as arguments can only be written as + "\"} as arguments can only be written as: *} ML{*fun make_imp P Q tau = @@ -294,7 +294,6 @@ end *} text {* - The reason is that one cannot pass the arguments @{term P}, @{term Q} and @{term "tau"} into an antiquotation. For example the following does \emph{not} work: *} @@ -357,7 +356,7 @@ text {* \begin{readmore} - There are many functions in @{ML_file "Pure/logic.ML"} and + There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms and types easier.\end{readmore} @@ -381,8 +380,23 @@ number representing their sum. \end{exercise} + (FIXME: maybe should go) - (FIXME: operation from page 19 of the implementation manual) +*} + +ML{*fun nat_to_int t = + (case t of + @{typ nat} => @{typ int} + | Type (s, ts) => Type (s, map nat_to_int ts) + | _ => t)*} + +text {* + +@{ML_response_fake [display,gray] +"map_types nat_to_int @{term \"a = (1::nat)\"}" +"Const (\"op =\", \"int \ int \ bool\") + $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"} + *} section {* Type-Checking *} @@ -431,7 +445,7 @@ result that type-checks. \end{exercise} - (FIXME: @{text "ctyp_of"}) + (FIXME: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT}) *} @@ -676,13 +690,33 @@ ML{*val double = (fn x => (x, x)) #-> (fn x => fn y => x + y)*} - text {* - - (FIXME: find a good exercise for combinators) *} + +(*<*) +setup {* + Sign.add_consts_i [("bar", @{typ "nat"},NoSyn)] +*} + +lemma "bar = (1::nat)" + oops + +setup {* + Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] + #> PureThy.add_defs false [((Binding.name "foo_def", + Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] + #> snd +*} + +lemma "foo = (1::nat)" + apply(simp add: foo_def) + done + +thm foo_def +(*>*) + end \ No newline at end of file