--- a/ProgTutorial/Advanced.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Advanced.thy Fri May 17 10:38:01 2019 +0200
@@ -132,14 +132,13 @@
\begin{isabelle}
\begin{graybox}
- \isacommand{setup}~\<open>\<verbopen>\<close> @{ML
-"fn thy =>
+ \isacommand{setup}~\<open>\<verbopen>\<close> @{ML \<open>fn thy =>
let
- val bar_const = ((@{binding \"BAR\"}, @{typ \"nat\"}), NoSyn)
+ val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)
val (_, thy') = Sign.declare_const @{context} bar_const thy
in
thy
-end"}~\<open>\<verbclose>\<close>\isanewline
+end\<close>}~\<open>\<verbclose>\<close>\isanewline
\<open>> ERROR: "Stale theory encountered"\<close>
\end{graybox}
\end{isabelle}
@@ -215,14 +214,14 @@
\begin{isabelle}
\begin{graybox}
- @{ML "let
- val trm = @{term \"(x, y, z, w)\"}
+ @{ML \<open>let
+ val trm = @{term "(x, y, z, w)"}
in
pwriteln (Pretty.chunks
[ pretty_term ctxt0 trm,
pretty_term ctxt1 trm,
pretty_term ctxt2 trm ])
-end"}\\
+end\<close>}\\
\setlength{\fboxsep}{0mm}
\<open>>\<close>~\<open>(\<close>\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>x\<close>}}\<open>,\<close>~%
\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>y\<close>}}\<open>,\<close>~%
@@ -241,9 +240,8 @@
The term we are printing is in all three cases the same---a tuple containing
- four free variables. As you can see, however, in case of @{ML "ctxt0"} all
- variables are highlighted indicating a problem, while in case of @{ML
- "ctxt1"} \<open>x\<close> and \<open>y\<close> are printed as normal (blue) free
+ four free variables. As you can see, however, in case of @{ML \<open>ctxt0\<close>} all
+ variables are highlighted indicating a problem, while in case of @{ML \<open>ctxt1\<close>} \<open>x\<close> and \<open>y\<close> are printed as normal (blue) free
variables, but not \<open>z\<close> and \<open>w\<close>. In the last case all variables
are printed as expected. The point of this example is that the context
contains the information which variables are fixed, and designates all other
@@ -253,18 +251,18 @@
fixing a variable twice
@{ML_matchresult_fake [gray, display]
- "@{context}
-|> Variable.add_fixes [\"x\", \"x\"]"
- "ERROR: Duplicate fixed variable(s): \"x\""}
+ \<open>@{context}
+|> Variable.add_fixes ["x", "x"]\<close>
+ \<open>ERROR: Duplicate fixed variable(s): "x"\<close>}
More importantly it also allows us to easily create fresh names for
fixed variables. For this you have to use the function @{ML_ind
variant_fixes in Variable} from the structure @{ML_structure Variable}.
@{ML_matchresult_fake [gray, display]
- "@{context}
-|> Variable.variant_fixes [\"y\", \"y\", \"z\"]"
- "([\"y\", \"ya\", \"z\"], ...)"}
+ \<open>@{context}
+|> Variable.variant_fixes ["y", "y", "z"]\<close>
+ \<open>(["y", "ya", "z"], ...)\<close>}
Now a fresh variant for the second occurence of \<open>y\<close> is created
avoiding any clash. In this way we can also create fresh free variables
@@ -274,16 +272,16 @@
string @{text [quotes] "x"} (Lines 6 and 7).
@{ML_matchresult_fake [display, gray, linenos]
- "let
+ \<open>let
val ctxt0 = @{context}
- val (_, ctxt1) = Variable.add_fixes [\"x\"] ctxt0
- val frees = replicate 2 (\"x\", @{typ nat})
+ val (_, ctxt1) = Variable.add_fixes ["x"] ctxt0
+ val frees = replicate 2 ("x", @{typ nat})
in
(Variable.variant_frees ctxt0 [] frees,
Variable.variant_frees ctxt1 [] frees)
-end"
- "([(\"x\", \"nat\"), (\"xa\", \"nat\")],
- [(\"xa\", \"nat\"), (\"xb\", \"nat\")])"}
+end\<close>
+ \<open>([("x", "nat"), ("xa", "nat")],
+ [("xa", "nat"), ("xb", "nat")])\<close>}
As you can see, if we create the fresh variables with the context \<open>ctxt0\<close>,
then we obtain \<open>x\<close> and \<open>xa\<close>; but in \<open>ctxt1\<close> we obtain \<open>xa\<close>
@@ -294,13 +292,13 @@
function @{ML_ind declare_term in Variable} from the structure @{ML_structure Variable}.
@{ML_matchresult_fake [gray, display]
- "let
- val ctxt1 = Variable.declare_term @{term \"(x, xa)\"} @{context}
- val frees = replicate 2 (\"x\", @{typ nat})
+ \<open>let
+ val ctxt1 = Variable.declare_term @{term "(x, xa)"} @{context}
+ val frees = replicate 2 ("x", @{typ nat})
in
Variable.variant_frees ctxt1 [] frees
-end"
- "[(\"xb\", \"nat\"), (\"xc\", \"nat\")]"}
+end\<close>
+ \<open>[("xb", "nat"), ("xc", "nat")]\<close>}
The result is \<open>xb\<close> and \<open>xc\<close> for the names of the fresh
variables, since \<open>x\<close> and \<open>xa\<close> occur in the term we declared.
@@ -310,12 +308,12 @@
\begin{isabelle}
\begin{graybox}
- @{ML "let
- val trm = @{term \"P x y z\"}
+ @{ML \<open>let
+ val trm = @{term "P x y z"}
val ctxt1 = Variable.declare_term trm @{context}
in
pwriteln (pretty_term ctxt1 trm)
-end"}\\
+end\<close>}\\
\setlength{\fboxsep}{0mm}
\<open>>\<close>~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>P\<close>}}~%
\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>x\<close>}}~%
@@ -330,14 +328,14 @@
@{ML_structure Syntax}. Consider the following code:
@{ML_matchresult_fake [gray, display]
- "let
+ \<open>let
val ctxt0 = @{context}
- val ctxt1 = Variable.declare_term @{term \"x::nat\"} ctxt0
+ val ctxt1 = Variable.declare_term @{term "x::nat"} ctxt0
in
- (Syntax.read_term ctxt0 \"x\",
- Syntax.read_term ctxt1 \"x\")
-end"
- "(Free (\"x\", \"'a\"), Free (\"x\", \"nat\"))"}
+ (Syntax.read_term ctxt0 "x",
+ Syntax.read_term ctxt1 "x")
+end\<close>
+ \<open>(Free ("x", "'a"), Free ("x", "nat"))\<close>}
Parsing the string in the context \<open>ctxt0\<close> results in a free variable
with a default polymorphic type, but in case of \<open>ctxt1\<close> we obtain a
@@ -346,14 +344,14 @@
is made, as the next example illustrates.
@{ML_matchresult_fake [gray, display]
- "let
- val ctxt1 = Variable.declare_term @{term \"x::nat\"} @{context}
- val ctxt2 = Variable.declare_term @{term \"x::int\"} ctxt1
+ \<open>let
+ val ctxt1 = Variable.declare_term @{term "x::nat"} @{context}
+ val ctxt2 = Variable.declare_term @{term "x::int"} ctxt1
in
- (Syntax.read_term ctxt1 \"x\",
- Syntax.read_term ctxt2 \"x\")
-end"
- "(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"}
+ (Syntax.read_term ctxt1 "x",
+ Syntax.read_term ctxt2 "x")
+end\<close>
+ \<open>(Free ("x", "nat"), Free ("x", "int"))\<close>}
The most useful feature of contexts is that one can export, or transfer,
terms and theorems between them. We show this first for terms.
@@ -361,15 +359,15 @@
\begin{isabelle}
\begin{graybox}
\begin{linenos}
- @{ML "let
+ @{ML \<open>let
val ctxt0 = @{context}
- val (_, ctxt1) = Variable.add_fixes [\"x\", \"y\", \"z\"] ctxt0
- val foo_trm = @{term \"P x y z\"}
+ val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0
+ val foo_trm = @{term "P x y z"}
in
singleton (Variable.export_terms ctxt1 ctxt0) foo_trm
|> pretty_term ctxt0
|> pwriteln
-end"}
+end\<close>}
\end{linenos}
\setlength{\fboxsep}{0mm}
\<open>>\<close>~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>P\<close>}}~%
@@ -401,15 +399,15 @@
whether it is actually provable).
@{ML_matchresult_fake [display, gray]
- "let
+ \<open>let
val thy = @{theory}
val ctxt0 = @{context}
- val (_, ctxt1) = Variable.add_fixes [\"P\", \"x\", \"y\", \"z\"] ctxt0
- val foo_thm = Skip_Proof.make_thm thy @{prop \"P x y z x y z\"}
+ val (_, ctxt1) = Variable.add_fixes ["P", "x", "y", "z"] ctxt0
+ val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z x y z"}
in
singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
-end"
- "?P ?x ?y ?z ?x ?y ?z"}
+end\<close>
+ \<open>?P ?x ?y ?z ?x ?y ?z\<close>}
Since we fixed all variables in \<open>ctxt1\<close>, in the exported
result all of them are schematic. The great point of contexts is
@@ -419,14 +417,14 @@
@{ML_structure Assumption}. Consider the following code.
@{ML_matchresult_fake [display, gray, linenos]
- "let
+ \<open>let
val ctxt0 = @{context}
- val ([eq], ctxt1) = Assumption.add_assumes [@{cprop \"x \<equiv> y\"}] ctxt0
+ val ([eq], ctxt1) = Assumption.add_assumes [@{cprop "x \<equiv> y"}] ctxt0
val eq' = Thm.symmetric eq
in
Assumption.export false ctxt1 ctxt0 eq'
-end"
- "x \<equiv> y \<Longrightarrow> y \<equiv> x"}
+end\<close>
+ \<open>x \<equiv> y \<Longrightarrow> y \<equiv> x\<close>}
The function @{ML_ind add_assumes in Assumption} from the structure
@{ML_structure Assumption} adds the assumption \mbox{\<open>x \<equiv> y\<close>}
@@ -451,16 +449,16 @@
in the following example.
@{ML_matchresult_fake [display, gray]
- "let
+ \<open>let
val ctxt0 = @{context}
val ((fvs, [eq]), ctxt1) = ctxt0
- |> Variable.add_fixes [\"x\", \"y\"]
- ||>> Assumption.add_assumes [@{cprop \"x \<equiv> y\"}]
+ |> Variable.add_fixes ["x", "y"]
+ ||>> Assumption.add_assumes [@{cprop "x \<equiv> y"}]
val eq' = Thm.symmetric eq
in
Proof_Context.export ctxt1 ctxt0 [eq']
-end"
- "[?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x]"}
+end\<close>
+ \<open>[?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x]\<close>}
\<close>
@@ -515,7 +513,7 @@
@{ML_type "Proof.context"}, although not every proof context constitutes a
valid local theory.
- @{ML "Context.>> o Context.map_theory"}
+ @{ML \<open>Context.>> o Context.map_theory\<close>}
@{ML_ind "Local_Theory.declaration"}
A similar command is \isacommand{local\_setup}, which expects a function
@@ -590,8 +588,8 @@
antiquotation \<open>@{binding \<dots>}\<close>. For example
@{ML_matchresult [display,gray]
- "@{binding \"name\"}"
- "name"}
+ \<open>@{binding "name"}\<close>
+ \<open>name\<close>}
An example where a qualified name is needed is the function
@{ML_ind define in Local_Theory}. This function is used below to define
@@ -634,7 +632,7 @@
Occasionally you have to calculate what the ``base'' name of a given
constant is. For this you can use the function @{ML_ind Long_Name.base_name}. For example:
- @{ML_matchresult [display,gray] "Long_Name.base_name \"List.list.Nil\"" "\"Nil\""}
+ @{ML_matchresult [display,gray] \<open>Long_Name.base_name "List.list.Nil"\<close> \<open>"Nil"\<close>}
\begin{readmore}
Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
--- a/ProgTutorial/Appendix.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Appendix.thy Fri May 17 10:38:01 2019 +0200
@@ -13,7 +13,7 @@
\begin{itemize}
\item translations/print translations;
- @{ML "Proof_Context.print_syntax"}
+ @{ML \<open>Proof_Context.print_syntax\<close>}
\item user space type systems (in the form that already exists)
--- a/ProgTutorial/Essential.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Essential.thy Fri May 17 10:38:01 2019 +0200
@@ -28,9 +28,9 @@
using the antiquotation \mbox{\<open>@{term \<dots>}\<close>}. For example
@{ML_matchresult [display,gray]
-"@{term \"(a::nat) + b = c\"}"
-"Const (\"HOL.eq\", _) $
- (Const (\"Groups.plus_class.plus\", _) $ _ $ _) $ _"}
+\<open>@{term "(a::nat) + b = c"}\<close>
+\<open>Const ("HOL.eq", _) $
+ (Const ("Groups.plus_class.plus", _) $ _ $ _) $ _\<close>}
constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using
the internal representation corresponding to the datatype @{ML_type_ind "term"},
@@ -54,8 +54,8 @@
variables. For example in
@{ML_matchresult_fake [display, gray]
- "@{term \"\<lambda>x y. x y\"}"
- "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}
+ \<open>@{term "\<lambda>x y. x y"}\<close>
+ \<open>Abs ("x", "'a \<Rightarrow> 'b", Abs ("y", "'a", Bound 1 $ Bound 0))\<close>}
the indices refer to the number of Abstractions (@{ML Abs}) that we need to
skip until we hit the @{ML Abs} that binds the corresponding
@@ -70,25 +70,25 @@
term shown above:
@{ML_matchresult_fake [display, gray]
-"@{term \"\<lambda>x y. x y\"}
+\<open>@{term "\<lambda>x y. x y"}
|> pretty_term @{context}
- |> pwriteln"
- "\<lambda>x. x"}
+ |> pwriteln\<close>
+ \<open>\<lambda>x. x\<close>}
This is one common source for puzzlement in Isabelle, which has
tacitly eta-contracted the output. You obtain a similar result
with beta-redexes
@{ML_matchresult_fake [display, gray]
-"let
- val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"}
- val arg1 = @{term \"1::int\"}
- val arg2 = @{term \"2::int\"}
+\<open>let
+ val redex = @{term "(\<lambda>(x::int) (y::int). x)"}
+ val arg1 = @{term "1::int"}
+ val arg2 = @{term "2::int"}
in
pretty_term @{context} (redex $ arg1 $ arg2)
|> pwriteln
-end"
- "1"}
+end\<close>
+ \<open>1\<close>}
There is a dedicated configuration value for switching off tacit
eta-contractions, namely @{ML_ind eta_contract in Syntax} (see Section
@@ -98,16 +98,16 @@
@{ML_matchresult_fake [display, gray]
- "let
- val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"}
- val arg1 = @{term \"1::int\"}
- val arg2 = @{term \"2::int\"}
+ \<open>let
+ val redex = @{term "(\<lambda>(x::int) (y::int). x)"}
+ val arg1 = @{term "1::int"}
+ val arg2 = @{term "2::int"}
val ctxt = Config.put show_abbrevs false @{context}
in
pretty_term ctxt (redex $ arg1 $ arg2)
|> pwriteln
-end"
- "(\<lambda>x y. x) 1 2"}
+end\<close>
+ \<open>(\<lambda>x y. x) 1 2\<close>}
Isabelle makes a distinction between \emph{free} variables (term-constructor
@{ML Free} and written on the user level in blue colour) and
@@ -115,15 +115,15 @@
leading question mark). Consider the following two examples
@{ML_matchresult_fake [display, gray]
-"let
- val v1 = Var ((\"x\", 3), @{typ bool})
- val v2 = Var ((\"x1\", 3), @{typ bool})
- val v3 = Free (\"x\", @{typ bool})
+\<open>let
+ val v1 = Var (("x", 3), @{typ bool})
+ val v2 = Var (("x1", 3), @{typ bool})
+ val v3 = Free ("x", @{typ bool})
in
pretty_terms @{context} [v1, v2, v3]
|> pwriteln
-end"
-"?x3, ?x1.3, x"}
+end\<close>
+\<open>?x3, ?x1.3, x\<close>}
When constructing terms, you are usually concerned with free
variables (as mentioned earlier, you cannot construct schematic
@@ -145,19 +145,19 @@
terms can be constructed. For example
@{ML_matchresult_fake_both [display,gray]
- "@{term \"x x\"}"
- "Type unification failed: Occurs check!"}
+ \<open>@{term "x x"}\<close>
+ \<open>Type unification failed: Occurs check!\<close>}
raises a typing error, while it is perfectly ok to construct the term
with the raw ML-constructors:
@{ML_matchresult_fake [display,gray]
-"let
- val omega = Free (\"x\", @{typ \"nat \<Rightarrow> nat\"}) $ Free (\"x\", @{typ nat})
+\<open>let
+ val omega = Free ("x", @{typ "nat \<Rightarrow> nat"}) $ Free ("x", @{typ nat})
in
pwriteln (pretty_term @{context} omega)
-end"
- "x x"}
+end\<close>
+ \<open>x x\<close>}
Sometimes the internal representation of terms can be surprisingly different
from what you see at the user-level, because the layers of
@@ -186,15 +186,15 @@
usually invisible \<open>Trueprop\<close>-coercions whenever necessary.
Consider for example the pairs
-@{ML_matchresult [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})"
-"(Free (\"P\", _) $ Free (\"x\", _),
- Const (\"HOL.Trueprop\", _) $ (Free (\"P\", _) $ Free (\"x\", _)))"}
+@{ML_matchresult [display,gray] \<open>(@{term "P x"}, @{prop "P x"})\<close>
+\<open>(Free ("P", _) $ Free ("x", _),
+ Const ("HOL.Trueprop", _) $ (Free ("P", _) $ Free ("x", _)))\<close>}
where a coercion is inserted in the second component and
- @{ML_matchresult [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
- "(Const (\"Pure.imp\", _) $ _ $ _,
- Const (\"Pure.imp\", _) $ _ $ _)"}
+ @{ML_matchresult [display,gray] \<open>(@{term "P x \<Longrightarrow> Q x"}, @{prop "P x \<Longrightarrow> Q x"})\<close>
+ \<open>(Const ("Pure.imp", _) $ _ $ _,
+ Const ("Pure.imp", _) $ _ $ _)\<close>}
where it is not (since it is already constructed by a meta-implication).
The purpose of the \<open>Trueprop\<close>-coercion is to embed formulae of
@@ -204,7 +204,7 @@
As already seen above, types can be constructed using the antiquotation
\<open>@{typ _}\<close>. For example:
- @{ML_matchresult_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
+ @{ML_matchresult_fake [display,gray] \<open>@{typ "bool \<Rightarrow> nat"}\<close> \<open>bool \<Rightarrow> nat\<close>}
The corresponding datatype is
\<close>
@@ -216,8 +216,8 @@
text \<open>
Like with terms, there is the distinction between free type
- variables (term-constructor @{ML "TFree"}) and schematic
- type variables (term-constructor @{ML "TVar"} and printed with
+ variables (term-constructor @{ML \<open>TFree\<close>}) and schematic
+ type variables (term-constructor @{ML \<open>TVar\<close>} and printed with
a leading question mark). A type constant,
like @{typ "int"} or @{typ bool}, are types with an empty list
of argument types. However, it needs a bit of effort to show an
@@ -225,8 +225,8 @@
Using just the antiquotation \<open>@{typ "bool"}\<close> we only see
@{ML_matchresult [display, gray]
- "@{typ \"bool\"}"
- "bool"}
+ \<open>@{typ "bool"}\<close>
+ \<open>bool\<close>}
which is the pretty printed version of \<open>bool\<close>. However, in PolyML
(version \<open>\<ge>\<close>5.3) it is easy to install your own pretty printer. With the
function below we mimic the behaviour of the usual pretty printer for
@@ -264,14 +264,14 @@
Now the type bool is printed out in full detail.
@{ML_matchresult [display,gray]
- "@{typ \"bool\"}"
- "Type (\"HOL.bool\", [])"}
+ \<open>@{typ "bool"}\<close>
+ \<open>Type ("HOL.bool", [])\<close>}
When printing out a list-type
@{ML_matchresult [display,gray]
- "@{typ \"'a list\"}"
- "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"}
+ \<open>@{typ "'a list"}\<close>
+ \<open>Type ("List.list", [TFree ("'a", ["HOL.type"])])\<close>}
we can see the full name of the type is actually \<open>List.list\<close>, indicating
that it is defined in the theory \<open>List\<close>. However, one has to be
@@ -280,8 +280,8 @@
still represented by its simple name.
@{ML_matchresult [display,gray]
- "@{typ \"bool \<Rightarrow> nat\"}"
- "Type (\"fun\", [Type (\"HOL.bool\", []), Type (\"Nat.nat\", [])])"}
+ \<open>@{typ "bool \<Rightarrow> nat"}\<close>
+ \<open>Type ("fun", [Type ("HOL.bool", []), Type ("Nat.nat", [])])\<close>}
We can restore the usual behaviour of Isabelle's pretty printer
with the code
@@ -295,10 +295,10 @@
the standard Isabelle way.
@{ML_matchresult_fake [display, gray]
- "@{typ \"bool\"};
-@{typ \"'a list\"}"
- "\"bool\"
-\"'a List.list\""}
+ \<open>@{typ "bool"};
+@{typ "'a list"}\<close>
+ \<open>"bool"
+"'a List.list"\<close>}
\begin{readmore}
Types are described in detail in \isccite{sec:types}. Their
@@ -338,19 +338,19 @@
to both functions. With @{ML make_imp} you obtain the intended term involving
the given arguments
- @{ML_matchresult [display,gray] "make_imp @{term S} @{term T}"
-"Const _ $
- Abs (\"x\", Type (\"Nat.nat\",[]),
- Const _ $ (Free (\"S\",_) $ _) $ (Free (\"T\",_) $ _))"}
+ @{ML_matchresult [display,gray] \<open>make_imp @{term S} @{term T}\<close>
+\<open>Const _ $
+ Abs ("x", Type ("Nat.nat",[]),
+ Const _ $ (Free ("S",_) $ _) $ (Free ("T",_) $ _))\<close>}
whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"}
and \<open>Q\<close> from the antiquotation.
- @{ML_matchresult [display,gray] "make_wrong_imp @{term S} @{term T}"
-"Const _ $
- Abs (\"x\", _,
- Const _ $ (Const _ $ (Free (\"P\",_) $ _)) $
- (Const _ $ (Free (\"Q\",_) $ _)))"}
+ @{ML_matchresult [display,gray] \<open>make_wrong_imp @{term S} @{term T}\<close>
+\<open>Const _ $
+ Abs ("x", _,
+ Const _ $ (Const _ $ (Free ("P",_) $ _)) $
+ (Const _ $ (Free ("Q",_) $ _)))\<close>}
There are a number of handy functions that are frequently used for
constructing terms. One is the function @{ML_ind list_comb in Term}, which
@@ -359,28 +359,28 @@
@{ML_matchresult_fake [display,gray]
-"let
- val trm = @{term \"P::bool \<Rightarrow> bool \<Rightarrow> bool\"}
- val args = [@{term \"True\"}, @{term \"False\"}]
+\<open>let
+ val trm = @{term "P::bool \<Rightarrow> bool \<Rightarrow> bool"}
+ val args = [@{term "True"}, @{term "False"}]
in
list_comb (trm, args)
-end"
-"Free (\"P\", \"bool \<Rightarrow> bool \<Rightarrow> bool\")
- $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
+end\<close>
+\<open>Free ("P", "bool \<Rightarrow> bool \<Rightarrow> bool")
+ $ Const ("True", "bool") $ Const ("False", "bool")\<close>}
Another handy function is @{ML_ind lambda in Term}, which abstracts a variable
in a term. For example
@{ML_matchresult_fake [display,gray]
-"let
- val x_nat = @{term \"x::nat\"}
- val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
+\<open>let
+ val x_nat = @{term "x::nat"}
+ val trm = @{term "(P::nat \<Rightarrow> bool) x"}
in
lambda x_nat trm
-end"
- "Abs (\"x\", \"Nat.nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
-
- In this example, @{ML lambda} produces a de Bruijn index (i.e.\ @{ML "Bound 0"}),
+end\<close>
+ \<open>Abs ("x", "Nat.nat", Free ("P", "bool \<Rightarrow> bool") $ Bound 0)\<close>}
+
+ In this example, @{ML lambda} produces a de Bruijn index (i.e.\ @{ML \<open>Bound 0\<close>}),
and an abstraction, where it also records the type of the abstracted
variable and for printing purposes also its name. Note that because of the
typing annotation on \<open>P\<close>, the variable \<open>x\<close> in \<open>P x\<close>
@@ -388,13 +388,13 @@
as in
@{ML_matchresult_fake [display,gray]
-"let
- val x_int = @{term \"x::int\"}
- val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
+\<open>let
+ val x_int = @{term "x::int"}
+ val trm = @{term "(P::nat \<Rightarrow> bool) x"}
in
lambda x_int trm
-end"
- "Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
+end\<close>
+ \<open>Abs ("x", "int", Free ("P", "nat \<Rightarrow> bool") $ Free ("x", "nat"))\<close>}
then the variable \<open>Free ("x", "nat")\<close> is \emph{not} abstracted.
This is a fundamental principle
@@ -407,26 +407,26 @@
@{term y}, and @{term x} by @{term True}.
@{ML_matchresult_fake [display,gray]
-"let
- val sub1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
- val sub2 = (@{term \"x::nat\"}, @{term \"True\"})
- val trm = @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
+\<open>let
+ val sub1 = (@{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"}, @{term "y::nat \<Rightarrow> nat"})
+ val sub2 = (@{term "x::nat"}, @{term "True"})
+ val trm = @{term "((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x"}
in
subst_free [sub1, sub2] trm
-end"
- "Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}
+end\<close>
+ \<open>Free ("y", "nat \<Rightarrow> nat") $ Const ("True", "bool")\<close>}
As can be seen, @{ML subst_free} does not take typability into account.
However it takes alpha-equivalence into account:
@{ML_matchresult_fake [display, gray]
-"let
- val sub = (@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})
- val trm = @{term \"(\<lambda>x::nat. x)\"}
+\<open>let
+ val sub = (@{term "(\<lambda>y::nat. y)"}, @{term "x::nat"})
+ val trm = @{term "(\<lambda>x::nat. x)"}
in
subst_free [sub] trm
-end"
- "Free (\"x\", \"nat\")"}
+end\<close>
+ \<open>Free ("x", "nat")\<close>}
Similarly the function @{ML_ind subst_bounds in Term}, replaces lose bound
variables with terms. To see how this function works, let us implement a
@@ -447,9 +447,9 @@
the body of the universal quantification. For example
@{ML_matchresult_fake [display, gray]
- "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"
-"([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
- Const (\"op =\", _) $ Bound 1 $ Bound 0)"}
+ \<open>strip_alls @{term "\<forall>x y. x = (y::bool)"}\<close>
+\<open>([Free ("x", "bool"), Free ("y", "bool")],
+ Const ("op =", _) $ Bound 1 $ Bound 0)\<close>}
Note that we produced in the body two dangling de Bruijn indices.
Later on we will also use the inverse function that
@@ -467,19 +467,19 @@
loose @{ML_ind Bound in Term}s with the stripped off variables.
@{ML_matchresult_fake [display, gray, linenos]
- "let
- val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}
+ \<open>let
+ val (vrs, trm) = strip_alls @{term "\<forall>x y. x = (y::bool)"}
in
subst_bounds (rev vrs, trm)
|> pretty_term @{context}
|> pwriteln
-end"
- "x = y"}
+end\<close>
+ \<open>x = y\<close>}
Note that in Line 4 we had to reverse the list of variables that @{ML
strip_alls} returned. The reason is that the head of the list the function
- @{ML subst_bounds} takes is the replacement for @{ML "Bound 0"}, the next
- element for @{ML "Bound 1"} and so on.
+ @{ML subst_bounds} takes is the replacement for @{ML \<open>Bound 0\<close>}, the next
+ element for @{ML \<open>Bound 1\<close>} and so on.
Notice also that this function might introduce name clashes, since we
substitute just a variable with the name recorded in an abstraction. This
@@ -489,12 +489,12 @@
@{ML_matchresult_fake [display,gray]
- "let
- val body = Bound 0 $ Free (\"x\", @{typ nat})
+ \<open>let
+ val body = Bound 0 $ Free ("x", @{typ nat})
in
- Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body)
-end"
- "(\"xa\", Free (\"xa\", \"Nat.nat \<Rightarrow> bool\") $ Free (\"x\", \"Nat.nat\"))"}
+ Term.dest_abs ("x", @{typ "nat \<Rightarrow> bool"}, body)
+end\<close>
+ \<open>("xa", Free ("xa", "Nat.nat \<Rightarrow> bool") $ Free ("x", "Nat.nat"))\<close>}
Sometimes it is necessary to manipulate de Bruijn indices in terms directly.
There are many functions to do this. We describe only two. The first,
@@ -502,13 +502,13 @@
of the loose bound variables in a term. In the code below
@{ML_matchresult_fake [display,gray]
-"@{term \"\<forall>x y z u. z = u\"}
+\<open>@{term "\<forall>x y z u. z = u"}
|> strip_alls
||> incr_boundvars 2
|> build_alls
|> pretty_term @{context}
- |> pwriteln"
- "\<forall>x y z u. x = y"}
+ |> pwriteln\<close>
+ \<open>\<forall>x y z u. x = y\<close>}
we first strip off the forall-quantified variables (thus creating two loose
bound variables in the body); then we increase the indices of the loose
@@ -520,14 +520,14 @@
contains a loose bound of a certain index. For example
@{ML_matchresult_fake [gray,display]
-"let
- val body = snd (strip_alls @{term \"\<forall>x y. x = (y::bool)\"})
+\<open>let
+ val body = snd (strip_alls @{term "\<forall>x y. x = (y::bool)"})
in
[loose_bvar1 (body, 0),
loose_bvar1 (body, 1),
loose_bvar1 (body, 2)]
-end"
- "[true, true, false]"}
+end\<close>
+ \<open>[true, true, false]\<close>}
There are also many convenient functions that construct specific HOL-terms
in the structure @{ML_structure HOLogic}. For example @{ML_ind mk_eq in
@@ -535,13 +535,13 @@
equality are calculated from the type of the arguments. For example
@{ML_matchresult_fake [gray,display]
-"let
- val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
+\<open>let
+ val eq = HOLogic.mk_eq (@{term "True"}, @{term "False"})
in
eq |> pretty_term @{context}
|> pwriteln
-end"
- "True = False"}
+end\<close>
+ \<open>True = False\<close>}
\begin{readmore}
There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file
@@ -569,7 +569,7 @@
text \<open>
will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}:
- @{ML_matchresult [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
+ @{ML_matchresult [display,gray] \<open>is_all @{term "\<forall>x::nat. P x"}\<close> \<open>false\<close>}
The problem is that the \<open>@term\<close>-antiquotation in the pattern
fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for
@@ -583,7 +583,7 @@
text \<open>
because now
- @{ML_matchresult [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
+ @{ML_matchresult [display,gray] \<open>is_all @{term "\<forall>x::nat. P x"}\<close> \<open>true\<close>}
matches correctly (the first wildcard in the pattern matches any type and the
second any term).
@@ -598,14 +598,14 @@
text \<open>
Unfortunately, also this function does \emph{not} work as expected, since
- @{ML_matchresult [display,gray] "is_nil @{term \"Nil\"}" "false"}
+ @{ML_matchresult [display,gray] \<open>is_nil @{term "Nil"}\<close> \<open>false\<close>}
The problem is that on the ML-level the name of a constant is more
subtle than you might expect. The function @{ML is_all} worked correctly,
because @{term "All"} is such a fundamental constant, which can be referenced
- by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at
-
- @{ML_matchresult [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", _)"}
+ by @{ML \<open>Const ("All", some_type)\<close> for some_type}. However, if you look at
+
+ @{ML_matchresult [display,gray] \<open>@{term "Nil"}\<close> \<open>Const ("List.list.Nil", _)\<close>}
the name of the constant \<open>Nil\<close> depends on the theory in which the
term constructor is defined (\<open>List\<close>) and also in which datatype
@@ -613,12 +613,12 @@
type-classes. Consider for example the constants for @{term "zero"} and
\mbox{@{term "times"}}:
- @{ML_matchresult [display,gray] "(@{term \"0::nat\"}, @{term \"times\"})"
- "(Const (\"Groups.zero_class.zero\", _),
- Const (\"Groups.times_class.times\", _))"}
+ @{ML_matchresult [display,gray] \<open>(@{term "0::nat"}, @{term "times"})\<close>
+ \<open>(Const ("Groups.zero_class.zero", _),
+ Const ("Groups.times_class.times", _))\<close>}
While you could use the complete name, for example
- @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
+ @{ML \<open>Const ("List.list.Nil", some_type)\<close> for some_type}, for referring to or
matching against \<open>Nil\<close>, this would make the code rather brittle.
The reason is that the theory and the name of the datatype can easily change.
To make the code more robust, it is better to use the antiquotation
@@ -637,7 +637,7 @@
For example
@{ML_matchresult [display,gray]
- "@{type_name \"list\"}" "\"List.list\""}
+ \<open>@{type_name "list"}\<close> \<open>"List.list"\<close>}
Although types of terms can often be inferred, there are many
situations where you need to construct types manually, especially
@@ -675,9 +675,9 @@
Here is an example:
@{ML_matchresult_fake [display,gray]
-"map_types nat_to_int @{term \"a = (1::nat)\"}"
-"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
- $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
+\<open>map_types nat_to_int @{term "a = (1::nat)"}\<close>
+\<open>Const ("op =", "int \<Rightarrow> int \<Rightarrow> bool")
+ $ Free ("a", "int") $ Const ("HOL.one_class.one", "int")\<close>}
If you want to obtain the list of free type-variables of a term, you
can use the function @{ML_ind add_tfrees in Term}
@@ -692,8 +692,8 @@
call them as follows
@{ML_matchresult [gray,display]
- "Term.add_tfrees @{term \"(a, b)\"} []"
- "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
+ \<open>Term.add_tfrees @{term "(a, b)"} []\<close>
+ \<open>[("'b", ["HOL.type"]), ("'a", ["HOL.type"])]\<close>}
The reason for this definition is that @{ML add_tfrees in Term} can
be easily folded over a list of terms. Similarly for all functions
@@ -799,9 +799,9 @@
structure @{ML_structure Vartab}.
@{ML_matchresult_fake [display,gray]
- "Vartab.dest tyenv_unif"
- "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")),
- ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"}
+ \<open>Vartab.dest tyenv_unif\<close>
+ \<open>[(("'a", 0), (["HOL.type"], "?'b List.list")),
+ (("'b", 0), (["HOL.type"], "nat"))]\<close>}
\<close>
text_raw \<open>
@@ -833,15 +833,15 @@
text \<open>
The first components in this list stand for the schematic type variables and
the second are the associated sorts and types. In this example the sort is
- the default sort \<open>HOL.type\<close>. Instead of @{ML "Vartab.dest"}, we will
+ the default sort \<open>HOL.type\<close>. Instead of @{ML \<open>Vartab.dest\<close>}, we will
use in what follows our own pretty-printing function from
Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s. For the type
environment in the example this function prints out the more legible:
@{ML_matchresult_fake [display, gray]
- "pretty_tyenv @{context} tyenv_unif"
- "[?'a := ?'b list, ?'b := nat]"}
+ \<open>pretty_tyenv @{context} tyenv_unif\<close>
+ \<open>[?'a := ?'b list, ?'b := nat]\<close>}
The way the unification function @{ML typ_unify in Sign} is implemented
using an initial type environment and initial index makes it easy to
@@ -883,8 +883,8 @@
true. This allows us to inspect the typing environment.
@{ML_matchresult_fake [display,gray]
- "pretty_tyenv @{context} tyenv"
- "[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]"}
+ \<open>pretty_tyenv @{context} tyenv\<close>
+ \<open>[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]\<close>}
As can be seen, the type variables \<open>?'a\<close> and \<open>?'b\<close> are instantiated
with a new type variable \<open>?'a1\<close> with sort \<open>{s1, s2}\<close>. Since a new
@@ -892,16 +892,16 @@
has been increased to \<open>1\<close>.
@{ML_matchresult [display,gray]
- "index"
- "1"}
+ \<open>index\<close>
+ \<open>1\<close>}
Let us now return to the unification problem \<open>?'a * ?'b\<close> and
\<open>?'b list * nat\<close> from the beginning of this section, and the
calculated type environment @{ML tyenv_unif}:
@{ML_matchresult_fake [display, gray]
- "pretty_tyenv @{context} tyenv_unif"
- "[?'a := ?'b list, ?'b := nat]"}
+ \<open>pretty_tyenv @{context} tyenv_unif\<close>
+ \<open>[?'a := ?'b list, ?'b := nat]\<close>}
Observe that the type environment which the function @{ML typ_unify in
Sign} returns is \emph{not} an instantiation in fully solved form: while \<open>?'b\<close> is instantiated to @{typ nat}, this is not propagated to the
@@ -912,8 +912,8 @@
?'b\<close>, you should use the function @{ML_ind norm_type in Envir}:
@{ML_matchresult_fake [display, gray]
- "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
- "nat list * nat"}
+ \<open>Envir.norm_type tyenv_unif @{typ_pat "?'a * ?'b"}\<close>
+ \<open>nat list * nat\<close>}
Matching of types can be done with the function @{ML_ind typ_match in Sign}
also from the structure @{ML_structure Sign}. This function returns a @{ML_type
@@ -932,16 +932,16 @@
Printing out the calculated matcher gives
@{ML_matchresult_fake [display,gray]
- "pretty_tyenv @{context} tyenv_match"
- "[?'a := bool list, ?'b := nat]"}
+ \<open>pretty_tyenv @{context} tyenv_match\<close>
+ \<open>[?'a := bool list, ?'b := nat]\<close>}
Unlike unification, which uses the function @{ML norm_type in Envir},
applying the matcher to a type needs to be done with the function
@{ML_ind subst_type in Envir}. For example
@{ML_matchresult_fake [display, gray]
- "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"
- "bool list * nat"}
+ \<open>Envir.subst_type tyenv_match @{typ_pat "?'a * ?'b"}\<close>
+ \<open>bool list * nat\<close>}
Be careful to observe the difference: always use
@{ML subst_type in Envir} for matchers and @{ML norm_type in Envir}
@@ -961,15 +961,15 @@
@{ML norm_type in Envir} to the type \<open>?'a * ?'b\<close> we obtain
@{ML_matchresult_fake [display, gray]
- "Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}"
- "nat list * nat"}
+ \<open>Envir.norm_type tyenv_match' @{typ_pat "?'a * ?'b"}\<close>
+ \<open>nat list * nat\<close>}
which does not solve the matching problem, and if
we apply @{ML subst_type in Envir} to the same type we obtain
@{ML_matchresult_fake [display, gray]
- "Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
- "?'b list * nat"}
+ \<open>Envir.subst_type tyenv_unif @{typ_pat "?'a * ?'b"}\<close>
+ \<open>?'b list * nat\<close>}
which does not solve the unification problem.
@@ -1024,8 +1024,8 @@
resulting term environment is
@{ML_matchresult_fake [display, gray]
- "pretty_env @{context} fo_env"
- "[?X := P, ?Y := \<lambda>a b. Q b a]"}
+ \<open>pretty_env @{context} fo_env\<close>
+ \<open>[?X := P, ?Y := \<lambda>a b. Q b a]\<close>}
The matcher can be applied to a term using the function @{ML_ind subst_term
in Envir} (remember the same convention for types applies to terms: @{ML
@@ -1034,14 +1034,14 @@
which is set to empty in the example below, and a term environment.
@{ML_matchresult_fake [display, gray]
- "let
- val trm = @{term_pat \"(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y\"}
+ \<open>let
+ val trm = @{term_pat "(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}
in
Envir.subst_term (Vartab.empty, fo_env) trm
|> pretty_term @{context}
|> pwriteln
-end"
- "P (\<lambda>a b. Q b a)"}
+end\<close>
+ \<open>P (\<lambda>a b. Q b a)\<close>}
First-order matching is useful for matching against applications and
variables. It can also deal with abstractions and a limited form of
@@ -1051,16 +1051,16 @@
case, first-order matching produces \<open>[?X := P]\<close>.
@{ML_matchresult_fake [display, gray]
- "let
- val fo_pat = @{term_pat \"\<lambda>y. (?X::nat\<Rightarrow>bool) y\"}
- val trm = @{term \"\<lambda>x. (P::nat\<Rightarrow>bool) x\"}
+ \<open>let
+ val fo_pat = @{term_pat "\<lambda>y. (?X::nat\<Rightarrow>bool) y"}
+ val trm = @{term "\<lambda>x. (P::nat\<Rightarrow>bool) x"}
val init = (Vartab.empty, Vartab.empty)
in
Pattern.first_order_match @{theory} (fo_pat, trm) init
|> snd
|> pretty_env @{context}
-end"
- "[?X := P]"}
+end\<close>
+ \<open>[?X := P]\<close>}
\<close>
text \<open>
@@ -1076,18 +1076,18 @@
that it is beta-normal, well-typed and has no loose bound variables.
@{ML_matchresult [display, gray]
- "let
+ \<open>let
val trm_list =
- [@{term_pat \"?X\"}, @{term_pat \"a\"},
- @{term_pat \"f (\<lambda>a b. ?X a b) c\"},
- @{term_pat \"\<lambda>a b. (+) a b\"},
- @{term_pat \"\<lambda>a. (+) a ?Y\"}, @{term_pat \"?X ?Y\"},
- @{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"},
- @{term_pat \"?X a\"}]
+ [@{term_pat "?X"}, @{term_pat "a"},
+ @{term_pat "f (\<lambda>a b. ?X a b) c"},
+ @{term_pat "\<lambda>a b. (+) a b"},
+ @{term_pat "\<lambda>a. (+) a ?Y"}, @{term_pat "?X ?Y"},
+ @{term_pat "\<lambda>a b. ?X a b ?Y"}, @{term_pat "\<lambda>a. ?X a a"},
+ @{term_pat "?X a"}]
in
map Pattern.pattern trm_list
-end"
- "[true, true, true, true, true, false, false, false, false]"}
+end\<close>
+ \<open>[true, true, true, true, true, false, false, false, false]\<close>}
The point of the restriction to patterns is that unification and matching
are decidable and produce most general unifiers, respectively matchers.
@@ -1102,15 +1102,15 @@
@{ML_structure Pattern}. An example for higher-order pattern unification is
@{ML_matchresult_fake [display, gray]
- "let
- val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"}
- val trm2 = @{term_pat \"\<lambda>u v. g u (f u)\"}
+ \<open>let
+ val trm1 = @{term_pat "\<lambda>x y. g (?X y x) (f (?Y x))"}
+ val trm2 = @{term_pat "\<lambda>u v. g u (f u)"}
val init = Envir.empty 0
val env = Pattern.unify (Context.Proof @{context}) (trm1, trm2) init (* FIXME: Reference to generic context *)
in
pretty_env @{context} (Envir.term_env env)
-end"
- "[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]"}
+end\<close>
+ \<open>[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]\<close>}
The function @{ML_ind "Envir.empty"} generates a record with a specified
max-index for the schematic variables (in the example the index is \<open>0\<close>) and empty type and term environments. The function @{ML_ind
@@ -1153,27 +1153,27 @@
We can print them out as follows.
@{ML_matchresult_fake [display, gray]
- "pretty_env @{context} (Envir.term_env un1);
+ \<open>pretty_env @{context} (Envir.term_env un1);
pretty_env @{context} (Envir.term_env un2);
-pretty_env @{context} (Envir.term_env un3)"
- "[?X := \<lambda>a. a, ?Y := f a]
+pretty_env @{context} (Envir.term_env un3)\<close>
+ \<open>[?X := \<lambda>a. a, ?Y := f a]
[?X := f, ?Y := a]
-[?X := \<lambda>b. f a]"}
+[?X := \<lambda>b. f a]\<close>}
In case of failure the function @{ML_ind unifiers in Unify} does not raise
an exception, rather returns the empty sequence. For example
@{ML_matchresult [display, gray]
-"let
- val trm1 = @{term \"a\"}
- val trm2 = @{term \"b\"}
+\<open>let
+ val trm1 = @{term "a"}
+ val trm2 = @{term "b"}
val init = Envir.empty 0
in
Unify.unifiers (Context.Proof @{context}, init, [(trm1, trm2)])
|> Seq.pull
-end"
-"NONE"}
+end\<close>
+\<open>NONE\<close>}
In order to find a reasonable solution for a unification problem, Isabelle
also tries first to solve the problem by higher-order pattern
@@ -1182,8 +1182,8 @@
manipulated as a configuration value. For example
@{ML_matchresult_fake [display,gray]
- "Config.get_global @{theory} (Unify.search_bound)"
- "Int 60"}
+ \<open>Config.get_global @{theory} (Unify.search_bound)\<close>
+ \<open>Int 60\<close>}
If this bound is reached during unification, Isabelle prints out the
warning message @{text [quotes] "Unification bound exceeded"} and
@@ -1267,14 +1267,14 @@
@{ML_matchresult_fake [gray,display,linenos]
- "let
+ \<open>let
val pat = Logic.strip_imp_concl (Thm.prop_of @{thm spec})
- val trm = @{term \"Trueprop (Q True)\"}
+ val trm = @{term "Trueprop (Q True)"}
val inst = matcher_inst @{context} pat trm 1
in
Drule.instantiate_normalize inst @{thm spec}
-end"
- "\<forall>x. Q x \<Longrightarrow> Q True"}
+end\<close>
+ \<open>\<forall>x. Q x \<Longrightarrow> Q True\<close>}
Note that we had to insert a \<open>Trueprop\<close>-coercion in Line 3 since the
conclusion of @{thm [source] spec} contains one.
@@ -1355,28 +1355,28 @@
type of a term. Consider for example:
@{ML_matchresult [display,gray]
- "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
+ \<open>type_of (@{term "f::nat \<Rightarrow> bool"} $ @{term "x::nat"})\<close> \<open>bool\<close>}
To calculate the type, this function traverses the whole term and will
detect any typing inconsistency. For example changing the type of the variable
@{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message:
@{ML_matchresult_fake [display,gray]
- "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})"
- "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
+ \<open>type_of (@{term "f::nat \<Rightarrow> bool"} $ @{term "x::int"})\<close>
+ \<open>*** Exception- TYPE ("type_of: type mismatch in application" \<dots>\<close>}
Since the complete traversal might sometimes be too costly and
not necessary, there is the function @{ML_ind fastype_of in Term}, which
also returns the type of a term.
@{ML_matchresult [display,gray]
- "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
+ \<open>fastype_of (@{term "f::nat \<Rightarrow> bool"} $ @{term "x::nat"})\<close> \<open>bool\<close>}
However, efficiency is gained on the expense of skipping some tests. You
can see this in the following example
@{ML_matchresult [display,gray]
- "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}
+ \<open>fastype_of (@{term "f::nat \<Rightarrow> bool"} $ @{term "x::int"})\<close> \<open>bool\<close>}
where no error is detected.
@@ -1388,15 +1388,15 @@
@{ML_ind check_term in Syntax}. An example is as follows:
@{ML_matchresult_fake [display,gray]
-"let
- val c = Const (@{const_name \"plus\"}, dummyT)
- val o = @{term \"1::nat\"}
- val v = Free (\"x\", dummyT)
+\<open>let
+ val c = Const (@{const_name "plus"}, dummyT)
+ val o = @{term "1::nat"}
+ val v = Free ("x", dummyT)
in
Syntax.check_term @{context} (c $ o $ v)
-end"
-"Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
- Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
+end\<close>
+\<open>Const ("HOL.plus_class.plus", "nat \<Rightarrow> nat \<Rightarrow> nat") $
+ Const ("HOL.one_class.one", "nat") $ Free ("x", "nat")\<close>}
Instead of giving explicitly the type for the constant \<open>plus\<close> and the free
variable \<open>x\<close>, type-inference fills in the missing information.
@@ -1433,67 +1433,67 @@
write:
@{ML_matchresult_fake [display,gray]
- "Thm.cterm_of @{context} @{term \"(a::nat) + b = c\"}"
- "a + b = c"}
+ \<open>Thm.cterm_of @{context} @{term "(a::nat) + b = c"}\<close>
+ \<open>a + b = c\<close>}
This can also be written with an antiquotation:
@{ML_matchresult_fake [display,gray]
- "@{cterm \"(a::nat) + b = c\"}"
- "a + b = c"}
+ \<open>@{cterm "(a::nat) + b = c"}\<close>
+ \<open>a + b = c\<close>}
Attempting to obtain the certified term for
@{ML_matchresult_fake_both [display,gray]
- "@{cterm \"1 + True\"}"
- "Type unification failed \<dots>"}
+ \<open>@{cterm "1 + True"}\<close>
+ \<open>Type unification failed \<dots>\<close>}
yields an error (since the term is not typable). A slightly more elaborate
example that type-checks is:
@{ML_matchresult_fake [display,gray]
-"let
- val natT = @{typ \"nat\"}
- val zero = @{term \"0::nat\"}
+\<open>let
+ val natT = @{typ "nat"}
+ val zero = @{term "0::nat"}
val plus = Const (@{const_name plus}, [natT, natT] ---> natT)
in
Thm.cterm_of @{context} (plus $ zero $ zero)
-end"
- "0 + 0"}
+end\<close>
+ \<open>0 + 0\<close>}
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 \<Rightarrow> bool"} on
the ML-level as follows:
@{ML_matchresult_fake [display,gray]
- "Thm.ctyp_of @{context} (@{typ nat} --> @{typ bool})"
- "nat \<Rightarrow> bool"}
+ \<open>Thm.ctyp_of @{context} (@{typ nat} --> @{typ bool})\<close>
+ \<open>nat \<Rightarrow> bool\<close>}
or with the antiquotation:
@{ML_matchresult_fake [display,gray]
- "@{ctyp \"nat \<Rightarrow> bool\"}"
- "nat \<Rightarrow> bool"}
+ \<open>@{ctyp "nat \<Rightarrow> bool"}\<close>
+ \<open>nat \<Rightarrow> bool\<close>}
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 apply in Thm} produces a certified application.
@{ML_matchresult_fake [display,gray]
- "Thm.apply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}"
- "P 3"}
+ \<open>Thm.apply @{cterm "P::nat \<Rightarrow> bool"} @{cterm "3::nat"}\<close>
+ \<open>P 3\<close>}
Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_structure Drule}
applies a list of @{ML_type cterm}s.
@{ML_matchresult_fake [display,gray]
- "let
- val chead = @{cterm \"P::unit \<Rightarrow> nat \<Rightarrow> bool\"}
- val cargs = [@{cterm \"()\"}, @{cterm \"3::nat\"}]
+ \<open>let
+ val chead = @{cterm "P::unit \<Rightarrow> nat \<Rightarrow> bool"}
+ val cargs = [@{cterm "()"}, @{cterm "3::nat"}]
in
Drule.list_comb (chead, cargs)
-end"
- "P () 3"}
+end\<close>
+ \<open>P () 3\<close>}
\begin{readmore}
For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see
@@ -1547,8 +1547,8 @@
final statement of the theorem.
@{ML_matchresult_fake [display, gray]
- "pwriteln (pretty_thm @{context} my_thm)"
- "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
+ \<open>pwriteln (pretty_thm @{context} my_thm)\<close>
+ \<open>\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t\<close>}
However, internally the code-snippet constructs the following
proof.
@@ -1613,12 +1613,12 @@
@{ML_matchresult [display,gray]
- "let
- fun pred s = match_string \"my_thm_simp\" s
+ \<open>let
+ fun pred s = match_string "my_thm_simp" s
in
exists pred (get_thm_names_from_ss @{context})
-end"
- "true"}
+end\<close>
+ \<open>true\<close>}
The main point of storing the theorems @{thm [source] my_thm} and @{thm
[source] my_thm_simp} is that they can now also be referenced with the
@@ -1717,22 +1717,22 @@
Testing them for alpha equality produces:
@{ML_matchresult [display,gray]
-"(Thm.eq_thm_prop (@{thm thm1}, @{thm thm2}),
- Thm.eq_thm_prop (@{thm thm2}, @{thm thm3}))"
-"(true, false)"}
+\<open>(Thm.eq_thm_prop (@{thm thm1}, @{thm thm2}),
+ Thm.eq_thm_prop (@{thm thm2}, @{thm thm3}))\<close>
+\<open>(true, false)\<close>}
Many functions destruct theorems into @{ML_type cterm}s. For example
the functions @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return
the left and right-hand side, respectively, of a meta-equality.
@{ML_matchresult_fake [display,gray]
- "let
+ \<open>let
val eq = @{thm True_def}
in
(Thm.lhs_of eq, Thm.rhs_of eq)
|> apply2 (Pretty.string_of o (pretty_cterm @{context}))
-end"
- "(True, (\<lambda>x. x) = (\<lambda>x. x))"}
+end\<close>
+ \<open>(True, (\<lambda>x. x) = (\<lambda>x. x))\<close>}
Other function produce terms that can be pattern-matched.
Suppose the following two theorems.
@@ -1746,22 +1746,22 @@
We can destruct them into premises and conclusions as follows.
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val ctxt = @{context}
fun prems_and_concl thm =
- [[Pretty.str \"Premises:\", pretty_terms ctxt (Thm.prems_of thm)],
- [Pretty.str \"Conclusion:\", pretty_term ctxt (Thm.concl_of thm)]]
+ [[Pretty.str "Premises:", pretty_terms ctxt (Thm.prems_of thm)],
+ [Pretty.str "Conclusion:", pretty_term ctxt (Thm.concl_of thm)]]
|> map Pretty.block
|> Pretty.chunks
|> pwriteln
in
prems_and_concl @{thm foo_test1};
prems_and_concl @{thm foo_test2}
-end"
-"Premises: ?A, ?B
+end\<close>
+\<open>Premises: ?A, ?B
Conclusion: ?C
Premises:
-Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C"}
+Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C\<close>}
Note that in the second case, there is no premise. The reason is that \<open>\<Longrightarrow>\<close>
separates premises and conclusion, while \<open>\<longrightarrow>\<close> is the object implication
@@ -1779,11 +1779,11 @@
unfold the constant @{term "True"} according to its definition (Line 2).
@{ML_matchresult_fake [display,gray,linenos]
- "Thm.reflexive @{cterm \"True\"}
+ \<open>Thm.reflexive @{cterm "True"}
|> Simplifier.rewrite_rule @{context} [@{thm True_def}]
|> pretty_thm @{context}
- |> pwriteln"
- "(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}
+ |> pwriteln\<close>
+ \<open>(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)\<close>}
Often it is necessary to transform theorems to and from the object
logic, that is replacing all \<open>\<longrightarrow>\<close> and \<open>\<forall>\<close> by \<open>\<Longrightarrow>\<close>
@@ -1796,20 +1796,20 @@
replaces all object connectives by equivalents in the meta logic. For example
@{ML_matchresult_fake [display, gray]
- "Object_Logic.rulify @{context} @{thm foo_test2}"
- "\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"}
+ \<open>Object_Logic.rulify @{context} @{thm foo_test2}\<close>
+ \<open>\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C\<close>}
The transformation in the other direction can be achieved with function
@{ML_ind atomize in Object_Logic} and the following code.
@{ML_matchresult_fake [display,gray]
- "let
+ \<open>let
val thm = @{thm foo_test1}
val meta_eq = Object_Logic.atomize @{context} (Thm.cprop_of thm)
in
Raw_Simplifier.rewrite_rule @{context} [meta_eq] thm
-end"
- "?A \<longrightarrow> ?B \<longrightarrow> ?C"}
+end\<close>
+ \<open>?A \<longrightarrow> ?B \<longrightarrow> ?C\<close>}
In this code the function @{ML atomize in Object_Logic} produces
a meta-equation between the given theorem and the theorem transformed
@@ -1838,8 +1838,8 @@
This function produces for the theorem @{thm [source] list.induct}
@{ML_matchresult_fake [display, gray]
- "atomize_thm @{context} @{thm list.induct}"
- "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
+ \<open>atomize_thm @{context} @{thm list.induct}\<close>
+ \<open>\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list\<close>}
Theorems can also be produced from terms by giving an explicit proof.
One way to achieve this is by using the function @{ML_ind prove in Goal}
@@ -1847,13 +1847,13 @@
to prove the term @{term "P \<Longrightarrow> P"}.
@{ML_matchresult_fake [display,gray]
- "let
- val trm = @{term \"P \<Longrightarrow> P::bool\"}
+ \<open>let
+ val trm = @{term "P \<Longrightarrow> P::bool"}
val tac = K (assume_tac @{context} 1)
in
- Goal.prove @{context} [\"P\"] [] trm tac
-end"
- "?P \<Longrightarrow> ?P"}
+ Goal.prove @{context} ["P"] [] trm tac
+end\<close>
+ \<open>?P \<Longrightarrow> ?P\<close>}
This function takes first a context and second a list of strings. This list
specifies which variables should be turned into schematic variables once the term
@@ -1879,8 +1879,8 @@
proposition.
@{ML_matchresult_fake [display, gray]
- "multi_test @{context} 3"
- "[\"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\"]"}
+ \<open>multi_test @{context} 3\<close>
+ \<open>["?f ?x = ?f ?x", "?f ?x = ?f ?x", "?f ?x = ?f ?x"]\<close>}
However you should be careful with @{ML prove_common in Goal} and very
large goals. If you increase the counter in the code above to \<open>3000\<close>,
@@ -1904,8 +1904,8 @@
reasons. An example of this function is as follows:
@{ML_matchresult_fake [display, gray]
- "Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"
- "True = False"}
+ \<open>Skip_Proof.make_thm @{theory} @{prop "True = False"}\<close>
+ \<open>True = False\<close>}
\begin{readmore}
Functions that setup goal states and prove theorems are implemented in
@@ -1927,8 +1927,8 @@
@{ML_ind get_tags in Thm}. So far the the auxiliary data of this lemma is
@{ML_matchresult_fake [display,gray]
- "Thm.get_tags @{thm foo_data}"
- "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"}
+ \<open>Thm.get_tags @{thm foo_data}\<close>
+ \<open>[("name", "General.foo_data"), ("kind", "lemma")]\<close>}
consisting of a name and a kind. When we store lemmas in the theorem database,
we might want to explicitly extend this data by attaching case names to the
@@ -1945,9 +1945,9 @@
The data of the theorem @{thm [source] foo_data'} is then as follows:
@{ML_matchresult_fake [display,gray]
- "Thm.get_tags @{thm foo_data'}"
- "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"),
- (\"case_names\", \"foo_case_one;foo_case_two\")]"}
+ \<open>Thm.get_tags @{thm foo_data'}\<close>
+ \<open>[("name", "General.foo_data'"), ("kind", "lemma"),
+ ("case_names", "foo_case_one;foo_case_two")]\<close>}
You can observe the case names of this lemma on the user level when using
the proof methods \<open>cases\<close> and \<open>induct\<close>. In the proof below
@@ -2037,10 +2037,10 @@
established theorem. This can be done with
@{ML_matchresult_fake [display,gray]
- "@{thm my_conjIa}
+ \<open>@{thm my_conjIa}
|> Thm.proof_body_of
- |> get_names"
- "[\"Essential.my_conjIa\"]"}
+ |> get_names\<close>
+ \<open>["Essential.my_conjIa"]\<close>}
whereby \<open>Essential\<close> refers to the theory name in which
we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
@@ -2051,13 +2051,13 @@
first level of the proof-tree, as follows.
@{ML_matchresult_fake [display,gray]
- "@{thm my_conjIa}
+ \<open>@{thm my_conjIa}
|> Thm.proof_body_of
|> get_pbodies
|> map get_names
- |> List.concat"
- "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\",
- \"Pure.protectI\"]"}
+ |> List.concat\<close>
+ \<open>["HOL.conjunct2", "HOL.conjunct1", "HOL.conjI", "Pure.protectD",
+ "Pure.protectI"]\<close>}
The theorems @{thm [source] Pure.protectD} and @{thm [source]
Pure.protectI} that are internal theorems are always part of a
@@ -2065,12 +2065,12 @@
count as a separate theorem, as you can see in the following code.
@{ML_matchresult_fake [display,gray]
- "@{thm my_conjIb}
+ \<open>@{thm my_conjIb}
|> Thm.proof_body_of
|> get_pbodies
|> map get_names
- |> List.concat"
- "[\"Pure.protectD\", \"Pure.protectI\"]"}
+ |> List.concat\<close>
+ \<open>["Pure.protectD", "Pure.protectI"]\<close>}
Interestingly, but not surprisingly, the proof of @{thm [source]
my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
@@ -2078,14 +2078,14 @@
are returned for @{thm [source] my_conjIc}.
@{ML_matchresult_fake [display,gray]
- "@{thm my_conjIc}
+ \<open>@{thm my_conjIc}
|> Thm.proof_body_of
|> get_pbodies
|> map get_names
- |> List.concat"
- "[\"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\",
- \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
- \"Pure.protectI\"]"}
+ |> List.concat\<close>
+ \<open>["HOL.Eq_TrueI", "HOL.simp_thms_25", "HOL.eq_reflection",
+ "HOL.conjunct2", "HOL.conjunct1", "HOL.TrueI", "Pure.protectD",
+ "Pure.protectI"]\<close>}
Of course we can also descend into the second level of the tree
``behind'' @{thm [source] my_conjIa} say, which
@@ -2093,16 +2093,16 @@
@{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
@{ML_matchresult_fake [display, gray]
- "@{thm my_conjIa}
+ \<open>@{thm my_conjIa}
|> Thm.proof_body_of
|> get_pbodies
|> map get_pbodies
|> (map o map) get_names
|> List.concat
|> List.concat
- |> duplicates (op=)"
- "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\",
- \"Pure.protectI\"]"}
+ |> duplicates (op=)\<close>
+ \<open>["HOL.spec", "HOL.and_def", "HOL.mp", "HOL.impI", "Pure.protectD",
+ "Pure.protectI"]\<close>}
\begin{exercise}
Have a look at the theorems that are used when a lemma is ``proved''
@@ -2309,7 +2309,7 @@
text \<open>
This gives a function from @{ML_type "theory -> theory"}, which
can be used for example with \isacommand{setup} or with
- @{ML "Context.>> o Context.map_theory"}.\footnote{\bf FIXME: explain what happens here.}
+ @{ML \<open>Context.>> o Context.map_theory\<close>}.\footnote{\bf FIXME: explain what happens here.}
As an example of a slightly more complicated theorem attribute, we implement
our own version of \<open>[THEN \<dots>]\<close>. This attribute will take a list of theorems
@@ -2409,8 +2409,8 @@
then you can see it is added to the initially empty list.
@{ML_matchresult_fake [display,gray]
- "MyThms.get @{context}"
- "[\"True\"]"}
+ \<open>MyThms.get @{context}\<close>
+ \<open>["True"]\<close>}
You can also add theorems using the command \isacommand{declare}.
\<close>
@@ -2423,8 +2423,8 @@
theorem list to be updated as:
@{ML_matchresult_fake [display,gray]
- "MyThms.get @{context}"
- "[\"True\", \"Suc (Suc 0) = 2\"]"}
+ \<open>MyThms.get @{context}\<close>
+ \<open>["True", "Suc (Suc 0) = 2"]\<close>}
The theorem @{thm [source] trueI_2} only appears once, since the
function @{ML_ind add_thm in Thm} tests for duplicates, before extending
@@ -2436,8 +2436,8 @@
text \<open>After this, the theorem list is again:
@{ML_matchresult_fake [display,gray]
- "MyThms.get @{context}"
- "[\"True\"]"}
+ \<open>MyThms.get @{context}\<close>
+ \<open>["True"]\<close>}
We used in this example two functions declared as @{ML_ind
declaration_attribute in Thm}, but there can be any number of them. We just
@@ -2469,7 +2469,7 @@
type. For example
@{ML_matchresult_fake [display,gray]
- "Pretty.str \"test\"" "String (\"test\", 4)"}
+ \<open>Pretty.str "test"\<close> \<open>String ("test", 4)\<close>}
where the result indicates that we transformed a string with length 4. Once
you have a pretty type, you can, for example, control where linebreaks may
@@ -2504,20 +2504,20 @@
we obtain the ugly output:
@{ML_matchresult_fake [display,gray]
-"tracing test_str"
-"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
+\<open>tracing test_str\<close>
+\<open>fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
-oooooooooooooobaaaaaaaaaaaar"}
+oooooooooooooobaaaaaaaaaaaar\<close>}
We obtain the same if we just use the function @{ML pprint}.
@{ML_matchresult_fake [display,gray]
-"pprint (Pretty.str test_str)"
-"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
+\<open>pprint (Pretty.str test_str)\<close>
+\<open>fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
-oooooooooooooobaaaaaaaaaaaar"}
+oooooooooooooobaaaaaaaaaaaar\<close>}
However by using pretty types you have the ability to indicate possible
linebreaks for example at each whitespace. You can achieve this with the
@@ -2527,60 +2527,60 @@
them with the function @{ML_ind blk in Pretty} as follows:
@{ML_matchresult_fake [display,gray]
-"let
- val ptrs = map Pretty.str (space_explode \" \" test_str)
+\<open>let
+ val ptrs = map Pretty.str (space_explode " " test_str)
in
pprint (Pretty.blk (0, Pretty.breaks ptrs))
-end"
-"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
+end\<close>
+\<open>fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
-fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
+fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar\<close>}
Here the layout of @{ML test_str} is much more pleasing to the
- eye. The @{ML "0"} in @{ML_ind blk in Pretty} stands for no hanging
+ eye. The @{ML \<open>0\<close>} in @{ML_ind blk in Pretty} stands for no hanging
indentation of the printed string. You can increase the indentation
and obtain
@{ML_matchresult_fake [display,gray]
-"let
- val ptrs = map Pretty.str (space_explode \" \" test_str)
+\<open>let
+ val ptrs = map Pretty.str (space_explode " " test_str)
in
pprint (Pretty.blk (3, Pretty.breaks ptrs))
-end"
-"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
+end\<close>
+\<open>fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
- fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
+ fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar\<close>}
where starting from the second line the indent is 3. If you want
that every line starts with the same indent, you can use the
function @{ML_ind indent in Pretty} as follows:
@{ML_matchresult_fake [display,gray]
-"let
- val ptrs = map Pretty.str (space_explode \" \" test_str)
+\<open>let
+ val ptrs = map Pretty.str (space_explode " " test_str)
in
pprint (Pretty.indent 10 (Pretty.blk (0, Pretty.breaks ptrs)))
-end"
-" fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
+end\<close>
+\<open> fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
- fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
+ fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar\<close>}
If you want to print out a list of items separated by commas and
have the linebreaks handled properly, you can use the function
@{ML_ind commas in Pretty}. For example
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
in
pprint (Pretty.blk (0, Pretty.commas ptrs))
-end"
-"99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006,
+end\<close>
+\<open>99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006,
100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015,
-100016, 100017, 100018, 100019, 100020"}
+100016, 100017, 100018, 100019, 100020\<close>}
where @{ML upto} generates a list of integers. You can print out this
list as a ``set'', that means enclosed inside @{text [quotes] "{"} and
@@ -2591,14 +2591,14 @@
text \<open>
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
in
- pprint (Pretty.enum \",\" \"{\" \"}\" ptrs)
-end"
-"{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006,
+ pprint (Pretty.enum "," "{" "}" ptrs)
+end\<close>
+\<open>{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006,
100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015,
- 100016, 100017, 100018, 100019, 100020}"}
+ 100016, 100017, 100018, 100019, 100020}\<close>}
As can be seen, this function prints out the ``set'' so that starting
from the second, each new line has an indentation of 2.
@@ -2623,58 +2623,58 @@
text \<open>
where Line 7 prints the beginning of the list and Line
- 8 the last item. We have to use @{ML "Pretty.brk 1"} in order
+ 8 the last item. We have to use @{ML \<open>Pretty.brk 1\<close>} in order
to insert a space (of length 1) before the
@{text [quotes] "and"}. This space is also a place where a line break
can occur. We do the same after the @{text [quotes] "and"}. This gives you
for example
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val ptrs1 = map (Pretty.str o string_of_int) (1 upto 22)
val ptrs2 = map (Pretty.str o string_of_int) (10 upto 28)
in
pprint (Pretty.blk (0, and_list ptrs1));
pprint (Pretty.blk (0, and_list ptrs2))
-end"
-"1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21
+end\<close>
+\<open>1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21
and 22
10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and
-28"}
+28\<close>}
Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out
a list of items, but automatically inserts forced breaks between each item.
Compare
@{ML_matchresult_fake [display,gray]
- "let
- val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"]
+ \<open>let
+ val a_and_b = [Pretty.str "a", Pretty.str "b"]
in
pprint (Pretty.blk (0, a_and_b));
pprint (Pretty.chunks a_and_b)
-end"
-"ab
+end\<close>
+\<open>ab
a
-b"}
+b\<close>}
The function @{ML_ind big_list in Pretty} helps with printing long lists.
It is used for example in the command \isacommand{print\_theorems}. An
example is as follows.
@{ML_matchresult_fake [display,gray]
- "let
+ \<open>let
val pstrs = map (Pretty.str o string_of_int) (4 upto 10)
in
- pprint (Pretty.big_list \"header\" pstrs)
-end"
- "header
+ pprint (Pretty.big_list "header" pstrs)
+end\<close>
+ \<open>header
4
5
6
7
8
9
- 10"}
+ 10\<close>}
The point of the pretty-printing functions is to conveninetly obtain
a lay-out of terms and types that is pleasing to the eye. If we print
@@ -2682,12 +2682,12 @@
exercise~\ref{ex:debruijn} we obtain the following:
@{ML_matchresult_fake [display,gray]
- "pprint (Syntax.pretty_term @{context} (de_bruijn 4))"
- "(P 3 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
+ \<open>pprint (Syntax.pretty_term @{context} (de_bruijn 4))\<close>
+ \<open>(P 3 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
(P 2 = P 3 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
(P 1 = P 2 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
(P 1 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<longrightarrow>
-P 4 \<and> P 3 \<and> P 2 \<and> P 1"}
+P 4 \<and> P 3 \<and> P 2 \<and> P 1\<close>}
We use the function @{ML_ind pretty_term in Syntax} for pretty-printing
terms. Next we like to pretty-print a term and its type. For this we use the
@@ -2716,16 +2716,16 @@
Now you can write
@{ML_matchresult_fake [display,gray]
- "tell_type @{context} @{term \"min (Suc 0)\"}"
- "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
+ \<open>tell_type @{context} @{term "min (Suc 0)"}\<close>
+ \<open>The term "min (Suc 0)" has type "nat \<Rightarrow> nat".\<close>}
To see the proper line breaking, you can try out the function on a bigger term
and type. For example:
@{ML_matchresult_fake [display,gray]
- "tell_type @{context} @{term \"(=) ((=) ((=) ((=) ((=) (=)))))\"}"
- "The term \"(=) ((=) ((=) ((=) ((=) (=)))))\" has type
-\"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
+ \<open>tell_type @{context} @{term "(=) ((=) ((=) ((=) ((=) (=)))))"}\<close>
+ \<open>The term "(=) ((=) ((=) ((=) ((=) (=)))))" has type
+"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool".\<close>}
\begin{readmore}
The general infrastructure for pretty-printing is implemented in the file
--- a/ProgTutorial/First_Steps.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/First_Steps.thy Fri May 17 10:38:01 2019 +0200
@@ -39,7 +39,7 @@
\begin{isabelle}
\begin{graybox}
\isacommand{ML}~\<open>\<verbopen>\<close>\isanewline
- \hspace{5mm}@{ML "3 + 4"}\isanewline
+ \hspace{5mm}@{ML \<open>3 + 4\<close>}\isanewline
\<open>\<verbclose>\<close>\isanewline
\<open>> 7\<close>\smallskip
\end{graybox}
@@ -61,7 +61,7 @@
\begin{isabelle}
\isacommand{lemma}~\<open>test:\<close>\isanewline
\isacommand{shows}~@{text [quotes] "True"}\isanewline
- \isacommand{ML\_prf}~\<open>\<verbopen>\<close>~@{ML "writeln \"Trivial!\""}~\<open>\<verbclose>\<close>\isanewline
+ \isacommand{ML\_prf}~\<open>\<verbopen>\<close>~@{ML \<open>writeln "Trivial!"\<close>}~\<open>\<verbclose>\<close>\isanewline
\isacommand{oops}
\end{isabelle}
\end{quote}
@@ -93,7 +93,7 @@
code. This can be done in a ``quick-and-dirty'' fashion using the function
@{ML_ind writeln in Output}. For example
- @{ML_matchresult_fake [display,gray] "writeln \"any string\"" "\"any string\""}
+ @{ML_matchresult_fake [display,gray] \<open>writeln "any string"\<close> \<open>"any string"\<close>}
will print out @{text [quotes] "any string"}.
This function expects a string as argument. If you develop under
@@ -110,9 +110,9 @@
for example:
@{ML_matchresult_fake [display,gray]
- "if 0 = 1 then true else (error \"foo\")"
-"*** foo
-***"}
+ \<open>if 0 = 1 then true else (error "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
@@ -137,8 +137,8 @@
They can be used as follows
@{ML_matchresult_fake [display,gray]
- "pwriteln (pretty_term @{context} @{term \"1::nat\"})"
- "\"1\""}
+ \<open>pwriteln (pretty_term @{context} @{term "1::nat"})\<close>
+ \<open>"1"\<close>}
If there is more than one term to be printed, you can use the
function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty}
@@ -160,8 +160,8 @@
Now by using this context @{ML pretty_term} prints out
@{ML_matchresult_fake [display, gray]
- "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})"
- "(1::nat, x::'a)"}
+ \<open>pwriteln (pretty_term show_types_ctxt @{term "(1::nat, x)"})\<close>
+ \<open>(1::nat, x::'a)\<close>}
where \<open>1\<close> and \<open>x\<close> are displayed with their inferred types.
Other configuration values that influence
@@ -204,8 +204,8 @@
instantiation of \<open>?P\<close> and \<open>?Q\<close>.
@{ML_matchresult_fake [display, gray]
- "pwriteln (pretty_thm @{context} @{thm conjI})"
- "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
+ \<open>pwriteln (pretty_thm @{context} @{thm conjI})\<close>
+ \<open>\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\<close>}
However, to improve the readability when printing theorems, we
can switch off the question marks as follows:
@@ -222,8 +222,8 @@
With this function, theorem @{thm [source] conjI} is now printed as follows:
@{ML_matchresult_fake [display, gray]
- "pwriteln (pretty_thm_no_vars @{context} @{thm conjI})"
- "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
+ \<open>pwriteln (pretty_thm_no_vars @{context} @{thm conjI})\<close>
+ \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q\<close>}
Again the functions @{ML commas} and @{ML block in Pretty} help
with printing more than one theorem.
@@ -265,17 +265,17 @@
\emph{not} print out information as
@{ML_matchresult_fake [display,gray]
-"pwriteln (Pretty.str \"First half,\");
-pwriteln (Pretty.str \"and second half.\")"
-"First half,
-and second half."}
+\<open>pwriteln (Pretty.str "First half,");
+pwriteln (Pretty.str "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]
-"pwriteln (Pretty.str (\"First half,\" ^ \"\\n\" ^ \"and second half.\"))"
-"First half,
-and second half."}
+\<open>pwriteln (Pretty.str ("First half," ^ "\\n" ^ "and second half."))\<close>
+\<open>First half,
+and second half.\<close>}
To ease this kind of string manipulations, there are a number
of library functions in Isabelle. For example, the function
@@ -283,9 +283,9 @@
and inserts newlines in between each element.
@{ML_matchresult_fake [display, gray]
- "pwriteln (Pretty.str (cat_lines [\"foo\", \"bar\"]))"
- "foo
-bar"}
+ \<open>pwriteln (Pretty.str (cat_lines ["foo", "bar"]))\<close>
+ \<open>foo
+bar\<close>}
Section \ref{sec:pretty} will explain the infrastructure that Isabelle
provides for more elaborate pretty printing.
@@ -383,20 +383,20 @@
text \<open>
This function takes a term and a context as arguments. If the term is of function
- type, then @{ML "apply_fresh_args"} returns the term with distinct variables
+ type, then @{ML \<open>apply_fresh_args\<close>} returns the term with distinct variables
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]
-"let
- val trm = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
+\<open>let
+ val trm = @{term "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}
val ctxt = @{context}
in
apply_fresh_args trm ctxt
|> pretty_term ctxt
|> pwriteln
-end"
- "P z za zb"}
+end\<close>
+ \<open>P z za zb\<close>}
You can read off this behaviour from how @{ML apply_fresh_args} is coded: in
Line 2, the function @{ML_ind fastype_of in Term} calculates the type of the
@@ -415,15 +415,15 @@
tremendously to avoid any name clashes. Consider for example:
@{ML_matchresult_fake [display,gray]
-"let
- val trm = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
+\<open>let
+ val trm = @{term "za::'a \<Rightarrow> 'b \<Rightarrow> 'c"}
val ctxt = @{context}
in
apply_fresh_args trm ctxt
|> pretty_term ctxt
|> pwriteln
-end"
- "za z zb"}
+end\<close>
+ \<open>za z zb\<close>}
where the \<open>za\<close> is correctly avoided.
@@ -444,7 +444,7 @@
\isacommand{setup}- or \isacommand{local\_setup}-command. These functions
have to be of type @{ML_type "theory -> theory"}, respectively
@{ML_type "local_theory -> local_theory"}. More than one such setup function
- can be composed with @{ML "#>"}. Consider for example the following code,
+ can be composed with @{ML \<open>#>\<close>}. Consider for example the following code,
where we store the theorems @{thm [source] conjI}, @{thm [source] conjunct1}
and @{thm [source] conjunct2} under alternative names.
\<close>
@@ -463,7 +463,7 @@
@{ML_ind note in Local_Theory} in the structure @{ML_structure Local_Theory};
it stores a theorem under a name.
In lines 5 to 6 we call this function to give alternative names for the three
- theorems. The point of @{ML "#>"} is that you can sequence such function calls.
+ theorems. The point of @{ML \<open>#>\<close>} is that you can sequence such function calls.
The remaining combinators we describe in this section add convenience for
the ``waterfall method'' of writing functions. The combinator @{ML_ind tap
@@ -501,9 +501,9 @@
text \<open>
which takes \<open>x\<close> as argument, and then increments \<open>x\<close>, but also keeps
- \<open>x\<close>. The intermediate result is therefore the pair @{ML "(x + 1, x)"
+ \<open>x\<close>. The intermediate result is therefore the pair @{ML \<open>(x + 1, x)\<close>
for x}. After that, the function increments the right-hand component of the
- pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
+ pair. So finally the result will be @{ML \<open>(x + 1, x + 1)\<close> for x}.
The combinators @{ML_ind "|>>" in Basics} and @{ML_ind "||>" in Basics} are
defined for functions manipulating pairs. The first applies the function to
@@ -522,8 +522,8 @@
These two functions can, for example, be used to avoid explicit \<open>lets\<close> for
intermediate values in functions that return pairs. As an example, suppose you
want to separate a list of integers into two lists according to a
- threshold. If the threshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"}
- should be separated as @{ML "([1,2,3,4], [6,5])"}. Such a function can be
+ threshold. If the threshold is @{ML \<open>5\<close>}, the list @{ML \<open>[1,6,2,5,3,4]\<close>}
+ should be separated as @{ML \<open>([1,2,3,4], [6,5])\<close>}. Such a function can be
implemented as
\<close>
@@ -537,7 +537,7 @@
text \<open>
where the return value of the recursive call is bound explicitly to
- the pair @{ML "(los, grs)" for los grs}. However, this function
+ the pair @{ML \<open>(los, grs)\<close> for los grs}. However, this function
can be implemented more concisely as
\<close>
@@ -588,37 +588,37 @@
the value by one, but also nest the intermediate results to the left. For example
@{ML_matchresult [display,gray]
- "acc_incs 1"
- "((((\"\", 1), 2), 3), 4)"}
+ \<open>acc_incs 1\<close>
+ \<open>(((("", 1), 2), 3), 4)\<close>}
You can continue this chain with:
@{ML_matchresult [display,gray]
- "acc_incs 1 ||>> (fn x => (x, x + 2))"
- "(((((\"\", 1), 2), 3), 4), 6)"}
+ \<open>acc_incs 1 ||>> (fn x => (x, x + 2))\<close>
+ \<open>((((("", 1), 2), 3), 4), 6)\<close>}
An example where this combinator is useful is as follows
@{ML_matchresult_fake [display, gray]
- "let
+ \<open>let
val ((names1, names2), _) =
@{context}
- |> Variable.variant_fixes (replicate 4 \"x\")
- ||>> Variable.variant_fixes (replicate 5 \"x\")
+ |> Variable.variant_fixes (replicate 4 "x")
+ ||>> Variable.variant_fixes (replicate 5 "x")
in
(names1, names2)
-end"
- "([\"x\", \"xa\", \"xb\", \"xc\"], [\"xd\", \"xe\", \"xf\", \"xg\", \"xh\"])"}
+end\<close>
+ \<open>(["x", "xa", "xb", "xc"], ["xd", "xe", "xf", "xg", "xh"])\<close>}
- Its purpose is to create nine variants of the string @{ML "\"x\""} so
+ Its purpose is to create nine variants of the string @{ML \<open>"x"\<close>} so
that no variant will clash with another. Suppose for some reason we want
to bind four variants to the lists @{ML_text "name1"} and the
rest to @{ML_text "name2"}. In order to obtain non-clashing
variants we have to thread the context through the function calls
(the context records which variants have been previously created).
- For the first call we can use @{ML "|>"}, but in the
+ For the first call we can use @{ML \<open>|>\<close>}, but in the
second and any further call to @{ML_ind variant_fixes in Variable} we
- have to use @{ML "||>>"} in order to account for the result(s)
+ have to use @{ML \<open>||>>\<close>} in order to account for the result(s)
obtained by previous calls.
A more realistic example for this combinator is the following code
@@ -640,20 +640,20 @@
the theorem corresponding to the definitions. For example for the first definition:
@{ML_matchresult_fake [display, gray]
- "let
+ \<open>let
val (one_trm, (_, one_thm)) = one_def
in
pwriteln (pretty_term ctxt' one_trm);
pwriteln (pretty_thm ctxt' one_thm)
-end"
- "One
-One \<equiv> 1"}
- Recall that @{ML "|>"} is the reverse function application. Recall also that
- the related reverse function composition is @{ML "#>"}. In fact all the
- combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
+end\<close>
+ \<open>One
+One \<equiv> 1\<close>}
+ Recall that @{ML \<open>|>\<close>} is the reverse function application. Recall also that
+ the related reverse function composition is @{ML \<open>#>\<close>}. In fact all the
+ combinators @{ML \<open>|->\<close>}, @{ML \<open>|>>\<close>} , @{ML \<open>||>\<close>} and @{ML \<open>||>>\<close>}
described above have related combinators for function composition, namely
@{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in
- Basics} and @{ML_ind "##>>" in Basics}. Using @{ML "#->"}, for example, the
+ Basics} and @{ML_ind "##>>" in Basics}. Using @{ML \<open>#->\<close>}, for example, the
function \<open>double\<close> can also be written as:
\<close>
@@ -667,22 +667,22 @@
sometimes necessary to do some ``plumbing'' in order to fit functions
together. We have already seen such plumbing in the function @{ML
apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
- list_comb}, which works over pairs, to fit with the combinator @{ML "|>"}. Such
+ list_comb}, which works over pairs, to fit with the combinator @{ML \<open>|>\<close>}. Such
plumbing is also needed in situations where a function operates over lists,
but one calculates only with a single element. An example is the function
@{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]
- "let
+ \<open>let
val ctxt = @{context}
in
- map (Syntax.parse_term ctxt) [\"m + n\", \"m * n\", \"m - (n::nat)\"]
+ map (Syntax.parse_term ctxt) ["m + n", "m * n", "m - (n::nat)"]
|> Syntax.check_terms ctxt
|> pretty_terms ctxt
|> pwriteln
-end"
- "m + n, m * n, m - n"}
+end\<close>
+ \<open>m + n, m * n, m - n\<close>}
\<close>
text \<open>
@@ -695,15 +695,15 @@
in terms of @{ML singleton} and @{ML check_terms in Syntax}.} For example
@{ML_matchresult_fake [display, gray, linenos]
- "let
+ \<open>let
val ctxt = @{context}
in
- Syntax.parse_term ctxt \"m - (n::nat)\"
+ Syntax.parse_term ctxt "m - (n::nat)"
|> singleton (Syntax.check_terms ctxt)
|> pretty_term ctxt
|> pwriteln
-end"
- "m - n"}
+end\<close>
+ \<open>m - n\<close>}
where in Line 5, the function operating over lists fits with the
single term generated in Line 4.
@@ -716,7 +716,7 @@
\end{readmore}
\begin{exercise}
- Find out what the combinator @{ML "K I"} does.
+ Find out what the combinator @{ML \<open>K I\<close>} does.
\end{exercise}
\<close>
@@ -743,7 +743,7 @@
are indicated by the @{ML_text @}-sign followed by text wrapped in \<open>{\<dots>}\<close>. For example, one can print out the name of the current theory with
the code
- @{ML_matchresult [display,gray] "Context.theory_name @{theory}" "\"First_Steps\""}
+ @{ML_matchresult [display,gray] \<open>Context.theory_name @{theory}\<close> \<open>"First_Steps"\<close>}
where \<open>@{theory}\<close> is an antiquotation that is substituted with the
current theory (remember that we assumed we are inside the theory
@@ -772,34 +772,34 @@
defined abbreviations. For example
@{ML_matchresult_fake [display, gray]
- "Proof_Context.print_abbrevs false @{context}"
-"\<dots>
+ \<open>Proof_Context.print_abbrevs false @{context}\<close>
+\<open>\<dots>
INTER \<equiv> INFI
Inter \<equiv> Inf
-\<dots>"}
+\<dots>\<close>}
The precise output of course depends on the abbreviations that are
currently defined; this can change over time.
You can also use antiquotations to refer to proved theorems:
\<open>@{thm \<dots>}\<close> for a single theorem
- @{ML_matchresult_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
+ @{ML_matchresult_fake [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]
- "@{thms conj_ac}"
-"(?P \<and> ?Q) = (?Q \<and> ?P)
+ \<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)"}
+((?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]
- "@{thm refl[THEN eq_reflection]}"
- "?x \<equiv> ?x"}
+ \<open>@{thm refl[THEN eq_reflection]}\<close>
+ \<open>?x \<equiv> ?x\<close>}
The point of these antiquotations is that referring to theorems in this way
makes your code independent from what theorems the user might have stored
@@ -817,9 +817,9 @@
The result can be printed out as follows.
@{ML_matchresult_fake [gray,display]
-"foo_thms |> pretty_thms_no_vars @{context}
- |> pwriteln"
- "True, False \<Longrightarrow> P"}
+\<open>foo_thms |> pretty_thms_no_vars @{context}
+ |> pwriteln\<close>
+ \<open>True, False \<Longrightarrow> P\<close>}
You can also refer to the current simpset via an antiquotation. To illustrate
this we implement the function that extracts the theorem names stored in a
@@ -841,8 +841,8 @@
The current simpset can be referred to using @{ML_ind simpset_of in Raw_Simplifier}.
@{ML_matchresult_fake [display,gray]
- "get_thm_names_from_ss @{context}"
- "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
+ \<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>}
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
@@ -885,8 +885,8 @@
in more detail in later sections.) An example for this antiquotation is:
@{ML_matchresult_fake [display,gray]
- "@{term_pat \"Suc (?x::nat)\"}"
- "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
+ \<open>@{term_pat "Suc (?x::nat)"}\<close>
+ \<open>Const ("Suc", "nat \<Rightarrow> nat") $ Var (("x", 0), "nat")\<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
@@ -981,18 +981,18 @@
The data can be retrieved with the projection functions defined above.
@{ML_matchresult_fake [display, gray]
-"project_int (nth foo_list 0);
-project_bool (nth foo_list 1)"
-"13
-true"}
+\<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]
-"project_bool (nth foo_list 0)"
-"*** exception Match raised"}
+\<open>project_bool (nth foo_list 0)\<close>
+\<open>*** exception Match raised\<close>}
This runtime error is the reason why ML is still type-sound despite
containing a universal type.
@@ -1063,8 +1063,8 @@
Section~\ref{sec:theories}). The lookup can now be performed as follows.
@{ML_matchresult_fake [display, gray]
-"lookup @{theory} \"conj\""
-"SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}
+\<open>lookup @{theory} "conj"\<close>
+\<open>SOME "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"\<close>}
An important point to note is that these tables (and data in general)
need to be treated in a purely functional fashion. Although
@@ -1077,8 +1077,8 @@
and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}
@{ML_matchresult_fake [display, gray]
-"lookup @{theory} \"conj\""
-"SOME \"True\""}
+\<open>lookup @{theory} "conj"\<close>
+\<open>SOME "True"\<close>}
there are no references involved. This is one of the most fundamental
coding conventions for programming in Isabelle. References
@@ -1096,11 +1096,11 @@
text \<open>
We initialise the reference with the empty list. Consequently a first
- lookup produces @{ML "ref []" in Unsynchronized}.
+ lookup produces @{ML \<open>ref []\<close> in Unsynchronized}.
@{ML_matchresult_fake [display,gray]
- "WrongRefData.get @{theory}"
- "ref []"}
+ \<open>WrongRefData.get @{theory}\<close>
+ \<open>ref []\<close>}
For updating the reference we use the following function
\<close>
@@ -1118,23 +1118,23 @@
text \<open>
A lookup in the current theory gives then the expected list
- @{ML "ref [1]" in Unsynchronized}.
+ @{ML \<open>ref [1]\<close> in Unsynchronized}.
@{ML_matchresult_fake [display,gray]
- "WrongRefData.get @{theory}"
- "ref [1]"}
+ \<open>WrongRefData.get @{theory}\<close>
+ \<open>ref [1]\<close>}
So far everything is as expected. But, the trouble starts if we attempt to
backtrack to the ``point'' before the \isacommand{setup}-command. There, we
would expect that the list is empty again. But since it is stored in a
reference, Isabelle has no control over it. So it is not empty, but still
- @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, if we execute the
- \isacommand{setup}-command again, we do not obtain @{ML "ref [1]" in
+ @{ML \<open>ref [1]\<close> in Unsynchronized}. Adding to the trouble, if we execute the
+ \isacommand{setup}-command again, we do not obtain @{ML \<open>ref [1]\<close> in
Unsynchronized}, but
@{ML_matchresult_fake [display,gray]
- "WrongRefData.get @{theory}"
- "ref [1, 1]"}
+ \<open>WrongRefData.get @{theory}\<close>
+ \<open>ref [1, 1]\<close>}
Now imagine how often you go backwards and forwards in your proof
scripts.\footnote{The same problem can be triggered in the Jedit GUI by
@@ -1180,22 +1180,22 @@
\<open>@{context}\<close> and update it in various ways.
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val ctxt0 = @{context}
- val ctxt1 = ctxt0 |> update @{term \"False\"}
- |> update @{term \"True \<and> True\"}
- val ctxt2 = ctxt0 |> update @{term \"1::nat\"}
- val ctxt3 = ctxt2 |> update @{term \"2::nat\"}
+ val ctxt1 = ctxt0 |> update @{term "False"}
+ |> update @{term "True \<and> True"}
+ val ctxt2 = ctxt0 |> update @{term "1::nat"}
+ val ctxt3 = ctxt2 |> update @{term "2::nat"}
in
print ctxt0;
print ctxt1;
print ctxt2;
print ctxt3
-end"
-"Empty!
+end\<close>
+\<open>Empty!
True \<and> True, False
1
-2, 1"}
+2, 1\<close>}
Many functions in Isabelle manage and update data in a similar
fashion. Consequently, such calculations with contexts occur frequently in
@@ -1272,8 +1272,8 @@
@{ML FooRules.get}:
@{ML_matchresult_fake [display,gray]
- "FooRules.get @{context}"
- "[\"True\", \"?C\",\"?B\"]"}
+ \<open>FooRules.get @{context}\<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
@@ -1309,30 +1309,30 @@
function @{ML_ind get in Config} from a proof context
@{ML_matchresult [display,gray]
- "Config.get @{context} bval"
- "true"}
+ \<open>Config.get @{context} bval\<close>
+ \<open>true\<close>}
or directly from a theory using the function @{ML_ind get_global in Config}
@{ML_matchresult [display,gray]
- "Config.get_global @{theory} bval"
- "true"}
+ \<open>Config.get_global @{theory} bval\<close>
+ \<open>true\<close>}
It is also possible to manipulate the configuration values
from the ML-level with the functions @{ML_ind put in Config}
and @{ML_ind put_global in Config}. For example
@{ML_matchresult [display,gray]
- "let
+ \<open>let
val ctxt = @{context}
- val ctxt' = Config.put sval \"foo\" ctxt
- val ctxt'' = Config.put sval \"bar\" ctxt'
+ val ctxt' = Config.put sval "foo" ctxt
+ val ctxt'' = Config.put sval "bar" ctxt'
in
(Config.get ctxt sval,
Config.get ctxt' sval,
Config.get ctxt'' sval)
-end"
- "(\"some string\", \"foo\", \"bar\")"}
+end\<close>
+ \<open>("some string", "foo", "bar")\<close>}
A concrete example for a configuration value is
@{ML_ind simp_trace in Raw_Simplifier}, which switches on trace information
--- a/ProgTutorial/Intro.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Intro.thy Fri May 17 10:38:01 2019 +0200
@@ -152,7 +152,7 @@
\begin{isabelle}
\begin{graybox}
\isacommand{ML}~\<open>\<verbopen>\<close>\isanewline
- \hspace{5mm}@{ML "3 + 4"}\isanewline
+ \hspace{5mm}@{ML \<open>3 + 4\<close>}\isanewline
\<open>\<verbclose>\<close>
\end{graybox}
\end{isabelle}
@@ -163,13 +163,13 @@
the enclosing \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> and just
write:
- @{ML [display,gray] "3 + 4"}
+ @{ML [display,gray] \<open>3 + 4\<close>}
Whenever appropriate we also show the response the code
generates when evaluated. This response is prefixed with a
@{text [quotes] ">"}, like:
- @{ML_matchresult [display,gray] "3 + 4" "7"}
+ @{ML_matchresult [display,gray] \<open>3 + 4\<close> \<open>7\<close>}
The user-level commands of Isabelle (i.e., the non-ML code) are written
in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},
--- a/ProgTutorial/Package/Ind_Code.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy Fri May 17 10:38:01 2019 +0200
@@ -494,13 +494,13 @@
the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows:
@{ML_matchresult_fake [display, gray]
-"let
- val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
+\<open>let
+ val ctrms = [@{cterm "a::nat"}, @{cterm "b::nat"}, @{cterm "c::nat"}]
val new_thm = all_elims ctrms @{thm all_elims_test}
in
pwriteln (pretty_thm_no_vars @{context} new_thm)
-end"
- "P a b c"}
+end\<close>
+ \<open>P a b c\<close>}
Note the difference with @{ML inst_spec_tac} from Page~\pageref{fun:instspectac}:
@{ML inst_spec_tac} is a tactic which operates on a goal state; in contrast
@@ -511,12 +511,12 @@
@{thm [source] imp_elims_test}:
@{ML_matchresult_fake [display, gray]
-"let
+\<open>let
val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}
in
pwriteln (pretty_thm_no_vars @{context} res)
-end"
- "C"}
+end\<close>
+ \<open>C\<close>}
Now we set up the proof for the introduction rule as follows:
\<close>
@@ -728,7 +728,7 @@
whether we are in the simple or complicated case by checking whether
the topmost connective is an \<open>\<forall>\<close>. The premises in the simple
case cannot have such a quantification, since the first step
- of @{ML "expand_tac"} was to ``rulify'' the lemma.
+ of @{ML \<open>expand_tac\<close>} was to ``rulify'' the lemma.
The premise of the complicated case must have at least one \<open>\<forall>\<close>
coming from the quantification over the \<open>preds\<close>. So
we can implement the following function
@@ -1011,7 +1011,7 @@
any name.} Line 21 registers the induction principles. For this we have
to use some specific attributes. The first @{ML_ind case_names in Rule_Cases}
corresponds to the case names that are used by Isar to reference the proof
- obligations in the induction. The second @{ML "consumes 1" in Rule_Cases}
+ obligations in the induction. The second @{ML \<open>consumes 1\<close> in Rule_Cases}
indicates that the first premise of the induction principle (namely
the predicate over which the induction proceeds) is eliminated.
--- a/ProgTutorial/Package/Ind_Interface.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy Fri May 17 10:38:01 2019 +0200
@@ -108,20 +108,20 @@
of @{term even} and @{term odd}
@{ML_matchresult [display,gray]
-"let
+\<open>let
val input = filtered_input
- (\"even and odd \" ^
- \"where \" ^
- \" even0[intro]: \\\"even 0\\\" \" ^
- \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^
- \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\" \")
+ ("even and odd " ^
+ "where " ^
+ " even0[intro]: \"even 0\" " ^
+ "| evenS[intro]: \"odd n \<Longrightarrow> even (Suc n)\" " ^
+ "| oddS[intro]: \"even n \<Longrightarrow> odd (Suc n)\" ")
in
parse spec_parser input
-end"
-"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
+end\<close>
+\<open>(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
[((even0,_), _),
((evenS,_), _),
- ((oddS,_), _)]), [])"}
+ ((oddS,_), _)]), [])\<close>}
then we get back the specifications of the predicates (with type and syntax annotations),
and specifications of the introduction rules. This is all the information we
--- a/ProgTutorial/Parsing.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Parsing.thy Fri May 17 10:38:01 2019 +0200
@@ -60,18 +60,18 @@
the rest of the input list. For example:
@{ML_matchresult [display,gray]
- "($$ \"h\") (Symbol.explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
+ \<open>($$ "h") (Symbol.explode "hello")\<close> \<open>("h", ["e", "l", "l", "o"])\<close>}
@{ML_matchresult [display,gray]
- "($$ \"w\") (Symbol.explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
+ \<open>($$ "w") (Symbol.explode "world")\<close> \<open>("w", ["o", "r", "l", "d"])\<close>}
- The function @{ML "$$"} will either succeed (as in the two examples above)
+ The function @{ML \<open>$$\<close>} will either succeed (as in the two examples above)
or raise the exception \<open>FAIL\<close> if no string can be consumed. For
example trying to parse
@{ML_matchresult_fake [display,gray]
- "($$ \"x\") (Symbol.explode \"world\")"
- "Exception FAIL raised"}
+ \<open>($$ "x") (Symbol.explode "world")\<close>
+ \<open>Exception FAIL raised\<close>}
will raise the exception \<open>FAIL\<close>. The function @{ML_ind "$$" in Scan} will also
fail if you try to consume more than a single character.
@@ -84,7 +84,7 @@
\item \<open>MORE\<close> indicates that there is not enough input for the parser. For example
in \<open>($$ "h") []\<close>.
\item \<open>ABORT\<close> indicates that a dead end is reached.
- It is used for example in the function @{ML "!!"} (see below).
+ It is used for example in the function @{ML \<open>!!\<close>} (see below).
\end{itemize}
However, note that these exceptions are private to the parser and cannot be accessed
@@ -98,15 +98,15 @@
Isabelle. To see the difference consider
@{ML_matchresult_fake [display,gray]
-"let
- val input = \"\<foo> bar\"
+\<open>let
+ val input = "\<foo> bar"
in
(String.explode input, Symbol.explode input)
-end"
-"([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"],
- [\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
+end\<close>
+\<open>(["\\", "<", "f", "o", "o", ">", " ", "b", "a", "r"],
+ ["\<foo>", " ", "b", "a", "r"])\<close>}
- Slightly more general than the parser @{ML "$$"} is the function
+ Slightly more general than the parser @{ML \<open>$$\<close>} is the function
@{ML_ind one in Scan}, in that it takes a predicate as argument and
then parses exactly
one item from the input list satisfying this predicate. For example the
@@ -114,22 +114,22 @@
[quotes] "w"}:
@{ML_matchresult [display,gray]
-"let
- val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")
- val input1 = Symbol.explode \"hello\"
- val input2 = Symbol.explode \"world\"
+\<open>let
+ val hw = Scan.one (fn x => x = "h" orelse x = "w")
+ val input1 = Symbol.explode "hello"
+ val input2 = Symbol.explode "world"
in
(hw input1, hw input2)
-end"
- "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
+end\<close>
+ \<open>(("h", ["e", "l", "l", "o"]),("w", ["o", "r", "l", "d"]))\<close>}
Two parsers can be connected in sequence by using the function @{ML_ind "--" in Scan}.
For example parsing \<open>h\<close>, \<open>e\<close> and \<open>l\<close> (in this
order) you can achieve by:
@{ML_matchresult [display,gray]
- "($$ \"h\" -- $$ \"e\" -- $$ \"l\") (Symbol.explode \"hello\")"
- "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
+ \<open>($$ "h" -- $$ "e" -- $$ "l") (Symbol.explode "hello")\<close>
+ \<open>((("h", "e"), "l"), ["l", "o"])\<close>}
Note how the result of consumed strings builds up on the left as nested pairs.
@@ -137,24 +137,24 @@
then you can use the function @{ML_ind this_string in Scan}.
@{ML_matchresult [display,gray]
- "Scan.this_string \"hell\" (Symbol.explode \"hello\")"
- "(\"hell\", [\"o\"])"}
+ \<open>Scan.this_string "hell" (Symbol.explode "hello")\<close>
+ \<open>("hell", ["o"])\<close>}
Parsers that explore alternatives can be constructed using the function
- @{ML_ind "||" in Scan}. The parser @{ML "(p || q)" for p q} returns the
+ @{ML_ind "||" in Scan}. The parser @{ML \<open>(p || q)\<close> for p q} returns the
result of \<open>p\<close>, in case it succeeds; otherwise it returns the
result of \<open>q\<close>. For example:
@{ML_matchresult [display,gray]
-"let
- val hw = $$ \"h\" || $$ \"w\"
- val input1 = Symbol.explode \"hello\"
- val input2 = Symbol.explode \"world\"
+\<open>let
+ val hw = $$ "h" || $$ "w"
+ val input1 = Symbol.explode "hello"
+ val input2 = Symbol.explode "world"
in
(hw input1, hw input2)
-end"
- "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
+end\<close>
+ \<open>(("h", ["e", "l", "l", "o"]), ("w", ["o", "r", "l", "d"]))\<close>}
The functions @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} work like the sequencing
function for parsers, except that they discard the item being parsed by the
@@ -163,95 +163,95 @@
For example:
@{ML_matchresult [display,gray]
-"let
- val just_e = $$ \"h\" |-- $$ \"e\"
- val just_h = $$ \"h\" --| $$ \"e\"
- val input = Symbol.explode \"hello\"
+\<open>let
+ val just_e = $$ "h" |-- $$ "e"
+ val just_h = $$ "h" --| $$ "e"
+ val input = Symbol.explode "hello"
in
(just_e input, just_h input)
-end"
- "((\"e\", [\"l\", \"l\", \"o\"]), (\"h\", [\"l\", \"l\", \"o\"]))"}
+end\<close>
+ \<open>(("e", ["l", "l", "o"]), ("h", ["l", "l", "o"]))\<close>}
- The parser @{ML "Scan.optional p x" for p x} returns the result of the parser
+ The parser @{ML \<open>Scan.optional p x\<close> for p x} returns the result of the parser
\<open>p\<close>, in case it succeeds; otherwise it returns
the default value \<open>x\<close>. For example:
@{ML_matchresult [display,gray]
-"let
- val p = Scan.optional ($$ \"h\") \"x\"
- val input1 = Symbol.explode \"hello\"
- val input2 = Symbol.explode \"world\"
+\<open>let
+ val p = Scan.optional ($$ "h") "x"
+ val input1 = Symbol.explode "hello"
+ val input2 = Symbol.explode "world"
in
(p input1, p input2)
-end"
- "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
+end\<close>
+ \<open>(("h", ["e", "l", "l", "o"]), ("x", ["w", "o", "r", "l", "d"]))\<close>}
The function @{ML_ind option in Scan} works similarly, except no default value can
be given. Instead, the result is wrapped as an \<open>option\<close>-type. For example:
@{ML_matchresult [display,gray]
-"let
- val p = Scan.option ($$ \"h\")
- val input1 = Symbol.explode \"hello\"
- val input2 = Symbol.explode \"world\"
+\<open>let
+ val p = Scan.option ($$ "h")
+ val input1 = Symbol.explode "hello"
+ val input2 = Symbol.explode "world"
in
(p input1, p input2)
-end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
+end\<close> \<open>((SOME "h", ["e", "l", "l", "o"]), (NONE, ["w", "o", "r", "l", "d"]))\<close>}
The function @{ML_ind ahead in Scan} parses some input, but leaves the original
input unchanged. For example:
@{ML_matchresult [display,gray]
- "Scan.ahead (Scan.this_string \"foo\") (Symbol.explode \"foo\")"
- "(\"foo\", [\"f\", \"o\", \"o\"])"}
+ \<open>Scan.ahead (Scan.this_string "foo") (Symbol.explode "foo")\<close>
+ \<open>("foo", ["f", "o", "o"])\<close>}
The function @{ML_ind "!!" in Scan} helps with producing appropriate error messages
during parsing. For example if you want to parse \<open>p\<close> immediately
followed by \<open>q\<close>, or start a completely different parser \<open>r\<close>,
you might write:
- @{ML [display,gray] "(p -- q) || r" for p q r}
+ @{ML [display,gray] \<open>(p -- q) || r\<close> for p q r}
However, this parser is problematic for producing a useful error
- message, if the parsing of @{ML "(p -- q)" for p q} fails. Because with the
+ message, if the parsing of @{ML \<open>(p -- q)\<close> for p q} fails. Because with the
parser above you lose the information that \<open>p\<close> should be followed by \<open>q\<close>.
To see this assume that \<open>p\<close> is present in the input, but it is not
- followed by \<open>q\<close>. That means @{ML "(p -- q)" for p q} will fail and
+ followed by \<open>q\<close>. That means @{ML \<open>(p -- q)\<close> for p q} will fail and
hence the alternative parser \<open>r\<close> will be tried. However, in many
circumstances this will be the wrong parser for the input ``\<open>p\<close>-followed-by-something''
and therefore will also fail. The error message is then caused by the failure
of \<open>r\<close>, not by the absence of \<open>q\<close> in the input. Such
- situation can be avoided when using the function @{ML "!!"}. This function
+ situation can be avoided when using the function @{ML \<open>!!\<close>}. This function
aborts the whole process of parsing in case of a failure and prints an error
message. For example if you invoke the parser
- @{ML [display,gray] "!! (fn _ => fn _ =>\"foo\") ($$ \"h\")"}
+ @{ML [display,gray] \<open>!! (fn _ => fn _ =>"foo") ($$ "h")\<close>}
on @{text [quotes] "hello"}, the parsing succeeds
@{ML_matchresult [display,gray]
- "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")"
- "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
+ \<open>(!! (fn _ => fn _ => "foo") ($$ "h")) (Symbol.explode "hello")\<close>
+ \<open>("h", ["e", "l", "l", "o"])\<close>}
but if you invoke it on @{text [quotes] "world"}
- @{ML_matchresult_fake [display,gray] "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
- "Exception ABORT raised"}
+ @{ML_matchresult_fake [display,gray] \<open>(!! (fn _ => fn _ => "foo") ($$ "h")) (Symbol.explode "world")\<close>
+ \<open>Exception ABORT raised\<close>}
then the parsing aborts and the error message \<open>foo\<close> is printed. In order to
see the error message properly, you need to prefix the parser with the function
@{ML_ind error in Scan}. For example:
@{ML_matchresult_fake [display,gray]
- "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
- "Exception Error \"foo\" raised"}
+ \<open>Scan.error (!! (fn _ => fn _ => "foo") ($$ "h")) (Symbol.explode "world")\<close>
+ \<open>Exception Error "foo" raised\<close>}
This kind of ``prefixing'' to see the correct error message is usually done by wrappers
such as @{ML_ind local_theory in Outer_Syntax}
(see Section~\ref{sec:newcommand} which explains this function in more detail).
- Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
+ Let us now return to our example of parsing @{ML \<open>(p -- q) || r\<close> for p q
r}. If you want to generate the correct error message for failure
of parsing \<open>p\<close>-followed-by-\<open>q\<close>, then you have to write:
\<close>
@@ -269,21 +269,21 @@
@{text [quotes] "h"}, @{text [quotes] "e"} and @{text [quotes] "w"}, and
the input @{text [quotes] "holle"}
- @{ML_matchresult_fake [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"holle\")"
- "Exception ERROR \"h is not followed by e\" raised"}
+ @{ML_matchresult_fake [display,gray] \<open>Scan.error (p_followed_by_q "h" "e" "w") (Symbol.explode "holle")\<close>
+ \<open>Exception ERROR "h is not followed by e" raised\<close>}
produces the correct error message. Running it with
- @{ML_matchresult [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"wworld\")"
- "((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}
+ @{ML_matchresult [display,gray] \<open>Scan.error (p_followed_by_q "h" "e" "w") (Symbol.explode "wworld")\<close>
+ \<open>(("w", "w"), ["o", "r", "l", "d"])\<close>}
yields the expected parsing.
- The function @{ML "Scan.repeat p" for p} will apply a parser \<open>p\<close> as
+ The function @{ML \<open>Scan.repeat p\<close> for p} will apply a parser \<open>p\<close> as
long as it succeeds. For example:
- @{ML_matchresult [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")"
- "([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
+ @{ML_matchresult [display,gray] \<open>Scan.repeat ($$ "h") (Symbol.explode "hhhhello")\<close>
+ \<open>(["h", "h", "h", "h"], ["e", "l", "l", "o"])\<close>}
Note that @{ML_ind repeat in Scan} stores the parsed items in a list. The function
@{ML_ind repeat1 in Scan} is similar, but requires that the parser \<open>p\<close>
@@ -294,8 +294,8 @@
the wrapper @{ML_ind finite in Scan} and the ``stopper-token''
@{ML_ind stopper in Symbol}. With them you can write:
- @{ML_matchresult [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")"
- "([\"h\", \"h\", \"h\", \"h\"], [])"}
+ @{ML_matchresult [display,gray] \<open>Scan.finite Symbol.stopper (Scan.repeat ($$ "h")) (Symbol.explode "hhhh")\<close>
+ \<open>(["h", "h", "h", "h"], [])\<close>}
The function @{ML stopper in Symbol} is the ``end-of-input'' indicator for parsing strings;
other stoppers need to be used when parsing, for example, tokens. However, this kind of
@@ -305,13 +305,13 @@
string as in
@{ML_matchresult [display,gray]
-"let
+\<open>let
val p = Scan.repeat (Scan.one Symbol.not_eof)
- val input = Symbol.explode \"foo bar foo\"
+ val input = Symbol.explode "foo bar foo"
in
Scan.finite Symbol.stopper p input
-end"
-"([\"f\", \"o\", \"o\", \" \", \"b\", \"a\", \"r\", \" \", \"f\", \"o\", \"o\"], [])"}
+end\<close>
+\<open>(["f", "o", "o", " ", "b", "a", "r", " ", "f", "o", "o"], [])\<close>}
where the function @{ML_ind not_eof in Symbol} ensures that we do not read beyond the
end of the input string (i.e.~stopper symbol).
@@ -319,13 +319,13 @@
The function @{ML_ind unless in Scan} takes two parsers: if the first one can
parse the input, then the whole parser fails; if not, then the second is tried. Therefore
- @{ML_matchresult_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"
- "Exception FAIL raised"}
+ @{ML_matchresult_fake_both [display,gray] \<open>Scan.unless ($$ "h") ($$ "w") (Symbol.explode "hello")\<close>
+ \<open>Exception FAIL raised\<close>}
fails, while
- @{ML_matchresult [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"world\")"
- "(\"w\",[\"o\", \"r\", \"l\", \"d\"])"}
+ @{ML_matchresult [display,gray] \<open>Scan.unless ($$ "h") ($$ "w") (Symbol.explode "world")\<close>
+ \<open>("w",["o", "r", "l", "d"])\<close>}
succeeds.
@@ -334,43 +334,43 @@
example below the marker symbol is a @{text [quotes] "*"}.
@{ML_matchresult [display,gray]
-"let
- val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))
- val input1 = Symbol.explode \"fooooo\"
- val input2 = Symbol.explode \"foo*ooo\"
+\<open>let
+ val p = Scan.repeat (Scan.unless ($$ "*") (Scan.one Symbol.not_eof))
+ val input1 = Symbol.explode "fooooo"
+ val input2 = Symbol.explode "foo*ooo"
in
(Scan.finite Symbol.stopper p input1,
Scan.finite Symbol.stopper p input2)
-end"
-"(([\"f\", \"o\", \"o\", \"o\", \"o\", \"o\"], []),
- ([\"f\", \"o\", \"o\"], [\"*\", \"o\", \"o\", \"o\"]))"}
+end\<close>
+\<open>((["f", "o", "o", "o", "o", "o"], []),
+ (["f", "o", "o"], ["*", "o", "o", "o"]))\<close>}
After parsing is done, you almost always want to apply a function to the parsed
items. One way to do this is the function @{ML_ind ">>" in Scan} where
- @{ML "(p >> f)" for p f} runs
+ @{ML \<open>(p >> f)\<close> for p f} runs
first the parser \<open>p\<close> and upon successful completion applies the
function \<open>f\<close> to the result. For example
@{ML_matchresult [display,gray]
-"let
+\<open>let
fun double (x, y) = (x ^ x, y ^ y)
- val parser = $$ \"h\" -- $$ \"e\"
+ val parser = $$ "h" -- $$ "e"
in
- (parser >> double) (Symbol.explode \"hello\")
-end"
-"((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"}
+ (parser >> double) (Symbol.explode "hello")
+end\<close>
+\<open>(("hh", "ee"), ["l", "l", "o"])\<close>}
doubles the two parsed input strings; or
@{ML_matchresult [display,gray]
-"let
+\<open>let
val p = Scan.repeat (Scan.one Symbol.not_eof)
- val input = Symbol.explode \"foo bar foo\"
+ val input = Symbol.explode "foo bar foo"
in
Scan.finite Symbol.stopper (p >> implode) input
-end"
-"(\"foo bar foo\",[])"}
+end\<close>
+\<open>("foo bar foo",[])\<close>}
where the single-character strings in the parsed output are transformed
back into one string.
@@ -380,8 +380,8 @@
untouched. For example
@{ML_matchresult [display,gray]
-"Scan.lift ($$ \"h\" -- $$ \"e\") (1, Symbol.explode \"hello\")"
-"((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
+\<open>Scan.lift ($$ "h" -- $$ "e") (1, Symbol.explode "hello")\<close>
+\<open>(("h", "e"), (1, ["l", "l", "o"]))\<close>}
\footnote{\bf FIXME: In which situations is \<open>lift\<close> useful? Give examples.}
@@ -426,8 +426,8 @@
loop, even if it is called without any input. For example
@{ML_matchresult_fake_both [display, gray]
- "parse_tree \"A\""
- "*** Exception- TOPLEVEL_ERROR raised"}
+ \<open>parse_tree "A"\<close>
+ \<open>*** Exception- TOPLEVEL_ERROR raised\<close>}
raises an exception indicating that the stack limit is reached. Such
looping parser are not useful, because of ML's strict evaluation of
@@ -450,20 +450,19 @@
exactly the parser what we wanted. An example is as follows:
@{ML_matchresult [display, gray]
- "let
- val input = Symbol.explode \"(A,((A))),A\"
+ \<open>let
+ val input = Symbol.explode "(A,((A))),A"
in
- Scan.finite Symbol.stopper (parse_tree \"A\") input
-end"
- "(Br (Br (Lf \"A\", Lf \"A\"), Lf \"A\"), [])"}
+ Scan.finite Symbol.stopper (parse_tree "A") input
+end\<close>
+ \<open>(Br (Br (Lf "A", Lf "A"), Lf "A"), [])\<close>}
\begin{exercise}\label{ex:scancmts}
Write a parser that parses an input string so that any comment enclosed
within \<open>(*\<dots>*)\<close> is replaced by the same comment but enclosed within
\<open>(**\<dots>**)\<close> in the output string. To enclose a string, you can use the
- function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML
- "s1 ^ s ^ s2" for s1 s2 s}. Hint: To simplify the task ignore the proper
+ function @{ML \<open>enclose s1 s2 s\<close> for s1 s2 s} which produces the string @{ML \<open>s1 ^ s ^ s2\<close> for s1 s2 s}. Hint: To simplify the task ignore the proper
nesting of comments.
\end{exercise}
\<close>
@@ -497,7 +496,7 @@
token parsers take into account the kind of tokens. The first example shows
how to generate a token list out of a string using the function
@{ML_ind explode in Token}. It is given the argument
- @{ML "Position.none"} since,
+ @{ML \<open>Position.none\<close>} since,
at the moment, we are not interested in generating precise error
messages. The following code
@@ -524,11 +523,11 @@
text \<open>
then lexing @{text [quotes] "hello world"} will produce
- @{ML_matchresult_fake [display,gray] "Token.explode
- (Thy_Header.get_keywords' @{context}) Position.none \"hello world\""
-"[Token (_,(Keyword, \"hello\"),_),
- Token (_,(Space, \" \"),_),
- Token (_,(Ident, \"world\"),_)]"}
+ @{ML_matchresult_fake [display,gray] \<open>Token.explode
+ (Thy_Header.get_keywords' @{context}) Position.none "hello world"\<close>
+\<open>[Token (_,(Keyword, "hello"),_),
+ Token (_,(Space, " "),_),
+ Token (_,(Ident, "world"),_)]\<close>}
Many parsing functions later on will require white space, comments and the like
to have already been filtered out. So from now on we are going to use the
@@ -536,12 +535,12 @@
For example:
@{ML_matchresult_fake [display,gray]
-"let
- val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none \"hello world\"
+\<open>let
+ val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none "hello world"
in
filter Token.is_proper input
-end"
-"[Token (_,(Ident, \"hello\"), _), Token (_,(Ident, \"world\"), _)]"}
+end\<close>
+\<open>[Token (_,(Ident, "hello"), _), Token (_,(Ident, "world"), _)]\<close>}
For convenience we define the function:
\<close>
@@ -554,10 +553,10 @@
If you now parse
@{ML_matchresult_fake [display,gray]
-"filtered_input \"inductive | for\""
-"[Token (_,(Command, \"inductive\"),_),
- Token (_,(Keyword, \"|\"),_),
- Token (_,(Keyword, \"for\"),_)]"}
+\<open>filtered_input "inductive | for"\<close>
+\<open>[Token (_,(Command, "inductive"),_),
+ Token (_,(Keyword, "|"),_),
+ Token (_,(Keyword, "for"),_)]\<close>}
you obtain a list consisting of only one command and two keyword tokens.
If you want to see which keywords and commands are currently known to Isabelle,
@@ -569,47 +568,47 @@
The parser @{ML_ind "$$$" in Parse} parses a single keyword. For example:
@{ML_matchresult [display,gray]
-"let
- val input1 = filtered_input \"where for\"
- val input2 = filtered_input \"| in\"
+\<open>let
+ val input1 = filtered_input "where for"
+ val input2 = filtered_input "| in"
in
- (Parse.$$$ \"where\" input1, Parse.$$$ \"|\" input2)
-end"
-"((\"where\",_), (\"|\",_))"}
+ (Parse.$$$ "where" input1, Parse.$$$ "|" input2)
+end\<close>
+\<open>(("where",_), ("|",_))\<close>}
Any non-keyword string can be parsed with the function @{ML_ind reserved in Parse}.
For example:
@{ML_matchresult [display,gray]
-"let
- val p = Parse.reserved \"bar\"
- val input = filtered_input \"bar\"
+\<open>let
+ val p = Parse.reserved "bar"
+ val input = filtered_input "bar"
in
p input
-end"
- "(\"bar\",[])"}
+end\<close>
+ \<open>("bar",[])\<close>}
- Like before, you can sequentially connect parsers with @{ML "--"}. For example:
+ Like before, you can sequentially connect parsers with @{ML \<open>--\<close>}. For example:
@{ML_matchresult [display,gray]
-"let
- val input = filtered_input \"| in\"
+\<open>let
+ val input = filtered_input "| in"
in
- (Parse.$$$ \"|\" -- Parse.$$$ \"in\") input
-end"
-"((\"|\", \"in\"), [])"}
+ (Parse.$$$ "|" -- Parse.$$$ "in") input
+end\<close>
+\<open>(("|", "in"), [])\<close>}
- The parser @{ML "Parse.enum s p" for s p} parses a possibly empty
+ The parser @{ML \<open>Parse.enum s p\<close> for s p} parses a possibly empty
list of items recognised by the parser \<open>p\<close>, where the items being parsed
are separated by the string \<open>s\<close>. For example:
@{ML_matchresult [display,gray]
-"let
- val input = filtered_input \"in | in | in foo\"
+\<open>let
+ val input = filtered_input "in | in | in foo"
in
- (Parse.enum \"|\" (Parse.$$$ \"in\")) input
-end"
-"([\"in\", \"in\", \"in\"], [_])"}
+ (Parse.enum "|" (Parse.$$$ "in")) input
+end\<close>
+\<open>(["in", "in", "in"], [_])\<close>}
The function @{ML_ind enum1 in Parse} works similarly, except that the
parsed list must be non-empty. Note that we had to add a string @{text
@@ -619,13 +618,13 @@
``stopper-token'' @{ML Token.stopper}. We can write:
@{ML_matchresult [display,gray]
-"let
- val input = filtered_input \"in | in | in\"
- val p = Parse.enum \"|\" (Parse.$$$ \"in\")
+\<open>let
+ val input = filtered_input "in | in | in"
+ val p = Parse.enum "|" (Parse.$$$ "in")
in
Scan.finite Token.stopper p input
-end"
-"([\"in\", \"in\", \"in\"], [])"}
+end\<close>
+\<open>(["in", "in", "in"], [])\<close>}
The following function will help to run examples.
\<close>
@@ -634,20 +633,19 @@
text \<open>
The function @{ML_ind "!!!" in Parse} can be used to force termination
- of the parser in case of a dead end, just like @{ML "Scan.!!"} (see previous
- section). A difference, however, is that the error message of @{ML
- "Parse.!!!"} is fixed to be @{text [quotes] "Outer syntax error"}
+ of the parser in case of a dead end, just like @{ML \<open>Scan.!!\<close>} (see previous
+ section). A difference, however, is that the error message of @{ML \<open>Parse.!!!\<close>} is fixed to be @{text [quotes] "Outer syntax error"}
together with a relatively precise description of the failure. For example:
@{ML_matchresult_fake [display,gray]
-"let
- val input = filtered_input \"in |\"
- val parse_bar_then_in = Parse.$$$ \"|\" -- Parse.$$$ \"in\"
+\<open>let
+ val input = filtered_input "in |"
+ val parse_bar_then_in = Parse.$$$ "|" -- Parse.$$$ "in"
in
parse (Parse.!!! parse_bar_then_in) input
-end"
-"Exception ERROR \"Outer syntax error: keyword \"|\" expected,
-but keyword in was found\" raised"
+end\<close>
+\<open>Exception ERROR "Outer syntax error: keyword "|" expected,
+but keyword in was found" raised\<close>
}
\begin{exercise} (FIXME)
@@ -672,9 +670,9 @@
where we pretend the parsed string starts on line 7. An example is
@{ML_matchresult_fake [display,gray]
-"filtered_input' \"foo \\n bar\""
-"[Token ((\"foo\", ({line=7, end_line=7}, {line=7})), (Ident, \"foo\"), _),
- Token ((\"bar\", ({line=8, end_line=8}, {line=8})), (Ident, \"bar\"), _)]"}
+\<open>filtered_input' "foo \\n bar"\<close>
+\<open>[Token (("foo", ({line=7, end_line=7}, {line=7})), (Ident, "foo"), _),
+ Token (("bar", ({line=8, end_line=8}, {line=8})), (Ident, "bar"), _)]\<close>}
in which the @{text [quotes] "\\n"} causes the second token to be in
line 8.
@@ -683,12 +681,12 @@
position and return it as part of the parser result. For example
@{ML_matchresult_fake [display,gray]
-"let
- val input = filtered_input' \"where\"
+\<open>let
+ val input = filtered_input' "where"
in
- parse (Parse.position (Parse.$$$ \"where\")) input
-end"
-"((\"where\", {line=7, end_line=7}), [])"}
+ parse (Parse.position (Parse.$$$ "where")) input
+end\<close>
+\<open>(("where", {line=7, end_line=7}), [])\<close>}
\begin{readmore}
The functions related to positions are implemented in the file
@@ -754,12 +752,12 @@
be parsed using the function @{ML_ind term in Parse}. For example:
@{ML_matchresult_fake [display,gray]
-"let
- val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none \"foo\"
+\<open>let
+ val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none "foo"
in
Parse.term input
-end"
-"(\"<markup>\", [])"}
+end\<close>
+\<open>("<markup>", [])\<close>}
The function @{ML_ind prop in Parse} is similar, except that it gives a different
@@ -767,15 +765,15 @@
the parsed string, but also some markup information. You can decode the
information with the function @{ML_ind parse in YXML} in @{ML_structure YXML}.
The result of the decoding is an XML-tree. You can see better what is going on if
- you replace @{ML Position.none} by @{ML "Position.line 42"}, say:
+ you replace @{ML Position.none} by @{ML \<open>Position.line 42\<close>}, say:
@{ML_matchresult_fake [display,gray]
-"let
- val input = Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 42) \"foo\"
+\<open>let
+ val input = Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 42) "foo"
in
YXML.parse (fst (Parse.term input))
-end"
-"Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"}
+end\<close>
+\<open>Elem ("token", [("line", "42"), ("end_line", "42")], [XML.Text "foo"])\<close>}
The positional information is stored as part of an XML-tree so that code
called later on will be able to give more precise error messages.
@@ -833,20 +831,20 @@
definition of @{term even} and @{term odd}:
@{ML_matchresult [display,gray]
-"let
+\<open>let
val input = filtered_input
- (\"even and odd \" ^
- \"where \" ^
- \" even0[intro]: \\\"even 0\\\" \" ^
- \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^
- \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
+ ("even and odd " ^
+ "where " ^
+ " even0[intro]: \"even 0\" " ^
+ "| evenS[intro]: \"odd n \<Longrightarrow> even (Suc n)\" " ^
+ "| oddS[intro]: \"even n \<Longrightarrow> odd (Suc n)\"")
in
parse spec_parser input
-end"
-"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
+end\<close>
+\<open>(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
[((even0,_),_),
((evenS,_),_),
- ((oddS,_),_)]), [])"}
+ ((oddS,_),_)]), [])\<close>}
\<close>
ML \<open>let
@@ -865,19 +863,19 @@
\isacommand{and}-separated
list of variables that can include optional type annotations and syntax translations.
For example:\footnote{Note that in the code we need to write
- \<open>\"int \<Rightarrow> bool\"\<close> in order to properly escape the double quotes
+ \<open>"int \<Rightarrow> bool"\<close> in order to properly escape the double quotes
in the compound type.}
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val input = filtered_input
- \"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\"
+ "foo::\"int \<Rightarrow> bool\" and bar::nat (\"BAR\" 100) and blonk"
in
parse Parse.vars input
-end"
-"([(foo, SOME _, NoSyn),
- (bar, SOME _, Mixfix (Source {text=\"BAR\",...}, [], 100, _)),
- (blonk, NONE, NoSyn)],[])"}
+end\<close>
+\<open>([(foo, SOME _, NoSyn),
+ (bar, SOME _, Mixfix (Source {text="BAR",...}, [], 100, _)),
+ (blonk, NONE, NoSyn)],[])\<close>}
\<close>
text \<open>
@@ -899,12 +897,12 @@
parsed by @{ML_ind prop in Parse}. However, they can include an optional
theorem name plus some attributes. For example
-@{ML_matchresult [display,gray] "let
- val input = filtered_input \"foo_lemma[intro,dest!]:\"
- val ((name, attrib), _) = parse (Parse_Spec.thm_name \":\") input
+@{ML_matchresult [display,gray] \<open>let
+ val input = filtered_input "foo_lemma[intro,dest!]:"
+ val ((name, attrib), _) = parse (Parse_Spec.thm_name ":") input
in
(name, map Token.name_of_src attrib)
-end" "(foo_lemma, [(\"intro\", _), (\"dest\", _)])"}
+end\<close> \<open>(foo_lemma, [("intro", _), ("dest", _)])\<close>}
The function @{ML_ind opt_thm_name in Parse_Spec} is the ``optional'' variant of
@{ML_ind thm_name in Parse_Spec}. Theorem names can contain attributes. The name
@@ -1019,7 +1017,7 @@
behaviour of the command. In the code above we used a
``do-nothing''-function, which because of the parser @{ML_ind succeed in Scan}
does not parse any argument, but immediately returns the simple
- function @{ML "Local_Theory.background_theory I"}. We can replace
+ function @{ML \<open>Local_Theory.background_theory I\<close>}. We can replace
this code by a function that first parses a proposition (using the
parser @{ML Parse.prop}), then prints out some tracing information
(using the function \<open>trace_prop\<close>) and finally does
@@ -1051,8 +1049,7 @@
``open up'' a proof in order to prove the proposition (for example
\isacommand{lemma}) or prove some other properties (for example
\isacommand{function}). To achieve this kind of behaviour, you have to use
- the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML
- "local_theory_to_proof" in Outer_Syntax} to set up the command.
+ the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML \<open>local_theory_to_proof\<close> in Outer_Syntax} to set up the command.
Below we show the command \isacommand{foobar\_goal} which takes a
proposition as argument and then starts a proof in order to prove
it. Therefore, we need to announce this command in the header
@@ -1084,7 +1081,7 @@
@{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.
In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the
proposition. Its argument @{ML NONE} stands for a locale (which we chose to
- omit); the argument @{ML "(K I)"} stands for a function that determines what
+ omit); the argument @{ML \<open>(K I)\<close>} stands for a function that determines what
should be done with the theorem once it is proved (we chose to just forget
about it).
--- a/ProgTutorial/Readme.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Readme.thy Fri May 17 10:38:01 2019 +0200
@@ -39,7 +39,7 @@
The following antiquotations are defined:
\begin{itemize}
- \item[$\bullet$] \<open>@{ML "expr" for vars in structs}\<close> should be used
+ \item[$\bullet$] \<open>@{ML \<open>expr\<close> for vars in structs}\<close> should be used
for displaying any ML-ex\-pression, because the antiquotation checks whether
the expression is valid ML-code. The \<open>for\<close>- and \<open>in\<close>-arguments are optional. The former is used for evaluating open
expressions by giving a list of free variables. The latter is used to
@@ -48,23 +48,23 @@
\begin{center}\small
\begin{tabular}{lll}
- \<open>@{ML "1 + 3"}\<close> & & @{ML "1 + 3"}\\
- \<open>@{ML "a + b" for a b}\<close> & \;\;produce\;\; & @{ML "a + b" for a b}\\
- \<open>@{ML Ident in OuterLex}\<close> & & @{ML Ident in OuterLex}\\
+ \<open>@{ML \<open>1 + 3\<close>}\<close> & & @{ML \<open>1 + 3\<close>}\\
+ \<open>@{ML \<open>a + b\<close> for a b}\<close> & \;\;produce\;\; & @{ML \<open>a + b\<close> for a b}\\
+ \<open>@{ML explode in Symbol}\<close> & & @{ML explode in Symbol}\\
\end{tabular}
\end{center}
- \item[$\bullet$] \<open>@{ML_matchresult "expr" "pat"}\<close> should be used to
+ \item[$\bullet$] \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> should be used to
display ML-expressions and their response. The first expression is checked
- like in the antiquotation \<open>@{ML "expr"}\<close>; the second is a pattern
+ like in the antiquotation \<open>@{ML \<open>expr\<close>}\<close>; the second is a pattern
that specifies the result the first expression produces. This pattern can
contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the
first expression will be checked against this pattern. Examples are:
\begin{center}\small
\begin{tabular}{l}
- \<open>@{ML_matchresult "1+2" "3"}\<close>\\
- \<open>@{ML_matchresult "(1+2,3)" "(3,\<dots>)"}\<close>
+ \<open>@{ML_matchresult \<open>1+2\<close> \<open>3\<close>}\<close>\\
+ \<open>@{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,\<dots>)\<close>}\<close>
\end{tabular}
\end{center}
@@ -72,8 +72,8 @@
\begin{center}\small
\begin{tabular}{p{3cm}p{3cm}}
- @{ML_matchresult "1+2" "3"} &
- @{ML_matchresult "(1+2,3)" "(3,\<dots>)"}
+ @{ML_matchresult \<open>1+2\<close> \<open>3\<close>} &
+ @{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,_)\<close>}
\end{tabular}
\end{center}
@@ -82,16 +82,16 @@
an abstract datatype (like @{ML_type thm} or @{ML_type cterm}).
\item[$\bullet$] \<open>@{ML_matchresult_fake "expr" "pat"}\<close> works just
- like the antiquotation \<open>@{ML_matchresult "expr" "pat"}\<close> above,
+ like the antiquotation \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> above,
except that the result-specification is not checked. Use this antiquotation
when the result cannot be constructed or the code generates an
exception. Examples are:
\begin{center}\small
\begin{tabular}{ll}
- \<open>@{ML_matchresult_fake\<close> & \<open>"cterm_of @{theory} @{term \"a + b = c\"}"}\<close>\\
+ \<open>@{ML_matchresult_fake\<close> & \<open>"cterm_of @{theory} @{term "a + b = c"}"}\<close>\\
& \<open>"a + b = c"}\<close>\smallskip\\
- \<open>@{ML_matchresult_fake\<close> & \<open>"($$ \"x\") (explode \"world\")"\<close>\\
+ \<open>@{ML_matchresult_fake\<close> & \<open>"($$ "x") (explode "world")"\<close>\\
& \<open>"Exception FAIL raised"}\<close>
\end{tabular}
\end{center}
@@ -100,8 +100,8 @@
\begin{center}\small
\begin{tabular}{p{7.2cm}}
- @{ML_matchresult_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\
- @{ML_matchresult_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"}
+ @{ML_matchresult_fake \<open>Thm.cterm_of @{context} @{term "a + b = c"}\<close> \<open>a + b = c\<close>}\smallskip\\
+ @{ML_matchresult_fake \<open>($$ "x") (Symbol.explode "world")\<close> \<open>Exception FAIL raised\<close>}
\end{tabular}
\end{center}
@@ -114,7 +114,7 @@
\begin{center}\small
\begin{tabular}{ll}
- \<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm \"1 + True\"}"\<close>\\
+ \<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm "1 + True"}"\<close>\\
& \<open>"Type unification failed \<dots>"}\<close>
\end{tabular}
\end{center}
@@ -123,20 +123,20 @@
referring to a file. It checks whether the file exists. An example
is
- @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"}
+ @{text [display] \<open>@{ML_file "Pure/General/basics.ML"}\<close>}
\end{itemize}
The listed antiquotations honour options including \<open>[display]\<close> and
\<open>[quotes]\<close>. For example
\begin{center}\small
- \<open>@{ML [quotes] "\"foo\" ^ \"bar\""}\<close> \;\;produces\;\; @{text [quotes] "foobar"}
+ \<open>@{ML [quotes] \<open>"foo" ^ "bar"\<close>}\<close> \;\;produces\;\; @{text [quotes] "foobar"}
\end{center}
whereas
\begin{center}\small
- \<open>@{ML "\"foo\" ^ \"bar\""}\<close> \;\;produces only\;\; \<open>foobar\<close>
+ \<open>@{ML \<open>"foo" ^ "bar"\<close>}\<close> \;\;produces only\;\; \<open>foobar\<close>
\end{center}
\item Functions and value bindings cannot be defined inside antiquotations; they need
--- a/ProgTutorial/Recipes/Antiquotes.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Antiquotes.thy Fri May 17 10:38:01 2019 +0200
@@ -31,11 +31,10 @@
We first describe the antiquotation \<open>ML_checked\<close> with the syntax:
- @{text [display] "@{ML_checked \"a_piece_of_code\"}"}
+ @{text [display] \<open>@{ML_checked "a_piece_of_code"}\<close>}
The code is checked by sending the ML-expression @{text [quotes] "val _ =
- a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML
- "ML_Context.eval_source_in"} in Line 7 below). The complete code of the
+ a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML \<open>ML_Context.eval_source_in\<close>} in Line 7 below). The complete code of the
document antiquotation is as follows:
\<close>
@@ -58,26 +57,26 @@
text \<open>
- The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this
+ The parser @{ML \<open>(Scan.lift Args.name)\<close>} in Line 7 parses a string, in this
case the code, and then calls the function @{ML output_ml}. As mentioned
before, the parsed code is sent to the ML-compiler in Line 4 using the
function @{ML ml_val}, which constructs the appropriate ML-expression, and
- using @{ML "eval_in" in ML_Context}, which calls the compiler. If the code is
- ``approved'' by the compiler, then the output function @{ML "output" in
+ using @{ML \<open>eval_in\<close> in ML_Context}, which calls the compiler. If the code is
+ ``approved'' by the compiler, then the output function @{ML \<open>output\<close> in
Document_Antiquotation} in the next line pretty prints the code. This function expects
that the code is a list of (pretty)strings where each string correspond to a
- line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)"
+ line in the output. Therefore the use of @{ML \<open>(space_explode "\\n" txt)\<close>
for txt} which produces such a list according to linebreaks. There are a
number of options for antiquotations that are observed by the function
- @{ML "output" in Document_Antiquotation} when printing the code (including \<open>[display]\<close>
- and \<open>[quotes]\<close>). The function @{ML "antiquotation_raw" in Thy_Output} in
+ @{ML \<open>output\<close> in Document_Antiquotation} when printing the code (including \<open>[display]\<close>
+ and \<open>[quotes]\<close>). The function @{ML \<open>antiquotation_raw\<close> in Thy_Output} in
Line 7 sets up the new document antiquotation.
\begin{readmore}
For more information about options of document antiquotations see \rsccite{sec:antiq}).
\end{readmore}
- Since we used the argument @{ML "Position.none"}, the compiler cannot give specific
+ Since we used the argument @{ML \<open>Position.none\<close>}, the compiler cannot give specific
information about the line number, in case an error is detected. We
can improve the code above slightly by writing
\<close>
@@ -116,7 +115,7 @@
going to implement the document antiquotation:
- @{text [display] "@{ML_resp \"a_piece_of_code\" \"a_pattern\"}"}
+ @{text [display] \<open>@{ML_resp "a_piece_of_code" "a_pattern"}\<close>}
To add some convenience and also to deal with large outputs, the user can
give a partial specification by using ellipses. For example \<open>(\<dots>, \<dots>)\<close>
@@ -193,7 +192,7 @@
the output (Lines 4 to 7) and the parser in the setup (Line 11). Now
you can write
- @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"}
+ @{text [display] \<open>@{ML_resp [display] "true andalso false" "false"}\<close>}
to obtain
@@ -201,7 +200,7 @@
or
- @{text [display] "@{ML_resp [display] \"let val i = 3 in (i * i, \"foo\") end\" \"(9, \<dots>)\"}"}
+ @{text [display] \<open>@{ML_resp [display] "let val i = 3 in (i * i, "foo") end" "(9, \<dots>)"}\<close>}
to obtain
--- a/ProgTutorial/Recipes/ExternalSolver.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/ExternalSolver.thy Fri May 17 10:38:01 2019 +0200
@@ -20,7 +20,7 @@
For example, consider running an ordinary shell commands:
@{ML_matchresult [display,gray]
- "Isabelle_System.bash_output \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}
+ \<open>Isabelle_System.bash_output "echo Hello world!"\<close> \<open>("Hello world!\n", 0)\<close>}
Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}
on Page~\pageref{rec:timeout}), i.e. external applications are killed
@@ -28,8 +28,8 @@
one second:
@{ML_matchresult_fake [display,gray]
- "Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\"
- handle TIMEOUT => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
+ \<open>Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output "sleep 30"
+ handle TIMEOUT => ("timeout", ~1)\<close> \<open>("timeout", ~1)\<close>}
The function @{ML bash_output in Isabelle_System} can also be used for more reasonable
applications, e.g. coupling external solvers with Isabelle. In that case,
@@ -46,7 +46,7 @@
In Isabelle, this application may now be executed by
- @{ML_matchresult_fake [display,gray] "Isabelle_System.bash_output \"$FOO\"" "\<dots>"}
+ @{ML_matchresult_fake [display,gray] \<open>Isabelle_System.bash_output "$FOO"\<close> \<open>\<dots>\<close>}
\<close>
--- a/ProgTutorial/Recipes/Introspection.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Introspection.thy Fri May 17 10:38:01 2019 +0200
@@ -53,10 +53,10 @@
established theorem. This can be done with
@{ML_matchresult [display,gray]
- "@{thm my_conjIa}
+ \<open>@{thm my_conjIa}
|> Thm.proof_body_of
- |> get_names"
- "[\"Introspection.my_conjIa\"]"}
+ |> get_names\<close>
+ \<open>["Introspection.my_conjIa"]\<close>}
\<close>
text \<open>
whereby \<open>Introspection\<close> refers to the theory name in which
@@ -68,13 +68,13 @@
first level of the proof-tree, as follows.
@{ML_matchresult_fake [display,gray]
- "@{thm my_conjIa}
+ \<open>@{thm my_conjIa}
|> Thm.proof_body_of
|> get_pbodies
|> map get_names
- |> List.concat"
- "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\",
- \"Pure.protectI\"]"}
+ |> List.concat\<close>
+ \<open>["HOL.conjunct2", "HOL.conjunct1", "HOL.conjI", "Pure.protectD",
+ "Pure.protectI"]\<close>}
\<close>
text \<open>
The theorems @{thm [source] protectD} and @{thm [source]
@@ -83,12 +83,12 @@
count as a separate theorem, as you can see in the following code.
@{ML_matchresult_fake [display,gray]
- "@{thm my_conjIb}
+ \<open>@{thm my_conjIb}
|> Thm.proof_body_of
|> get_pbodies
|> map get_names
- |> List.concat"
- "[\"Pure.protectD\", \"Pure.protectI\"]"}
+ |> List.concat\<close>
+ \<open>["Pure.protectD", "Pure.protectI"]\<close>}
\<close>
text \<open>
Interestingly, but not surprisingly, the proof of @{thm [source]
@@ -97,14 +97,14 @@
are returned for @{thm [source] my_conjIc}.
@{ML_matchresult_fake [display,gray]
- "@{thm my_conjIc}
+ \<open>@{thm my_conjIc}
|> Thm.proof_body_of
|> get_pbodies
|> map get_names
- |> List.concat"
- "[\"HOL.implies_True_equals\", \"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\",
- \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
- \"Pure.protectI\"]"}
+ |> List.concat\<close>
+ \<open>["HOL.implies_True_equals", "HOL.Eq_TrueI", "HOL.simp_thms_25", "HOL.eq_reflection",
+ "HOL.conjunct2", "HOL.conjunct1", "HOL.TrueI", "Pure.protectD",
+ "Pure.protectI"]\<close>}
\<close>
text \<open>
Of course we can also descend into the second level of the tree
@@ -113,16 +113,16 @@
@{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
@{ML_matchresult_fake [display, gray]
- "@{thm my_conjIa}
+ \<open>@{thm my_conjIa}
|> Thm.proof_body_of
|> get_pbodies
|> map get_pbodies
|> (map o map) get_names
|> List.concat
|> List.concat
- |> duplicates (op =)"
- "[\"\", \"Pure.protectD\",
- \"Pure.protectI\"]"}
+ |> duplicates (op =)\<close>
+ \<open>["", "Pure.protectD",
+ "Pure.protectI"]\<close>}
\<close>
--- a/ProgTutorial/Recipes/Oracle.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Oracle.thy Fri May 17 10:38:01 2019 +0200
@@ -76,21 +76,18 @@
text \<open>
Here is the string representation of the term @{term "p = (q = p)"}:
- @{ML_matchresult
- "translate @{term \"p = (q = p)\"}"
- "\" ( p <=> ( q <=> p ) ) \""}
+ @{ML_matchresult \<open>translate @{term "p = (q = p)"}\<close>
+ \<open>" ( p <=> ( q <=> p ) ) "\<close>}
Let us check, what the solver returns when given a tautology:
- @{ML_matchresult
- "IffSolver.decide (translate @{term \"p = (q = p) = q\"})"
- "true"}
+ @{ML_matchresult \<open>IffSolver.decide (translate @{term "p = (q = p) = q"})\<close>
+ \<open>true\<close>}
And here is what it returns for a formula which is not valid:
- @{ML_matchresult
- "IffSolver.decide (translate @{term \"p = (q = p)\"})"
- "false"}
+ @{ML_matchresult \<open>IffSolver.decide (translate @{term "p = (q = p)"})\<close>
+ \<open>false\<close>}
\<close>
text \<open>
@@ -113,7 +110,7 @@
text \<open>
Here is what we get when applying the oracle:
- @{ML_matchresult_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"}
+ @{ML_matchresult_fake \<open>iff_oracle @{cprop "p = (p::bool)"}\<close> \<open>p = p\<close>}
(FIXME: is there a better way to present the theorem?)
--- a/ProgTutorial/Recipes/Sat.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Sat.thy Fri May 17 10:38:01 2019 +0200
@@ -33,7 +33,7 @@
text \<open>
then the resulting propositional formula @{ML pform} is
- @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in Prop_Logic}
+ @{ML [display] \<open>Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)\<close> in Prop_Logic}
where indices are assigned for the variables
@@ -43,8 +43,8 @@
input table is empty (i.e.~@{ML Termtab.empty}) and the output table is
@{ML_matchresult_fake [display,gray]
- "Termtab.dest table"
- "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"}
+ \<open>Termtab.dest table\<close>
+ \<open>[(Free ("A", "bool"), 1), (Free ("B", "bool"), 2)]\<close>}
An index is also produced whenever the translation
function cannot find an appropriate propositional formula for a term.
@@ -55,22 +55,22 @@
Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty\<close>
text \<open>
- returns @{ML "BoolVar 1" in Prop_Logic} for @{ML pform'} and the table
+ returns @{ML \<open>BoolVar 1\<close> in Prop_Logic} for @{ML pform'} and the table
@{ML table'} is:
@{ML_matchresult_fake [display,gray]
- "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')"
- "(\<forall>x. P x, 1)"}
+ \<open>map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')\<close>
+ \<open>(\<forall>x. P x, 1)\<close>}
In the print out of the tabel, we used some pretty printing scaffolding
to see better which assignment the table contains.
Having produced a propositional formula, you can now call the SAT solvers
- with the function @{ML "SAT_Solver.invoke_solver"}. For example
+ with the function @{ML \<open>SAT_Solver.invoke_solver\<close>}. For example
@{ML_matchresult_fake [display,gray]
- "SAT_Solver.invoke_solver \"minisat\" pform"
- "SAT_Solver.SATISFIABLE assg"}
+ \<open>SAT_Solver.invoke_solver "minisat" pform\<close>
+ \<open>SAT_Solver.SATISFIABLE assg\<close>}
\<close>
text \<open>
@@ -78,12 +78,12 @@
the returned function \<open>assg\<close>
@{ML_matchresult [display,gray]
-"let
- val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver \"auto\" pform
+\<open>let
+ val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver "auto" pform
in
(assg 1, assg 2, assg 3)
-end"
- "(NONE, SOME true, NONE)"}
+end\<close>
+ \<open>(NONE, SOME true, NONE)\<close>}
we obtain a possible assignment for the variables \<open>A\<close> an \<open>B\<close>
that makes the formula satisfiable.
@@ -102,7 +102,7 @@
done
text \<open>
- However, for proving anything more exciting using @{ML "sat_tac" in SAT} you
+ However, for proving anything more exciting using @{ML \<open>sat_tac\<close> in SAT} you
have to use a SAT solver that can produce a proof. The internal
one is not usuable for this.
--- a/ProgTutorial/Recipes/TimeLimit.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/TimeLimit.thy Fri May 17 10:38:01 2019 +0200
@@ -21,25 +21,25 @@
Now the call
- @{ML_matchresult_fake_both [display,gray] "ackermann (4, 12)" "\<dots>"}
+ @{ML_matchresult_fake_both [display,gray] \<open>ackermann (4, 12)\<close> \<open>\<dots>\<close>}
takes a bit of time before it finishes. To avoid this, the call can be encapsulated
in a time limit of five seconds. For this you have to write
@{ML_matchresult_fake_both [display,gray]
-"Timeout.apply (Time.fromSeconds 5) ackermann (4, 12)
- handle TIMEOUT => ~1"
-"~1"}
+\<open>Timeout.apply (Time.fromSeconds 5) ackermann (4, 12)
+ handle TIMEOUT => ~1\<close>
+\<open>~1\<close>}
where \<open>TimeOut\<close> is the exception raised when the time limit
is reached.
- Note that @{ML "apply" in Timeout} is only meaningful when you use PolyML 5.2.1
+ Note that @{ML \<open>apply\<close> in Timeout} is only meaningful when you use PolyML 5.2.1
or later, because this version of PolyML has the infrastructure for multithreaded
- programming on which @{ML "apply" in Timeout} relies.
+ programming on which @{ML \<open>apply\<close> in Timeout} relies.
\begin{readmore}
- The function @{ML "apply" in Timeout} is defined in the structure
+ The function @{ML \<open>apply\<close> in Timeout} is defined in the structure
@{ML_structure Timeout} which can be found in the file
@{ML_file "Pure/concurrent/timeout.ML"}.
\end{readmore}
--- a/ProgTutorial/Recipes/Timing.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Timing.thy Fri May 17 10:38:01 2019 +0200
@@ -41,7 +41,7 @@
tactics are lazy functions and you need to force them to run, otherwise the
timing will be meaningless. The simplifier tactic, amongst others, can be
forced to run by just applying the state to it. But ``fully'' lazy tactics,
- such as @{ML "resolve_tac"}, need even more ``standing-on-ones-head'' to force
+ such as @{ML \<open>resolve_tac\<close>}, need even more ``standing-on-ones-head'' to force
them to run.
The time between start and finish of the simplifier will be calculated
--- a/ProgTutorial/Solutions.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Solutions.thy Fri May 17 10:38:01 2019 +0200
@@ -56,11 +56,11 @@
as follows:
@{ML_matchresult_fake [display,gray]
- "@{prop \"\<forall>x y z. P x = P z\"}
+ \<open>@{prop "\<forall>x y z. P x = P z"}
|> kill_trivial_quantifiers
|> pretty_term @{context}
- |> pwriteln"
- "\<forall>x z. P x = P z"}
+ |> pwriteln\<close>
+ \<open>\<forall>x z. P x = P z\<close>}
\<close>
@@ -111,13 +111,13 @@
normally return. For example:
@{ML_matchresult [display,gray]
-"let
- val input1 = (Symbol.explode \"foo bar\")
- val input2 = (Symbol.explode \"foo (*test*) bar (*test*)\")
+\<open>let
+ val input1 = (Symbol.explode "foo bar")
+ val input2 = (Symbol.explode "foo (*test*) bar (*test*)")
in
(scan_all input1, scan_all input2)
-end"
-"(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
+end\<close>
+\<open>("foo bar", "foo (**test**) bar (**test**)")\<close>}
\<close>
text \<open>\solution{ex:contextfree}\<close>
@@ -331,8 +331,8 @@
This function generates for example:
@{ML_matchresult_fake [display,gray]
- "pwriteln (pretty_term @{context} (term_tree 2))"
- "(1 + 2) + (3 + 4)"}
+ \<open>pwriteln (pretty_term @{context} (term_tree 2))\<close>
+ \<open>(1 + 2) + (3 + 4)\<close>}
The next function constructs a goal of the form \<open>P \<dots>\<close> with a term
produced by @{ML term_tree} filled in.
@@ -344,7 +344,7 @@
Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
two tactics, \<open>c_tac\<close> and \<open>s_tac\<close>, for the conversion and simproc,
respectively. The idea is to first apply the conversion (respectively simproc) and
- then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}.
+ then prove the remaining goal using @{ML \<open>cheat_tac\<close> in Skip_Proof}.
\<close>
ML Skip_Proof.cheat_tac
--- a/ProgTutorial/Tactical.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Tactical.thy Fri May 17 10:38:01 2019 +0200
@@ -48,17 +48,17 @@
This proof translates to the following ML-code.
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val ctxt = @{context}
- val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
+ val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
in
- Goal.prove ctxt [\"P\", \"Q\"] [] goal
+ Goal.prove ctxt ["P", "Q"] [] goal
(fn _ => eresolve_tac @{context} [@{thm disjE}] 1
THEN resolve_tac @{context} [@{thm disjI2}] 1
THEN assume_tac @{context} 1
THEN resolve_tac @{context} [@{thm disjI1}] 1
THEN assume_tac @{context} 1)
-end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
+end\<close> \<open>?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P\<close>}
To start the proof, the function @{ML_ind prove in Goal} sets up a goal
state for proving the goal @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. We can give this
@@ -764,16 +764,16 @@
The function @{ML_ind RS in Drule}, for example, does this.
@{ML_matchresult_fake [display,gray]
- "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
+ \<open>@{thm disjI1} RS @{thm conjI}\<close> \<open>\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q\<close>}
In this example it instantiates the first premise of the \<open>conjI\<close>-theorem
with the theorem \<open>disjI1\<close>. If the instantiation is impossible, as in the
case of
@{ML_matchresult_fake_both [display,gray]
- "@{thm conjI} RS @{thm mp}"
-"*** Exception- THM (\"RSN: no unifiers\", 1,
-[\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
+ \<open>@{thm conjI} RS @{thm mp}\<close>
+\<open>*** Exception- THM ("RSN: no unifiers", 1,
+["\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q", "\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q"]) raised\<close>}
then the function raises an exception. The function @{ML_ind RSN in Drule}
is similar to @{ML RS}, but takes an additional number as argument. This
@@ -783,8 +783,8 @@
the function @{ML_ind MRS in Drule}:
@{ML_matchresult_fake [display,gray]
- "[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}"
- "\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"}
+ \<open>[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}\<close>
+ \<open>\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)\<close>}
If you need to instantiate lists of theorems, you can use the
functions @{ML_ind RL in Drule} and @{ML_ind OF in Drule}. For
@@ -792,16 +792,16 @@
instantiated with every theorem in the first.
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val list1 = [@{thm impI}, @{thm disjI2}]
val list2 = [@{thm conjI}, @{thm disjI1}]
in
list1 RL list2
-end"
-"[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q,
+end\<close>
+\<open>[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q,
\<lbrakk>?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q,
(?P1 \<Longrightarrow> ?Q1) \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<or> ?Q,
- ?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]"}
+ ?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]\<close>}
\begin{readmore}
The combinators for instantiating theorems with other theorems are
@@ -981,7 +981,7 @@
There is even another way of implementing this tactic: in automatic proof
procedures (in contrast to tactics that might be called by the user) there
are often long lists of tactics that are applied to the first
- subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' @{context} 1"},
+ subgoal. Instead of writing the code above and then calling @{ML \<open>foo_tac'' @{context} 1\<close>},
you can also just write
\<close>
@@ -1097,7 +1097,7 @@
convention therefore, tactics visible to the user should either change
something or fail.
- To comply with this convention, we could simply delete the @{ML "K all_tac"}
+ To comply with this convention, we could simply delete the @{ML \<open>K all_tac\<close>}
in @{ML select_tac'} or delete @{ML TRY} from @{ML select_tac''}. But for
the sake of argument, let us suppose that this deletion is \emph{not} an
option. In such cases, you can use the combinator @{ML_ind CHANGED in
@@ -1459,10 +1459,10 @@
empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier}
@{ML_matchresult_fake [display,gray]
- "print_ss @{context} empty_ss"
-"Simplification rules:
+ \<open>print_ss @{context} empty_ss\<close>
+\<open>Simplification rules:
Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
you can see it contains nothing. This simpset is usually not useful, except as a
building block to build bigger simpsets. For example you can add to @{ML empty_ss}
@@ -1475,11 +1475,11 @@
Printing then out the components of the simpset gives:
@{ML_matchresult_fake [display,gray]
- "print_ss @{context} (Raw_Simplifier.simpset_of ss1)"
-"Simplification rules:
+ \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss1)\<close>
+\<open>Simplification rules:
??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
\footnote{\bf FIXME: Why does it print out ??.unknown}
@@ -1492,13 +1492,13 @@
gives
@{ML_matchresult_fake [display,gray]
- "print_ss @{context} (Raw_Simplifier.simpset_of ss2)"
-"Simplification rules:
+ \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss2)\<close>
+\<open>Simplification rules:
??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
Congruences rules:
Complete_Lattices.Inf_class.INFIMUM:
\<lbrakk>A1 = B1; \<And>x. x \<in> B1 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1
-Simproc patterns:"}
+Simproc patterns:\<close>}
Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss}
expects this form of the simplification and congruence rules. This is
@@ -1509,10 +1509,10 @@
HOL_basic_ss in Simpdata}. While printing out the components of this simpset
@{ML_matchresult_fake [display,gray]
- "print_ss @{context} HOL_basic_ss"
-"Simplification rules:
+ \<open>print_ss @{context} HOL_basic_ss\<close>
+\<open>Simplification rules:
Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
also produces ``nothing'', the printout is somewhat misleading. In fact
the @{ML HOL_basic_ss} is setup so that it can solve goals of the
@@ -1543,8 +1543,8 @@
connectives in HOL.
@{ML_matchresult_fake [display,gray]
- "print_ss @{context} HOL_ss"
-"Simplification rules:
+ \<open>print_ss @{context} HOL_ss\<close>
+\<open>Simplification rules:
Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V
HOL.the_eq_trivial: THE x. x = y \<equiv> y
HOL.the_sym_eq_trivial: THE ya. y = ya \<equiv> y
@@ -1554,7 +1554,7 @@
\<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')
op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
Simproc patterns:
- \<dots>"}
+ \<dots>\<close>}
\begin{readmore}
The simplifier for HOL is set up in @{ML_file "HOL/Tools/simpdata.ML"}.
@@ -1755,7 +1755,7 @@
(FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy)
- (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.)
+ (FIXME: explain @{ML simplify} and @{ML \<open>Simplifier.rewrite_rule\<close>} etc.)
\<close>
@@ -2065,29 +2065,29 @@
instance of the (meta)reflexivity theorem. For example:
@{ML_matchresult_fake [display,gray]
- "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
- "Foo \<or> Bar \<equiv> Foo \<or> Bar"}
+ \<open>Conv.all_conv @{cterm "Foo \<or> Bar"}\<close>
+ \<open>Foo \<or> Bar \<equiv> Foo \<or> Bar\<close>}
Another simple conversion is @{ML_ind no_conv in Conv} which always raises the
exception @{ML CTERM}.
@{ML_matchresult_fake [display,gray]
- "Conv.no_conv @{cterm True}"
- "*** Exception- CTERM (\"no conversion\", []) raised"}
+ \<open>Conv.no_conv @{cterm True}\<close>
+ \<open>*** Exception- CTERM ("no conversion", []) raised\<close>}
A more interesting conversion is the function @{ML_ind beta_conversion in Thm}: it
produces a meta-equation between a term and its beta-normal form. For example
@{ML_matchresult_fake [display,gray]
- "let
- val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
- val two = @{cterm \"2::nat\"}
- val ten = @{cterm \"10::nat\"}
+ \<open>let
+ val add = @{cterm "\<lambda>x y. x + (y::nat)"}
+ val two = @{cterm "2::nat"}
+ val ten = @{cterm "10::nat"}
val ctrm = Thm.apply (Thm.apply add two) ten
in
Thm.beta_conversion true ctrm
-end"
- "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
+end\<close>
+ \<open>((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10\<close>}
If you run this example, you will notice that the actual response is the
seemingly nonsensical @{term
@@ -2097,25 +2097,25 @@
we obtain the expected result.
@{ML_matchresult [display,gray]
-"let
- val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
- val two = @{cterm \"2::nat\"}
- val ten = @{cterm \"10::nat\"}
+\<open>let
+ val add = @{cterm "\<lambda>x y. x + (y::nat)"}
+ val two = @{cterm "2::nat"}
+ val ten = @{cterm "10::nat"}
val ctrm = Thm.apply (Thm.apply add two) ten
in
Thm.prop_of (Thm.beta_conversion true ctrm)
-end"
-"Const (\"Pure.eq\",_) $
- (Abs (\"x\",_,Abs (\"y\",_,_)) $_$_) $
- (Const (\"Groups.plus_class.plus\",_) $ _ $ _)"}
+end\<close>
+\<open>Const ("Pure.eq",_) $
+ (Abs ("x",_,Abs ("y",_,_)) $_$_) $
+ (Const ("Groups.plus_class.plus",_) $ _ $ _)\<close>}
or in the pretty-printed form
@{ML_matchresult_fake [display,gray]
-"let
- val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
- val two = @{cterm \"2::nat\"}
- val ten = @{cterm \"10::nat\"}
+\<open>let
+ val add = @{cterm "\<lambda>x y. x + (y::nat)"}
+ val two = @{cterm "2::nat"}
+ val ten = @{cterm "10::nat"}
val ctrm = Thm.apply (Thm.apply add two) ten
val ctxt = @{context}
|> Config.put eta_contract false
@@ -2124,8 +2124,8 @@
Thm.prop_of (Thm.beta_conversion true ctrm)
|> pretty_term ctxt
|> pwriteln
-end"
-"(\<lambda>x y. x + y) 2 10 \<equiv> 2 + 10"}
+end\<close>
+\<open>(\<lambda>x y. x + y) 2 10 \<equiv> 2 + 10\<close>}
The argument @{ML true} in @{ML beta_conversion in Thm} indicates that
the right-hand side should be fully beta-normalised. If instead
@@ -2147,12 +2147,12 @@
to @{term "Foo \<longrightarrow> Bar"}. The code is as follows.
@{ML_matchresult_fake [display,gray]
-"let
- val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
+\<open>let
+ val ctrm = @{cterm "True \<and> (Foo \<longrightarrow> Bar)"}
in
Conv.rewr_conv @{thm true_conj1} ctrm
-end"
- "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
+end\<close>
+ \<open>True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar\<close>}
Note, however, that the function @{ML_ind rewr_conv in Conv} only rewrites the
outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match
@@ -2166,14 +2166,14 @@
which applies one conversion after another. For example
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv1 = Thm.beta_conversion false
val conv2 = Conv.rewr_conv @{thm true_conj1}
- val ctrm = Thm.apply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}
+ val ctrm = Thm.apply @{cterm "\<lambda>x. x \<and> False"} @{cterm "True"}
in
(conv1 then_conv conv2) ctrm
-end"
- "(\<lambda>x. x \<and> False) True \<equiv> False"}
+end\<close>
+ \<open>(\<lambda>x. x \<and> False) True \<equiv> False\<close>}
where we first beta-reduce the term and then rewrite according to
@{thm [source] true_conj1}. (When running this example recall the
@@ -2183,14 +2183,14 @@
first one, and if it does not apply, tries the second. For example
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
- val ctrm1 = @{cterm \"True \<and> Q\"}
- val ctrm2 = @{cterm \"P \<or> (True \<and> Q)\"}
+ val ctrm1 = @{cterm "True \<and> Q"}
+ val ctrm2 = @{cterm "P \<or> (True \<and> Q)"}
in
(conv ctrm1, conv ctrm2)
-end"
-"(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
+end\<close>
+\<open>(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)\<close>}
Here the conversion @{thm [source] true_conj1} only applies
in the first case, but fails in the second. The whole conversion
@@ -2200,13 +2200,13 @@
For example
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
- val ctrm = @{cterm \"True \<or> P\"}
+ val ctrm = @{cterm "True \<or> P"}
in
conv ctrm
-end"
- "True \<or> P \<equiv> True \<or> P"}
+end\<close>
+ \<open>True \<or> P \<equiv> True \<or> P\<close>}
Rewriting with more than one theorem can be done using the function
@{ML_ind rewrs_conv in Conv} from the structure @{ML_structure Conv}.
@@ -2221,13 +2221,13 @@
For example
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv = Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})
- val ctrm = @{cterm \"P \<or> (True \<and> Q)\"}
+ val ctrm = @{cterm "P \<or> (True \<and> Q)"}
in
conv ctrm
-end"
-"P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
+end\<close>
+\<open>P \<or> (True \<and> Q) \<equiv> P \<or> Q\<close>}
The reason for this behaviour is that \<open>(op \<or>)\<close> expects two
arguments. Therefore the term must be of the form \<open>(Const \<dots> $ t1) $ t2\<close>. The
@@ -2239,13 +2239,13 @@
abstraction. For example:
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv = Conv.rewr_conv @{thm true_conj1}
- val ctrm = @{cterm \"\<lambda>P. True \<and> (P \<and> Foo)\"}
+ val ctrm = @{cterm "\<lambda>P. True \<and> (P \<and> Foo)"}
in
Conv.abs_conv (K conv) @{context} ctrm
-end"
- "\<lambda>P. True \<and> (P \<and> Foo) \<equiv> \<lambda>P. P \<and> Foo"}
+end\<close>
+ \<open>\<lambda>P. True \<and> (P \<and> Foo) \<equiv> \<lambda>P. P \<and> Foo\<close>}
Note that this conversion needs a context as an argument. We also give the
conversion as \<open>(K conv)\<close>, which is a function that ignores its
@@ -2280,13 +2280,13 @@
conversion in action, consider the following example:
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv = true_conj1_conv @{context}
- val ctrm = @{cterm \"distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
+ val ctrm = @{cterm "distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x"}
in
conv ctrm
-end"
- "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
+end\<close>
+ \<open>distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x\<close>}
\<close>
text \<open>
@@ -2323,17 +2323,17 @@
two results are calculated.
@{ML_matchresult_fake [display, gray]
- "let
+ \<open>let
val ctxt = @{context}
val conv = Conv.try_conv (Conv.rewrs_conv @{thms conj_assoc})
val conv_top = Conv.top_conv (K conv) ctxt
val conv_bot = Conv.bottom_conv (K conv) ctxt
- val ctrm = @{cterm \"(a \<and> (b \<and> c)) \<and> d\"}
+ val ctrm = @{cterm "(a \<and> (b \<and> c)) \<and> d"}
in
(conv_top ctrm, conv_bot ctrm)
-end"
- "(\"(a \<and> (b \<and> c)) \<and> d \<equiv> a \<and> (b \<and> (c \<and> d))\",
- \"(a \<and> (b \<and> c)) \<and> d \<equiv> (a \<and> b) \<and> (c \<and> d)\")"}
+end\<close>
+ \<open>("(a \<and> (b \<and> c)) \<and> d \<equiv> a \<and> (b \<and> (c \<and> d))",
+ "(a \<and> (b \<and> c)) \<and> d \<equiv> (a \<and> b) \<and> (c \<and> d)")\<close>}
To see how much control you have over rewriting with conversions, let us
make the task a bit more complicated by rewriting according to the rule
@@ -2359,14 +2359,14 @@
@{ML_matchresult_fake [display,gray]
-"let
- val ctrm = @{cterm \"if P (True \<and> 1 \<noteq> (2::nat))
- then True \<and> True else True \<and> False\"}
+\<open>let
+ val ctrm = @{cterm "if P (True \<and> 1 \<noteq> (2::nat))
+ then True \<and> True else True \<and> False"}
in
if_true1_conv @{context} ctrm
-end"
-"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False
-\<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
+end\<close>
+\<open>if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False
+\<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False\<close>}
\<close>
text \<open>
@@ -2383,13 +2383,13 @@
new theorem as follows
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv = Conv.fconv_rule (true_conj1_conv @{context})
val thm = @{thm foo_test}
in
conv thm
-end"
- "?P \<or> \<not> ?P"}
+end\<close>
+ \<open>?P \<or> \<not> ?P\<close>}
Finally, Isabelle provides function @{ML_ind CONVERSION in Tactical}
for turning conversions into tactics. This needs some predefined conversion
@@ -2420,7 +2420,7 @@
Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)\<close>
text \<open>
- We call the conversions with the argument @{ML "~1"}. By this we
+ We call the conversions with the argument @{ML \<open>~1\<close>}. By this we
analyse all parameters, all premises and the conclusion of a goal
state. If we call @{ML concl_conv in Conv} with
a non-negative number, say \<open>n\<close>, then this conversions will
@@ -2466,8 +2466,8 @@
left-hand side in the right-hand side.
@{ML_matchresult_fake [display,gray]
- "Drule.abs_def @{thm id1_def}"
- "id1 \<equiv> \<lambda>x. x"}
+ \<open>Drule.abs_def @{thm id1_def}\<close>
+ \<open>id1 \<equiv> \<lambda>x. x\<close>}
Unfortunately, Isabelle has no built-in function that transforms the
theorems in the other direction. We can implement one using
@@ -2514,8 +2514,8 @@
produce meta-variables for the theorem. An example is as follows.
@{ML_matchresult_fake [display, gray]
- "unabs_def @{context} @{thm id2_def}"
- "id2 ?x1 \<equiv> ?x1"}
+ \<open>unabs_def @{context} @{thm id2_def}\<close>
+ \<open>id2 ?x1 \<equiv> ?x1\<close>}
\<close>
text \<open>