--- a/ProgTutorial/Tactical.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Tactical.thy Fri May 17 10:38:01 2019 +0200
@@ -48,17 +48,17 @@
This proof translates to the following ML-code.
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val ctxt = @{context}
- val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
+ val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
in
- Goal.prove ctxt [\"P\", \"Q\"] [] goal
+ Goal.prove ctxt ["P", "Q"] [] goal
(fn _ => eresolve_tac @{context} [@{thm disjE}] 1
THEN resolve_tac @{context} [@{thm disjI2}] 1
THEN assume_tac @{context} 1
THEN resolve_tac @{context} [@{thm disjI1}] 1
THEN assume_tac @{context} 1)
-end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
+end\<close> \<open>?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P\<close>}
To start the proof, the function @{ML_ind prove in Goal} sets up a goal
state for proving the goal @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. We can give this
@@ -764,16 +764,16 @@
The function @{ML_ind RS in Drule}, for example, does this.
@{ML_matchresult_fake [display,gray]
- "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
+ \<open>@{thm disjI1} RS @{thm conjI}\<close> \<open>\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q\<close>}
In this example it instantiates the first premise of the \<open>conjI\<close>-theorem
with the theorem \<open>disjI1\<close>. If the instantiation is impossible, as in the
case of
@{ML_matchresult_fake_both [display,gray]
- "@{thm conjI} RS @{thm mp}"
-"*** Exception- THM (\"RSN: no unifiers\", 1,
-[\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
+ \<open>@{thm conjI} RS @{thm mp}\<close>
+\<open>*** Exception- THM ("RSN: no unifiers", 1,
+["\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q", "\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q"]) raised\<close>}
then the function raises an exception. The function @{ML_ind RSN in Drule}
is similar to @{ML RS}, but takes an additional number as argument. This
@@ -783,8 +783,8 @@
the function @{ML_ind MRS in Drule}:
@{ML_matchresult_fake [display,gray]
- "[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}"
- "\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"}
+ \<open>[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}\<close>
+ \<open>\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)\<close>}
If you need to instantiate lists of theorems, you can use the
functions @{ML_ind RL in Drule} and @{ML_ind OF in Drule}. For
@@ -792,16 +792,16 @@
instantiated with every theorem in the first.
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val list1 = [@{thm impI}, @{thm disjI2}]
val list2 = [@{thm conjI}, @{thm disjI1}]
in
list1 RL list2
-end"
-"[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q,
+end\<close>
+\<open>[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q,
\<lbrakk>?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q,
(?P1 \<Longrightarrow> ?Q1) \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<or> ?Q,
- ?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]"}
+ ?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]\<close>}
\begin{readmore}
The combinators for instantiating theorems with other theorems are
@@ -981,7 +981,7 @@
There is even another way of implementing this tactic: in automatic proof
procedures (in contrast to tactics that might be called by the user) there
are often long lists of tactics that are applied to the first
- subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' @{context} 1"},
+ subgoal. Instead of writing the code above and then calling @{ML \<open>foo_tac'' @{context} 1\<close>},
you can also just write
\<close>
@@ -1097,7 +1097,7 @@
convention therefore, tactics visible to the user should either change
something or fail.
- To comply with this convention, we could simply delete the @{ML "K all_tac"}
+ To comply with this convention, we could simply delete the @{ML \<open>K all_tac\<close>}
in @{ML select_tac'} or delete @{ML TRY} from @{ML select_tac''}. But for
the sake of argument, let us suppose that this deletion is \emph{not} an
option. In such cases, you can use the combinator @{ML_ind CHANGED in
@@ -1459,10 +1459,10 @@
empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier}
@{ML_matchresult_fake [display,gray]
- "print_ss @{context} empty_ss"
-"Simplification rules:
+ \<open>print_ss @{context} empty_ss\<close>
+\<open>Simplification rules:
Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
you can see it contains nothing. This simpset is usually not useful, except as a
building block to build bigger simpsets. For example you can add to @{ML empty_ss}
@@ -1475,11 +1475,11 @@
Printing then out the components of the simpset gives:
@{ML_matchresult_fake [display,gray]
- "print_ss @{context} (Raw_Simplifier.simpset_of ss1)"
-"Simplification rules:
+ \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss1)\<close>
+\<open>Simplification rules:
??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
\footnote{\bf FIXME: Why does it print out ??.unknown}
@@ -1492,13 +1492,13 @@
gives
@{ML_matchresult_fake [display,gray]
- "print_ss @{context} (Raw_Simplifier.simpset_of ss2)"
-"Simplification rules:
+ \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss2)\<close>
+\<open>Simplification rules:
??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
Congruences rules:
Complete_Lattices.Inf_class.INFIMUM:
\<lbrakk>A1 = B1; \<And>x. x \<in> B1 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1
-Simproc patterns:"}
+Simproc patterns:\<close>}
Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss}
expects this form of the simplification and congruence rules. This is
@@ -1509,10 +1509,10 @@
HOL_basic_ss in Simpdata}. While printing out the components of this simpset
@{ML_matchresult_fake [display,gray]
- "print_ss @{context} HOL_basic_ss"
-"Simplification rules:
+ \<open>print_ss @{context} HOL_basic_ss\<close>
+\<open>Simplification rules:
Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
also produces ``nothing'', the printout is somewhat misleading. In fact
the @{ML HOL_basic_ss} is setup so that it can solve goals of the
@@ -1543,8 +1543,8 @@
connectives in HOL.
@{ML_matchresult_fake [display,gray]
- "print_ss @{context} HOL_ss"
-"Simplification rules:
+ \<open>print_ss @{context} HOL_ss\<close>
+\<open>Simplification rules:
Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V
HOL.the_eq_trivial: THE x. x = y \<equiv> y
HOL.the_sym_eq_trivial: THE ya. y = ya \<equiv> y
@@ -1554,7 +1554,7 @@
\<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')
op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
Simproc patterns:
- \<dots>"}
+ \<dots>\<close>}
\begin{readmore}
The simplifier for HOL is set up in @{ML_file "HOL/Tools/simpdata.ML"}.
@@ -1755,7 +1755,7 @@
(FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy)
- (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.)
+ (FIXME: explain @{ML simplify} and @{ML \<open>Simplifier.rewrite_rule\<close>} etc.)
\<close>
@@ -2065,29 +2065,29 @@
instance of the (meta)reflexivity theorem. For example:
@{ML_matchresult_fake [display,gray]
- "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
- "Foo \<or> Bar \<equiv> Foo \<or> Bar"}
+ \<open>Conv.all_conv @{cterm "Foo \<or> Bar"}\<close>
+ \<open>Foo \<or> Bar \<equiv> Foo \<or> Bar\<close>}
Another simple conversion is @{ML_ind no_conv in Conv} which always raises the
exception @{ML CTERM}.
@{ML_matchresult_fake [display,gray]
- "Conv.no_conv @{cterm True}"
- "*** Exception- CTERM (\"no conversion\", []) raised"}
+ \<open>Conv.no_conv @{cterm True}\<close>
+ \<open>*** Exception- CTERM ("no conversion", []) raised\<close>}
A more interesting conversion is the function @{ML_ind beta_conversion in Thm}: it
produces a meta-equation between a term and its beta-normal form. For example
@{ML_matchresult_fake [display,gray]
- "let
- val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
- val two = @{cterm \"2::nat\"}
- val ten = @{cterm \"10::nat\"}
+ \<open>let
+ val add = @{cterm "\<lambda>x y. x + (y::nat)"}
+ val two = @{cterm "2::nat"}
+ val ten = @{cterm "10::nat"}
val ctrm = Thm.apply (Thm.apply add two) ten
in
Thm.beta_conversion true ctrm
-end"
- "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
+end\<close>
+ \<open>((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10\<close>}
If you run this example, you will notice that the actual response is the
seemingly nonsensical @{term
@@ -2097,25 +2097,25 @@
we obtain the expected result.
@{ML_matchresult [display,gray]
-"let
- val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
- val two = @{cterm \"2::nat\"}
- val ten = @{cterm \"10::nat\"}
+\<open>let
+ val add = @{cterm "\<lambda>x y. x + (y::nat)"}
+ val two = @{cterm "2::nat"}
+ val ten = @{cterm "10::nat"}
val ctrm = Thm.apply (Thm.apply add two) ten
in
Thm.prop_of (Thm.beta_conversion true ctrm)
-end"
-"Const (\"Pure.eq\",_) $
- (Abs (\"x\",_,Abs (\"y\",_,_)) $_$_) $
- (Const (\"Groups.plus_class.plus\",_) $ _ $ _)"}
+end\<close>
+\<open>Const ("Pure.eq",_) $
+ (Abs ("x",_,Abs ("y",_,_)) $_$_) $
+ (Const ("Groups.plus_class.plus",_) $ _ $ _)\<close>}
or in the pretty-printed form
@{ML_matchresult_fake [display,gray]
-"let
- val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
- val two = @{cterm \"2::nat\"}
- val ten = @{cterm \"10::nat\"}
+\<open>let
+ val add = @{cterm "\<lambda>x y. x + (y::nat)"}
+ val two = @{cterm "2::nat"}
+ val ten = @{cterm "10::nat"}
val ctrm = Thm.apply (Thm.apply add two) ten
val ctxt = @{context}
|> Config.put eta_contract false
@@ -2124,8 +2124,8 @@
Thm.prop_of (Thm.beta_conversion true ctrm)
|> pretty_term ctxt
|> pwriteln
-end"
-"(\<lambda>x y. x + y) 2 10 \<equiv> 2 + 10"}
+end\<close>
+\<open>(\<lambda>x y. x + y) 2 10 \<equiv> 2 + 10\<close>}
The argument @{ML true} in @{ML beta_conversion in Thm} indicates that
the right-hand side should be fully beta-normalised. If instead
@@ -2147,12 +2147,12 @@
to @{term "Foo \<longrightarrow> Bar"}. The code is as follows.
@{ML_matchresult_fake [display,gray]
-"let
- val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
+\<open>let
+ val ctrm = @{cterm "True \<and> (Foo \<longrightarrow> Bar)"}
in
Conv.rewr_conv @{thm true_conj1} ctrm
-end"
- "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
+end\<close>
+ \<open>True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar\<close>}
Note, however, that the function @{ML_ind rewr_conv in Conv} only rewrites the
outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match
@@ -2166,14 +2166,14 @@
which applies one conversion after another. For example
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv1 = Thm.beta_conversion false
val conv2 = Conv.rewr_conv @{thm true_conj1}
- val ctrm = Thm.apply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}
+ val ctrm = Thm.apply @{cterm "\<lambda>x. x \<and> False"} @{cterm "True"}
in
(conv1 then_conv conv2) ctrm
-end"
- "(\<lambda>x. x \<and> False) True \<equiv> False"}
+end\<close>
+ \<open>(\<lambda>x. x \<and> False) True \<equiv> False\<close>}
where we first beta-reduce the term and then rewrite according to
@{thm [source] true_conj1}. (When running this example recall the
@@ -2183,14 +2183,14 @@
first one, and if it does not apply, tries the second. For example
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
- val ctrm1 = @{cterm \"True \<and> Q\"}
- val ctrm2 = @{cterm \"P \<or> (True \<and> Q)\"}
+ val ctrm1 = @{cterm "True \<and> Q"}
+ val ctrm2 = @{cterm "P \<or> (True \<and> Q)"}
in
(conv ctrm1, conv ctrm2)
-end"
-"(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
+end\<close>
+\<open>(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)\<close>}
Here the conversion @{thm [source] true_conj1} only applies
in the first case, but fails in the second. The whole conversion
@@ -2200,13 +2200,13 @@
For example
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
- val ctrm = @{cterm \"True \<or> P\"}
+ val ctrm = @{cterm "True \<or> P"}
in
conv ctrm
-end"
- "True \<or> P \<equiv> True \<or> P"}
+end\<close>
+ \<open>True \<or> P \<equiv> True \<or> P\<close>}
Rewriting with more than one theorem can be done using the function
@{ML_ind rewrs_conv in Conv} from the structure @{ML_structure Conv}.
@@ -2221,13 +2221,13 @@
For example
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv = Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})
- val ctrm = @{cterm \"P \<or> (True \<and> Q)\"}
+ val ctrm = @{cterm "P \<or> (True \<and> Q)"}
in
conv ctrm
-end"
-"P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
+end\<close>
+\<open>P \<or> (True \<and> Q) \<equiv> P \<or> Q\<close>}
The reason for this behaviour is that \<open>(op \<or>)\<close> expects two
arguments. Therefore the term must be of the form \<open>(Const \<dots> $ t1) $ t2\<close>. The
@@ -2239,13 +2239,13 @@
abstraction. For example:
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv = Conv.rewr_conv @{thm true_conj1}
- val ctrm = @{cterm \"\<lambda>P. True \<and> (P \<and> Foo)\"}
+ val ctrm = @{cterm "\<lambda>P. True \<and> (P \<and> Foo)"}
in
Conv.abs_conv (K conv) @{context} ctrm
-end"
- "\<lambda>P. True \<and> (P \<and> Foo) \<equiv> \<lambda>P. P \<and> Foo"}
+end\<close>
+ \<open>\<lambda>P. True \<and> (P \<and> Foo) \<equiv> \<lambda>P. P \<and> Foo\<close>}
Note that this conversion needs a context as an argument. We also give the
conversion as \<open>(K conv)\<close>, which is a function that ignores its
@@ -2280,13 +2280,13 @@
conversion in action, consider the following example:
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv = true_conj1_conv @{context}
- val ctrm = @{cterm \"distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
+ val ctrm = @{cterm "distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x"}
in
conv ctrm
-end"
- "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
+end\<close>
+ \<open>distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x\<close>}
\<close>
text \<open>
@@ -2323,17 +2323,17 @@
two results are calculated.
@{ML_matchresult_fake [display, gray]
- "let
+ \<open>let
val ctxt = @{context}
val conv = Conv.try_conv (Conv.rewrs_conv @{thms conj_assoc})
val conv_top = Conv.top_conv (K conv) ctxt
val conv_bot = Conv.bottom_conv (K conv) ctxt
- val ctrm = @{cterm \"(a \<and> (b \<and> c)) \<and> d\"}
+ val ctrm = @{cterm "(a \<and> (b \<and> c)) \<and> d"}
in
(conv_top ctrm, conv_bot ctrm)
-end"
- "(\"(a \<and> (b \<and> c)) \<and> d \<equiv> a \<and> (b \<and> (c \<and> d))\",
- \"(a \<and> (b \<and> c)) \<and> d \<equiv> (a \<and> b) \<and> (c \<and> d)\")"}
+end\<close>
+ \<open>("(a \<and> (b \<and> c)) \<and> d \<equiv> a \<and> (b \<and> (c \<and> d))",
+ "(a \<and> (b \<and> c)) \<and> d \<equiv> (a \<and> b) \<and> (c \<and> d)")\<close>}
To see how much control you have over rewriting with conversions, let us
make the task a bit more complicated by rewriting according to the rule
@@ -2359,14 +2359,14 @@
@{ML_matchresult_fake [display,gray]
-"let
- val ctrm = @{cterm \"if P (True \<and> 1 \<noteq> (2::nat))
- then True \<and> True else True \<and> False\"}
+\<open>let
+ val ctrm = @{cterm "if P (True \<and> 1 \<noteq> (2::nat))
+ then True \<and> True else True \<and> False"}
in
if_true1_conv @{context} ctrm
-end"
-"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False
-\<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
+end\<close>
+\<open>if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False
+\<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False\<close>}
\<close>
text \<open>
@@ -2383,13 +2383,13 @@
new theorem as follows
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val conv = Conv.fconv_rule (true_conj1_conv @{context})
val thm = @{thm foo_test}
in
conv thm
-end"
- "?P \<or> \<not> ?P"}
+end\<close>
+ \<open>?P \<or> \<not> ?P\<close>}
Finally, Isabelle provides function @{ML_ind CONVERSION in Tactical}
for turning conversions into tactics. This needs some predefined conversion
@@ -2420,7 +2420,7 @@
Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)\<close>
text \<open>
- We call the conversions with the argument @{ML "~1"}. By this we
+ We call the conversions with the argument @{ML \<open>~1\<close>}. By this we
analyse all parameters, all premises and the conclusion of a goal
state. If we call @{ML concl_conv in Conv} with
a non-negative number, say \<open>n\<close>, then this conversions will
@@ -2466,8 +2466,8 @@
left-hand side in the right-hand side.
@{ML_matchresult_fake [display,gray]
- "Drule.abs_def @{thm id1_def}"
- "id1 \<equiv> \<lambda>x. x"}
+ \<open>Drule.abs_def @{thm id1_def}\<close>
+ \<open>id1 \<equiv> \<lambda>x. x\<close>}
Unfortunately, Isabelle has no built-in function that transforms the
theorems in the other direction. We can implement one using
@@ -2514,8 +2514,8 @@
produce meta-variables for the theorem. An example is as follows.
@{ML_matchresult_fake [display, gray]
- "unabs_def @{context} @{thm id2_def}"
- "id2 ?x1 \<equiv> ?x1"}
+ \<open>unabs_def @{context} @{thm id2_def}\<close>
+ \<open>id2 ?x1 \<equiv> ?x1\<close>}
\<close>
text \<open>