Email Gateway (Aug 18 2022 at 19:38): Email Gateway (Aug 18 2022 at 19:38):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Alfio,
it works like this
lemma "(⋀x. P x) ≡ Trueprop (∀x. P x)"
apply (rule)
apply (rule allI)
apply (assumption)
apply (rule spec, assumption)
done
But I agree that there are some "strange" steps. Lets try to go through
the proof step by step (please correct me if I claim anything wrong in
the following ;)).
In Line 1 we apply "rule", which on its own (without arguments) uses a
default rule that is determined by the syntactic structure of the goal.
Since I was not able to find any rule that directly reduces a
meta-equality into two implications with
find_theorems "(?A ==> ?B) ==> (?B ==> ?A) ==> ?A == ?B"
but such a rule is obviously applied. This step is somewhat "magic" (I
guess it is part of the Isabelle/Isar/Pure framework).
Lines 2 and 3 are nothing special.
Line 4, applies spec directly followed by assumption (internally many
methods do not just return a single result, but in fact an (possibly)
infinite list of results (due to higher-order unification)). Thus, by
composing methods into a single apply step, we can "pick" the desired
result of such a sequence, more specifically, the above states "use the
first result of spec which is directly solvable by assumption". If such
a result does not exist, the composition returns an empty result
sequence (i.e., fails). If we do not compose these two steps, the first
element of the result sequence is taken. To this end, let as have a look
at "spec", which is
ALL x. ?P x ==> ?P ?x
with "rule spec" we try to unify the conclusion of the current goal with
the conclusion of spec, i.e,
P x with ?P ?x
one possible unifier is ?x = P x and ?P = (%x. x) (the identity
function), instantiating spec to
ALL x. (%x. x) x ==> (%x. x) (P x)
which is immediately beta-reduced to
ALL x. x ==> P x
and thus explains the result of applying just "rule spec" without
"assumption".
hope this helps
chris
Email Gateway (Aug 18 2022 at 19:38):From: Alfio Martini <alfio.martini@acm.org>
Thanks Christian,
This was a very instructive explanation! Besides, taking into account the
sequence
of apply steps I sent before, I have just read in the very good old
tutorial the following
statement:
"The methods drule spec and erule allE do precisely the same inference."
All the best!
Email Gateway (Aug 18 2022 at 19:38):From: Brian Huffman <huffman@in.tum.de>
You used a too-specific pattern with your theorem search. A term like
"?A ==> ?B" is parsed as "Trueprop ?A ==> Trueprop ?B", with ?A and ?B
of type "bool". Of course you want ?A and ?B to be parsed as type
"prop" here, so you need to add "PROP" tags to tell the parser what
you want:
find_theorems "(PROP ?A ==> PROP ?B) ==> (PROP ?B ==> PROP ?A) ==>
PROP ?A == PROP ?B"
found 1 theorem(s):
Pure.equal_intr_rule:
[| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |] ==> PROP ?phi
== PROP ?psi
If there is any "magic" it is in the parser, which magically inserts
"Trueprop" everywhere unless you tell it not to. ;)
Email Gateway (Aug 18 2022 at 19:38):From: Christian Sternagel <c-sterna@jaist.ac.jp>
On 05/11/2012 02:27 PM, Brian Huffman wrote:
On Fri, May 11, 2012 at 6:59 AM, Christian Sternagel
<c-sterna@jaist.ac.jp> wrote:Since I was not able to find any rule that directly reduces a meta-equality
into two implications withfind_theorems "(?A ==> ?B) ==> (?B ==> ?A) ==> ?A == ?B"
but such a rule is obviously applied. This step is somewhat "magic" (I guess
it is part of the Isabelle/Isar/Pure framework).You used a too-specific pattern with your theorem search. A term like
"?A ==> ?B" is parsed as "Trueprop ?A ==> Trueprop ?B", with ?A and ?B
of type "bool". Of course you want ?A and ?B to be parsed as type
"prop" here, so you need to add "PROP" tags to tell the parser what
you want:find_theorems "(PROP ?A ==> PROP ?B) ==> (PROP ?B ==> PROP ?A) ==>
PROP ?A == PROP ?B"found 1 theorem(s):
Pure.equal_intr_rule:
[| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |] ==> PROP ?phi
== PROP ?psiIf there is any "magic" it is in the parser, which magically inserts
"Trueprop" everywhere unless you tell it not to. ;)
Thanks, what a relief ;)
- Brian
Email Gateway (Aug 18 2022 at 19:38):From: Makarius <makarius@sketis.net>
BTW, src/HOL/HOL.thy subsubsection {* Atomizing meta-level connectives *}
has proper Isar proofs for these Pure-vs-HOL theorems. This reduces the
magic to some extent.
When showing such things in public I usually make the Trueprop explicit
like this:
notation Trueprop ("Tr")
or even:
notation Trueprop ("\<^bold>T\<^bold>r")
Makarius
Email Gateway (Aug 18 2022 at 20:06):From: Alfio Martini <alfio.martini@acm.org>
Dear Users,
Attached to this e-mail is an image of small theory where I adapt an
example of
Paulson, from the book "ML for the Working Programmer". I have two simple
doubts:
1) In the proof of the theorem, below in the file (and in the image), I use
recursion induction together
with "induct_tac" (as taught in the tutorial) and everything works as
expected. However, If I try to use
apply (induction b rule: NNF.induct) as suggested by the new tutorial from
Tobias
Nipkow (e.g., section 2.3, page 15) , I get the following error message:
ill-typed instantiation: b :; 'a.
Why this is so?
2) This is perhaps for Makarius: In the image one sees that I have a total
of 11 subgoals,
but only 10 are printed. I would expect to reach the eleventh subgoal by
scrolling down in the output
window, but it does not work like that.
Many thanks!
PS: Using Isabelle-2012-RC1-Windows
Working-Paulson-NNF-exercise.PNG
t1201201.thy
Email Gateway (Aug 18 2022 at 20:06):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Alfio,
Actually this is independent from the interface you use. The number of
subgoals that are printed is controlled by the configuration option
"goals_limit" (see isar-ref p. 143). You can set it like
declare [[goals_limit=20]]
when in theory mode (i.e., not inside a proof), or like
note [[goals_limit=20]]
when in proof mode. (I don't know if it is possible to set it in "prove"
mode however ;)).
hope this helps
chris
Email Gateway (Aug 18 2022 at 20:06):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Alfio,
"induct"/"induction" is not the same as "induct_tac" (all methods with a
"_tac" suffix are emulations for traditional tactics (as used in
apply-style proofs) and are considered "improper" by isar-ref p. 173.
One difference is that with traditional tactics case-analysis (case_tac)
and induction (induct_tac) is possible over meta-bound variables, for
"induct"/"induction" however, you need free variables (I guess in
reality the difference is more subtle, so please Isabelle-gurus, correct
me). Moreover your statement
theorem "∀b. ∀e. valbool b e = valbool (NNF b) e"
is a bit strange since by-default all variables are
(meta-)all-quantified after a successful proof. With proper methods you
can proof the statement as follows:
theorem "valbool b e = valbool (NNF b) e"
by (induction b rule: NNF.induct) auto
which is short for
theorem "valbool b e = valbool (NNF b) e"
apply (induction b rule: NNF.induct)
apply (auto)
done
The resulting thm is "valbool ?b ?e = valbool (NNF ?b) ?e" (note the
question marks which mark schematic variables, i.e., variables that can
be instantiated arbitrarily according to their type). Your original
version results in "ALL b e. valbool b e = valbool (NNF b) e" (which is
equivalent, but not so nice to use, since you cannot directly
instantiate it).
hope this helps
chris
Email Gateway (Aug 18 2022 at 20:06):From: Brian Huffman <huffman@in.tum.de>
I was about to suggest the same thing.
Another standard idiom is to use "fix" to introduce a new free
variable, which can then be used with "induct":
theorem "\<forall>b. \<forall>e. valbool b e = valbool (NNF b) e"
proof (rule allI)
fix b
show "\<forall>e. valbool b e = valbool (NNF b) e"
by (induction b rule:NNF.induct) auto
qed
(Note that simply "proof", which applies a default intro rule, would
also work in place of "proof (rule allI)".)
Email Gateway (Aug 18 2022 at 20:07):From: Alfio Martini <alfio.martini@acm.org>
Thank you Christian!
That was very helpful! Cheers
Email Gateway (Aug 18 2022 at 20:07):From: Lars Noschinski <noschinl@in.tum.de>
This should be "using [[goals_limit=20]]]" then.
-- Lars
Email Gateway (Aug 18 2022 at 20:07):From: Alfio Martini <alfio.martini@acm.org>
Dear Christian and Brian,
Many thanks for your reply. Some remarks below:
(all methods with a "_tac" suffix are emulations for traditional tactics
(as used in apply-style proofs) and are considered "improper" by >isar-ref
p. 173
I looked at section 9.2.3 in the reference manual and did not find
"induct_tac" in the list of improper proof methods. But assuming it
is, I think that the tutorial, for instance, Chapter 2, should be updated,
shouldn´t it?
Moreover your statement
theorem "∀b. ∀e. valbool b e = valbool (NNF b) e"
is a bit strange since by-default all variables are (meta-)all-quantified
after a successful proof. With proper methods you can proof the >statement
as follows:
theorem "valbool b e = valbool (NNF b) e"
by (induction b rule: NNF.induct) auto
Good point. However, whenever I am playing (training) with Isabelle,
I use toy problems like this. This means that I want Isabelle to
check the proof I made by hand, so my level of abstraction is
the set of rules of natural deduction. I usually play like this: first
an exploratory proof using procedural style and auto and then a
detailed step-by-step proof using the Isar language. I know
that free variables become logical variables (in the sense of Prolog)
and thus, operationally behave as if the were universally quantified and
can be used more directly by the simplifier.
But at the "playing level" I prefer to proceed like in a hand-made proof,
first stripping off all the quantifiers and then applying induction. In this
kind of exercise I can use this theorem further by applying rule allE and
so on. So, I assume that this kind of approach can be only done
with Isar and the fix command, as pointed out by Brian, which I usually
do.
Your original version results in "ALL b e. valbool b e = valbool (NNF >b)
e" (which is equivalent, but not so nice to use, since you cannot >directly
instantiate it).
I think I spoke about this above, but I would like to capture in a
precise way (in a theorem) this equivalence. Informally we
all know that they are. I often think about it. Do you know how
to write (in Isabelle) this "equivalence"?
All the Best!
On Tue, May 8, 2012 at 2:13 AM, Christian Sternagel <c-sterna@jaist.ac.jp>wrote:
Dear Alfio,
On 05/08/2012 01:03 PM, Alfio Martini wrote:
1) In the proof of the theorem, below in the file (and in the image), I
use
recursion induction together
with "induct_tac" (as taught in the tutorial) and everything works as
expected. However, If I try to useapply (induction b rule: NNF.induct) as suggested by the new tutorial from
Tobias
Nipkow (e.g., section 2.3, page 15) , I get the following error message:ill-typed instantiation: b :; 'a.
Why this is so?
"induct"/"induction" is not the same as "induct_tac" (all methods with a
"_tac" suffix are emulations for traditional tactics (as used in
apply-style proofs) and are considered "improper" by isar-ref p. 173. One
difference is that with traditional tactics case-analysis (case_tac) and
induction (induct_tac) is possible over meta-bound variables, for
"induct"/"induction" however, you need free variables (I guess in reality
the difference is more subtle, so please Isabelle-gurus, correct me).
Moreover your statementtheorem "∀b. ∀e. valbool b e = valbool (NNF b) e"
is a bit strange since by-default all variables are (meta-)all-quantified
after a successful proof. With proper methods you can proof the statement
as follows:theorem "valbool b e = valbool (NNF b) e"
by (induction b rule: NNF.induct) autowhich is short for
theorem "valbool b e = valbool (NNF b) e"
apply (induction b rule: NNF.induct)
apply (auto)
doneThe resulting thm is "valbool ?b ?e = valbool (NNF ?b) ?e" (note the
question marks which mark schematic variables, i.e., variables that can be
instantiated arbitrarily according to their type). Your original version
results in "ALL b e. valbool b e = valbool (NNF b) e" (which is equivalent,
but not so nice to use, since you cannot directly instantiate it).hope this helps
chris
Email Gateway (Aug 18 2022 at 20:07):From: Alfio Martini <alfio.martini@acm.org>
Dear Brian,
Thanks for your reply!
Another standard idiom is to use "fix" to introduce a new free
variable, which can then be used with "induct":
theorem "\<forall>b. \<forall>e. valbool b e = valbool (NNF b) e"
proof (rule allI)
fix b
show "\<forall>e. valbool b e = valbool (NNF b) e"
by (induction b rule:NNF.induct) auto
qed
That is the way I go about it when using Isar. So the question that
remains is: how to prove the theorem above (with all the (two)
quantifiers) using the procedural style (and without using induct_tac)?
All the Best!
On Tue, May 8, 2012 at 2:21 AM, Brian Huffman <huffman@in.tum.de> wrote:
On Tue, May 8, 2012 at 7:13 AM, Christian Sternagel
<c-sterna@jaist.ac.jp> wrote:Dear Alfio,
On 05/08/2012 01:03 PM, Alfio Martini wrote:
1) In the proof of the theorem, below in the file (and in the image), I
use
recursion induction together
with "induct_tac" (as taught in the tutorial) and everything works as
expected. However, If I try to useapply (induction b rule: NNF.induct) as suggested by the new tutorial
from
Tobias
Nipkow (e.g., section 2.3, page 15) , I get the following error message:ill-typed instantiation: b :; 'a.
Why this is so?
"induct"/"induction" is not the same as "induct_tac" (all methods with a
"_tac" suffix are emulations for traditional tactics (as used in
apply-style
proofs) and are considered "improper" by isar-ref p. 173. One difference
is
that with traditional tactics case-analysis (case_tac) and induction
(induct_tac) is possible over meta-bound variables, for
"induct"/"induction"
however, you need free variables (I guess in reality the difference is
more
subtle, so please Isabelle-gurus, correct me). Moreover your statementtheorem "∀b. ∀e. valbool b e = valbool (NNF b) e"
is a bit strange since by-default all variables are (meta-)all-quantified
after a successful proof. With proper methods you can proof the
statement as
follows:theorem "valbool b e = valbool (NNF b) e"
by (induction b rule: NNF.induct) autoI was about to suggest the same thing.
Another standard idiom is to use "fix" to introduce a new free
variable, which can then be used with "induct":theorem "\<forall>b. \<forall>e. valbool b e = valbool (NNF b) e"
proof (rule allI)
fix b
show "\<forall>e. valbool b e = valbool (NNF b) e"
by (induction b rule:NNF.induct) auto
qed(Note that simply "proof", which applies a default intro rule, would
also work in place of "proof (rule allI)".)
- Brian
Email Gateway (Aug 18 2022 at 20:07):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Right! Thanks! cheers chris
Email Gateway (Aug 18 2022 at 20:07):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Alfio,
Maybe the closest you get to this equivalence is
lemma "(⋀x. P x) ≡ Trueprop (∀x. P x)"
by (rule) (rule allI, assumption, rule spec)
which shows that meta-all-quantification is the same as
HOL-all-quantification. It is not possible to prove that schematic
variables are equivalent to meta-all-quantified variables inside the
logic. Also the need for the explicit Trueprop (which turns something of
type "bool" [the type of HOL formulas] into type "prop" [the type of
propositions in the general Isabelle framework]) in the above proof
hints that we are doing something non-standard (for lack of a better
expression).
To convince yourself that the equivalence is not only informal, the
theorems allI and spec should be enough.
just my 2 cents
chris
Email Gateway (Aug 18 2022 at 20:07):From: Lars Noschinski <noschinl@in.tum.de>
On 08.05.2012 21:40, Alfio Martini wrote:
I looked at section 9.2.3 in the reference manual and did not find
"induct_tac" in the list of improper proof methods. But assuming it
is, I think that the tutorial, for instance, Chapter 2, should be updated,
shouldn´t it?
This tutorial is a bit dated (but still very useful). I think Tobias
Nipkow is working on a newer version.
But at the "playing level" I prefer to proceed like in a hand-made proof,
first stripping off all the quantifiers and then applying induction. In this
kind of exercise I can use this theorem further by applying rule allE and
so on. So, I assume that this kind of approach can be only done
with Isar and the fix command, as pointed out by Brian, which I usually
do.
If you really want to do step-by-step application of natural deduction
rules, you might want to use the old-style rule_tac and erule_tac
methods, because they allow you to instantiate meta-quantified variable
(syntax is "rule_tac x=... in exI").
-- Lars
Email Gateway (Aug 18 2022 at 20:07):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
... both of which are definitely in the list of "harmful" proof methods of section 9.2.3.
It would seem to me that the use of tactic emulation proof methods (i.e. methods whose name end with "_tac") in one place and the warnings against their use in another place reflects more the inclinations of the respective authors of these documents than the date at which these were written.
Jasmin
Email Gateway (Aug 18 2022 at 20:08):From: Makarius <makarius@sketis.net>
It is probably both the inclination and the date.
Many years ago, Larry Paulson invented a very nice natural deduction rule
framework called Isabelle/Pure with one main composition principle called
"RS" (now visible in Isar as "rule" method or "OF" attribute). For
various technical reasons he also added erule/drule/frule variants, and
some means for explicit instantiations under a local quantifier
erule_tac/drule_tac/frule_tac.
10 years later I came up with a natural deduction proof framework called
Isabelle/Isar. It worked out just with the original Pure principles, the
add-on zoo was not required. The isar-ref manual explains this Pure style
of structured natural deduction in chapter 1 and 2.
Later I also re-integrated all the old stuff into the Isabelle/Isar
infrastructure, so that existing material could be converted to Isar
syntax in a superficial sense, without rewriting things deeply. Someone
(not me) invented the name "apply style" for this guest mode of
Isabelle/Isar. This is the class of "improper language elements" within
proper Isar turned out quite succesful, so that its guest status is
occasionally forgotten.
Concerning rule_tac in particular: it is already mostly obsolete in ML
because the FOCUS combinators address the the demand for working under
local quantifiers more directly. It is a re-use of Isar proof contexts
for ML tactic programming.
Makarius
Email Gateway (Aug 18 2022 at 20:08):From: Tobias Nipkow <nipkow@in.tum.de>
Not a newer version but a completely new and much more compact document
"Programming and Proving in Isabelle/HOL" which you can find for example at
http://isabelle.in.tum.de/website-Isabelle2012-RC2/documentation.html and in the
release in a few weeks. It minimizes "apply" and does not introduce *rule_tac
but structured proofs.
But, as Lars wrote, that tutorial is still useful, but I do not recommend it for
beginners anymore.
Tobias
Email Gateway (Aug 18 2022 at 20:08):From: Alfio Martini <alfio.martini@acm.org>
Dear Christian,
Thanks for your reply. The proposition below is simple and
precise enough for me. The use of allI was clear, but I was
not so sure about spec, to be honest.
Many thanks!
Email Gateway (Aug 18 2022 at 20:08):From: Alfio Martini <alfio.martini@acm.org>
Dear Christian,
I was a little puzzled by you "atomic" proof below
lemma "(⋀x. P x) ≡ Trueprop (∀x. P x)"
by (rule) (rule allI, assumption, rule spec)
and wanted to see the details myself. But using step-by-step apply commands
this was the only way I could solve the goal:
lemma "(⋀x. P x) ≡ Trueprop (∀x. P x)"
apply (rule)
apply (rule allI)
apply (assumption)
apply (rename_tac x0)
apply (erule allE)
apply (assumption)
done
That is to say, I had to use "allE" instead of "spec". The renaming above
was
included because I was a little confused by a scope of a specific arbitrary
variable.
best!
Last updated: Nov 21 2024 at 12:39 UTC