--- a/ProgTutorial/Tactical.thy Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/Tactical.thy Tue May 21 14:37:39 2019 +0200
@@ -47,7 +47,7 @@
text \<open>
This proof translates to the following ML-code.
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
\<open>let
val ctxt = @{context}
val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
@@ -763,17 +763,19 @@
constraints is by pre-instantiating theorems with other theorems.
The function @{ML_ind RS in Drule}, for example, does this.
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<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]
+ @{ML_response [display,gray]
\<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>}
+\<open>exception THM 1 raised\<dots>
+ RSN: no unifiers
+ \<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q
+ \<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\<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
@@ -782,7 +784,7 @@
If you want to instantiate more than one premise of a theorem, you can use
the function @{ML_ind MRS in Drule}:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}\<close>
\<open>\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)\<close>}
@@ -791,17 +793,17 @@
example in the code below, every theorem in the second list is
instantiated with every theorem in the first.
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val list1 = [@{thm impI}, @{thm disjI2}]
val list2 = [@{thm conjI}, @{thm disjI1}]
in
list1 RL list2
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]\<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"]\<close>}
\begin{readmore}
The combinators for instantiating theorems with other theorems are
@@ -1458,7 +1460,7 @@
prints out some parts of a simpset. If you use it to print out the components of the
empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier}
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>print_ss @{context} empty_ss\<close>
\<open>Simplification rules:
Congruences rules:
@@ -1474,10 +1476,10 @@
text \<open>
Printing then out the components of the simpset gives:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>print_ss @{context} (Raw_Simplifier.simpset_of ss1)\<close>
\<open>Simplification rules:
- ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
+ ??.unknown: A1 - B1 \<inter> C1 \<equiv> A1 - B1 \<union> (A1 - C1)
Congruences rules:
Simproc patterns:\<close>}
@@ -1491,12 +1493,12 @@
text \<open>
gives
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>print_ss @{context} (Raw_Simplifier.simpset_of ss2)\<close>
\<open>Simplification rules:
- ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
+ ??.unknown: A1 - B1 \<inter> C1 \<equiv> A1 - B1 \<union> (A1 - C1)
Congruences rules:
- Complete_Lattices.Inf_class.INFIMUM:
+ Complete_Lattices.Inf_class.Inf:
\<lbrakk>A1 = B1; \<And>x. x \<in> B1 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1
Simproc patterns:\<close>}
@@ -1508,7 +1510,7 @@
In the context of HOL, the first really useful simpset is @{ML_ind
HOL_basic_ss in Simpdata}. While printing out the components of this simpset
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>print_ss @{context} HOL_basic_ss\<close>
\<open>Simplification rules:
Congruences rules:
@@ -1534,6 +1536,7 @@
apply(tactic \<open>ALLGOALS (simp_tac (put_simpset HOL_basic_ss @{context}))\<close>)
done
+declare [[ML_print_depth = 200]]
text \<open>
This behaviour is not because of simplification rules, but how the subgoaler, solver
and looper are set up in @{ML HOL_basic_ss}.
@@ -1542,17 +1545,17 @@
already many useful simplification and congruence rules for the logical
connectives in HOL.
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<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
+ HOL.the_sym_eq_trivial: THE y. y = y \<equiv> y
\<dots>
Congruences rules:
HOL.simp_implies: \<dots>
\<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'
+ HOL.implies: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
Simproc patterns:
\<dots>\<close>}
@@ -2064,16 +2067,16 @@
is the function @{ML_ind all_conv in Conv}, which maps a @{ML_type cterm} to an
instance of the (meta)reflexivity theorem. For example:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<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]
+ @{ML_response [display,gray]
\<open>Conv.no_conv @{cterm True}\<close>
- \<open>*** Exception- CTERM ("no conversion", []) raised\<close>}
+ \<open>exception CTERM \<dots>: no conversion\<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
@@ -2111,7 +2114,7 @@
or in the pretty-printed form
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val add = @{cterm "\<lambda>x y. x + (y::nat)"}
val two = @{cterm "2::nat"}
@@ -2146,7 +2149,7 @@
It can be used for example to rewrite @{term "True \<and> (Foo \<longrightarrow> Bar)"}
to @{term "Foo \<longrightarrow> Bar"}. The code is as follows.
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val ctrm = @{cterm "True \<and> (Foo \<longrightarrow> Bar)"}
in
@@ -2182,7 +2185,7 @@
The conversion combinator @{ML_ind else_conv in Conv} tries out the
first one, and if it does not apply, tries the second. For example
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
val ctrm1 = @{cterm "True \<and> Q"}
@@ -2190,7 +2193,7 @@
in
(conv ctrm1, conv ctrm2)
end\<close>
-\<open>(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)\<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
@@ -2199,7 +2202,7 @@
behaviour can also be achieved with conversion combinator @{ML_ind try_conv in Conv}.
For example
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
val ctrm = @{cterm "True \<or> P"}
@@ -2220,14 +2223,14 @@
a conversion to the first, respectively second, argument of an application.
For example
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val conv = Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})
val ctrm = @{cterm "P \<or> (True \<and> Q)"}
in
conv ctrm
end\<close>
-\<open>P \<or> (True \<and> Q) \<equiv> P \<or> Q\<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
@@ -2238,14 +2241,14 @@
The function @{ML_ind abs_conv in Conv} applies a conversion under an
abstraction. For example:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val conv = Conv.rewr_conv @{thm true_conj1}
val ctrm = @{cterm "\<lambda>P. True \<and> (P \<and> Foo)"}
in
Conv.abs_conv (K conv) @{context} ctrm
end\<close>
- \<open>\<lambda>P. True \<and> (P \<and> Foo) \<equiv> \<lambda>P. P \<and> Foo\<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
@@ -2279,7 +2282,7 @@
to be able to pattern-match the term. To see this
conversion in action, consider the following example:
-@{ML_matchresult_fake [display,gray]
+@{ML_response [display,gray]
\<open>let
val conv = true_conj1_conv @{context}
val ctrm = @{cterm "distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x"}
@@ -2358,7 +2361,7 @@
soon as it found one redex. Here is an example for this conversion:
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val ctrm = @{cterm "if P (True \<and> 1 \<noteq> (2::nat))
then True \<and> True else True \<and> False"}
@@ -2382,7 +2385,7 @@
Using the conversion you can transform this theorem into a
new theorem as follows
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>let
val conv = Conv.fconv_rule (true_conj1_conv @{context})
val thm = @{thm foo_test}
@@ -2465,7 +2468,7 @@
into @{thm [source] id2_def} by abstracting all variables on the
left-hand side in the right-hand side.
- @{ML_matchresult_fake [display,gray]
+ @{ML_response [display,gray]
\<open>Drule.abs_def @{thm id1_def}\<close>
\<open>id1 \<equiv> \<lambda>x. x\<close>}
@@ -2513,7 +2516,7 @@
export the context \<open>ctxt'\<close> back to \<open>ctxt\<close> in order to
produce meta-variables for the theorem. An example is as follows.
- @{ML_matchresult_fake [display, gray]
+ @{ML_response [display, gray]
\<open>unabs_def @{context} @{thm id2_def}\<close>
\<open>id2 ?x1 \<equiv> ?x1\<close>}
\<close>