--- a/ProgTutorial/First_Steps.thy Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/First_Steps.thy Tue May 21 14:37:39 2019 +0200
@@ -4,7 +4,6 @@
chapter \<open>First Steps\label{chp:firststeps}\<close>
-
text \<open>
\begin{flushright}
{\em ``The most effective debugging tool is still careful thought,\\
@@ -109,10 +108,9 @@
You can print out error messages with the function @{ML_ind error in Library};
for example:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>if 0 = 1 then true else (error "foo")\<close>
-\<open>*** foo
-***\<close>}
+\<open>foo\<close>}
This function raises the exception \<open>ERROR\<close>, which will then
be displayed by the infrastructure indicating that it is an error by
@@ -132,11 +130,14 @@
ML %grayML\<open>val pretty_term = Syntax.pretty_term
val pwriteln = Pretty.writeln\<close>
-
+(* We redfine pwriteln to return a value not just a side effect on the output in order to
+use some checking of output with ML_response antiquotation. *)
+ML %invisible\<open>val pretty_term = Syntax.pretty_term
+val pwriteln = YXML.content_of o Pretty.string_of\<close>
text \<open>
They can be used as follows
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>pwriteln (pretty_term @{context} @{term "1::nat"})\<close>
\<open>"1"\<close>}
@@ -159,7 +160,7 @@
text \<open>
Now by using this context @{ML pretty_term} prints out
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>pwriteln (pretty_term show_types_ctxt @{term "(1::nat, x)"})\<close>
\<open>(1::nat, x::'a)\<close>}
@@ -203,7 +204,7 @@
@{thm [source] conjI} shown below can be used for any (typable)
instantiation of \<open>?P\<close> and \<open>?Q\<close>.
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>pwriteln (pretty_thm @{context} @{thm conjI})\<close>
\<open>\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\<close>}
@@ -221,7 +222,7 @@
text \<open>
With this function, theorem @{thm [source] conjI} is now printed as follows:
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>pwriteln (pretty_thm_no_vars @{context} @{thm conjI})\<close>
\<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q\<close>}
@@ -267,12 +268,12 @@
@{ML_matchresult_fake [display,gray]
\<open>pwriteln (Pretty.str "First half,");
pwriteln (Pretty.str "and second half.")\<close>
-\<open>First half,
-and second half.\<close>}
+\<open>"First half,
+and second half."\<close>}
but as a single string with appropriate formatting. For example
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
\<open>pwriteln (Pretty.str ("First half," ^ "\\n" ^ "and second half."))\<close>
\<open>First half,
and second half.\<close>}
@@ -282,7 +283,7 @@
@{ML_ind cat_lines in Library} concatenates a list of strings
and inserts newlines in between each element.
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>pwriteln (Pretty.str (cat_lines ["foo", "bar"]))\<close>
\<open>foo
bar\<close>}
@@ -387,7 +388,7 @@
applied to it. For example, below three variables are applied to the term
@{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val trm = @{term "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}
val ctxt = @{context}
@@ -414,7 +415,7 @@
terms involving fresh variables. For this the infrastructure helps
tremendously to avoid any name clashes. Consider for example:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val trm = @{term "za::'a \<Rightarrow> 'b \<Rightarrow> 'c"}
val ctxt = @{context}
@@ -599,7 +600,7 @@
An example where this combinator is useful is as follows
- @{ML_matchresult_fake [display, gray]
+ @{ML_matchresult [display, gray]
\<open>let
val ((names1, names2), _) =
@{context}
@@ -639,12 +640,12 @@
both as pairs. We can use this information for example to print out the definiens and
the theorem corresponding to the definitions. For example for the first definition:
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>let
val (one_trm, (_, one_thm)) = one_def
in
- pwriteln (pretty_term ctxt' one_trm);
- pwriteln (pretty_thm ctxt' one_thm)
+ (pwriteln (pretty_term ctxt' one_trm),
+ pwriteln (pretty_thm ctxt' one_thm))
end\<close>
\<open>One
One \<equiv> 1\<close>}
@@ -673,7 +674,7 @@
@{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check
a list of terms. Consider the code:
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>let
val ctxt = @{context}
in
@@ -694,7 +695,7 @@
Syntax} in the file @{ML_file "Pure/Syntax/syntax.ML"} that is implemented
in terms of @{ML singleton} and @{ML check_terms in Syntax}.} For example
- @{ML_matchresult_fake [display, gray, linenos]
+ @{ML_response [display, gray, linenos]
\<open>let
val ctxt = @{context}
in
@@ -774,7 +775,7 @@
@{ML_matchresult_fake [display, gray]
\<open>Proof_Context.print_abbrevs false @{context}\<close>
\<open>\<dots>
-INTER \<equiv> INFI
+INTER \<equiv> INFIMUM
Inter \<equiv> Inf
\<dots>\<close>}
@@ -783,21 +784,22 @@
You can also use antiquotations to refer to proved theorems:
\<open>@{thm \<dots>}\<close> for a single theorem
- @{ML_matchresult_fake [display,gray] \<open>@{thm allI}\<close> \<open>(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x\<close>}
+ @{ML_response [display,gray] \<open>@{thm allI}\<close> \<open>(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x\<close>}
and \<open>@{thms \<dots>}\<close> for more than one
-@{ML_matchresult_fake [display,gray]
+
+@{ML_response [display,gray]
\<open>@{thms conj_ac}\<close>
-\<open>(?P \<and> ?Q) = (?Q \<and> ?P)
-(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
-((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)\<close>}
+\<open>["(?P \<and> ?Q) = (?Q \<and> ?P)",
+ "(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)",
+ "((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"]\<close>}
The thm-antiquotations can also be used for manipulating theorems. For
example, if you need the version of the theorem @{thm [source] refl} that
has a meta-equality instead of an equality, you can write
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
\<open>@{thm refl[THEN eq_reflection]}\<close>
\<open>?x \<equiv> ?x\<close>}
@@ -816,7 +818,7 @@
text \<open>
The result can be printed out as follows.
- @{ML_matchresult_fake [gray,display]
+ @{ML_response [gray,display]
\<open>foo_thms |> pretty_thms_no_vars @{context}
|> pwriteln\<close>
\<open>True, False \<Longrightarrow> P\<close>}
@@ -840,9 +842,9 @@
simp-rules. Now you can feed in the current simpset into this function.
The current simpset can be referred to using @{ML_ind simpset_of in Raw_Simplifier}.
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>get_thm_names_from_ss @{context}\<close>
- \<open>["Nat.of_nat_eq_id", "Int.of_int_eq_id", "Nat.One_nat_def", \<dots>]\<close>}
+ \<open>["Euclidean_Division.euclidean_size_int_def",\<dots>\<close>}
Again, this way of referencing simpsets makes you independent from additions
of lemmas to the simpset by the user, which can potentially cause loops in your
@@ -884,9 +886,9 @@
so that the ML-system can understand it. (All these functions will be explained
in more detail in later sections.) An example for this antiquotation is:
- @{ML_matchresult_fake [display,gray]
+ @{ML_matchresult [display,gray]
\<open>@{term_pat "Suc (?x::nat)"}\<close>
- \<open>Const ("Suc", "nat \<Rightarrow> nat") $ Var (("x", 0), "nat")\<close>}
+ \<open>Const ("Nat.Suc", _) $ Var (("x", 0), _)\<close>}
which shows the internal representation of the term \<open>Suc ?x\<close>. Similarly
we can write an antiquotation for type patterns. Its code is
@@ -980,19 +982,19 @@
text \<open>
The data can be retrieved with the projection functions defined above.
- @{ML_matchresult_fake [display, gray]
-\<open>project_int (nth foo_list 0);
-project_bool (nth foo_list 1)\<close>
-\<open>13
+ @{ML_response [display, gray]
+\<open>(project_int (nth foo_list 0),
+project_bool (nth foo_list 1))\<close>
+\<open>13,
true\<close>}
Notice that we access the integer as an integer and the boolean as
a boolean. If we attempt to access the integer as a boolean, then we get
a runtime error.
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>project_bool (nth foo_list 0)\<close>
-\<open>*** exception Match raised\<close>}
+\<open>exception Match raised\<close>}
This runtime error is the reason why ML is still type-sound despite
containing a universal type.
@@ -1062,7 +1064,7 @@
\emph{current} theory is updated (this is explained further in
Section~\ref{sec:theories}). The lookup can now be performed as follows.
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>lookup @{theory} "conj"\<close>
\<open>SOME "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"\<close>}
@@ -1073,10 +1075,11 @@
setup %gray \<open>update "conj" @{thm TrueI}\<close>
+
text \<open>
and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}
-@{ML_matchresult_fake [display, gray]
+@{ML_response [display, gray]
\<open>lookup @{theory} "conj"\<close>
\<open>SOME "True"\<close>}
@@ -1271,9 +1274,9 @@
The rules in the list can be retrieved using the function
@{ML FooRules.get}:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>FooRules.get @{context}\<close>
- \<open>["True", "?C","?B"]\<close>}
+ \<open>["True", "?C", "?B"]\<close>}
Note that this function takes a proof context as argument. This might be
confusing, since the theorem list is stored as theory data. It becomes clear by knowing