--- a/ProgTutorial/Tactical.thy Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Tactical.thy Thu May 16 19:56:12 2019 +0200
@@ -47,7 +47,7 @@
text \<open>
This proof translates to the following ML-code.
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
"let
val ctxt = @{context}
val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
@@ -396,7 +396,7 @@
text \<open>
A simple tactic for easy discharge of any proof obligations, even difficult ones, is
- @{ML_ind cheat_tac in Skip_Proof} in the structure @{ML_struct Skip_Proof}.
+ @{ML_ind cheat_tac in Skip_Proof} in the structure @{ML_structure Skip_Proof}.
This tactic corresponds to the Isabelle command \isacommand{sorry} and is
sometimes useful during the development of tactics.
\<close>
@@ -763,14 +763,14 @@
constraints is by pre-instantiating theorems with other theorems.
The function @{ML_ind RS in Drule}, for example, does this.
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
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_response_fake_both [display,gray]
+ @{ML_matchresult_fake_both [display,gray]
"@{thm conjI} RS @{thm mp}"
"*** Exception- THM (\"RSN: no unifiers\", 1,
[\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
@@ -782,7 +782,7 @@
If you want to instantiate more than one premise of a theorem, you can use
the function @{ML_ind MRS in Drule}:
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}"
"\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"}
@@ -791,7 +791,7 @@
example in the code below, every theorem in the second list is
instantiated with every theorem in the first.
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"let
val list1 = [@{thm impI}, @{thm disjI2}]
val list2 = [@{thm conjI}, @{thm disjI1}]
@@ -1293,7 +1293,7 @@
tactic should explore all possibilites of applying these rules to a
propositional formula until a goal state is reached in which all subgoals
are discharged. For this you can use the tactic combinator @{ML_ind
- DEPTH_SOLVE in Search} in the structure @{ML_struct Search}.
+ DEPTH_SOLVE in Search} in the structure @{ML_structure Search}.
\end{exercise}
\begin{exercise}
@@ -1359,7 +1359,7 @@
it can only deal with rewriting rules whose left-hand sides are higher order
pattern (see Section \ref{sec:univ} on unification). Whether a term is a pattern
or not can be tested with the function @{ML_ind pattern in Pattern} from
- the structure @{ML_struct Pattern}. If a rule is not a pattern and you want
+ the structure @{ML_structure Pattern}. If a rule is not a pattern and you want
to use it for rewriting, then you have to use simprocs or conversions, both
of which we shall describe in the next section.
@@ -1458,7 +1458,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_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"print_ss @{context} empty_ss"
"Simplification rules:
Congruences rules:
@@ -1474,7 +1474,7 @@
text \<open>
Printing then out the components of the simpset gives:
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"print_ss @{context} (Raw_Simplifier.simpset_of ss1)"
"Simplification rules:
??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
@@ -1491,7 +1491,7 @@
text \<open>
gives
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"print_ss @{context} (Raw_Simplifier.simpset_of ss2)"
"Simplification rules:
??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
@@ -1508,7 +1508,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_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"print_ss @{context} HOL_basic_ss"
"Simplification rules:
Congruences rules:
@@ -1542,7 +1542,7 @@
already many useful simplification and congruence rules for the logical
connectives in HOL.
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"print_ss @{context} HOL_ss"
"Simplification rules:
Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V
@@ -2064,21 +2064,21 @@
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_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
"Foo \<or> Bar \<equiv> Foo \<or> Bar"}
Another simple conversion is @{ML_ind no_conv in Conv} which always raises the
exception @{ML CTERM}.
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"Conv.no_conv @{cterm True}"
"*** Exception- CTERM (\"no conversion\", []) raised"}
A more interesting conversion is the function @{ML_ind beta_conversion in Thm}: it
produces a meta-equation between a term and its beta-normal form. For example
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"let
val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
val two = @{cterm \"2::nat\"}
@@ -2096,7 +2096,7 @@
If we get hold of the ``raw'' representation of the produced theorem,
we obtain the expected result.
- @{ML_response [display,gray]
+ @{ML_matchresult [display,gray]
"let
val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
val two = @{cterm \"2::nat\"}
@@ -2111,7 +2111,7 @@
or in the pretty-printed form
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"let
val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
val two = @{cterm \"2::nat\"}
@@ -2146,7 +2146,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_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"let
val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
in
@@ -2165,7 +2165,7 @@
combinators. The simplest conversion combinator is @{ML_ind then_conv in Conv},
which applies one conversion after another. For example
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"let
val conv1 = Thm.beta_conversion false
val conv2 = Conv.rewr_conv @{thm true_conj1}
@@ -2182,7 +2182,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_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"let
val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
val ctrm1 = @{cterm \"True \<and> Q\"}
@@ -2199,7 +2199,7 @@
behaviour can also be achieved with conversion combinator @{ML_ind try_conv in Conv}.
For example
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"let
val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
val ctrm = @{cterm \"True \<or> P\"}
@@ -2209,7 +2209,7 @@
"True \<or> P \<equiv> True \<or> P"}
Rewriting with more than one theorem can be done using the function
- @{ML_ind rewrs_conv in Conv} from the structure @{ML_struct Conv}.
+ @{ML_ind rewrs_conv in Conv} from the structure @{ML_structure Conv}.
Apart from the function @{ML beta_conversion in Thm}, which is able to fully
@@ -2220,7 +2220,7 @@
a conversion to the first, respectively second, argument of an application.
For example
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"let
val conv = Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})
val ctrm = @{cterm \"P \<or> (True \<and> Q)\"}
@@ -2238,7 +2238,7 @@
The function @{ML_ind abs_conv in Conv} applies a conversion under an
abstraction. For example:
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"let
val conv = Conv.rewr_conv @{thm true_conj1}
val ctrm = @{cterm \"\<lambda>P. True \<and> (P \<and> Foo)\"}
@@ -2279,7 +2279,7 @@
to be able to pattern-match the term. To see this
conversion in action, consider the following example:
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
"let
val conv = true_conj1_conv @{context}
val ctrm = @{cterm \"distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
@@ -2322,7 +2322,7 @@
according to the two meta-equations produces two results. Below these
two results are calculated.
- @{ML_response_fake [display, gray]
+ @{ML_matchresult_fake [display, gray]
"let
val ctxt = @{context}
val conv = Conv.try_conv (Conv.rewrs_conv @{thms conj_assoc})
@@ -2358,7 +2358,7 @@
soon as it found one redex. Here is an example for this conversion:
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"let
val ctrm = @{cterm \"if P (True \<and> 1 \<noteq> (2::nat))
then True \<and> True else True \<and> False\"}
@@ -2382,7 +2382,7 @@
Using the conversion you can transform this theorem into a
new theorem as follows
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"let
val conv = Conv.fconv_rule (true_conj1_conv @{context})
val thm = @{thm foo_test}
@@ -2460,12 +2460,12 @@
Although both definitions define the same function, the theorems @{thm
[source] id1_def} and @{thm [source] id2_def} are different meta-equations. However it is
easy to transform one into the other. The function @{ML_ind abs_def
- in Drule} from the structure @{ML_struct Drule} can automatically transform
+ in Drule} from the structure @{ML_structure Drule} can automatically transform
theorem @{thm [source] id1_def}
into @{thm [source] id2_def} by abstracting all variables on the
left-hand side in the right-hand side.
- @{ML_response_fake [display,gray]
+ @{ML_matchresult_fake [display,gray]
"Drule.abs_def @{thm id1_def}"
"id1 \<equiv> \<lambda>x. x"}
@@ -2513,7 +2513,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_response_fake [display, gray]
+ @{ML_matchresult_fake [display, gray]
"unabs_def @{context} @{thm id2_def}"
"id2 ?x1 \<equiv> ?x1"}
\<close>