--- 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