--- a/ProgTutorial/Essential.thy Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/Essential.thy Tue May 21 14:37:39 2019 +0200
@@ -45,6 +45,15 @@
| Abs of string * typ * term
| $ of term * term\<close>
+ML \<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)
+end\<close>
+
text \<open>
This datatype implements Church-style lambda-terms, where types are
explicitly recorded in variables, constants and abstractions. The
@@ -53,7 +62,7 @@
terms use the usual de Bruijn index mechanism for representing bound
variables. For example in
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>@{term "\<lambda>x y. x y"}\<close>
\<open>Abs ("x", "'a \<Rightarrow> 'b", Abs ("y", "'a", Bound 1 $ Bound 0))\<close>}
@@ -69,7 +78,7 @@
Be careful if you pretty-print terms. Consider pretty-printing the abstraction
term shown above:
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>@{term "\<lambda>x y. x y"}
|> pretty_term @{context}
|> pwriteln\<close>
@@ -79,7 +88,7 @@
tacitly eta-contracted the output. You obtain a similar result
with beta-redexes
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>let
val redex = @{term "(\<lambda>(x::int) (y::int). x)"}
val arg1 = @{term "1::int"}
@@ -97,7 +106,7 @@
value @{ML_ind show_abbrevs in Syntax}. For example
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>let
val redex = @{term "(\<lambda>(x::int) (y::int). x)"}
val arg1 = @{term "1::int"}
@@ -114,7 +123,7 @@
\emph{schematic} variables (term-constructor @{ML Var} and written with a
leading question mark). Consider the following two examples
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>let
val v1 = Var (("x", 3), @{typ bool})
val v2 = Var (("x1", 3), @{typ bool})
@@ -144,20 +153,20 @@
Constructing terms via antiquotations has the advantage that only typable
terms can be constructed. For example
- @{ML_matchresult_fake_both [display,gray]
+ @{ML_response [display,gray]
\<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]
+ @{ML_response [display,gray]
\<open>let
val omega = Free ("x", @{typ "nat \<Rightarrow> nat"}) $ Free ("x", @{typ nat})
in
pwriteln (pretty_term @{context} omega)
end\<close>
- \<open>x x\<close>}
+ "x x"}
Sometimes the internal representation of terms can be surprisingly different
from what you see at the user-level, because the layers of
@@ -204,7 +213,7 @@
As already seen above, types can be constructed using the antiquotation
\<open>@{typ _}\<close>. For example:
- @{ML_matchresult_fake [display,gray] \<open>@{typ "bool \<Rightarrow> nat"}\<close> \<open>bool \<Rightarrow> nat\<close>}
+ @{ML_response [display,gray] \<open>@{typ "bool \<Rightarrow> nat"}\<close> \<open>bool \<Rightarrow> nat\<close>}
The corresponding datatype is
\<close>
@@ -294,11 +303,11 @@
After that the types for booleans, lists and so on are printed out again
the standard Isabelle way.
- @{ML_matchresult_fake [display, gray]
- \<open>@{typ "bool"};
-@{typ "'a list"}\<close>
- \<open>"bool"
-"'a List.list"\<close>}
+ @{ML_response [display, gray]
+ \<open>(@{typ "bool"},
+@{typ "'a list"})\<close>
+ \<open>("bool",
+"'a list")\<close>}
\begin{readmore}
Types are described in detail in \isccite{sec:types}. Their
@@ -358,7 +367,7 @@
term list applied to the term. For example
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
\<open>let
val trm = @{term "P::bool \<Rightarrow> bool \<Rightarrow> bool"}
val args = [@{term "True"}, @{term "False"}]
@@ -366,19 +375,19 @@
list_comb (trm, args)
end\<close>
\<open>Free ("P", "bool \<Rightarrow> bool \<Rightarrow> bool")
- $ Const ("True", "bool") $ Const ("False", "bool")\<close>}
+ $ Const ("HOL.True", "bool") $ Const ("HOL.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]
+ @{ML_response [display,gray]
\<open>let
val x_nat = @{term "x::nat"}
val trm = @{term "(P::nat \<Rightarrow> bool) x"}
in
lambda x_nat trm
end\<close>
- \<open>Abs ("x", "Nat.nat", Free ("P", "bool \<Rightarrow> bool") $ Bound 0)\<close>}
+ \<open>Abs ("x", "nat", Free ("P", "nat \<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
@@ -387,7 +396,7 @@
is of the same type as the abstracted variable. If it is of different type,
as in
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val x_int = @{term "x::int"}
val trm = @{term "(P::nat \<Rightarrow> bool) x"}
@@ -406,7 +415,7 @@
"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by
@{term y}, and @{term x} by @{term True}.
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val sub1 = (@{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"}, @{term "y::nat \<Rightarrow> nat"})
val sub2 = (@{term "x::nat"}, @{term "True"})
@@ -414,12 +423,12 @@
in
subst_free [sub1, sub2] trm
end\<close>
- \<open>Free ("y", "nat \<Rightarrow> nat") $ Const ("True", "bool")\<close>}
+ \<open>Free ("y", "nat \<Rightarrow> nat") $ Const ("HOL.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]
+ @{ML_response [display, gray]
\<open>let
val sub = (@{term "(\<lambda>y::nat. y)"}, @{term "x::nat"})
val trm = @{term "(\<lambda>x::nat. x)"}
@@ -446,10 +455,10 @@
The function returns a pair consisting of the stripped off variables and
the body of the universal quantification. For example
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<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>}
+ Const ("HOL.eq",\<dots>) $ 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
@@ -466,7 +475,7 @@
bound variables. With the function @{ML subst_bounds}, you can replace these
loose @{ML_ind Bound in Term}s with the stripped off variables.
- @{ML_matchresult_fake [display, gray, linenos]
+ @{ML_response [display, gray, linenos]
\<open>let
val (vrs, trm) = strip_alls @{term "\<forall>x y. x = (y::bool)"}
in
@@ -488,20 +497,20 @@
the loose de Bruijn index is replaced by a unique free variable. For example
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val body = Bound 0 $ Free ("x", @{typ nat})
in
Term.dest_abs ("x", @{typ "nat \<Rightarrow> bool"}, body)
end\<close>
- \<open>("xa", Free ("xa", "Nat.nat \<Rightarrow> bool") $ Free ("x", "Nat.nat"))\<close>}
+ \<open>("xa", Free ("xa", "nat \<Rightarrow> bool") $ Free ("x", "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,
@{ML_ind incr_boundvars in Term}, increases by an integer the indices
of the loose bound variables in a term. In the code below
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
\<open>@{term "\<forall>x y z u. z = u"}
|> strip_alls
||> incr_boundvars 2
@@ -519,7 +528,7 @@
The second function, @{ML_ind loose_bvar1 in Text}, tests whether a term
contains a loose bound of a certain index. For example
- @{ML_matchresult_fake [gray,display]
+ @{ML_matchresult [gray,display]
\<open>let
val body = snd (strip_alls @{term "\<forall>x y. x = (y::bool)"})
in
@@ -534,7 +543,7 @@
HOLogic} constructs an equality out of two terms. The types needed in this
equality are calculated from the type of the arguments. For example
-@{ML_matchresult_fake [gray,display]
+@{ML_response [gray,display]
\<open>let
val eq = HOLogic.mk_eq (@{term "True"}, @{term "False"})
in
@@ -674,10 +683,10 @@
text \<open>
Here is an example:
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
\<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>}
+\<open>Const ("HOL.eq", "int \<Rightarrow> int \<Rightarrow> bool")
+ $ Free ("a", "int") $ Const ("Groups.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}
@@ -798,9 +807,9 @@
@{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
structure @{ML_structure Vartab}.
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>Vartab.dest tyenv_unif\<close>
- \<open>[(("'a", 0), (["HOL.type"], "?'b List.list")),
+ \<open>[(("'a", 0), (["HOL.type"], "?'b list")),
(("'b", 0), (["HOL.type"], "nat"))]\<close>}
\<close>
@@ -839,7 +848,7 @@
environment in the example this function prints out the more legible:
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>pretty_tyenv @{context} tyenv_unif\<close>
\<open>[?'a := ?'b list, ?'b := nat]\<close>}
@@ -877,15 +886,21 @@
Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0)
end\<close>
+declare[[show_sorts]]
+
text \<open>
To print out the result type environment we switch on the printing
of sort information by setting @{ML_ind show_sorts in Syntax} to
true. This allows us to inspect the typing environment.
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>pretty_tyenv @{context} tyenv\<close>
\<open>[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]\<close>}
-
+\<close>
+
+declare[[show_sorts=false]]
+
+text\<open>
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
type variable has been introduced the @{ML index}, originally being \<open>0\<close>,
@@ -899,7 +914,7 @@
\<open>?'b list * nat\<close> from the beginning of this section, and the
calculated type environment @{ML tyenv_unif}:
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>pretty_tyenv @{context} tyenv_unif\<close>
\<open>[?'a := ?'b list, ?'b := nat]\<close>}
@@ -911,9 +926,9 @@
performance reasons. To apply such a type environment to a type, say \<open>?'a *
?'b\<close>, you should use the function @{ML_ind norm_type in Envir}:
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>Envir.norm_type tyenv_unif @{typ_pat "?'a * ?'b"}\<close>
- \<open>nat list * nat\<close>}
+ \<open>nat list \<times> 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
@@ -931,7 +946,7 @@
text \<open>
Printing out the calculated matcher gives
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>pretty_tyenv @{context} tyenv_match\<close>
\<open>[?'a := bool list, ?'b := nat]\<close>}
@@ -939,9 +954,9 @@
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]
+ @{ML_response [display, gray]
\<open>Envir.subst_type tyenv_match @{typ_pat "?'a * ?'b"}\<close>
- \<open>bool list * nat\<close>}
+ \<open>bool list \<times> nat\<close>}
Be careful to observe the difference: always use
@{ML subst_type in Envir} for matchers and @{ML norm_type in Envir}
@@ -960,16 +975,16 @@
Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. If we apply
@{ML norm_type in Envir} to the type \<open>?'a * ?'b\<close> we obtain
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>Envir.norm_type tyenv_match' @{typ_pat "?'a * ?'b"}\<close>
- \<open>nat list * nat\<close>}
+ \<open>nat list \<times> 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]
+ @{ML_response [display, gray]
\<open>Envir.subst_type tyenv_unif @{typ_pat "?'a * ?'b"}\<close>
- \<open>?'b list * nat\<close>}
+ \<open>?'b list \<times> nat\<close>}
which does not solve the unification problem.
@@ -1023,7 +1038,7 @@
the type environment is empty and can be ignored. The
resulting term environment is
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>pretty_env @{context} fo_env\<close>
\<open>[?X := P, ?Y := \<lambda>a b. Q b a]\<close>}
@@ -1033,7 +1048,7 @@
unifiers). The function @{ML subst_term in Envir} expects a type environment,
which is set to empty in the example below, and a term environment.
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>let
val trm = @{term_pat "(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}
in
@@ -1050,7 +1065,7 @@
matching \<open>\<lambda>x. P x\<close> against the pattern \<open>\<lambda>y. ?X y\<close>. In this
case, first-order matching produces \<open>[?X := P]\<close>.
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>let
val fo_pat = @{term_pat "\<lambda>y. (?X::nat\<Rightarrow>bool) y"}
val trm = @{term "\<lambda>x. (P::nat\<Rightarrow>bool) x"}
@@ -1101,7 +1116,7 @@
and @{ML_ind unify in Pattern}, both implemented in the structure
@{ML_structure Pattern}. An example for higher-order pattern unification is
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<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)"}
@@ -1152,13 +1167,15 @@
We can print them out as follows.
- @{ML_matchresult_fake [display, gray]
- \<open>pretty_env @{context} (Envir.term_env un1);
-pretty_env @{context} (Envir.term_env un2);
-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]\<close>}
+ @{ML_response [display, gray]
+ \<open>pretty_env @{context} (Envir.term_env un1)\<close>
+ \<open>[?X := \<lambda>a. a, ?Y := f a]\<close>}
+ @{ML_response [display, gray]
+ \<open>pretty_env @{context} (Envir.term_env un2)\<close>
+ \<open>[?X := f, ?Y := a]\<close>}
+ @{ML_response [display, gray]
+ \<open>pretty_env @{context} (Envir.term_env un3)\<close>
+ \<open>[?X := \<lambda>b. f a]\<close>}
In case of failure the function @{ML_ind unifiers in Unify} does not raise
@@ -1181,9 +1198,9 @@
called. This function has a built-in bound, which can be accessed and
manipulated as a configuration value. For example
- @{ML_matchresult_fake [display,gray]
+ @{ML_matchresult [display,gray]
\<open>Config.get_global @{theory} (Unify.search_bound)\<close>
- \<open>Int 60\<close>}
+ \<open>60\<close>}
If this bound is reached during unification, Isabelle prints out the
warning message @{text [quotes] "Unification bound exceeded"} and
@@ -1266,7 +1283,7 @@
@{term "Q True"}.
- @{ML_matchresult_fake [gray,display,linenos]
+ @{ML_response [gray,display,linenos]
\<open>let
val pat = Logic.strip_imp_concl (Thm.prop_of @{thm spec})
val trm = @{term "Trueprop (Q True)"}
@@ -1361,9 +1378,9 @@
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]
+ @{ML_response [display,gray]
\<open>type_of (@{term "f::nat \<Rightarrow> bool"} $ @{term "x::int"})\<close>
- \<open>*** Exception- TYPE ("type_of: type mismatch in application" \<dots>\<close>}
+ \<open>exception TYPE raised \<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
@@ -1387,7 +1404,7 @@
complete type. The type inference can be invoked with the function
@{ML_ind check_term in Syntax}. An example is as follows:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val c = Const (@{const_name "plus"}, dummyT)
val o = @{term "1::nat"}
@@ -1395,8 +1412,8 @@
in
Syntax.check_term @{context} (c $ o $ v)
end\<close>
-\<open>Const ("HOL.plus_class.plus", "nat \<Rightarrow> nat \<Rightarrow> nat") $
- Const ("HOL.one_class.one", "nat") $ Free ("x", "nat")\<close>}
+\<open>Const ("Groups.plus_class.plus", "nat \<Rightarrow> nat \<Rightarrow> nat") $
+ Const ("Groups.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.
@@ -1432,26 +1449,26 @@
Certification is always relative to a context. For example you can
write:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<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]
+ @{ML_response [display,gray]
\<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]
+ @{ML_response [display,gray]
\<open>@{cterm "1 + True"}\<close>
- \<open>Type unification failed \<dots>\<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]
+@{ML_response [display,gray]
\<open>let
val natT = @{typ "nat"}
val zero = @{term "0::nat"}
@@ -1465,13 +1482,13 @@
you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on
the ML-level as follows:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>Thm.ctyp_of @{context} (@{typ nat} --> @{typ bool})\<close>
\<open>nat \<Rightarrow> bool\<close>}
or with the antiquotation:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>@{ctyp "nat \<Rightarrow> bool"}\<close>
\<open>nat \<Rightarrow> bool\<close>}
@@ -1479,14 +1496,14 @@
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]
+ @{ML_response [display,gray]
\<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]
+ @{ML_response [display,gray]
\<open>let
val chead = @{cterm "P::unit \<Rightarrow> nat \<Rightarrow> bool"}
val cargs = [@{cterm "()"}, @{cterm "3::nat"}]
@@ -1546,7 +1563,7 @@
If we print out the value of @{ML my_thm} then we see only the
final statement of the theorem.
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>pwriteln (pretty_thm @{context} my_thm)\<close>
\<open>\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t\<close>}
@@ -1725,14 +1742,14 @@
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]
+ @{ML_response [display,gray]
\<open>let
val eq = @{thm True_def}
in
(Thm.lhs_of eq, Thm.rhs_of eq)
- |> apply2 (Pretty.string_of o (pretty_cterm @{context}))
+ |> apply2 (YXML.content_of o Pretty.string_of o (pretty_cterm @{context}))
end\<close>
- \<open>(True, (\<lambda>x. x) = (\<lambda>x. x))\<close>}
+ \<open>("True", "(\<lambda>x. x) = (\<lambda>x. x)")\<close>}
Other function produce terms that can be pattern-matched.
Suppose the following two theorems.
@@ -1778,7 +1795,7 @@
this, we build the theorem @{term "True \<equiv> True"} (Line 1) and then
unfold the constant @{term "True"} according to its definition (Line 2).
- @{ML_matchresult_fake [display,gray,linenos]
+ @{ML_response [display,gray,linenos]
\<open>Thm.reflexive @{cterm "True"}
|> Simplifier.rewrite_rule @{context} [@{thm True_def}]
|> pretty_thm @{context}
@@ -1795,14 +1812,14 @@
@{ML_ind rulify in Object_Logic}
replaces all object connectives by equivalents in the meta logic. For example
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<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]
+ @{ML_response [display,gray]
\<open>let
val thm = @{thm foo_test1}
val meta_eq = Object_Logic.atomize @{context} (Thm.cprop_of thm)
@@ -1837,16 +1854,16 @@
text \<open>
This function produces for the theorem @{thm [source] list.induct}
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<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>}
+ \<open>"\<forall>P list. P [] \<longrightarrow> (\<forall>x1 x2. P x2 \<longrightarrow> P (x1 # x2)) \<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}
in the structure @{ML_structure Goal}. For example below we use this function
to prove the term @{term "P \<Longrightarrow> P"}.
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val trm = @{term "P \<Longrightarrow> P::bool"}
val tac = K (assume_tac @{context} 1)
@@ -1868,17 +1885,17 @@
\<close>
ML %grayML\<open>fun rep_goals i = replicate i @{prop "f x = f x"}
-fun rep_tacs i = replicate i (resolve_tac @{context} [@{thm refl}])
+fun rep_tacs ctxt i = replicate i (resolve_tac ctxt [@{thm refl}])
fun multi_test ctxt i =
Goal.prove_common ctxt NONE ["f", "x"] [] (rep_goals i)
- (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))\<close>
+ (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs ctxt i)) 1))\<close>
text \<open>
With them we can now produce three theorem instances of the
proposition.
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>multi_test @{context} 3\<close>
\<open>["?f ?x = ?f ?x", "?f ?x = ?f ?x", "?f ?x = ?f ?x"]\<close>}
@@ -1903,7 +1920,7 @@
purposes, or when explicit proof construction should be omitted due to performace
reasons. An example of this function is as follows:
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>Skip_Proof.make_thm @{theory} @{prop "True = False"}\<close>
\<open>True = False\<close>}
@@ -1919,16 +1936,16 @@
Thm}. Assume you prove the following lemma.
\<close>
-lemma foo_data:
+theorem foo_data:
shows "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
text \<open>
The auxiliary data of this lemma can be retrieved using the function
@{ML_ind get_tags in Thm}. So far the the auxiliary data of this lemma is
- @{ML_matchresult_fake [display,gray]
+ @{ML_matchresult [display,gray]
\<open>Thm.get_tags @{thm foo_data}\<close>
- \<open>[("name", "General.foo_data"), ("kind", "lemma")]\<close>}
+ \<open>[("name", "Essential.foo_data"), ("kind", "theorem")]\<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
@@ -1944,10 +1961,10 @@
text \<open>
The data of the theorem @{thm [source] foo_data'} is then as follows:
- @{ML_matchresult_fake [display,gray]
+ @{ML_matchresult [display,gray]
\<open>Thm.get_tags @{thm foo_data'}\<close>
- \<open>[("name", "General.foo_data'"), ("kind", "lemma"),
- ("case_names", "foo_case_one;foo_case_two")]\<close>}
+ \<open>[("name", "Essential.foo_data'"),
+ ("case_names", "foo_case_one;foo_case_two"), ("kind", "theorem")]\<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
@@ -2001,12 +2018,22 @@
ML %grayML\<open>fun pthms_of (PBody {thms, ...}) = map #2 thms
val get_names = (map Proofterm.thm_node_name) o pthms_of
-val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of\<close>
+val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of
+fun get_all_names thm =
+let
+ (*proof body with digest*)
+ val body = Proofterm.strip_thm (Thm.proof_body_of thm);
+ (*all theorems used in the graph of nested proofs*)
+in Proofterm.fold_body_thms
+ (fn {name, ...} => insert (op =) name) [body] []
+end\<close>
text \<open>
To see what their purpose is, consider the following three short proofs.
\<close>
-
+ML \<open>
+
+\<close>
lemma my_conjIa:
shows "A \<and> B \<Longrightarrow> A \<and> B"
apply(rule conjI)
@@ -2026,7 +2053,9 @@
apply(auto)
done
-
+ML "Proofterm.proofs"
+ML \<open>@{thm my_conjIa}
+ |> get_all_names\<close>
text \<open>
While the information about which theorems are used is obvious in
the first two proofs, it is not obvious in the third, because of the
@@ -2036,7 +2065,7 @@
extracting this information. Let us first extract the name of the
established theorem. This can be done with
- @{ML_matchresult_fake [display,gray]
+ @{ML_matchresult [display,gray]
\<open>@{thm my_conjIa}
|> Thm.proof_body_of
|> get_names\<close>
@@ -2048,61 +2077,44 @@
theorem. Notice that the first proof above references
three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1}
and @{thm [source] conjunct2}. We can obtain them by descending into the
- first level of the proof-tree, as follows.
-
- @{ML_matchresult_fake [display,gray]
+ proof-tree. The function @{ML get_all_names} recursively selects all names.
+
+ @{ML_response [display,gray]
\<open>@{thm my_conjIa}
- |> Thm.proof_body_of
- |> get_pbodies
- |> map get_names
- |> List.concat\<close>
- \<open>["HOL.conjunct2", "HOL.conjunct1", "HOL.conjI", "Pure.protectD",
- "Pure.protectI"]\<close>}
+ |> get_all_names |> sort string_ord\<close>
+ \<open>["", "HOL.All_def", "HOL.FalseE", "HOL.False_def", "HOL.TrueI", "HOL.True_def",
+ "HOL.True_or_False", "HOL.allI", "HOL.and_def", "HOL.conjI",
+ "HOL.conjunct1", "HOL.conjunct2", "HOL.disjE", "HOL.eqTrueE", "HOL.eqTrueI",
+ "HOL.ext", "HOL.fun_cong", "HOL.iffD1", "HOL.iffD2", "HOL.iffI",
+ "HOL.impI", "HOL.mp", "HOL.or_def", "HOL.refl", "HOL.rev_iffD1",
+ "HOL.rev_iffD2", "HOL.spec", "HOL.ssubst", "HOL.subst", "HOL.sym",
+ "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
- proof in Isabelle. Note also that applications of \<open>assumption\<close> do not
+ proof in Isabelle. The other theorems are the theorems used in the proofs of the theorems
+ @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
+
+ Note also that applications of \<open>assumption\<close> do not
count as a separate theorem, as you can see in the following code.
- @{ML_matchresult_fake [display,gray]
+ @{ML_matchresult [display,gray]
\<open>@{thm my_conjIb}
- |> Thm.proof_body_of
- |> get_pbodies
- |> map get_names
- |> List.concat\<close>
- \<open>["Pure.protectD", "Pure.protectI"]\<close>}
+ |> get_all_names |> sort string_ord\<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}
and @{thm [source] my_conjIb}, as can be seen by the theorems that
are returned for @{thm [source] my_conjIc}.
-
- @{ML_matchresult_fake [display,gray]
+
+ @{ML_response [display,gray]
\<open>@{thm my_conjIc}
- |> Thm.proof_body_of
- |> get_pbodies
- |> map get_names
- |> 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
- means we obtain the theorems that are used in order to prove
- @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
-
- @{ML_matchresult_fake [display, gray]
- \<open>@{thm my_conjIa}
- |> Thm.proof_body_of
- |> get_pbodies
- |> map get_pbodies
- |> (map o map) get_names
- |> List.concat
- |> List.concat
- |> duplicates (op=)\<close>
- \<open>["HOL.spec", "HOL.and_def", "HOL.mp", "HOL.impI", "Pure.protectD",
- "Pure.protectI"]\<close>}
+ |> get_all_names\<close>
+ \<open>["HOL.simp_thms_25", "Pure.conjunctionD1", "Pure.conjunctionD2", "Pure.conjunctionI",
+ "HOL.rev_mp", "HOL.exI", "HOL.allE", "HOL.exE",\<dots>]\<close>}
+
\begin{exercise}
Have a look at the theorems that are used when a lemma is ``proved''
@@ -2408,7 +2420,7 @@
text \<open>
then you can see it is added to the initially empty list.
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>MyThms.get @{context}\<close>
\<open>["True"]\<close>}
@@ -2422,7 +2434,7 @@
not need to be explicitly given. These three declarations will cause the
theorem list to be updated as:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>MyThms.get @{context}\<close>
\<open>["True", "Suc (Suc 0) = 2"]\<close>}
@@ -2435,7 +2447,7 @@
text \<open>After this, the theorem list is again:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>MyThms.get @{context}\<close>
\<open>["True"]\<close>}
@@ -2482,7 +2494,7 @@
\<close>
ML %grayML\<open>fun pprint prt = tracing (Pretty.string_of prt)\<close>
-
+ML %invisible\<open>val pprint = YXML.content_of o Pretty.string_of\<close>
text \<open>
The point of the pretty-printing infrastructure is to give hints about how to
layout text and let Isabelle do the actual layout. Let us first explain
@@ -2512,7 +2524,7 @@
We obtain the same if we just use the function @{ML pprint}.
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
\<open>pprint (Pretty.str test_str)\<close>
\<open>fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
@@ -2526,7 +2538,7 @@
list. To print this list of pretty types as a single string, we concatenate
them with the function @{ML_ind blk in Pretty} as follows:
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
\<open>let
val ptrs = map Pretty.str (space_explode " " test_str)
in
@@ -2542,7 +2554,7 @@
indentation of the printed string. You can increase the indentation
and obtain
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
\<open>let
val ptrs = map Pretty.str (space_explode " " test_str)
in
@@ -2557,7 +2569,7 @@
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]
+@{ML_response [display,gray]
\<open>let
val ptrs = map Pretty.str (space_explode " " test_str)
in
@@ -2572,7 +2584,7 @@
have the linebreaks handled properly, you can use the function
@{ML_ind commas in Pretty}. For example
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
\<open>let
val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
in
@@ -2590,7 +2602,7 @@
text \<open>
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
\<open>let
val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
in
@@ -2629,39 +2641,48 @@
can occur. We do the same after the @{text [quotes] "and"}. This gives you
for example
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
\<open>let
val ptrs1 = map (Pretty.str o string_of_int) (1 upto 22)
+in
+ pprint (Pretty.blk (0, and_list ptrs1))
+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\<close>}
+@{ML_response [display,gray]
+\<open>let
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\<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
+\<open>10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and
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]
+ @{ML_response [display,gray]
\<open>let
val a_and_b = [Pretty.str "a", Pretty.str "b"]
in
- pprint (Pretty.blk (0, a_and_b));
+ pprint (Pretty.blk (0, a_and_b))
+end\<close>
+\<open>ab\<close>}
+ @{ML_response [display,gray]
+ \<open>let
+ val a_and_b = [Pretty.str "a", Pretty.str "b"]
+in
pprint (Pretty.chunks a_and_b)
end\<close>
-\<open>ab
-a
+\<open>a
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]
+ @{ML_response [display,gray]
\<open>let
val pstrs = map (Pretty.str o string_of_int) (4 upto 10)
in
@@ -2681,7 +2702,7 @@
out the the terms produced by the the function @{ML de_bruijn} from
exercise~\ref{ex:debruijn} we obtain the following:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<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>