diff -r b11653b11bd3 -r cd612b489504 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Mon Oct 20 06:22:11 2008 +0000 +++ b/CookBook/FirstSteps.thy Mon Oct 27 18:48:52 2008 +0100 @@ -5,7 +5,8 @@ chapter {* First Steps *} -text {* +text {* + Isabelle programming is done in Standard ML. Just like lemmas and proofs, code in Isabelle is part of a theory. If you want to follow the code written in this chapter, we @@ -27,11 +28,11 @@ The easiest and quickest way to include code in a theory is by using the \isacommand{ML} command. For example\smallskip -\isacommand{ML} -@{ML_text "{"}@{ML_text "*"}\isanewline +\isa{\isacommand{ML} +\isacharverbatimopen\isanewline \hspace{5mm}@{ML "3 + 4"}\isanewline -@{ML_text "*"}@{ML_text "}"}\isanewline -@{ML_text "> 7"}\smallskip +\isacharverbatimclose\isanewline +@{ML_text "> 7"}\smallskip} Expressions inside \isacommand{ML} commands are immediately evaluated, like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of @@ -40,15 +41,15 @@ commands the undo operation behaves slightly counter-intuitive, because if you define\smallskip -\isacommand{ML} -@{ML_text "{"}@{ML_text "*"}\isanewline -@{ML_text "val foo = true"}\isanewline -@{ML_text "*"}@{ML_text "}"}\isanewline -@{ML_text "> true"}\smallskip +\isa{\isacommand{ML} +\isacharverbatimopen\isanewline +\hspace{5mm}@{ML_text "val foo = true"}\isanewline +\isacharverbatimclose\isanewline +@{ML_text "> true"}\smallskip} then Isabelle's undo operation has no effect on the definition of @{ML_text "foo"}. Note that from now on we will drop the - \isacommand{ML} @{ML_text "{"}@{ML_text "* \ *"}@{ML_text "}"} whenever + \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever we show code and its response. Once a portion of code is relatively stable, one usually wants to @@ -65,7 +66,8 @@ \end{tabular} \end{center} - Note that from now on we are going to drop the the + Note that from now on we are going to drop the + \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}. *} @@ -100,25 +102,22 @@ It is also possible to redirect the channel where the @{ML_text "foo"} is printed to a separate file, e.g. to prevent Proof General from choking on massive amounts of trace output. This rediretion can be achieved using the code -*} - -ML {* - val strip_specials = - let - fun strip ("\^A" :: _ :: cs) = strip cs - | strip (c :: cs) = c :: strip cs - | strip [] = []; - in implode o strip o explode end; - fun redirect_tracing stream = - Output.tracing_fn := (fn s => +@{ML_decl [display] +"val strip_specials = +let + fun strip (\"\\^A\" :: _ :: cs) = strip cs + | strip (c :: cs) = c :: strip cs + | strip [] = []; +in implode o strip o explode end; + +fun redirect_tracing stream = + Output.tracing_fn := (fn s => (TextIO.output (stream, (strip_specials s)); - TextIO.output (stream, "\n"); - TextIO.flushOut stream)); -*} + TextIO.output (stream, \"\\n\"); + TextIO.flushOut stream));"} -text {* - Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} + Calling @{ML_text "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} will cause that all tracing information is printed into the file @{ML_text "foo.bar"}. *} @@ -143,13 +142,9 @@ Note, however, that antiquotations are statically scoped, that is the value is determined at ``compile-time'', not ``run-time''. For example the function -*} + @{ML_decl [display] + "fun not_current_thyname () = Context.theory_name @{theory}"} -ML {* - fun not_current_thyname () = Context.theory_name @{theory} -*} - -text {* 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 @{ML_text "FirstSteps"}, no matter where the @@ -160,7 +155,6 @@ In a similar way you can use antiquotations to refer to theorems or simpsets: - @{ML [display] "@{thm allI}"} @{ML [display] "@{simpset}"} @@ -240,7 +234,7 @@ text {* - @{ML_response [display] "@{typ \"bool \ nat\"}" "Type \"} + @{ML_response_fake [display] "@{typ \"bool \ nat\"}" "bool \ nat"} (FIXME: Unlike the term antiquotation, @{text "@{typ \}"} does not print the internal representation. Is there a reason for this, that needs to be explained @@ -263,29 +257,19 @@ dynamically. For example, a function that returns the implication @{text "\(x::\). P x \ Q x"} taking @{term P}, @{term Q} and the typ @{term "\"} as arguments can only be written as -*} - -ML {* - fun make_imp P Q tau = +@{ML_decl [display] +"fun make_imp P Q tau = let - val x = Free ("x",tau) + val x = Free (\"x\",tau) in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x), HOLogic.mk_Trueprop (Q $ x))) - end -*} - -text {* + end"} The reason is that one cannot pass the arguments @{term P}, @{term Q} and @{term "tau"} into an antiquotation. For example the following does not work. -*} -ML {* - fun make_wrong_imp P Q tau = @{prop "\x. P x \ Q x"} -*} - -text {* + @{ML_decl [display] "fun make_wrong_imp P Q tau = @{prop \"\x. P x \ Q x\"}"} To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} to both functions. @@ -397,18 +381,16 @@ application. This combinator, and several variants are defined in @{ML_file "Pure/General/basics.ML"}.} -*} - -ML {* -let +@{ML_response_fake [display] +"let val thy = @{theory} - val assm1 = cterm_of thy @{prop "\(x::nat). P x \ Q x"} - val assm2 = cterm_of thy @{prop "((P::nat\bool) t)"} + val assm1 = cterm_of thy @{prop \"\(x::nat). P x \ Q x\"} + val assm2 = cterm_of thy @{prop \"((P::nat\bool) t)\"} val Pt_implies_Qt = assume assm1 - |> forall_elim (cterm_of thy @{term "t::nat"}); + |> forall_elim (cterm_of thy @{term \"t::nat\"}); val Qt = implies_elim Pt_implies_Qt (assume assm2); in @@ -416,10 +398,7 @@ Qt |> implies_intr assm2 |> implies_intr assm1 -end -*} - -text {* +end" "(FIXME)"} This code-snippet constructs the following proof: @@ -507,51 +486,43 @@ with the variables @{text xs} that will be generalised once the goal is proved. The @{text "tac"} is the tactic which proves the goal and which can make use of the local assumptions. -*} - - -ML {* -let +@{ML_response_fake [display] +"let val ctxt = @{context} - val goal = @{prop "P \ Q \ Q \ P"} + val goal = @{prop \"P \ Q \ Q \ P\"} in - Goal.prove ctxt ["P", "Q"] [] goal (fn _ => + Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ => eresolve_tac [disjE] 1 THEN resolve_tac [disjI2] 1 THEN assume_tac 1 THEN resolve_tac [disjI1] 1 THEN assume_tac 1) -end -*} - -text {* +end" "(FIXME)"} \begin{readmore} To learn more about the function @{ML Goal.prove} see \isccite{sec:results}. \end{readmore} -*} - -text {* An alternative way to transcribe this proof is as follows *} + An alternative way to transcribe this proof is as follows -ML {* -let +@{ML_response_fake [display] +"let val ctxt = @{context} - val goal = @{prop "P \ Q \ Q \ P"} + val goal = @{prop \"P \ Q \ Q \ P\"} in - Goal.prove ctxt ["P", "Q"] [] goal (fn _ => + Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ => (eresolve_tac [disjE] THEN' resolve_tac [disjI2] THEN' assume_tac THEN' resolve_tac [disjI1] THEN' assume_tac) 1) -end +end" "(FIXME)"} + + (FIXME: are there any advantages/disadvantages about this way?) *} -text {* (FIXME: are there any advantages/disadvantages about this way?) *} - section {* Storing Theorems *} section {* Theorem Attributes *}