isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:f286dfa9f173
+:2728e8daebc0
 theory FirstSteps
 imports Base
 begin
 chapter {* First Steps *}
 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 given in
 this chapter, we assume you are working inside the theory starting with
 text {*
 Theorems also include schematic variables, such as @{text "?P"},
 @{text "?Q"} and so on.
 @{ML_response_fake [display, gray]
-"writeln (string_of_thm @{context} @{thm conjI})"
+"tracing (string_of_thm @{context} @{thm conjI})"
 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 In order to improve the readability of theorems we convert
 these schematic variables into free variables using the
 function @{ML [index] import in Variable}.
 text {*
 Theorem @{thm [source] conjI} is now printed as follows:
 @{ML_response_fake [display, gray]
-"writeln (string_of_thm_no_vars @{context} @{thm conjI})"
+"tracing (string_of_thm_no_vars @{context} @{thm conjI})"
 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
 Again the function @{ML commas} helps with printing more than one theorem.
 *}
 val t = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
 val ctxt = @{context}
 in
 apply_fresh_args t ctxt
 |> Syntax.string_of_term ctxt
-|> writeln
+|> tracing
 end"
 "P z za zb"}
 You can read off this behaviour from how @{ML apply_fresh_args} is
 coded: in Line 2, the function @{ML [index] fastype_of} calculates the type of the
 val t = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
 val ctxt = @{context}
 in
 apply_fresh_args t ctxt
 |> Syntax.string_of_term ctxt
-|> writeln
+|> tracing
 end"
 "za z zb"}
 where the @{text "za"} is correctly avoided.
 "let
 val v1 = Var ((\"x\", 3), @{typ bool})
 val v2 = Var ((\"x1\", 3), @{typ bool})
 val v3 = Free (\"x\", @{typ bool})
 in
-writeln (Syntax.string_of_term @{context} v1);
+tracing (Syntax.string_of_term @{context} v1);
-writeln (Syntax.string_of_term @{context} v2);
+tracing (Syntax.string_of_term @{context} v2);
-writeln (Syntax.string_of_term @{context} v3)
+tracing (Syntax.string_of_term @{context} v3)
 end"
 "?x3
 ?x1.3
 x"}
 @{ML_response_fake [display,gray]
 "let
 val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})
 in
-writeln (Syntax.string_of_term @{context} omega)
+tracing (Syntax.string_of_term @{context} omega)
 end"
 "x x"}
 with the raw ML-constructors.
 @{ML_response_fake [gray,display]
 "let
 val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
 in
-writeln (Syntax.string_of_term @{context} eq)
+tracing (Syntax.string_of_term @{context} eq)
 end"
 "True = False"}
 *}
 text {*
 | SOME i => Int.toString i
 val s3 =
 case realOut (!r) of
 NONE => "NONE"
 | SOME x => Real.toString x
-val () = writeln (concat [s1, " ", s2, " ", s3, "\n"])
+val () = tracing (concat [s1, " ", s2, " ", s3, "\n"])
 end*}
 ML_val{*structure t = Test(U) *}
 ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*}
 string}. This can be done with the function @{ML [index] string_of in Pretty}. In what
 follows we will use the following wrapper function for printing a pretty
 type:
 *}
-ML{*fun pprint prt = writeln (Pretty.string_of prt)*}
+ML{*fun pprint prt = tracing (Pretty.string_of prt)*}
 text {*
 The point of the pretty-printing infrastructure is to give hints about how to
 layout text and let Isabelle do the actual layout. Let us first explain
 how you can insert places where a line break can occur. For this assume the
 We deliberately chose a large string so that it spans over more than one line.
 If we print out the string using the usual ``quick-and-dirty'' method, then
 we obtain the ugly output:
 @{ML_response_fake [display,gray]
-"writeln test_str"
+"tracing test_str"
 "fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
 oooooooooooooobaaaaaaaaaaaar"}
 *}
 text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely  *}
-ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> writeln *}
+ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
-ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *}
+ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
-ML {* Pretty.mark Markup.subgoal (Pretty.str "foo") |> Pretty.string_of  |> writeln *}
+ML {* Pretty.mark Markup.subgoal (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
-ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *}
+ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
 text {*
 Still to be done:
 What happens with big formulae?
 text {*
 printing into the goal buffer as part of the proof state
 *}
-ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> writeln *}
+ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
-ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *}
+ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
 text {* writing into the goal buffer *}
 ML {* fun my_hook interactive state =
 (interactive ? Proof.goal_message (fn () => Pretty.str
 ML {*Datatype.get_info @{theory} "List.list"*}
 section {* Name Space(TBD) *}
 end

changeset 301	2728e8daebc0
parent 299	d0b81d6e1b28
child 304	14173c0e8688